Revised semantics of comparisons between a pointer and 0.

It used to be that a pointer value (Vptr) always compare unequal to the
null pointer (Vint Int.zero).  However, this may not be true in the
final machine code when pointer addition overflows and wraps around
to the bit pattern 0.  This patch checks the validity of the pointer
being compared with 0, and makes the comparison undefined if the
pointer is out of bounds.

Note: only the IA32 back-end was updated, ARM and PowerPC need updating.

9 files changed, 44 insertions, 31 deletions

diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index bb9bd592..20b6cf93 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -135,7 +135,7 @@ Proof.
   inv H. econstructor; eauto.
 (* default *)
   econstructor. constructor. eauto. constructor. 
-  simpl. inv H0. auto. auto. 
+  simpl. inv H0. auto. 
 Qed.
 
 Lemma eval_load:
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 92004a2f..ff3ccfa1 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -2121,12 +2121,14 @@ Proof.
   assert (IP: forall i b ofs,
     cmatch (Val.cmpu_bool valid c (Vint i) (Vptr b ofs)) (cmp_different_blocks c)).
   {
-    intros. simpl. destruct (Int.eq i Int.zero). apply cmp_different_blocks_sound. apply cmp_different_blocks_none.
+    intros. simpl. destruct (Int.eq i Int.zero && (valid b (Int.unsigned ofs) || valid b (Int.unsigned ofs - 1))).
+    apply cmp_different_blocks_sound. apply cmp_different_blocks_none.
   }
   assert (PI: forall i b ofs,
     cmatch (Val.cmpu_bool valid c (Vptr b ofs) (Vint i)) (cmp_different_blocks c)).
   {
-    intros. simpl. destruct (Int.eq i Int.zero). apply cmp_different_blocks_sound. apply cmp_different_blocks_none.
+    intros. simpl. destruct (Int.eq i Int.zero && (valid b (Int.unsigned ofs) || valid b (Int.unsigned ofs - 1))).
+    apply cmp_different_blocks_sound. apply cmp_different_blocks_none.
   }
   unfold cmpu_bool; inversion H; subst; inversion H0; subst;
   auto using cmatch_top, cmp_different_blocks_none, pcmp_none,
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 4e572277..b6b75abe 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -273,7 +273,6 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
   | cast_case_p2bool =>
       match v with
       | Vint i => Some (Vint (cast_int_int IBool Signed i))
-      | Vptr _ _ => Some (Vint Int.one)
       | _ => None
       end
   | cast_case_l2l =>
@@ -391,7 +390,6 @@ Definition bool_val (v: val) (t: type) : option bool :=
   | bool_case_p =>
       match v with
       | Vint n => Some (negb (Int.eq n Int.zero))
-      | Vptr b ofs => Some true
       | _ => None
       end
   | bool_case_l =>
@@ -426,7 +424,6 @@ Definition sem_notbool (v: val) (ty: type) : option val :=
   | bool_case_p =>
       match v with
       | Vint n => Some (Val.of_bool (Int.eq n Int.zero))
-      | Vptr _ _ => Some Vfalse
       | _ => None
       end
   | bool_case_l =>
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 7f61c657..847e4856 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -333,7 +333,6 @@ Proof.
   econstructor; split. econstructor; eauto with cshm. simpl. eauto. 
   unfold Val.cmpu, Val.cmpu_bool. simpl.
   destruct (Int.eq i Int.zero); simpl; constructor.
-  exists Vtrue; split. econstructor; eauto with cshm. constructor.
 (* long *)
   econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. 
   destruct (Int64.eq i Int64.zero); simpl; constructor. 
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 43d34007..bdeeff2a 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -1390,7 +1390,6 @@ Proof.
   destruct (Float.cmp Ceq f Float.zero); constructor; auto with ty.
   destruct (Float32.cmp Ceq f Float32.zero); constructor; auto with ty.
   destruct (Int.eq i Int.zero); constructor; auto with ty.
-  constructor; auto with ty.
   destruct (Int64.eq i Int64.zero); constructor; auto with ty.
 - (* notint *)
   unfold sem_notint in SEM; DestructCases; auto with ty.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 5cf59d94..3364ec6a 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -267,11 +267,8 @@ Proof.
   constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto.
   constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto.
   constructor. simpl. destruct (Int.eq i Int.zero); auto.
-  constructor; auto.
   constructor. simpl. destruct (Int.eq i Int.zero); auto.
-  constructor; auto.
   constructor. simpl. destruct (Int.eq i Int.zero); auto.
-  constructor; auto.
 (* long *)
   destruct ty; try (destruct f); try discriminate.
   destruct v; inv H. constructor.
diff --git a/common/Values.v b/common/Values.v
index a12fb636..e7dce7e9 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -111,15 +111,13 @@ Proof.
   simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto.
 Qed.
 
-(** Truth values.  Pointers and non-zero integers are treated as [True].
+(** Truth values.  Non-zero integers are treated as [True].
   The integer 0 (also used to represent the null pointer) is [False].
-  [Vundef] and floats are neither true nor false. *)
+  Other values are neither true nor false. *)
 
 Inductive bool_of_val: val -> bool -> Prop :=
   | bool_of_val_int:
