Pointers one past

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

1 files changed, 37 insertions, 51 deletions

diff --git a/ia32/Op.v b/ia32/Op.v
index 93a867a..66ee633 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -722,10 +722,16 @@ Hypothesis valid_pointer_inj:
   Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
 
-Hypothesis valid_pointer_no_overflow:
+Hypothesis weak_valid_pointer_inj:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_pointer_no_overflow:
+  forall b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 
 Hypothesis valid_different_pointers_inj:
@@ -753,50 +759,17 @@ Ltac InvInject :=
   | _ => idtac
   end.
 
-Remark val_add_inj:
-  forall v1 v1' v2 v2',
-  val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.add v1 v2) (Val.add v1' v2').
-Proof.
-  intros. inv H; inv H0; simpl; econstructor; eauto. 
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-Qed.
-
 Lemma eval_condition_inj:
   forall cond vl1 vl2 b,
   val_list_inject f vl1 vl2 ->
   eval_condition cond vl1 m1 = Some b ->
   eval_condition cond vl2 m2 = Some b.
 Proof.
-Opaque Int.add.
-  assert (CMPU:
-    forall c v1 v2 v1' v2' b,
-    val_inject f v1 v1' ->
-    val_inject f v2 v2' ->
-    Val.cmpu_bool (Mem.valid_pointer m1) c v1 v2 = Some b ->
-    Val.cmpu_bool (Mem.valid_pointer m2) c v1' v2' = Some b).
-  intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
-  destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
-  destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
-  rewrite (valid_pointer_inj _ H2 Heqb4).
-  rewrite (valid_pointer_inj _ H Heqb0). simpl.
-  destruct (zeq b1 b0); simpl in H1.
-  inv H1. rewrite H in H2; inv H2. rewrite zeq_true. 
-  decEq. apply Int.translate_cmpu.
-  eapply valid_pointer_no_overflow; eauto.
-  eapply valid_pointer_no_overflow; eauto.
-  exploit valid_different_pointers_inj; eauto. intros P.
-  destruct (zeq b2 b3); auto.
-  destruct P. congruence. 
-  destruct c; simpl in H1; inv H1.
-  simpl; decEq. rewrite Int.eq_false; auto. congruence.
-  simpl; decEq. rewrite Int.eq_false; auto. congruence.
-
   intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
-  eauto.
+  eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; simpl in H0; inv H0; auto.
-  eauto. 
+  eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
 Qed.
@@ -816,13 +789,13 @@ Lemma eval_addressing_inj:
   exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
 Proof.
   intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto. apply val_add_inj; auto.
-  apply val_add_inj; auto. inv H4; simpl; auto.
-  apply val_add_inj; auto. apply val_add_inj; auto. inv H2; simpl; auto.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto. inv H4; simpl; auto.
-  apply val_add_inj; auto.
+  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto. apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto. inv H4; simpl; auto.
+  apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. inv H2; simpl; auto.
+  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto. inv H4; simpl; auto.
+  apply Values.val_add_inject; auto.
 Qed.
 
 Lemma eval_operation_inj:
@@ -903,10 +876,20 @@ Proof.
   intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. 
 Qed.
 
-Remark valid_pointer_no_overflow_extends:
+Remark weak_valid_pointer_extends:
+  forall m1 m2, Mem.extends m1 m2 ->
+  forall b1 ofs b2 delta,
+  Some(b1, 0) = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+Proof.
+  intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto. 
+Qed.
+
+Remark weak_valid_pointer_no_overflow_extends:
   forall m1 b1 ofs b2 delta,
   Some(b1, 0) = Some(b2, delta) ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 Proof.
   intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2.
@@ -934,7 +917,8 @@ Lemma eval_condition_lessdef:
 Proof.
   intros. eapply eval_condition_inj with (f := fun b => Some(b, 0)) (m1 := m1).
   apply valid_pointer_extends; auto.
-  apply valid_pointer_no_overflow_extends; auto. 
+  apply weak_valid_pointer_extends; auto.
+  apply weak_valid_pointer_no_overflow_extends.
   apply valid_different_pointers_extends; auto.
   rewrite <- val_list_inject_lessdef. eauto. auto.
 Qed.
@@ -953,7 +937,8 @@ Proof.
   eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
   intros. rewrite <- val_inject_lessdef; auto.
   apply valid_pointer_extends; auto.
-  apply valid_pointer_no_overflow_extends; auto. 
+  apply weak_valid_pointer_extends; auto.
+  apply weak_valid_pointer_no_overflow_extends.
   apply valid_different_pointers_extends; auto.
   rewrite <- val_inject_lessdef; auto.
   eauto. auto. 
@@ -1009,7 +994,8 @@ Lemma eval_condition_inject:
 Proof.
   intros. eapply eval_condition_inj with (f := f) (m1 := m1); eauto.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
-  intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
 Qed.
 
@@ -1041,9 +1027,9 @@ Proof.
   eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
   exact symbol_address_inject.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
-  intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
 Qed.
 
 End EVAL_INJECT.
-