diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-12-07 12:14:08 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-07 12:14:08 +0100 |
| commit | 3bb0c75456a0dcab079e7614c3bbd3ba971e4519 (patch) | |
| tree | 1dac031c6b94aafb7e28f63857dbdbe2f4870066 /backend/Inlining.v | |
| parent | 90b76a0842b7f080893dd70a7c0c6bc878f4056b (diff) | |
| download | compcert-kvx-3bb0c75456a0dcab079e7614c3bbd3ba971e4519.tar.gz compcert-kvx-3bb0c75456a0dcab079e7614c3bbd3ba971e4519.zip | |
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.
Diffstat (limited to 'backend/Inlining.v')
| -rw-r--r-- | backend/Inlining.v | 13 |
1 files changed, 9 insertions, 4 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 *) |