1 {-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables #-}
2 {-# OPTIONS -fno-allow-overlapping-instances -fglasgow-exts #-}
3 -- -fglagow-exts for kind signatures
6 ( zdfSolveFrom, zdfRewriteFrom
7 , ForwardTransfers(..), BackwardTransfers(..)
8 , ForwardRewrites(..), BackwardRewrites(..)
9 , ForwardFixedPoint, BackwardFixedPoint
13 , zdfDecoratedGraph -- not yet implemented
23 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 names, 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, now called ZipDataflow0 and destined for the bit bucket.
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 :: a -> BlockId -> a
123 , bt_middle_in :: a -> middle -> a
124 , bt_last_in :: (BlockId -> a) -> last -> 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 :: a -> BlockId -> a
134 , ft_middle_out :: a -> middle -> a
135 , ft_last_outs :: a -> last -> 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.
147 -- The type of the replacement graph is given as a type parameter 'g'
148 -- of kind * -> * -> *. This design offers great flexibility to clients,
149 -- but it might be worth simplifying this module by replacing this type
150 -- parameter with AGraph everywhere (SLPJ 19 May 2008).
152 data BackwardRewrites middle last a g = BackwardRewrites
153 { br_first :: a -> BlockId -> Maybe (g middle last)
154 , br_middle :: a -> middle -> Maybe (g middle last)
155 , br_last :: (BlockId -> a) -> last -> Maybe (g middle last)
156 , br_exit :: Maybe (g middle last)
159 -- | A forward rewrite takes the same inputs as a forward transfer,
160 -- but instead of producing a fact, it produces a replacement graph or Nothing.
162 data ForwardRewrites middle last a g = ForwardRewrites
163 { fr_first :: a -> BlockId -> Maybe (g middle last)
164 , fr_middle :: a -> middle -> Maybe (g middle last)
165 , fr_last :: a -> last -> Maybe (g middle last)
166 , fr_exit :: a -> Maybe (g middle last)
169 {- ===================== FIXED POINTS =================== -}
171 -- | The result of combined analysis and transformation is a
172 -- solution to the set of dataflow equations together with a 'contained value'.
173 -- This solution is a member of type class 'FixedPoint', which is parameterized by
174 -- * middle and last nodes 'm' and 'l'
175 -- * data flow fact 'fact'
176 -- * the type 'a' of the contained value
178 -- In practice, the contained value 'zdfFpContents' is either a
179 -- rewritten graph, when rewriting, or (), when solving without
180 -- rewriting. A function 'zdfFpMap' allows a client to change
181 -- the contents without changing other values.
183 -- To save space, we provide the solution 'zdfFpFacts' as a mapping
184 -- from BlockId to fact; if necessary, facts on edges can be
185 -- reconstructed using the transfer functions; this functionality is
186 -- intended to be included as the 'zdfDecoratedGraph', but the code
187 -- has not yet been implemented.
189 -- The solution may also includes a fact 'zdfFpOuputFact', which is
190 -- not associated with any label:
191 -- * for a backward problem, this is the fact at entry
192 -- * for a forward problem, this is the fact at the distinguished exit node,
193 -- if such a node is present
195 -- For a forward problem only, the solution includes 'zdfFpLastOuts',
196 -- which is the set of facts on edges leaving the graph.
198 -- The flag 'zdfGraphChanged' tells whether the engine did any rewriting.
200 class FixedPoint fp where
201 zdfFpContents :: fp m l fact a -> a
202 zdfFpFacts :: fp m l fact a -> BlockEnv fact
203 zdfFpOutputFact :: fp m l fact a -> fact -- entry for backward; exit for forward
204 zdfDecoratedGraph :: fp m l fact a -> Graph (fact, m) (fact, l)
205 zdfGraphChanged :: fp m l fact a -> ChangeFlag
206 zdfFpMap :: (a -> b) -> (fp m l fact a -> fp m l fact b)
208 -- | The class 'FixedPoint' has two instances: one for forward problems and
209 -- one for backward problems. The 'CommonFixedPoint' defines all fields
210 -- common to both. (The instance declarations are uninteresting and appear below.)
212 data CommonFixedPoint m l fact a = FP
213 { fp_facts :: BlockEnv fact
214 , fp_out :: fact -- entry for backward; exit for forward
215 , fp_changed :: ChangeFlag
216 , fp_dec_graph :: Graph (fact, m) (fact, l)
220 -- | The common fixed point is sufficient for a backward problem.
221 type BackwardFixedPoint = CommonFixedPoint
223 -- | A forward problem needs the common fields, plus the facts on the outedges.
224 data ForwardFixedPoint m l fact a = FFP
225 { ffp_common :: CommonFixedPoint m l fact a
226 , zdfFpLastOuts :: LastOutFacts fact
230 {- ============== SOLVING AND REWRITING ============== -}
232 type PassName = String
234 -- | zdfSolveFrom is an overloaded name that resolves to a pure
235 -- analysis with no rewriting. It has only two instances: forward and
236 -- backward. Since it needs no rewrites, the type parameters of the
237 -- class are transfer functions and the fixed point.
240 -- An iterative solver normally starts with the bottom fact at every
241 -- node, but it can be useful in other contexts as well. For this
242 -- reason the initial set of facts (at labelled blocks only) is a
243 -- parameter to the solver.
245 -- The constraints on the type signature exist purely for debugging;
246 -- they make it possible to prettyprint nodes and facts. The parameter of
247 -- type 'PassName' is also used just for debugging.
249 -- Note that the result is a fixed point with no contents, that is,
250 -- the contents have type ().
252 -- The intent of the rest of the type signature should be obvious.
253 -- If not, place a skype call to norman-ramsey or complain bitterly
254 -- to norman-ramsey@acm.org.
256 class DataflowSolverDirection transfers fixedpt where
257 zdfSolveFrom :: (DebugNodes m l, Outputable a)
258 => BlockEnv a -- Initial facts (unbound == bottom)
260 -> DataflowLattice a -- Lattice
261 -> transfers m l a -- Dataflow transfer functions
262 -> a -- Fact flowing in (at entry or exit)
263 -> Graph m l -- Graph to be analyzed
264 -> fixedpt m l a () -- Answers
266 -- There are exactly two instances: forward and backward
267 instance DataflowSolverDirection ForwardTransfers ForwardFixedPoint
268 where zdfSolveFrom = solve_f
270 instance DataflowSolverDirection BackwardTransfers BackwardFixedPoint
271 where zdfSolveFrom = solve_b
274 -- | zdfRewriteFrom is an overloaded name that resolves to an
275 -- interleaved analysis and transformation. It too is instantiated in
276 -- forward and backward directions.
278 -- The type parameters of the class include not only transfer
279 -- functions and the fixed point but also rewrites and the type
280 -- constructor (here called 'graph') for making rewritten graphs. As
281 -- above, in the definitoins of the rewrites, it might simplify
282 -- matters if 'graph' were replaced with 'AGraph'.
284 -- The type signature of 'zdfRewriteFrom' is that of 'zdfSolveFrom'
285 -- with additional parameters and a different result. Of course the
286 -- rewrites are an additional parameter, but there are further
287 -- parameters which reflect the fact that rewriting consumes both
288 -- OptimizationFuel and Uniqs.
290 -- The result type is changed to reflect fuel consumption, and also
291 -- the resulting fixed point containts a rewritten graph.
293 -- John Dias is going to improve the management of Uniqs and Fuel so
294 -- that it doesn't make us sick to look at the types.
296 class DataflowSolverDirection transfers fixedpt =>
297 DataflowDirection transfers fixedpt rewrites
298 (graph :: * -> * -> *) where
299 zdfRewriteFrom :: (DebugNodes m l, Outputable a)
300 => RewritingDepth -- whether to rewrite a rewritten graph
301 -> BlockEnv a -- initial facts (unbound == botton)
305 -> rewrites m l a graph
306 -> a -- fact flowing in (at entry or exit)
309 -> FuelMonad (fixedpt m l a (Graph m l))
311 data RewritingDepth = RewriteShallow | RewriteDeep
312 -- When a transformation proposes to rewrite a node,
313 -- you can either ask the system to
314 -- * "shallow": accept the new graph, analyse it without further rewriting
315 -- * "deep": recursively analyse-and-rewrite the new graph
318 -- There are currently four instances, but there could be more
319 -- forward, backward (instantiates transfers, fixedpt, rewrites)
320 -- Graph, AGraph (instantiates graph)
322 instance DataflowDirection ForwardTransfers ForwardFixedPoint ForwardRewrites Graph
323 where zdfRewriteFrom = rewrite_f_graph
325 instance DataflowDirection ForwardTransfers ForwardFixedPoint ForwardRewrites AGraph
326 where zdfRewriteFrom = rewrite_f_agraph
328 instance DataflowDirection BackwardTransfers BackwardFixedPoint BackwardRewrites Graph
329 where zdfRewriteFrom = rewrite_b_graph
331 instance DataflowDirection BackwardTransfers BackwardFixedPoint BackwardRewrites AGraph
332 where zdfRewriteFrom = rewrite_b_agraph
335 {- =================== IMPLEMENTATIONS ===================== -}
338 -----------------------------------------------------------
339 -- solve_f: forward, pure
341 solve_f :: (DebugNodes m l, Outputable a)
342 => BlockEnv a -- initial facts (unbound == bottom)
344 -> DataflowLattice a -- lattice
345 -> ForwardTransfers m l a -- dataflow transfer functions
347 -> Graph m l -- graph to be analyzed
348 -> ForwardFixedPoint m l a () -- answers
349 solve_f env name lattice transfers in_fact g =
350 runWithInfiniteFuel $ runDFM panic_us lattice $
351 fwd_pure_anal name env transfers in_fact g
352 where panic_us = panic "pure analysis pulled on a UniqSupply"
354 rewrite_f_graph :: (DebugNodes m l, Outputable a)
359 -> ForwardTransfers m l a
360 -> ForwardRewrites m l a Graph
361 -> a -- fact flowing in (at entry or exit)
364 -> FuelMonad (ForwardFixedPoint m l a (Graph m l))
365 rewrite_f_graph depth start_facts name lattice transfers rewrites in_fact g u =
367 do fuel <- fuelRemaining
368 (fp, fuel') <- forward_rew maybeRewriteWithFuel return depth start_facts name
369 transfers rewrites in_fact g fuel
370 fuelDecrement name fuel fuel'
373 rewrite_f_agraph :: (DebugNodes m l, Outputable a)
378 -> ForwardTransfers m l a
379 -> ForwardRewrites m l a AGraph
380 -> a -- fact flowing in (at entry or exit)
383 -> FuelMonad (ForwardFixedPoint m l a (Graph m l))
384 rewrite_f_agraph depth start_facts name lattice transfers rewrites in_fact g u =
386 do fuel <- fuelRemaining
387 (fp, fuel') <- forward_rew maybeRewriteWithFuel areturn depth start_facts name
388 transfers rewrites in_fact g fuel
389 fuelDecrement name fuel fuel'
392 areturn :: AGraph m l -> DFM a (Graph m l)
393 areturn g = liftUSM $ graphOfAGraph g
397 graphToLGraph :: LastNode l => Graph m l -> DFM a (LGraph m l)
398 graphToLGraph (Graph (ZLast (LastOther l)) blockenv)
399 | isBranchNode l = return $ LGraph (branchNodeTarget l) blockenv
400 graphToLGraph (Graph tail blockenv) =
401 do id <- freshBlockId "temporary entry label"
402 return $ LGraph id $ insertBlock (Block id tail) blockenv
405 -- | Here we prefer not simply to slap on 'goto eid' because this
406 -- introduces an unnecessary basic block at each rewrite, and we don't
407 -- want to stress out the finite map more than necessary
408 lgraphToGraph :: LastNode l => LGraph m l -> Graph m l
409 lgraphToGraph (LGraph eid blocks) =
410 if flip any (eltsUFM blocks) $ \block -> any (== eid) (succs block) then
411 Graph (ZLast (mkBranchNode eid)) blocks
412 else -- common case: entry is not a branch target
413 let Block _ entry = lookupBlockEnv blocks eid `orElse` panic "missing entry!"
414 in Graph entry (delFromUFM blocks eid)
417 class (Outputable m, Outputable l, LastNode l, Outputable (LGraph m l)) => DebugNodes m l
419 fwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
422 -> ForwardTransfers m l a
425 -> DFM a (ForwardFixedPoint m l a ())
427 fwd_pure_anal name env transfers in_fact g =
428 do (fp, _) <- anal_f name env transfers panic_rewrites in_fact g panic_fuel
430 where -- definitiely a case of "I love lazy evaluation"
431 anal_f = forward_sol (\_ _ -> Nothing) panic_return panic_depth
432 panic_rewrites = panic "pure analysis asked for a rewrite function"
433 panic_fuel = panic "pure analysis asked for fuel"
434 panic_return = panic "pure analysis tried to return a rewritten graph"
435 panic_depth = panic "pure analysis asked for a rewrite depth"
437 -----------------------------------------------------------------------
439 -- Here beginneth the super-general functions
441 -- Think of them as (typechecked) macros
442 -- * They are not exported
444 -- * They are called by the specialised wrappers
445 -- above, and always inlined into their callers
447 -- There are four functions, one for each combination of:
451 -- A "solver" produces a (DFM f (f, Fuel)),
452 -- where f is the fact at entry(Bwd)/exit(Fwd)
453 -- and from the DFM you can extract
458 -- A "rewriter" produces a rewritten *Graph* as well
460 -- Both constrain their rewrites by
462 -- b) RewritingDepth: shallow/deep
464 -----------------------------------------------------------------------
466 type Fuel = OptimizationFuel
468 {-# INLINE forward_sol #-}
471 (DebugNodes m l, LastNode l, Outputable a)
472 => (forall a . Fuel -> Maybe a -> Maybe a)
473 -- Squashes proposed rewrites if there is
474 -- no more fuel; OR if we are doing a pure
475 -- analysis, so totally ignore the rewrite
476 -- ie. For pure-analysis the fn is (\_ _ -> Nothing)
477 -> (g m l -> DFM a (Graph m l))
478 -- Transforms the kind of graph 'g' wanted by the
479 -- client (in ForwardRewrites) to the kind forward_sol likes
480 -> RewritingDepth -- Shallow/deep
482 -> BlockEnv a -- Initial set of facts
483 -> ForwardTransfers m l a
484 -> ForwardRewrites m l a g
488 -> DFM a (ForwardFixedPoint m l a (), Fuel)
489 forward_sol check_maybe return_graph = forw
491 forw :: RewritingDepth
494 -> ForwardTransfers m l a
495 -> ForwardRewrites m l a g
499 -> DFM a (ForwardFixedPoint m l a (), Fuel)
500 forw rewrite name start_facts transfers rewrites =
501 let anal_f :: DFM a b -> a -> Graph m l -> DFM a b
502 anal_f finish in' g =
503 do { fwd_pure_anal name emptyBlockEnv transfers in' g; finish }
505 solve :: DFM a b -> a -> Graph m l -> Fuel -> DFM a (b, Fuel)
506 solve finish in_fact (Graph entry blockenv) fuel =
507 let blocks = G.postorder_dfs_from blockenv entry
508 set_or_save = mk_set_or_save (isJust . lookupBlockEnv blockenv)
509 set_successor_facts (Block id tail) fuel =
510 do { idfact <- getFact id
511 ; (last_outs, fuel) <-
512 case check_maybe fuel $ fr_first rewrites idfact id of
513 Nothing -> solve_tail idfact tail fuel
515 do g <- return_graph g
516 (a, fuel) <- subAnalysis' $
518 RewriteDeep -> solve getExitFact idfact g (oneLessFuel fuel)
520 do { a <- anal_f getExitFact idfact g
521 ; return (a, oneLessFuel fuel) }
522 solve_tail a tail fuel
523 ; set_or_save last_outs
526 in do { (last_outs, fuel) <- solve_tail in_fact entry fuel
527 ; set_or_save last_outs
528 ; fuel <- run "forward" name set_successor_facts blocks fuel
533 solve_tail in' (G.ZTail m t) fuel =
534 case check_maybe fuel $ fr_middle rewrites in' m of
535 Nothing -> solve_tail (ft_middle_out transfers in' m) t fuel
537 do { g <- return_graph g
538 ; (a, fuel) <- subAnalysis' $
540 RewriteDeep -> solve getExitFact in' g (oneLessFuel fuel)
541 RewriteShallow -> do { a <- anal_f getExitFact in' g
542 ; return (a, oneLessFuel fuel) }
543 ; solve_tail a t fuel
545 solve_tail in' (G.ZLast l) fuel =
546 case check_maybe fuel $ either_last rewrites in' l of
548 case l of LastOther l -> return (ft_last_outs transfers in' l, fuel)
549 LastExit -> do { setExitFact (ft_exit_out transfers in')
550 ; return (LastOutFacts [], fuel) }
552 do { g <- return_graph g
553 ; (last_outs :: LastOutFacts a, fuel) <- subAnalysis' $
555 RewriteDeep -> solve lastOutFacts in' g (oneLessFuel fuel)
556 RewriteShallow -> do { los <- anal_f lastOutFacts in' g
557 ; return (los, fuel) }
558 ; return (last_outs, fuel)
561 fixed_point in_fact g fuel =
562 do { setAllFacts start_facts
563 ; (a, fuel) <- solve getExitFact in_fact g fuel
564 ; facts <- getAllFacts
565 ; last_outs <- lastOutFacts
566 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
567 ; let fp = FFP cfp last_outs
571 either_last rewrites in' (LastExit) = fr_exit rewrites in'
572 either_last rewrites in' (LastOther l) = fr_last rewrites in' l
579 mk_set_or_save :: (DataflowAnalysis df, Monad (df a), Outputable a) =>
580 (BlockId -> Bool) -> LastOutFacts a -> df a ()
581 mk_set_or_save is_local (LastOutFacts l) = mapM_ set_or_save_one l
582 where set_or_save_one (id, a) =
583 if is_local id then setFact id a else addLastOutFact (id, a)
588 {-# INLINE forward_rew #-}
591 (DebugNodes m l, LastNode l, Outputable a)
592 => (forall a . Fuel -> Maybe a -> Maybe a)
593 -> (g m l -> DFM a (Graph m l)) -- option on what to rewrite
597 -> ForwardTransfers m l a
598 -> ForwardRewrites m l a g
602 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
603 forward_rew check_maybe return_graph = forw
605 solve = forward_sol check_maybe return_graph
606 forw :: RewritingDepth
609 -> ForwardTransfers m l a
610 -> ForwardRewrites m l a g
614 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
615 forw depth xstart_facts name transfers rewrites in_factx gx fuelx =
616 let rewrite :: BlockEnv a -> DFM a b
617 -> a -> Graph m l -> Fuel
618 -> DFM a (b, Graph m l, Fuel)
619 rewrite start finish in_fact g fuel =
620 let Graph entry blockenv = g
621 blocks = G.postorder_dfs_from blockenv entry
622 in do { solve depth name start transfers rewrites in_fact g fuel
623 ; eid <- freshBlockId "temporary entry id"
624 ; (rewritten, fuel) <-
625 rew_tail (ZFirst eid) in_fact entry emptyBlockEnv fuel
626 ; (rewritten, fuel) <- rewrite_blocks blocks rewritten fuel
628 ; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
630 don't_rewrite finish in_fact g fuel =
631 do { solve depth name emptyBlockEnv transfers rewrites in_fact g fuel
633 ; return (a, g, fuel)
636 -> a -> Graph m l -> Fuel
637 -> DFM a (b, Graph m l, Fuel)
638 inner_rew = case depth of RewriteShallow -> don't_rewrite
639 RewriteDeep -> rewrite emptyBlockEnv
641 do { (a, g, fuel) <- rewrite xstart_facts getExitFact in_factx gx fuelx
642 ; facts <- getAllFacts
643 ; changed <- graphWasRewritten
644 ; last_outs <- lastOutFacts
645 ; let cfp = FP facts a changed (panic "no decoration?!") g
646 ; let fp = FFP cfp last_outs
649 rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
650 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
651 rewrite_blocks [] rewritten fuel = return (rewritten, fuel)
652 rewrite_blocks (G.Block id t : bs) rewritten fuel =
655 case check_maybe fuel $ fr_first rewrites a id of
656 Nothing -> do { (rewritten, fuel) <- rew_tail h a t rewritten fuel
657 ; rewrite_blocks bs rewritten fuel }
658 Just g -> do { markGraphRewritten
659 ; g <- return_graph g
660 ; (outfact, g, fuel) <- inner_rew getExitFact a g fuel
661 ; let (blocks, h) = splice_head' (ZFirst id) g
662 ; (rewritten, fuel) <-
663 rew_tail h outfact t (blocks `plusUFM` rewritten) fuel
664 ; rewrite_blocks bs rewritten fuel }
666 rew_tail head in' (G.ZTail m t) rewritten fuel =
667 my_trace "Rewriting middle node" (ppr m) $
668 case check_maybe fuel $ fr_middle rewrites in' m of
669 Nothing -> rew_tail (G.ZHead head m) (ft_middle_out transfers in' m) t
671 Just g -> do { markGraphRewritten
672 ; g <- return_graph g
673 ; (a, g, fuel) <- inner_rew getExitFact in' g fuel
674 ; let (blocks, h) = G.splice_head' head g
675 ; rew_tail h a t (blocks `plusUFM` rewritten) fuel
677 rew_tail h in' (G.ZLast l) rewritten fuel =
678 my_trace "Rewriting last node" (ppr l) $
679 case check_maybe fuel $ either_last rewrites in' l of
680 Nothing -> -- can throw away facts because this is the rewriting phase
681 return (insertBlock (zipht h (G.ZLast l)) rewritten, fuel)
682 Just g -> do { markGraphRewritten
683 ; g <- return_graph g
684 ; ((), g, fuel) <- inner_rew (return ()) in' g fuel
685 ; let g' = G.splice_head_only' h g
686 ; return (G.lg_blocks g' `plusUFM` rewritten, fuel)
688 either_last rewrites in' (LastExit) = fr_exit rewrites in'
689 either_last rewrites in' (LastOther l) = fr_last rewrites in' l
692 --lastOutFacts :: (DataflowAnalysis m, Monad (m f)) => m f (LastOutFacts f)
693 lastOutFacts :: DFM f (LastOutFacts f)
694 lastOutFacts = bareLastOutFacts >>= return . LastOutFacts
696 {- ================================================================ -}
698 solve_b :: (DebugNodes m l, Outputable a)
699 => BlockEnv a -- initial facts (unbound == bottom)
701 -> DataflowLattice a -- lattice
702 -> BackwardTransfers m l a -- dataflow transfer functions
704 -> Graph m l -- graph to be analyzed
705 -> BackwardFixedPoint m l a () -- answers
706 solve_b env name lattice transfers exit_fact g =
707 runWithInfiniteFuel $ runDFM panic_us lattice $
708 bwd_pure_anal name env transfers g exit_fact
709 where panic_us = panic "pure analysis pulled on a UniqSupply"
712 rewrite_b_graph :: (DebugNodes m l, Outputable a)
717 -> BackwardTransfers m l a
718 -> BackwardRewrites m l a Graph
719 -> a -- fact flowing in at exit
722 -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
723 rewrite_b_graph depth start_facts name lattice transfers rewrites exit_fact g u =
725 do fuel <- fuelRemaining
726 (fp, fuel') <- backward_rew maybeRewriteWithFuel return depth start_facts name
727 transfers rewrites g exit_fact fuel
728 fuelDecrement name fuel fuel'
731 rewrite_b_agraph :: (DebugNodes m l, Outputable a)
736 -> BackwardTransfers m l a
737 -> BackwardRewrites m l a AGraph
738 -> a -- fact flowing in at exit
741 -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
742 rewrite_b_agraph depth start_facts name lattice transfers rewrites exit_fact g u =
744 do fuel <- fuelRemaining
745 (fp, fuel') <- backward_rew maybeRewriteWithFuel areturn depth start_facts name
746 transfers rewrites g exit_fact fuel
747 fuelDecrement name fuel fuel'
752 {-# INLINE backward_sol #-}
755 (DebugNodes m l, LastNode l, Outputable a)
756 => (forall a . Fuel -> Maybe a -> Maybe a)
757 -> (g m l -> DFM a (Graph m l)) -- option on what to rewrite
761 -> BackwardTransfers m l a
762 -> BackwardRewrites m l a g
766 -> DFM a (BackwardFixedPoint m l a (), Fuel)
767 backward_sol check_maybe return_graph = back
769 back :: RewritingDepth
772 -> BackwardTransfers m l a
773 -> BackwardRewrites m l a g
777 -> DFM a (BackwardFixedPoint m l a (), Fuel)
778 back rewrite name start_facts transfers rewrites =
779 let anal_b :: Graph m l -> a -> DFM a a
781 do { fp <- bwd_pure_anal name emptyBlockEnv transfers g out
782 ; return $ zdfFpOutputFact fp }
784 subsolve :: g m l -> a -> Fuel -> DFM a (a, Fuel)
787 RewriteDeep -> \g a fuel ->
788 subAnalysis' $ do { g <- return_graph g; solve g a (oneLessFuel fuel) }
789 RewriteShallow -> \g a fuel ->
790 subAnalysis' $ do { g <- return_graph g; a <- anal_b g a
791 ; return (a, oneLessFuel fuel) }
793 solve :: Graph m l -> a -> Fuel -> DFM a (a, Fuel)
794 solve (Graph entry blockenv) exit_fact fuel =
795 let blocks = reverse $ G.postorder_dfs_from blockenv entry
796 last_in _env (LastExit) = exit_fact
797 last_in env (LastOther l) = bt_last_in transfers env l
798 last_rew _env (LastExit) = br_exit rewrites
799 last_rew env (LastOther l) = br_last rewrites env l
800 set_block_fact block fuel =
801 let (h, l) = G.goto_end (G.unzip block) in
804 case check_maybe fuel $ last_rew env l of
805 Nothing -> return (last_in env l, fuel)
806 Just g -> subsolve g exit_fact fuel
807 ; set_head_fact h a fuel
810 in do { fuel <- run "backward" name set_block_fact blocks fuel
811 ; eid <- freshBlockId "temporary entry id"
812 ; fuel <- set_block_fact (Block eid entry) fuel
818 set_head_fact (G.ZFirst id) a fuel =
819 case check_maybe fuel $ br_first rewrites a id of
820 Nothing -> do { setFact id a; return fuel }
821 Just g -> do { (a, fuel) <- subsolve g a fuel
825 set_head_fact (G.ZHead h m) a fuel =
826 case check_maybe fuel $ br_middle rewrites a m of
827 Nothing -> set_head_fact h (bt_middle_in transfers a m) fuel
828 Just g -> do { (a, fuel) <- subsolve g a fuel
829 ; set_head_fact h a fuel }
831 fixed_point g exit_fact fuel =
832 do { setAllFacts start_facts
833 ; (a, fuel) <- solve g exit_fact fuel
834 ; facts <- getAllFacts
835 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
840 bwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
843 -> BackwardTransfers m l a
846 -> DFM a (BackwardFixedPoint m l a ())
848 bwd_pure_anal name env transfers g exit_fact =
849 do (fp, _) <- anal_b name env transfers panic_rewrites g exit_fact panic_fuel
851 where -- another case of "I love lazy evaluation"
852 anal_b = backward_sol (\_ _ -> Nothing) panic_return panic_depth
853 panic_rewrites = panic "pure analysis asked for a rewrite function"
854 panic_fuel = panic "pure analysis asked for fuel"
855 panic_return = panic "pure analysis tried to return a rewritten graph"
856 panic_depth = panic "pure analysis asked for a rewrite depth"
859 {- ================================================================ -}
861 {-# INLINE backward_rew #-}
864 (DebugNodes m l, LastNode l, Outputable a)
865 => (forall a . Fuel -> Maybe a -> Maybe a)
866 -> (g m l -> DFM a (Graph m l)) -- option on what to rewrite
870 -> BackwardTransfers m l a
871 -> BackwardRewrites m l a g
875 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
876 backward_rew check_maybe return_graph = back
878 solve = backward_sol check_maybe return_graph
879 back :: RewritingDepth
882 -> BackwardTransfers m l a
883 -> BackwardRewrites m l a g
887 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
888 back depth xstart_facts name transfers rewrites gx exit_fact fuelx =
889 let rewrite :: BlockEnv a
890 -> Graph m l -> a -> Fuel
891 -> DFM a (a, Graph m l, Fuel)
892 rewrite start g exit_fact fuel =
893 let Graph entry blockenv = g
894 blocks = reverse $ G.postorder_dfs_from blockenv entry
895 in do { solve depth name start transfers rewrites g exit_fact fuel
896 ; eid <- freshBlockId "temporary entry id"
897 ; (rewritten, fuel) <- rewrite_blocks blocks emptyBlockEnv fuel
898 ; (rewritten, fuel) <- rewrite_blocks [Block eid entry] rewritten fuel
900 ; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
902 don't_rewrite g exit_fact fuel =
904 solve depth name emptyBlockEnv transfers rewrites g exit_fact fuel
905 ; return (zdfFpOutputFact fp, g, fuel) }
906 inner_rew = case depth of RewriteShallow -> don't_rewrite
907 RewriteDeep -> rewrite emptyBlockEnv
908 inner_rew :: Graph m l -> a -> Fuel -> DFM a (a, Graph m l, Fuel)
910 do { (a, g, fuel) <- rewrite xstart_facts gx exit_fact fuelx
911 ; facts <- getAllFacts
912 ; changed <- graphWasRewritten
913 ; let fp = FP facts a changed (panic "no decoration?!") g
916 rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
917 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
918 rewrite_blocks bs rewritten fuel =
920 ; let rew [] r f = return (r, f)
922 do { (r, f) <- rewrite_block env b r f; rew bs r f }
923 ; rew bs rewritten fuel }
924 rewrite_block env b rewritten fuel =
925 let (h, l) = G.goto_end (G.unzip b) in
926 case maybeRewriteWithFuel fuel $ either_last env l of
927 Nothing -> propagate fuel h (last_in env l) (ZLast l) rewritten
929 do { markGraphRewritten
930 ; g <- return_graph g
931 ; (a, g, fuel) <- inner_rew g exit_fact fuel
932 ; let G.Graph t new_blocks = g
933 ; let rewritten' = new_blocks `plusUFM` rewritten
934 ; propagate fuel h a t rewritten' -- continue at entry of g
936 either_last _env (LastExit) = br_exit rewrites
937 either_last env (LastOther l) = br_last rewrites env l
938 last_in _env (LastExit) = exit_fact
939 last_in env (LastOther l) = bt_last_in transfers env l
940 propagate fuel (ZHead h m) a tail rewritten =
941 case maybeRewriteWithFuel fuel $ br_middle rewrites a m of
943 propagate fuel h (bt_middle_in transfers a m) (ZTail m tail) rewritten
945 do { markGraphRewritten
946 ; g <- return_graph g
947 ; my_trace "Rewrote middle node"
948 (f4sep [ppr m, text "to", pprGraph g]) $
950 ; (a, g, fuel) <- inner_rew g a fuel
951 ; let Graph t newblocks = G.splice_tail g tail
952 ; propagate fuel h a t (newblocks `plusUFM` rewritten) }
953 propagate fuel (ZFirst id) a tail rewritten =
954 case maybeRewriteWithFuel fuel $ br_first rewrites a id of
955 Nothing -> do { checkFactMatch id a
956 ; return (insertBlock (Block id tail) rewritten, fuel) }
958 do { markGraphRewritten
959 ; g <- return_graph g
960 ; my_trace "Rewrote first node"
961 (f4sep [ppr id <> colon, text "to", pprGraph g]) $ return ()
962 ; (a, g, fuel) <- inner_rew g a fuel
963 ; checkFactMatch id a
964 ; let Graph t newblocks = G.splice_tail g tail
965 ; let r = insertBlock (Block id t) (newblocks `plusUFM` rewritten)
969 {- ================================================================ -}
971 instance FixedPoint CommonFixedPoint where
972 zdfFpFacts = fp_facts
973 zdfFpOutputFact = fp_out
974 zdfGraphChanged = fp_changed
975 zdfDecoratedGraph = fp_dec_graph
976 zdfFpContents = fp_contents
977 zdfFpMap f (FP fs out ch dg a) = FP fs out ch dg (f a)
979 instance FixedPoint ForwardFixedPoint where
980 zdfFpFacts = fp_facts . ffp_common
981 zdfFpOutputFact = fp_out . ffp_common
982 zdfGraphChanged = fp_changed . ffp_common
983 zdfDecoratedGraph = fp_dec_graph . ffp_common
984 zdfFpContents = fp_contents . ffp_common
985 zdfFpMap f (FFP fp los) = FFP (zdfFpMap f fp) los
991 my_trace :: String -> SDoc -> a -> a
992 my_trace = if dump_things then pprTrace else \_ _ a -> a
995 -- | Here's a function to run an action on blocks until we reach a fixed point.
996 run :: (Outputable a, DebugNodes m l) =>
997 String -> String -> (Block m l -> b -> DFM a b) -> [Block m l] -> b -> DFM a b
998 run dir name do_block blocks b =
999 do { show_blocks $ iterate (1::Int) }
1001 -- N.B. Each iteration starts with the same transaction limit;
1002 -- only the rewrites in the final iteration actually count
1003 trace_block b block =
1004 my_trace "about to do" (text name <+> text "on" <+> ppr (blockId block)) $
1007 do { markFactsUnchanged
1008 ; b <- foldM trace_block b blocks
1009 ; changed <- factsStatus
1010 ; facts <- getAllFacts
1011 ; let depth = 0 -- was nesting depth
1014 NoChange -> unchanged depth $ return b
1016 pprFacts depth n facts $
1017 if n < 1000 then iterate (n+1)
1020 msg n = concat [name, " didn't converge in ", show n, " " , dir,
1022 my_nest depth sdoc = my_trace "" $ nest (3*depth) sdoc
1023 ppIter depth n = my_nest depth (empty $$ text "*************** iteration" <+> pp_i n)
1024 pp_i n = int n <+> text "of" <+> text name <+> text "on" <+> graphId
1025 unchanged depth = my_nest depth (text "facts are unchanged")
1027 pprFacts depth n env =
1028 my_nest depth (text "facts for iteration" <+> pp_i n <+> text "are:" $$
1029 (nest 2 $ vcat $ map pprFact $ ufmToList env))
1030 pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)
1031 graphId = case blocks of { Block id _ : _ -> ppr id ; [] -> text "<empty>" }
1032 show_blocks = my_trace "Blocks:" (vcat (map pprBlock blocks))
1033 pprBlock (Block id t) = nest 2 (pprFact (id, t))
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 $ ufmToList env
1052 pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)