1 {-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables #-}
2 {-# OPTIONS -fglasgow-exts #-}
3 -- -fglagow-exts for kind signatures
6 ( DebugNodes(), RewritingDepth(..), LastOutFacts(..)
7 , zdfSolveFrom, zdfRewriteFrom
8 , ForwardTransfers(..), BackwardTransfers(..)
9 , ForwardRewrites(..), BackwardRewrites(..)
10 , ForwardFixedPoint, BackwardFixedPoint
14 , zdfDecoratedGraph -- not yet implemented
25 import qualified ZipCfg as G
37 This module implements two useful tools:
39 1. An iterative solver for dataflow problems
41 2. The combined dataflow-analysis-and-transformation framework
42 described by Lerner, Grove, and Chambers in their excellent
43 2002 POPL paper (http://tinyurl.com/3zycbr or
44 http://tinyurl.com/3pnscd).
46 Each tool comes in two flavors: one for forward dataflow problems
47 and one for backward dataflow problems.
49 We quote the paper above:
51 Dataflow analyses can have mutually beneficial interactions.
52 Previous efforts to exploit these interactions have either
53 (1) iteratively performed each individual analysis until no
54 further improvements are discovered or (2) developed "super-
55 analyses" that manually combine conceptually separate anal-
56 yses. We have devised a new approach that allows anal-
57 yses to be defined independently while still enabling them
58 to be combined automatically and profitably. Our approach
59 avoids the loss of precision associated with iterating indi-
60 vidual analyses and the implementation difficulties of man-
61 ually writing a super-analysis.
63 The key idea is to provide at each CFG node not only a dataflow
64 transfer function but also a rewriting function that has the option to
65 replace the node with a new (possibly empty) graph. The rewriting
66 function takes a dataflow fact as input, and the fact is used to
67 justify any rewriting. For example, in a backward problem, the fact
68 that variable x is dead can be used to justify rewriting node
70 to the empty graph. In a forward problem, the fact that x == 7 can
71 be used to justify rewriting node
75 which in turn will be analyzed and produce a new fact:
78 In its most general form, this module takes as input graph, transfer
79 equations, rewrites, and an initial set of dataflow facts, and
80 iteratively computes a new graph and a new set of dataflow facts such
82 * The set of facts is a fixed point of the transfer equations
83 * The graph has been rewritten as much as is consistent with
84 the given facts and requested rewriting depth (see below)
85 N.B. 'A set of facts' is shorthand for 'A finite map from CFG label to fact'.
87 The types of transfer equations, rewrites, and fixed points are
88 different for forward and backward problems. To avoid cluttering the
89 name space with two versions of every names, other names such as
90 zdfSolveFrom are overloaded to work in both forward or backward
91 directions. This design decision is based on experience with the
92 predecessor module, now called ZipDataflow0 and destined for the bit bucket.
95 This module is deliberately very abstract. It is a completely general
96 framework and well-nigh impossible to understand in isolation. The
97 cautious reader will begin with some concrete examples in the form of
98 clients. NR recommends
100 CmmLiveZ A simple liveness analysis
102 CmmSpillReload.removeDeadAssignmentsAndReloads
103 A piece of spaghetti to pull on, which leads to
104 - a two-part liveness analysis that tracks
105 variables live in registers and live on the stack
106 - elimination of assignments to dead variables
107 - elimination of redundant reloads
109 Even hearty souls should avoid the CmmProcPointZ client, at least for
115 {- ============ TRANSFER FUNCTIONS AND REWRITES =========== -}
117 -- | For a backward transfer, you're given the fact on a node's
118 -- outedge and you compute the fact on the inedge. Facts have type 'a'.
119 -- A last node may have multiple outedges, each pointing to a labelled
120 -- block, so instead of a fact it is given a mapping from BlockId to fact.
122 data BackwardTransfers middle last a = BackwardTransfers
123 { bt_first_in :: a -> BlockId -> a
124 , bt_middle_in :: a -> middle -> a
125 , bt_last_in :: (BlockId -> a) -> last -> a
128 -- | For a forward transfer, you're given the fact on a node's
129 -- inedge and you compute the fact on the outedge. Because a last node
130 -- may have multiple outedges, each pointing to a labelled
131 -- block, so instead of a fact it produces a list of (BlockId, fact) pairs.
133 data ForwardTransfers middle last a = ForwardTransfers
134 { ft_first_out :: a -> BlockId -> a
135 , ft_middle_out :: a -> middle -> a
136 , ft_last_outs :: a -> last -> LastOutFacts a
137 , ft_exit_out :: a -> a
140 newtype LastOutFacts a = LastOutFacts [(BlockId, a)]
141 -- ^ These are facts flowing out of a last node to the node's successors.
142 -- They are either to be set (if they pertain to the graph currently
143 -- under analysis) or propagated out of a sub-analysis
146 -- | A backward rewrite takes the same inputs as a backward transfer,
147 -- but instead of producing a fact, it produces a replacement graph or Nothing.
148 -- The type of the replacement graph is given as a type parameter 'g'
149 -- of kind * -> * -> *. This design offers great flexibility to clients,
150 -- but it might be worth simplifying this module by replacing this type
151 -- parameter with AGraph everywhere (SLPJ 19 May 2008).
153 data BackwardRewrites middle last a = BackwardRewrites
154 { br_first :: a -> BlockId -> Maybe (AGraph middle last)
155 , br_middle :: a -> middle -> Maybe (AGraph middle last)
156 , br_last :: (BlockId -> a) -> last -> Maybe (AGraph middle last)
157 , br_exit :: Maybe (AGraph middle last)
160 -- | A forward rewrite takes the same inputs as a forward transfer,
161 -- but instead of producing a fact, it produces a replacement graph or Nothing.
163 data ForwardRewrites middle last a = ForwardRewrites
164 { fr_first :: a -> BlockId -> Maybe (AGraph middle last)
165 , fr_middle :: a -> middle -> Maybe (AGraph middle last)
166 , fr_last :: a -> last -> Maybe (AGraph middle last)
167 , fr_exit :: a -> Maybe (AGraph middle last)
170 {- ===================== FIXED POINTS =================== -}
172 -- | The result of combined analysis and transformation is a
173 -- solution to the set of dataflow equations together with a 'contained value'.
174 -- This solution is a member of type class 'FixedPoint', which is parameterized by
175 -- * middle and last nodes 'm' and 'l'
176 -- * data flow fact 'fact'
177 -- * the type 'a' of the contained value
179 -- In practice, the contained value 'zdfFpContents' is either a
180 -- rewritten graph, when rewriting, or (), when solving without
181 -- rewriting. A function 'zdfFpMap' allows a client to change
182 -- the contents without changing other values.
184 -- To save space, we provide the solution 'zdfFpFacts' as a mapping
185 -- from BlockId to fact; if necessary, facts on edges can be
186 -- reconstructed using the transfer functions; this functionality is
187 -- intended to be included as the 'zdfDecoratedGraph', but the code
188 -- has not yet been implemented.
190 -- The solution may also includes a fact 'zdfFpOuputFact', which is
191 -- not associated with any label:
192 -- * for a backward problem, this is the fact at entry
193 -- * for a forward problem, this is the fact at the distinguished exit node,
194 -- if such a node is present
196 -- For a forward problem only, the solution includes 'zdfFpLastOuts',
197 -- which is the set of facts on edges leaving the graph.
199 -- The flag 'zdfGraphChanged' tells whether the engine did any rewriting.
201 class FixedPoint fp where
202 zdfFpContents :: fp m l fact a -> a
203 zdfFpFacts :: fp m l fact a -> BlockEnv fact
204 zdfFpOutputFact :: fp m l fact a -> fact -- entry for backward; exit for forward
205 zdfDecoratedGraph :: fp m l fact a -> Graph (fact, m) (fact, l)
206 zdfGraphChanged :: fp m l fact a -> ChangeFlag
207 zdfFpMap :: (a -> b) -> (fp m l fact a -> fp m l fact b)
209 -- | The class 'FixedPoint' has two instances: one for forward problems and
210 -- one for backward problems. The 'CommonFixedPoint' defines all fields
211 -- common to both. (The instance declarations are uninteresting and appear below.)
213 data CommonFixedPoint m l fact a = FP
214 { fp_facts :: BlockEnv fact
215 , fp_out :: fact -- entry for backward; exit for forward
216 , fp_changed :: ChangeFlag
217 , fp_dec_graph :: Graph (fact, m) (fact, l)
221 -- | The common fixed point is sufficient for a backward problem.
222 type BackwardFixedPoint = CommonFixedPoint
224 -- | A forward problem needs the common fields, plus the facts on the outedges.
225 data ForwardFixedPoint m l fact a = FFP
226 { ffp_common :: CommonFixedPoint m l fact a
227 , zdfFpLastOuts :: LastOutFacts fact
231 {- ============== SOLVING AND REWRITING ============== -}
233 type PassName = String
235 -- | 'zdfSolveFrom' is an overloaded name that resolves to a pure
236 -- analysis with no rewriting. It has only two instances: forward and
237 -- backward. Since it needs no rewrites, the type parameters of the
238 -- class are transfer functions and the fixed point.
241 -- An iterative solver normally starts with the bottom fact at every
242 -- node, but it can be useful in other contexts as well. For this
243 -- reason the initial set of facts (at labelled blocks only) is a
244 -- parameter to the solver.
246 -- The constraints on the type signature exist purely for debugging;
247 -- they make it possible to prettyprint nodes and facts. The parameter of
248 -- type 'PassName' is also used just for debugging.
250 -- Note that the result is a fixed point with no contents, that is,
251 -- the contents have type ().
253 -- The intent of the rest of the type signature should be obvious.
254 -- If not, place a skype call to norman-ramsey or complain bitterly
255 -- to <norman-ramsey@acm.org>.
257 class DataflowSolverDirection transfers fixedpt where
258 zdfSolveFrom :: (DebugNodes m l, Outputable a)
259 => BlockEnv a -- ^ Initial facts (unbound == bottom)
261 -> DataflowLattice a -- ^ Lattice
262 -> transfers m l a -- ^ Dataflow transfer functions
263 -> a -- ^ Fact flowing in (at entry or exit)
264 -> Graph m l -- ^ Graph to be analyzed
265 -> FuelMonad (fixedpt m l a ()) -- ^ Answers
267 -- There are exactly two instances: forward and backward
268 instance DataflowSolverDirection ForwardTransfers ForwardFixedPoint
269 where zdfSolveFrom = solve_f
271 instance DataflowSolverDirection BackwardTransfers BackwardFixedPoint
272 where zdfSolveFrom = solve_b
275 -- | zdfRewriteFrom is an overloaded name that resolves to an
276 -- interleaved analysis and transformation. It too is instantiated in
277 -- forward and backward directions.
279 -- The type parameters of the class include not only transfer
280 -- functions and the fixed point but also rewrites and the type
281 -- constructor (here called 'graph') for making rewritten graphs. As
282 -- above, in the definitoins of the rewrites, it might simplify
283 -- matters if 'graph' were replaced with 'AGraph'.
285 -- The type signature of 'zdfRewriteFrom' is that of 'zdfSolveFrom'
286 -- with additional parameters and a different result. Of course the
287 -- rewrites are an additional parameter, but there are further
288 -- parameters which reflect the fact that rewriting consumes both
289 -- OptimizationFuel and Uniqs.
291 -- The result type is changed to reflect fuel consumption, and also
292 -- the resulting fixed point containts a rewritten graph.
294 -- John Dias is going to improve the management of Uniqs and Fuel so
295 -- that it doesn't make us sick to look at the types.
297 class DataflowSolverDirection transfers fixedpt =>
298 DataflowDirection transfers fixedpt rewrites where
299 zdfRewriteFrom :: (DebugNodes m l, Outputable a)
300 => RewritingDepth -- whether to rewrite a rewritten graph
301 -> BlockEnv a -- initial facts (unbound == botton)
306 -> a -- fact flowing in (at entry or exit)
308 -> FuelMonad (fixedpt m l a (Graph m l))
310 data RewritingDepth = RewriteShallow | RewriteDeep
311 -- When a transformation proposes to rewrite a node,
312 -- you can either ask the system to
313 -- * "shallow": accept the new graph, analyse it without further rewriting
314 -- * "deep": recursively analyse-and-rewrite the new graph
317 -- There are currently four instances, but there could be more
318 -- forward, backward (instantiates transfers, fixedpt, rewrites)
319 -- Graph, AGraph (instantiates graph)
321 instance DataflowDirection ForwardTransfers ForwardFixedPoint ForwardRewrites
322 where zdfRewriteFrom = rewrite_f_agraph
324 instance DataflowDirection BackwardTransfers BackwardFixedPoint BackwardRewrites
325 where zdfRewriteFrom = rewrite_b_agraph
328 {- =================== IMPLEMENTATIONS ===================== -}
331 -----------------------------------------------------------
332 -- solve_f: forward, pure
334 solve_f :: (DebugNodes m l, Outputable a)
335 => BlockEnv a -- initial facts (unbound == bottom)
337 -> DataflowLattice a -- lattice
338 -> ForwardTransfers m l a -- dataflow transfer functions
340 -> Graph m l -- graph to be analyzed
341 -> FuelMonad (ForwardFixedPoint m l a ()) -- answers
342 solve_f env name lattice transfers in_fact g =
343 runDFM lattice $ fwd_pure_anal name env transfers in_fact g
345 rewrite_f_agraph :: (DebugNodes m l, Outputable a)
350 -> ForwardTransfers m l a
351 -> ForwardRewrites m l a
352 -> a -- fact flowing in (at entry or exit)
354 -> FuelMonad (ForwardFixedPoint m l a (Graph m l))
355 rewrite_f_agraph depth start_facts name lattice transfers rewrites in_fact g =
357 do fuel <- fuelRemaining
358 (fp, fuel') <- forward_rew maybeRewriteWithFuel depth start_facts name
359 transfers rewrites in_fact g fuel
360 fuelDecrement name fuel fuel'
363 areturn :: AGraph m l -> DFM a (Graph m l)
364 areturn g = liftToDFM $ liftUniq $ graphOfAGraph g
368 graphToLGraph :: LastNode l => Graph m l -> DFM a (LGraph m l)
369 graphToLGraph (Graph (ZLast (LastOther l)) blockenv)
370 | isBranchNode l = return $ LGraph (branchNodeTarget l) blockenv
371 graphToLGraph (Graph tail blockenv) =
372 do id <- freshBlockId "temporary entry label"
373 return $ LGraph id $ insertBlock (Block id tail) blockenv
376 -- | Here we prefer not simply to slap on 'goto eid' because this
377 -- introduces an unnecessary basic block at each rewrite, and we don't
378 -- want to stress out the finite map more than necessary
379 lgraphToGraph :: LastNode l => LGraph m l -> Graph m l
380 lgraphToGraph (LGraph eid blocks) =
381 if flip any (eltsUFM blocks) $ \block -> any (== eid) (succs block) then
382 Graph (ZLast (mkBranchNode eid)) blocks
383 else -- common case: entry is not a branch target
384 let Block _ entry = lookupBlockEnv blocks eid `orElse` panic "missing entry!"
385 in Graph entry (delFromUFM blocks eid)
388 class (Outputable m, Outputable l, LastNode l, Outputable (LGraph m l)) => DebugNodes m l
390 fwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
393 -> ForwardTransfers m l a
396 -> DFM a (ForwardFixedPoint m l a ())
398 fwd_pure_anal name env transfers in_fact g =
399 do (fp, _) <- anal_f name env transfers panic_rewrites in_fact g panic_fuel
401 where -- definitiely a case of "I love lazy evaluation"
402 anal_f = forward_sol (\_ _ -> Nothing) panic_depth
403 panic_rewrites = panic "pure analysis asked for a rewrite function"
404 panic_fuel = panic "pure analysis asked for fuel"
405 panic_depth = panic "pure analysis asked for a rewrite depth"
407 -----------------------------------------------------------------------
409 -- Here beginneth the super-general functions
411 -- Think of them as (typechecked) macros
412 -- * They are not exported
414 -- * They are called by the specialised wrappers
415 -- above, and always inlined into their callers
417 -- There are four functions, one for each combination of:
421 -- A "solver" produces a (DFM f (f, Fuel)),
422 -- where f is the fact at entry(Bwd)/exit(Fwd)
423 -- and from the DFM you can extract
428 -- A "rewriter" produces a rewritten *Graph* as well
430 -- Both constrain their rewrites by
432 -- b) RewritingDepth: shallow/deep
434 -----------------------------------------------------------------------
436 type Fuel = OptimizationFuel
438 {-# INLINE forward_sol #-}
441 (DebugNodes m l, LastNode l, Outputable a)
442 => (forall a . Fuel -> Maybe a -> Maybe a)
443 -- Squashes proposed rewrites if there is
444 -- no more fuel; OR if we are doing a pure
445 -- analysis, so totally ignore the rewrite
446 -- ie. For pure-analysis the fn is (\_ _ -> Nothing)
447 -> RewritingDepth -- Shallow/deep
449 -> BlockEnv a -- Initial set of facts
450 -> ForwardTransfers m l a
451 -> ForwardRewrites m l a
455 -> DFM a (ForwardFixedPoint m l a (), Fuel)
456 forward_sol check_maybe = forw
458 forw :: RewritingDepth
461 -> ForwardTransfers m l a
462 -> ForwardRewrites m l a
466 -> DFM a (ForwardFixedPoint m l a (), Fuel)
467 forw rewrite name start_facts transfers rewrites =
468 let anal_f :: DFM a b -> a -> Graph m l -> DFM a b
469 anal_f finish in' g =
470 do { fwd_pure_anal name emptyBlockEnv transfers in' g; finish }
472 solve :: DFM a b -> a -> Graph m l -> Fuel -> DFM a (b, Fuel)
473 solve finish in_fact (Graph entry blockenv) fuel =
474 let blocks = G.postorder_dfs_from blockenv entry
475 set_or_save = mk_set_or_save (isJust . lookupBlockEnv blockenv)
476 set_successor_facts (Block id tail) fuel =
477 do { idfact <- getFact id
478 ; (last_outs, fuel) <-
479 case check_maybe fuel $ fr_first rewrites idfact id of
480 Nothing -> solve_tail (ft_first_out transfers idfact id) tail fuel
483 (a, fuel) <- subAnalysis' $
485 RewriteDeep -> solve getExitFact idfact g (oneLessFuel fuel)
487 do { a <- anal_f getExitFact idfact g
488 ; return (a, oneLessFuel fuel) }
489 solve_tail a tail fuel
490 ; set_or_save last_outs
493 in do { (last_outs, fuel) <- solve_tail in_fact entry fuel
494 ; set_or_save last_outs
495 ; fuel <- run "forward" name set_successor_facts blocks fuel
500 solve_tail in' (G.ZTail m t) fuel =
501 case check_maybe fuel $ fr_middle rewrites in' m of
502 Nothing -> solve_tail (ft_middle_out transfers in' m) t fuel
505 ; (a, fuel) <- subAnalysis' $
507 RewriteDeep -> solve getExitFact in' g (oneLessFuel fuel)
508 RewriteShallow -> do { a <- anal_f getExitFact in' g
509 ; return (a, oneLessFuel fuel) }
510 ; solve_tail a t fuel
512 solve_tail in' (G.ZLast l) fuel =
513 case check_maybe fuel $ either_last rewrites in' l of
515 case l of LastOther l -> return (ft_last_outs transfers in' l, fuel)
516 LastExit -> do { setExitFact (ft_exit_out transfers in')
517 ; return (LastOutFacts [], fuel) }
520 ; (last_outs :: LastOutFacts a, fuel) <- subAnalysis' $
522 RewriteDeep -> solve lastOutFacts in' g (oneLessFuel fuel)
523 RewriteShallow -> do { los <- anal_f lastOutFacts in' g
524 ; return (los, fuel) }
525 ; return (last_outs, fuel)
528 fixed_point in_fact g fuel =
529 do { setAllFacts start_facts
530 ; (a, fuel) <- solve getExitFact in_fact g fuel
531 ; facts <- getAllFacts
532 ; last_outs <- lastOutFacts
533 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
534 ; let fp = FFP cfp last_outs
538 either_last rewrites in' (LastExit) = fr_exit rewrites in'
539 either_last rewrites in' (LastOther l) = fr_last rewrites in' l
546 mk_set_or_save :: (DataflowAnalysis df, Monad (df a), Outputable a) =>
547 (BlockId -> Bool) -> LastOutFacts a -> df a ()
548 mk_set_or_save is_local (LastOutFacts l) = mapM_ set_or_save_one l
549 where set_or_save_one (id, a) =
550 if is_local id then setFact id a else addLastOutFact (id, a)
555 {-# INLINE forward_rew #-}
558 (DebugNodes m l, LastNode l, Outputable a)
559 => (forall a . Fuel -> Maybe a -> Maybe a)
563 -> ForwardTransfers m l a
564 -> ForwardRewrites m l a
568 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
569 forward_rew check_maybe = forw
571 solve = forward_sol check_maybe
572 forw :: RewritingDepth
575 -> ForwardTransfers m l a
576 -> ForwardRewrites m l a
580 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
581 forw depth xstart_facts name transfers rewrites in_factx gx fuelx =
582 let rewrite :: BlockEnv a -> DFM a b
583 -> a -> Graph m l -> Fuel
584 -> DFM a (b, Graph m l, Fuel)
585 rewrite start finish in_fact g fuel =
586 let Graph entry blockenv = g
587 blocks = G.postorder_dfs_from blockenv entry
588 in do { solve depth name start transfers rewrites in_fact g fuel
589 ; eid <- freshBlockId "temporary entry id"
590 ; (rewritten, fuel) <-
591 rew_tail (ZFirst eid) in_fact entry emptyBlockEnv fuel
592 ; (rewritten, fuel) <- rewrite_blocks blocks rewritten fuel
594 ; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
596 don't_rewrite facts finish in_fact g fuel =
597 do { solve depth name facts transfers rewrites in_fact g fuel
599 ; return (a, g, fuel)
601 inner_rew :: DFM a f -> a -> Graph m l -> Fuel -> DFM a (f, Graph m l, Fuel)
602 inner_rew f i g fu = getAllFacts >>= \facts -> inner_rew' facts f i g fu
603 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
604 RewriteDeep -> rewrite
606 do { (a, g, fuel) <- rewrite xstart_facts getExitFact in_factx gx fuelx
607 ; facts <- getAllFacts
608 ; changed <- graphWasRewritten
609 ; last_outs <- lastOutFacts
610 ; let cfp = FP facts a changed (panic "no decoration?!") g
611 ; let fp = FFP cfp last_outs
614 rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
615 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
616 rewrite_blocks [] rewritten fuel = return (rewritten, fuel)
617 rewrite_blocks (G.Block id t : bs) rewritten fuel =
620 case check_maybe fuel $ fr_first rewrites a id of
621 Nothing -> do { (rewritten, fuel) <-
622 rew_tail h (ft_first_out transfers a id)
624 ; rewrite_blocks bs rewritten fuel }
625 Just g -> do { markGraphRewritten
627 ; (outfact, g, fuel) <- inner_rew getExitFact a g fuel
628 ; let (blocks, h) = splice_head' (ZFirst id) g
629 ; (rewritten, fuel) <-
630 rew_tail h outfact t (blocks `plusUFM` rewritten) fuel
631 ; rewrite_blocks bs rewritten fuel }
633 rew_tail head in' (G.ZTail m t) rewritten fuel =
634 my_trace "Rewriting middle node" (ppr m) $
635 case check_maybe fuel $ fr_middle rewrites in' m of
636 Nothing -> rew_tail (G.ZHead head m) (ft_middle_out transfers in' m) t
638 Just g -> do { markGraphRewritten
640 ; (a, g, fuel) <- inner_rew getExitFact in' g fuel
641 ; let (blocks, h) = G.splice_head' head g
642 ; rew_tail h a t (blocks `plusUFM` rewritten) fuel
644 rew_tail h in' (G.ZLast l) rewritten fuel =
645 my_trace "Rewriting last node" (ppr l) $
646 case check_maybe fuel $ either_last rewrites in' l of
647 Nothing -> do check_facts in' l
648 return (insertBlock (zipht h (G.ZLast l)) rewritten, fuel)
649 Just g -> do { markGraphRewritten
651 ; ((), g, fuel) <- inner_rew (return ()) in' g fuel
652 ; let g' = G.splice_head_only' h g
653 ; return (G.lg_blocks g' `plusUFM` rewritten, fuel)
655 either_last rewrites in' (LastExit) = fr_exit rewrites in'
656 either_last rewrites in' (LastOther l) = fr_last rewrites in' l
657 check_facts in' (LastOther l) =
658 let LastOutFacts last_outs = ft_last_outs transfers in' l
659 in mapM (uncurry checkFactMatch) last_outs
660 check_facts _ LastExit = return []
663 lastOutFacts :: DFM f (LastOutFacts f)
664 lastOutFacts = bareLastOutFacts >>= return . LastOutFacts
666 {- ================================================================ -}
668 solve_b :: (DebugNodes m l, Outputable a)
669 => BlockEnv a -- initial facts (unbound == bottom)
671 -> DataflowLattice a -- lattice
672 -> BackwardTransfers m l a -- dataflow transfer functions
674 -> Graph m l -- graph to be analyzed
675 -> FuelMonad (BackwardFixedPoint m l a ()) -- answers
676 solve_b env name lattice transfers exit_fact g =
677 runDFM lattice $ bwd_pure_anal name env transfers g exit_fact
680 rewrite_b_agraph :: (DebugNodes m l, Outputable a)
685 -> BackwardTransfers m l a
686 -> BackwardRewrites m l a
687 -> a -- fact flowing in at exit
689 -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
690 rewrite_b_agraph depth start_facts name lattice transfers rewrites exit_fact g =
692 do fuel <- fuelRemaining
693 (fp, fuel') <- backward_rew maybeRewriteWithFuel depth start_facts name
694 transfers rewrites g exit_fact fuel
695 fuelDecrement name fuel fuel'
700 {-# INLINE backward_sol #-}
703 (DebugNodes m l, LastNode l, Outputable a)
704 => (forall a . Fuel -> Maybe a -> Maybe a)
708 -> BackwardTransfers m l a
709 -> BackwardRewrites m l a
713 -> DFM a (BackwardFixedPoint m l a (), Fuel)
714 backward_sol check_maybe = back
716 back :: RewritingDepth
719 -> BackwardTransfers m l a
720 -> BackwardRewrites m l a
724 -> DFM a (BackwardFixedPoint m l a (), Fuel)
725 back rewrite name start_facts transfers rewrites =
726 let anal_b :: Graph m l -> a -> DFM a a
728 do { fp <- bwd_pure_anal name emptyBlockEnv transfers g out
729 ; return $ zdfFpOutputFact fp }
731 subsolve :: AGraph m l -> a -> Fuel -> DFM a (a, Fuel)
734 RewriteDeep -> \g a fuel ->
735 subAnalysis' $ do { g <- areturn g; solve g a (oneLessFuel fuel) }
736 RewriteShallow -> \g a fuel ->
737 subAnalysis' $ do { g <- areturn g; a <- anal_b g a
738 ; return (a, oneLessFuel fuel) }
740 solve :: Graph m l -> a -> Fuel -> DFM a (a, Fuel)
741 solve (Graph entry blockenv) exit_fact fuel =
742 let blocks = reverse $ G.postorder_dfs_from blockenv entry
743 last_in _env (LastExit) = exit_fact
744 last_in env (LastOther l) = bt_last_in transfers env l
745 last_rew _env (LastExit) = br_exit rewrites
746 last_rew env (LastOther l) = br_last rewrites env l
747 set_block_fact block fuel =
748 let (h, l) = G.goto_end (G.unzip block) in
751 case check_maybe fuel $ last_rew env l of
752 Nothing -> return (last_in env l, fuel)
753 Just g -> subsolve g exit_fact fuel
754 ; set_head_fact h a fuel
757 in do { fuel <- run "backward" name set_block_fact blocks fuel
758 ; eid <- freshBlockId "temporary entry id"
759 ; fuel <- set_block_fact (Block eid entry) fuel
765 set_head_fact (G.ZFirst id) a fuel =
766 case check_maybe fuel $ br_first rewrites a id of
767 Nothing -> do { my_trace "set_head_fact" (ppr id) $
768 setFact id $ bt_first_in transfers a id
770 Just g -> do { (a, fuel) <- subsolve g a fuel
774 set_head_fact (G.ZHead h m) a fuel =
775 case check_maybe fuel $ br_middle rewrites a m of
776 Nothing -> set_head_fact h (bt_middle_in transfers a m) fuel
777 Just g -> do { (a, fuel) <- subsolve g a fuel
778 ; set_head_fact h a fuel }
780 fixed_point g exit_fact fuel =
781 do { setAllFacts start_facts
782 ; (a, fuel) <- solve g exit_fact fuel
783 ; facts <- getAllFacts
784 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
789 bwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
792 -> BackwardTransfers m l a
795 -> DFM a (BackwardFixedPoint m l a ())
797 bwd_pure_anal name env transfers g exit_fact =
798 do (fp, _) <- anal_b name env transfers panic_rewrites g exit_fact panic_fuel
800 where -- another case of "I love lazy evaluation"
801 anal_b = backward_sol (\_ _ -> Nothing) panic_depth
802 panic_rewrites = panic "pure analysis asked for a rewrite function"
803 panic_fuel = panic "pure analysis asked for fuel"
804 panic_depth = panic "pure analysis asked for a rewrite depth"
807 {- ================================================================ -}
809 {-# INLINE backward_rew #-}
812 (DebugNodes m l, LastNode l, Outputable a)
813 => (forall a . Fuel -> Maybe a -> Maybe a)
817 -> BackwardTransfers m l a
818 -> BackwardRewrites m l a
822 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
823 backward_rew check_maybe = back
825 solve = backward_sol check_maybe
826 back :: RewritingDepth
829 -> BackwardTransfers m l a
830 -> BackwardRewrites m l a
834 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
835 back depth xstart_facts name transfers rewrites gx exit_fact fuelx =
836 let rewrite :: BlockEnv a
837 -> Graph m l -> a -> Fuel
838 -> DFM a (a, Graph m l, Fuel)
839 rewrite start g exit_fact fuel =
840 let Graph entry blockenv = g
841 blocks = reverse $ G.postorder_dfs_from blockenv entry
842 in do { solve depth name start transfers rewrites g exit_fact fuel
844 ; my_trace "facts after solving" (ppr env) $ return ()
845 ; eid <- freshBlockId "temporary entry id"
846 ; (rewritten, fuel) <- rewrite_blocks True blocks emptyBlockEnv fuel
847 -- We can't have the fact check fail on the bogus entry, which _may_ change
848 ; (rewritten, fuel) <- rewrite_blocks False [Block eid entry] rewritten fuel
850 ; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
852 don't_rewrite facts g exit_fact fuel =
854 solve depth name facts transfers rewrites g exit_fact fuel
855 ; return (zdfFpOutputFact fp, g, fuel) }
856 inner_rew :: Graph m l -> a -> Fuel -> DFM a (a, Graph m l, Fuel)
857 inner_rew g a f = getAllFacts >>= \facts -> inner_rew' facts g a f
858 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
859 RewriteDeep -> rewrite
861 do { (a, g, fuel) <- rewrite xstart_facts gx exit_fact fuelx
862 ; facts <- getAllFacts
863 ; changed <- graphWasRewritten
864 ; let fp = FP facts a changed (panic "no decoration?!") g
867 rewrite_blocks :: Bool -> [Block m l] -> (BlockEnv (Block m l))
868 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
869 rewrite_blocks check bs rewritten fuel =
871 ; let rew [] r f = return (r, f)
873 do { (r, f) <- rewrite_block check env b r f; rew bs r f }
874 ; rew bs rewritten fuel }
875 rewrite_block check env b rewritten fuel =
876 let (h, l) = G.goto_end (G.unzip b) in
877 case maybeRewriteWithFuel fuel $ either_last env l of
878 Nothing -> propagate check fuel h (last_in env l) (ZLast l) rewritten
880 do { markGraphRewritten
882 ; (a, g, fuel) <- inner_rew g exit_fact fuel
883 ; let G.Graph t new_blocks = g
884 ; let rewritten' = new_blocks `plusUFM` rewritten
885 ; propagate check fuel h a t rewritten' -- continue at entry of g
887 either_last _env (LastExit) = br_exit rewrites
888 either_last env (LastOther l) = br_last rewrites env l
889 last_in _env (LastExit) = exit_fact
890 last_in env (LastOther l) = bt_last_in transfers env l
891 propagate check fuel (ZHead h m) a tail rewritten =
892 case maybeRewriteWithFuel fuel $ br_middle rewrites a m of
894 propagate check fuel h (bt_middle_in transfers a m) (ZTail m tail) rewritten
896 do { markGraphRewritten
898 ; my_trace "With Facts" (ppr a) $ return ()
899 ; my_trace " Rewrote middle node"
900 (f4sep [ppr m, text "to", pprGraph g]) $
902 ; (a, g, fuel) <- inner_rew g a fuel
903 ; let Graph t newblocks = G.splice_tail g tail
904 ; propagate check fuel h a t (newblocks `plusUFM` rewritten) }
905 propagate check fuel (ZFirst id) a tail rewritten =
906 case maybeRewriteWithFuel fuel $ br_first rewrites a id of
907 Nothing -> do { if check then checkFactMatch id $ bt_first_in transfers a id
909 ; return (insertBlock (Block id tail) rewritten, fuel) }
911 do { markGraphRewritten
913 ; my_trace "Rewrote first node"
914 (f4sep [ppr id <> colon, text "to", pprGraph g]) $ return ()
915 ; (a, g, fuel) <- inner_rew g a fuel
916 ; if check then checkFactMatch id a else return ()
917 ; let Graph t newblocks = G.splice_tail g tail
918 ; let r = insertBlock (Block id t) (newblocks `plusUFM` rewritten)
922 {- ================================================================ -}
924 instance FixedPoint CommonFixedPoint where
925 zdfFpFacts = fp_facts
926 zdfFpOutputFact = fp_out
927 zdfGraphChanged = fp_changed
928 zdfDecoratedGraph = fp_dec_graph
929 zdfFpContents = fp_contents
930 zdfFpMap f (FP fs out ch dg a) = FP fs out ch dg (f a)
932 instance FixedPoint ForwardFixedPoint where
933 zdfFpFacts = fp_facts . ffp_common
934 zdfFpOutputFact = fp_out . ffp_common
935 zdfGraphChanged = fp_changed . ffp_common
936 zdfDecoratedGraph = fp_dec_graph . ffp_common
937 zdfFpContents = fp_contents . ffp_common
938 zdfFpMap f (FFP fp los) = FFP (zdfFpMap f fp) los
944 my_trace :: String -> SDoc -> a -> a
945 my_trace = if dump_things then pprTrace else \_ _ a -> a
948 -- | Here's a function to run an action on blocks until we reach a fixed point.
949 run :: (Outputable a, DebugNodes m l) =>
950 String -> String -> (Block m l -> b -> DFM a b) -> [Block m l] -> b -> DFM a b
951 run dir name do_block blocks b =
952 do { show_blocks $ iterate (1::Int) }
954 -- N.B. Each iteration starts with the same transaction limit;
955 -- only the rewrites in the final iteration actually count
956 trace_block b block =
957 my_trace "about to do" (text name <+> text "on" <+> ppr (blockId block)) $
960 do { markFactsUnchanged
961 ; b <- foldM trace_block b blocks
962 ; changed <- factsStatus
963 ; facts <- getAllFacts
964 ; let depth = 0 -- was nesting depth
967 NoChange -> unchanged depth $ return b
969 pprFacts depth n facts $
970 if n < 1000 then iterate (n+1)
973 msg n = concat [name, " didn't converge in ", show n, " " , dir,
975 my_nest depth sdoc = my_trace "" $ nest (3*depth) sdoc
976 ppIter depth n = my_nest depth (empty $$ text "*************** iteration" <+> pp_i n)
977 pp_i n = int n <+> text "of" <+> text name <+> text "on" <+> graphId
979 my_nest depth (text "facts for" <+> graphId <+> text "are unchanged")
981 graphId = case blocks of { Block id _ : _ -> ppr id ; [] -> text "<empty>" }
982 show_blocks = my_trace "Blocks:" (vcat (map pprBlock blocks))
983 pprBlock (Block id t) = nest 2 (pprFact (id, t))
984 pprFacts depth n env =
985 my_nest depth (text "facts for iteration" <+> pp_i n <+> text "are:" $$
986 (nest 2 $ vcat $ map pprFact $ ufmToList env))
987 pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)
990 f4sep :: [SDoc] -> SDoc
992 f4sep (d:ds) = fsep (d : map (nest 4) ds)
995 subAnalysis' :: (Monad (m f), DataflowAnalysis m, Outputable f) =>
998 do { a <- subAnalysis $
999 do { a <- m; facts <- getAllFacts
1000 ; my_trace "after sub-analysis facts are" (pprFacts facts) $
1002 ; facts <- getAllFacts
1003 ; my_trace "in parent analysis facts are" (pprFacts facts) $
1005 where pprFacts env = nest 2 $ vcat $ map pprFact $ ufmToList env
1006 pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)