diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-06-22 16:39:53 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-06-22 16:39:53 +0200 |
| commit | fb44646eb7308c1dd6a44b85415528982083200b (patch) | |
| tree | 46d088a96e09516a5b94693099b408361aebf691 /backend/Deadcodeproof.v | |
| parent | 9b31f673da13a4f4d04d937ac2b9e934c9b8291d (diff) | |
| download | compcert-kvx-fb44646eb7308c1dd6a44b85415528982083200b.tar.gz compcert-kvx-fb44646eb7308c1dd6a44b85415528982083200b.zip | |
Stricter control of permissions in memory injections and extensions
As suggested by Lennart Beringer, this commits strengthens memory injections and extensions so as to guarantee that the permissions of existing memory locations are not increased by the injection/extension. The only increase of permissions permitted is empty locations in the source memory state of the injection/extension being mapped to nonempty locations.
Diffstat (limited to 'backend/Deadcodeproof.v')
| -rw-r--r-- | backend/Deadcodeproof.v | 16 |
1 files changed, 14 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). |