diff options
| -rw-r--r-- | backend/Inlining.v | 13 | ||||
| -rw-r--r-- | backend/Inliningaux.ml | 80 | ||||
| -rw-r--r-- | backend/Inliningspec.v | 12 | ||||
| -rw-r--r-- | doc/ccomp.1 | 5 | ||||
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Driver.ml | 5 | ||||
| -rw-r--r-- | extraction/extraction.v | 2 |
7 files changed, 105 insertions, 13 deletions
diff --git a/backend/Inlining.v b/backend/Inlining.v index 91cc119d..f7ee4166 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -27,12 +27,16 @@ Definition funenv : Type := PTree.t function. Definition size_fenv (fenv: funenv) := PTree_Properties.cardinal fenv. -Parameter should_inline: ident -> function -> bool. +Parameter inlining_info: Type. (* abstract type, implemented on the Caml side *) -Definition add_globdef (fenv: funenv) (idg: ident * globdef fundef unit) : funenv := +Parameter inlining_analysis: program -> inlining_info. + +Parameter should_inline: inlining_info -> ident -> function -> bool. + +Definition add_globdef (io: inlining_info) (fenv: funenv) (idg: ident * globdef fundef unit) : funenv := match idg with | (id, Gfun (Internal f)) => - if should_inline id f + if should_inline io id f then PTree.set id f fenv else PTree.remove id fenv | (id, _) => @@ -40,7 +44,8 @@ Definition add_globdef (fenv: funenv) (idg: ident * globdef fundef unit) : funen end. Definition funenv_program (p: program) : funenv := - List.fold_left add_globdef p.(prog_defs) (PTree.empty function). + let io := inlining_analysis p in + List.fold_left (add_globdef io) p.(prog_defs) (PTree.empty function). (** State monad *) diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml index df33e1ac..164773ae 100644 --- a/backend/Inliningaux.ml +++ b/backend/Inliningaux.ml @@ -10,7 +10,83 @@ (* *) (* *********************************************************************) +open AST +open Datatypes +open FSetAVL +open Maps +open Op +open Ordered +open !RTL + +module PSet = Make(OrderedPositive) + +type inlining_info = { + call_cnt : int PTree.t; (* Count the number of direct calls to a function *) + addr_taken : PSet.t; (* The set of globals which have their address taken *) +} + +let empty_inlining_info = { + call_cnt = PTree.empty; + addr_taken = PSet.empty; +} + +let call_count id io = + match PTree.get id io.call_cnt with + | Some cnt -> cnt + | None -> 0 + +let called id io = + let call_cnt = PTree.set id (1 + call_count id io) io.call_cnt in + { io with call_cnt = call_cnt } + +let address_taken id io = + PSet.mem id io.addr_taken + +let rec used_id io ids = + match ids with + | [] -> io + | id::ids -> + used_id {io with addr_taken = PSet.add id io.addr_taken} ids + +let used_in_globvar io gv = + let used_in_init_data io = function + | Init_addrof (id,_) -> used_id io [id] + | _ -> io in + List.fold_left used_in_init_data io gv.gvar_init + +let fun_inline_analysis id io fn = + let inst io nid = function + | Iop (op, args, dest, succ) -> used_id io (globals_operation op) + | Iload (chunk, addr, args, dest, succ) + | Istore (chunk, addr, args, dest, succ) -> used_id io (globals_addressing addr) + | Ibuiltin (ef, args, dest, succ) -> used_id io (globals_of_builtin_args args) + | Icall (_, Coq_inr cid, _, _, _) + | Itailcall (_, Coq_inr cid, _) -> called cid io + | _ -> io in + PTree.fold inst fn.fn_code io + +(* Gather information about the program used for inlining heuristic *) +let inlining_analysis (p: program) = + if !Clflags.option_finline && !Clflags.option_finline_functions_called_once then + List.fold_left (fun io idg -> + match idg with + | fid, Gfun (Internal f) -> fun_inline_analysis fid io f + | _, Gvar gv -> used_in_globvar io gv + | _ -> io) empty_inlining_info p.prog_defs + else + empty_inlining_info + +(* Test whether a function is static and called only once *) +let static_called_once id io = + if !Clflags.option_finline_functions_called_once then + C2C.atom_is_static id && call_count id io <= 1 && not (address_taken id io) + else + false + (* To be considered: heuristics based on size of function? *) -let should_inline (id: AST.ident) (f: RTL.coq_function) = - !Clflags.option_finline && C2C.atom_is_inline id +let should_inline (io: inlining_info) (id: ident) (f: coq_function) = + if !Clflags.option_finline then + C2C.atom_is_inline id || static_called_once id io + else + false diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index 6e8a94a6..c345c942 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -39,19 +39,19 @@ Proof. discriminate. rewrite PTree.gso; auto. } - assert (ADD: forall dm fenv idg, + assert (ADD: forall io dm fenv idg, P dm fenv -> - P (PTree.set (fst idg) (snd idg) dm) (add_globdef fenv idg)). - { intros dm fenv [id g]; simpl; intros. + P (PTree.set (fst idg) (snd idg) dm) (add_globdef io fenv idg)). + { intros io dm fenv [id g]; simpl; intros. destruct g as [ [f|ef] | v]; auto. - destruct (should_inline id f); auto. + destruct (should_inline io id f); auto. red; intros. rewrite ! PTree.gsspec in *. destruct (peq id0 id); auto. inv H0; auto. } - assert (REC: forall l dm fenv, + assert (REC: forall p l dm fenv, P dm fenv -> P (fold_left (fun x idg => PTree.set (fst idg) (snd idg) x) l dm) - (fold_left add_globdef l fenv)). + (fold_left (add_globdef p) l fenv)). { induction l; simpl; intros. - auto. - apply IHl. apply ADD; auto. diff --git a/doc/ccomp.1 b/doc/ccomp.1 index 906e0ffc..c476b196 100644 --- a/doc/ccomp.1 +++ b/doc/ccomp.1 @@ -143,6 +143,11 @@ Turn on/off inlining of functions. Enabled by default. . .TP +.BR \-finline\-functions\-called\-once ", " \-fno\-inline\-functions\-called\-once +Turn on/off inlining of functions only required by a single caller. +Enabled by default. +. +.TP .BR \-fredundancy ", " \-fno\-redundancy Turn on/off redundancy elimination. Enabled by default. diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 2d92e09b..a886ee9b 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -34,6 +34,7 @@ let option_finline_asm = ref false let option_mthumb = ref (Configuration.model = "armv7m") let option_Osize = ref false let option_finline = ref true +let option_finline_functions_called_once = ref true let option_dprepro = ref false let option_dparse = ref false let option_dcmedium = ref false diff --git a/driver/Driver.ml b/driver/Driver.ml index 124bc587..0e01dbb5 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -268,6 +268,8 @@ Processing options: -fcse Perform common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] -finline Perform inlining of functions [on] + -finline-functions-called-once Integrate functions only required by their + single caller [on] Code generation options: (use -fno-<opt> to turn off -f<opt>) -ffpu Use FP registers for some integer operations [on] -fsmall-data <n> Set maximal size <n> for allocation in small data area @@ -337,7 +339,7 @@ let language_support_options = [ ] let optimization_options = [ - option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy + option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy; option_finline_functions_called_once; ] let set_all opts () = List.iter (fun r -> r := true) opts @@ -458,6 +460,7 @@ let cmdline_actions = @ f_opt "cse" option_fcse @ f_opt "redundancy" option_fredundancy @ f_opt "inline" option_finline + @ f_opt "inline-functions-called-once" option_finline_functions_called_once (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) diff --git a/extraction/extraction.v b/extraction/extraction.v index 247d6cfb..c5751e2b 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -76,6 +76,8 @@ Extraction Inline RTLgen.ret RTLgen.error RTLgen.bind RTLgen.bind2. (* Inlining *) Extract Inlined Constant Inlining.should_inline => "Inliningaux.should_inline". +Extract Inlined Constant Inlining.inlining_info => "Inliningaux.inlining_info". +Extract Inlined Constant Inlining.inlining_analysis => "Inliningaux.inlining_analysis". Extraction Inline Inlining.ret Inlining.bind. (* Allocation *) |