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

7 files changed, 138 insertions, 80 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index c1e3bd1..f2eb84f 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -246,10 +246,8 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val :=
   | _, _ => None
   end.
 
-Definition eval_compare_null (c: comparison) (n: int) : option val :=
-  if Int.eq n Int.zero 
-  then match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end
-  else None.
+Definition eval_compare_mismatch (c: comparison) : option val :=
+  match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end.
 
 Definition eval_binop
             (op: binary_operation) (arg1 arg2: val) (m: mem): option val :=
@@ -288,11 +286,15 @@ Definition eval_binop
   | Ocmp c, Vptr b1 n1, Vptr b2 n2 =>
       if valid_pointer m b1 (Int.signed n1)
       && valid_pointer m b2 (Int.signed n2) then
-        if eq_block b1 b2 then Some(Val.of_bool(Int.cmp c n1 n2)) else None
+        if eq_block b1 b2
+        then Some(Val.of_bool(Int.cmp c n1 n2))
+        else eval_compare_mismatch c
       else
         None
-  | Ocmp c, Vptr b1 n1, Vint n2 => eval_compare_null c n2
-  | Ocmp c, Vint n1, Vptr b2 n2 => eval_compare_null c n1
+  | Ocmp c, Vptr b1 n1, Vint n2 =>
+      if Int.eq n2 Int.zero then eval_compare_mismatch c else None
+  | Ocmp c, Vint n1, Vptr b2 n2 =>
+      if Int.eq n1 Int.zero then eval_compare_mismatch c else None
   | Ocmpu c, Vint n1, Vint n2 =>
       Some (Val.of_bool(Int.cmpu c n1 n2))
   | Ocmpf c, Vfloat f1, Vfloat f2 =>
diff --git a/backend/Op.v b/backend/Op.v
index 2094d59..b1136f9 100644
--- a/backend/Op.v
+++ b/backend/Op.v
@@ -117,10 +117,8 @@ Inductive addressing: Set :=
   operations such as division by zero.  [eval_condition] returns a boolean,
   [eval_operation] and [eval_addressing] return a value. *)
 
-Definition eval_compare_null (c: comparison) (n: int) : option bool :=
-  if Int.eq n Int.zero 
-  then match c with Ceq => Some false | Cne => Some true | _ => None end
-  else None.
+Definition eval_compare_mismatch (c: comparison) : option bool :=
+  match c with Ceq => Some false | Cne => Some true | _ => None end.
 
 Definition eval_condition (cond: condition) (vl: list val) (m: mem):
                option bool :=
@@ -130,18 +128,20 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem):
   | Ccomp c, Vptr b1 n1 :: Vptr b2 n2 :: nil =>
       if valid_pointer m b1 (Int.signed n1)
       && valid_pointer m b2 (Int.signed n2) then
-        if eq_block b1 b2 then Some (Int.cmp c n1 n2) else None
+        if eq_block b1 b2
+        then Some (Int.cmp c n1 n2)
+        else eval_compare_mismatch c
       else None
   | Ccomp c, Vptr b1 n1 :: Vint n2 :: nil =>
-      eval_compare_null c n2
+      if Int.eq n2 Int.zero then eval_compare_mismatch c else None
   | Ccomp c, Vint n1 :: Vptr b2 n2 :: nil =>
-      eval_compare_null c n1
+      if Int.eq n1 Int.zero then eval_compare_mismatch c else None
   | Ccompu c, Vint n1 :: Vint n2 :: nil =>
       Some (Int.cmpu c n1 n2)
   | Ccompimm c n, Vint n1 :: nil =>
       Some (Int.cmp c n1 n)
   | Ccompimm c n, Vptr b1 n1 :: nil =>
-      eval_compare_null c n
+      if Int.eq n Int.zero then eval_compare_mismatch c else None
   | Ccompuimm c n, Vint n1 :: nil =>
       Some (Int.cmpu c n1 n)
   | Ccompf c, Vfloat f1 :: Vfloat f2 :: nil =>
@@ -294,15 +294,13 @@ Ltac FuncInv :=
       idtac
   end.
 
-Remark eval_negate_compare_null:
-  forall c n b,
-  eval_compare_null c n = Some b ->
-  eval_compare_null (negate_comparison c) n = Some (negb b).
+Remark eval_negate_compare_mismatch:
+  forall c b,
+  eval_compare_mismatch c = Some b ->
+  eval_compare_mismatch (negate_comparison c) = Some (negb b).
 Proof.
-  intros until b. unfold eval_compare_null.
-  case (Int.eq n Int.zero). 
-  destruct c; intro EQ; simplify_eq EQ; intros; subst b; reflexivity.
-  intro; discriminate. 
+  intros until b. unfold eval_compare_mismatch.
+  destruct c; intro EQ; inv EQ; auto. 
 Qed.
 
 Lemma eval_negate_condition:
