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 --- cfrontend/Cminorgenproof.v | 41 ++++++++++++++++++++++++--------------- cfrontend/Cop.v | 29 ++++++++++++++-------------- cfrontend/Cshmgenproof.v | 3 ++- cfrontend/Initializersproof.v | 15 ++++++++++++--- cfrontend/SimplLocalsproof.v | 45 ++++++++++++++++++++++++++----------------- 5 files changed, 82 insertions(+), 51 deletions(-) (limited to 'cfrontend') 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: -- cgit v1.2.3