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.

2 files changed, 6 insertions, 3 deletions

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 *)