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

6 files changed, 122 insertions, 125 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 9593afd..d585760 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -465,8 +465,9 @@ Definition do_ef_free
 Definition memcpy_args_ok
   (sz al: Z) (bdst: block) (odst: Z) (bsrc: block) (osrc: Z) : Prop :=
       (al = 1 \/ al = 2 \/ al = 4 \/ al = 8)
-   /\ sz > 0
-   /\ (al | sz) /\ (al | osrc) /\ (al | odst)
+   /\ sz >= 0 /\ (al | sz)
+   /\ (sz > 0 -> (al | osrc))
+   /\ (sz > 0 -> (al | odst))
    /\ (bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc).
 
 Remark memcpy_check_args:
@@ -479,10 +480,14 @@ Proof with try (right; intuition omega).
     destruct (zeq al 4); auto. destruct (zeq al 8); auto...
   unfold memcpy_args_ok. destruct X...
   assert (al > 0) by (intuition omega).
-  destruct (zlt 0 sz)...
+  destruct (zle 0 sz)...
   destruct (Zdivide_dec al sz); auto...
-  destruct (Zdivide_dec al osrc); auto...
-  destruct (Zdivide_dec al odst); auto...
+  assert(U: forall x, {sz > 0 -> (al | x)} + {~(sz > 0 -> (al | x))}).
+    intros. destruct (zeq sz 0). 
+    left; intros; omegaContradiction.
+    destruct (Zdivide_dec al x); auto. right; red; intros. elim n0. apply H0. omega. 
+  destruct (U osrc); auto...
+  destruct (U odst); auto...
   assert (Y: {bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc}
            +{~(bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc)}).
     destruct (eq_block bsrc bdst); auto.
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index f402ac2..59c056d 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -220,8 +220,8 @@ Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int):
       assign_loc ty m b ofs v m'
   | assign_loc_copy: forall b' ofs' bytes m',
       access_mode ty = By_copy ->
