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/Inliningspec.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/Inliningspec.v')
| -rw-r--r-- | backend/Inliningspec.v | 12 |
1 files changed, 6 insertions, 6 deletions
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. |