From a74f6b45d72834b5b8417297017bd81424123d98 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 7 Mar 2010 15:52:58 +0000 Subject: Merge of the newmem and newextcalls branches: - Revised memory model with concrete representation of ints & floats, and per-byte access permissions - Revised Globalenvs implementation - Matching changes in all languages and proofs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Stackingproof.v | 29 +++++++++++++++++++++-------- 1 file changed, 21 insertions(+), 8 deletions(-) (limited to 'backend/Stackingproof.v') diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index ba42958..f44eac2 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -27,7 +27,7 @@ Require Import AST. Require Import Integers. Require Import Values. Require Import Op. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -1145,7 +1145,7 @@ Lemma functions_translated: exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. Proof - (Genv.find_funct_transf_partial transf_fundef TRANSF). + (Genv.find_funct_transf_partial transf_fundef _ TRANSF). Lemma function_ptr_translated: forall v f, @@ -1153,7 +1153,7 @@ Lemma function_ptr_translated: exists tf, Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. Proof - (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF). + (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF). Lemma sig_preserved: forall f tf, transf_fundef f = OK tf -> Mach.funsig tf = Linear.funsig f. @@ -1166,6 +1166,15 @@ Proof. intro. inversion H. reflexivity. Qed. +Lemma stacksize_preserved: + forall f tf, transf_function f = OK tf -> Mach.fn_stacksize tf = Linear.fn_stacksize f. +Proof. + intros until tf; unfold transf_function. + destruct (zlt (Linear.fn_stacksize f) 0). simpl; congruence. + destruct (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))). simpl; congruence. + intros. inversion H; reflexivity. +Qed. + Lemma find_function_translated: forall f0 tf0 ls ls0 rs fr cs ros f, agree f0 tf0 ls ls0 rs fr cs -> @@ -1478,10 +1487,12 @@ Proof. simpl. intuition congruence. simpl. intuition congruence. econstructor; split. eapply plus_right. eexact A. - simpl shift_sp. eapply exec_Mtailcall; eauto. traceEq. + simpl shift_sp. eapply exec_Mtailcall; eauto. + rewrite (stacksize_preserved _ _ TRANSL); eauto. + traceEq. econstructor; eauto. intros; symmetry; eapply agree_return_regs; eauto. - intros. inv WTI. generalize (H3 _ H0). tauto. + intros. inv WTI. generalize (H4 _ H0). tauto. apply agree_callee_save_return_regs. (* Llabel *) @@ -1524,7 +1535,9 @@ Proof. intros [ls' [A [B C]]]. econstructor; split. eapply plus_right. eauto. - simpl shift_sp. econstructor; eauto. traceEq. + simpl shift_sp. econstructor; eauto. + rewrite (stacksize_preserved _ _ TRANSL); eauto. + traceEq. econstructor; eauto. intros. symmetry. eapply agree_return_regs; eauto. apply agree_callee_save_return_regs. @@ -1583,13 +1596,13 @@ Proof. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. econstructor; split. econstructor. + eapply Genv.init_mem_transf_partial; eauto. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. eauto. eauto. - rewrite (Genv.init_mem_transf_partial _ _ TRANSF). econstructor; eauto. constructor. eapply Genv.find_funct_ptr_prop; eauto. - intros. rewrite H2 in H4. simpl in H4. contradiction. + intros. rewrite H3 in H5. simpl in H5. contradiction. simpl; red; auto. Qed. -- cgit v1.2.3