Merge pull request #31 from AbsInt/null-ptr-cmp

Revised semantics of comparisons between a pointer and 0.

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