From 611e7b09253dbbb98e9cd4ca4e07a60b50e693fd Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 8 Jul 2008 12:04:42 +0000 Subject: Fusion partielle de la branche contsem: - semantiques a continuation pour Cminor et CminorSel - goto dans Cminor Suppression de backend/RTLbigstep.v, devenu inutile. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenproof.v | 1126 +++++++++++++++++++------------------------------ 1 file changed, 440 insertions(+), 686 deletions(-) (limited to 'backend/RTLgenproof.v') diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index e02463a..1074ddd 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -355,7 +355,8 @@ Proof. intros until tf. unfold transl_fundef, transf_partial_fundef. case f; intro. unfold transl_function. - case (transl_fun f0 init_state); simpl; intros. + destruct (reserve_labels (fn_body f0) (PTree.empty node, init_state)) as [ngoto s0]. + case (transl_fun f0 ngoto s0); simpl; intros. discriminate. destruct p. simpl in H. inversion H. reflexivity. intro. inversion H. reflexivity. @@ -415,6 +416,42 @@ Proof. exists rs; split. subst nd. apply star_refl. auto. Qed. +(** Correctness of the translation of [switch] statements *) + +Lemma transl_switch_correct: + forall cs sp rs m i code r nexits t ns, + tr_switch code r nexits t ns -> + rs#r = Vint i -> + exists nd, + star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs m) /\ + nth_error nexits (comptree_match i t) = Some nd. +Proof. + induction 1; intros; simpl. + exists n. split. apply star_refl. auto. + + caseEq (Int.eq i key); intros. + exists nfound; split. + apply star_one. eapply exec_Icond_true; eauto. + simpl. rewrite H2. congruence. auto. + exploit IHtr_switch; eauto. intros [nd [EX MATCH]]. + exists nd; split. + eapply star_step. eapply exec_Icond_false; eauto. + simpl. rewrite H2. congruence. eexact EX. traceEq. + auto. + + caseEq (Int.ltu i key); intros. + exploit IHtr_switch1; eauto. intros [nd [EX MATCH]]. + exists nd; split. + eapply star_step. eapply exec_Icond_true; eauto. + simpl. rewrite H2. congruence. eexact EX. traceEq. + auto. + exploit IHtr_switch2; eauto. intros [nd [EX MATCH]]. + exists nd; split. + eapply star_step. eapply exec_Icond_false; eauto. + simpl. rewrite H2. congruence. eexact EX. traceEq. + auto. +Qed. + (** ** Semantic preservation for the translation of expressions *) Section CORRECTNESS_EXPR. @@ -429,7 +466,7 @@ Variable m: mem. I /\ P e, le, m, a ------------- State cs code sp ns rs m || | - t|| t|* + || |* || | \/ v e, le, m', v ------------ State cs code sp nd rs' m' @@ -824,7 +861,73 @@ Proof End CORRECTNESS_EXPR. -(** ** Semantic preservation for the translation of terminating statements *) +(** ** Measure over CminorSel states *) + +Open Local Scope nat_scope. + +Fixpoint size_stmt (s: stmt) : nat := + match s with + | Sskip => 0 + | Sseq s1 s2 => (size_stmt s1 + size_stmt s2 + 1) + | Sifthenelse e s1 s2 => (size_stmt s1 + size_stmt s2 + 1) + | Sloop s1 => (size_stmt s1 + 1) + | Sblock s1 => (size_stmt s1 + 1) + | Sexit n => 0 + | Slabel lbl s1 => (size_stmt s1 + 1) + | _ => 1 + end. + +Fixpoint size_cont (k: cont) : nat := + match k with + | Kseq s k1 => (size_stmt s + size_cont k1 + 1) + | Kblock k1 => (size_cont k1 + 1) + | _ => 0%nat + end. + +Definition measure_state (S: CminorSel.state) := + match S with + | CminorSel.State _ s k _ _ _ => + existS (fun (x: nat) => nat) + (size_stmt s + size_cont k) + (size_stmt s) + | _ => + existS (fun (x: nat) => nat) 0 0 + end. + +Require Import Relations. +Require Import Wellfounded. + +Definition lt_state (S1 S2: CminorSel.state) := + lexprod nat (fun (x: nat) => nat) + lt (fun (x: nat) => lt) + (measure_state S1) (measure_state S2). + +Lemma lt_state_intro: + forall f1 s1 k1 sp1 e1 m1 f2 s2 k2 sp2 e2 m2, + size_stmt s1 + size_cont k1 < size_stmt s2 + size_cont k2 + \/ (size_stmt s1 + size_cont k1 = size_stmt s2 + size_cont k2 + /\ size_stmt s1 < size_stmt s2) -> + lt_state (CminorSel.State f1 s1 k1 sp1 e1 m1) + (CminorSel.State f2 s2 k2 sp2 e2 m2). +Proof. + intros. unfold lt_state. simpl. destruct H as [A | [A B]]. + apply left_lex. auto. + rewrite A. apply right_lex. auto. +Qed. + +Ltac Lt_state := + apply lt_state_intro; simpl; try omega. + +Require Import Wf_nat. + +Lemma lt_state_wf: + well_founded lt_state. +Proof. + unfold lt_state. apply wf_inverse_image with (f := measure_state). + apply wf_lexprod. apply lt_wf. intros. apply lt_wf. +Qed. + +(** ** Semantic preservation for the translation of statements *) (** The simulation diagram for the translation of statements is of the following form: @@ -854,718 +957,369 @@ End CORRECTNESS_EXPR. [e']. Moreover, the program point reached must correspond to the outcome [out]. This is captured by the following [state_for_outcome] predicate. *) -Inductive state_for_outcome - (ncont: node) (nexits: list node) (nret: node) (rret: option reg) - (cs: list stackframe) (c: code) (sp: val) (rs: regset) (m: mem): - outcome -> RTL.state -> Prop := - | state_for_normal: - state_for_outcome ncont nexits nret rret cs c sp rs m - Out_normal (State cs c sp ncont rs m) - | state_for_exit: forall n nexit, - nth_error nexits n = Some nexit -> - state_for_outcome ncont nexits nret rret cs c sp rs m - (Out_exit n) (State cs c sp nexit rs m) - | state_for_return_none: - rret = None -> - state_for_outcome ncont nexits nret rret cs c sp rs m - (Out_return None) (State cs c sp nret rs m) - | state_for_return_some: forall r v, - rret = Some r -> - rs#r = v -> - state_for_outcome ncont nexits nret rret cs c sp rs m - (Out_return (Some v)) (State cs c sp nret rs m) - | state_for_return_tail: forall v, - state_for_outcome ncont nexits nret rret cs c sp rs m - (Out_tailcall_return v) (Returnstate cs v m). - -Definition transl_stmt_prop - (sp: val) (e: env) (m: mem) (a: stmt) - (t: trace) (e': env) (m': mem) (out: outcome) : Prop := - forall cs code map ns ncont nexits nret rret rs - (MWF: map_wf map) - (TE: tr_stmt code map a ns ncont nexits nret rret) - (ME: match_env map e nil rs), - exists rs', exists st, - state_for_outcome ncont nexits nret rret cs code sp rs' m' out st - /\ star step tge (State cs code sp ns rs m) t st - /\ match_env map e' nil rs'. - -(** Finally, the correctness condition for the translation of functions - is that the translated RTL function, when applied to the same arguments - as the original Cminor function, returns the same value and performs - the same modifications on the memory state. *) - -Definition transl_function_prop - (m: mem) (f: CminorSel.fundef) (vargs: list val) - (t: trace) (m': mem) (vres: val) : Prop := - forall cs tf - (TE: transl_fundef f = OK tf), - star step tge (Callstate cs tf vargs m) t (Returnstate cs vres m'). - -Lemma transl_funcall_internal_correct: - forall (m : mem) (f : CminorSel.function) - (vargs : list val) (m1 : mem) (sp : block) (e : env) (t : trace) - (e2 : env) (m2 : mem) (out: outcome) (vres : val), - Mem.alloc m 0 (fn_stackspace f) = (m1, sp) -> - set_locals (fn_vars f) (set_params vargs (CminorSel.fn_params f)) = e -> - exec_stmt ge (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out -> - transl_stmt_prop (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out -> - outcome_result_value out f.(CminorSel.fn_sig).(sig_res) vres -> - transl_function_prop m (Internal f) vargs t - (outcome_free_mem out m2 sp) vres. +Inductive tr_funbody (c: code) (map: mapping) (f: CminorSel.function) + (ngoto: labelmap) (nret: node) (rret: option reg) : Prop := + | tr_funbody_intro: forall nentry r, + rret = ret_reg f.(CminorSel.fn_sig) r -> + tr_stmt c map f.(fn_body) nentry nret nil ngoto nret rret -> + tr_funbody c map f ngoto nret rret. + +Inductive tr_cont: RTL.code -> mapping -> + CminorSel.cont -> node -> list node -> labelmap -> node -> option reg -> + list RTL.stackframe -> Prop := + | tr_Kseq: forall c map s k nd nexits ngoto nret rret cs n, + tr_stmt c map s nd n nexits ngoto nret rret -> + tr_cont c map k n nexits ngoto nret rret cs -> + tr_cont c map (Kseq s k) nd nexits ngoto nret rret cs + | tr_Kblock: forall c map k nd nexits ngoto nret rret cs, + tr_cont c map k nd nexits ngoto nret rret cs -> + tr_cont c map (Kblock k) nd (nd :: nexits) ngoto nret rret cs + | tr_Kstop: forall c map ngoto nret rret cs, + c!nret = Some(Ireturn rret) -> + match_stacks Kstop cs -> + tr_cont c map Kstop nret nil ngoto nret rret cs + | tr_Kcall: forall c map optid f sp e k ngoto nret rret cs, + c!nret = Some(Ireturn rret) -> + match_stacks (Kcall optid f sp e k) cs -> + tr_cont c map (Kcall optid f sp e k) nret nil ngoto nret rret cs + +with match_stacks: CminorSel.cont -> list RTL.stackframe -> Prop := + | match_stacks_stop: + match_stacks Kstop nil + | match_stacks_call: forall optid f sp e k r c n rs cs map nexits ngoto nret rret n', + map_wf map -> + tr_funbody c map f ngoto nret rret -> + match_env map e nil rs -> + tr_store_optvar c map r optid n n' -> + ~reg_in_map map r -> + tr_cont c map k n' nexits ngoto nret rret cs -> + match_stacks (Kcall optid f sp e k) (Stackframe r c sp n rs :: cs). + +Inductive match_states: CminorSel.state -> RTL.state -> Prop := + | match_state: + forall f s k sp e m cs c ns rs map ncont nexits ngoto nret rret + (MWF: map_wf map) + (TS: tr_stmt c map s ns ncont nexits ngoto nret rret) + (TF: tr_funbody c map f ngoto nret rret) + (TK: tr_cont c map k ncont nexits ngoto nret rret cs) + (ME: match_env map e nil rs), + match_states (CminorSel.State f s k sp e m) + (RTL.State cs c sp ns rs m) + | match_callstate: + forall f args k m cs tf + (TF: transl_fundef f = OK tf) + (MS: match_stacks k cs), + match_states (CminorSel.Callstate f args k m) + (RTL.Callstate cs tf args m) + | match_returnstate: + forall v k m cs + (MS: match_stacks k cs), + match_states (CminorSel.Returnstate v k m) + (RTL.Returnstate cs v m). + +Lemma match_stacks_call_cont: + forall c map k ncont nexits ngoto nret rret cs, + tr_cont c map k ncont nexits ngoto nret rret cs -> + match_stacks (call_cont k) cs /\ c!nret = Some(Ireturn rret). Proof. - intros; red; intros. - generalize TE; simpl. caseEq (transl_function f); simpl. 2: congruence. - intros tfi EQ1 EQ2. injection EQ2; clear EQ2; intro EQ2. - assert (TR: tr_function f tfi). apply transl_function_charact; auto. - rewrite <- EQ2. inversion TR. subst f0. - - pose (rs := init_regs vargs rparams). - assert (ME: match_env map2 e nil rs). - rewrite <- H0. unfold rs. - eapply match_init_env_init_reg; eauto. - - assert (MWF: map_wf map2). - assert (map_valid init_mapping init_state) by apply init_mapping_valid. - exploit (add_vars_valid (CminorSel.fn_params f)); eauto. intros [A B]. - eapply add_vars_wf; eauto. eapply add_vars_wf; eauto. apply init_mapping_wf. - - exploit H2; eauto. intros [rs' [st [OUT [EX ME']]]]. - - eapply star_left. - eapply exec_function_internal; eauto. simpl. - inversion OUT; clear OUT; subst out st; simpl in H3; simpl. - - (* Out_normal *) - unfold ret_reg in H6. destruct (sig_res (CminorSel.fn_sig f)). contradiction. - subst vres orret. - eapply star_right. unfold rs in EX. eexact EX. - change Vundef with (regmap_optget None Vundef rs'). - apply exec_Ireturn. auto. reflexivity. - - (* Out_exit *) - contradiction. - - (* Out_return None *) - subst orret. - unfold ret_reg in H8. destruct (sig_res (CminorSel.fn_sig f)). contradiction. - subst vres. - eapply star_right. unfold rs in EX. eexact EX. - change Vundef with (regmap_optget None Vundef rs'). - apply exec_Ireturn. auto. - reflexivity. - - (* Out_return Some *) - subst orret. - unfold ret_reg in H8. unfold ret_reg in H9. - destruct (sig_res (CminorSel.fn_sig f)). inversion H9. - subst vres. - eapply star_right. unfold rs in EX. eexact EX. - replace v with (regmap_optget (Some rret) Vundef rs'). - apply exec_Ireturn. auto. - simpl. congruence. - reflexivity. - contradiction. - - (* a tail call *) - subst v. rewrite E0_right. auto. traceEq. + induction 1; simpl; auto. Qed. -Lemma transl_funcall_external_correct: - forall (ef : external_function) (m : mem) (args : list val) (t: trace) (res : val), - event_match ef args t res -> - transl_function_prop m (External ef) args t m res. +Lemma tr_cont_call_cont: + forall c map k ncont nexits ngoto nret rret cs, + tr_cont c map k ncont nexits ngoto nret rret cs -> + tr_cont c map (call_cont k) nret nil ngoto nret rret cs. Proof. - intros; red; intros. unfold transl_function in TE; simpl in TE. - inversion TE; subst tf. - apply star_one. apply exec_function_external. auto. + induction 1; simpl; auto; econstructor; eauto. Qed. -Lemma transl_stmt_Sskip_correct: - forall (sp: val) (e : env) (m : mem), - transl_stmt_prop sp e m Sskip E0 e m Out_normal. +Lemma tr_find_label: + forall c map lbl n (ngoto: labelmap) nret rret s' k' cs, + ngoto!lbl = Some n -> + forall s k ns1 nd1 nexits1, + find_label lbl s k = Some (s', k') -> + tr_stmt c map s ns1 nd1 nexits1 ngoto nret rret -> + tr_cont c map k nd1 nexits1 ngoto nret rret cs -> + exists ns2, exists nd2, exists nexits2, + c!n = Some(Inop ns2) + /\ tr_stmt c map s' ns2 nd2 nexits2 ngoto nret rret + /\ tr_cont c map k' nd2 nexits2 ngoto nret rret cs. Proof. - intros; red; intros; inv TE. - exists rs; econstructor. - split. constructor. - split. apply star_refl. - auto. -Qed. - -Remark state_for_outcome_stop: - forall ncont1 ncont2 nexits nret rret cs code sp rs m out st, - state_for_outcome ncont1 nexits nret rret cs code sp rs m out st -> - out <> Out_normal -> - state_for_outcome ncont2 nexits nret rret cs code sp rs m out st. -Proof. - intros. inv H; congruence || econstructor; eauto. -Qed. - -Lemma transl_stmt_Sseq_continue_correct: - forall (sp : val) (e : env) (m : mem) (t: trace) (s1 : stmt) - (t1: trace) (e1 : env) (m1 : mem) (s2 : stmt) (t2: trace) - (e2 : env) (m2 : mem) (out : outcome), - exec_stmt ge sp e m s1 t1 e1 m1 Out_normal -> - transl_stmt_prop sp e m s1 t1 e1 m1 Out_normal -> - exec_stmt ge sp e1 m1 s2 t2 e2 m2 out -> - transl_stmt_prop sp e1 m1 s2 t2 e2 m2 out -> - t = t1 ** t2 -> - transl_stmt_prop sp e m (Sseq s1 s2) t e2 m2 out. -Proof. - intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. inv OUT1. - exploit H2; eauto. intros [rs2 [st2 [OUT2 [EX2 ME2]]]]. - exists rs2; exists st2. - split. eauto. - split. eapply star_trans; eauto. - auto. + induction s; intros until nexits1; simpl; try congruence. + (* seq *) + caseEq (find_label lbl s1 (Kseq s2 k)); intros. + inv H1. inv H2. eapply IHs1; eauto. econstructor; eauto. + inv H2. eapply IHs2; eauto. + (* ifthenelse *) + caseEq (find_label lbl s1 k); intros. + inv H1. inv H2. eapply IHs1; eauto. + inv H2. eapply IHs2; eauto. + (* loop *) + intros. inversion H1; subst. + eapply IHs; eauto. econstructor; eauto. + (* block *) + intros. inv H1. + eapply IHs; eauto. econstructor; eauto. + (* label *) + destruct (ident_eq lbl l); intros. + inv H0. inv H1. + assert (n0 = n). change positive with node in H4. congruence. subst n0. + exists ns1; exists nd1; exists nexits1; auto. + inv H1. eapply IHs; eauto. Qed. -Lemma transl_stmt_Sseq_stop_correct: - forall (sp : val) (e : env) (m : mem) (t: trace) (s1 s2 : stmt) (e1 : env) - (m1 : mem) (out : outcome), - exec_stmt ge sp e m s1 t e1 m1 out -> - transl_stmt_prop sp e m s1 t e1 m1 out -> - out <> Out_normal -> - transl_stmt_prop sp e m (Sseq s1 s2) t e1 m1 out. +Theorem transl_step_correct: + forall S1 t S2, CminorSel.step ge S1 t S2 -> + forall R1, match_states S1 R1 -> + exists R2, + (plus RTL.step tge R1 t R2 \/ (star RTL.step tge R1 t R2 /\ lt_state S2 S1)) + /\ match_states S2 R2. Proof. - intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. - exists rs1; exists st1. - split. eapply state_for_outcome_stop; eauto. - auto. -Qed. - -Lemma transl_stmt_Sassign_correct: - forall (sp : val) (e : env) (m : mem) (id : ident) (a : expr) - (v : val), - eval_expr ge sp e m nil a v -> - transl_stmt_prop sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal. -Proof. - intros; red; intros; inv TE. + induction 1; intros R1 MSTATE; inv MSTATE. + + (* skip seq *) + inv TS. inv TK. econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. + + (* skip block *) + inv TS. inv TK. econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. constructor. + + (* skip return *) + inv TS. + assert (c!ncont = Some(Ireturn rret) /\ match_stacks k cs). + inv TK; simpl in H; try contradiction; auto. + destruct H1. + assert (rret = None). + inv TF. unfold ret_reg. rewrite H0. auto. + subst rret. + econstructor; split. + left; apply plus_one. eapply exec_Ireturn. eauto. + simpl. constructor; auto. + + (* assign *) + inv TS. + exploit transl_expr_correct; eauto. + intros [rs' [A [B [C D]]]]. + exploit tr_store_var_correct; eauto. + intros [rs'' [E F]]. + rewrite C in F. + econstructor; split. + right; split. eapply star_trans. eexact A. eexact E. traceEq. Lt_state. + econstructor; eauto. constructor. + + (* store *) + inv TS. + exploit transl_exprlist_correct; eauto. + intros [rs' [A [B [C D]]]]. exploit transl_expr_correct; eauto. - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exploit tr_store_var_correct; eauto. intros [rs2 [EX2 ME2]]. - exists rs2; econstructor. - split. constructor. - split. eapply star_trans. eexact EX1. eexact EX2. traceEq. - congruence. -Qed. - -Lemma transl_stmt_Sstore_correct: - forall (sp : val) (e : env) (m : mem) (chunk : memory_chunk) - (addr: addressing) (al: exprlist) (b: expr) - (vl: list val) (v: val) (vaddr: val) (m' : mem), - eval_exprlist ge sp e m nil al vl -> - eval_expr ge sp e m nil b v -> - eval_addressing ge sp addr vl = Some vaddr -> - storev chunk m vaddr v = Some m' -> - transl_stmt_prop sp e m (Sstore chunk addr al b) E0 e m' Out_normal. -Proof. - intros; red; intros; inv TE. - exploit transl_exprlist_correct; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exploit transl_expr_correct; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. - exists rs2; econstructor. - (* Outcome *) - split. constructor. - (* Exec *) - split. eapply star_trans. eexact EX1. - eapply star_right. eexact EX2. - eapply exec_Istore; eauto. - assert (rs2##rl = rs1##rl). - apply list_map_exten. intros r' IN. symmetry. apply OTHER2. auto. - rewrite H3; rewrite RES1. - rewrite (@eval_addressing_preserved _ _ ge tge). eexact H1. - exact symbols_preserved. - rewrite RES2. auto. - reflexivity. traceEq. - (* Match-env *) - auto. -Qed. + intros [rs'' [E [F [G J]]]]. + assert (rs''##rl = vl). + rewrite <- C. apply list_map_exten. intros. symmetry. apply J. auto. + econstructor; split. + left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity. + eapply exec_Istore with (a := vaddr); eauto. + rewrite H3. rewrite <- H1. apply eval_addressing_preserved. exact symbols_preserved. + rewrite G. eauto. + traceEq. + econstructor; eauto. constructor. -Lemma transl_stmt_Scall_correct: - forall (sp : val) (e : env) (m : mem) (optid : option ident) - (sig : signature) (a : expr) (bl : exprlist) (vf : val) - (vargs : list val) (f : CminorSel.fundef) (t : trace) (m' : mem) - (vres : val) (e' : env), - eval_expr ge sp e m nil a vf -> - eval_exprlist ge sp e m nil bl vargs -> - Genv.find_funct ge vf = Some f -> - CminorSel.funsig f = sig -> - eval_funcall ge m f vargs t m' vres -> - transl_function_prop m f vargs t m' vres -> - e' = set_optvar optid vres e -> - transl_stmt_prop sp e m (Scall optid sig a bl) t e' m' Out_normal. -Proof. - intros; red; intros; inv TE. + (* call *) + inv TS. exploit transl_expr_correct; eauto. - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + intros [rs' [A [B [C D]]]]. exploit transl_exprlist_correct; eauto. - intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. - exploit functions_translated; eauto. intros [tf [TFIND TF]]. - exploit H4; eauto. intro EXF. - exploit (tr_store_optvar_correct (rs2#rd <- vres)); eauto. - apply match_env_update_temp; eauto. - intros [rs3 [EX3 ME3]]. - exists rs3; econstructor. - (* Outcome *) - split. constructor. - (* Exec *) - split. eapply star_trans. eexact EX1. - eapply star_trans. eexact EX2. - eapply star_left. eapply exec_Icall; eauto. - simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. - eapply sig_transl_function; eauto. - eapply star_trans. rewrite RES2. eexact EXF. - eapply star_left. apply exec_return. - eexact EX3. - reflexivity. reflexivity. reflexivity. reflexivity. traceEq. - (* Match-env *) - rewrite Regmap.gss in ME3. auto. -Qed. - -Lemma transl_stmt_Salloc_correct: - forall (sp : val) (e : env) (m : mem) (id : ident) (a : expr) - (n : int) (m' : mem) (b : block), - eval_expr ge sp e m nil a (Vint n) -> - alloc m 0 (Int.signed n) = (m', b) -> - transl_stmt_prop sp e m (Salloc id a) E0 - (PTree.set id (Vptr b Int.zero) e) m' Out_normal. -Proof. - intros; red; intros; inv TE. - exploit transl_expr_correct; eauto. - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exploit (tr_store_var_correct (rs1#rd <- (Vptr b Int.zero))); eauto. - apply match_env_update_temp; eauto. - intros [rs2 [EX2 ME2]]. - exists rs2; econstructor. - (* Outcome *) - split. constructor. - (* Execution *) - split. eapply star_trans. eexact EX1. - eapply star_left. 2: eexact EX2. - eapply exec_Ialloc; eauto. - reflexivity. traceEq. - (* Match-env *) - rewrite Regmap.gss in ME2. auto. -Qed. - -Lemma transl_stmt_Sifthenelse_correct: - forall (sp : val) (e : env) (m : mem) (a : condexpr) (s1 s2 : stmt) - (v : bool) (t : trace) (e' : env) (m' : mem) (out : outcome), - eval_condexpr ge sp e m nil a v -> - exec_stmt ge sp e m (if v then s1 else s2) t e' m' out -> - transl_stmt_prop sp e m (if v then s1 else s2) t e' m' out -> - transl_stmt_prop sp e m (Sifthenelse a s1 s2) t e' m' out. -Proof. - intros; red; intros; inv TE. - exploit transl_condexpr_correct; eauto. - intros [rs1 [EX1 [ME1 OTHER1]]]. - assert (tr_stmt code map (if v then s1 else s2) (if v then ntrue else nfalse) - ncont nexits nret rret). - destruct v; auto. - exploit H1; eauto. intros [rs2 [st2 [OUT2 [EX2 ME2]]]]. - exists rs2; exists st2. - split. eauto. - split. eapply star_trans. eexact EX1. eexact EX2. auto. - auto. -Qed. - -Lemma transl_stmt_Sloop_loop_correct: - forall (sp: val) (e : env) (m : mem) (sl : stmt) (t t1: trace) - (e1 : env) (m1 : mem) (t2: trace) (e2 : env) (m2 : mem) - (out : outcome), - exec_stmt ge sp e m sl t1 e1 m1 Out_normal -> - transl_stmt_prop sp e m sl t1 e1 m1 Out_normal -> - exec_stmt ge sp e1 m1 (Sloop sl) t2 e2 m2 out -> - transl_stmt_prop sp e1 m1 (Sloop sl) t2 e2 m2 out -> - t = t1 ** t2 -> - transl_stmt_prop sp e m (Sloop sl) t e2 m2 out. -Proof. - intros; red; intros; inversion TE. subst. - exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. inv OUT1. - exploit H2; eauto. intros [rs2 [st2 [OUT2 [EX2 ME2]]]]. - exists rs2; exists st2. - split. eauto. - split. eapply star_trans. eexact EX1. - eapply star_left. apply exec_Inop; eauto. eexact EX2. - reflexivity. traceEq. - auto. -Qed. - -Lemma transl_stmt_Sloop_stop_correct: - forall (sp: val) (e : env) (m : mem) (t: trace) (sl : stmt) - (e1 : env) (m1 : mem) (out : outcome), - exec_stmt ge sp e m sl t e1 m1 out -> - transl_stmt_prop sp e m sl t e1 m1 out -> - out <> Out_normal -> - transl_stmt_prop sp e m (Sloop sl) t e1 m1 out. -Proof. - intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. - exists rs1; exists st1. - split. eapply state_for_outcome_stop; eauto. - auto. -Qed. - -Lemma transl_stmt_Sblock_correct: - forall (sp: val) (e : env) (m : mem) (sl : stmt) (t: trace) - (e1 : env) (m1 : mem) (out : outcome), - exec_stmt ge sp e m sl t e1 m1 out -> - transl_stmt_prop sp e m sl t e1 m1 out -> - transl_stmt_prop sp e m (Sblock sl) t e1 m1 (outcome_block out). -Proof. - intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. - exists rs1; exists st1. - split. inv OUT1; simpl; try (econstructor; eauto). - destruct n; simpl in H1. - inv H1. constructor. - constructor. auto. - auto. -Qed. - -Lemma transl_stmt_Sexit_correct: - forall (sp: val) (e : env) (m : mem) (n : nat), - transl_stmt_prop sp e m (Sexit n) E0 e m (Out_exit n). -Proof. - intros; red; intros; inv TE. - exists rs; econstructor. - split. econstructor; eauto. - split. apply star_refl. - auto. -Qed. - -Lemma transl_switch_correct: - forall cs sp rs m i code r nexits t ns, - tr_switch code r nexits t ns -> - rs#r = Vint i -> - exists nd, - star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs m) /\ - nth_error nexits (comptree_match i t) = Some nd. -Proof. - induction 1; intros; simpl. - exists n. split. apply star_refl. auto. - - caseEq (Int.eq i key); intros. - exists nfound; split. - apply star_one. eapply exec_Icond_true; eauto. - simpl. rewrite H2. congruence. auto. - exploit IHtr_switch; eauto. intros [nd [EX MATCH]]. - exists nd; split. - eapply star_step. eapply exec_Icond_false; eauto. - simpl. rewrite H2. congruence. eexact EX. traceEq. - auto. + intros [rs'' [E [F [G J]]]]. + exploit functions_translated; eauto. intros [tf [P Q]]. + econstructor; split. + left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity. + eapply exec_Icall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto. + apply sig_transl_function; auto. + traceEq. + rewrite G. constructor. auto. econstructor; eauto. - caseEq (Int.ltu i key); intros. - exploit IHtr_switch1; eauto. intros [nd [EX MATCH]]. - exists nd; split. - eapply star_step. eapply exec_Icond_true; eauto. - simpl. rewrite H2. congruence. eexact EX. traceEq. - auto. - exploit IHtr_switch2; eauto. intros [nd [EX MATCH]]. - exists nd; split. - eapply star_step. eapply exec_Icond_false; eauto. - simpl. rewrite H2. congruence. eexact EX. traceEq. - auto. -Qed. + (* tailcall *) + inv TS. + exploit transl_expr_correct; eauto. + intros [rs' [A [B [C D]]]]. + exploit transl_exprlist_correct; eauto. + intros [rs'' [E [F [G J]]]]. + exploit functions_translated; eauto. intros [tf [P Q]]. + exploit match_stacks_call_cont; eauto. intros [U V]. + econstructor; split. + left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity. + eapply exec_Itailcall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto. + apply sig_transl_function; auto. + traceEq. + rewrite G. constructor; auto. -Lemma transl_stmt_Sswitch_correct: - forall (sp : val) (e : env) (m : mem) (a : expr) - (cases : list (int * nat)) (default : nat) (n : int), - eval_expr ge sp e m nil a (Vint n) -> - transl_stmt_prop sp e m (Sswitch a cases default) E0 e m - (Out_exit (switch_target n default cases)). -Proof. - intros; red; intros; inv TE. + (* alloc *) + inv TS. exploit transl_expr_correct; eauto. - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exploit transl_switch_correct; eauto. intros [nd [EX2 MO2]]. - exists rs1; econstructor. - split. econstructor. - rewrite (validate_switch_correct _ _ _ H3 n). eauto. - split. eapply star_trans. eexact EX1. eexact EX2. traceEq. - auto. -Qed. - -Lemma transl_stmt_Sreturn_none_correct: - forall (sp: val) (e : env) (m : mem), - transl_stmt_prop sp e m (Sreturn None) E0 e m (Out_return None). -Proof. - intros; red; intros; inv TE. - exists rs; econstructor. - split. constructor. auto. - split. apply star_refl. - auto. -Qed. - -Lemma transl_stmt_Sreturn_some_correct: - forall (sp : val) (e : env) (m : mem) (a : expr) (v : val), - eval_expr ge sp e m nil a v -> - transl_stmt_prop sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v)). -Proof. - intros; red; intros; inv TE. + intros [rs1 [A [B [C D]]]]. + set (rs2 := rs1#rd <- (Vptr b Int.zero)). + assert (match_env map e nil rs2). unfold rs2; eauto with rtlg. + exploit tr_store_var_correct. eauto. auto. eexact H1. + intros [rs3 [E F]]. + unfold rs2 in F. rewrite Regmap.gss in F. + econstructor; split. + left. apply plus_star_trans with E0 (State cs c sp n2 rs2 m') E0. + eapply plus_right. eexact A. unfold rs2. eapply exec_Ialloc; eauto. traceEq. + eexact E. traceEq. + econstructor; eauto. constructor. + + (* seq *) + inv TS. + econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. econstructor; eauto. + + (* ifthenelse *) + inv TS. + exploit transl_condexpr_correct; eauto. + intros [rs' [A [B C]]]. + econstructor; split. + right; split. eexact A. destruct b; Lt_state. + destruct b; econstructor; eauto. + + (* loop *) + inversion TS; subst. + econstructor; split. + left. apply plus_one. eapply exec_Inop; eauto. + econstructor; eauto. + econstructor; eauto. + + (* block *) + inv TS. + econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. econstructor; eauto. + + (* exit seq *) + inv TS. inv TK. + econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. econstructor; eauto. + + (* exit block 0 *) + inv TS. inv TK. simpl in H0. inv H0. + econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. econstructor; eauto. + + (* exit block n+1 *) + inv TS. inv TK. simpl in H0. + econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. econstructor; eauto. + + (* switch *) + inv TS. + exploit transl_expr_correct; eauto. + intros [rs' [A [B [C D]]]]. + exploit transl_switch_correct; eauto. + intros [nd [E F]]. + econstructor; split. + right; split. eapply star_trans. eexact A. eexact E. traceEq. Lt_state. + econstructor; eauto. + rewrite (validate_switch_correct _ _ _ H3 n). constructor. auto. + + (* return none *) + inv TS. + exploit match_stacks_call_cont; eauto. intros [U V]. + econstructor; split. + left; apply plus_one. eapply exec_Ireturn; eauto. + simpl. constructor; auto. + + (* return some *) + inv TS. exploit transl_expr_correct; eauto. - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exists rs1; econstructor. - split. econstructor. reflexivity. auto. - eauto. -Qed. - -Lemma transl_stmt_Stailcall_correct: - forall (sp : block) (e : env) (m : mem) (sig : signature) (a : expr) - (bl : exprlist) (vf : val) (vargs : list val) (f : CminorSel.fundef) - (t : trace) (m' : mem) (vres : val), - eval_expr ge (Vptr sp Int.zero) e m nil a vf -> - eval_exprlist ge (Vptr sp Int.zero) e m nil bl vargs -> - Genv.find_funct ge vf = Some f -> - CminorSel.funsig f = sig -> - eval_funcall ge (free m sp) f vargs t m' vres -> - transl_function_prop (free m sp) f vargs t m' vres -> - transl_stmt_prop (Vptr sp Int.zero) e m (Stailcall sig a bl) t e - m' (Out_tailcall_return vres). -Proof. - intros; red; intros; inv TE. - exploit transl_expr_correct; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exploit transl_exprlist_correct; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. - exploit functions_translated; eauto. intros [tf [TFIND TF]]. - exploit H4; eauto. intro EXF. - exists rs2; econstructor. - split. constructor. - split. - eapply star_trans. eexact EX1. - eapply star_trans. eexact EX2. - eapply star_step. - eapply exec_Itailcall; eauto. - simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. - eapply sig_transl_function; eauto. - rewrite RES2. eexact EXF. - reflexivity. reflexivity. traceEq. - auto. -Qed. - -(** The correctness of the translation then follows by application - of the mutual induction principle for Cminor evaluation derivations - to the lemmas above. *) - -Theorem transl_function_correct: - forall m f vargs t m' vres, - eval_funcall ge m f vargs t m' vres -> - transl_function_prop m f vargs t m' vres. -Proof - (eval_funcall_ind2 ge - transl_function_prop - transl_stmt_prop - - transl_funcall_internal_correct - transl_funcall_external_correct - transl_stmt_Sskip_correct - transl_stmt_Sassign_correct - transl_stmt_Sstore_correct - transl_stmt_Scall_correct - transl_stmt_Salloc_correct - transl_stmt_Sifthenelse_correct - transl_stmt_Sseq_continue_correct - transl_stmt_Sseq_stop_correct - transl_stmt_Sloop_loop_correct - transl_stmt_Sloop_stop_correct - transl_stmt_Sblock_correct - transl_stmt_Sexit_correct - transl_stmt_Sswitch_correct - transl_stmt_Sreturn_none_correct - transl_stmt_Sreturn_some_correct - transl_stmt_Stailcall_correct). - -Theorem transl_stmt_correct: - forall sp e m s t e' m' out, - exec_stmt ge sp e m s t e' m' out -> - transl_stmt_prop sp e m s t e' m' out. -Proof - (exec_stmt_ind2 ge - transl_function_prop - transl_stmt_prop - - transl_funcall_internal_correct - transl_funcall_external_correct - transl_stmt_Sskip_correct - transl_stmt_Sassign_correct - transl_stmt_Sstore_correct - transl_stmt_Scall_correct - transl_stmt_Salloc_correct - transl_stmt_Sifthenelse_correct - transl_stmt_Sseq_continue_correct - transl_stmt_Sseq_stop_correct - transl_stmt_Sloop_loop_correct - transl_stmt_Sloop_stop_correct - transl_stmt_Sblock_correct - transl_stmt_Sexit_correct - transl_stmt_Sswitch_correct - transl_stmt_Sreturn_none_correct - transl_stmt_Sreturn_some_correct - transl_stmt_Stailcall_correct). - -(** ** Semantic preservation for the translation of divering statements *) - -Fixpoint size_stmt (s: stmt) : nat := - match s with - | Sseq s1 s2 => (1 + size_stmt s1 + size_stmt s2)%nat - | Sifthenelse e s1 s2 => (1 + size_stmt s1 + size_stmt s2)%nat - | Sloop s1 => (1 + size_stmt s1)%nat - | Sblock s1 => (1 + size_stmt s1)%nat - | _ => 1%nat - end. - -Theorem transl_function_correct_divergence: - forall m fd vargs t tfd cs, - evalinf_funcall ge m fd vargs t -> - transl_fundef fd = OK tfd -> - forever_N step tge O (Callstate cs tfd vargs m) t. -Proof. - cofix FUNCALL. - assert (STMT: forall sp e m s t, - execinf_stmt ge sp e m s t -> - forall cs code map ns ncont nexits nret rret rs - (MWF: map_wf map) - (TE: tr_stmt code map s ns ncont nexits nret rret) - (ME: match_env map e nil rs), - forever_N step tge (size_stmt s) (State cs code sp ns rs m) t). - cofix STMT; intros. - inv H; inversion TE; subst. - (* Scall *) - destruct (transl_expr_correct _ _ _ _ _ _ H0 - cs _ _ _ _ _ _ _ MWF H7 ME) - as [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - destruct (transl_exprlist_correct _ _ _ _ _ _ H1 - cs _ _ _ _ _ _ _ MWF H8 ME1) - as [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. - destruct (functions_translated _ _ H2) as [tf [TFIND TF]]. - eapply forever_N_star with (p := O). - eapply star_trans. eexact EX1. eexact EX2. reflexivity. - simpl; omega. - eapply forever_N_plus with (p := O). - apply plus_one. eapply exec_Icall; eauto. - simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. - eapply sig_transl_function; eauto. - eapply FUNCALL. rewrite RES2. eexact H4. assumption. - reflexivity. traceEq. - (* Sifthenelse *) - destruct (transl_condexpr_correct _ _ _ _ _ _ H0 - cs _ _ _ _ _ _ _ MWF H11 ME) - as [rs1 [EX1 [ME1 OTHER1]]]. - eapply forever_N_star with (p := size_stmt (if v then s1 else s2)). - eexact EX1. destruct v; simpl; omega. - eapply STMT. eexact H1. eauto. destruct v; eauto. eauto. - traceEq. - (* Sseq, 1 *) - eapply forever_N_star with (p := size_stmt s1). - apply star_refl. simpl; omega. - eapply STMT; eauto. - traceEq. - (* Sseq, 2 *) - destruct (transl_stmt_correct _ _ _ _ _ _ _ _ H0 - cs _ _ _ _ _ _ _ _ MWF H9 ME) - as [rs1 [st1 [OUT1 [EX1 ME1]]]]. - inv OUT1. - eapply forever_N_star with (p := size_stmt s2). - eexact EX1. simpl; omega. - eapply STMT; eauto. - traceEq. - (* Sloop, body *) - eapply forever_N_star with (p := size_stmt s0). - apply star_refl. simpl; omega. - eapply STMT; eauto. - traceEq. - (* Sloop, loop *) - destruct (transl_stmt_correct _ _ _ _ _ _ _ _ H0 - cs _ _ _ _ _ _ _ _ MWF H2 ME) - as [rs1 [st1 [OUT1 [EX1 ME1]]]]. - inv OUT1. - eapply forever_N_plus with (p := size_stmt (Sloop s0)). - eapply plus_right. eexact EX1. eapply exec_Inop; eauto. reflexivity. - eapply STMT; eauto. - traceEq. - (* Sblock *) - eapply forever_N_star with (p := size_stmt s0). - apply star_refl. simpl; omega. - eapply STMT; eauto. - traceEq. - (* Stailcall *) - destruct (transl_expr_correct _ _ _ _ _ _ H0 - cs _ _ _ _ _ _ _ MWF H6 ME) - as [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - destruct (transl_exprlist_correct _ _ _ _ _ _ H1 - cs _ _ _ _ _ _ _ MWF H12 ME1) - as [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. - destruct (functions_translated _ _ H2) as [tf [TFIND TF]]. - eapply forever_N_star with (p := O). - eapply star_trans. eexact EX1. eexact EX2. reflexivity. - simpl; omega. - eapply forever_N_plus with (p := O). - apply plus_one. eapply exec_Itailcall; eauto. - simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. - eapply sig_transl_function; eauto. - eapply FUNCALL. rewrite RES2. eexact H4. assumption. - reflexivity. traceEq. - (* funcall *) - intros. inversion H. subst m0 fd vargs0 t0. - generalize H0; simpl. caseEq (transl_function f); simpl. 2: congruence. - intros tfi EQ1 EQ2. injection EQ2; clear EQ2; intro EQ2. - assert (TR: tr_function f tfi). apply transl_function_charact; auto. - rewrite <- EQ2. inversion TR. subst f0. + intros [rs' [A [B [C D]]]]. + exploit match_stacks_call_cont; eauto. intros [U V]. + econstructor; split. + left; eapply plus_right. eexact A. eapply exec_Ireturn; eauto. traceEq. + simpl. rewrite C. constructor; auto. + + (* label *) + inv TS. + econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. + + (* goto *) + inv TS. inversion TF; subst. + exploit tr_find_label; eauto. eapply tr_cont_call_cont; eauto. + intros [ns2 [nd2 [nexits2 [A [B C]]]]]. + econstructor; split. + left; apply plus_one. eapply exec_Inop; eauto. + econstructor; eauto. + + (* internal call *) + monadInv TF. exploit transl_function_charact; eauto. intro TRF. + inversion TRF. subst f0. + pose (e := set_locals (fn_vars f) (set_params vargs (CminorSel.fn_params f))). pose (rs := init_regs vargs rparams). assert (ME: match_env map2 e nil rs). - rewrite <- H2. unfold rs. - eapply match_init_env_init_reg; eauto. + unfold rs, e. eapply match_init_env_init_reg; eauto. assert (MWF: map_wf map2). - assert (map_valid init_mapping init_state) by apply init_mapping_valid. + assert (map_valid init_mapping s0) by apply init_mapping_valid. exploit (add_vars_valid (CminorSel.fn_params f)); eauto. intros [A B]. eapply add_vars_wf; eauto. eapply add_vars_wf; eauto. apply init_mapping_wf. - eapply forever_N_plus with (p := size_stmt (fn_body f)). - apply plus_one. eapply exec_function_internal; eauto. - simpl. eapply STMT; eauto. - traceEq. + econstructor; split. + left; apply plus_one. eapply exec_function_internal; simpl; eauto. + simpl. econstructor; eauto. + econstructor; eauto. + inversion MS; subst; econstructor; eauto. + + (* external call *) + monadInv TF. + econstructor; split. + left; apply plus_one. eapply exec_function_external; eauto. + constructor; auto. + + (* return *) + inv MS. + set (rs' := (rs#r <- v)). + assert (match_env map e nil rs'). unfold rs'; eauto with rtlg. + exploit tr_store_optvar_correct. eauto. eauto. eexact H. intros [rs'' [A B]]. + econstructor; split. + left; eapply plus_left. constructor. eexact A. traceEq. + econstructor; eauto. constructor. unfold rs' in B. rewrite Regmap.gss in B. auto. Qed. -(** ** Semantic preservation for whole programs. *) +Lemma transl_initial_states: + forall S, CminorSel.initial_state prog S -> + exists R, RTL.initial_state tprog R /\ match_states S R. +Proof. + induction 1. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + econstructor; split. + econstructor. rewrite (transform_partial_program_main _ _ TRANSL). fold tge. + rewrite symbols_preserved. eexact H. + eexact A. + rewrite <- H1. apply sig_transl_function; auto. + rewrite (Genv.init_mem_transf_partial _ _ TRANSL). constructor. auto. constructor. +Qed. -(** The correctness of the translation follows: - if the original Cminor program executes with observable behavior [beh], - then the generated RTL program executes with the same behavior. *) +Lemma transl_final_states: + forall S R r, + match_states S R -> CminorSel.final_state S r -> RTL.final_state R r. +Proof. + intros. inv H0. inv H. inv MS. constructor. +Qed. -Theorem transl_program_correct: +Theorem transf_program_correct: forall (beh: program_behavior), - CminorSel.exec_program prog beh -> - RTL.exec_program tprog beh. + CminorSel.exec_program prog beh -> RTL.exec_program tprog beh. Proof. - intros. inv H. - (* termination *) - exploit function_ptr_translated; eauto. intros [tf [TFIND TRANSLF]]. - exploit transl_function_correct; eauto. intro EX. - econstructor. - econstructor. - rewrite symbols_preserved. - replace (prog_main tprog) with (prog_main prog). eauto. - symmetry; apply transform_partial_program_main with transl_fundef. - exact TRANSL. - eexact TFIND. - generalize (sig_transl_function _ _ TRANSLF). congruence. - unfold fundef; rewrite (Genv.init_mem_transf_partial transl_fundef prog TRANSL). - eexact EX. - constructor. - (* divergence *) - exploit function_ptr_translated; eauto. intros [tf [TFIND TRANSLF]]. - exploit transl_function_correct_divergence; eauto. intro EX. - econstructor. - econstructor. - rewrite symbols_preserved. - replace (prog_main tprog) with (prog_main prog). eauto. - symmetry; apply transform_partial_program_main with transl_fundef. - exact TRANSL. - eexact TFIND. - generalize (sig_transl_function _ _ TRANSLF). congruence. - eapply forever_N_forever. - unfold fundef; rewrite (Genv.init_mem_transf_partial transl_fundef prog TRANSL). - eexact EX. + unfold CminorSel.exec_program, RTL.exec_program; intros. + eapply simulation_star_wf_preservation with (order := lt_state); eauto. + eexact transl_initial_states. + eexact transl_final_states. + apply lt_state_wf. + exact transl_step_correct. Qed. End CORRECTNESS. -- cgit v1.2.3