diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-15 00:00:33 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-15 00:00:33 +0100 |
| commit | 192d5f379b3f1efa6f12b45af36f7cfea21d6d50 (patch) | |
| tree | 1c60908b258159a96ac1c55f5aef4d89f4594cae /backend/Inliningaux.ml | |
| parent | 9e706de1eb25d6d6dbeb1eb2ced71e48523a499f (diff) | |
| download | compcert-kvx-192d5f379b3f1efa6f12b45af36f7cfea21d6d50.tar.gz compcert-kvx-192d5f379b3f1efa6f12b45af36f7cfea21d6d50.zip | |
more inlining
Diffstat (limited to 'backend/Inliningaux.ml')
| -rw-r--r-- | backend/Inliningaux.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml index d58704ca..cf308962 100644 --- a/backend/Inliningaux.ml +++ b/backend/Inliningaux.ml @@ -17,7 +17,8 @@ open Maps open Op open Ordered open! RTL - +open Camlcoq + module PSet = Make(OrderedPositive) type inlining_info = { @@ -83,13 +84,15 @@ let static_called_once id io = else false -(* To be considered: heuristics based on size of function? *) +(* D. Monniaux: attempt at heuristic based on size *) +let small_enough (f : coq_function) = + P.to_int (RTL.max_pc_function f) <= !Clflags.option_inline_auto_threshold let should_inline (io: inlining_info) (id: ident) (f: coq_function) = if !Clflags.option_finline then begin match C2C.atom_inline id with | C2C.Inline -> true | C2C.Noinline -> false - | C2C.No_specifier -> static_called_once id io + | C2C.No_specifier -> static_called_once id io || small_enough f end else false |