From f774d5f2d604f747e72e2d3bb56cc3f90090e2dd Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 15 Feb 2013 16:24:13 +0000
Subject: Pointers one past

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 Changelog                     |   4 +-
 arm/Asmgen.v                  |   8 +-
 arm/Asmgenproof.v             |   4 +-
 arm/Asmgenproof1.v            |  16 ++--
 arm/Op.v                      | 123 +++++++++++-------------------
 backend/Inlining.v            |   2 +-
 backend/Inliningproof.v       |  10 +--
 backend/Inliningspec.v        |   4 +-
 backend/Reloadtyping.v        |   5 +-
 cfrontend/Cminorgenproof.v    |  41 ++++++----
 cfrontend/Cop.v               |  29 +++----
 cfrontend/Cshmgenproof.v      |   3 +-
 cfrontend/Initializersproof.v |  15 +++-
 cfrontend/SimplLocalsproof.v  |  45 ++++++-----
 common/Events.v               |   6 +-
 common/Memory.v               | 173 ++++++++++++++++++++++++++++++++----------
 common/Memtype.v              |  53 +++++++++++--
 common/Values.v               | 167 +++++++++++++++++++++++++++++++++++-----
 ia32/Asmgenproof1.v           |   9 ++-
 ia32/Op.v                     |  88 +++++++++------------
 powerpc/Op.v                  |  84 +++++++++-----------
 21 files changed, 565 insertions(+), 324 deletions(-)

diff --git a/Changelog b/Changelog
index 81429ef..243cdff 100644
--- a/Changelog
+++ b/Changelog
@@ -7,7 +7,9 @@ Development version
   reductions to be incorrectly merged.
 - Better error and warning messages for declarations of variables
   of size >= 2^32 bits.
-
+- Comparisons involving pointers "one past" the end of a block are
+  now defined.  (They used to be undefined behavior.)
+  (Contributed by Robbert Krebbers).
 
 Release 1.12.1, 2013-01-29
 ==========================
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index b78dfb6..05e7010 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -57,9 +57,9 @@ Definition is_immed_mem_float (x: int) : bool :=
 Fixpoint decompose_int_rec (N: nat) (n p: int) : list int :=
   match N with
   | Datatypes.O =>
-      if Int.eq_dec n Int.zero then nil else n :: nil
+      if Int.eq n Int.zero then nil else n :: nil
   | Datatypes.S M =>
-      if Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero then
+      if Int.eq (Int.and n (Int.shl (Int.repr 3) p)) Int.zero then
         decompose_int_rec M n (Int.add p (Int.repr 2))
       else
         let m := Int.shl (Int.repr 255) p in
@@ -86,14 +86,14 @@ Definition iterate_op (op1 op2: shift_op -> instruction) (l: list int) (k: code)
 Definition loadimm (r: ireg) (n: int) (k: code) :=
   let d1 := decompose_int n in
   let d2 := decompose_int (Int.not n) in
-  if le_dec (List.length d1) (List.length d2)
+  if NPeano.leb (List.length d1) (List.length d2)
   then iterate_op (Pmov r) (Porr r r) d1 k
   else iterate_op (Pmvn r) (Pbic r r) d2 k.
 
 Definition addimm (r1 r2: ireg) (n: int) (k: code) :=
   let d1 := decompose_int n in
   let d2 := decompose_int (Int.neg n) in
-  if le_dec (List.length d1) (List.length d2)
+  if NPeano.leb (List.length d1) (List.length d2)
   then iterate_op (Padd r1 r2) (Padd r1 r1) d1 k
   else iterate_op (Psub r1 r2) (Psub r1 r1) d2 k.
 
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index b0598e9..365917c 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -348,7 +348,7 @@ Remark loadimm_label:
   forall r n k, find_label lbl (loadimm r n k) = find_label lbl k.
 Proof.
   intros. unfold loadimm.
-  destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n))));
+  destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.not n))));
   auto with labels.
 Qed.
 Hint Rewrite loadimm_label: labels.
@@ -357,7 +357,7 @@ Remark addimm_label:
   forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k.
 Proof.
   intros; unfold addimm.
-  destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n))));
+  destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n))));
   auto with labels.
 Qed.
 Hint Rewrite addimm_label: labels.
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 19edcd9..658fc98 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -480,10 +480,10 @@ Lemma decompose_int_rec_or:
   forall N n p x, List.fold_left Int.or (decompose_int_rec N n p) x = Int.or x n.
 Proof.
   induction N; intros; simpl.
-  destruct (Int.eq_dec n Int.zero); simpl. 
+  predSpec Int.eq Int.eq_spec n Int.zero; simpl.
   subst n. rewrite Int.or_zero. auto.
   auto.
-  destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+  predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero.
   auto.
   simpl. rewrite IHN. rewrite Int.or_assoc. decEq. rewrite <- Int.and_or_distrib.
   rewrite Int.or_not_self. apply Int.and_mone.
@@ -493,10 +493,10 @@ Lemma decompose_int_rec_xor:
   forall N n p x, List.fold_left Int.xor (decompose_int_rec N n p) x = Int.xor x n.
 Proof.
   induction N; intros; simpl.
-  destruct (Int.eq_dec n Int.zero); simpl. 
+  predSpec Int.eq Int.eq_spec n Int.zero; simpl.
   subst n. rewrite Int.xor_zero. auto.
   auto.
-  destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+  predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero.
   auto.
   simpl. rewrite IHN. rewrite Int.xor_assoc. decEq. rewrite <- Int.and_xor_distrib.
   rewrite Int.xor_not_self. apply Int.and_mone.
@@ -506,10 +506,10 @@ Lemma decompose_int_rec_add:
   forall N n p x, List.fold_left Int.add (decompose_int_rec N n p) x = Int.add x n.
 Proof.
   induction N; intros; simpl.
-  destruct (Int.eq_dec n Int.zero); simpl. 
+  predSpec Int.eq Int.eq_spec n Int.zero; simpl.
   subst n. rewrite Int.add_zero. auto.
   auto.
-  destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+  predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero.
   auto.
   simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and. 
   rewrite Int.or_not_self. apply Int.and_mone. apply Int.and_not_self.
@@ -647,7 +647,7 @@ Lemma loadimm_correct:
   /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
   intros. unfold loadimm.
-  destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n)))).
+  destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.not n)))).
   (* mov - orr* *)
   replace (Vint n) with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) Vzero).
   apply iterate_op_correct.
@@ -672,7 +672,7 @@ Lemma addimm_correct:
   /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
   intros. unfold addimm.
-  destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n)))).
+  destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))).
   (* add - add* *)
   replace (Val.add (rs r2) (Vint n))
      with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (rs r2)).
diff --git a/arm/Op.v b/arm/Op.v
index f26bccc..291d64f 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -697,10 +697,16 @@ Hypothesis valid_pointer_inj:
   Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
 
-Hypothesis valid_pointer_no_overflow:
+Hypothesis weak_valid_pointer_inj:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_pointer_no_overflow:
+  forall b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 
 Hypothesis valid_different_pointers_inj:
@@ -728,25 +734,6 @@ Ltac InvInject :=
   | _ => idtac
   end.
 
