diff options
-rw-r--r-- | .depend | 2 | ||||
-rw-r--r-- | Changelog | 5 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 30 | ||||
-rw-r--r-- | cfrontend/Cexec.v | 9 | ||||
-rw-r--r-- | cfrontend/Clight.v | 3 | ||||
-rw-r--r-- | cfrontend/Csem.v | 3 | ||||
-rw-r--r-- | cfrontend/Cshmgen.v | 2 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof.v | 4 | ||||
-rw-r--r-- | cfrontend/Ctypes.v | 231 | ||||
-rw-r--r-- | cfrontend/Initializers.v | 13 | ||||
-rw-r--r-- | cfrontend/Initializersproof.v | 52 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 6 | ||||
-rw-r--r-- | cfrontend/SimplLocalsproof.v | 18 | ||||
-rw-r--r-- | cparser/C.mli | 1 | ||||
-rw-r--r-- | cparser/Cprint.ml | 1 | ||||
-rw-r--r-- | cparser/Cutil.ml | 26 | ||||
-rw-r--r-- | cparser/Cutil.mli | 8 | ||||
-rw-r--r-- | cparser/Elab.ml | 21 | ||||
-rw-r--r-- | cparser/Lexer.mll | 5 | ||||
-rw-r--r-- | cparser/PackedStructs.ml | 386 | ||||
-rw-r--r-- | cparser/Parser.mly | 20 | ||||
-rw-r--r-- | exportclight/Clightdefs.v | 28 | ||||
-rw-r--r-- | exportclight/ExportClight.ml | 13 | ||||
-rw-r--r-- | lib/Camlcoq.ml | 55 | ||||
-rw-r--r-- | test/regression/packedstruct1.c | 14 | ||||
-rw-r--r-- | test/regression/packedstruct2.c | 10 |
26 files changed, 538 insertions, 428 deletions
@@ -92,7 +92,7 @@ cfrontend/Csyntax.vo cfrontend/Csyntax.glob cfrontend/Csyntax.v.beautified: cfro cfrontend/Csem.vo cfrontend/Csem.glob cfrontend/Csem.v.beautified: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo common/Smallstep.vo cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob cfrontend/Cstrategy.v.beautified: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cexec.vo cfrontend/Cexec.glob cfrontend/Cexec.v.beautified: cfrontend/Cexec.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo -cfrontend/Initializers.vo cfrontend/Initializers.glob cfrontend/Initializers.v.beautified: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo +cfrontend/Initializers.vo cfrontend/Initializers.glob cfrontend/Initializers.v.beautified: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob cfrontend/Initializersproof.v.beautified: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob cfrontend/SimplExpr.v.beautified: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob cfrontend/SimplExprspec.v.beautified: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Memory.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo @@ -15,6 +15,11 @@ Development trunk: - PowerPC: more efficient implementation of division on 64-bit integers. - Minor simplifications in the generic solvers for dataflow analysis. - Small improvements in compilation times for the register allocation pass. +- Support for _Alignas(N) attribute from ISO C 2011. +- Revised implementation of packed structs, taking advantage of _Alignas. +- Suppressed the pragma "packed", replaced by a struct-level attribute + __packed__(params) or __attribute__(packed(params)). +- Fixed compile-time error when assigning a long long RHS to a bitfield. Release 2.0, 2013-06-21 diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 20e00c8c..dd9cfbf4 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 70a02c19..f83c7009 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 3bd06dff..6a579993 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 0f9b3f8a..5d94c537 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 a303a7fd..fd349856 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 24576fc6..79069449 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 8d00b955..abd015c8 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 e7debfcb..ec06cfdb 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 f3de05c1..ef9ec6ca 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 897a2ee5..ec82869f 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 83e73753..62bbd67d 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. diff --git a/cparser/C.mli b/cparser/C.mli index ce58504b..5d904078 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -77,6 +77,7 @@ type attribute = | AConst | AVolatile | ARestrict + | AAlignas of int (* always a power of 2 *) | Attr of string * attr_arg list type attributes = attribute list diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index e97f0411..c6864ff3 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -91,6 +91,7 @@ let attribute pp = function | AConst -> fprintf pp "const" | AVolatile -> fprintf pp "volatile" | ARestrict -> fprintf pp "restrict" + | AAlignas n -> fprintf pp "_Alignas(%d)" n | Attr(name, []) -> fprintf pp "__attribute__((%s))" name | Attr(name, arg1 :: args) -> fprintf pp "__attribute__((%s(" name; diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 2fc269cc..982bf785 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -71,6 +71,14 @@ let rec find_custom_attributes (names: string list) (al: attributes) = | _ :: tl -> find_custom_attributes names tl +let rec remove_custom_attributes (names: string list) (al: attributes) = + match al with + | [] -> [] + | Attr(name, args) :: tl when List.mem name names -> + remove_custom_attributes names tl + | a :: tl -> + a :: remove_custom_attributes names tl + (* Adding top-level attributes to a type. Doesn't need to unroll defns. *) (* Array types cannot carry attributes, so add them to the element type. *) @@ -147,6 +155,15 @@ let attr_is_type_related = function | Attr(("packed" | "__packed__"), _) -> true | _ -> false +(* Extracting alignment value from a set of attributes. Return 0 if none. *) + +let alignas_attribute al = + let rec alignas_attr accu = function + | [] -> accu + | AAlignas n :: al -> alignas_attr (max n accu) al + | a :: al -> alignas_attr accu al + in alignas_attr 0 al + (* Type compatibility *) exception Incompat @@ -266,6 +283,8 @@ let alignof_fkind = function let enum_ikind = IInt let rec alignof env t = + let a = alignas_attribute (attributes_of_type env t) in + if a > 0 then Some a else match t with | TVoid _ -> !config.alignof_void | TInt(ik, _) -> Some(alignof_ikind ik) @@ -325,6 +344,13 @@ let cautious_mul (a: int64) (b: int) = (* Return size of type, in bytes, or [None] if the type is incomplete *) let rec sizeof env t = + match sizeof_aux env t with + | None -> None + | Some sz -> + let a = alignas_attribute (attributes_of_type env t) in + Some (if a > 0 then align sz a else sz) + +and sizeof_aux env t = match t with | TVoid _ -> !config.sizeof_void | TInt(ik, _) -> Some(sizeof_ikind ik) diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 7e23a723..98ab54eb 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -33,9 +33,15 @@ val remove_attributes : attributes -> attributes -> attributes (* Difference [attr1 \ attr2] between two sets of attributes *) val incl_attributes : attributes -> attributes -> bool (* Check that first set of attributes is a subset of second set. *) +val alignas_attribute : attributes -> int + (* Extract the value of the [_Alignas] attributes, if any. + Return 0 if none, a (positive) power of two alignment if some. *) val find_custom_attributes : string list -> attributes -> attr_arg list list (* Extract arguments of custom [Attr] attributes whose names appear in the given list of names. *) +val remove_custom_attributes : string list -> attributes -> attributes + (* Remove all [Attr] attributes whose names appear + in the given list of names. *) val attributes_of_type : Env.t -> typ -> attributes (* Return the attributes of the given type, expanding typedefs if needed. *) val add_attributes_type : attributes -> typ -> typ @@ -44,6 +50,8 @@ val remove_attributes_type : Env.t -> attributes -> typ -> typ (* Remove the given set of attributes to those of the given type. *) val erase_attributes_type : Env.t -> typ -> typ (* Erase the attributes of the given type. *) +val change_attributes_type : Env.t -> (attributes -> attributes) -> typ -> typ + (* Apply the given function to the top-level attributes of the given type *) val attr_is_type_related: attribute -> bool (* Is an attribute type-related (true) or variable-related (false)? *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index fa9fd241..b25ad55e 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -280,12 +280,31 @@ let elab_gcc_attr loc env = function | _ -> warning loc "ill-formed attribute, ignored"; [] +let is_power_of_two n = n > 0L && Int64.(logand n (pred n)) = 0L + +let extract_alignas loc a = + match a with + | Attr(("aligned"|"__aligned__"), args) -> + begin match args with + | [AInt n] when is_power_of_two n -> AAlignas (Int64.to_int n) + | _ -> warning loc "bad 'aligned' attribute, ignored"; a + end + | _ -> a + let elab_attribute loc env = function | ("const", []) -> [AConst] | ("restrict", []) -> [ARestrict] | ("volatile", []) -> [AVolatile] + | ("_Alignas", [a]) -> + begin match elab_attr_arg loc env a with + | AInt n when is_power_of_two n -> [AAlignas (Int64.to_int n)] + | _ -> warning loc "bad _Alignas value, ignored"; [] + end | (("__attribute" | "__attribute__"), l) -> - List.flatten (List.map (elab_gcc_attr loc env) l) + List.map (extract_alignas loc) + (List.flatten (List.map (elab_gcc_attr loc env) l)) + | ("__packed__", args) -> + [Attr("__packed__", List.map (elab_attr_arg loc env) args)] | ("__asm__", _) -> [] (* MacOS X noise *) | (name, _) -> warning loc "`%s' annotation ignored" name; [] diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 0820e4e7..90e4d3cc 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -123,6 +123,7 @@ let init_lexicon _ = ("for", fun loc -> FOR loc); ("if", fun loc -> IF loc); ("else", fun _ -> ELSE); + ("sizeof", fun loc -> SIZEOF loc); (*** Implementation specific keywords ***) ("__signed__", fun loc -> SIGNED loc); ("__inline__", fun loc -> INLINE loc); @@ -150,6 +151,7 @@ let init_lexicon _ = ("_Alignof", fun loc -> ALIGNOF loc); ("__alignof", fun loc -> ALIGNOF loc); ("__alignof__", fun loc -> ALIGNOF loc); + ("_Alignas", fun loc -> ALIGNAS loc); ("__volatile__", fun loc -> VOLATILE loc); ("__volatile", fun loc -> VOLATILE loc); @@ -160,6 +162,7 @@ let init_lexicon _ = (*** weimer: GCC arcana ***) ("__restrict", fun loc -> RESTRICT loc); ("restrict", fun loc -> RESTRICT loc); + ("__packed__", fun loc -> PACKED loc); (* ("__extension__", EXTENSION); *) (**** MS VC ***) ("__int64", fun loc -> INT64 loc); @@ -487,7 +490,9 @@ rule initial = | ';' { (SEMICOLON (currentLoc lexbuf)) } | ',' {COMMA} | '.' {DOT} +(* XL: redundant? | "sizeof" {SIZEOF (currentLoc lexbuf)} +*) | "__asm" { if !msvcMode then MSASM (msasm lexbuf, currentLoc lexbuf) else (ASM (currentLoc lexbuf)) } diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index 13a00ce4..5d0bac91 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -23,37 +23,11 @@ open Env open Cerrors open Transform -type field_info = { - fi_offset: int; (* byte offset within struct *) - fi_swap: bool (* true if byte-swapped *) -} +(* The set of struct fields that are byte-swapped. + A field is identified by a pair (struct name, field name). *) -(* Mapping from struct name to size. - Only packed structs are mentioned in this table. *) - -let packed_structs : (ident, int) Hashtbl.t = Hashtbl.create 17 - -(* Mapping from (struct name, field name) to field_info. - Only fields of packed structs are mentioned in this table. *) - -let packed_fields : (ident * string, field_info) Hashtbl.t - = Hashtbl.create 57 - -(* The current packing parameters. The first two are 0 if packing is - turned off. *) - -let max_field_align = ref 0 -let min_struct_align = ref 0 -let byte_swap_fields = ref false - -(* Alignment *) - -let is_pow2 n = - n > 0 && n land (n - 1) = 0 - -let align x boundary = - assert (is_pow2 boundary); - (x + boundary - 1) land (lnot (boundary - 1)) +let byteswapped_fields : (ident * string, unit) Hashtbl.t + = Hashtbl.create 57 (* What are the types that can be byte-swapped? *) @@ -65,88 +39,87 @@ let rec can_byte_swap env ty = | TArray(ty_elt, _, _) -> can_byte_swap env ty_elt | _ -> (false, false) -(* Compute size and alignment of a type, taking "aligned" attributes - into account *) - -let sizeof_alignof loc env ty = - match sizeof env ty, alignof env ty with - | Some sz, Some al -> - begin match find_custom_attributes ["aligned"; "__aligned__"] - (attributes_of_type env ty) with - | [] -> - (sz, al) - | [[AInt n]] when is_pow2 (Int64.to_int n) -> - let al' = max al (Int64.to_int n) in - (align sz al', al') - | _ -> - warning "%a: Warning: Ill-formed 'aligned' attribute, ignored" - formatloc loc; - (sz, al) - end - | _, _ -> - error "%a: Error: struct field has incomplete type" formatloc loc; - (0, 1) - -(* Layout algorithm *) - -let layout_struct mfa msa swapped loc env struct_id fields = - let rec layout max_al pos = function - | [] -> - (max_al, pos) - | f :: rem -> - if f.fld_bitfield <> None then - error "%a: Error: bitfields in packed structs not allowed" - formatloc loc; - let (sz, al) = sizeof_alignof loc env f.fld_typ in - let swap = - if swapped then begin - let (can_swap, must_swap) = can_byte_swap env f.fld_typ in - if not can_swap then - error "%a: Error: cannot byte-swap field of type '%a'" - formatloc loc Cprint.typ f.fld_typ; - must_swap - end else false in - let al1 = min al mfa in - let pos1 = align pos al1 in - Hashtbl.add packed_fields - (struct_id, f.fld_name) - {fi_offset = pos1; fi_swap = swap}; - let pos2 = pos1 + sz in - layout (max max_al al1) pos2 rem in - let (al, sz) = layout 1 0 fields in - if al >= msa then - (0, sz) +(* "Safe" [alignof] function, with detection of incomplete types. *) + +let safe_alignof loc env ty = + match alignof env ty with + | Some al -> al + | None -> + error "%a: Error: incomplete type for a struct field" formatloc loc; 1 + +(* Remove existing [_Alignas] attributes and add the given [_Alignas] attr. *) + +let remove_alignas_attr attrs = + List.filter (function AAlignas _ -> false | _ -> true) attrs +let set_alignas_attr al attrs = + add_attributes [AAlignas al] (remove_alignas_attr attrs) + +(* Rewriting field declarations *) + +let transf_field_decl mfa swapped loc env struct_id f = + if f.fld_bitfield <> None then + error "%a: Error: bitfields in packed structs not allowed" + formatloc loc; + (* Register as byte-swapped if needed *) + if swapped then begin + let (can_swap, must_swap) = can_byte_swap env f.fld_typ in + if not can_swap then + error "%a: Error: cannot byte-swap field of type '%a'" + formatloc loc Cprint.typ f.fld_typ; + if must_swap then + Hashtbl.add byteswapped_fields (struct_id, f.fld_name) () + end; + (* Reduce alignment if requested *) + if mfa = 0 then f else begin + let al = safe_alignof loc env f.fld_typ in + { f with fld_typ = + change_attributes_type env (set_alignas_attr (min mfa al)) f.fld_typ } + end + +(* Rewriting struct declarations *) + +let transf_struct_decl mfa msa swapped loc env struct_id attrs ml = + let ml' = + List.map (transf_field_decl mfa swapped loc env struct_id) ml in + if msa = 0 then (attrs, ml') else begin + let al' = (* natural alignment of the transformed struct *) + List.fold_left + (fun a f' -> max a (safe_alignof loc env f'.fld_typ)) + 1 ml' in + (set_alignas_attr (max msa al') attrs, ml') + end + +(* Rewriting composite declarations *) + +let is_pow2 n = n > 0 && n land (n - 1) = 0 + +let packed_param_value loc n = + let m = Int64.to_int n in + if n <> Int64.of_int m then + (error "%a: __packed__ parameter `%Ld' is too large" formatloc loc n; 0) + else if m = 0 || is_pow2 m then + m else - (msa, align sz msa) - -(* Rewriting of struct declarations *) - -let payload_field sz = - { fld_name = "__payload"; - fld_typ = TArray(TInt(IUChar, []), Some(Int64.of_int sz), []); - fld_bitfield = None} + (error "%a: __packed__ parameter `%Ld' must be a power of 2" formatloc loc n; 0) let transf_composite loc env su id attrs ml = match su with | Union -> (attrs, ml) | Struct -> let (mfa, msa, swapped) = - if !max_field_align > 0 then - (!max_field_align, !min_struct_align, !byte_swap_fields) - else if find_custom_attributes ["packed";"__packed__"] attrs <> [] then - (1, 0, false) - else - (0, 0, false) in - if mfa = 0 then (attrs, ml) else begin - let (al, sz) = layout_struct mfa msa swapped loc env id ml in - Hashtbl.add packed_structs id sz; - let attrs = - if al = 0 then attrs else - add_attributes [Attr("__aligned__", [AInt(Int64.of_int al)])] attrs - and field = - payload_field sz - in (attrs, [field]) - end + match find_custom_attributes ["packed";"__packed__"] attrs with + | [] -> (0L, 0L, false) + | [[]] -> (1L, 0L, false) + | [[AInt n]] -> (n, 0L, false) + | [[AInt n; AInt p]] -> (n, p, false) + | [[AInt n; AInt p; AInt q]] -> (n, p, q <> 0L) + | _ -> + error "%a: ill-formed or ambiguous __packed__ attribute" + formatloc loc; + (0L, 0L, false) in + let mfa = packed_param_value loc mfa in + let msa = packed_param_value loc msa in + transf_struct_decl mfa msa swapped loc env id attrs ml (* Accessor functions *) @@ -172,28 +145,6 @@ let ecast ty e = {edesc = ECast(ty, e); etyp = ty} let ecast_opt env ty e = if compatible_types env ty e.etyp then e else ecast ty e -(* *e *) -let ederef ty e = {edesc = EUnop(Oderef, e); etyp = ty} - -(* e + n *) -let eoffset e n = - {edesc = EBinop(Oadd, e, intconst (Int64.of_int n) IInt, e.etyp); - etyp = e.etyp} - -(* *((ty * ) (base.__payload + offset)) *) -let dot_packed_field base pf ty = - let payload = - {edesc = EUnop(Odot "__payload", base); - etyp = TArray(TInt(IChar,[]),None,[]) } in - ederef ty (ecast (TPtr(ty, [])) (eoffset payload pf.fi_offset)) - -(* *((ty * ) (base->__payload + offset)) *) -let arrow_packed_field base pf ty = - let payload = - {edesc = EUnop(Oarrow "__payload", base); - etyp = TArray(TInt(IChar,[]),None,[]) } in - ederef ty (ecast (TPtr(ty, [])) (eoffset payload pf.fi_offset)) - (* (ty) __builtin_readNN_reversed(&lval) or (ty) __builtin_bswapNN(lval) *) @@ -256,38 +207,26 @@ let bswap_write loc env lhs rhs = let transf_expr loc env ctx e = - let is_packed_access ty fieldname = + let is_byteswapped ty fieldname = match unroll env ty with - | TStruct(id, _) -> - (try Some(Hashtbl.find packed_fields (id, fieldname)) - with Not_found -> None) - | _ -> None in + | TStruct(id, _) -> Hashtbl.mem byteswapped_fields (id, fieldname) + | _ -> false in - let is_packed_access_ptr ty fieldname = + let is_byteswapped_ptr ty fieldname = match unroll env ty with - | TPtr(ty', _) -> is_packed_access ty' fieldname - | _ -> None in + | TPtr(ty', _) -> is_byteswapped ty' fieldname + | _ -> false in (* Transformation of l-values. Return transformed expr plus [true] if l-value is a byte-swapped field and [false] otherwise. *) let rec lvalue e = match e.edesc with | EUnop(Odot fieldname, e1) -> - let e1' = texp Val e1 in - begin match is_packed_access e1.etyp fieldname with - | None -> - ({edesc = EUnop(Odot fieldname, e1'); etyp = e.etyp}, false) - | Some pf -> - (dot_packed_field e1' pf e.etyp, pf.fi_swap) - end + ({edesc = EUnop(Odot fieldname, texp Val e1); etyp = e.etyp}, + is_byteswapped e1.etyp fieldname) | EUnop(Oarrow fieldname, e1) -> - let e1' = texp Val e1 in - begin match is_packed_access_ptr e1.etyp fieldname with - | None -> - ({edesc = EUnop(Oarrow fieldname, e1'); etyp = e.etyp}, false) - | Some pf -> - (arrow_packed_field e1' pf e.etyp, pf.fi_swap) - end + ({edesc = EUnop(Oarrow fieldname, texp Val e1); etyp = e.etyp}, + is_byteswapped_ptr e1.etyp fieldname) | EBinop(Oindex, e1, e2, tyres) -> let (e1', swap) = lvalue e1 in ({edesc = EBinop(Oindex, e1', e2, tyres); etyp = e.etyp}, swap) @@ -383,74 +322,52 @@ let transf_fundef env f = (* Initializers *) -let extract_byte env e i = - let ty = unary_conversion env e.etyp in - let e1 = - if i = 0 then e else - { edesc = EBinop(Oshr, e, intconst (Int64.of_int (i*8)) IInt, ty); - etyp = ty } in - { edesc = EBinop(Oand, e1, intconst 0xFFL IInt, ty); etyp = ty } - -let init_packed_struct loc env struct_id struct_sz initdata = - - let new_initdata = Array.make struct_sz (Init_single (intconst 0L IUChar)) in - - let enter_scalar pos e sz bigendian = - for i = 0 to sz - 1 do - let bytenum = if bigendian then sz - 1 - i else i in - new_initdata.(pos + i) <- Init_single(extract_byte env e bytenum) - done in - - let rec enter_init pos ty init bigendian = - match (unroll env ty, init) with - | (TInt(ik, _), Init_single e) -> - enter_scalar pos e (sizeof_ikind ik) bigendian - | (TEnum(_, _), Init_single e) -> - enter_scalar pos e (sizeof_ikind enum_ikind) bigendian - | (TPtr _, Init_single e) -> - enter_scalar pos e ((!Machine.config).sizeof_ptr) bigendian - | (TArray(ty_elt, _, _), Init_array il) -> - begin match sizeof env ty_elt with - | Some sz -> enter_init_array pos ty_elt sz il bigendian - | None -> fatal_error "%a: Internal error: incomplete type in init data" formatloc loc - end - | (_, _) -> - error "%a: Unsupported initializer for packed struct" formatloc loc - and enter_init_array pos ty sz il bigendian = - match il with - | [] -> () - | i1 :: il' -> - enter_init pos ty i1 bigendian; - enter_init_array (pos + sz) ty sz il' bigendian in - - let enter_field (fld, init) = - let finfo = - try Hashtbl.find packed_fields (struct_id, fld.fld_name) - with Not_found -> - fatal_error "%a: Internal error: non-packed field in packed struct" - formatloc loc in - enter_init finfo.fi_offset fld.fld_typ init - ((!Machine.config).bigendian <> finfo.fi_swap) in - - List.iter enter_field initdata; - - Init_struct(struct_id, [ - (payload_field struct_sz, Init_array (Array.to_list new_initdata)) - ]) +let extract_byte n i = + Int64.(logand (shift_right_logical n (i * 8)) 0xFFL) + +let byteswap_int nbytes n = + let res = ref 0L in + for i = 0 to nbytes - 1 do + res := Int64.(logor (shift_left !res 8) (extract_byte n i)) + done; + !res let transf_init loc env i = - let rec trinit = function - | Init_single e as i -> i - | Init_array il -> Init_array (List.map trinit il) - | Init_struct(id, fld_init_list) -> - begin try - let sz = Hashtbl.find packed_structs id in - init_packed_struct loc env id sz fld_init_list - with Not_found -> - Init_struct(id, List.map (fun (f,i) -> (f, trinit i)) fld_init_list) + (* [swap] is [None] if no byte swapping needed, [Some ty] if + byte-swapping is needed, with target type [ty] *) + let rec trinit swap = function + | Init_single e as i -> + begin match swap with + | None -> i + | Some ty -> + match Ceval.constant_expr env ty e with + | Some(CInt(n, ik, _)) -> + let n' = byteswap_int (sizeof_ikind ik) n in + Init_single {edesc = EConst(CInt(n', ik, "")); etyp = e.etyp} + | _ -> + error "%a: Error: initializer for byte-swapped field is not \ + a compile-time integer constant" formatloc loc; i end - | Init_union(id, fld, i) -> Init_union(id, fld, trinit i) - in trinit i + | Init_array il -> + let swap_elt = + match swap with + | None -> None + | Some ty -> + match unroll env ty with + | TArray(ty_elt, _, _) -> Some ty_elt + | _ -> assert false in + Init_array (List.map (trinit swap_elt) il) + | Init_struct(id, fld_init_list) -> + let trinit_field (f, i) = + let swap_f = + if Hashtbl.mem byteswapped_fields (id, f.fld_name) + then Some f.fld_typ + else None in + (f, trinit swap_f i) in + Init_struct(id, List.map trinit_field fld_init_list) + | Init_union(id, fld, i) -> + Init_union(id, fld, trinit None i) + in trinit None i (* Declarations *) @@ -460,39 +377,6 @@ let transf_decl loc env (sto, id, ty, init_opt) = | None -> None | Some i -> Some (transf_init loc env i)) -(* Pragmas *) - -let re_pack = Str.regexp "pack\\b" -let re_pack_1 = Str.regexp "pack[ \t]*(\\([ \t0-9,]*\\))[ \t]*$" -let re_comma = Str.regexp ",[ \t]*" - -let process_pragma loc s = - if Str.string_match re_pack s 0 then begin - if Str.string_match re_pack_1 s 0 then begin - let arg = Str.matched_group 1 s in - let (mfa, msa, bs) = - match List.map int_of_string (Str.split re_comma arg) with - | [] -> (0, 0, false) - | [x] -> (x, 0, false) - | [x;y] -> (x, y, false) - | x :: y :: z :: _ -> (x, y, z = 1) in - if mfa = 0 || is_pow2 mfa then - max_field_align := mfa - else - error "%a: Error: In #pragma pack, max field alignment must be a power of 2" formatloc loc; - if msa = 0 || is_pow2 msa then - min_struct_align := msa - else - error "%a: Error: In #pragma pack, min struct alignment must be a power of 2" formatloc loc; - byte_swap_fields := bs; - true - end else begin - warning "%a: Warning: Ill-formed #pragma pack, ignored" formatloc loc; - false - end - end else - false - (* Global declarations *) let rec transf_globdecls env accu = function @@ -531,14 +415,10 @@ let rec transf_globdecls env accu = function (g :: accu) gl | Gpragma p -> - if process_pragma g.gloc p - then transf_globdecls env accu gl - else transf_globdecls env (g :: accu) gl + transf_globdecls env (g :: accu) gl (* Program *) let program p = - min_struct_align := 0; - max_field_align := 0; - byte_swap_fields := false; + Hashtbl.clear byteswapped_fields; transf_globdecls (Builtins.environment()) [] p diff --git a/cparser/Parser.mly b/cparser/Parser.mly index 83b1984c..cd515ded 100644 --- a/cparser/Parser.mly +++ b/cparser/Parser.mly @@ -220,7 +220,7 @@ let transformOffsetOf (speclist, dtype) member = %token<Cabs.cabsloc> VOLATILE EXTERN STATIC CONST RESTRICT AUTO REGISTER %token<Cabs.cabsloc> THREAD -%token<Cabs.cabsloc> SIZEOF ALIGNOF +%token<Cabs.cabsloc> SIZEOF ALIGNOF ALIGNAS %token EQ PLUS_EQ MINUS_EQ STAR_EQ SLASH_EQ PERCENT_EQ %token AND_EQ PIPE_EQ CIRC_EQ INF_INF_EQ SUP_SUP_EQ @@ -252,7 +252,7 @@ let transformOffsetOf (speclist, dtype) member = %token<Cabs.cabsloc> ATTRIBUTE INLINE ASM TYPEOF FUNCTION__ PRETTY_FUNCTION__ %token LABEL__ -%token<Cabs.cabsloc> BUILTIN_VA_ARG ATTRIBUTE_USED +%token<Cabs.cabsloc> BUILTIN_VA_ARG ATTRIBUTE_USED PACKED %token BUILTIN_VA_LIST %token BLOCKATTRIBUTE %token<Cabs.cabsloc> BUILTIN_TYPES_COMPAT BUILTIN_OFFSETOF @@ -1244,6 +1244,13 @@ attribute_nocv: | ATTRIBUTE_USED { ("__attribute__", [ VARIABLE "used" ]), $1 } *)*/ +| ALIGNAS paren_comma_expression + { ("_Alignas", [smooth_expression(fst $2)]), $1 } +| ALIGNAS LPAREN type_name RPAREN + { let (b, d) = $3 in + ("_Alignas", [TYPE_ALIGNOF(b, d)]), $1 } +| PACKED LPAREN attr_list RPAREN { ("__packed__", $3), $1 } +| PACKED { ("__packed__", []), $1 } | DECLSPEC paren_attr_list_ne { ("__declspec", $2), $1 } | MSATTR { (fst $1, []), snd $1 } /* ISO 6.7.3 */ @@ -1265,10 +1272,17 @@ attribute: /* (* sm: I need something that just includes __attribute__ and nothing more, * to support them appearing between the 'struct' keyword and the type name. - * Actually, a declspec can appear there as well (on MSVC) *) */ + * Actually, a declspec can appear there as well (on MSVC). + * XL: ... and so does _Alignas(). *) */ just_attribute: ATTRIBUTE LPAREN paren_attr_list RPAREN { ("__attribute__", $3) } +| ALIGNAS paren_comma_expression + { ("_Alignas", [smooth_expression(fst $2)]) } +| ALIGNAS LPAREN type_name RPAREN + { let (b, d) = $3 in ("_Alignas", [TYPE_ALIGNOF(b, d)]) } +| PACKED LPAREN attr_list RPAREN { ("__packed__", $3) } +| PACKED { ("__packed__", []) } | DECLSPEC paren_attr_list_ne { ("__declspec", $2) } ; diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v index 1cb93d54..246e12c1 100644 --- a/exportclight/Clightdefs.v +++ b/exportclight/Clightdefs.v @@ -39,18 +39,26 @@ Definition tdouble := Tfloat F64 noattr. Definition tptr (t: type) := Tpointer t noattr. Definition tarray (t: type) (sz: Z) := Tarray t sz noattr. -Definition volatile_attr := {| attr_volatile := true |}. +Definition volatile_attr := {| attr_volatile := true; attr_alignas := None |}. -Definition tvolatile (ty: type) := +Definition tattr (a: attr) (ty: type) := match ty with | Tvoid => Tvoid - | Tint sz si a => Tint sz si volatile_attr - | Tlong si a => Tlong si volatile_attr - | Tfloat sz a => Tfloat sz volatile_attr - | Tpointer elt a => Tpointer elt volatile_attr - | Tarray elt sz a => Tarray elt sz volatile_attr + | Tint sz si _ => Tint sz si a + | Tlong si _ => Tlong si a + | Tfloat sz _ => Tfloat sz a + | Tpointer elt _ => Tpointer elt a + | Tarray elt sz _ => Tarray elt sz a | Tfunction args res => Tfunction args res - | Tstruct id fld a => Tstruct id fld volatile_attr - | Tunion id fld a => Tunion id fld volatile_attr - | Tcomp_ptr id a => Tcomp_ptr id volatile_attr + | Tstruct id fld _ => Tstruct id fld a + | Tunion id fld _ => Tunion id fld a + | Tcomp_ptr id _ => Tcomp_ptr id a end. + +Definition tvolatile (ty: type) := tattr volatile_attr ty. + +Definition talignas (n: N) (ty: type) := + tattr {| attr_volatile := false; attr_alignas := Some n |} ty. + +Definition tvolatile_alignas (n: N) (ty: type) := + tattr {| attr_volatile := true; attr_alignas := Some n |} ty. diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 9027f86d..8c83fabb 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -137,10 +137,15 @@ let coqint64 p n = let use_struct_names = ref true let rec typ p t = - let a = attr_of_type t in - if a (*.attr_volatile*) - then fprintf p "(tvolatile %a)" rtyp t - else rtyp p t + match attr_of_type t with + | { attr_volatile = false; attr_alignas = None} -> + rtyp p t + | { attr_volatile = true; attr_alignas = None} -> + fprintf p "(tvolatile %a)" rtyp t + | { attr_volatile = false; attr_alignas = Some n} -> + fprintf p "(talignas %ld%%N %a)" (N.to_int32 n) rtyp t + | { attr_volatile = true; attr_alignas = Some n} -> + fprintf p "(tvolatile_alignas %ld%%N %a)" (N.to_int32 n) rtyp t and rtyp p = function | Tvoid -> fprintf p "tvoid" diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 30e67051..929b61e3 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -17,6 +17,7 @@ open Datatypes open BinNums +open BinNat open BinInt open BinPos open Floats @@ -115,6 +116,57 @@ module P = struct end +(* Coq's [N] type and some of its operations *) + +module N = struct + + type t = coq_N = N0 | Npos of positive + + let zero = N0 + let one = Npos Coq_xH + let succ = N.succ + let pred = N.pred + let add = N.add + let sub = N.sub + let mul = N.mul + let eq x y = (N.compare x y = Eq) + let lt x y = (N.compare x y = Lt) + let gt x y = (N.compare x y = Gt) + let le x y = (N.compare x y <> Gt) + let ge x y = (N.compare x y <> Lt) + let compare x y = match N.compare x y with Lt -> -1 | Eq -> 0 | Gt -> 1 + + let to_int = function + | N0 -> 0 + | Npos p -> P.to_int p + + let of_int n = + if n = 0 then N0 else Npos (P.of_int n) + + let to_int32 = function + | N0 -> 0l + | Npos p -> P.to_int32 p + + let of_int32 n = + if n = 0l then N0 else Npos (P.of_int32 n) + + let to_int64 = function + | N0 -> 0L + | Npos p -> P.to_int64 p + + let of_int64 n = + if n = 0L then N0 else Npos (P.of_int64 n) + + let (+) = add + let (-) = sub + let ( * ) = mul + let (=) = eq + let (<) = lt + let (<=) = le + let (>) = gt + let (>=) = ge +end + (* Coq's [Z] type and some of its operations *) module Z = struct @@ -176,6 +228,8 @@ module Z = struct let of_uint64 n = if n = 0L then Z0 else Zpos (P.of_int64 n) + let of_N = Z.of_N + let rec to_string_rec base buff x = if x = Z0 then () else begin let (q, r) = Z.div_eucl x base in @@ -215,6 +269,7 @@ module Z = struct let (>=) = ge end + (* Alternate names *) let camlint_of_coqint : Integers.Int.int -> int32 = Z.to_int32 diff --git a/test/regression/packedstruct1.c b/test/regression/packedstruct1.c index e7b6c1dc..e5526ed9 100644 --- a/test/regression/packedstruct1.c +++ b/test/regression/packedstruct1.c @@ -6,9 +6,7 @@ /* Simple packing */ -#pragma pack(1) - -struct s1 { unsigned short x; int y; double z; }; +struct __packed__ s1 { unsigned short x; int y; double z; }; void test1(void) { @@ -22,9 +20,7 @@ void test1(void) /* Packing plus alignment */ -#pragma pack(2,16) - -struct s2 { unsigned char x; int y; double z; }; +struct __packed__(2,16) s2 { unsigned char x; int y; double z; }; char filler1; @@ -42,8 +38,6 @@ void test2(void) /* Now with byte-swapped fields */ -#pragma pack(1,1,1) - struct s3 { unsigned char x; unsigned short y; @@ -53,7 +47,7 @@ struct s3 { char * p; unsigned int t[3]; unsigned char s[2]; -}; +} __packed__(1,1,1); struct s3 s3; @@ -83,8 +77,6 @@ void test3(void) /* Back to normal */ -#pragma pack() - struct s4 { unsigned short x; int y; double z; }; void test4(void) diff --git a/test/regression/packedstruct2.c b/test/regression/packedstruct2.c index 0c383a47..37c736ec 100644 --- a/test/regression/packedstruct2.c +++ b/test/regression/packedstruct2.c @@ -4,9 +4,7 @@ /* Simple packing */ -#pragma pack(1) - -struct s1 { unsigned short x; int y; char z; }; +struct __packed__ s1 { unsigned short x; int y; char z; }; struct s1 s1 = { 2345, -12345678, 'x' }; @@ -17,9 +15,7 @@ void test1(void) /* Now with byte-swapped fields */ -#pragma pack(1,1,1) - -struct s3 { +struct __packed__(1,1,1) s3 { unsigned char x; unsigned short y; unsigned int z; @@ -47,8 +43,6 @@ void test3(void) /* Back to normal */ -#pragma pack() - struct s4 { unsigned short x; int y; double z; }; struct s4 s4 = { 123, -456789, 3.14159 }; |