@@ -313,15 +311,16 @@ Proof.
   intros. 
   destruct cond; simpl in H; FuncInv; try subst b; simpl.
   rewrite Int.negate_cmp. auto.
-  apply eval_negate_compare_null; auto.
-  apply eval_negate_compare_null; auto.
+  destruct (Int.eq i Int.zero). apply eval_negate_compare_mismatch; auto. discriminate.
+  destruct (Int.eq i0 Int.zero). apply eval_negate_compare_mismatch; auto. discriminate.
   destruct (valid_pointer m b0 (Int.signed i) &&
             valid_pointer m b1 (Int.signed i0)).
   destruct (eq_block b0 b1). rewrite Int.negate_cmp. congruence.
-  discriminate. discriminate.
+  apply eval_negate_compare_mismatch; auto. 
+  discriminate.
   rewrite Int.negate_cmpu. auto.
   rewrite Int.negate_cmp. auto.
-  apply eval_negate_compare_null; auto.
+  destruct (Int.eq i Int.zero). apply eval_negate_compare_mismatch; auto. discriminate.
   rewrite Int.negate_cmpu. auto.
   auto.
   rewrite negb_elim. auto.
@@ -688,14 +687,21 @@ Definition eval_addressing_total
   | _, _ => Vundef
   end.
 
+Lemma eval_compare_mismatch_weaken:
+  forall c b,
+  eval_compare_mismatch c = Some b ->
+  Val.cmp_mismatch c = Val.of_bool b.
+Proof.
+  unfold eval_compare_mismatch. intros. destruct c; inv H; auto.
+Qed.
+
 Lemma eval_compare_null_weaken:
-  forall c i b,
-  eval_compare_null c i = Some b ->
-  (if Int.eq i Int.zero then Val.cmp_mismatch c else Vundef) = Val.of_bool b.
+  forall n c b,
+  (if Int.eq n Int.zero then eval_compare_mismatch c else None) = Some b ->
+  (if Int.eq n Int.zero then Val.cmp_mismatch c else Vundef) = Val.of_bool b.
 Proof.
-  unfold eval_compare_null. intros. 
-  destruct (Int.eq i Int.zero); try discriminate.
-  destruct c; try discriminate; inversion H; reflexivity.
+  intros. destruct (Int.eq n Int.zero). apply eval_compare_mismatch_weaken. auto.
+  discriminate.
 Qed.
 
 Lemma eval_condition_weaken:
@@ -709,7 +715,9 @@ Proof.
   try (apply eval_compare_null_weaken; auto).
   destruct (valid_pointer m b0 (Int.signed i) &&
             valid_pointer m b1 (Int.signed i0)).
-  unfold eq_block in H. destruct (zeq b0 b1); congruence.
+  unfold eq_block in H. destruct (zeq b0 b1).
+  congruence.
+  apply eval_compare_mismatch_weaken; auto.
   discriminate.
   symmetry. apply Val.notbool_negb_1. 
   symmetry. apply Val.notbool_negb_1. 
@@ -814,10 +822,8 @@ Proof.
   generalize H0.
   caseEq (valid_pointer m1 b0 (Int.signed i)); intro; simpl; try congruence.
   caseEq (valid_pointer m1 b1 (Int.signed i0)); intro; simpl; try congruence.
-  destruct (eq_block b0 b1); try congruence.
-  intro. inv H2. 
   rewrite (Mem.valid_pointer_lessdef _ _ _ _ MEM H1).
-  rewrite (Mem.valid_pointer_lessdef _ _ _ _ MEM H).
+  rewrite (Mem.valid_pointer_lessdef _ _ _ _ MEM H). simpl.
   auto.
 Qed.
 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 07c3e7b..8b4713d 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -808,16 +808,16 @@ Theorem eval_comp_ptr_int:
   forall le c a x1 x2 b y v,
   eval_expr ge sp e m le a (Vptr x1 x2) ->
   eval_expr ge sp e m le b (Vint y) ->
-  Cminor.eval_compare_null c y = Some v ->
+  (if Int.eq y Int.zero then Cminor.eval_compare_mismatch c else None) = Some v ->
   eval_expr ge sp e m le (comp c a b) v.
 Proof.
   intros until v.
   unfold comp; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. unfold Cminor.eval_compare_null in H1. unfold eval_compare_null.
-  destruct (Int.eq y Int.zero); try discriminate. 
+  EvalOp. simpl. destruct (Int.eq y Int.zero); try discriminate.
+  unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch.
   destruct c; try discriminate; auto.
-  EvalOp. simpl. unfold Cminor.eval_compare_null in H1. unfold eval_compare_null.
-  destruct (Int.eq y Int.zero); try discriminate. 
+  EvalOp. simpl. destruct (Int.eq y Int.zero); try discriminate.
+  unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch.
   destruct c; try discriminate; auto.
 Qed.
 
@@ -825,17 +825,17 @@ Theorem eval_comp_int_ptr:
   forall le c a x b y1 y2 v,
   eval_expr ge sp e m le a (Vint x) ->
   eval_expr ge sp e m le b (Vptr y1 y2) ->
-  Cminor.eval_compare_null c x = Some v ->
+  (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v ->
   eval_expr ge sp e m le (comp c a b) v.
 Proof.
   intros until v.
   unfold comp; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. unfold Cminor.eval_compare_null in H1. unfold eval_compare_null.
-  destruct (Int.eq x Int.zero); try discriminate. 
-  destruct c; simpl; try discriminate; auto.
-  EvalOp. simpl. unfold Cminor.eval_compare_null in H1. unfold eval_compare_null.
-  destruct (Int.eq x Int.zero); try discriminate. 
-  destruct c; simpl; try discriminate; auto.
+  EvalOp. simpl. destruct (Int.eq x Int.zero); try discriminate.
+  unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch.
+  destruct c; try discriminate; auto.
+  EvalOp. simpl. destruct (Int.eq x Int.zero); try discriminate.
+  unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch.
+  destruct c; try discriminate; auto.
 Qed.
 
 Theorem eval_comp_ptr_ptr:
@@ -849,11 +849,26 @@ Theorem eval_comp_ptr_ptr:
 Proof.
   intros until y2.
   unfold comp; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. rewrite H1. simpl. 
-  subst y1. rewrite dec_eq_true. 
+  EvalOp. simpl. rewrite H1. subst y1. rewrite dec_eq_true. 
   destruct (Int.cmp c x2 y2); reflexivity.
 Qed.
 
+Theorem eval_comp_ptr_ptr_2:
+  forall le c a x1 x2 b y1 y2 v,
+  eval_expr ge sp e m le a (Vptr x1 x2) ->
+  eval_expr ge sp e m le b (Vptr y1 y2) ->
+  valid_pointer m x1 (Int.signed x2) &&
+  valid_pointer m y1 (Int.signed y2) = true ->
+  x1 <> y1 ->
+  Cminor.eval_compare_mismatch c = Some v ->
+  eval_expr ge sp e m le (comp c a b) v.
+Proof.
+  intros until y2.
+  unfold comp; case (comp_match a b); intros; InvEval.
+  EvalOp. simpl. rewrite H1. rewrite dec_eq_false; auto.
+  destruct c; simpl in H3; inv H3; auto.
+Qed.
+
 Theorem eval_compu:
   forall le c a x b y,
   eval_expr ge sp e m le a (Vint x) ->
@@ -1133,7 +1148,9 @@ Proof.
   generalize H1; clear H1.
   case_eq (valid_pointer m b (Int.signed i) && valid_pointer m b0 (Int.signed i0)); intros.
   destruct (eq_block b b0); inv H2.
-  eapply eval_comp_ptr_ptr; eauto. discriminate.
+  eapply eval_comp_ptr_ptr; eauto.
+  eapply eval_comp_ptr_ptr_2; eauto.
+  discriminate.
   eapply eval_compu; eauto.
   eapply eval_compf; eauto.
 Qed.
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.
diff --git a/common/Mem.v b/common/Mem.v
index d369b80..35d93ed 100644
--- a/common/Mem.v
+++ b/common/Mem.v
@@ -1870,6 +1870,30 @@ Proof.
   eapply valid_pointer_inj; eauto.
 Qed.
 
+Lemma different_pointers_inject:
+  forall f m m' b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
+  mem_inject f m m' ->
+  b1 <> b2 ->
+  valid_pointer m b1 (Int.signed ofs1) = true ->
+  valid_pointer m b2 (Int.signed ofs2) = true ->
+  f b1 = Some (b1', delta1) ->
+  f b2 = Some (b2', delta2) ->
+  b1' <> b2' \/
+  Int.signed (Int.add ofs1 (Int.repr delta1)) <>
+  Int.signed (Int.add ofs2 (Int.repr delta2)).
+Proof.
+  intros. 
+  rewrite valid_pointer_valid_access in H1. 
+  rewrite valid_pointer_valid_access in H2. 
+  rewrite (address_inject _ _ _ _ _ _ _ _ H H1 H3). 
+  rewrite (address_inject _ _ _ _ _ _ _ _ H H2 H4). 
+  inv H1. simpl in H7. inv H2. simpl in H9.
+  exploit (mi_no_overlap _ _ _ H); eauto.
+  intros [A | [A | [A | [A | A]]]].
+  auto. omegaContradiction. omegaContradiction. 
+  right. omega. right. omega.
+Qed.
+
 (** Relation between injections and loads. *)
 
 Lemma load_inject: