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 --- cfrontend/Cexec.v | 15 ++++-- cfrontend/Clight.v | 4 +- cfrontend/Ctypes.v | 33 ++++++------ cfrontend/Initializers.v | 7 +-- cfrontend/Initializersproof.v | 65 ++++------------------ cfrontend/SimplLocalsproof.v | 123 +++++++++++++++++++++++++++++------------- 6 files changed, 122 insertions(+), 125 deletions(-) (limited to 'cfrontend') 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. -- cgit v1.2.3