Pointers one past

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

4 files changed, 334 insertions, 65 deletions

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. 
-