From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: 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 --- backend/RTLgenproof.v | 1584 ++++++++++++++++++++++++------------------------- 1 file changed, 786 insertions(+), 798 deletions(-) (limited to 'backend/RTLgenproof.v') diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 2ce961bc..15f305a8 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1,4 +1,4 @@ -(** Correctness proof for RTL generation: main proof. *) +(** Correctness proof for RTL generation. *) Require Import Coqlib. Require Import Maps. @@ -7,144 +7,411 @@ Require Import Integers. Require Import Values. Require Import Mem. Require Import Events. +Require Import Smallstep. Require Import Globalenvs. -Require Import Op. +Require Import Switch. Require Import Registers. Require Import Cminor. +Require Import Op. +Require Import CminorSel. Require Import RTL. Require Import RTLgen. -Require Import RTLgenproof1. +Require Import RTLgenspec. + +(** * Correspondence between Cminor environments and RTL register sets *) + +(** A compilation environment (mapping) is well-formed if + the following properties hold: +- Two distinct Cminor local variables are mapped to distinct pseudo-registers. +- A Cminor local variable and a let-bound variable are mapped to + distinct pseudo-registers. +*) + +Record map_wf (m: mapping) : Prop := + mk_map_wf { + map_wf_inj: + (forall id1 id2 r, + m.(map_vars)!id1 = Some r -> m.(map_vars)!id2 = Some r -> id1 = id2); + map_wf_disj: + (forall id r, + m.(map_vars)!id = Some r -> In r m.(map_letvars) -> False) + }. + +Lemma init_mapping_wf: + map_wf init_mapping. +Proof. + unfold init_mapping; split; simpl. + intros until r. rewrite PTree.gempty. congruence. + tauto. +Qed. + +Lemma add_var_wf: + forall s1 s2 map name r map', + add_var map name s1 = OK (r,map') s2 -> + map_wf map -> map_valid map s1 -> map_wf map'. +Proof. + intros. monadInv H. + apply mk_map_wf; simpl. + intros until r0. repeat rewrite PTree.gsspec. + destruct (peq id1 name); destruct (peq id2 name). + congruence. + intros. inv H. elimtype False. + apply valid_fresh_absurd with r0 s1. + apply H1. left; exists id2; auto. + eauto with rtlg. + intros. inv H2. elimtype False. + apply valid_fresh_absurd with r0 s1. + apply H1. left; exists id1; auto. + eauto with rtlg. + inv H0. eauto. + intros until r0. rewrite PTree.gsspec. + destruct (peq id name). + intros. inv H. + apply valid_fresh_absurd with r0 s1. + apply H1. right; auto. + eauto with rtlg. + inv H0; eauto. +Qed. + +Lemma add_vars_wf: + forall names s1 s2 map map' rl, + add_vars map names s1 = OK (rl,map') s2 -> + map_wf map -> map_valid map s1 -> map_wf map'. +Proof. + induction names; simpl; intros; monadInv H. + auto. + exploit add_vars_valid; eauto. intros [A B]. + eapply add_var_wf; eauto. +Qed. + +Lemma add_letvar_wf: + forall map r, + map_wf map -> ~reg_in_map map r -> map_wf (add_letvar map r). +Proof. + intros. inv H. unfold add_letvar; constructor; simpl. + auto. + intros. elim H1; intro. subst r0. elim H0. left; exists id; auto. + eauto. +Qed. + +(** An RTL register environment matches a Cminor local environment and + let-environment if the value of every local or let-bound variable in + the Cminor environments is identical to the value of the + corresponding pseudo-register in the RTL register environment. *) + +Record match_env + (map: mapping) (e: Cminor.env) (le: Cminor.letenv) (rs: regset) : Prop := + mk_match_env { + me_vars: + (forall id v, + e!id = Some v -> exists r, map.(map_vars)!id = Some r /\ rs#r = v); + me_letvars: + rs##(map.(map_letvars)) = le + }. + +Lemma match_env_find_var: + forall map e le rs id v r, + match_env map e le rs -> + e!id = Some v -> + map.(map_vars)!id = Some r -> + rs#r = v. +Proof. + intros. exploit me_vars; eauto. intros [r' [EQ' RS]]. + replace r with r'. auto. congruence. +Qed. + +Lemma match_env_find_letvar: + forall map e le rs idx v r, + match_env map e le rs -> + List.nth_error le idx = Some v -> + List.nth_error map.(map_letvars) idx = Some r -> + rs#r = v. +Proof. + intros. exploit me_letvars; eauto. intros. + rewrite <- H2 in H0. rewrite list_map_nth in H0. + change reg with positive in H1. rewrite H1 in H0. + simpl in H0. congruence. +Qed. + +Lemma match_env_invariant: + forall map e le rs rs', + match_env map e le rs -> + (forall r, (reg_in_map map r) -> rs'#r = rs#r) -> + match_env map e le rs'. +Proof. + intros. inversion H. apply mk_match_env. + intros. exploit me_vars0; eauto. intros [r [A B]]. + exists r; split. auto. rewrite H0; auto. left; exists id; auto. + rewrite <- me_letvars0. apply list_map_exten. intros. + symmetry. apply H0. right; auto. +Qed. + +(** Matching between environments is preserved when an unmapped register + (not corresponding to any Cminor variable) is assigned in the RTL + execution. *) + +Lemma match_env_update_temp: + forall map e le rs r v, + match_env map e le rs -> + ~(reg_in_map map r) -> + match_env map e le (rs#r <- v). +Proof. + intros. apply match_env_invariant with rs; auto. + intros. case (Reg.eq r r0); intro. + subst r0; contradiction. + apply Regmap.gso; auto. +Qed. +Hint Resolve match_env_update_temp: rtlg. + +(** Matching between environments is preserved by simultaneous + assignment to a Cminor local variable (in the Cminor environments) + and to the corresponding RTL pseudo-register (in the RTL register + environment). *) + +Lemma match_env_update_var: + forall map e le rs id r v, + map_wf map -> + map.(map_vars)!id = Some r -> + match_env map e le rs -> + match_env map (PTree.set id v e) le (rs#r <- v). +Proof. + intros. inversion H. inversion H1. apply mk_match_env. + intros id' v'. rewrite PTree.gsspec. destruct (peq id' id); intros. + subst id'. inv H2. exists r; split. auto. apply PMap.gss. + exploit me_vars0; eauto. intros [r' [A B]]. + exists r'; split. auto. rewrite PMap.gso; auto. + red; intros. subst r'. elim n. eauto. + rewrite <- me_letvars0. apply list_map_exten; intros. + symmetry. apply PMap.gso. red; intros. subst x. eauto. +Qed. + +Lemma match_env_bind_letvar: + forall map e le rs r v, + match_env map e le rs -> + rs#r = v -> + match_env (add_letvar map r) e (v :: le) rs. +Proof. + intros. inv H. unfold add_letvar. apply mk_match_env; simpl; auto. +Qed. + +Lemma match_env_unbind_letvar: + forall map e le rs r v, + match_env (add_letvar map r) e (v :: le) rs -> + match_env map e le rs. +Proof. + unfold add_letvar; intros. inv H. simpl in *. + constructor. auto. congruence. +Qed. + +Lemma match_env_empty: + forall map, + map.(map_letvars) = nil -> + match_env map (PTree.empty val) nil (Regmap.init Vundef). +Proof. + intros. apply mk_match_env. + intros. rewrite PTree.gempty in H0. discriminate. + rewrite H. reflexivity. +Qed. + +(** The assignment of function arguments to local variables (on the Cminor + side) and pseudo-registers (on the RTL side) preserves matching + between environments. *) + +Lemma match_set_params_init_regs: + forall il rl s1 map2 s2 vl, + add_vars init_mapping il s1 = OK (rl, map2) s2 -> + match_env map2 (set_params vl il) nil (init_regs vl rl) + /\ (forall r, reg_fresh r s2 -> (init_regs vl rl)#r = Vundef). +Proof. + induction il; intros. + + inv H. split. apply match_env_empty. auto. intros. + simpl. apply Regmap.gi. + + monadInv H. simpl. + exploit add_vars_valid; eauto. apply init_mapping_valid. intros [A B]. + exploit add_var_valid; eauto. intros [A' B']. clear B'. + monadInv EQ1. + destruct vl as [ | v1 vs]. + (* vl = nil *) + destruct (IHil _ _ _ _ nil EQ) as [ME UNDEF]. inv ME. split. + constructor; simpl. + intros id v. repeat rewrite PTree.gsspec. destruct (peq id a); intros. + subst a. inv H. exists x1; split. auto. apply Regmap.gi. + replace (init_regs nil x) with (Regmap.init Vundef) in me_vars0. eauto. + destruct x; reflexivity. + destruct (map_letvars x0). auto. simpl in me_letvars0. congruence. + intros. apply Regmap.gi. + (* vl = v1 :: vs *) + destruct (IHil _ _ _ _ vs EQ) as [ME UNDEF]. inv ME. split. + constructor; simpl. + intros id v. repeat rewrite PTree.gsspec. destruct (peq id a); intros. + subst a. inv H. exists x1; split. auto. apply Regmap.gss. + exploit me_vars0; eauto. intros [r' [C D]]. + exists r'; split. auto. rewrite Regmap.gso. auto. + apply valid_fresh_different with s. + apply B. left; exists id; auto. + eauto with rtlg. + destruct (map_letvars x0). auto. simpl in me_letvars0. congruence. + intros. rewrite Regmap.gso. apply UNDEF. + apply reg_fresh_decr with s2; eauto with rtlg. + apply sym_not_equal. apply valid_fresh_different with s2; auto. +Qed. + +Lemma match_set_locals: + forall map1 s1, + map_wf map1 -> + forall il rl map2 s2 e le rs, + match_env map1 e le rs -> + (forall r, reg_fresh r s1 -> rs#r = Vundef) -> + add_vars map1 il s1 = OK (rl, map2) s2 -> + match_env map2 (set_locals il e) le rs. +Proof. + induction il; simpl in *; intros. + + inv H2. auto. + + monadInv H2. + exploit IHil; eauto. intro. + monadInv EQ1. + constructor. + intros id v. simpl. repeat rewrite PTree.gsspec. + destruct (peq id a). subst a. intro. + exists x1. split. auto. inv H3. + apply H1. apply reg_fresh_decr with s. + eapply add_vars_incr; eauto. + eauto with rtlg. + intros. eapply me_vars; eauto. + simpl. eapply me_letvars; eauto. +Qed. + +Lemma match_init_env_init_reg: + forall params s0 rparams map1 s1 vars rvars map2 s2 vparams, + add_vars init_mapping params s0 = OK (rparams, map1) s1 -> + add_vars map1 vars s1 = OK (rvars, map2) s2 -> + match_env map2 (set_locals vars (set_params vparams params)) + nil (init_regs vparams rparams). +Proof. + intros. + exploit match_set_params_init_regs; eauto. intros [A B]. + eapply match_set_locals; eauto. + eapply add_vars_wf; eauto. apply init_mapping_wf. + apply init_mapping_valid. +Qed. + +(** * The simulation argument *) + +Require Import Errors. Section CORRECTNESS. -Variable prog: Cminor.program. +Variable prog: CminorSel.program. Variable tprog: RTL.program. -Hypothesis TRANSL: transl_program prog = Some tprog. +Hypothesis TRANSL: transl_program prog = OK tprog. -Let ge : Cminor.genv := Genv.globalenv prog. +Let ge : CminorSel.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. *) + CminorSel 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_fundef. - exact TRANSL. -Qed. +Proof + (Genv.find_symbol_transf_partial transl_fundef _ TRANSL). Lemma function_ptr_translated: - forall (b: block) (f: Cminor.fundef), + forall (b: block) (f: CminorSel.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Some tf. -Proof. - intros. - generalize - (Genv.find_funct_ptr_transf_partial transl_fundef TRANSL H). - case (transl_fundef f). - intros tf [A B]. exists tf. tauto. - intros [A B]. elim B. reflexivity. -Qed. + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. +Proof + (Genv.find_funct_ptr_transf_partial transl_fundef TRANSL). Lemma functions_translated: - forall (v: val) (f: Cminor.fundef), + forall (v: val) (f: CminorSel.fundef), Genv.find_funct ge v = Some f -> exists tf, - Genv.find_funct tge v = Some tf /\ transl_fundef f = Some tf. -Proof. - intros. - generalize - (Genv.find_funct_transf_partial transl_fundef TRANSL H). - case (transl_fundef f). - intros tf [A B]. exists tf. tauto. - intros [A B]. elim B. reflexivity. -Qed. + Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf. +Proof + (Genv.find_funct_transf_partial transl_fundef TRANSL). Lemma sig_transl_function: - forall (f: Cminor.fundef) (tf: RTL.fundef), - transl_fundef f = Some tf -> - RTL.funsig tf = Cminor.funsig f. + forall (f: CminorSel.fundef) (tf: RTL.fundef), + transl_fundef f = OK tf -> + RTL.funsig tf = CminorSel.funsig f. Proof. intros until tf. unfold transl_fundef, transf_partial_fundef. case f; intro. unfold transl_function. - case (transl_fun f0 init_state); intros. + case (transl_fun f0 init_state); simpl; intros. discriminate. - destruct p. inversion H. reflexivity. + destruct p. simpl in H. inversion H. reflexivity. intro. inversion H. 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' -> +Lemma tr_move_correct: + forall r1 ns r2 nd cs code sp rs m, + tr_move code ns r1 nd r2 -> exists rs', - exec_instrs tge s'.(st_code) sp ns rs m E0 nd rs' m /\ + star step tge (State cs code sp ns rs m) E0 (State cs code sp 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. + intros. inv H. + exists rs; split. constructor. auto. + exists (rs#r2 <- (rs#r1)); split. + apply star_one. eapply exec_Iop. eauto. auto. + 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 + e, le, m, a ------------- State cs code sp ns rs m || | - || |* + t|| t|* || | \/ v - e', m', v ----------- nd, rs', m' + e, le, m', v ------------ State cs code sp nd rs' m' I /\ Q >> - where [transl_expr map mut a rd nd s = OK ns s']. + where [tr_expr code map pr a ns nd rd] is assumed to hold. 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). + to value [v]. + The right vertical arrow represents the execution of zero, one or + several instructions in the generated RTL flow graph [code]. - The invariant [I] is the agreement between Cminor environments and - RTL register environment, as captured by [match_envs]. + The invariant [I] is the agreement between CminorSel environments + [e], [le] and the RTL register environment [rs], + 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 precondition [P] is the well-formedness of the compilation + environment [mut]. 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''.) + [rs'], register [rd] contains value [v], and the registers in + the set of preserved registers [pr] are unchanged, as are the registers + in the codomain of [map]. We formalize this simulation property by the following predicate - parameterized by the Cminor evaluation (left arrow). *) + parameterized by the CminorSel evaluation (left arrow). *) Definition transl_expr_correct (sp: val) (le: letenv) (e: env) (m: mem) (a: expr) (t: trace) (m': mem) (v: val) : Prop := - forall map rd nd s ns s' rs - (MWF: map_wf map s) - (TE: transl_expr map a rd nd s = OK ns s') - (ME: match_env map e le rs) - (TRG: target_reg_ok s map a rd), + forall cs code map pr ns nd rd rs + (MWF: map_wf map) + (TE: tr_expr code map pr a ns nd rd) + (ME: match_env map e le rs), exists rs', - exec_instrs tge s'.(st_code) sp ns rs m t nd rs' m' + star step tge (State cs code sp ns rs m) t (State cs code sp nd rs' m') /\ match_env map e le rs' /\ rs'#rd = v - /\ (forall r, - reg_valid r s -> reg_in_map map r \/ r <> rd -> rs'#r = rs#r). + /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r). (** The simulation properties for lists of expressions and for conditional expressions are similar. *) @@ -152,122 +419,113 @@ Definition transl_expr_correct Definition transl_exprlist_correct (sp: val) (le: letenv) (e: env) (m: mem) (al: exprlist) (t: trace) (m': mem) (vl: list val) : Prop := - forall map rl nd s ns s' rs - (MWF: map_wf map s) - (TE: transl_exprlist map al rl nd s = OK ns s') - (ME: match_env map e le rs) - (TRG: target_regs_ok s map al rl), + forall cs code map pr ns nd rl rs + (MWF: map_wf map) + (TE: tr_exprlist code map pr al ns nd rl) + (ME: match_env map e le rs), exists rs', - exec_instrs tge s'.(st_code) sp ns rs m t nd rs' m' + star step tge (State cs code sp ns rs m) t (State cs code sp nd rs' m') /\ match_env map e le rs' /\ rs'##rl = vl - /\ (forall r, - reg_valid r s -> reg_in_map map r \/ ~(In r rl) -> rs'#r = rs#r). + /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r). Definition transl_condition_correct (sp: val) (le: letenv) (e: env) (m: mem) (a: condexpr) (t: trace) (m': mem) (vb: bool) : Prop := - forall map ntrue nfalse s ns s' rs - (MWF: map_wf map s) - (TE: transl_condition map a ntrue nfalse s = OK ns s') + forall cs code map pr ns ntrue nfalse rs + (MWF: map_wf map) + (TE: tr_condition code map pr a ns ntrue nfalse) (ME: match_env map e le rs), exists rs', - exec_instrs tge s'.(st_code) sp ns rs m t (if vb then ntrue else nfalse) rs' m' + star step tge (State cs code sp ns rs m) t + (State cs code sp (if vb then ntrue else nfalse) rs' m') /\ match_env map e le rs' - /\ (forall r, reg_valid r s -> 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. + /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r). + (** The simulation diagram for the translation of statements is of the following form: << I /\ P - e, m, a ------------- ns, rs, m + e, m, a -------------- State cs code sp ns rs m || | - || |* + t|| t|* || | \/ v - e', m', out --------- nd, rs', m' + e', m', out -------------- st' I /\ Q >> - where [transl_stmt map a ncont nexits nret rret s = OK ns s']. + where [tr_stmt code map a ns ncont nexits nret rret] holds. 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). + with outcome [out]. + The right vertical arrow represents the execution of + zero, one or several instructions in the generated RTL flow graph [code]. - The invariant [I] is the agreement between Cminor environments and + The invariant [I] is the agreement between CminorSel 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]. *) + The precondition [P] is the well-formedness of the compilation + environment [mut]. + + The postcondition [Q] characterizes the final RTL state [st']. + It must have memory state [m'] and a register state [rs'] that matches + [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_correct (sp: val) (e: env) (m: mem) (a: stmt) (t: trace) (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 t nd rs' m' - /\ match_env map e' nil rs' - /\ match_return_outcome out rret rs'. + 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. *) + as the original CminorSel function, returns the same value, produces + the same trace of events, and performs the same modifications on the + memory state. *) Definition transl_function_correct - (m: mem) (f: Cminor.fundef) (vargs: list val) - (t: trace) (m':mem) (vres: val) : Prop := - forall tf - (TE: transl_fundef f = Some tf), - exec_function tge tf vargs m t vres m'. + (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'). (** The correctness of the translation is a huge induction over - the Cminor evaluation derivation for the source program. To keep + the CminorSel 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, + lemma. There is one lemma for each CminorSel evaluation rule. + It takes as hypotheses the premises of the CminorSel evaluation rule, plus the induction hypotheses, that is, the [transl_expr_correct], etc, corresponding to the evaluations of sub-expressions or sub-statements. *) @@ -276,35 +534,22 @@ Lemma transl_expr_Evar_correct: e!id = Some v -> transl_expr_correct sp le e m (Evar id) E0 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; subst. - (* Optimized case rd = r *) - rewrite MV in H3; injection H3; 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. congruence. -(* Result value *) - split. rewrite RES1. eauto with rtlg. -(* Other regs *) - intros. destruct (Reg.eq rd r0). - subst r0. inversion TRG; subst. - congruence. - byContradiction. tauto. + intros; red; intros. inv TE. + exploit tr_move_correct; eauto. intros [rs' [A [B C]]]. + exists rs'; split. eauto. + destruct H2 as [D | [E F]]. + (* optimized case *) + subst r. + assert (forall r, rs'#r = rs#r). + intros. destruct (Reg.eq r rd). subst r. auto. auto. + split. eapply match_env_invariant; eauto. + split. rewrite B. eapply match_env_find_var; eauto. auto. - - intro; monadSimpl. + (* general case *) + split. eapply match_env_invariant; eauto. + intros. apply C. congruence. + split. rewrite B. eapply match_env_find_var; eauto. + intros. apply C. intuition congruence. Qed. Lemma transl_expr_Eop_correct: @@ -313,36 +558,25 @@ Lemma transl_expr_Eop_correct: (v: val), eval_exprlist ge sp le e m al t m1 vl -> transl_exprlist_correct sp le e m al t m1 vl -> - eval_operation ge sp op vl = Some v -> + eval_operation ge sp op vl m1 = Some v -> transl_expr_correct sp le e m (Eop op al) t m1 v. Proof. - intros until v. intros EEL TEL EOP. red; intros. - simpl in TE. monadInv TE. intro EQ1. - exploit TEL. 2: eauto. eauto with rtlg. eauto. eauto with rtlg. - intros [rs1 [EX1 [ME1 [RR1 RO1]]]]. + intros; red; intros. inv TE. + exploit H0; eauto. 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. + split. eapply star_right. eexact EX1. + eapply exec_Iop; eauto. subst vl. - rewrite (@eval_operation_preserved Cminor.fundef RTL.fundef ge tge). - eexact EOP. + rewrite (@eval_operation_preserved CminorSel.fundef RTL.fundef ge tge). + auto. exact symbols_preserved. traceEq. (* Match-env *) - split. inversion TRG. eauto with rtlg. + split. eauto with rtlg. (* Result reg *) split. apply Regmap.gss. (* Other regs *) - intros. rewrite Regmap.gso. - apply RO1. eauto with rtlg. - destruct (In_dec Reg.eq r l). - left. elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWF EQ r i); intro. - auto. byContradiction; eauto with rtlg. - right; auto. - red; intro; subst r. - elim H0; intro. inversion TRG. contradiction. - tauto. + intros. rewrite Regmap.gso. auto. intuition congruence. Qed. Lemma transl_expr_Eload_correct: @@ -356,30 +590,19 @@ Lemma transl_expr_Eload_correct: Mem.loadv chunk m1 a = Some v -> transl_expr_correct sp le e m (Eload chunk addr al) t m1 v. Proof. - intros; red; intros. simpl in TE. monadInv TE. intro EQ1. clear TE. - assert (MWF1: map_wf map s1). eauto with rtlg. - assert (TRG1: target_regs_ok s1 map al l). eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG1). - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + intros; red; intros. inv TE. + exploit H0; eauto. 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. + split. eapply star_right. eexact EX1. eapply exec_Iload; eauto. rewrite RES1. rewrite (@eval_addressing_preserved _ _ ge tge). - eexact H1. exact symbols_preserved. assumption. traceEq. + exact H1. exact symbols_preserved. traceEq. (* Match-env *) - split. eapply match_env_update_temp. assumption. inversion TRG. assumption. + split. eauto with rtlg. (* Result *) split. apply Regmap.gss. (* Other regs *) - intros. rewrite Regmap.gso. apply OTHER1. - eauto with rtlg. - 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. + intros. rewrite Regmap.gso. auto. intuition congruence. Qed. Lemma transl_expr_Estore_correct: @@ -397,35 +620,18 @@ Lemma transl_expr_Estore_correct: t = t1 ** t2 -> transl_expr_correct sp le e m (Estore chunk addr al b) t m3 v. Proof. - intros; red; intros. simpl in TE; monadInv TE. intro EQ2; clear TE. - assert (MWF2: map_wf map s2). - apply map_wf_incr with s. - apply state_incr_trans2 with s0 s1; eauto with rtlg. - assumption. - assert (TRG2: target_regs_ok s2 map al l). - apply target_regs_ok_incr with s0; eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ MWF2 EQ2 ME TRG2). - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - assert (MWF1: map_wf map s1). eauto with rtlg. - assert (TRG1: target_reg_ok s1 map b rd). - inversion TRG. apply target_reg_other; eauto with rtlg. - generalize (H2 _ _ _ _ _ _ _ MWF1 EQ1 ME1 TRG1). - intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + intros; red; intros; inv TE. + exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exploit H2; eauto. 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). + 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. - 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 H6; rewrite RES1. + right. apply in_or_app. auto. + rewrite H5; rewrite RES1. rewrite (@eval_addressing_preserved _ _ ge tge). eexact H3. exact symbols_preserved. rewrite RES2. assumption. @@ -435,110 +641,52 @@ Proof. (* Result *) split. assumption. (* Other regs *) - intro r'; intros. transitivity (rs1#r'). - apply OTHER2. apply reg_valid_incr with s; eauto with rtlg. - assumption. - apply OTHER1. apply reg_valid_incr with s. - apply state_incr_trans2 with s0 s1; 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. + intro r'; intros. transitivity (rs1#r'). + apply OTHER2. intuition. + auto. +Qed. Lemma transl_expr_Ecall_correct: forall (sp: val) (le : letenv) (e : env) (m : mem) (sig : signature) (a : expr) (bl : exprlist) (t t1: trace) (m1: mem) (t2: trace) (m2 : mem) (t3: trace) (m3: mem) (vf : val) - (vargs : list val) (vres : val) (f : Cminor.fundef), + (vargs : list val) (vres : val) (f : CminorSel.fundef), eval_expr ge sp le e m a t1 m1 vf -> transl_expr_correct sp le e m a t1 m1 vf -> eval_exprlist ge sp le e m1 bl t2 m2 vargs -> transl_exprlist_correct sp le e m1 bl t2 m2 vargs -> Genv.find_funct ge vf = Some f -> - Cminor.funsig f = sig -> + CminorSel.funsig f = sig -> eval_funcall ge m2 f vargs t3 m3 vres -> transl_function_correct m2 f vargs t3 m3 vres -> t = t1 ** t2 ** t3 -> transl_expr_correct sp le e m (Ecall sig a bl) t m3 vres. Proof. - intros. red; simpl; intros. - monadInv TE. intro EQ3. clear TE. - 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 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 TRGr). - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - clear 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 bl l). - apply target_regs_ok_incr with s1; eauto with rtlg. - generalize (H2 _ _ _ _ _ _ _ MWFbl EQ2 ME1 TRGl). - intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. - clear 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 - t3 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. - 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 (sig_transl_function _ _ TF). congruence. - rewrite RES2. assumption. - + intros; red; intros; inv TE. + exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + exploit functions_translated; eauto. intros [tf [TFIND TF]]. + exploit H6; eauto. intro EXF. 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. - eexact EX3. reflexivity. traceEq. + 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_right. rewrite RES2. eexact EXF. + apply exec_return. reflexivity. reflexivity. reflexivity. traceEq. (* Match env *) - split. apply match_env_update_temp. assumption. - inversion TRG. assumption. + split. eauto with rtlg. (* 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. - 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. - 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. + rewrite Regmap.gso. transitivity (rs1#r). + apply OTHER2. simpl; tauto. + apply OTHER1; auto. + intuition congruence. Qed. Lemma transl_expr_Econdition_correct: @@ -552,52 +700,20 @@ Lemma transl_expr_Econdition_correct: t = t1 ** t2 -> transl_expr_correct sp le e m (Econdition a b c) t m2 v2. Proof. - intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE. - - assert (MWF1: map_wf map s1). - apply map_wf_incr with s. eauto with rtlg. assumption. - generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME). - intros [rs1 [EX1 [ME1 OTHER1]]]. - destruct v1. - - assert (MWF0: map_wf map s0). eauto with rtlg. - assert (TRG0: target_reg_ok s0 map b rd). - inversion TRG. apply target_reg_other; eauto with rtlg. - generalize (H2 _ _ _ _ _ _ _ MWF0 EQ0 ME1 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. - eexact EX2. auto. -(* 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 (TRGc: target_reg_ok s map c rd). - inversion TRG. apply target_reg_other; auto. - generalize (H2 _ _ _ _ _ _ _ MWF EQ ME1 TRGc). - intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + intros; red; intros; inv TE. + exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]]. + assert (tr_expr code map pr (if v1 then b else c) (if v1 then ntrue else nfalse) nd rd). + destruct v1; auto. + exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exists rs2. (* Exec *) - split. eapply exec_trans. eexact EX1. - apply exec_instrs_incr with s0. eauto with rtlg. - eexact EX2. auto. + split. eapply star_trans. eexact EX1. eexact EX2. auto. (* 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. + intros. transitivity (rs1#r); auto. Qed. Lemma transl_expr_Elet_correct: @@ -611,47 +727,25 @@ Lemma transl_expr_Elet_correct: t = t1 ** t2 -> transl_expr_correct sp le e m (Elet a b) t m2 v2. Proof. - intros; red; intros. - simpl in TE; monadInv TE. intro EQ1. - assert (MWF1: map_wf map s1). eauto with rtlg. - assert (TRG1: target_reg_ok s1 map a r). - eapply target_reg_other; eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG1). - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - assert (MWF2: map_wf (add_letvar map r) s0). - apply add_letvar_wf; eauto with rtlg. - assert (ME2: match_env (add_letvar map r) e (v1 :: le) rs1). - apply match_env_letvar; assumption. - assert (TRG2: target_reg_ok s0 (add_letvar map r) b rd). - inversion TRG. apply target_reg_other. - unfold reg_in_map, add_letvar; simpl. red; intro. - elim H10; intro. apply H4. left. assumption. - elim H11; intro. apply valid_fresh_absurd with rd s. - assumption. rewrite <- H12. eauto with rtlg. - apply H4. right. assumption. - eauto with rtlg. - generalize (H2 _ _ _ _ _ _ _ MWF2 EQ0 ME2 TRG2). + intros; red; intros; inv TE. + exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + assert (map_wf (add_letvar map r)). + eapply add_letvar_wf; eauto. + exploit H2; eauto. eapply match_env_bind_letvar; eauto. intros [rs2 [EX2 [ME3 [RES2 OTHER2]]]]. exists rs2. (* Exec *) - split. eapply exec_trans. eexact EX1. - apply exec_instrs_incr with s1. eauto with rtlg. eexact EX2. auto. + split. eapply star_trans. eexact EX1. eexact EX2. auto. (* Match-env *) - split. apply mk_match_env. exact (me_vars _ _ _ _ ME3). - generalize (me_letvars _ _ _ _ ME3). - unfold add_letvar; simpl. intro X; injection X; auto. + split. eapply match_env_unbind_letvar; eauto. (* Result *) split. assumption. (* Other regs *) intros. transitivity (rs1#r0). - apply OTHER2. eauto with rtlg. - elim H5; intro. left. + apply OTHER2. elim H4; intro; auto. unfold reg_in_map, add_letvar; simpl. - unfold reg_in_map in H6; tauto. - tauto. - apply OTHER1. eauto with rtlg. - right. red; intro. apply valid_fresh_absurd with r0 s. - assumption. rewrite H6. eauto with rtlg. + unfold reg_in_map in H5; tauto. + auto. Qed. Lemma transl_expr_Eletvar_correct: @@ -660,35 +754,22 @@ Lemma transl_expr_Eletvar_correct: nth_error le n = Some v -> transl_expr_correct sp le e m (Eletvar n) E0 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]]]. + intros; red; intros; inv TE. + exploit tr_move_correct; eauto. intros [rs1 [EX1 [RES1 OTHER1]]]. exists rs1. (* Exec *) - split. exact EX1. + split. eexact 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. + split. apply match_env_invariant with rs. auto. + intros. destruct H2 as [A | [B C]]. + subst r. destruct (Reg.eq r0 rd). subst r0; auto. auto. + apply OTHER1. intuition congruence. (* Result *) - split. rewrite RES1. - generalize H. rewrite <- (me_letvars _ _ _ _ ME). - change positive with reg. - rewrite list_map_nth. rewrite NE. simpl. congruence. + split. rewrite RES1. eapply match_env_find_letvar; eauto. (* 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. + intros. destruct H2 as [A | [B C]]. + subst r. destruct (Reg.eq r0 rd). subst r0; auto. auto. + apply OTHER1. intuition congruence. Qed. Lemma transl_expr_Ealloc_correct: @@ -700,47 +781,35 @@ Lemma transl_expr_Ealloc_correct: Mem.alloc m1 0 (Int.signed n) = (m2, b) -> transl_expr_correct sp le e m (Ealloc a) t m2 (Vptr b Int.zero). Proof. - intros until b; intros EE TEC ALLOC; red; intros. - simpl in TE. monadInv TE. intro EQ1. - assert (TRG': target_reg_ok s1 map a r); eauto with rtlg. - assert (MWF': map_wf map s1). eauto with rtlg. - generalize (TEC _ _ _ _ _ _ _ MWF' EQ1 ME TRG'). - intros [rs1 [EX1 [ME1 [RR1 RO1]]]]. + intros; red; intros; inv TE. + exploit H0; eauto. intros [rs1 [EX1 [ME1 [RR1 RO1]]]]. exists (rs1#rd <- (Vptr b Int.zero)). (* Exec *) - split. eapply exec_trans. eexact EX1. - apply exec_instrs_incr with s1. eauto with rtlg. - apply exec_one; eapply exec_Ialloc. eauto with rtlg. + split. eapply star_right. eexact EX1. + eapply exec_Ialloc. eauto with rtlg. eexact RR1. assumption. traceEq. (* Match-env *) - split. inversion TRG. eauto with rtlg. + split. eauto with rtlg. (* Result *) split. apply Regmap.gss. (* Other regs *) - intros. rewrite Regmap.gso. - apply RO1. eauto with rtlg. - case (Reg.eq r0 r); intro. - subst r0. left. elim (alloc_reg_fresh_or_in_map _ _ _ _ _ MWF EQ); intro. - auto. byContradiction; eauto with rtlg. - right; assumption. - elim H0; intro. red; intro. subst r0. inversion TRG. contradiction. - auto. + intros. rewrite Regmap.gso. auto. intuition congruence. Qed. Lemma transl_condition_CEtrue_correct: forall (sp: val) (le : letenv) (e : env) (m : mem), transl_condition_correct sp le e m CEtrue E0 m true. Proof. - intros; red; intros. simpl in TE; monadInv TE. subst ns. - exists rs. split. apply exec_refl. split. auto. auto. + intros; red; intros; inv TE. + exists rs. split. apply star_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 E0 m false. Proof. - intros; red; intros. simpl in TE; monadInv TE. subst ns. - exists rs. split. apply exec_refl. split. auto. auto. + intros; red; intros; inv TE. + exists rs. split. apply star_refl. split. auto. auto. Qed. Lemma transl_condition_CEcond_correct: @@ -749,33 +818,24 @@ Lemma transl_condition_CEcond_correct: (m1 : mem) (vl : list val) (b : bool), eval_exprlist ge sp le e m al t1 m1 vl -> transl_exprlist_correct sp le e m al t1 m1 vl -> - eval_condition cond vl = Some b -> + eval_condition cond vl m1 = Some b -> transl_condition_correct sp le e m (CEcond cond al) t1 m1 b. Proof. - intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE. - assert (MWF1: map_wf map s1). eauto with rtlg. - assert (TRG: target_regs_ok s1 map al l). eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG). - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + intros; red; intros; inv TE. + exploit H0; eauto. 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. + split. eapply star_right. eexact EX1. destruct b. - eapply exec_Icond_true. eauto with rtlg. + eapply exec_Icond_true; eauto. rewrite RES1. assumption. - eapply exec_Icond_false. eauto with rtlg. + eapply exec_Icond_false; eauto. rewrite RES1. assumption. traceEq. (* Match-env *) split. assumption. (* Regs *) - intros. apply OTHER1. eauto with rtlg. - 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. + auto. Qed. Lemma transl_condition_CEcondition_correct: @@ -789,47 +849,31 @@ Lemma transl_condition_CEcondition_correct: t = t1 ** t2 -> transl_condition_correct sp le e m (CEcondition a b c) t m2 vb2. Proof. - intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE. - assert (MWF1: map_wf map s1). eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME). - intros [rs1 [EX1 [ME1 OTHER1]]]. - destruct vb1. - - assert (MWF0: map_wf map s0). eauto with rtlg. - generalize (H2 _ _ _ _ _ _ _ MWF0 EQ0 ME1). - intros [rs2 [EX2 [ME2 OTHER2]]]. - exists rs2. - split. eapply exec_trans. eexact EX1. - apply exec_instrs_incr with s1. eauto with rtlg. - eexact EX2. auto. - split. assumption. - intros. transitivity (rs1#r). - apply OTHER2; eauto with rtlg. - apply OTHER1; eauto with rtlg. - - generalize (H2 _ _ _ _ _ _ _ MWF EQ ME1). - intros [rs2 [EX2 [ME2 OTHER2]]]. + intros; red; intros; inv TE. + exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]]. + assert (tr_condition code map pr (if vb1 then b else c) + (if vb1 then ntrue' else nfalse') ntrue nfalse). + destruct vb1; auto. + exploit H2; eauto. intros [rs2 [EX2 [ME2 OTHER2]]]. exists rs2. - split. eapply exec_trans. eexact EX1. - apply exec_instrs_incr with s0. eauto with rtlg. - eexact EX2. auto. - split. assumption. - intros. transitivity (rs1#r). - apply OTHER2; eauto with rtlg. - apply OTHER1; eauto with rtlg. +(* Execution *) + split. eapply star_trans. eexact EX1. eexact EX2. auto. +(* Match-env *) + split. auto. +(* Regs *) + intros. transitivity (rs1#r); auto. Qed. Lemma transl_exprlist_Enil_correct: forall (sp: val) (le : letenv) (e : env) (m : mem), transl_exprlist_correct sp le e m Enil E0 m nil. Proof. - intros; red; intros. - generalize TE. simpl. destruct rl; monadSimpl. - subst s'; subst ns. exists rs. - split. apply exec_refl. + intros; red; intros; inv TE. + exists rs. + split. apply star_refl. split. assumption. split. reflexivity. - intros. reflexivity. + auto. Qed. Lemma transl_exprlist_Econs_correct: @@ -843,93 +887,90 @@ Lemma transl_exprlist_Econs_correct: t = t1 ** t2 -> transl_exprlist_correct sp le e m (Econs a bl) t m2 (v :: vl). Proof. - intros. red. intros. - inversion TRG. - rewrite <- H10 in TE. simpl in TE. monadInv TE. intro EQ1. - assert (MWF1: map_wf map s1); eauto with rtlg. - assert (TRG1: target_reg_ok s1 map a r); eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG1). - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - generalize (H2 _ _ _ _ _ _ _ MWF EQ ME1 H11). - intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + intros; red; intros; inv TE. + exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exists rs2. (* Exec *) - split. eapply exec_trans. eexact EX1. - apply exec_instrs_incr with s1. eauto with rtlg. - eexact EX2. auto. + split. eapply star_trans. eexact EX1. eexact EX2. auto. (* Match-env *) split. assumption. (* Results *) - split. simpl. rewrite RES2. rewrite OTHER2. rewrite RES1. - reflexivity. - eauto with rtlg. - eauto with rtlg. + split. simpl. rewrite RES2. rewrite OTHER2. rewrite RES1. auto. + simpl; tauto. (* Other regs *) - simpl. intros. - transitivity (rs1#r0). - apply OTHER2; auto. tauto. - apply OTHER1; auto. eauto with rtlg. - elim H13; intro. left; assumption. right; apply sym_not_equal; tauto. + intros. transitivity (rs1#r). + apply OTHER2; auto. simpl; tauto. + apply OTHER1; auto. Qed. Lemma transl_funcall_internal_correct: - forall (m : mem) (f : Cminor.function) + 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), + (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 (Cminor.fn_params f)) = e -> + 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_correct (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out -> - outcome_result_value out f.(Cminor.fn_sig).(sig_res) vres -> - transl_function_correct m (Internal f) - vargs t (Mem.free m2 sp) vres. + outcome_result_value out f.(CminorSel.fn_sig).(sig_res) vres -> + transl_function_correct m (Internal f) vargs t + (outcome_free_mem out m2 sp) vres. Proof. intros; red; intros. - generalize TE. unfold transl_fundef, transl_function; simpl. - 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). + 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. + 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. - 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. - - set (rr := ret_reg (Cminor.fn_sig f) r) in *. - assert (RRG: return_reg_ok s3 y0 rr). - apply return_reg_ok_incr with s2. eauto with rtlg. - unfold rr; apply new_reg_return_ok with s1; assumption. - - generalize (H2 _ _ _ _ _ _ _ _ _ rs MWF EQ3 ME OUT RRG). - intros [rs1 [EX1 [ME1 MR1]]]. - - rewrite <- TF. apply exec_funct_internal with m1 n rs1 rr; simpl. - assumption. - exact EX1. - 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 rr, 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. + (* 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. Qed. Lemma transl_funcall_external_correct: @@ -939,17 +980,27 @@ Lemma transl_funcall_external_correct: Proof. intros; red; intros. unfold transl_function in TE; simpl in TE. inversion TE; subst tf. - apply exec_funct_external. auto. + apply star_one. apply exec_function_external. auto. Qed. Lemma transl_stmt_Sskip_correct: forall (sp: val) (e : env) (m : mem), transl_stmt_correct sp e m Sskip E0 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. + 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: @@ -963,22 +1014,13 @@ Lemma transl_stmt_Sseq_continue_correct: t = t1 ** t2 -> transl_stmt_correct sp e m (Sseq s1 s2) t e2 m2 out. Proof. - intros; red; intros. simpl in TE; monadInv TE. intro EQ0. - assert (MWF1: map_wf map s0). eauto with rtlg. - assert (OUTs: outcome_node Out_normal n nexits nret n). - simpl. auto. - assert (RRG1: return_reg_ok s0 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 s0. eauto with rtlg. - eexact EX2. auto. -(* Match-env + return *) - tauto. + 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. Qed. Lemma transl_stmt_Sseq_stop_correct: @@ -989,13 +1031,11 @@ Lemma transl_stmt_Sseq_stop_correct: out <> Out_normal -> transl_stmt_correct sp e m (Sseq s1 s2) t e1 m1 out. Proof. - intros; red; intros. - simpl in TE; monadInv TE. intro EQ0; clear TE. - assert (MWF1: map_wf map s0). eauto with rtlg. - assert (OUTs: outcome_node out n nexits nret nd). - destruct out; simpl; auto. tauto. - assert (RRG1: return_reg_ok s0 map rret). eauto with rtlg. - exact (H0 _ _ _ _ _ _ _ _ _ _ MWF1 EQ0 ME OUTs RRG1). + 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_Sexpr_correct: @@ -1005,14 +1045,11 @@ Lemma transl_stmt_Sexpr_correct: transl_expr_correct sp nil e m a t m1 v -> transl_stmt_correct sp e m (Sexpr a) t e 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 a r). eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ MWF0 EQ1 ME TRG). - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exists rs1; simpl; tauto. + intros; red; intros; inv TE. + exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exists rs1; econstructor. + split. constructor. + eauto. Qed. Lemma transl_stmt_Sassign_correct: @@ -1022,26 +1059,17 @@ Lemma transl_stmt_Sassign_correct: transl_expr_correct sp nil e m a t m1 v -> transl_stmt_correct sp e m (Sassign id a) t (PTree.set id v e) m1 Out_normal. Proof. - intros; red; intros. - simpl in TE. monadInv TE. intro EQ2. - assert (MWF0: map_wf map s2). - apply map_wf_incr with s. eauto 6 with rtlg. auto. - assert (TRGa: target_reg_ok s2 map a r0). eauto 6 with rtlg. - generalize (H0 _ _ _ _ _ _ _ MWF0 EQ2 ME TRGa). - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - generalize (add_move_correct _ _ sp _ _ _ _ rs1 m1 EQ1). - intros [rs2 [EX2 [RES2 OTHER2]]]. - exists rs2. -(* Exec *) - split. inversion OUT; subst. eapply exec_trans. eexact EX1. - apply exec_instrs_incr with s2. eauto with rtlg. - eexact EX2. traceEq. -(* Match-env *) - split. - apply match_env_update_var with rs1 r s s0; auto. - congruence. -(* Outcome *) - simpl; auto. + intros; red; intros; inv TE. + exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exploit tr_move_correct; eauto. intros [rs2 [EX2 [RES2 OTHER2]]]. + exists rs2; econstructor. + split. constructor. + split. eapply star_trans. eexact EX1. eexact EX2. traceEq. + apply match_env_invariant with (rs1#rv <- v). + apply match_env_update_var; auto. + intros. rewrite Regmap.gsspec. destruct (peq r rv). + subst r. congruence. + auto. Qed. Lemma transl_stmt_Sifthenelse_correct: @@ -1055,45 +1083,15 @@ Lemma transl_stmt_Sifthenelse_correct: t = t1 ** t2 -> transl_stmt_correct sp e m (Sifthenelse a s1 s2) t e2 m2 out. Proof. - intros; red; intros until rs; intro MWF. - simpl. case (more_likely a s1 s2); monadSimpl; intro EQ2; intros. - assert (MWF1: map_wf map s3). eauto with rtlg. - generalize (H0 _ _ _ _ _ _ rs MWF1 EQ2 ME). - 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 s3. - eauto with rtlg. eexact EX2. auto. - 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. eexact EX2. auto. - tauto. - - assert (MWF1: map_wf map s3). eauto with rtlg. - generalize (H0 _ _ _ _ _ _ rs MWF1 EQ2 ME). - 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. eexact EX2. auto. - 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 s3. - eauto with rtlg. eexact EX2. auto. - tauto. + intros; red; intros; inv TE. + exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]]. + assert (tr_stmt code map (if v1 then s1 else s2) (if v1 then ntrue else nfalse) ncont nexits nret rret). + destruct v1; auto. + exploit H2; 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: @@ -1107,34 +1105,15 @@ Lemma transl_stmt_Sloop_loop_correct: t = t1 ** t2 -> transl_stmt_correct sp e m (Sloop sl) t 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 E0 ns rs1 m1 t2. - apply exec_one. apply exec_Inop. - generalize EQ1. unfold update_instr. - case (plt n (st_nextnode s1)); intro; monadSimpl. - rewrite <- H5. simpl. apply PTree.gss. - exact EX2. - reflexivity. traceEq. - tauto. + 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: @@ -1145,25 +1124,12 @@ Lemma transl_stmt_Sloop_stop_correct: out <> Out_normal -> transl_stmt_correct sp e m (Sloop sl) t 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. + 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) @@ -1172,65 +1138,59 @@ Lemma transl_stmt_Sblock_correct: transl_stmt_correct sp e m sl t e1 m1 out -> transl_stmt_correct sp e m (Sblock sl) t 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. + 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. - 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_exit_correct: - forall nexits ex s nd s', - transl_exit nexits ex s = OK nd s' -> - nth_error nexits ex = Some nd. -Proof. - intros until s'. unfold transl_exit. - case (nth_error nexits ex); intros; simplify_eq H; congruence. Qed. Lemma transl_stmt_Sexit_correct: forall (sp: val) (e : env) (m : mem) (n : nat), transl_stmt_correct sp e m (Sexit n) E0 e m (Out_exit n). Proof. - intros; red; intros. - simpl in TE. simpl in OUT. - generalize (transl_exit_correct _ _ _ _ _ TE); intro. - assert (ns = nd). congruence. subst ns. - exists rs. simpl. intuition. apply exec_refl. + intros; red; intros; inv TE. + exists rs; econstructor. + split. econstructor; eauto. + split. apply star_refl. + auto. Qed. Lemma transl_switch_correct: - forall sp rs m r i nexits nd default cases s ns s', - transl_switch r nexits cases default s = OK ns s' -> - nth_error nexits (switch_target i default cases) = Some nd -> + forall cs sp rs m i code r nexits t ns, + tr_switch code r nexits t ns -> rs#r = Vint i -> - exec_instrs tge s'.(st_code) sp ns rs m E0 nd rs m. + 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 cases; simpl; intros. - generalize (transl_exit_correct _ _ _ _ _ H). intros. - assert (ns = nd). congruence. subst ns. apply exec_refl. - destruct a as [key1 exit1]. monadInv H. clear H. intro EQ1. - caseEq (Int.eq i key1); intro IEQ; rewrite IEQ in H0. - (* i = key1 *) - apply exec_trans with E0 n0 rs m E0. apply exec_one. - eapply exec_Icond_true. eauto with rtlg. simpl. rewrite H1. congruence. - generalize (transl_exit_correct _ _ _ _ _ EQ0); intro. - assert (n0 = nd). congruence. subst n0. apply exec_refl. traceEq. - (* i <> key1 *) - apply exec_trans with E0 n rs m E0. apply exec_one. - eapply exec_Icond_false. eauto with rtlg. simpl. rewrite H1. congruence. - apply exec_instrs_incr with s0; eauto with rtlg. traceEq. + 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. Lemma transl_stmt_Sswitch_correct: @@ -1242,32 +1202,25 @@ Lemma transl_stmt_Sswitch_correct: transl_stmt_correct sp e m (Sswitch a cases default) t1 e m1 (Out_exit (switch_target n default cases)). Proof. - intros; red; intros. monadInv TE. clear TE; intros EQ1. - simpl in OUT. - assert (state_incr s s1). eauto with rtlg. - - red in H0. - assert (MWF1: map_wf map s1). eauto with rtlg. - assert (TRG1: target_reg_ok s1 map a r). eauto with rtlg. - destruct (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG1) - as [rs' [EXEC1 [ME1 [RES1 OTHER1]]]]. - simpl. exists rs'. - (* execution *) - split. eapply exec_trans. eexact EXEC1. - apply exec_instrs_incr with s1. eauto with rtlg. - eapply transl_switch_correct; eauto. traceEq. - (* match_env & match_reg *) - tauto. + intros; red; intros; inv TE. + exploit H0; 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 _ _ _ H4 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_correct sp e m (Sreturn None) E0 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. + intros; red; intros; inv TE. + exists rs; econstructor. + split. constructor. auto. + split. apply star_refl. + auto. Qed. Lemma transl_stmt_Sreturn_some_correct: @@ -1277,33 +1230,59 @@ Lemma transl_stmt_Sreturn_some_correct: transl_expr_correct sp nil e m a t m1 v -> transl_stmt_correct sp e m (Sreturn (Some a)) t e m1 (Out_return (Some v)). Proof. - intros; red; intros. generalize TE; simpl. - destruct rret. intro EQ. - assert (TRG: target_reg_ok s map a r). - inversion RRG. apply target_reg_other; auto. - generalize (H0 _ _ _ _ _ _ _ MWF EQ ME TRG). - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - simpl in OUT. subst nd. exists rs1. tauto. - - monadSimpl. + intros; red; intros; inv TE. + exploit H0; 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) (t t1 : trace) (m1 : mem) (t2 : trace) (m2 : mem) + (t3 : trace) (m3 : mem) (vf : val) (vargs : list val) (vres : val) + (f : CminorSel.fundef), + eval_expr ge (Vptr sp Int.zero) nil e m a t1 m1 vf -> + transl_expr_correct (Vptr sp Int.zero) nil e m a t1 m1 vf -> + eval_exprlist ge (Vptr sp Int.zero) nil e m1 bl t2 m2 vargs -> + transl_exprlist_correct (Vptr sp Int.zero) nil e m1 bl t2 m2 vargs -> + Genv.find_funct ge vf = Some f -> + CminorSel.funsig f = sig -> + eval_funcall ge (free m2 sp) f vargs t3 m3 vres -> + transl_function_correct (free m2 sp) f vargs t3 m3 vres -> + t = t1 ** t2 ** t3 -> + transl_stmt_correct (Vptr sp Int.zero) e m (Stailcall sig a bl) + t e m3 (Out_tailcall_return vres). +Proof. + intros; red; intros; inv TE. + exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + exploit functions_translated; eauto. intros [tf [TFIND TF]]. + exploit H6; 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 + of the mutual induction principle for CminorSel evaluation derivations to the lemmas above. *) -Scheme eval_expr_ind_5 := Minimality for eval_expr Sort Prop - with eval_condexpr_ind_5 := Minimality for eval_condexpr Sort Prop - with eval_exprlist_ind_5 := Minimality for eval_exprlist Sort Prop - with eval_funcall_ind_5 := Minimality for eval_funcall Sort Prop - with exec_stmt_ind_5 := Minimality for exec_stmt Sort Prop. - Theorem transl_function_correctness: forall m f vargs t m' vres, eval_funcall ge m f vargs t m' vres -> transl_function_correct m f vargs t m' vres. Proof - (eval_funcall_ind_5 ge + (eval_funcall_ind5 ge transl_expr_correct transl_condition_correct transl_exprlist_correct @@ -1339,26 +1318,35 @@ Proof transl_stmt_Sexit_correct transl_stmt_Sswitch_correct transl_stmt_Sreturn_none_correct - transl_stmt_Sreturn_some_correct). + transl_stmt_Sreturn_some_correct + transl_stmt_Stailcall_correct). + +Require Import Smallstep. + +(** The correctness of the translation follows: if the original CminorSel + program executes with trace [t] and exit code [r], then the generated + RTL program terminates with the same trace and exit code. *) Theorem transl_program_correct: - forall (t: trace) (r: val), - Cminor.exec_program prog t r -> - RTL.exec_program tprog t r. + forall (t: trace) (r: int), + CminorSel.exec_program prog t (Vint r) -> + RTL.exec_program tprog (Terminates t r). Proof. intros t 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. + exploit transl_function_correctness; 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. - split. exact TFIND. - split. generalize (sig_transl_function _ _ TRANSLF). congruence. + eexact TFIND. + generalize (sig_transl_function _ _ TRANSLF). congruence. unfold fundef; rewrite (Genv.init_mem_transf_partial transl_fundef prog TRANSL). - exact (transl_function_correctness _ _ _ _ _ _ EVAL _ TRANSLF). + eexact EX. + constructor. Qed. End CORRECTNESS. -- cgit