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.

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.