From f7270a57205abd7314203eaef9b752a7abd13ed7 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 21 Sep 2010 07:34:06 +0000
Subject: Memory.v: added drop_perm operation Globalenvs.v: used drop_perm to
 set appropriate permissions on global variables   (Notempty if volatile;
 Readable if readonly; Writable otherwise)

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1510 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/Memory.v | 337 ++++++++++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 315 insertions(+), 22 deletions(-)

(limited to 'common/Memory.v')

diff --git a/common/Memory.v b/common/Memory.v
index 0e9fbfa5..6de00e7c 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -440,7 +440,6 @@ Next Obligation.
 Qed.
 Next Obligation.
   unfold clearN, update.
-(*  destruct (noread_undef m b0 ofs); auto.*)
   destruct (zeq b0 b). subst b0. 
   destruct (zle lo ofs); simpl; auto.
   destruct (zlt ofs hi); simpl; auto.
@@ -546,16 +545,21 @@ Proof.
   apply IHvl. 
 Qed.
 
+Remark getN_exten:
+  forall c1 c2 n p,
+  (forall i, p <= i < p + Z_of_nat n -> c1 i = c2 i) ->
+  getN n p c1 = getN n p c2.
+Proof.
+  induction n; intros. auto. rewrite inj_S in H. simpl. decEq. 
+  apply H. omega. apply IHn. intros. apply H. omega.
+Qed.
+
 Remark getN_setN_outside:
   forall vl q c n p,
   p + Z_of_nat n <= q \/ q + Z_of_nat (length vl) <= p ->
   getN n p (setN vl q c) = getN n p c.
 Proof.
-  induction n; intros; simpl.
-  auto.
-  rewrite inj_S in H. decEq.
-  apply setN_outside. omega. 
-  apply IHn. omega.
+  intros. apply getN_exten. intros. apply setN_outside. omega. 
 Qed.
 
 Lemma store_noread_undef:
@@ -564,20 +568,19 @@ Lemma store_noread_undef:
        perm m b' ofs' Readable \/ 
         update b (setN (encode_val ch v) ofs (mem_contents m b)) (mem_contents m) b' ofs' = Undef.
 Proof.
