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.

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: