Pointers one past

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

5 files changed, 82 insertions, 51 deletions

diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 9bbf040..a61808a 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1573,26 +1573,37 @@ Proof.
     apply val_inject_val_of_optbool.
     apply val_inject_val_of_optbool.
 Opaque Int.add.
-    unfold Val.cmpu. simpl. 
-    destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; simpl; auto.
-    destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; simpl; auto.
-    exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb. econstructor; eauto. 
-    intros V1. rewrite V1.
-    exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb0. econstructor; eauto. 
-    intros V2. rewrite V2. simpl.
-    destruct (zeq b1 b0).
+    unfold Val.cmpu. simpl.
+    destruct (zeq b1 b0); subst.
     (* same blocks *)
-    subst b1. rewrite H in H0; inv H0. rewrite zeq_true. 
-    rewrite Int.translate_cmpu. apply val_inject_val_of_optbool.
-    eapply Mem.valid_pointer_inject_no_overflow; eauto.
-    eapply Mem.valid_pointer_inject_no_overflow; eauto.
+    rewrite H0 in H. inv H. rewrite zeq_true.
+    fold (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)).
+    fold (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)).
+    fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+    fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs0 (Int.repr delta)))).
+    destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)) eqn:?; auto.
+    destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; auto.
+    rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb) by eauto.
+    rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0) by eauto.
+    rewrite Int.translate_cmpu
+      by eauto using Mem.weak_valid_pointer_inject_no_overflow.
+    apply val_inject_val_of_optbool.
     (* different source blocks *)
+    destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; auto.
+    destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; auto.
     destruct (zeq b2 b3).
-    exploit Mem.different_pointers_inject; eauto. intros [A|A]. 
-    congruence.
-    destruct c; simpl; auto. 
+    fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+    fold (Mem.weak_valid_pointer tm b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))).
+    rewrite Mem.valid_pointer_implies
+      by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb); eauto).
+    rewrite Mem.valid_pointer_implies
+      by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0); eauto).
+    exploit Mem.different_pointers_inject; eauto. intros [A|A]; [congruence |].
+    destruct c; simpl; auto.
     rewrite Int.eq_false. constructor. congruence.
     rewrite Int.eq_false. constructor. congruence.
+    rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb) by eauto.
+    rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0) by eauto.
     apply val_inject_val_of_optbool.
   (* cmpf *)
   inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 9d581b6..af7aaa8 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -714,13 +714,6 @@ Definition classify_cmp (ty1: type) (ty2: type) :=
   | _ , _ => cmp_default
   end.
 
-Function sem_cmp_mismatch (c: comparison): option val :=
-  match c with
-  | Ceq =>  Some Vfalse
-  | Cne =>  Some Vtrue
-  | _   => None
-  end.
-
 Function sem_cmp (c:comparison)
                   (v1: val) (t1: type) (v2: val) (t2: type)
                   (m: mem): option val :=
@@ -739,16 +732,24 @@ Function sem_cmp (c:comparison)
       match v1,v2 with
       | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
       | Vptr b1 ofs1,  Vptr b2 ofs2  =>
-          if Mem.valid_pointer m b1 (Int.unsigned ofs1)
-          && Mem.valid_pointer m b2 (Int.unsigned ofs2) then
-            if zeq b1 b2
+          if zeq b1 b2 then
+            if Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)
+               && Mem.weak_valid_pointer m b2 (Int.unsigned ofs2)
             then Some (Val.of_bool (Int.cmpu c ofs1 ofs2))
-            else sem_cmp_mismatch c
-          else None
+            else None
+          else
+            if Mem.valid_pointer m b1 (Int.unsigned ofs1)
+               && Mem.valid_pointer m b2 (Int.unsigned ofs2)
+            then option_map Val.of_bool (Val.cmp_different_blocks c)
+            else None
       | Vptr b ofs, Vint n =>
-          if Int.eq n Int.zero then sem_cmp_mismatch c else None
+          if Int.eq n Int.zero
+          then option_map Val.of_bool (Val.cmp_different_blocks c)
+          else None
       | Vint n, Vptr b ofs =>
-          if Int.eq n Int.zero then sem_cmp_mismatch c else None
+          if Int.eq n Int.zero
+          then option_map Val.of_bool (Val.cmp_different_blocks c)
+          else None
       | _,  _ => None
       end
   | cmp_case_ff =>
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 74a6da5..ad5ada6 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -574,7 +574,8 @@ Proof.
   inversion H8. eauto with cshm.
   (* pp ptr ptr *)
   inversion H10. eapply eval_Ebinop; eauto with cshm.
-  simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9. auto.
+  simpl. unfold Val.cmpu. simpl. unfold Mem.weak_valid_pointer in *. 
+  rewrite H3. rewrite H9. auto.
   inversion H10. eapply eval_Ebinop; eauto with cshm.
   simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9.
   destruct cmp; simpl in *; inv H; auto.
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index ca9c5b0..b64c309 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -380,6 +380,13 @@ Proof.
   eelim Mem.perm_empty; eauto. 
 Qed.
 
