From fe8baff11737d3785ff51d20ace9ab31665cd295 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 12 May 2011 09:41:09 +0000 Subject: cparser: support for attributes over struct and union. cparser: added experimental emulation of packed structs (PackedStruct.ml) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1650 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cparser/.depend | 154 ++++++++--------- cparser/Bitfields.ml | 6 +- cparser/C.mli | 5 +- cparser/Cleanup.ml | 6 +- cparser/Cprint.ml | 10 +- cparser/Cutil.ml | 34 +++- cparser/Cutil.mli | 6 +- cparser/Elab.ml | 39 +++-- cparser/Env.ml | 1 + cparser/Env.mli | 1 + cparser/Makefile | 2 +- cparser/PackedStructs.ml | 434 +++++++++++++++++++++++++++++++++++++++++++++++ cparser/Parse.ml | 4 +- cparser/Rename.ml | 9 +- cparser/StructByValue.ml | 6 +- cparser/Transform.ml | 23 ++- cparser/Transform.mli | 8 +- 17 files changed, 613 insertions(+), 135 deletions(-) create mode 100644 cparser/PackedStructs.ml (limited to 'cparser') diff --git a/cparser/.depend b/cparser/.depend index d2338ef..2d6b280 100644 --- a/cparser/.depend +++ b/cparser/.depend @@ -1,86 +1,88 @@ -AddCasts.cmi: C.cmi -Bitfields.cmi: C.cmi -Builtins.cmi: Env.cmi C.cmi -Ceval.cmi: Env.cmi C.cmi -Cleanup.cmi: C.cmi -C.cmi: -Cprint.cmi: C.cmi -Cutil.cmi: Env.cmi C.cmi -Elab.cmi: C.cmi -Env.cmi: C.cmi -Errors.cmi: -GCC.cmi: Builtins.cmi -Lexer.cmi: Parser.cmi -Machine.cmi: -PackedStructs.cmi: C.cmi -Parse_aux.cmi: -Parse.cmi: C.cmi -Parser.cmi: Cabs.cmo -Rename.cmi: C.cmi -SimplExpr.cmi: C.cmi -StructAssign.cmi: C.cmi -StructByValue.cmi: C.cmi -Transform.cmi: Env.cmi C.cmi -Unblock.cmi: C.cmi -AddCasts.cmo: Transform.cmi Cutil.cmi C.cmi AddCasts.cmi -AddCasts.cmx: Transform.cmx Cutil.cmx C.cmi AddCasts.cmi -Bitfields.cmo: Transform.cmi Machine.cmi Cutil.cmi C.cmi Bitfields.cmi -Bitfields.cmx: Transform.cmx Machine.cmx Cutil.cmx C.cmi Bitfields.cmi -Builtins.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi -Builtins.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmi -Cabshelper.cmo: Cabs.cmo -Cabshelper.cmx: Cabs.cmx -Cabs.cmo: -Cabs.cmx: -Ceval.cmo: Machine.cmi Cutil.cmi C.cmi Ceval.cmi -Ceval.cmx: Machine.cmx Cutil.cmx C.cmi Ceval.cmi -Cleanup.cmo: Cutil.cmi C.cmi Cleanup.cmi -Cleanup.cmx: Cutil.cmx C.cmi Cleanup.cmi -Cprint.cmo: C.cmi Cprint.cmi -Cprint.cmx: C.cmi Cprint.cmi -Cutil.cmo: Machine.cmi Errors.cmi Env.cmi Cprint.cmi C.cmi Cutil.cmi -Cutil.cmx: Machine.cmx Errors.cmx Env.cmx Cprint.cmx C.cmi Cutil.cmi +AddCasts.cmi: C.cmi +Bitfields.cmi: C.cmi +Builtins.cmi: Env.cmi C.cmi +C.cmi: +Ceval.cmi: Env.cmi C.cmi +Cleanup.cmi: C.cmi +Cprint.cmi: C.cmi +Cutil.cmi: Env.cmi C.cmi +Elab.cmi: C.cmi +Env.cmi: C.cmi +Errors.cmi: +GCC.cmi: Builtins.cmi +Lexer.cmi: Parser.cmi +Machine.cmi: +PackedStructs.cmi: C.cmi +Parse.cmi: C.cmi +Parse_aux.cmi: +Parser.cmi: Cabs.cmo +Rename.cmi: C.cmi +SimplExpr.cmi: C.cmi +StructAssign.cmi: C.cmi +StructByValue.cmi: C.cmi +Transform.cmi: Env.cmi C.cmi +Unblock.cmi: C.cmi +AddCasts.cmo: Transform.cmi Cutil.cmi C.cmi AddCasts.cmi +AddCasts.cmx: Transform.cmx Cutil.cmx C.cmi AddCasts.cmi +Bitfields.cmo: Transform.cmi Machine.cmi Cutil.cmi C.cmi Bitfields.cmi +Bitfields.cmx: Transform.cmx Machine.cmx Cutil.cmx C.cmi Bitfields.cmi +Builtins.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi +Builtins.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmi +Cabs.cmo: +Cabs.cmx: +Cabshelper.cmo: Cabs.cmo +Cabshelper.cmx: Cabs.cmx +Ceval.cmo: Machine.cmi Cutil.cmi C.cmi Ceval.cmi +Ceval.cmx: Machine.cmx Cutil.cmx C.cmi Ceval.cmi +Cleanup.cmo: Cutil.cmi C.cmi Cleanup.cmi +Cleanup.cmx: Cutil.cmx C.cmi Cleanup.cmi +Cprint.cmo: C.cmi Cprint.cmi +Cprint.cmx: C.cmi Cprint.cmi +Cutil.cmo: Machine.cmi Errors.cmi Env.cmi Cprint.cmi C.cmi Cutil.cmi +Cutil.cmx: Machine.cmx Errors.cmx Env.cmx Cprint.cmx C.cmi Cutil.cmi Elab.cmo: Parser.cmi Machine.cmi Lexer.cmi Errors.cmi Env.cmi Cutil.cmi \ Cprint.cmi Cleanup.cmi Ceval.cmi Cabshelper.cmo Cabs.cmo C.cmi \ - Builtins.cmi Elab.cmi + Builtins.cmi Elab.cmi Elab.cmx: Parser.cmx Machine.cmx Lexer.cmx Errors.cmx Env.cmx Cutil.cmx \ Cprint.cmx Cleanup.cmx Ceval.cmx Cabshelper.cmx Cabs.cmx C.cmi \ - Builtins.cmx Elab.cmi -Env.cmo: C.cmi Env.cmi -Env.cmx: C.cmi Env.cmi -Errors.cmo: Errors.cmi -Errors.cmx: Errors.cmi -GCC.cmo: Cutil.cmi C.cmi Builtins.cmi GCC.cmi -GCC.cmx: Cutil.cmx C.cmi Builtins.cmx GCC.cmi -Lexer.cmo: Parser.cmi Parse_aux.cmi Cabshelper.cmo Lexer.cmi -Lexer.cmx: Parser.cmx Parse_aux.cmx Cabshelper.cmx Lexer.cmi -Machine.cmo: Machine.cmi -Machine.cmx: Machine.cmi -Main.cmo: Parse.cmi GCC.cmi Cprint.cmi Builtins.cmi -Main.cmx: Parse.cmx GCC.cmx Cprint.cmx Builtins.cmx + Builtins.cmx Elab.cmi +Env.cmo: C.cmi Env.cmi +Env.cmx: C.cmi Env.cmi +Errors.cmo: Errors.cmi +Errors.cmx: Errors.cmi +GCC.cmo: Cutil.cmi C.cmi Builtins.cmi GCC.cmi +GCC.cmx: Cutil.cmx C.cmi Builtins.cmx GCC.cmi +Lexer.cmo: Parser.cmi Parse_aux.cmi Cabshelper.cmo Lexer.cmi +Lexer.cmx: Parser.cmx Parse_aux.cmx Cabshelper.cmx Lexer.cmi +Machine.cmo: Machine.cmi +Machine.cmx: Machine.cmi +Main.cmo: Parse.cmi GCC.cmi Cprint.cmi Builtins.cmi +Main.cmx: Parse.cmx GCC.cmx Cprint.cmx Builtins.cmx PackedStructs.cmo: Errors.cmi Env.cmi Cutil.cmi C.cmi Builtins.cmi \ - PackedStructs.cmi + PackedStructs.cmi PackedStructs.cmx: Errors.cmx Env.cmx Cutil.cmx C.cmi Builtins.cmx \ - PackedStructs.cmi -Parse_aux.cmo: Errors.cmi Cabshelper.cmo Parse_aux.cmi -Parse_aux.cmx: Errors.cmx Cabshelper.cmx Parse_aux.cmi + PackedStructs.cmi Parse.cmo: Unblock.cmi StructByValue.cmi StructAssign.cmi SimplExpr.cmi \ - Rename.cmi Errors.cmi Elab.cmi Bitfields.cmi AddCasts.cmi Parse.cmi + Rename.cmi PackedStructs.cmi Errors.cmi Elab.cmi Bitfields.cmi \ + AddCasts.cmi Parse.cmi Parse.cmx: Unblock.cmx StructByValue.cmx StructAssign.cmx SimplExpr.cmx \ - Rename.cmx Errors.cmx Elab.cmx Bitfields.cmx AddCasts.cmx Parse.cmi -Parser.cmo: Parse_aux.cmi Cabshelper.cmo Cabs.cmo Parser.cmi -Parser.cmx: Parse_aux.cmx Cabshelper.cmx Cabs.cmx Parser.cmi -Rename.cmo: Errors.cmi Cutil.cmi C.cmi Builtins.cmi Rename.cmi -Rename.cmx: Errors.cmx Cutil.cmx C.cmi Builtins.cmx Rename.cmi -SimplExpr.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi SimplExpr.cmi -SimplExpr.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi SimplExpr.cmi + Rename.cmx PackedStructs.cmx Errors.cmx Elab.cmx Bitfields.cmx \ + AddCasts.cmx Parse.cmi +Parse_aux.cmo: Errors.cmi Cabshelper.cmo Parse_aux.cmi +Parse_aux.cmx: Errors.cmx Cabshelper.cmx Parse_aux.cmi +Parser.cmo: Parse_aux.cmi Cabshelper.cmo Cabs.cmo Parser.cmi +Parser.cmx: Parse_aux.cmx Cabshelper.cmx Cabs.cmx Parser.cmi +Rename.cmo: Errors.cmi Cutil.cmi C.cmi Builtins.cmi Rename.cmi +Rename.cmx: Errors.cmx Cutil.cmx C.cmi Builtins.cmx Rename.cmi +SimplExpr.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi SimplExpr.cmi +SimplExpr.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi SimplExpr.cmi StructAssign.cmo: Transform.cmi Machine.cmi Errors.cmi Env.cmi Cutil.cmi \ - C.cmi StructAssign.cmi + C.cmi StructAssign.cmi StructAssign.cmx: Transform.cmx Machine.cmx Errors.cmx Env.cmx Cutil.cmx \ - C.cmi StructAssign.cmi -StructByValue.cmo: Transform.cmi Env.cmi Cutil.cmi C.cmi StructByValue.cmi -StructByValue.cmx: Transform.cmx Env.cmx Cutil.cmx C.cmi StructByValue.cmi -Transform.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi Transform.cmi -Transform.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmx Transform.cmi -Unblock.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi Unblock.cmi -Unblock.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi Unblock.cmi + C.cmi StructAssign.cmi +StructByValue.cmo: Transform.cmi Env.cmi Cutil.cmi C.cmi StructByValue.cmi +StructByValue.cmx: Transform.cmx Env.cmx Cutil.cmx C.cmi StructByValue.cmi +Transform.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi Transform.cmi +Transform.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmx Transform.cmi +Unblock.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi Unblock.cmi +Unblock.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi Unblock.cmi diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 472b6a4..5ab4eb4 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -116,10 +116,10 @@ let rec transf_members env id count = function end end -let transf_composite env su id ml = +let transf_composite env su id attr ml = match su with - | Struct -> transf_members env id 1 ml - | Union -> ml + | Struct -> (attr, transf_members env id 1 ml) + | Union -> (attr, ml) (* Bitfield manipulation expressions *) diff --git a/cparser/C.mli b/cparser/C.mli index 9d5a7d7..35e872d 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -231,8 +231,9 @@ type globdecl = and globdecl_desc = | Gdecl of decl (* variable declaration, function prototype *) | Gfundef of fundef (* function definition *) - | Gcompositedecl of struct_or_union * ident (* struct/union declaration *) - | Gcompositedef of struct_or_union * ident * field list + | Gcompositedecl of struct_or_union * ident * attributes + (* struct/union declaration *) + | Gcompositedef of struct_or_union * ident * attributes * field list (* struct/union definition *) | Gtypedef of ident * typ (* typedef *) | Genumdef of ident * (ident * exp option) list (* enum definition *) diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml index be28989..17b2f98 100644 --- a/cparser/Cleanup.ml +++ b/cparser/Cleanup.ml @@ -143,7 +143,7 @@ let rec add_needed_globdecls accu = function if needed f.fd_name then (add_fundef f; add_needed_globdecls accu rem) else add_needed_globdecls (g :: accu) rem - | Gcompositedef(_, id, flds) -> + | Gcompositedef(_, id, _, flds) -> if needed id then (List.iter add_field flds; add_needed_globdecls accu rem) else add_needed_globdecls (g :: accu) rem @@ -176,8 +176,8 @@ let rec simpl_globdecls accu = function match g.gdesc with | Gdecl((sto, id, ty, init) as decl) -> visible_decl decl || needed id | Gfundef f -> f.fd_storage = Storage_default || needed f.fd_name - | Gcompositedecl(_, id) -> needed id - | Gcompositedef(_, id, flds) -> needed id + | Gcompositedecl(_, id, _) -> needed id + | Gcompositedef(_, id, _, flds) -> needed id | Gtypedef(id, ty) -> needed id | Genumdef(id, enu) -> List.exists (fun (id, _) -> needed id) enu | Gpragma s -> true in diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 3d023a8..5887e87 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -470,13 +470,15 @@ let globdecl pp g = fprintf pp "%a@ @ " full_decl d | Gfundef f -> fundef pp f - | Gcompositedecl(kind, id) -> - fprintf pp "%s %a;@ @ " + | Gcompositedecl(kind, id, attrs) -> + fprintf pp "%s%a %a;@ @ " (match kind with Struct -> "struct" | Union -> "union") + attributes attrs ident id - | Gcompositedef(kind, id, flds) -> - fprintf pp "@[%s %a {" + | Gcompositedef(kind, id, attrs, flds) -> + fprintf pp "@[%s%a %a {" (match kind with Struct -> "struct" | Union -> "union") + attributes attrs ident id; List.iter (fun fld -> fprintf pp "@ %a;" field fld) flds; fprintf pp "@;<0 -2>};@]@ @ " diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 7aac659..2e664df 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -107,8 +107,10 @@ let rec attributes_of_type env t = | TArray(ty, sz, a) -> add_attributes a (attributes_of_type env ty) | TFun(ty, params, vararg, a) -> a | TNamed(s, a) -> attributes_of_type env (unroll env t) - | TStruct(s, a) -> a - | TUnion(s, a) -> a + | TStruct(s, a) -> + let ci = Env.find_struct env s in add_attributes ci.ci_attr a + | TUnion(s, a) -> + let ci = Env.find_union env s in add_attributes ci.ci_attr a (* Changing the attributes of a type (at top-level) *) (* Same hack as above for array types. *) @@ -377,16 +379,20 @@ let incomplete_type env t = (* Computing composite_info records *) -let composite_info_decl env su = - { ci_kind = su; ci_members = []; ci_alignof = None; ci_sizeof = None } +let composite_info_decl env su attr = + { ci_kind = su; ci_members = []; + ci_alignof = None; ci_sizeof = None; + ci_attr = attr } -let composite_info_def env su m = +let composite_info_def env su attr m = { ci_kind = su; ci_members = m; ci_alignof = alignof_struct_union env m; ci_sizeof = - match su with + begin match su with | Struct -> sizeof_struct env m - | Union -> sizeof_union env m } + | Union -> sizeof_union env m + end; + ci_attr = attr } (* Type of a function definition *) @@ -646,6 +652,17 @@ let is_literal_0 e = | EConst(CInt(0L, _, _)) -> true | _ -> false +(* Assignment compatibility check over attributes. + Standard attributes ("const", "volatile", "restrict") can safely + be added (to the rhs type to get the lhs type) but must not be dropped. + Custom attributes can safely be dropped but must not be added. *) + +let valid_assignment_attr afrom ato = + let is_covariant = function Attr _ -> false | _ -> true in + let (afrom1, afrom2) = List.partition is_covariant afrom + and (ato1, ato2) = List.partition is_covariant ato in + incl_attributes afrom1 ato1 && incl_attributes ato2 afrom2 + (* Check that an assignment is allowed *) let valid_assignment env from tto = @@ -653,7 +670,8 @@ let valid_assignment env from tto = | (TInt _ | TFloat _), (TInt _ | TFloat _) -> true | TInt _, TPtr _ -> is_literal_0 from | TPtr(ty, _), TPtr(ty', _) -> - incl_attributes (attributes_of_type env ty) (attributes_of_type env ty') + valid_assignment_attr (attributes_of_type env ty) + (attributes_of_type env ty') && (is_void_type env ty || is_void_type env ty' || compatible_types env (erase_attributes_type env ty) diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index d4c9441..7bd9119 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -69,8 +69,10 @@ val incomplete_type : Env.t -> typ -> bool (* Computing composite_info records *) -val composite_info_decl: Env.t -> struct_or_union -> Env.composite_info -val composite_info_def: Env.t -> struct_or_union -> field list -> Env.composite_info +val composite_info_decl: + Env.t -> struct_or_union -> attributes -> Env.composite_info +val composite_info_def: + Env.t -> struct_or_union -> attributes -> field list -> Env.composite_info (* Type classification functions *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index bbb049e..eaba8d8 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -417,15 +417,13 @@ let rec elab_specifier ?(only = false) loc env specifier = | [Cabs.Tstruct(id, optmembers, a)] -> let (id', env') = - elab_struct_or_union only Struct loc id optmembers env in - let attr' = add_attributes !attr (elab_attributes loc env a) in - (!sto, !inline, TStruct(id', attr'), env') + elab_struct_or_union only Struct loc id optmembers a env in + (!sto, !inline, TStruct(id', !attr), env') | [Cabs.Tunion(id, optmembers, a)] -> let (id', env') = - elab_struct_or_union only Union loc id optmembers env in - let attr' = add_attributes !attr (elab_attributes loc env a) in - (!sto, !inline, TUnion(id', attr'), env') + elab_struct_or_union only Union loc id optmembers a env in + (!sto, !inline, TUnion(id', !attr), env') | [Cabs.Tenum(id, optmembers, a)] -> let env' = @@ -581,7 +579,7 @@ and elab_field_group env (spec, fieldlist) = (* Elaboration of a struct or union *) -and elab_struct_or_union_info kind loc env members = +and elab_struct_or_union_info kind loc env members attrs = let (m, env') = mmap elab_field_group env members in let m = List.flatten m in (* Check for incomplete types *) @@ -594,11 +592,16 @@ and elab_struct_or_union_info kind loc env members = error loc "member '%s' has incomplete type" fld.fld_name; check_incomplete rem in check_incomplete m; - (composite_info_def env' kind m, env') + (composite_info_def env' kind attrs m, env') (* Elaboration of a struct or union *) -and elab_struct_or_union only kind loc tag optmembers env = +and elab_struct_or_union only kind loc tag optmembers attrs env = + let attrs' = + elab_attributes loc env attrs in + let warn_attrs () = + if attrs' <> [] then + warning loc "attributes over struct/union ignored in this context" in let optbinding = if tag = "" then None else Env.lookup_composite env tag in match optbinding, optmembers with @@ -609,16 +612,17 @@ and elab_struct_or_union only kind loc tag optmembers env = and the composite was bound in another scope, create a new incomplete composite instead via the case "_, None" below. *) + warn_attrs(); (tag', env) | Some(tag', ({ci_sizeof = None} as ci)), Some members when Env.in_current_scope env tag' -> if ci.ci_kind <> kind then error loc "struct/union mismatch on tag '%s'" tag; (* finishing the definition of an incomplete struct or union *) - let (ci', env') = elab_struct_or_union_info kind loc env members in + let (ci', env') = elab_struct_or_union_info kind loc env members attrs' in (* Emit a global definition for it *) emit_elab (elab_loc loc) - (Gcompositedef(kind, tag', ci'.ci_members)); + (Gcompositedef(kind, tag', attrs', ci'.ci_members)); (* Replace infos but keep same ident *) (tag', Env.add_composite env' tag' ci') | Some(tag', {ci_sizeof = Some _}), Some _ @@ -629,26 +633,27 @@ and elab_struct_or_union only kind loc tag optmembers env = (* declaration of an incomplete struct or union *) if tag = "" then error loc "anonymous, incomplete struct or union"; - let ci = composite_info_decl env kind in + let ci = composite_info_decl env kind attrs' in (* enter it with a new name *) let (tag', env') = Env.enter_composite env tag ci in (* emit it *) emit_elab (elab_loc loc) - (Gcompositedecl(kind, tag')); + (Gcompositedecl(kind, tag', attrs')); (tag', env') | _, Some members -> (* definition of a complete struct or union *) - let ci1 = composite_info_decl env kind in + let ci1 = composite_info_decl env kind attrs' in (* enter it, incomplete, with a new name *) let (tag', env') = Env.enter_composite env tag ci1 in (* emit a declaration so that inner structs and unions can refer to it *) emit_elab (elab_loc loc) - (Gcompositedecl(kind, tag')); + (Gcompositedecl(kind, tag', attrs')); (* elaborate the members *) - let (ci2, env'') = elab_struct_or_union_info kind loc env' members in + let (ci2, env'') = + elab_struct_or_union_info kind loc env' members attrs' in (* emit a definition *) emit_elab (elab_loc loc) - (Gcompositedef(kind, tag', ci2.ci_members)); + (Gcompositedef(kind, tag', attrs', ci2.ci_members)); (* Replace infos but keep same ident *) (tag', Env.add_composite env'' tag' ci2) diff --git a/cparser/Env.ml b/cparser/Env.ml index 777b3e1..164fe59 100644 --- a/cparser/Env.ml +++ b/cparser/Env.ml @@ -65,6 +65,7 @@ type composite_info = { ci_members: field list; (* members, in order *) ci_alignof: int option; (* alignment; None if incomplete *) ci_sizeof: int option; (* size; None if incomplete *) + ci_attr: attributes (* attributes, if any *) } (* Infos associated with an ordinary identifier *) diff --git a/cparser/Env.mli b/cparser/Env.mli index e7a74af..01f95ca 100644 --- a/cparser/Env.mli +++ b/cparser/Env.mli @@ -29,6 +29,7 @@ type composite_info = { ci_members: C.field list; (* members, in order *) ci_alignof: int option; (* alignment; None if incomplete *) ci_sizeof: int option; (* size; None if incomplete *) + ci_attr: C.attributes (* attributes, if any *) } type ident_info = II_ident of C.storage * C.typ | II_enum of int64 diff --git a/cparser/Makefile b/cparser/Makefile index f4c1274..9767b48 100644 --- a/cparser/Makefile +++ b/cparser/Makefile @@ -16,7 +16,7 @@ SRCS=Errors.ml Cabs.ml Cabshelper.ml Parse_aux.ml Parser.ml Lexer.ml \ Cleanup.ml Elab.ml Rename.ml \ Transform.ml \ Unblock.ml SimplExpr.ml AddCasts.ml StructByValue.ml StructAssign.ml \ - Bitfields.ml \ + Bitfields.ml PackedStructs.ml \ Parse.ml COBJS=uint64.o diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml new file mode 100644 index 0000000..edd45ff --- /dev/null +++ b/cparser/PackedStructs.ml @@ -0,0 +1,434 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Emulation of #pragma pack (experimental) *) + +open Printf +open C +open Cutil +open Env +open Errors + +type field_info = { + fi_offset: int; (* byte offset within struct *) + fi_swap: ikind option (* Some ik if byte-swapped *) +} + +(* 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)) + +(* 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 swap = + if swapped then begin + match unroll env f.fld_typ with + | TInt(ik, _) -> + if sizeof_ikind ik = 1 then None else Some ik + | _ -> + error "%a: Error: byte-swapped fields must have integer type" + formatloc loc; + None + end else + None in + let (sz, al) = + match sizeof env f.fld_typ, alignof env f.fld_typ with + | Some s, Some a -> (s, a) + | _, _ -> error "%a: struct field has incomplete type" formatloc loc; + (0, 1) 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) + else + (msa, align sz msa) + +(* Rewriting of struct declarations *) + +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 + let attrs = + if al = 0 then attrs else + add_attributes [Attr("__aligned__", [AInt(Int64.of_int al)])] attrs + and field = + {fld_name = "__payload"; + fld_typ = TArray(TInt(IChar, []), Some(Int64.of_int sz), []); + fld_bitfield = None} + in (attrs, [field]) + end + +(* Accessor functions *) + +let lookup_function loc env name = + try + match Env.lookup_ident env name with + | (id, II_ident(sto, ty)) -> (id, ty) + | (id, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name)) + with Env.Error msg -> + fatal_error "%a: Error: %s" formatloc loc (Env.error_message msg) + +(* (ty) e *) +let ecast ty e = {edesc = ECast(ty, e); etyp = ty} + +(* *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_read_intNN_reversed(&lval) *) +let bswap_read loc env lval ik = + let uik = unsigned_ikind_of ik in + let bsize = sizeof_ikind ik * 8 in + let (id, fty) = + lookup_function loc env (sprintf "__builtin_read_int%d_reversed" bsize) in + let fn = {edesc = EVar id; etyp = fty} in + let args = + if uik = ik + then [eaddrof lval] + else [ecast (TPtr(TInt(uik,[]),[])) (eaddrof lval)] in + let call = {edesc = ECall(fn, args); etyp = TInt(uik, [])} in + if ik = uik then call else ecast (TInt(ik,[])) call + +(* __builtin_write_intNN_reversed(&lhs,rhs) *) +let bswap_write loc env lhs rhs ik = + let uik = unsigned_ikind_of ik in + let bsize = sizeof_ikind ik * 8 in + let (id, fty) = + lookup_function loc env (sprintf "__builtin_write_int%d_reversed" bsize) in + let fn = {edesc = EVar id; etyp = fty} in + let args = + if uik = ik + then [eaddrof lhs; rhs] + else [ecast (TPtr(TInt(uik,[]),[])) (eaddrof lhs); + ecast (TInt(uik,[])) rhs] in + {edesc = ECall(fn, args); etyp = TVoid[]} + +(* Expressions *) + +type context = Val | Effects + +let transf_expr loc env ctx e = + + let is_packed_access ty fieldname = + match unroll env ty with + | TStruct(id, _) -> + (try Some(Hashtbl.find packed_fields (id, fieldname)) + with Not_found -> None) + | _ -> None in + + let is_packed_access_ptr ty fieldname = + match unroll env ty with + | TPtr(ty', _) -> is_packed_access ty' fieldname + | _ -> None in + + (* Transformation of l-values. Return transformed expr plus + [Some ik] if l-value is a byte-swapped field of kind [ik] + or [None] 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}, None) + | Some pf -> + (dot_packed_field e1' pf e.etyp, pf.fi_swap) + end + | 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}, None) + | Some pf -> + (arrow_packed_field e1' pf e.etyp, pf.fi_swap) + end + | _ -> + (texp Val e, None) + + and texp ctx e = + match e.edesc with + | EConst _ -> e + | ESizeof _ -> e + | EVar _ -> e + + | EUnop(Odot _, _) | EUnop(Oarrow _, _) -> + let (e', swap) = lvalue e in + begin match swap with + | None -> e' + | Some ik -> bswap_read loc env e' ik + end + + | EUnop((Oaddrof|Opreincr|Opredecr|Opostincr|Opostdecr as op), e1) -> + let (e1', swap) = lvalue e1 in + if swap <> None then + error "%a: Error: &, ++ and -- over byte-swap field are not supported" + formatloc loc; + {edesc = EUnop(op, e1'); etyp = e.etyp} + + | EUnop(op, e1) -> + {edesc = EUnop(op, texp Val e1); etyp = e.etyp} + + | EBinop(Oassign, e1, e2, ty) -> + let (e1', swap) = lvalue e1 in + let e2' = texp Val e2 in + begin match swap with + | None -> + {edesc = EBinop(Oassign, e1', e2', ty); etyp = e.etyp} + | Some ik -> + if ctx <> Effects then + error "%a: Error: assignment over byte-swapped field in value context is not supported" + formatloc loc; + bswap_write loc env e1' e2' ik + end + + | EBinop((Oadd_assign|Osub_assign|Omul_assign|Odiv_assign|Omod_assign| + Oand_assign|Oor_assign|Oxor_assign|Oshl_assign|Oshr_assign as op), + e1, e2, ty) -> + let (e1', swap) = lvalue e1 in + let e2' = texp Val e2 in + if swap <> None then + error "%a: Error: op-assignment over byte-swapped field in value context is not supported" + formatloc loc; + {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp} + + | EBinop(Ocomma, e1, e2, ty) -> + {edesc = EBinop(Ocomma, texp Effects e1, texp Val e2, ty); + etyp = e.etyp} + + | EBinop(op, e1, e2, ty) -> + {edesc = EBinop(op, texp Val e1, texp Val e2, ty); etyp = e.etyp} + + | EConditional(e1, e2, e3) -> + {edesc = EConditional(texp Val e1, texp ctx e2, texp ctx e3); + etyp = e.etyp} + + | ECast(ty, e1) -> + {edesc = ECast(ty, texp Val e1); etyp = e.etyp} + + | ECall(e1, el) -> + {edesc = ECall(texp Val e1, List.map (texp Val) el); etyp = e.etyp} + + in texp ctx e + +(* Statements *) + +let rec transf_stmt env s = + match s.sdesc with + | Sskip -> s + | Sdo e -> + {sdesc = Sdo(transf_expr s.sloc env Effects e); sloc = s.sloc} + | Sseq(s1, s2) -> + {sdesc = Sseq(transf_stmt env s1, transf_stmt env s2); sloc = s.sloc } + | Sif(e, s1, s2) -> + {sdesc = Sif(transf_expr s.sloc env Val e, + transf_stmt env s1, transf_stmt env s2); + sloc = s.sloc} + | Swhile(e, s1) -> + {sdesc = Swhile(transf_expr s.sloc env Val e, transf_stmt env s1); + sloc = s.sloc} + | Sdowhile(s1, e) -> + {sdesc = Sdowhile(transf_stmt env s1, transf_expr s.sloc env Val e); + sloc = s.sloc} + | Sfor(s1, e, s2, s3) -> + {sdesc = Sfor(transf_stmt env s1, transf_expr s.sloc env Val e, + transf_stmt env s2, transf_stmt env s3); + sloc = s.sloc} + | Sbreak -> s + | Scontinue -> s + | Sswitch(e, s1) -> + {sdesc = Sswitch(transf_expr s.sloc env Val e, + transf_stmt env s1); sloc = s.sloc} + | Slabeled(lbl, s) -> + {sdesc = Slabeled(lbl, transf_stmt env s); sloc = s.sloc} + | Sgoto lbl -> s + | Sreturn None -> s + | Sreturn (Some e) -> + {sdesc = Sreturn(Some(transf_expr s.sloc env Val e)); sloc = s.sloc} + | Sblock _ | Sdecl _ -> + assert false (* should not occur in unblocked code *) + +(* Functions *) + +let transf_fundef env f = + { f with fd_body = transf_stmt env f.fd_body } + +(* Initializers *) + +let rec check_init i = + match i with + | Init_single e -> true + | Init_array il -> List.for_all check_init il + | Init_struct(id, fld_init_list) -> + List.for_all + (fun (f, i) -> + not (Hashtbl.mem packed_fields (id, f.fld_name))) + fld_init_list + | Init_union(id, fld, i) -> + check_init i + +(* Declarations *) + +let transf_decl loc env (sto, id, ty, init_opt as decl) = + begin match init_opt with + | None -> () + | Some i -> + if not (check_init i) then + error "%a: Error: Initialization of packed structs is not supported" + formatloc loc + end; + decl + +(* 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 + | [] -> List.rev accu + | g :: gl -> + match g.gdesc with + | Gdecl((sto, id, ty, init) as d) -> + transf_globdecls + (Env.add_ident env id sto ty) + ({g with gdesc = Gdecl(transf_decl g.gloc env d)} :: accu) + gl + | Gfundef f -> + transf_globdecls + (Env.add_ident env f.fd_name f.fd_storage (fundef_typ f)) + ({g with gdesc = Gfundef(transf_fundef env f)} :: accu) + gl + | Gcompositedecl(su, id, attr) -> + transf_globdecls + (Env.add_composite env id (composite_info_decl env su attr)) + (g :: accu) + gl + | Gcompositedef(su, id, attr, fl) -> + let (attr', fl') = transf_composite g.gloc env su id attr fl in + transf_globdecls + (Env.add_composite env id (composite_info_def env su attr' fl')) + ({g with gdesc = Gcompositedef(su, id, attr', fl')} :: accu) + gl + | Gtypedef(id, ty) -> + transf_globdecls + (Env.add_typedef env id ty) + (g :: accu) + gl + | Genumdef _ -> + transf_globdecls + env + (g :: accu) + gl + | Gpragma p -> + if process_pragma g.gloc p + then transf_globdecls env accu gl + else transf_globdecls env (g :: accu) gl + +(* Program *) + +let program p = + min_struct_align := 0; + max_field_align := 0; + byte_swap_fields := false; + transf_globdecls (Builtins.environment()) [] p diff --git a/cparser/Parse.ml b/cparser/Parse.ml index ed988f9..abef83c 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -24,9 +24,10 @@ let transform_program t p = (run_pass (SimplExpr.program ~volatile:(CharSet.mem 'v' t)) 'e' (run_pass StructAssign.program 'S' (run_pass StructByValue.program 's' + (run_pass PackedStructs.program 'p' (run_pass Bitfields.program 'f' (run_pass Unblock.program 'b' - p)))))) + p))))))) let parse_transformations s = let t = ref CharSet.empty in @@ -40,6 +41,7 @@ let parse_transformations s = | 'S' -> set "bsS" | 'v' -> set "ev" | 'f' -> set "bf" + | 'p' -> set "bp" | _ -> ()) s; !t diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 4b2f350..d58c8ad 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -197,11 +197,12 @@ and globdecl_desc env = function | Gfundef fd -> let (fd', env') = fundef env fd in (Gfundef fd', env') - | Gcompositedecl(kind, id) -> + | Gcompositedecl(kind, id, attr) -> let (id', env') = rename env id in - (Gcompositedecl(kind, id'), env') - | Gcompositedef(kind, id, members) -> - (Gcompositedef(kind, ident env id, List.map (field env) members), env) + (Gcompositedecl(kind, id', attr), env') + | Gcompositedef(kind, id, attr, members) -> + (Gcompositedef(kind, ident env id, attr, List.map (field env) members), + env) | Gtypedef(id, ty) -> let (id', env') = rename env id in (Gtypedef(id', typ env' ty), env') diff --git a/cparser/StructByValue.ml b/cparser/StructByValue.ml index c66af32..60c1154 100644 --- a/cparser/StructByValue.ml +++ b/cparser/StructByValue.ml @@ -22,7 +22,7 @@ open C open Cutil open Transform -(* In function argument types, struct s -> struct s * +(* In function argument types, struct s -> const struct s * In function result types, struct s -> void + add 1st parameter struct s * Try to preserve original typedef names when no change. *) @@ -286,8 +286,8 @@ let transf_fundef env f = (* Composites *) -let transf_composite env su id fl = - List.map (fun f -> {f with fld_typ = transf_type env f.fld_typ}) fl +let transf_composite env su id attr fl = + (attr, List.map (fun f -> {f with fld_typ = transf_type env f.fld_typ}) fl) (* Entry point *) diff --git a/cparser/Transform.ml b/cparser/Transform.ml index 911d613..4fd83ae 100644 --- a/cparser/Transform.ml +++ b/cparser/Transform.ml @@ -45,8 +45,10 @@ let get_temps () = let program ?(decl = fun env d -> d) ?(fundef = fun env fd -> fd) - ?(composite = fun env su id fl -> fl) + ?(composite = fun env su id attr fl -> (attr, fl)) ?(typedef = fun env id ty -> ty) + ?(enum = fun env id members -> members) + ?(pragma = fun env s -> s) p = let rec transf_globdecls env accu = function @@ -59,16 +61,19 @@ let program | Gfundef f -> (Gfundef(fundef env f), Env.add_ident env f.fd_name f.fd_storage (fundef_typ f)) - | Gcompositedecl(su, id) -> - (Gcompositedecl(su, id), - Env.add_composite env id (composite_info_decl env su)) - | Gcompositedef(su, id, fl) -> - (Gcompositedef(su, id, composite env su id fl), - Env.add_composite env id (composite_info_def env su fl)) + | Gcompositedecl(su, id, attr) -> + (Gcompositedecl(su, id, attr), + Env.add_composite env id (composite_info_decl env su attr)) + | Gcompositedef(su, id, attr, fl) -> + let (attr', fl') = composite env su id attr fl in + (Gcompositedef(su, id, attr', fl'), + Env.add_composite env id (composite_info_def env su attr fl)) | Gtypedef(id, ty) -> (Gtypedef(id, typedef env id ty), Env.add_typedef env id ty) - | Genumdef _ as gd -> (gd, env) - | Gpragma _ as gd -> (gd, env) + | Genumdef(id, members) -> + (Genumdef(id, enum env id members), env) + | Gpragma s -> + (Gpragma(pragma env s), env) in transf_globdecls env' ({g with gdesc = desc'} :: accu) gl diff --git a/cparser/Transform.mli b/cparser/Transform.mli index 960d890..8f2c5f8 100644 --- a/cparser/Transform.mli +++ b/cparser/Transform.mli @@ -23,8 +23,12 @@ val get_temps : unit -> C.decl list val program : ?decl:(Env.t -> C.decl -> C.decl) -> ?fundef:(Env.t -> C.fundef -> C.fundef) -> - ?composite:(Env.t -> - C.struct_or_union -> C.ident -> C.field list -> C.field list) -> + ?composite:(Env.t -> C.struct_or_union -> + C.ident -> C.attributes -> C.field list -> + C.attributes * C.field list) -> ?typedef:(Env.t -> C.ident -> Env.typedef_info -> Env.typedef_info) -> + ?enum:(Env.t -> C.ident -> (C.ident * C.exp option) list -> + (C.ident * C.exp option) list) -> + ?pragma:(Env.t -> string -> string) -> C.program -> C.program -- cgit v1.2.3