Merge of the "alignas" branch.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

11 files changed, 234 insertions, 137 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 20e00c8..dd9cfbf 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -206,9 +206,21 @@ let convertInt n = coqint_of_camlint(Int64.to_int32 n)
 
 (** Attributes *)
 
-let convertAttr a = List.mem AVolatile a
-
-let mergeAttr a1 a2 = a1 || a2
+let rec log2 n = if n = 1 then 0 else 1 + log2 (n lsr 1)
+
+let convertAttr a =
+  { attr_volatile = List.mem AVolatile a;
+    attr_alignas = 
+      let n = Cutil.alignas_attribute a in
+      if n > 0 then Some (N.of_int (log2 n)) else None }
+
+let mergeAttr a1 a2 =
+  { attr_volatile = a1.attr_volatile || a2.attr_volatile;
+    attr_alignas =
+      match a1.attr_alignas, a2.attr_alignas with
+      | None, aa -> aa
+      | aa, None -> aa
+      | Some n1, Some n2 -> Some (if N.le n1 n2 then n1 else n2) }
 
 let mergeTypAttr ty a2 =
   match ty with
@@ -340,9 +352,10 @@ let rec convertTypList env = function
   | t1 :: tl -> Tcons(convertTyp env t1, convertTypList env tl)
 
 let cacheCompositeDef env su id attr flds =
-  (* we currently ignore attributes on structs and unions *)
   let ty =
-    match su with C.Struct -> C.TStruct(id, []) | C.Union -> C.TUnion(id, []) in
+    match su with
+    | C.Struct -> C.TStruct(id, attr)
+    | C.Union  -> C.TUnion(id, attr) in
   Hashtbl.add compositeCache id (convertTyp env ty)
 
 let rec projFunType env ty =
@@ -821,6 +834,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
   let id' = intern_string id.name in
   let ty' = convertTyp env ty in 
   let sz = Ctypes.sizeof ty' in
+  let al = Ctypes.alignof ty' in
   let attr = Cutil.attributes_of_type env ty in
   let init' =
     match optinit with
@@ -828,10 +842,6 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
         if sto = C.Storage_extern then [] else [Init_space sz]
     | Some i ->
         convertInitializer env ty i in
-  let align =
-    match Cutil.find_custom_attributes ["aligned"; "__aligned__"] attr with
-    | [[C.AInt n]] -> Some(Int64.to_int n)
-    | _            -> Cutil.alignof env ty in
   let (section, near_access) =
     Sections.for_variable env id' ty (optinit <> None) in
   if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then
@@ -839,7 +849,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
                    id.name (Z.to_string sz));
   Hashtbl.add decl_atom id'
     { a_storage = sto;
-      a_alignment = align;
+      a_alignment = Some (Z.to_int al);
       a_sections = [section];
       a_small_data = near_access;
       a_inline = false;
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 70a02c1..f83c700 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -285,7 +285,7 @@ Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) : o
   end.
 
 Definition assign_copy_ok (ty: type) (b: block) (ofs: int) (b': block) (ofs': int) : Prop :=