+Lemma mem_empty_not_weak_valid_pointer:
+  forall b ofs, Mem.weak_valid_pointer Mem.empty b ofs = false.
+Proof.
+  intros. unfold Mem.weak_valid_pointer.
+  now rewrite !mem_empty_not_valid_pointer.
+Qed.
+
 Lemma sem_cmp_match:
   forall c v1 ty1 v2 ty2 m v v1' v2' v',
   sem_cmp c v1 ty1 v2 ty2 Mem.empty = Some v ->
@@ -391,10 +398,12 @@ Opaque zeq.
   intros. unfold sem_cmp in *.
   destruct (classify_cmp ty1 ty2); try (destruct s); inv H1; inv H2; inv H; inv H0; auto with mval.
   destruct (Int.eq n Int.zero); try discriminate. 
-  unfold sem_cmp_mismatch in *. destruct c; inv H3; inv H2; constructor.
+  unfold Val.cmp_different_blocks in *. destruct c; inv H3; inv H2; constructor.
   destruct (Int.eq n Int.zero); try discriminate. 
-  unfold sem_cmp_mismatch in *. destruct c; inv H2; inv H1; constructor.
-  rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. discriminate.
+  unfold Val.cmp_different_blocks in *. destruct c; inv H2; inv H1; constructor.
+  rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4.
+  rewrite (mem_empty_not_weak_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. simpl in H4.
+  destruct (zeq (Z.pos id) (Z.pos id0)); discriminate.
 Qed.
 
 Lemma sem_binary_match:
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index c496a5e..e3aa4e2 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -1006,8 +1006,8 @@ Proof.
     apply RPSRC. omega.
   assert (PDST: Mem.perm m bdst (Int.unsigned odst) Cur Nonempty).
     apply RPDST. omega.
-  exploit Mem.address_inject.  eauto. apply Mem.perm_cur_max. eexact PSRC. eauto. intros EQ1.
-  exploit Mem.address_inject.  eauto. apply Mem.perm_cur_max. eexact PDST. eauto. intros EQ2.
+  exploit Mem.address_inject.  eauto. eexact PSRC. eauto. intros EQ1.
+  exploit Mem.address_inject.  eauto. eexact PDST. eauto. intros EQ2.
   exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]].
   exploit Mem.storebytes_mapped_inject; eauto. intros [tm' [C D]].
   exists tm'. 
@@ -1372,35 +1372,44 @@ Lemma sem_cmp_inject:
   exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 tm = Some tv /\ val_inject f v tv.
 Proof.
   unfold sem_cmp; intros. 
-  assert (MM: sem_cmp_mismatch cmp = Some v ->
-              exists tv, sem_cmp_mismatch cmp = Some tv /\ val_inject f v tv).
+  assert (MM: option_map Val.of_bool (Val.cmp_different_blocks cmp) = Some v ->
+      exists tv, option_map Val.of_bool (Val.cmp_different_blocks cmp) = Some tv /\ val_inject f v tv).
     intros. exists v; split; auto. 
     destruct cmp; simpl in H2; inv H2; auto.
 
   destruct (classify_cmp ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject.
   destruct (Int.eq i Int.zero); try discriminate; auto.
   destruct (Int.eq i Int.zero); try discriminate; auto.
-  destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
-  destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
-  simpl in H3.
-  rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb).
-  rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0).
-  simpl.
-  destruct (zeq b1 b0).  subst b1. rewrite H0 in H2; inv H2. rewrite zeq_true.
-  replace  (Int.cmpu cmp (Int.add ofs1 (Int.repr delta))
+
+  destruct (zeq b1 b0); subst.
+  rewrite H0 in H2. inv H2. rewrite zeq_true.
+  destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)) eqn:?; try discriminate.
+  destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
+  simpl H3.
+  rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb) by eauto.
+  rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0) by eauto.
+  simpl. replace  (Int.cmpu cmp (Int.add ofs1 (Int.repr delta))
                          (Int.add ofs0 (Int.repr delta)))
      with  (Int.cmpu cmp ofs1 ofs0).
   inv H3; TrivialInject.
   symmetry. apply Int.translate_cmpu. 
-  eapply Mem.valid_pointer_inject_no_overflow; eauto.
-  eapply Mem.valid_pointer_inject_no_overflow; eauto.
-  destruct (zeq b2 b3).
-  exploit Mem.different_pointers_inject; eauto. intros [A|A]. contradiction.
+  eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
+  eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
+  destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
+  destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
+  destruct (zeq b2 b3); subst.
+  rewrite Mem.valid_pointer_implies
+    by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb); eauto).
+  rewrite Mem.valid_pointer_implies
+    by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0); eauto).
+  simpl.
+  exploit Mem.different_pointers_inject; eauto. intros [[]|A]. easy.
   destruct cmp; simpl in H3; inv H3.
   simpl. unfold Int.eq. rewrite zeq_false; auto.
   simpl. unfold Int.eq. rewrite zeq_false; auto.
-  auto.
-  econstructor; eauto. econstructor; eauto. 
+  rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb) by eauto.
+  rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0) by eauto.
+  simpl in H3 |- *. auto.
 Qed.
 
 Lemma sem_binary_operation_inject: