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.

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 *)