Represent struct and union types by name instead of by structure.

1 files changed, 552 insertions, 331 deletions

diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index c437a6bc..091c5276 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -16,6 +16,7 @@
 (** Type expressions for the Compcert C and Clight languages *)
 
 Require Import Coqlib.
+Require Import Maps.
 Require Import AST.
 Require Import Errors.
 Require Archi.
@@ -63,32 +64,6 @@ Definition noattr := {| attr_volatile := false; attr_alignas := None |}.
   of the function arguments (list [targs]), and the type of the
   function result ([tres]).  Variadic functions and old-style unprototyped
   functions are not supported.
-- In C, struct and union types are named and compared by name.
-  This enables the definition of recursive struct types such as
-<<
-  struct s1 { int n; struct * s1 next; };
->>
-  Note that recursion within types must go through a pointer type.
-  For instance, the following is not allowed in C.
-<<
-  struct s2 { int n; struct s2 next; };
->>
-  In Compcert C, struct and union types [Tstruct id fields] and
-  [Tunion id fields] are compared by structure: the [fields]
-  argument gives the names and types of the members.  The identifier
-  [id] is a local name which can be used in conjuction with the
-  [Tcomp_ptr] constructor to express recursive types.  [Tcomp_ptr id]
-  stands for a pointer type to the nearest enclosing [Tstruct]
-  or [Tunion] type named [id].  For instance. the structure [s1]
-  defined above in C is expressed by
-<<
-  Tstruct "s1" (Fcons "n" (Tint I32 Signed)
-               (Fcons "next" (Tcomp_ptr "s1")
-               Fnil))
->>
-  Note that the incorrect structure [s2] above cannot be expressed at
-  all, since [Tcomp_ptr] lets us refer to a pointer to an enclosing
-  structure or union, but not to the structure or union directly.
 *)
 
 Inductive type : Type :=
@@ -99,35 +74,27 @@ Inductive type : Type :=
   | Tpointer: type -> attr -> type                 (**r pointer types ([*ty]) *)
   | Tarray: type -> Z -> attr -> type              (**r array types ([ty[len]]) *)
   | Tfunction: typelist -> type -> calling_convention -> type    (**r function types *)
-  | Tstruct: ident -> fieldlist -> attr -> type    (**r struct types *)
-  | Tunion: ident -> fieldlist -> attr -> type     (**r union types *)
-  | Tcomp_ptr: ident -> attr -> type               (**r pointer to named struct or union *)
-
+  | Tstruct: ident -> attr -> type                 (**r struct types *)
+  | Tunion: ident -> attr -> type                  (**r union types *)
 with typelist : Type :=
   | Tnil: typelist
-  | Tcons: type -> typelist -> typelist
-
-with fieldlist : Type :=
-  | Fnil: fieldlist
-  | Fcons: ident -> type -> fieldlist -> fieldlist.
+  | Tcons: type -> typelist -> typelist.
 
 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}.
+with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2}.
 Proof.
   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 bool_dec. intros E1 E2 E3.
+  generalize ident_eq zeq bool_dec ident_eq; intros.
   decide equality.
   decide equality.
   decide equality.
-  generalize ident_eq. intros E1. decide equality.
 Defined.
 
-Opaque type_eq typelist_eq fieldlist_eq.
+Opaque type_eq typelist_eq.
 
 (** Extract the attributes of a type. *)
 
@@ -140,9 +107,8 @@ Definition attr_of_type (ty: type) :=
   | Tpointer elt a => a
   | Tarray elt sz a => a
   | Tfunction args res cc => noattr
-  | Tstruct id fld a => a
-  | Tunion id fld a => a
-  | Tcomp_ptr id a => a
+  | Tstruct id a => a
+  | Tunion id a => a
   end.
 
 (** Change the top-level attributes of a type *)
@@ -156,9 +122,8 @@ Definition change_attributes (f: attr -> attr) (ty: type) : type :=
   | Tpointer elt a => Tpointer elt (f a)
   | Tarray elt sz a => Tarray elt sz (f a)
   | Tfunction args res cc => ty
-  | Tstruct id fld a => Tstruct id fld (f a)
-  | Tunion id fld a => Tunion id fld (f a)
-  | Tcomp_ptr id a => Tcomp_ptr id (f a)
+  | Tstruct id a => Tstruct id (f a)
+  | Tunion id a => Tunion id (f a)
   end.
 
 (** Erase the top-level attributes of a type *)
@@ -181,6 +146,39 @@ Definition attr_union (a1 a2: attr) : attr :=
 Definition merge_attributes (ty: type) (a: attr) : type :=
   change_attributes (attr_union a) ty.
 
+(** Syntax for [struct] and [union] definitions.  [struct] and [union]
+  are collectively called "composites".  Each compilation unit
+  comes with a list of top-level definitions of composites. *)
+
+Inductive struct_or_union : Type := Struct | Union.
+
+Definition members : Type := list (ident * type).
+
+Inductive composite_definition : Type :=
+  Composite (id: ident) (su: struct_or_union) (m: members) (a: attr).
+
+(** For type-checking, compilation and semantics purposes, the composite
+  definitions are collected in the following [composite_env] environment.
+  The [composite] record contains additional information compared with
+  the [composite_definition], such as size and alignment information. *)
+
+Record composite : Type := {
+  co_su: struct_or_union;
+  co_members: members;
+  co_attr: attr;
+  co_sizeof: Z;
+  co_alignof: Z;
+  co_sizeof_pos: co_sizeof >= 0;
+  co_alignof_two_p: exists n, co_alignof = two_power_nat n;
+  co_sizeof_alignof: (co_alignof | co_sizeof)
+}.
+
+Definition composite_env : Type := PTree.t composite.
+
+(** * Operations over types *)
+
+(** ** Conversions *)
+
 Definition type_int32s := Tint I32 Signed noattr.
 Definition type_bool := Tint IBool Signed noattr.
 
