diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
commit | 355b4abcee015c3fae9ac5653c25259e104a886c (patch) | |
tree | cfdb5b17f36b815bb358699cf420f64eba9dfe25 /backend/Constpropproof.v | |
parent | 22ff08b38616ceef336f5f974d4edc4d37d955e8 (diff) |
Fusion des modifications faites sur les branches "tailcalls" et "smallstep".
En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Constpropproof.v')
-rw-r--r-- | backend/Constpropproof.v | 609 |
1 files changed, 322 insertions, 287 deletions
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index ee24187..dfa828b 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -9,6 +9,7 @@ Require Import Values. Require Import Events. Require Import Mem. Require Import Globalenvs. +Require Import Smallstep. Require Import Op. Require Import Registers. Require Import RTL. @@ -41,6 +42,13 @@ Definition val_match_approx (a: approx) (v: val) : Prop := Definition regs_match_approx (a: D.t) (rs: regset) : Prop := forall r, val_match_approx (D.get r a) rs#r. +Lemma regs_match_approx_top: + forall rs, regs_match_approx D.top rs. +Proof. + intros. red; intros. simpl. rewrite PTree.gempty. + unfold Approx.top, val_match_approx. auto. +Qed. + Lemma val_match_approx_increasing: forall a1 a2 v, Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v. @@ -123,10 +131,10 @@ Ltac InvVLMA := approximations returned by [eval_static_operation]. *) Lemma eval_static_condition_correct: - forall cond al vl b, + forall cond al vl m b, val_list_match_approx al vl -> eval_static_condition cond al = Some b -> - eval_condition cond vl = Some b. + eval_condition cond vl m = Some b. Proof. intros until b. unfold eval_static_condition. @@ -135,9 +143,9 @@ Proof. Qed. Lemma eval_static_operation_correct: - forall op sp al vl v, + forall op sp al vl m v, val_list_match_approx al vl -> - eval_operation ge sp op vl = Some v -> + eval_operation ge sp op vl m = Some v -> val_match_approx (eval_static_operation op al) v. Proof. intros until v. @@ -183,7 +191,7 @@ Proof. rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence. caseEq (eval_static_condition c vl0). - intros. generalize (eval_static_condition_correct _ _ _ _ H H1). + intros. generalize (eval_static_condition_correct _ _ _ m _ H H1). intro. rewrite H2 in H0. destruct b; injection H0; intro; subst v; simpl; auto. intros; simpl; auto. @@ -194,80 +202,40 @@ Proof. auto. Qed. -(** The correctness of the transfer function follows: if the register - state before a transition matches the static approximations at that - program point, the register state after that transition matches - the static approximation returned by the transfer function. *) - -Lemma transfer_correct: - forall f c sp pc rs m t pc' rs' m' ra, - exec_instr ge c sp pc rs m t pc' rs' m' -> - c = f.(fn_code) -> - regs_match_approx ra rs -> - regs_match_approx (transfer f pc ra) rs'. -Proof. - induction 1; intros; subst c; unfold transfer; rewrite H; auto. - (* Iop *) - apply regs_match_approx_update. - apply eval_static_operation_correct with sp rs##args. - eapply approx_regs_val_list. auto. auto. auto. - (* Iload *) - apply regs_match_approx_update; auto. simpl; auto. - (* Icall *) - apply regs_match_approx_update; auto. simpl; auto. - (* Ialloc *) - apply regs_match_approx_update; auto. simpl; auto. -Qed. - (** The correctness of the static analysis follows from the results above and the fact that the result of the static analysis is a solution of the forward dataflow inequations. *) Lemma analyze_correct_1: - forall f approxs, - analyze f = Some approxs -> - forall c sp pc rs m t pc' rs' m', - exec_instr ge c sp pc rs m t pc' rs' m' -> - c = f.(fn_code) -> - regs_match_approx approxs!!pc rs -> - regs_match_approx approxs!!pc' rs'. + forall f pc rs pc', + In pc' (successors f pc) -> + regs_match_approx (transfer f pc (analyze f)!!pc) rs -> + regs_match_approx (analyze f)!!pc' rs. Proof. - intros. + intros until pc'. unfold analyze. + caseEq (DS.fixpoint (successors f) (fn_nextpc f) (transfer f) + ((fn_entrypoint f, D.top) :: nil)). + intros approxs; intros. apply regs_match_approx_increasing with (transfer f pc approxs!!pc). - eapply DS.fixpoint_solution. - unfold analyze in H. eexact H. + eapply DS.fixpoint_solution; eauto. elim (fn_code_wf f pc); intro. auto. - generalize (exec_instr_present _ _ _ _ _ _ _ _ _ _ H0). - rewrite H1. intro. contradiction. - eapply successors_correct. rewrite <- H1. eauto. - eapply transfer_correct; eauto. -Qed. - -Lemma analyze_correct_2: - forall f approxs, - analyze f = Some approxs -> - forall c sp pc rs m t pc' rs' m', - exec_instrs ge c sp pc rs m t pc' rs' m' -> - c = f.(fn_code) -> - regs_match_approx approxs!!pc rs -> - regs_match_approx approxs!!pc' rs'. -Proof. - intros f approxs ANL. induction 1. + unfold successors in H0; rewrite H2 in H0; simpl; contradiction. auto. - intros. eapply analyze_correct_1; eauto. - eauto. + intros. rewrite PMap.gi. apply regs_match_approx_top. Qed. Lemma analyze_correct_3: - forall f approxs rs, - analyze f = Some approxs -> - regs_match_approx approxs!!(f.(fn_entrypoint)) rs. + forall f rs, + regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs. Proof. - intros. + intros. unfold analyze. + caseEq (DS.fixpoint (successors f) (fn_nextpc f) (transfer f) + ((fn_entrypoint f, D.top) :: nil)). + intros approxs; intros. apply regs_match_approx_increasing with D.top. - eapply DS.fixpoint_entry. unfold analyze in H; eexact H. - auto with coqlib. - red; intros. rewrite D.get_top. simpl; auto. + eapply DS.fixpoint_entry; eauto. auto with coqlib. + apply regs_match_approx_top. + intros. rewrite PMap.gi. apply regs_match_approx_top. Qed. (** * Correctness of strength reduction *) @@ -296,9 +264,9 @@ Proof. Qed. Lemma cond_strength_reduction_correct: - forall cond args, + forall cond args m, let (cond', args') := cond_strength_reduction approx cond args in - eval_condition cond' rs##args' = eval_condition cond rs##args. + eval_condition cond' rs##args' m = eval_condition cond rs##args m. Proof. intros. unfold cond_strength_reduction. case (cond_strength_reduction_match cond args); intros. @@ -312,7 +280,6 @@ Proof. caseEq (intval approx r1); intros. simpl. rewrite (intval_correct _ _ H). destruct (rs#r2); auto. rewrite Int.swap_cmpu. auto. - destruct c; reflexivity. caseEq (intval approx r2); intros. simpl. rewrite (intval_correct _ _ H0). auto. auto. @@ -320,10 +287,10 @@ Proof. Qed. Lemma make_addimm_correct: - forall n r v, + forall n r m v, let (op, args) := make_addimm n r in - eval_operation ge sp Oadd (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oadd (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_addimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -333,10 +300,10 @@ Proof. Qed. Lemma make_shlimm_correct: - forall n r v, + forall n r m v, let (op, args) := make_shlimm n r in - eval_operation ge sp Oshl (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oshl (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_shlimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -347,10 +314,10 @@ Proof. Qed. Lemma make_shrimm_correct: - forall n r v, + forall n r m v, let (op, args) := make_shrimm n r in - eval_operation ge sp Oshr (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oshr (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_shrimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -359,10 +326,10 @@ Proof. Qed. Lemma make_shruimm_correct: - forall n r v, + forall n r m v, let (op, args) := make_shruimm n r in - eval_operation ge sp Oshru (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oshru (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_shruimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -373,10 +340,10 @@ Proof. Qed. Lemma make_mulimm_correct: - forall n r v, + forall n r m v, let (op, args) := make_mulimm n r in - eval_operation ge sp Omul (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Omul (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_mulimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -384,8 +351,8 @@ Proof. generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intros. subst n. simpl in H1. simpl. FuncInv. rewrite Int.mul_one in H0. congruence. caseEq (Int.is_power2 n); intros. - replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil)) - with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)). + replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil) m) + with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil) m). apply make_shlimm_correct. simpl. generalize (Int.is_power2_range _ _ H1). change (Z_of_nat wordsize) with 32. intro. rewrite H2. @@ -394,10 +361,10 @@ Proof. Qed. Lemma make_andimm_correct: - forall n r v, + forall n r m v, let (op, args) := make_andimm n r in - eval_operation ge sp Oand (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oand (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_andimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -408,10 +375,10 @@ Proof. Qed. Lemma make_orimm_correct: - forall n r v, + forall n r m v, let (op, args) := make_orimm n r in - eval_operation ge sp Oor (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oor (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_orimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -422,10 +389,10 @@ Proof. Qed. Lemma make_xorimm_correct: - forall n r v, + forall n r m v, let (op, args) := make_xorimm n r in - eval_operation ge sp Oxor (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oxor (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_xorimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -434,18 +401,18 @@ Proof. Qed. Lemma op_strength_reduction_correct: - forall op args v, + forall op args m v, let (op', args') := op_strength_reduction approx op args in - eval_operation ge sp op rs##args = Some v -> - eval_operation ge sp op' rs##args' = Some v. + eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op' rs##args' m = Some v. Proof. intros; unfold op_strength_reduction; case (op_strength_reduction_match op args); intros; simpl List.map. (* Oadd *) caseEq (intval approx r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil) m). apply make_addimm_correct. simpl. destruct rs#r2; auto. rewrite Int.add_commut; auto. caseEq (intval approx r2); intros. @@ -456,16 +423,16 @@ Proof. rewrite (intval_correct _ _ H) in H0. assumption. caseEq (intval approx r2); intros. rewrite (intval_correct _ _ H0). - replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil)). + replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil) m) + with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil) m). apply make_addimm_correct. simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto. assumption. (* Omul *) caseEq (intval approx r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil) m). apply make_mulimm_correct. simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto. caseEq (intval approx r2); intros. @@ -485,8 +452,8 @@ Proof. caseEq (intval approx r2); intros. caseEq (Int.is_power2 i); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)). + replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil) m) + with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil) m). apply make_shruimm_correct. simpl. destruct rs#r1; auto. change 32 with (Z_of_nat wordsize). @@ -499,8 +466,8 @@ Proof. (* Oand *) caseEq (intval approx r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil) m). apply make_andimm_correct. simpl. destruct rs#r2; auto. rewrite Int.and_commut; auto. caseEq (intval approx r2); intros. @@ -509,8 +476,8 @@ Proof. (* Oor *) caseEq (intval approx r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil) m). apply make_orimm_correct. simpl. destruct rs#r2; auto. rewrite Int.or_commut; auto. caseEq (intval approx r2); intros. @@ -519,8 +486,8 @@ Proof. (* Oxor *) caseEq (intval approx r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil) m). apply make_xorimm_correct. simpl. destruct rs#r2; auto. rewrite Int.xor_commut; auto. caseEq (intval approx r2); intros. @@ -647,261 +614,329 @@ Let tge := Genv.globalenv tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof (Genv.find_symbol_transf transf_fundef prog). +Proof. + intros; unfold ge, tge, tprog, transf_program. + apply Genv.find_symbol_transf. +Qed. Lemma functions_translated: - forall (v: val) (f: RTL.fundef), + forall (v: val) (f: fundef), Genv.find_funct ge v = Some f -> Genv.find_funct tge v = Some (transf_fundef f). -Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog). +Proof. + intros. + exact (Genv.find_funct_transf transf_fundef H). +Qed. Lemma function_ptr_translated: - forall (v: block) (f: RTL.fundef), - Genv.find_funct_ptr ge v = Some f -> - Genv.find_funct_ptr tge v = Some (transf_fundef f). -Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog). + forall (b: block) (f: fundef), + Genv.find_funct_ptr ge b = Some f -> + Genv.find_funct_ptr tge b = Some (transf_fundef f). +Proof. + intros. + exact (Genv.find_funct_ptr_transf transf_fundef H). +Qed. -Lemma sig_translated: - forall (f: RTL.fundef), +Lemma sig_function_translated: + forall f, funsig (transf_fundef f) = funsig f. Proof. - intro. case f; intros; simpl. - unfold transf_function. case (analyze f0); intros; reflexivity. - reflexivity. + intros. destruct f; reflexivity. +Qed. + +Lemma transf_ros_correct: + forall ros rs f approx, + regs_match_approx ge approx rs -> + find_function ge ros rs = Some f -> + find_function tge (transf_ros approx ros) rs = Some (transf_fundef f). +Proof. + intros until approx; intro MATCH. + destruct ros; simpl. + intro. + exploit functions_translated; eauto. intro FIND. + caseEq (D.get r approx); intros; auto. + generalize (Int.eq_spec i0 Int.zero); case (Int.eq i0 Int.zero); intros; auto. + generalize (MATCH r). rewrite H0. intros [b [A B]]. + rewrite <- symbols_preserved in A. + rewrite B in FIND. rewrite H1 in FIND. + rewrite Genv.find_funct_find_funct_ptr in FIND. + simpl. rewrite A. auto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge i). + intro. apply function_ptr_translated. auto. + congruence. Qed. (** The proof of semantic preservation is a simulation argument based on diagrams of the following form: << - pc, rs, m ------------------- pc, rs, m - | | - | | - v v - pc', rs', m' ---------------- pc', rs', m' + st1 --------------- st2 + | | + t| |t + | | + v v + st1'--------------- st2' >> The left vertical arrow represents a transition in the - original RTL code. The top horizontal bar expresses that the values - of registers [rs] match their compile-time approximations at point [pc]. + original RTL code. The top horizontal bar is the [match_states] + invariant between the initial state [st1] in the original RTL code + and an initial state [st2] in the transformed code. + This invariant expresses that all code fragments appearing in [st2] + are obtained by [transf_code] transformation of the corresponding + fragments in [st1]. Moreover, the values of registers in [st1] + must match their compile-time approximations at the current program + point. These two parts of the diagram are the hypotheses. In conclusions, we want to prove the other two parts: the right vertical arrow, which is a transition in the transformed RTL code, and the bottom - horizontal bar, which means that [rs'] matches the compile-time - approximations at [pc']. - - To help express those diagrams, we define the following propositions - parameterized by the transition in the original RTL code (left arrow) - and summarizing the three other arrows of the diagram. *) - -Definition exec_instr_prop - (c: code) (sp: val) - (pc: node) (rs: regset) (m: mem) (t: trace) - (pc': node) (rs': regset) (m': mem) : Prop := - exec_instr tge c sp pc rs m t pc' rs' m' /\ - forall f approxs - (CF: c = f.(RTL.fn_code)) - (ANL: analyze f = Some approxs) - (MATCH: regs_match_approx ge approxs!!pc rs), - exec_instr tge (transf_code approxs c) sp pc rs m t pc' rs' m'. - -Definition exec_instrs_prop - (c: code) (sp: val) - (pc: node) (rs: regset) (m: mem) (t: trace) - (pc': node) (rs': regset) (m': mem) : Prop := - exec_instrs tge c sp pc rs m t pc' rs' m' /\ - forall f approxs - (CF: c = f.(RTL.fn_code)) - (ANL: analyze f = Some approxs) - (MATCH: regs_match_approx ge approxs!!pc rs), - exec_instrs tge (transf_code approxs c) sp pc rs m t pc' rs' m'. - -Definition exec_function_prop - (f: RTL.fundef) (args: list val) (m: mem) (t: trace) - (res: val) (m': mem) : Prop := - exec_function tge (transf_fundef f) args m t res m'. + horizontal bar, which means that the [match_state] predicate holds + between the final states [st1'] and [st2']. *) + +Inductive match_stackframes: stackframe -> stackframe -> Prop := + match_stackframe_intro: + forall res c sp pc rs f, + c = f.(RTL.fn_code) -> + (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). + +Inductive match_states: state -> state -> Prop := + | match_states_intro: + forall s c sp pc rs m f s' + (CF: c = f.(RTL.fn_code)) + (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_call: + forall s f args m s', + list_forall2 match_stackframes s s' -> + match_states (Callstate s f args m) + (Callstate s' (transf_fundef f) args m) + | match_states_return: + forall s s' v m, + list_forall2 match_stackframes s s' -> + match_states (Returnstate s v m) + (Returnstate s' v m). Ltac TransfInstr := match goal with - | H1: (PTree.get ?pc ?c = Some ?instr), - H2: (analyze ?f = Some ?approxs) |- _ => - cut ((transf_code approxs c)!pc = Some(transf_instr approxs!!pc instr)); + | 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; unfold option_map; rewrite H1; reflexivity ] end. -(** The predicates above serve as induction hypotheses in the proof of - simulation, which proceeds by induction over the - evaluation derivation of the original code. *) +(** The proof of simulation proceeds by case analysis on the transition + taken in the source code. *) -Lemma transf_funct_correct: - forall f args m t res m', - exec_function ge f args m t res m' -> - exec_function_prop f args m t res m'. +Lemma transf_step_correct: + forall s1 t s2, + step ge s1 t s2 -> + forall s1' (MS: match_states s1 s1'), + exists s2', step tge s1' t s2' /\ match_states s2 s2'. Proof. - apply (exec_function_ind_3 ge - exec_instr_prop exec_instrs_prop exec_function_prop); - intros; red. + induction 1; intros; inv MS. + (* Inop *) - split; [idtac| intros; TransfInstr]. - apply exec_Inop; auto. - intros; apply exec_Inop; auto. + exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split. + TransfInstr; intro. eapply exec_Inop; eauto. + econstructor; eauto. + eapply analyze_correct_1 with (pc := pc); eauto. + unfold successors; rewrite H; auto with coqlib. + unfold transfer; rewrite H. auto. + (* Iop *) - split; [idtac| intros; TransfInstr]. - apply exec_Iop with op args. auto. - rewrite (eval_operation_preserved symbols_preserved). auto. - caseEq (op_strength_reduction approxs!!pc op args); + exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split. + TransfInstr. caseEq (op_strength_reduction (analyze f)!!pc op args); intros op' args' OSR. - assert (eval_operation tge sp op' rs##args' = Some v). + assert (eval_operation tge sp op' rs##args' m = Some v). rewrite (eval_operation_preserved symbols_preserved). - generalize (op_strength_reduction_correct ge approxs!!pc sp rs - MATCH op args v). + generalize (op_strength_reduction_correct ge (analyze f)!!pc sp rs + MATCH op args m v). rewrite OSR; simpl. auto. generalize (eval_static_operation_correct ge op sp - (approx_regs args approxs!!pc) rs##args v + (approx_regs args (analyze f)!!pc) rs##args m v (approx_regs_val_list _ _ _ args MATCH) H0). - case (eval_static_operation op (approx_regs args approxs!!pc)); intros; - simpl in H1; + case (eval_static_operation op (approx_regs args (analyze f)!!pc)); intros; + simpl in H2; eapply exec_Iop; eauto; simpl. - simpl in H2; congruence. - simpl in H2; congruence. + congruence. + congruence. elim H2; intros b [A B]. rewrite symbols_preserved. rewrite A; rewrite B; auto. + econstructor; eauto. + eapply analyze_correct_1 with (pc := pc); eauto. + unfold successors; rewrite H; auto with coqlib. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. + eapply eval_static_operation_correct; eauto. + apply approx_regs_val_list; auto. + (* Iload *) - split; [idtac| intros; TransfInstr]. - eapply exec_Iload; eauto. - rewrite (eval_addressing_preserved symbols_preserved). auto. - caseEq (addr_strength_reduction approxs!!pc addr args); + caseEq (addr_strength_reduction (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). - generalize (addr_strength_reduction_correct ge approxs!!pc sp rs + generalize (addr_strength_reduction_correct ge (analyze f)!!pc sp rs MATCH addr args). rewrite ASR; simpl. congruence. - intro. eapply exec_Iload; eauto. + TransfInstr. rewrite ASR. intro. + exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split. + eapply exec_Iload; eauto. + econstructor; eauto. + apply analyze_correct_1 with pc; auto. + unfold successors; rewrite H; auto with coqlib. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. simpl; auto. + (* Istore *) - split; [idtac| intros; TransfInstr]. - eapply exec_Istore; eauto. - rewrite (eval_addressing_preserved symbols_preserved). auto. - caseEq (addr_strength_reduction approxs!!pc addr args); + caseEq (addr_strength_reduction (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). - generalize (addr_strength_reduction_correct ge approxs!!pc sp rs + generalize (addr_strength_reduction_correct ge (analyze f)!!pc sp rs MATCH addr args). - rewrite ASR; simpl. congruence. - intro. eapply exec_Istore; eauto. + rewrite ASR; simpl. congruence. + TransfInstr. rewrite ASR. intro. + exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split. + eapply exec_Istore; eauto. + econstructor; eauto. + apply analyze_correct_1 with pc; auto. + unfold successors; rewrite H; auto with coqlib. + unfold transfer; rewrite H. auto. + (* Icall *) - assert (find_function tge ros rs = Some (transf_fundef f)). - generalize H0; unfold find_function; destruct ros. - apply functions_translated. - rewrite symbols_preserved. destruct (Genv.find_symbol ge i). - apply function_ptr_translated. congruence. - assert (funsig (transf_fundef f) = sig). - generalize (sig_translated f). congruence. - split; [idtac| intros; TransfInstr]. - eapply exec_Icall; eauto. - set (ros' := - match ros with - | inl r => - match D.get r approxs !! pc with - | Novalue => ros - | Unknown => ros - | I _ => ros - | F _ => ros - | S symb ofs => if Int.eq ofs Int.zero then inr reg symb else ros - end - | inr _ => ros - end). - intros; eapply exec_Icall; eauto. - unfold ros'; destruct ros; auto. - caseEq (D.get r approxs!!pc); intros; auto. - generalize (Int.eq_spec i0 Int.zero); case (Int.eq i0 Int.zero); intros; auto. - generalize (MATCH r). rewrite H7. intros [b [A B]]. - rewrite <- symbols_preserved in A. - generalize H4. simpl. rewrite A. rewrite B. subst i0. - rewrite Genv.find_funct_find_funct_ptr. auto. + exploit transf_ros_correct; eauto. intro FIND'. + TransfInstr; intro. + econstructor; split. + eapply exec_Icall; eauto. apply sig_function_translated; auto. + constructor; auto. constructor; auto. + econstructor; eauto. + intros. apply analyze_correct_1 with pc; auto. + unfold successors; rewrite H; auto with coqlib. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. simpl. auto. + + (* Itailcall *) + exploit transf_ros_correct; eauto. intros FIND'. + TransfInstr; intro. + econstructor; split. + eapply exec_Itailcall; eauto. apply sig_function_translated; auto. + constructor; auto. (* Ialloc *) - split; [idtac|intros; TransfInstr]. - eapply exec_Ialloc; eauto. - intros. eapply exec_Ialloc; eauto. + TransfInstr; intro. + exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- (Vptr b Int.zero)) m'); split. + eapply exec_Ialloc; eauto. + econstructor; eauto. + apply analyze_correct_1 with pc; auto. + unfold successors; rewrite H; auto with coqlib. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. simpl; auto. (* Icond, true *) - split; [idtac| intros; TransfInstr]. - eapply exec_Icond_true; eauto. - caseEq (cond_strength_reduction approxs!!pc cond args); + exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. + caseEq (cond_strength_reduction (analyze f)!!pc cond args); intros cond' args' CSR. - assert (eval_condition cond' rs##args' = Some true). + assert (eval_condition cond' rs##args' m = Some true). generalize (cond_strength_reduction_correct - ge approxs!!pc rs MATCH cond args). + ge (analyze f)!!pc rs MATCH cond args m). rewrite CSR. intro. congruence. - caseEq (eval_static_condition cond (approx_regs args approxs!!pc)). + TransfInstr. rewrite CSR. + caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)). intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ _ + generalize (eval_static_condition_correct ge cond _ _ m _ (approx_regs_val_list _ _ _ args MATCH) ESC); intro. replace b with true. intro; eapply exec_Inop; eauto. congruence. - intros. eapply exec_Icond_true; eauto. + intros. eapply exec_Icond_true; eauto. + econstructor; eauto. + apply analyze_correct_1 with pc; auto. + unfold successors; rewrite H; auto with coqlib. + unfold transfer; rewrite H; auto. (* Icond, false *) - split; [idtac| intros; TransfInstr]. - eapply exec_Icond_false; eauto. - caseEq (cond_strength_reduction approxs!!pc cond args); + exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. + caseEq (cond_strength_reduction (analyze f)!!pc cond args); intros cond' args' CSR. - assert (eval_condition cond' rs##args' = Some false). + assert (eval_condition cond' rs##args' m = Some false). generalize (cond_strength_reduction_correct - ge approxs!!pc rs MATCH cond args). + ge (analyze f)!!pc rs MATCH cond args m). rewrite CSR. intro. congruence. - caseEq (eval_static_condition cond (approx_regs args approxs!!pc)). + TransfInstr. rewrite CSR. + caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)). intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ _ + generalize (eval_static_condition_correct ge cond _ _ m _ (approx_regs_val_list _ _ _ args MATCH) ESC); intro. replace b with false. intro; eapply exec_Inop; eauto. congruence. - intros. eapply exec_Icond_false; eauto. - - (* refl *) - split. apply exec_refl. intros. apply exec_refl. - (* one *) - elim H0; intros. - split. apply exec_one; auto. - intros. apply exec_one. eapply H2; eauto. - (* trans *) - elim H0; intros. elim H2; intros. - split. - apply exec_trans with t1 pc2 rs2 m2 t2; auto. - intros; apply exec_trans with t1 pc2 rs2 m2 t2. - eapply H5; eauto. eapply H7; eauto. - eapply analyze_correct_2; eauto. auto. + intros. eapply exec_Icond_false; eauto. + econstructor; eauto. + apply analyze_correct_1 with pc; auto. + unfold successors; rewrite H; auto with coqlib. + unfold transfer; rewrite H; auto. + + (* Ireturn *) + exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split. + eapply exec_Ireturn; eauto. TransfInstr; auto. + constructor; auto. (* internal function *) - elim H1; intros. - simpl. unfold transf_function. - caseEq (analyze f). - intros approxs ANL. - eapply exec_funct_internal; simpl; eauto. - eapply H5. reflexivity. auto. + simpl. unfold transf_function. + econstructor; split. + eapply exec_function_internal; simpl; eauto. + simpl. econstructor; eauto. apply analyze_correct_3; auto. - TransfInstr; auto. - intros. eapply exec_funct_internal; eauto. + (* external function *) - unfold transf_function; simpl. apply exec_funct_external; auto. + simpl. econstructor; split. + eapply exec_function_external; eauto. + constructor; auto. + + (* return *) + inv H3. inv H1. + econstructor; split. + eapply exec_return; eauto. + econstructor; eauto. +Qed. + +Lemma transf_initial_states: + forall st1, initial_state prog st1 -> + exists st2, initial_state tprog st2 /\ match_states st1 st2. +Proof. + intros. inversion H. + exploit function_ptr_translated; eauto. intro FIND. + exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split. + econstructor; eauto. + 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. +Qed. + +Lemma transf_final_states: + forall st1 st2 r, + match_states st1 st2 -> final_state st1 r -> final_state st2 r. +Proof. + intros. inv H0. inv H. inv H4. constructor. Qed. (** The preservation of the observable behavior of the program then - follows. *) + follows, using the generic preservation theorem + [Smallstep.simulation_step_preservation]. *) Theorem transf_program_correct: - forall (t: trace) (r: val), - exec_program prog t r -> exec_program tprog t r. + forall (beh: program_behavior), + exec_program prog beh -> exec_program tprog beh. Proof. - intros t r [b [f [m [SYMB [FIND [SIG EXEC]]]]]]. - red. exists b. exists (transf_fundef f). exists m. - split. change (prog_main tprog) with (prog_main prog). - rewrite symbols_preserved. auto. - split. apply function_ptr_translated; auto. - split. generalize (sig_translated f). congruence. - apply transf_funct_correct. - unfold tprog, transf_program. rewrite Genv.init_mem_transf. - exact EXEC. + unfold exec_program; intros. + eapply simulation_step_preservation; eauto. + eexact transf_initial_states. + eexact transf_final_states. + exact transf_step_correct. Qed. End PRESERVATION. |