-  (alignof ty | Int.unsigned ofs') /\ (alignof ty | Int.unsigned ofs) /\
+  (alignof_blockcopy ty | Int.unsigned ofs') /\ (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').
@@ -295,9 +295,10 @@ 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 ty > 0). apply alignof_pos; auto.
-  destruct (Zdivide_dec (alignof ty) (Int.unsigned ofs')); auto...
-  destruct (Zdivide_dec (alignof ty) (Int.unsigned ofs)); auto...
+  assert (alignof_blockcopy ty > 0).
+  { unfold alignof_blockcopy. apply Z.min_case. omega. apply alignof_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 \/
               Int.unsigned ofs' = Int.unsigned ofs \/
               Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 3bd06df..6a57999 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -218,7 +218,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 ty | Int.unsigned ofs') -> (alignof ty | Int.unsigned ofs) ->
+      (alignof_blockcopy ty | Int.unsigned ofs') ->
+      (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/Csem.v b/cfrontend/Csem.v
index 0f9b3f8..5d94c53 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -91,7 +91,8 @@ Inductive assign_loc {F V: Type} (ge: Genv.t F V) (ty: type) (m: mem) (b: block)
       assign_loc ge ty m b ofs v t m'
   | assign_loc_copy: forall b' ofs' bytes m',
       access_mode ty = By_copy ->
-      (alignof ty | Int.unsigned ofs') -> (alignof ty | Int.unsigned ofs) ->
+      (alignof_blockcopy ty | Int.unsigned ofs') ->
+      (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/Cshmgen.v b/cfrontend/Cshmgen.v
index a303a7f..fd34985 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -307,7 +307,7 @@ Definition make_load (addr: expr) (ty_res: type) :=
   by-copy assignment of a value of Clight type [ty]. *)
 
 Definition make_memcpy (dst src: expr) (ty: type) :=
-  Sbuiltin None (EF_memcpy (Ctypes.sizeof ty) (Ctypes.alignof ty))
+  Sbuiltin None (EF_memcpy (Ctypes.sizeof ty) (Ctypes.alignof_blockcopy ty))
                 (dst :: src :: nil).
 
 (** [make_store addr ty rhs] stores the value of the
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 24576fc..7906944 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -657,9 +657,9 @@ Proof.
   econstructor.
   econstructor. eauto. econstructor. eauto. constructor. 
   econstructor; eauto. 
-  apply alignof_1248.
+  apply alignof_blockcopy_1248.
   apply sizeof_pos. 
-  apply sizeof_alignof_compat.
+  eapply Zdivide_trans. apply alignof_blockcopy_divides. apply sizeof_alignof_compat.
 Qed.
  
 Lemma make_store_correct:
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 8d00b95..abd015c 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -45,14 +45,15 @@ Inductive floatsize : Type :=
   | F32: floatsize
   | F64: floatsize.
 
-(** Every type carries a set of attributes.  Currently, only one
-  attribute is modeled: [volatile]. *)
+(** Every type carries a set of attributes.  Currently, only two
+  attributes are modeled: [volatile] and [_Alignas(n)] (from ISO C 2011). *)
 
 Record attr : Type := mk_attr {
-  attr_volatile: bool
+  attr_volatile: bool;
+  attr_alignas: option N         (**r log2 of required alignment *)
 }.
 
-Definition noattr := {| attr_volatile := false |}.
+Definition noattr := {| attr_volatile := false; attr_alignas := None |}.
 
 (** The syntax of type expressions.  Some points to note:
 - Array types [Tarray n] carry the size [n] of the array.
@@ -113,10 +114,11 @@ Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2}
 with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2}
 with fieldlist_eq: forall (fld1 fld2: fieldlist), {fld1=fld2} + {fld1<>fld2}.
 Proof.
-  assert (forall (x y: intsize), {x=y} + {x<>y}). decide equality.
-  assert (forall (x y: signedness), {x=y} + {x<>y}). decide equality.
-  assert (forall (x y: floatsize), {x=y} + {x<>y}). decide equality.
-  assert (forall (x y: attr), {x=y} + {x<>y}). decide equality. apply bool_dec.
+  assert (forall (x y: intsize), {x=y} + {x<>y}) by decide equality.
+  assert (forall (x y: signedness), {x=y} + {x<>y}) by decide equality.
+  assert (forall (x y: floatsize), {x=y} + {x<>y}) by decide equality.
+  assert (forall (x y: attr), {x=y} + {x<>y}).
+  { decide equality. decide equality. apply N.eq_dec. apply bool_dec. }
   generalize ident_eq zeq. intros E1 E2. 
   decide equality.
   decide equality.
@@ -161,21 +163,25 @@ Definition typeconv (ty: type) : type :=
 (** Natural alignment of a type, in bytes. *)
 
 Fixpoint alignof (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 t'
-  | Tfunction _ _ => 1
-  | Tstruct _ fld _ => alignof_fields fld
-  | Tunion _ fld _ => alignof_fields fld
-  | Tcomp_ptr _ _ => 4
+  match attr_alignas (attr_of_type t) with
+  | Some l => two_p (Z.of_N l)
+  | None =>
+      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 t'
+      | Tfunction _ _ => 1
+      | Tstruct _ fld _ => alignof_fields fld
+      | Tunion _ fld _ => alignof_fields fld
+      | Tcomp_ptr _ _ => 4
+      end
   end
 
 with alignof_fields (f: fieldlist) : Z :=
@@ -187,49 +193,72 @@ with alignof_fields (f: fieldlist) : Z :=
 Scheme type_ind2 := Induction for type Sort Prop
   with fieldlist_ind2 := Induction for fieldlist Sort Prop.
 
-Lemma alignof_1248:
-  forall t, alignof t = 1 \/ alignof t = 2 \/ alignof t = 4 \/ alignof t = 8
-with alignof_fields_1248:
-  forall f, alignof_fields f = 1 \/ alignof_fields f = 2 \/ alignof_fields f = 4 \/ alignof_fields f = 8.
+Lemma alignof_two_p:
+  forall t, exists n, alignof t = two_power_nat n
+with alignof_fields_two_p:
+  forall f, exists n, alignof_fields f = two_power_nat n.
 Proof.
-  induction t; simpl; auto.
-  destruct i; auto.
-  destruct f; auto.
-  induction f; simpl; auto.
-  rewrite Zmax_spec. destruct (zlt (alignof_fields f) (alignof t)); auto.
+  assert (X: forall t a,
+    (exists n, a = two_power_nat n) ->
+    exists n,
+    match attr_alignas (attr_of_type t) with
+    | Some l => two_p (Z.of_N l)
+    | None => a
+    end = two_power_nat n).
+  {
+    intros.  
+    destruct (attr_alignas (attr_of_type t)).
+    exists (N.to_nat n). rewrite two_power_nat_two_p. rewrite N_nat_Z. auto.
+    auto.
+  }
+  induction t; apply X; simpl; auto.
+  exists 0%nat; auto.
+  destruct i.
+    exists 0%nat; auto. exists 1%nat; auto. exists 2%nat; auto.
+    exists 0%nat; auto. exists 3%nat; auto.
+  destruct f.
+    exists 2%nat; auto. exists 3%nat; auto.
+  exists 2%nat; auto.
+  exists 0%nat; auto.
+  exists 2%nat; auto.
+  induction f; simpl.
+  exists 0%nat; auto.
+  apply Z.max_case; auto.
 Qed.
 
 Lemma alignof_pos:
   forall t, alignof t > 0.
 Proof.
-  intros. generalize (alignof_1248 t). omega.
+  intros. destruct (alignof_two_p t) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
 Qed.
 
 Lemma alignof_fields_pos:
   forall f, alignof_fields f > 0.
 Proof.
-  intros. generalize (alignof_fields_1248 f). omega.
+  intros. destruct (alignof_fields_two_p f) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
 Qed.
 
 (** Size of a type, in bytes. *)
 
 Fixpoint sizeof (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' 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
+  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)
 
 with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z :=
   match fld with
@@ -246,23 +275,15 @@ with sizeof_union (fld: fieldlist) : Z :=
 Lemma sizeof_pos:
   forall t, sizeof t > 0.
 Proof.
-  intro t0.
-  apply (type_ind2 (fun t => sizeof t > 0)
-                   (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0));
-  intros; simpl; auto; try omega.
+  assert (X: forall t sz, sz > 0 -> align sz (alignof t) > 0).
+  {
+    intros. generalize (align_le sz (alignof t) (alignof_pos t)). omega. 
+  }
+Local Opaque alignof.
+  induction t; simpl; apply X; try xomega.
   destruct i; omega.
   destruct f; omega.
-  apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega.
-  destruct H. 
-  generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)). 
-  generalize (Zmax1 1 (sizeof_struct f 0)). omega. 
-  generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)). 
-  generalize (Zmax1 1 (sizeof_union f)). omega. 
-  split. omega. auto.
-  destruct H0. split; intros.
-  generalize (Zmax2 (sizeof t) (sizeof_union f)). omega.
-  apply H1. 
-  generalize (align_le pos (alignof t) (alignof_pos t)). omega.
+  apply Zmult_gt_0_compat. auto. xomega.
 Qed.
 
 Lemma sizeof_struct_incr:
@@ -271,17 +292,14 @@ Proof.
   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. 
-  assert (sizeof t > 0) by apply sizeof_pos. omega.
+  apply align_le. apply alignof_pos.
+  generalize (sizeof_pos t); omega.
 Qed.
 
 Lemma sizeof_alignof_compat:
   forall t, (alignof t | sizeof t).
 Proof.
-  induction t; simpl; try (apply Zdivide_refl).
-  apply Zdivide_mult_l. auto.
-  apply align_divides. apply alignof_fields_pos.
-  apply align_divides. apply alignof_fields_pos.
+  intros. destruct t; apply align_divides; apply alignof_pos.
 Qed.
 
 (** Byte offset for a field in a struct or union.
@@ -333,7 +351,7 @@ Lemma field_offset_in_range:
 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_fields_pos.
+  eapply Zle_trans. eapply Zle_max_r. apply align_le. apply alignof_pos.
 Qed.
 
 (** Second, two distinct fields do not overlap *)
@@ -484,40 +502,83 @@ with unroll_composite_fields (fld: fieldlist) : fieldlist :=
   | Fcons id ty fld' => Fcons id (unroll_composite ty) (unroll_composite_fields fld')
   end.
 
+Lemma attr_of_type_unroll_composite:
+  forall ty, attr_of_type (unroll_composite ty) = attr_of_type ty.
+Proof.
+  intros. destruct ty; simpl; auto; destruct (ident_eq i cid); auto.
+Qed.
+
 Lemma alignof_unroll_composite:
   forall ty, alignof (unroll_composite ty) = alignof ty.
 Proof.
+Local Transparent alignof.
   apply (type_ind2 (fun ty => alignof (unroll_composite ty) = alignof ty)
                    (fun fld => alignof_fields (unroll_composite_fields fld) = alignof_fields fld));
   simpl; intros; auto.
-  destruct (ident_eq i cid); auto. 
-  destruct (ident_eq i cid); auto. 
-  destruct (ident_eq i cid); auto.
-  decEq; auto.
+  rewrite H; auto.
+  destruct (ident_eq i cid); auto. simpl. rewrite H; auto.
+  destruct (ident_eq i cid); auto. simpl. rewrite H; auto.
+  destruct (ident_eq i cid); auto. congruence.
 Qed.
 
 Lemma sizeof_unroll_composite:
   forall ty, sizeof (unroll_composite ty) = sizeof ty.
 Proof.
-Opaque alignof.
+Local Opaque alignof.
   apply (type_ind2 (fun ty => sizeof (unroll_composite ty) = sizeof ty)
                    (fun fld => 
                       sizeof_union (unroll_composite_fields fld) = sizeof_union fld
                    /\ forall pos,
                       sizeof_struct (unroll_composite_fields fld) pos = sizeof_struct fld pos));
   simpl; intros; auto.
-  congruence.
-  destruct H. rewrite <- (alignof_unroll_composite (Tstruct i f a)).
-  simpl. destruct (ident_eq i cid); simpl. auto. rewrite H0; auto.
-  destruct H. rewrite <- (alignof_unroll_composite (Tunion i f a)).
-  simpl. destruct (ident_eq i cid); simpl. auto. rewrite H; auto.
-  destruct (ident_eq i cid); auto.
-  destruct H0. split. congruence.
-  intros. rewrite alignof_unroll_composite. rewrite H1. rewrite H. auto.
+- rewrite H. rewrite <- (alignof_unroll_composite (Tarray t z a)). 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.
+  destruct H. destruct (ident_eq i cid). auto. simpl. rewrite H. auto.
+- destruct (ident_eq i cid); auto. 
+- destruct H0. split. 
+  + congruence.
+  + intros. rewrite H1. rewrite H. rewrite alignof_unroll_composite. auto.
 Qed.
 
 End UNROLL_COMPOSITE.
 
+(** A variatn of [alignof] for use in block copy operations
+  (which do not support alignments greater than 8). *)
+
+Definition alignof_blockcopy (ty: type) := Zmin 8 (alignof ty).
+
+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.
+Qed.
+
+Lemma alignof_blockcopy_divides:
+  forall ty, (alignof_blockcopy ty | alignof ty).
+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.
+  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. *)
 
 Fixpoint type_of_params (params: list (ident * type)) : typelist :=
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index e7debfc..ec06cfd 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -19,6 +19,7 @@ Require Import Floats.
 Require Import Values.
 Require Import AST.
 Require Import Memory.
+Require Import Globalenvs.
 Require Import Ctypes.
 Require Import Cop.
 Require Import Csyntax.
@@ -173,11 +174,15 @@ 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 :: nil)
+      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 OK (Init_space(sizeof tyelt) :: nil)
-      else transl_init_array tyelt il sz
+      if zle sz 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)
   | 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 f3de05c..ef9ec6c 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -523,21 +523,22 @@ 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.
+  Genv.init_data_size data <= sizeof ty.
+Proof with (simpl; apply align_le; apply alignof_pos).
+Local Opaque alignof.
   intros. monadInv H. destruct x0. 
   monadInv EQ2.
   destruct ty; try discriminate. 
-  destruct i0; inv EQ2; reflexivity.
-  inv EQ2; reflexivity.
-  inv EQ2; reflexivity.
-  destruct ty; inv EQ2; reflexivity. 
+  destruct i0; inv EQ2...
+  inv EQ2...
+  inv EQ2...
+  destruct ty; inv EQ2...
   destruct ty; try discriminate.
-  destruct f0; inv EQ2; reflexivity.
+  destruct f0; inv EQ2...
   destruct ty; try discriminate.
-  destruct i0; inv EQ2; reflexivity.
-  inv EQ2; reflexivity.
-  inv EQ2; reflexivity.
+  destruct i0; inv EQ2...
+  inv EQ2...
+  inv EQ2...
 Qed.
 
 Notation idlsize := Genv.init_data_list_size.
@@ -616,25 +617,31 @@ with transl_init_list_size:
 Proof.
   induction i; intros. 
   (* single *)
-  monadInv H. simpl. rewrite (transl_init_single_size _ _ _ EQ). omega.
+  monadInv H. simpl. rewrite padding_size. omega. eapply transl_init_single_size; eauto.
   (* compound *)
   simpl in H. destruct ty; try discriminate.
   (* compound array *)
-  destruct (zle z 0). 
-  monadInv H. simpl. repeat rewrite Zmax_spec. rewrite zlt_true. rewrite zlt_true. ring.
-  omega. generalize (sizeof_pos ty); omega.
-  simpl. rewrite Zmax_spec. rewrite zlt_false.
-  eapply (proj1 (transl_init_list_size il)). auto. omega.
+  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.
+  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 *)
-  destruct f. 
-  inv H. reflexivity.
+  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.
   (* compound union *)
