1 {-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables #-}
2 {-# OPTIONS -fglasgow-exts #-}
3 -- -fglagow-exts for kind signatures
6 ( DebugNodes(), RewritingDepth(..), LastOutFacts(..)
7 , zdfSolveFrom, zdfRewriteFrom
9 , ForwardTransfers(..), BackwardTransfers(..)
10 , ForwardRewrites(..), BackwardRewrites(..)
11 , ForwardFixedPoint, BackwardFixedPoint
15 , zdfDecoratedGraph -- not yet implemented
18 , zdfBRewriteFromL, zdfFRewriteFromL
25 import OptimizationFuel as F
28 import qualified ZipCfg as G
39 This module implements two useful tools:
41 1. An iterative solver for dataflow problems
43 2. The combined dataflow-analysis-and-transformation framework
44 described by Lerner, Grove, and Chambers in their excellent
45 2002 POPL paper (http://tinyurl.com/3zycbr or
46 http://tinyurl.com/3pnscd).
48 Each tool comes in two flavors: one for forward dataflow problems
49 and one for backward dataflow problems.
51 We quote the paper above:
53 Dataflow analyses can have mutually beneficial interactions.
54 Previous efforts to exploit these interactions have either
55 (1) iteratively performed each individual analysis until no
56 further improvements are discovered or (2) developed "super-
57 analyses" that manually combine conceptually separate anal-
58 yses. We have devised a new approach that allows anal-
59 yses to be defined independently while still enabling them
60 to be combined automatically and profitably. Our approach
61 avoids the loss of precision associated with iterating indi-
62 vidual analyses and the implementation difficulties of man-
63 ually writing a super-analysis.
65 The key idea is to provide at each CFG node not only a dataflow
66 transfer function but also a rewriting function that has the option to
67 replace the node with a new (possibly empty) graph. The rewriting
68 function takes a dataflow fact as input, and the fact is used to
69 justify any rewriting. For example, in a backward problem, the fact
70 that variable x is dead can be used to justify rewriting node
72 to the empty graph. In a forward problem, the fact that x == 7 can
73 be used to justify rewriting node
77 which in turn will be analyzed and produce a new fact:
80 In its most general form, this module takes as input graph, transfer
81 equations, rewrites, and an initial set of dataflow facts, and
82 iteratively computes a new graph and a new set of dataflow facts such
84 * The set of facts is a fixed point of the transfer equations
85 * The graph has been rewritten as much as is consistent with
86 the given facts and requested rewriting depth (see below)
87 N.B. 'A set of facts' is shorthand for 'A finite map from CFG label to fact'.
89 The types of transfer equations, rewrites, and fixed points are
90 different for forward and backward problems. To avoid cluttering the
91 name space with two versions of every name, other names such as
92 zdfSolveFrom are overloaded to work in both forward or backward
93 directions. This design decision is based on experience with the
94 predecessor module, which has been mercifully deleted.
97 This module is deliberately very abstract. It is a completely general
98 framework and well-nigh impossible to understand in isolation. The
99 cautious reader will begin with some concrete examples in the form of
100 clients. NR recommends
102 CmmLiveZ A simple liveness analysis
104 CmmSpillReload.removeDeadAssignmentsAndReloads
105 A piece of spaghetti to pull on, which leads to
106 - a two-part liveness analysis that tracks
107 variables live in registers and live on the stack
108 - elimination of assignments to dead variables
109 - elimination of redundant reloads
111 Even hearty souls should avoid the CmmProcPointZ client, at least for
117 {- ============ TRANSFER FUNCTIONS AND REWRITES =========== -}
119 -- | For a backward transfer, you're given the fact on a node's
120 -- outedge and you compute the fact on the inedge. Facts have type 'a'.
121 -- A last node may have multiple outedges, each pointing to a labelled
122 -- block, so instead of a fact it is given a mapping from BlockId to fact.
124 data BackwardTransfers middle last a = BackwardTransfers
125 { bt_first_in :: BlockId -> a -> a
126 , bt_middle_in :: middle -> a -> a
127 , bt_last_in :: last -> (BlockId -> a) -> a
130 -- | For a forward transfer, you're given the fact on a node's
131 -- inedge and you compute the fact on the outedge. Because a last node
132 -- may have multiple outedges, each pointing to a labelled
133 -- block, so instead of a fact it produces a list of (BlockId, fact) pairs.
135 data ForwardTransfers middle last a = ForwardTransfers
136 { ft_first_out :: BlockId -> a -> a
137 , ft_middle_out :: middle -> a -> a
138 , ft_last_outs :: last -> a -> LastOutFacts a
139 , ft_exit_out :: a -> a
142 newtype LastOutFacts a = LastOutFacts [(BlockId, a)]
143 -- ^ These are facts flowing out of a last node to the node's successors.
144 -- They are either to be set (if they pertain to the graph currently
145 -- under analysis) or propagated out of a sub-analysis
148 -- | A backward rewrite takes the same inputs as a backward transfer,
149 -- but instead of producing a fact, it produces a replacement graph or Nothing.
151 data BackwardRewrites middle last a = BackwardRewrites
152 { br_first :: BlockId -> a -> Maybe (AGraph middle last)
153 , br_middle :: middle -> a -> Maybe (AGraph middle last)
154 , br_last :: last -> (BlockId -> a) -> Maybe (AGraph middle last)
155 , br_exit :: Maybe (AGraph middle last)
158 -- | A forward rewrite takes the same inputs as a forward transfer,
159 -- but instead of producing a fact, it produces a replacement graph or Nothing.
161 data ForwardRewrites middle last a = ForwardRewrites
162 { fr_first :: BlockId -> a -> Maybe (AGraph middle last)
163 , fr_middle :: middle -> a -> Maybe (AGraph middle last)
164 , fr_last :: last -> a -> Maybe (AGraph middle last)
165 , fr_exit :: a -> Maybe (AGraph middle last)
168 {- ===================== FIXED POINTS =================== -}
170 -- | The result of combined analysis and transformation is a
171 -- solution to the set of dataflow equations together with a 'contained value'.
172 -- This solution is a member of type class 'FixedPoint', which is parameterized by
173 -- * middle and last nodes 'm' and 'l'
174 -- * data flow fact 'fact'
175 -- * the type 'a' of the contained value
177 -- In practice, the contained value 'zdfFpContents' is either a
178 -- rewritten graph, when rewriting, or (), when solving without
179 -- rewriting. A function 'zdfFpMap' allows a client to change
180 -- the contents without changing other values.
182 -- To save space, we provide the solution 'zdfFpFacts' as a mapping
183 -- from BlockId to fact; if necessary, facts on edges can be
184 -- reconstructed using the transfer functions; this functionality is
185 -- intended to be included as the 'zdfDecoratedGraph', but the code
186 -- has not yet been implemented.
188 -- The solution may also includes a fact 'zdfFpOuputFact', which is
189 -- not associated with any label:
190 -- * for a backward problem, this is the fact at entry
191 -- * for a forward problem, this is the fact at the distinguished exit node,
192 -- if such a node is present
194 -- For a forward problem only, the solution includes 'zdfFpLastOuts',
195 -- which is the set of facts on edges leaving the graph.
197 -- The flag 'zdfGraphChanged' tells whether the engine did any rewriting.
199 class FixedPoint fp where
200 zdfFpContents :: fp m l fact a -> a
201 zdfFpFacts :: fp m l fact a -> BlockEnv fact
202 zdfFpOutputFact :: fp m l fact a -> fact -- entry for backward; exit for forward
203 zdfDecoratedGraph :: fp m l fact a -> Graph (fact, m) (fact, l)
204 zdfGraphChanged :: fp m l fact a -> ChangeFlag
205 zdfFpMap :: (a -> b) -> (fp m l fact a -> fp m l fact b)
207 -- | The class 'FixedPoint' has two instances: one for forward problems and
208 -- one for backward problems. The 'CommonFixedPoint' defines all fields
209 -- common to both. (The instance declarations are uninteresting and appear below.)
211 data CommonFixedPoint m l fact a = FP
212 { fp_facts :: BlockEnv fact
213 , fp_out :: fact -- entry for backward; exit for forward
214 , fp_changed :: ChangeFlag
215 , fp_dec_graph :: Graph (fact, m) (fact, l)
219 -- | The common fixed point is sufficient for a backward problem.
220 type BackwardFixedPoint = CommonFixedPoint
222 -- | A forward problem needs the common fields, plus the facts on the outedges.
223 data ForwardFixedPoint m l fact a = FFP
224 { ffp_common :: CommonFixedPoint m l fact a
225 , zdfFpLastOuts :: LastOutFacts fact
229 {- ============== SOLVING AND REWRITING ============== -}
231 type PassName = String
233 -- | 'zdfSolveFrom' is an overloaded name that resolves to a pure
234 -- analysis with no rewriting. It has only two instances: forward and
235 -- backward. Since it needs no rewrites, the type parameters of the
236 -- class are transfer functions and the fixed point.
239 -- An iterative solver normally starts with the bottom fact at every
240 -- node, but it can be useful in other contexts as well. For this
241 -- reason the initial set of facts (at labelled blocks only) is a
242 -- parameter to the solver.
244 -- The constraints on the type signature exist purely for debugging;
245 -- they make it possible to prettyprint nodes and facts. The parameter of
246 -- type 'PassName' is also used just for debugging.
248 -- Note that the result is a fixed point with no contents, that is,
249 -- the contents have type ().
251 -- The intent of the rest of the type signature should be obvious.
252 -- If not, place a skype call to norman-ramsey or complain bitterly
253 -- to <norman-ramsey@acm.org>.
255 class DataflowSolverDirection transfers fixedpt where
256 zdfSolveFrom :: (DebugNodes m l, Outputable a)
257 => BlockEnv a -- ^ Initial facts (unbound == bottom)
259 -> DataflowLattice a -- ^ Lattice
260 -> transfers m l a -- ^ Dataflow transfer functions
261 -> a -- ^ Fact flowing in (at entry or exit)
262 -> Graph m l -- ^ Graph to be analyzed
263 -> FuelMonad (fixedpt m l a ()) -- ^ Answers
264 zdfSolveFromL :: (DebugNodes m l, Outputable a)
265 => BlockEnv a -- Initial facts (unbound == bottom)
267 -> DataflowLattice a -- Lattice
268 -> transfers m l a -- Dataflow transfer functions
269 -> a -- Fact flowing in (at entry or exit)
270 -> LGraph m l -- Graph to be analyzed
271 -> FuelMonad (fixedpt m l a ()) -- Answers
272 zdfSolveFromL b p l t a g = zdfSolveFrom b p l t a $ quickGraph g
274 -- There are exactly two instances: forward and backward
275 instance DataflowSolverDirection ForwardTransfers ForwardFixedPoint
276 where zdfSolveFrom = solve_f
278 instance DataflowSolverDirection BackwardTransfers BackwardFixedPoint
279 where zdfSolveFrom = solve_b
282 -- | zdfRewriteFrom is an overloaded name that resolves to an
283 -- interleaved analysis and transformation. It too is instantiated in
284 -- forward and backward directions.
286 -- The type parameters of the class include not only transfer
287 -- functions and the fixed point but also rewrites.
289 -- The type signature of 'zdfRewriteFrom' is that of 'zdfSolveFrom'
290 -- with the rewrites and a rewriting depth as additional parameters,
291 -- as well as a different result, which contains a rewritten graph.
293 class DataflowSolverDirection transfers fixedpt =>
294 DataflowDirection transfers fixedpt rewrites where
295 zdfRewriteFrom :: (DebugNodes m l, Outputable a)
296 => RewritingDepth -- whether to rewrite a rewritten graph
297 -> BlockEnv a -- initial facts (unbound == bottom)
302 -> a -- fact flowing in (at entry or exit)
304 -> FuelMonad (fixedpt m l a (Graph m l))
306 -- Temporarily lifting from Graph to LGraph -- an experiment to see how we
307 -- can eliminate some hysteresis between Graph and LGraph.
308 -- Perhaps Graph should be confined to dataflow code.
309 -- Trading space for time
310 quickGraph :: LastNode l => LGraph m l -> Graph m l
311 quickGraph g = Graph (ZLast $ mkBranchNode $ lg_entry g) $ lg_blocks g
313 quickLGraph :: LastNode l => Graph m l -> FuelMonad (LGraph m l)
314 quickLGraph (Graph (ZLast (LastOther l)) blockenv)
315 | isBranchNode l = return $ LGraph (branchNodeTarget l) blockenv
316 quickLGraph g = F.lGraphOfGraph g
318 fixptWithLGraph :: LastNode l => CommonFixedPoint m l fact (Graph m l) ->
319 FuelMonad (CommonFixedPoint m l fact (LGraph m l))
320 fixptWithLGraph cfp =
321 do fp_c <- quickLGraph $ fp_contents cfp
322 return $ cfp {fp_contents = fp_c}
324 ffixptWithLGraph :: LastNode l => ForwardFixedPoint m l fact (Graph m l) ->
325 FuelMonad (ForwardFixedPoint m l fact (LGraph m l))
326 ffixptWithLGraph fp =
327 do common <- fixptWithLGraph $ ffp_common fp
328 return $ fp {ffp_common = common}
330 zdfFRewriteFromL :: (DebugNodes m l, Outputable a)
331 => RewritingDepth -- whether to rewrite a rewritten graph
332 -> BlockEnv a -- initial facts (unbound == bottom)
335 -> ForwardTransfers m l a
336 -> ForwardRewrites m l a
337 -> a -- fact flowing in (at entry or exit)
339 -> FuelMonad (ForwardFixedPoint m l a (LGraph m l))
340 zdfFRewriteFromL d b p l t r a g@(LGraph _ _) =
341 do fp <- zdfRewriteFrom d b p l t r a $ quickGraph g
344 zdfBRewriteFromL :: (DebugNodes m l, Outputable a)
345 => RewritingDepth -- whether to rewrite a rewritten graph
346 -> BlockEnv a -- initial facts (unbound == bottom)
349 -> BackwardTransfers m l a
350 -> BackwardRewrites m l a
351 -> a -- fact flowing in (at entry or exit)
353 -> FuelMonad (BackwardFixedPoint m l a (LGraph m l))
354 zdfBRewriteFromL d b p l t r a g@(LGraph _ _) =
355 do fp <- zdfRewriteFrom d b p l t r a $ quickGraph g
359 data RewritingDepth = RewriteShallow | RewriteDeep
360 -- When a transformation proposes to rewrite a node,
361 -- you can either ask the system to
362 -- * "shallow": accept the new graph, analyse it without further rewriting
363 -- * "deep": recursively analyse-and-rewrite the new graph
366 -- There are currently four instances, but there could be more
367 -- forward, backward (instantiates transfers, fixedpt, rewrites)
368 -- Graph, AGraph (instantiates graph)
370 instance DataflowDirection ForwardTransfers ForwardFixedPoint ForwardRewrites
371 where zdfRewriteFrom = rewrite_f_agraph
373 instance DataflowDirection BackwardTransfers BackwardFixedPoint BackwardRewrites
374 where zdfRewriteFrom = rewrite_b_agraph
377 {- =================== IMPLEMENTATIONS ===================== -}
380 -----------------------------------------------------------
381 -- solve_f: forward, pure
383 solve_f :: (DebugNodes m l, Outputable a)
384 => BlockEnv a -- initial facts (unbound == bottom)
386 -> DataflowLattice a -- lattice
387 -> ForwardTransfers m l a -- dataflow transfer functions
389 -> Graph m l -- graph to be analyzed
390 -> FuelMonad (ForwardFixedPoint m l a ()) -- answers
391 solve_f env name lattice transfers in_fact g =
392 runDFM lattice $ fwd_pure_anal name env transfers in_fact g
394 rewrite_f_agraph :: (DebugNodes m l, Outputable a)
399 -> ForwardTransfers m l a
400 -> ForwardRewrites m l a
401 -> a -- fact flowing in (at entry or exit)
403 -> FuelMonad (ForwardFixedPoint m l a (Graph m l))
404 rewrite_f_agraph depth start_facts name lattice transfers rewrites in_fact g =
406 do fuel <- fuelRemaining
407 (fp, fuel') <- forward_rew maybeRewriteWithFuel depth start_facts name
408 transfers rewrites in_fact g fuel
409 fuelDecrement name fuel fuel'
412 areturn :: AGraph m l -> DFM a (Graph m l)
413 areturn g = liftToDFM $ liftUniq $ graphOfAGraph g
415 -- | Here we prefer not simply to slap on 'goto eid' because this
416 -- introduces an unnecessary basic block at each rewrite, and we don't
417 -- want to stress out the finite map more than necessary
418 lgraphToGraph :: LastNode l => LGraph m l -> Graph m l
419 lgraphToGraph (LGraph eid blocks) =
420 if flip any (eltsBlockEnv blocks) $ \block -> any (== eid) (succs block) then
421 Graph (ZLast (mkBranchNode eid)) blocks
422 else -- common case: entry is not a branch target
423 let Block _ entry = lookupBlockEnv blocks eid `orElse` panic "missing entry!"
424 in Graph entry (delFromBlockEnv blocks eid)
427 class (Outputable m, Outputable l, LastNode l, Outputable (LGraph m l)) => DebugNodes m l
429 fwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
432 -> ForwardTransfers m l a
435 -> DFM a (ForwardFixedPoint m l a ())
437 fwd_pure_anal name env transfers in_fact g =
438 do (fp, _) <- anal_f name env transfers panic_rewrites in_fact g panic_fuel
440 where -- definitely a case of "I love lazy evaluation"
441 anal_f = forward_sol (\_ _ -> Nothing) panic_depth
442 panic_rewrites = panic "pure analysis asked for a rewrite function"
443 panic_fuel = panic "pure analysis asked for fuel"
444 panic_depth = panic "pure analysis asked for a rewrite depth"
446 -----------------------------------------------------------------------
448 -- Here beginneth the super-general functions
450 -- Think of them as (typechecked) macros
451 -- * They are not exported
453 -- * They are called by the specialised wrappers
454 -- above, and always inlined into their callers
456 -- There are four functions, one for each combination of:
460 -- A "solver" produces a (DFM f (f, Fuel)),
461 -- where f is the fact at entry(Bwd)/exit(Fwd)
462 -- and from the DFM you can extract
467 -- A "rewriter" produces a rewritten *Graph* as well
469 -- Both constrain their rewrites by
471 -- b) RewritingDepth: shallow/deep
473 -----------------------------------------------------------------------
475 type Fuel = OptimizationFuel
479 (DebugNodes m l, LastNode l, Outputable a)
480 => (forall a . Fuel -> Maybe a -> Maybe a)
481 -- Squashes proposed rewrites if there is
482 -- no more fuel; OR if we are doing a pure
483 -- analysis, so totally ignore the rewrite
484 -- ie. For pure-analysis the fn is (\_ _ -> Nothing)
485 -> RewritingDepth -- Shallow/deep
487 -> BlockEnv a -- Initial set of facts
488 -> ForwardTransfers m l a
489 -> ForwardRewrites m l a
493 -> DFM a (ForwardFixedPoint m l a (), Fuel)
494 forward_sol check_maybe = forw
496 forw :: RewritingDepth
499 -> ForwardTransfers m l a
500 -> ForwardRewrites m l a
504 -> DFM a (ForwardFixedPoint m l a (), Fuel)
505 forw rewrite name start_facts transfers rewrites =
506 let anal_f :: DFM a b -> a -> Graph m l -> DFM a b
507 anal_f finish in' g =
508 do { fwd_pure_anal name emptyBlockEnv transfers in' g; finish }
510 solve :: DFM a b -> a -> Graph m l -> Fuel -> DFM a (b, Fuel)
511 solve finish in_fact (Graph entry blockenv) fuel =
512 let blocks = G.postorder_dfs_from blockenv entry
513 set_or_save = mk_set_or_save (isJust . lookupBlockEnv blockenv)
514 set_successor_facts (Block id tail) fuel =
515 do { idfact <- getFact id
516 ; (last_outs, fuel) <- rec_rewrite (fr_first rewrites id idfact)
517 (ft_first_out transfers id idfact)
518 getExitFact (solve_tail tail)
519 (solve_tail tail) idfact fuel
520 ; set_or_save last_outs
522 in do { (last_outs, fuel) <- solve_tail entry in_fact fuel
523 -- last_outs contains a mix of internal facts, which
524 -- are inputs to 'run', and external facts, which
525 -- are going to be forgotten by 'run'
526 ; set_or_save last_outs
527 ; fuel <- run "forward" name set_successor_facts blocks fuel
528 ; set_or_save last_outs
529 -- Re-set facts that may have been forgotten by run
533 -- The need for both k1 and k2 suggests that maybe there's an opportunity
534 -- for improvement here -- in most cases, they're the same...
535 rec_rewrite rewritten analyzed finish k1 k2 in' fuel =
536 case check_maybe fuel rewritten of -- fr_first rewrites id idfact of
537 Nothing -> k1 analyzed fuel
538 Just g -> do g <- areturn g
539 (a, fuel) <- subAnalysis' $
541 RewriteDeep -> solve finish in' g (oneLessFuel fuel)
542 RewriteShallow -> do { a <- anal_f finish in' g
543 ; return (a, oneLessFuel fuel) }
545 solve_tail (G.ZTail m t) in' fuel =
546 rec_rewrite (fr_middle rewrites m in') (ft_middle_out transfers m in')
547 getExitFact (solve_tail t) (solve_tail t) in' fuel
548 solve_tail (G.ZLast (LastOther l)) in' fuel =
549 rec_rewrite (fr_last rewrites l in') (ft_last_outs transfers l in')
550 lastOutFacts k k in' fuel
551 where k a b = return (a, b)
552 solve_tail (G.ZLast LastExit) in' fuel =
553 rec_rewrite (fr_exit rewrites in') (ft_exit_out transfers in')
554 lastOutFacts k (\a b -> return (a, b)) in' fuel
555 where k a fuel = do { setExitFact a ; return (LastOutFacts [], fuel) }
557 fixed_point in_fact g fuel =
558 do { setAllFacts start_facts
559 ; (a, fuel) <- solve getExitFact in_fact g fuel
560 ; facts <- getAllFacts
561 ; last_outs <- lastOutFacts
562 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
563 ; let fp = FFP cfp last_outs
571 mk_set_or_save :: (DataflowAnalysis df, Monad (df a), Outputable a) =>
572 (BlockId -> Bool) -> LastOutFacts a -> df a ()
573 mk_set_or_save is_local (LastOutFacts l) = mapM_ set_or_save_one l
574 where set_or_save_one (id, a) =
575 if is_local id then setFact id a else pprTrace "addLastOutFact" (ppr $ length l) $ addLastOutFact (id, a)
581 (DebugNodes m l, LastNode l, Outputable a)
582 => (forall a . Fuel -> Maybe a -> Maybe a)
586 -> ForwardTransfers m l a
587 -> ForwardRewrites m l a
591 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
592 forward_rew check_maybe = forw
594 solve = forward_sol check_maybe
595 forw :: RewritingDepth
598 -> ForwardTransfers m l a
599 -> ForwardRewrites m l a
603 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
604 forw depth xstart_facts name transfers rewrites in_factx gx fuelx =
605 let rewrite :: BlockEnv a -> DFM a b
606 -> a -> Graph m l -> Fuel
607 -> DFM a (b, Graph m l, Fuel)
608 rewrite start finish in_fact g fuel =
609 in_fact `seq` g `seq`
610 let Graph entry blockenv = g
611 blocks = G.postorder_dfs_from blockenv entry
612 in do { solve depth name start transfers rewrites in_fact g fuel
613 ; eid <- freshBlockId "temporary entry id"
614 ; (rewritten, fuel) <-
615 rew_tail (ZFirst eid) in_fact entry emptyBlockEnv fuel
616 ; (rewritten, fuel) <- rewrite_blocks blocks rewritten fuel
618 ; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
620 don't_rewrite facts finish in_fact g fuel =
621 do { solve depth name facts transfers rewrites in_fact g fuel
623 ; return (a, g, fuel)
625 inner_rew :: DFM a f -> a -> Graph m l -> Fuel -> DFM a (f, Graph m l, Fuel)
626 inner_rew f i g fu = getAllFacts >>= \facts -> inner_rew' facts f i g fu
627 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
628 RewriteDeep -> rewrite
630 do { (a, g, fuel) <- rewrite xstart_facts getExitFact in_factx gx fuelx
631 ; facts <- getAllFacts
632 ; changed <- graphWasRewritten
633 ; last_outs <- lastOutFacts
634 ; let cfp = FP facts a changed (panic "no decoration?!") g
635 ; let fp = FFP cfp last_outs
638 -- JD: WHY AREN'T WE TAKING ANY FUEL HERE?
639 rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
640 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
641 rewrite_blocks [] rewritten fuel = return (rewritten, fuel)
642 rewrite_blocks (G.Block id t : bs) rewritten fuel =
645 case check_maybe fuel $ fr_first rewrites id a of
646 Nothing -> do { (rewritten, fuel) <-
647 rew_tail h (ft_first_out transfers id a)
649 ; rewrite_blocks bs rewritten fuel }
650 Just g -> do { markGraphRewritten
652 ; (outfact, g, fuel) <- inner_rew getExitFact a g fuel
653 ; let (blocks, h) = splice_head' h g
654 ; (rewritten, fuel) <-
655 rew_tail h outfact t (blocks `plusBlockEnv` rewritten) fuel
656 ; rewrite_blocks bs rewritten fuel }
658 rew_tail head in' (G.ZTail m t) rewritten fuel =
659 in' `seq` rewritten `seq`
660 my_trace "Rewriting middle node" (ppr m) $
661 case check_maybe fuel $ fr_middle rewrites m in' of
662 Nothing -> rew_tail (G.ZHead head m) (ft_middle_out transfers m in') t
664 Just g -> do { markGraphRewritten
666 ; (a, g, fuel) <- inner_rew getExitFact in' g fuel
667 ; let (blocks, h) = G.splice_head' head g
668 ; rew_tail h a t (blocks `plusBlockEnv` rewritten) fuel
670 rew_tail h in' (G.ZLast l) rewritten fuel =
671 in' `seq` rewritten `seq`
672 my_trace "Rewriting last node" (ppr l) $
673 case check_maybe fuel $ either_last rewrites in' l of
674 Nothing -> do check_facts in' l
675 return (insertBlock (zipht h (G.ZLast l)) rewritten, fuel)
676 Just g -> do { markGraphRewritten
679 my_trace "Just" (ppr g) $ inner_rew (return ()) in' g fuel
680 ; let g' = G.splice_head_only' h g
681 ; return (G.lg_blocks g' `plusBlockEnv` rewritten, fuel)
683 either_last rewrites in' (LastExit) = fr_exit rewrites in'
684 either_last rewrites in' (LastOther l) = fr_last rewrites l in'
685 check_facts in' (LastOther l) =
686 let LastOutFacts last_outs = ft_last_outs transfers l in'
687 in mapM (uncurry checkFactMatch) last_outs
688 check_facts _ LastExit = return []
691 lastOutFacts :: DFM f (LastOutFacts f)
692 lastOutFacts = bareLastOutFacts >>= return . LastOutFacts
694 {- ================================================================ -}
696 solve_b :: (DebugNodes m l, Outputable a)
697 => BlockEnv a -- initial facts (unbound == bottom)
699 -> DataflowLattice a -- lattice
700 -> BackwardTransfers m l a -- dataflow transfer functions
702 -> Graph m l -- graph to be analyzed
703 -> FuelMonad (BackwardFixedPoint m l a ()) -- answers
704 solve_b env name lattice transfers exit_fact g =
705 runDFM lattice $ bwd_pure_anal name env transfers g exit_fact
708 rewrite_b_agraph :: (DebugNodes m l, Outputable a)
713 -> BackwardTransfers m l a
714 -> BackwardRewrites m l a
715 -> a -- fact flowing in at exit
717 -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
718 rewrite_b_agraph depth start_facts name lattice transfers rewrites exit_fact g =
720 do fuel <- fuelRemaining
721 (fp, fuel') <- backward_rew maybeRewriteWithFuel depth start_facts name
722 transfers rewrites g exit_fact fuel
723 fuelDecrement name fuel fuel'
730 (DebugNodes m l, LastNode l, Outputable a)
731 => (forall a . Fuel -> Maybe a -> Maybe a)
735 -> BackwardTransfers m l a
736 -> BackwardRewrites m l a
740 -> DFM a (BackwardFixedPoint m l a (), Fuel)
741 backward_sol check_maybe = back
743 back :: RewritingDepth
746 -> BackwardTransfers m l a
747 -> BackwardRewrites m l a
751 -> DFM a (BackwardFixedPoint m l a (), Fuel)
752 back rewrite name start_facts transfers rewrites =
753 let anal_b :: Graph m l -> a -> DFM a a
755 do { fp <- bwd_pure_anal name emptyBlockEnv transfers g out
756 ; return $ zdfFpOutputFact fp }
758 subsolve :: AGraph m l -> a -> Fuel -> DFM a (a, Fuel)
761 RewriteDeep -> \g a fuel ->
762 subAnalysis' $ do { g <- areturn g; solve g a (oneLessFuel fuel) }
763 RewriteShallow -> \g a fuel ->
764 subAnalysis' $ do { g <- areturn g; a <- anal_b g a
765 ; return (a, oneLessFuel fuel) }
767 solve :: Graph m l -> a -> Fuel -> DFM a (a, Fuel)
768 solve (Graph entry blockenv) exit_fact fuel =
769 let blocks = reverse $ G.postorder_dfs_from blockenv entry
770 last_in _env (LastExit) = exit_fact
771 last_in env (LastOther l) = bt_last_in transfers l env
772 last_rew _env (LastExit) = br_exit rewrites
773 last_rew env (LastOther l) = br_last rewrites l env
774 set_block_fact block fuel =
775 let (h, l) = G.goto_end (G.unzip block) in
778 case check_maybe fuel $ last_rew env l of
779 Nothing -> return (last_in env l, fuel)
780 Just g -> do g' <- areturn g
781 my_trace "analysis rewrites last node"
782 (ppr l <+> pprGraph g') $
783 subsolve g exit_fact fuel
784 ; set_head_fact h a fuel
787 in do { fuel <- run "backward" name set_block_fact blocks fuel
788 ; eid <- freshBlockId "temporary entry id"
789 ; fuel <- set_block_fact (Block eid entry) fuel
795 set_head_fact (G.ZFirst id) a fuel =
796 case check_maybe fuel $ br_first rewrites id a of
797 Nothing -> do { my_trace "set_head_fact" (ppr id <+> text "=" <+>
798 ppr (bt_first_in transfers id a)) $
799 setFact id $ bt_first_in transfers id a
801 Just g -> do { g' <- areturn g
802 ; (a, fuel) <- my_trace "analysis rewrites first node"
803 (ppr id <+> pprGraph g') $
805 ; setFact id $ bt_first_in transfers id a
808 set_head_fact (G.ZHead h m) a fuel =
809 case check_maybe fuel $ br_middle rewrites m a of
810 Nothing -> set_head_fact h (bt_middle_in transfers m a) fuel
811 Just g -> do { g' <- areturn g
812 ; (a, fuel) <- my_trace "analysis rewrites middle node"
813 (ppr m <+> pprGraph g') $
815 ; set_head_fact h a fuel }
817 fixed_point g exit_fact fuel =
818 do { setAllFacts start_facts
819 ; (a, fuel) <- solve g exit_fact fuel
820 ; facts <- getAllFacts
821 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
826 bwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
829 -> BackwardTransfers m l a
832 -> DFM a (BackwardFixedPoint m l a ())
834 bwd_pure_anal name env transfers g exit_fact =
835 do (fp, _) <- anal_b name env transfers panic_rewrites g exit_fact panic_fuel
837 where -- another case of "I love lazy evaluation"
838 anal_b = backward_sol (\_ _ -> Nothing) panic_depth
839 panic_rewrites = panic "pure analysis asked for a rewrite function"
840 panic_fuel = panic "pure analysis asked for fuel"
841 panic_depth = panic "pure analysis asked for a rewrite depth"
844 {- ================================================================ -}
848 (DebugNodes m l, LastNode l, Outputable a)
849 => (forall a . Fuel -> Maybe a -> Maybe a)
853 -> BackwardTransfers m l a
854 -> BackwardRewrites m l a
858 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
859 backward_rew check_maybe = back
861 solve = backward_sol check_maybe
862 back :: RewritingDepth
865 -> BackwardTransfers m l a
866 -> BackwardRewrites m l a
870 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
871 back depth xstart_facts name transfers rewrites gx exit_fact fuelx =
872 let rewrite :: BlockEnv a
873 -> Graph m l -> a -> Fuel
874 -> DFM a (a, Graph m l, Fuel)
875 rewrite start g exit_fact fuel =
876 let Graph entry blockenv = g
877 blocks = reverse $ G.postorder_dfs_from blockenv entry
878 in do { (FP _ in_fact _ _ _, _) <- -- don't drop the entry fact!
879 solve depth name start transfers rewrites g exit_fact fuel
880 --; env <- getAllFacts
881 -- ; my_trace "facts after solving" (ppr env) $ return ()
882 ; eid <- freshBlockId "temporary entry id"
883 ; (rewritten, fuel) <- rewrite_blocks True blocks emptyBlockEnv fuel
884 -- We can't have the fact check fail on the bogus entry, which _may_ change
885 ; (rewritten, fuel) <-
886 rewrite_blocks False [Block eid entry] rewritten fuel
887 ; my_trace "eid" (ppr eid) $ return ()
888 ; my_trace "exit_fact" (ppr exit_fact) $ return ()
889 ; my_trace "in_fact" (ppr in_fact) $ return ()
890 ; return (in_fact, lgraphToGraph (LGraph eid rewritten), fuel)
891 } -- Remember: the entry fact computed by @solve@ accounts for rewriting
892 don't_rewrite facts g exit_fact fuel =
894 solve depth name facts transfers rewrites g exit_fact fuel
895 ; return (zdfFpOutputFact fp, g, fuel) }
896 inner_rew :: Graph m l -> a -> Fuel -> DFM a (a, Graph m l, Fuel)
897 inner_rew g a f = getAllFacts >>= \facts -> inner_rew' facts g a f
898 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
899 RewriteDeep -> rewrite
901 do { (a, g, fuel) <- rewrite xstart_facts gx exit_fact fuelx
902 ; facts <- getAllFacts
903 ; changed <- graphWasRewritten
904 ; let fp = FP facts a changed (panic "no decoration?!") g
907 rewrite_blocks :: Bool -> [Block m l] -> (BlockEnv (Block m l))
908 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
909 rewrite_blocks check bs rewritten fuel =
911 ; let rew [] r f = return (r, f)
913 do { (r, f) <- rewrite_block check env b r f; rew bs r f }
914 ; rew bs rewritten fuel }
915 rewrite_block check env b rewritten fuel =
916 let (h, l) = G.goto_end (G.unzip b) in
917 case maybeRewriteWithFuel fuel $ either_last env l of
918 Nothing -> propagate check fuel h (last_in env l) (ZLast l) rewritten
920 do { markGraphRewritten
922 ; (a, g, fuel) <- inner_rew g exit_fact fuel
923 ; let G.Graph t new_blocks = g
924 ; let rewritten' = new_blocks `plusBlockEnv` rewritten
925 ; propagate check fuel h a t rewritten' -- continue at entry of g
927 either_last _env (LastExit) = br_exit rewrites
928 either_last env (LastOther l) = br_last rewrites l env
929 last_in _env (LastExit) = exit_fact
930 last_in env (LastOther l) = bt_last_in transfers l env
931 propagate check fuel (ZHead h m) a tail rewritten =
932 case maybeRewriteWithFuel fuel $ br_middle rewrites m a of
934 propagate check fuel h (bt_middle_in transfers m a) (ZTail m tail) rewritten
936 do { markGraphRewritten
938 ; my_trace "With Facts" (ppr a) $ return ()
939 ; my_trace " Rewrote middle node"
940 (f4sep [ppr m, text "to", pprGraph g]) $
942 ; (a, g, fuel) <- inner_rew g a fuel
943 ; let Graph t newblocks = G.splice_tail g tail
944 ; my_trace "propagating facts" (ppr a) $
945 propagate check fuel h a t (newblocks `plusBlockEnv` rewritten) }
946 propagate check fuel (ZFirst id) a tail rewritten =
947 case maybeRewriteWithFuel fuel $ br_first rewrites id a of
948 Nothing -> do { if check then
949 checkFactMatch id $ bt_first_in transfers id a
951 ; return (insertBlock (Block id tail) rewritten, fuel) }
953 do { markGraphRewritten
955 ; my_trace "Rewrote first node"
956 (f4sep [ppr id <> colon, text "to", pprGraph g]) $ return ()
957 ; (a, g, fuel) <- inner_rew g a fuel
958 ; if check then checkFactMatch id (bt_first_in transfers id a)
960 ; let Graph t newblocks = G.splice_tail g tail
961 ; let r = insertBlock (Block id t) (newblocks `plusBlockEnv` rewritten)
965 {- ================================================================ -}
967 instance FixedPoint CommonFixedPoint where
968 zdfFpFacts = fp_facts
969 zdfFpOutputFact = fp_out
970 zdfGraphChanged = fp_changed
971 zdfDecoratedGraph = fp_dec_graph
972 zdfFpContents = fp_contents
973 zdfFpMap f (FP fs out ch dg a) = FP fs out ch dg (f a)
975 instance FixedPoint ForwardFixedPoint where
976 zdfFpFacts = fp_facts . ffp_common
977 zdfFpOutputFact = fp_out . ffp_common
978 zdfGraphChanged = fp_changed . ffp_common
979 zdfDecoratedGraph = fp_dec_graph . ffp_common
980 zdfFpContents = fp_contents . ffp_common
981 zdfFpMap f (FFP fp los) = FFP (zdfFpMap f fp) los
987 my_trace :: String -> SDoc -> a -> a
988 my_trace = if dump_things then pprTrace else \_ _ a -> a
991 -- | Here's a function to run an action on blocks until we reach a fixed point.
992 run :: (Outputable a, DebugNodes m l) =>
993 String -> String -> (Block m l -> b -> DFM a b) -> [Block m l] -> b -> DFM a b
994 run dir name do_block blocks b =
995 do { show_blocks $ iterate (1::Int) }
997 -- N.B. Each iteration starts with the same transaction limit;
998 -- only the rewrites in the final iteration actually count
999 trace_block (b, cnt) block =
1000 do b' <- my_trace "about to do" (text name <+> text "on" <+>
1001 ppr (blockId block) <+> ppr cnt) $
1003 return (b', cnt + 1)
1005 do { forgetLastOutFacts
1006 ; markFactsUnchanged
1007 ; (b, _) <- foldM trace_block (b, 0 :: Int) blocks
1008 ; changed <- factsStatus
1009 ; facts <- getAllFacts
1010 ; let depth = 0 -- was nesting depth
1013 NoChange -> unchanged depth $ return b
1015 pprFacts depth n facts $
1016 if n < 1000 then iterate (n+1)
1019 msg n = concat [name, " didn't converge in ", show n, " " , dir,
1021 my_nest depth sdoc = my_trace "" $ nest (3*depth) sdoc
1022 ppIter depth n = my_nest depth (empty $$ text "*************** iteration" <+> pp_i n)
1023 pp_i n = int n <+> text "of" <+> text name <+> text "on" <+> graphId
1025 my_nest depth (text "facts for" <+> graphId <+> text "are unchanged")
1027 graphId = case blocks of { Block id _ : _ -> ppr id ; [] -> text "<empty>" }
1028 show_blocks = my_trace "Blocks:" (vcat (map pprBlock blocks))
1029 pprBlock (Block id t) = nest 2 (pprFact (id, t))
1030 pprFacts depth n env =
1031 my_nest depth (text "facts for iteration" <+> pp_i n <+> text "are:" $$
1032 (nest 2 $ vcat $ map pprFact $ blockEnvToList env))
1033 pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)
1036 f4sep :: [SDoc] -> SDoc
1038 f4sep (d:ds) = fsep (d : map (nest 4) ds)
1041 subAnalysis' :: (Monad (m f), DataflowAnalysis m, Outputable f) =>
1044 do { a <- subAnalysis $
1045 do { a <- m; -- facts <- getAllFacts
1046 ; -- my_trace "after sub-analysis facts are" (pprFacts facts) $
1048 -- ; facts <- getAllFacts
1049 ; -- my_trace "in parent analysis facts are" (pprFacts facts) $
1051 -- where pprFacts env = nest 2 $ vcat $ map pprFact $ blockEnvToList env
1052 -- pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)