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

3 files changed, 427 insertions, 46 deletions

diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index a29c249..4a57a37 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -523,10 +523,18 @@ Fixpoint init_data_list_size (il: list init_data) {struct il} : Z :=
   | i :: il' => init_data_size i + init_data_list_size il'
   end.
 
+Definition perm_globvar (gv: globvar V) : permission :=
+  if gv.(gvar_volatile) then Nonempty
+  else if gv.(gvar_readonly) then Readable
+  else Writable.
+
 Definition alloc_variable (m: mem) (idv: ident * globvar V) : option mem :=
   let init := idv#2.(gvar_init) in
   let (m', b) := Mem.alloc m 0 (init_data_list_size init) in
-  store_init_data_list m' b 0 init.
+  match store_init_data_list m' b 0 init with
+  | None => None
+  | Some m'' => Mem.drop_perm m'' b 0 (init_data_list_size init) (perm_globvar idv#2)
+  end.
 
 Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V))
                          {struct vl} : option mem :=
@@ -564,8 +572,11 @@ Proof.
   unfold alloc_variable. 
   set (init := gvar_init a#2).
   caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC.
-  caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE REC.
-  rewrite (IHvl _ _ REC). 
+  caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE.
+  caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence.
+  intros m3 DROP REC.
+  rewrite (IHvl _ _ REC).
+  rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
   rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
   rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC).
   unfold block in *; omega.
