From fb44646eb7308c1dd6a44b85415528982083200b Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 22 Jun 2016 16:39:53 +0200
Subject: 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.
---
 backend/Deadcodeproof.v | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

(limited to 'backend/Deadcodeproof.v')

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).
-- 
cgit