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/Constpropproof.v | 57 +++++++++++++++++++++++------------------------- 1 file changed, 27 insertions(+), 30 deletions(-) (limited to 'backend/Constpropproof.v') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index fff9a60..6671960 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -19,7 +19,7 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import Events. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Smallstep. Require Import Op. @@ -152,7 +152,7 @@ Lemma functions_translated: Genv.find_funct tge v = Some (transf_fundef f). Proof. intros. - exact (Genv.find_funct_transf transf_fundef H). + exact (Genv.find_funct_transf transf_fundef _ _ H). Qed. Lemma function_ptr_translated: @@ -161,7 +161,7 @@ Lemma function_ptr_translated: Genv.find_funct_ptr tge b = Some (transf_fundef f). Proof. intros. - exact (Genv.find_funct_ptr_transf transf_fundef H). + exact (Genv.find_funct_ptr_transf transf_fundef _ _ H). Qed. Lemma sig_function_translated: @@ -220,21 +220,19 @@ Qed. Inductive match_stackframes: stackframe -> stackframe -> Prop := match_stackframe_intro: - forall res c sp pc rs f, - c = f.(RTL.fn_code) -> + forall res sp pc rs f, (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) -> match_stackframes - (Stackframe res c sp pc rs) - (Stackframe res (transf_code (analyze f) c) sp pc rs). + (Stackframe res f sp pc rs) + (Stackframe res (transf_function f) sp pc rs). Inductive match_states: state -> state -> Prop := | match_states_intro: - forall s c sp pc rs m f s' - (CF: c = f.(RTL.fn_code)) + forall s sp pc rs m f s' (MATCH: regs_match_approx ge (analyze f)!!pc rs) (STACKS: list_forall2 match_stackframes s s'), - match_states (State s c sp pc rs m) - (State s' (transf_code (analyze f) c) sp pc rs m) + match_states (State s f sp pc rs m) + (State s' (transf_function f) sp pc rs m) | match_states_call: forall s f args m s', list_forall2 match_stackframes s s' -> @@ -249,9 +247,9 @@ Inductive match_states: state -> state -> Prop := Ltac TransfInstr := match goal with | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ => - cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr)); - [ simpl - | unfold transf_code; rewrite PTree.gmap; + cut ((transf_function f).(fn_code)!pc = Some(transf_instr (analyze f)!!pc instr)); + [ simpl transf_instr + | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; unfold option_map; rewrite H1; reflexivity ] end. @@ -267,7 +265,7 @@ Proof. induction 1; intros; inv MS. (* Inop *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split. + exists (State s' (transf_function f) sp pc' rs m); split. TransfInstr; intro. eapply exec_Inop; eauto. econstructor; eauto. eapply analyze_correct_1 with (pc := pc); eauto. @@ -275,11 +273,11 @@ Proof. unfold transfer; rewrite H. auto. (* Iop *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split. + exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split. TransfInstr. caseEq (op_strength_reduction (approx_reg (analyze f)!!pc) op args); intros op' args' OSR. assert (eval_operation tge sp op' rs##args' = Some v). - rewrite (eval_operation_preserved symbols_preserved). + rewrite (eval_operation_preserved _ _ symbols_preserved). generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs MATCH op args v). rewrite OSR; simpl. auto. @@ -305,12 +303,12 @@ Proof. caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args); intros addr' args' ASR. assert (eval_addressing tge sp addr' rs##args' = Some a). - rewrite (eval_addressing_preserved symbols_preserved). + rewrite (eval_addressing_preserved _ _ symbols_preserved). generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs MATCH addr args). rewrite ASR; simpl. congruence. TransfInstr. rewrite ASR. intro. - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split. + exists (State s' (transf_function f) sp pc' (rs#dst <- v) m); split. eapply exec_Iload; eauto. econstructor; eauto. eapply analyze_correct_1; eauto. simpl; auto. @@ -321,12 +319,12 @@ Proof. caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args); intros addr' args' ASR. assert (eval_addressing tge sp addr' rs##args' = Some a). - rewrite (eval_addressing_preserved symbols_preserved). + rewrite (eval_addressing_preserved _ _ symbols_preserved). generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs MATCH addr args). rewrite ASR; simpl. congruence. TransfInstr. rewrite ASR. intro. - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split. + exists (State s' (transf_function f) sp pc' rs m'); split. eapply exec_Istore; eauto. econstructor; eauto. eapply analyze_correct_1; eauto. simpl; auto. @@ -351,7 +349,7 @@ Proof. constructor; auto. (* Icond, true *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. + exists (State s' (transf_function f) sp ifso rs m); split. caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); intros cond' args' CSR. assert (eval_condition cond' rs##args' = Some true). @@ -371,7 +369,7 @@ Proof. unfold transfer; rewrite H; auto. (* Icond, false *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. + exists (State s' (transf_function f) sp ifnot rs m); split. caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); intros cond' args' CSR. assert (eval_condition cond' rs##args' = Some false). @@ -391,7 +389,7 @@ Proof. unfold transfer; rewrite H; auto. (* Ijumptable *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split. + exists (State s' (transf_function f) sp pc' rs m); split. caseEq (intval (approx_reg (analyze f)!!pc) arg); intros. exploit intval_correct; eauto. eexact MATCH. intro VRS. eapply exec_Inop; eauto. TransfInstr. rewrite H2. @@ -403,7 +401,7 @@ Proof. unfold transfer; rewrite H; auto. (* Ireturn *) - exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split. + exists (Returnstate s' (regmap_optget or Vundef rs) m'); split. eapply exec_Ireturn; eauto. TransfInstr; auto. constructor; auto. @@ -432,15 +430,14 @@ Lemma transf_initial_states: Proof. intros. inversion H. exploit function_ptr_translated; eauto. intro FIND. - exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split. + exists (Callstate nil (transf_fundef f) nil m0); split. econstructor; eauto. + apply Genv.init_mem_transf; auto. replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. reflexivity. - rewrite <- H2. apply sig_function_translated. - replace (Genv.init_mem tprog) with (Genv.init_mem prog). - constructor. constructor. auto. - symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. + rewrite <- H3. apply sig_function_translated. + constructor. constructor. Qed. Lemma transf_final_states: -- cgit v1.2.3