Inlining of static functions which are only called once. (#37)

New inlining heuristic for static functions.

Static functions that are only called once can always be inlined,
since they can be removed safely after inlining and no call
prologue, epilogue, as well as register saving and needs to be
generated.

1 files changed, 78 insertions, 2 deletions

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