Merge pull request #102 from AbsInt/memory_permissions

Stricter control of permissions in memory injections and extensions

5 files changed, 154 insertions, 9 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:
diff --git a/common/Memory.v b/common/Memory.v
index 0ea9e3b0..f32d21c7 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -2823,7 +2823,10 @@ Qed.
 Record extends' (m1 m2: mem) : Prop :=
   mk_extends {
     mext_next: nextblock m1 = nextblock m2;
-    mext_inj:  mem_inj inject_id m1 m2
+    mext_inj:  mem_inj inject_id m1 m2;
+    mext_perm_inv: forall b ofs k p,
+      perm m2 b ofs k p ->
+      perm m1 b ofs k p \/ ~perm m1 b ofs Max Nonempty
   }.
 
 Definition extends := extends'.
@@ -2836,6 +2839,7 @@ Proof.
   intros. unfold inject_id in H; inv H. apply Z.divide_0_r.
   intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega.
   apply memval_lessdef_refl.
+  tauto.
 Qed.
 
 Theorem load_extends:
@@ -2890,10 +2894,11 @@ Proof.
   intros [m2' [A B]].
   exists m2'; split.
   replace (ofs + 0) with ofs in A by omega. auto.
-  split; auto.
+  constructor; auto.
   rewrite (nextblock_store _ _ _ _ _ _ H0).
   rewrite (nextblock_store _ _ _ _ _ _ A).
   auto.
+  intros. exploit mext_perm_inv0; intuition eauto using perm_store_1, perm_store_2.
 Qed.
 
 Theorem store_outside_extends:
@@ -2907,6 +2912,7 @@ Proof.
   rewrite (nextblock_store _ _ _ _ _ _ H0). auto.
   eapply store_outside_inj; eauto.
   unfold inject_id; intros. inv H2. eapply H1; eauto. omega.
+  intros. eauto using perm_store_2. 
 Qed.
 
 Theorem storev_extends:
@@ -2940,10 +2946,11 @@ Proof.
   intros [m2' [A B]].
   exists m2'; split.
   replace (ofs + 0) with ofs in A by omega. auto.
-  split; auto.
+  constructor; auto.
   rewrite (nextblock_storebytes _ _ _ _ _ H0).
   rewrite (nextblock_storebytes _ _ _ _ _ A).
   auto.
+  intros. exploit mext_perm_inv0; intuition eauto using perm_storebytes_1, perm_storebytes_2.
 Qed.
 
 Theorem storebytes_outside_extends:
@@ -2957,6 +2964,7 @@ Proof.
   rewrite (nextblock_storebytes _ _ _ _ _ H0). auto.
   eapply storebytes_outside_inj; eauto.
   unfold inject_id; intros. inv H2. eapply H1; eauto. omega.
+  intros. eauto using perm_storebytes_2. 
 Qed.
 
 Theorem alloc_extends:
@@ -2988,6 +2996,15 @@ Proof.
   eapply perm_implies with Freeable; auto with mem.
   eapply perm_alloc_2; eauto.
   omega.
+  intros. eapply perm_alloc_inv in H; eauto.
+  generalize (perm_alloc_inv _ _ _ _ _ H0 b0 ofs Max Nonempty); intros PERM.
+  destruct (eq_block b0 b).
+  subst b0. 
+  assert (EITHER: lo1 <= ofs < hi1 \/ ~(lo1 <= ofs < hi1)) by omega.
+  destruct EITHER.
+  left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto.
+  right; tauto.
+  exploit mext_perm_inv0; intuition eauto using perm_alloc_1, perm_alloc_4.
 Qed.
 
 Theorem free_left_extends:
@@ -2999,6 +3016,10 @@ Proof.
   intros. inv H. constructor.
   rewrite (nextblock_free _ _ _ _ _ H0). auto.
   eapply free_left_inj; eauto.
+  intros. exploit mext_perm_inv0; eauto. intros [A|A]. 
+  eapply perm_free_inv in A; eauto. destruct A as [[A B]|A]; auto.
+  subst b0. right; eapply perm_free_2; eauto.
+  intuition eauto using perm_free_3.
 Qed.
 
 Theorem free_right_extends:
@@ -3012,6 +3033,7 @@ Proof.
   rewrite (nextblock_free _ _ _ _ _ H0). auto.
   eapply free_right_inj; eauto.
   unfold inject_id; intros. inv H. eapply H1; eauto. omega.
+  intros. eauto using perm_free_3. 
 Qed.
 
 Theorem free_parallel_extends:
@@ -3029,13 +3051,17 @@ Proof.
     eapply perm_inj with (b1 := b); eauto.
     eapply free_range_perm; eauto.
   destruct X as [m2' FREE]. exists m2'; split; auto.
-  inv H. constructor.
+  constructor.
   rewrite (nextblock_free _ _ _ _ _ H0).
   rewrite (nextblock_free _ _ _ _ _ FREE). auto.
   eapply free_right_inj with (m1 := m1'); eauto.
   eapply free_left_inj; eauto.
-  unfold inject_id; intros. inv H.
+  unfold inject_id; intros. inv H1.
   eapply perm_free_2. eexact H0. instantiate (1 := ofs); omega. eauto.
+  intros. exploit mext_perm_inv0; eauto using perm_free_3. intros [A|A].
+  eapply perm_free_inv in A; eauto. destruct A as [[A B]|A]; auto.
+  subst b0. right; eapply perm_free_2; eauto.
+  right; intuition eauto using perm_free_3.
 Qed.
 
 Theorem valid_block_extends:
@@ -3054,6 +3080,13 @@ Proof.
   eapply perm_inj; eauto.
 Qed.
 
+Theorem perm_extends_inv:
+  forall m1 m2 b ofs k p,
+  extends m1 m2 -> perm m2 b ofs k p -> perm m1 b ofs k p \/ ~perm m1 b ofs Max Nonempty.
+Proof.
+  intros. inv H; eauto.
+Qed.
+
 Theorem valid_access_extends:
   forall m1 m2 chunk b ofs p,
   extends m1 m2 -> valid_access m1 chunk b ofs p -> valid_access m2 chunk b ofs p.
@@ -3110,7 +3143,12 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop :=
       forall b b' delta ofs,
       f b = Some(b', delta) ->
       perm m1 b (Int.unsigned ofs) Max Nonempty \/ perm m1 b (Int.unsigned ofs - 1) Max Nonempty ->
-      delta >= 0 /\ 0 <= Int.unsigned ofs + delta <= Int.max_unsigned
+      delta >= 0 /\ 0 <= Int.unsigned ofs + delta <= Int.max_unsigned;
+    mi_perm_inv:
+      forall b1 ofs b2 delta k p,
+      f b1 = Some(b2, delta) ->
+      perm m2 b2 (ofs + delta) k p ->
+      perm m1 b1 ofs k p \/ ~perm m1 b1 ofs Max Nonempty
   }.
 Definition inject := inject'.
 
@@ -3148,6 +3186,16 @@ Proof.
   intros. inv H0. eapply perm_inj; eauto.
 Qed.
 
+Theorem perm_inject_inv:
+  forall f m1 m2 b1 ofs b2 delta k p,
+  inject f m1 m2 ->
+  f b1 = Some(b2, delta) ->
+  perm m2 b2 (ofs + delta) k p ->
+  perm m1 b1 ofs k p \/ ~perm m1 b1 ofs Max Nonempty.
+Proof.
+  intros. eapply mi_perm_inv; eauto.
+Qed.
+
 Theorem range_perm_inject:
   forall f m1 m2 b1 b2 delta lo hi k p,
   f b1 = Some(b2, delta) ->
@@ -3433,6 +3481,9 @@ Proof.
 (* representable *)
   intros. eapply mi_representable; try eassumption.
   destruct H4; eauto with mem.
+(* perm inv *)
+  intros. exploit mi_perm_inv0; eauto using perm_store_2. 
+  intuition eauto using perm_store_1, perm_store_2.
 Qed.
 
 Theorem store_unmapped_inject:
@@ -3455,6 +3506,9 @@ Proof.
 (* representable *)
   intros. eapply mi_representable; try eassumption.
   destruct H3; eauto with mem.
+(* perm inv *)
+  intros. exploit mi_perm_inv0; eauto using perm_store_2. 
+  intuition eauto using perm_store_1, perm_store_2.
 Qed.
 
 Theorem store_outside_inject:
@@ -3478,6 +3532,8 @@ Proof.
   auto.
 (* representable *)
   eauto with mem.
+(* perm inv *)
+  intros. eauto using perm_store_2.
 Qed.
 
 Theorem storev_mapped_inject:
@@ -3521,6 +3577,9 @@ Proof.
 (* representable *)
   intros. eapply mi_representable0; eauto.
   destruct H4; eauto using perm_storebytes_2.
+(* perm inv *)
+  intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. 
+  intuition eauto using perm_storebytes_1, perm_storebytes_2.
 Qed.
 
 Theorem storebytes_unmapped_inject:
@@ -3543,6 +3602,9 @@ Proof.
 (* representable *)
   intros. eapply mi_representable0; eauto.
   destruct H3; eauto using perm_storebytes_2.
+(* perm inv *)
+  intros. exploit mi_perm_inv0; eauto.
+  intuition eauto using perm_storebytes_1, perm_storebytes_2.
 Qed.
 
 Theorem storebytes_outside_inject:
@@ -3566,6 +3628,8 @@ Proof.
   auto.
 (* representable *)
   auto.
+(* perm inv *)
+  intros. eapply mi_perm_inv0; eauto using perm_storebytes_2.
 Qed.
 
 Theorem storebytes_empty_inject:
@@ -3587,6 +3651,9 @@ Proof.
 (* representable *)
   intros. eapply mi_representable0; eauto.
   destruct H3; eauto using perm_storebytes_2.
+(* perm inv *)
+  intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. 
+  intuition eauto using perm_storebytes_1, perm_storebytes_2.
 Qed.
 
 (* Preservation of allocations *)
@@ -3609,6 +3676,10 @@ Proof.
   auto.
 (* representable *)
   auto.
+(* perm inv *)
+  intros. eapply perm_alloc_inv in H2; eauto. destruct (eq_block b0 b2).
+  subst b0. eelim fresh_block_alloc; eauto. 
+  eapply mi_perm_inv0; eauto.
 Qed.
 
 Theorem alloc_left_unmapped_inject:
@@ -3652,6 +3723,10 @@ Proof.
   destruct (eq_block b b1); try discriminate.
   eapply mi_representable0; try eassumption.
   destruct H4; eauto using perm_alloc_4.
+(* perm inv *)
+  intros. unfold f' in H3; destruct (eq_block b0 b1); try discriminate.
+  exploit mi_perm_inv0; eauto. 
+  intuition eauto using perm_alloc_1, perm_alloc_4.
 (* incr *)
   split. auto.
 (* image *)
@@ -3734,6 +3809,14 @@ Proof.
    generalize (Int.unsigned_range_2 ofs). omega.
   eapply mi_representable0; try eassumption.
   destruct H10; eauto using perm_alloc_4.
+(* perm inv *)
+  intros. unfold f' in H9; destruct (eq_block b0 b1).
+  inversion H9; clear H9; subst b0 b3 delta0.
+  assert (EITHER: lo <= ofs < hi \/ ~(lo <= ofs < hi)) by omega.
+  destruct EITHER.
+  left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto.
+  right; intros A. eapply perm_alloc_inv in A; eauto. rewrite dec_eq_true in A. tauto.
+  exploit mi_perm_inv0; eauto. intuition eauto using perm_alloc_1, perm_alloc_4.
 (* incr *)
   split. auto.
 (* image of b1 *)
@@ -3790,6 +3873,10 @@ Proof.
 (* representable *)
   intros. eapply mi_representable0; try eassumption.
   destruct H2; eauto with mem.
+(* perm inv *)
+  intros. exploit mi_perm_inv0; eauto. intuition eauto using perm_free_3.
+  eapply perm_free_inv in H4; eauto. destruct H4 as [[A B] | A]; auto.
+  subst b1. right; eapply perm_free_2; eauto. 
 Qed.
 
 Lemma free_list_left_inject:
@@ -3825,6 +3912,8 @@ Proof.
   auto.
 (* representable *)
   auto.
+(* perm inv *)
+  intros. eauto using perm_free_3.
 Qed.
 
 Lemma perm_free_list:
@@ -3900,6 +3989,7 @@ Proof.
   intros. destruct H. constructor; eauto.
   eapply drop_outside_inj; eauto.
   intros. unfold valid_block in *. erewrite nextblock_drop; eauto.
+  intros. eapply mi_perm_inv0; eauto using perm_drop_4.
 Qed.
 
 (** Composing two memory injections. *)
@@ -3973,6 +4063,15 @@ Proof.
     ((Int.unsigned ofs - 1) + delta1) by omega.
   destruct H0; eauto using perm_inj.
   rewrite H. omega.
+(* perm inv *)
+  intros. 
+  destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate.
+  destruct (f' b') as [[b'' delta''] |] eqn:?; try discriminate.
+  inversion H; clear H; subst b'' delta.
+  replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') in H0 by omega.
+  exploit mi_perm_inv1; eauto. intros [A|A].
+  eapply mi_perm_inv0; eauto.
+  right; red; intros. elim A. eapply perm_inj; eauto.
 Qed.
 
 Lemma val_lessdef_inject_compose:
@@ -4007,6 +4106,10 @@ Proof.
 (* representable *)
   eapply mi_representable0; eauto.
   destruct H1; eauto using perm_extends.
+(* perm inv *)
+  exploit mi_perm_inv0; eauto. intros [A|A].
+  eapply mext_perm_inv0; eauto.
+  right; red; intros; elim A. eapply perm_extends; eauto.
 Qed.
 
 Lemma inject_extends_compose:
@@ -4026,19 +4129,27 @@ Proof.
   red; intros. eapply mi_no_overlap0; eauto.
 (* representable *)
   eapply mi_representable0; eauto.
+(* perm inv *)
+  exploit mext_perm_inv0; eauto. intros [A|A].
+  eapply mi_perm_inv0; eauto.
+  right; red; intros; elim A. eapply perm_inj; eauto.
 Qed.
 
 Lemma extends_extends_compose:
   forall m1 m2 m3,
   extends m1 m2 -> extends m2 m3 -> extends m1 m3.
 Proof.
-  intros. inv H; inv H0; constructor; intros.
+  intros. inversion H; subst; inv H0; constructor; intros.
   (* nextblock *)
   congruence.
   (* meminj *)
   replace inject_id with (compose_meminj inject_id inject_id).
   eapply mem_inj_compose; eauto.
   apply extensionality; intros. unfold compose_meminj, inject_id. auto.
+  (* perm inv *)
+  exploit mext_perm_inv1; eauto. intros [A|A]. 
+  eapply mext_perm_inv0; eauto.
+  right; red; intros; elim A. eapply perm_extends; eauto.
 Qed.
 
 (** Injecting a memory into itself. *)
@@ -4075,6 +4186,10 @@ Proof.
 (* range *)
   unfold flat_inj; intros.
   destruct (plt b (nextblock m)); inv H0. generalize (Int.unsigned_range_2 ofs); omega.
+(* perm inv *)
+  unfold flat_inj; intros.
+  destruct (plt b1 (nextblock m)); inv H0.
+  rewrite Zplus_0_r in H1; auto.
 Qed.
 
 Theorem empty_inject_neutral:
diff --git a/common/Separation.v b/common/Separation.v
index 4d87443b..6a7ffbea 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -627,6 +627,10 @@ Next Obligation.
 - intros. eapply Mem.valid_block_unchanged_on; eauto. 
 - assumption.
 - assumption.
+- intros. destruct (Mem.perm_dec m0 b1 ofs Max Nonempty); auto.
+  eapply mi_perm_inv; eauto. 
+  eapply Mem.perm_unchanged_on_2; eauto.
+  eapply IMG; eauto. 
 Qed.
 Next Obligation.
   eapply Mem.valid_block_inject_2; eauto.