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.

1 files changed, 122 insertions, 7 deletions

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: