From e89f1e606bc8c9c425628392adc9c69cec666b5e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 22 Dec 2014 19:34:45 +0100 Subject: Represent struct and union types by name instead of by structure. --- cfrontend/Ctypes.v | 883 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 552 insertions(+), 331 deletions(-) (limited to 'cfrontend/Ctypes.v') 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. -- cgit