diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Deadcodeproof.v | 16 | ||||
| -rw-r--r-- | backend/Unusedglobproof.v | 11 | ||||
| -rw-r--r-- | backend/ValueDomain.v | 3 |
3 files changed, 28 insertions, 2 deletions
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 72881b94..26953479 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -39,8 +39,10 @@ Definition locset := block -> Z -> Prop. Record magree (m1 m2: mem) (P: locset) : Prop := mk_magree { ma_perm: forall b ofs k p, - Mem.perm m1 b ofs k p -> - Mem.perm m2 b ofs k p; + Mem.perm m1 b ofs k p -> Mem.perm m2 b ofs k p; + ma_perm_inv: + forall b ofs k p, + Mem.perm m2 b ofs k p -> Mem.perm m1 b ofs k p \/ ~Mem.perm m1 b ofs Max Nonempty; ma_memval: forall b ofs, Mem.perm m1 b ofs Cur Readable -> @@ -65,6 +67,7 @@ Lemma mextends_agree: Proof. intros. destruct H. destruct mext_inj. constructor; intros. - replace ofs with (ofs + 0) by omega. eapply mi_perm; eauto. auto. +- eauto. - exploit mi_memval; eauto. unfold inject_id; eauto. rewrite Zplus_0_r. auto. - auto. @@ -157,6 +160,8 @@ Proof. constructor; intros. - eapply Mem.perm_storebytes_1; eauto. eapply ma_perm; eauto. eapply Mem.perm_storebytes_2; eauto. +- exploit ma_perm_inv; eauto using Mem.perm_storebytes_2. + intuition eauto using Mem.perm_storebytes_1, Mem.perm_storebytes_2. - rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0). rewrite (Mem.storebytes_mem_contents _ _ _ _ _ ST2). rewrite ! PMap.gsspec. destruct (peq b0 b). @@ -201,6 +206,8 @@ Lemma magree_storebytes_left: Proof. intros. constructor; intros. - eapply ma_perm; eauto. eapply Mem.perm_storebytes_2; eauto. +- exploit ma_perm_inv; eauto. + intuition eauto using Mem.perm_storebytes_1, Mem.perm_storebytes_2. - rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0). rewrite PMap.gsspec. destruct (peq b0 b). + subst b0. rewrite Mem.setN_outside. eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. @@ -242,6 +249,11 @@ Proof. assert (Mem.perm m2 b0 ofs k p). { eapply ma_perm; eauto. eapply Mem.perm_free_3; eauto. } exploit Mem.perm_free_inv; eauto. intros [[A B] | A]; auto. subst b0. eelim Mem.perm_free_2. eexact H0. eauto. eauto. +- (* inverse permissions *) + exploit ma_perm_inv; eauto using Mem.perm_free_3. intros [A|A]. + eapply Mem.perm_free_inv in A; eauto. destruct A as [[A B] | A]; auto. + subst b0; right; eapply Mem.perm_free_2; eauto. + right; intuition eauto using Mem.perm_free_3. - (* contents *) rewrite (Mem.free_result _ _ _ _ _ H0). rewrite (Mem.free_result _ _ _ _ _ FREE). diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index bb40a2d3..44cf1e8a 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -1178,6 +1178,17 @@ Proof. destruct (ident_eq id1 id2). congruence. left; eapply Genv.global_addresses_distinct; eauto. - exploit init_meminj_invert; eauto. intros (A & id & B & C). subst delta. split. omega. generalize (Int.unsigned_range_2 ofs). omega. +- exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). + exploit (Genv.init_mem_characterization_gen p); eauto. + exploit (Genv.init_mem_characterization_gen tp); eauto. + destruct gd as [f|v]. ++ intros (P2 & Q2) (P1 & Q1). + apply Q2 in H0. destruct H0. subst. replace ofs with 0 by omega. + left; apply Mem.perm_cur; auto. ++ intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). + apply Q2 in H0. destruct H0. subst. + left. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. + apply P1. omega. Qed. End INIT_MEM. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 8b76f44d..3c80d733 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -3766,6 +3766,9 @@ Proof. - (* overflow *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. rewrite Zplus_0_r. split. omega. apply Int.unsigned_range_2. +- (* perm inv *) + intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. + rewrite Zplus_0_r in H2. auto. Qed. Lemma inj_of_bc_preserves_globals: |