Merge of the newmem branch:

- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 126 insertions, 150 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 508c414..0d29a23 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -956,3 +956,9 @@ let atom_is_small_data a ofs =
     (Hashtbl.find decl_atom a).a_small_data
   with Not_found ->
     false
+
+let atom_is_inline a =
+  try
+    (Hashtbl.find decl_atom a).a_inline
+  with Not_found ->
+    false
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 1a66ec9..f94e081 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -150,10 +150,10 @@ Proof.
 Qed.
 
 Lemma perm_freelist:
-  forall fbl m m' b ofs p,
+  forall fbl m m' b ofs k p,
   Mem.free_list m fbl = Some m' ->
-  Mem.perm m' b ofs p ->
-  Mem.perm m b ofs p.
+  Mem.perm m' b ofs k p ->
+  Mem.perm m b ofs k p.
 Proof.
   induction fbl; simpl; intros until p.
   congruence.
@@ -177,7 +177,7 @@ Lemma free_list_freeable:
   forall l m m',
   Mem.free_list m l = Some m' ->
   forall b lo hi,
-  In (b, lo, hi) l -> Mem.range_perm m b lo hi Freeable.
+  In (b, lo, hi) l -> Mem.range_perm m b lo hi Cur Freeable.
 Proof.
   induction l; simpl; intros.
   contradiction.
@@ -189,18 +189,6 @@ Proof.
   red; intros. eapply Mem.perm_free_3; eauto. exploit IHl; eauto.
 Qed.
 
-Lemma bounds_freelist:
-  forall b l m m',
-  Mem.free_list m l = Some m' -> Mem.bounds m' b = Mem.bounds m b.
-Proof.
-  induction l; simpl; intros.
-  inv H; auto.
-  revert H. destruct a as [[b' lo'] hi'].
-  caseEq (Mem.free m b' lo' hi'); try congruence.
-  intros m1 FREE1 FREE2.
-  transitivity (Mem.bounds m1 b). eauto. eapply Mem.bounds_free; eauto.
-Qed.
-
 Lemma nextblock_storev:
   forall chunk m addr v m',
   Mem.storev chunk m addr v = Some m' -> Mem.nextblock m' = Mem.nextblock m.
@@ -324,8 +312,8 @@ Record match_env (f: meminj) (cenv: compilenv)
 
 (** The sizes of blocks appearing in [e] agree with their types *)
     me_bounds:
-      forall id b lv,
-      PTree.get id e = Some(b, lv) -> Mem.bounds m b = (0, sizeof lv)
+      forall id b lv ofs p,
+      PTree.get id e = Some(b, lv) -> Mem.perm m b ofs Max p -> 0 <= ofs < sizeof lv
   }.
 
 Hint Resolve me_low_high.
@@ -351,7 +339,7 @@ Proof.
   rewrite <- H4. eapply Mem.load_store_other; eauto. 
   left. congruence.
   (* bounds *)
-  intros. rewrite (Mem.bounds_store _ _ _ _ _ _ H0). eauto. 
+  intros. eauto with mem. 
 Qed.
 
 (** Preservation by assignment to a Csharpminor variable that is 
@@ -403,7 +391,7 @@ Proof.
   (* temps *)
   intros. rewrite PTree.gso. auto. unfold for_temp, for_var; congruence. 
   (* bounds *)
-  intros. rewrite (Mem.bounds_store _ _ _ _ _ _ H2). eauto. 
+  intros. eauto with mem. 
 Qed.
 
 (** Preservation by assignment to a Csharpminor temporary and the
@@ -442,16 +430,14 @@ Lemma match_env_invariant:
   (forall b ofs chunk v, 
      lo <= b < hi -> Mem.load chunk m1 b ofs = Some v ->
      Mem.load chunk m2 b ofs = Some v) ->
-  (forall b,
-     lo <= b < hi -> Mem.bounds m2 b = Mem.bounds m1 b) ->
+  (forall b ofs p,
+     lo <= b < hi -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
   match_env f cenv e le m1 te sp lo hi ->
   match_env f cenv e le m2 te sp lo hi.
 Proof.
   intros. inv H1. constructor; eauto.
   (* vars *)
   intros. geninv (me_vars0 id); econstructor; eauto.
-  (* bounds *)
-  intros. rewrite H0. eauto. eauto.
 Qed.
 
 (** [match_env] is insensitive to the Cminor values of stack-allocated data. *)
@@ -551,10 +537,10 @@ Proof.
   exploit Mem.alloc_result; eauto. unfold block; omega.
 (* bounds *)
   intros. rewrite PTree.gsspec in H.
-  rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). 
+  exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. 
   destruct (peq id0 id). 
-  inv H. apply dec_eq_true.
-  rewrite dec_eq_false. eauto. 
+  inv H. rewrite zeq_true. auto. 
+  rewrite zeq_false. eauto. 
   apply Mem.valid_not_valid_diff with m1.
   exploit me_bounded0; eauto. intros [A B]. auto. 
   eauto with mem.
@@ -599,7 +585,8 @@ Proof.
   intros. eapply me_incr0; eauto. rewrite <- OTHER; eauto. 
   exploit Mem.alloc_result; eauto. unfold block in *; omega.
 (* bounds *)
-  intros. rewrite (Mem.bounds_alloc_other _ _ _ _ _ ALLOC). eauto.
+  intros. exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. 
+  rewrite zeq_false. eauto. 
   exploit me_bounded0; eauto.
 Qed.
 
@@ -634,7 +621,7 @@ Lemma match_env_external_call:
   mem_unchanged_on (loc_unmapped f1) m1 m2 ->
   inject_incr f1 f2 ->
   inject_separated f1 f2 m1 m1' ->
-  (forall b, Mem.valid_block m1 b -> Mem.bounds m2 b = Mem.bounds m1 b) ->
+  (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
   hi <= Mem.nextblock m1 -> sp < Mem.nextblock m1' ->
   match_env f2 cenv e le m2 te sp lo hi.
 Proof.
@@ -661,7 +648,7 @@ Proof.
   instantiate (1 := b). red; omega. intros. 
   apply me_incr0 with b delta. congruence. auto.
 (* bounds *)
-  intros. rewrite BOUNDS; eauto. 
+  intros. eapply me_bounds0; eauto. eapply BOUNDS; eauto. 
   red. exploit me_bounded0; eauto. omega.
 Qed.
 
@@ -704,13 +691,12 @@ Inductive match_globalenvs (f: meminj) (bound: Z): Prop :=
   that are not images of C#minor local variable blocks.
 *)
 
-Definition padding_freeable (f: meminj) (m: mem) (tm: mem) (sp: block) (sz: Z) : Prop :=
+Definition padding_freeable (f: meminj) (e: Csharpminor.env) (tm: mem) (sp: block) (sz: Z) : Prop :=
   forall ofs, 
   0 <= ofs < sz ->
-  Mem.perm tm sp ofs Freeable
-  \/ exists b, exists delta, 
-       f b = Some(sp, delta) 
-       /\ Mem.low_bound m b + delta <= ofs < Mem.high_bound m b + delta.
+  Mem.perm tm sp ofs Cur Freeable
+  \/ exists id, exists b, exists lv, exists delta,
+     e!id = Some(b, lv) /\ f b = Some(sp, delta) /\ delta <= ofs < delta + sizeof lv.
 
 Inductive match_callstack (f: meminj) (m: mem) (tm: mem):
                           callstack -> Z -> Z -> Prop :=
@@ -724,7 +710,7 @@ Inductive match_callstack (f: meminj) (m: mem) (tm: mem):
         (BOUND: hi <= bound)
         (TBOUND: sp < tbound)
         (MENV: match_env f cenv e le m te sp lo hi)
-        (PERM: padding_freeable f m tm sp tf.(fn_stackspace))
+        (PERM: padding_freeable f e tm sp tf.(fn_stackspace))
         (MCS: match_callstack f m tm cs lo sp),
       match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) bound tbound.
 
@@ -742,22 +728,20 @@ Qed.
     generalize those for [match_env]. *)
 
 Lemma padding_freeable_invariant:
-  forall f1 m1 tm1 sp sz cenv e le te lo hi f2 m2 tm2,
-  padding_freeable f1 m1 tm1 sp sz ->
+  forall f1 m1 tm1 sp sz cenv e le te lo hi f2 tm2,
+  padding_freeable f1 e tm1 sp sz ->
   match_env f1 cenv e le m1 te sp lo hi ->
-  (forall ofs, Mem.perm tm1 sp ofs Freeable -> Mem.perm tm2 sp ofs Freeable) ->
-  (forall b, b < hi -> Mem.bounds m2 b = Mem.bounds m1 b) ->
+  (forall ofs, Mem.perm tm1 sp ofs Cur Freeable -> Mem.perm tm2 sp ofs Cur Freeable) ->
   (forall b, b < hi -> f2 b = f1 b) ->
-  padding_freeable f2 m2 tm2 sp sz.
+  padding_freeable f2 e tm2 sp sz.
 Proof.
   intros; red; intros.
-  exploit H; eauto. intros [A | [b [delta [A B]]]].
+  exploit H; eauto. intros [A | [id [b [lv [delta [A [B C]]]]]]].
   left; auto. 
-  exploit me_inv; eauto. intros [id [lv C]]. 
-  exploit me_bounded; eauto. intros [D E]. 
-  right; exists b; exists delta. split.
-  rewrite H3; auto. 
-  rewrite H2; auto.
+  exploit me_bounded; eauto. intros [D E].
+  right; exists id; exists b; exists lv; exists delta; split.
+  auto.
+  rewrite H2; auto. 
 Qed.
 
 Lemma match_callstack_store_mapped:
@@ -775,7 +759,6 @@ Proof.
   eapply match_env_store_mapped; eauto. congruence.
   eapply padding_freeable_invariant; eauto. 
   intros; eauto with mem.
-  intros. eapply Mem.bounds_store; eauto.
 Qed.
 
 Lemma match_callstack_storev_mapped:
@@ -800,21 +783,17 @@ Lemma match_callstack_invariant:
     hi <= bound ->
     match_env f cenv e le m te sp lo hi ->
     match_env f cenv e le m' te sp lo hi) ->
-  (forall b,
-    b < bound -> Mem.bounds m' b = Mem.bounds m b) ->
-  (forall b ofs p,
-    b < tbound -> Mem.perm tm b ofs p -> Mem.perm tm' b ofs p) ->
+  (forall b ofs k p,
+    b < tbound -> Mem.perm tm b ofs k p -> Mem.perm tm' b ofs k p) ->
   match_callstack f m' tm' cs bound tbound.
 Proof.
   induction 1; intros.
   econstructor; eauto.
   constructor; auto.
-  eapply padding_freeable_invariant; eauto. 
-  intros. apply H1. omega.
+  eapply padding_freeable_invariant; eauto.
   eapply IHmatch_callstack; eauto. 
   intros. eapply H0; eauto. inv MENV; omega.
   intros. apply H1; auto. inv MENV; omega. 
-  intros. apply H2; auto. omega. 
 Qed.
 
 Lemma match_callstack_store_local:
@@ -828,14 +807,11 @@ Lemma match_callstack_store_local:
 Proof.
   intros. inv H3. constructor; auto.
   eapply match_env_store_local; eauto.
-  eapply padding_freeable_invariant; eauto.
-  intros. eapply Mem.bounds_store; eauto.
   eapply match_callstack_invariant; eauto.
   intros. apply match_env_invariant with m1; auto.
   intros. rewrite <- H6. eapply Mem.load_store_other; eauto. 
-  left. inv MENV. exploit me_bounded0; eauto. unfold block in *; omega. 
-  intros. eapply Mem.bounds_store; eauto.
-  intros. eapply Mem.bounds_store; eauto.
+  left. inv MENV. exploit me_bounded0; eauto. unfold block in *; omega.
+  intros. eauto with mem.
 Qed.
 
 (** A variant of [match_callstack_store_local] where the Cminor environment
@@ -923,11 +899,9 @@ Proof.
   assert ({tm' | Mem.free tm sp 0 (fn_stackspace tf) = Some tm'}).
   apply Mem.range_perm_free.
   red; intros.
-  exploit PERM; eauto. intros [A | [b [delta [A B]]]].
+  exploit PERM; eauto. intros [A | [id [b [lv [delta [A [B C]]]]]]]. 
   auto.
-  exploit me_inv0; eauto. intros [id [lv C]]. 
-  exploit me_bounds0; eauto. intro D. rewrite D in B; simpl in B.
-  assert (Mem.range_perm m b 0 (sizeof lv) Freeable). 
+  assert (Mem.range_perm m b 0 (sizeof lv) Cur Freeable). 
   eapply free_list_freeable; eauto. eapply in_blocks_of_env; eauto.
   replace ofs with ((ofs - delta) + delta) by omega. 
   eapply Mem.perm_inject; eauto. apply H0. omega. 
@@ -943,15 +917,13 @@ Proof.
   intros. exploit in_blocks_of_env_inv; eauto. 
   intros [id [lv [A [B C]]]]. 
   exploit me_bounded0; eauto. unfold block; omega.
-  intros. eapply bounds_freelist; eauto.
-  intros. eapply bounds_freelist; eauto.
+  intros. eapply perm_freelist; eauto.
   intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega.
   eapply Mem.free_inject; eauto.
   intros. exploit me_inv0; eauto. intros [id [lv A]]. 
   exists 0; exists (sizeof lv); split.
   eapply in_blocks_of_env; eauto.
-  exploit me_bounds0; eauto. intro B. 
-  exploit Mem.perm_in_bounds; eauto. rewrite B; simpl. auto.
+  eapply me_bounds0; eauto. eapply Mem.perm_max. eauto. 
 Qed.
 
 (** Preservation of [match_callstack] by allocations. *)
@@ -975,7 +947,6 @@ Proof.
   constructor; auto.
   eapply match_env_alloc_other; eauto. omega. destruct (f2 b); auto. destruct p; omega.
   eapply padding_freeable_invariant; eauto. 
-  intros. eapply Mem.bounds_alloc_other; eauto. unfold block; omega.
   intros. apply H1. unfold block; omega.
   apply IHmatch_callstack. 
   inv MENV; omega. 
@@ -1004,9 +975,12 @@ Proof.
   constructor.
   omega. auto. 
   eapply match_env_alloc_same; eauto.
-  eapply padding_freeable_invariant; eauto. 
-  intros. eapply Mem.bounds_alloc_other; eauto. unfold block in *; omega.
-  intros. apply OTHER. unfold block in *; omega. 
+  red; intros. exploit PERM; eauto. intros [A | [id' [b' [lv' [delta' [A [B C]]]]]]].
+  left; auto.
+  right; exists id'; exists b'; exists lv'; exists delta'.
+  split. rewrite PTree.gso; auto. congruence. 
+  split. apply INCR; auto. 
+  auto.
   eapply match_callstack_alloc_below; eauto.
   inv MENV. unfold block in *; omega.
   inv ACOND. auto. omega. omega.
@@ -1059,43 +1033,42 @@ Qed.
 
 (** Decidability of the predicate "this is not a padding location" *)
 
-Definition is_reachable (f: meminj) (m: mem) (sp: block) (ofs: Z) : Prop :=
-  exists b, exists delta, 
-  f b = Some(sp, delta)
-  /\ Mem.low_bound m b + delta <= ofs < Mem.high_bound m b + delta.
+Definition is_reachable (f: meminj) (e: Csharpminor.env) (sp: block) (ofs: Z) : Prop :=
+  exists id, exists b, exists lv, exists delta,
+  e!id = Some(b, lv) /\ f b = Some(sp, delta) /\ delta <= ofs < delta + sizeof lv.
 
 Lemma is_reachable_dec:
-  forall f cenv e le m te sp lo hi ofs,
-  match_env f cenv e le m te sp lo hi ->
-  {is_reachable f m sp ofs} + {~is_reachable f m sp ofs}.
+  forall f e sp ofs, is_reachable f e sp ofs \/ ~is_reachable f e sp ofs.
 Proof.
-  intros.
-  set (P := fun (b: block) =>
-       match f b with
-       | None => False
-       | Some(b', delta) =>
-           b' = sp /\ Mem.low_bound m b + delta <= ofs < Mem.high_bound m b + delta
-       end).
-  assert ({forall b, Intv.In b (lo, hi) -> ~P b} + {exists b, Intv.In b (lo, hi) /\ P b}).
-  apply Intv.forall_dec. intro b. unfold P. 
-  destruct (f b) as [[b' delta] | ]. 
-  destruct (eq_block b' sp).
-  destruct (zle (Mem.low_bound m b + delta) ofs).
-  destruct (zlt ofs (Mem.high_bound m b + delta)).
-  right; auto.
-  left; intuition.
-  left; intuition.
-  left; intuition.
-  left; intuition.
-  inv H. destruct H0.
-  right; red; intros [b [delta [A [B C]]]].
-  elim (n b). 
-  exploit me_inv0; eauto. intros [id [lv D]]. exploit me_bounded0; eauto. 
-  red. rewrite A. auto. 
-  left. destruct e0 as [b [A B]]. red in B; revert B.
-  case_eq (f b). intros [b' delta] EQ [C [D E]]. subst b'. 
-  exists b; exists delta. auto. 
-  tauto. 
+  intros. 
+  set (pred := fun id_b_lv : ident * (block * var_kind) =>
+                 match id_b_lv with
+                 | (id, (b, lv)) =>
+                      match f b with
+                           | None => false
+                           | Some(sp', delta) =>
+                               if eq_block sp sp'
+                               then zle delta ofs && zlt ofs (delta + sizeof lv)
+                               else false
+                      end
+                 end).
+  destruct (List.existsb pred (PTree.elements e)) as []_eqn.
+  rewrite List.existsb_exists in Heqb. 
+  destruct Heqb as [[id [b lv]] [A B]].
+  simpl in B. destruct (f b) as [[sp' delta] |]_eqn; try discriminate.
+  destruct (eq_block sp sp'); try discriminate.
+  destruct (andb_prop _ _ B). 
+  left; red. exists id; exists b; exists lv; exists delta.
+  split. apply PTree.elements_complete; auto. 
+  split. congruence.
+  split; eapply proj_sumbool_true; eauto.
+  right; red. intros [id [b [lv [delta [A [B C]]]]]].
+  assert (existsb pred (PTree.elements e) = true).
+  rewrite List.existsb_exists. exists (id, (b, lv)); split.
+  apply PTree.elements_correct; auto. 
+  simpl. rewrite B. rewrite dec_eq_true.
+  unfold proj_sumbool. destruct C. rewrite zle_true; auto. rewrite zlt_true; auto. 
+  congruence.
 Qed.
 
 (** Preservation of [match_callstack] by external calls. *)
@@ -1106,14 +1079,14 @@ Lemma match_callstack_external_call:
   mem_unchanged_on (loc_out_of_reach f1 m1) m1' m2' ->
   inject_incr f1 f2 ->
   inject_separated f1 f2 m1 m1' ->
-  (forall b, Mem.valid_block m1 b -> Mem.bounds m2 b = Mem.bounds m1 b) ->
+  (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
   forall cs bound tbound,
   match_callstack f1 m1 m1' cs bound tbound ->
   bound <= Mem.nextblock m1 -> tbound <= Mem.nextblock m1' ->
   match_callstack f2 m2 m2' cs bound tbound.
 Proof.
   intros until m2'. 
-  intros UNMAPPED OUTOFREACH INCR SEPARATED BOUNDS.
+  intros UNMAPPED OUTOFREACH INCR SEPARATED MAXPERMS.
   destruct OUTOFREACH as [OUTOFREACH1 OUTOFREACH2].
   induction 1; intros.
 (* base case *)
@@ -1127,18 +1100,16 @@ Proof.
   eapply match_env_external_call; eauto. omega. omega. 
   (* padding-freeable *)
   red; intros.
-  destruct (is_reachable_dec _ _ _ _ _ _ _ _ _ ofs MENV).
-  destruct i as [b [delta [A B]]].
-  right; exists b; exists delta; split.
-  apply INCR; auto. rewrite BOUNDS. auto. 
-  exploit me_inv; eauto. intros [id [lv C]].
-  exploit me_bounded; eauto. intros. red; omega.
+  destruct (is_reachable_dec f1 e sp ofs).
+  destruct H3 as [id [b [lv [delta [A [B C]]]]]].
+  right; exists id; exists b; exists lv; exists delta.
+  split. auto. split. apply INCR; auto. auto.
   exploit PERM; eauto. intros [A|A]; try contradiction. left.
-  apply OUTOFREACH1; auto. red; intros. 
-  assert ((ofs < Mem.low_bound m1 b0 + delta \/ ofs >= Mem.high_bound m1 b0 + delta)
-          \/ Mem.low_bound m1 b0 + delta <= ofs < Mem.high_bound m1 b0 + delta)
-  by omega. destruct H4; auto.
-  elim n. exists b0; exists delta; auto.
+  apply OUTOFREACH1; auto. red; intros.
+  red; intros; elim H3.
+  exploit me_inv; eauto. intros [id [lv B]].
+  exploit me_bounds; eauto. intros C.
+  red. exists id; exists b0; exists lv; exists delta. intuition omega. 
   (* induction *)
   eapply IHmatch_callstack; eauto. inv MENV; omega. omega.
 Qed.
@@ -2091,7 +2062,7 @@ Proof.
   split. auto.
   split. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
   eapply match_callstack_external_call; eauto.
-  intros. eapply external_call_bounds; eauto.
+  intros. eapply external_call_max_perm; eauto.
   omega. omega.
   eapply external_call_nextblock_incr; eauto.
   eapply external_call_nextblock_incr; eauto.
@@ -2189,8 +2160,9 @@ Lemma match_callstack_alloc_variable:
   forall atk id lv cenv sz cenv' sz' tm sp e tf m m' b te le lo cs f tv,
   assign_variable atk (id, lv) (cenv, sz) = (cenv', sz') ->
   Mem.valid_block tm sp ->
-  Mem.bounds tm sp = (0, tf.(fn_stackspace)) ->
-  Mem.range_perm tm sp 0 tf.(fn_stackspace) Freeable ->
+  (forall ofs k p,
+    Mem.perm tm sp ofs k p -> 0 <= ofs < tf.(fn_stackspace)) ->
+  Mem.range_perm tm sp 0 tf.(fn_stackspace) Cur Freeable ->
   tf.(fn_stackspace) <= Int.max_unsigned ->
   Mem.alloc m 0 (sizeof lv) = (m', b) ->
   match_callstack f m tm 
@@ -2198,7 +2170,8 @@ Lemma match_callstack_alloc_variable:
                   (Mem.nextblock m) (Mem.nextblock tm) ->
   Mem.inject f m tm ->
   0 <= sz -> sz' <= tf.(fn_stackspace) ->
-  (forall b delta, f b = Some(sp, delta) -> Mem.high_bound m b + delta <= sz) ->
+  (forall b delta ofs k p,
+     f b = Some(sp, delta) -> Mem.perm m b ofs k p -> ofs + delta < sz) ->
   e!id = None ->
   te!(for_var id) = Some tv ->
   exists f',
@@ -2207,8 +2180,8 @@ Lemma match_callstack_alloc_variable:
   /\ match_callstack f' m' tm
                      (Frame cenv' tf (PTree.set id (b, lv) e) le te sp lo (Mem.nextblock m') :: cs)
                      (Mem.nextblock m') (Mem.nextblock tm)
-  /\ (forall b delta,
-      f' b = Some(sp, delta) -> Mem.high_bound m' b + delta <= sz').
+  /\ (forall b delta ofs k p,
+      f' b = Some(sp, delta) -> Mem.perm m' b ofs k p -> ofs + delta < sz').
 Proof.
   intros until tv. intros ASV VALID BOUNDS PERMS NOOV ALLOC MCS INJ LO HI RANGE E TE.
   generalize ASV. unfold assign_variable. 
@@ -2222,23 +2195,22 @@ Proof.
     generalize (align_le sz (size_chunk chunk) SIZEPOS). fold ofs. intro SZOFS.
     exploit Mem.alloc_left_mapped_inject.
       eauto. eauto. eauto. 
-      instantiate (1 := ofs). omega. 
-      right; rewrite BOUNDS; simpl. omega.
-      intros. apply Mem.perm_implies with Freeable; auto with mem.
+      instantiate (1 := ofs). omega.
+      intros. exploit BOUNDS; eauto. omega. 
+      intros. apply Mem.perm_implies with Freeable; auto with mem. apply Mem.perm_cur. 
       apply PERMS. rewrite LV in H1. simpl in H1. omega.
       rewrite LV; simpl. rewrite Zminus_0_r. unfold ofs. 
       apply inj_offset_aligned_var.
-      intros. generalize (RANGE _ _ H1). omega. 
+      intros. generalize (RANGE _ _ _ _ _ H1 H2). omega. 
     intros [f1 [MINJ1 [INCR1 [SAME OTHER]]]].
     exists f1; split. auto. split. auto. split. 
     eapply match_callstack_alloc_left; eauto.
     rewrite <- LV; auto. 
     rewrite SAME; constructor.
-    intros. rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). 
-    destruct (eq_block b0 b); simpl.
+    intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b0 b).
     subst b0. assert (delta = ofs) by congruence. subst delta.  
     rewrite LV. simpl. omega.
-    rewrite OTHER in H1; eauto. generalize (RANGE _ _ H1). omega. 
+    intro. rewrite OTHER in H1; eauto. generalize (RANGE _ _ _ _ _ H1 H3). omega. 
   (* 1.2 info = Var_local chunk *)
     intro EQ; injection EQ; intros; clear EQ. subst sz'. rewrite <- H0.
     exploit Mem.alloc_left_unmapped_inject; eauto.
@@ -2247,8 +2219,7 @@ Proof.
     eapply match_callstack_alloc_left; eauto. 
     rewrite <- LV; auto.
     rewrite SAME; constructor.
-    intros. rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). 
-    destruct (eq_block b0 b); simpl.
+    intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b0 b).
     subst b0. congruence.
     rewrite OTHER in H; eauto.
   (* 2 info = Var_stack_array ofs *)
@@ -2259,29 +2230,29 @@ Proof.
   exploit Mem.alloc_left_mapped_inject. eauto. eauto. eauto. 
     instantiate (1 := ofs). 
     generalize Int.min_signed_neg. omega.
-    right; rewrite BOUNDS; simpl. generalize Int.min_signed_neg. omega.
-    intros. apply Mem.perm_implies with Freeable; auto with mem.
+    intros. exploit BOUNDS; eauto. generalize Int.min_signed_neg. omega.
+    intros. apply Mem.perm_implies with Freeable; auto with mem. apply Mem.perm_cur.
     apply PERMS. rewrite LV in H3. simpl in H3. omega.
     rewrite LV; simpl. rewrite Zminus_0_r. unfold ofs. 
     apply inj_offset_aligned_array'.
-    intros. generalize (RANGE _ _ H3). omega. 
+    intros. generalize (RANGE _ _ _ _ _ H3 H4). omega. 
   intros [f1 [MINJ1 [INCR1 [SAME OTHER]]]].
   exists f1; split. auto. split. auto. split. 
   subst cenv'. eapply match_callstack_alloc_left; eauto.
   rewrite <- LV; auto. 
   rewrite SAME; constructor.
-  intros. rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). 
-  destruct (eq_block b0 b); simpl.
+  intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b0 b).
   subst b0. assert (delta = ofs) by congruence. subst delta. 
   rewrite LV. simpl. omega.
-  rewrite OTHER in H3; eauto. generalize (RANGE _ _ H3). omega. 
+  intro. rewrite OTHER in H3; eauto. generalize (RANGE _ _ _ _ _ H3 H5). omega. 
 Qed.
 
 Lemma match_callstack_alloc_variables_rec:
   forall tm sp cenv' tf le te lo cs atk,
   Mem.valid_block tm sp ->
-  Mem.bounds tm sp = (0, tf.(fn_stackspace)) ->
-  Mem.range_perm tm sp 0 tf.(fn_stackspace) Freeable ->
+  (forall ofs k p,
+    Mem.perm tm sp ofs k p -> 0 <= ofs < tf.(fn_stackspace)) ->
+  Mem.range_perm tm sp 0 tf.(fn_stackspace) Cur Freeable ->
   tf.(fn_stackspace) <= Int.max_unsigned ->
   forall e m vars e' m',
   alloc_variables e m vars e' m' ->
@@ -2292,8 +2263,8 @@ Lemma match_callstack_alloc_variables_rec:
                   (Mem.nextblock m) (Mem.nextblock tm) ->
   Mem.inject f m tm ->
   0 <= sz ->
-  (forall b delta,
-     f b = Some(sp, delta) -> Mem.high_bound m b + delta <= sz) ->
+  (forall b delta ofs k p,
+     f b = Some(sp, delta) -> Mem.perm m b ofs k p -> ofs + delta < sz) ->
   (forall id lv, In (id, lv) vars -> te!(for_var id) <> None) ->
   list_norepet (List.map (@fst ident var_kind) vars) ->
   (forall id lv, In (id, lv) vars -> e!id = None) ->
@@ -2395,8 +2366,7 @@ Proof.
   intros. 
   unfold build_compilenv in H. 
   eapply match_callstack_alloc_variables_rec; eauto with mem.
-  eapply Mem.bounds_alloc_same; eauto.
-  red; intros; eauto with mem.
+  red; intros. eapply Mem.perm_alloc_2; eauto. 
   eapply match_callstack_alloc_right; eauto.
   eapply Mem.alloc_right_inject; eauto. omega. 
   intros. elim (Mem.valid_not_valid_diff tm sp sp); eauto with mem.
@@ -3257,7 +3227,7 @@ Proof.
                  (Mem.nextblock m') (Mem.nextblock tm')).
     apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
     eapply match_callstack_external_call; eauto.
-    intros. eapply external_call_bounds; eauto.
+    intros. eapply external_call_max_perm; eauto.
     omega. omega. 
     eapply external_call_nextblock_incr; eauto.
     eapply external_call_nextblock_incr; eauto.
@@ -3414,7 +3384,7 @@ Opaque PTree.set.
   econstructor; eauto.
   apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
   eapply match_callstack_external_call; eauto.
-  intros. eapply external_call_bounds; eauto.
+  intros. eapply external_call_max_perm; eauto.
   omega. omega.
   eapply external_call_nextblock_incr; eauto.
   eapply external_call_nextblock_incr; eauto.
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 627db89..37f15cf 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -327,8 +327,8 @@ Qed.
 Lemma mem_empty_not_valid_pointer:
   forall b ofs, Mem.valid_pointer Mem.empty b ofs = false.
 Proof.
-  intros. unfold Mem.valid_pointer. destruct (Mem.perm_dec Mem.empty b ofs Nonempty); auto.
-  red in p. simpl in p. contradiction.
+  intros. unfold Mem.valid_pointer. destruct (Mem.perm_dec Mem.empty b ofs Cur Nonempty); auto.
+  eelim Mem.perm_empty; eauto. 
 Qed.
 
 Lemma sem_cmp_match: