From f774d5f2d604f747e72e2d3bb56cc3f90090e2dd Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 15 Feb 2013 16:24:13 +0000 Subject: Pointers one past git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Op.v | 88 +++++++++++++++++++++++++++------------------------------------ 1 file changed, 37 insertions(+), 51 deletions(-) (limited to 'ia32/Op.v') 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. - -- cgit v1.2.3