From f7693b3d897b90fd3bc2533be002dc0bdcd9f6c2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 6 Oct 2012 15:46:47 +0000 Subject: Merge of branch seq-and-or. See Changelog for details. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenproof.v | 143 +++++++------------------------------------------- 1 file changed, 18 insertions(+), 125 deletions(-) (limited to 'backend/RTLgenproof.v') diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index e06224a..659e8d0 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -520,9 +520,6 @@ Definition transl_expr_prop /\ rs'#rd = v /\ (forall r, In r pr -> rs'#r = rs#r). -(** The simulation properties for lists of expressions and for - conditional expressions are similar. *) - Definition transl_exprlist_prop (le: letenv) (al: exprlist) (vl: list val) : Prop := forall cs f map pr ns nd rl rs @@ -535,18 +532,6 @@ Definition transl_exprlist_prop /\ rs'##rl = vl /\ (forall r, In r pr -> rs'#r = rs#r). -Definition transl_condition_prop - (le: letenv) (a: condexpr) (vb: bool) : Prop := - forall cs f map pr ns ntrue nfalse rs - (MWF: map_wf map) - (TE: tr_condition f.(fn_code) map pr a ns ntrue nfalse) - (ME: match_env map e le rs), - exists rs', - star step tge (State cs f sp ns rs m) E0 - (State cs f sp (if vb then ntrue else nfalse) rs' m) - /\ match_env map e le rs' - /\ (forall r, In r pr -> rs'#r = rs#r). - (** The correctness of the translation is a huge induction over the Cminor evaluation derivation for the source program. To keep the proof manageable, we put each case of the proof in a separate @@ -632,22 +617,25 @@ Proof. Qed. Lemma transl_expr_Econdition_correct: - 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 -> + forall (le : letenv) (cond : condition) (al: exprlist) (ifso ifnot : expr) + (vl: list val) (vcond : bool) (v : val), + eval_exprlist ge sp e m le al vl -> + transl_exprlist_prop le al vl -> + eval_condition cond vl m = Some 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. + transl_expr_prop le (Econdition cond al ifso ifnot) v. Proof. - intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]]. + intros; red; intros; inv TE. inv H14. + exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd dst). destruct vcond; auto. - exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + exploit H3; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exists rs2. (* Exec *) - split. eapply star_trans. eexact EX1. eexact EX2. auto. + split. eapply star_trans. eexact EX1. + eapply star_left. eapply exec_Icond. eauto. rewrite RES1; eauto. reflexivity. + eexact EX2. reflexivity. traceEq. (* Match-env *) split. assumption. (* Result value *) @@ -710,67 +698,6 @@ Proof. apply OTHER1. intuition congruence. Qed. -Lemma transl_condition_CEtrue_correct: - 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 (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 (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]]]]. - exists rs1. -(* Exec *) - split. eapply star_right. eexact EX1. - eapply exec_Icond with (b := b); eauto. - rewrite RES1. auto. - traceEq. -(* Match-env *) - split. assumption. -(* Regs *) - auto. -Qed. - -Lemma transl_condition_CEcondition_correct: - 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 f.(fn_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 *) - 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 (le : letenv), transl_exprlist_prop le Enil nil. @@ -814,31 +741,8 @@ Theorem transl_expr_correct: 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 + (eval_expr_ind2 ge sp e m transl_expr_prop - transl_condition_prop transl_exprlist_prop transl_expr_Evar_correct transl_expr_Eop_correct @@ -846,22 +750,16 @@ Proof 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 + (eval_exprlist_ind2 ge sp e m transl_expr_prop - transl_condition_prop transl_exprlist_prop transl_expr_Evar_correct transl_expr_Eop_correct @@ -869,10 +767,6 @@ Proof 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). @@ -886,7 +780,7 @@ Fixpoint size_stmt (s: stmt) : nat := match s with | Sskip => 0 | Sseq s1 s2 => (size_stmt s1 + size_stmt s2 + 1) - | Sifthenelse e s1 s2 => (size_stmt s1 + size_stmt s2 + 1) + | Sifthenelse cond el s1 s2 => (size_stmt s1 + size_stmt s2 + 1) | Sloop s1 => (size_stmt s1 + 1) | Sblock s1 => (size_stmt s1 + 1) | Sexit n => 0 @@ -1219,11 +1113,10 @@ Proof. econstructor; eauto. econstructor; eauto. (* ifthenelse *) - inv TS. - exploit transl_condexpr_correct; eauto. - intros [rs' [A [B C]]]. + inv TS. inv H13. + exploit transl_exprlist_correct; eauto. intros [rs' [A [B [C D]]]]. econstructor; split. - right; split. eexact A. destruct b; Lt_state. + left. eapply plus_right. eexact A. eapply exec_Icond; eauto. rewrite C; eauto. traceEq. destruct b; econstructor; eauto. (* loop *) -- cgit v1.2.3