summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend2
-rw-r--r--Changelog5
-rw-r--r--cfrontend/C2C.ml30
-rw-r--r--cfrontend/Cexec.v9
-rw-r--r--cfrontend/Clight.v3
-rw-r--r--cfrontend/Csem.v3
-rw-r--r--cfrontend/Cshmgen.v2
-rw-r--r--cfrontend/Cshmgenproof.v4
-rw-r--r--cfrontend/Ctypes.v231
-rw-r--r--cfrontend/Initializers.v13
-rw-r--r--cfrontend/Initializersproof.v52
-rw-r--r--cfrontend/PrintCsyntax.ml6
-rw-r--r--cfrontend/SimplLocalsproof.v18
-rw-r--r--cparser/C.mli1
-rw-r--r--cparser/Cprint.ml1
-rw-r--r--cparser/Cutil.ml26
-rw-r--r--cparser/Cutil.mli8
-rw-r--r--cparser/Elab.ml21
-rw-r--r--cparser/Lexer.mll5
-rw-r--r--cparser/PackedStructs.ml386
-rw-r--r--cparser/Parser.mly20
-rw-r--r--exportclight/Clightdefs.v28
-rw-r--r--exportclight/ExportClight.ml13
-rw-r--r--lib/Camlcoq.ml55
-rw-r--r--test/regression/packedstruct1.c14
-rw-r--r--test/regression/packedstruct2.c10
26 files changed, 538 insertions, 428 deletions
diff --git a/.depend b/.depend
index 0e6c556..24941d8 100644
--- a/.depend
+++ b/.depend
@@ -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
diff --git a/Changelog b/Changelog
index abc016a..e53b46c 100644
--- a/Changelog
+++ b/Changelog
@@ -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 20e00c8..dd9cfbf 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -206,9 +206,21 @@ let convertInt n = coqint_of_camlint(Int64.to_int32 n)
(** Attributes *)
-let convertAttr a = List.mem AVolatile a
-
-let mergeAttr a1 a2 = a1 || a2
+let rec log2 n = if n = 1 then 0 else 1 + log2 (n lsr 1)
+
+let convertAttr a =
+ { attr_volatile = List.mem AVolatile a;
+ attr_alignas =
+ let n = Cutil.alignas_attribute a in
+ if n > 0 then Some (N.of_int (log2 n)) else None }
+
+let mergeAttr a1 a2 =
+ { attr_volatile = a1.attr_volatile || a2.attr_volatile;
+ attr_alignas =
+ match a1.attr_alignas, a2.attr_alignas with
+ | None, aa -> aa
+ | aa, None -> aa
+ | Some n1, Some n2 -> Some (if N.le n1 n2 then n1 else n2) }
let mergeTypAttr ty a2 =
match ty with
@@ -340,9 +352,10 @@ let rec convertTypList env = function
| t1 :: tl -> Tcons(convertTyp env t1, convertTypList env tl)
let cacheCompositeDef env su id attr flds =
- (* we currently ignore attributes on structs and unions *)
let ty =
- match su with C.Struct -> C.TStruct(id, []) | C.Union -> C.TUnion(id, []) in
+ match su with
+ | C.Struct -> C.TStruct(id, attr)
+ | C.Union -> C.TUnion(id, attr) in
Hashtbl.add compositeCache id (convertTyp env ty)
let rec projFunType env ty =
@@ -821,6 +834,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
let id' = intern_string id.name in
let ty' = convertTyp env ty in
let sz = Ctypes.sizeof ty' in
+ let al = Ctypes.alignof ty' in
let attr = Cutil.attributes_of_type env ty in
let init' =
match optinit with
@@ -828,10 +842,6 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
if sto = C.Storage_extern then [] else [Init_space sz]
| Some i ->
convertInitializer env ty i in
- let align =
- match Cutil.find_custom_attributes ["aligned"; "__aligned__"] attr with
- | [[C.AInt n]] -> Some(Int64.to_int n)
- | _ -> Cutil.alignof env ty in
let (section, near_access) =
Sections.for_variable env id' ty (optinit <> None) in
if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then
@@ -839,7 +849,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
id.name (Z.to_string sz));
Hashtbl.add decl_atom id'
{ a_storage = sto;
- a_alignment = align;
+ a_alignment = Some (Z.to_int al);
a_sections = [section];
a_small_data = near_access;
a_inline = false;
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 70a02c1..f83c700 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -285,7 +285,7 @@ Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) : o
end.
Definition assign_copy_ok (ty: type) (b: block) (ofs: int) (b': block) (ofs': int) : Prop :=
- (alignof ty | Int.unsigned ofs') /\ (alignof ty | Int.unsigned ofs) /\
+ (alignof_blockcopy ty | Int.unsigned ofs') /\ (alignof_blockcopy ty | Int.unsigned ofs) /\
(b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs
\/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs
\/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs').
@@ -295,9 +295,10 @@ Remark check_assign_copy:
{ assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }.
Proof with try (right; intuition omega).
intros. unfold assign_copy_ok.
- assert (alignof ty > 0). apply alignof_pos; auto.
- destruct (Zdivide_dec (alignof ty) (Int.unsigned ofs')); auto...
- destruct (Zdivide_dec (alignof ty) (Int.unsigned ofs)); auto...
+ assert (alignof_blockcopy ty > 0).
+ { unfold alignof_blockcopy. apply Z.min_case. omega. apply alignof_pos. }
+ destruct (Zdivide_dec (alignof_blockcopy ty) (Int.unsigned ofs')); auto...
+ destruct (Zdivide_dec (alignof_blockcopy ty) (Int.unsigned ofs)); auto...
assert (Y: {b' <> b \/
Int.unsigned ofs' = Int.unsigned ofs \/
Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 3bd06df..6a57999 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -218,7 +218,8 @@ Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int):
assign_loc ty m b ofs v m'
| assign_loc_copy: forall b' ofs' bytes m',
access_mode ty = By_copy ->
- (alignof ty | Int.unsigned ofs') -> (alignof ty | Int.unsigned ofs) ->
+ (alignof_blockcopy ty | Int.unsigned ofs') ->
+ (alignof_blockcopy ty | Int.unsigned ofs) ->
b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs
\/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs
\/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs' ->
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 0f9b3f8..5d94c53 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -91,7 +91,8 @@ Inductive assign_loc {F V: Type} (ge: Genv.t F V) (ty: type) (m: mem) (b: block)
assign_loc ge ty m b ofs v t m'
| assign_loc_copy: forall b' ofs' bytes m',
access_mode ty = By_copy ->
- (alignof ty | Int.unsigned ofs') -> (alignof ty | Int.unsigned ofs) ->
+ (alignof_blockcopy ty | Int.unsigned ofs') ->
+ (alignof_blockcopy ty | Int.unsigned ofs) ->
b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs
\/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs
\/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs' ->
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index a303a7f..fd34985 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -307,7 +307,7 @@ Definition make_load (addr: expr) (ty_res: type) :=
by-copy assignment of a value of Clight type [ty]. *)
Definition make_memcpy (dst src: expr) (ty: type) :=
- Sbuiltin None (EF_memcpy (Ctypes.sizeof ty) (Ctypes.alignof ty))
+ Sbuiltin None (EF_memcpy (Ctypes.sizeof ty) (Ctypes.alignof_blockcopy ty))
(dst :: src :: nil).
(** [make_store addr ty rhs] stores the value of the
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 24576fc..7906944 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -657,9 +657,9 @@ Proof.
econstructor.
econstructor. eauto. econstructor. eauto. constructor.
econstructor; eauto.
- apply alignof_1248.
+ apply alignof_blockcopy_1248.
apply sizeof_pos.
- apply sizeof_alignof_compat.
+ eapply Zdivide_trans. apply alignof_blockcopy_divides. apply sizeof_alignof_compat.
Qed.
Lemma make_store_correct:
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 8d00b95..abd015c 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -45,14 +45,15 @@ Inductive floatsize : Type :=
| F32: floatsize
| F64: floatsize.
-(** Every type carries a set of attributes. Currently, only one
- attribute is modeled: [volatile]. *)
+(** Every type carries a set of attributes. Currently, only two
+ attributes are modeled: [volatile] and [_Alignas(n)] (from ISO C 2011). *)
Record attr : Type := mk_attr {
- attr_volatile: bool
+ attr_volatile: bool;
+ attr_alignas: option N (**r log2 of required alignment *)
}.
-Definition noattr := {| attr_volatile := false |}.
+Definition noattr := {| attr_volatile := false; attr_alignas := None |}.
(** The syntax of type expressions. Some points to note:
- Array types [Tarray n] carry the size [n] of the array.
@@ -113,10 +114,11 @@ Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2}
with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2}
with fieldlist_eq: forall (fld1 fld2: fieldlist), {fld1=fld2} + {fld1<>fld2}.
Proof.
- assert (forall (x y: intsize), {x=y} + {x<>y}). decide equality.
- assert (forall (x y: signedness), {x=y} + {x<>y}). decide equality.
- assert (forall (x y: floatsize), {x=y} + {x<>y}). decide equality.
- assert (forall (x y: attr), {x=y} + {x<>y}). decide equality. apply bool_dec.
+ assert (forall (x y: intsize), {x=y} + {x<>y}) by decide equality.
+ assert (forall (x y: signedness), {x=y} + {x<>y}) by decide equality.
+ assert (forall (x y: floatsize), {x=y} + {x<>y}) by decide equality.
+ assert (forall (x y: attr), {x=y} + {x<>y}).
+ { decide equality. decide equality. apply N.eq_dec. apply bool_dec. }
generalize ident_eq zeq. intros E1 E2.
decide equality.
decide equality.
@@ -161,21 +163,25 @@ Definition typeconv (ty: type) : type :=
(** Natural alignment of a type, in bytes. *)
Fixpoint alignof (t: type) : Z :=
- match t with
- | Tvoid => 1
- | Tint I8 _ _ => 1
- | Tint I16 _ _ => 2
- | Tint I32 _ _ => 4
- | Tint IBool _ _ => 1
- | Tlong _ _ => 8
- | Tfloat F32 _ => 4
- | Tfloat F64 _ => 8
- | Tpointer _ _ => 4
- | Tarray t' _ _ => alignof t'
- | Tfunction _ _ => 1
- | Tstruct _ fld _ => alignof_fields fld
- | Tunion _ fld _ => alignof_fields fld
- | Tcomp_ptr _ _ => 4
+ match attr_alignas (attr_of_type t) with
+ | Some l => two_p (Z.of_N l)
+ | None =>
+ match t with
+ | Tvoid => 1
+ | Tint I8 _ _ => 1
+ | Tint I16 _ _ => 2
+ | Tint I32 _ _ => 4
+ | Tint IBool _ _ => 1
+ | Tlong _ _ => 8
+ | Tfloat F32 _ => 4
+ | Tfloat F64 _ => 8
+ | Tpointer _ _ => 4
+ | Tarray t' _ _ => alignof t'
+ | Tfunction _ _ => 1
+ | Tstruct _ fld _ => alignof_fields fld
+ | Tunion _ fld _ => alignof_fields fld
+ | Tcomp_ptr _ _ => 4
+ end
end
with alignof_fields (f: fieldlist) : Z :=
@@ -187,49 +193,72 @@ with alignof_fields (f: fieldlist) : Z :=
Scheme type_ind2 := Induction for type Sort Prop
with fieldlist_ind2 := Induction for fieldlist Sort Prop.
-Lemma alignof_1248:
- forall t, alignof t = 1 \/ alignof t = 2 \/ alignof t = 4 \/ alignof t = 8
-with alignof_fields_1248:
- forall f, alignof_fields f = 1 \/ alignof_fields f = 2 \/ alignof_fields f = 4 \/ alignof_fields f = 8.
+Lemma alignof_two_p:
+ forall t, exists n, alignof t = two_power_nat n
+with alignof_fields_two_p:
+ forall f, exists n, alignof_fields f = two_power_nat n.
Proof.
- induction t; simpl; auto.
- destruct i; auto.
- destruct f; auto.
- induction f; simpl; auto.
- rewrite Zmax_spec. destruct (zlt (alignof_fields f) (alignof t)); auto.
+ assert (X: forall t a,
+ (exists n, a = two_power_nat n) ->
+ exists n,
+ match attr_alignas (attr_of_type t) with
+ | Some l => two_p (Z.of_N l)
+ | None => a
+ end = two_power_nat n).
+ {
+ intros.
+ destruct (attr_alignas (attr_of_type t)).
+ exists (N.to_nat n). rewrite two_power_nat_two_p. rewrite N_nat_Z. auto.
+ auto.
+ }
+ induction t; apply X; simpl; auto.
+ exists 0%nat; auto.
+ destruct i.
+ exists 0%nat; auto. exists 1%nat; auto. exists 2%nat; auto.
+ exists 0%nat; auto. exists 3%nat; auto.
+ destruct f.
+ exists 2%nat; auto. exists 3%nat; auto.
+ exists 2%nat; auto.
+ exists 0%nat; auto.
+ exists 2%nat; auto.
+ induction f; simpl.
+ exists 0%nat; auto.
+ apply Z.max_case; auto.
Qed.
Lemma alignof_pos:
forall t, alignof t > 0.
Proof.
- intros. generalize (alignof_1248 t). omega.
+ intros. destruct (alignof_two_p t) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
Qed.
Lemma alignof_fields_pos:
forall f, alignof_fields f > 0.
Proof.
- intros. generalize (alignof_fields_1248 f). omega.
+ intros. destruct (alignof_fields_two_p f) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
Qed.
(** Size of a type, in bytes. *)
Fixpoint sizeof (t: type) : Z :=
- match t with
- | Tvoid => 1
- | Tint I8 _ _ => 1
- | Tint I16 _ _ => 2
- | Tint I32 _ _ => 4
- | Tint IBool _ _ => 1
- | Tlong _ _ => 8
- | Tfloat F32 _ => 4
- | Tfloat F64 _ => 8
- | Tpointer _ _ => 4
- | Tarray t' n _ => sizeof t' * Zmax 1 n
- | Tfunction _ _ => 1
- | Tstruct _ fld _ => align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
- | Tunion _ fld _ => align (Zmax 1 (sizeof_union fld)) (alignof t)
- | Tcomp_ptr _ _ => 4
- end
+ let sz :=
+ match t with
+ | Tvoid => 1
+ | Tint I8 _ _ => 1
+ | Tint I16 _ _ => 2
+ | Tint I32 _ _ => 4
+ | Tint IBool _ _ => 1
+ | Tlong _ _ => 8
+ | Tfloat F32 _ => 4
+ | Tfloat F64 _ => 8
+ | Tpointer _ _ => 4
+ | Tarray t' n _ => sizeof t' * Zmax 1 n
+ | Tfunction _ _ => 1
+ | Tstruct _ fld _ => Zmax 1 (sizeof_struct fld 0)
+ | Tunion _ fld _ => Zmax 1 (sizeof_union fld)
+ | Tcomp_ptr _ _ => 4
+ end
+ in align sz (alignof t)
with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z :=
match fld with
@@ -246,23 +275,15 @@ with sizeof_union (fld: fieldlist) : Z :=
Lemma sizeof_pos:
forall t, sizeof t > 0.
Proof.
- intro t0.
- apply (type_ind2 (fun t => sizeof t > 0)
- (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0));
- intros; simpl; auto; try omega.
+ assert (X: forall t sz, sz > 0 -> align sz (alignof t) > 0).
+ {
+ intros. generalize (align_le sz (alignof t) (alignof_pos t)). omega.
+ }
+Local Opaque alignof.
+ induction t; simpl; apply X; try xomega.
destruct i; omega.
destruct f; omega.
- apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega.
- destruct H.
- generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)).
- generalize (Zmax1 1 (sizeof_struct f 0)). omega.
- generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)).
- generalize (Zmax1 1 (sizeof_union f)). omega.
- split. omega. auto.
- destruct H0. split; intros.
- generalize (Zmax2 (sizeof t) (sizeof_union f)). omega.
- apply H1.
- generalize (align_le pos (alignof t) (alignof_pos t)). omega.
+ apply Zmult_gt_0_compat. auto. xomega.
Qed.
Lemma sizeof_struct_incr:
@@ -271,17 +292,14 @@ Proof.
induction fld; intros; simpl. omega.
eapply Zle_trans. 2: apply IHfld.
apply Zle_trans with (align pos (alignof t)).
- apply align_le. apply alignof_pos.
- assert (sizeof t > 0) by apply sizeof_pos. omega.
+ apply align_le. apply alignof_pos.
+ generalize (sizeof_pos t); omega.
Qed.
Lemma sizeof_alignof_compat:
forall t, (alignof t | sizeof t).
Proof.
- induction t; simpl; try (apply Zdivide_refl).
- apply Zdivide_mult_l. auto.
- apply align_divides. apply alignof_fields_pos.
- apply align_divides. apply alignof_fields_pos.
+ intros. destruct t; apply align_divides; apply alignof_pos.
Qed.
(** Byte offset for a field in a struct or union.
@@ -333,7 +351,7 @@ Lemma field_offset_in_range:
Proof.
intros. exploit field_offset_rec_in_range; eauto. intros [A B].
split. auto. simpl. eapply Zle_trans. eauto.
- eapply Zle_trans. eapply Zle_max_r. apply align_le. apply alignof_fields_pos.
+ eapply Zle_trans. eapply Zle_max_r. apply align_le. apply alignof_pos.
Qed.
(** Second, two distinct fields do not overlap *)
@@ -484,40 +502,83 @@ with unroll_composite_fields (fld: fieldlist) : fieldlist :=
| Fcons id ty fld' => Fcons id (unroll_composite ty) (unroll_composite_fields fld')
end.
+Lemma attr_of_type_unroll_composite:
+ forall ty, attr_of_type (unroll_composite ty) = attr_of_type ty.
+Proof.
+ intros. destruct ty; simpl; auto; destruct (ident_eq i cid); auto.
+Qed.
+
Lemma alignof_unroll_composite:
forall ty, alignof (unroll_composite ty) = alignof ty.
Proof.
+Local Transparent alignof.
apply (type_ind2 (fun ty => alignof (unroll_composite ty) = alignof ty)
(fun fld => alignof_fields (unroll_composite_fields fld) = alignof_fields fld));
simpl; intros; auto.
- destruct (ident_eq i cid); auto.
- destruct (ident_eq i cid); auto.
- destruct (ident_eq i cid); auto.
- decEq; auto.
+ rewrite H; auto.
+ destruct (ident_eq i cid); auto. simpl. rewrite H; auto.
+ destruct (ident_eq i cid); auto. simpl. rewrite H; auto.
+ destruct (ident_eq i cid); auto. congruence.
Qed.
Lemma sizeof_unroll_composite:
forall ty, sizeof (unroll_composite ty) = sizeof ty.
Proof.
-Opaque alignof.
+Local Opaque alignof.
apply (type_ind2 (fun ty => sizeof (unroll_composite ty) = sizeof ty)
(fun fld =>
sizeof_union (unroll_composite_fields fld) = sizeof_union fld
/\ forall pos,
sizeof_struct (unroll_composite_fields fld) pos = sizeof_struct fld pos));
simpl; intros; auto.
- congruence.
- destruct H. rewrite <- (alignof_unroll_composite (Tstruct i f a)).
- simpl. destruct (ident_eq i cid); simpl. auto. rewrite H0; auto.
- destruct H. rewrite <- (alignof_unroll_composite (Tunion i f a)).
- simpl. destruct (ident_eq i cid); simpl. auto. rewrite H; auto.
- destruct (ident_eq i cid); auto.
- destruct H0. split. congruence.
- intros. rewrite alignof_unroll_composite. rewrite H1. rewrite H. auto.
+- rewrite H. rewrite <- (alignof_unroll_composite (Tarray t z a)). auto.
+- rewrite <- (alignof_unroll_composite (Tstruct i f a)). simpl.
+ destruct H. destruct (ident_eq i cid). auto. simpl. rewrite H0. auto.
+- rewrite <- (alignof_unroll_composite (Tunion i f a)). simpl.
+ destruct H. destruct (ident_eq i cid). auto. simpl. rewrite H. auto.
+- destruct (ident_eq i cid); auto.
+- destruct H0. split.
+ + congruence.
+ + intros. rewrite H1. rewrite H. rewrite alignof_unroll_composite. auto.
Qed.
End UNROLL_COMPOSITE.
+(** A variatn of [alignof] for use in block copy operations
+ (which do not support alignments greater than 8). *)
+
+Definition alignof_blockcopy (ty: type) := Zmin 8 (alignof ty).
+
+Lemma alignof_blockcopy_1248:
+ forall ty, let a := alignof_blockcopy ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8.
+Proof.
+ intros. unfold a, alignof_blockcopy.
+ destruct (alignof_two_p ty) as [n EQ]. rewrite EQ.
+ destruct n; auto.
+ destruct n; auto.
+ destruct n; auto.
+ right; right; right. apply Z.min_l.
+ rewrite two_power_nat_two_p. rewrite ! inj_S.
+ change 8 with (two_p 3).
+ apply two_p_monotone. omega.
+Qed.
+
+Lemma alignof_blockcopy_divides:
+ forall ty, (alignof_blockcopy ty | alignof ty).
+Proof.
+ intros. unfold alignof_blockcopy.
+ destruct (alignof_two_p ty) as [n EQ]. rewrite EQ.
+ destruct n. apply Zdivide_refl.
+ destruct n. apply Zdivide_refl.
+ destruct n. apply Zdivide_refl.
+ replace (two_power_nat (S(S(S n)))) with (two_p (3 + Z.of_nat n)).
+ rewrite two_p_is_exp by omega. change (two_p 3) with 8.
+ apply Z.min_case.
+ exists (two_p (Z.of_nat n)). ring.
+ apply Zdivide_refl.
+ rewrite two_power_nat_two_p. rewrite !inj_S. f_equal. omega.
+Qed.
+
(** Extracting a type list from a function parameter declaration. *)
Fixpoint type_of_params (params: list (ident * type)) : typelist :=
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index e7debfc..ec06cfd 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -19,6 +19,7 @@ Require Import Floats.
Require Import Values.
Require Import AST.
Require Import Memory.
+Require Import Globalenvs.
Require Import Ctypes.
Require Import Cop.
Require Import Csyntax.
@@ -173,11 +174,15 @@ Fixpoint transl_init (ty: type) (i: initializer)
{struct i} : res (list init_data) :=
match i, ty with
| Init_single a, _ =>
- do d <- transl_init_single ty a; OK (d :: nil)
+ do d <- transl_init_single ty a;
+ OK (d :: padding (Genv.init_data_size d) (sizeof ty))
| Init_compound il, Tarray tyelt sz _ =>
- if zle sz 0
- then OK (Init_space(sizeof tyelt) :: nil)
- else transl_init_array tyelt il sz
+ if zle sz 0 then
+ OK (Init_space(sizeof ty) :: nil)
+ else
+ do dl <- transl_init_array tyelt il sz;
+ OK(let n := sizeof ty - sizeof tyelt * sz in
+ if zle n 0 then dl else dl ++ Init_space n :: nil)
| Init_compound il, Tstruct _ Fnil _ =>
OK (Init_space (sizeof ty) :: nil)
| Init_compound il, Tstruct id fl _ =>
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index f3de05c..ef9ec6c 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -523,21 +523,22 @@ Qed.
Lemma transl_init_single_size:
forall ty a data,
transl_init_single ty a = OK data ->
- Genv.init_data_size data = sizeof ty.
-Proof.
+ Genv.init_data_size data <= sizeof ty.
+Proof with (simpl; apply align_le; apply alignof_pos).
+Local Opaque alignof.
intros. monadInv H. destruct x0.
monadInv EQ2.
destruct ty; try discriminate.
- destruct i0; inv EQ2; reflexivity.
- inv EQ2; reflexivity.
- inv EQ2; reflexivity.
- destruct ty; inv EQ2; reflexivity.
+ destruct i0; inv EQ2...
+ inv EQ2...
+ inv EQ2...
+ destruct ty; inv EQ2...
destruct ty; try discriminate.
- destruct f0; inv EQ2; reflexivity.
+ destruct f0; inv EQ2...
destruct ty; try discriminate.
- destruct i0; inv EQ2; reflexivity.
- inv EQ2; reflexivity.
- inv EQ2; reflexivity.
+ destruct i0; inv EQ2...
+ inv EQ2...
+ inv EQ2...
Qed.
Notation idlsize := Genv.init_data_list_size.
@@ -616,25 +617,31 @@ with transl_init_list_size:
Proof.
induction i; intros.
(* single *)
- monadInv H. simpl. rewrite (transl_init_single_size _ _ _ EQ). omega.
+ monadInv H. simpl. rewrite padding_size. omega. eapply transl_init_single_size; eauto.
(* compound *)
simpl in H. destruct ty; try discriminate.
(* compound array *)
- destruct (zle z 0).
- monadInv H. simpl. repeat rewrite Zmax_spec. rewrite zlt_true. rewrite zlt_true. ring.
- omega. generalize (sizeof_pos ty); omega.
- simpl. rewrite Zmax_spec. rewrite zlt_false.
- eapply (proj1 (transl_init_list_size il)). auto. omega.
+ set (sz := sizeof (Tarray ty z a)) in *.
+ destruct (zle z 0). inv H. simpl. rewrite Z.max_l. omega.
+ generalize (sizeof_pos (Tarray ty z a)). unfold sz; omega.
+ monadInv H. exploit (proj1 (transl_init_list_size il)); eauto. intros SX.
+ assert (sizeof ty * z <= sz).
+ { unfold sz. simpl. rewrite Z.max_r. apply align_le; apply alignof_pos. omega. }
+ destruct (zle (sz - sizeof ty * z)).
+ omega.
+ rewrite idlsize_app. simpl. rewrite Z.max_l by omega. omega.
(* compound struct *)
- destruct f.
- inv H. reflexivity.
+ set (sz := sizeof (Tstruct i f a)) in *.
+ destruct f.
+ inv H. simpl. rewrite Z.max_l. omega. generalize (sizeof_pos (Tstruct i Fnil a)); unfold sz; omega.
replace (idlsize data) with (idlsize data + 0) by omega.
eapply (proj1 (proj2 (transl_init_list_size il))). eauto.
rewrite sizeof_struct_eq. 2: congruence.
apply align_le. apply alignof_pos.
(* compound union *)
+ set (sz := sizeof (Tunion i f a)) in *.
destruct f.
- inv H. reflexivity.
+ inv H. simpl. rewrite Z.max_l. omega. generalize (sizeof_pos (Tunion i Fnil a)); unfold sz; omega.
eapply (proj2 (proj2 (transl_init_list_size il))). eauto.
rewrite sizeof_union_eq. 2: congruence.
eapply Zle_trans. 2: apply align_le. simpl. apply Zmax_bound_l. omega.
@@ -767,12 +774,17 @@ Proof.
(* single *)
monadInv H3.
exploit transl_init_single_steps; eauto. intros.
- simpl. rewrite H3. auto.
+ simpl. rewrite H3. apply store_init_data_list_padding.
(* array *)
destruct (zle sz 0).
exploit exec_init_array_length; eauto. destruct il; intros.
subst. inv H. inv H1. auto. omegaContradiction.
+ monadInv H1.
+ change (align (sizeof ty * Z.max 1 sz) (alignof (Tarray ty sz a)))
+ with (sizeof (Tarray ty sz a)).
+ destruct (zle (sizeof (Tarray ty sz a) - sizeof ty * sz) 0).
eauto.
+ eapply store_init_data_list_app; eauto.
(* struct *)
destruct fl.
inv H. inv H1. auto.
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 897a2ee..ec82869 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -78,7 +78,11 @@ let struct_unions = ref StructUnion.empty
(* Declarator (identifier + type) *)
let attributes a =
- if attr_volatile a then " volatile" else ""
+ let s1 = if a.attr_volatile then " volatile" else "" in
+ match a.attr_alignas with
+ | None -> s1
+ | Some l ->
+ sprintf " _Alignas(%Ld)%s" (Int64.shift_left 1L (N.to_int l)) s1
let name_optid id =
if id = "" then "" else " " ^ id
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 83e7375..62bbd67 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -761,10 +761,12 @@ Qed.
Lemma sizeof_by_value:
forall ty chunk,
- access_mode ty = By_value chunk -> sizeof ty = size_chunk chunk.
+ access_mode ty = By_value chunk -> size_chunk chunk <= sizeof ty.
Proof.
- unfold access_mode; intros.
- destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto.
+ unfold access_mode; intros.
+Local Opaque alignof.
+ destruct ty; try destruct i; try destruct s; try destruct f; inv H;
+ apply align_le; apply alignof_pos.
Qed.
Definition env_initial_value (e: env) (m: mem) :=
@@ -782,7 +784,7 @@ Proof.
apply IHalloc_variables. red; intros. rewrite PTree.gsspec in H2.
destruct (peq id0 id). inv H2.
eapply Mem.load_alloc_same'; eauto.
- omega. erewrite sizeof_by_value; eauto. omega.
+ omega. rewrite Zplus_0_l. eapply sizeof_by_value; eauto.
apply Zdivide_0.
eapply Mem.load_alloc_other; eauto.
Qed.
@@ -1044,10 +1046,10 @@ Proof.
exploit Mem.storebytes_mapped_inject; eauto. intros [tm' [C D]].
exists tm'.
split. eapply assign_loc_copy; try rewrite EQ1; try rewrite EQ2; eauto.
- eapply Mem.aligned_area_inject with (m := m); eauto. apply alignof_1248.
- apply sizeof_alignof_compat.
- eapply Mem.aligned_area_inject with (m := m); eauto. apply alignof_1248.
- apply sizeof_alignof_compat.
+ eapply Mem.aligned_area_inject with (m := m); eauto. apply alignof_blockcopy_1248.
+ eapply Zdivide_trans. apply alignof_blockcopy_divides. apply sizeof_alignof_compat.
+ eapply Mem.aligned_area_inject with (m := m); eauto. apply alignof_blockcopy_1248.
+ eapply Zdivide_trans. apply alignof_blockcopy_divides. apply sizeof_alignof_compat.
eapply Mem.disjoint_or_equal_inject with (m := m); eauto.
apply Mem.range_perm_max with Cur; auto.
apply Mem.range_perm_max with Cur; auto.
diff --git a/cparser/C.mli b/cparser/C.mli
index ce58504..5d90407 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 e97f041..c6864ff 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 2fc269c..982bf78 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 7e23a72..98ab54e 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 fa9fd24..b25ad55 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 0820e4e..90e4d3c 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 13a00ce..5d0bac9 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 83b1984..cd515de 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 1cb93d5..246e12c 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 9027f86..8c83fab 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 30e6705..929b61e 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 e7b6c1d..e5526ed 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 0c383a4..37c736e 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 };
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 07:54:35 +0000