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
488 {-# INLINE forward_sol #-}
491 (DebugNodes m l, LastNode l, Outputable a)
492 => (forall a . Fuel -> Maybe a -> Maybe a)
493 -- Squashes proposed rewrites if there is
494 -- no more fuel; OR if we are doing a pure
495 -- analysis, so totally ignore the rewrite
496 -- ie. For pure-analysis the fn is (\_ _ -> Nothing)
497 -> RewritingDepth -- Shallow/deep
499 -> BlockEnv a -- Initial set of facts
500 -> ForwardTransfers m l a
501 -> ForwardRewrites m l a
505 -> DFM a (ForwardFixedPoint m l a (), Fuel)
506 forward_sol check_maybe = forw
508 forw :: RewritingDepth
511 -> ForwardTransfers m l a
512 -> ForwardRewrites m l a
516 -> DFM a (ForwardFixedPoint m l a (), Fuel)
517 forw rewrite name start_facts transfers rewrites =
518 let anal_f :: DFM a b -> a -> Graph m l -> DFM a b
519 anal_f finish in' g =
520 do { fwd_pure_anal name emptyBlockEnv transfers in' g; finish }
522 solve :: DFM a b -> a -> Graph m l -> Fuel -> DFM a (b, Fuel)
523 solve finish in_fact (Graph entry blockenv) fuel =
524 let blocks = G.postorder_dfs_from blockenv entry
525 set_or_save = mk_set_or_save (isJust . lookupBlockEnv blockenv)
526 set_successor_facts (Block id _ tail) fuel =
527 do { idfact <- getFact id
528 ; (last_outs, fuel) <-
529 case check_maybe fuel $ fr_first rewrites idfact id of
530 Nothing -> solve_tail (ft_first_out transfers idfact id) tail fuel
533 (a, fuel) <- subAnalysis' $
535 RewriteDeep -> solve getExitFact idfact g (oneLessFuel fuel)
537 do { a <- anal_f getExitFact idfact g
538 ; return (a, oneLessFuel fuel) }
539 solve_tail a tail fuel
540 ; set_or_save last_outs
543 in do { (last_outs, fuel) <- solve_tail in_fact entry fuel
544 ; set_or_save last_outs
545 ; fuel <- run "forward" name set_successor_facts blocks fuel
550 solve_tail in' (G.ZTail m t) fuel =
551 case check_maybe fuel $ fr_middle rewrites in' m of
552 Nothing -> solve_tail (ft_middle_out transfers in' m) t fuel
555 ; (a, fuel) <- subAnalysis' $
557 RewriteDeep -> solve getExitFact in' g (oneLessFuel fuel)
558 RewriteShallow -> do { a <- anal_f getExitFact in' g
559 ; return (a, oneLessFuel fuel) }
560 ; solve_tail a t fuel
562 solve_tail in' (G.ZLast l) fuel =
563 case check_maybe fuel $ either_last rewrites in' l of
565 case l of LastOther l -> return (ft_last_outs transfers in' l, fuel)
566 LastExit -> do { setExitFact (ft_exit_out transfers in')
567 ; return (LastOutFacts [], fuel) }
570 ; (last_outs :: LastOutFacts a, fuel) <- subAnalysis' $
572 RewriteDeep -> solve lastOutFacts in' g (oneLessFuel fuel)
573 RewriteShallow -> do { los <- anal_f lastOutFacts in' g
574 ; return (los, fuel) }
575 ; return (last_outs, fuel)
578 fixed_point in_fact g fuel =
579 do { setAllFacts start_facts
580 ; (a, fuel) <- solve getExitFact in_fact g fuel
581 ; facts <- getAllFacts
582 ; last_outs <- lastOutFacts
583 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
584 ; let fp = FFP cfp last_outs
588 either_last rewrites in' (LastExit) = fr_exit rewrites in'
589 either_last rewrites in' (LastOther l) = fr_last rewrites in' l
596 mk_set_or_save :: (DataflowAnalysis df, Monad (df a), Outputable a) =>
597 (BlockId -> Bool) -> LastOutFacts a -> df a ()
598 mk_set_or_save is_local (LastOutFacts l) = mapM_ set_or_save_one l
599 where set_or_save_one (id, a) =
600 if is_local id then setFact id a else addLastOutFact (id, a)
605 {-# INLINE forward_rew #-}
608 (DebugNodes m l, LastNode l, Outputable a)
609 => (forall a . Fuel -> Maybe a -> Maybe a)
613 -> ForwardTransfers m l a
614 -> ForwardRewrites m l a
618 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
619 forward_rew check_maybe = forw
621 solve = forward_sol check_maybe
622 forw :: RewritingDepth
625 -> ForwardTransfers m l a
626 -> ForwardRewrites m l a
630 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
631 forw depth xstart_facts name transfers rewrites in_factx gx fuelx =
632 let rewrite :: BlockEnv a -> DFM a b
633 -> a -> Graph m l -> Fuel
634 -> DFM a (b, Graph m l, Fuel)
635 rewrite start finish in_fact g fuel =
636 let Graph entry blockenv = g
637 blocks = G.postorder_dfs_from blockenv entry
638 in do { solve depth name start transfers rewrites in_fact g fuel
639 ; eid <- freshBlockId "temporary entry id"
640 ; (rewritten, fuel) <-
641 rew_tail (ZFirst eid emptyStackInfo)
642 in_fact entry emptyBlockEnv fuel
643 ; (rewritten, fuel) <- rewrite_blocks blocks rewritten fuel
645 ; return (a, lgraphToGraph (LGraph eid 0 rewritten), fuel)
647 don't_rewrite facts finish in_fact g fuel =
648 do { solve depth name facts transfers rewrites in_fact g fuel
650 ; return (a, g, fuel)
652 inner_rew :: DFM a f -> a -> Graph m l -> Fuel -> DFM a (f, Graph m l, Fuel)
653 inner_rew f i g fu = getAllFacts >>= \facts -> inner_rew' facts f i g fu
654 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
655 RewriteDeep -> rewrite
657 do { (a, g, fuel) <- rewrite xstart_facts getExitFact in_factx gx fuelx
658 ; facts <- getAllFacts
659 ; changed <- graphWasRewritten
660 ; last_outs <- lastOutFacts
661 ; let cfp = FP facts a changed (panic "no decoration?!") g
662 ; let fp = FFP cfp last_outs
665 rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
666 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
667 rewrite_blocks [] rewritten fuel = return (rewritten, fuel)
668 rewrite_blocks (G.Block id off t : bs) rewritten fuel =
669 do let h = ZFirst id off
671 case check_maybe fuel $ fr_first rewrites a id of
672 Nothing -> do { (rewritten, fuel) <-
673 rew_tail h (ft_first_out transfers a id)
675 ; rewrite_blocks bs rewritten fuel }
676 Just g -> do { markGraphRewritten
678 ; (outfact, g, fuel) <- inner_rew getExitFact a g fuel
679 ; let (blocks, h) = splice_head' h g
680 ; (rewritten, fuel) <-
681 rew_tail h outfact t (blocks `plusBlockEnv` rewritten) fuel
682 ; rewrite_blocks bs rewritten fuel }
684 rew_tail head in' (G.ZTail m t) rewritten fuel =
685 my_trace "Rewriting middle node" (ppr m) $
686 case check_maybe fuel $ fr_middle rewrites in' m of
687 Nothing -> rew_tail (G.ZHead head m) (ft_middle_out transfers in' m) t
689 Just g -> do { markGraphRewritten
691 ; (a, g, fuel) <- inner_rew getExitFact in' g fuel
692 ; let (blocks, h) = G.splice_head' head g
693 ; rew_tail h a t (blocks `plusBlockEnv` rewritten) fuel
695 rew_tail h in' (G.ZLast l) rewritten fuel =
696 my_trace "Rewriting last node" (ppr l) $
697 case check_maybe fuel $ either_last rewrites in' l of
698 Nothing -> do check_facts in' l
699 return (insertBlock (zipht h (G.ZLast l)) rewritten, fuel)
700 Just g -> do { markGraphRewritten
702 ; ((), g, fuel) <- inner_rew (return ()) in' g fuel
703 ; let g' = G.splice_head_only' h g
704 ; return (G.lg_blocks g' `plusBlockEnv` rewritten, fuel)
706 either_last rewrites in' (LastExit) = fr_exit rewrites in'
707 either_last rewrites in' (LastOther l) = fr_last rewrites in' l
708 check_facts in' (LastOther l) =
709 let LastOutFacts last_outs = ft_last_outs transfers in' l
710 in mapM (uncurry checkFactMatch) last_outs
711 check_facts _ LastExit = return []
714 lastOutFacts :: DFM f (LastOutFacts f)
715 lastOutFacts = bareLastOutFacts >>= return . LastOutFacts
717 {- ================================================================ -}
719 solve_b :: (DebugNodes m l, Outputable a)
720 => BlockEnv a -- initial facts (unbound == bottom)
722 -> DataflowLattice a -- lattice
723 -> BackwardTransfers m l a -- dataflow transfer functions
725 -> Graph m l -- graph to be analyzed
726 -> FuelMonad (BackwardFixedPoint m l a ()) -- answers
727 solve_b env name lattice transfers exit_fact g =
728 runDFM lattice $ bwd_pure_anal name env transfers g exit_fact
731 rewrite_b_agraph :: (DebugNodes m l, Outputable a)
736 -> BackwardTransfers m l a
737 -> BackwardRewrites m l a
738 -> a -- fact flowing in at exit
740 -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
741 rewrite_b_agraph depth start_facts name lattice transfers rewrites exit_fact g =
743 do fuel <- fuelRemaining
744 (fp, fuel') <- backward_rew maybeRewriteWithFuel depth start_facts name
745 transfers rewrites g exit_fact fuel
746 fuelDecrement name fuel fuel'
751 {-# INLINE backward_sol #-}
754 (DebugNodes m l, LastNode l, Outputable a)
755 => (forall a . Fuel -> Maybe a -> Maybe a)
759 -> BackwardTransfers m l a
760 -> BackwardRewrites m l a
764 -> DFM a (BackwardFixedPoint m l a (), Fuel)
765 backward_sol check_maybe = back
767 back :: RewritingDepth
770 -> BackwardTransfers m l a
771 -> BackwardRewrites m l a
775 -> DFM a (BackwardFixedPoint m l a (), Fuel)
776 back rewrite name start_facts transfers rewrites =
777 let anal_b :: Graph m l -> a -> DFM a a
779 do { fp <- bwd_pure_anal name emptyBlockEnv transfers g out
780 ; return $ zdfFpOutputFact fp }
782 subsolve :: AGraph m l -> a -> Fuel -> DFM a (a, Fuel)
785 RewriteDeep -> \g a fuel ->
786 subAnalysis' $ do { g <- areturn g; solve g a (oneLessFuel fuel) }
787 RewriteShallow -> \g a fuel ->
788 subAnalysis' $ do { g <- areturn g; a <- anal_b g a
789 ; return (a, oneLessFuel fuel) }
791 solve :: Graph m l -> a -> Fuel -> DFM a (a, Fuel)
792 solve (Graph entry blockenv) exit_fact fuel =
793 let blocks = reverse $ G.postorder_dfs_from blockenv entry
794 last_in _env (LastExit) = exit_fact
795 last_in env (LastOther l) = bt_last_in transfers env l
796 last_rew _env (LastExit) = br_exit rewrites
797 last_rew env (LastOther l) = br_last rewrites env l
798 set_block_fact block fuel =
799 let (h, l) = G.goto_end (G.unzip block) in
802 case check_maybe fuel $ last_rew env l of
803 Nothing -> return (last_in env l, fuel)
804 Just g -> do g' <- areturn g
805 my_trace "analysis rewrites last node"
806 (ppr l <+> pprGraph g') $
807 subsolve g exit_fact fuel
808 ; set_head_fact h a fuel
811 in do { fuel <- run "backward" name set_block_fact blocks fuel
812 ; eid <- freshBlockId "temporary entry id"
813 ; fuel <- set_block_fact (Block eid emptyStackInfo entry) fuel
819 set_head_fact (G.ZFirst id _) a fuel =
820 case check_maybe fuel $ br_first rewrites a id of
821 Nothing -> do { my_trace "set_head_fact" (ppr id <+> text "=" <+>
822 ppr (bt_first_in transfers a id)) $
823 setFact id $ bt_first_in transfers a id
825 Just g -> do { g' <- areturn g
826 ; (a, fuel) <- my_trace "analysis rewrites first node"
827 (ppr id <+> pprGraph g') $
829 ; setFact id $ bt_first_in transfers a id
832 set_head_fact (G.ZHead h m) a fuel =
833 case check_maybe fuel $ br_middle rewrites a m of
834 Nothing -> set_head_fact h (bt_middle_in transfers a m) fuel
835 Just g -> do { g' <- areturn g
836 ; (a, fuel) <- my_trace "analysis rewrites middle node"
837 (ppr m <+> pprGraph g') $
839 ; set_head_fact h a fuel }
841 fixed_point g exit_fact fuel =
842 do { setAllFacts start_facts
843 ; (a, fuel) <- solve g exit_fact fuel
844 ; facts <- getAllFacts
845 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
850 bwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
853 -> BackwardTransfers m l a
856 -> DFM a (BackwardFixedPoint m l a ())
858 bwd_pure_anal name env transfers g exit_fact =
859 do (fp, _) <- anal_b name env transfers panic_rewrites g exit_fact panic_fuel
861 where -- another case of "I love lazy evaluation"
862 anal_b = backward_sol (\_ _ -> Nothing) panic_depth
863 panic_rewrites = panic "pure analysis asked for a rewrite function"
864 panic_fuel = panic "pure analysis asked for fuel"
865 panic_depth = panic "pure analysis asked for a rewrite depth"
868 {- ================================================================ -}
870 {-# INLINE backward_rew #-}
873 (DebugNodes m l, LastNode l, Outputable a)
874 => (forall a . Fuel -> Maybe a -> Maybe a)
878 -> BackwardTransfers m l a
879 -> BackwardRewrites m l a
883 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
884 backward_rew check_maybe = back
886 solve = backward_sol check_maybe
887 back :: RewritingDepth
890 -> BackwardTransfers m l a
891 -> BackwardRewrites m l a
895 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
896 back depth xstart_facts name transfers rewrites gx exit_fact fuelx =
897 let rewrite :: BlockEnv a
898 -> Graph m l -> a -> Fuel
899 -> DFM a (a, Graph m l, Fuel)
900 rewrite start g exit_fact fuel =
901 let Graph entry blockenv = g
902 blocks = reverse $ G.postorder_dfs_from blockenv entry
903 in do { (FP env in_fact _ _ _, _) <- -- don't drop the entry fact!
904 solve depth name start transfers rewrites g exit_fact fuel
905 --; env <- getAllFacts
906 -- ; my_trace "facts after solving" (ppr env) $ return ()
907 ; eid <- freshBlockId "temporary entry id"
908 ; (rewritten, fuel) <- rewrite_blocks True blocks emptyBlockEnv fuel
909 -- We can't have the fact check fail on the bogus entry, which _may_ change
910 ; (rewritten, fuel) <-
911 rewrite_blocks False [Block eid emptyStackInfo entry]
913 ; my_trace "eid" (ppr eid) $ return ()
914 ; my_trace "exit_fact" (ppr exit_fact) $ return ()
915 ; my_trace "in_fact" (ppr in_fact) $ return ()
916 ; return (in_fact, lgraphToGraph (LGraph eid 0 rewritten), fuel)
917 } -- Remember: the entry fact computed by @solve@ accounts for rewriting
918 don't_rewrite facts g exit_fact fuel =
920 solve depth name facts transfers rewrites g exit_fact fuel
921 ; return (zdfFpOutputFact fp, g, fuel) }
922 inner_rew :: Graph m l -> a -> Fuel -> DFM a (a, Graph m l, Fuel)
923 inner_rew g a f = getAllFacts >>= \facts -> inner_rew' facts g a f
924 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
925 RewriteDeep -> rewrite
927 do { (a, g, fuel) <- rewrite xstart_facts gx exit_fact fuelx
928 ; facts <- getAllFacts
929 ; changed <- graphWasRewritten
930 ; let fp = FP facts a changed (panic "no decoration?!") g
933 rewrite_blocks :: Bool -> [Block m l] -> (BlockEnv (Block m l))
934 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
935 rewrite_blocks check bs rewritten fuel =
937 ; let rew [] r f = return (r, f)
939 do { (r, f) <- rewrite_block check env b r f; rew bs r f }
940 ; rew bs rewritten fuel }
941 rewrite_block check env b rewritten fuel =
942 let (h, l) = G.goto_end (G.unzip b) in
943 case maybeRewriteWithFuel fuel $ either_last env l of
944 Nothing -> propagate check fuel h (last_in env l) (ZLast l) rewritten
946 do { markGraphRewritten
948 ; (a, g, fuel) <- inner_rew g exit_fact fuel
949 ; let G.Graph t new_blocks = g
950 ; let rewritten' = new_blocks `plusBlockEnv` rewritten
951 ; propagate check fuel h a t rewritten' -- continue at entry of g
953 either_last _env (LastExit) = br_exit rewrites
954 either_last env (LastOther l) = br_last rewrites env l
955 last_in _env (LastExit) = exit_fact
956 last_in env (LastOther l) = bt_last_in transfers env l
957 propagate check fuel (ZHead h m) a tail rewritten =
958 case maybeRewriteWithFuel fuel $ br_middle rewrites a m of
960 propagate check fuel h (bt_middle_in transfers a m) (ZTail m tail) rewritten
962 do { markGraphRewritten
964 ; my_trace "With Facts" (ppr a) $ return ()
965 ; my_trace " Rewrote middle node"
966 (f4sep [ppr m, text "to", pprGraph g]) $
968 ; (a, g, fuel) <- inner_rew g a fuel
969 ; let Graph t newblocks = G.splice_tail g tail
970 ; my_trace "propagating facts" (ppr a) $
971 propagate check fuel h a t (newblocks `plusBlockEnv` rewritten) }
972 propagate check fuel (ZFirst id off) a tail rewritten =
973 case maybeRewriteWithFuel fuel $ br_first rewrites a id of
974 Nothing -> do { if check then
975 checkFactMatch id $ bt_first_in transfers a id
977 ; return (insertBlock (Block id off tail) rewritten, fuel) }
979 do { markGraphRewritten
981 ; my_trace "Rewrote first node"
982 (f4sep [ppr id <> colon, text "to", pprGraph g]) $ return ()
983 ; (a, g, fuel) <- inner_rew g a fuel
984 ; if check then checkFactMatch id (bt_first_in transfers a id)
986 ; let Graph t newblocks = G.splice_tail g tail
987 ; let r = insertBlock (Block id off t) (newblocks `plusBlockEnv` rewritten)
991 {- ================================================================ -}
993 instance FixedPoint CommonFixedPoint where
994 zdfFpFacts = fp_facts
995 zdfFpOutputFact = fp_out
996 zdfGraphChanged = fp_changed
997 zdfDecoratedGraph = fp_dec_graph
998 zdfFpContents = fp_contents
999 zdfFpMap f (FP fs out ch dg a) = FP fs out ch dg (f a)
1001 instance FixedPoint ForwardFixedPoint where
1002 zdfFpFacts = fp_facts . ffp_common
1003 zdfFpOutputFact = fp_out . ffp_common
1004 zdfGraphChanged = fp_changed . ffp_common
1005 zdfDecoratedGraph = fp_dec_graph . ffp_common
1006 zdfFpContents = fp_contents . ffp_common
1007 zdfFpMap f (FFP fp los) = FFP (zdfFpMap f fp) los
1013 my_trace :: String -> SDoc -> a -> a
1014 my_trace = if dump_things then pprTrace else \_ _ a -> a
1017 -- | Here's a function to run an action on blocks until we reach a fixed point.
1018 run :: (Outputable a, DebugNodes m l) =>
1019 String -> String -> (Block m l -> b -> DFM a b) -> [Block m l] -> b -> DFM a b
1020 run dir name do_block blocks b =
1021 do { show_blocks $ iterate (1::Int) }
1023 -- N.B. Each iteration starts with the same transaction limit;
1024 -- only the rewrites in the final iteration actually count
1025 trace_block (b, cnt) block =
1026 do b' <- my_trace "about to do" (text name <+> text "on" <+>
1027 ppr (blockId block) <+> ppr cnt) $
1029 return (b', cnt + 1)
1031 do { markFactsUnchanged
1033 my_trace "block count:" (ppr (length blocks)) $
1034 foldM trace_block (b, 0 :: Int) blocks
1035 ; changed <- factsStatus
1036 ; facts <- getAllFacts
1037 ; let depth = 0 -- was nesting depth
1040 NoChange -> unchanged depth $ return b
1042 pprFacts depth n facts $
1043 if n < 1000 then iterate (n+1)
1046 msg n = concat [name, " didn't converge in ", show n, " " , dir,
1048 my_nest depth sdoc = my_trace "" $ nest (3*depth) sdoc
1049 ppIter depth n = my_nest depth (empty $$ text "*************** iteration" <+> pp_i n)
1050 pp_i n = int n <+> text "of" <+> text name <+> text "on" <+> graphId
1052 my_nest depth (text "facts for" <+> graphId <+> text "are unchanged")
1054 graphId = case blocks of { Block id _ _ : _ -> ppr id ; [] -> text "<empty>" }
1055 show_blocks = my_trace "Blocks:" (vcat (map pprBlock blocks))
1056 pprBlock (Block id off t) = nest 2 (pprFact' (id, off, t))
1057 pprFacts depth n env =
1058 my_nest depth (text "facts for iteration" <+> pp_i n <+> text "are:" $$
1059 (nest 2 $ vcat $ map pprFact $ blockEnvToList env))
1060 pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)
1061 pprFact' (id, off, a) = hang (ppr id <> parens (ppr off) <> colon) 4 (ppr a)
1064 f4sep :: [SDoc] -> SDoc
1066 f4sep (d:ds) = fsep (d : map (nest 4) ds)
1069 subAnalysis' :: (Monad (m f), DataflowAnalysis m, Outputable f) =>
1072 do { a <- subAnalysis $
1073 do { a <- m; facts <- getAllFacts
1074 ; -- my_trace "after sub-analysis facts are" (pprFacts facts) $
1076 ; facts <- getAllFacts
1077 ; -- my_trace "in parent analysis facts are" (pprFacts facts) $
1079 where pprFacts env = nest 2 $ vcat $ map pprFact $ blockEnvToList env
1080 pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)