From 165407527b1be7df6a376791719321c788e55149 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 18 Sep 2006 15:52:24 +0000 Subject: Simplification de Cminor: les affectations de variables locales ne sont plus des expressions mais des statements (Eassign -> Sassign). Cela simplifie les preuves et ameliore la qualite du RTL produit. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@111 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenproof.v | 463 ++++++++++++++++++++++---------------------------- 1 file changed, 204 insertions(+), 259 deletions(-) (limited to 'backend/RTLgenproof.v') diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 24cc41b..2ce961b 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -133,57 +133,48 @@ Qed. Definition transl_expr_correct (sp: val) (le: letenv) (e: env) (m: mem) (a: expr) - (t: trace) (e': env) (m': mem) (v: val) : Prop := - forall map mut rd nd s ns s' rs + (t: trace) (m': mem) (v: val) : Prop := + forall map rd nd s ns s' rs (MWF: map_wf map s) - (TE: transl_expr map mut a rd nd s = OK ns s') + (TE: transl_expr map a rd nd s = OK ns s') (ME: match_env map e le rs) - (MUT: incl (mutated_expr a) mut) - (TRG: target_reg_ok s map mut a rd), + (TRG: target_reg_ok s map a rd), exists rs', exec_instrs tge s'.(st_code) sp ns rs m t nd rs' m' - /\ match_env map e' le rs' + /\ match_env map e le rs' /\ rs'#rd = v /\ (forall r, - reg_valid r s -> ~(mutated_reg map mut r) -> - reg_in_map map r \/ r <> rd -> - rs'#r = rs#r). + reg_valid r s -> reg_in_map map r \/ r <> rd -> rs'#r = rs#r). (** The simulation properties for lists of expressions and for conditional expressions are similar. *) Definition transl_exprlist_correct (sp: val) (le: letenv) (e: env) (m: mem) (al: exprlist) - (t: trace) (e': env) (m': mem) (vl: list val) : Prop := - forall map mut rl nd s ns s' rs + (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 mut al rl nd s = OK ns s') + (TE: transl_exprlist map al rl nd s = OK ns s') (ME: match_env map e le rs) - (MUT: incl (mutated_exprlist al) mut) - (TRG: target_regs_ok s map mut al rl), + (TRG: target_regs_ok s map al rl), exists rs', exec_instrs tge s'.(st_code) sp ns rs m t nd rs' m' - /\ match_env map e' le rs' + /\ match_env map e le rs' /\ rs'##rl = vl /\ (forall r, - reg_valid r s -> ~(mutated_reg map mut r) -> - reg_in_map map r \/ ~(In r rl) -> - rs'#r = rs#r). + reg_valid r s -> reg_in_map map r \/ ~(In r rl) -> rs'#r = rs#r). Definition transl_condition_correct (sp: val) (le: letenv) (e: env) (m: mem) (a: condexpr) - (t: trace) (e': env) (m': mem) (vb: bool) : Prop := - forall map mut ntrue nfalse s ns s' rs + (t: trace) (m': mem) (vb: bool) : Prop := + forall map ntrue nfalse s ns s' rs (MWF: map_wf map s) - (TE: transl_condition map mut a ntrue nfalse s = OK ns s') - (ME: match_env map e le rs) - (MUT: incl (mutated_condexpr a) mut), + (TE: transl_condition map a ntrue nfalse s = OK ns s') + (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' - /\ match_env map e' le rs' - /\ (forall r, - reg_valid r s -> ~(mutated_reg map mut r) -> - rs'#r = rs#r). + /\ 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 @@ -283,7 +274,7 @@ Definition transl_function_correct 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 e m 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. @@ -294,43 +285,40 @@ Proof. (* Exec *) split. assumption. (* Match-env *) - split. inversion TRG. + split. inversion TRG; subst. (* Optimized case rd = r *) - rewrite MV in H5; injection H5; intro; subst 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. red; intro; subst r1. contradiction. + assumption. intros. apply OTHER1. congruence. (* Result value *) split. rewrite RES1. eauto with rtlg. (* Other regs *) - intros. case (Reg.eq rd r0); intro. - subst r0. inversion TRG. - rewrite MV in H8; injection H8; intro; subst r. apply RES1. - byContradiction. tauto. - apply OTHER1; auto. + intros. destruct (Reg.eq rd r0). + subst r0. inversion TRG; subst. + congruence. + byContradiction. tauto. + auto. intro; monadSimpl. Qed. Lemma transl_expr_Eop_correct: forall (sp: val) (le : letenv) (e : env) (m : mem) (op : operation) - (al : exprlist) (t: trace) (e1 : env) (m1 : mem) (vl : list val) + (al : exprlist) (t: trace) (m1 : mem) (vl : list val) (v: val), - eval_exprlist ge sp le e m al t e1 m1 vl -> - transl_exprlist_correct sp le e m al t e1 m1 vl -> + 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 -> - transl_expr_correct sp le e m (Eop op al) t e1 m1 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. - simpl in MUT. - assert (TRG': target_regs_ok s1 map mut al l); eauto with rtlg. - assert (MWF': map_wf map s1). eauto with rtlg. - generalize (TEL _ _ _ _ _ _ _ _ MWF' EQ1 ME MUT TRG'). + exploit TEL. 2: eauto. eauto with rtlg. eauto. eauto with rtlg. intros [rs1 [EX1 [ME1 [RR1 RO1]]]]. exists (rs1#rd <- v). (* Exec *) @@ -347,74 +335,31 @@ Proof. split. apply Regmap.gss. (* Other regs *) intros. rewrite Regmap.gso. - apply RO1. eauto with rtlg. assumption. - case (In_dec Reg.eq r l); intro. - left. elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r i); intro. - assumption. byContradiction; eauto with rtlg. - right; assumption. + 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 H1; intro. inversion TRG. contradiction. + elim H0; intro. inversion TRG. contradiction. tauto. Qed. -Lemma transl_expr_Eassign_correct: - forall (sp: val) (le : letenv) (e : env) (m : mem) - (id : ident) (a : expr) (t: trace) (e1 : env) (m1 : mem) - (v : val), - eval_expr ge sp le e m a t e1 m1 v -> - transl_expr_correct sp le e m a t e1 m1 v -> - transl_expr_correct sp le e m (Eassign id a) t (PTree.set id v e1) m1 v. -Proof. - intros; red; intros. - simpl in TE. monadInv TE. intro EQ1. - simpl in MUT. - assert (MWF0: map_wf map s1). eauto with rtlg. - assert (MUTa: incl (mutated_expr a) mut). - red. intros. apply MUT. simpl. tauto. - assert (TRGa: target_reg_ok s1 map mut a rd). - inversion TRG. apply target_reg_other; eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ _ MWF0 EQ1 ME MUTa TRGa). - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - generalize (add_move_correct _ _ sp _ _ _ _ rs1 m1 EQ0). - intros [rs2 [EX2 [RES2 OTHER2]]]. - exists rs2. -(* Exec *) - split. eapply exec_trans. eexact EX1. - apply exec_instrs_incr with s1. eauto with rtlg. - eexact EX2. traceEq. -(* Match-env *) - split. - apply match_env_update_var with rs1 r s s0; auto. - congruence. -(* Result *) - split. case (Reg.eq rd r); intro. - subst r. congruence. - rewrite OTHER2; auto. -(* Other regs *) - intros. transitivity (rs1#r0). - apply OTHER2. red; intro; subst r0. - apply H2. red. exists id. split. apply MUT. red; tauto. - generalize EQ; unfold find_var. - destruct ((map_vars map)!id); monadSimpl. congruence. - apply OTHER1. eauto with rtlg. assumption. assumption. -Qed. - Lemma transl_expr_Eload_correct: forall (sp: val) (le : letenv) (e : env) (m : mem) (chunk : memory_chunk) (addr : addressing) - (al : exprlist) (t: trace) (e1 : env) (m1 : mem) (v : val) + (al : exprlist) (t: trace) (m1 : mem) (v : val) (vl : list val) (a: val), - eval_exprlist ge sp le e m al t e1 m1 vl -> - transl_exprlist_correct sp le e m al t e1 m1 vl -> + 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 e1 m1 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. - simpl in MUT. assert (MWF1: map_wf map s1). eauto with rtlg. - assert (TRG1: target_regs_ok s1 map mut al l). eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT TRG1). + assert (TRG1: target_regs_ok s1 map al l). eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG1). intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. exists (rs1#rd <- v). (* Exec *) @@ -429,9 +374,9 @@ Proof. split. apply Regmap.gss. (* Other regs *) intros. rewrite Regmap.gso. apply OTHER1. - eauto with rtlg. assumption. + eauto with rtlg. case (In_dec Reg.eq r l); intro. - elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r i); 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. @@ -440,34 +385,31 @@ 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) (e1 : env) (m1 : mem) - (vl : list val) (t2: trace) (e2 : env) (m2 m3 : mem) + (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 e1 m1 vl -> - transl_exprlist_correct sp le e m al t1 e1 m1 vl -> - eval_expr ge sp le e1 m1 b t2 e2 m2 v -> - transl_expr_correct sp le e1 m1 b t2 e2 m2 v -> + 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 e2 m3 v. + 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. - simpl in MUT. assert (MWF2: map_wf map s2). apply map_wf_incr with s. apply state_incr_trans2 with s0 s1; eauto with rtlg. assumption. - assert (MUT2: incl (mutated_exprlist al) mut). eauto with coqlib. - assert (TRG2: target_regs_ok s2 map mut al l). + assert (TRG2: target_regs_ok s2 map al l). apply target_regs_ok_incr with s0; eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ _ MWF2 EQ2 ME MUT2 TRG2). + generalize (H0 _ _ _ _ _ _ _ MWF2 EQ2 ME TRG2). intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. assert (MWF1: map_wf map s1). eauto with rtlg. - assert (MUT1: incl (mutated_expr b) mut). eauto with coqlib. - assert (TRG1: target_reg_ok s1 map mut b rd). + assert (TRG1: target_reg_ok s1 map b rd). inversion TRG. apply target_reg_other; eauto with rtlg. - generalize (H2 _ _ _ _ _ _ _ _ MWF1 EQ1 ME1 MUT1 TRG1). + generalize (H2 _ _ _ _ _ _ _ MWF1 EQ1 ME1 TRG1). intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exists rs2. (* Exec *) @@ -479,7 +421,7 @@ Proof. assert (rs2##l = rs1##l). apply list_map_exten. intros r' IN. symmetry. apply OTHER2. eauto with rtlg. eauto with rtlg. - elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r' IN); intro. + 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. @@ -495,55 +437,53 @@ Proof. (* Other regs *) intro r'; intros. transitivity (rs1#r'). apply OTHER2. apply reg_valid_incr with s; eauto with rtlg. - assumption. assumption. + assumption. apply OTHER1. apply reg_valid_incr with s. apply state_incr_trans2 with s0 s1; eauto with rtlg. assumption. - assumption. case (In_dec Reg.eq r' l); intro. - elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r' i); intro. + case (In_dec Reg.eq r' l); intro. + elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWF EQ r' i); intro. tauto. byContradiction; eauto with rtlg. tauto. Qed. Lemma transl_expr_Ecall_correct: forall (sp: val) (le : letenv) (e : env) (m : mem) (sig : signature) (a : expr) (bl : exprlist) (t t1: trace) - (e1: env) (m1: mem) (t2: trace) (e2 : env) (m2 : mem) + (m1: mem) (t2: trace) (m2 : mem) (t3: trace) (m3: mem) (vf : val) (vargs : list val) (vres : val) (f : Cminor.fundef), - eval_expr ge sp le e m a t1 e1 m1 vf -> - transl_expr_correct sp le e m a t1 e1 m1 vf -> - eval_exprlist ge sp le e1 m1 bl t2 e2 m2 vargs -> - transl_exprlist_correct sp le e1 m1 bl t2 e2 m2 vargs -> + 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 -> 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 e2 m3 vres. + 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 (MUTa: incl (mutated_expr a) mut). eauto with coqlib. - assert (MUTbl: incl (mutated_exprlist bl) mut). eauto with coqlib. assert (MWFa: map_wf map s3). apply map_wf_incr with s. apply state_incr_trans3 with s0 s1 s2; eauto with rtlg. assumption. - assert (TRGr: target_reg_ok s3 map mut a r). + 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 MUTa TRGr). + generalize (H0 _ _ _ _ _ _ _ MWFa EQ3 ME TRGr). intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - clear MUTa MWFa TRGr. + 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 mut bl l). + assert (TRGl: target_regs_ok s2 map bl l). apply target_regs_ok_incr with s1; eauto with rtlg. - generalize (H2 _ _ _ _ _ _ _ _ MWFbl EQ2 ME1 MUTbl TRGl). + generalize (H2 _ _ _ _ _ _ _ MWFbl EQ2 ME1 TRGl). intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. - clear MUTbl MWFbl TRGl. + clear MWFbl TRGl. generalize (functions_translated vf f H3). intros [tf [TFIND TF]]. generalize (H6 tf TF). intro EXF. @@ -554,11 +494,9 @@ Proof. eauto with rtlg. simpl. replace (rs2#r) with vf. eexact TFIND. rewrite <- RES1. symmetry. apply OTHER2. apply reg_valid_incr with s0; eauto with rtlg. - apply target_reg_not_mutated with s0 a. - eauto with rtlg. eauto with rtlg. assert (MWFs0: map_wf map s0). eauto with rtlg. case (In_dec Reg.eq r l); intro. - elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWFs0 EQ0 r i); intro. + 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. @@ -584,10 +522,9 @@ Proof. apply reg_valid_incr with s. apply state_incr_trans2 with s0 s1; eauto with rtlg. assumption. - assumption. assert (MWFs0: map_wf map s0). eauto with rtlg. case (In_dec Reg.eq r0 l); intro. - elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWFs0 EQ0 r0 i); intro. + 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. @@ -595,10 +532,9 @@ Proof. apply reg_valid_incr with s. apply state_incr_trans3 with s0 s1 s2; eauto with rtlg. assumption. - assumption. case (Reg.eq r0 r); intro. subst r0. - elim (alloc_reg_fresh_or_in_map _ _ _ _ _ _ MWF EQ); intro. + elim (alloc_reg_fresh_or_in_map _ _ _ _ _ MWF EQ); intro. tauto. byContradiction; eauto with rtlg. tauto. red; intro; subst r0. @@ -607,30 +543,27 @@ Qed. Lemma transl_expr_Econdition_correct: forall (sp: val) (le : letenv) (e : env) (m : mem) - (a : condexpr) (b c : expr) (t t1: trace) (e1 : env) (m1 : mem) - (v1 : bool) (t2: trace) (e2 : env) (m2 : mem) (v2 : val), - eval_condexpr ge sp le e m a t1 e1 m1 v1 -> - transl_condition_correct sp le e m a t1 e1 m1 v1 -> - eval_expr ge sp le e1 m1 (if v1 then b else c) t2 e2 m2 v2 -> - transl_expr_correct sp le e1 m1 (if v1 then b else c) t2 e2 m2 v2 -> + (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 e2 m2 v2. + 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. - simpl in MUT. assert (MWF1: map_wf map s1). apply map_wf_incr with s. eauto with rtlg. assumption. - assert (MUT1: incl (mutated_condexpr a) mut). eauto with coqlib. - generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT1). + generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME). intros [rs1 [EX1 [ME1 OTHER1]]]. destruct v1. assert (MWF0: map_wf map s0). eauto with rtlg. - assert (MUT0: incl (mutated_expr b) mut). eauto with coqlib. - assert (TRG0: target_reg_ok s0 map mut b rd). + assert (TRG0: target_reg_ok s0 map b rd). inversion TRG. apply target_reg_other; eauto with rtlg. - generalize (H2 _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 MUT0 TRG0). + generalize (H2 _ _ _ _ _ _ _ MWF0 EQ0 ME1 TRG0). intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exists rs2. (* Exec *) @@ -647,10 +580,9 @@ Proof. apply OTHER1; auto. apply reg_valid_incr with s. apply state_incr_trans with s0; eauto with rtlg. assumption. - assert (MUTc: incl (mutated_expr c) mut). eauto with coqlib. - assert (TRGc: target_reg_ok s map mut c rd). + assert (TRGc: target_reg_ok s map c rd). inversion TRG. apply target_reg_other; auto. - generalize (H2 _ _ _ _ _ _ _ _ MWF EQ ME1 MUTc TRGc). + generalize (H2 _ _ _ _ _ _ _ MWF EQ ME1 TRGc). intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exists rs2. (* Exec *) @@ -670,38 +602,35 @@ Qed. Lemma transl_expr_Elet_correct: forall (sp: val) (le : letenv) (e : env) (m : mem) - (a b : expr) (t t1: trace) (e1 : env) (m1 : mem) (v1 : val) - (t2: trace) (e2 : env) (m2 : mem) (v2 : val), - eval_expr ge sp le e m a t1 e1 m1 v1 -> - transl_expr_correct sp le e m a t1 e1 m1 v1 -> - eval_expr ge sp (v1 :: le) e1 m1 b t2 e2 m2 v2 -> - transl_expr_correct sp (v1 :: le) e1 m1 b t2 e2 m2 v2 -> + (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 e2 m2 v2. + transl_expr_correct sp le e m (Elet a b) t m2 v2. Proof. intros; red; intros. simpl in TE; monadInv TE. intro EQ1. - simpl in MUT. assert (MWF1: map_wf map s1). eauto with rtlg. - assert (MUT1: incl (mutated_expr a) mut). eauto with coqlib. - assert (TRG1: target_reg_ok s1 map mut a r). + assert (TRG1: target_reg_ok s1 map a r). eapply target_reg_other; eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT1 TRG1). + 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 (MUT2: incl (mutated_expr b) mut). eauto with coqlib. - assert (ME2: match_env (add_letvar map r) e1 (v1 :: le) rs1). + 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) mut b rd). + 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 H11; intro. apply H4. left. assumption. - elim H12; intro. apply valid_fresh_absurd with rd s. - assumption. rewrite <- H13. eauto with rtlg. + 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 MUT2 TRG2). + generalize (H2 _ _ _ _ _ _ _ MWF2 EQ0 ME2 TRG2). intros [rs2 [EX2 [ME3 [RES2 OTHER2]]]]. exists rs2. (* Exec *) @@ -716,22 +645,20 @@ Proof. (* Other regs *) intros. transitivity (rs1#r0). apply OTHER2. eauto with rtlg. - unfold mutated_reg. unfold add_letvar; simpl. assumption. - elim H6; intro. left. + elim H5; intro. left. unfold reg_in_map, add_letvar; simpl. - unfold reg_in_map in H7; tauto. + unfold reg_in_map in H6; tauto. tauto. apply OTHER1. eauto with rtlg. - assumption. right. red; intro. apply valid_fresh_absurd with r0 s. - assumption. rewrite H7. eauto with rtlg. + assumption. rewrite H6. eauto with rtlg. Qed. Lemma transl_expr_Eletvar_correct: forall (sp: val) (le : list val) (e : env) (m : mem) (n : nat) (v : val), nth_error le n = Some v -> - transl_expr_correct sp le e m (Eletvar n) E0 e m v. + transl_expr_correct sp le e m (Eletvar n) E0 m v. Proof. intros; red; intros. simpl in TE; monadInv TE. intro EQ1. @@ -766,19 +693,18 @@ Qed. Lemma transl_expr_Ealloc_correct: forall (sp: val) (le : letenv) (e : env) (m : mem) - (a : expr) (t: trace) (e1 : env) (m1 : mem) (n: int) + (a : expr) (t: trace) (m1 : mem) (n: int) (m2: mem) (b: block), - eval_expr ge sp le e m a t e1 m1 (Vint n) -> - transl_expr_correct sp le e m a t e1 m1 (Vint n) -> + 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 e1 m2 (Vptr b Int.zero). + 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. - simpl in MUT. - assert (TRG': target_reg_ok s1 map mut a r); eauto with rtlg. + 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 MUT TRG'). + generalize (TEC _ _ _ _ _ _ _ MWF' EQ1 ME TRG'). intros [rs1 [EX1 [ME1 [RR1 RO1]]]]. exists (rs1#rd <- (Vptr b Int.zero)). (* Exec *) @@ -792,18 +718,18 @@ Proof. split. apply Regmap.gss. (* Other regs *) intros. rewrite Regmap.gso. - apply RO1. eauto with rtlg. assumption. + apply RO1. eauto with rtlg. case (Reg.eq r0 r); intro. - subst r0. left. elim (alloc_reg_fresh_or_in_map _ _ _ _ _ _ MWF EQ); intro. + subst r0. left. elim (alloc_reg_fresh_or_in_map _ _ _ _ _ MWF EQ); intro. auto. byContradiction; eauto with rtlg. right; assumption. - elim H1; intro. red; intro. subst r0. inversion TRG. contradiction. + elim H0; intro. red; intro. subst r0. inversion TRG. contradiction. auto. Qed. Lemma transl_condition_CEtrue_correct: forall (sp: val) (le : letenv) (e : env) (m : mem), - transl_condition_correct sp le e m CEtrue E0 e m true. + 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. @@ -811,7 +737,7 @@ Qed. Lemma transl_condition_CEfalse_correct: forall (sp: val) (le : letenv) (e : env) (m : mem), - transl_condition_correct sp le e m CEfalse E0 e m false. + 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. @@ -819,19 +745,17 @@ Qed. Lemma transl_condition_CEcond_correct: forall (sp: val) (le : letenv) (e : env) (m : mem) - (cond : condition) (al : exprlist) (t1: trace) (e1 : env) + (cond : condition) (al : exprlist) (t1: trace) (m1 : mem) (vl : list val) (b : bool), - eval_exprlist ge sp le e m al t1 e1 m1 vl -> - transl_exprlist_correct sp le e m al t1 e1 m1 vl -> + 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 -> - transl_condition_correct sp le e m (CEcond cond al) t1 e1 m1 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. - simpl in MUT. - assert (TRG: target_regs_ok s1 map mut al l). - eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT TRG). + assert (TRG: target_regs_ok s1 map al l). eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG). intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. exists rs1. (* Exec *) @@ -847,35 +771,32 @@ Proof. (* Match-env *) split. assumption. (* Regs *) - intros. apply OTHER1. eauto with rtlg. assumption. + 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. + elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWF EQ r i); intro. tauto. byContradiction; eauto with rtlg. tauto. Qed. Lemma transl_condition_CEcondition_correct: forall (sp: val) (le : letenv) (e : env) (m : mem) - (a b c : condexpr) (t t1: trace) (e1 : env) (m1 : mem) - (vb1 : bool) (t2: trace) (e2 : env) (m2 : mem) (vb2 : bool), - eval_condexpr ge sp le e m a t1 e1 m1 vb1 -> - transl_condition_correct sp le e m a t1 e1 m1 vb1 -> - eval_condexpr ge sp le e1 m1 (if vb1 then b else c) t2 e2 m2 vb2 -> - transl_condition_correct sp le e1 m1 (if vb1 then b else c) t2 e2 m2 vb2 -> + (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 e2 m2 vb2. + 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. - simpl in MUT. assert (MWF1: map_wf map s1). eauto with rtlg. - assert (MUTa: incl (mutated_condexpr a) mut). eauto with coqlib. - generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUTa). + generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME). intros [rs1 [EX1 [ME1 OTHER1]]]. destruct vb1. assert (MWF0: map_wf map s0). eauto with rtlg. - assert (MUTb: incl (mutated_condexpr b) mut). eauto with coqlib. - generalize (H2 _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 MUTb). + generalize (H2 _ _ _ _ _ _ _ MWF0 EQ0 ME1). intros [rs2 [EX2 [ME2 OTHER2]]]. exists rs2. split. eapply exec_trans. eexact EX1. @@ -886,8 +807,7 @@ Proof. apply OTHER2; eauto with rtlg. apply OTHER1; eauto with rtlg. - assert (MUTc: incl (mutated_condexpr c) mut). eauto with coqlib. - generalize (H2 _ _ _ _ _ _ _ _ MWF EQ ME1 MUTc). + generalize (H2 _ _ _ _ _ _ _ MWF EQ ME1). intros [rs2 [EX2 [ME2 OTHER2]]]. exists rs2. split. eapply exec_trans. eexact EX1. @@ -901,7 +821,7 @@ Qed. Lemma transl_exprlist_Enil_correct: forall (sp: val) (le : letenv) (e : env) (m : mem), - transl_exprlist_correct sp le e m Enil E0 e m nil. + transl_exprlist_correct sp le e m Enil E0 m nil. Proof. intros; red; intros. generalize TE. simpl. destruct rl; monadSimpl. @@ -914,26 +834,23 @@ Qed. Lemma transl_exprlist_Econs_correct: forall (sp: val) (le : letenv) (e : env) (m : mem) - (a : expr) (bl : exprlist) (t t1: trace) (e1 : env) (m1 : mem) - (v : val) (t2: trace) (e2 : env) (m2 : mem) (vl : list val), - eval_expr ge sp le e m a t1 e1 m1 v -> - transl_expr_correct sp le e m a t1 e1 m1 v -> - eval_exprlist ge sp le e1 m1 bl t2 e2 m2 vl -> - transl_exprlist_correct sp le e1 m1 bl t2 e2 m2 vl -> + (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 e2 m2 (v :: vl). + transl_exprlist_correct sp le e m (Econs a bl) t m2 (v :: vl). Proof. intros. red. intros. inversion TRG. - rewrite <- H11 in TE. simpl in TE. monadInv TE. intro EQ1. - simpl in MUT. - assert (MUT1: incl (mutated_expr a) mut); eauto with coqlib. - assert (MUT2: incl (mutated_exprlist bl) mut); eauto with coqlib. + 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 mut a r); eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT1 TRG1). + 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 MUT2 H12). + generalize (H2 _ _ _ _ _ _ _ MWF EQ ME1 H11). intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exists rs2. (* Exec *) @@ -947,13 +864,12 @@ Proof. reflexivity. eauto with rtlg. eauto with rtlg. - assumption. (* Other regs *) simpl. intros. transitivity (rs1#r0). apply OTHER2; auto. tauto. apply OTHER1; auto. eauto with rtlg. - elim H15; intro. left; assumption. right; apply sym_not_equal; tauto. + elim H13; intro. left; assumption. right; apply sym_not_equal; tauto. Qed. Lemma transl_funcall_internal_correct: @@ -1084,36 +1000,65 @@ Qed. Lemma transl_stmt_Sexpr_correct: forall (sp: val) (e : env) (m : mem) (a : expr) (t: trace) - (e1 : env) (m1 : mem) (v : val), - eval_expr ge sp nil e m a t e1 m1 v -> - transl_expr_correct sp nil e m a t e1 m1 v -> - transl_stmt_correct sp e m (Sexpr a) t e1 m1 Out_normal. + (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. Proof. intros; red; intros. simpl in OUT. subst nd. unfold transl_stmt in TE. monadInv TE. intro EQ1. assert (MWF0: map_wf map s0). eauto with rtlg. - assert (TRG: target_reg_ok s0 map (mutated_expr a) a r). eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ _ MWF0 EQ1 ME (incl_refl (mutated_expr a)) TRG). + 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. 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. +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. +Qed. + Lemma transl_stmt_Sifthenelse_correct: forall (sp: val) (e : env) (m : mem) (a : condexpr) - (s1 s2 : stmt) (t t1: trace) (e1 : env) (m1 : mem) + (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 e1 m1 v1 -> - transl_condition_correct sp nil e m a t1 e1 m1 v1 -> - exec_stmt ge sp e1 m1 (if v1 then s1 else s2) t2 e2 m2 out -> - transl_stmt_correct sp e1 m1 (if v1 then s1 else s2) t2 e2 m2 out -> + 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. 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 (incl_refl _)). + generalize (H0 _ _ _ _ _ _ rs MWF1 EQ2 ME). intros [rs1 [EX1 [ME1 OTHER1]]]. destruct v1. assert (MWF0: map_wf map s0). eauto with rtlg. @@ -1132,7 +1077,7 @@ Proof. tauto. assert (MWF1: map_wf map s3). eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ rs MWF1 EQ2 ME (incl_refl _)). + generalize (H0 _ _ _ _ _ _ rs MWF1 EQ2 ME). intros [rs1 [EX1 [ME1 OTHER1]]]. destruct v1. generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF EQ ME1 OUT RRG). @@ -1291,10 +1236,10 @@ Qed. Lemma transl_stmt_Sswitch_correct: forall (sp : val) (e : env) (m : mem) (a : expr) (cases : list (int * nat)) (default : nat) - (t1 : trace) (e1 : env) (m1 : mem) (n : int), - eval_expr ge sp nil e m a t1 e1 m1 (Vint n) -> - transl_expr_correct sp nil e m a t1 e1 m1 (Vint n) -> - transl_stmt_correct sp e m (Sswitch a cases default) t1 e1 m1 + (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 (Out_exit (switch_target n default cases)). Proof. intros; red; intros. monadInv TE. clear TE; intros EQ1. @@ -1303,8 +1248,8 @@ Proof. red in H0. assert (MWF1: map_wf map s1). eauto with rtlg. - assert (TRG1: target_reg_ok s1 map (mutated_expr a) a r). eauto with rtlg. - destruct (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME (incl_refl _) TRG1) + 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 *) @@ -1327,16 +1272,16 @@ Qed. Lemma transl_stmt_Sreturn_some_correct: forall (sp: val) (e : env) (m : mem) (a : expr) (t: trace) - (e1 : env) (m1 : mem) (v : val), - eval_expr ge sp nil e m a t e1 m1 v -> - transl_expr_correct sp nil e m a t e1 m1 v -> - transl_stmt_correct sp e m (Sreturn (Some a)) t e1 m1 (Out_return (Some v)). + (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)). Proof. intros; red; intros. generalize TE; simpl. destruct rret. intro EQ. - assert (TRG: target_reg_ok s map (mutated_expr a) a r). + assert (TRG: target_reg_ok s map a r). inversion RRG. apply target_reg_other; auto. - generalize (H0 _ _ _ _ _ _ _ _ MWF EQ ME (incl_refl _) TRG). + generalize (H0 _ _ _ _ _ _ _ MWF EQ ME TRG). intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. simpl in OUT. subst nd. exists rs1. tauto. @@ -1366,7 +1311,6 @@ Proof transl_stmt_correct transl_expr_Evar_correct - transl_expr_Eassign_correct transl_expr_Eop_correct transl_expr_Eload_correct transl_expr_Estore_correct @@ -1385,6 +1329,7 @@ Proof transl_funcall_external_correct transl_stmt_Sskip_correct transl_stmt_Sexpr_correct + transl_stmt_Sassign_correct transl_stmt_Sifthenelse_correct transl_stmt_Sseq_continue_correct transl_stmt_Sseq_stop_correct -- cgit v1.2.3