From c48b9097201dc9a1e326acdbce491fe16cab01e6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 28 Aug 2007 12:57:58 +0000 Subject: Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenproof.v | 1024 +++++++++++++++++++++++++++++-------------------- 1 file changed, 616 insertions(+), 408 deletions(-) (limited to 'backend/RTLgenproof.v') diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 15f305a8..e9a04fcc 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -94,13 +94,13 @@ Proof. eauto. Qed. -(** An RTL register environment matches a Cminor local environment and +(** An RTL register environment matches a CminorSel 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 + the CminorSel 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 := + (map: mapping) (e: env) (le: letenv) (rs: regset) : Prop := mk_match_env { me_vars: (forall id v, @@ -367,6 +367,51 @@ Proof. split. apply Regmap.gss. intros; apply Regmap.gso; auto. Qed. +(** Correctness of the code generated by [store_var] and [store_optvar]. *) + +Lemma tr_store_var_correct: + forall rs cs code map r id ns nd e sp m, + tr_store_var code map r id ns nd -> + map_wf map -> + match_env map e nil rs -> + exists rs', + star step tge (State cs code sp ns rs m) + E0 (State cs code sp nd rs' m) + /\ match_env map (PTree.set id rs#r e) nil rs'. +Proof. + intros. destruct H as [rv [A B]]. + exploit tr_move_correct; eauto. intros [rs' [EX [RES OTHER]]]. + exists rs'; split. eexact EX. + apply match_env_invariant with (rs#rv <- (rs#r)). + apply match_env_update_var; auto. + intros. rewrite Regmap.gsspec. destruct (peq r0 rv). + subst r0; auto. + auto. +Qed. + +Lemma tr_store_optvar_correct: + forall rs cs code map r optid ns nd e sp m, + tr_store_optvar code map r optid ns nd -> + map_wf map -> + match_env map e nil rs -> + exists rs', + star step tge (State cs code sp ns rs m) + E0 (State cs code sp nd rs' m) + /\ match_env map (set_optvar optid rs#r e) nil rs'. +Proof. + intros. destruct optid; simpl in *. + eapply tr_store_var_correct; eauto. + exists rs; split. subst nd. apply star_refl. auto. +Qed. + +(** ** Semantic preservation for the translation of expressions *) + +Section CORRECTNESS_EXPR. + +Variable sp: val. +Variable e: env. +Variable m: mem. + (** The proof of semantic preservation for the translation of expressions is a simulation argument based on diagrams of the following form: << @@ -380,16 +425,14 @@ Qed. I /\ Q >> 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] - to value [v]. + The left vertical arrow represents an evaluation of the expression [a]. 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 CminorSel environments - [e], [le] and the RTL register environment [rs], - as captured by [match_envs]. + The invariant [I] is the agreement between Cminor environments and + RTL register environment, as captured by [match_envs]. - The precondition [P] is the well-formedness of the compilation + The precondition [P] includes the well-formedness of the compilation environment [mut]. The postconditions [Q] state that in the final register environment @@ -400,15 +443,14 @@ Qed. We formalize this simulation property by the following predicate 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 := +Definition transl_expr_prop + (le: letenv) (a: expr) (v: val) : Prop := 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', - star step tge (State cs code sp ns rs m) t (State cs code sp nd rs' m') + star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) /\ match_env map e le rs' /\ rs'#rd = v /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r). @@ -416,123 +458,44 @@ Definition transl_expr_correct (** 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) - (t: trace) (m': mem) (vl: list val) : Prop := +Definition transl_exprlist_prop + (le: letenv) (al: exprlist) (vl: list val) : Prop := 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', - star step tge (State cs code sp ns rs m) t (State cs code sp nd rs' m') + star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) /\ match_env map e le rs' /\ rs'##rl = vl /\ (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 := +Definition transl_condition_prop + (le: letenv) (a: condexpr) (vb: bool) : Prop := 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', - star step tge (State cs code sp ns rs m) t - (State cs code sp (if vb then ntrue else nfalse) rs' m') + star step tge (State cs code sp ns rs m) E0 + (State cs code sp (if vb then ntrue else nfalse) rs' m) /\ match_env map e le rs' /\ (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 -------------- State cs code sp ns rs m - || | - t|| t|* - || | - \/ v - e', m', out -------------- st' - I /\ Q ->> - where [tr_stmt code map a ns ncont nexits nret rret] holds. - The left vertical arrow represents an execution of the statement [a] - 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 CminorSel environments and - RTL register environment, as captured by [match_envs]. - - 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 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 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: 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 CminorSel evaluation derivation for the source program. To keep + 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 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, + 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_prop], 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) E0 m v. + forall (le : letenv) (id : positive) (v : val), + e ! id = Some v -> + transl_expr_prop le (Evar id) v. Proof. intros; red; intros. inv TE. exploit tr_move_correct; eauto. intros [rs' [A [B C]]]. @@ -553,13 +516,12 @@ Proof. Qed. Lemma transl_expr_Eop_correct: - forall (sp: val) (le : letenv) (e : env) (m : mem) (op : operation) - (al : exprlist) (t: trace) (m1 : mem) (vl : list val) - (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 m1 = Some v -> - transl_expr_correct sp le e m (Eop op al) t m1 v. + forall (le : letenv) (op : operation) (args : exprlist) + (vargs : list val) (v : val), + eval_exprlist ge sp e m le args vargs -> + transl_exprlist_prop le args vargs -> + eval_operation ge sp op vargs m = Some v -> + transl_expr_prop le (Eop op args) v. Proof. intros; red; intros. inv TE. exploit H0; eauto. intros [rs1 [EX1 [ME1 [RR1 RO1]]]]. @@ -567,7 +529,7 @@ Proof. (* Exec *) split. eapply star_right. eexact EX1. eapply exec_Iop; eauto. - subst vl. + subst vargs. rewrite (@eval_operation_preserved CminorSel.fundef RTL.fundef ge tge). auto. exact symbols_preserved. traceEq. @@ -580,15 +542,13 @@ Proof. Qed. Lemma transl_expr_Eload_correct: - forall (sp: val) (le : letenv) (e : env) (m : mem) - (chunk : memory_chunk) (addr : addressing) - (al : exprlist) (t: trace) (m1 : mem) (v : val) - (vl : list val) (a: val), - eval_exprlist ge sp le e m al t m1 vl -> - transl_exprlist_correct sp le e m al t 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) t m1 v. + forall (le : letenv) (chunk : memory_chunk) (addr : Op.addressing) + (args : exprlist) (vargs : list val) (vaddr v : val), + eval_exprlist ge sp e m le args vargs -> + transl_exprlist_prop le args vargs -> + Op.eval_addressing ge sp addr vargs = Some vaddr -> + loadv chunk m vaddr = Some v -> + transl_expr_prop le (Eload chunk addr args) v. Proof. intros; red; intros. inv TE. exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. @@ -605,105 +565,19 @@ Proof. intros. rewrite Regmap.gso. auto. intuition congruence. Qed. -Lemma transl_expr_Estore_correct: - forall (sp: val) (le : letenv) (e : env) (m : mem) - (chunk : memory_chunk) (addr : addressing) - (al : exprlist) (b : expr) (t t1: trace) (m1 : mem) - (vl : list val) (t2: trace) (m2 m3 : mem) - (v : val) (a: val), - eval_exprlist ge sp le e m al t1 m1 vl -> - transl_exprlist_correct sp le e m al t1 m1 vl -> - eval_expr ge sp le e m1 b t2 m2 v -> - transl_expr_correct sp le e m1 b t2 m2 v -> - eval_addressing ge sp addr vl = Some a -> - Mem.storev chunk m2 a v = Some m3 -> - t = t1 ** t2 -> - transl_expr_correct sp le e m (Estore chunk addr al b) t m3 v. -Proof. - 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 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. - right. apply in_or_app. auto. - rewrite H5; rewrite RES1. - rewrite (@eval_addressing_preserved _ _ ge tge). - eexact H3. exact symbols_preserved. - rewrite RES2. assumption. - reflexivity. traceEq. -(* Match-env *) - split. assumption. -(* Result *) - split. assumption. -(* Other regs *) - 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 : 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 -> - 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; 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 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. eauto with rtlg. -(* Result *) - split. apply Regmap.gss. -(* Other regs *) - intros. - rewrite Regmap.gso. transitivity (rs1#r). - apply OTHER2. simpl; tauto. - apply OTHER1; auto. - intuition congruence. -Qed. - Lemma transl_expr_Econdition_correct: - forall (sp: val) (le : letenv) (e : env) (m : mem) - (a : condexpr) (b c : expr) (t t1: trace) (m1 : mem) - (v1 : bool) (t2: trace) (m2 : mem) (v2 : val), - eval_condexpr ge sp le e m a t1 m1 v1 -> - transl_condition_correct sp le e m a t1 m1 v1 -> - eval_expr ge sp le e m1 (if v1 then b else c) t2 m2 v2 -> - transl_expr_correct sp le e m1 (if v1 then b else c) t2 m2 v2 -> - t = t1 ** t2 -> - transl_expr_correct sp le e m (Econdition a b c) t m2 v2. + forall (le : letenv) (cond : condexpr) (ifso ifnot : expr) + (vcond : bool) (v : val), + eval_condexpr ge sp e m le cond vcond -> + transl_condition_prop le cond vcond -> + eval_expr ge sp e m le (if vcond then ifso else ifnot) v -> + transl_expr_prop le (if vcond then ifso else ifnot) v -> + transl_expr_prop le (Econdition cond ifso ifnot) v. Proof. 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. + assert (tr_expr code map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd). + destruct vcond; auto. exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exists rs2. (* Exec *) @@ -717,15 +591,12 @@ Proof. Qed. Lemma transl_expr_Elet_correct: - forall (sp: val) (le : letenv) (e : env) (m : mem) - (a b : expr) (t t1: trace) (m1 : mem) (v1 : val) - (t2: trace) (m2 : mem) (v2 : val), - eval_expr ge sp le e m a t1 m1 v1 -> - transl_expr_correct sp le e m a t1 m1 v1 -> - eval_expr ge sp (v1 :: le) e m1 b t2 m2 v2 -> - transl_expr_correct sp (v1 :: le) e m1 b t2 m2 v2 -> - t = t1 ** t2 -> - transl_expr_correct sp le e m (Elet a b) t m2 v2. + forall (le : letenv) (a1 a2 : expr) (v1 v2 : val), + eval_expr ge sp e m le a1 v1 -> + transl_expr_prop le a1 v1 -> + eval_expr ge sp e m (v1 :: le) a2 v2 -> + transl_expr_prop (v1 :: le) a2 v2 -> + transl_expr_prop le (Elet a1 a2) v2. Proof. intros; red; intros; inv TE. exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. @@ -744,15 +615,14 @@ Proof. intros. transitivity (rs1#r0). apply OTHER2. elim H4; intro; auto. unfold reg_in_map, add_letvar; simpl. - unfold reg_in_map in H5; tauto. + unfold reg_in_map in H6; tauto. auto. Qed. Lemma transl_expr_Eletvar_correct: - forall (sp: val) (le : list val) (e : env) - (m : mem) (n : nat) (v : val), + forall (le : list val) (n : nat) (v : val), nth_error le n = Some v -> - transl_expr_correct sp le e m (Eletvar n) E0 m v. + transl_expr_prop le (Eletvar n) v. Proof. intros; red; intros; inv TE. exploit tr_move_correct; eauto. intros [rs1 [EX1 [RES1 OTHER1]]]. @@ -772,54 +642,29 @@ Proof. apply OTHER1. intuition congruence. Qed. -Lemma transl_expr_Ealloc_correct: - forall (sp: val) (le : letenv) (e : env) (m : mem) - (a : expr) (t: trace) (m1 : mem) (n: int) - (m2: mem) (b: block), - eval_expr ge sp le e m a t m1 (Vint n) -> - transl_expr_correct sp le e m a t m1 (Vint n) -> - 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; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [EX1 [ME1 [RR1 RO1]]]]. - exists (rs1#rd <- (Vptr b Int.zero)). -(* Exec *) - split. eapply star_right. eexact EX1. - eapply exec_Ialloc. eauto with rtlg. - eexact RR1. assumption. traceEq. -(* Match-env *) - split. eauto with rtlg. -(* Result *) - split. apply Regmap.gss. -(* Other regs *) - 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. + forall (le : letenv), + transl_condition_prop le CEtrue true. Proof. 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. + forall (le : letenv), + transl_condition_prop le CEfalse false. Proof. intros; red; intros; inv TE. exists rs. split. apply star_refl. split. auto. auto. Qed. Lemma transl_condition_CEcond_correct: - forall (sp: val) (le : letenv) (e : env) (m : mem) - (cond : condition) (al : exprlist) (t1: trace) - (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 m1 = Some b -> - transl_condition_correct sp le e m (CEcond cond al) t1 m1 b. + forall (le : letenv) (cond : condition) (args : exprlist) + (vargs : list val) (b : bool), + eval_exprlist ge sp e m le args vargs -> + transl_exprlist_prop le args vargs -> + eval_condition cond vargs m = Some b -> + transl_condition_prop le (CEcond cond args) b. Proof. intros; red; intros; inv TE. exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. @@ -839,21 +684,18 @@ Proof. Qed. Lemma transl_condition_CEcondition_correct: - forall (sp: val) (le : letenv) (e : env) (m : mem) - (a b c : condexpr) (t t1: trace) (m1 : mem) - (vb1 : bool) (t2: trace) (m2 : mem) (vb2 : bool), - eval_condexpr ge sp le e m a t1 m1 vb1 -> - transl_condition_correct sp le e m a t1 m1 vb1 -> - eval_condexpr ge sp le e m1 (if vb1 then b else c) t2 m2 vb2 -> - transl_condition_correct sp le e m1 (if vb1 then b else c) t2 m2 vb2 -> - t = t1 ** t2 -> - transl_condition_correct sp le e m (CEcondition a b c) t m2 vb2. + forall (le : letenv) (cond ifso ifnot : condexpr) (vcond v : bool), + eval_condexpr ge sp e m le cond vcond -> + transl_condition_prop le cond vcond -> + eval_condexpr ge sp e m le (if vcond then ifso else ifnot) v -> + transl_condition_prop le (if vcond then ifso else ifnot) v -> + transl_condition_prop le (CEcondition cond ifso ifnot) v. Proof. 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. + assert (tr_condition code map pr (if vcond then ifso else ifnot) + (if vcond then ntrue' else nfalse') ntrue nfalse). + destruct vcond; auto. exploit H2; eauto. intros [rs2 [EX2 [ME2 OTHER2]]]. exists rs2. (* Execution *) @@ -865,8 +707,8 @@ Proof. 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. + forall (le : letenv), + transl_exprlist_prop le Enil nil. Proof. intros; red; intros; inv TE. exists rs. @@ -877,15 +719,13 @@ Proof. Qed. Lemma transl_exprlist_Econs_correct: - forall (sp: val) (le : letenv) (e : env) (m : mem) - (a : expr) (bl : exprlist) (t t1: trace) (m1 : mem) - (v : val) (t2: trace) (m2 : mem) (vl : list val), - eval_expr ge sp le e m a t1 m1 v -> - transl_expr_correct sp le e m a t1 m1 v -> - eval_exprlist ge sp le e m1 bl t2 m2 vl -> - transl_exprlist_correct sp le e m1 bl t2 m2 vl -> - t = t1 ** t2 -> - transl_exprlist_correct sp le e m (Econs a bl) t m2 (v :: vl). + forall (le : letenv) (a1 : expr) (al : exprlist) (v1 : val) + (vl : list val), + eval_expr ge sp e m le a1 v1 -> + transl_expr_prop le a1 v1 -> + eval_exprlist ge sp e m le al vl -> + transl_exprlist_prop le al vl -> + transl_exprlist_prop le (Econs a1 al) (v1 :: vl). Proof. intros; red; intros; inv TE. exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. @@ -904,6 +744,153 @@ Proof. apply OTHER1; auto. Qed. +Theorem transl_expr_correct: + forall le a v, + eval_expr ge sp e m le a v -> + transl_expr_prop le a v. +Proof + (eval_expr_ind3 ge sp e m + transl_expr_prop + transl_condition_prop + transl_exprlist_prop + transl_expr_Evar_correct + transl_expr_Eop_correct + transl_expr_Eload_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). + +Theorem transl_condexpr_correct: + forall le a v, + eval_condexpr ge sp e m le a v -> + transl_condition_prop le a v. +Proof + (eval_condexpr_ind3 ge sp e m + transl_expr_prop + transl_condition_prop + transl_exprlist_prop + transl_expr_Evar_correct + transl_expr_Eop_correct + transl_expr_Eload_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). + + +Theorem transl_exprlist_correct: + forall le a v, + eval_exprlist ge sp e m le a v -> + transl_exprlist_prop le a v. +Proof + (eval_exprlist_ind3 ge sp e m + transl_expr_prop + transl_condition_prop + transl_exprlist_prop + transl_expr_Evar_correct + transl_expr_Eop_correct + transl_expr_Eload_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). + +End CORRECTNESS_EXPR. + +(** ** Semantic preservation for the translation of terminating statements *) + +(** The simulation diagram for the translation of statements + is of the following form: +<< + I /\ P + e, m, a ---------------- State cs code sp ns rs m + || | + t|| t|* + || | + \/ v + e', m', out ------------------ st' + I /\ Q +>> + where [tr_stmt code map a ns ncont nexits nret rret] holds. + The left vertical arrow represents an execution of the statement [a]. + 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 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 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_prop + (sp: val) (e: env) (m: mem) (a: stmt) + (t: trace) (e': env) (m': mem) (out: outcome) : Prop := + forall cs code map ns ncont nexits nret rret rs + (MWF: map_wf map) + (TE: tr_stmt code map a ns ncont nexits nret rret) + (ME: match_env map e nil rs), + exists rs', exists st, + state_for_outcome ncont nexits nret rret cs code sp rs' m' out st + /\ star step tge (State cs code sp ns rs m) t st + /\ match_env map e' nil rs'. + +(** Finally, the correctness condition for the translation of functions + is that the translated RTL function, when applied to the same arguments + as the original Cminor function, returns the same value and performs + the same modifications on the memory state. *) + +Definition transl_function_prop + (m: mem) (f: CminorSel.fundef) (vargs: list val) + (t: trace) (m': mem) (vres: val) : Prop := + forall cs tf + (TE: transl_fundef f = OK tf), + star step tge (Callstate cs tf vargs m) t (Returnstate cs vres m'). + Lemma transl_funcall_internal_correct: forall (m : mem) (f : CminorSel.function) (vargs : list val) (m1 : mem) (sp : block) (e : env) (t : trace) @@ -911,9 +898,9 @@ Lemma transl_funcall_internal_correct: Mem.alloc m 0 (fn_stackspace f) = (m1, sp) -> set_locals (fn_vars f) (set_params vargs (CminorSel.fn_params f)) = e -> exec_stmt ge (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out -> - transl_stmt_correct (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out -> + transl_stmt_prop (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out -> outcome_result_value out f.(CminorSel.fn_sig).(sig_res) vres -> - transl_function_correct m (Internal f) vargs t + transl_function_prop m (Internal f) vargs t (outcome_free_mem out m2 sp) vres. Proof. intros; red; intros. @@ -976,7 +963,7 @@ Qed. Lemma transl_funcall_external_correct: forall (ef : external_function) (m : mem) (args : list val) (t: trace) (res : val), event_match ef args t res -> - transl_function_correct m (External ef) args t m res. + transl_function_prop m (External ef) args t m res. Proof. intros; red; intros. unfold transl_function in TE; simpl in TE. inversion TE; subst tf. @@ -985,7 +972,7 @@ 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. + transl_stmt_prop sp e m Sskip E0 e m Out_normal. Proof. intros; red; intros; inv TE. exists rs; econstructor. @@ -1008,11 +995,11 @@ Lemma transl_stmt_Sseq_continue_correct: (t1: trace) (e1 : env) (m1 : mem) (s2 : stmt) (t2: trace) (e2 : env) (m2 : mem) (out : outcome), exec_stmt ge sp e m s1 t1 e1 m1 Out_normal -> - transl_stmt_correct sp e m s1 t1 e1 m1 Out_normal -> + transl_stmt_prop sp e m s1 t1 e1 m1 Out_normal -> exec_stmt ge sp e1 m1 s2 t2 e2 m2 out -> - transl_stmt_correct sp e1 m1 s2 t2 e2 m2 out -> + transl_stmt_prop sp e1 m1 s2 t2 e2 m2 out -> t = t1 ** t2 -> - transl_stmt_correct sp e m (Sseq s1 s2) t e2 m2 out. + transl_stmt_prop sp e m (Sseq s1 s2) t e2 m2 out. Proof. intros; red; intros; inv TE. exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. inv OUT1. @@ -1027,9 +1014,9 @@ Lemma transl_stmt_Sseq_stop_correct: forall (sp : val) (e : env) (m : mem) (t: trace) (s1 s2 : stmt) (e1 : env) (m1 : mem) (out : outcome), exec_stmt ge sp e m s1 t e1 m1 out -> - transl_stmt_correct sp e m s1 t e1 m1 out -> + transl_stmt_prop sp e m s1 t e1 m1 out -> out <> Out_normal -> - transl_stmt_correct sp e m (Sseq s1 s2) t e1 m1 out. + transl_stmt_prop sp e m (Sseq s1 s2) t e1 m1 out. Proof. intros; red; intros; inv TE. exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. @@ -1038,56 +1025,135 @@ Proof. auto. Qed. -Lemma transl_stmt_Sexpr_correct: - forall (sp: val) (e : env) (m : mem) (a : expr) (t: trace) - (m1 : mem) (v : val), - eval_expr ge sp nil e m a t m1 v -> - transl_expr_correct sp nil e m a t m1 v -> - transl_stmt_correct sp e m (Sexpr a) t e m1 Out_normal. +Lemma transl_stmt_Sassign_correct: + forall (sp : val) (e : env) (m : mem) (id : ident) (a : expr) + (v : val), + eval_expr ge sp e m nil a v -> + transl_stmt_prop sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal. Proof. intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exists rs1; econstructor. + exploit transl_expr_correct; eauto. + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exploit tr_store_var_correct; eauto. intros [rs2 [EX2 ME2]]. + exists rs2; econstructor. split. constructor. - eauto. + split. eapply star_trans. eexact EX1. eexact EX2. traceEq. + congruence. Qed. -Lemma transl_stmt_Sassign_correct: - forall (sp: val) (e : env) (m : mem) - (id : ident) (a : expr) (t: trace) (m1 : mem) (v : val), - eval_expr ge sp nil e m a t m1 v -> - 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. +Lemma transl_stmt_Sstore_correct: + forall (sp : val) (e : env) (m : mem) (chunk : memory_chunk) + (addr: addressing) (al: exprlist) (b: expr) + (vl: list val) (v: val) (vaddr: val) (m' : mem), + eval_exprlist ge sp e m nil al vl -> + eval_expr ge sp e m nil b v -> + eval_addressing ge sp addr vl = Some vaddr -> + storev chunk m vaddr v = Some m' -> + transl_stmt_prop sp e m (Sstore chunk addr al b) E0 e m' Out_normal. Proof. - intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exploit tr_move_correct; eauto. intros [rs2 [EX2 [RES2 OTHER2]]]. + intros; red; intros; inv TE. + exploit transl_exprlist_correct; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exploit transl_expr_correct; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exists rs2; econstructor. + (* Outcome *) split. constructor. - 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. + (* Exec *) + split. eapply star_trans. eexact EX1. + eapply star_right. eexact EX2. + eapply exec_Istore; eauto. + assert (rs2##rl = rs1##rl). + apply list_map_exten. intros r' IN. symmetry. apply OTHER2. auto. + rewrite H3; rewrite RES1. + rewrite (@eval_addressing_preserved _ _ ge tge). eexact H1. + exact symbols_preserved. + rewrite RES2. auto. + reflexivity. traceEq. + (* Match-env *) auto. Qed. +Lemma transl_stmt_Scall_correct: + forall (sp : val) (e : env) (m : mem) (optid : option ident) + (sig : signature) (a : expr) (bl : exprlist) (vf : val) + (vargs : list val) (f : CminorSel.fundef) (t : trace) (m' : mem) + (vres : val) (e' : env), + eval_expr ge sp e m nil a vf -> + eval_exprlist ge sp e m nil bl vargs -> + Genv.find_funct ge vf = Some f -> + CminorSel.funsig f = sig -> + eval_funcall ge m f vargs t m' vres -> + transl_function_prop m f vargs t m' vres -> + e' = set_optvar optid vres e -> + transl_stmt_prop sp e m (Scall optid sig a bl) t e' m' Out_normal. +Proof. + intros; red; intros; inv TE. + exploit transl_expr_correct; eauto. + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exploit transl_exprlist_correct; eauto. + intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + exploit functions_translated; eauto. intros [tf [TFIND TF]]. + exploit H4; eauto. intro EXF. + exploit (tr_store_optvar_correct (rs2#rd <- vres)); eauto. + apply match_env_update_temp; eauto. + intros [rs3 [EX3 ME3]]. + exists rs3; econstructor. + (* Outcome *) + split. constructor. + (* Exec *) + split. eapply star_trans. eexact EX1. + eapply star_trans. eexact EX2. + eapply star_left. eapply exec_Icall; eauto. + simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. + eapply sig_transl_function; eauto. + eapply star_trans. rewrite RES2. eexact EXF. + eapply star_left. apply exec_return. + eexact EX3. + reflexivity. reflexivity. reflexivity. reflexivity. traceEq. + (* Match-env *) + rewrite Regmap.gss in ME3. auto. +Qed. + +Lemma transl_stmt_Salloc_correct: + forall (sp : val) (e : env) (m : mem) (id : ident) (a : expr) + (n : int) (m' : mem) (b : block), + eval_expr ge sp e m nil a (Vint n) -> + alloc m 0 (Int.signed n) = (m', b) -> + transl_stmt_prop sp e m (Salloc id a) E0 + (PTree.set id (Vptr b Int.zero) e) m' Out_normal. +Proof. + intros; red; intros; inv TE. + exploit transl_expr_correct; eauto. + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exploit (tr_store_var_correct (rs1#rd <- (Vptr b Int.zero))); eauto. + apply match_env_update_temp; eauto. + intros [rs2 [EX2 ME2]]. + exists rs2; econstructor. + (* Outcome *) + split. constructor. + (* Execution *) + split. eapply star_trans. eexact EX1. + eapply star_left. 2: eexact EX2. + eapply exec_Ialloc; eauto. + reflexivity. traceEq. + (* Match-env *) + rewrite Regmap.gss in ME2. auto. +Qed. + Lemma transl_stmt_Sifthenelse_correct: - forall (sp: val) (e : env) (m : mem) (a : condexpr) - (s1 s2 : stmt) (t t1: trace) (m1 : mem) - (v1 : bool) (t2: trace) (e2 : env) (m2 : mem) (out : outcome), - eval_condexpr ge sp nil e m a t1 m1 v1 -> - transl_condition_correct sp nil e m a t1 m1 v1 -> - exec_stmt ge sp e m1 (if v1 then s1 else s2) t2 e2 m2 out -> - transl_stmt_correct sp e m1 (if v1 then s1 else s2) t2 e2 m2 out -> - t = t1 ** t2 -> - transl_stmt_correct sp e m (Sifthenelse a s1 s2) t e2 m2 out. + forall (sp : val) (e : env) (m : mem) (a : condexpr) (s1 s2 : stmt) + (v : bool) (t : trace) (e' : env) (m' : mem) (out : outcome), + eval_condexpr ge sp e m nil a v -> + exec_stmt ge sp e m (if v then s1 else s2) t e' m' out -> + transl_stmt_prop sp e m (if v then s1 else s2) t e' m' out -> + transl_stmt_prop sp e m (Sifthenelse a s1 s2) t e' m' out. Proof. intros; red; intros; inv TE. - exploit 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]]]]. + exploit transl_condexpr_correct; eauto. + intros [rs1 [EX1 [ME1 OTHER1]]]. + assert (tr_stmt code map (if v then s1 else s2) (if v then ntrue else nfalse) + ncont nexits nret rret). + destruct v; auto. + exploit H1; eauto. intros [rs2 [st2 [OUT2 [EX2 ME2]]]]. exists rs2; exists st2. split. eauto. split. eapply star_trans. eexact EX1. eexact EX2. auto. @@ -1099,11 +1165,11 @@ Lemma transl_stmt_Sloop_loop_correct: (e1 : env) (m1 : mem) (t2: trace) (e2 : env) (m2 : mem) (out : outcome), exec_stmt ge sp e m sl t1 e1 m1 Out_normal -> - transl_stmt_correct sp e m sl t1 e1 m1 Out_normal -> + transl_stmt_prop sp e m sl t1 e1 m1 Out_normal -> exec_stmt ge sp e1 m1 (Sloop sl) t2 e2 m2 out -> - transl_stmt_correct sp e1 m1 (Sloop sl) t2 e2 m2 out -> + transl_stmt_prop sp e1 m1 (Sloop sl) t2 e2 m2 out -> t = t1 ** t2 -> - transl_stmt_correct sp e m (Sloop sl) t e2 m2 out. + transl_stmt_prop sp e m (Sloop sl) t e2 m2 out. Proof. intros; red; intros; inversion TE. subst. exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. inv OUT1. @@ -1120,9 +1186,9 @@ Lemma transl_stmt_Sloop_stop_correct: forall (sp: val) (e : env) (m : mem) (t: trace) (sl : stmt) (e1 : env) (m1 : mem) (out : outcome), exec_stmt ge sp e m sl t e1 m1 out -> - transl_stmt_correct sp e m sl t e1 m1 out -> + transl_stmt_prop sp e m sl t e1 m1 out -> out <> Out_normal -> - transl_stmt_correct sp e m (Sloop sl) t e1 m1 out. + transl_stmt_prop sp e m (Sloop sl) t e1 m1 out. Proof. intros; red; intros; inv TE. exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. @@ -1135,8 +1201,8 @@ Lemma transl_stmt_Sblock_correct: forall (sp: val) (e : env) (m : mem) (sl : stmt) (t: trace) (e1 : env) (m1 : mem) (out : outcome), exec_stmt ge sp e m sl t e1 m1 out -> - transl_stmt_correct sp e m sl t e1 m1 out -> - transl_stmt_correct sp e m (Sblock sl) t e1 m1 (outcome_block out). + transl_stmt_prop sp e m sl t e1 m1 out -> + transl_stmt_prop sp e m (Sblock sl) t e1 m1 (outcome_block out). Proof. intros; red; intros; inv TE. exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. @@ -1150,7 +1216,7 @@ 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). + transl_stmt_prop sp e m (Sexit n) E0 e m (Out_exit n). Proof. intros; red; intros; inv TE. exists rs; econstructor. @@ -1195,26 +1261,25 @@ Qed. Lemma transl_stmt_Sswitch_correct: forall (sp : val) (e : env) (m : mem) (a : expr) - (cases : list (int * nat)) (default : nat) - (t1 : trace) (m1 : mem) (n : int), - eval_expr ge sp nil e m a t1 m1 (Vint n) -> - transl_expr_correct sp nil e m a t1 m1 (Vint n) -> - transl_stmt_correct sp e m (Sswitch a cases default) t1 e m1 + (cases : list (int * nat)) (default : nat) (n : int), + eval_expr ge sp e m nil a (Vint n) -> + transl_stmt_prop sp e m (Sswitch a cases default) E0 e m (Out_exit (switch_target n default cases)). Proof. intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exploit transl_expr_correct; eauto. + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. exploit transl_switch_correct; eauto. intros [nd [EX2 MO2]]. exists rs1; econstructor. split. econstructor. - rewrite (validate_switch_correct _ _ _ H4 n). eauto. + rewrite (validate_switch_correct _ _ _ H3 n). eauto. split. eapply star_trans. eexact EX1. eexact EX2. traceEq. auto. Qed. Lemma transl_stmt_Sreturn_none_correct: forall (sp: val) (e : env) (m : mem), - transl_stmt_correct sp e m (Sreturn None) E0 e m (Out_return None). + transl_stmt_prop sp e m (Sreturn None) E0 e m (Out_return None). Proof. intros; red; intros; inv TE. exists rs; econstructor. @@ -1224,14 +1289,13 @@ Proof. Qed. Lemma transl_stmt_Sreturn_some_correct: - forall (sp: val) (e : env) (m : mem) (a : expr) (t: trace) - (m1 : mem) (v : val), - eval_expr ge sp nil e m a t m1 v -> - 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)). + forall (sp : val) (e : env) (m : mem) (a : expr) (v : val), + eval_expr ge sp e m nil a v -> + transl_stmt_prop sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v)). Proof. intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exploit transl_expr_correct; eauto. + intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. exists rs1; econstructor. split. econstructor. reflexivity. auto. eauto. @@ -1239,26 +1303,22 @@ 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 -> + (bl : exprlist) (vf : val) (vargs : list val) (f : CminorSel.fundef) + (t : trace) (m' : mem) (vres : val), + eval_expr ge (Vptr sp Int.zero) e m nil a vf -> + eval_exprlist ge (Vptr sp Int.zero) e m nil bl vargs -> Genv.find_funct ge vf = Some f -> CminorSel.funsig f = sig -> - eval_funcall ge (free 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). + eval_funcall ge (free m sp) f vargs t m' vres -> + transl_function_prop (free m sp) f vargs t m' vres -> + transl_stmt_prop (Vptr sp Int.zero) e m (Stailcall sig a bl) t e + m' (Out_tailcall_return vres). Proof. intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + exploit transl_expr_correct; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + exploit transl_exprlist_correct; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exploit functions_translated; eauto. intros [tf [TFIND TF]]. - exploit H6; eauto. intro EXF. + exploit H4; eauto. intro EXF. exists rs2; econstructor. split. constructor. split. @@ -1274,41 +1334,25 @@ Proof. Qed. (** The correctness of the translation then follows by application - of the mutual induction principle for CminorSel evaluation derivations + of the mutual induction principle for Cminor evaluation derivations to the lemmas above. *) -Theorem transl_function_correctness: +Theorem transl_function_correct: 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. + transl_function_prop m f vargs t m' vres. Proof - (eval_funcall_ind5 ge - transl_expr_correct - transl_condition_correct - transl_exprlist_correct - transl_function_correct - transl_stmt_correct - - transl_expr_Evar_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_expr_Ealloc_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 + (eval_funcall_ind2 ge + transl_function_prop + transl_stmt_prop + transl_funcall_internal_correct transl_funcall_external_correct transl_stmt_Sskip_correct - transl_stmt_Sexpr_correct transl_stmt_Sassign_correct + transl_stmt_Sstore_correct + transl_stmt_Scall_correct + transl_stmt_Salloc_correct transl_stmt_Sifthenelse_correct transl_stmt_Sseq_continue_correct transl_stmt_Sseq_stop_correct @@ -1321,21 +1365,171 @@ Proof transl_stmt_Sreturn_some_correct transl_stmt_Stailcall_correct). -Require Import Smallstep. +Theorem transl_stmt_correct: + forall sp e m s t e' m' out, + exec_stmt ge sp e m s t e' m' out -> + transl_stmt_prop sp e m s t e' m' out. +Proof + (exec_stmt_ind2 ge + transl_function_prop + transl_stmt_prop + + transl_funcall_internal_correct + transl_funcall_external_correct + transl_stmt_Sskip_correct + transl_stmt_Sassign_correct + transl_stmt_Sstore_correct + transl_stmt_Scall_correct + transl_stmt_Salloc_correct + transl_stmt_Sifthenelse_correct + transl_stmt_Sseq_continue_correct + transl_stmt_Sseq_stop_correct + transl_stmt_Sloop_loop_correct + transl_stmt_Sloop_stop_correct + transl_stmt_Sblock_correct + transl_stmt_Sexit_correct + transl_stmt_Sswitch_correct + transl_stmt_Sreturn_none_correct + transl_stmt_Sreturn_some_correct + transl_stmt_Stailcall_correct). -(** 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. *) +(** ** Semantic preservation for the translation of divering statements *) + +Fixpoint size_stmt (s: stmt) : nat := + match s with + | Sseq s1 s2 => (1 + size_stmt s1 + size_stmt s2)%nat + | Sifthenelse e s1 s2 => (1 + size_stmt s1 + size_stmt s2)%nat + | Sloop s1 => (1 + size_stmt s1)%nat + | Sblock s1 => (1 + size_stmt s1)%nat + | _ => 1%nat + end. + +Theorem transl_function_correct_divergence: + forall m fd vargs t tfd cs, + evalinf_funcall ge m fd vargs t -> + transl_fundef fd = OK tfd -> + forever_N step tge O (Callstate cs tfd vargs m) t. +Proof. + cofix FUNCALL. + assert (STMT: forall sp e m s t, + execinf_stmt ge sp e m s t -> + forall cs code map ns ncont nexits nret rret rs + (MWF: map_wf map) + (TE: tr_stmt code map s ns ncont nexits nret rret) + (ME: match_env map e nil rs), + forever_N step tge (size_stmt s) (State cs code sp ns rs m) t). + cofix STMT; intros. + inv H; inversion TE; subst. + (* Scall *) + destruct (transl_expr_correct _ _ _ _ _ _ H0 + cs _ _ _ _ _ _ _ MWF H7 ME) + as [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + destruct (transl_exprlist_correct _ _ _ _ _ _ H1 + cs _ _ _ _ _ _ _ MWF H8 ME1) + as [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + destruct (functions_translated _ _ H2) as [tf [TFIND TF]]. + eapply forever_N_star with (p := O). + eapply star_trans. eexact EX1. eexact EX2. reflexivity. + simpl; omega. + eapply forever_N_plus with (p := O). + apply plus_one. eapply exec_Icall; eauto. + simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. + eapply sig_transl_function; eauto. + eapply FUNCALL. rewrite RES2. eexact H4. assumption. + reflexivity. traceEq. + (* Sifthenelse *) + destruct (transl_condexpr_correct _ _ _ _ _ _ H0 + cs _ _ _ _ _ _ _ MWF H11 ME) + as [rs1 [EX1 [ME1 OTHER1]]]. + eapply forever_N_star with (p := size_stmt (if v then s1 else s2)). + eexact EX1. destruct v; simpl; omega. + eapply STMT. eexact H1. eauto. destruct v; eauto. eauto. + traceEq. + (* Sseq, 1 *) + eapply forever_N_star with (p := size_stmt s1). + apply star_refl. simpl; omega. + eapply STMT; eauto. + traceEq. + (* Sseq, 2 *) + destruct (transl_stmt_correct _ _ _ _ _ _ _ _ H0 + cs _ _ _ _ _ _ _ _ MWF H9 ME) + as [rs1 [st1 [OUT1 [EX1 ME1]]]]. + inv OUT1. + eapply forever_N_star with (p := size_stmt s2). + eexact EX1. simpl; omega. + eapply STMT; eauto. + traceEq. + (* Sloop, body *) + eapply forever_N_star with (p := size_stmt s0). + apply star_refl. simpl; omega. + eapply STMT; eauto. + traceEq. + (* Sloop, loop *) + destruct (transl_stmt_correct _ _ _ _ _ _ _ _ H0 + cs _ _ _ _ _ _ _ _ MWF H2 ME) + as [rs1 [st1 [OUT1 [EX1 ME1]]]]. + inv OUT1. + eapply forever_N_plus with (p := size_stmt (Sloop s0)). + eapply plus_right. eexact EX1. eapply exec_Inop; eauto. reflexivity. + eapply STMT; eauto. + traceEq. + (* Sblock *) + eapply forever_N_star with (p := size_stmt s0). + apply star_refl. simpl; omega. + eapply STMT; eauto. + traceEq. + (* Stailcall *) + destruct (transl_expr_correct _ _ _ _ _ _ H0 + cs _ _ _ _ _ _ _ MWF H6 ME) + as [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + destruct (transl_exprlist_correct _ _ _ _ _ _ H1 + cs _ _ _ _ _ _ _ MWF H12 ME1) + as [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + destruct (functions_translated _ _ H2) as [tf [TFIND TF]]. + eapply forever_N_star with (p := O). + eapply star_trans. eexact EX1. eexact EX2. reflexivity. + simpl; omega. + eapply forever_N_plus with (p := O). + apply plus_one. eapply exec_Itailcall; eauto. + simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. + eapply sig_transl_function; eauto. + eapply FUNCALL. rewrite RES2. eexact H4. assumption. + reflexivity. traceEq. + (* funcall *) + intros. inversion H. subst m0 fd vargs0 t0. + generalize H0; simpl. caseEq (transl_function f); simpl. 2: congruence. + intros tfi EQ1 EQ2. injection EQ2; clear EQ2; intro EQ2. + assert (TR: tr_function f tfi). apply transl_function_charact; auto. + rewrite <- EQ2. inversion TR. subst f0. + pose (rs := init_regs vargs rparams). + assert (ME: match_env map2 e nil rs). + rewrite <- H2. unfold rs. + eapply match_init_env_init_reg; eauto. + 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. + eapply forever_N_plus with (p := size_stmt (fn_body f)). + apply plus_one. eapply exec_function_internal; eauto. + simpl. eapply STMT; eauto. + traceEq. +Qed. + +(** ** Semantic preservation for whole programs. *) + +(** The correctness of the translation follows: + if the original Cminor program executes with observable behavior [beh], + then the generated RTL program executes with the same behavior. *) Theorem transl_program_correct: - forall (t: trace) (r: int), - CminorSel.exec_program prog t (Vint r) -> - RTL.exec_program tprog (Terminates t r). + forall (beh: program_behavior), + CminorSel.exec_program prog beh -> + RTL.exec_program tprog beh. Proof. - intros t r [b [f [m [SYMB [FUNC [SIG EVAL]]]]]]. - generalize (function_ptr_translated _ _ FUNC). - intros [tf [TFIND TRANSLF]]. - exploit transl_function_correctness; eauto. intro EX. + intros. inv H. + (* termination *) + exploit function_ptr_translated; eauto. intros [tf [TFIND TRANSLF]]. + exploit transl_function_correct; eauto. intro EX. econstructor. econstructor. rewrite symbols_preserved. @@ -1347,6 +1541,20 @@ Proof. unfold fundef; rewrite (Genv.init_mem_transf_partial transl_fundef prog TRANSL). eexact EX. constructor. + (* divergence *) + exploit function_ptr_translated; eauto. intros [tf [TFIND TRANSLF]]. + exploit transl_function_correct_divergence; eauto. intro EX. + econstructor. + econstructor. + rewrite symbols_preserved. + replace (prog_main tprog) with (prog_main prog). eauto. + symmetry; apply transform_partial_program_main with transl_fundef. + exact TRANSL. + eexact TFIND. + generalize (sig_transl_function _ _ TRANSLF). congruence. + eapply forever_N_forever. + unfold fundef; rewrite (Genv.init_mem_transf_partial transl_fundef prog TRANSL). + eexact EX. Qed. End CORRECTNESS. -- cgit