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/Ctypes.v | 173 +++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 121 insertions(+), 52 deletions(-) (limited to 'cfrontend/Ctypes.v') diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index abd015c8..c9ef996a 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. *) -- cgit