-      (alignof_blockcopy ty | Int.unsigned ofs') ->
-      (alignof_blockcopy ty | Int.unsigned ofs) ->
+      (sizeof ty > 0 -> (alignof_blockcopy ty | Int.unsigned ofs')) ->
+      (sizeof ty > 0 -> (alignof_blockcopy ty | Int.unsigned ofs)) ->
       b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs
               \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs
               \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs' ->
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 2b409ab..ec4780e 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -251,10 +251,10 @@ Fixpoint sizeof (t: type) : Z :=
   | Tfloat F32 _ => 4
   | Tfloat F64 _ => 8
   | Tpointer _ _ => 4
-  | Tarray t' n _ => sizeof t' * Zmax 1 n
+  | Tarray t' n _ => sizeof t' * Zmax 0 n
   | Tfunction _ _ _ => 1
-  | Tstruct _ fld _ => align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
-  | Tunion _ fld _ => align (Zmax 1 (sizeof_union fld)) (alignof t)
+  | Tstruct _ fld _ => align (sizeof_struct fld 0) (alignof t)
+  | Tunion _ fld _ => align (sizeof_union fld) (alignof t)
   | Tcomp_ptr _ _ => 4
   end
 
@@ -271,25 +271,23 @@ with sizeof_union (fld: fieldlist) : Z :=
   end.
 
 Lemma sizeof_pos:
-  forall t, sizeof t > 0.
+  forall t, sizeof t >= 0
+with sizeof_struct_incr:
+  forall fld pos, pos <= sizeof_struct fld pos.
 Proof.
-Local Opaque alignof.
-  assert (X: forall n t, n > 0 -> align n (alignof t) > 0).
+- Local Opaque alignof.
+  assert (X: forall n t, n >= 0 -> align n (alignof t) >= 0).
   {
     intros. generalize (align_le n (alignof t) (alignof_pos t)). omega.
   }
   induction t; simpl; try xomega.
   destruct i; omega.
   destruct f; omega.
-  apply Zmult_gt_0_compat. auto. xomega.
-  apply X. xomega. 
-  apply X. xomega.
-Qed.
-
-Lemma sizeof_struct_incr:
-  forall fld pos, pos <= sizeof_struct fld pos.
-Proof.
-  induction fld; intros; simpl. omega. 
+  change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega. 
+  apply X. apply Zle_ge. apply sizeof_struct_incr. 
+  apply X. induction f; simpl; xomega.
+- induction fld; intros; simpl.
+  omega. 
   eapply Zle_trans. 2: apply IHfld.
   apply Zle_trans with (align pos (alignof t)). 
   apply align_le. apply alignof_pos.
@@ -318,9 +316,9 @@ Local Transparent alignof.
 - rewrite H; apply Zdivide_refl.
 - destruct H. rewrite H. apply Z.divide_mul_l; auto. 
 - apply Zdivide_refl.
-- change (alignof (Tstruct i f a) | align (Z.max 1 (sizeof_struct f 0)) (alignof (Tstruct i f a))).
+- change (alignof (Tstruct i f a) | align (sizeof_struct f 0) (alignof (Tstruct i f a))).
   apply align_divides. apply alignof_pos.
-- change (alignof (Tunion i f a) | align (Z.max 1 (sizeof_union f)) (alignof (Tunion i f a))).
+- change (alignof (Tunion i f a) | align (sizeof_union f) (alignof (Tunion i f a))).
   apply align_divides. apply alignof_pos.
 - rewrite H; apply Zdivide_refl.
 Qed.
@@ -376,7 +374,6 @@ Proof.
   split. auto.
 Local Opaque alignof. 
   simpl. eapply Zle_trans; eauto. 
-  apply Zle_trans with (Z.max 1 (sizeof_struct fld 0)). xomega. 
   apply align_le. apply alignof_pos. 
 Qed.
 
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index fa54627..1b339c1 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -175,12 +175,7 @@ Fixpoint transl_init (ty: type) (i: initializer)
   | Init_single a, _ =>
       do d <- transl_init_single ty a; OK (d :: nil)
   | Init_compound il, Tarray tyelt nelt _ =>
-      if zle nelt 0 then
-        OK (Init_space(sizeof ty) :: nil)
-      else
-        transl_init_array tyelt il nelt
-  | Init_compound il, Tstruct _ Fnil _ =>
-      OK (Init_space (sizeof ty) :: nil)
+      transl_init_array tyelt il (Zmax 0 nelt)
   | Init_compound il, Tstruct id fl _ =>
       transl_init_struct id ty fl il 0
   | Init_compound il, Tunion _ Fnil _ =>
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index b6fc728..ca2a40c 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -562,38 +562,6 @@ Proof.
   rewrite IHd1. omega.
 Qed.
 
-Remark sizeof_struct_incr:
-  forall fl pos, pos <= sizeof_struct fl pos.
-Proof.
-  induction fl; intros; simpl. 
-  omega.
-  eapply Zle_trans. apply align_le with (y := alignof t). apply alignof_pos.
-  eapply Zle_trans. 2: apply IHfl.
-  generalize (sizeof_pos t); omega.
-Qed.
-
-Remark sizeof_struct_eq:
-  forall id fl a,
-  fl <> Fnil ->
-  sizeof (Tstruct id fl a) = align (sizeof_struct fl 0) (alignof (Tstruct id fl a)).
-Proof.
-  intros. simpl. f_equal. rewrite Zmax_spec. apply zlt_false. 
-  destruct fl. congruence. simpl. 
-  apply Zle_ge. eapply Zle_trans. 2: apply sizeof_struct_incr. 
-  assert (0 <= align 0 (alignof t)). apply align_le. apply alignof_pos. 
-  generalize (sizeof_pos t). omega.
-Qed.
-
-Remark sizeof_union_eq:
-  forall id fl a,
-  fl <> Fnil ->
-  sizeof (Tunion id fl a) = align (sizeof_union fl) (alignof (Tunion id fl a)).
-Proof.
-  intros. simpl. f_equal. rewrite Zmax_spec. apply zlt_false. 
-  destruct fl. congruence. simpl. 
-  apply Zle_ge. apply Zmax_bound_l. generalize (sizeof_pos t). omega.
-Qed.
-
 Lemma transl_init_size:
   forall i ty data,
   transl_init ty i = OK data ->
@@ -622,28 +590,18 @@ Proof.
 + (* compound *)
   simpl in H. destruct ty; try discriminate.
 * (* compound array *)
-  set (sz := sizeof (Tarray ty z a)) in *.
-  destruct (zle z 0).
-  inv H. simpl. rewrite Z.max_l. omega.
-  generalize (sizeof_pos (Tarray ty z a)). unfold sz; omega.
-  unfold sz; simpl. rewrite Z.max_r by omega. 
-  eapply (proj1 (transl_init_list_size il)); eauto.
+  simpl. eapply (proj1 (transl_init_list_size il)); eauto.
 * (* compound struct *)
-  set (sz := sizeof (Tstruct i f a)) in *.
-  destruct f.
-  inv H. simpl. rewrite Z.max_l. omega. generalize (sizeof_pos (Tstruct i Fnil a)); unfold sz; omega. 
   replace (idlsize data) with (idlsize data + 0) by omega.
   eapply (proj1 (proj2 (transl_init_list_size il))). eauto.
-  rewrite sizeof_struct_eq. 2: congruence. 
-  apply align_le. apply alignof_pos.
+Local Opaque alignof.
+  simpl. apply align_le. apply alignof_pos.
 * (* compound union *)
   set (sz := sizeof (Tunion i f a)) in *.
   destruct f.
-  inv H. simpl. rewrite Z.max_l. omega. generalize (sizeof_pos (Tunion i Fnil a)); unfold sz; omega. 
+  inv H. simpl. assert (sz >= 0) by (apply sizeof_pos). xomega. 
   eapply (proj2 (proj2 (transl_init_list_size il))). eauto. 
-  rewrite sizeof_union_eq. 2: congruence. 
-  eapply Zle_trans. 2: apply align_le. simpl. apply Zmax_bound_l. omega. 
-  apply alignof_pos.
+  simpl. eapply Zle_trans. 2: apply align_le. xomega. apply alignof_pos. 
 
 - induction il.
 + (* base cases *)
@@ -730,10 +688,9 @@ Combined Scheme exec_init_scheme from exec_init_ind3, exec_init_array_ind3, exec
 
 Remark exec_init_array_length:
   forall m b ofs ty sz il m', 
-  exec_init_array m b ofs ty sz il m' ->
-  match il with Init_nil => sz = 0 | Init_cons _ _ => sz > 0 end.
+  exec_init_array m b ofs ty sz il m' -> sz >= 0.
 Proof.
-  induction 1. auto. destruct il; omega. 
+  induction 1; omega.
 Qed.
 
 Lemma store_init_data_list_app:
@@ -773,13 +730,9 @@ Local Opaque sizeof.
 - (* single *)
   monadInv H3. simpl. erewrite transl_init_single_steps by eauto. auto.
 - (* array *)
-  destruct (zle sz 0).
-  exploit exec_init_array_length; eauto. destruct il; intros.
-  subst. inv H. inv H1. auto. omegaContradiction.
-  eauto.
+  replace (Z.max 0 sz) with sz in H1. eauto.
+  assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega. 
 - (* struct *)
-  destruct fl.
-  inv H. inv H1. auto.
   replace ofs with (ofs + 0) by omega. eauto.
 - (* union *)
   monadInv H1. eapply store_init_data_list_app. eauto.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index ae98130..9b97b3b 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -1019,19 +1019,39 @@ Lemma assign_loc_inject:
       f b = None -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v).
 Proof.
   intros. inv H.
-  (* by value *)
+- (* by value *)
   exploit Mem.storev_mapped_inject; eauto. intros [tm' [A B]].
   exists tm'; split. eapply assign_loc_value; eauto. 
   split. auto.
   intros. rewrite <- H5. eapply Mem.load_store_other; eauto.
   left. inv H0. congruence.
-  (* by copy *)
+- (* by copy *)
   inv H0. inv H1.
   rename b' into bsrc. rename ofs'0 into osrc. 
   rename loc into bdst. rename ofs into odst.
   rename loc' into bdst'. rename b2 into bsrc'.
+  destruct (zeq (sizeof ty) 0).
++ (* special case size = 0 *)
+  assert (bytes = nil).
+  { exploit (Mem.loadbytes_empty m bsrc (Int.unsigned osrc) (sizeof ty)).
+    omega. congruence. }
+  subst.
+  destruct (Mem.range_perm_storebytes tm bdst' (Int.unsigned (Int.add odst (Int.repr delta))) nil)
+  as [tm' SB].
+  simpl. red; intros; omegaContradiction.
+  exists tm'.
+  split. eapply assign_loc_copy; eauto. 
+  intros; omegaContradiction.
+  intros; omegaContradiction.
+  rewrite e; right; omega.
+  apply Mem.loadbytes_empty. omega. 
+  split. eapply Mem.storebytes_empty_inject; eauto. 
+  intros. rewrite <- H0. eapply Mem.load_storebytes_other; eauto. 
+  left. congruence.
++ (* general case size > 0 *)
   exploit Mem.loadbytes_length; eauto. intros LEN.
-  assert (SZPOS: sizeof ty > 0) by apply sizeof_pos.
+  assert (SZPOS: sizeof ty > 0).
+  { generalize (sizeof_pos ty); omega. }
   assert (RPSRC: Mem.range_perm m bsrc (Int.unsigned osrc) (Int.unsigned osrc + sizeof ty) Cur Nonempty).
     eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem.
   assert (RPDST: Mem.range_perm m bdst (Int.unsigned odst) (Int.unsigned odst + sizeof ty) Cur Nonempty).
@@ -1048,10 +1068,10 @@ Proof.
   exploit Mem.storebytes_mapped_inject; eauto. intros [tm' [C D]].
   exists tm'. 
   split. eapply assign_loc_copy; try rewrite EQ1; try rewrite EQ2; eauto. 
-  eapply Mem.aligned_area_inject with (m := m); eauto.
+  intros; eapply Mem.aligned_area_inject with (m := m); eauto.
   apply alignof_blockcopy_1248.
   apply sizeof_alignof_blockcopy_compat.
-  eapply Mem.aligned_area_inject with (m := m); eauto.
+  intros; eapply Mem.aligned_area_inject with (m := m); eauto.
   apply alignof_blockcopy_1248.
   apply sizeof_alignof_blockcopy_compat.
   eapply Mem.disjoint_or_equal_inject with (m := m); eauto.
@@ -1218,24 +1238,66 @@ Proof.
   apply in_map. apply PTree.elements_correct. auto.
 Qed.
 
+Fixpoint freelist_no_overlap (l: list (block * Z * Z)) : Prop :=
+  match l with
+  | nil => True
+  | (b, lo, hi) :: l' =>
+      freelist_no_overlap l' /\
+      (forall b' lo' hi', In (b', lo', hi') l' ->
+       b' <> b \/ hi' <= lo \/ hi <= lo')
+  end.
+
 Lemma can_free_list:
   forall l m,
   (forall b lo hi, In (b, lo, hi) l -> Mem.range_perm m b lo hi Cur Freeable) ->
-  list_norepet (map (fun b_lo_hi => fst(fst b_lo_hi)) l) ->
+  freelist_no_overlap l ->
   exists m', Mem.free_list m l = Some m'.
 Proof.
   induction l; simpl; intros.
-  exists m; auto.
-  destruct a as [[b lo] hi]. simpl in H0. inv H0. 
+- exists m; auto.
+- destruct a as [[b lo] hi]. destruct H0.
   destruct (Mem.range_perm_free m b lo hi) as [m1 A]; auto. 
-  rewrite A. apply IHl; auto. intros. 
-  red; intros. eapply Mem.perm_free_1; eauto. 
-  left; red; intros. subst b0. elim H3.
-  set (F := fun b_lo_hi : block * Z * Z => fst (fst b_lo_hi)).
-  change b with (F (b,lo0,hi0)). eapply in_map; auto.
+  rewrite A. apply IHl; auto.
+  intros. red; intros. eapply Mem.perm_free_1; eauto. 
+  exploit H1; eauto. intros [B|B]. auto. right; omega.   
   eapply H; eauto. 
 Qed.
 
+Lemma blocks_of_env_no_overlap:
+  forall j cenv e le m lo hi te tle tlo thi tm,
+  match_envs j cenv e le m lo hi te tle tlo thi ->
+  Mem.inject j m tm ->
+  (forall id b ty, 
+   e!id = Some(b, ty) -> Mem.range_perm m b 0 (sizeof ty) Cur Freeable) ->
+  forall l,
+  list_norepet (List.map fst l) ->
+  (forall id bty, In (id, bty) l -> te!id = Some bty) ->
+  freelist_no_overlap (List.map block_of_binding l).
+Proof.
+  intros until tm; intros ME MINJ PERMS. induction l; simpl; intros.
+- auto.
+- destruct a as [id [b ty]]. simpl in *. inv H. split.
+  + apply IHl; auto.
+  + intros. exploit list_in_map_inv; eauto. intros [[id' [b'' ty']] [A B]].
+    simpl in A. inv A. rename b'' into b'. 
+    assert (TE: te!id = Some(b, ty)) by eauto. 
+    assert (TE': te!id' = Some(b', ty')) by eauto. 
+    exploit me_mapped. eauto. eexact TE. intros [b0 [INJ E]]. 
+    exploit me_mapped. eauto. eexact TE'. intros [b0' [INJ' E']]. 
+    destruct (zle (sizeof ty) 0); auto. 
+    destruct (zle (sizeof ty') 0); auto. 
+    assert (b0 <> b0').
+    { eapply me_inj; eauto. red; intros; subst; elim H3.
+      change id' with (fst (id', (b', ty'))). apply List.in_map; auto. }
+    assert (Mem.perm m b0 0 Max Nonempty). 
+    { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable.
+      eapply PERMS; eauto. omega. auto with mem. }
+    assert (Mem.perm m b0' 0 Max Nonempty). 
+    { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable.
+      eapply PERMS; eauto. omega. auto with mem. }
+    exploit Mem.mi_no_overlap; eauto. intros [A|A]. auto. omegaContradiction.
+Qed.
+
 Lemma free_list_right_inject:
   forall j m1 l m2 m2',
   Mem.inject j m1 m2 ->
@@ -1262,8 +1324,10 @@ Theorem match_envs_free_blocks:
   /\ Mem.inject j m' tm'.
 Proof.
   intros. 
-  assert (exists tm', Mem.free_list tm (blocks_of_env te) = Some tm').
+  assert (X: exists tm', Mem.free_list tm (blocks_of_env te) = Some tm').
+  {
     apply can_free_list.
+  - (* permissions *)
     intros. unfold blocks_of_env in H2.
     exploit list_in_map_inv; eauto. intros [[id [b' ty]] [EQ IN]].
     simpl in EQ; inv EQ. 
@@ -1272,30 +1336,13 @@ Proof.
     change 0 with (0 + 0). replace (sizeof ty) with (sizeof ty + 0) by omega.
     eapply Mem.range_perm_inject; eauto. 
     eapply free_blocks_of_env_perm_2; eauto.
-    (* no repetitions *)
-    set (F := fun id => match te!id with Some(b, ty) => b | None => xH end).
-    replace (map (fun b_lo_hi : block * Z * Z => fst (fst b_lo_hi)) (blocks_of_env te))
-       with (map F (map (fun x => fst x) (PTree.elements te))).
-    apply list_map_norepet. apply PTree.elements_keys_norepet. 
-    intros. 
-    exploit list_in_map_inv. eexact H2. intros [[id1 [b1' ty1]] [EQ1 IN1]].
-    exploit list_in_map_inv. eexact H3. intros [[id2 [b2' ty2]] [EQ2 IN2]].
-    simpl in *. subst x y.
-    assert (te!id1 = Some(b1', ty1)) by (apply PTree.elements_complete; auto).
-    assert (te!id2 = Some(b2', ty2)) by (apply PTree.elements_complete; auto).
-    exploit me_mapped. eauto. eexact H5. intros [b1 [P1 Q1]].
-    exploit me_mapped. eauto. eexact H6. intros [b2 [P2 Q2]].
-    assert (b1 <> b2) by (eapply me_inj; eauto). 
-    exploit Mem.mi_no_overlap; eauto. 
-    instantiate (1 := 0). apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
-    eapply free_blocks_of_env_perm_2; eauto. generalize (sizeof_pos ty1); omega.
-    instantiate (1 := 0). apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
-    eapply free_blocks_of_env_perm_2; eauto. generalize (sizeof_pos ty2); omega.
-    intros [A | A]; try omegaContradiction. 
-    unfold F. rewrite H5; rewrite H6. auto.
-    unfold blocks_of_env. repeat rewrite list_map_compose. apply list_map_exten; intros. 
-    unfold F. destruct x as [id [b ty]]. simpl. erewrite PTree.elements_complete; eauto. auto.
-  destruct H2 as [tm' FREE].
+  - (* no overlap *)
+    unfold blocks_of_env; eapply blocks_of_env_no_overlap; eauto. 
+    intros. eapply free_blocks_of_env_perm_2; eauto.
+    apply PTree.elements_keys_norepet.
+    intros. apply PTree.elements_complete; auto. 
+  }
+  destruct X as [tm' FREE].
   exists tm'; split; auto.
   eapply free_list_right_inject; eauto. 
   eapply Mem.free_list_left_inject; eauto.