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
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 name, 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, which has been mercifully deleted.
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 :: BlockId -> a -> a
124 , bt_middle_in :: middle -> a -> a
125 , bt_last_in :: last -> (BlockId -> a) -> 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 :: BlockId -> a -> a
135 , ft_middle_out :: middle -> a -> a
136 , ft_last_outs :: last -> a -> 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.
149 data BackwardRewrites middle last a = BackwardRewrites
150 { br_first :: BlockId -> a -> Maybe (AGraph middle last)
151 , br_middle :: middle -> a -> Maybe (AGraph middle last)
152 , br_last :: last -> (BlockId -> a) -> Maybe (AGraph middle last)
153 , br_exit :: Maybe (AGraph middle last)
156 -- | A forward rewrite takes the same inputs as a forward transfer,
157 -- but instead of producing a fact, it produces a replacement graph or Nothing.
159 data ForwardRewrites middle last a = ForwardRewrites
160 { fr_first :: BlockId -> a -> Maybe (AGraph middle last)
161 , fr_middle :: middle -> a -> Maybe (AGraph middle last)
162 , fr_last :: last -> a -> Maybe (AGraph middle last)
163 , fr_exit :: a -> Maybe (AGraph middle last)
166 {- ===================== FIXED POINTS =================== -}
168 -- | The result of combined analysis and transformation is a
169 -- solution to the set of dataflow equations together with a 'contained value'.
170 -- This solution is a member of type class 'FixedPoint', which is parameterized by
171 -- * middle and last nodes 'm' and 'l'
172 -- * data flow fact 'fact'
173 -- * the type 'a' of the contained value
175 -- In practice, the contained value 'zdfFpContents' is either a
176 -- rewritten graph, when rewriting, or (), when solving without
177 -- rewriting. A function 'zdfFpMap' allows a client to change
178 -- the contents without changing other values.
180 -- To save space, we provide the solution 'zdfFpFacts' as a mapping
181 -- from BlockId to fact; if necessary, facts on edges can be
182 -- reconstructed using the transfer functions; this functionality is
183 -- intended to be included as the 'zdfDecoratedGraph', but the code
184 -- has not yet been implemented.
186 -- The solution may also includes a fact 'zdfFpOuputFact', which is
187 -- not associated with any label:
188 -- * for a backward problem, this is the fact at entry
189 -- * for a forward problem, this is the fact at the distinguished exit node,
190 -- if such a node is present
192 -- For a forward problem only, the solution includes 'zdfFpLastOuts',
193 -- which is the set of facts on edges leaving the graph.
195 -- The flag 'zdfGraphChanged' tells whether the engine did any rewriting.
197 class FixedPoint fp where
198 zdfFpContents :: fp m l fact a -> a
199 zdfFpFacts :: fp m l fact a -> BlockEnv fact
200 zdfFpOutputFact :: fp m l fact a -> fact -- entry for backward; exit for forward
201 zdfDecoratedGraph :: fp m l fact a -> Graph (fact, m) (fact, l)
202 zdfGraphChanged :: fp m l fact a -> ChangeFlag
203 zdfFpMap :: (a -> b) -> (fp m l fact a -> fp m l fact b)
205 -- | The class 'FixedPoint' has two instances: one for forward problems and
206 -- one for backward problems. The 'CommonFixedPoint' defines all fields
207 -- common to both. (The instance declarations are uninteresting and appear below.)
209 data CommonFixedPoint m l fact a = FP
210 { fp_facts :: BlockEnv fact
211 , fp_out :: fact -- entry for backward; exit for forward
212 , fp_changed :: ChangeFlag
213 , fp_dec_graph :: Graph (fact, m) (fact, l)
217 -- | The common fixed point is sufficient for a backward problem.
218 type BackwardFixedPoint = CommonFixedPoint
220 -- | A forward problem needs the common fields, plus the facts on the outedges.
221 data ForwardFixedPoint m l fact a = FFP
222 { ffp_common :: CommonFixedPoint m l fact a
223 , zdfFpLastOuts :: LastOutFacts fact
227 {- ============== SOLVING AND REWRITING ============== -}
229 type PassName = String
231 -- | 'zdfSolveFrom' is an overloaded name that resolves to a pure
232 -- analysis with no rewriting. It has only two instances: forward and
233 -- backward. Since it needs no rewrites, the type parameters of the
234 -- class are transfer functions and the fixed point.
237 -- An iterative solver normally starts with the bottom fact at every
238 -- node, but it can be useful in other contexts as well. For this
239 -- reason the initial set of facts (at labelled blocks only) is a
240 -- parameter to the solver.
242 -- The constraints on the type signature exist purely for debugging;
243 -- they make it possible to prettyprint nodes and facts. The parameter of
244 -- type 'PassName' is also used just for debugging.
246 -- Note that the result is a fixed point with no contents, that is,
247 -- the contents have type ().
249 -- The intent of the rest of the type signature should be obvious.
250 -- If not, place a skype call to norman-ramsey or complain bitterly
251 -- to <norman-ramsey@acm.org>.
253 class DataflowSolverDirection transfers fixedpt where
254 zdfSolveFrom :: (DebugNodes m l, Outputable a)
255 => BlockEnv a -- ^ Initial facts (unbound == bottom)
257 -> DataflowLattice a -- ^ Lattice
258 -> transfers m l a -- ^ Dataflow transfer functions
259 -> a -- ^ Fact flowing in (at entry or exit)
260 -> Graph m l -- ^ Graph to be analyzed
261 -> FuelMonad (fixedpt m l a ()) -- ^ Answers
262 zdfSolveFromL :: (DebugNodes m l, Outputable a)
263 => BlockEnv a -- Initial facts (unbound == bottom)
265 -> DataflowLattice a -- Lattice
266 -> transfers m l a -- Dataflow transfer functions
267 -> a -- Fact flowing in (at entry or exit)
268 -> LGraph m l -- Graph to be analyzed
269 -> FuelMonad (fixedpt m l a ()) -- Answers
270 zdfSolveFromL b p l t a g = zdfSolveFrom b p l t a $ quickGraph g
272 -- There are exactly two instances: forward and backward
273 instance DataflowSolverDirection ForwardTransfers ForwardFixedPoint
274 where zdfSolveFrom = solve_f
276 instance DataflowSolverDirection BackwardTransfers BackwardFixedPoint
277 where zdfSolveFrom = solve_b
280 -- | zdfRewriteFrom is an overloaded name that resolves to an
281 -- interleaved analysis and transformation. It too is instantiated in
282 -- forward and backward directions.
284 -- The type parameters of the class include not only transfer
285 -- functions and the fixed point but also rewrites.
287 -- The type signature of 'zdfRewriteFrom' is that of 'zdfSolveFrom'
288 -- with the rewrites and a rewriting depth as additional parameters,
289 -- as well as a different result, which contains a rewritten graph.
291 class DataflowSolverDirection transfers fixedpt =>
292 DataflowDirection transfers fixedpt rewrites where
293 zdfRewriteFrom :: (DebugNodes m l, Outputable a)
294 => RewritingDepth -- whether to rewrite a rewritten graph
295 -> BlockEnv a -- initial facts (unbound == bottom)
300 -> a -- fact flowing in (at entry or exit)
302 -> FuelMonad (fixedpt m l a (Graph m l))
304 -- Temporarily lifting from Graph to LGraph -- an experiment to see how we
305 -- can eliminate some hysteresis between Graph and LGraph.
306 -- Perhaps Graph should be confined to dataflow code.
307 -- Trading space for time
308 quickGraph :: LastNode l => LGraph m l -> Graph m l
309 quickGraph g = Graph (ZLast $ mkBranchNode $ lg_entry g) $ lg_blocks g
311 quickLGraph :: LastNode l => Graph m l -> FuelMonad (LGraph m l)
312 quickLGraph (Graph (ZLast (LastOther l)) blockenv)
313 | isBranchNode l = return $ LGraph (branchNodeTarget l) blockenv
314 quickLGraph g = F.lGraphOfGraph g
316 fixptWithLGraph :: LastNode l => CommonFixedPoint m l fact (Graph m l) ->
317 FuelMonad (CommonFixedPoint m l fact (LGraph m l))
318 fixptWithLGraph cfp =
319 do fp_c <- quickLGraph $ fp_contents cfp
320 return $ cfp {fp_contents = fp_c}
322 ffixptWithLGraph :: LastNode l => ForwardFixedPoint m l fact (Graph m l) ->
323 FuelMonad (ForwardFixedPoint m l fact (LGraph m l))
324 ffixptWithLGraph fp =
325 do common <- fixptWithLGraph $ ffp_common fp
326 return $ fp {ffp_common = common}
328 zdfFRewriteFromL :: (DebugNodes m l, Outputable a)
329 => RewritingDepth -- whether to rewrite a rewritten graph
330 -> BlockEnv a -- initial facts (unbound == bottom)
333 -> ForwardTransfers m l a
334 -> ForwardRewrites m l a
335 -> a -- fact flowing in (at entry or exit)
337 -> FuelMonad (ForwardFixedPoint m l a (LGraph m l))
338 zdfFRewriteFromL d b p l t r a g@(LGraph _ _) =
339 do fp <- zdfRewriteFrom d b p l t r a $ quickGraph g
342 zdfBRewriteFromL :: (DebugNodes m l, Outputable a)
343 => RewritingDepth -- whether to rewrite a rewritten graph
344 -> BlockEnv a -- initial facts (unbound == bottom)
347 -> BackwardTransfers m l a
348 -> BackwardRewrites m l a
349 -> a -- fact flowing in (at entry or exit)
351 -> FuelMonad (BackwardFixedPoint m l a (LGraph m l))
352 zdfBRewriteFromL d b p l t r a g@(LGraph _ _) =
353 do fp <- zdfRewriteFrom d b p l t r a $ quickGraph g
357 data RewritingDepth = RewriteShallow | RewriteDeep
358 -- When a transformation proposes to rewrite a node,
359 -- you can either ask the system to
360 -- * "shallow": accept the new graph, analyse it without further rewriting
361 -- * "deep": recursively analyse-and-rewrite the new graph
364 -- There are currently four instances, but there could be more
365 -- forward, backward (instantiates transfers, fixedpt, rewrites)
366 -- Graph, AGraph (instantiates graph)
368 instance DataflowDirection ForwardTransfers ForwardFixedPoint ForwardRewrites
369 where zdfRewriteFrom = rewrite_f_agraph
371 instance DataflowDirection BackwardTransfers BackwardFixedPoint BackwardRewrites
372 where zdfRewriteFrom = rewrite_b_agraph
375 {- =================== IMPLEMENTATIONS ===================== -}
378 -----------------------------------------------------------
379 -- solve_f: forward, pure
381 solve_f :: (DebugNodes m l, Outputable a)
382 => BlockEnv a -- initial facts (unbound == bottom)
384 -> DataflowLattice a -- lattice
385 -> ForwardTransfers m l a -- dataflow transfer functions
387 -> Graph m l -- graph to be analyzed
388 -> FuelMonad (ForwardFixedPoint m l a ()) -- answers
389 solve_f env name lattice transfers in_fact g =
390 runDFM lattice $ fwd_pure_anal name env transfers in_fact g
392 rewrite_f_agraph :: (DebugNodes m l, Outputable a)
397 -> ForwardTransfers m l a
398 -> ForwardRewrites m l a
399 -> a -- fact flowing in (at entry or exit)
401 -> FuelMonad (ForwardFixedPoint m l a (Graph m l))
402 rewrite_f_agraph depth start_facts name lattice transfers rewrites in_fact g =
404 do fuel <- fuelRemaining
405 (fp, fuel') <- forward_rew maybeRewriteWithFuel depth start_facts name
406 transfers rewrites in_fact g fuel
407 fuelDecrement name fuel fuel'
410 areturn :: AGraph m l -> DFM a (Graph m l)
411 areturn g = liftToDFM $ liftUniq $ graphOfAGraph g
413 -- | Here we prefer not simply to slap on 'goto eid' because this
414 -- introduces an unnecessary basic block at each rewrite, and we don't
415 -- want to stress out the finite map more than necessary
416 lgraphToGraph :: LastNode l => LGraph m l -> Graph m l
417 lgraphToGraph (LGraph eid blocks) =
418 if flip any (eltsBlockEnv blocks) $ \block -> any (== eid) (succs block) then
419 Graph (ZLast (mkBranchNode eid)) blocks
420 else -- common case: entry is not a branch target
421 let Block _ entry = lookupBlockEnv blocks eid `orElse` panic "missing entry!"
422 in Graph entry (delFromBlockEnv blocks eid)
425 class (Outputable m, Outputable l, LastNode l, Outputable (LGraph m l)) => DebugNodes m l
427 fwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
430 -> ForwardTransfers m l a
433 -> DFM a (ForwardFixedPoint m l a ())
435 fwd_pure_anal name env transfers in_fact g =
436 do (fp, _) <- anal_f name env transfers panic_rewrites in_fact g panic_fuel
438 where -- definitely a case of "I love lazy evaluation"
439 anal_f = forward_sol (\_ _ -> Nothing) panic_depth
440 panic_rewrites = panic "pure analysis asked for a rewrite function"
441 panic_fuel = panic "pure analysis asked for fuel"
442 panic_depth = panic "pure analysis asked for a rewrite depth"
444 -----------------------------------------------------------------------
446 -- Here beginneth the super-general functions
448 -- Think of them as (typechecked) macros
449 -- * They are not exported
451 -- * They are called by the specialised wrappers
452 -- above, and always inlined into their callers
454 -- There are four functions, one for each combination of:
458 -- A "solver" produces a (DFM f (f, Fuel)),
459 -- where f is the fact at entry(Bwd)/exit(Fwd)
460 -- and from the DFM you can extract
465 -- A "rewriter" produces a rewritten *Graph* as well
467 -- Both constrain their rewrites by
469 -- b) RewritingDepth: shallow/deep
471 -----------------------------------------------------------------------
473 type Fuel = OptimizationFuel
477 (DebugNodes m l, LastNode l, Outputable a)
478 => (forall a . Fuel -> Maybe a -> Maybe a)
479 -- Squashes proposed rewrites if there is
480 -- no more fuel; OR if we are doing a pure
481 -- analysis, so totally ignore the rewrite
482 -- ie. For pure-analysis the fn is (\_ _ -> Nothing)
483 -> RewritingDepth -- Shallow/deep
485 -> BlockEnv a -- Initial set of facts
486 -> ForwardTransfers m l a
487 -> ForwardRewrites m l a
491 -> DFM a (ForwardFixedPoint m l a (), Fuel)
492 forward_sol check_maybe = forw
494 forw :: RewritingDepth
497 -> ForwardTransfers m l a
498 -> ForwardRewrites m l a
502 -> DFM a (ForwardFixedPoint m l a (), Fuel)
503 forw rewrite name start_facts transfers rewrites =
504 let anal_f :: DFM a b -> a -> Graph m l -> DFM a b
505 anal_f finish in' g =
506 do { _ <- fwd_pure_anal name emptyBlockEnv transfers in' g; finish }
508 solve :: DFM a b -> a -> Graph m l -> Fuel -> DFM a (b, Fuel)
509 solve finish in_fact (Graph entry blockenv) fuel =
510 let blocks = G.postorder_dfs_from blockenv entry
511 set_or_save = mk_set_or_save (isJust . lookupBlockEnv blockenv)
512 set_successor_facts (Block id tail) fuel =
513 do { idfact <- getFact id
514 ; (last_outs, fuel) <- rec_rewrite (fr_first rewrites id idfact)
515 (ft_first_out transfers id idfact)
516 getExitFact (solve_tail tail)
517 (solve_tail tail) idfact fuel
518 ; set_or_save last_outs
520 in do { (last_outs, fuel) <- solve_tail entry in_fact fuel
521 -- last_outs contains a mix of internal facts, which
522 -- are inputs to 'run', and external facts, which
523 -- are going to be forgotten by 'run'
524 ; set_or_save last_outs
525 ; fuel <- run "forward" name set_successor_facts blocks fuel
526 ; set_or_save last_outs
527 -- Re-set facts that may have been forgotten by run
531 -- The need for both k1 and k2 suggests that maybe there's an opportunity
532 -- for improvement here -- in most cases, they're the same...
533 rec_rewrite rewritten analyzed finish k1 k2 in' fuel =
534 case check_maybe fuel rewritten of -- fr_first rewrites id idfact of
535 Nothing -> k1 analyzed fuel
536 Just g -> do g <- areturn g
537 (a, fuel) <- subAnalysis' $
539 RewriteDeep -> solve finish in' g (oneLessFuel fuel)
540 RewriteShallow -> do { a <- anal_f finish in' g
541 ; return (a, oneLessFuel fuel) }
543 solve_tail (G.ZTail m t) in' fuel =
544 rec_rewrite (fr_middle rewrites m in') (ft_middle_out transfers m in')
545 getExitFact (solve_tail t) (solve_tail t) in' fuel
546 solve_tail (G.ZLast (LastOther l)) in' fuel =
547 rec_rewrite (fr_last rewrites l in') (ft_last_outs transfers l in')
548 lastOutFacts k k in' fuel
549 where k a b = return (a, b)
550 solve_tail (G.ZLast LastExit) in' fuel =
551 rec_rewrite (fr_exit rewrites in') (ft_exit_out transfers in')
552 lastOutFacts k (\a b -> return (a, b)) in' fuel
553 where k a fuel = do { setExitFact a ; return (LastOutFacts [], fuel) }
555 fixed_point in_fact g fuel =
556 do { setAllFacts start_facts
557 ; (a, fuel) <- solve getExitFact in_fact g fuel
558 ; facts <- getAllFacts
559 ; last_outs <- lastOutFacts
560 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
561 ; let fp = FFP cfp last_outs
569 mk_set_or_save :: (DataflowAnalysis df, Monad (df a), Outputable a) =>
570 (BlockId -> Bool) -> LastOutFacts a -> df a ()
571 mk_set_or_save is_local (LastOutFacts l) = mapM_ set_or_save_one l
572 where set_or_save_one (id, a) =
573 if is_local id then setFact id a else pprTrace "addLastOutFact" (ppr $ length l) $ addLastOutFact (id, a)
579 (DebugNodes m l, LastNode l, Outputable a)
580 => (forall a . Fuel -> Maybe a -> Maybe a)
584 -> ForwardTransfers m l a
585 -> ForwardRewrites m l a
589 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
590 forward_rew check_maybe = forw
592 solve = forward_sol check_maybe
593 forw :: RewritingDepth
596 -> ForwardTransfers m l a
597 -> ForwardRewrites m l a
601 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
602 forw depth xstart_facts name transfers rewrites in_factx gx fuelx =
603 let rewrite :: BlockEnv a -> DFM a b
604 -> a -> Graph m l -> Fuel
605 -> DFM a (b, Graph m l, Fuel)
606 rewrite start finish in_fact g fuel =
607 in_fact `seq` g `seq`
608 let Graph entry blockenv = g
609 blocks = G.postorder_dfs_from blockenv entry
610 in do { _ <- solve depth name start transfers rewrites in_fact g fuel
611 ; eid <- freshBlockId "temporary entry id"
612 ; (rewritten, fuel) <-
613 rew_tail (ZFirst eid) in_fact entry emptyBlockEnv fuel
614 ; (rewritten, fuel) <- rewrite_blocks blocks rewritten fuel
616 ; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
618 don't_rewrite facts finish in_fact g fuel =
619 do { _ <- solve depth name facts transfers rewrites in_fact g fuel
621 ; return (a, g, fuel)
623 inner_rew :: DFM a f -> a -> Graph m l -> Fuel -> DFM a (f, Graph m l, Fuel)
624 inner_rew f i g fu = getAllFacts >>= \facts -> inner_rew' facts f i g fu
625 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
626 RewriteDeep -> rewrite
628 do { (a, g, fuel) <- rewrite xstart_facts getExitFact in_factx gx fuelx
629 ; facts <- getAllFacts
630 ; changed <- graphWasRewritten
631 ; last_outs <- lastOutFacts
632 ; let cfp = FP facts a changed (panic "no decoration?!") g
633 ; let fp = FFP cfp last_outs
636 -- JD: WHY AREN'T WE TAKING ANY FUEL HERE?
637 rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
638 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
639 rewrite_blocks [] rewritten fuel = return (rewritten, fuel)
640 rewrite_blocks (G.Block id t : bs) rewritten fuel =
643 case check_maybe fuel $ fr_first rewrites id a of
644 Nothing -> do { (rewritten, fuel) <-
645 rew_tail h (ft_first_out transfers id a)
647 ; rewrite_blocks bs rewritten fuel }
648 Just g -> do { markGraphRewritten
650 ; (outfact, g, fuel) <- inner_rew getExitFact a g fuel
651 ; let (blocks, h) = splice_head' h g
652 ; (rewritten, fuel) <-
653 rew_tail h outfact t (blocks `plusBlockEnv` rewritten) fuel
654 ; rewrite_blocks bs rewritten fuel }
656 rew_tail head in' (G.ZTail m t) rewritten fuel =
657 in' `seq` rewritten `seq`
658 my_trace "Rewriting middle node" (ppr m) $
659 case check_maybe fuel $ fr_middle rewrites m in' of
660 Nothing -> rew_tail (G.ZHead head m) (ft_middle_out transfers m in') t
662 Just g -> do { markGraphRewritten
664 ; (a, g, fuel) <- inner_rew getExitFact in' g fuel
665 ; let (blocks, h) = G.splice_head' head g
666 ; rew_tail h a t (blocks `plusBlockEnv` rewritten) fuel
668 rew_tail h in' (G.ZLast l) rewritten fuel =
669 in' `seq` rewritten `seq`
670 my_trace "Rewriting last node" (ppr l) $
671 case check_maybe fuel $ either_last rewrites in' l of
672 Nothing -> do check_facts in' l
673 return (insertBlock (zipht h (G.ZLast l)) rewritten, fuel)
674 Just g -> do { markGraphRewritten
677 my_trace "Just" (ppr g) $ inner_rew (return ()) in' g fuel
678 ; let g' = G.splice_head_only' h g
679 ; return (G.lg_blocks g' `plusBlockEnv` rewritten, fuel)
681 either_last rewrites in' (LastExit) = fr_exit rewrites in'
682 either_last rewrites in' (LastOther l) = fr_last rewrites l in'
683 check_facts in' (LastOther l) =
684 let LastOutFacts last_outs = ft_last_outs transfers l in'
685 in mapM_ (uncurry checkFactMatch) last_outs
686 check_facts _ LastExit = return ()
689 lastOutFacts :: DFM f (LastOutFacts f)
690 lastOutFacts = bareLastOutFacts >>= return . LastOutFacts
692 {- ================================================================ -}
694 solve_b :: (DebugNodes m l, Outputable a)
695 => BlockEnv a -- initial facts (unbound == bottom)
697 -> DataflowLattice a -- lattice
698 -> BackwardTransfers m l a -- dataflow transfer functions
700 -> Graph m l -- graph to be analyzed
701 -> FuelMonad (BackwardFixedPoint m l a ()) -- answers
702 solve_b env name lattice transfers exit_fact g =
703 runDFM lattice $ bwd_pure_anal name env transfers g exit_fact
706 rewrite_b_agraph :: (DebugNodes m l, Outputable a)
711 -> BackwardTransfers m l a
712 -> BackwardRewrites m l a
713 -> a -- fact flowing in at exit
715 -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
716 rewrite_b_agraph depth start_facts name lattice transfers rewrites exit_fact g =
718 do fuel <- fuelRemaining
719 (fp, fuel') <- backward_rew maybeRewriteWithFuel depth start_facts name
720 transfers rewrites g exit_fact fuel
721 fuelDecrement name fuel fuel'
728 (DebugNodes m l, LastNode l, Outputable a)
729 => (forall a . Fuel -> Maybe a -> Maybe a)
733 -> BackwardTransfers m l a
734 -> BackwardRewrites m l a
738 -> DFM a (BackwardFixedPoint m l a (), Fuel)
739 backward_sol check_maybe = back
741 back :: RewritingDepth
744 -> BackwardTransfers m l a
745 -> BackwardRewrites m l a
749 -> DFM a (BackwardFixedPoint m l a (), Fuel)
750 back rewrite name start_facts transfers rewrites =
751 let anal_b :: Graph m l -> a -> DFM a a
753 do { fp <- bwd_pure_anal name emptyBlockEnv transfers g out
754 ; return $ zdfFpOutputFact fp }
756 subsolve :: AGraph m l -> a -> Fuel -> DFM a (a, Fuel)
759 RewriteDeep -> \g a fuel ->
760 subAnalysis' $ do { g <- areturn g; solve g a (oneLessFuel fuel) }
761 RewriteShallow -> \g a fuel ->
762 subAnalysis' $ do { g <- areturn g; a <- anal_b g a
763 ; return (a, oneLessFuel fuel) }
765 solve :: Graph m l -> a -> Fuel -> DFM a (a, Fuel)
766 solve (Graph entry blockenv) exit_fact fuel =
767 let blocks = reverse $ G.postorder_dfs_from blockenv entry
768 last_in _env (LastExit) = exit_fact
769 last_in env (LastOther l) = bt_last_in transfers l env
770 last_rew _env (LastExit) = br_exit rewrites
771 last_rew env (LastOther l) = br_last rewrites l env
772 set_block_fact block fuel =
773 let (h, l) = G.goto_end (G.unzip block) in
776 case check_maybe fuel $ last_rew env l of
777 Nothing -> return (last_in env l, fuel)
778 Just g -> do g' <- areturn g
779 my_trace "analysis rewrites last node"
780 (ppr l <+> pprGraph g') $
781 subsolve g exit_fact fuel
782 ; _ <- set_head_fact h a fuel
785 in do { fuel <- run "backward" name set_block_fact blocks fuel
786 ; eid <- freshBlockId "temporary entry id"
787 ; fuel <- set_block_fact (Block eid entry) fuel
793 set_head_fact (G.ZFirst id) a fuel =
794 case check_maybe fuel $ br_first rewrites id a of
795 Nothing -> do { my_trace "set_head_fact" (ppr id <+> text "=" <+>
796 ppr (bt_first_in transfers id a)) $
797 setFact id $ bt_first_in transfers id a
799 Just g -> do { g' <- areturn g
800 ; (a, fuel) <- my_trace "analysis rewrites first node"
801 (ppr id <+> pprGraph g') $
803 ; setFact id $ bt_first_in transfers id a
806 set_head_fact (G.ZHead h m) a fuel =
807 case check_maybe fuel $ br_middle rewrites m a of
808 Nothing -> set_head_fact h (bt_middle_in transfers m a) fuel
809 Just g -> do { g' <- areturn g
810 ; (a, fuel) <- my_trace "analysis rewrites middle node"
811 (ppr m <+> pprGraph g') $
813 ; set_head_fact h a fuel }
815 fixed_point g exit_fact fuel =
816 do { setAllFacts start_facts
817 ; (a, fuel) <- solve g exit_fact fuel
818 ; facts <- getAllFacts
819 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
824 bwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
827 -> BackwardTransfers m l a
830 -> DFM a (BackwardFixedPoint m l a ())
832 bwd_pure_anal name env transfers g exit_fact =
833 do (fp, _) <- anal_b name env transfers panic_rewrites g exit_fact panic_fuel
835 where -- another case of "I love lazy evaluation"
836 anal_b = backward_sol (\_ _ -> Nothing) panic_depth
837 panic_rewrites = panic "pure analysis asked for a rewrite function"
838 panic_fuel = panic "pure analysis asked for fuel"
839 panic_depth = panic "pure analysis asked for a rewrite depth"
842 {- ================================================================ -}
846 (DebugNodes m l, LastNode l, Outputable a)
847 => (forall a . Fuel -> Maybe a -> Maybe a)
851 -> BackwardTransfers m l a
852 -> BackwardRewrites m l a
856 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
857 backward_rew check_maybe = back
859 solve = backward_sol check_maybe
860 back :: RewritingDepth
863 -> BackwardTransfers m l a
864 -> BackwardRewrites m l a
868 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
869 back depth xstart_facts name transfers rewrites gx exit_fact fuelx =
870 let rewrite :: BlockEnv a
871 -> Graph m l -> a -> Fuel
872 -> DFM a (a, Graph m l, Fuel)
873 rewrite start g exit_fact fuel =
874 let Graph entry blockenv = g
875 blocks = reverse $ G.postorder_dfs_from blockenv entry
876 in do { (FP _ in_fact _ _ _, _) <- -- don't drop the entry fact!
877 solve depth name start transfers rewrites g exit_fact fuel
878 --; env <- getAllFacts
879 -- ; my_trace "facts after solving" (ppr env) $ return ()
880 ; eid <- freshBlockId "temporary entry id"
881 ; (rewritten, fuel) <- rewrite_blocks True blocks emptyBlockEnv fuel
882 -- We can't have the fact check fail on the bogus entry, which _may_ change
883 ; (rewritten, fuel) <-
884 rewrite_blocks False [Block eid entry] rewritten fuel
885 ; my_trace "eid" (ppr eid) $ return ()
886 ; my_trace "exit_fact" (ppr exit_fact) $ return ()
887 ; my_trace "in_fact" (ppr in_fact) $ return ()
888 ; return (in_fact, lgraphToGraph (LGraph eid rewritten), fuel)
889 } -- Remember: the entry fact computed by @solve@ accounts for rewriting
890 don't_rewrite facts g exit_fact fuel =
892 solve depth name facts transfers rewrites g exit_fact fuel
893 ; return (zdfFpOutputFact fp, g, fuel) }
894 inner_rew :: Graph m l -> a -> Fuel -> DFM a (a, Graph m l, Fuel)
895 inner_rew g a f = getAllFacts >>= \facts -> inner_rew' facts g a f
896 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
897 RewriteDeep -> rewrite
899 do { (a, g, fuel) <- rewrite xstart_facts gx exit_fact fuelx
900 ; facts <- getAllFacts
901 ; changed <- graphWasRewritten
902 ; let fp = FP facts a changed (panic "no decoration?!") g
905 rewrite_blocks :: Bool -> [Block m l] -> (BlockEnv (Block m l))
906 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
907 rewrite_blocks check bs rewritten fuel =
909 ; let rew [] r f = return (r, f)
911 do { (r, f) <- rewrite_block check env b r f; rew bs r f }
912 ; rew bs rewritten fuel }
913 rewrite_block check env b rewritten fuel =
914 let (h, l) = G.goto_end (G.unzip b) in
915 case maybeRewriteWithFuel fuel $ either_last env l of
916 Nothing -> propagate check fuel h (last_in env l) (ZLast l) rewritten
918 do { markGraphRewritten
920 ; (a, g, fuel) <- inner_rew g exit_fact fuel
921 ; let G.Graph t new_blocks = g
922 ; let rewritten' = new_blocks `plusBlockEnv` rewritten
923 ; propagate check fuel h a t rewritten' -- continue at entry of g
925 either_last _env (LastExit) = br_exit rewrites
926 either_last env (LastOther l) = br_last rewrites l env
927 last_in _env (LastExit) = exit_fact
928 last_in env (LastOther l) = bt_last_in transfers l env
929 propagate check fuel (ZHead h m) a tail rewritten =
930 case maybeRewriteWithFuel fuel $ br_middle rewrites m a of
932 propagate check fuel h (bt_middle_in transfers m a) (ZTail m tail) rewritten
934 do { markGraphRewritten
936 ; my_trace "With Facts" (ppr a) $ return ()
937 ; my_trace " Rewrote middle node"
938 (f4sep [ppr m, text "to", pprGraph g]) $
940 ; (a, g, fuel) <- inner_rew g a fuel
941 ; let Graph t newblocks = G.splice_tail g tail
942 ; my_trace "propagating facts" (ppr a) $
943 propagate check fuel h a t (newblocks `plusBlockEnv` rewritten) }
944 propagate check fuel (ZFirst id) a tail rewritten =
945 case maybeRewriteWithFuel fuel $ br_first rewrites id a of
946 Nothing -> do { if check then
947 checkFactMatch id $ bt_first_in transfers id a
949 ; return (insertBlock (Block id tail) rewritten, fuel) }
951 do { markGraphRewritten
953 ; my_trace "Rewrote first node"
954 (f4sep [ppr id <> colon, text "to", pprGraph g]) $ return ()
955 ; (a, g, fuel) <- inner_rew g a fuel
956 ; if check then checkFactMatch id (bt_first_in transfers id a)
958 ; let Graph t newblocks = G.splice_tail g tail
959 ; let r = insertBlock (Block id t) (newblocks `plusBlockEnv` rewritten)
963 {- ================================================================ -}
965 instance FixedPoint CommonFixedPoint where
966 zdfFpFacts = fp_facts
967 zdfFpOutputFact = fp_out
968 zdfGraphChanged = fp_changed
969 zdfDecoratedGraph = fp_dec_graph
970 zdfFpContents = fp_contents
971 zdfFpMap f (FP fs out ch dg a) = FP fs out ch dg (f a)
973 instance FixedPoint ForwardFixedPoint where
974 zdfFpFacts = fp_facts . ffp_common
975 zdfFpOutputFact = fp_out . ffp_common
976 zdfGraphChanged = fp_changed . ffp_common
977 zdfDecoratedGraph = fp_dec_graph . ffp_common
978 zdfFpContents = fp_contents . ffp_common
979 zdfFpMap f (FFP fp los) = FFP (zdfFpMap f fp) los
985 my_trace :: String -> SDoc -> a -> a
986 my_trace = if dump_things then pprTrace else \_ _ a -> a
989 -- | Here's a function to run an action on blocks until we reach a fixed point.
990 run :: (Outputable a, DebugNodes m l) =>
991 String -> String -> (Block m l -> b -> DFM a b) -> [Block m l] -> b -> DFM a b
992 run dir name do_block blocks b =
993 do { show_blocks $ iterate (1::Int) }
995 -- N.B. Each iteration starts with the same transaction limit;
996 -- only the rewrites in the final iteration actually count
997 trace_block (b, cnt) block =
998 do b' <- my_trace "about to do" (text name <+> text "on" <+>
999 ppr (blockId block) <+> ppr cnt) $
1001 return (b', cnt + 1)
1003 do { forgetLastOutFacts
1004 ; markFactsUnchanged
1005 ; (b, _) <- foldM trace_block (b, 0 :: Int) blocks
1006 ; changed <- factsStatus
1007 ; facts <- getAllFacts
1008 ; let depth = 0 -- was nesting depth
1011 NoChange -> unchanged depth $ return b
1013 pprFacts depth n facts $
1014 if n < 1000 then iterate (n+1)
1017 msg n = concat [name, " didn't converge in ", show n, " " , dir,
1019 my_nest depth sdoc = my_trace "" $ nest (3*depth) sdoc
1020 ppIter depth n = my_nest depth (empty $$ text "*************** iteration" <+> pp_i n)
1021 pp_i n = int n <+> text "of" <+> text name <+> text "on" <+> graphId
1023 my_nest depth (text "facts for" <+> graphId <+> text "are unchanged")
1025 graphId = case blocks of { Block id _ : _ -> ppr id ; [] -> text "<empty>" }
1026 show_blocks = my_trace "Blocks:" (vcat (map pprBlock blocks))
1027 pprBlock (Block id t) = nest 2 (pprFact (id, t))
1028 pprFacts depth n env =
1029 my_nest depth (text "facts for iteration" <+> pp_i n <+> text "are:" $$
1030 (nest 2 $ vcat $ map pprFact $ blockEnvToList env))
1031 pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)
1034 f4sep :: [SDoc] -> SDoc
1036 f4sep (d:ds) = fsep (d : map (nest 4) ds)
1039 subAnalysis' :: (Monad (m f), DataflowAnalysis m, Outputable f) =>
1042 do { a <- subAnalysis $
1043 do { a <- m; -- facts <- getAllFacts
1044 ; -- my_trace "after sub-analysis facts are" (pprFacts facts) $
1046 -- ; facts <- getAllFacts
1047 ; -- my_trace "in parent analysis facts are" (pprFacts facts) $
1049 -- where pprFacts env = nest 2 $ vcat $ map pprFact $ blockEnvToList env
1050 -- pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)