+  set (sz := sizeof (Tunion i f a)) in *.
   destruct f.
-  inv H. reflexivity.
+  inv H. simpl. rewrite Z.max_l. omega. generalize (sizeof_pos (Tunion i Fnil a)); unfold sz; omega. 
   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. 
@@ -767,12 +774,17 @@ Proof.
   (* single *)
   monadInv H3.
   exploit transl_init_single_steps; eauto. intros. 
-  simpl. rewrite H3. auto.
+  simpl. rewrite H3. apply store_init_data_list_padding. 
   (* 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 *)
   destruct fl.
   inv H. inv H1. auto.
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 897a2ee..ec82869 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -78,7 +78,11 @@ let struct_unions = ref StructUnion.empty
 (* Declarator (identifier + type) *)
 
 let attributes a =
-  if attr_volatile a then " volatile" else ""
+  let s1 = if a.attr_volatile then " volatile" else "" in
+  match a.attr_alignas with
+  | None -> s1
+  | Some l ->
+      sprintf " _Alignas(%Ld)%s" (Int64.shift_left 1L (N.to_int l)) s1
 
 let name_optid id =
   if id = "" then "" else " " ^ id
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 83e7375..62bbd67 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -761,10 +761,12 @@ Qed.
 
 Lemma sizeof_by_value:
   forall ty chunk,
-  access_mode ty = By_value chunk -> sizeof ty = size_chunk chunk.
+  access_mode ty = By_value chunk -> size_chunk chunk <= sizeof ty.
 Proof.
-  unfold access_mode; intros. 
-  destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto.
+  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.
 Qed.
 
 Definition env_initial_value (e: env) (m: mem) :=
@@ -782,7 +784,7 @@ Proof.
   apply IHalloc_variables. red; intros. rewrite PTree.gsspec in H2. 
   destruct (peq id0 id). inv H2. 
   eapply Mem.load_alloc_same'; eauto. 
-  omega. erewrite sizeof_by_value; eauto. omega. 
+  omega. rewrite Zplus_0_l. eapply sizeof_by_value; eauto. 
   apply Zdivide_0. 
   eapply Mem.load_alloc_other; eauto. 
 Qed.
@@ -1044,10 +1046,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. apply alignof_1248.
-  apply sizeof_alignof_compat.
-  eapply Mem.aligned_area_inject with (m := m); eauto. apply alignof_1248.
-  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.
+  eapply Zdivide_trans. apply alignof_blockcopy_divides. apply sizeof_alignof_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.