diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Inlining.v | 13 | ||||
-rw-r--r-- | backend/Inliningaux.ml | 80 | ||||
-rw-r--r-- | backend/Inliningspec.v | 12 |
3 files changed, 93 insertions, 12 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. |