From f9c799143067c3197dc925f7fd916206d075a25d Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 6 Nov 2013 10:39:43 +0000 Subject: Revised treatment of _Alignas, for better compatibility with GCC and Clang, and to avoid wasting global variable space by inflating their sizeof needlessly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2362 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cexec.v | 3 +- cfrontend/Cshmgenproof.v | 4 +- cfrontend/Ctypes.v | 173 +++++++++++++++++++++++++++++------------- cfrontend/Initializers.v | 14 ++-- cfrontend/Initializersproof.v | 120 ++++++++++++++--------------- cfrontend/SimplLocalsproof.v | 18 +++-- 6 files changed, 196 insertions(+), 136 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index f83c700..03cab54 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -295,8 +295,7 @@ Remark check_assign_copy: { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }. Proof with try (right; intuition omega). intros. unfold assign_copy_ok. - assert (alignof_blockcopy ty > 0). - { unfold alignof_blockcopy. apply Z.min_case. omega. apply alignof_pos. } + assert (alignof_blockcopy ty > 0) by apply alignof_blockcopy_pos. destruct (Zdivide_dec (alignof_blockcopy ty) (Int.unsigned ofs')); auto... destruct (Zdivide_dec (alignof_blockcopy ty) (Int.unsigned ofs)); auto... assert (Y: {b' <> b \/ diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 7906944..1eb5830 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -658,8 +658,8 @@ Proof. econstructor. eauto. econstructor. eauto. constructor. econstructor; eauto. apply alignof_blockcopy_1248. - apply sizeof_pos. - eapply Zdivide_trans. apply alignof_blockcopy_divides. apply sizeof_alignof_compat. + apply sizeof_pos. + apply sizeof_alignof_blockcopy_compat. Qed. Lemma make_store_correct: diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index abd015c..c9ef996 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -160,7 +160,7 @@ Definition typeconv (ty: type) : type := (** * Operations over types *) -(** Natural alignment of a type, in bytes. *) +(** Alignment of a type, in bytes. *) Fixpoint alignof (t: type) : Z := match attr_alignas (attr_of_type t) with @@ -241,24 +241,22 @@ Qed. (** Size of a type, in bytes. *) Fixpoint sizeof (t: type) : Z := - let sz := - match t with - | Tvoid => 1 - | Tint I8 _ _ => 1 - | Tint I16 _ _ => 2 - | Tint I32 _ _ => 4 - | Tint IBool _ _ => 1 - | Tlong _ _ => 8 - | Tfloat F32 _ => 4 - | Tfloat F64 _ => 8 - | Tpointer _ _ => 4 - | Tarray t' n _ => sizeof t' * Zmax 1 n - | Tfunction _ _ => 1 - | Tstruct _ fld _ => Zmax 1 (sizeof_struct fld 0) - | Tunion _ fld _ => Zmax 1 (sizeof_union fld) - | Tcomp_ptr _ _ => 4 - end - in align sz (alignof t) + match t with + | Tvoid => 1 + | Tint I8 _ _ => 1 + | Tint I16 _ _ => 2 + | Tint I32 _ _ => 4 + | Tint IBool _ _ => 1 + | Tlong _ _ => 8 + | Tfloat F32 _ => 4 + | Tfloat F64 _ => 8 + | Tpointer _ _ => 4 + | Tarray t' n _ => sizeof t' * Zmax 1 n + | Tfunction _ _ => 1 + | Tstruct _ fld _ => align (Zmax 1 (sizeof_struct fld 0)) (alignof t) + | Tunion _ fld _ => align (Zmax 1 (sizeof_union fld)) (alignof t) + | Tcomp_ptr _ _ => 4 + end with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z := match fld with @@ -275,15 +273,17 @@ with sizeof_union (fld: fieldlist) : Z := Lemma sizeof_pos: forall t, sizeof t > 0. Proof. - assert (X: forall t sz, sz > 0 -> align sz (alignof t) > 0). +Local Opaque alignof. + assert (X: forall n t, n > 0 -> align n (alignof t) > 0). { - intros. generalize (align_le sz (alignof t) (alignof_pos t)). omega. + intros. generalize (align_le n (alignof t) (alignof_pos t)). omega. } -Local Opaque alignof. - induction t; simpl; apply X; try xomega. + 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: @@ -296,10 +296,33 @@ Proof. generalize (sizeof_pos t); omega. Qed. +Fixpoint naturally_aligned (t: type) : Prop := + match t with + | Tint _ _ a | Tlong _ a | Tfloat _ a | Tpointer _ a | Tcomp_ptr _ a => + attr_alignas a = None + | Tarray t' _ a => + attr_alignas a = None /\ naturally_aligned t' + | Tvoid | Tfunction _ _ | Tstruct _ _ _ | Tunion _ _ _ => + True + end. + Lemma sizeof_alignof_compat: - forall t, (alignof t | sizeof t). + forall t, naturally_aligned t -> (alignof t | sizeof t). Proof. - intros. destruct t; apply align_divides; apply alignof_pos. +Local Transparent alignof. + induction t; simpl; intros. +- apply Zdivide_refl. +- rewrite H. destruct i; apply Zdivide_refl. +- rewrite H; apply Zdivide_refl. +- rewrite H. destruct f; apply Zdivide_refl. +- 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))). + apply align_divides. apply alignof_pos. +- change (alignof (Tunion i f a) | align (Z.max 1 (sizeof_union f)) (alignof (Tunion i f a))). + apply align_divides. apply alignof_pos. +- rewrite H; apply Zdivide_refl. Qed. (** Byte offset for a field in a struct or union. @@ -350,8 +373,11 @@ Lemma field_offset_in_range: 0 <= ofs /\ ofs + sizeof ty <= sizeof (Tstruct sid fld a). Proof. intros. exploit field_offset_rec_in_range; eauto. intros [A B]. - split. auto. simpl. eapply Zle_trans. eauto. - eapply Zle_trans. eapply Zle_max_r. apply align_le. apply alignof_pos. + 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. (** Second, two distinct fields do not overlap *) @@ -531,7 +557,7 @@ Local Opaque alignof. /\ forall pos, sizeof_struct (unroll_composite_fields fld) pos = sizeof_struct fld pos)); simpl; intros; auto. -- rewrite H. rewrite <- (alignof_unroll_composite (Tarray t z a)). auto. +- rewrite H. auto. - rewrite <- (alignof_unroll_composite (Tstruct i f a)). simpl. destruct H. destruct (ident_eq i cid). auto. simpl. rewrite H0. auto. - rewrite <- (alignof_unroll_composite (Tunion i f a)). simpl. @@ -544,39 +570,82 @@ Qed. End UNROLL_COMPOSITE. -(** A variatn of [alignof] for use in block copy operations - (which do not support alignments greater than 8). *) +(** A variant of [alignof] for use in block copy operations. + Block copy operations do not support alignments greater than 8, + and require the size to be an integral multiple of the alignment. *) -Definition alignof_blockcopy (ty: type) := Zmin 8 (alignof ty). +Fixpoint alignof_blockcopy (t: type) : Z := + match t with + | Tvoid => 1 + | Tint I8 _ _ => 1 + | Tint I16 _ _ => 2 + | Tint I32 _ _ => 4 + | Tint IBool _ _ => 1 + | Tlong _ _ => 8 + | Tfloat F32 _ => 4 + | Tfloat F64 _ => 8 + | Tpointer _ _ => 4 + | Tarray t' _ _ => alignof_blockcopy t' + | Tfunction _ _ => 1 + | Tstruct _ fld _ => Zmin 8 (alignof t) + | Tunion _ fld _ => Zmin 8 (alignof t) + | Tcomp_ptr _ _ => 4 + end. Lemma alignof_blockcopy_1248: forall ty, let a := alignof_blockcopy ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8. Proof. - intros. unfold a, alignof_blockcopy. - destruct (alignof_two_p ty) as [n EQ]. rewrite EQ. - destruct n; auto. - destruct n; auto. - destruct n; auto. - right; right; right. apply Z.min_l. - rewrite two_power_nat_two_p. rewrite ! inj_S. - change 8 with (two_p 3). - apply two_p_monotone. omega. + assert (X: forall ty, let a := Zmin 8 (alignof ty) in + a = 1 \/ a = 2 \/ a = 4 \/ a = 8). + { + intros. destruct (alignof_two_p ty) as [n EQ]. unfold a; rewrite EQ. + destruct n; auto. + destruct n; auto. + destruct n; auto. + right; right; right. apply Z.min_l. + rewrite two_power_nat_two_p. rewrite ! inj_S. + change 8 with (two_p 3). apply two_p_monotone. omega. + } + induction ty; simpl; auto. + destruct i; auto. + destruct f; auto. Qed. -Lemma alignof_blockcopy_divides: - forall ty, (alignof_blockcopy ty | alignof ty). +Lemma alignof_blockcopy_pos: + forall ty, alignof_blockcopy ty > 0. Proof. - intros. unfold alignof_blockcopy. - destruct (alignof_two_p ty) as [n EQ]. rewrite EQ. - destruct n. apply Zdivide_refl. - destruct n. apply Zdivide_refl. - destruct n. apply Zdivide_refl. - replace (two_power_nat (S(S(S n)))) with (two_p (3 + Z.of_nat n)). - rewrite two_p_is_exp by omega. change (two_p 3) with 8. - apply Z.min_case. - exists (two_p (Z.of_nat n)). ring. + intros. generalize (alignof_blockcopy_1248 ty). simpl. intuition omega. +Qed. + +Lemma sizeof_alignof_blockcopy_compat: + forall ty, (alignof_blockcopy ty | sizeof ty). +Proof. + assert (X: forall ty sz, (alignof ty | sz) -> (Zmin 8 (alignof ty) | sz)). + { + intros. destruct (alignof_two_p ty) as [n EQ]. rewrite EQ in *. + destruct n; auto. + destruct n; auto. + destruct n; auto. + eapply Zdivide_trans; eauto. + apply Z.min_case. + replace (two_power_nat (S(S(S n)))) with (two_p (3 + Z.of_nat n)). + rewrite two_p_is_exp by omega. change (two_p 3) with 8. + exists (two_p (Z.of_nat n)). ring. + rewrite two_power_nat_two_p. rewrite !inj_S. f_equal. omega. + apply Zdivide_refl. + } + Local Opaque alignof. + induction ty; simpl. + apply Zdivide_refl. + destruct i; apply Zdivide_refl. + apply Zdivide_refl. + destruct f; apply Zdivide_refl. + apply Zdivide_refl. + apply Z.divide_mul_l. auto. + apply Zdivide_refl. + apply X. apply align_divides. apply alignof_pos. + apply X. apply align_divides. apply alignof_pos. apply Zdivide_refl. - rewrite two_power_nat_two_p. rewrite !inj_S. f_equal. omega. Qed. (** Extracting a type list from a function parameter declaration. *) diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index ec06cfd..fa54627 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -167,22 +167,18 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data := Return the corresponding list of initialization data. *) Definition padding (frm to: Z) : list init_data := - let n := to - frm in - if zle n 0 then nil else Init_space n :: nil. + if zlt frm to then Init_space (to - frm) :: nil else nil. Fixpoint transl_init (ty: type) (i: initializer) {struct i} : res (list init_data) := match i, ty with | Init_single a, _ => - do d <- transl_init_single ty a; - OK (d :: padding (Genv.init_data_size d) (sizeof ty)) - | Init_compound il, Tarray tyelt sz _ => - if zle sz 0 then + 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 - do dl <- transl_init_array tyelt il sz; - OK(let n := sizeof ty - sizeof tyelt * sz in - if zle n 0 then dl else dl ++ Init_space n :: nil) + transl_init_array tyelt il nelt | Init_compound il, Tstruct _ Fnil _ => OK (Init_space (sizeof ty) :: nil) | Init_compound il, Tstruct id fl _ => diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index ef9ec6c..5db4718 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -523,35 +523,36 @@ Qed. Lemma transl_init_single_size: forall ty a data, transl_init_single ty a = OK data -> - Genv.init_data_size data <= sizeof ty. -Proof with (simpl; apply align_le; apply alignof_pos). -Local Opaque alignof. + Genv.init_data_size data = sizeof ty. +Proof. intros. monadInv H. destruct x0. monadInv EQ2. destruct ty; try discriminate. - destruct i0; inv EQ2... - inv EQ2... - inv EQ2... - destruct ty; inv EQ2... + destruct i0; inv EQ2; auto. + inv EQ2; auto. + inv EQ2; auto. + destruct ty; inv EQ2; auto. destruct ty; try discriminate. - destruct f0; inv EQ2... + destruct f0; inv EQ2; auto. destruct ty; try discriminate. - destruct i0; inv EQ2... - inv EQ2... - inv EQ2... + destruct i0; auto. + inv EQ2. + inv EQ2. + inv EQ2; auto. + inv EQ2. + inv EQ2; auto. + inv EQ2; auto. Qed. Notation idlsize := Genv.init_data_list_size. Remark padding_size: - forall frm to, - frm <= to -> idlsize (padding frm to) = to - frm. + forall frm to, frm <= to -> idlsize (padding frm to) = to - frm. Proof. - intros. unfold padding. - destruct (zle (to - frm) 0). + unfold padding; intros. destruct (zlt frm to). + simpl. xomega. simpl. omega. - simpl. rewrite Zmax_spec. rewrite zlt_true. omega. omega. -Qed. +Qed. Remark idlsize_app: forall d1 d2, idlsize (d1 ++ d2) = idlsize d1 + idlsize d2. @@ -615,22 +616,19 @@ with transl_init_list_size: idlsize data = sizeof ty). Proof. - induction i; intros. - (* single *) - monadInv H. simpl. rewrite padding_size. omega. eapply transl_init_single_size; eauto. - (* compound *) +- induction i; intros. ++ (* single *) + monadInv H. simpl. erewrite transl_init_single_size by eauto. omega. ++ (* compound *) simpl in H. destruct ty; try discriminate. - (* compound array *) +* (* compound array *) set (sz := sizeof (Tarray ty z a)) in *. - destruct (zle z 0). inv H. simpl. rewrite Z.max_l. omega. + destruct (zle z 0). + inv H. simpl. rewrite Z.max_l. omega. generalize (sizeof_pos (Tarray ty z a)). unfold sz; omega. - monadInv H. exploit (proj1 (transl_init_list_size il)); eauto. intros SX. - assert (sizeof ty * z <= sz). - { unfold sz. simpl. rewrite Z.max_r. apply align_le; apply alignof_pos. omega. } - destruct (zle (sz - sizeof ty * z)). - omega. - rewrite idlsize_app. simpl. rewrite Z.max_l by omega. omega. - (* compound struct *) + unfold sz; simpl. rewrite Z.max_r by omega. + 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. @@ -638,7 +636,7 @@ Proof. eapply (proj1 (proj2 (transl_init_list_size il))). eauto. rewrite sizeof_struct_eq. 2: congruence. apply align_le. apply alignof_pos. - (* compound union *) +* (* 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. @@ -647,33 +645,33 @@ Proof. eapply Zle_trans. 2: apply align_le. simpl. apply Zmax_bound_l. omega. apply alignof_pos. - induction il. - (* base cases *) +- induction il. ++ (* base cases *) simpl. intuition. - (* arrays *) +* (* arrays *) destruct (zeq sz 0); inv H. simpl. ring. - (* structs *) +* (* structs *) destruct fl; inv H. - simpl in H0. generalize (padding_size pos (sizeof ty) H0). omega. - (* unions *) + simpl in H0. rewrite padding_size by omega. omega. +* (* unions *) inv H. - (* inductive cases *) - destruct IHil as [A [B C]]. split. - (* arrays *) ++ (* inductive cases *) + destruct IHil as [A [B C]]. split; [idtac|split]. +* (* arrays *) intros. monadInv H. - rewrite idlsize_app. + rewrite idlsize_app. rewrite (transl_init_size _ _ _ EQ). rewrite (A _ _ _ EQ1). ring. - (* structs *) - split. intros. simpl in H. destruct fl; monadInv H. - repeat rewrite idlsize_app. +* (* structs *) + intros. simpl in H. destruct fl; monadInv H. + rewrite ! idlsize_app. simpl in H0. rewrite padding_size. rewrite (transl_init_size _ _ _ EQ). rewrite <- (B _ _ _ _ _ EQ1). omega. auto. apply align_le. apply alignof_pos. - (* unions *) +* (* unions *) intros. simpl in H. monadInv H. rewrite idlsize_app. rewrite (transl_init_size _ _ _ EQ). @@ -754,7 +752,7 @@ Remark store_init_data_list_padding: forall frm to b ofs m, Genv.store_init_data_list ge m b ofs (padding frm to) = Some m. Proof. - intros. unfold padding. destruct (zle (to - frm) 0); auto. + intros. unfold padding. destruct (zlt frm to); auto. Qed. Lemma transl_init_sound_gen: @@ -770,40 +768,34 @@ Lemma transl_init_sound_gen: transl_init_struct id ty fl il pos = OK data -> Genv.store_init_data_list ge m b (ofs + pos) data = Some m'). Proof. +Local Opaque sizeof. apply exec_init_scheme; simpl; intros. - (* single *) - monadInv H3. - exploit transl_init_single_steps; eauto. intros. - simpl. rewrite H3. apply store_init_data_list_padding. - (* array *) +- (* 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. - monadInv H1. - change (align (sizeof ty * Z.max 1 sz) (alignof (Tarray ty sz a))) - with (sizeof (Tarray ty sz a)). - destruct (zle (sizeof (Tarray ty sz a) - sizeof ty * sz) 0). eauto. - eapply store_init_data_list_app; eauto. - (* struct *) +- (* 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. apply store_init_data_list_padding. +- (* union *) + monadInv H1. eapply store_init_data_list_app. eauto. + apply store_init_data_list_padding. - (* array, empty *) +- (* array, empty *) inv H. auto. - (* array, nonempty *) +- (* array, nonempty *) monadInv H3. eapply store_init_data_list_app. eauto. rewrite (transl_init_size _ _ _ EQ). eauto. - - (* struct, empty *) +- (* struct, empty *) destruct fl; simpl in H; inv H. inv H0. apply store_init_data_list_padding. - (* struct, nonempty *) +- (* struct, nonempty *) destruct fl; simpl in H3; inv H3. monadInv H4. eapply store_init_data_list_app. apply store_init_data_list_padding. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 62bbd67..8a26b08 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -764,9 +764,11 @@ Lemma sizeof_by_value: access_mode ty = By_value chunk -> size_chunk chunk <= sizeof ty. Proof. unfold access_mode; intros. -Local Opaque alignof. - destruct ty; try destruct i; try destruct s; try destruct f; inv H; - apply align_le; apply alignof_pos. + assert (size_chunk chunk = sizeof ty). + { + destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto. + } + omega. Qed. Definition env_initial_value (e: env) (m: mem) := @@ -1046,10 +1048,12 @@ 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. apply alignof_blockcopy_1248. - eapply Zdivide_trans. apply alignof_blockcopy_divides. apply sizeof_alignof_compat. - eapply Mem.aligned_area_inject with (m := m); eauto. apply alignof_blockcopy_1248. - eapply Zdivide_trans. apply alignof_blockcopy_divides. apply sizeof_alignof_compat. + 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. + apply alignof_blockcopy_1248. + apply sizeof_alignof_blockcopy_compat. eapply Mem.disjoint_or_equal_inject with (m := m); eauto. apply Mem.range_perm_max with Cur; auto. apply Mem.range_perm_max with Cur; auto. -- cgit v1.2.3