From 92b2d35f701ae55129fe2c34066d59d045460852 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 17 Jun 2019 19:00:36 +0200 Subject: Change the expected types for arguments to __builtin_annot, and extended asm Currently, the arguments to __builtin_annot, __builtin_ais_annot, __builtin_debug, and extended asm statements are treated like arguments to an unprototyped or vararg function call. In particular, arguments of type "float" are converted to "double", generating useless code. To avoid this extra, useless conversion, this commit changes the types expected for the arguments to these built-ins and to extended asm statements. Now they are the types of the arguments themselves, after performing the usual unary conversions (e.g. char -> int), but without the problematic float -> double conversion. This ensures that no code is generated to change the representation of the arguments. --- cfrontend/C2C.ml | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 5428d0cc..b81bd022 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -596,6 +596,12 @@ and convertParams env = function | [] -> Tnil | (id, ty) :: rem -> Tcons(convertTyp env ty, convertParams env rem) +(* Convert types for the arguments to a function call. The types for + fixed arguments are taken from the function prototype. The types + for other arguments (variable-argument function or unprototyped K&R + functions) are taken from the types of the function arguments, + after default argument conversion. *) + let rec convertTypArgs env tl el = match tl, el with | _, [] -> Tnil @@ -605,6 +611,20 @@ let rec convertTypArgs env tl el = | (id, t1) :: tl, e1 :: el -> Tcons(convertTyp env t1, convertTypArgs env tl el) +(* Convert types for the arguments to inline asm statements and to + the special built-in functions __builtin_annot, __builtin_ais_annot_ + and __builtin_debug. The types are taken from the types of the + arguments, after performing the usual unary conversions. + Hence char becomes int but float remains float and is not promoted + to double. The goal is to preserve the representation of the arguments + and avoid inserting compiled code to convert the arguments. *) + +let rec convertTypAnnotArgs env = function + | [] -> Tnil + | e1 :: el -> + Tcons(convertTyp env (Cutil.unary_conversion env e1.etyp), + convertTypAnnotArgs env el) + let convertField env f = if f.fld_bitfield <> None then unsupported "bit field in struct or union (consider adding option [-fbitfields])"; @@ -845,7 +865,7 @@ let rec convertExpr env e = | {edesc = C.EVar id} :: args2 -> (id.name, args2) | _::args2 -> error "argument 2 of '__builtin_debug' must be either a string literal or a variable"; ("", args2) | [] -> assert false (* catched earlier *) in - let targs2 = convertTypArgs env [] args2 in + let targs2 = convertTypAnnotArgs env args2 in Ebuiltin( AST.EF_debug(P.of_int64 kind, intern_string text, typlist_of_typelist targs2), @@ -854,7 +874,7 @@ let rec convertExpr env e = | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) -> begin match args with | {edesc = C.EConst(CStr txt)} :: args1 -> - let targs1 = convertTypArgs env [] args1 in + let targs1 = convertTypAnnotArgs env args1 in Ebuiltin( AST.EF_annot(P.of_int 1,coqstring_of_camlstring txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) @@ -882,7 +902,7 @@ let rec convertExpr env e = let file,line = !currentLocation in let fun_name = !currentFunction in let loc_string = Printf.sprintf "# file:%s line:%d function:%s\n" file line fun_name in - let targs1 = convertTypArgs env [] args1 in + let targs1 = convertTypAnnotArgs env args1 in AisAnnot.validate_ais_annot env !currentLocation txt args1; Ebuiltin( AST.EF_annot(P.of_int 2,coqstring_of_camlstring (loc_string ^ txt), typlist_of_typelist targs1), @@ -983,14 +1003,14 @@ let convertAsm loc env txt outputs inputs clobber = match output' with None -> TVoid [] | Some e -> e.etyp in (* Build the Ebuiltin expression *) let e = - let tinputs = convertTypArgs env [] inputs' in + let tinputs = convertTypAnnotArgs env inputs' in let toutput = convertTyp env ty_res in Ebuiltin( AST.EF_inline_asm(coqstring_of_camlstring txt', signature_of_type tinputs toutput AST.cc_default, clobber'), tinputs, convertExprList env inputs', - convertTyp env ty_res) in + toutput) in (* Add an assignment to the output, if any *) match output' with | None -> e -- cgit From fb20aab431a768299118ed30822af59cab13325e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 2 Jul 2019 14:55:31 +0200 Subject: Remove the cparser/Builtins module Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`. --- cfrontend/C2C.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index b81bd022..4d0e52e1 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -155,8 +155,8 @@ let ais_annot_functions = [] let builtins_generic = { - Builtins.typedefs = []; - Builtins.functions = + builtin_typedefs = []; + builtin_functions = ais_annot_functions @ [ @@ -300,9 +300,12 @@ let builtins_generic = { (* Add processor-dependent builtins *) -let builtins = - Builtins.({ typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; - functions = builtins_generic.Builtins.functions @ CBuiltins.builtins.functions }) +let builtins = { + builtin_typedefs = + builtins_generic.builtin_typedefs @ CBuiltins.builtins.builtin_typedefs; + builtin_functions = + builtins_generic.builtin_functions @ CBuiltins.builtins.builtin_functions +} (** ** The known attributes *) @@ -1233,7 +1236,7 @@ let convertFundecl env (sto, id, ty, optinit) = 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.Builtins.functions + && List.mem_assoc id.name builtins.builtin_functions then AST.EF_builtin(id'', sg) else AST.EF_external(id'', sg) in (id', AST.Gfun(Ctypes.External(ef, args, res, cconv))) @@ -1432,7 +1435,7 @@ let convertProgram p = Hashtbl.clear decl_atom; Hashtbl.clear stringTable; Hashtbl.clear wstringTable; - let p = cleanupGlobals (Builtins.declarations() @ p) in + let p = cleanupGlobals (Env.initial_declarations() @ p) in try let env = translEnv Env.empty p in let typs = convertCompositedefs env [] p in -- cgit From 633e60ed36c07c4b6cb4b1dc93b9eea312882ceb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 4 Jul 2019 17:49:11 +0200 Subject: Make __builtin_sel available from C source code It is type-checked like a conditional expression then translated to a call to the known builtin function. --- cfrontend/C2C.ml | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 4d0e52e1..2e6bbe67 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -181,6 +181,11 @@ let builtins_generic = { TInt(IULong, []); TInt(IULong, [])], false); + (* Selection *) + "__builtin_sel", + (TVoid [], + [TInt(C.IBool, [])], + true); (* Annotations *) "__builtin_annot", (TVoid [], @@ -941,6 +946,10 @@ let rec convertExpr env e = Econs(va_list_ptr dst, Econs(va_list_ptr src, Enil)), Tvoid) + | C.ECall({edesc = C.EVar {name = "__builtin_sel"}}, [arg1; arg2; arg3]) -> + ewrap (Ctyping.eselection (convertExpr env arg1) + (convertExpr env arg2) (convertExpr env arg3)) + | C.ECall({edesc = C.EVar {name = "printf"}}, args) when !Clflags.option_interp -> let targs = convertTypArgs env [] args -- cgit