From d97caa16d15b0faca8386a060ec2bfaedad3cdab Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 11 Jun 2021 16:00:04 +0200 Subject: Revise the declaration of __compcert_* helper functions Don't put them in the C environment used for elaboration. Instead, add them directly to the generated CompCert C at the end of the C2C translation. --- cfrontend/C2C.ml | 161 +++++++++++++++++++++++++++---------------------------- 1 file changed, 79 insertions(+), 82 deletions(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 6fce9764..25d3654f 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -253,88 +253,11 @@ let builtins_generic = { (TVoid [], [TPtr(TVoid [], [])], false); - "__compcert_va_int32", - (TInt(IUInt, []), - [TPtr(TVoid [], [])], - false); - "__compcert_va_int64", - (TInt(IULongLong, []), - [TPtr(TVoid [], [])], - false); - "__compcert_va_float64", - (TFloat(FDouble, []), - [TPtr(TVoid [], [])], - false); - "__compcert_va_composite", - (TPtr(TVoid [], []), - [TPtr(TVoid [], []); TInt(IULong, [])], - false); (* Optimization hints *) "__builtin_unreachable", (TVoid [], [], false); "__builtin_expect", - (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false); - (* Helper functions for int64 arithmetic *) - "__compcert_i64_dtos", - (TInt(ILongLong, []), - [TFloat(FDouble, [])], - false); - "__compcert_i64_dtou", - (TInt(IULongLong, []), - [TFloat(FDouble, [])], - false); - "__compcert_i64_stod", - (TFloat(FDouble, []), - [TInt(ILongLong, [])], - false); - "__compcert_i64_utod", - (TFloat(FDouble, []), - [TInt(IULongLong, [])], - false); - "__compcert_i64_stof", - (TFloat(FFloat, []), - [TInt(ILongLong, [])], - false); - "__compcert_i64_utof", - (TFloat(FFloat, []), - [TInt(IULongLong, [])], - false); - "__compcert_i64_sdiv", - (TInt(ILongLong, []), - [TInt(ILongLong, []); TInt(ILongLong, [])], - false); - "__compcert_i64_udiv", - (TInt(IULongLong, []), - [TInt(IULongLong, []); TInt(IULongLong, [])], - false); - "__compcert_i64_smod", - (TInt(ILongLong, []), - [TInt(ILongLong, []); TInt(ILongLong, [])], - false); - "__compcert_i64_umod", - (TInt(IULongLong, []), - [TInt(IULongLong, []); TInt(IULongLong, [])], - false); - "__compcert_i64_shl", - (TInt(ILongLong, []), - [TInt(ILongLong, []); TInt(IInt, [])], - false); - "__compcert_i64_shr", - (TInt(IULongLong, []), - [TInt(IULongLong, []); TInt(IInt, [])], - false); - "__compcert_i64_sar", - (TInt(ILongLong, []), - [TInt(ILongLong, []); TInt(IInt, [])], - false); - "__compcert_i64_smulh", - (TInt(ILongLong, []), - [TInt(ILongLong, []); TInt(ILongLong, [])], - false); - "__compcert_i64_umulh", - (TInt(IULongLong, []), - [TInt(IULongLong, []); TInt(IULongLong, [])], - false) + (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false) ] } @@ -1280,7 +1203,6 @@ let convertFundef loc env fd = (** External function declaration *) let re_builtin = Str.regexp "__builtin_" -let re_runtime = Str.regexp "__compcert_i64_" let convertFundecl env (sto, id, ty, optinit) = let (args, res, cconv) = @@ -1293,7 +1215,6 @@ let convertFundecl env (sto, id, ty, optinit) = let ef = if id.name = "malloc" then AST.EF_malloc else if id.name = "free" then AST.EF_free else - if Str.string_match re_runtime id.name 0 then AST.EF_runtime(id'', sg) else if Str.string_match re_builtin id.name 0 && List.mem_assoc id.name builtins.builtin_functions then AST.EF_builtin(id'', sg) @@ -1415,6 +1336,81 @@ let rec convertCompositedefs env res gl = | _ -> convertCompositedefs env res gl' +(** Add declarations for the helper functions + (for varargs and for int64 arithmetic) *) + +let helper_functions () = [ + "__compcert_va_int32", + Tint(I32, Unsigned, noattr), + [Tpointer(Tvoid, noattr)]; + "__compcert_va_int64", + Tlong(Unsigned, noattr), + [Tpointer(Tvoid, noattr)]; + "__compcert_va_float64", + Tfloat(F64, noattr), + [Tpointer(Tvoid, noattr)]; + "__compcert_va_composite", + Tpointer(Tvoid, noattr), + [Tpointer(Tvoid, noattr); convertIkind (Cutil.size_t_ikind()) noattr]; + "__compcert_i64_dtos", + Tlong(Signed, noattr), + [Tfloat(F64, noattr)]; + "__compcert_i64_dtou", + Tlong(Unsigned, noattr), + [Tfloat(F64, noattr)]; + "__compcert_i64_stod", + Tfloat(F64, noattr), + [Tlong(Signed, noattr)]; + "__compcert_i64_utod", + Tfloat(F64, noattr), + [Tlong(Unsigned, noattr)]; + "__compcert_i64_stof", + Tfloat(F32, noattr), + [Tlong(Signed, noattr)]; + "__compcert_i64_utof", + Tfloat(F32, noattr), + [Tlong(Unsigned, noattr)]; + "__compcert_i64_sdiv", + Tlong(Signed, noattr), + [Tlong(Signed, noattr); Tlong(Signed, noattr)]; + "__compcert_i64_udiv", + Tlong(Unsigned, noattr), + [Tlong(Unsigned, noattr); Tlong(Unsigned, noattr)]; + "__compcert_i64_smod", + Tlong(Signed, noattr), + [Tlong(Signed, noattr); Tlong(Signed, noattr)]; + "__compcert_i64_umod", + Tlong(Unsigned, noattr), + [Tlong(Unsigned, noattr); Tlong(Unsigned, noattr)]; + "__compcert_i64_shl", + Tlong(Signed, noattr), + [Tlong(Signed, noattr); Tint(I32, Signed, noattr)]; + "__compcert_i64_shr", + Tlong(Unsigned, noattr), + [Tlong(Unsigned, noattr); Tint(I32, Signed, noattr)]; + "__compcert_i64_sar", + Tlong(Signed, noattr), + [Tlong(Signed, noattr); Tint(I32, Signed, noattr)]; + "__compcert_i64_smulh", + Tlong(Signed, noattr), + [Tlong(Signed, noattr); Tlong(Signed, noattr)]; + "__compcert_i64_umulh", + Tlong(Unsigned, noattr), + [Tlong(Unsigned, noattr); Tlong(Unsigned, noattr)] +] + +let helper_function_declaration (name, tyres, tyargs) = + let tyargs = + List.fold_right (fun t tl -> Tcons(t, tl)) tyargs Tnil in + let ef = + AST.EF_runtime(coqstring_of_camlstring name, + signature_of_type tyargs tyres AST.cc_default) in + (intern_string name, + AST.Gfun (Ctypes.External(ef, tyargs, tyres, AST.cc_default))) + +let add_helper_functions globs = + List.map helper_function_declaration (helper_functions()) @ globs + (** Build environment of typedefs, structs, unions and enums *) let rec translEnv env = function @@ -1512,10 +1508,11 @@ let convertProgram p = comp_env := ce; let gl1 = convertGlobdecls env [] p in let gl2 = globals_for_strings gl1 in + let gl3 = add_helper_functions gl2 in comp_env := Maps.PTree.empty; let p' = - { prog_defs = gl2; - prog_public = public_globals gl2; + { prog_defs = gl3; + prog_public = public_globals gl3; prog_main = intern_string !Clflags.main_function_name; prog_types = typs; prog_comp_env = ce } in -- cgit From 47fae389c800034e002c9f8a398e9adc79a14b81 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 17 May 2021 18:07:02 +0200 Subject: Native support for bit fields (#400) This big PR adds support for bit fields in structs and unions to the verified part of CompCert, namely the CompCert C and Clight languages. The compilation of bit field accesses to normal integer accesses + shifts and masks is done and proved correct as part of the Cshmgen pass. The layout of bit fields in memory is done by the functions in module Ctypes. It follows the ELF ABI layout algorithm. As a bonus, basic soundness properties of the layout are shown, such as "two different bit fields do not overlap" or "a bit field and a regular field do not overlap". All this replaces the previous emulation of bit fields by source-to-source rewriting in the unverified front-end of CompCert (module cparse/Bitfield.ml). This emulation was prone to errors (see nonstandard layout instead. The core idea for the PR is that expressions in l-value position denote not just a block, a byte offset and a type, but also a bitfield designator saying whether all the bits of the type are accessed (designator Full) or only some of its bits (designator Bits). Designators of the Bits kind appear when the l-value is a bit field access; the bit width and bit offset in Bits are computed by the functions in Ctypes that implement the layout algorithm. Consequently, both in the semantics of CompCert C and Clight and in the SimplExpr, SimplLocals and Cshmgen compilation passes, pairs of a type and a bitfield designator are used in a number of places where a single type was used before. The introduction of bit fields has a big impact on static initialization (module cfrontend/Initializers.v), which had to be rewritten in large part, along with its soundness proof (cfrontend/Initializersproof.v). Both static initialization and run-time manipulation of bit fields are tested in test/abi using differential testing against GCC and randomly-generated structs. This work exposed subtle interactions between bit fields and the volatile modifier. Currently, the volatile modifier is ignored when accessing a bit field (and a warning is printed at compile-time), just like it is ignored when accessing a struct or union as a r-value. Currently, the natural alignment of bit fields and their storage units cannot be modified with the aligned attribute. _Alignas on bit fields is rejected as per C11, and the packed modifier cannot be applied to a struct containing bit fields. --- cfrontend/C2C.ml | 39 ++++++++++++++++++++++++++++++++++----- 1 file changed, 34 insertions(+), 5 deletions(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 6fce9764..efcf8dfc 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -612,7 +612,7 @@ let checkFunctionType env tres targs = end end -let rec convertTyp env t = +let rec convertTyp env ?bitwidth t = match t with | C.TVoid a -> Tvoid | C.TInt(ik, a) -> @@ -643,7 +643,21 @@ let rec convertTyp env t = | C.TUnion(id, a) -> Tunion(intern_string id.name, convertAttr a) | C.TEnum(id, a) -> - convertIkind Cutil.enum_ikind (convertAttr a) + let ik = + match bitwidth with + | None -> Cutil.enum_ikind + | Some w -> + let info = Env.find_enum env id in + let representable sg = + List.for_all (fun (_, v, _) -> Cutil.int_representable v w sg) + info.Env.ei_members in + if representable false then + Cutil.unsigned_ikind_of Cutil.enum_ikind + else if representable true then + Cutil.signed_ikind_of Cutil.enum_ikind + else + Cutil.enum_ikind in + convertIkind ik (convertAttr a) and convertParams env = function | [] -> Tnil @@ -679,9 +693,16 @@ let rec convertTypAnnotArgs env = function convertTypAnnotArgs env el) let convertField env f = - if f.fld_bitfield <> None then - unsupported "bit field in struct or union (consider adding option [-fbitfields])"; - (intern_string f.fld_name, convertTyp env f.fld_typ) + let id = intern_string f.fld_name + and ty = convertTyp env ?bitwidth: f.fld_bitfield f.fld_typ in + match f.fld_bitfield with + | None -> Member_plain(id, ty) + | Some w -> + match ty with + | Tint(sz, sg, attr) -> + Member_bitfield(id, sz, sg, attr, Z.of_uint w, f.fld_name = "") + | _ -> + fatal_error "bitfield must have type int" let convertCompositedef env su id attr members = if Cutil.find_custom_attributes ["packed";"__packed__"] attr <> [] then @@ -784,6 +805,11 @@ let convertFloat f kind = (** Expressions *) +let check_volatile_bitfield env e = + if Cutil.is_bitfield env e + && List.mem AVolatile (Cutil.attributes_of_type env e.etyp) then + warning Diagnostics.Unnamed "access to a volatile bit field, the 'volatile' qualifier is ignored" + let ezero = Eval(Vint(coqint_of_camlint 0l), type_int32s) let ewrap = function @@ -798,6 +824,7 @@ let rec convertExpr env e = | C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _) | C.EBinop(C.Oindex, _, _, _) -> let l = convertLvalue env e in + check_volatile_bitfield env e; ewrap (Ctyping.evalof l) | C.EConst(C.CInt(i, k, _)) -> @@ -867,6 +894,7 @@ let rec convertExpr env e = if Cutil.is_composite_type env e2.etyp && List.mem AVolatile (Cutil.attributes_of_type env e2.etyp) then warning Diagnostics.Unnamed "assignment of a value of volatile composite type, the 'volatile' qualifier is ignored"; + check_volatile_bitfield env e1; ewrap (Ctyping.eassign e1' e2') | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign| C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign| @@ -887,6 +915,7 @@ let rec convertExpr env e = | _ -> assert false in let e1' = convertLvalue env e1 in let e2' = convertExpr env e2 in + check_volatile_bitfield env e1; ewrap (Ctyping.eassignop op' e1' e2') | C.EBinop(C.Ocomma, e1, e2, _) -> ewrap (Ctyping.ecomma (convertExpr env e1) (convertExpr env e2)) -- cgit