@@ -208,15 +206,51 @@ Definition default_argument_conversion (ty: type) : type :=
   | _                   => remove_attributes ty
   end.
 
-(** * Operations over types *)
+(** ** Complete types *)
 
-(** Alignment of a type, in bytes. *)
+(** A type is complete if it fully describes an object.
+  All struct and union names appearing in the type must be defined,
+  unless they occur under a pointer or function type.  [void] and
+  function types are incomplete types. *)
 
-Fixpoint alignof (t: type) : Z :=
-  match attr_alignas (attr_of_type t) with
+Fixpoint complete_type (env: composite_env) (t: type) : bool :=
+  match t with
+  | Tvoid => false
+  | Tint _ _ _ => true
+  | Tlong _ _ => true
+  | Tfloat _ _ => true
+  | Tpointer _ _ => true
+  | Tarray t' _ _ => complete_type env t'
+  | Tfunction _ _ _ => false
+  | Tstruct id _ | Tunion id _ =>
+      match env!id with Some co => true | None => false end
+  end.
+
+Definition complete_or_function_type (env: composite_env) (t: type) : bool :=
+  match t with
+  | Tfunction _ _ _ => true
+  | _ => complete_type env t
+  end.
+
+(** ** Alignment of a type *)
+
+(** Adjust the natural alignment [al] based on the attributes [a] attached
+  to the type.  If an "alignas" attribute is given, use it as alignment
+  in preference to [al]. *)
+
+Definition align_attr (a: attr) (al: Z) : Z :=
+  match attr_alignas a with
   | Some l => two_p (Z.of_N l)
-  | None =>
-      match t with
+  | None => al
+  end.
+
+(** In the ISO C standard, alignment is defined only for complete
+  types.  However, it is convenient that [alignof] is a total
+  function.  For incomplete types, it returns 1. *)
+
+Fixpoint alignof (env: composite_env) (t: type) : Z :=
+  align_attr (attr_of_type t)
+   (match t with
       | Tvoid => 1
       | Tint I8 _ _ => 1
       | Tint I16 _ _ => 2
@@ -226,42 +260,26 @@ Fixpoint alignof (t: type) : Z :=
       | Tfloat F32 _ => 4
       | Tfloat F64 _ => Archi.align_float64
       | Tpointer _ _ => 4
-      | Tarray t' _ _ => alignof t'
+      | Tarray t' _ _ => alignof env t'
       | Tfunction _ _ _ => 1
-      | Tstruct _ fld _ => alignof_fields fld
-      | Tunion _ fld _ => alignof_fields fld
-      | Tcomp_ptr _ _ => 4
-      end
-  end
-
-with alignof_fields (f: fieldlist) : Z :=
-  match f with
-  | Fnil => 1
-  | Fcons id t f' => Zmax (alignof t) (alignof_fields f')
-  end.
-
-Scheme type_ind2 := Induction for type Sort Prop
-  with fieldlist_ind2 := Induction for fieldlist Sort Prop.
+      | Tstruct id _ | Tunion id _ =>
+          match env!id with Some co => co_alignof co | None => 1 end
+    end).
+
+Remark align_attr_two_p:
+  forall al a,
+  (exists n, al = two_power_nat n) ->
+  (exists n, align_attr a al = two_power_nat n).
+Proof.
+  intros. unfold align_attr. destruct (attr_alignas a).   
+  exists (N.to_nat n). rewrite two_power_nat_two_p. rewrite N_nat_Z. auto.
+  auto.
+Qed.
 
 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.
+  forall env t, exists n, alignof env t = two_power_nat n.
 Proof.
-  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.
+  induction t; apply align_attr_two_p; simpl.
   exists 0%nat; auto.
   destruct i.
     exists 0%nat; auto.
@@ -273,28 +291,28 @@ Proof.
     exists 2%nat; auto.
     (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity).
   exists 2%nat; auto.
+  apply IHt.
   exists 0%nat; auto.
-  exists 2%nat; auto.
-  induction f; simpl.
-  exists 0%nat; auto.
-  apply Z.max_case; auto.
+  destruct (env!i). apply co_alignof_two_p. exists 0%nat; auto.
+  destruct (env!i). apply co_alignof_two_p. exists 0%nat; auto.
 Qed.
 
 Lemma alignof_pos:
-  forall t, alignof t > 0.
+  forall env t, alignof env t > 0.
 Proof.
-  intros. destruct (alignof_two_p t) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
+  intros. destruct (alignof_two_p env t) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
 Qed.
 
-Lemma alignof_fields_pos:
-  forall f, alignof_fields f > 0.
-Proof.
-  intros. destruct (alignof_fields_two_p f) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
-Qed.
+(** ** Size of a type *)
 
-(** Size of a type, in bytes. *)
+(** In the ISO C standard, size is defined only for complete
+  types.  However, it is convenient that [sizeof] is a total
+  function.  For [void] and function types, we follow GCC and define
+  their size to be 1.  For undefined structures and unions, the size is 
+  arbitrarily taken to be 0.
+*)
 
-Fixpoint sizeof (t: type) : Z :=
+Fixpoint sizeof (env: composite_env) (t: type) : Z :=
   match t with
   | Tvoid => 1
   | Tint I8 _ _ => 1
@@ -305,199 +323,217 @@ Fixpoint sizeof (t: type) : Z :=
   | Tfloat F32 _ => 4
   | Tfloat F64 _ => 8
   | Tpointer _ _ => 4
-  | Tarray t' n _ => sizeof t' * Zmax 0 n
+  | Tarray t' n _ => sizeof env t' * Z.max 0 n
   | Tfunction _ _ _ => 1
-  | Tstruct _ fld _ => align (sizeof_struct fld 0) (alignof t)
-  | Tunion _ fld _ => align (sizeof_union fld) (alignof t)
-  | Tcomp_ptr _ _ => 4
-  end
-
-with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z :=
-  match fld with
-  | Fnil => pos
-  | Fcons id t fld' => sizeof_struct fld' (align pos (alignof t) + sizeof t)
-  end
-
-with sizeof_union (fld: fieldlist) : Z :=
-  match fld with
-  | Fnil => 0
-  | Fcons id t fld' => Zmax (sizeof t) (sizeof_union fld')
+  | Tstruct id _ | Tunion id _ =>
+      match env!id with Some co => co_sizeof co | None => 0 end
   end.
 
 Lemma sizeof_pos:
-  forall t, sizeof t >= 0
-with sizeof_struct_incr:
-  forall fld pos, pos <= sizeof_struct fld pos.
+  forall env t, sizeof env t >= 0.
 Proof.
-- Local Opaque alignof.
-  assert (X: forall n t, n >= 0 -> align n (alignof t) >= 0).
-  {
-    intros. generalize (align_le n (alignof t) (alignof_pos t)). omega.
-  }
-  induction t; simpl; try xomega.
+  induction t; simpl; try omega.
   destruct i; omega.
   destruct f; omega.
-  change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega. 
-  apply X. apply Zle_ge. apply sizeof_struct_incr. 
-  apply X. induction f; simpl; xomega.
-- 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.
-  generalize (sizeof_pos t); omega.
+  change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega.
+  destruct (env!i). apply co_sizeof_pos. omega.
+  destruct (env!i). apply co_sizeof_pos. omega.
 Qed.
 
+(** The size of a type is an integral multiple of its alignment,
+  unless the alignment was artificially increased with the [__Alignas]
+  attribute. *)
+
 Fixpoint naturally_aligned (t: type) : Prop :=
+  attr_alignas (attr_of_type t) = None /\
   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
+  | Tarray t' _ _ => naturally_aligned t'
+  | _ => True
   end.
 
 Lemma sizeof_alignof_compat:
-  forall t, naturally_aligned t -> (alignof t | sizeof t).
+  forall env t, naturally_aligned t -> (alignof env t | sizeof env t).
 Proof.
-Local Transparent alignof.
-  induction t; simpl; intros.
+  induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl. 
 - apply Zdivide_refl.
-- rewrite H. destruct i; apply Zdivide_refl.
-- rewrite H. exists (8 / Archi.align_int64); reflexivity. 
-- rewrite H. destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity. 
-- rewrite H; apply Zdivide_refl.
-- destruct H. rewrite H. apply Z.divide_mul_l; auto. 
+- destruct i; apply Zdivide_refl.
+- exists (8 / Archi.align_int64); reflexivity. 
+- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity. 
 - apply Zdivide_refl.
-- change (alignof (Tstruct i f a) | align (sizeof_struct f 0) (alignof (Tstruct i f a))).
-  apply align_divides. apply alignof_pos.
-- change (alignof (Tunion i f a) | align (sizeof_union f) (alignof (Tunion i f a))).
-  apply align_divides. apply alignof_pos.
-- rewrite H; apply Zdivide_refl.
+- apply Z.divide_mul_l; auto. 
+- apply Zdivide_refl.
+- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. 
+- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. 
 Qed.
 
-(** Byte offset for a field in a struct or union.
-  Field are laid out consecutively, and padding is inserted
-  to align each field to the natural alignment for its type. *)
+(** ** Size and alignment for composite definitions *)
+
+(** The alignment for a structure or union is the max of the alignment
+  of its members. *)
 
-Open Local Scope string_scope.
+Fixpoint alignof_composite (env: composite_env) (m: members) : Z :=
+  match m with
+  | nil => 1
+  | (id, t) :: m' => Z.max (alignof env t) (alignof_composite env m')
+  end.
+
+(** The size of a structure corresponds to its layout: fields are
+  laid out consecutively, and padding is inserted to align
+  each field to the alignment for its type. *)
+
+Fixpoint sizeof_struct (env: composite_env) (cur: Z) (m: members) : Z :=
+  match m with
+  | nil => cur
+  | (id, t) :: m' => sizeof_struct env (align cur (alignof env t) + sizeof env t) m'
+  end.
+
+(** The size of an union is the max of the sizes of its members. *)
 
-Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
-                              {struct fld} : res Z :=
+Fixpoint sizeof_union (env: composite_env) (m: members) : Z :=
+  match m with
+  | nil => 0
+  | (id, t) :: m' => Z.max (sizeof env t) (sizeof_union env m')
+  end.
+
+Lemma alignof_composite_two_p:
+  forall env m, exists n, alignof_composite env m = two_power_nat n.
+Proof.
+  induction m as [|[id t]]; simpl. 
+- exists 0%nat; auto.
+- apply Z.max_case; auto. apply alignof_two_p.
+Qed.
+
+Lemma alignof_composite_pos:
+  forall env m a, align_attr a (alignof_composite env m) > 0.
+Proof.
+  intros.
+  exploit align_attr_two_p. apply (alignof_composite_two_p env m). 
+  instantiate (1 := a). intros [n EQ]. 
+  rewrite EQ; apply two_power_nat_pos.
+Qed.
+
+Lemma sizeof_struct_incr:
+  forall env m cur, cur <= sizeof_struct env cur m.
+Proof.
+  induction m as [|[id t]]; simpl; intros.
+- omega.
+- apply Zle_trans with (align cur (alignof env t)). 
+  apply align_le. apply alignof_pos.
+  apply Zle_trans with (align cur (alignof env t) + sizeof env t).
+  generalize (sizeof_pos env t); omega. 
+  apply IHm.
+Qed.
+
+Lemma sizeof_union_pos:
+  forall env m, 0 <= sizeof_union env m.
+Proof.
+  induction m as [|[id t]]; simpl; xomega.
+Qed.
+
+(** ** Byte offset for a field of a structure *)
+
+(** [field_offset env id fld] returns the byte offset for field [id]
+  in a structure whose members are [fld].  Fields are laid out
+  consecutively, and padding is inserted to align each field to the
+  alignment for its type. *)
+
+Fixpoint field_offset_rec (env: composite_env) (id: ident) (fld: members) (pos: Z)
+                          {struct fld} : res Z :=
   match fld with
-  | Fnil => Error (MSG "Unknown field " :: CTX id :: nil)
-  | Fcons id' t fld' =>
+  | nil => Error (MSG "Unknown field " :: CTX id :: nil)
+  | (id', t) :: fld' =>
       if ident_eq id id'
-      then OK (align pos (alignof t))
-      else field_offset_rec id fld' (align pos (alignof t) + sizeof t)
+      then OK (align pos (alignof env t))
+      else field_offset_rec env id fld' (align pos (alignof env t) + sizeof env t)
   end.
 
-Definition field_offset (id: ident) (fld: fieldlist) : res Z :=
-  field_offset_rec id fld 0.
+Definition field_offset (env: composite_env) (id: ident) (fld: members) : res Z :=
+  field_offset_rec env id fld 0.
 
-Fixpoint field_type (id: ident) (fld: fieldlist) {struct fld} : res type :=
+Fixpoint field_type (id: ident) (fld: members) {struct fld} : res type :=
   match fld with
-  | Fnil => Error (MSG "Unknown field " :: CTX id :: nil)
-  | Fcons id' t fld' => if ident_eq id id' then OK t else field_type id fld'
+  | nil => Error (MSG "Unknown field " :: CTX id :: nil)
+  | (id', t) :: fld' => if ident_eq id id' then OK t else field_type id fld'
   end.
 
 (** Some sanity checks about field offsets.  First, field offsets are 
   within the range of acceptable offsets. *)
 
 Remark field_offset_rec_in_range:
-  forall id ofs ty fld pos,
-  field_offset_rec id fld pos = OK ofs -> field_type id fld = OK ty ->
-  pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos.
+  forall env id ofs ty fld pos,
+  field_offset_rec env id fld pos = OK ofs -> field_type id fld = OK ty ->
+  pos <= ofs /\ ofs + sizeof env ty <= sizeof_struct env pos fld.
 Proof.
-  intros until ty. induction fld; simpl.
-  congruence.
-  destruct (ident_eq id i); intros.
-  inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr.
+  intros until ty. induction fld as [|[i t]]; simpl; intros.
+- discriminate.
+- destruct (ident_eq id i); intros.
+  inv H. inv H0. split.
+  apply align_le. apply alignof_pos. apply sizeof_struct_incr.
   exploit IHfld; eauto. intros [A B]. split; auto. 
-  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)).
-  apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega. 
+  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof env t)).
+  apply align_le. apply alignof_pos. generalize (sizeof_pos env t). omega. 
 Qed.
 
 Lemma field_offset_in_range:
-  forall sid fld a fid ofs ty,
-  field_offset fid fld = OK ofs -> field_type fid fld = OK ty ->
-  0 <= ofs /\ ofs + sizeof ty <= sizeof (Tstruct sid fld a).
+  forall env fld id ofs ty,
+  field_offset env id fld = OK ofs -> field_type id fld = OK ty ->
+  0 <= ofs /\ ofs + sizeof env ty <= sizeof_struct env 0 fld.
 Proof.
-  intros. exploit field_offset_rec_in_range; eauto. intros [A B].
-  split. auto.
-Local Opaque alignof. 
-  simpl. eapply Zle_trans; eauto. 
-  apply align_le. apply alignof_pos. 
+  intros. eapply field_offset_rec_in_range; eauto.
 Qed.
 
 (** Second, two distinct fields do not overlap *)
 
 Lemma field_offset_no_overlap:
-  forall id1 ofs1 ty1 id2 ofs2 ty2 fld,
-  field_offset id1 fld = OK ofs1 -> field_type id1 fld = OK ty1 ->
-  field_offset id2 fld = OK ofs2 -> field_type id2 fld = OK ty2 ->
+  forall env id1 ofs1 ty1 id2 ofs2 ty2 fld,
+  field_offset env id1 fld = OK ofs1 -> field_type id1 fld = OK ty1 ->
+  field_offset env id2 fld = OK ofs2 -> field_type id2 fld = OK ty2 ->
   id1 <> id2 ->
-  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1.
+  ofs1 + sizeof env ty1 <= ofs2 \/ ofs2 + sizeof env ty2 <= ofs1.
 Proof.
-  intros until ty2. intros fld0 A B C D NEQ.
-  assert (forall fld pos,
-  field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 ->
-  field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 ->
-  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1).
-  induction fld; intro pos; simpl. congruence.
-  destruct (ident_eq id1 i); destruct (ident_eq id2 i).
-  congruence. 
-  subst i. intros. inv H; inv H0.
+  intros until fld. unfold field_offset. generalize 0 as pos.
+  induction fld as [|[i t]]; simpl; intros.
+- discriminate.
+- destruct (ident_eq id1 i); destruct (ident_eq id2 i).
++ congruence. 
++ subst i. inv H; inv H0.
   exploit field_offset_rec_in_range. eexact H1. eauto. tauto.  
-  subst i. intros. inv H1; inv H2.
++ subst i. inv H1; inv H2.
   exploit field_offset_rec_in_range. eexact H. eauto. tauto. 
-  intros. eapply IHfld; eauto.
-
-  apply H with fld0 0; auto.
++ eapply IHfld; eauto.
 Qed.
 
 (** Third, if a struct is a prefix of another, the offsets of common fields
     are the same. *)
 
-Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist :=
-  match fld1 with
-  | Fnil => fld2
-  | Fcons id ty fld => Fcons id ty (fieldlist_app fld fld2)
-  end.
-
 Lemma field_offset_prefix:
-  forall id ofs fld2 fld1,
-  field_offset id fld1 = OK ofs ->
-  field_offset id (fieldlist_app fld1 fld2) = OK ofs.
+  forall env id ofs fld2 fld1,
+  field_offset env id fld1 = OK ofs ->
+  field_offset env id (fld1 ++ fld2) = OK ofs.
 Proof.
-  intros until fld2.
-  assert (forall fld1 pos, 
-    field_offset_rec id fld1 pos = OK ofs ->
-    field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs).
-  induction fld1; intros pos; simpl. congruence.
-  destruct (ident_eq id i); auto.
-  intros. unfold field_offset; auto. 
+  intros until fld1. unfold field_offset. generalize 0 as pos. 
+  induction fld1 as [|[i t]]; simpl; intros.
+- discriminate.
+- destruct (ident_eq id i); auto. 
 Qed.
 
 (** Fourth, the position of each field respects its alignment. *)
 
 Lemma field_offset_aligned:
-  forall id fld ofs ty,
-  field_offset id fld = OK ofs -> field_type id fld = OK ty ->
-  (alignof ty | ofs).
+  forall env id fld ofs ty,
+  field_offset env id fld = OK ofs -> field_type id fld = OK ty ->
+  (alignof env ty | ofs).
 Proof.
-  assert (forall id ofs ty fld pos,
-          field_offset_rec id fld pos = OK ofs -> field_type id fld = OK ty ->
-          (alignof ty | ofs)).
-  induction fld; simpl; intros.
-  discriminate.
-  destruct (ident_eq id i). inv H; inv H0. 
-  apply align_divides. apply alignof_pos. 
-  eapply IHfld; eauto.
-  intros. eapply H with (pos := 0); eauto.
+  intros until ty. unfold field_offset. generalize 0 as pos. revert fld. 
+  induction fld as [|[i t]]; simpl; intros.
+- discriminate.
+- destruct (ident_eq id i).
++ inv H; inv H0. apply align_divides. apply alignof_pos.
++ eauto.
 Qed.
 
+(** ** Access modes *)
+
 (** The [access_mode] function describes how a l-value of the given
 type must be accessed:
 - [By_value ch]: access by value, i.e. by loading from the address
@@ -530,9 +566,8 @@ Definition access_mode (ty: type) : mode :=
   | Tpointer _ _ => By_value Mint32
   | Tarray _ _ _ => By_reference
   | Tfunction _ _ _ => By_reference
-  | Tstruct _ _ _ => By_copy
-  | Tunion _ _ _ => By_copy
-  | Tcomp_ptr _ _ => By_nothing
+  | Tstruct _ _ => By_copy
+  | Tunion _ _ => By_copy
 end.
 
 (** For the purposes of the semantics and the compiler, a type denotes
@@ -545,87 +580,13 @@ Definition type_is_volatile (ty: type) : bool :=
   | _          => false
   end.
 
-(** Unroll the type of a structure or union field, substituting
-    [Tcomp_ptr] by a pointer to the structure. *)
-
-Section UNROLL_COMPOSITE.
-
-Variable cid: ident.
-Variable comp: type.
-
-Fixpoint unroll_composite (ty: type) : type :=
-  match ty with
-  | Tvoid => ty
-  | Tint _ _ _ => ty
-  | Tlong _ _ => ty
-  | Tfloat _ _ => ty
-  | Tpointer t1 a => Tpointer (unroll_composite t1) a
-  | Tarray t1 sz a => Tarray (unroll_composite t1) sz a
-  | Tfunction t1 t2 a => Tfunction (unroll_composite_list t1) (unroll_composite t2) a
-  | Tstruct id fld a => if ident_eq id cid then ty else Tstruct id (unroll_composite_fields fld) a
-  | Tunion id fld a => if ident_eq id cid then ty else Tunion id (unroll_composite_fields fld) a
-  | Tcomp_ptr id a => if ident_eq id cid then Tpointer comp a else ty
-  end
-
-with unroll_composite_list (tl: typelist) : typelist :=
-  match tl with
-  | Tnil => Tnil
-  | Tcons t1 tl' => Tcons (unroll_composite t1) (unroll_composite_list tl')
-  end
-
-with unroll_composite_fields (fld: fieldlist) : fieldlist :=
-  match fld with
-  | Fnil => Fnil
-  | 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.
-  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.
-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.
-- 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.
-  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.
+(** ** Alignment for block copy operations *)
 
 (** 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. *)
 
-Fixpoint alignof_blockcopy (t: type) : Z :=
+Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z :=
   match t with
   | Tvoid => 1
   | Tint I8 _ _ => 1
@@ -636,20 +597,22 @@ Fixpoint alignof_blockcopy (t: type) : Z :=
   | Tfloat F32 _ => 4
   | Tfloat F64 _ => 8
   | Tpointer _ _ => 4
-  | Tarray t' _ _ => alignof_blockcopy t'
+  | Tarray t' _ _ => alignof_blockcopy env t'
   | Tfunction _ _ _ => 1
-  | Tstruct _ fld _ => Zmin 8 (alignof t)
-  | Tunion _ fld _ => Zmin 8 (alignof t)
-  | Tcomp_ptr _ _ => 4
+  | Tstruct id _ | Tunion id _ =>
+      match env!id with
+      | Some co => Z.min 8 (co_alignof co)
+      | None => 1
+      end
   end.
 
 Lemma alignof_blockcopy_1248:
-  forall ty, let a := alignof_blockcopy ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8.
+  forall env ty, let a := alignof_blockcopy env ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8.
 Proof.
-  assert (X: forall ty, let a := Zmin 8 (alignof ty) in
+  assert (X: forall co, let a := Zmin 8 (co_alignof co) in
              a = 1 \/ a = 2 \/ a = 4 \/ a = 8).
   {
-    intros. destruct (alignof_two_p ty) as [n EQ]. unfold a; rewrite EQ. 
+    intros. destruct (co_alignof_two_p co) as [n EQ]. unfold a; rewrite EQ. 
     destruct n; auto.
     destruct n; auto.
     destruct n; auto.
@@ -660,45 +623,47 @@ Proof.
   induction ty; simpl; auto.
   destruct i; auto.
   destruct f; auto.
+  destruct (env!i); auto. 
+  destruct (env!i); auto.
 Qed.
 
 Lemma alignof_blockcopy_pos:
-  forall ty, alignof_blockcopy ty > 0.
+  forall env ty, alignof_blockcopy env ty > 0.
 Proof.
-  intros. generalize (alignof_blockcopy_1248 ty). simpl. intuition omega.
+  intros. generalize (alignof_blockcopy_1248 env ty). simpl. intuition omega.
 Qed.
 
 Lemma sizeof_alignof_blockcopy_compat:
-  forall ty, (alignof_blockcopy ty | sizeof ty).
+  forall env ty, (alignof_blockcopy env ty | sizeof env ty).
 Proof.
-  assert (X: forall ty sz, (alignof ty | sz) -> (Zmin 8 (alignof ty) | sz)).
+  assert (X: forall co, (Z.min 8 (co_alignof co) | co_sizeof co)).
   {
-    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. 
+    intros. apply Zdivide_trans with (co_alignof co). 2: apply co_sizeof_alignof.
+    destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ.
+    destruct n. apply Zdivide_refl.
+    destruct n. apply Zdivide_refl.
+    destruct n. apply Zdivide_refl.
     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.
+    exists (two_p (Z.of_nat n)). 
+    change 8 with (two_p 3). 
+    rewrite <- two_p_is_exp by omega.
     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.
+  apply Z.divide_mul_l. auto.
+  apply Zdivide_refl.
+  destruct (env!i). apply X. apply Zdivide_0. 
+  destruct (env!i). apply X. apply Zdivide_0. 
 Qed.
 
+(** ** C types and back-end types *)
+
 (** Extracting a type list from a function parameter declaration. *)
 
 Fixpoint type_of_params (params: list (ident * type)) : typelist :=
@@ -735,3 +700,259 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
 Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature :=
   mksignature (typlist_of_typelist args) (opttyp_of_type res) cc.
 
+(** * Construction of the composite environment *)
+
+Definition sizeof_composite (env: composite_env) (su: struct_or_union) (m: members) : Z :=
+  match su with
+  | Struct => sizeof_struct env 0 m
+  | Union  => sizeof_union env m
+  end.
+
+Lemma sizeof_composite_pos:
+  forall env su m, 0 <= sizeof_composite env su m.
+Proof.
+  intros. destruct su; simpl.
+  apply sizeof_struct_incr.
+  apply sizeof_union_pos.
+Qed.
+
+Fixpoint complete_members (env: composite_env) (m: members) : bool :=
+  match m with
+  | nil => true
+  | (id, t) :: m' => complete_type env t && complete_members env m'
+  end.
+
+(** Convert a composite definition to its internal representation.
+  The size and alignment of the composite are determined at this time.
+  The alignment takes into account the [__Alignas] attributes
+  associated with the definition.  The size is rounded up to a multiple
+  of the alignment.  
+
+  The conversion fails if a type of a member is not complete.  This rules
+  out incorrect recursive definitions such as
+<<
+    struct s { int x; struct s next; }
+>>
+  Here, when we process the definition of [struct s], the identifier [s]
+  is not bound yet in the composite environment, hence field [next]
+  has an incomplete type.  However, recursions that go through a pointer type
+  are correctly handled:
+<<
+    struct s { int x; struct s * next; }
+>>
+  Here, [next] has a pointer type, which is always complete, even though
+  [s] is not yet bound to a composite.
+*)
+
+Program Definition composite_of_def
+     (env: composite_env) (id: ident) (su: struct_or_union) (m: members) (a: attr)
+     : res composite :=
+  match env!id, complete_members env m return _ with
+  | Some _, _ =>
+      Error (MSG "Multiple definitions of struct or union " :: CTX id :: nil)
+  | None, false =>
+      Error (MSG "Incomplete struct or union " :: CTX id :: nil)
+  | None, true =>
+      let al := align_attr a (alignof_composite env m) in
+      OK {| co_su := su;
+            co_members := m;
+            co_attr := a;
+            co_sizeof := align (sizeof_composite env su m) al;
+            co_alignof := al;
+            co_sizeof_pos := _;
+            co_alignof_two_p := _;
+            co_sizeof_alignof := _ |}
+  end.
+Next Obligation.
+  apply Zle_ge. eapply Zle_trans. eapply sizeof_composite_pos. 
+  apply align_le; apply alignof_composite_pos.
+Qed.
+Next Obligation.
+  apply align_attr_two_p. apply alignof_composite_two_p.
+Qed.
+Next Obligation.
+  apply align_divides. apply alignof_composite_pos.
+Qed.
+
+(** The composite environment for a program is obtained by entering
+  its composite definitions in sequence.  The definitions are assumed
+  to be listed in dependency order: the definition of a composite
+  must precede all uses of this composite, unless the use is under
+  a pointer or function type. *)
+
+Local Open Scope error_monad_scope.
+
+Fixpoint add_composite_definitions (env: composite_env) (defs: list composite_definition) : res composite_env :=
+  match defs with
+  | nil => OK env
+  | Composite id su m a :: defs =>
+      do co <- composite_of_def env id su m a;
+      add_composite_definitions (PTree.set id co env) defs
+  end.
+
+Definition build_composite_env (defs: list composite_definition) :=
+  add_composite_definitions (PTree.empty _) defs.
+
+(** Stability properties for alignments and sizes.  If the type is
+  complete in a composite environment [env], its size and alignment
+  are unchanged if we add more definitions to [env]. *)
+
+Section STABILITY.
+
+Variables env env': composite_env.
+Hypothesis extends: forall id co, env!id = Some co -> env'!id = Some co.
+
+Lemma alignof_stable:
+  forall t, complete_type env t = true -> alignof env' t = alignof env t.
+Proof.
+  induction t; simpl; intros; f_equal; auto.
+  destruct (env!i) as [co|] eqn:E; try discriminate. 
+  erewrite extends by eauto. auto.
+  destruct (env!i) as [co|] eqn:E; try discriminate. 
+  erewrite extends by eauto. auto.
+Qed.
+
+Lemma sizeof_stable:
+  forall t, complete_type env t = true -> sizeof env' t = sizeof env t.
+Proof.
+  induction t; simpl; intros; auto.
+  rewrite IHt by auto. auto.
+  destruct (env!i) as [co|] eqn:E; try discriminate. 
+  erewrite extends by eauto. auto.
+  destruct (env!i) as [co|] eqn:E; try discriminate. 
+  erewrite extends by eauto. auto.
+Qed.
+
+Lemma complete_type_stable:
+  forall t, complete_type env t = true -> complete_type env' t = true.
+Proof.
+  induction t; simpl; intros; auto.
+  destruct (env!i) as [co|] eqn:E; try discriminate. 
+  erewrite extends by eauto. auto.
+  destruct (env!i) as [co|] eqn:E; try discriminate. 
+  erewrite extends by eauto. auto.
+Qed.
+
+Lemma alignof_composite_stable:
+  forall m, complete_members env m = true -> alignof_composite env' m = alignof_composite env m.
+Proof.
+  induction m as [|[id t]]; simpl; intros. 
+  auto.
+  InvBooleans. rewrite alignof_stable by auto. rewrite IHm by auto. auto.
+Qed.
+
+Lemma sizeof_struct_stable:
+  forall m pos, complete_members env m = true -> sizeof_struct env' pos m = sizeof_struct env pos m.
+Proof.
+  induction m as [|[id t]]; simpl; intros.
+  auto.
+  InvBooleans. rewrite alignof_stable by auto. rewrite sizeof_stable by auto. 
+  rewrite IHm by auto. auto.
+Qed.
+
+Lemma sizeof_union_stable:
+  forall m, complete_members env m = true -> sizeof_union env' m = sizeof_union env m.
+Proof.
+  induction m as [|[id t]]; simpl; intros.
+  auto.
+  InvBooleans. rewrite sizeof_stable by auto. rewrite IHm by auto. auto.
+Qed.
+
+Lemma sizeof_composite_stable:
+  forall su m, complete_members env m = true -> sizeof_composite env' su m = sizeof_composite env su m.
+Proof.
+  intros. destruct su; simpl. 
+  apply sizeof_struct_stable; auto. 
+  apply sizeof_union_stable; auto.
+Qed.
+
+Lemma complete_members_stable:
+  forall m, complete_members env m = true -> complete_members env' m = true.
+Proof.
+  induction m as [|[id t]]; simpl; intros.
+  auto.
+  InvBooleans. rewrite complete_type_stable by auto. rewrite IHm by auto. auto.
+Qed.
+
+End STABILITY.
+
+Lemma add_composite_definitions_incr:
+  forall id co defs env1 env2,
+  add_composite_definitions env1 defs = OK env2 ->
+  env1!id = Some co -> env2!id = Some co.
+Proof.
+  induction defs; simpl; intros.
+- inv H; auto.
+- destruct a; monadInv H. 
+  eapply IHdefs; eauto. rewrite PTree.gso; auto.
+  red; intros; subst id0. unfold composite_of_def in EQ. rewrite H0 in EQ; discriminate.
+Qed.
+
+(** It follows that the sizes and alignments contained in the composite
+  environment produced by [build_composite_env] are consistent with
+  the sizes and alignments of the members of the composite types. *)
+
+Definition composite_consistent (env: composite_env) (co: composite) : Prop :=
+     complete_members env (co_members co) = true
+  /\ co_alignof co = align_attr (co_attr co) (alignof_composite env (co_members co))
+  /\ co_sizeof co = align (sizeof_composite env (co_su co) (co_members co)) (co_alignof co).
+
+Definition composite_env_consistent (env: composite_env) : Prop :=
+  forall id co, env!id = Some co -> composite_consistent env co.
+
+Theorem build_composite_env_consistent:
+  forall defs env, build_composite_env defs = OK env -> composite_env_consistent env.
+Proof.
+  cut (forall defs env0 env,
+       add_composite_definitions env0 defs = OK env ->
+       composite_env_consistent env0 ->
+       composite_env_consistent env).
+  intros. eapply H; eauto. red; intros. rewrite PTree.gempty in H1; discriminate.
+  induction defs as [|d1 defs]; simpl; intros.
+- inv H; auto.
+- destruct d1; monadInv H.
+  eapply IHdefs; eauto.
+  set (env1 := PTree.set id x env0) in *.
+  unfold composite_of_def in EQ.
+  destruct (env0!id) eqn:E; try discriminate. 
+  destruct (complete_members env0 m) eqn:C; inversion EQ; clear EQ.
+  assert (forall id1 co1, env0!id1 = Some co1 -> env1!id1 = Some co1).
+  { intros. unfold env1. rewrite PTree.gso; auto. congruence. }
+  red; intros. unfold env1 in H2; rewrite PTree.gsspec in H2; destruct (peq id0 id).
++ subst id0. inversion H2; clear H2. subst co. 
+  red; rewrite <- H1; simpl. 
+  assert (A: alignof_composite env1 m = alignof_composite env0 m)
+  by (apply alignof_composite_stable; assumption).
+  rewrite A.
+  split. eapply complete_members_stable; eauto. 
+  split. auto.
+  f_equal. symmetry. apply sizeof_composite_stable; assumption.
++ exploit H0; eauto. intros (P & Q & R).
+  assert (A: alignof_composite env1 (co_members co) = alignof_composite env0 (co_members co))
+  by (apply alignof_composite_stable; assumption).
+  red. rewrite A.
+  split. eapply complete_members_stable; eauto. 
+  split. auto.
+  rewrite R. f_equal. symmetry. apply sizeof_composite_stable; assumption.
+Qed.
+
+(** Moreover, every composite definition is reflected in the composite environment. *)
+
+Theorem build_composite_env_charact:
+  forall id su m a defs env,
+  build_composite_env defs = OK env ->
+  In (Composite id su m a) defs ->
+  exists co, env!id = Some co /\ co_members co = m /\ co_attr co = a /\ co_su co = su.
+Proof.
+  intros until defs. unfold build_composite_env. generalize (PTree.empty composite) as env0. 
+  revert defs. induction defs as [|d1 defs]; simpl; intros.
+- contradiction.
+- destruct d1; monadInv H.
+  destruct H0; [idtac|eapply IHdefs;eauto]. inv H. 
+  unfold composite_of_def in EQ. 
+  destruct (env0!id) eqn:E; try discriminate. 
+  destruct (complete_members env0 m) eqn:C; simplify_eq EQ. clear EQ; intros EQ.
+  exists x.
+  split. eapply add_composite_definitions_incr; eauto. apply PTree.gss.
+  subst x; auto.
+Qed.