@@ -595,8 +606,12 @@ Proof.
   intros until m'. simpl. unfold alloc_variable. 
   set (init := gvar_init a#2).
   caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC.
-  caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE REC PERM.
-  eapply IHvl; eauto. 
+  caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE.
+  caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence.
+  intros m3 DROP REC PERM.
+  assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem.
+  eapply IHvl; eauto.
+  eapply Mem.perm_drop_3; eauto. 
   eapply store_init_data_list_perm; eauto. 
   eauto with mem.
 Qed.
@@ -685,13 +700,19 @@ Proof.
   unfold alloc_variable. 
   set (init := gvar_init a#2).
   caseEq (Mem.alloc m 0 (init_data_list_size init)); intros m1 b1 ALLOC.
-  caseEq (store_init_data_list m1 b1 0 init); try congruence. intros m2 STO REC VAL.
+  caseEq (store_init_data_list m1 b1 0 init); try congruence. intros m2 STO.
+  caseEq (Mem.drop_perm m2 b1 0 (init_data_list_size init) (perm_globvar a#2)); try congruence.
+  intros m3 DROP RED VALID.
+  assert (b <> b1). apply Mem.valid_not_valid_diff with m; eauto with mem.
+  transitivity (Mem.load chunk m3 b p).
+  apply IHvl; auto. red.
+  rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
+  rewrite (store_init_data_list_nextblock _ _ _ _ STO).
+  change (Mem.valid_block m1 b). eauto with mem.
   transitivity (Mem.load chunk m2 b p). 
-  apply IHvl; auto. red. rewrite (store_init_data_list_nextblock _ _ _ _ STO).
-  change (Mem.valid_block m1 b). eauto with mem. 
+  eapply Mem.load_drop; eauto. 
   transitivity (Mem.load chunk m1 b p).
-  eapply store_init_data_list_outside; eauto. left. 
-  apply Mem.valid_not_valid_diff with m; eauto with mem.
+  eapply store_init_data_list_outside; eauto. 
   eapply Mem.load_alloc_unchanged; eauto.
 Qed. 
 
@@ -714,8 +735,8 @@ Lemma alloc_variables_charact:
   In (id, gv) vl ->
   exists b, find_symbol (add_variables g vl) id = Some b 
          /\ find_var_info (add_variables g vl) b = Some gv
-         /\ Mem.range_perm m' b 0 (init_data_list_size gv.(gvar_init)) Writable
-         /\ load_store_init_data m' b 0 gv.(gvar_init).
+         /\ Mem.range_perm m' b 0 (init_data_list_size gv.(gvar_init)) (perm_globvar gv)
+         /\ (gv.(gvar_volatile) = false -> load_store_init_data m' b 0 gv.(gvar_init)).
 Proof.
   induction vl; simpl.
   contradiction.
@@ -724,7 +745,9 @@ Proof.
   caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init gv'))); try congruence.
   intros m1 b ALLOC. 
   caseEq (store_init_data_list m1 b 0 (gvar_init gv')); try congruence.
-  intros m2 STORE REC NOREPET IN. inv NOREPET.
+  intros m2 STORE.
+  caseEq (Mem.drop_perm m2 b 0 (init_data_list_size (gvar_init gv')) (perm_globvar gv')); try congruence.
+  intros m3 DROP REC NOREPET IN. inv NOREPET.
   exploit Mem.alloc_result; eauto. intro BEQ. 
   destruct IN. inv H.
   exists (Mem.nextblock m); split. 
@@ -733,17 +756,24 @@ Proof.
   split. rewrite add_variables_same_address. unfold find_var_info; simpl.
   rewrite NEXT. apply ZMap.gss.
   simpl. rewrite <- NEXT; omega.
-  split. red; intros. eapply alloc_variables_perm; eauto. 
-  eapply store_init_data_list_perm; eauto.
-  apply Mem.perm_implies with Freeable; eauto with mem.
+  split. red; intros.
+  eapply alloc_variables_perm; eauto.
+  eapply Mem.perm_drop_1; eauto. 
+  intros NOVOL. 
   apply load_store_init_data_invariant with m2.
-  intros. eapply load_alloc_variables; eauto. 
-  red. rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
+  intros. transitivity (Mem.load chunk m3 (Mem.nextblock m) ofs).
+  eapply load_alloc_variables; eauto. 
+  red. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
+  rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
   change (Mem.valid_block m1 (Mem.nextblock m)). eauto with mem.
+  eapply Mem.load_drop; eauto. repeat right. 
+  unfold perm_globvar. rewrite NOVOL. destruct (gvar_readonly gv); auto with mem.
   eapply store_init_data_list_charact; eauto. 
 
-  apply IHvl with m2; auto.
-  simpl. rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
+  apply IHvl with m3; auto.
+  simpl.
+  rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
+  rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
   rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). unfold block in *; omega.
 Qed.
 
@@ -785,8 +815,8 @@ Theorem find_var_exists:
   init_mem p = Some m ->
   exists b, find_symbol (globalenv p) id = Some b
          /\ find_var_info (globalenv p) b = Some gv
-         /\ Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) Writable
-         /\ load_store_init_data (globalenv p) m b 0 gv.(gvar_init).
+         /\ Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) (perm_globvar gv)
+         /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p) m b 0 gv.(gvar_init)).
 Proof.
   intros. exploit alloc_variables_charact; eauto. 
   instantiate (1 := Mem.empty). rewrite add_functions_nextvar. rewrite Mem.nextblock_empty; auto.
@@ -839,11 +869,15 @@ Lemma alloc_variable_neutral:
   Mem.inject_neutral thr m'.
 Proof.
   intros until m'. unfold alloc_variable. 
-  caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init id#2))); intros m1 b; intros.
+  caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init id#2))); intros m1 b ALLOC.
+  caseEq (store_init_data_list ge m1 b 0 (gvar_init id#2)); try congruence.
+  intros m2 STORE DROP NEUTRAL NEXT.
+  eapply Mem.drop_inject_neutral; eauto. 
   eapply store_init_data_list_neutral with (b := b).
   eapply Mem.alloc_inject_neutral; eauto.
-  rewrite (Mem.alloc_result _ _ _ _ _ H). auto.
+  rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto.
   eauto.
+  rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto.
 Qed.
 
 Lemma alloc_variables_neutral:
@@ -1067,6 +1101,10 @@ Proof.
   destruct (Mem.alloc m 0 (init_data_list_size init)). 
   rewrite store_init_data_list_match. 
   destruct (store_init_data_list (globalenv p) m0 b 0 init); auto.
+  change (perm_globvar (mkglobvar info2 init ro vo))
+    with (perm_globvar (mkglobvar info1 init ro vo)).
+  destruct (Mem.drop_perm m1 b 0 (init_data_list_size init)
+    (perm_globvar (mkglobvar info1 init ro vo))); auto.
 Qed.
 
 Theorem init_mem_match:
diff --git a/common/Memory.v b/common/Memory.v
index 0e9fbfa..6de00e7 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.
diff --git a/common/Memtype.v b/common/Memtype.v
index cbf3ffe..050cc84 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -137,6 +137,13 @@ Fixpoint free_list (m: mem) (l: list (block * Z * Z)) {struct l}: option mem :=
       end
   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. *)
+
+Parameter drop_perm: forall (m: mem) (b: block) (lo hi: Z) (p: permission), option mem.
+
 (** * Permissions, block validity, access validity, and bounds *)
 
 (** The next block of a memory state is the block identifier for the
@@ -647,6 +654,42 @@ Axiom load_free:
   b <> bf \/ lo >= hi \/ ofs + size_chunk chunk <= lo \/ hi <= ofs ->
   load chunk m2 b ofs = load chunk m1 b ofs.
 
+(** ** Properties of [drop_perm]. *)
+
+Axiom nextblock_drop:
+  forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
+  nextblock m' = nextblock m.
+
+Axiom 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.
+Axiom 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' }.
+
+Axiom perm_drop_1:
+  forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
+  forall ofs, lo <= ofs < hi -> perm m' b ofs p.
+Axiom perm_drop_2:
+  forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
+  forall ofs p', lo <= ofs < hi -> perm m' b ofs p' -> perm_order p p'.
+Axiom perm_drop_3:
+  forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
+  forall b' ofs p', b' <> b \/ ofs < lo \/ hi <= ofs -> perm m b' ofs p' -> perm m' b' ofs p'.
+Axiom perm_drop_4:
+  forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
+  forall b' ofs p', perm m' b' ofs p' -> perm m b' ofs p'.
+
+Axiom bounds_drop:
+  forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
+  forall b', bounds m' b' = bounds m b'.
+
+Axiom load_drop:
+  forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
+  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.
+
 (** * Relating two memory states. *)
 
 (** ** Memory extensions *)
@@ -973,4 +1016,11 @@ Axiom store_inject_neutral:
   val_inject (flat_inj thr) v v ->
   inject_neutral thr m'.
 
+Axiom 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'.
+
 End MEM.