-      forall n, bool_of_val (Vint n) (negb (Int.eq n Int.zero))
-  | bool_of_val_ptr:
-      forall b ofs, bool_of_val (Vptr b ofs) true.
+      forall n, bool_of_val (Vint n) (negb (Int.eq n Int.zero)).
 
 (** Arithmetic operations *)
 
@@ -695,7 +693,9 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool :=
   | Vint n1, Vint n2 =>
       Some (Int.cmpu c n1 n2)
   | Vint n1, Vptr b2 ofs2 =>
-      if Int.eq n1 Int.zero then cmp_different_blocks c else None
+      if Int.eq n1 Int.zero && weak_valid_ptr b2 (Int.unsigned ofs2)
+      then cmp_different_blocks c
+      else None
   | Vptr b1 ofs1, Vptr b2 ofs2 =>
       if eq_block b1 b2 then
         if weak_valid_ptr b1 (Int.unsigned ofs1)
@@ -708,7 +708,9 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool :=
         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
+      if Int.eq n2 Int.zero && weak_valid_ptr b1 (Int.unsigned ofs1)
+      then cmp_different_blocks c
+      else None
   | _, _ => None
   end.
 
@@ -1175,8 +1177,8 @@ Proof.
   destruct c; auto. 
   destruct x; destruct y; simpl; auto.
   rewrite Int.negate_cmpu. auto.
-  destruct (Int.eq i Int.zero); auto. 
-  destruct (Int.eq i0 Int.zero); auto.
+  destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto. 
+  destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto.
   destruct (eq_block 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))).
@@ -1222,8 +1224,8 @@ Proof.
     destruct c; auto.
   destruct x; destruct y; simpl; auto.
   rewrite Int.swap_cmpu. auto.
-  case (Int.eq i Int.zero); auto.
-  case (Int.eq i0 Int.zero); auto.
+  destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto.
+  destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto.
   destruct (eq_block b b0); subst.
   rewrite dec_eq_true.
   destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1));
@@ -1423,19 +1425,23 @@ Lemma cmpu_bool_lessdef:
   cmpu_bool valid_ptr' c v1' v2' = Some b.
 Proof.
   intros. 
+  assert (A: 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 v1; simpl in H2; try discriminate;
   destruct v2; simpl in H2; try discriminate;
   inv H0; inv H1; simpl; auto.
+  destruct (Int.eq i Int.zero && (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))) eqn:E; try discriminate.
+  InvBooleans. rewrite H0, A by auto. auto. 
+  destruct (Int.eq i0 Int.zero && (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1))) eqn:E; try discriminate.
+  InvBooleans. rewrite H0, A by auto. auto. 
   destruct (eq_block 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.
+  erewrite ! A by eauto. auto.
   destruct (valid_ptr b0 (Int.unsigned i)) eqn:?; try discriminate.
   destruct (valid_ptr b1 (Int.unsigned i0)) eqn:?; try discriminate.
-  erewrite !H by eauto. auto.
+  erewrite ! H by eauto. auto.
 Qed.
 
 Lemma of_optbool_lessdef:
@@ -1599,7 +1605,17 @@ Lemma val_cmpu_bool_inject:
 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 b1 (Int.unsigned ofs1)) in H1.
+  fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+  destruct (Int.eq i Int.zero); auto.
+  destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate.
+  erewrite weak_valid_ptr_inj by eauto. auto. 
+- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1.
+  fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+  destruct (Int.eq i Int.zero); auto.
+  destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate.
+  erewrite weak_valid_ptr_inj by eauto. 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)))). 
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 7d71d1a2..0ca343fb 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -462,12 +462,14 @@ Proof.
   rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity.
   destruct (Int.ltu i i0); reflexivity.
 (* int ptr *)
-  destruct (Int.eq i Int.zero) eqn:?; try discriminate.
+  destruct (Int.eq i Int.zero &&
+    (Mem.valid_pointer m b0 (Int.unsigned i0) || Mem.valid_pointer m b0 (Int.unsigned i0 - 1))) eqn:?; try discriminate.
   destruct c; simpl in *; inv H1.
   rewrite Heqb1; reflexivity. 
   rewrite Heqb1; reflexivity.
 (* ptr int *)
-  destruct (Int.eq i0 Int.zero) eqn:?; try discriminate.
+  destruct (Int.eq i0 Int.zero &&
+    (Mem.valid_pointer m b0 (Int.unsigned i) || Mem.valid_pointer m b0 (Int.unsigned i - 1))) eqn:?; try discriminate.
   destruct c; simpl in *; inv H1.
   rewrite Heqb1; reflexivity. 
   rewrite Heqb1; reflexivity.
diff --git a/ia32/Op.v b/ia32/Op.v
index 846d094f..ecc67c46 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -647,6 +647,7 @@ Definition is_trivial_op (op: operation) : bool :=
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
   | Ocmp (Ccompu _) => true
+  | Ocmp (Ccompuimm _ _) => true
   | _ => false
   end.
 
@@ -656,7 +657,7 @@ Lemma op_depends_on_memory_correct:
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
   intros until m2. destruct op; simpl; try congruence.
-  destruct c; simpl; try congruence. reflexivity. 
+  destruct c; simpl; auto; congruence.
 Qed.
 
 (** Global variables mentioned in an operation or addressing mode *)