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 names, 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, now called ZipDataflow0 and destined for the bit bucket.
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 :: a -> BlockId -> a
126 , bt_middle_in :: a -> middle -> a
127 , bt_last_in :: (BlockId -> a) -> last -> 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 :: a -> BlockId -> a
137 , ft_middle_out :: a -> middle -> a
138 , ft_last_outs :: a -> last -> 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 :: a -> BlockId -> Maybe (AGraph middle last)
153 , br_middle :: a -> middle -> Maybe (AGraph middle last)
154 , br_last :: (BlockId -> a) -> last -> 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 :: a -> BlockId -> Maybe (AGraph middle last)
163 , fr_middle :: a -> middle -> Maybe (AGraph middle last)
164 , fr_last :: a -> last -> 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 and the type
288 -- constructor (here called 'graph') for making rewritten graphs. As
289 -- above, in the definitoins of the rewrites, it might simplify
290 -- matters if 'graph' were replaced with 'AGraph'.
292 -- The type signature of 'zdfRewriteFrom' is that of 'zdfSolveFrom'
293 -- with additional parameters and a different result. Of course the
294 -- rewrites are an additional parameter, but there are further
295 -- parameters which reflect the fact that rewriting consumes both
296 -- OptimizationFuel and Uniqs.
298 -- The result type is changed to reflect fuel consumption, and also
299 -- the resulting fixed point containts a rewritten graph.
301 -- John Dias is going to improve the management of Uniqs and Fuel so
302 -- that it doesn't make us sick to look at the types.
304 class DataflowSolverDirection transfers fixedpt =>
305 DataflowDirection transfers fixedpt rewrites where
306 zdfRewriteFrom :: (DebugNodes m l, Outputable a)
307 => RewritingDepth -- whether to rewrite a rewritten graph
308 -> BlockEnv a -- initial facts (unbound == botton)
313 -> a -- fact flowing in (at entry or exit)
315 -> FuelMonad (fixedpt m l a (Graph m l))
317 -- Temporarily lifting from Graph to LGraph -- an experiment to see how we
318 -- can eliminate some hysteresis between Graph and LGraph.
319 -- Perhaps Graph should be confined to dataflow code.
320 -- Trading space for time
321 quickGraph :: LastNode l => LGraph m l -> Graph m l
322 quickGraph g = Graph (ZLast $ mkBranchNode $ lg_entry g) $ lg_blocks g
324 quickLGraph :: LastNode l => Int -> Graph m l -> FuelMonad (LGraph m l)
325 quickLGraph args (Graph (ZLast (LastOther l)) blockenv)
326 | isBranchNode l = return $ LGraph (branchNodeTarget l) args blockenv
327 quickLGraph args g = F.lGraphOfGraph g args
329 fixptWithLGraph :: LastNode l => Int -> CommonFixedPoint m l fact (Graph m l) ->
330 FuelMonad (CommonFixedPoint m l fact (LGraph m l))
331 fixptWithLGraph args cfp =
332 do fp_c <- quickLGraph args $ fp_contents cfp
333 return $ cfp {fp_contents = fp_c}
335 ffixptWithLGraph :: LastNode l => Int -> ForwardFixedPoint m l fact (Graph m l) ->
336 FuelMonad (ForwardFixedPoint m l fact (LGraph m l))
337 ffixptWithLGraph args fp =
338 do common <- fixptWithLGraph args $ ffp_common fp
339 return $ fp {ffp_common = common}
341 zdfFRewriteFromL :: (DebugNodes m l, Outputable a)
342 => RewritingDepth -- whether to rewrite a rewritten graph
343 -> BlockEnv a -- initial facts (unbound == botton)
346 -> ForwardTransfers m l a
347 -> ForwardRewrites m l a
348 -> a -- fact flowing in (at entry or exit)
350 -> FuelMonad (ForwardFixedPoint m l a (LGraph m l))
351 zdfFRewriteFromL d b p l t r a g@(LGraph _ args _) =
352 do fp <- zdfRewriteFrom d b p l t r a $ quickGraph g
353 ffixptWithLGraph args fp
355 zdfBRewriteFromL :: (DebugNodes m l, Outputable a)
356 => RewritingDepth -- whether to rewrite a rewritten graph
357 -> BlockEnv a -- initial facts (unbound == botton)
360 -> BackwardTransfers m l a
361 -> BackwardRewrites m l a
362 -> a -- fact flowing in (at entry or exit)
364 -> FuelMonad (BackwardFixedPoint m l a (LGraph m l))
365 zdfBRewriteFromL d b p l t r a g@(LGraph _ args _) =
366 do fp <- zdfRewriteFrom d b p l t r a $ quickGraph g
367 fixptWithLGraph args fp
370 data RewritingDepth = RewriteShallow | RewriteDeep
371 -- When a transformation proposes to rewrite a node,
372 -- you can either ask the system to
373 -- * "shallow": accept the new graph, analyse it without further rewriting
374 -- * "deep": recursively analyse-and-rewrite the new graph
377 -- There are currently four instances, but there could be more
378 -- forward, backward (instantiates transfers, fixedpt, rewrites)
379 -- Graph, AGraph (instantiates graph)
381 instance DataflowDirection ForwardTransfers ForwardFixedPoint ForwardRewrites
382 where zdfRewriteFrom = rewrite_f_agraph
384 instance DataflowDirection BackwardTransfers BackwardFixedPoint BackwardRewrites
385 where zdfRewriteFrom = rewrite_b_agraph
388 {- =================== IMPLEMENTATIONS ===================== -}
391 -----------------------------------------------------------
392 -- solve_f: forward, pure
394 solve_f :: (DebugNodes m l, Outputable a)
395 => BlockEnv a -- initial facts (unbound == bottom)
397 -> DataflowLattice a -- lattice
398 -> ForwardTransfers m l a -- dataflow transfer functions
400 -> Graph m l -- graph to be analyzed
401 -> FuelMonad (ForwardFixedPoint m l a ()) -- answers
402 solve_f env name lattice transfers in_fact g =
403 runDFM lattice $ fwd_pure_anal name env transfers in_fact g
405 rewrite_f_agraph :: (DebugNodes m l, Outputable a)
410 -> ForwardTransfers m l a
411 -> ForwardRewrites m l a
412 -> a -- fact flowing in (at entry or exit)
414 -> FuelMonad (ForwardFixedPoint m l a (Graph m l))
415 rewrite_f_agraph depth start_facts name lattice transfers rewrites in_fact g =
417 do fuel <- fuelRemaining
418 (fp, fuel') <- forward_rew maybeRewriteWithFuel depth start_facts name
419 transfers rewrites in_fact g fuel
420 fuelDecrement name fuel fuel'
423 areturn :: AGraph m l -> DFM a (Graph m l)
424 areturn g = liftToDFM $ liftUniq $ graphOfAGraph g
426 -- | Here we prefer not simply to slap on 'goto eid' because this
427 -- introduces an unnecessary basic block at each rewrite, and we don't
428 -- want to stress out the finite map more than necessary
429 lgraphToGraph :: LastNode l => LGraph m l -> Graph m l
430 lgraphToGraph (LGraph eid _ blocks) =
431 if flip any (eltsBlockEnv blocks) $ \block -> any (== eid) (succs block) then
432 Graph (ZLast (mkBranchNode eid)) blocks
433 else -- common case: entry is not a branch target
434 let Block _ _ entry = lookupBlockEnv blocks eid `orElse` panic "missing entry!"
435 in Graph entry (delFromBlockEnv blocks eid)
438 class (Outputable m, Outputable l, LastNode l, Outputable (LGraph m l)) => DebugNodes m l
440 fwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
443 -> ForwardTransfers m l a
446 -> DFM a (ForwardFixedPoint m l a ())
448 fwd_pure_anal name env transfers in_fact g =
449 do (fp, _) <- anal_f name env transfers panic_rewrites in_fact g panic_fuel
451 where -- definitely a case of "I love lazy evaluation"
452 anal_f = forward_sol (\_ _ -> Nothing) panic_depth
453 panic_rewrites = panic "pure analysis asked for a rewrite function"
454 panic_fuel = panic "pure analysis asked for fuel"
455 panic_depth = panic "pure analysis asked for a rewrite depth"
457 -----------------------------------------------------------------------
459 -- Here beginneth the super-general functions
461 -- Think of them as (typechecked) macros
462 -- * They are not exported
464 -- * They are called by the specialised wrappers
465 -- above, and always inlined into their callers
467 -- There are four functions, one for each combination of:
471 -- A "solver" produces a (DFM f (f, Fuel)),
472 -- where f is the fact at entry(Bwd)/exit(Fwd)
473 -- and from the DFM you can extract
478 -- A "rewriter" produces a rewritten *Graph* as well
480 -- Both constrain their rewrites by
482 -- b) RewritingDepth: shallow/deep
484 -----------------------------------------------------------------------
486 type Fuel = OptimizationFuel
490 (DebugNodes m l, LastNode l, Outputable a)
491 => (forall a . Fuel -> Maybe a -> Maybe a)
492 -- Squashes proposed rewrites if there is
493 -- no more fuel; OR if we are doing a pure
494 -- analysis, so totally ignore the rewrite
495 -- ie. For pure-analysis the fn is (\_ _ -> Nothing)
496 -> RewritingDepth -- Shallow/deep
498 -> BlockEnv a -- Initial set of facts
499 -> ForwardTransfers m l a
500 -> ForwardRewrites m l a
504 -> DFM a (ForwardFixedPoint m l a (), Fuel)
505 forward_sol check_maybe = forw
507 forw :: RewritingDepth
510 -> ForwardTransfers m l a
511 -> ForwardRewrites m l a
515 -> DFM a (ForwardFixedPoint m l a (), Fuel)
516 forw rewrite name start_facts transfers rewrites =
517 let anal_f :: DFM a b -> a -> Graph m l -> DFM a b
518 anal_f finish in' g =
519 do { fwd_pure_anal name emptyBlockEnv transfers in' g; finish }
521 solve :: DFM a b -> a -> Graph m l -> Fuel -> DFM a (b, Fuel)
522 solve finish in_fact (Graph entry blockenv) fuel =
523 let blocks = G.postorder_dfs_from blockenv entry
524 set_or_save = mk_set_or_save (isJust . lookupBlockEnv blockenv)
525 set_successor_facts (Block id _ tail) fuel =
526 do { idfact <- getFact id
527 ; (last_outs, fuel) <-
528 case check_maybe fuel $ fr_first rewrites idfact id of
529 Nothing -> solve_tail (ft_first_out transfers idfact id) tail fuel
532 (a, fuel) <- subAnalysis' $
534 RewriteDeep -> solve getExitFact idfact g (oneLessFuel fuel)
536 do { a <- anal_f getExitFact idfact g
537 ; return (a, oneLessFuel fuel) }
538 solve_tail a tail fuel
539 ; set_or_save last_outs
542 in do { (last_outs, fuel) <- solve_tail in_fact entry fuel
543 ; set_or_save last_outs
544 ; fuel <- run "forward" name set_successor_facts blocks fuel
549 solve_tail in' (G.ZTail m t) fuel =
550 case check_maybe fuel $ fr_middle rewrites in' m of
551 Nothing -> solve_tail (ft_middle_out transfers in' m) t fuel
554 ; (a, fuel) <- subAnalysis' $
556 RewriteDeep -> solve getExitFact in' g (oneLessFuel fuel)
557 RewriteShallow -> do { a <- anal_f getExitFact in' g
558 ; return (a, oneLessFuel fuel) }
559 ; solve_tail a t fuel
561 solve_tail in' (G.ZLast l) fuel =
562 case check_maybe fuel $ either_last rewrites in' l of
564 case l of LastOther l -> return (ft_last_outs transfers in' l, fuel)
565 LastExit -> do { setExitFact (ft_exit_out transfers in')
566 ; return (LastOutFacts [], fuel) }
569 ; (last_outs :: LastOutFacts a, fuel) <- subAnalysis' $
571 RewriteDeep -> solve lastOutFacts in' g (oneLessFuel fuel)
572 RewriteShallow -> do { los <- anal_f lastOutFacts in' g
573 ; return (los, fuel) }
574 ; return (last_outs, fuel)
577 fixed_point in_fact g fuel =
578 do { setAllFacts start_facts
579 ; (a, fuel) <- solve getExitFact in_fact g fuel
580 ; facts <- getAllFacts
581 ; last_outs <- lastOutFacts
582 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
583 ; let fp = FFP cfp last_outs
587 either_last rewrites in' (LastExit) = fr_exit rewrites in'
588 either_last rewrites in' (LastOther l) = fr_last rewrites in' l
595 mk_set_or_save :: (DataflowAnalysis df, Monad (df a), Outputable a) =>
596 (BlockId -> Bool) -> LastOutFacts a -> df a ()
597 mk_set_or_save is_local (LastOutFacts l) = mapM_ set_or_save_one l
598 where set_or_save_one (id, a) =
599 if is_local id then setFact id a else addLastOutFact (id, a)
605 (DebugNodes m l, LastNode l, Outputable a)
606 => (forall a . Fuel -> Maybe a -> Maybe a)
610 -> ForwardTransfers m l a
611 -> ForwardRewrites m l a
615 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
616 forward_rew check_maybe = forw
618 solve = forward_sol check_maybe
619 forw :: RewritingDepth
622 -> ForwardTransfers m l a
623 -> ForwardRewrites m l a
627 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
628 forw depth xstart_facts name transfers rewrites in_factx gx fuelx =
629 let rewrite :: BlockEnv a -> DFM a b
630 -> a -> Graph m l -> Fuel
631 -> DFM a (b, Graph m l, Fuel)
632 rewrite start finish in_fact g fuel =
633 let Graph entry blockenv = g
634 blocks = G.postorder_dfs_from blockenv entry
635 in do { solve depth name start transfers rewrites in_fact g fuel
636 ; eid <- freshBlockId "temporary entry id"
637 ; (rewritten, fuel) <-
638 rew_tail (ZFirst eid emptyStackInfo)
639 in_fact entry emptyBlockEnv fuel
640 ; (rewritten, fuel) <- rewrite_blocks blocks rewritten fuel
642 ; return (a, lgraphToGraph (LGraph eid 0 rewritten), fuel)
644 don't_rewrite facts finish in_fact g fuel =
645 do { solve depth name facts transfers rewrites in_fact g fuel
647 ; return (a, g, fuel)
649 inner_rew :: DFM a f -> a -> Graph m l -> Fuel -> DFM a (f, Graph m l, Fuel)
650 inner_rew f i g fu = getAllFacts >>= \facts -> inner_rew' facts f i g fu
651 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
652 RewriteDeep -> rewrite
654 do { (a, g, fuel) <- rewrite xstart_facts getExitFact in_factx gx fuelx
655 ; facts <- getAllFacts
656 ; changed <- graphWasRewritten
657 ; last_outs <- lastOutFacts
658 ; let cfp = FP facts a changed (panic "no decoration?!") g
659 ; let fp = FFP cfp last_outs
662 rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
663 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
664 rewrite_blocks [] rewritten fuel = return (rewritten, fuel)
665 rewrite_blocks (G.Block id off t : bs) rewritten fuel =
666 do let h = ZFirst id off
668 case check_maybe fuel $ fr_first rewrites a id of
669 Nothing -> do { (rewritten, fuel) <-
670 rew_tail h (ft_first_out transfers a id)
672 ; rewrite_blocks bs rewritten fuel }
673 Just g -> do { markGraphRewritten
675 ; (outfact, g, fuel) <- inner_rew getExitFact a g fuel
676 ; let (blocks, h) = splice_head' h g
677 ; (rewritten, fuel) <-
678 rew_tail h outfact t (blocks `plusBlockEnv` rewritten) fuel
679 ; rewrite_blocks bs rewritten fuel }
681 rew_tail head in' (G.ZTail m t) rewritten fuel =
682 my_trace "Rewriting middle node" (ppr m) $
683 case check_maybe fuel $ fr_middle rewrites in' m of
684 Nothing -> rew_tail (G.ZHead head m) (ft_middle_out transfers in' m) t
686 Just g -> do { markGraphRewritten
688 ; (a, g, fuel) <- inner_rew getExitFact in' g fuel
689 ; let (blocks, h) = G.splice_head' head g
690 ; rew_tail h a t (blocks `plusBlockEnv` rewritten) fuel
692 rew_tail h in' (G.ZLast l) rewritten fuel =
693 my_trace "Rewriting last node" (ppr l) $
694 case check_maybe fuel $ either_last rewrites in' l of
695 Nothing -> do check_facts in' l
696 return (insertBlock (zipht h (G.ZLast l)) rewritten, fuel)
697 Just g -> do { markGraphRewritten
699 ; ((), g, fuel) <- inner_rew (return ()) in' g fuel
700 ; let g' = G.splice_head_only' h g
701 ; return (G.lg_blocks g' `plusBlockEnv` rewritten, fuel)
703 either_last rewrites in' (LastExit) = fr_exit rewrites in'
704 either_last rewrites in' (LastOther l) = fr_last rewrites in' l
705 check_facts in' (LastOther l) =
706 let LastOutFacts last_outs = ft_last_outs transfers in' l
707 in mapM (uncurry checkFactMatch) last_outs
708 check_facts _ LastExit = return []
711 lastOutFacts :: DFM f (LastOutFacts f)
712 lastOutFacts = bareLastOutFacts >>= return . LastOutFacts
714 {- ================================================================ -}
716 solve_b :: (DebugNodes m l, Outputable a)
717 => BlockEnv a -- initial facts (unbound == bottom)
719 -> DataflowLattice a -- lattice
720 -> BackwardTransfers m l a -- dataflow transfer functions
722 -> Graph m l -- graph to be analyzed
723 -> FuelMonad (BackwardFixedPoint m l a ()) -- answers
724 solve_b env name lattice transfers exit_fact g =
725 runDFM lattice $ bwd_pure_anal name env transfers g exit_fact
728 rewrite_b_agraph :: (DebugNodes m l, Outputable a)
733 -> BackwardTransfers m l a
734 -> BackwardRewrites m l a
735 -> a -- fact flowing in at exit
737 -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
738 rewrite_b_agraph depth start_facts name lattice transfers rewrites exit_fact g =
740 do fuel <- fuelRemaining
741 (fp, fuel') <- backward_rew maybeRewriteWithFuel depth start_facts name
742 transfers rewrites g exit_fact fuel
743 fuelDecrement name fuel fuel'
750 (DebugNodes m l, LastNode l, Outputable a)
751 => (forall a . Fuel -> Maybe a -> Maybe a)
755 -> BackwardTransfers m l a
756 -> BackwardRewrites m l a
760 -> DFM a (BackwardFixedPoint m l a (), Fuel)
761 backward_sol check_maybe = back
763 back :: RewritingDepth
766 -> BackwardTransfers m l a
767 -> BackwardRewrites m l a
771 -> DFM a (BackwardFixedPoint m l a (), Fuel)
772 back rewrite name start_facts transfers rewrites =
773 let anal_b :: Graph m l -> a -> DFM a a
775 do { fp <- bwd_pure_anal name emptyBlockEnv transfers g out
776 ; return $ zdfFpOutputFact fp }
778 subsolve :: AGraph m l -> a -> Fuel -> DFM a (a, Fuel)
781 RewriteDeep -> \g a fuel ->
782 subAnalysis' $ do { g <- areturn g; solve g a (oneLessFuel fuel) }
783 RewriteShallow -> \g a fuel ->
784 subAnalysis' $ do { g <- areturn g; a <- anal_b g a
785 ; return (a, oneLessFuel fuel) }
787 solve :: Graph m l -> a -> Fuel -> DFM a (a, Fuel)
788 solve (Graph entry blockenv) exit_fact fuel =
789 let blocks = reverse $ G.postorder_dfs_from blockenv entry
790 last_in _env (LastExit) = exit_fact
791 last_in env (LastOther l) = bt_last_in transfers env l
792 last_rew _env (LastExit) = br_exit rewrites
793 last_rew env (LastOther l) = br_last rewrites env l
794 set_block_fact block fuel =
795 let (h, l) = G.goto_end (G.unzip block) in
798 case check_maybe fuel $ last_rew env l of
799 Nothing -> return (last_in env l, fuel)
800 Just g -> do g' <- areturn g
801 my_trace "analysis rewrites last node"
802 (ppr l <+> pprGraph g') $
803 subsolve g exit_fact fuel
804 ; set_head_fact h a fuel
807 in do { fuel <- run "backward" name set_block_fact blocks fuel
808 ; eid <- freshBlockId "temporary entry id"
809 ; fuel <- set_block_fact (Block eid emptyStackInfo entry) fuel
815 set_head_fact (G.ZFirst id _) a fuel =
816 case check_maybe fuel $ br_first rewrites a id of
817 Nothing -> do { my_trace "set_head_fact" (ppr id <+> text "=" <+>
818 ppr (bt_first_in transfers a id)) $
819 setFact id $ bt_first_in transfers a id
821 Just g -> do { g' <- areturn g
822 ; (a, fuel) <- my_trace "analysis rewrites first node"
823 (ppr id <+> pprGraph g') $
825 ; setFact id $ bt_first_in transfers a id
828 set_head_fact (G.ZHead h m) a fuel =
829 case check_maybe fuel $ br_middle rewrites a m of
830 Nothing -> set_head_fact h (bt_middle_in transfers a m) fuel
831 Just g -> do { g' <- areturn g
832 ; (a, fuel) <- my_trace "analysis rewrites middle node"
833 (ppr m <+> pprGraph g') $
835 ; set_head_fact h a fuel }
837 fixed_point g exit_fact fuel =
838 do { setAllFacts start_facts
839 ; (a, fuel) <- solve g exit_fact fuel
840 ; facts <- getAllFacts
841 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
846 bwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
849 -> BackwardTransfers m l a
852 -> DFM a (BackwardFixedPoint m l a ())
854 bwd_pure_anal name env transfers g exit_fact =
855 do (fp, _) <- anal_b name env transfers panic_rewrites g exit_fact panic_fuel
857 where -- another case of "I love lazy evaluation"
858 anal_b = backward_sol (\_ _ -> Nothing) panic_depth
859 panic_rewrites = panic "pure analysis asked for a rewrite function"
860 panic_fuel = panic "pure analysis asked for fuel"
861 panic_depth = panic "pure analysis asked for a rewrite depth"
864 {- ================================================================ -}
868 (DebugNodes m l, LastNode l, Outputable a)
869 => (forall a . Fuel -> Maybe a -> Maybe a)
873 -> BackwardTransfers m l a
874 -> BackwardRewrites m l a
878 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
879 backward_rew check_maybe = back
881 solve = backward_sol check_maybe
882 back :: RewritingDepth
885 -> BackwardTransfers m l a
886 -> BackwardRewrites m l a
890 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
891 back depth xstart_facts name transfers rewrites gx exit_fact fuelx =
892 let rewrite :: BlockEnv a
893 -> Graph m l -> a -> Fuel
894 -> DFM a (a, Graph m l, Fuel)
895 rewrite start g exit_fact fuel =
896 let Graph entry blockenv = g
897 blocks = reverse $ G.postorder_dfs_from blockenv entry
898 in do { (FP _ in_fact _ _ _, _) <- -- don't drop the entry fact!
899 solve depth name start transfers rewrites g exit_fact fuel
900 --; env <- getAllFacts
901 -- ; my_trace "facts after solving" (ppr env) $ return ()
902 ; eid <- freshBlockId "temporary entry id"
903 ; (rewritten, fuel) <- rewrite_blocks True blocks emptyBlockEnv fuel
904 -- We can't have the fact check fail on the bogus entry, which _may_ change
905 ; (rewritten, fuel) <-
906 rewrite_blocks False [Block eid emptyStackInfo entry]
908 ; my_trace "eid" (ppr eid) $ return ()
909 ; my_trace "exit_fact" (ppr exit_fact) $ return ()
910 ; my_trace "in_fact" (ppr in_fact) $ return ()
911 ; return (in_fact, lgraphToGraph (LGraph eid 0 rewritten), fuel)
912 } -- Remember: the entry fact computed by @solve@ accounts for rewriting
913 don't_rewrite facts g exit_fact fuel =
915 solve depth name facts transfers rewrites g exit_fact fuel
916 ; return (zdfFpOutputFact fp, g, fuel) }
917 inner_rew :: Graph m l -> a -> Fuel -> DFM a (a, Graph m l, Fuel)
918 inner_rew g a f = getAllFacts >>= \facts -> inner_rew' facts g a f
919 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
920 RewriteDeep -> rewrite
922 do { (a, g, fuel) <- rewrite xstart_facts gx exit_fact fuelx
923 ; facts <- getAllFacts
924 ; changed <- graphWasRewritten
925 ; let fp = FP facts a changed (panic "no decoration?!") g
928 rewrite_blocks :: Bool -> [Block m l] -> (BlockEnv (Block m l))
929 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
930 rewrite_blocks check bs rewritten fuel =
932 ; let rew [] r f = return (r, f)
934 do { (r, f) <- rewrite_block check env b r f; rew bs r f }
935 ; rew bs rewritten fuel }
936 rewrite_block check env b rewritten fuel =
937 let (h, l) = G.goto_end (G.unzip b) in
938 case maybeRewriteWithFuel fuel $ either_last env l of
939 Nothing -> propagate check fuel h (last_in env l) (ZLast l) rewritten
941 do { markGraphRewritten
943 ; (a, g, fuel) <- inner_rew g exit_fact fuel
944 ; let G.Graph t new_blocks = g
945 ; let rewritten' = new_blocks `plusBlockEnv` rewritten
946 ; propagate check fuel h a t rewritten' -- continue at entry of g
948 either_last _env (LastExit) = br_exit rewrites
949 either_last env (LastOther l) = br_last rewrites env l
950 last_in _env (LastExit) = exit_fact
951 last_in env (LastOther l) = bt_last_in transfers env l
952 propagate check fuel (ZHead h m) a tail rewritten =
953 case maybeRewriteWithFuel fuel $ br_middle rewrites a m of
955 propagate check fuel h (bt_middle_in transfers a m) (ZTail m tail) rewritten
957 do { markGraphRewritten
959 ; my_trace "With Facts" (ppr a) $ return ()
960 ; my_trace " Rewrote middle node"
961 (f4sep [ppr m, text "to", pprGraph g]) $
963 ; (a, g, fuel) <- inner_rew g a fuel
964 ; let Graph t newblocks = G.splice_tail g tail
965 ; my_trace "propagating facts" (ppr a) $
966 propagate check fuel h a t (newblocks `plusBlockEnv` rewritten) }
967 propagate check fuel (ZFirst id off) a tail rewritten =
968 case maybeRewriteWithFuel fuel $ br_first rewrites a id of
969 Nothing -> do { if check then
970 checkFactMatch id $ bt_first_in transfers a id
972 ; return (insertBlock (Block id off tail) rewritten, fuel) }
974 do { markGraphRewritten
976 ; my_trace "Rewrote first node"
977 (f4sep [ppr id <> colon, text "to", pprGraph g]) $ return ()
978 ; (a, g, fuel) <- inner_rew g a fuel
979 ; if check then checkFactMatch id (bt_first_in transfers a id)
981 ; let Graph t newblocks = G.splice_tail g tail
982 ; let r = insertBlock (Block id off t) (newblocks `plusBlockEnv` rewritten)
986 {- ================================================================ -}
988 instance FixedPoint CommonFixedPoint where
989 zdfFpFacts = fp_facts
990 zdfFpOutputFact = fp_out
991 zdfGraphChanged = fp_changed
992 zdfDecoratedGraph = fp_dec_graph
993 zdfFpContents = fp_contents
994 zdfFpMap f (FP fs out ch dg a) = FP fs out ch dg (f a)
996 instance FixedPoint ForwardFixedPoint where
997 zdfFpFacts = fp_facts . ffp_common
998 zdfFpOutputFact = fp_out . ffp_common
999 zdfGraphChanged = fp_changed . ffp_common
1000 zdfDecoratedGraph = fp_dec_graph . ffp_common
1001 zdfFpContents = fp_contents . ffp_common
1002 zdfFpMap f (FFP fp los) = FFP (zdfFpMap f fp) los
1008 my_trace :: String -> SDoc -> a -> a
1009 my_trace = if dump_things then pprTrace else \_ _ a -> a
1012 -- | Here's a function to run an action on blocks until we reach a fixed point.
1013 run :: (Outputable a, DebugNodes m l) =>
1014 String -> String -> (Block m l -> b -> DFM a b) -> [Block m l] -> b -> DFM a b
1015 run dir name do_block blocks b =
1016 do { show_blocks $ iterate (1::Int) }
1018 -- N.B. Each iteration starts with the same transaction limit;
1019 -- only the rewrites in the final iteration actually count
1020 trace_block (b, cnt) block =
1021 do b' <- my_trace "about to do" (text name <+> text "on" <+>
1022 ppr (blockId block) <+> ppr cnt) $
1024 return (b', cnt + 1)
1026 do { markFactsUnchanged
1028 my_trace "block count:" (ppr (length blocks)) $
1029 foldM trace_block (b, 0 :: Int) blocks
1030 ; changed <- factsStatus
1031 ; facts <- getAllFacts
1032 ; let depth = 0 -- was nesting depth
1035 NoChange -> unchanged depth $ return b
1037 pprFacts depth n facts $
1038 if n < 1000 then iterate (n+1)
1041 msg n = concat [name, " didn't converge in ", show n, " " , dir,
1043 my_nest depth sdoc = my_trace "" $ nest (3*depth) sdoc
1044 ppIter depth n = my_nest depth (empty $$ text "*************** iteration" <+> pp_i n)
1045 pp_i n = int n <+> text "of" <+> text name <+> text "on" <+> graphId
1047 my_nest depth (text "facts for" <+> graphId <+> text "are unchanged")
1049 graphId = case blocks of { Block id _ _ : _ -> ppr id ; [] -> text "<empty>" }
1050 show_blocks = my_trace "Blocks:" (vcat (map pprBlock blocks))
1051 pprBlock (Block id off t) = nest 2 (pprFact' (id, off, t))
1052 pprFacts depth n env =
1053 my_nest depth (text "facts for iteration" <+> pp_i n <+> text "are:" $$
1054 (nest 2 $ vcat $ map pprFact $ blockEnvToList env))
1055 pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)
1056 pprFact' (id, off, a) = hang (ppr id <> parens (ppr off) <> colon) 4 (ppr a)
1059 f4sep :: [SDoc] -> SDoc
1061 f4sep (d:ds) = fsep (d : map (nest 4) ds)
1064 subAnalysis' :: (Monad (m f), DataflowAnalysis m, Outputable f) =>
1067 do { a <- subAnalysis $
1068 do { a <- m; -- facts <- getAllFacts
1069 ; -- my_trace "after sub-analysis facts are" (pprFacts facts) $
1071 -- ; facts <- getAllFacts
1072 ; -- my_trace "in parent analysis facts are" (pprFacts facts) $
1074 -- where pprFacts env = nest 2 $ vcat $ map pprFact $ blockEnvToList env
1075 -- pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)