-intros.
-destruct VA as [? _].
-(*specialize (H ofs').*)
-unfold update.
-destruct (zeq b' b).
-subst b'.
-assert (ofs <= ofs' < ofs + size_chunk ch \/ (ofs' < ofs \/ ofs' >= ofs + size_chunk ch)) by omega.
-destruct H0.
-exploit (H ofs'); auto; intro.
-eauto with mem.
-rewrite setN_outside.
-destruct (noread_undef m b ofs'); auto.
-rewrite encode_val_length. rewrite <- size_chunk_conv; auto.
-destruct (noread_undef m b' ofs'); auto.
+  intros.
+  destruct VA as [? _].
+  unfold update.
+  destruct (zeq b' b).
+  subst b'.
+  assert (ofs <= ofs' < ofs + size_chunk ch \/ (ofs' < ofs \/ ofs' >= ofs + size_chunk ch)) by omega.
+  destruct H0.
+  exploit (H ofs'); auto; intro.
+  eauto with mem.
+  rewrite setN_outside.
+  destruct (noread_undef m b ofs'); auto.
+  rewrite encode_val_length. rewrite <- size_chunk_conv; auto.
+  destruct (noread_undef m b' ofs'); auto.
 Qed.
 
 (** [store chunk m b ofs v] perform a write in memory state [m].
@@ -588,8 +591,8 @@ Qed.
 Definition store (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val): option mem :=
  match valid_access_dec m chunk b ofs Writable with
  | left VA => Some (mkmem (update b 
-                                               (setN (encode_val chunk v) ofs (m.(mem_contents) b))
-                                              m.(mem_contents))
+                                  (setN (encode_val chunk v) ofs (m.(mem_contents) b))
+                                  m.(mem_contents))
                     m.(mem_access)
                     m.(bounds)
                     m.(nextblock)
@@ -609,6 +612,44 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
   | _ => None
   end.
 
+(** [drop_perm m b lo hi p] sets the permissions of the byte range
+    [(b, lo) ... (b, hi - 1)] to [p].  These bytes must have permissions
+    at least [p] in the initial memory state [m].
+    Returns updated memory state, or [None] if insufficient permissions. *)
+
+Program Definition drop_perm (m: mem) (b: block) (lo hi: Z) (p: permission): option mem :=
+  if range_perm_dec m b lo hi p then
+    Some (mkmem (update b 
+                        (fun ofs => if zle lo ofs && zlt ofs hi && negb (perm_order_dec p Readable)
+                                    then Undef else m.(mem_contents) b ofs)
+                        m.(mem_contents))
+                (update b
+                        (fun ofs => if zle lo ofs && zlt ofs hi then Some p else m.(mem_access) b ofs)
+                        m.(mem_access))
+                m.(bounds) m.(nextblock) _ _ _ _)
+  else None.
+Next Obligation.
+  destruct m; auto.
+Qed.
+Next Obligation.
+  destruct m; auto.
+Qed.
+Next Obligation.
+  unfold update. destruct (zeq b0 b). subst b0.
+  destruct (zle lo ofs). destruct (zlt ofs hi).
+  exploit range_perm_in_bounds; eauto. omega. intros. omegaContradiction. 
+  simpl. eapply bounds_noaccess; eauto. 
+  simpl. eapply bounds_noaccess; eauto.
+  eapply bounds_noaccess; eauto. 
+Qed.
+Next Obligation.
+  unfold update. destruct (zeq b0 b). subst b0. 
+  destruct (zle lo ofs && zlt ofs hi). 
+  destruct (perm_order_dec p Readable); simpl; auto.
+  eapply noread_undef; eauto.
+  eapply noread_undef; eauto.
+Qed.
+
 (** * Properties of the memory operations *)
 
 (** Properties of the empty store. *)
@@ -1694,6 +1735,148 @@ Hint Local Resolve valid_block_free_1 valid_block_free_2
              perm_free_1 perm_free_2 perm_free_3 
              valid_access_free_1 valid_access_free_inv_1: mem.
 
+(** ** Properties related to [drop_perm] *)
+
+Theorem range_perm_drop_1:
+  forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> range_perm m b lo hi p.
+Proof.
+  unfold drop_perm; intros. 
+  destruct (range_perm_dec m b lo hi p). auto. discriminate.
+Qed.
+
+Theorem range_perm_drop_2:
+  forall m b lo hi p,
+  range_perm m b lo hi p -> {m' | drop_perm m b lo hi p = Some m' }.
+Proof.
+  unfold drop_perm; intros. 
+  destruct (range_perm_dec m b lo hi p). econstructor. eauto. contradiction.
+Qed.
+
+Section DROP.
+
+Variable m: mem.
+Variable b: block.
+Variable lo hi: Z.
+Variable p: permission.
+Variable m': mem.
+Hypothesis DROP: drop_perm m b lo hi p = Some m'.
+
+Theorem nextblock_drop:
+  nextblock m' = nextblock m.
+Proof.
+  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP; auto.
+Qed.
+
+Theorem perm_drop_1:
+  forall ofs, lo <= ofs < hi -> perm m' b ofs p.
+Proof.
+  intros.
+  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP.
+  unfold perm. simpl. rewrite update_s. unfold proj_sumbool. 
+  rewrite zle_true. rewrite zlt_true. simpl. constructor.
+  omega. omega. 
+Qed.
+  
+Theorem perm_drop_2:
+  forall ofs p', lo <= ofs < hi -> perm m' b ofs p' -> perm_order p p'.
+Proof.
+  intros.
+  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP.
+  revert H0. unfold perm; simpl. rewrite update_s. unfold proj_sumbool. 
+  rewrite zle_true. rewrite zlt_true. simpl. auto. 
+  omega. omega. 
+Qed.
+
+Theorem perm_drop_3:
+  forall b' ofs p', b' <> b \/ ofs < lo \/ hi <= ofs -> perm m b' ofs p' -> perm m' b' ofs p'.
+Proof.
+  intros.
+  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP.
+  unfold perm; simpl. unfold update. destruct (zeq b' b). subst b'. 
+  unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi). 
+  byContradiction. intuition omega.
+  auto. auto. auto.
+Qed.
+
+Theorem perm_drop_4:
+  forall b' ofs p', perm m' b' ofs p' -> perm m b' ofs p'.
+Proof.
+  intros.
+  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP.
+  revert H. unfold perm; simpl. unfold update. destruct (zeq b' b). 
+  subst b'. unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi).
+  simpl. intros. apply perm_implies with p. apply r. tauto. auto.
+  auto. auto. auto.
+Qed.
+
+Theorem bounds_drop:
+  forall b', bounds m' b' = bounds m b'.
+Proof.
+  intros.
+  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP.
+  unfold bounds; simpl. auto.
+Qed.
+
+Lemma valid_access_drop_1:
+  forall chunk b' ofs p', 
+  b' <> b \/ ofs + size_chunk chunk <= lo \/ hi <= ofs \/ perm_order p p' ->
+  valid_access m chunk b' ofs p' -> valid_access m' chunk b' ofs p'.
+Proof.
+  intros. destruct H0. split; auto. 
+  red; intros.
+  destruct (zeq b' b). subst b'.
+  destruct (zlt ofs0 lo). eapply perm_drop_3; eauto. 
+  destruct (zle hi ofs0). eapply perm_drop_3; eauto.
+  apply perm_implies with p. eapply perm_drop_1; eauto. omega. 
+  generalize (size_chunk_pos chunk); intros. intuition. omegaContradiction. omegaContradiction.
+  eapply perm_drop_3; eauto.
+Qed.
+
+Lemma valid_access_drop_2:
+  forall chunk b' ofs p', 
+  valid_access m' chunk b' ofs p' -> valid_access m chunk b' ofs p'.
+Proof.
+  intros. destruct H; split; auto. 
+  red; intros. eapply perm_drop_4; eauto. 
+Qed.
+
+(*
+Lemma valid_access_drop_3:
+  forall chunk b' ofs p',
+  valid_access m' chunk b' ofs p' ->
+  b' <> b \/ Intv.disjoint (lo, hi) (ofs, ofs + size_chunk chunk) \/ perm_order p p'.
+Proof.
+  intros. destruct H. 
+  destruct (zeq b' b); auto. subst b'.
+  destruct (Intv.disjoint_dec (lo, hi) (ofs, ofs + size_chunk chunk)); auto. 
+  exploit intv_not_disjoint; eauto. intros [x [A B]]. 
+  right; right. apply perm_drop_2 with x. auto. apply H. auto. 
+Qed.
+*)
+
+Theorem load_drop:
+  forall chunk b' ofs, 
+  b' <> b \/ ofs + size_chunk chunk <= lo \/ hi <= ofs \/ perm_order p Readable ->
+  load chunk m' b' ofs = load chunk m b' ofs.
+Proof.
+  intros.
+  unfold load.
+  destruct (valid_access_dec m chunk b' ofs Readable).
+  rewrite pred_dec_true.
+  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP. simpl.
+  unfold update. destruct (zeq b' b). subst b'. decEq. decEq. 
+  apply getN_exten. rewrite <- size_chunk_conv. intros.
+  unfold proj_sumbool. destruct (zle lo i). destruct (zlt i hi). destruct (perm_order_dec p Readable).
+  auto.
+  elimtype False. intuition.
+  auto. auto. auto.
+  eapply valid_access_drop_1; eauto. 
+  rewrite pred_dec_false. auto.
+  red; intros; elim n. eapply valid_access_drop_2; eauto.
+Qed.
+
+End DROP.
+
 (** * Extensionality properties *)
 
 Lemma mem_access_ext:
@@ -2109,6 +2292,103 @@ Proof.
   rewrite (clearN_out _ _ _ _ _ _ H4); auto.
 Qed.
 
+(** Preservation of [drop_perm] operations. *)
+
+Lemma drop_unmapped_inj:
+  forall f m1 m2 b lo hi p m1',
+  mem_inj f m1 m2 ->
+  drop_perm m1 b lo hi p = Some m1' ->
+  f b = None ->
+  mem_inj f m1' m2.
+Proof.
+  intros. inv H. constructor. 
+  intros. eapply mi_access0. eauto.
+  eapply valid_access_drop_2; eauto. 
+  intros. replace (mem_contents m1' b1 ofs) with (mem_contents m1 b1 ofs). 
+  apply mi_memval0; auto. 
+  eapply perm_drop_4; eauto. 
+  unfold drop_perm in H0. destruct (range_perm_dec m1 b lo hi p); inv H0. 
+  simpl. rewrite update_o; auto. congruence.
+Qed.
+
+Lemma drop_mapped_inj:
+  forall f m1 m2 b1 b2 delta lo hi p m1',
+  mem_inj f m1 m2 ->
+  drop_perm m1 b1 lo hi p = Some m1' ->
+  meminj_no_overlap f m1 ->
+  f b1 = Some(b2, delta) ->
+  exists m2',
+      drop_perm m2 b2 (lo + delta) (hi + delta) p = Some m2'
+   /\ mem_inj f m1' m2'.
+Proof.
+  intros. 
+  assert ({ m2' | drop_perm m2 b2 (lo + delta) (hi + delta) p = Some m2' }).
+  apply range_perm_drop_2. red; intros. 
+  replace ofs with ((ofs - delta) + delta) by omega.
+  eapply perm_inj; eauto. eapply range_perm_drop_1; eauto. omega. 
+  destruct X as [m2' DROP]. exists m2'; split; auto.
+  inv H. constructor; intros.
+(* access *)
+  exploit mi_access0; eauto. eapply valid_access_drop_2; eauto.
+  intros [A B]. split; auto. red; intros.
+  destruct (eq_block b1 b0). subst b0. rewrite H2 in H; inv H.
+  (* b1 = b0 *)
+  destruct (zlt ofs0 (lo + delta0)). eapply perm_drop_3; eauto. 
+  destruct (zle (hi + delta0) ofs0). eapply perm_drop_3; eauto.
+  destruct H3 as [C D].
+  assert (perm_order p p0).
+    eapply perm_drop_2. eexact H0. instantiate (1 := ofs0 - delta0). omega. 
+    apply C. omega. 
+  apply perm_implies with p; auto.
+  eapply perm_drop_1. eauto. omega.
+  (* b1 <> b0 *)
+  eapply perm_drop_3; eauto.
+  exploit H1; eauto. intros [P | P]. auto. right. 
+  destruct (zlt lo hi). 
+  exploit range_perm_in_bounds. eapply range_perm_drop_1. eexact H0. auto. 
+  intros [U V].
+  exploit valid_access_drop_2. eexact H0. eauto.
+  intros [C D].
+  exploit range_perm_in_bounds. eexact C. generalize (size_chunk_pos chunk); omega. 
+  intros [X Y].
+  generalize (size_chunk_pos chunk). omega.
+  omega.
+(* memval *)
+  assert (A: perm m1 b0 ofs Nonempty). eapply perm_drop_4; eauto.
+  exploit mi_memval0; eauto. intros B.
+  unfold drop_perm in *. 
+  destruct (range_perm_dec m1 b1 lo hi p); inversion H0; clear H0. clear H5.
+  destruct (range_perm_dec m2 b2 (lo + delta) (hi + delta) p); inversion DROP; clear DROP. clear H4.
+  simpl. unfold update. destruct (zeq b0 b1). 
+  (* b1 = b0 *)
+  subst b0. rewrite H2 in H; inv H. rewrite zeq_true. unfold proj_sumbool. 
+  destruct (zle lo ofs).
+  rewrite zle_true. 
+  destruct (zlt ofs hi).
+  rewrite zlt_true.
+  destruct (perm_order_dec p Readable).
+  simpl. auto.
+  simpl. constructor.
+  omega.
+  rewrite zlt_false. simpl. auto. omega. 
+  omega.
+  rewrite zle_false. simpl. auto. omega.
+  (* b1 <> b0 *)
+  destruct (zeq b3 b2).
+  (* b2 = b3 *)
+  subst b3. exploit H1. eauto. eauto. eauto. intros [P | P]. congruence.
+  exploit perm_in_bounds; eauto. intros X.
+  destruct (zle (lo + delta) (ofs + delta0)).
+  destruct (zlt (ofs + delta0) (hi + delta)).
+  destruct (zlt lo hi). 
+  exploit range_perm_in_bounds. eexact r. auto. intros [Y Z].
+  omegaContradiction.
+  omegaContradiction.
+  simpl. auto.
+  simpl. auto.
+  auto.
+Qed.
+
 (** * Memory extensions *)
 
 (**  A store [m2] extends a store [m1] if [m2] can be obtained from [m1]
@@ -3030,6 +3310,19 @@ Proof.
   intros [m'' [A B]]. congruence.
 Qed. 
 
+Theorem drop_inject_neutral:
+  forall m b lo hi p m' thr,
+  drop_perm m b lo hi p = Some m' ->
+  inject_neutral thr m ->
+  b < thr ->
+  inject_neutral thr m'.
+Proof.
+  unfold inject_neutral; intros.
+  exploit drop_mapped_inj; eauto. apply flat_inj_no_overlap. 
+  unfold flat_inj. apply zlt_true; eauto. 
+  repeat rewrite Zplus_0_r. intros [m'' [A B]]. congruence.
+Qed.
+
 End Mem.
 
 Notation mem := Mem.mem.
-- 
cgit