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