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