summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-11-06 10:39:43 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-11-06 10:39:43 +0000
commitf9c799143067c3197dc925f7fd916206d075a25d (patch)
treea7ecd744efdd58fe38cb7ef2a2e8a77c196797b8
parent61b43d3e1be5e8aad11cb3036fdb1872f0f363c3 (diff)
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
-rw-r--r--cfrontend/Cexec.v3
-rw-r--r--cfrontend/Cshmgenproof.v4
-rw-r--r--cfrontend/Ctypes.v173
-rw-r--r--cfrontend/Initializers.v14
-rw-r--r--cfrontend/Initializersproof.v120
-rw-r--r--cfrontend/SimplLocalsproof.v18
-rw-r--r--cparser/Cutil.ml27
-rw-r--r--cparser/Cutil.mli2
-rw-r--r--test/regression/Makefile2
-rw-r--r--test/regression/Results/alignas9
-rw-r--r--test/regression/alignas.c95
11 files changed, 320 insertions, 147 deletions
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.
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 982bf78..cae831d 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -79,8 +79,21 @@ let rec remove_custom_attributes (names: string list) (al: attributes) =
| a :: tl ->
a :: remove_custom_attributes names tl
+(* Is an attribute type-related (true) or variable-related (false)? *)
+
+let attr_is_type_related = function
+ | Attr(("packed" | "__packed__"), _) -> true
+ | _ -> false
+
+(* Is an attribute applicable to a whole array (true) or only to
+ array elements (false)? *)
+
+let attr_array_applicable = function
+ | AConst | AVolatile | ARestrict | AAlignas _ -> false
+ | Attr _ -> true
+
(* Adding top-level attributes to a type. Doesn't need to unroll defns. *)
-(* Array types cannot carry attributes, so add them to the element type. *)
+(* For array types, standard attrs are pushed to the element type. *)
let rec add_attributes_type attr t =
match t with
@@ -88,7 +101,9 @@ let rec add_attributes_type attr t =
| TInt(ik, a) -> TInt(ik, add_attributes attr a)
| TFloat(fk, a) -> TFloat(fk, add_attributes attr a)
| TPtr(ty, a) -> TPtr(ty, add_attributes attr a)
- | TArray(ty, sz, a) -> TArray(add_attributes_type attr ty, sz, a)
+ | TArray(ty, sz, a) ->
+ let (attr_arr, attr_elt) = List.partition attr_array_applicable attr in
+ TArray(add_attributes_type attr_elt ty, sz, add_attributes attr_arr a)
| TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, add_attributes attr
a)
| TNamed(s, a) -> TNamed(s, add_attributes attr a)
@@ -133,7 +148,7 @@ let rec change_attributes_type env (f: attributes -> attributes) t =
| TFloat(fk, a) -> TFloat(fk, f a)
| TPtr(ty, a) -> TPtr(ty, f a)
| TArray(ty, sz, a) ->
- TArray(change_attributes_type env f ty, sz, a)
+ TArray(change_attributes_type env f ty, sz, f a)
| TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, f a)
| TNamed(s, a) ->
let t1 = unroll env t in
@@ -149,12 +164,6 @@ let remove_attributes_type env attr t =
let erase_attributes_type env t =
change_attributes_type env (fun a -> []) t
-(* Is an attribute type-related (true) or variable-related (false)? *)
-
-let attr_is_type_related = function
- | Attr(("packed" | "__packed__"), _) -> true
- | _ -> false
-
(* Extracting alignment value from a set of attributes. Return 0 if none. *)
let alignas_attribute al =
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 98ab54e..35f7338 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -53,7 +53,7 @@ val erase_attributes_type : Env.t -> typ -> typ
val change_attributes_type : Env.t -> (attributes -> attributes) -> typ -> typ
(* Apply the given function to the top-level attributes of the given type *)
val attr_is_type_related: attribute -> bool
-(* Is an attribute type-related (true) or variable-related (false)? *)
+ (* Is an attribute type-related (true) or variable-related (false)? *)
(* Type compatibility *)
val compatible_types : ?noattrs: bool -> Env.t -> typ -> typ -> bool
diff --git a/test/regression/Makefile b/test/regression/Makefile
index a37f901..8dc7678 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -17,7 +17,7 @@ TESTS=int32 int64 floats floats-basics \
TESTS_COMP=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \
bitfields5 bitfields6 bitfields7 bitfields8 \
- builtins-$(ARCH) packedstruct1 packedstruct2
+ builtins-$(ARCH) packedstruct1 packedstruct2 alignas
# Can run, both in compiled mode and in interpreter mode,
# but produce processor-dependent results, so no reference output in Results
diff --git a/test/regression/Results/alignas b/test/regression/Results/alignas
new file mode 100644
index 0000000..1fc87a4
--- /dev/null
+++ b/test/regression/Results/alignas
@@ -0,0 +1,9 @@
+a: size = 4, alignment = 16, address mod 16 = 0
+b: size = 12, alignment = 16, address mod 16 = 0
+bb: size = 12, alignment = 16, address mod 16 = 0
+c: size = 32, alignment = 16, address mod 16 = 0
+d: size = 32, alignment = 32, address mod 32 = 0
+e: size = 16, alignment = 16, address mod 16 = 0
+f: size = 32, alignment = 32, address mod 32 = 0
+g: size = 96, alignment = 16, address mod 16 = 0
+h: size = 192, alignment = 64, address mod 64 = 0
diff --git a/test/regression/alignas.c b/test/regression/alignas.c
new file mode 100644
index 0000000..4e887d3
--- /dev/null
+++ b/test/regression/alignas.c
@@ -0,0 +1,95 @@
+/* _Alignas and its interactions with sizeof */
+
+#include <stdio.h>
+
+#if __STDC_VERSION__ < 201100 && defined(__GNUC__)
+#define _Alignas(x) __attribute__((aligned(x)))
+#define _Alignof(x) __alignof__(x)
+#endif
+
+/* Base type */
+int _Alignas(16) a;
+char filler1;
+
+/* Array */
+_Alignas(16) int b[3];
+
+typedef int int3[3];
+_Alignas(16) int3 bb;
+
+#if 0
+typedef _Alignas(16) int int16;
+int16 bbb[3];
+#endif
+
+char filler2;
+
+/* Struct */
+struct s {
+ char y;
+ int _Alignas(16) x;
+};
+
+struct s c;
+char filler3;
+
+struct s _Alignas(32) d;
+char filler4;
+
+/* Union */
+union u {
+ int _Alignas(16) x;
+ char y;
+};
+
+union u e;
+char filler5;
+
+union u _Alignas(32) f;
+char filler6;
+
+/* Arrays of structs */
+
+struct s g[3];
+char filler7;
+
+struct _Alignas(64) ss {
+ char y;
+ int _Alignas(16) x;
+};
+
+struct ss h[3];
+char filler8;
+
+/* Test harness */
+
+int main()
+{
+ printf("a: size = %u, alignment = %u, address mod 16 = %u\n",
+ (unsigned) sizeof(a), (unsigned) _Alignof(a), ((unsigned) &a) & 0xF);
+ printf("b: size = %u, alignment = %u, address mod 16 = %u\n",
+ (unsigned) sizeof(b), (unsigned) _Alignof(b), ((unsigned) &b) & 0xF);
+ printf("bb: size = %u, alignment = %u, address mod 16 = %u\n",
+ (unsigned) sizeof(bb), (unsigned) _Alignof(bb), ((unsigned) &bb) & 0xF);
+#if 0
+ printf("bbb: size = %u, alignment = %u, address mod 16 = %u\n",
+ (unsigned) sizeof(bbb), (unsigned) _Alignof(bbb), ((unsigned) &bbb) & 0xF);
+#endif
+ printf("c: size = %u, alignment = %u, address mod 16 = %u\n",
+ (unsigned) sizeof(c), (unsigned) _Alignof(c), ((unsigned) &c) & 0xF);
+ printf("d: size = %u, alignment = %u, address mod 32 = %u\n",
+ (unsigned) sizeof(d), (unsigned) _Alignof(d), ((unsigned) &d) & 0x1F);
+ printf("e: size = %u, alignment = %u, address mod 16 = %u\n",
+ (unsigned) sizeof(e), (unsigned) _Alignof(e), ((unsigned) &e) & 0xF);
+ printf("f: size = %u, alignment = %u, address mod 32 = %u\n",
+ (unsigned) sizeof(f), (unsigned) _Alignof(f), ((unsigned) &f) & 0x1F);
+ printf("g: size = %u, alignment = %u, address mod 16 = %u\n",
+ (unsigned) sizeof(g), (unsigned) _Alignof(g), ((unsigned) &g) & 0xF);
+ printf("h: size = %u, alignment = %u, address mod 64 = %u\n",
+ (unsigned) sizeof(h), (unsigned) _Alignof(h), ((unsigned) &h) & 0x3F);
+ return 0;
+}
+
+
+
+