Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs vers des blocs differents!

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

3 files changed, 37 insertions, 28 deletions

diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 54f5ceb..a603875 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -791,14 +791,22 @@ Proof.
   intros; destruct b; unfold Val.of_bool, Vtrue, Vfalse; constructor.
 Qed.
 
-Remark val_inject_eval_compare_null:
-  forall f c i v,  
-  eval_compare_null c i = Some v ->
+Remark val_inject_eval_compare_mismatch:
+  forall f c v,  
+  eval_compare_mismatch c = Some v ->
   val_inject f v v.
 Proof.
-  unfold eval_compare_null; intros.
-  destruct (Int.eq i Int.zero). 
+  unfold eval_compare_mismatch; intros.
   destruct c; inv H; unfold Vfalse, Vtrue; constructor.
+Qed.
+
+Remark val_inject_eval_compare_null:
+  forall f i c v,  
+  (if Int.eq i Int.zero then eval_compare_mismatch c else None) = Some v ->
+  val_inject f v v.
+Proof.
+  intros. destruct (Int.eq i Int.zero). 
+  eapply val_inject_eval_compare_mismatch; eauto. 
   discriminate.
 Qed.
 
@@ -820,17 +828,6 @@ Ltac TrivialOp :=
   | _ => idtac
   end.
 
-Remark eval_compare_null_inv:
-  forall c i v,
-  eval_compare_null c i = Some v ->
-  i = Int.zero /\ (c = Ceq /\ v = Vfalse \/ c = Cne /\ v = Vtrue).
-Proof.
-  intros until v. unfold eval_compare_null.
-  predSpec Int.eq Int.eq_spec i Int.zero.
-  case c; intro EQ; simplify_eq EQ; intro; subst v; tauto.
-  congruence.
-Qed.
-
 (** Correctness of [transl_constant]. *)
 
 Lemma transl_constant_correct:
@@ -921,22 +918,34 @@ Proof.
   (* cmp ptr ptr *)
   caseEq (valid_pointer m b1 (Int.signed ofs1) && valid_pointer m b0 (Int.signed ofs0)); 
   intro EQ; rewrite EQ in H4; try discriminate.
-  destruct (eq_block b1 b0); inv H4.
-  assert (b3 = b2) by congruence. subst b3.
-  assert (x0 = x) by congruence. subst x0.
   elim (andb_prop _ _ EQ); intros.
-  exists (Val.of_bool (Int.cmp c ofs1 ofs0)); split.
   exploit (Mem.valid_pointer_inject f m tm b0 ofs0); eauto. 
   intro VP; rewrite VP; clear VP.
-  exploit (Mem.valid_pointer_inject f m tm b0 ofs1); eauto. 
+  exploit (Mem.valid_pointer_inject f m tm b1 ofs1); eauto. 
   intro VP; rewrite VP; clear VP.
+  destruct (eq_block b1 b0); inv H4.
+  (* same blocks in source *)
+  assert (b3 = b2) by congruence. subst b3.
+  assert (x0 = x) by congruence. subst x0.
+  exists (Val.of_bool (Int.cmp c ofs1 ofs0)); split.
   unfold eq_block; rewrite zeq_true; simpl.
   decEq. decEq. rewrite Int.translate_cmp. auto. 
   eapply valid_pointer_inject_no_overflow; eauto.
   eapply valid_pointer_inject_no_overflow; eauto.
-  apply val_inject_val_of_bool. 
-  (* *)
+  apply val_inject_val_of_bool.
+  (* different blocks in source *)
+  simpl. exists v; split; [idtac | eapply val_inject_eval_compare_mismatch; eauto].
+  destruct (eq_block b2 b3); auto.
+  exploit different_pointers_inject; eauto. intros [A|A]. 
+  congruence.
+  decEq. destruct c; simpl in H6; inv H6; unfold Int.cmp.
+  predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr x)) (Int.add ofs0 (Int.repr x0)).
+  congruence. auto.
+  predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr x)) (Int.add ofs0 (Int.repr x0)).
+  congruence. auto.
+  (* cmpu *)
   inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  (* cmpf *)
   inv H0; try discriminate; inv H1; inv H; TrivialOp.
 Qed.
 
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 35d3cce..871f883 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -292,7 +292,7 @@ Function sem_cmp (c:comparison)
           && valid_pointer m b2 (Int.signed ofs2) then
             if zeq b1 b2
             then Some (Val.of_bool (Int.cmp c ofs1 ofs2))
-            else None
+            else sem_cmp_mismatch c
           else None
       | Vptr b ofs, Vint n =>
           if Int.eq n Int.zero then sem_cmp_mismatch c else None
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index f6bef93..2491e52 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -305,14 +305,14 @@ Proof.
   (* ipip ptr ptr *)
   inversion H10. eapply eval_Ebinop; eauto with cshm.
   simpl. rewrite H3. unfold eq_block. rewrite H9. auto.
+  inversion H10. eapply eval_Ebinop; eauto with cshm.
+  simpl. rewrite H3. unfold eq_block. rewrite H9. auto.
   (* ipip ptr int *)
   inversion H9. eapply eval_Ebinop; eauto with cshm.
-  simpl. unfold eval_compare_null. rewrite H8. 
-  functional inversion H; subst; auto.
+  simpl. rewrite H8. auto.
   (* ipip int ptr *)
   inversion H9. eapply eval_Ebinop; eauto with cshm.
-  simpl. unfold eval_compare_null. rewrite H8. 
-  functional inversion H; subst; auto.
+  simpl. rewrite H8. auto.
   (* ff *)
   inversion H8. eauto with cshm.
 Qed.