From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 9 Feb 2006 14:55:48 +0000 Subject: Initial import of compcert git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenproof.v | 1302 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1302 insertions(+) create mode 100644 backend/RTLgenproof.v (limited to 'backend/RTLgenproof.v') diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v new file mode 100644 index 00000000..98462d28 --- /dev/null +++ b/backend/RTLgenproof.v @@ -0,0 +1,1302 @@ +(** Correctness proof for RTL generation: main proof. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Mem. +Require Import Globalenvs. +Require Import Op. +Require Import Registers. +Require Import Cminor. +Require Import RTL. +Require Import RTLgen. +Require Import RTLgenproof1. + +Section CORRECTNESS. + +Variable prog: Cminor.program. +Variable tprog: RTL.program. +Hypothesis TRANSL: transl_program prog = Some tprog. + +Let ge : Cminor.genv := Genv.globalenv prog. +Let tge : RTL.genv := Genv.globalenv tprog. + +(** Relationship between the global environments for the original + Cminor program and the generated RTL program. *) + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + intro. unfold ge, tge. + apply Genv.find_symbol_transf_partial with transl_function. + exact TRANSL. +Qed. + +Lemma function_ptr_translated: + forall (b: block) (f: Cminor.function), + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transl_function f = Some tf. +Proof. + intros. + generalize + (Genv.find_funct_ptr_transf_partial transl_function TRANSL H). + case (transl_function f). + intros tf [A B]. exists tf. tauto. + intros [A B]. elim B. reflexivity. +Qed. + +Lemma functions_translated: + forall (v: val) (f: Cminor.function), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transl_function f = Some tf. +Proof. + intros. + generalize + (Genv.find_funct_transf_partial transl_function TRANSL H). + case (transl_function f). + intros tf [A B]. exists tf. tauto. + intros [A B]. elim B. reflexivity. +Qed. + +(** Correctness of the code generated by [add_move]. *) + +Lemma add_move_correct: + forall r1 r2 sp nd s ns s' rs m, + add_move r1 r2 nd s = OK ns s' -> + exists rs', + exec_instrs tge s'.(st_code) sp ns rs m nd rs' m /\ + rs'#r2 = rs#r1 /\ + (forall r, r <> r2 -> rs'#r = rs#r). +Proof. + intros until m. + unfold add_move. case (Reg.eq r1 r2); intro. + monadSimpl. subst s'; subst r2; subst ns. + exists rs. split. apply exec_refl. split. auto. auto. + intro. exists (rs#r2 <- (rs#r1)). + split. apply exec_one. eapply exec_Iop. eauto with rtlg. + reflexivity. + split. apply Regmap.gss. + intros. apply Regmap.gso; auto. +Qed. + +(** The proof of semantic preservation for the translation of expressions + is a simulation argument based on diagrams of the following form: +<< + I /\ P + e, m, a ------------- ns, rs, m + || | + || |* + || | + \/ v + e', m', v ----------- nd, rs', m' + I /\ Q +>> + where [transl_expr map mut a rd nd s = OK ns s']. + The left vertical arrow represents an evaluation of the expression [a] + (assumption). The right vertical arrow represents the execution of + zero, one or several instructions in the generated RTL flow graph + found in the final state [s'] (conclusion). + + The invariant [I] is the agreement between Cminor environments and + RTL register environment, as captured by [match_envs]. + + The preconditions [P] include the well-formedness of the compilation + environment [mut] and the validity of [rd] as a target register. + + The postconditions [Q] state that in the final register environment + [rs'], register [rd] contains value [v], and most other registers + valid in [s] are unchanged w.r.t. the initial register environment + [rs]. (See below for a precise specification of ``most other + registers''.) + + We formalize this simulation property by the following predicate + parameterized by the Cminor evaluation (left arrow). *) + +Definition transl_expr_correct + (sp: val) (le: letenv) (e: env) (m: mem) (a: expr) + (e': env) (m': mem) (v: val) : Prop := + forall map mut rd nd s ns s' rs + (MWF: map_wf map s) + (TE: transl_expr map mut a rd nd s = OK ns s') + (ME: match_env map e le rs) + (MUT: incl (mutated_expr a) mut) + (TRG: target_reg_ok s map mut a rd), + exists rs', + exec_instrs tge s'.(st_code) sp ns rs m nd rs' m' + /\ match_env map e' le rs' + /\ rs'#rd = v + /\ (forall r, + reg_valid r s -> ~(mutated_reg map mut r) -> + reg_in_map map r \/ r <> rd -> + rs'#r = rs#r). + +(** The simulation properties for lists of expressions and for + conditional expressions are similar. *) + +Definition transl_exprlist_correct + (sp: val) (le: letenv) (e: env) (m: mem) (al: exprlist) + (e': env) (m': mem) (vl: list val) : Prop := + forall map mut rl nd s ns s' rs + (MWF: map_wf map s) + (TE: transl_exprlist map mut al rl nd s = OK ns s') + (ME: match_env map e le rs) + (MUT: incl (mutated_exprlist al) mut) + (TRG: target_regs_ok s map mut al rl), + exists rs', + exec_instrs tge s'.(st_code) sp ns rs m nd rs' m' + /\ match_env map e' le rs' + /\ rs'##rl = vl + /\ (forall r, + reg_valid r s -> ~(mutated_reg map mut r) -> + reg_in_map map r \/ ~(In r rl) -> + rs'#r = rs#r). + +Definition transl_condition_correct + (sp: val) (le: letenv) (e: env) (m: mem) (a: condexpr) + (e': env) (m': mem) (vb: bool) : Prop := + forall map mut ntrue nfalse s ns s' rs + (MWF: map_wf map s) + (TE: transl_condition map mut a ntrue nfalse s = OK ns s') + (ME: match_env map e le rs) + (MUT: incl (mutated_condexpr a) mut), + exists rs', + exec_instrs tge s'.(st_code) sp ns rs m (if vb then ntrue else nfalse) rs' m' + /\ match_env map e' le rs' + /\ (forall r, + reg_valid r s -> ~(mutated_reg map mut r) -> + rs'#r = rs#r). + +(** For statements, we define the following auxiliary predicates + relating the outcome of the Cminor execution with the final node + and value of the return register in the RTL execution. *) + +Definition outcome_node + (out: outcome) + (ncont: node) (nexits: list node) (nret: node) (nd: node) : Prop := + match out with + | Out_normal => ncont = nd + | Out_exit n => nth_error nexits n = Some nd + | Out_return _ => nret = nd + end. + +Definition match_return_reg + (rs: regset) (rret: option reg) (v: val) : Prop := + match rret with + | None => True + | Some r => rs#r = v + end. + +Definition match_return_outcome + (out: outcome) (rret: option reg) (rs: regset) : Prop := + match out with + | Out_normal => True + | Out_exit n => True + | Out_return optv => + match rret, optv with + | None, None => True + | Some r, Some v => rs#r = v + | _, _ => False + end + end. + +(** The simulation diagram for the translation of statements and + lists of statements is of the following form: +<< + I /\ P + e, m, a ------------- ns, rs, m + || | + || |* + || | + \/ v + e', m', out --------- nd, rs', m' + I /\ Q +>> + where [transl_stmt map a ncont nexits nret rret s = OK ns s']. + The left vertical arrow represents an execution of the statement [a] + (assumption). The right vertical arrow represents the execution of + zero, one or several instructions in the generated RTL flow graph + found in the final state [s'] (conclusion). + + The invariant [I] is the agreement between Cminor environments and + RTL register environment, as captured by [match_envs]. + + The preconditions [P] include the well-formedness of the compilation + environment [mut] and the agreement between the outcome [out] + and the end node [nd]. + + The postcondition [Q] states agreement between the outcome [out] + and the value of the return register [rret]. *) + +Definition transl_stmt_correct + (sp: val) (e: env) (m: mem) (a: stmt) + (e': env) (m': mem) (out: outcome) : Prop := + forall map ncont nexits nret rret s ns s' nd rs + (MWF: map_wf map s) + (TE: transl_stmt map a ncont nexits nret rret s = OK ns s') + (ME: match_env map e nil rs) + (OUT: outcome_node out ncont nexits nret nd) + (RRG: return_reg_ok s map rret), + exists rs', + exec_instrs tge s'.(st_code) sp ns rs m nd rs' m' + /\ match_env map e' nil rs' + /\ match_return_outcome out rret rs'. + +Definition transl_stmtlist_correct + (sp: val) (e: env) (m: mem) (al: stmtlist) + (e': env) (m': mem) (out: outcome) : Prop := + forall map ncont nexits nret rret s ns s' nd rs + (MWF: map_wf map s) + (TE: transl_stmtlist map al ncont nexits nret rret s = OK ns s') + (ME: match_env map e nil rs) + (OUT: outcome_node out ncont nexits nret nd) + (RRG: return_reg_ok s map rret), + exists rs', + exec_instrs tge s'.(st_code) sp ns rs m nd rs' m' + /\ match_env map e' nil rs' + /\ match_return_outcome out rret 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_correct + (m: mem) (f: Cminor.function) (vargs: list val) + (m':mem) (vres: val) : Prop := + forall tf + (TE: transl_function f = Some tf), + exec_function tge tf vargs m vres m'. + +(** The correctness of the translation is a huge induction over + the Cminor evaluation derivation for the source program. To keep + the proof manageable, we put each case of the proof in a separate + lemma. There is one lemma for each Cminor evaluation rule. + It takes as hypotheses the premises of the Cminor evaluation rule, + plus the induction hypotheses, that is, the [transl_expr_correct], etc, + corresponding to the evaluations of sub-expressions or sub-statements. *) + +Lemma transl_expr_Evar_correct: + forall (sp: val) (le: letenv) (e: env) (m: mem) (id: ident) (v: val), + e!id = Some v -> + transl_expr_correct sp le e m (Evar id) e m v. +Proof. + intros; red; intros. monadInv TE. intro. + generalize EQ; unfold find_var. caseEq (map_vars map)!id. + intros r' MV; monadSimpl. subst s0; subst r'. + generalize (add_move_correct _ _ sp _ _ _ _ rs m TE0). + intros [rs1 [EX1 [RES1 OTHER1]]]. + exists rs1. +(* Exec *) + split. assumption. +(* Match-env *) + split. inversion TRG. + (* Optimized case rd = r *) + rewrite MV in H5; injection H5; intro; subst r. + apply match_env_exten with rs. + intros. case (Reg.eq r rd); intro. + subst r; assumption. apply OTHER1; assumption. + assumption. + (* General case rd is temp *) + apply match_env_invariant with rs. + assumption. intros. apply OTHER1. red; intro; subst r1. contradiction. +(* Result value *) + split. rewrite RES1. eauto with rtlg. +(* Other regs *) + intros. case (Reg.eq rd r0); intro. + subst r0. inversion TRG. + rewrite MV in H8; injection H8; intro; subst r. apply RES1. + byContradiction. tauto. + apply OTHER1; auto. + + intro; monadSimpl. +Qed. + +Lemma transl_expr_Eop_correct: + forall (sp: val) (le : letenv) (e : env) (m : mem) (op : operation) + (al : exprlist) (e1 : env) (m1 : mem) (vl : list val) + (v: val), + eval_exprlist ge sp le e m al e1 m1 vl -> + transl_exprlist_correct sp le e m al e1 m1 vl -> + eval_operation ge sp op vl = Some v -> + transl_expr_correct sp le e m (Eop op al) e1 m1 v. +Proof. + intros until v. intros EEL TEL EOP. red; intros. + simpl in TE. monadInv TE. intro EQ1. + simpl in MUT. + assert (TRG': target_regs_ok s1 map mut al l); eauto with rtlg. + assert (MWF': map_wf map s1). eauto with rtlg. + generalize (TEL _ _ _ _ _ _ _ _ MWF' EQ1 ME MUT TRG'). + intros [rs1 [EX1 [ME1 [RR1 RO1]]]]. + exists (rs1#rd <- v). +(* Exec *) + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s1. eauto with rtlg. + apply exec_one; eapply exec_Iop. eauto with rtlg. + subst vl. + rewrite (@eval_operation_preserved Cminor.function RTL.function ge tge). + eexact EOP. + exact symbols_preserved. +(* Match-env *) + split. inversion TRG. eauto with rtlg. +(* Result reg *) + split. apply Regmap.gss. +(* Other regs *) + intros. rewrite Regmap.gso. + apply RO1. eauto with rtlg. assumption. + case (In_dec Reg.eq r l); intro. + left. elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r i); intro. + assumption. byContradiction; eauto with rtlg. + right; assumption. + red; intro; subst r. + elim H1; intro. inversion TRG. contradiction. + tauto. +Qed. + +Lemma transl_expr_Eassign_correct: + forall (sp: val) (le : letenv) (e : env) (m : mem) + (id : ident) (a : expr) (e1 : env) (m1 : mem) + (v : val), + eval_expr ge sp le e m a e1 m1 v -> + transl_expr_correct sp le e m a e1 m1 v -> + transl_expr_correct sp le e m (Eassign id a) (PTree.set id v e1) m1 v. +Proof. + intros; red; intros. + simpl in TE. monadInv TE. intro EQ1. + simpl in MUT. + assert (MWF0: map_wf map s1). eauto with rtlg. + assert (MUTa: incl (mutated_expr a) mut). + red. intros. apply MUT. simpl. tauto. + assert (TRGa: target_reg_ok s1 map mut a rd). + inversion TRG. apply target_reg_other; eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ _ MWF0 EQ1 ME MUTa TRGa). + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + generalize (add_move_correct _ _ sp _ _ _ _ rs1 m1 EQ0). + intros [rs2 [EX2 [RES2 OTHER2]]]. + exists rs2. +(* Exec *) + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s1. eauto with rtlg. + exact EX2. +(* Match-env *) + split. + apply match_env_update_var with rs1 r s s0; auto. + congruence. +(* Result *) + split. case (Reg.eq rd r); intro. + subst r. congruence. + rewrite OTHER2; auto. +(* Other regs *) + intros. transitivity (rs1#r0). + apply OTHER2. red; intro; subst r0. + apply H2. red. exists id. split. apply MUT. red; tauto. + generalize EQ; unfold find_var. + destruct ((map_vars map)!id); monadSimpl. congruence. + apply OTHER1. eauto with rtlg. assumption. assumption. +Qed. + +Lemma transl_expr_Eload_correct: + forall (sp: val) (le : letenv) (e : env) (m : mem) + (chunk : memory_chunk) (addr : addressing) + (al : exprlist) (e1 : env) (m1 : mem) (v : val) + (vl : list val) (a: val), + eval_exprlist ge sp le e m al e1 m1 vl -> + transl_exprlist_correct sp le e m al e1 m1 vl -> + eval_addressing ge sp addr vl = Some a -> + Mem.loadv chunk m1 a = Some v -> + transl_expr_correct sp le e m (Eload chunk addr al) e1 m1 v. +Proof. + intros; red; intros. simpl in TE. monadInv TE. intro EQ1. clear TE. + simpl in MUT. + assert (MWF1: map_wf map s1). eauto with rtlg. + assert (TRG1: target_regs_ok s1 map mut al l). eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT TRG1). + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exists (rs1#rd <- v). +(* Exec *) + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s1. eauto with rtlg. + apply exec_one. eapply exec_Iload. eauto with rtlg. + rewrite RES1. rewrite (@eval_addressing_preserved _ _ ge tge). + eexact H1. exact symbols_preserved. assumption. +(* Match-env *) + split. eapply match_env_update_temp. assumption. inversion TRG. assumption. +(* Result *) + split. apply Regmap.gss. +(* Other regs *) + intros. rewrite Regmap.gso. apply OTHER1. + eauto with rtlg. assumption. + case (In_dec Reg.eq r l); intro. + elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r i); intro. + tauto. byContradiction. eauto with rtlg. + tauto. + red; intro; subst r. inversion TRG. tauto. +Qed. + +Lemma transl_expr_Estore_correct: + forall (sp: val) (le : letenv) (e : env) (m : mem) + (chunk : memory_chunk) (addr : addressing) + (al : exprlist) (b : expr) (e1 : env) (m1 : mem) + (vl : list val) (e2 : env) (m2 m3 : mem) + (v : val) (a: val), + eval_exprlist ge sp le e m al e1 m1 vl -> + transl_exprlist_correct sp le e m al e1 m1 vl -> + eval_expr ge sp le e1 m1 b e2 m2 v -> + transl_expr_correct sp le e1 m1 b e2 m2 v -> + eval_addressing ge sp addr vl = Some a -> + Mem.storev chunk m2 a v = Some m3 -> + transl_expr_correct sp le e m (Estore chunk addr al b) e2 m3 v. +Proof. + intros; red; intros. simpl in TE; monadInv TE. intro EQ2; clear TE. + simpl in MUT. + assert (MWF2: map_wf map s2). + apply map_wf_incr with s. + apply state_incr_trans2 with s0 s1; eauto with rtlg. + assumption. + assert (MUT2: incl (mutated_exprlist al) mut). eauto with coqlib. + assert (TRG2: target_regs_ok s2 map mut al l). + apply target_regs_ok_incr with s0; eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ _ MWF2 EQ2 ME MUT2 TRG2). + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + assert (MWF1: map_wf map s1). eauto with rtlg. + assert (MUT1: incl (mutated_expr b) mut). eauto with coqlib. + assert (TRG1: target_reg_ok s1 map mut b rd). + inversion TRG. apply target_reg_other; eauto with rtlg. + generalize (H2 _ _ _ _ _ _ _ _ MWF1 EQ1 ME1 MUT1 TRG1). + intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + exists rs2. +(* Exec *) + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s2. eauto with rtlg. + eapply exec_trans. eexact EX2. + apply exec_instrs_incr with s1. eauto with rtlg. + apply exec_one. eapply exec_Istore. eauto with rtlg. + assert (rs2##l = rs1##l). + apply list_map_exten. intros r' IN. symmetry. apply OTHER2. + eauto with rtlg. eauto with rtlg. + elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r' IN); intro. + tauto. right. apply sym_not_equal. + apply valid_fresh_different with s. inversion TRG; assumption. + assumption. + rewrite H5; rewrite RES1. + rewrite (@eval_addressing_preserved _ _ ge tge). + eexact H3. exact symbols_preserved. + rewrite RES2. assumption. +(* Match-env *) + split. assumption. +(* Result *) + split. assumption. +(* Other regs *) + intro r'; intros. transitivity (rs1#r'). + apply OTHER2. apply reg_valid_incr with s; eauto with rtlg. + assumption. assumption. + apply OTHER1. apply reg_valid_incr with s. + apply state_incr_trans2 with s0 s1; eauto with rtlg. assumption. + assumption. case (In_dec Reg.eq r' l); intro. + elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r' i); intro. + tauto. byContradiction; eauto with rtlg. tauto. +Qed. + +Lemma transl_expr_Ecall_correct: + forall (sp: val) (le : letenv) (e : env) (m : mem) + (sig : signature) (a : expr) (bl : exprlist) + (e1 e2 : env) (m1 m2 m3 : mem) (vf : val) + (vargs : list val) (vres : val) (f : Cminor.function), + eval_expr ge sp le e m a e1 m1 vf -> + transl_expr_correct sp le e m a e1 m1 vf -> + eval_exprlist ge sp le e1 m1 bl e2 m2 vargs -> + transl_exprlist_correct sp le e1 m1 bl e2 m2 vargs -> + Genv.find_funct ge vf = Some f -> + Cminor.fn_sig f = sig -> + eval_funcall ge m2 f vargs m3 vres -> + transl_function_correct m2 f vargs m3 vres -> + transl_expr_correct sp le e m (Ecall sig a bl) e2 m3 vres. +Proof. + intros. red; simpl; intros. + monadInv TE. intro EQ3. clear TE. + assert (MUTa: incl (mutated_expr a) mut). eauto with coqlib. + assert (MUTbl: incl (mutated_exprlist bl) mut). eauto with coqlib. + assert (MWFa: map_wf map s3). + apply map_wf_incr with s. + apply state_incr_trans3 with s0 s1 s2; eauto with rtlg. + assumption. + assert (TRGr: target_reg_ok s3 map mut a r). + apply target_reg_ok_incr with s0. + apply state_incr_trans2 with s1 s2; eauto with rtlg. + eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ _ MWFa EQ3 ME MUTa TRGr). + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + clear MUTa MWFa TRGr. + assert (MWFbl: map_wf map s2). + apply map_wf_incr with s. + apply state_incr_trans2 with s0 s1; eauto with rtlg. + assumption. + assert (TRGl: target_regs_ok s2 map mut bl l). + apply target_regs_ok_incr with s1; eauto with rtlg. + generalize (H2 _ _ _ _ _ _ _ _ MWFbl EQ2 ME1 MUTbl TRGl). + intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + clear MUTbl MWFbl TRGl. + + generalize (functions_translated vf f H3). intros [tf [TFIND TF]]. + generalize (H6 tf TF). intro EXF. + + assert (EX3: exec_instrs tge (st_code s2) sp n rs2 m2 + nd (rs2#rd <- vres) m3). + apply exec_one. eapply exec_Icall. + eauto with rtlg. simpl. replace (rs2#r) with vf. eexact TFIND. + rewrite <- RES1. symmetry. apply OTHER2. + apply reg_valid_incr with s0; eauto with rtlg. + apply target_reg_not_mutated with s0 a. + eauto with rtlg. eauto with rtlg. + assert (MWFs0: map_wf map s0). eauto with rtlg. + case (In_dec Reg.eq r l); intro. + elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWFs0 EQ0 r i); intro. + tauto. byContradiction. apply valid_fresh_absurd with r s0. + eauto with rtlg. assumption. + tauto. + generalize TF. unfold transl_function. + destruct (transl_fun f init_state). + intro; discriminate. destruct p. intros. injection TF0. intro. + rewrite <- H7; simpl. auto. + rewrite RES2. assumption. + + exists (rs2#rd <- vres). +(* Exec *) + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s3. eauto with rtlg. + eapply exec_trans. eexact EX2. + apply exec_instrs_incr with s2. eauto with rtlg. + exact EX3. +(* Match env *) + split. apply match_env_update_temp. assumption. + inversion TRG. assumption. +(* Result *) + split. apply Regmap.gss. +(* Other regs *) + intros. + rewrite Regmap.gso. transitivity (rs1#r0). + apply OTHER2. + apply reg_valid_incr with s. + apply state_incr_trans2 with s0 s1; eauto with rtlg. + assumption. + assumption. + assert (MWFs0: map_wf map s0). eauto with rtlg. + case (In_dec Reg.eq r0 l); intro. + elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWFs0 EQ0 r0 i); intro. + tauto. byContradiction. apply valid_fresh_absurd with r0 s0. + eauto with rtlg. assumption. + tauto. + apply OTHER1. + apply reg_valid_incr with s. + apply state_incr_trans3 with s0 s1 s2; eauto with rtlg. + assumption. + assumption. + case (Reg.eq r0 r); intro. + subst r0. + elim (alloc_reg_fresh_or_in_map _ _ _ _ _ _ MWF EQ); intro. + tauto. byContradiction; eauto with rtlg. + tauto. + red; intro; subst r0. + inversion TRG. tauto. +Qed. + +Lemma transl_expr_Econdition_correct: + forall (sp: val) (le : letenv) (e : env) (m : mem) + (a : condexpr) (b c : expr) (e1 : env) (m1 : mem) + (v1 : bool) (e2 : env) (m2 : mem) (v2 : val), + eval_condexpr ge sp le e m a e1 m1 v1 -> + transl_condition_correct sp le e m a e1 m1 v1 -> + eval_expr ge sp le e1 m1 (if v1 then b else c) e2 m2 v2 -> + transl_expr_correct sp le e1 m1 (if v1 then b else c) e2 m2 v2 -> + transl_expr_correct sp le e m (Econdition a b c) e2 m2 v2. +Proof. + intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE. + simpl in MUT. + + assert (MWF1: map_wf map s1). + apply map_wf_incr with s. eauto with rtlg. assumption. + assert (MUT1: incl (mutated_condexpr a) mut). eauto with coqlib. + generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT1). + intros [rs1 [EX1 [ME1 OTHER1]]]. + destruct v1. + + assert (MWF0: map_wf map s0). eauto with rtlg. + assert (MUT0: incl (mutated_expr b) mut). eauto with coqlib. + assert (TRG0: target_reg_ok s0 map mut b rd). + inversion TRG. apply target_reg_other; eauto with rtlg. + generalize (H2 _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 MUT0 TRG0). + intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + exists rs2. +(* Exec *) + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s1. eauto with rtlg. + exact EX2. +(* Match-env *) + split. assumption. +(* Result value *) + split. assumption. +(* Other regs *) + intros. transitivity (rs1#r). + apply OTHER2; auto. eauto with rtlg. + apply OTHER1; auto. apply reg_valid_incr with s. + apply state_incr_trans with s0; eauto with rtlg. assumption. + + assert (MUTc: incl (mutated_expr c) mut). eauto with coqlib. + assert (TRGc: target_reg_ok s map mut c rd). + inversion TRG. apply target_reg_other; auto. + generalize (H2 _ _ _ _ _ _ _ _ MWF EQ ME1 MUTc TRGc). + intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + exists rs2. +(* Exec *) + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s0. eauto with rtlg. + exact EX2. +(* Match-env *) + split. assumption. +(* Result value *) + split. assumption. +(* Other regs *) + intros. transitivity (rs1#r). + apply OTHER2; auto. eauto with rtlg. + apply OTHER1; auto. apply reg_valid_incr with s. + apply state_incr_trans2 with s0 s1; eauto with rtlg. assumption. +Qed. + +Lemma transl_expr_Elet_correct: + forall (sp: val) (le : letenv) (e : env) (m : mem) + (a b : expr) (e1 : env) (m1 : mem) (v1 : val) + (e2 : env) (m2 : mem) (v2 : val), + eval_expr ge sp le e m a e1 m1 v1 -> + transl_expr_correct sp le e m a e1 m1 v1 -> + eval_expr ge sp (v1 :: le) e1 m1 b e2 m2 v2 -> + transl_expr_correct sp (v1 :: le) e1 m1 b e2 m2 v2 -> + transl_expr_correct sp le e m (Elet a b) e2 m2 v2. +Proof. + intros; red; intros. + simpl in TE; monadInv TE. intro EQ1. + simpl in MUT. + assert (MWF1: map_wf map s1). eauto with rtlg. + assert (MUT1: incl (mutated_expr a) mut). eauto with coqlib. + assert (TRG1: target_reg_ok s1 map mut a r). + eapply target_reg_other; eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT1 TRG1). + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + assert (MWF2: map_wf (add_letvar map r) s0). + apply add_letvar_wf; eauto with rtlg. + assert (MUT2: incl (mutated_expr b) mut). eauto with coqlib. + assert (ME2: match_env (add_letvar map r) e1 (v1 :: le) rs1). + apply match_env_letvar; assumption. + assert (TRG2: target_reg_ok s0 (add_letvar map r) mut b rd). + inversion TRG. apply target_reg_other. + unfold reg_in_map, add_letvar; simpl. red; intro. + elim H10; intro. apply H3. left. assumption. + elim H11; intro. apply valid_fresh_absurd with rd s. + assumption. rewrite <- H12. eauto with rtlg. + apply H3. right. assumption. + eauto with rtlg. + generalize (H2 _ _ _ _ _ _ _ _ MWF2 EQ0 ME2 MUT2 TRG2). + intros [rs2 [EX2 [ME3 [RES2 OTHER2]]]]. + exists rs2. +(* Exec *) + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s1. eauto with rtlg. exact EX2. +(* Match-env *) + split. apply mk_match_env. exact (me_vars _ _ _ _ ME3). + generalize (me_letvars _ _ _ _ ME3). + unfold add_letvar; simpl. intro X; injection X; auto. +(* Result *) + split. assumption. +(* Other regs *) + intros. transitivity (rs1#r0). + apply OTHER2. eauto with rtlg. + unfold mutated_reg. unfold add_letvar; simpl. assumption. + elim H5; intro. left. + unfold reg_in_map, add_letvar; simpl. + unfold reg_in_map in H6; tauto. + tauto. + apply OTHER1. eauto with rtlg. + assumption. + right. red; intro. apply valid_fresh_absurd with r0 s. + assumption. rewrite H6. eauto with rtlg. +Qed. + +Lemma transl_expr_Eletvar_correct: + forall (sp: val) (le : list val) (e : env) + (m : mem) (n : nat) (v : val), + nth_error le n = Some v -> + transl_expr_correct sp le e m (Eletvar n) e m v. +Proof. + intros; red; intros. + simpl in TE; monadInv TE. intro EQ1. + generalize EQ. unfold find_letvar. + caseEq (nth_error (map_letvars map) n). + intros r0 NE; monadSimpl. subst s0; subst r0. + generalize (add_move_correct _ _ sp _ _ _ _ rs m EQ1). + intros [rs1 [EX1 [RES1 OTHER1]]]. + exists rs1. +(* Exec *) + split. exact EX1. +(* Match-env *) + split. inversion TRG. + assert (r = rd). congruence. + subst r. apply match_env_exten with rs. + intros. case (Reg.eq r rd); intro. subst r; auto. auto. auto. + apply match_env_invariant with rs. auto. + intros. apply OTHER1. red;intro;subst r1. contradiction. +(* Result *) + split. rewrite RES1. + generalize H. rewrite <- (me_letvars _ _ _ _ ME). + change positive with reg. + rewrite list_map_nth. rewrite NE. simpl. congruence. +(* Other regs *) + intros. inversion TRG. + assert (r = rd). congruence. subst r. + case (Reg.eq r0 rd); intro. subst r0; auto. auto. + apply OTHER1. red; intro; subst r0. tauto. + + intro; monadSimpl. +Qed. + +Lemma transl_condition_CEtrue_correct: + forall (sp: val) (le : letenv) (e : env) (m : mem), + transl_condition_correct sp le e m CEtrue e m true. +Proof. + intros; red; intros. simpl in TE; monadInv TE. subst ns. + exists rs. split. apply exec_refl. split. auto. auto. +Qed. + +Lemma transl_condition_CEfalse_correct: + forall (sp: val) (le : letenv) (e : env) (m : mem), + transl_condition_correct sp le e m CEfalse e m false. +Proof. + intros; red; intros. simpl in TE; monadInv TE. subst ns. + exists rs. split. apply exec_refl. split. auto. auto. +Qed. + +Lemma transl_condition_CEcond_correct: + forall (sp: val) (le : letenv) (e : env) (m : mem) + (cond : condition) (al : exprlist) (e1 : env) + (m1 : mem) (vl : list val) (b : bool), + eval_exprlist ge sp le e m al e1 m1 vl -> + transl_exprlist_correct sp le e m al e1 m1 vl -> + eval_condition cond vl = Some b -> + transl_condition_correct sp le e m (CEcond cond al) e1 m1 b. +Proof. + intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE. + assert (MWF1: map_wf map s1). eauto with rtlg. + simpl in MUT. + assert (TRG: target_regs_ok s1 map mut al l). + eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT TRG). + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exists rs1. +(* Exec *) + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s1. eauto with rtlg. + apply exec_one. + destruct b. + eapply exec_Icond_true. eauto with rtlg. + rewrite RES1. assumption. + eapply exec_Icond_false. eauto with rtlg. + rewrite RES1. assumption. +(* Match-env *) + split. assumption. +(* Regs *) + intros. apply OTHER1. eauto with rtlg. assumption. + case (In_dec Reg.eq r l); intro. + elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r i); intro. + tauto. byContradiction; eauto with rtlg. + tauto. +Qed. + +Lemma transl_condition_CEcondition_correct: + forall (sp: val) (le : letenv) (e : env) (m : mem) + (a b c : condexpr) (e1 : env) (m1 : mem) + (vb1 : bool) (e2 : env) (m2 : mem) (vb2 : bool), + eval_condexpr ge sp le e m a e1 m1 vb1 -> + transl_condition_correct sp le e m a e1 m1 vb1 -> + eval_condexpr ge sp le e1 m1 (if vb1 then b else c) e2 m2 vb2 -> + transl_condition_correct sp le e1 m1 (if vb1 then b else c) e2 m2 vb2 -> + transl_condition_correct sp le e m (CEcondition a b c) e2 m2 vb2. +Proof. + intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE. + simpl in MUT. + assert (MWF1: map_wf map s1). eauto with rtlg. + assert (MUTa: incl (mutated_condexpr a) mut). eauto with coqlib. + generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUTa). + intros [rs1 [EX1 [ME1 OTHER1]]]. + destruct vb1. + + assert (MWF0: map_wf map s0). eauto with rtlg. + assert (MUTb: incl (mutated_condexpr b) mut). eauto with coqlib. + generalize (H2 _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 MUTb). + intros [rs2 [EX2 [ME2 OTHER2]]]. + exists rs2. + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s1. eauto with rtlg. + exact EX2. + split. assumption. + intros. transitivity (rs1#r). + apply OTHER2; eauto with rtlg. + apply OTHER1; eauto with rtlg. + + assert (MUTc: incl (mutated_condexpr c) mut). eauto with coqlib. + generalize (H2 _ _ _ _ _ _ _ _ MWF EQ ME1 MUTc). + intros [rs2 [EX2 [ME2 OTHER2]]]. + exists rs2. + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s0. eauto with rtlg. + exact EX2. + split. assumption. + intros. transitivity (rs1#r). + apply OTHER2; eauto with rtlg. + apply OTHER1; eauto with rtlg. +Qed. + +Lemma transl_exprlist_Enil_correct: + forall (sp: val) (le : letenv) (e : env) (m : mem), + transl_exprlist_correct sp le e m Enil e m nil. +Proof. + intros; red; intros. + generalize TE. simpl. destruct rl; monadSimpl. + subst s'; subst ns. exists rs. + split. apply exec_refl. + split. assumption. + split. reflexivity. + intros. reflexivity. +Qed. + +Lemma transl_exprlist_Econs_correct: + forall (sp: val) (le : letenv) (e : env) (m : mem) + (a : expr) (bl : exprlist) (e1 : env) (m1 : mem) + (v : val) (e2 : env) (m2 : mem) (vl : list val), + eval_expr ge sp le e m a e1 m1 v -> + transl_expr_correct sp le e m a e1 m1 v -> + eval_exprlist ge sp le e1 m1 bl e2 m2 vl -> + transl_exprlist_correct sp le e1 m1 bl e2 m2 vl -> + transl_exprlist_correct sp le e m (Econs a bl) e2 m2 (v :: vl). +Proof. + intros. red. intros. + inversion TRG. + rewrite <- H10 in TE. simpl in TE. monadInv TE. intro EQ1. + simpl in MUT. + assert (MUT1: incl (mutated_expr a) mut); eauto with coqlib. + assert (MUT2: incl (mutated_exprlist bl) mut); eauto with coqlib. + assert (MWF1: map_wf map s1); eauto with rtlg. + assert (TRG1: target_reg_ok s1 map mut a r); eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT1 TRG1). + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + generalize (H2 _ _ _ _ _ _ _ _ MWF EQ ME1 MUT2 H11). + intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + exists rs2. +(* Exec *) + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s1. eauto with rtlg. assumption. +(* Match-env *) + split. assumption. +(* Results *) + split. simpl. rewrite RES2. rewrite OTHER2. rewrite RES1. + reflexivity. + eauto with rtlg. + eauto with rtlg. + assumption. +(* Other regs *) + simpl. intros. + transitivity (rs1#r0). + apply OTHER2; auto. tauto. + apply OTHER1; auto. eauto with rtlg. + elim H14; intro. left; assumption. right; apply sym_not_equal; tauto. +Qed. + +Lemma transl_funcall_correct: + forall (m : mem) (f : Cminor.function) (vargs : list val) + (m1 : mem) (sp : block) (e e2 : env) (m2 : mem) + (out : outcome) (vres : val), + Mem.alloc m 0 (fn_stackspace f) = (m1, sp) -> + set_locals (Cminor.fn_vars f) (set_params vargs (Cminor.fn_params f)) = e -> + exec_stmtlist ge (Vptr sp Int.zero) e m1 (fn_body f) e2 m2 out -> + transl_stmtlist_correct (Vptr sp Int.zero) e m1 (fn_body f) e2 m2 out -> + outcome_result_value out f.(Cminor.fn_sig).(sig_res) vres -> + transl_function_correct m f vargs (Mem.free m2 sp) vres. +Proof. + intros; red; intros. + generalize TE. unfold transl_function. + caseEq (transl_fun f init_state). + intros; discriminate. + intros ns s. unfold transl_fun. monadSimpl. + subst ns. intros EQ4. injection EQ4; intro TF; clear EQ4. + subst s4. + + pose (rs := init_regs vargs x). + assert (ME: match_env y0 e nil rs). + rewrite <- H0. unfold rs. + eapply match_init_env_init_reg; eauto. + + assert (OUT: outcome_node out n nil n n). + red. generalize H3. unfold outcome_result_value. + destruct out; contradiction || auto. + + assert (MWF1: map_wf y0 s1). + eapply add_vars_wf. eexact EQ0. + eapply add_vars_wf. eexact EQ. + apply init_mapping_wf. + + assert (MWF: map_wf y0 s3). + apply map_wf_incr with s1. apply state_incr_trans with s2; eauto with rtlg. + assumption. + + assert (RRG: return_reg_ok s3 y0 (ret_reg (Cminor.fn_sig f) r)). + apply return_reg_ok_incr with s2. eauto with rtlg. + apply new_reg_return_ok with s1; assumption. + + generalize (H2 _ _ _ _ _ _ _ _ _ rs MWF EQ3 ME OUT RRG). + intros [rs1 [EX1 [ME1 MR1]]]. + + apply exec_funct with m1 n rs1 (ret_reg (Cminor.fn_sig f) r). + rewrite <- TF; simpl; assumption. + rewrite <- TF; simpl. exact EX1. + rewrite <- TF; simpl. apply instr_at_incr with s3. + eauto with rtlg. discriminate. eauto with rtlg. + generalize MR1. unfold match_return_outcome. + generalize H3. unfold outcome_result_value. + unfold ret_reg; destruct (sig_res (Cminor.fn_sig f)). + unfold regmap_optget. destruct out; try contradiction. + destruct o; try contradiction. intros; congruence. + unfold regmap_optget. destruct out; contradiction||auto. + destruct o; contradiction||auto. +Qed. + +Lemma transl_stmt_Sexpr_correct: + forall (sp: val) (e : env) (m : mem) (a : expr) + (e1 : env) (m1 : mem) (v : val), + eval_expr ge sp nil e m a e1 m1 v -> + transl_expr_correct sp nil e m a e1 m1 v -> + transl_stmt_correct sp e m (Sexpr a) e1 m1 Out_normal. +Proof. + intros; red; intros. + simpl in OUT. subst nd. + unfold transl_stmt in TE. monadInv TE. intro EQ1. + assert (MWF0: map_wf map s0). eauto with rtlg. + assert (TRG: target_reg_ok s0 map (mutated_expr a) a r). eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ _ MWF0 EQ1 ME (incl_refl (mutated_expr a)) TRG). + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exists rs1; simpl; tauto. +Qed. + +Lemma transl_stmt_Sifthenelse_correct: + forall (sp: val) (e : env) (m : mem) (a : condexpr) + (sl1 sl2 : stmtlist) (e1 : env) (m1 : mem) + (v1 : bool) (e2 : env) (m2 : mem) (out : outcome), + eval_condexpr ge sp nil e m a e1 m1 v1 -> + transl_condition_correct sp nil e m a e1 m1 v1 -> + exec_stmtlist ge sp e1 m1 (if v1 then sl1 else sl2) e2 m2 out -> + transl_stmtlist_correct sp e1 m1 (if v1 then sl1 else sl2) e2 m2 out -> + transl_stmt_correct sp e m (Sifthenelse a sl1 sl2) e2 m2 out. +Proof. + intros; red; intros until rs; intro MWF. + simpl. case (more_likely a sl1 sl2); monadSimpl; intro EQ2; intros. + assert (MWF1: map_wf map s1). eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ rs MWF1 EQ2 ME (incl_refl _)). + intros [rs1 [EX1 [ME1 OTHER1]]]. + destruct v1. + assert (MWF0: map_wf map s0). eauto with rtlg. + assert (RRG0: return_reg_ok s0 map rret). eauto with rtlg. + generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 OUT RRG0). + intros [rs2 [EX2 [ME2 MRE2]]]. + exists rs2. split. + eapply exec_trans. eexact EX1. apply exec_instrs_incr with s1. + eauto with rtlg. exact EX2. + tauto. + generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF EQ ME1 OUT RRG). + intros [rs2 [EX2 [ME2 MRE2]]]. + exists rs2. split. + eapply exec_trans. eexact EX1. apply exec_instrs_incr with s0. + eauto with rtlg. exact EX2. + tauto. + + assert (MWF1: map_wf map s1). eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ rs MWF1 EQ2 ME (incl_refl _)). + intros [rs1 [EX1 [ME1 OTHER1]]]. + destruct v1. + generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF EQ ME1 OUT RRG). + intros [rs2 [EX2 [ME2 MRE2]]]. + exists rs2. split. + eapply exec_trans. eexact EX1. apply exec_instrs_incr with s0. + eauto with rtlg. exact EX2. + tauto. + assert (MWF0: map_wf map s0). eauto with rtlg. + assert (RRG0: return_reg_ok s0 map rret). eauto with rtlg. + generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 OUT RRG0). + intros [rs2 [EX2 [ME2 MRE2]]]. + exists rs2. split. + eapply exec_trans. eexact EX1. apply exec_instrs_incr with s1. + eauto with rtlg. exact EX2. + tauto. +Qed. + +Lemma transl_stmt_Sloop_loop_correct: + forall (sp: val) (e : env) (m : mem) (sl : stmtlist) + (e1 : env) (m1 : mem) (e2 : env) (m2 : mem) + (out : outcome), + exec_stmtlist ge sp e m sl e1 m1 Out_normal -> + transl_stmtlist_correct sp e m sl e1 m1 Out_normal -> + exec_stmt ge sp e1 m1 (Sloop sl) e2 m2 out -> + transl_stmt_correct sp e1 m1 (Sloop sl) e2 m2 out -> + transl_stmt_correct sp e m (Sloop sl) e2 m2 out. +Proof. + intros; red; intros. + generalize TE. simpl. monadSimpl. subst s2; subst n0. intros. + assert (MWF0: map_wf map s0). apply map_wf_incr with s. + eapply reserve_instr_incr; eauto. + assumption. + assert (OUT0: outcome_node Out_normal n nexits nret n). + unfold outcome_node. auto. + assert (RRG0: return_reg_ok s0 map rret). + apply return_reg_ok_incr with s. + eapply reserve_instr_incr; eauto. + assumption. + generalize (H0 _ _ _ _ _ _ _ _ _ _ MWF0 EQ0 ME OUT0 RRG0). + intros [rs1 [EX1 [ME1 MR1]]]. + generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF TE ME1 OUT RRG). + intros [rs2 [EX2 [ME2 MR2]]]. + exists rs2. + split. eapply exec_trans. + apply exec_instrs_extends with s1. + eapply update_instr_extends. + eexact EQ. eauto with rtlg. eexact EQ1. eexact EX1. + apply exec_trans with ns rs1 m1. + apply exec_one. apply exec_Inop. + generalize EQ1. unfold update_instr. + case (plt n (st_nextnode s1)); intro; monadSimpl. + rewrite <- H4. simpl. apply PTree.gss. + exact EX2. + tauto. +Qed. + +Lemma transl_stmt_Sloop_stop_correct: + forall (sp: val) (e : env) (m : mem) (sl : stmtlist) + (e1 : env) (m1 : mem) (out : outcome), + exec_stmtlist ge sp e m sl e1 m1 out -> + transl_stmtlist_correct sp e m sl e1 m1 out -> + out <> Out_normal -> + transl_stmt_correct sp e m (Sloop sl) e1 m1 out. +Proof. + intros; red; intros. + simpl in TE. monadInv TE. subst s2; subst n0. + assert (MWF0: map_wf map s0). apply map_wf_incr with s. + eapply reserve_instr_incr; eauto. assumption. + assert (OUT0: outcome_node out n nexits nret nd). + generalize OUT. unfold outcome_node. + destruct out; auto. elim H1; auto. + assert (RRG0: return_reg_ok s0 map rret). + apply return_reg_ok_incr with s. + eapply reserve_instr_incr; eauto. + assumption. + generalize (H0 _ _ _ _ _ _ _ _ _ _ MWF0 EQ0 ME OUT0 RRG0). + intros [rs1 [EX1 [ME1 MR1]]]. + exists rs1. split. + apply exec_instrs_extends with s1. + eapply update_instr_extends. + eexact EQ. eauto with rtlg. eexact EQ1. eexact EX1. + tauto. +Qed. + +Lemma transl_stmt_Sblock_correct: + forall (sp: val) (e : env) (m : mem) (sl : stmtlist) + (e1 : env) (m1 : mem) (out : outcome), + exec_stmtlist ge sp e m sl e1 m1 out -> + transl_stmtlist_correct sp e m sl e1 m1 out -> + transl_stmt_correct sp e m (Sblock sl) e1 m1 (outcome_block out). +Proof. + intros; red; intros. simpl in TE. + assert (OUT': outcome_node out ncont (ncont :: nexits) nret nd). + generalize OUT. unfold outcome_node, outcome_block. + destruct out. + auto. + destruct n. simpl. intro; unfold value; congruence. + simpl. auto. + auto. + generalize (H0 _ _ _ _ _ _ _ _ _ _ MWF TE ME OUT' RRG). + intros [rs1 [EX1 [ME1 MR1]]]. + exists rs1. + split. assumption. + split. assumption. + generalize MR1. unfold match_return_outcome, outcome_block. + destruct out; auto. + destruct n; simpl; auto. +Qed. + +Lemma transl_stmt_Sexit_correct: + forall (sp: val) (e : env) (m : mem) (n : nat), + transl_stmt_correct sp e m (Sexit n) e m (Out_exit n). +Proof. + intros; red; intros. + generalize TE. simpl. caseEq (nth_error nexits n). + intros n' NE. monadSimpl. subst n'. + simpl in OUT. assert (ns = nd). congruence. subst ns. + exists rs. intuition. apply exec_refl. + intro. monadSimpl. +Qed. + +Lemma transl_stmt_Sreturn_none_correct: + forall (sp: val) (e : env) (m : mem), + transl_stmt_correct sp e m (Sreturn None) e m (Out_return None). +Proof. + intros; red; intros. generalize TE. simpl. + destruct rret; monadSimpl. + simpl in OUT. subst ns; subst nret. + exists rs. intuition. apply exec_refl. +Qed. + +Lemma transl_stmt_Sreturn_some_correct: + forall (sp: val) (e : env) (m : mem) (a : expr) + (e1 : env) (m1 : mem) (v : val), + eval_expr ge sp nil e m a e1 m1 v -> + transl_expr_correct sp nil e m a e1 m1 v -> + transl_stmt_correct sp e m (Sreturn (Some a)) e1 m1 (Out_return (Some v)). +Proof. + intros; red; intros. generalize TE; simpl. + destruct rret. intro EQ. + assert (TRG: target_reg_ok s map (mutated_expr a) a r). + inversion RRG. apply target_reg_other; auto. + generalize (H0 _ _ _ _ _ _ _ _ MWF EQ ME (incl_refl _) TRG). + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + simpl in OUT. subst nd. exists rs1. tauto. + + monadSimpl. +Qed. + +Lemma transl_stmtlist_Snil_correct: + forall (sp: val) (e : env) (m : mem), + transl_stmtlist_correct sp e m Snil e m Out_normal. +Proof. + intros; red; intros. simpl in TE. monadInv TE. + subst s'; subst ns. + simpl in OUT. subst ncont. + exists rs. simpl. intuition. apply exec_refl. +Qed. + +Lemma transl_stmtlist_Scons_continue_correct: + forall (sp: val) (e : env) (m : mem) (s : stmt) + (sl : stmtlist) (e1 : env) (m1 : mem) (e2 : env) + (m2 : mem) (out : outcome), + exec_stmt ge sp e m s e1 m1 Out_normal -> + transl_stmt_correct sp e m s e1 m1 Out_normal -> + exec_stmtlist ge sp e1 m1 sl e2 m2 out -> + transl_stmtlist_correct sp e1 m1 sl e2 m2 out -> + transl_stmtlist_correct sp e m (Scons s sl) e2 m2 out. +Proof. + intros; red; intros. simpl in TE; monadInv TE. intro EQ0. + assert (MWF1: map_wf map s1). eauto with rtlg. + assert (OUTs: outcome_node Out_normal n nexits nret n). + simpl. auto. + assert (RRG1: return_reg_ok s1 map rret). eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ _ _ _ MWF1 EQ0 ME OUTs RRG1). + intros [rs1 [EX1 [ME1 MR1]]]. + generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF EQ ME1 OUT RRG). + intros [rs2 [EX2 [ME2 MR2]]]. + exists rs2. +(* Exec *) + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s1. eauto with rtlg. + exact EX2. +(* Match-env + return *) + tauto. +Qed. + +Lemma transl_stmtlist_Scons_stop_correct: + forall (sp: val) (e : env) (m : mem) (s : stmt) + (sl : stmtlist) (e1 : env) (m1 : mem) (out : outcome), + exec_stmt ge sp e m s e1 m1 out -> + transl_stmt_correct sp e m s e1 m1 out -> + out <> Out_normal -> + transl_stmtlist_correct sp e m (Scons s sl) e1 m1 out. +Proof. + intros; red; intros. + simpl in TE; monadInv TE. intro EQ0; clear TE. + assert (MWF1: map_wf map s1). eauto with rtlg. + assert (OUTs: outcome_node out n nexits nret nd). + destruct out; simpl; auto. tauto. + assert (RRG1: return_reg_ok s1 map rret). eauto with rtlg. + exact (H0 _ _ _ _ _ _ _ _ _ _ MWF1 EQ0 ME OUTs RRG1). +Qed. + +(** The correctness of the translation then follows by application + of the mutual induction principle for Cminor evaluation derivations + to the lemmas above. *) + +Scheme eval_expr_ind_6 := Minimality for eval_expr Sort Prop + with eval_condexpr_ind_6 := Minimality for eval_condexpr Sort Prop + with eval_exprlist_ind_6 := Minimality for eval_exprlist Sort Prop + with eval_funcall_ind_6 := Minimality for eval_funcall Sort Prop + with exec_stmt_ind_6 := Minimality for exec_stmt Sort Prop + with exec_stmtlist_ind_6 := Minimality for exec_stmtlist Sort Prop. + +Theorem transl_function_correctness: + forall m f vargs m' vres, + eval_funcall ge m f vargs m' vres -> + transl_function_correct m f vargs m' vres. +Proof + (eval_funcall_ind_6 ge + transl_expr_correct + transl_condition_correct + transl_exprlist_correct + transl_function_correct + transl_stmt_correct + transl_stmtlist_correct + + transl_expr_Evar_correct + transl_expr_Eassign_correct + transl_expr_Eop_correct + transl_expr_Eload_correct + transl_expr_Estore_correct + transl_expr_Ecall_correct + transl_expr_Econdition_correct + transl_expr_Elet_correct + transl_expr_Eletvar_correct + transl_condition_CEtrue_correct + transl_condition_CEfalse_correct + transl_condition_CEcond_correct + transl_condition_CEcondition_correct + transl_exprlist_Enil_correct + transl_exprlist_Econs_correct + transl_funcall_correct + transl_stmt_Sexpr_correct + transl_stmt_Sifthenelse_correct + transl_stmt_Sloop_loop_correct + transl_stmt_Sloop_stop_correct + transl_stmt_Sblock_correct + transl_stmt_Sexit_correct + transl_stmt_Sreturn_none_correct + transl_stmt_Sreturn_some_correct + transl_stmtlist_Snil_correct + transl_stmtlist_Scons_continue_correct + transl_stmtlist_Scons_stop_correct). + +Theorem transl_program_correct: + forall (r: val), + Cminor.exec_program prog r -> + RTL.exec_program tprog r. +Proof. + intros r [b [f [m [SYMB [FUNC [SIG EVAL]]]]]]. + generalize (function_ptr_translated _ _ FUNC). + intros [tf [TFIND TRANSLF]]. + red; exists b; exists tf; exists m. + split. rewrite symbols_preserved. + replace (prog_main tprog) with (prog_main prog). + assumption. + symmetry; apply transform_partial_program_main with transl_function. + exact TRANSL. + split. exact TFIND. + split. generalize TRANSLF. unfold transl_function. + destruct (transl_fun f init_state). + intro; discriminate. destruct p; intro EQ; injection EQ; intro EQ1. + rewrite <- EQ1. simpl. congruence. + rewrite (Genv.init_mem_transf_partial transl_function prog TRANSL). + exact (transl_function_correctness _ _ _ _ _ EVAL _ TRANSLF). +Qed. + +End CORRECTNESS. -- cgit