1 {-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables, KindSignatures,
5 ( DebugNodes(), RewritingDepth(..), LastOutFacts(..)
6 , zdfSolveFrom, zdfRewriteFrom
8 , ForwardTransfers(..), BackwardTransfers(..)
9 , ForwardRewrites(..), BackwardRewrites(..)
10 , ForwardFixedPoint, BackwardFixedPoint
14 , zdfDecoratedGraph -- not yet implemented
17 , zdfBRewriteFromL, zdfFRewriteFromL
24 import OptimizationFuel as F
27 import qualified ZipCfg as G
36 This module implements two useful tools:
38 1. An iterative solver for dataflow problems
40 2. The combined dataflow-analysis-and-transformation framework
41 described by Lerner, Grove, and Chambers in their excellent
42 2002 POPL paper (http://tinyurl.com/3zycbr or
43 http://tinyurl.com/3pnscd).
45 Each tool comes in two flavors: one for forward dataflow problems
46 and one for backward dataflow problems.
48 We quote the paper above:
50 Dataflow analyses can have mutually beneficial interactions.
51 Previous efforts to exploit these interactions have either
52 (1) iteratively performed each individual analysis until no
53 further improvements are discovered or (2) developed "super-
54 analyses" that manually combine conceptually separate anal-
55 yses. We have devised a new approach that allows anal-
56 yses to be defined independently while still enabling them
57 to be combined automatically and profitably. Our approach
58 avoids the loss of precision associated with iterating indi-
59 vidual analyses and the implementation difficulties of man-
60 ually writing a super-analysis.
62 The key idea is to provide at each CFG node not only a dataflow
63 transfer function but also a rewriting function that has the option to
64 replace the node with a new (possibly empty) graph. The rewriting
65 function takes a dataflow fact as input, and the fact is used to
66 justify any rewriting. For example, in a backward problem, the fact
67 that variable x is dead can be used to justify rewriting node
69 to the empty graph. In a forward problem, the fact that x == 7 can
70 be used to justify rewriting node
74 which in turn will be analyzed and produce a new fact:
77 In its most general form, this module takes as input graph, transfer
78 equations, rewrites, and an initial set of dataflow facts, and
79 iteratively computes a new graph and a new set of dataflow facts such
81 * The set of facts is a fixed point of the transfer equations
82 * The graph has been rewritten as much as is consistent with
83 the given facts and requested rewriting depth (see below)
84 N.B. 'A set of facts' is shorthand for 'A finite map from CFG label to fact'.
86 The types of transfer equations, rewrites, and fixed points are
87 different for forward and backward problems. To avoid cluttering the
88 name space with two versions of every name, other names such as
89 zdfSolveFrom are overloaded to work in both forward or backward
90 directions. This design decision is based on experience with the
91 predecessor module, which has been mercifully deleted.
94 This module is deliberately very abstract. It is a completely general
95 framework and well-nigh impossible to understand in isolation. The
96 cautious reader will begin with some concrete examples in the form of
97 clients. NR recommends
99 CmmLiveZ A simple liveness analysis
101 CmmSpillReload.removeDeadAssignmentsAndReloads
102 A piece of spaghetti to pull on, which leads to
103 - a two-part liveness analysis that tracks
104 variables live in registers and live on the stack
105 - elimination of assignments to dead variables
106 - elimination of redundant reloads
108 Even hearty souls should avoid the CmmProcPointZ client, at least for
114 {- ============ TRANSFER FUNCTIONS AND REWRITES =========== -}
116 -- | For a backward transfer, you're given the fact on a node's
117 -- outedge and you compute the fact on the inedge. Facts have type 'a'.
118 -- A last node may have multiple outedges, each pointing to a labelled
119 -- block, so instead of a fact it is given a mapping from BlockId to fact.
121 data BackwardTransfers middle last a = BackwardTransfers
122 { bt_first_in :: BlockId -> a -> a
123 , bt_middle_in :: middle -> a -> a
124 , bt_last_in :: last -> (BlockId -> a) -> a
127 -- | For a forward transfer, you're given the fact on a node's
128 -- inedge and you compute the fact on the outedge. Because a last node
129 -- may have multiple outedges, each pointing to a labelled
130 -- block, so instead of a fact it produces a list of (BlockId, fact) pairs.
132 data ForwardTransfers middle last a = ForwardTransfers
133 { ft_first_out :: BlockId -> a -> a
134 , ft_middle_out :: middle -> a -> a
135 , ft_last_outs :: last -> a -> LastOutFacts a
136 , ft_exit_out :: a -> a
139 newtype LastOutFacts a = LastOutFacts [(BlockId, a)]
140 -- ^ These are facts flowing out of a last node to the node's successors.
141 -- They are either to be set (if they pertain to the graph currently
142 -- under analysis) or propagated out of a sub-analysis
145 -- | A backward rewrite takes the same inputs as a backward transfer,
146 -- but instead of producing a fact, it produces a replacement graph or Nothing.
148 data BackwardRewrites middle last a = BackwardRewrites
149 { br_first :: BlockId -> a -> Maybe (AGraph middle last)
150 , br_middle :: middle -> a -> Maybe (AGraph middle last)
151 , br_last :: last -> (BlockId -> a) -> Maybe (AGraph middle last)
152 , br_exit :: Maybe (AGraph middle last)
155 -- | A forward rewrite takes the same inputs as a forward transfer,
156 -- but instead of producing a fact, it produces a replacement graph or Nothing.
158 data ForwardRewrites middle last a = ForwardRewrites
159 { fr_first :: BlockId -> a -> Maybe (AGraph middle last)
160 , fr_middle :: middle -> a -> Maybe (AGraph middle last)
161 , fr_last :: last -> a -> Maybe (AGraph middle last)
162 , fr_exit :: a -> Maybe (AGraph middle last)
165 {- ===================== FIXED POINTS =================== -}
167 -- | The result of combined analysis and transformation is a
168 -- solution to the set of dataflow equations together with a 'contained value'.
169 -- This solution is a member of type class 'FixedPoint', which is parameterized by
170 -- * middle and last nodes 'm' and 'l'
171 -- * data flow fact 'fact'
172 -- * the type 'a' of the contained value
174 -- In practice, the contained value 'zdfFpContents' is either a
175 -- rewritten graph, when rewriting, or (), when solving without
176 -- rewriting. A function 'zdfFpMap' allows a client to change
177 -- the contents without changing other values.
179 -- To save space, we provide the solution 'zdfFpFacts' as a mapping
180 -- from BlockId to fact; if necessary, facts on edges can be
181 -- reconstructed using the transfer functions; this functionality is
182 -- intended to be included as the 'zdfDecoratedGraph', but the code
183 -- has not yet been implemented.
185 -- The solution may also includes a fact 'zdfFpOuputFact', which is
186 -- not associated with any label:
187 -- * for a backward problem, this is the fact at entry
188 -- * for a forward problem, this is the fact at the distinguished exit node,
189 -- if such a node is present
191 -- For a forward problem only, the solution includes 'zdfFpLastOuts',
192 -- which is the set of facts on edges leaving the graph.
194 -- The flag 'zdfGraphChanged' tells whether the engine did any rewriting.
196 class FixedPoint fp where
197 zdfFpContents :: fp m l fact a -> a
198 zdfFpFacts :: fp m l fact a -> BlockEnv fact
199 zdfFpOutputFact :: fp m l fact a -> fact -- entry for backward; exit for forward
200 zdfDecoratedGraph :: fp m l fact a -> Graph (fact, m) (fact, l)
201 zdfGraphChanged :: fp m l fact a -> ChangeFlag
202 zdfFpMap :: (a -> b) -> (fp m l fact a -> fp m l fact b)
204 -- | The class 'FixedPoint' has two instances: one for forward problems and
205 -- one for backward problems. The 'CommonFixedPoint' defines all fields
206 -- common to both. (The instance declarations are uninteresting and appear below.)
208 data CommonFixedPoint m l fact a = FP
209 { fp_facts :: BlockEnv fact
210 , fp_out :: fact -- entry for backward; exit for forward
211 , fp_changed :: ChangeFlag
212 , fp_dec_graph :: Graph (fact, m) (fact, l)
216 -- | The common fixed point is sufficient for a backward problem.
217 type BackwardFixedPoint = CommonFixedPoint
219 -- | A forward problem needs the common fields, plus the facts on the outedges.
220 data ForwardFixedPoint m l fact a = FFP
221 { ffp_common :: CommonFixedPoint m l fact a
222 , zdfFpLastOuts :: LastOutFacts fact
226 {- ============== SOLVING AND REWRITING ============== -}
228 type PassName = String
230 -- | 'zdfSolveFrom' is an overloaded name that resolves to a pure
231 -- analysis with no rewriting. It has only two instances: forward and
232 -- backward. Since it needs no rewrites, the type parameters of the
233 -- class are transfer functions and the fixed point.
236 -- An iterative solver normally starts with the bottom fact at every
237 -- node, but it can be useful in other contexts as well. For this
238 -- reason the initial set of facts (at labelled blocks only) is a
239 -- parameter to the solver.
241 -- The constraints on the type signature exist purely for debugging;
242 -- they make it possible to prettyprint nodes and facts. The parameter of
243 -- type 'PassName' is also used just for debugging.
245 -- Note that the result is a fixed point with no contents, that is,
246 -- the contents have type ().
248 -- The intent of the rest of the type signature should be obvious.
249 -- If not, place a skype call to norman-ramsey or complain bitterly
250 -- to <norman-ramsey@acm.org>.
252 class DataflowSolverDirection transfers fixedpt where
253 zdfSolveFrom :: (DebugNodes m l, Outputable a)
254 => BlockEnv a -- ^ Initial facts (unbound == bottom)
256 -> DataflowLattice a -- ^ Lattice
257 -> transfers m l a -- ^ Dataflow transfer functions
258 -> a -- ^ Fact flowing in (at entry or exit)
259 -> Graph m l -- ^ Graph to be analyzed
260 -> FuelMonad (fixedpt m l a ()) -- ^ Answers
261 zdfSolveFromL :: (DebugNodes m l, Outputable a)
262 => BlockEnv a -- Initial facts (unbound == bottom)
264 -> DataflowLattice a -- Lattice
265 -> transfers m l a -- Dataflow transfer functions
266 -> a -- Fact flowing in (at entry or exit)
267 -> LGraph m l -- Graph to be analyzed
268 -> FuelMonad (fixedpt m l a ()) -- Answers
269 zdfSolveFromL b p l t a g = zdfSolveFrom b p l t a $ quickGraph g
271 -- There are exactly two instances: forward and backward
272 instance DataflowSolverDirection ForwardTransfers ForwardFixedPoint
273 where zdfSolveFrom = solve_f
275 instance DataflowSolverDirection BackwardTransfers BackwardFixedPoint
276 where zdfSolveFrom = solve_b
279 -- | zdfRewriteFrom is an overloaded name that resolves to an
280 -- interleaved analysis and transformation. It too is instantiated in
281 -- forward and backward directions.
283 -- The type parameters of the class include not only transfer
284 -- functions and the fixed point but also rewrites.
286 -- The type signature of 'zdfRewriteFrom' is that of 'zdfSolveFrom'
287 -- with the rewrites and a rewriting depth as additional parameters,
288 -- as well as a different result, which contains a rewritten graph.
290 class DataflowSolverDirection transfers fixedpt =>
291 DataflowDirection transfers fixedpt rewrites where
292 zdfRewriteFrom :: (DebugNodes m l, Outputable a)
293 => RewritingDepth -- whether to rewrite a rewritten graph
294 -> BlockEnv a -- initial facts (unbound == bottom)
299 -> a -- fact flowing in (at entry or exit)
301 -> FuelMonad (fixedpt m l a (Graph m l))
303 -- Temporarily lifting from Graph to LGraph -- an experiment to see how we
304 -- can eliminate some hysteresis between Graph and LGraph.
305 -- Perhaps Graph should be confined to dataflow code.
306 -- Trading space for time
307 quickGraph :: LastNode l => LGraph m l -> Graph m l
308 quickGraph g = Graph (ZLast $ mkBranchNode $ lg_entry g) $ lg_blocks g
310 quickLGraph :: LastNode l => Graph m l -> FuelMonad (LGraph m l)
311 quickLGraph (Graph (ZLast (LastOther l)) blockenv)
312 | isBranchNode l = return $ LGraph (branchNodeTarget l) blockenv
313 quickLGraph g = F.lGraphOfGraph g
315 fixptWithLGraph :: LastNode l => CommonFixedPoint m l fact (Graph m l) ->
316 FuelMonad (CommonFixedPoint m l fact (LGraph m l))
317 fixptWithLGraph cfp =
318 do fp_c <- quickLGraph $ fp_contents cfp
319 return $ cfp {fp_contents = fp_c}
321 ffixptWithLGraph :: LastNode l => ForwardFixedPoint m l fact (Graph m l) ->
322 FuelMonad (ForwardFixedPoint m l fact (LGraph m l))
323 ffixptWithLGraph fp =
324 do common <- fixptWithLGraph $ ffp_common fp
325 return $ fp {ffp_common = common}
327 zdfFRewriteFromL :: (DebugNodes m l, Outputable a)
328 => RewritingDepth -- whether to rewrite a rewritten graph
329 -> BlockEnv a -- initial facts (unbound == bottom)
332 -> ForwardTransfers m l a
333 -> ForwardRewrites m l a
334 -> a -- fact flowing in (at entry or exit)
336 -> FuelMonad (ForwardFixedPoint m l a (LGraph m l))
337 zdfFRewriteFromL d b p l t r a g@(LGraph _ _) =
338 do fp <- zdfRewriteFrom d b p l t r a $ quickGraph g
341 zdfBRewriteFromL :: (DebugNodes m l, Outputable a)
342 => RewritingDepth -- whether to rewrite a rewritten graph
343 -> BlockEnv a -- initial facts (unbound == bottom)
346 -> BackwardTransfers m l a
347 -> BackwardRewrites m l a
348 -> a -- fact flowing in (at entry or exit)
350 -> FuelMonad (BackwardFixedPoint m l a (LGraph m l))
351 zdfBRewriteFromL d b p l t r a g@(LGraph _ _) =
352 do fp <- zdfRewriteFrom d b p l t r a $ quickGraph g
356 data RewritingDepth = RewriteShallow | RewriteDeep
357 -- When a transformation proposes to rewrite a node,
358 -- you can either ask the system to
359 -- * "shallow": accept the new graph, analyse it without further rewriting
360 -- * "deep": recursively analyse-and-rewrite the new graph
363 -- There are currently four instances, but there could be more
364 -- forward, backward (instantiates transfers, fixedpt, rewrites)
365 -- Graph, AGraph (instantiates graph)
367 instance DataflowDirection ForwardTransfers ForwardFixedPoint ForwardRewrites
368 where zdfRewriteFrom = rewrite_f_agraph
370 instance DataflowDirection BackwardTransfers BackwardFixedPoint BackwardRewrites
371 where zdfRewriteFrom = rewrite_b_agraph
374 {- =================== IMPLEMENTATIONS ===================== -}
377 -----------------------------------------------------------
378 -- solve_f: forward, pure
380 solve_f :: (DebugNodes m l, Outputable a)
381 => BlockEnv a -- initial facts (unbound == bottom)
383 -> DataflowLattice a -- lattice
384 -> ForwardTransfers m l a -- dataflow transfer functions
386 -> Graph m l -- graph to be analyzed
387 -> FuelMonad (ForwardFixedPoint m l a ()) -- answers
388 solve_f env name lattice transfers in_fact g =
389 runDFM lattice $ fwd_pure_anal name env transfers in_fact g
391 rewrite_f_agraph :: (DebugNodes m l, Outputable a)
396 -> ForwardTransfers m l a
397 -> ForwardRewrites m l a
398 -> a -- fact flowing in (at entry or exit)
400 -> FuelMonad (ForwardFixedPoint m l a (Graph m l))
401 rewrite_f_agraph depth start_facts name lattice transfers rewrites in_fact g =
403 do fuel <- fuelRemaining
404 (fp, fuel') <- forward_rew maybeRewriteWithFuel depth start_facts name
405 transfers rewrites in_fact g fuel
406 fuelDecrement name fuel fuel'
409 areturn :: AGraph m l -> DFM a (Graph m l)
410 areturn g = liftToDFM $ liftUniq $ graphOfAGraph g
412 -- | Here we prefer not simply to slap on 'goto eid' because this
413 -- introduces an unnecessary basic block at each rewrite, and we don't
414 -- want to stress out the finite map more than necessary
415 lgraphToGraph :: LastNode l => LGraph m l -> Graph m l
416 lgraphToGraph (LGraph eid blocks) =
417 if flip any (eltsBlockEnv blocks) $ \block -> any (== eid) (succs block) then
418 Graph (ZLast (mkBranchNode eid)) blocks
419 else -- common case: entry is not a branch target
420 let Block _ entry = lookupBlockEnv blocks eid `orElse` panic "missing entry!"
421 in Graph entry (delFromBlockEnv blocks eid)
424 class (Outputable m, Outputable l, LastNode l, Outputable (LGraph m l)) => DebugNodes m l
426 fwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
429 -> ForwardTransfers m l a
432 -> DFM a (ForwardFixedPoint m l a ())
434 fwd_pure_anal name env transfers in_fact g =
435 do (fp, _) <- anal_f name env transfers panic_rewrites in_fact g panic_fuel
437 where -- definitely a case of "I love lazy evaluation"
438 anal_f = forward_sol (\_ _ -> Nothing) panic_depth
439 panic_rewrites = panic "pure analysis asked for a rewrite function"
440 panic_fuel = panic "pure analysis asked for fuel"
441 panic_depth = panic "pure analysis asked for a rewrite depth"
443 -----------------------------------------------------------------------
445 -- Here beginneth the super-general functions
447 -- Think of them as (typechecked) macros
448 -- * They are not exported
450 -- * They are called by the specialised wrappers
451 -- above, and always inlined into their callers
453 -- There are four functions, one for each combination of:
457 -- A "solver" produces a (DFM f (f, Fuel)),
458 -- where f is the fact at entry(Bwd)/exit(Fwd)
459 -- and from the DFM you can extract
464 -- A "rewriter" produces a rewritten *Graph* as well
466 -- Both constrain their rewrites by
468 -- b) RewritingDepth: shallow/deep
470 -----------------------------------------------------------------------
472 type Fuel = OptimizationFuel
476 (DebugNodes m l, LastNode l, Outputable a)
477 => (forall a . Fuel -> Maybe a -> Maybe a)
478 -- Squashes proposed rewrites if there is
479 -- no more fuel; OR if we are doing a pure
480 -- analysis, so totally ignore the rewrite
481 -- ie. For pure-analysis the fn is (\_ _ -> Nothing)
482 -> RewritingDepth -- Shallow/deep
484 -> BlockEnv a -- Initial set of facts
485 -> ForwardTransfers m l a
486 -> ForwardRewrites m l a
490 -> DFM a (ForwardFixedPoint m l a (), Fuel)
491 forward_sol check_maybe = forw
493 forw :: RewritingDepth
496 -> ForwardTransfers m l a
497 -> ForwardRewrites m l a
501 -> DFM a (ForwardFixedPoint m l a (), Fuel)
502 forw rewrite name start_facts transfers rewrites =
503 let anal_f :: DFM a b -> a -> Graph m l -> DFM a b
504 anal_f finish in' g =
505 do { _ <- fwd_pure_anal name emptyBlockEnv transfers in' g; finish }
507 solve :: DFM a b -> a -> Graph m l -> Fuel -> DFM a (b, Fuel)
508 solve finish in_fact (Graph entry blockenv) fuel =
509 let blocks = G.postorder_dfs_from blockenv entry
510 set_or_save = mk_set_or_save (isJust . lookupBlockEnv blockenv)
511 set_successor_facts (Block id tail) fuel =
512 do { idfact <- getFact id
513 ; (last_outs, fuel) <- rec_rewrite (fr_first rewrites id idfact)
514 (ft_first_out transfers id idfact)
515 getExitFact (solve_tail tail)
516 (solve_tail tail) idfact fuel
517 ; set_or_save last_outs
519 in do { (last_outs, fuel) <- solve_tail entry in_fact fuel
520 -- last_outs contains a mix of internal facts, which
521 -- are inputs to 'run', and external facts, which
522 -- are going to be forgotten by 'run'
523 ; set_or_save last_outs
524 ; fuel <- run "forward" name set_successor_facts blocks fuel
525 ; set_or_save last_outs
526 -- 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 :: forall t bI bW.
534 Maybe (AGraph m l) -> t -> DFM a bW
535 -> (t -> Fuel -> DFM a bI)
536 -> (bW -> Fuel -> DFM a bI)
537 -> a -> Fuel -> DFM a bI
538 rec_rewrite rewritten analyzed finish k1 k2 in' fuel =
539 case check_maybe fuel rewritten of -- fr_first rewrites id idfact of
540 Nothing -> k1 analyzed fuel
541 Just g -> do g <- areturn g
542 (a, fuel) <- subAnalysis' $
544 RewriteDeep -> solve finish in' g (oneLessFuel fuel)
545 RewriteShallow -> do { a <- anal_f finish in' g
546 ; return (a, oneLessFuel fuel) }
548 solve_tail (G.ZTail m t) in' fuel =
549 rec_rewrite (fr_middle rewrites m in') (ft_middle_out transfers m in')
550 getExitFact (solve_tail t) (solve_tail t) in' fuel
551 solve_tail (G.ZLast (LastOther l)) in' fuel =
552 rec_rewrite (fr_last rewrites l in') (ft_last_outs transfers l in')
553 lastOutFacts k k in' fuel
554 where k a b = return (a, b)
555 solve_tail (G.ZLast LastExit) in' fuel =
556 rec_rewrite (fr_exit rewrites in') (ft_exit_out transfers in')
557 lastOutFacts k (\a b -> return (a, b)) in' fuel
558 where k a fuel = do { setExitFact a ; return (LastOutFacts [], fuel) }
560 fixed_point in_fact g fuel =
561 do { setAllFacts start_facts
562 ; (a, fuel) <- solve getExitFact in_fact g fuel
563 ; facts <- getAllFacts
564 ; last_outs <- lastOutFacts
565 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
566 ; let fp = FFP cfp last_outs
574 mk_set_or_save :: (DataflowAnalysis df, Monad (df a), Outputable a) =>
575 (BlockId -> Bool) -> LastOutFacts a -> df a ()
576 mk_set_or_save is_local (LastOutFacts l) = mapM_ set_or_save_one l
577 where set_or_save_one (id, a) =
578 if is_local id then setFact id a else addLastOutFact (id, a)
584 (DebugNodes m l, LastNode l, Outputable a)
585 => (forall a . Fuel -> Maybe a -> Maybe a)
589 -> ForwardTransfers m l a
590 -> ForwardRewrites m l a
594 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
595 forward_rew check_maybe = forw
597 forw :: RewritingDepth
600 -> ForwardTransfers m l a
601 -> ForwardRewrites m l a
605 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
606 forw depth xstart_facts name transfers rewrites in_factx gx fuelx =
607 let rewrite :: BlockEnv a -> DFM a b
608 -> a -> Graph m l -> Fuel
609 -> DFM a (b, Graph m l, Fuel)
610 rewrite start finish in_fact g fuel =
611 in_fact `seq` g `seq`
612 let Graph entry blockenv = g
613 blocks = G.postorder_dfs_from blockenv entry
614 in do { _ <- forward_sol check_maybe depth name start
615 transfers rewrites in_fact g fuel
616 ; eid <- freshBlockId "temporary entry id"
617 ; (rewritten, fuel) <-
618 rew_tail (ZFirst eid) in_fact entry emptyBlockEnv fuel
619 ; (rewritten, fuel) <- rewrite_blocks blocks rewritten fuel
621 ; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
624 don't_rewrite :: forall t.
625 BlockEnv a -> DFM a t -> a
627 -> DFM a (t, Graph m l, Fuel)
628 don't_rewrite facts finish in_fact g fuel =
629 do { _ <- forward_sol check_maybe depth name facts
630 transfers rewrites in_fact g fuel
632 ; return (a, g, fuel)
635 inner_rew :: DFM a f -> a -> Graph m l -> Fuel -> DFM a (f, Graph m l, Fuel)
636 inner_rew f i g fu = getAllFacts >>= \facts -> inner_rew' facts f i g fu
637 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
638 RewriteDeep -> rewrite
640 do { (a, g, fuel) <- rewrite xstart_facts getExitFact in_factx gx fuelx
641 ; facts <- getAllFacts
642 ; changed <- graphWasRewritten
643 ; last_outs <- lastOutFacts
644 ; let cfp = FP facts a changed (panic "no decoration?!") g
645 ; let fp = FFP cfp last_outs
649 -- JD: WHY AREN'T WE TAKING ANY FUEL HERE?
650 rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
651 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
652 rewrite_blocks [] rewritten fuel = return (rewritten, fuel)
653 rewrite_blocks (G.Block id t : bs) rewritten fuel =
656 case check_maybe fuel $ fr_first rewrites id a of
657 Nothing -> do { (rewritten, fuel) <-
658 rew_tail h (ft_first_out transfers id a)
660 ; rewrite_blocks bs rewritten fuel }
661 Just g -> do { markGraphRewritten
663 ; (outfact, g, fuel) <- inner_rew getExitFact a g fuel
664 ; let (blocks, h) = splice_head' h g
665 ; (rewritten, fuel) <-
666 rew_tail h outfact t (blocks `plusBlockEnv` rewritten) fuel
667 ; rewrite_blocks bs rewritten fuel }
669 rew_tail head in' (G.ZTail m t) rewritten fuel =
670 in' `seq` rewritten `seq`
671 my_trace "Rewriting middle node" (ppr m) $
672 case check_maybe fuel $ fr_middle rewrites m in' of
673 Nothing -> rew_tail (G.ZHead head m) (ft_middle_out transfers m in') t
675 Just g -> do { markGraphRewritten
677 ; (a, g, fuel) <- inner_rew getExitFact in' g fuel
678 ; let (blocks, h) = G.splice_head' head g
679 ; rew_tail h a t (blocks `plusBlockEnv` rewritten) fuel
681 rew_tail h in' (G.ZLast l) rewritten fuel =
682 in' `seq` rewritten `seq`
683 my_trace "Rewriting last node" (ppr l) $
684 case check_maybe fuel $ either_last rewrites in' l of
685 Nothing -> do check_facts in' l
686 return (insertBlock (zipht h (G.ZLast l)) rewritten, fuel)
687 Just g -> do { markGraphRewritten
690 my_trace "Just" (ppr g) $ inner_rew (return ()) in' g fuel
691 ; let g' = G.splice_head_only' h g
692 ; return (G.lg_blocks g' `plusBlockEnv` rewritten, fuel)
694 either_last rewrites in' (LastExit) = fr_exit rewrites in'
695 either_last rewrites in' (LastOther l) = fr_last rewrites l in'
696 check_facts in' (LastOther l) =
697 let LastOutFacts last_outs = ft_last_outs transfers l in'
698 in mapM_ (uncurry checkFactMatch) last_outs
699 check_facts _ LastExit = return ()
702 lastOutFacts :: DFM f (LastOutFacts f)
703 lastOutFacts = bareLastOutFacts >>= return . LastOutFacts
705 {- ================================================================ -}
707 solve_b :: (DebugNodes m l, Outputable a)
708 => BlockEnv a -- initial facts (unbound == bottom)
710 -> DataflowLattice a -- lattice
711 -> BackwardTransfers m l a -- dataflow transfer functions
713 -> Graph m l -- graph to be analyzed
714 -> FuelMonad (BackwardFixedPoint m l a ()) -- answers
715 solve_b env name lattice transfers exit_fact g =
716 runDFM lattice $ bwd_pure_anal name env transfers g exit_fact
719 rewrite_b_agraph :: (DebugNodes m l, Outputable a)
724 -> BackwardTransfers m l a
725 -> BackwardRewrites m l a
726 -> a -- fact flowing in at exit
728 -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
729 rewrite_b_agraph depth start_facts name lattice transfers rewrites exit_fact g =
731 do fuel <- fuelRemaining
732 (fp, fuel') <- backward_rew maybeRewriteWithFuel depth start_facts name
733 transfers rewrites g exit_fact fuel
734 fuelDecrement name fuel fuel'
741 (DebugNodes m l, LastNode l, Outputable a)
742 => (forall a . Fuel -> Maybe a -> Maybe a)
746 -> BackwardTransfers m l a
747 -> BackwardRewrites m l a
751 -> DFM a (BackwardFixedPoint m l a (), Fuel)
752 backward_sol check_maybe = back
754 back :: RewritingDepth
757 -> BackwardTransfers m l a
758 -> BackwardRewrites m l a
762 -> DFM a (BackwardFixedPoint m l a (), Fuel)
763 back rewrite name start_facts transfers rewrites =
764 let anal_b :: Graph m l -> a -> DFM a a
766 do { fp <- bwd_pure_anal name emptyBlockEnv transfers g out
767 ; return $ zdfFpOutputFact fp }
769 subsolve :: AGraph m l -> a -> Fuel -> DFM a (a, Fuel)
772 RewriteDeep -> \g a fuel ->
773 subAnalysis' $ do { g <- areturn g; solve g a (oneLessFuel fuel) }
774 RewriteShallow -> \g a fuel ->
775 subAnalysis' $ do { g <- areturn g; a <- anal_b g a
776 ; return (a, oneLessFuel fuel) }
778 solve :: Graph m l -> a -> Fuel -> DFM a (a, Fuel)
779 solve (Graph entry blockenv) exit_fact fuel =
780 let blocks = reverse $ G.postorder_dfs_from blockenv entry
781 last_in _env (LastExit) = exit_fact
782 last_in env (LastOther l) = bt_last_in transfers l env
783 last_rew _env (LastExit) = br_exit rewrites
784 last_rew env (LastOther l) = br_last rewrites l env
785 set_block_fact block fuel =
786 let (h, l) = G.goto_end (G.unzip block) in
789 case check_maybe fuel $ last_rew env l of
790 Nothing -> return (last_in env l, fuel)
791 Just g -> do g' <- areturn g
792 my_trace "analysis rewrites last node"
793 (ppr l <+> pprGraph g') $
794 subsolve g exit_fact fuel
795 ; _ <- set_head_fact h a fuel
798 in do { fuel <- run "backward" name set_block_fact blocks fuel
799 ; eid <- freshBlockId "temporary entry id"
800 ; fuel <- set_block_fact (Block eid entry) fuel
806 set_head_fact (G.ZFirst id) a fuel =
807 case check_maybe fuel $ br_first rewrites id a of
808 Nothing -> do { my_trace "set_head_fact" (ppr id <+> text "=" <+>
809 ppr (bt_first_in transfers id a)) $
810 setFact id $ bt_first_in transfers id a
812 Just g -> do { g' <- areturn g
813 ; (a, fuel) <- my_trace "analysis rewrites first node"
814 (ppr id <+> pprGraph g') $
816 ; setFact id $ bt_first_in transfers id a
819 set_head_fact (G.ZHead h m) a fuel =
820 case check_maybe fuel $ br_middle rewrites m a of
821 Nothing -> set_head_fact h (bt_middle_in transfers m a) fuel
822 Just g -> do { g' <- areturn g
823 ; (a, fuel) <- my_trace "analysis rewrites middle node"
824 (ppr m <+> pprGraph g') $
826 ; set_head_fact h a fuel }
828 fixed_point g exit_fact fuel =
829 do { setAllFacts start_facts
830 ; (a, fuel) <- solve g exit_fact fuel
831 ; facts <- getAllFacts
832 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
837 bwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
840 -> BackwardTransfers m l a
843 -> DFM a (BackwardFixedPoint m l a ())
845 bwd_pure_anal name env transfers g exit_fact =
846 do (fp, _) <- anal_b name env transfers panic_rewrites g exit_fact panic_fuel
848 where -- another case of "I love lazy evaluation"
849 anal_b = backward_sol (\_ _ -> Nothing) panic_depth
850 panic_rewrites = panic "pure analysis asked for a rewrite function"
851 panic_fuel = panic "pure analysis asked for fuel"
852 panic_depth = panic "pure analysis asked for a rewrite depth"
855 {- ================================================================ -}
859 (DebugNodes m l, LastNode l, Outputable a)
860 => (forall a . Fuel -> Maybe a -> Maybe a)
864 -> BackwardTransfers m l a
865 -> BackwardRewrites m l a
869 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
870 backward_rew check_maybe = back
872 solve = backward_sol check_maybe
873 back :: RewritingDepth
876 -> BackwardTransfers m l a
877 -> BackwardRewrites m l a
881 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
882 back depth xstart_facts name transfers rewrites gx exit_fact fuelx =
883 let rewrite :: BlockEnv a
884 -> Graph m l -> a -> Fuel
885 -> DFM a (a, Graph m l, Fuel)
886 rewrite start g exit_fact fuel =
887 let Graph entry blockenv = g
888 blocks = reverse $ G.postorder_dfs_from blockenv entry
889 in do { (FP _ in_fact _ _ _, _) <- -- don't drop the entry fact!
890 solve depth name start transfers rewrites g exit_fact fuel
891 --; env <- getAllFacts
892 -- ; my_trace "facts after solving" (ppr env) $ return ()
893 ; eid <- freshBlockId "temporary entry id"
894 ; (rewritten, fuel) <- rewrite_blocks True blocks emptyBlockEnv fuel
895 -- We can't have the fact check fail on the bogus entry, which _may_ change
896 ; (rewritten, fuel) <-
897 rewrite_blocks False [Block eid entry] rewritten fuel
898 ; my_trace "eid" (ppr eid) $ return ()
899 ; my_trace "exit_fact" (ppr exit_fact) $ return ()
900 ; my_trace "in_fact" (ppr in_fact) $ return ()
901 ; return (in_fact, lgraphToGraph (LGraph eid rewritten), fuel)
902 } -- Remember: the entry fact computed by @solve@ accounts for rewriting
903 don't_rewrite facts g exit_fact fuel =
905 solve depth name facts transfers rewrites g exit_fact fuel
906 ; return (zdfFpOutputFact fp, g, fuel) }
907 inner_rew :: Graph m l -> a -> Fuel -> DFM a (a, Graph m l, Fuel)
908 inner_rew g a f = getAllFacts >>= \facts -> inner_rew' facts g a f
909 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
910 RewriteDeep -> rewrite
912 do { (a, g, fuel) <- rewrite xstart_facts gx exit_fact fuelx
913 ; facts <- getAllFacts
914 ; changed <- graphWasRewritten
915 ; let fp = FP facts a changed (panic "no decoration?!") g
918 rewrite_blocks :: Bool -> [Block m l] -> (BlockEnv (Block m l))
919 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
920 rewrite_blocks check bs rewritten fuel =
922 ; let rew [] r f = return (r, f)
924 do { (r, f) <- rewrite_block check env b r f; rew bs r f }
925 ; rew bs rewritten fuel }
926 rewrite_block check env b rewritten fuel =
927 let (h, l) = G.goto_end (G.unzip b) in
928 case maybeRewriteWithFuel fuel $ either_last env l of
929 Nothing -> propagate check fuel h (last_in env l) (ZLast l) rewritten
931 do { markGraphRewritten
933 ; (a, g, fuel) <- inner_rew g exit_fact fuel
934 ; let G.Graph t new_blocks = g
935 ; let rewritten' = new_blocks `plusBlockEnv` rewritten
936 ; propagate check fuel h a t rewritten' -- continue at entry of g
938 either_last _env (LastExit) = br_exit rewrites
939 either_last env (LastOther l) = br_last rewrites l env
940 last_in _env (LastExit) = exit_fact
941 last_in env (LastOther l) = bt_last_in transfers l env
942 propagate check fuel (ZHead h m) a tail rewritten =
943 case maybeRewriteWithFuel fuel $ br_middle rewrites m a of
945 propagate check fuel h (bt_middle_in transfers m a) (ZTail m tail) rewritten
947 do { markGraphRewritten
949 ; my_trace "With Facts" (ppr a) $ return ()
950 ; my_trace " Rewrote middle node"
951 (f4sep [ppr m, text "to", pprGraph g]) $
953 ; (a, g, fuel) <- inner_rew g a fuel
954 ; let Graph t newblocks = G.splice_tail g tail
955 ; my_trace "propagating facts" (ppr a) $
956 propagate check fuel h a t (newblocks `plusBlockEnv` rewritten) }
957 propagate check fuel (ZFirst id) a tail rewritten =
958 case maybeRewriteWithFuel fuel $ br_first rewrites id a of
959 Nothing -> do { if check then
960 checkFactMatch id $ bt_first_in transfers id a
962 ; return (insertBlock (Block id tail) rewritten, fuel) }
964 do { markGraphRewritten
966 ; my_trace "Rewrote first node"
967 (f4sep [ppr id <> colon, text "to", pprGraph g]) $ return ()
968 ; (a, g, fuel) <- inner_rew g a fuel
969 ; if check then checkFactMatch id (bt_first_in transfers id a)
971 ; let Graph t newblocks = G.splice_tail g tail
972 ; let r = insertBlock (Block id t) (newblocks `plusBlockEnv` rewritten)
976 {- ================================================================ -}
978 instance FixedPoint CommonFixedPoint where
979 zdfFpFacts = fp_facts
980 zdfFpOutputFact = fp_out
981 zdfGraphChanged = fp_changed
982 zdfDecoratedGraph = fp_dec_graph
983 zdfFpContents = fp_contents
984 zdfFpMap f (FP fs out ch dg a) = FP fs out ch dg (f a)
986 instance FixedPoint ForwardFixedPoint where
987 zdfFpFacts = fp_facts . ffp_common
988 zdfFpOutputFact = fp_out . ffp_common
989 zdfGraphChanged = fp_changed . ffp_common
990 zdfDecoratedGraph = fp_dec_graph . ffp_common
991 zdfFpContents = fp_contents . ffp_common
992 zdfFpMap f (FFP fp los) = FFP (zdfFpMap f fp) los
998 my_trace :: String -> SDoc -> a -> a
999 my_trace = if dump_things then pprTrace else \_ _ a -> a
1002 -- | Here's a function to run an action on blocks until we reach a fixed point.
1003 run :: (Outputable a, DebugNodes m l) =>
1004 String -> String -> (Block m l -> b -> DFM a b) -> [Block m l] -> b -> DFM a b
1005 run dir name do_block blocks b =
1006 do { show_blocks $ iterate (1::Int) }
1008 -- N.B. Each iteration starts with the same transaction limit;
1009 -- only the rewrites in the final iteration actually count
1010 trace_block (b, cnt) block =
1011 do b' <- my_trace "about to do" (text name <+> text "on" <+>
1012 ppr (blockId block) <+> ppr cnt) $
1014 return (b', cnt + 1)
1016 do { forgetLastOutFacts
1017 ; markFactsUnchanged
1018 ; (b, _) <- foldM trace_block (b, 0 :: Int) blocks
1019 ; changed <- factsStatus
1020 ; facts <- getAllFacts
1021 ; let depth = 0 -- was nesting depth
1024 NoChange -> unchanged depth $ return b
1026 pprFacts depth n facts $
1027 if n < 1000 then iterate (n+1)
1030 msg n = concat [name, " didn't converge in ", show n, " " , dir,
1032 my_nest depth sdoc = my_trace "" $ nest (3*depth) sdoc
1033 ppIter depth n = my_nest depth (empty $$ text "*************** iteration" <+> pp_i n)
1034 pp_i n = int n <+> text "of" <+> text name <+> text "on" <+> graphId
1036 my_nest depth (text "facts for" <+> graphId <+> text "are unchanged")
1038 graphId = case blocks of { Block id _ : _ -> ppr id ; [] -> text "<empty>" }
1039 show_blocks = my_trace "Blocks:" (vcat (map pprBlock blocks))
1040 pprBlock (Block id t) = nest 2 (pprFact (id, t))
1041 pprFacts depth n env =
1042 my_nest depth (text "facts for iteration" <+> pp_i n <+> text "are:" $$
1043 (nest 2 $ vcat $ map pprFact $ blockEnvToList env))
1045 pprFact :: (Outputable a, Outputable b) => (a,b) -> SDoc
1046 pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)
1048 f4sep :: [SDoc] -> SDoc
1050 f4sep (d:ds) = fsep (d : map (nest 4) ds)
1053 subAnalysis' :: (Monad (m f), DataflowAnalysis m, Outputable f) =>
1056 do { a <- subAnalysis $
1057 do { a <- m; -- facts <- getAllFacts
1058 ; -- my_trace "after sub-analysis facts are" (pprFacts facts) $
1060 -- ; facts <- getAllFacts
1061 ; -- my_trace "in parent analysis facts are" (pprFacts facts) $
1063 -- where pprFacts env = nest 2 $ vcat $ map pprFact $ blockEnvToList env
1064 -- pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)