From 51e8bc524d570439f868ec0bdbf718cb53ca7669 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 30 Dec 2013 16:37:05 +0000 Subject: Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union). __builtin_memcpy_aligned now supports the case sz = 0. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2392 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Events.v | 54 ++++++++++++++++++++++++++++----------- common/Memory.v | 78 ++++++++++++++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 111 insertions(+), 21 deletions(-) (limited to 'common') diff --git a/common/Events.v b/common/Events.v index cf57650..8b6d25f 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1230,8 +1230,9 @@ Qed. Inductive extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := | extcall_memcpy_sem_intro: forall bdst odst bsrc osrc m bytes m', - al = 1 \/ al = 2 \/ al = 4 \/ al = 8 -> sz > 0 -> - (al | sz) -> (al | Int.unsigned osrc) -> (al | Int.unsigned odst) -> + al = 1 \/ al = 2 \/ al = 4 \/ al = 8 -> sz >= 0 -> (al | sz) -> + (sz > 0 -> (al | Int.unsigned osrc)) -> + (sz > 0 -> (al | Int.unsigned odst)) -> bsrc <> bdst \/ Int.unsigned osrc = Int.unsigned odst \/ Int.unsigned osrc + sz <= Int.unsigned odst \/ Int.unsigned odst + sz <= Int.unsigned osrc -> @@ -1244,19 +1245,19 @@ Lemma extcall_memcpy_ok: extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None cc_default). Proof. intros. constructor. -(* return type *) +- (* return type *) intros. inv H. constructor. -(* change of globalenv *) +- (* change of globalenv *) intros. inv H1. econstructor; eauto. -(* valid blocks *) +- (* valid blocks *) intros. inv H. eauto with mem. -(* perms *) +- (* perms *) intros. inv H. eapply Mem.perm_storebytes_2; eauto. -(* readonly *) +- (* readonly *) intros. inv H. eapply Mem.storebytes_unchanged_on; eauto. intros; red; intros. elim H8. apply Mem.perm_cur_max. eapply Mem.storebytes_range_perm; eauto. -(* extensions *) +- (* extensions *) intros. inv H. inv H1. inv H13. inv H14. inv H10. inv H11. exploit Mem.loadbytes_length; eauto. intros LEN. @@ -1272,8 +1273,31 @@ Proof. eapply Mem.storebytes_range_perm; eauto. erewrite list_forall2_length; eauto. tauto. -(* injections *) +- (* injections *) intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12. + destruct (zeq sz 0). ++ (* special case sz = 0 *) + assert (bytes = nil). + { exploit (Mem.loadbytes_empty m1 bsrc (Int.unsigned osrc) sz). omega. congruence. } + subst. + destruct (Mem.range_perm_storebytes m1' b0 (Int.unsigned (Int.add odst (Int.repr delta0))) nil) + as [m2' SB]. + simpl. red; intros; omegaContradiction. + exists f, Vundef, m2'. + split. econstructor; eauto. + intros; omegaContradiction. + intros; omegaContradiction. + right; omega. + apply Mem.loadbytes_empty. omega. + split. auto. + split. eapply Mem.storebytes_empty_inject; eauto. + split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros. + congruence. + split. eapply Mem.storebytes_unchanged_on; eauto. + simpl; intros; omegaContradiction. + split. apply inject_incr_refl. + red; intros; congruence. ++ (* general case sz > 0 *) exploit Mem.loadbytes_length; eauto. intros LEN. assert (RPSRC: Mem.range_perm m1 bsrc (Int.unsigned osrc) (Int.unsigned osrc + sz) Cur Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. @@ -1291,11 +1315,11 @@ Proof. exploit Mem.storebytes_mapped_inject; eauto. intros [m2' [C D]]. exists f; exists Vundef; exists m2'. split. econstructor; try rewrite EQ1; try rewrite EQ2; eauto. - eapply Mem.aligned_area_inject with (m := m1); eauto. - eapply Mem.aligned_area_inject with (m := m1); eauto. + intros; eapply Mem.aligned_area_inject with (m := m1); eauto. + intros; eapply Mem.aligned_area_inject with (m := m1); eauto. eapply Mem.disjoint_or_equal_inject with (m := m1); eauto. apply Mem.range_perm_max with Cur; auto. - apply Mem.range_perm_max with Cur; auto. + apply Mem.range_perm_max with Cur; auto. omega. split. constructor. split. auto. split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros. @@ -1308,13 +1332,13 @@ Proof. omega. split. apply inject_incr_refl. red; intros; congruence. -(* trace length *) +- (* trace length *) intros; inv H. simpl; omega. -(* receptive *) +- (* receptive *) intros. assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. -(* determ *) +- (* determ *) intros; inv H; inv H0. split. constructor. intros; split; congruence. Qed. diff --git a/common/Memory.v b/common/Memory.v index 1115ed7..79fc8a0 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -29,6 +29,7 @@ Require Import Zwf. Require Import Axioms. Require Import Coqlib. +Require Intv. Require Import Maps. Require Import AST. Require Import Integers. @@ -513,12 +514,21 @@ Proof. apply H. omega. apply IHn. intros. apply H. omega. Qed. +Remark getN_setN_disjoint: + forall vl q c n p, + Intv.disjoint (p, p + Z_of_nat n) (q, q + Z_of_nat (length vl)) -> + getN n p (setN vl q c) = getN n p c. +Proof. + intros. apply getN_exten. intros. apply setN_other. + intros; red; intros; subst r. eelim H; eauto. +Qed. + Remark getN_setN_outside: forall vl q c n p, p + Z_of_nat n <= q \/ q + Z_of_nat (length vl) <= p -> getN n p (setN vl q c) = getN n p c. Proof. - intros. apply getN_exten. intros. apply setN_outside. omega. + intros. apply getN_setN_disjoint. apply Intv.disjoint_range. auto. Qed. Remark setN_default: @@ -1559,12 +1569,10 @@ Proof. red; eauto with mem. Qed. -Theorem loadbytes_storebytes_other: +Theorem loadbytes_storebytes_disjoint: forall b' ofs' len, len >= 0 -> - b' <> b - \/ ofs' + len <= ofs - \/ ofs + Z_of_nat (length bytes) <= ofs' -> + b' <> b \/ Intv.disjoint (ofs', ofs' + len) (ofs, ofs + Z_of_nat (length bytes)) -> loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len. Proof. intros. unfold loadbytes. @@ -1572,13 +1580,25 @@ Proof. rewrite pred_dec_true. rewrite storebytes_mem_contents. decEq. rewrite PMap.gsspec. destruct (peq b' b). subst b'. - apply getN_setN_outside. rewrite nat_of_Z_eq; auto. intuition congruence. + apply getN_setN_disjoint. rewrite nat_of_Z_eq; auto. intuition congruence. auto. red; auto with mem. apply pred_dec_false. red; intros; elim n. red; auto with mem. Qed. +Theorem loadbytes_storebytes_other: + forall b' ofs' len, + len >= 0 -> + b' <> b + \/ ofs' + len <= ofs + \/ ofs + Z_of_nat (length bytes) <= ofs' -> + loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len. +Proof. + intros. apply loadbytes_storebytes_disjoint; auto. + destruct H0; auto. right. apply Intv.disjoint_range; auto. +Qed. + Theorem load_storebytes_other: forall chunk b' ofs', b' <> b @@ -2599,6 +2619,31 @@ Proof. eauto with mem. Qed. +Lemma storebytes_empty_inj: + forall f m1 b1 ofs1 m1' m2 b2 ofs2 m2', + mem_inj f m1 m2 -> + storebytes m1 b1 ofs1 nil = Some m1' -> + storebytes m2 b2 ofs2 nil = Some m2' -> + mem_inj f m1' m2'. +Proof. + intros. destruct H. constructor. +(* perm *) + intros. + eapply perm_storebytes_1; eauto. + eapply mi_perm0; eauto. + eapply perm_storebytes_2; eauto. +(* align *) + intros. eapply mi_align0 with (ofs := ofs) (p := p); eauto. + red; intros. eapply perm_storebytes_2; eauto. +(* mem_contents *) + intros. + assert (perm m1 b0 ofs Cur Readable). eapply perm_storebytes_2; eauto. + rewrite (storebytes_mem_contents _ _ _ _ _ H0). + rewrite (storebytes_mem_contents _ _ _ _ _ H1). + simpl. rewrite ! PMap.gsspec. + destruct (peq b0 b1); destruct (peq b3 b2); subst; eapply mi_memval0; eauto. +Qed. + (** Preservation of allocations *) Lemma alloc_right_inj: @@ -3583,6 +3628,27 @@ Proof. auto. Qed. +Theorem storebytes_empty_inject: + forall f m1 b1 ofs1 m1' m2 b2 ofs2 m2', + inject f m1 m2 -> + storebytes m1 b1 ofs1 nil = Some m1' -> + storebytes m2 b2 ofs2 nil = Some m2' -> + inject f m1' m2'. +Proof. + intros. inversion H. constructor; intros. +(* inj *) + eapply storebytes_empty_inj; eauto. +(* freeblocks *) + intros. apply mi_freeblocks0. red; intros; elim H2; eapply storebytes_valid_block_1; eauto. +(* mappedblocks *) + intros. eapply storebytes_valid_block_1; eauto. +(* no overlap *) + red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. +(* representable *) + intros. eapply mi_representable0; eauto. + destruct H3; eauto using perm_storebytes_2. +Qed. + (* Preservation of allocations *) Theorem alloc_right_inject: -- cgit v1.2.3