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
532 -- The need for both k1 and k2 suggests that maybe there's an opportunity
533 -- for improvement here -- in most cases, they're the same...
534 rec_rewrite :: forall t bI bW.
535 Maybe (AGraph m l) -> t -> DFM a bW
536 -> (t -> Fuel -> DFM a bI)
537 -> (bW -> Fuel -> DFM a bI)
538 -> a -> Fuel -> DFM a bI
539 rec_rewrite rewritten analyzed finish k1 k2 in' fuel =
540 case check_maybe fuel rewritten of -- fr_first rewrites id idfact of
541 Nothing -> k1 analyzed fuel
542 Just g -> do g <- areturn g
543 (a, fuel) <- subAnalysis' $
545 RewriteDeep -> solve finish in' g (oneLessFuel fuel)
546 RewriteShallow -> do { a <- anal_f finish in' g
547 ; return (a, oneLessFuel fuel) }
549 solve_tail (G.ZTail m t) in' fuel =
550 rec_rewrite (fr_middle rewrites m in') (ft_middle_out transfers m in')
551 getExitFact (solve_tail t) (solve_tail t) in' fuel
552 solve_tail (G.ZLast (LastOther l)) in' fuel =
553 rec_rewrite (fr_last rewrites l in') (ft_last_outs transfers l in')
554 lastOutFacts k k in' fuel
555 where k a b = return (a, b)
556 solve_tail (G.ZLast LastExit) in' fuel =
557 rec_rewrite (fr_exit rewrites in') (ft_exit_out transfers in')
558 lastOutFacts k (\a b -> return (a, b)) in' fuel
559 where k a fuel = do { setExitFact a ; return (LastOutFacts [], 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
575 mk_set_or_save :: (DataflowAnalysis df, Monad (df a), Outputable a) =>
576 (BlockId -> Bool) -> LastOutFacts a -> df a ()
577 mk_set_or_save is_local (LastOutFacts l) = mapM_ set_or_save_one l
578 where set_or_save_one (id, a) =
579 if is_local id then setFact id a else addLastOutFact (id, a)
585 (DebugNodes m l, LastNode l, Outputable a)
586 => (forall a . Fuel -> Maybe a -> Maybe a)
590 -> ForwardTransfers m l a
591 -> ForwardRewrites m l a
595 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
596 forward_rew check_maybe = forw
598 forw :: RewritingDepth
601 -> ForwardTransfers m l a
602 -> ForwardRewrites m l a
606 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
607 forw depth xstart_facts name transfers rewrites in_factx gx fuelx =
608 let rewrite :: BlockEnv a -> DFM a b
609 -> a -> Graph m l -> Fuel
610 -> DFM a (b, Graph m l, Fuel)
611 rewrite start finish in_fact g fuel =
612 in_fact `seq` g `seq`
613 let Graph entry blockenv = g
614 blocks = G.postorder_dfs_from blockenv entry
615 in do { _ <- forward_sol check_maybe depth name start
616 transfers rewrites in_fact g fuel
617 ; eid <- freshBlockId "temporary entry id"
618 ; (rewritten, fuel) <-
619 rew_tail (ZFirst eid) in_fact entry emptyBlockEnv fuel
620 ; (rewritten, fuel) <- rewrite_blocks blocks rewritten fuel
622 ; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
625 don't_rewrite :: forall t.
626 BlockEnv a -> DFM a t -> a
628 -> DFM a (t, Graph m l, Fuel)
629 don't_rewrite facts finish in_fact g fuel =
630 do { _ <- forward_sol check_maybe depth name facts
631 transfers rewrites in_fact g fuel
633 ; return (a, g, fuel)
636 inner_rew :: DFM a f -> a -> Graph m l -> Fuel -> DFM a (f, Graph m l, Fuel)
637 inner_rew f i g fu = getAllFacts >>= \facts -> inner_rew' facts f i g fu
638 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
639 RewriteDeep -> rewrite
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
650 -- JD: WHY AREN'T WE TAKING ANY FUEL HERE?
651 rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
652 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
653 rewrite_blocks [] rewritten fuel = return (rewritten, fuel)
654 rewrite_blocks (G.Block id t : bs) rewritten fuel =
657 case check_maybe fuel $ fr_first rewrites id a of
658 Nothing -> do { (rewritten, fuel) <-
659 rew_tail h (ft_first_out transfers id a)
661 ; rewrite_blocks bs rewritten fuel }
662 Just g -> do { markGraphRewritten
664 ; (outfact, g, fuel) <- inner_rew getExitFact a g fuel
665 ; let (blocks, h) = splice_head' h g
666 ; (rewritten, fuel) <-
667 rew_tail h outfact t (blocks `plusBlockEnv` rewritten) fuel
668 ; rewrite_blocks bs rewritten fuel }
670 rew_tail head in' (G.ZTail m t) rewritten fuel =
671 in' `seq` rewritten `seq`
672 my_trace "Rewriting middle node" (ppr m) $
673 case check_maybe fuel $ fr_middle rewrites m in' of
674 Nothing -> rew_tail (G.ZHead head m) (ft_middle_out transfers m in') t
676 Just g -> do { markGraphRewritten
678 ; (a, g, fuel) <- inner_rew getExitFact in' g fuel
679 ; let (blocks, h) = G.splice_head' head g
680 ; rew_tail h a t (blocks `plusBlockEnv` rewritten) fuel
682 rew_tail h in' (G.ZLast l) rewritten fuel =
683 in' `seq` rewritten `seq`
684 my_trace "Rewriting last node" (ppr l) $
685 case check_maybe fuel $ either_last rewrites in' l of
686 Nothing -> do check_facts in' l
687 return (insertBlock (zipht h (G.ZLast l)) rewritten, fuel)
688 Just g -> do { markGraphRewritten
691 my_trace "Just" (ppr g) $ inner_rew (return ()) in' g fuel
692 ; let g' = G.splice_head_only' h g
693 ; return (G.lg_blocks g' `plusBlockEnv` rewritten, fuel)
695 either_last rewrites in' (LastExit) = fr_exit rewrites in'
696 either_last rewrites in' (LastOther l) = fr_last rewrites l in'
697 check_facts in' (LastOther l) =
698 let LastOutFacts last_outs = ft_last_outs transfers l in'
699 in mapM_ (uncurry checkFactMatch) last_outs
700 check_facts _ LastExit = return ()
703 lastOutFacts :: DFM f (LastOutFacts f)
704 lastOutFacts = bareLastOutFacts >>= return . LastOutFacts
706 {- ================================================================ -}
708 solve_b :: (DebugNodes m l, Outputable a)
709 => BlockEnv a -- initial facts (unbound == bottom)
711 -> DataflowLattice a -- lattice
712 -> BackwardTransfers m l a -- dataflow transfer functions
714 -> Graph m l -- graph to be analyzed
715 -> FuelMonad (BackwardFixedPoint m l a ()) -- answers
716 solve_b env name lattice transfers exit_fact g =
717 runDFM lattice $ bwd_pure_anal name env transfers g exit_fact
720 rewrite_b_agraph :: (DebugNodes m l, Outputable a)
725 -> BackwardTransfers m l a
726 -> BackwardRewrites m l a
727 -> a -- fact flowing in at exit
729 -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
730 rewrite_b_agraph depth start_facts name lattice transfers rewrites exit_fact g =
732 do fuel <- fuelRemaining
733 (fp, fuel') <- backward_rew maybeRewriteWithFuel depth start_facts name
734 transfers rewrites g exit_fact fuel
735 fuelDecrement name fuel fuel'
742 (DebugNodes m l, LastNode l, Outputable a)
743 => (forall a . Fuel -> Maybe a -> Maybe a)
747 -> BackwardTransfers m l a
748 -> BackwardRewrites m l a
752 -> DFM a (BackwardFixedPoint m l a (), Fuel)
753 backward_sol check_maybe = back
755 back :: RewritingDepth
758 -> BackwardTransfers m l a
759 -> BackwardRewrites m l a
763 -> DFM a (BackwardFixedPoint m l a (), Fuel)
764 back rewrite name start_facts transfers rewrites =
765 let anal_b :: Graph m l -> a -> DFM a a
767 do { fp <- bwd_pure_anal name emptyBlockEnv transfers g out
768 ; return $ zdfFpOutputFact fp }
770 subsolve :: AGraph m l -> a -> Fuel -> DFM a (a, Fuel)
773 RewriteDeep -> \g a fuel ->
774 subAnalysis' $ do { g <- areturn g; solve g a (oneLessFuel fuel) }
775 RewriteShallow -> \g a fuel ->
776 subAnalysis' $ do { g <- areturn g; a <- anal_b g a
777 ; return (a, oneLessFuel fuel) }
779 solve :: Graph m l -> a -> Fuel -> DFM a (a, Fuel)
780 solve (Graph entry blockenv) exit_fact fuel =
781 let blocks = reverse $ G.postorder_dfs_from blockenv entry
782 last_in _env (LastExit) = exit_fact
783 last_in env (LastOther l) = bt_last_in transfers l env
784 last_rew _env (LastExit) = br_exit rewrites
785 last_rew env (LastOther l) = br_last rewrites l env
786 set_block_fact block fuel =
787 let (h, l) = G.goto_end (G.unzip block) in
790 case check_maybe fuel $ last_rew env l of
791 Nothing -> return (last_in env l, fuel)
792 Just g -> do g' <- areturn g
793 my_trace "analysis rewrites last node"
794 (ppr l <+> pprGraph g') $
795 subsolve g exit_fact fuel
796 ; _ <- set_head_fact h a fuel
799 in do { fuel <- run "backward" name set_block_fact blocks fuel
800 ; eid <- freshBlockId "temporary entry id"
801 ; fuel <- set_block_fact (Block eid entry) fuel
807 set_head_fact (G.ZFirst id) a fuel =
808 case check_maybe fuel $ br_first rewrites id a of
809 Nothing -> do { my_trace "set_head_fact" (ppr id <+> text "=" <+>
810 ppr (bt_first_in transfers id a)) $
811 setFact id $ bt_first_in transfers id a
813 Just g -> do { g' <- areturn g
814 ; (a, fuel) <- my_trace "analysis rewrites first node"
815 (ppr id <+> pprGraph g') $
817 ; setFact id $ bt_first_in transfers id a
820 set_head_fact (G.ZHead h m) a fuel =
821 case check_maybe fuel $ br_middle rewrites m a of
822 Nothing -> set_head_fact h (bt_middle_in transfers m a) fuel
823 Just g -> do { g' <- areturn g
824 ; (a, fuel) <- my_trace "analysis rewrites middle node"
825 (ppr m <+> pprGraph g') $
827 ; set_head_fact h a fuel }
829 fixed_point g exit_fact fuel =
830 do { setAllFacts start_facts
831 ; (a, fuel) <- solve g exit_fact fuel
832 ; facts <- getAllFacts
833 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
838 bwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
841 -> BackwardTransfers m l a
844 -> DFM a (BackwardFixedPoint m l a ())
846 bwd_pure_anal name env transfers g exit_fact =
847 do (fp, _) <- anal_b name env transfers panic_rewrites g exit_fact panic_fuel
849 where -- another case of "I love lazy evaluation"
850 anal_b = backward_sol (\_ _ -> Nothing) panic_depth
851 panic_rewrites = panic "pure analysis asked for a rewrite function"
852 panic_fuel = panic "pure analysis asked for fuel"
853 panic_depth = panic "pure analysis asked for a rewrite depth"
856 {- ================================================================ -}
860 (DebugNodes m l, LastNode l, Outputable a)
861 => (forall a . Fuel -> Maybe a -> Maybe a)
865 -> BackwardTransfers m l a
866 -> BackwardRewrites m l a
870 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
871 backward_rew check_maybe = back
873 solve = backward_sol check_maybe
874 back :: RewritingDepth
877 -> BackwardTransfers m l a
878 -> BackwardRewrites m l a
882 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
883 back depth xstart_facts name transfers rewrites gx exit_fact fuelx =
884 let rewrite :: BlockEnv a
885 -> Graph m l -> a -> Fuel
886 -> DFM a (a, Graph m l, Fuel)
887 rewrite start g exit_fact fuel =
888 let Graph entry blockenv = g
889 blocks = reverse $ G.postorder_dfs_from blockenv entry
890 in do { (FP _ in_fact _ _ _, _) <- -- don't drop the entry fact!
891 solve depth name start transfers rewrites g exit_fact fuel
892 --; env <- getAllFacts
893 -- ; my_trace "facts after solving" (ppr env) $ return ()
894 ; eid <- freshBlockId "temporary entry id"
895 ; (rewritten, fuel) <- rewrite_blocks True blocks emptyBlockEnv fuel
896 -- We can't have the fact check fail on the bogus entry, which _may_ change
897 ; (rewritten, fuel) <-
898 rewrite_blocks False [Block eid entry] rewritten fuel
899 ; my_trace "eid" (ppr eid) $ return ()
900 ; my_trace "exit_fact" (ppr exit_fact) $ return ()
901 ; my_trace "in_fact" (ppr in_fact) $ return ()
902 ; return (in_fact, lgraphToGraph (LGraph eid rewritten), fuel)
903 } -- Remember: the entry fact computed by @solve@ accounts for rewriting
904 don't_rewrite facts g exit_fact fuel =
906 solve depth name facts transfers rewrites g exit_fact fuel
907 ; return (zdfFpOutputFact fp, g, fuel) }
908 inner_rew :: Graph m l -> a -> Fuel -> DFM a (a, Graph m l, Fuel)
909 inner_rew g a f = getAllFacts >>= \facts -> inner_rew' facts g a f
910 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
911 RewriteDeep -> rewrite
913 do { (a, g, fuel) <- rewrite xstart_facts gx exit_fact fuelx
914 ; facts <- getAllFacts
915 ; changed <- graphWasRewritten
916 ; let fp = FP facts a changed (panic "no decoration?!") g
919 rewrite_blocks :: Bool -> [Block m l] -> (BlockEnv (Block m l))
920 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
921 rewrite_blocks check bs rewritten fuel =
923 ; let rew [] r f = return (r, f)
925 do { (r, f) <- rewrite_block check env b r f; rew bs r f }
926 ; rew bs rewritten fuel }
927 rewrite_block check env b rewritten fuel =
928 let (h, l) = G.goto_end (G.unzip b) in
929 case maybeRewriteWithFuel fuel $ either_last env l of
930 Nothing -> propagate check fuel h (last_in env l) (ZLast l) rewritten
932 do { markGraphRewritten
934 ; (a, g, fuel) <- inner_rew g exit_fact fuel
935 ; let G.Graph t new_blocks = g
936 ; let rewritten' = new_blocks `plusBlockEnv` rewritten
937 ; propagate check fuel h a t rewritten' -- continue at entry of g
939 either_last _env (LastExit) = br_exit rewrites
940 either_last env (LastOther l) = br_last rewrites l env
941 last_in _env (LastExit) = exit_fact
942 last_in env (LastOther l) = bt_last_in transfers l env
943 propagate check fuel (ZHead h m) a tail rewritten =
944 case maybeRewriteWithFuel fuel $ br_middle rewrites m a of
946 propagate check fuel h (bt_middle_in transfers m a) (ZTail m tail) rewritten
948 do { markGraphRewritten
950 ; my_trace "With Facts" (ppr a) $ return ()
951 ; my_trace " Rewrote middle node"
952 (f4sep [ppr m, text "to", pprGraph g]) $
954 ; (a, g, fuel) <- inner_rew g a fuel
955 ; let Graph t newblocks = G.splice_tail g tail
956 ; my_trace "propagating facts" (ppr a) $
957 propagate check fuel h a t (newblocks `plusBlockEnv` rewritten) }
958 propagate check fuel (ZFirst id) a tail rewritten =
959 case maybeRewriteWithFuel fuel $ br_first rewrites id a of
960 Nothing -> do { if check then
961 checkFactMatch id $ bt_first_in transfers id a
963 ; return (insertBlock (Block id tail) rewritten, fuel) }
965 do { markGraphRewritten
967 ; my_trace "Rewrote first node"
968 (f4sep [ppr id <> colon, text "to", pprGraph g]) $ return ()
969 ; (a, g, fuel) <- inner_rew g a fuel
970 ; if check then checkFactMatch id (bt_first_in transfers id a)
972 ; let Graph t newblocks = G.splice_tail g tail
973 ; let r = insertBlock (Block id t) (newblocks `plusBlockEnv` rewritten)
977 {- ================================================================ -}
979 instance FixedPoint CommonFixedPoint where
980 zdfFpFacts = fp_facts
981 zdfFpOutputFact = fp_out
982 zdfGraphChanged = fp_changed
983 zdfDecoratedGraph = fp_dec_graph
984 zdfFpContents = fp_contents
985 zdfFpMap f (FP fs out ch dg a) = FP fs out ch dg (f a)
987 instance FixedPoint ForwardFixedPoint where
988 zdfFpFacts = fp_facts . ffp_common
989 zdfFpOutputFact = fp_out . ffp_common
990 zdfGraphChanged = fp_changed . ffp_common
991 zdfDecoratedGraph = fp_dec_graph . ffp_common
992 zdfFpContents = fp_contents . ffp_common
993 zdfFpMap f (FFP fp los) = FFP (zdfFpMap f fp) los
999 my_trace :: String -> SDoc -> a -> a
1000 my_trace = if dump_things then pprTrace else \_ _ a -> a
1003 -- | Here's a function to run an action on blocks until we reach a fixed point.
1004 run :: (Outputable a, DebugNodes m l) =>
1005 String -> String -> (Block m l -> b -> DFM a b) -> [Block m l] -> b -> DFM a b
1006 run dir name do_block blocks b =
1007 do { show_blocks $ iterate (1::Int) }
1009 -- N.B. Each iteration starts with the same transaction limit;
1010 -- only the rewrites in the final iteration actually count
1011 trace_block (b, cnt) block =
1012 do b' <- my_trace "about to do" (text name <+> text "on" <+>
1013 ppr (blockId block) <+> ppr cnt) $
1015 return (b', cnt + 1)
1017 do { forgetLastOutFacts
1018 ; markFactsUnchanged
1019 ; (b, _) <- foldM trace_block (b, 0 :: Int) blocks
1020 ; changed <- factsStatus
1021 ; facts <- getAllFacts
1022 ; let depth = 0 -- was nesting depth
1025 NoChange -> unchanged depth $ return b
1027 pprFacts depth n facts $
1028 if n < 1000 then iterate (n+1)
1031 msg n = concat [name, " didn't converge in ", show n, " " , dir,
1033 my_nest depth sdoc = my_trace "" $ nest (3*depth) sdoc
1034 ppIter depth n = my_nest depth (empty $$ text "*************** iteration" <+> pp_i n)
1035 pp_i n = int n <+> text "of" <+> text name <+> text "on" <+> graphId
1037 my_nest depth (text "facts for" <+> graphId <+> text "are unchanged")
1039 graphId = case blocks of { Block id _ : _ -> ppr id ; [] -> text "<empty>" }
1040 show_blocks = my_trace "Blocks:" (vcat (map pprBlock blocks))
1041 pprBlock (Block id t) = nest 2 (pprFact (id, t))
1042 pprFacts depth n env =
1043 my_nest depth (text "facts for iteration" <+> pp_i n <+> text "are:" $$
1044 (nest 2 $ vcat $ map pprFact $ blockEnvToList env))
1046 pprFact :: (Outputable a, Outputable b) => (a,b) -> SDoc
1047 pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)
1049 f4sep :: [SDoc] -> SDoc
1051 f4sep (d:ds) = fsep (d : map (nest 4) ds)
1054 subAnalysis' :: (Monad (m f), DataflowAnalysis m, Outputable f) =>
1057 do { a <- subAnalysis $
1058 do { a <- m; -- facts <- getAllFacts
1059 ; -- my_trace "after sub-analysis facts are" (pprFacts facts) $
1061 -- ; facts <- getAllFacts
1062 ; -- my_trace "in parent analysis facts are" (pprFacts facts) $
1064 -- where pprFacts env = nest 2 $ vcat $ map pprFact $ blockEnvToList env
1065 -- pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)