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

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;
+}
+
+
+
+