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

2 files changed, 111 insertions, 21 deletions

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: