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 --- arm/Op.v | 123 ++++++++++++++++++++++++--------------------------------------- 1 file changed, 46 insertions(+), 77 deletions(-) (limited to 'arm/Op.v') diff --git a/arm/Op.v b/arm/Op.v index f26bcccc..291d64f1 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -697,10 +697,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: @@ -728,25 +734,6 @@ 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. - -Remark val_sub_inj: - forall v1 v1' v2 v2', - val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.sub v1 v2) (Val.sub v1' v2'). -Proof. - intros. inv H; inv H0; simpl; auto. - econstructor; eauto. rewrite Int.sub_add_l. auto. - destruct (zeq b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite zeq_true. - rewrite Int.sub_shifted. auto. -Qed. - Remark eval_shift_inj: forall s v v', val_inject f v v' -> val_inject f (eval_shift s v) (eval_shift s v'). Proof. @@ -759,45 +746,13 @@ Lemma eval_condition_inj: eval_condition cond vl1 m1 = Some b -> eval_condition cond vl2 m2 = Some b. Proof. -Opaque Int.add. - assert (CMP: - forall c v1 v2 v1' v2' b, - val_inject f v1 v1' -> - val_inject f v2 v2' -> - Val.cmp_bool c v1 v2 = Some b -> - Val.cmp_bool c v1' v2' = Some b). - intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto. - - 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. - eapply CMP; eauto. - eapply CMPU; eauto. - eapply CMP. eauto. eapply eval_shift_inj. eauto. auto. - eapply CMPU. eauto. eapply eval_shift_inj. eauto. auto. - eapply CMP; try eassumption; eauto. - eapply CMPU; try eassumption; eauto. + eauto 4 using val_cmp_bool_inject. + eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies. + eauto using val_cmp_bool_inject, eval_shift_inj. + eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies, eval_shift_inj. + eauto 4 using val_cmp_bool_inject. + eauto 4 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. inv H3; simpl in H0; inv H0; auto. @@ -819,15 +774,15 @@ Lemma eval_operation_inj: exists v2, eval_operation genv sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. Proof. intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. - apply val_add_inj; auto. - apply val_add_inj; auto. - apply val_add_inj; auto. apply eval_shift_inj; 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 eval_shift_inj; auto. + apply Values.val_add_inject; auto. - apply val_sub_inj; auto. - apply val_sub_inj; auto. apply eval_shift_inj; auto. - apply val_sub_inj; auto. apply eval_shift_inj; auto. - apply (@val_sub_inj (Vint i) (Vint i) v v'); auto. + apply Values.val_sub_inject; auto. + apply Values.val_sub_inject; auto. apply eval_shift_inj; auto. + apply Values.val_sub_inject; auto. apply eval_shift_inj; auto. + apply (@Values.val_sub_inject f (Vint i) (Vint i) v v'); auto. inv H4; inv H2; simpl; auto. inv H4; inv H3; simpl in H1; inv H1. simpl. @@ -888,10 +843,10 @@ Proof. val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs)). exact symbol_address_inj. 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 eval_shift_inj; 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 eval_shift_inj; auto. + apply Values.val_add_inject; auto. Qed. End EVAL_COMPAT. @@ -913,10 +868,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. @@ -944,7 +909,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. @@ -963,7 +929,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. @@ -1019,7 +986,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. @@ -1051,7 +1019,8 @@ 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. -- cgit