-Remark val_add_inj:
-  forall v1 v1' v2 v2',
-  val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.add v1 v2) (Val.add v1' v2').
-Proof.
-  intros. inv H; inv H0; simpl; econstructor; eauto. 
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-Qed.
-
-Remark val_sub_inj:
-  forall v1 v1' v2 v2',
-  val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.sub v1 v2) (Val.sub v1' v2').
-Proof.
-  intros. inv H; inv H0; simpl; auto.
-  econstructor; eauto. rewrite Int.sub_add_l. auto.
-  destruct (zeq b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite zeq_true. 
-  rewrite Int.sub_shifted. auto.
-Qed.
-
 Remark eval_shift_inj:
   forall s v v', val_inject f v v' -> val_inject f (eval_shift s v) (eval_shift s v').
 Proof.
@@ -759,45 +746,13 @@ Lemma eval_condition_inj:
   eval_condition cond vl1 m1 = Some b ->
   eval_condition cond vl2 m2 = Some b.
 Proof.
-Opaque Int.add.
-  assert (CMP:
-    forall c v1 v2 v1' v2' b,
-    val_inject f v1 v1' ->
-    val_inject f v2 v2' ->
-    Val.cmp_bool c v1 v2 = Some b ->
-    Val.cmp_bool c v1' v2' = Some b).
-  intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
-
-  assert (CMPU:
-    forall c v1 v2 v1' v2' b,
-    val_inject f v1 v1' ->
-    val_inject f v2 v2' ->
-    Val.cmpu_bool (Mem.valid_pointer m1) c v1 v2 = Some b ->
-    Val.cmpu_bool (Mem.valid_pointer m2) c v1' v2' = Some b).
-  intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
-  destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
-  destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
-  rewrite (valid_pointer_inj _ H2 Heqb4).
-  rewrite (valid_pointer_inj _ H Heqb0). simpl.
-  destruct (zeq b1 b0); simpl in H1.
-  inv H1. rewrite H in H2; inv H2. rewrite zeq_true. 
-  decEq. apply Int.translate_cmpu.
-  eapply valid_pointer_no_overflow; eauto.
-  eapply valid_pointer_no_overflow; eauto.
-  exploit valid_different_pointers_inj; eauto. intros P.
-  destruct (zeq b2 b3); auto.
-  destruct P. congruence. 
-  destruct c; simpl in H1; inv H1.
-  simpl; decEq. rewrite Int.eq_false; auto. congruence.
-  simpl; decEq. rewrite Int.eq_false; auto. congruence.
-
   intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl.
-  eapply CMP; eauto.
-  eapply CMPU; eauto.
-  eapply CMP. eauto. eapply eval_shift_inj. eauto. auto.
-  eapply CMPU. eauto. eapply eval_shift_inj. eauto. auto.
-  eapply CMP; try eassumption; eauto.
-  eapply CMPU; try eassumption; eauto.
+  eauto 4 using val_cmp_bool_inject.
+  eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
+  eauto using val_cmp_bool_inject, eval_shift_inj.
+  eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies, eval_shift_inj.
+  eauto 4 using val_cmp_bool_inject.
+  eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; simpl in H0; inv H0; auto.
@@ -819,15 +774,15 @@ Lemma eval_operation_inj:
   exists v2, eval_operation genv sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2.
 Proof.
   intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto. apply eval_shift_inj; auto.
-  apply val_add_inj; auto.
+  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto. apply eval_shift_inj; auto.
+  apply Values.val_add_inject; auto.
 
-  apply val_sub_inj; auto.
-  apply val_sub_inj; auto. apply eval_shift_inj; auto.
-  apply val_sub_inj; auto. apply eval_shift_inj; auto.
-  apply (@val_sub_inj (Vint i) (Vint i) v v'); auto.
+  apply Values.val_sub_inject; auto.
+  apply Values.val_sub_inject; auto. apply eval_shift_inj; auto.
+  apply Values.val_sub_inject; auto. apply eval_shift_inj; auto.
+  apply (@Values.val_sub_inject f (Vint i) (Vint i) v v'); auto.
 
   inv H4; inv H2; simpl; auto.
   inv H4; inv H3; simpl in H1; inv H1. simpl. 
@@ -888,10 +843,10 @@ Proof.
             val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs)).
   exact symbol_address_inj.
   intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto. apply eval_shift_inj; auto.
-  apply val_add_inj; auto.
+  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto. apply eval_shift_inj; auto.
+  apply Values.val_add_inject; auto.
 Qed.
 
 End EVAL_COMPAT.
@@ -913,10 +868,20 @@ Proof.
   intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. 
 Qed.
 
-Remark valid_pointer_no_overflow_extends:
+Remark weak_valid_pointer_extends:
+  forall m1 m2, Mem.extends m1 m2 ->
+  forall b1 ofs b2 delta,
+  Some(b1, 0) = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+Proof.
+  intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto.
+Qed.
+
+Remark weak_valid_pointer_no_overflow_extends:
   forall m1 b1 ofs b2 delta,
   Some(b1, 0) = Some(b2, delta) ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 Proof.
   intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2.
@@ -944,7 +909,8 @@ Lemma eval_condition_lessdef:
 Proof.
   intros. eapply eval_condition_inj with (f := fun b => Some(b, 0)) (m1 := m1).
   apply valid_pointer_extends; auto.
-  apply valid_pointer_no_overflow_extends; auto. 
+  apply weak_valid_pointer_extends; auto.
+  apply weak_valid_pointer_no_overflow_extends.
   apply valid_different_pointers_extends; auto.
   rewrite <- val_list_inject_lessdef. eauto. auto.
 Qed.
@@ -963,7 +929,8 @@ Proof.
   eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
   intros. rewrite <- val_inject_lessdef; auto.
   apply valid_pointer_extends; auto.
-  apply valid_pointer_no_overflow_extends; auto. 
+  apply weak_valid_pointer_extends; auto.
+  apply weak_valid_pointer_no_overflow_extends.
   apply valid_different_pointers_extends; auto.
   rewrite <- val_inject_lessdef; auto.
   eauto. auto. 
@@ -1019,7 +986,8 @@ Lemma eval_condition_inject:
 Proof.
   intros. eapply eval_condition_inj with (f := f) (m1 := m1); eauto.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
-  intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
 Qed.
 
@@ -1051,7 +1019,8 @@ Proof.
   eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
   exact symbol_address_inject.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
-  intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
 Qed.
 
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 5075fd6..a9b1e7e 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -454,7 +454,7 @@ Local Open Scope string_scope.
 
 Definition transf_function (fenv: funenv) (f: function) : Errors.res function :=
   let '(R ctx s _) := expand_function fenv f initstate in
-  if zle s.(st_stksize) Int.max_unsigned then
+  if zlt s.(st_stksize) Int.max_unsigned then
     OK (mkfunction f.(fn_sig) 
                    (sregs ctx f.(fn_params))
                    s.(st_stksize)
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 9536141..ba61ed0 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -398,7 +398,7 @@ Inductive match_stacks (F: meminj) (m m': mem):
         (AG: agree_regs F ctx rs rs')
         (SP: F sp = Some(sp', ctx.(dstk)))
         (PRIV: range_private F m m' sp' (ctx.(dstk) + ctx.(mstk)) f'.(fn_stacksize))
-        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
         (RES: Ple res ctx.(mreg))
         (BELOW: sp' < bound),
@@ -409,7 +409,7 @@ Inductive match_stacks (F: meminj) (m m': mem):
   | match_stacks_untailcall: forall stk res f' sp' rpc rs' stk' bound ctx
         (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs')
         (PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize))
-        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
         (RET: ctx.(retinfo) = Some (rpc, res))
         (BELOW: sp' < bound),
@@ -775,7 +775,7 @@ Inductive match_states: state -> state -> Prop :=
         (MINJ: Mem.inject F m m')
         (VB: Mem.valid_block m' sp')
         (PRIV: range_private F m m' sp' (ctx.(dstk) + ctx.(mstk)) f'.(fn_stacksize))
-        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)),
       match_states (State stk f (Vptr sp Int.zero) pc rs m)
                    (State stk' f' (Vptr sp' Int.zero) (spc ctx pc) rs' m')
@@ -796,7 +796,7 @@ Inductive match_states: state -> state -> Prop :=
         (MINJ: Mem.inject F m m')
         (VB: Mem.valid_block m' sp')
         (PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize))
-        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)),
       match_states (Callstate stk (Internal f) vargs m)
                    (State stk' f' (Vptr sp' Int.zero) pc' rs' m')
@@ -814,7 +814,7 @@ Inductive match_states: state -> state -> Prop :=
         (MINJ: Mem.inject F m m')
         (VB: Mem.valid_block m' sp')
         (PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize))
-        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)),
       match_states (Returnstate stk v m)
                    (State stk' f' (Vptr sp' Int.zero) pc' rs' m').
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index 06826c2..82ef9cf 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -664,7 +664,7 @@ Inductive tr_function: function -> function -> Prop :=
       f'.(fn_sig) = f.(fn_sig) ->
       f'.(fn_params) = sregs ctx f.(fn_params) ->
       f'.(fn_entrypoint) = spc ctx f.(fn_entrypoint) ->
-      0 <= fn_stacksize f' <= Int.max_unsigned ->
+      0 <= fn_stacksize f' < Int.max_unsigned ->
       tr_function f f'.
 
 Lemma transf_function_spec:
@@ -672,7 +672,7 @@ Lemma transf_function_spec:
 Proof.
   intros. unfold transf_function in H.
   destruct (expand_function fenv f initstate) as [ctx s i] eqn:?. 
-  destruct (zle (st_stksize s) Int.max_unsigned); inv H.
+  destruct (zlt (st_stksize s) Int.max_unsigned); inv H.
   monadInv Heqr. set (ctx := initcontext x x0 (max_def_function f) (fn_stacksize f)) in *.
 Opaque initstate.
   destruct INCR3. inversion EQ1. inversion EQ.
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index 9f5563c..c005139 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -288,8 +288,7 @@ Proof.
     rewrite loc_arguments_type; auto.
   destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty. 
   auto 10 with reloadty.
-
-  destruct (ef_reloads ef) as [] eqn:?.
+  destruct (ef_reloads ef) eqn:?.
   assert (arity_ok (sig_args (ef_sig ef)) = true) by intuition congruence.
   assert (map mreg_type (regs_for args) = map Loc.type args).
     apply wt_regs_for. apply arity_ok_enough. congruence.
@@ -297,8 +296,6 @@ Proof.
   auto 10 with reloadty.
   auto with reloadty.
 
-
-
   assert (map mreg_type (regs_for args) = map Loc.type args).
     eauto with reloadty.
   auto with reloadty.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 9bbf040..a61808a 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1573,26 +1573,37 @@ Proof.
     apply val_inject_val_of_optbool.
     apply val_inject_val_of_optbool.
 Opaque Int.add.
-    unfold Val.cmpu. simpl. 
-    destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; simpl; auto.
-    destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; simpl; auto.
-    exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb. econstructor; eauto. 
-    intros V1. rewrite V1.
-    exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb0. econstructor; eauto. 
-    intros V2. rewrite V2. simpl.
-    destruct (zeq b1 b0).
+    unfold Val.cmpu. simpl.
+    destruct (zeq b1 b0); subst.
     (* same blocks *)
-    subst b1. rewrite H in H0; inv H0. rewrite zeq_true. 
-    rewrite Int.translate_cmpu. apply val_inject_val_of_optbool.
-    eapply Mem.valid_pointer_inject_no_overflow; eauto.
-    eapply Mem.valid_pointer_inject_no_overflow; eauto.
+    rewrite H0 in H. inv H. rewrite zeq_true.
+    fold (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)).
+    fold (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)).
+    fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+    fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs0 (Int.repr delta)))).
+    destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)) eqn:?; auto.
+    destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; auto.
+    rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb) by eauto.
+    rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0) by eauto.
+    rewrite Int.translate_cmpu
+      by eauto using Mem.weak_valid_pointer_inject_no_overflow.
+    apply val_inject_val_of_optbool.
     (* different source blocks *)
+    destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; auto.
+    destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; auto.
     destruct (zeq b2 b3).
-    exploit Mem.different_pointers_inject; eauto. intros [A|A]. 
-    congruence.
-    destruct c; simpl; auto. 
+    fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+    fold (Mem.weak_valid_pointer tm b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))).
+    rewrite Mem.valid_pointer_implies
+      by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb); eauto).
+    rewrite Mem.valid_pointer_implies
+      by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0); eauto).
+    exploit Mem.different_pointers_inject; eauto. intros [A|A]; [congruence |].
+    destruct c; simpl; auto.
     rewrite Int.eq_false. constructor. congruence.
     rewrite Int.eq_false. constructor. congruence.
+    rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb) by eauto.
+    rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0) by eauto.
     apply val_inject_val_of_optbool.
   (* cmpf *)
   inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 9d581b6..af7aaa8 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -714,13 +714,6 @@ Definition classify_cmp (ty1: type) (ty2: type) :=
   | _ , _ => cmp_default
   end.
 
-Function sem_cmp_mismatch (c: comparison): option val :=
-  match c with
-  | Ceq =>  Some Vfalse
-  | Cne =>  Some Vtrue
-  | _   => None
-  end.
-
 Function sem_cmp (c:comparison)
                   (v1: val) (t1: type) (v2: val) (t2: type)
                   (m: mem): option val :=
@@ -739,16 +732,24 @@ Function sem_cmp (c:comparison)
       match v1,v2 with
       | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
       | Vptr b1 ofs1,  Vptr b2 ofs2  =>
-          if Mem.valid_pointer m b1 (Int.unsigned ofs1)
-          && Mem.valid_pointer m b2 (Int.unsigned ofs2) then
-            if zeq b1 b2
+          if zeq b1 b2 then
+            if Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)
+               && Mem.weak_valid_pointer m b2 (Int.unsigned ofs2)
             then Some (Val.of_bool (Int.cmpu c ofs1 ofs2))
-            else sem_cmp_mismatch c
-          else None
+            else None
+          else
+            if Mem.valid_pointer m b1 (Int.unsigned ofs1)
+               && Mem.valid_pointer m b2 (Int.unsigned ofs2)
+            then option_map Val.of_bool (Val.cmp_different_blocks c)
+            else None
       | Vptr b ofs, Vint n =>
-          if Int.eq n Int.zero then sem_cmp_mismatch c else None
+          if Int.eq n Int.zero
+          then option_map Val.of_bool (Val.cmp_different_blocks c)
+          else None
       | Vint n, Vptr b ofs =>
-          if Int.eq n Int.zero then sem_cmp_mismatch c else None
+          if Int.eq n Int.zero
+          then option_map Val.of_bool (Val.cmp_different_blocks c)
+          else None
       | _,  _ => None
       end
   | cmp_case_ff =>
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 74a6da5..ad5ada6 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -574,7 +574,8 @@ Proof.
   inversion H8. eauto with cshm.
   (* pp ptr ptr *)
   inversion H10. eapply eval_Ebinop; eauto with cshm.
-  simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9. auto.
+  simpl. unfold Val.cmpu. simpl. unfold Mem.weak_valid_pointer in *. 
+  rewrite H3. rewrite H9. auto.
   inversion H10. eapply eval_Ebinop; eauto with cshm.
   simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9.
   destruct cmp; simpl in *; inv H; auto.
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index ca9c5b0..b64c309 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -380,6 +380,13 @@ Proof.
   eelim Mem.perm_empty; eauto. 
 Qed.
 
+Lemma mem_empty_not_weak_valid_pointer:
+  forall b ofs, Mem.weak_valid_pointer Mem.empty b ofs = false.
+Proof.
+  intros. unfold Mem.weak_valid_pointer.
+  now rewrite !mem_empty_not_valid_pointer.
+Qed.
+
 Lemma sem_cmp_match:
   forall c v1 ty1 v2 ty2 m v v1' v2' v',
   sem_cmp c v1 ty1 v2 ty2 Mem.empty = Some v ->
@@ -391,10 +398,12 @@ Opaque zeq.
   intros. unfold sem_cmp in *.
   destruct (classify_cmp ty1 ty2); try (destruct s); inv H1; inv H2; inv H; inv H0; auto with mval.
   destruct (Int.eq n Int.zero); try discriminate. 
-  unfold sem_cmp_mismatch in *. destruct c; inv H3; inv H2; constructor.
+  unfold Val.cmp_different_blocks in *. destruct c; inv H3; inv H2; constructor.
   destruct (Int.eq n Int.zero); try discriminate. 
-  unfold sem_cmp_mismatch in *. destruct c; inv H2; inv H1; constructor.
-  rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. discriminate.
+  unfold Val.cmp_different_blocks in *. destruct c; inv H2; inv H1; constructor.
+  rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4.
+  rewrite (mem_empty_not_weak_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. simpl in H4.
+  destruct (zeq (Z.pos id) (Z.pos id0)); discriminate.
 Qed.
 
 Lemma sem_binary_match:
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index c496a5e..e3aa4e2 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -1006,8 +1006,8 @@ Proof.
     apply RPSRC. omega.
   assert (PDST: Mem.perm m bdst (Int.unsigned odst) Cur Nonempty).
     apply RPDST. omega.
-  exploit Mem.address_inject.  eauto. apply Mem.perm_cur_max. eexact PSRC. eauto. intros EQ1.
-  exploit Mem.address_inject.  eauto. apply Mem.perm_cur_max. eexact PDST. eauto. intros EQ2.
+  exploit Mem.address_inject.  eauto. eexact PSRC. eauto. intros EQ1.
+  exploit Mem.address_inject.  eauto. eexact PDST. eauto. intros EQ2.
   exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]].
   exploit Mem.storebytes_mapped_inject; eauto. intros [tm' [C D]].
   exists tm'. 
@@ -1372,35 +1372,44 @@ Lemma sem_cmp_inject:
   exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 tm = Some tv /\ val_inject f v tv.
 Proof.
   unfold sem_cmp; intros. 
-  assert (MM: sem_cmp_mismatch cmp = Some v ->
-              exists tv, sem_cmp_mismatch cmp = Some tv /\ val_inject f v tv).
+  assert (MM: option_map Val.of_bool (Val.cmp_different_blocks cmp) = Some v ->
+      exists tv, option_map Val.of_bool (Val.cmp_different_blocks cmp) = Some tv /\ val_inject f v tv).
     intros. exists v; split; auto. 
     destruct cmp; simpl in H2; inv H2; auto.
 
   destruct (classify_cmp ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject.
   destruct (Int.eq i Int.zero); try discriminate; auto.
   destruct (Int.eq i Int.zero); try discriminate; auto.
-  destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
-  destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
-  simpl in H3.
-  rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb).
-  rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0).
-  simpl.
-  destruct (zeq b1 b0).  subst b1. rewrite H0 in H2; inv H2. rewrite zeq_true.
-  replace  (Int.cmpu cmp (Int.add ofs1 (Int.repr delta))
+
+  destruct (zeq b1 b0); subst.
+  rewrite H0 in H2. inv H2. rewrite zeq_true.
+  destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)) eqn:?; try discriminate.
+  destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
+  simpl H3.
+  rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb) by eauto.
+  rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0) by eauto.
+  simpl. replace  (Int.cmpu cmp (Int.add ofs1 (Int.repr delta))
                          (Int.add ofs0 (Int.repr delta)))
      with  (Int.cmpu cmp ofs1 ofs0).
   inv H3; TrivialInject.
   symmetry. apply Int.translate_cmpu. 
-  eapply Mem.valid_pointer_inject_no_overflow; eauto.
-  eapply Mem.valid_pointer_inject_no_overflow; eauto.
-  destruct (zeq b2 b3).
-  exploit Mem.different_pointers_inject; eauto. intros [A|A]. contradiction.
+  eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
+  eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
+  destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
+  destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
+  destruct (zeq b2 b3); subst.
+  rewrite Mem.valid_pointer_implies
+    by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb); eauto).
+  rewrite Mem.valid_pointer_implies
+    by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0); eauto).
+  simpl.
+  exploit Mem.different_pointers_inject; eauto. intros [[]|A]. easy.
   destruct cmp; simpl in H3; inv H3.
   simpl. unfold Int.eq. rewrite zeq_false; auto.
   simpl. unfold Int.eq. rewrite zeq_false; auto.
-  auto.
-  econstructor; eauto. econstructor; eauto. 
+  rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb) by eauto.
+  rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0) by eauto.
+  simpl in H3 |- *. auto.
 Qed.
 
 Lemma sem_binary_operation_inject:
diff --git a/common/Events.v b/common/Events.v
index fd1acd0..3f81e60 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1229,7 +1229,7 @@ Proof.
   assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Cur Freeable).
     eapply Mem.free_range_perm; eauto.
   exploit Mem.address_inject; eauto. 
-    apply Mem.perm_implies with Freeable; auto with mem. apply Mem.perm_cur_max.
+    apply Mem.perm_implies with Freeable; auto with mem.
     apply H0. instantiate (1 := lo). omega. 
   intro EQ.
   assert (Mem.range_perm m1' b2 (Int.unsigned lo + delta - 4) (Int.unsigned lo + delta + Int.unsigned sz) Cur Freeable).
@@ -1357,8 +1357,8 @@ Proof.
     apply RPSRC. omega.
   assert (PDST: Mem.perm m1 bdst (Int.unsigned odst) Cur Nonempty).
     apply RPDST. omega.
-  exploit Mem.address_inject.  eauto. apply Mem.perm_cur_max. eexact PSRC. eauto. intros EQ1.
-  exploit Mem.address_inject.  eauto. apply Mem.perm_cur_max. eexact PDST. eauto. intros EQ2.
+  exploit Mem.address_inject.  eauto. eexact PSRC. eauto. intros EQ1.
+  exploit Mem.address_inject.  eauto. eexact PDST. eauto. intros EQ2.
   exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]].
   exploit Mem.storebytes_mapped_inject; eauto. intros [m2' [C D]].
   exists f; exists Vundef; exists m2'.
diff --git a/common/Memory.v b/common/Memory.v
index 514e1e0..04a3dda 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -287,9 +287,8 @@ Proof.
   right; red; intro V; inv V; contradiction.
 Qed.
 
-(** [valid_pointer] is a boolean-valued function that says whether
-    the byte at the given location is nonempty. *)
-
+(** [valid_pointer m b ofs] returns [true] if the address [b, ofs]
+  is nonempty in [m] and [false] if it is empty. *)
 Definition valid_pointer (m: mem) (b: block) (ofs: Z): bool :=
   perm_dec m b ofs Cur Nonempty.
 
@@ -313,6 +312,28 @@ Proof.
   destruct H. apply H. simpl. omega.
 Qed.
 
+(** C allows pointers one past the last element of an array.  These are not
+  valid according to the previously defined [valid_pointer]. The property
+  [weak_valid_pointer m b ofs] holds if address [b, ofs] is a valid pointer
+  in [m], or a pointer one past a valid block in [m].  *)
+
+Definition weak_valid_pointer (m: mem) (b: block) (ofs: Z) :=
+  valid_pointer m b ofs || valid_pointer m b (ofs - 1).
+
+Lemma weak_valid_pointer_spec:
+  forall m b ofs,
+  weak_valid_pointer m b ofs = true <->
+    valid_pointer m b ofs = true \/ valid_pointer m b (ofs - 1) = true.
+Proof.
+  intros. unfold weak_valid_pointer. now rewrite orb_true_iff.
+Qed.
+Lemma valid_pointer_implies:
+  forall m b ofs,
+  valid_pointer m b ofs = true -> weak_valid_pointer m b ofs = true.
+Proof.
+  intros. apply weak_valid_pointer_spec. auto.
+Qed.
+
 (** * Operations over memory stores *)
 
 (** The initial store *)
@@ -2887,6 +2908,15 @@ Proof.
   eapply valid_access_extends; eauto.
 Qed.
 
+Theorem weak_valid_pointer_extends:
+  forall m1 m2 b ofs,
+  extends m1 m2 ->
+  weak_valid_pointer m1 b ofs = true -> weak_valid_pointer m2 b ofs = true.
+Proof.
+  intros until 1. unfold weak_valid_pointer. rewrite !orb_true_iff.
+  intros []; eauto using valid_pointer_extends.
+Qed.
+
 (** * Memory injections *)
 
 (** A memory state [m1] injects into another memory state [m2] via the
@@ -2899,7 +2929,8 @@ Qed.
 - if [f b = Some(b', delta)], [b'] must be valid in [m2];
 - distinct blocks in [m1] are mapped to non-overlapping sub-blocks in [m2];
 - the sizes of [m2]'s blocks are representable with unsigned machine integers;
-- the offsets [delta] are representable with unsigned machine integers.
+- pointers that could be represented using unsigned machine integers remain
+  representable after the injection.
 *)
 
 Record inject' (f: meminj) (m1 m2: mem) : Prop :=
@@ -2913,12 +2944,11 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop :=
     mi_no_overlap:
       meminj_no_overlap f m1;
     mi_representable:
-      forall b b' delta ofs k p,
+      forall b b' delta ofs,
       f b = Some(b', delta) ->
-      perm m1 b (Int.unsigned ofs) k p ->
+      weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
       delta >= 0 /\ 0 <= Int.unsigned ofs + delta <= Int.max_unsigned
   }.
-
 Definition inject := inject'.
 
 Local Hint Resolve mi_mappedblocks: mem.
@@ -2987,6 +3017,18 @@ Proof.
   eapply valid_access_inject; eauto.
 Qed.
 
+Theorem weak_valid_pointer_inject:
+  forall f m1 m2 b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  inject f m1 m2 ->
+  weak_valid_pointer m1 b1 ofs = true ->
+  weak_valid_pointer m2 b2 (ofs + delta) = true.
+Proof.
+  intros until 2. unfold weak_valid_pointer. rewrite !orb_true_iff.
+  replace (ofs + delta - 1) with ((ofs - 1) + delta) by omega.
+  intros []; eauto using valid_pointer_inject.
+Qed.
+
 (** The following lemmas establish the absence of machine integer overflow
   during address computations. *)
 
@@ -3006,17 +3048,19 @@ Qed.
 *)
 
 Lemma address_inject:
-  forall f m1 m2 b1 ofs1 b2 delta,
+  forall f m1 m2 b1 ofs1 b2 delta p,
   inject f m1 m2 ->
-  perm m1 b1 (Int.unsigned ofs1) Max Nonempty ->
+  perm m1 b1 (Int.unsigned ofs1) Cur p ->
   f b1 = Some (b2, delta) ->
   Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
 Proof.
-  intros.
+  intros. apply (perm_implies _ _ _ _ _ Nonempty) in H0; [| constructor].
+  rewrite <-valid_pointer_nonempty_perm in H0.
+  apply valid_pointer_implies in H0.
   exploit mi_representable; eauto. intros [A B].
   assert (0 <= delta <= Int.max_unsigned).
     generalize (Int.unsigned_range ofs1). omega.
-  unfold Int.add. repeat rewrite Int.unsigned_repr; auto.
+  unfold Int.add. repeat rewrite Int.unsigned_repr; omega.
 Qed.
 
 Lemma address_inject':
@@ -3027,22 +3071,29 @@ Lemma address_inject':
   Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
 Proof.
   intros. destruct H0. eapply address_inject; eauto. 
-  apply perm_cur_max. apply H0. generalize (size_chunk_pos chunk). omega. 
+  apply H0. generalize (size_chunk_pos chunk). omega. 
+Qed.
+
+Theorem weak_valid_pointer_inject_no_overflow:
+  forall f m1 m2 b ofs b' delta,
+  inject f m1 m2 ->
+  weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+  f b = Some(b', delta) ->
+  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+Proof.
+  intros. exploit mi_representable; eauto. intros.
+  pose proof (Int.unsigned_range ofs).
+  rewrite Int.unsigned_repr; omega.
 Qed.
 
 Theorem valid_pointer_inject_no_overflow:
-  forall f m1 m2 b ofs b' x,
+  forall f m1 m2 b ofs b' delta,
   inject f m1 m2 ->
   valid_pointer m1 b (Int.unsigned ofs) = true ->
-  f b = Some(b', x) ->
-  0 <= Int.unsigned ofs + Int.unsigned (Int.repr x) <= Int.max_unsigned.
+  f b = Some(b', delta) ->
+  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 Proof.
-  intros. rewrite valid_pointer_valid_access in H0.
-  assert (perm m1 b (Int.unsigned ofs) Cur Nonempty).
-    apply H0. simpl. omega.
-  exploit mi_representable; eauto. intros [A B].
-  rewrite Int.unsigned_repr; auto.
-  generalize (Int.unsigned_range ofs). omega.
+  eauto using weak_valid_pointer_inject_no_overflow, valid_pointer_implies.
 Qed.
 
 Theorem valid_pointer_inject_val:
@@ -3058,6 +3109,19 @@ Proof.
   rewrite valid_pointer_valid_access in H0. eauto.
 Qed.
 
+Theorem weak_valid_pointer_inject_val:
+  forall f m1 m2 b ofs b' ofs',
+  inject f m1 m2 ->
+  weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+  val_inject f (Vptr b ofs) (Vptr b' ofs') ->
+  weak_valid_pointer m2 b' (Int.unsigned ofs') = true.
+Proof.
+  intros. inv H1. exploit mi_representable; try eassumption. intros.
+  pose proof (Int.unsigned_range ofs).
+  exploit weak_valid_pointer_inject; eauto.
+  unfold Int.add. repeat rewrite Int.unsigned_repr; auto; omega.
+Qed.
+
 Theorem inject_no_overlap:
   forall f m1 m2 b1 b2 b1' b2' delta1 delta2 ofs1 ofs2,
   inject f m1 m2 ->
@@ -3213,7 +3277,10 @@ Proof.
 (* no overlap *)
   red; intros. eauto with mem.
 (* representable *)
-  eauto with mem. 
+  intros. eapply mi_representable; try eassumption.
+  rewrite weak_valid_pointer_spec in *.
+  rewrite !valid_pointer_nonempty_perm in H4 |- *.
+  destruct H4; eauto with mem.
 Qed.
 
 Theorem store_unmapped_inject:
@@ -3234,7 +3301,10 @@ Proof.
 (* no overlap *)
   red; intros. eauto with mem.
 (* representable *)
-  eauto with mem.
+  intros. eapply mi_representable; try eassumption.
+  rewrite weak_valid_pointer_spec in *.
+  rewrite !valid_pointer_nonempty_perm in H3 |- *.
+  destruct H3; eauto with mem.
 Qed.
 
 Theorem store_outside_inject:
@@ -3299,7 +3369,10 @@ Proof.
 (* no overlap *)
   red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. 
 (* representable *)
-  intros. eapply mi_representable0; eauto. eapply perm_storebytes_2; eauto. 
+  intros. eapply mi_representable0; eauto.
+  rewrite weak_valid_pointer_spec in *.
+  rewrite !valid_pointer_nonempty_perm in H4 |- *.
+  destruct H4; eauto using perm_storebytes_2. 
 Qed.
 
 Theorem storebytes_unmapped_inject:
@@ -3320,7 +3393,10 @@ Proof.
 (* no overlap *)
   red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. 
 (* representable *)
-  intros. eapply mi_representable0; eauto. eapply perm_storebytes_2; eauto. 
+  intros. eapply mi_representable0; eauto.
+  rewrite weak_valid_pointer_spec in *.
+  rewrite !valid_pointer_nonempty_perm in H3 |- *.
+  destruct H3; eauto using perm_storebytes_2.
 Qed.
 
 Theorem storebytes_outside_inject:
@@ -3406,8 +3482,11 @@ Proof.
   exploit perm_alloc_inv. eauto. eexact H7. rewrite zeq_false; auto. 
 (* representable *)
   unfold f'; intros.
-  exploit perm_alloc_inv; eauto. 
-  destruct (zeq b b1). congruence. eauto with mem.
+  destruct (zeq b b1); try discriminate.
+  eapply mi_representable0; try eassumption.
+  rewrite weak_valid_pointer_spec in *.
+  rewrite !valid_pointer_nonempty_perm in H4 |- *.
+  destruct H4; eauto using perm_alloc_4.
 (* incr *)
   split. auto. 
 (* image *)
@@ -3422,7 +3501,7 @@ Theorem alloc_left_mapped_inject:
   alloc m1 lo hi = (m1', b1) ->
   valid_block m2 b2 ->
   0 <= delta <= Int.max_unsigned ->
-  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs <= Int.max_unsigned) ->
+  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Int.max_unsigned) ->
   (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) ->
   inj_offset_aligned delta (hi-lo) ->
   (forall b delta' ofs k p,
@@ -3478,11 +3557,20 @@ Proof.
     eapply H6; eauto. omega.
   eauto.
 (* representable *)
-  unfold f'; intros. exploit perm_alloc_inv; eauto. destruct (zeq b b1); intros.
-  inversion H9; subst b' delta0. exploit H3. apply H4 with (k := k) (p := p); eauto.
-  intros [A | A]. generalize (Int.unsigned_range_2 ofs). omega.
-  generalize (Int.unsigned_range_2 ofs). omega.
-  eauto.
+  unfold f'; intros.
+  rewrite weak_valid_pointer_spec in *.
+  rewrite !valid_pointer_nonempty_perm in H10.
+  destruct (zeq b b1).
+   subst. injection H9; intros; subst b' delta0. destruct H10.
+    exploit perm_alloc_inv; eauto; rewrite zeq_true; intro.
+    exploit H3. apply H4 with (k := Cur) (p := Nonempty); eauto.
+    generalize (Int.unsigned_range_2 ofs). omega.
+   exploit perm_alloc_inv; eauto; rewrite zeq_true; intro.
+   exploit H3. apply H4 with (k := Cur) (p := Nonempty); eauto.
+   generalize (Int.unsigned_range_2 ofs). omega.
+  eapply mi_representable0; try eassumption.
+  rewrite !weak_valid_pointer_spec, !valid_pointer_nonempty_perm.
+  destruct H10; eauto using perm_alloc_4.
 (* incr *)
   split. auto.
 (* image of b1 *)
@@ -3537,7 +3625,10 @@ Proof.
 (* no overlap *)
   red; intros. eauto with mem. 
 (* representable *)
-  eauto with mem. 
+  intros. eapply mi_representable0; try eassumption.
+  rewrite weak_valid_pointer_spec in *.
+  rewrite !valid_pointer_nonempty_perm in H2 |- *.
+  destruct H2; eauto with mem.
 Qed.
 
 Lemma free_list_left_inject:
@@ -3686,9 +3777,13 @@ Proof.
   set (ofs' := Int.repr (Int.unsigned ofs + delta1)).
   assert (Int.unsigned ofs' = Int.unsigned ofs + delta1). 
     unfold ofs'; apply Int.unsigned_repr. auto.
-  exploit mi_representable1. eauto. instantiate (3 := ofs'). 
-  rewrite H. eapply perm_inj; eauto. rewrite H. intros [C D].
-  omega.
+  exploit mi_representable1. eauto. instantiate (1 := ofs').
+  rewrite H.
+  rewrite weak_valid_pointer_spec, !valid_pointer_nonempty_perm in *.
+  replace (Int.unsigned ofs + delta1 - 1) with
+    ((Int.unsigned ofs - 1) + delta1) by omega.
+  destruct H0; eauto using perm_inj.
+  rewrite H. omega.
 Qed.
 
 Lemma val_lessdef_inject_compose:
@@ -3721,7 +3816,9 @@ Proof.
 (* no overlap *)
   red; intros. eapply mi_no_overlap0; eauto; eapply perm_extends; eauto.
 (* representable *)
-  eapply mi_representable0; eauto. eapply perm_extends; eauto. 
+  eapply mi_representable0; eauto.
+  rewrite weak_valid_pointer_spec, !valid_pointer_nonempty_perm in *.
+  destruct H1; eauto using perm_extends.
 Qed.
 
 Lemma inject_extends_compose:
diff --git a/common/Memtype.v b/common/Memtype.v
index a39daf4..59dc7a3 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -259,6 +259,22 @@ Axiom valid_pointer_valid_access:
   forall m b ofs,
   valid_pointer m b ofs = true <-> valid_access m Mint8unsigned b ofs Nonempty.
 
+(** C allows pointers one past the last element of an array.  These are not
+  valid according to the previously defined [valid_pointer]. The property
+  [weak_valid_pointer m b ofs] holds if address [b, ofs] is a valid pointer
+  in [m], or a pointer one past a valid block in [m].  *)
+
+Definition weak_valid_pointer (m: mem) (b: block) (ofs: Z) :=
+  valid_pointer m b ofs || valid_pointer m b (ofs - 1).
+
+Axiom weak_valid_pointer_spec:
+  forall m b ofs,
+  weak_valid_pointer m b ofs = true <->
+    valid_pointer m b ofs = true \/ valid_pointer m b (ofs - 1) = true.
+Axiom valid_pointer_implies:
+  forall m b ofs,
+  valid_pointer m b ofs = true -> weak_valid_pointer m b ofs = true.
+
 (** * Properties of the memory operations *)
 
 (** ** Properties of the initial memory state. *)
@@ -899,6 +915,10 @@ Axiom valid_access_extends:
 Axiom valid_pointer_extends:
   forall m1 m2 b ofs,
   extends m1 m2 -> valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true.
+Axiom weak_valid_pointer_extends:
+  forall m1 m2 b ofs,
+  extends m1 m2 ->
+  weak_valid_pointer m1 b ofs = true -> weak_valid_pointer m2 b ofs = true.
 
 (** * Memory injections *)
 
@@ -950,19 +970,33 @@ Axiom valid_pointer_inject:
   valid_pointer m1 b1 ofs = true ->
   valid_pointer m2 b2 (ofs + delta) = true.
 
+Axiom weak_valid_pointer_inject:
+  forall f m1 m2 b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  inject f m1 m2 ->
+  weak_valid_pointer m1 b1 ofs = true ->
+  weak_valid_pointer m2 b2 (ofs + delta) = true.
+
 Axiom address_inject:
-  forall f m1 m2 b1 ofs1 b2 delta,
+  forall f m1 m2 b1 ofs1 b2 delta p,
   inject f m1 m2 ->
-  perm m1 b1 (Int.unsigned ofs1) Max Nonempty ->
+  perm m1 b1 (Int.unsigned ofs1) Cur p ->
   f b1 = Some (b2, delta) ->
   Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
 
 Axiom valid_pointer_inject_no_overflow:
-  forall f m1 m2 b ofs b' x,
+  forall f m1 m2 b ofs b' delta,
   inject f m1 m2 ->
   valid_pointer m1 b (Int.unsigned ofs) = true ->
-  f b = Some(b', x) ->
-  0 <= Int.unsigned ofs + Int.unsigned (Int.repr x) <= Int.max_unsigned.
+  f b = Some(b', delta) ->
+  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+
+Axiom weak_valid_pointer_inject_no_overflow:
+  forall f m1 m2 b ofs b' delta,
+  inject f m1 m2 ->
+  weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+  f b = Some(b', delta) ->
+  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 
 Axiom valid_pointer_inject_val:
   forall f m1 m2 b ofs b' ofs',
@@ -971,6 +1005,13 @@ Axiom valid_pointer_inject_val:
   val_inject f (Vptr b ofs) (Vptr b' ofs') ->
   valid_pointer m2 b' (Int.unsigned ofs') = true.
 
+Axiom weak_valid_pointer_inject_val:
+  forall f m1 m2 b ofs b' ofs',
+  inject f m1 m2 ->
+  weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+  val_inject f (Vptr b ofs) (Vptr b' ofs') ->
+  weak_valid_pointer m2 b' (Int.unsigned ofs') = true.
+
 Axiom inject_no_overlap:
   forall f m1 m2 b1 b2 b1' b2' delta1 delta2 ofs1 ofs2,
   inject f m1 m2 ->
@@ -1103,7 +1144,7 @@ Axiom alloc_left_mapped_inject:
   alloc m1 lo hi = (m1', b1) ->
   valid_block m2 b2 ->
   0 <= delta <= Int.max_unsigned ->
-  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs <= Int.max_unsigned) ->
+  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Int.max_unsigned) ->
   (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) ->
   inj_offset_aligned delta (hi-lo) ->
   (forall b delta' ofs k p,
diff --git a/common/Values.v b/common/Values.v
index f02fa70..f629628 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -349,6 +349,7 @@ Definition divf (v1 v2: val): val :=
 Section COMPARISONS.
 
 Variable valid_ptr: block -> Z -> bool.
+Let weak_valid_ptr (b: block) (ofs: Z) := valid_ptr b ofs || valid_ptr b (ofs - 1).
 
 Definition cmp_bool (c: comparison) (v1 v2: val): option bool :=
   match v1, v2 with
@@ -370,11 +371,16 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool :=
   | Vint n1, Vptr b2 ofs2 =>
       if Int.eq n1 Int.zero then cmp_different_blocks c else None
   | Vptr b1 ofs1, Vptr b2 ofs2 =>
-      if valid_ptr b1 (Int.unsigned ofs1) && valid_ptr b2 (Int.unsigned ofs2) then
-        if zeq b1 b2
+      if zeq b1 b2 then
+        if weak_valid_ptr b1 (Int.unsigned ofs1)
+           && weak_valid_ptr b2 (Int.unsigned ofs2)
         then Some (Int.cmpu c ofs1 ofs2)
-        else cmp_different_blocks c
-      else None
+        else None
+      else
+        if valid_ptr b1 (Int.unsigned ofs1)
+           && valid_ptr b2 (Int.unsigned ofs2)
+        then cmp_different_blocks c
+        else None
   | Vptr b1 ofs1, Vint n2 =>
       if Int.eq n2 Int.zero then cmp_different_blocks c else None
   | _, _ => None
@@ -802,8 +808,12 @@ Proof.
   rewrite Int.negate_cmpu. auto.
   destruct (Int.eq i Int.zero); auto. 
   destruct (Int.eq i0 Int.zero); auto.
+  destruct (zeq b b0).
+  destruct ((valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1)) &&
+            (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))).
+  rewrite Int.negate_cmpu. auto.
+  auto.
   destruct (valid_ptr b (Int.unsigned i) && valid_ptr b0 (Int.unsigned i0)); auto.
-  destruct (zeq b b0); auto. rewrite Int.negate_cmpu. auto.
 Qed.
 
 Lemma not_of_optbool:
@@ -821,7 +831,8 @@ Qed.
 
 Theorem negate_cmpu:
   forall valid_ptr c x y,
-  cmpu valid_ptr (negate_comparison c) x y = notbool (cmpu valid_ptr c x y).
+  cmpu valid_ptr (negate_comparison c) x y =
+    notbool (cmpu valid_ptr c x y).
 Proof.
   intros. unfold cmpu. rewrite negate_cmpu_bool. apply not_of_optbool.
 Qed.
@@ -835,7 +846,8 @@ Qed.
 
 Theorem swap_cmpu_bool:
   forall valid_ptr c x y,
-  cmpu_bool valid_ptr (swap_comparison c) x y = cmpu_bool valid_ptr c y x.
+  cmpu_bool valid_ptr (swap_comparison c) x y =
+    cmpu_bool valid_ptr c y x.
 Proof.
   assert (forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c).
     destruct c; auto.
@@ -843,10 +855,15 @@ Proof.
   rewrite Int.swap_cmpu. auto.
   case (Int.eq i Int.zero); auto.
   case (Int.eq i0 Int.zero); auto.
-  destruct (valid_ptr b (Int.unsigned i)); destruct (valid_ptr b0 (Int.unsigned i0)); auto.
-  simpl. destruct (zeq b b0); subst. 
-  rewrite zeq_true. rewrite Int.swap_cmpu. auto.
-  rewrite zeq_false; auto.
+  destruct (zeq b b0); subst.
+  rewrite zeq_true.
+  destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1));
+  destruct (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1));
+  simpl; auto.
+  rewrite Int.swap_cmpu. auto.
+  rewrite zeq_false by auto.
+  destruct (valid_ptr b (Int.unsigned i));
+    destruct (valid_ptr b0 (Int.unsigned i0)); simpl; auto.
 Qed.
 
 Theorem negate_cmpf_eq:
@@ -904,25 +921,29 @@ Proof.
 Qed.
 
 Theorem cmpu_ne_0_optbool:
-  forall valid_ptr ob, cmpu valid_ptr Cne (of_optbool ob) (Vint Int.zero) = of_optbool ob.
+  forall valid_ptr ob,
+  cmpu valid_ptr Cne (of_optbool ob) (Vint Int.zero) = of_optbool ob.
 Proof.
   intros. destruct ob; simpl; auto. destruct b; auto. 
 Qed.
 
 Theorem cmpu_eq_1_optbool:
-  forall valid_ptr ob, cmpu valid_ptr Ceq (of_optbool ob) (Vint Int.one) = of_optbool ob.
+  forall valid_ptr ob,
+  cmpu valid_ptr Ceq (of_optbool ob) (Vint Int.one) = of_optbool ob.
 Proof.
   intros. destruct ob; simpl; auto. destruct b; auto. 
 Qed.
 
 Theorem cmpu_eq_0_optbool:
-  forall valid_ptr ob, cmpu valid_ptr Ceq (of_optbool ob) (Vint Int.zero) = of_optbool (option_map negb ob).
+  forall valid_ptr ob,
+  cmpu valid_ptr Ceq (of_optbool ob) (Vint Int.zero) = of_optbool (option_map negb ob).
 Proof.
   intros. destruct ob; simpl; auto. destruct b; auto. 
 Qed.
 
 Theorem cmpu_ne_1_optbool:
-  forall valid_ptr ob, cmpu valid_ptr Cne (of_optbool ob) (Vint Int.one) = of_optbool (option_map negb ob).
+  forall valid_ptr ob,
+  cmpu valid_ptr Cne (of_optbool ob) (Vint Int.one) = of_optbool (option_map negb ob).
 Proof.
   intros. destruct ob; simpl; auto. destruct b; auto. 
 Qed.
@@ -1030,9 +1051,16 @@ Proof.
   destruct v1; simpl in H2; try discriminate;
   destruct v2; simpl in H2; try discriminate;
   inv H0; inv H1; simpl; auto.
+  destruct (zeq b0 b1).
+  assert (forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true ->
+                        valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true).
+    intros until ofs. rewrite ! orb_true_iff. intuition. 
+  destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)) eqn:?; try discriminate.
+  destruct (valid_ptr b1 (Int.unsigned i0) || valid_ptr b1 (Int.unsigned i0 - 1)) eqn:?; try discriminate.
+  erewrite !H0 by eauto. auto.
   destruct (valid_ptr b0 (Int.unsigned i)) eqn:?; try discriminate.
   destruct (valid_ptr b1 (Int.unsigned i0)) eqn:?; try discriminate.
-  rewrite (H _ _ Heqb2). rewrite (H _ _ Heqb0). auto.
+  erewrite !H by eauto. auto.
 Qed.
 
 Lemma of_optbool_lessdef:
@@ -1087,14 +1115,118 @@ Inductive val_list_inject (mi: meminj): list val -> list val-> Prop:=
 
 Hint Resolve val_nil_inject val_cons_inject.
 
+Section VAL_INJ_OPS.
+
+Variable f: meminj.
+
 Lemma val_load_result_inject:
-  forall f chunk v1 v2,
+  forall chunk v1 v2,
   val_inject f v1 v2 ->
   val_inject f (Val.load_result chunk v1) (Val.load_result chunk v2).
 Proof.
   intros. inv H; destruct chunk; simpl; econstructor; eauto.
 Qed.
 
+Remark val_add_inject:
+  forall v1 v1' v2 v2',
+  val_inject f v1 v1' ->
+  val_inject f v2 v2' ->
+  val_inject f (Val.add v1 v2) (Val.add v1' v2').
+Proof.
+  intros. inv H; inv H0; simpl; econstructor; eauto.
+  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+Qed.
+
+Remark val_sub_inject:
+  forall v1 v1' v2 v2',
+  val_inject f v1 v1' ->
+  val_inject f v2 v2' ->
+  val_inject f (Val.sub v1 v2) (Val.sub v1' v2').
+Proof.
+  intros. inv H; inv H0; simpl; auto.
+  econstructor; eauto. rewrite Int.sub_add_l. auto.
+  destruct (zeq b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite zeq_true.
+  rewrite Int.sub_shifted. auto.
+Qed.
+
+Lemma val_cmp_bool_inject:
+  forall c v1 v2 v1' v2' b,
+  val_inject f v1 v1' ->
+  val_inject f v2 v2' ->
+  Val.cmp_bool c v1 v2 = Some b ->
+  Val.cmp_bool c v1' v2' = Some b.
+Proof.
+  intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
+Qed.
+
+Variable (valid_ptr1 valid_ptr2 : block -> Z -> bool).
+
+Let weak_valid_ptr1 b ofs := valid_ptr1 b ofs || valid_ptr1 b (ofs - 1).
+Let weak_valid_ptr2 b ofs := valid_ptr2 b ofs || valid_ptr2 b (ofs - 1).
+
+Hypothesis valid_ptr_inj:
+  forall b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  valid_ptr1 b1 (Int.unsigned ofs) = true ->
+  valid_ptr2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_ptr_inj:
+  forall b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  weak_valid_ptr1 b1 (Int.unsigned ofs) = true ->
+  weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_ptr_no_overflow:
+  forall b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  weak_valid_ptr1 b1 (Int.unsigned ofs) = true ->
+  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+
+Hypothesis valid_different_ptrs_inj:
+  forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
+  b1 <> b2 ->
+  valid_ptr1 b1 (Int.unsigned ofs1) = true ->
+  valid_ptr1 b2 (Int.unsigned ofs2) = true ->
+  f b1 = Some (b1', delta1) ->
+  f b2 = Some (b2', delta2) ->
+  b1' <> b2' \/
+  Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)).
+
+Lemma val_cmpu_bool_inject:
+  forall c v1 v2 v1' v2' b,
+  val_inject f v1 v1' ->
+  val_inject f v2 v2' ->
+  Val.cmpu_bool valid_ptr1 c v1 v2 = Some b ->
+  Val.cmpu_bool valid_ptr2 c v1' v2' = Some b.
+Proof.
+  Local Opaque Int.add.
+  intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
+  fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1.
+  fold (weak_valid_ptr1 b0 (Int.unsigned ofs0)) in H1.
+  fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+  fold (weak_valid_ptr2 b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))). 
+  destruct (zeq b1 b0); subst.
+  rewrite H in H2. inv H2. rewrite zeq_true.
+  destruct (weak_valid_ptr1 b0 (Int.unsigned ofs1)) eqn:?; try discriminate.
+  destruct (weak_valid_ptr1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
+  erewrite !weak_valid_ptr_inj by eauto. simpl.
+  rewrite <-H1. simpl. decEq. apply Int.translate_cmpu; eauto.
+  destruct (valid_ptr1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
+  destruct (valid_ptr1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
+  destruct (zeq b2 b3); subst.
+  assert (valid_ptr_implies: forall b ofs, valid_ptr1 b ofs = true -> weak_valid_ptr1 b ofs = true).
+    intros. unfold weak_valid_ptr1. rewrite H0; auto. 
+  erewrite !weak_valid_ptr_inj by eauto using valid_ptr_implies. simpl.
+  exploit valid_different_ptrs_inj; eauto. intros [?|?]; [congruence |].
+  destruct c; simpl in H1; inv H1.
+  simpl; decEq. rewrite Int.eq_false; auto. congruence.
+  simpl; decEq. rewrite Int.eq_false; auto. congruence.
+  now erewrite !valid_ptr_inj by eauto.
+Qed.
+
+End VAL_INJ_OPS.
+
 (** Monotone evolution of a memory injection. *)
 
 Definition inject_incr (f1 f2: meminj) : Prop :=
@@ -1185,4 +1317,3 @@ Proof.
   unfold compose_meminj; rewrite H1; rewrite H3; eauto. 
   rewrite Int.add_assoc. decEq. unfold Int.add. apply Int.eqm_samerepr. auto with ints.
 Qed. 
-
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 7a4348b..b524539 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -1110,10 +1110,11 @@ Proof.
   rewrite Heqb1; reflexivity.
 (* ptr ptr *)
   simpl. 
-  destruct (Mem.valid_pointer m b0 (Int.unsigned i) &&
-            Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate.
+  fold (Mem.weak_valid_pointer m b0 (Int.unsigned i)) in *.
+  fold (Mem.weak_valid_pointer m b1 (Int.unsigned i0)) in *.
   destruct (zeq b0 b1).
-  inversion H1.
+  destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i) &&
+            Mem.weak_valid_pointer m b1 (Int.unsigned i0)); inversion H1.
   destruct c; simpl; auto.
   destruct (Int.eq i i0); reflexivity.
   destruct (Int.eq i i0); auto.
@@ -1121,6 +1122,8 @@ Proof.
   rewrite int_not_ltu. destruct (Int.ltu i i0); simpl; destruct (Int.eq i i0); auto.
   rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity.
   destruct (Int.ltu i i0); reflexivity.
+  destruct (Mem.valid_pointer m b0 (Int.unsigned i) &&
+            Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate.
   destruct c; simpl in *; inv H1; reflexivity.
 Qed.
 
diff --git a/ia32/Op.v b/ia32/Op.v
index 93a867a..66ee633 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -722,10 +722,16 @@ Hypothesis valid_pointer_inj:
   Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
 
-Hypothesis valid_pointer_no_overflow:
+Hypothesis weak_valid_pointer_inj:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_pointer_no_overflow:
+  forall b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 
 Hypothesis valid_different_pointers_inj:
@@ -753,50 +759,17 @@ Ltac InvInject :=
   | _ => idtac
   end.
 
-Remark val_add_inj:
-  forall v1 v1' v2 v2',
-  val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.add v1 v2) (Val.add v1' v2').
-Proof.
-  intros. inv H; inv H0; simpl; econstructor; eauto. 
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-Qed.
-
 Lemma eval_condition_inj:
   forall cond vl1 vl2 b,
   val_list_inject f vl1 vl2 ->
   eval_condition cond vl1 m1 = Some b ->
   eval_condition cond vl2 m2 = Some b.
 Proof.
-Opaque Int.add.
-  assert (CMPU:
-    forall c v1 v2 v1' v2' b,
-    val_inject f v1 v1' ->
-    val_inject f v2 v2' ->
-    Val.cmpu_bool (Mem.valid_pointer m1) c v1 v2 = Some b ->
-    Val.cmpu_bool (Mem.valid_pointer m2) c v1' v2' = Some b).
-  intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
-  destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
-  destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
-  rewrite (valid_pointer_inj _ H2 Heqb4).
-  rewrite (valid_pointer_inj _ H Heqb0). simpl.
-  destruct (zeq b1 b0); simpl in H1.
-  inv H1. rewrite H in H2; inv H2. rewrite zeq_true. 
-  decEq. apply Int.translate_cmpu.
-  eapply valid_pointer_no_overflow; eauto.
-  eapply valid_pointer_no_overflow; eauto.
-  exploit valid_different_pointers_inj; eauto. intros P.
-  destruct (zeq b2 b3); auto.
-  destruct P. congruence. 
-  destruct c; simpl in H1; inv H1.
-  simpl; decEq. rewrite Int.eq_false; auto. congruence.
-  simpl; decEq. rewrite Int.eq_false; auto. congruence.
-
   intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
-  eauto.
+  eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; simpl in H0; inv H0; auto.
-  eauto. 
+  eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
 Qed.
@@ -816,13 +789,13 @@ Lemma eval_addressing_inj:
   exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
 Proof.
   intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto. apply val_add_inj; auto.
-  apply val_add_inj; auto. inv H4; simpl; auto.
-  apply val_add_inj; auto. apply val_add_inj; auto. inv H2; simpl; auto.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto. inv H4; simpl; auto.
-  apply val_add_inj; auto.
+  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto. apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto. inv H4; simpl; auto.
+  apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. inv H2; simpl; auto.
+  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto. inv H4; simpl; auto.
+  apply Values.val_add_inject; auto.
 Qed.
 
 Lemma eval_operation_inj:
@@ -903,10 +876,20 @@ Proof.
   intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. 
 Qed.
 
-Remark valid_pointer_no_overflow_extends:
+Remark weak_valid_pointer_extends:
+  forall m1 m2, Mem.extends m1 m2 ->
+  forall b1 ofs b2 delta,
+  Some(b1, 0) = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+Proof.
+  intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto. 
+Qed.
+
+Remark weak_valid_pointer_no_overflow_extends:
   forall m1 b1 ofs b2 delta,
   Some(b1, 0) = Some(b2, delta) ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 Proof.
   intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2.
@@ -934,7 +917,8 @@ Lemma eval_condition_lessdef:
 Proof.
   intros. eapply eval_condition_inj with (f := fun b => Some(b, 0)) (m1 := m1).
   apply valid_pointer_extends; auto.
-  apply valid_pointer_no_overflow_extends; auto. 
+  apply weak_valid_pointer_extends; auto.
+  apply weak_valid_pointer_no_overflow_extends.
   apply valid_different_pointers_extends; auto.
   rewrite <- val_list_inject_lessdef. eauto. auto.
 Qed.
@@ -953,7 +937,8 @@ Proof.
   eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
   intros. rewrite <- val_inject_lessdef; auto.
   apply valid_pointer_extends; auto.
-  apply valid_pointer_no_overflow_extends; auto. 
+  apply weak_valid_pointer_extends; auto.
+  apply weak_valid_pointer_no_overflow_extends.
   apply valid_different_pointers_extends; auto.
   rewrite <- val_inject_lessdef; auto.
   eauto. auto. 
@@ -1009,7 +994,8 @@ Lemma eval_condition_inject:
 Proof.
   intros. eapply eval_condition_inj with (f := f) (m1 := m1); eauto.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
-  intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
 Qed.
 
@@ -1041,9 +1027,9 @@ Proof.
   eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
   exact symbol_address_inject.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
-  intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
 Qed.
 
 End EVAL_INJECT.
-
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 4a1fb62..a8936fe 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -652,10 +652,16 @@ Hypothesis valid_pointer_inj:
   Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
 
-Hypothesis valid_pointer_no_overflow:
+Hypothesis weak_valid_pointer_inj:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_pointer_no_overflow:
+  forall b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 
 Hypothesis valid_different_pointers_inj:
@@ -683,50 +689,17 @@ Ltac InvInject :=
   | _ => idtac
   end.
 
-Remark val_add_inj:
-  forall v1 v1' v2 v2',
-  val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.add v1 v2) (Val.add v1' v2').
-Proof.
-  intros. inv H; inv H0; simpl; econstructor; eauto. 
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-Qed.
-
 Lemma eval_condition_inj:
   forall cond vl1 vl2 b,
   val_list_inject f vl1 vl2 ->
   eval_condition cond vl1 m1 = Some b ->
   eval_condition cond vl2 m2 = Some b.
 Proof.
-Opaque Int.add.
-  assert (CMPU:
-    forall c v1 v2 v1' v2' b,
-    val_inject f v1 v1' ->
-    val_inject f v2 v2' ->
-    Val.cmpu_bool (Mem.valid_pointer m1) c v1 v2 = Some b ->
-    Val.cmpu_bool (Mem.valid_pointer m2) c v1' v2' = Some b).
-  intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
-  destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
-  destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
-  rewrite (valid_pointer_inj _ H2 Heqb4).
-  rewrite (valid_pointer_inj _ H Heqb0). simpl.
-  destruct (zeq b1 b0); simpl in H1.
-  inv H1. rewrite H in H2; inv H2. rewrite zeq_true. 
-  decEq. apply Int.translate_cmpu.
-  eapply valid_pointer_no_overflow; eauto.
-  eapply valid_pointer_no_overflow; eauto.
-  exploit valid_different_pointers_inj; eauto. intros P.
-  destruct (zeq b2 b3); auto.
-  destruct P. congruence. 
-  destruct c; simpl in H1; inv H1.
-  simpl; decEq. rewrite Int.eq_false; auto. congruence.
-  simpl; decEq. rewrite Int.eq_false; auto. congruence.
-
   intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
-  eauto.
+  eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; simpl in H0; inv H0; auto.
-  eauto. 
+  eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
 Qed.
@@ -749,8 +722,8 @@ Proof.
   inv H; simpl; econstructor; eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto.
+  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto.
   inv H4; inv H2; simpl; auto. econstructor; eauto. 
     rewrite Int.sub_add_l. auto.
     destruct (zeq b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite zeq_true. 
@@ -805,11 +778,8 @@ Lemma eval_addressing_inj:
   eval_addressing genv sp1 addr vl1 = Some v1 ->
   exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
 Proof.
-  intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto.
+  intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists;
+    auto using Values.val_add_inject.
 Qed.
 
 End EVAL_COMPAT.
@@ -831,10 +801,20 @@ Proof.
   intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. 
 Qed.
 
-Remark valid_pointer_no_overflow_extends:
+Remark weak_valid_pointer_extends:
+  forall m1 m2, Mem.extends m1 m2 ->
+  forall b1 ofs b2 delta,
+  Some(b1, 0) = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+Proof.
+  intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto.
+Qed.
+
+Remark weak_valid_pointer_no_overflow_extends:
   forall m1 b1 ofs b2 delta,
   Some(b1, 0) = Some(b2, delta) ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 Proof.
   intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2.
@@ -862,7 +842,8 @@ Lemma eval_condition_lessdef:
 Proof.
   intros. eapply eval_condition_inj with (f := fun b => Some(b, 0)) (m1 := m1).
   apply valid_pointer_extends; auto.
-  apply valid_pointer_no_overflow_extends; auto. 
+  apply weak_valid_pointer_extends; auto.
+  apply weak_valid_pointer_no_overflow_extends; auto.
   apply valid_different_pointers_extends; auto.
   rewrite <- val_list_inject_lessdef. eauto. auto.
 Qed.
@@ -881,7 +862,8 @@ Proof.
   eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
   intros. rewrite <- val_inject_lessdef; auto.
   apply valid_pointer_extends; auto.
-  apply valid_pointer_no_overflow_extends; auto. 
+  apply weak_valid_pointer_extends; auto.
+  apply weak_valid_pointer_no_overflow_extends; auto.
   apply valid_different_pointers_extends; auto.
   rewrite <- val_inject_lessdef; auto.
   eauto. auto. 
@@ -937,7 +919,8 @@ Lemma eval_condition_inject:
 Proof.
   intros. eapply eval_condition_inj with (f := f) (m1 := m1); eauto.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
-  intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
 Qed.
 
@@ -969,7 +952,8 @@ Proof.
   eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
   exact symbol_address_inject.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
-  intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
 Qed.
 
-- 
cgit v1.2.3