From 239cbd2ebab8814b11d7ef43c35a17ce56a7ba0b Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 11 May 2011 11:47:38 +0000 Subject: cparser/StructAssign: always use __builtin_memcpy + alignment indication (simpler and globally more efficient) cfrontend/C2C.ml: specialization of __builtin_memcpy over size */PrintAsm.ml: revised expansion of __builtin_memcpy_* ia32/Asm.ml: typo in comment git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1649 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/C2C.ml | 140 ++++++++++++++++++++++++++++++++++++------------------- 1 file changed, 91 insertions(+), 49 deletions(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 1a6539a..1ee63b8 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -111,7 +111,19 @@ let builtins_generic = { TPtr(TVoid [AConst], []); TInt(Cutil.size_t_ikind, [])], false); - "__builtin_memcpy_words", + "__builtin_memcpy_al2", + (TVoid [], + [TPtr(TVoid [], []); + TPtr(TVoid [AConst], []); + TInt(Cutil.size_t_ikind, [])], + false); + "__builtin_memcpy_al4", + (TVoid [], + [TPtr(TVoid [], []); + TPtr(TVoid [AConst], []); + TInt(Cutil.size_t_ikind, [])], + false); + "__builtin_memcpy_al8", (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [AConst], []); @@ -172,65 +184,89 @@ let globals_for_strings globs = (fun s id l -> global_for_string s id :: l) stringTable globs -(** ** Handling of stubs for variadic functions *) +(** ** Declaration of special external functions *) + +let special_externals_table : (string, fundef) Hashtbl.t = Hashtbl.create 47 -let stub_function_table = Hashtbl.create 47 +let register_special_external c_name int_name targs tres inline = + if not (Hashtbl.mem special_externals_table c_name) then begin + Hashtbl.add special_externals_table c_name + (External({ef_id = intern_string int_name; + ef_sig = signature_of_type targs tres; + ef_inline = inline}, + targs, tres)) + end + +let declare_special_externals k = + Hashtbl.fold + (fun c_name fd k -> + Datatypes.Coq_pair(intern_string c_name, fd) :: k) + special_externals_table k + +(** ** Handling of stubs for variadic functions *) let register_stub_function name tres targs = let rec letters_of_type = function | Tnil -> [] | Tcons(Tfloat _, tl) -> "f" :: letters_of_type tl | Tcons(_, tl) -> "i" :: letters_of_type tl in + let rec types_of_types = function + | Tnil -> Tnil + | Tcons(Tfloat _, tl) -> Tcons(Tfloat F64, types_of_types tl) + | Tcons(_, tl) -> Tcons(Tpointer Tvoid, types_of_types tl) in let stub_name = name ^ "$" ^ String.concat "" (letters_of_type targs) in - try - (stub_name, Hashtbl.find stub_function_table stub_name) - with Not_found -> - let rec types_of_types = function - | Tnil -> Tnil - | Tcons(Tfloat _, tl) -> Tcons(Tfloat F64, types_of_types tl) - | Tcons(_, tl) -> Tcons(Tpointer Tvoid, types_of_types tl) in - let stub_type = Tfunction (types_of_types targs, tres) in - Hashtbl.add stub_function_table stub_name stub_type; - (stub_name, stub_type) - -let declare_stub_function stub_name stub_type = - match stub_type with - | Tfunction(targs, tres) -> - Datatypes.Coq_pair(intern_string stub_name, - External({ ef_id = intern_string stub_name; - ef_sig = signature_of_type targs tres; - ef_inline = false }, - targs, tres)) - | _ -> assert false - -let declare_stub_functions k = - Hashtbl.fold (fun n i k -> declare_stub_function n i :: k) - stub_function_table k + let targs = types_of_types targs in + register_special_external stub_name stub_name targs tres false; + (stub_name, Tfunction (targs, tres)) (** ** Handling of annotations *) -let annot_function_list = ref [] let annot_function_next = ref 0 let register_annotation_function txt targs tres = incr annot_function_next; let fun_name = - intern_string - (Printf.sprintf "__builtin_annotation_%d" !annot_function_next) - and ext_ident = - intern_string - (Printf.sprintf "__builtin_annotation_\"%s\"" txt) in - annot_function_list := - Datatypes.Coq_pair(fun_name, - External({ ef_id = ext_ident; - ef_sig = signature_of_type targs tres; - ef_inline = true }, - targs, tres)) :: !annot_function_list; - Evalof(Evar(fun_name, Tfunction(targs, tres)), Tfunction(targs, tres)) - -let declare_annotation_functions k = - List.rev_append !annot_function_list k + Printf.sprintf "__builtin_annotation_%d" !annot_function_next + and int_name = + Printf.sprintf "__builtin_annotation_\"%s\"" txt in + register_special_external fun_name int_name targs tres true; + Evalof(Evar(intern_string fun_name, Tfunction(targs, tres)), + Tfunction(targs, tres)) + +(** ** Handling of inlined memcpy functions *) + +let alignof_pointed ty = + match ty with + | Tpointer ty' -> camlint_of_z (alignof ty') + | _ -> 1l (* safe default *) + +let register_inlined_memcpy basename sz = + let name = Printf.sprintf "%s_sz%ld" basename sz in + let targs = Tcons(Tpointer Tvoid, Tcons(Tpointer Tvoid, Tnil)) in + let tres = Tvoid in + register_special_external name name targs tres true; + Evalof(Evar(intern_string name, Tfunction(targs, tres)), + Tfunction(targs, tres)) + +let memcpy_inline_threshold = ref 64l + +let make_builtin_memcpy name fn args = + match args with + | Econs(dst, Econs(src, Econs(sz, Enil))) -> + let sz1 = + match Initializers.constval sz with + | CompcertErrors.OK(Vint n) -> Some (camlint_of_coqint n) + | _ -> None in + begin match sz1 with + | Some sz2 when sz2 <= !memcpy_inline_threshold -> + let fn = register_inlined_memcpy name sz2 in + Ecall(fn, Econs(dst, Econs(src, Enil)), Tvoid) + | _ -> + Ecall(fn, args, Tvoid) + end + | _ -> + Ecall(fn, args, Tvoid) (** ** Translation functions *) @@ -539,6 +575,13 @@ let rec convertExpr env e = ezero end + | C.ECall({edesc = C.EVar {name = ("__builtin_memcpy" + |"__builtin_memcpy_al2" + |"__builtin_memcpy_al4" + |"__builtin_memcpy_al8" as name)}} as fn, + args) -> + make_builtin_memcpy name (convertExpr env fn) (convertExprList env args) + | C.ECall(fn, args) -> match projFunType env fn.etyp with | None -> @@ -727,8 +770,8 @@ let convertFundef env fd = (** External function declaration *) let noninlined_builtin_functions = [ - "__builtin_memcpy"; - "__builtin_memcpy_words" + "__builtin_memcpy"; "__builtin_memcpy_al2"; + "__builtin_memcpy_al4"; "__builtin_memcpy_al8" ] let convertFundecl env (sto, id, ty, optinit) = @@ -889,17 +932,16 @@ let convertProgram p = stringNum := 0; Hashtbl.clear decl_atom; Hashtbl.clear stringTable; - Hashtbl.clear stub_function_table; + Hashtbl.clear special_externals_table; let p = Builtins.declarations() @ p in try let (funs1, vars1) = convertGlobdecls (translEnv Env.empty p) [] [] (cleanupGlobals p) in - let funs2 = declare_stub_functions funs1 in - let funs3 = declare_annotation_functions funs2 in + let funs2 = declare_special_externals funs1 in let vars2 = globals_for_strings vars1 in if !numErrors > 0 then None - else Some { AST.prog_funct = funs3; + else Some { AST.prog_funct = funs2; AST.prog_vars = vars2; AST.prog_main = intern_string "main" } with Env.Error msg -> -- cgit v1.2.3