From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- backend/ValueAnalysis.v | 628 ++++++++++++++++++++++++------------------------ 1 file changed, 314 insertions(+), 314 deletions(-) (limited to 'backend/ValueAnalysis.v') diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 22121075..979f8c0e 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -231,7 +231,7 @@ Definition definitive_initializer (init: list init_data) : bool := Definition alloc_global (rm: romem) (idg: ident * globdef fundef unit): romem := match idg with - | (id, Gfun f) => + | (id, Gfun f) => PTree.remove id rm | (id, Gvar v) => if v.(gvar_readonly) && negb v.(gvar_volatile) && definitive_initializer v.(gvar_init) @@ -255,26 +255,26 @@ Lemma analyze_entrypoint: /\ ematch bc (init_regs vl (fn_params f)) ae /\ mmatch bc m am. Proof. - intros. - unfold analyze. + intros. + unfold analyze. set (lu := Liveness.last_uses f). set (entry := VA.State (einit_regs f.(fn_params)) mfunction_entry). destruct (DS.fixpoint (fn_code f) successors_instr (transfer' f lu rm) (fn_entrypoint f) entry) as [res|] eqn:FIX. - assert (A: VA.ge res!!(fn_entrypoint f) entry) by (eapply DS.fixpoint_entry; eauto). destruct (res!!(fn_entrypoint f)) as [ | ae am ]; simpl in A. contradiction. - destruct A as [A1 A2]. - exists ae, am. - split. auto. - split. eapply ematch_ge; eauto. apply ematch_init; auto. + destruct A as [A1 A2]. + exists ae, am. + split. auto. + split. eapply ematch_ge; eauto. apply ematch_init; auto. auto. - exists AE.top, mtop. - split. apply PMap.gi. - split. apply ematch_ge with (einit_regs (fn_params f)). - apply ematch_init; auto. apply AE.ge_top. - eapply mmatch_top'; eauto. + split. apply PMap.gi. + split. apply ematch_ge with (einit_regs (fn_params f)). + apply ematch_init; auto. apply AE.ge_top. + eapply mmatch_top'; eauto. Qed. - + Lemma analyze_successor: forall f n ae am instr s rm ae' am', (analyze rm f)!!n = VA.State ae am -> @@ -291,9 +291,9 @@ Proof. - assert (A: VA.ge res!!s (transfer' f lu rm n res#n)). { eapply DS.fixpoint_solution; eauto with coqlib. intros. unfold transfer'. simpl. auto. } - rewrite H in A. unfold transfer' in A. rewrite H2 in A. rewrite H2. + rewrite H in A. unfold transfer' in A. rewrite H2 in A. rewrite H2. destruct lu!n. - eapply VA.ge_trans. eauto. split; auto. apply eforget_ge. + eapply VA.ge_trans. eauto. split; auto. apply eforget_ge. auto. - rewrite H2. rewrite PMap.gi. split; intros. apply AE.ge_top. eapply mmatch_top'; eauto. Qed. @@ -311,11 +311,11 @@ Lemma analyze_succ: /\ ematch bc e ae'' /\ mmatch bc m am''. Proof. - intros. exploit analyze_successor; eauto. rewrite H2. + intros. exploit analyze_successor; eauto. rewrite H2. destruct (analyze rm f)#s as [ | ae'' am'']; simpl; try tauto. intros [A B]. exists ae'', am''. - split. auto. - split. eapply ematch_ge; eauto. eauto. + split. auto. + split. eapply ematch_ge; eauto. eauto. Qed. (** ** Analysis of registers and builtin arguments *) @@ -323,7 +323,7 @@ Qed. Lemma areg_sound: forall bc e ae r, ematch bc e ae -> vmatch bc (e#r) (areg ae r). Proof. - intros. apply H. + intros. apply H. Qed. Lemma aregs_sound: @@ -347,8 +347,8 @@ Lemma abuiltin_arg_sound: Proof. intros until am; intros EM RM MM GM SP. induction 1; simpl; eauto with va. -- eapply loadv_sound; eauto. simpl. rewrite Int.add_zero_l. auto with va. -- simpl. rewrite Int.add_zero_l. auto with va. +- eapply loadv_sound; eauto. simpl. rewrite Int.add_zero_l. auto with va. +- simpl. rewrite Int.add_zero_l. auto with va. - eapply loadv_sound; eauto. apply symbol_address_sound; auto. - apply symbol_address_sound; auto. Qed. @@ -367,7 +367,7 @@ Proof. intros until am; intros EM RM MM GM SP. induction 1; simpl. - constructor. -- constructor; auto. eapply abuiltin_arg_sound; eauto. +- constructor; auto. eapply abuiltin_arg_sound; eauto. Qed. Lemma set_builtin_res_sound: @@ -376,7 +376,7 @@ Lemma set_builtin_res_sound: vmatch bc v av -> ematch bc (regmap_setres res v rs) (set_builtin_res res av ae). Proof. - intros. destruct res; simpl; auto. apply ematch_update; auto. + intros. destruct res; simpl; auto. apply ematch_update; auto. Qed. (** ** Constructing block classifications *) @@ -396,24 +396,24 @@ Qed. Lemma vmatch_no_stack: forall v x, vmatch bc v x -> vmatch bc v (Ifptr Nonstack). Proof. - induction 1; constructor; auto; eapply pmatch_no_stack; eauto. + induction 1; constructor; auto; eapply pmatch_no_stack; eauto. Qed. Lemma smatch_no_stack: forall m b p, smatch bc m b p -> smatch bc m b Nonstack. Proof. - intros. destruct H as [A B]. split; intros. - eapply vmatch_no_stack; eauto. - eapply pmatch_no_stack; eauto. + intros. destruct H as [A B]. split; intros. + eapply vmatch_no_stack; eauto. + eapply pmatch_no_stack; eauto. Qed. Lemma mmatch_no_stack: forall m am astk, mmatch bc m am -> mmatch bc m {| am_stack := astk; am_glob := PTree.empty _; am_nonstack := Nonstack; am_top := Nonstack |}. Proof. intros. destruct H. constructor; simpl; intros. -- elim (NOSTACK b); auto. +- elim (NOSTACK b); auto. - rewrite PTree.gempty in H0; discriminate. -- eapply smatch_no_stack; eauto. -- eapply smatch_no_stack; eauto. +- eapply smatch_no_stack; eauto. +- eapply smatch_no_stack; eauto. - auto. Qed. @@ -439,8 +439,8 @@ Theorem allocate_stack: /\ (forall b, Plt b sp -> bc' b = bc b) /\ (forall v x, vmatch bc v x -> vmatch bc' v (Ifptr Nonstack)). Proof. - intros until am; intros ALLOC GENV RO MM NOSTACK. - exploit Mem.nextblock_alloc; eauto. intros NB. + intros until am; intros ALLOC GENV RO MM NOSTACK. + exploit Mem.nextblock_alloc; eauto. intros NB. exploit Mem.alloc_result; eauto. intros SP. assert (SPINVALID: bc sp = BCinvalid). { rewrite SP. eapply bc_below_invalid. apply Plt_strict. eapply mmatch_below; eauto. } @@ -450,13 +450,13 @@ Proof. { assert (forall b, f b = BCstack -> b = sp). { unfold f; intros. destruct (eq_block b sp); auto. eelim NOSTACK; eauto. } - intros. transitivity sp; auto. symmetry; auto. + intros. transitivity sp; auto. symmetry; auto. } assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2). { assert (forall b id, f b = BCglob id -> bc b = BCglob id). { unfold f; intros. destruct (eq_block b sp). congruence. auto. } - intros. eapply (bc_glob bc); eauto. + intros. eapply (bc_glob bc); eauto. } set (bc' := BC f F_stack F_glob). unfold f in bc'. assert (BC'EQ: forall b, bc b <> BCinvalid -> bc' b = bc b). @@ -466,15 +466,15 @@ Proof. (* Part 2: invariance properties *) assert (SM: forall b p, bc b <> BCinvalid -> smatch bc m b p -> smatch bc' m' b Nonstack). { - intros. + intros. apply smatch_incr with bc; auto. - apply smatch_inv with m. + apply smatch_inv with m. apply smatch_no_stack with p; auto. - intros. eapply Mem.loadbytes_alloc_unchanged; eauto. eapply mmatch_below; eauto. + intros. eapply Mem.loadbytes_alloc_unchanged; eauto. eapply mmatch_below; eauto. } assert (SMSTACK: smatch bc' m' sp Pbot). { - split; intros. + split; intros. exploit Mem.load_alloc_same; eauto. intros EQ. subst v. constructor. exploit Mem.loadbytes_alloc_same; eauto with coqlib. congruence. } @@ -483,15 +483,15 @@ Proof. - (* incr *) assumption. - (* sp is BCstack *) - simpl; apply dec_eq_true. + simpl; apply dec_eq_true. - (* genv match *) eapply genv_match_exten; eauto. simpl; intros. destruct (eq_block b sp); intuition congruence. - simpl; intros. destruct (eq_block b sp); congruence. + simpl; intros. destruct (eq_block b sp); congruence. - (* romatch *) - apply romatch_exten with bc. - eapply romatch_alloc; eauto. eapply mmatch_below; eauto. - simpl; intros. destruct (eq_block b sp); intuition. + apply romatch_exten with bc. + eapply romatch_alloc; eauto. eapply mmatch_below; eauto. + simpl; intros. destruct (eq_block b sp); intuition. - (* mmatch *) constructor; simpl; intros. + (* stack *) @@ -504,16 +504,16 @@ Proof. destruct (eq_block b sp). congruence. eapply SM; auto. eapply mmatch_nonstack; eauto. + (* top *) destruct (eq_block b sp). - subst b. apply smatch_ge with Pbot. apply SMSTACK. constructor. + subst b. apply smatch_ge with Pbot. apply SMSTACK. constructor. eapply SM; auto. eapply mmatch_top; eauto. + (* below *) - red; simpl; intros. rewrite NB. destruct (eq_block b sp). - subst b; rewrite SP; xomega. - exploit mmatch_below; eauto. xomega. + red; simpl; intros. rewrite NB. destruct (eq_block b sp). + subst b; rewrite SP; xomega. + exploit mmatch_below; eauto. xomega. - (* unchanged *) simpl; intros. apply dec_eq_false. apply Plt_ne. auto. - (* values *) - intros. apply vmatch_incr with bc; auto. eapply vmatch_no_stack; eauto. + intros. apply vmatch_incr with bc; auto. eapply vmatch_no_stack; eauto. Qed. (** Construction 2: turn the stack into an "other" block, at public calls or function returns *) @@ -540,15 +540,15 @@ Proof. { unfold f; intros. destruct (eq_block b1 sp); try discriminate. - destruct (eq_block b2 sp); try discriminate. - eapply bc_stack; eauto. + destruct (eq_block b2 sp); try discriminate. + eapply bc_stack; eauto. } assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2). { unfold f; intros. destruct (eq_block b1 sp); try discriminate. - destruct (eq_block b2 sp); try discriminate. - eapply bc_glob; eauto. + destruct (eq_block b2 sp); try discriminate. + eapply bc_glob; eauto. } set (bc' := BC f F_stack F_glob). unfold f in bc'. @@ -556,7 +556,7 @@ Proof. assert (PM: forall b ofs p, pmatch bc b ofs p -> pmatch bc' b ofs Ptop). { intros. assert (pmatch bc b ofs Ptop) by (eapply pmatch_top'; eauto). - inv H0. constructor; simpl. destruct (eq_block b sp); congruence. + inv H0. constructor; simpl. destruct (eq_block b sp); congruence. } assert (VM: forall v x, vmatch bc v x -> vmatch bc' v Vtop). { @@ -571,32 +571,32 @@ Proof. (* Conclusions *) exists bc'; splitall. - (* nostack *) - red; simpl; intros. destruct (eq_block b sp). congruence. - red; intros. elim n. eapply bc_stack; eauto. + red; simpl; intros. destruct (eq_block b sp). congruence. + red; intros. elim n. eapply bc_stack; eauto. - (* bc' sp is BCother *) - simpl; apply dec_eq_true. + simpl; apply dec_eq_true. - (* other blocks *) - intros; simpl; apply dec_eq_false; auto. + intros; simpl; apply dec_eq_false; auto. - (* values *) auto. - (* genv *) - apply genv_match_exten with bc; auto. + apply genv_match_exten with bc; auto. simpl; intros. destruct (eq_block b sp); intuition congruence. simpl; intros. destruct (eq_block b sp); auto. - (* romatch *) - apply romatch_exten with bc; auto. - simpl; intros. destruct (eq_block b sp); intuition. + apply romatch_exten with bc; auto. + simpl; intros. destruct (eq_block b sp); intuition. - (* mmatch top *) - constructor; simpl; intros. + constructor; simpl; intros. + destruct (eq_block b sp). congruence. elim n. eapply bc_stack; eauto. + rewrite PTree.gempty in H0; discriminate. + destruct (eq_block b sp). subst b. eapply SM. eapply mmatch_stack; eauto. - eapply SM. eapply mmatch_nonstack; eauto. + eapply SM. eapply mmatch_nonstack; eauto. + destruct (eq_block b sp). subst b. eapply SM. eapply mmatch_stack; eauto. eapply SM. eapply mmatch_top; eauto. - + red; simpl; intros. destruct (eq_block b sp). + + red; simpl; intros. destruct (eq_block b sp). subst b. eapply mmatch_below; eauto. congruence. eapply mmatch_below; eauto. Qed. @@ -626,15 +626,15 @@ Proof. { unfold f; intros. destruct (eq_block b1 sp); try discriminate. - destruct (eq_block b2 sp); try discriminate. - eapply bc_stack; eauto. + destruct (eq_block b2 sp); try discriminate. + eapply bc_stack; eauto. } assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2). { unfold f; intros. destruct (eq_block b1 sp); try discriminate. - destruct (eq_block b2 sp); try discriminate. - eapply bc_glob; eauto. + destruct (eq_block b2 sp); try discriminate. + eapply bc_glob; eauto. } set (bc' := BC f F_stack F_glob). unfold f in bc'. @@ -642,11 +642,11 @@ Proof. assert (PM: forall b ofs p, pge Nonstack p -> pmatch bc b ofs p -> pmatch bc' b ofs Ptop). { intros. assert (pmatch bc b ofs Nonstack) by (eapply pmatch_ge; eauto). - inv H1. constructor; simpl; destruct (eq_block b sp); congruence. + inv H1. constructor; simpl; destruct (eq_block b sp); congruence. } assert (VM: forall v x, vge (Ifptr Nonstack) x -> vmatch bc v x -> vmatch bc' v Vtop). { - intros. apply vmatch_ifptr; intros. subst v. + intros. apply vmatch_ifptr; intros. subst v. inv H0; inv H; eapply PM; eauto. } assert (SM: forall b p, pge Nonstack p -> smatch bc m b p -> smatch bc' m b Ptop). @@ -658,31 +658,31 @@ Proof. (* Conclusions *) exists bc'; splitall. - (* nostack *) - red; simpl; intros. destruct (eq_block b sp). congruence. - red; intros. elim n. eapply bc_stack; eauto. + red; simpl; intros. destruct (eq_block b sp). congruence. + red; intros. elim n. eapply bc_stack; eauto. - (* bc' sp is BCinvalid *) - simpl; apply dec_eq_true. + simpl; apply dec_eq_true. - (* other blocks *) - intros; simpl; apply dec_eq_false; auto. + intros; simpl; apply dec_eq_false; auto. - (* values *) auto. - (* genv *) - apply genv_match_exten with bc; auto. + apply genv_match_exten with bc; auto. simpl; intros. destruct (eq_block b sp); intuition congruence. simpl; intros. destruct (eq_block b sp); congruence. - (* romatch *) - apply romatch_exten with bc; auto. - simpl; intros. destruct (eq_block b sp); intuition. + apply romatch_exten with bc; auto. + simpl; intros. destruct (eq_block b sp); intuition. - (* mmatch top *) - constructor; simpl; intros. + constructor; simpl; intros. + destruct (eq_block b sp). congruence. elim n. eapply bc_stack; eauto. + rewrite PTree.gempty in H0; discriminate. + destruct (eq_block b sp). congruence. - eapply SM. eauto. eapply mmatch_nonstack; eauto. + eapply SM. eauto. eapply mmatch_nonstack; eauto. + destruct (eq_block b sp). congruence. - eapply SM. eauto. eapply mmatch_nonstack; eauto. - red; intros; elim n. eapply bc_stack; eauto. - + red; simpl; intros. destruct (eq_block b sp). congruence. + eapply SM. eauto. eapply mmatch_nonstack; eauto. + red; intros; elim n. eapply bc_stack; eauto. + + red; simpl; intros. destruct (eq_block b sp). congruence. eapply mmatch_below; eauto. Qed. @@ -718,29 +718,29 @@ Proof. { assert (forall b, f b = BCstack -> b = sp). { unfold f; intros. destruct (eq_block b sp); auto. eelim NOSTACK; eauto. } - intros. transitivity sp; auto. symmetry; auto. + intros. transitivity sp; auto. symmetry; auto. } assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2). { assert (forall b id, f b = BCglob id -> callee b = BCglob id). { unfold f; intros. destruct (eq_block b sp). congruence. auto. } - intros. eapply (bc_glob callee); eauto. + intros. eapply (bc_glob callee); eauto. } set (bc := BC f F_stack F_glob). unfold f in bc. assert (INCR: bc_incr caller bc). { - red; simpl; intros. destruct (eq_block b sp). congruence. - symmetry; apply SAME; auto. + red; simpl; intros. destruct (eq_block b sp). congruence. + symmetry; apply SAME; auto. } (* Invariance properties *) - assert (PM: forall b ofs p, pmatch callee b ofs p -> pmatch bc b ofs Ptop). + assert (PM: forall b ofs p, pmatch callee b ofs p -> pmatch bc b ofs Ptop). { intros. assert (pmatch callee b ofs Ptop) by (eapply pmatch_top'; eauto). inv H0. constructor; simpl. destruct (eq_block b sp); congruence. } assert (VM: forall v x, vmatch callee v x -> vmatch bc v Vtop). { - intros. assert (vmatch callee v0 Vtop) by (eapply vmatch_top; eauto). + intros. assert (vmatch callee v0 Vtop) by (eapply vmatch_top; eauto). inv H0; constructor; eauto. } assert (SM: forall b p, smatch callee m b p -> smatch bc m b Ptop). @@ -752,38 +752,38 @@ Proof. - (* result value *) eapply VM; eauto. - (* environment *) - eapply ematch_incr; eauto. + eapply ematch_incr; eauto. - (* romem *) apply romatch_exten with callee; auto. - intros; simpl. destruct (eq_block b sp); intuition. + intros; simpl. destruct (eq_block b sp); intuition. - (* mmatch *) constructor; simpl; intros. + (* stack *) apply ablock_init_sound. destruct (eq_block b sp). - subst b. eapply SM. eapply mmatch_nonstack; eauto. congruence. + subst b. eapply SM. eapply mmatch_nonstack; eauto. congruence. elim (NOSTACK b); auto. + (* globals *) rewrite PTree.gempty in H0; discriminate. + (* nonstack *) destruct (eq_block b sp). congruence. eapply SM; auto. eapply mmatch_nonstack; eauto. + (* top *) - eapply SM. eapply mmatch_top; eauto. + eapply SM. eapply mmatch_top; eauto. destruct (eq_block b sp); congruence. + (* below *) - red; simpl; intros. destruct (eq_block b sp). + red; simpl; intros. destruct (eq_block b sp). subst b. eapply mmatch_below; eauto. congruence. eapply mmatch_below; eauto. - (* genv *) eapply genv_match_exten with caller; eauto. - simpl; intros. destruct (eq_block b sp). intuition congruence. + simpl; intros. destruct (eq_block b sp). intuition congruence. split; intros. rewrite SAME in H by eauto with va. auto. apply <- (proj1 GE2) in H. apply (proj1 GE1) in H. auto. - simpl; intros. destruct (eq_block b sp). congruence. + simpl; intros. destruct (eq_block b sp). congruence. rewrite <- SAME; eauto with va. - (* sp *) simpl. apply dec_eq_true. - (* unchanged *) - simpl; intros. destruct (eq_block b sp). congruence. + simpl; intros. destruct (eq_block b sp). congruence. symmetry. apply SAME; auto. eapply Plt_trans. eauto. apply BELOW. congruence. Qed. @@ -820,19 +820,19 @@ Proof. { assert (forall b, f b = BCstack -> b = sp). { unfold f; intros. destruct (eq_block b sp); auto. eelim NOSTACK; eauto. } - intros. transitivity sp; auto. symmetry; auto. + intros. transitivity sp; auto. symmetry; auto. } assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2). { assert (forall b id, f b = BCglob id -> callee b = BCglob id). { unfold f; intros. destruct (eq_block b sp). congruence. auto. } - intros. eapply (bc_glob callee); eauto. + intros. eapply (bc_glob callee); eauto. } set (bc := BC f F_stack F_glob). unfold f in bc. assert (INCR1: bc_incr caller bc). { - red; simpl; intros. destruct (eq_block b sp). congruence. - symmetry; apply SAME; auto. + red; simpl; intros. destruct (eq_block b sp). congruence. + symmetry; apply SAME; auto. } assert (INCR2: bc_incr callee bc). { @@ -840,14 +840,14 @@ Proof. } (* Invariance properties *) - assert (PM: forall b ofs p, pmatch callee b ofs p -> pmatch bc b ofs Nonstack). + assert (PM: forall b ofs p, pmatch callee b ofs p -> pmatch bc b ofs Nonstack). { intros. assert (pmatch callee b ofs Ptop) by (eapply pmatch_top'; eauto). inv H0. constructor; simpl; destruct (eq_block b sp); congruence. } assert (VM: forall v x, vmatch callee v x -> vmatch bc v (Ifptr Nonstack)). { - intros. assert (vmatch callee v0 Vtop) by (eapply vmatch_top; eauto). + intros. assert (vmatch callee v0 Vtop) by (eapply vmatch_top; eauto). inv H0; constructor; eauto. } assert (SM: forall b p, smatch callee m b p -> smatch bc m b Nonstack). @@ -856,21 +856,21 @@ Proof. } assert (BSTK: bmatch bc m sp (am_stack am)). { - apply bmatch_incr with caller; eauto. + apply bmatch_incr with caller; eauto. } (* Conclusions *) exists bc; splitall. - (* result value *) eapply VM; eauto. - (* environment *) - eapply ematch_incr; eauto. + eapply ematch_incr; eauto. - (* romem *) apply romatch_exten with callee; auto. - intros; simpl. destruct (eq_block b sp); intuition. + intros; simpl. destruct (eq_block b sp); intuition. - (* mmatch *) constructor; simpl; intros. + (* stack *) - destruct (eq_block b sp). + destruct (eq_block b sp). subst b. exact BSTK. elim (NOSTACK b); auto. + (* globals *) @@ -878,12 +878,12 @@ Proof. + (* nonstack *) destruct (eq_block b sp). congruence. eapply SM; auto. eapply mmatch_nonstack; eauto. + (* top *) - destruct (eq_block b sp). - subst. apply smatch_ge with (ab_summary (am_stack am)). apply BSTK. apply pge_lub_l. + destruct (eq_block b sp). + subst. apply smatch_ge with (ab_summary (am_stack am)). apply BSTK. apply pge_lub_l. apply smatch_ge with Nonstack. eapply SM. eapply mmatch_top; eauto. apply pge_lub_r. + (* below *) - red; simpl; intros. destruct (eq_block b sp). - subst b. apply Plt_le_trans with bound. apply BELOW. congruence. auto. + red; simpl; intros. destruct (eq_block b sp). + subst b. apply Plt_le_trans with bound. apply BELOW. congruence. auto. eapply mmatch_below; eauto. - (* genv *) eapply genv_match_exten; eauto. @@ -892,7 +892,7 @@ Proof. - (* sp *) simpl. apply dec_eq_true. - (* unchanged *) - simpl; intros. destruct (eq_block b sp). congruence. + simpl; intros. destruct (eq_block b sp). congruence. symmetry. apply SAME; auto. eapply Plt_trans. eauto. apply BELOW. congruence. Qed. @@ -919,19 +919,19 @@ Proof. intros until am; intros EC GENV ARGS RO MM NOSTACK. (* Part 1: using ec_mem_inject *) exploit (@external_call_mem_inject ef _ _ ge vargs m t vres m' (inj_of_bc bc) m vargs). - apply inj_of_bc_preserves_globals; auto. + apply inj_of_bc_preserves_globals; auto. exact EC. eapply mmatch_inj; eauto. eapply mmatch_below; eauto. - revert ARGS. generalize vargs. + revert ARGS. generalize vargs. induction vargs0; simpl; intros; constructor. - eapply vmatch_inj; eauto. auto. + eapply vmatch_inj; eauto. auto. intros (j' & vres' & m'' & EC' & IRES & IMEM & UNCH1 & UNCH2 & IINCR & ISEP). assert (JBELOW: forall b, Plt b (Mem.nextblock m) -> j' b = inj_of_bc bc b). { intros. destruct (inj_of_bc bc b) as [[b' delta] | ] eqn:EQ. - eapply IINCR; eauto. + eapply IINCR; eauto. destruct (j' b) as [[b'' delta'] | ] eqn:EQ'; auto. - exploit ISEP; eauto. tauto. + exploit ISEP; eauto. tauto. } (* Part 2: constructing bc' from j' *) set (f := fun b => if plt b (Mem.nextblock m) @@ -941,13 +941,13 @@ Proof. { assert (forall b, f b = BCstack -> bc b = BCstack). { unfold f; intros. destruct (plt b (Mem.nextblock m)); auto. destruct (j' b); discriminate. } - intros. apply (bc_stack bc); auto. + intros. apply (bc_stack bc); auto. } assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2). { assert (forall b id, f b = BCglob id -> bc b = BCglob id). { unfold f; intros. destruct (plt b (Mem.nextblock m)); auto. destruct (j' b); discriminate. } - intros. eapply (bc_glob bc); eauto. + intros. eapply (bc_glob bc); eauto. } set (bc' := BC f F_stack F_glob). unfold f in bc'. assert (INCR: bc_incr bc bc'). @@ -956,34 +956,34 @@ Proof. } assert (BC'INV: forall b, bc' b <> BCinvalid -> exists b' delta, j' b = Some(b', delta)). { - simpl; intros. destruct (plt b (Mem.nextblock m)). + simpl; intros. destruct (plt b (Mem.nextblock m)). exists b, 0. rewrite JBELOW by auto. apply inj_of_bc_valid; auto. - destruct (j' b) as [[b' delta] | ]. - exists b', delta; auto. + destruct (j' b) as [[b' delta] | ]. + exists b', delta; auto. congruence. } (* Part 3: injection wrt j' implies matching with top wrt bc' *) assert (PMTOP: forall b b' delta ofs, j' b = Some (b', delta) -> pmatch bc' b ofs Ptop). { - intros. constructor. simpl; unfold f. + intros. constructor. simpl; unfold f. destruct (plt b (Mem.nextblock m)). - rewrite JBELOW in H by auto. eapply inj_of_bc_inv; eauto. + rewrite JBELOW in H by auto. eapply inj_of_bc_inv; eauto. rewrite H; congruence. } assert (VMTOP: forall v v', Val.inject j' v v' -> vmatch bc' v Vtop). { - intros. inv H; constructor. eapply PMTOP; eauto. + intros. inv H; constructor. eapply PMTOP; eauto. } assert (SMTOP: forall b, bc' b <> BCinvalid -> smatch bc' m' b Ptop). { intros; split; intros. - - exploit BC'INV; eauto. intros (b' & delta & J'). - exploit Mem.load_inject. eexact IMEM. eauto. eauto. intros (v' & A & B). + - exploit BC'INV; eauto. intros (b' & delta & J'). + exploit Mem.load_inject. eexact IMEM. eauto. eauto. intros (v' & A & B). eapply VMTOP; eauto. - - exploit BC'INV; eauto. intros (b'' & delta & J'). + - exploit BC'INV; eauto. intros (b'' & delta & J'). exploit Mem.loadbytes_inject. eexact IMEM. eauto. eauto. intros (bytes & A & B). - inv B. inv H3. inv H7. eapply PMTOP; eauto. + inv B. inv H3. inv H7. eapply PMTOP; eauto. } (* Conclusions *) exists bc'; splitall. @@ -1004,29 +1004,29 @@ Proof. exploit RO; eauto. intros (R & P & Q). split; auto. split. apply bmatch_incr with bc; auto. apply bmatch_inv with m; auto. - intros. eapply Mem.loadbytes_unchanged_on_1. eapply external_call_readonly; eauto. - auto. intros; red. apply Q. - intros; red; intros; elim (Q ofs). + intros. eapply Mem.loadbytes_unchanged_on_1. eapply external_call_readonly; eauto. + auto. intros; red. apply Q. + intros; red; intros; elim (Q ofs). eapply external_call_max_perm with (m2 := m'); eauto. destruct (j' b); congruence. - (* mmatch top *) constructor; simpl; intros. - + apply ablock_init_sound. apply SMTOP. simpl; congruence. + + apply ablock_init_sound. apply SMTOP. simpl; congruence. + rewrite PTree.gempty in H0; discriminate. + apply SMTOP; auto. - + apply SMTOP; auto. - + red; simpl; intros. destruct (plt b (Mem.nextblock m)). - eapply Plt_le_trans. eauto. eapply external_call_nextblock; eauto. - destruct (j' b) as [[bx deltax] | ] eqn:J'. - eapply Mem.valid_block_inject_1; eauto. + + apply SMTOP; auto. + + red; simpl; intros. destruct (plt b (Mem.nextblock m)). + eapply Plt_le_trans. eauto. eapply external_call_nextblock; eauto. + destruct (j' b) as [[bx deltax] | ] eqn:J'. + eapply Mem.valid_block_inject_1; eauto. congruence. - (* nostack *) - red; simpl; intros. destruct (plt b (Mem.nextblock m)). + red; simpl; intros. destruct (plt b (Mem.nextblock m)). apply NOSTACK; auto. destruct (j' b); congruence. - (* unmapped blocks are invariant *) intros. eapply Mem.loadbytes_unchanged_on_1; auto. - apply UNCH1; auto. intros; red. unfold inj_of_bc; rewrite H0; auto. + apply UNCH1; auto. intros; red. unfold inj_of_bc; rewrite H0; auto. Qed. Remark list_forall2_in_l: @@ -1036,8 +1036,8 @@ Proof. induction 1; simpl; intros. - contradiction. - destruct H1. - + subst. exists b1; auto. - + exploit IHlist_forall2; eauto. intros (x2 & U & V). exists x2; auto. + + subst. exists b1; auto. + + exploit IHlist_forall2; eauto. intros (x2 & U & V). exists x2; auto. Qed. (** ** Semantic invariant *) @@ -1122,10 +1122,10 @@ Lemma sound_stack_ext: Proof. induction 1; intros INV. - constructor. -- assert (Plt sp bound') by eauto with va. +- assert (Plt sp bound') by eauto with va. eapply sound_stack_public_call; eauto. apply IHsound_stack; intros. apply INV. xomega. rewrite SAME; auto. xomega. auto. auto. -- assert (Plt sp bound') by eauto with va. +- assert (Plt sp bound') by eauto with va. eapply sound_stack_private_call; eauto. apply IHsound_stack; intros. apply INV. xomega. rewrite SAME; auto. xomega. auto. auto. apply bmatch_ext with m; auto. intros. apply INV. xomega. auto. auto. auto. @@ -1137,7 +1137,7 @@ Lemma sound_stack_inv: (forall b ofs n, Plt b bound -> bc b = BCinvalid -> n >= 0 -> Mem.loadbytes m' b ofs n = Mem.loadbytes m b ofs n) -> sound_stack bc stk m' bound. Proof. - intros. eapply sound_stack_ext; eauto. intros. rewrite <- H0; auto. + intros. eapply sound_stack_ext; eauto. intros. rewrite <- H0; auto. Qed. Lemma sound_stack_storev: @@ -1147,13 +1147,13 @@ Lemma sound_stack_storev: sound_stack bc stk m bound -> sound_stack bc stk m' bound. Proof. - intros. apply sound_stack_inv with m; auto. + intros. apply sound_stack_inv with m; auto. destruct addr; simpl in H; try discriminate. assert (A: pmatch bc b i Ptop). { inv H0; eapply pmatch_top'; eauto. } - inv A. - intros. eapply Mem.loadbytes_store_other; eauto. left; congruence. -Qed. + inv A. + intros. eapply Mem.loadbytes_store_other; eauto. left; congruence. +Qed. Lemma sound_stack_storebytes: forall m b ofs bytes m' bc aaddr stk bound, @@ -1162,12 +1162,12 @@ Lemma sound_stack_storebytes: sound_stack bc stk m bound -> sound_stack bc stk m' bound. Proof. - intros. apply sound_stack_inv with m; auto. + intros. apply sound_stack_inv with m; auto. assert (A: pmatch bc b ofs Ptop). { inv H0; eapply pmatch_top'; eauto. } - inv A. - intros. eapply Mem.loadbytes_storebytes_other; eauto. left; congruence. -Qed. + inv A. + intros. eapply Mem.loadbytes_storebytes_other; eauto. left; congruence. +Qed. Lemma sound_stack_free: forall m b lo hi m' bc stk bound, @@ -1185,10 +1185,10 @@ Lemma sound_stack_new_bound: Ple bound bound' -> sound_stack bc stk m bound'. Proof. - intros. inv H. + intros. inv H. - constructor. -- eapply sound_stack_public_call with (bound' := bound'0); eauto. xomega. -- eapply sound_stack_private_call with (bound' := bound'0); eauto. xomega. +- eapply sound_stack_public_call with (bound' := bound'0); eauto. xomega. +- eapply sound_stack_private_call with (bound' := bound'0); eauto. xomega. Qed. Lemma sound_stack_exten: @@ -1197,15 +1197,15 @@ Lemma sound_stack_exten: (forall b, Plt b bound -> bc1 b = bc b) -> sound_stack bc1 stk m bound. Proof. - intros. inv H. + intros. inv H. - constructor. -- assert (Plt sp bound') by eauto with va. +- assert (Plt sp bound') by eauto with va. eapply sound_stack_public_call; eauto. - rewrite H0; auto. xomega. + rewrite H0; auto. xomega. intros. rewrite H0; auto. xomega. -- assert (Plt sp bound') by eauto with va. +- assert (Plt sp bound') by eauto with va. eapply sound_stack_private_call; eauto. - rewrite H0; auto. xomega. + rewrite H0; auto. xomega. intros. rewrite H0; auto. xomega. Qed. @@ -1226,7 +1226,7 @@ Lemma sound_succ_state: sound_state (State s f (Vptr sp Int.zero) pc' e' m'). Proof. intros. exploit analyze_succ; eauto. intros (ae'' & am'' & AN & EM & MM). - econstructor; eauto. + econstructor; eauto. Qed. Theorem sound_step: @@ -1235,72 +1235,72 @@ Proof. induction 1; intros SOUND; inv SOUND. - (* nop *) - eapply sound_succ_state; eauto. simpl; auto. + eapply sound_succ_state; eauto. simpl; auto. unfold transfer; rewrite H. auto. - (* op *) - eapply sound_succ_state; eauto. simpl; auto. - unfold transfer; rewrite H. eauto. + eapply sound_succ_state; eauto. simpl; auto. + unfold transfer; rewrite H. eauto. apply ematch_update; auto. eapply eval_static_operation_sound; eauto with va. - (* load *) - eapply sound_succ_state; eauto. simpl; auto. - unfold transfer; rewrite H. eauto. - apply ematch_update; auto. eapply loadv_sound; eauto with va. + eapply sound_succ_state; eauto. simpl; auto. + unfold transfer; rewrite H. eauto. + apply ematch_update; auto. eapply loadv_sound; eauto with va. eapply eval_static_addressing_sound; eauto with va. - (* store *) exploit eval_static_addressing_sound; eauto with va. intros VMADDR. - eapply sound_succ_state; eauto. simpl; auto. - unfold transfer; rewrite H. eauto. - eapply storev_sound; eauto. - destruct a; simpl in H1; try discriminate. eapply romatch_store; eauto. - eapply sound_stack_storev; eauto. + eapply sound_succ_state; eauto. simpl; auto. + unfold transfer; rewrite H. eauto. + eapply storev_sound; eauto. + destruct a; simpl in H1; try discriminate. eapply romatch_store; eauto. + eapply sound_stack_storev; eauto. - (* call *) assert (TR: transfer f rm pc ae am = transfer_call ae am args res). { unfold transfer; rewrite H; auto. } - unfold transfer_call, analyze_call in TR. - destruct (pincl (am_nonstack am) Nonstack && + unfold transfer_call, analyze_call in TR. + destruct (pincl (am_nonstack am) Nonstack && forallb (fun av => vpincl av Nonstack) (aregs ae args)) eqn:NOLEAK. + (* private call *) InvBooleans. - exploit analyze_successor; eauto. simpl; eauto. rewrite TR. intros SUCC. + exploit analyze_successor; eauto. simpl; eauto. rewrite TR. intros SUCC. exploit hide_stack; eauto. apply pincl_ge; auto. intros (bc' & A & B & C & D & E & F & G). apply sound_call_state with bc'; auto. * eapply sound_stack_private_call with (bound' := Mem.nextblock m) (bc' := bc); eauto. apply Ple_refl. eapply mmatch_below; eauto. - eapply mmatch_stack; eauto. - * intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v. - apply D with (areg ae r). + eapply mmatch_stack; eauto. + * intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v. + apply D with (areg ae r). rewrite forallb_forall in H2. apply vpincl_ge. apply H2. apply in_map; auto. auto with va. + (* public call *) - exploit analyze_successor; eauto. simpl; eauto. rewrite TR. intros SUCC. + exploit analyze_successor; eauto. simpl; eauto. rewrite TR. intros SUCC. exploit anonymize_stack; eauto. intros (bc' & A & B & C & D & E & F & G). apply sound_call_state with bc'; auto. * eapply sound_stack_public_call with (bound' := Mem.nextblock m) (bc' := bc); eauto. apply Ple_refl. eapply mmatch_below; eauto. - * intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v. + * intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v. apply D with (areg ae r). auto with va. - (* tailcall *) exploit anonymize_stack; eauto. intros (bc' & A & B & C & D & E & F & G). apply sound_call_state with bc'; auto. - erewrite Mem.nextblock_free by eauto. + erewrite Mem.nextblock_free by eauto. apply sound_stack_new_bound with stk. apply sound_stack_exten with bc. eapply sound_stack_free; eauto. intros. apply C. apply Plt_ne; auto. - apply Plt_Ple. eapply mmatch_below; eauto. congruence. - intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v. + apply Plt_Ple. eapply mmatch_below; eauto. congruence. + intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v. apply D with (areg ae r). auto with va. - eapply romatch_free; eauto. - eapply mmatch_free; eauto. + eapply romatch_free; eauto. + eapply mmatch_free; eauto. - (* builtin *) assert (SPVALID: Plt sp0 (Mem.nextblock m)) by (eapply mmatch_below; eauto with va). @@ -1314,72 +1314,72 @@ Proof. { unfold transfer_builtin_default, analyze_call; intros TR'. set (aargs := map (abuiltin_arg ae am rm) args) in *. assert (ARGS: list_forall2 (vmatch bc) vargs aargs) by (eapply abuiltin_args_sound; eauto). - destruct (pincl (am_nonstack am) Nonstack && + destruct (pincl (am_nonstack am) Nonstack && forallb (fun av => vpincl av Nonstack) aargs) eqn: NOLEAK. * (* private builtin call *) InvBooleans. rewrite forallb_forall in H3. exploit hide_stack; eauto. apply pincl_ge; auto. intros (bc1 & A & B & C & D & E & F & G). - exploit external_call_match; eauto. + exploit external_call_match; eauto. intros. exploit list_forall2_in_l; eauto. intros (av & U & V). - eapply D; eauto with va. apply vpincl_ge. apply H3; auto. + eapply D; eauto with va. apply vpincl_ge. apply H3; auto. intros (bc2 & J & K & L & M & N & O & P & Q). exploit (return_from_private_call bc bc2); eauto. eapply mmatch_below; eauto. rewrite K; auto. intros. rewrite K; auto. rewrite C; auto. - apply bmatch_inv with m. eapply mmatch_stack; eauto. + apply bmatch_inv with m. eapply mmatch_stack; eauto. intros. apply Q; auto. - eapply external_call_nextblock; eauto. + eapply external_call_nextblock; eauto. intros (bc3 & U & V & W & X & Y & Z & AA). - eapply sound_succ_state with (bc := bc3); eauto. simpl; auto. - apply set_builtin_res_sound; auto. - apply sound_stack_exten with bc. + eapply sound_succ_state with (bc := bc3); eauto. simpl; auto. + apply set_builtin_res_sound; auto. + apply sound_stack_exten with bc. apply sound_stack_inv with m. auto. intros. apply Q. red. eapply Plt_trans; eauto. rewrite C; auto. exact AA. * (* public builtin call *) - exploit anonymize_stack; eauto. + exploit anonymize_stack; eauto. intros (bc1 & A & B & C & D & E & F & G). - exploit external_call_match; eauto. + exploit external_call_match; eauto. intros. exploit list_forall2_in_l; eauto. intros (av & U & V). eapply D; eauto with va. intros (bc2 & J & K & L & M & N & O & P & Q). exploit (return_from_public_call bc bc2); eauto. eapply mmatch_below; eauto. rewrite K; auto. intros. rewrite K; auto. rewrite C; auto. - eapply external_call_nextblock; eauto. + eapply external_call_nextblock; eauto. intros (bc3 & U & V & W & X & Y & Z & AA). - eapply sound_succ_state with (bc := bc3); eauto. simpl; auto. - apply set_builtin_res_sound; auto. - apply sound_stack_exten with bc. + eapply sound_succ_state with (bc := bc3); eauto. simpl; auto. + apply set_builtin_res_sound; auto. + apply sound_stack_exten with bc. apply sound_stack_inv with m. auto. intros. apply Q. red. eapply Plt_trans; eauto. rewrite C; auto. exact AA. } - unfold transfer_builtin in TR. + unfold transfer_builtin in TR. destruct ef; auto. + (* volatile load *) inv H0; auto. inv H3; auto. inv H1. exploit abuiltin_arg_sound; eauto. intros VM1. eapply sound_succ_state; eauto. simpl; auto. - apply set_builtin_res_sound; auto. + apply set_builtin_res_sound; auto. inv H3. * (* true volatile access *) assert (V: vmatch bc v (Ifptr Glob)). { inv H4; simpl in *; constructor. econstructor. eapply GE; eauto. } - destruct (va_strict tt). apply vmatch_lub_r. apply vnormalize_sound. auto. + destruct (va_strict tt). apply vmatch_lub_r. apply vnormalize_sound. auto. apply vnormalize_sound. eapply vmatch_ge; eauto. constructor. constructor. * (* normal memory access *) exploit loadv_sound; eauto. simpl; eauto. intros V. - destruct (va_strict tt). + destruct (va_strict tt). apply vmatch_lub_l. auto. - eapply vnormalize_cast; eauto. eapply vmatch_top; eauto. + eapply vnormalize_cast; eauto. eapply vmatch_top; eauto. + (* volatile store *) - inv H0; auto. inv H3; auto. inv H4; auto. inv H1. + inv H0; auto. inv H3; auto. inv H4; auto. inv H1. exploit abuiltin_arg_sound. eauto. eauto. eauto. eauto. eauto. eexact H0. intros VM1. exploit abuiltin_arg_sound. eauto. eauto. eauto. eauto. eauto. eexact H2. intros VM2. inv H9. @@ -1394,84 +1394,84 @@ Proof. eapply romatch_store; eauto. eapply sound_stack_storev; eauto. simpl; eauto. + (* memcpy *) - inv H0; auto. inv H3; auto. inv H4; auto. inv H1. + inv H0; auto. inv H3; auto. inv H4; auto. inv H1. exploit abuiltin_arg_sound. eauto. eauto. eauto. eauto. eauto. eexact H0. intros VM1. exploit abuiltin_arg_sound. eauto. eauto. eauto. eauto. eauto. eexact H2. intros VM2. - eapply sound_succ_state; eauto. simpl; auto. + eapply sound_succ_state; eauto. simpl; auto. apply set_builtin_res_sound; auto. constructor. - eapply storebytes_sound; eauto. - apply match_aptr_of_aval; auto. - eapply Mem.loadbytes_length; eauto. - intros. eapply loadbytes_sound; eauto. apply match_aptr_of_aval; auto. - eapply romatch_storebytes; eauto. - eapply sound_stack_storebytes; eauto. + eapply storebytes_sound; eauto. + apply match_aptr_of_aval; auto. + eapply Mem.loadbytes_length; eauto. + intros. eapply loadbytes_sound; eauto. apply match_aptr_of_aval; auto. + eapply romatch_storebytes; eauto. + eapply sound_stack_storebytes; eauto. + (* annot *) - inv H1. eapply sound_succ_state; eauto. simpl; auto. apply set_builtin_res_sound; auto. constructor. + inv H1. eapply sound_succ_state; eauto. simpl; auto. apply set_builtin_res_sound; auto. constructor. + (* annot val *) inv H0; auto. inv H3; auto. inv H1. eapply sound_succ_state; eauto. simpl; auto. apply set_builtin_res_sound; auto. eapply abuiltin_arg_sound; eauto. + (* debug *) - inv H1. eapply sound_succ_state; eauto. simpl; auto. apply set_builtin_res_sound; auto. constructor. + inv H1. eapply sound_succ_state; eauto. simpl; auto. apply set_builtin_res_sound; auto. constructor. - (* cond *) - eapply sound_succ_state; eauto. - simpl. destruct b; auto. - unfold transfer; rewrite H; auto. + eapply sound_succ_state; eauto. + simpl. destruct b; auto. + unfold transfer; rewrite H; auto. - (* jumptable *) - eapply sound_succ_state; eauto. - simpl. eapply list_nth_z_in; eauto. + eapply sound_succ_state; eauto. + simpl. eapply list_nth_z_in; eauto. unfold transfer; rewrite H; auto. - (* return *) exploit anonymize_stack; eauto. intros (bc' & A & B & C & D & E & F & G). apply sound_return_state with bc'; auto. - erewrite Mem.nextblock_free by eauto. + erewrite Mem.nextblock_free by eauto. apply sound_stack_new_bound with stk. apply sound_stack_exten with bc. eapply sound_stack_free; eauto. intros. apply C. apply Plt_ne; auto. apply Plt_Ple. eapply mmatch_below; eauto with va. - destruct or; simpl. eapply D; eauto. constructor. - eapply romatch_free; eauto. + destruct or; simpl. eapply D; eauto. constructor. + eapply romatch_free; eauto. eapply mmatch_free; eauto. - (* internal function *) - exploit allocate_stack; eauto. + exploit allocate_stack; eauto. intros (bc' & A & B & C & D & E & F & G). - exploit (analyze_entrypoint rm f args m' bc'); eauto. + exploit (analyze_entrypoint rm f args m' bc'); eauto. intros (ae & am & AN & EM & MM'). - econstructor; eauto. - erewrite Mem.alloc_result by eauto. + econstructor; eauto. + erewrite Mem.alloc_result by eauto. apply sound_stack_exten with bc; auto. - apply sound_stack_inv with m; auto. + apply sound_stack_inv with m; auto. intros. eapply Mem.loadbytes_alloc_unchanged; eauto. intros. apply F. erewrite Mem.alloc_result by eauto. auto. - (* external function *) exploit external_call_match; eauto with va. intros (bc' & A & B & C & D & E & F & G & K). - econstructor; eauto. + econstructor; eauto. apply sound_stack_new_bound with (Mem.nextblock m). apply sound_stack_exten with bc; auto. - apply sound_stack_inv with m; auto. + apply sound_stack_inv with m; auto. eapply external_call_nextblock; eauto. - (* return *) inv STK. + (* from public call *) - exploit return_from_public_call; eauto. + exploit return_from_public_call; eauto. intros; rewrite SAME; auto. - intros (bc1 & A & B & C & D & E & F & G). + intros (bc1 & A & B & C & D & E & F & G). destruct (analyze rm f)#pc as [ |ae' am'] eqn:EQ; simpl in AN; try contradiction. destruct AN as [A1 A2]. eapply sound_regular_state with (bc := bc1); eauto. apply sound_stack_exten with bc'; auto. - eapply ematch_ge; eauto. apply ematch_update. auto. auto. + eapply ematch_ge; eauto. apply ematch_update. auto. auto. + (* from private call *) - exploit return_from_private_call; eauto. + exploit return_from_private_call; eauto. intros; rewrite SAME; auto. - intros (bc1 & A & B & C & D & E & F & G). + intros (bc1 & A & B & C & D & E & F & G). destruct (analyze rm f)#pc as [ |ae' am'] eqn:EQ; simpl in AN; try contradiction. destruct AN as [A1 A2]. eapply sound_regular_state with (bc := bc1); eauto. apply sound_stack_exten with bc'; auto. @@ -1498,8 +1498,8 @@ Lemma initial_block_classification: /\ (forall b id, bc b = BCglob id -> Genv.find_symbol ge id = Some b) /\ (forall b, Mem.valid_block m b -> bc b <> BCinvalid). Proof. - intros. - set (f := fun b => + intros. + set (f := fun b => if plt b (Genv.genv_next ge) then match Genv.invert_symbol ge b with None => BCother | Some id => BCglob id end else @@ -1511,8 +1511,8 @@ Proof. destruct (Genv.invert_symbol ge b1) as [id1|] eqn:I1; inv H0. destruct (plt b2 (Genv.genv_next ge)); try discriminate. destruct (Genv.invert_symbol ge b2) as [id2|] eqn:I2; inv H1. - exploit Genv.invert_find_symbol. eexact I1. - exploit Genv.invert_find_symbol. eexact I2. + exploit Genv.invert_find_symbol. eexact I1. + exploit Genv.invert_find_symbol. eexact I2. congruence. } assert (F_stack: forall b1 b2, f b1 = BCstack -> f b2 = BCstack -> b1 = b2). @@ -1523,19 +1523,19 @@ Proof. } set (bc := BC f F_stack F_glob). unfold f in bc. exists bc; splitall. -- split; simpl; intros. +- split; simpl; intros. + split; intros. * rewrite pred_dec_true by (eapply Genv.genv_symb_range; eauto). erewrite Genv.find_invert_symbol; eauto. - * apply Genv.invert_find_symbol. + * apply Genv.invert_find_symbol. destruct (plt b (Genv.genv_next ge)); try discriminate. destruct (Genv.invert_symbol ge b); congruence. - + rewrite ! pred_dec_true by assumption. + + rewrite ! pred_dec_true by assumption. destruct (Genv.invert_symbol); split; congruence. - red; simpl; intros. destruct (plt b (Genv.genv_next ge)); try congruence. - erewrite <- Genv.init_mem_genv_next by eauto. auto. -- red; simpl; intros. - destruct (plt b (Genv.genv_next ge)). + erewrite <- Genv.init_mem_genv_next by eauto. auto. +- red; simpl; intros. + destruct (plt b (Genv.genv_next ge)). destruct (Genv.invert_symbol ge b); congruence. congruence. - simpl; intros. destruct (plt b (Genv.genv_next ge)); try discriminate. @@ -1561,13 +1561,13 @@ Proof. vge (Ifptr Glob) av -> pge Glob (ab_summary (ablock_store chunk ab p av))). { - intros. simpl. unfold vplub; destruct av; auto. + intros. simpl. unfold vplub; destruct av; auto. inv H0. apply plub_least; auto. inv H0. apply plub_least; auto. } destruct id; auto. - simpl. destruct (propagate_float_constants tt); auto. - simpl. destruct (propagate_float_constants tt); auto. + simpl. destruct (propagate_float_constants tt); auto. + simpl. destruct (propagate_float_constants tt); auto. apply DFL. constructor. constructor. Qed. @@ -1576,7 +1576,7 @@ Lemma store_init_data_list_summary: pge Glob (ab_summary ab) -> pge Glob (ab_summary (store_init_data_list ab p idl)). Proof. - induction idl; simpl; intros. auto. apply IHidl. apply store_init_data_summary; auto. + induction idl; simpl; intros. auto. apply IHidl. apply store_init_data_summary; auto. Qed. Lemma store_init_data_sound: @@ -1588,7 +1588,7 @@ Proof. intros. destruct id; try (eapply ablock_store_sound; eauto; constructor). simpl. destruct (propagate_float_constants tt); eapply ablock_store_sound; eauto; constructor. simpl. destruct (propagate_float_constants tt); eapply ablock_store_sound; eauto; constructor. - simpl in H. inv H. auto. + simpl in H. inv H. auto. simpl in H. destruct (Genv.find_symbol ge i) as [b'|] eqn:FS; try discriminate. eapply ablock_store_sound; eauto. constructor. constructor. apply GMATCH; auto. Qed. @@ -1602,7 +1602,7 @@ Proof. induction idl; simpl; intros. - inv H; auto. - destruct (Genv.store_init_data ge m b p a) as [m1|] eqn:SI; try discriminate. - eapply IHidl; eauto. eapply store_init_data_sound; eauto. + eapply IHidl; eauto. eapply store_init_data_sound; eauto. Qed. Lemma store_init_data_other: @@ -1614,7 +1614,7 @@ Lemma store_init_data_other: Proof. intros. eapply bmatch_inv; eauto. intros. destruct id; try (eapply Mem.loadbytes_store_other; eauto; fail); simpl in H. - inv H; auto. + inv H; auto. destruct (Genv.find_symbol ge i); try discriminate. eapply Mem.loadbytes_store_other; eauto. Qed. @@ -1626,10 +1626,10 @@ Lemma store_init_data_list_other: bmatch bc m b' ab -> bmatch bc m' b' ab. Proof. - induction idl; simpl; intros. + induction idl; simpl; intros. inv H; auto. destruct (Genv.store_init_data ge m b p a) as [m1|] eqn:SI; try discriminate. - eapply IHidl; eauto. eapply store_init_data_other; eauto. + eapply IHidl; eauto. eapply store_init_data_other; eauto. Qed. Lemma store_zeros_same: @@ -1640,8 +1640,8 @@ Lemma store_zeros_same: Proof. intros until n. functional induction (store_zeros m b pos n); intros. - inv H. auto. -- eapply IHo; eauto. change p with (vplub (I Int.zero) p). - eapply smatch_store; eauto. constructor. +- eapply IHo; eauto. change p with (vplub (I Int.zero) p). + eapply smatch_store; eauto. constructor. - discriminate. Qed. @@ -1654,8 +1654,8 @@ Lemma store_zeros_other: Proof. intros until n. functional induction (store_zeros m b p n); intros. - inv H. auto. -- eapply IHo; eauto. eapply bmatch_inv; eauto. - intros. eapply Mem.loadbytes_store_other; eauto. +- eapply IHo; eauto. eapply bmatch_inv; eauto. + intros. eapply Mem.loadbytes_store_other; eauto. - discriminate. Qed. @@ -1673,16 +1673,16 @@ Lemma alloc_global_match: initial_mem_match bc m' (Genv.add_global g idg). Proof. intros; red; intros. destruct idg as [id [fd | gv]]; simpl in *. -- destruct (Mem.alloc m 0 1) as [m1 b1] eqn:ALLOC. +- destruct (Mem.alloc m 0 1) as [m1 b1] eqn:ALLOC. unfold Genv.find_var_info, Genv.add_global in H2; simpl in H2. - assert (Plt b (Mem.nextblock m)). + assert (Plt b (Mem.nextblock m)). { rewrite <- H. eapply Genv.genv_vars_range; eauto. } - assert (b <> b1). + assert (b <> b1). { apply Plt_ne. erewrite Mem.alloc_result by eauto. auto. } - apply bmatch_inv with m. - eapply H0; eauto. - intros. transitivity (Mem.loadbytes m1 b ofs n). - eapply Mem.loadbytes_drop; eauto. + apply bmatch_inv with m. + eapply H0; eauto. + intros. transitivity (Mem.loadbytes m1 b ofs n). + eapply Mem.loadbytes_drop; eauto. eapply Mem.loadbytes_alloc_unchanged; eauto. - set (sz := Genv.init_data_list_size (gvar_init gv)) in *. destruct (Mem.alloc m 0 sz) as [m1 b1] eqn:ALLOC. @@ -1690,28 +1690,28 @@ Proof. destruct (Genv.store_init_data_list ge m2 b1 0 (gvar_init gv)) as [m3 | ] eqn:SIDL; try discriminate. unfold Genv.find_var_info, Genv.add_global in H2; simpl in H2. rewrite PTree.gsspec in H2. destruct (peq b (Genv.genv_next g)). -+ inversion H2; clear H2; subst v. ++ inversion H2; clear H2; subst v. assert (b = b1). { erewrite Mem.alloc_result by eauto. congruence. } - clear e. subst b. - apply bmatch_inv with m3. - eapply store_init_data_list_sound; eauto. + clear e. subst b. + apply bmatch_inv with m3. + eapply store_init_data_list_sound; eauto. apply ablock_init_sound. - eapply store_zeros_same; eauto. - split; intros. - exploit Mem.load_alloc_same; eauto. intros EQ; subst v; constructor. + eapply store_zeros_same; eauto. + split; intros. + exploit Mem.load_alloc_same; eauto. intros EQ; subst v; constructor. exploit Mem.loadbytes_alloc_same; eauto with coqlib. congruence. - intros. eapply Mem.loadbytes_drop; eauto. - right; right; right. unfold Genv.perm_globvar. rewrite H3, H4. constructor. -+ assert (Plt b (Mem.nextblock m)). + intros. eapply Mem.loadbytes_drop; eauto. + right; right; right. unfold Genv.perm_globvar. rewrite H3, H4. constructor. ++ assert (Plt b (Mem.nextblock m)). { rewrite <- H. eapply Genv.genv_vars_range; eauto. } - assert (b <> b1). + assert (b <> b1). { apply Plt_ne. erewrite Mem.alloc_result by eauto. auto. } apply bmatch_inv with m3. - eapply store_init_data_list_other; eauto. - eapply store_zeros_other; eauto. - apply bmatch_inv with m. - eapply H0; eauto. - intros. eapply Mem.loadbytes_alloc_unchanged; eauto. + eapply store_init_data_list_other; eauto. + eapply store_zeros_other; eauto. + apply bmatch_inv with m. + eapply H0; eauto. + intros. eapply Mem.loadbytes_alloc_unchanged; eauto. intros. eapply Mem.loadbytes_drop; eauto. Qed. @@ -1722,12 +1722,12 @@ Lemma alloc_globals_match: Genv.alloc_globals ge m gl = Some m' -> initial_mem_match bc m' (Genv.add_globals g gl). Proof. - induction gl; simpl; intros. -- inv H1; auto. + induction gl; simpl; intros. +- inv H1; auto. - destruct (Genv.alloc_global ge m a) as [m1|] eqn:AG; try discriminate. - eapply IHgl; eauto. - erewrite Genv.alloc_global_nextblock; eauto. simpl. congruence. - eapply alloc_global_match; eauto. + eapply IHgl; eauto. + erewrite Genv.alloc_global_nextblock; eauto. simpl. congruence. + eapply alloc_global_match; eauto. Qed. Definition romem_consistent (g: genv) (rm: romem) := @@ -1747,19 +1747,19 @@ Proof. intros; red; intros. destruct idg as [id1 [fd1 | v1]]; unfold Genv.add_global, Genv.find_symbol, Genv.find_var_info, alloc_global in *; simpl in *. - rewrite PTree.gsspec in H0. rewrite PTree.grspec in H1. unfold PTree.elt_eq in *. - destruct (peq id id1). congruence. eapply H; eauto. + destruct (peq id id1). congruence. eapply H; eauto. - rewrite PTree.gsspec in H0. destruct (peq id id1). -+ inv H0. rewrite PTree.gss. ++ inv H0. rewrite PTree.gss. destruct (gvar_readonly v1 && negb (gvar_volatile v1) && definitive_initializer (gvar_init v1)) eqn:RO. InvBooleans. rewrite negb_true_iff in H4. rewrite PTree.gss in H1. - exists v1. intuition congruence. + exists v1. intuition congruence. rewrite PTree.grs in H1. discriminate. -+ rewrite PTree.gso. eapply H; eauto. ++ rewrite PTree.gso. eapply H; eauto. destruct (gvar_readonly v1 && negb (gvar_volatile v1) && definitive_initializer (gvar_init v1)). - rewrite PTree.gso in H1; auto. - rewrite PTree.gro in H1; auto. - apply Plt_ne. eapply Genv.genv_symb_range; eauto. + rewrite PTree.gso in H1; auto. + rewrite PTree.gro in H1; auto. + apply Plt_ne. eapply Genv.genv_symb_range; eauto. Qed. Lemma alloc_globals_consistent: @@ -1767,14 +1767,14 @@ Lemma alloc_globals_consistent: romem_consistent g rm -> romem_consistent (Genv.add_globals g gl) (List.fold_left alloc_global gl rm). Proof. - induction gl; simpl; intros. auto. apply IHgl. apply alloc_global_consistent; auto. + induction gl; simpl; intros. auto. apply IHgl. apply alloc_global_consistent; auto. Qed. End INIT. Theorem initial_mem_matches: forall m, - Genv.init_mem prog = Some m -> + Genv.init_mem prog = Some m -> exists bc, genv_match bc ge /\ bc_below bc (Mem.nextblock m) @@ -1783,7 +1783,7 @@ Theorem initial_mem_matches: /\ (forall b, Mem.valid_block m b -> bc b <> BCinvalid). Proof. intros. - exploit initial_block_classification; eauto. intros (bc & GE & BELOW & NOSTACK & INV & VALID). + exploit initial_block_classification; eauto. intros (bc & GE & BELOW & NOSTACK & INV & VALID). exists bc; splitall; auto. assert (A: initial_mem_match bc m ge). { @@ -1796,34 +1796,34 @@ Proof. red; intros. rewrite PTree.gempty in H1; discriminate. } red; intros. - exploit B; eauto. intros (v & FV & RO & NVOL & EQ). - split. subst ab. apply store_init_data_list_summary. constructor. - split. subst ab. eapply A; eauto. - unfold ge in FV; exploit Genv.init_mem_characterization; eauto. - intros (P & Q & R). - intros; red; intros. exploit Q; eauto. intros [U V]. - unfold Genv.perm_globvar in V; rewrite RO, NVOL in V. inv V. + exploit B; eauto. intros (v & FV & RO & NVOL & EQ). + split. subst ab. apply store_init_data_list_summary. constructor. + split. subst ab. eapply A; eauto. + unfold ge in FV; exploit Genv.init_mem_characterization; eauto. + intros (P & Q & R). + intros; red; intros. exploit Q; eauto. intros [U V]. + unfold Genv.perm_globvar in V; rewrite RO, NVOL in V. inv V. Qed. -End INITIAL. +End INITIAL. Require Import Axioms. Theorem sound_initial: forall prog st, initial_state prog st -> sound_state prog st. Proof. - destruct 1. + destruct 1. exploit initial_mem_matches; eauto. intros (bc & GE & BELOW & NOSTACK & RM & VALID). - apply sound_call_state with bc. -- constructor. -- simpl; tauto. + apply sound_call_state with bc. +- constructor. +- simpl; tauto. - exact RM. - apply mmatch_inj_top with m0. replace (inj_of_bc bc) with (Mem.flat_inj (Mem.nextblock m0)). eapply Genv.initmem_inject; eauto. symmetry; apply extensionality; unfold Mem.flat_inj; intros x. - destruct (plt x (Mem.nextblock m0)). - apply inj_of_bc_valid; auto. + destruct (plt x (Mem.nextblock m0)). + apply inj_of_bc_valid; auto. unfold inj_of_bc. erewrite bc_below_invalid; eauto. - exact GE. - exact NOSTACK. @@ -1848,7 +1848,7 @@ Lemma avalue_sound: /\ bc sp = BCstack. Proof. intros. inv H. exists bc; split; auto. rewrite AN. apply EM. -Qed. +Qed. Definition aaddr (a: VA.t) (r: reg) : aptr := match a with @@ -1867,7 +1867,7 @@ Lemma aaddr_sound: Proof. intros. inv H. exists bc; split; auto. unfold aaddr; rewrite AN. apply match_aptr_of_aval. rewrite <- H0. apply EM. -Qed. +Qed. Definition aaddressing (a: VA.t) (addr: addressing) (args: list reg) : aptr := match a with @@ -1884,8 +1884,8 @@ Lemma aaddressing_sound: /\ genv_match bc (Genv.globalenv prog) /\ bc sp = BCstack. Proof. - intros. inv H. exists bc; split; auto. - unfold aaddressing. rewrite AN. apply match_aptr_of_aval. + intros. inv H. exists bc; split; auto. + unfold aaddressing. rewrite AN. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va. Qed. @@ -1895,7 +1895,7 @@ Qed. Definition aaddr_arg (a: VA.t) (ba: builtin_arg reg) : aptr := match a with | VA.Bot => Pbot - | VA.State ae am => + | VA.State ae am => match ba with | BA r => aptr_of_aval (AE.get r ae) | BA_addrstack ofs => Stk ofs @@ -1914,7 +1914,7 @@ Lemma aaddr_arg_sound_1: eval_builtin_arg ge (fun r : positive => rs # r) (Vptr sp Int.zero) m a (Vptr b ofs) -> pmatch bc b ofs (aaddr_arg (VA.State ae am) a). Proof. - intros. + intros. apply pmatch_ge with (aptr_of_aval (abuiltin_arg ae am rm a)). simpl. destruct a; try (apply pge_top); simpl; apply pge_refl. apply match_aptr_of_aval. eapply abuiltin_arg_sound; eauto. -- cgit