From 3bb0c75456a0dcab079e7614c3bbd3ba971e4519 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 7 Dec 2017 12:14:08 +0100 Subject: 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. --- backend/Inliningspec.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'backend/Inliningspec.v') 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. -- cgit