1 {-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables #-}
2 {-# OPTIONS -fno-allow-overlapping-instances -fglasgow-exts #-}
3 -- -fglagow-exts for kind signatures
6 ( DebugNodes(), RewritingDepth(..), LastOutFacts(..)
7 , zdfSolveFrom, zdfRewriteFrom
8 , ForwardTransfers(..), BackwardTransfers(..)
9 , ForwardRewrites(..), BackwardRewrites(..)
10 , ForwardFixedPoint, BackwardFixedPoint
14 , zdfDecoratedGraph -- not yet implemented
25 import qualified ZipCfg as G
37 This module implements two useful tools:
39 1. An iterative solver for dataflow problems
41 2. The combined dataflow-analysis-and-transformation framework
42 described by Lerner, Grove, and Chambers in their excellent
43 2002 POPL paper (http://tinyurl.com/3zycbr or
44 http://tinyurl.com/3pnscd).
46 Each tool comes in two flavors: one for forward dataflow problems
47 and one for backward dataflow problems.
49 We quote the paper above:
51 Dataflow analyses can have mutually beneficial interactions.
52 Previous efforts to exploit these interactions have either
53 (1) iteratively performed each individual analysis until no
54 further improvements are discovered or (2) developed "super-
55 analyses" that manually combine conceptually separate anal-
56 yses. We have devised a new approach that allows anal-
57 yses to be defined independently while still enabling them
58 to be combined automatically and profitably. Our approach
59 avoids the loss of precision associated with iterating indi-
60 vidual analyses and the implementation difficulties of man-
61 ually writing a super-analysis.
63 The key idea is to provide at each CFG node not only a dataflow
64 transfer function but also a rewriting function that has the option to
65 replace the node with a new (possibly empty) graph. The rewriting
66 function takes a dataflow fact as input, and the fact is used to
67 justify any rewriting. For example, in a backward problem, the fact
68 that variable x is dead can be used to justify rewriting node
70 to the empty graph. In a forward problem, the fact that x == 7 can
71 be used to justify rewriting node
75 which in turn will be analyzed and produce a new fact:
78 In its most general form, this module takes as input graph, transfer
79 equations, rewrites, and an initial set of dataflow facts, and
80 iteratively computes a new graph and a new set of dataflow facts such
82 * The set of facts is a fixed point of the transfer equations
83 * The graph has been rewritten as much as is consistent with
84 the given facts and requested rewriting depth (see below)
85 N.B. 'A set of facts' is shorthand for 'A finite map from CFG label to fact'.
87 The types of transfer equations, rewrites, and fixed points are
88 different for forward and backward problems. To avoid cluttering the
89 name space with two versions of every names, other names such as
90 zdfSolveFrom are overloaded to work in both forward or backward
91 directions. This design decision is based on experience with the
92 predecessor module, now called ZipDataflow0 and destined for the bit bucket.
95 This module is deliberately very abstract. It is a completely general
96 framework and well-nigh impossible to understand in isolation. The
97 cautious reader will begin with some concrete examples in the form of
98 clients. NR recommends
100 CmmLiveZ A simple liveness analysis
102 CmmSpillReload.removeDeadAssignmentsAndReloads
103 A piece of spaghetti to pull on, which leads to
104 - a two-part liveness analysis that tracks
105 variables live in registers and live on the stack
106 - elimination of assignments to dead variables
107 - elimination of redundant reloads
109 Even hearty souls should avoid the CmmProcPointZ client, at least for
115 {- ============ TRANSFER FUNCTIONS AND REWRITES =========== -}
117 -- | For a backward transfer, you're given the fact on a node's
118 -- outedge and you compute the fact on the inedge. Facts have type 'a'.
119 -- A last node may have multiple outedges, each pointing to a labelled
120 -- block, so instead of a fact it is given a mapping from BlockId to fact.
122 data BackwardTransfers middle last a = BackwardTransfers
123 { bt_first_in :: a -> BlockId -> a
124 , bt_middle_in :: a -> middle -> a
125 , bt_last_in :: (BlockId -> a) -> last -> a
128 -- | For a forward transfer, you're given the fact on a node's
129 -- inedge and you compute the fact on the outedge. Because a last node
130 -- may have multiple outedges, each pointing to a labelled
131 -- block, so instead of a fact it produces a list of (BlockId, fact) pairs.
133 data ForwardTransfers middle last a = ForwardTransfers
134 { ft_first_out :: a -> BlockId -> a
135 , ft_middle_out :: a -> middle -> a
136 , ft_last_outs :: a -> last -> LastOutFacts a
137 , ft_exit_out :: a -> a
140 newtype LastOutFacts a = LastOutFacts [(BlockId, a)]
141 -- ^ These are facts flowing out of a last node to the node's successors.
142 -- They are either to be set (if they pertain to the graph currently
143 -- under analysis) or propagated out of a sub-analysis
146 -- | A backward rewrite takes the same inputs as a backward transfer,
147 -- but instead of producing a fact, it produces a replacement graph or Nothing.
148 -- The type of the replacement graph is given as a type parameter 'g'
149 -- of kind * -> * -> *. This design offers great flexibility to clients,
150 -- but it might be worth simplifying this module by replacing this type
151 -- parameter with AGraph everywhere (SLPJ 19 May 2008).
153 data BackwardRewrites middle last a g = BackwardRewrites
154 { br_first :: a -> BlockId -> Maybe (g middle last)
155 , br_middle :: a -> middle -> Maybe (g middle last)
156 , br_last :: (BlockId -> a) -> last -> Maybe (g middle last)
157 , br_exit :: Maybe (g middle last)
160 -- | A forward rewrite takes the same inputs as a forward transfer,
161 -- but instead of producing a fact, it produces a replacement graph or Nothing.
163 data ForwardRewrites middle last a g = ForwardRewrites
164 { fr_first :: a -> BlockId -> Maybe (g middle last)
165 , fr_middle :: a -> middle -> Maybe (g middle last)
166 , fr_last :: a -> last -> Maybe (g middle last)
167 , fr_exit :: a -> Maybe (g middle last)
170 {- ===================== FIXED POINTS =================== -}
172 -- | The result of combined analysis and transformation is a
173 -- solution to the set of dataflow equations together with a 'contained value'.
174 -- This solution is a member of type class 'FixedPoint', which is parameterized by
175 -- * middle and last nodes 'm' and 'l'
176 -- * data flow fact 'fact'
177 -- * the type 'a' of the contained value
179 -- In practice, the contained value 'zdfFpContents' is either a
180 -- rewritten graph, when rewriting, or (), when solving without
181 -- rewriting. A function 'zdfFpMap' allows a client to change
182 -- the contents without changing other values.
184 -- To save space, we provide the solution 'zdfFpFacts' as a mapping
185 -- from BlockId to fact; if necessary, facts on edges can be
186 -- reconstructed using the transfer functions; this functionality is
187 -- intended to be included as the 'zdfDecoratedGraph', but the code
188 -- has not yet been implemented.
190 -- The solution may also includes a fact 'zdfFpOuputFact', which is
191 -- not associated with any label:
192 -- * for a backward problem, this is the fact at entry
193 -- * for a forward problem, this is the fact at the distinguished exit node,
194 -- if such a node is present
196 -- For a forward problem only, the solution includes 'zdfFpLastOuts',
197 -- which is the set of facts on edges leaving the graph.
199 -- The flag 'zdfGraphChanged' tells whether the engine did any rewriting.
201 class FixedPoint fp where
202 zdfFpContents :: fp m l fact a -> a
203 zdfFpFacts :: fp m l fact a -> BlockEnv fact
204 zdfFpOutputFact :: fp m l fact a -> fact -- entry for backward; exit for forward
205 zdfDecoratedGraph :: fp m l fact a -> Graph (fact, m) (fact, l)
206 zdfGraphChanged :: fp m l fact a -> ChangeFlag
207 zdfFpMap :: (a -> b) -> (fp m l fact a -> fp m l fact b)
209 -- | The class 'FixedPoint' has two instances: one for forward problems and
210 -- one for backward problems. The 'CommonFixedPoint' defines all fields
211 -- common to both. (The instance declarations are uninteresting and appear below.)
213 data CommonFixedPoint m l fact a = FP
214 { fp_facts :: BlockEnv fact
215 , fp_out :: fact -- entry for backward; exit for forward
216 , fp_changed :: ChangeFlag
217 , fp_dec_graph :: Graph (fact, m) (fact, l)
221 -- | The common fixed point is sufficient for a backward problem.
222 type BackwardFixedPoint = CommonFixedPoint
224 -- | A forward problem needs the common fields, plus the facts on the outedges.
225 data ForwardFixedPoint m l fact a = FFP
226 { ffp_common :: CommonFixedPoint m l fact a
227 , zdfFpLastOuts :: LastOutFacts fact
231 {- ============== SOLVING AND REWRITING ============== -}
233 type PassName = String
235 -- | zdfSolveFrom is an overloaded name that resolves to a pure
236 -- analysis with no rewriting. It has only two instances: forward and
237 -- backward. Since it needs no rewrites, the type parameters of the
238 -- class are transfer functions and the fixed point.
241 -- An iterative solver normally starts with the bottom fact at every
242 -- node, but it can be useful in other contexts as well. For this
243 -- reason the initial set of facts (at labelled blocks only) is a
244 -- parameter to the solver.
246 -- The constraints on the type signature exist purely for debugging;
247 -- they make it possible to prettyprint nodes and facts. The parameter of
248 -- type 'PassName' is also used just for debugging.
250 -- Note that the result is a fixed point with no contents, that is,
251 -- the contents have type ().
253 -- The intent of the rest of the type signature should be obvious.
254 -- If not, place a skype call to norman-ramsey or complain bitterly
255 -- to norman-ramsey@acm.org.
257 class DataflowSolverDirection transfers fixedpt where
258 zdfSolveFrom :: (DebugNodes m l, Outputable a)
259 => BlockEnv a -- Initial facts (unbound == bottom)
261 -> DataflowLattice a -- Lattice
262 -> transfers m l a -- Dataflow transfer functions
263 -> a -- Fact flowing in (at entry or exit)
264 -> Graph m l -- Graph to be analyzed
265 -> FuelMonad (fixedpt m l a ()) -- Answers
267 -- There are exactly two instances: forward and backward
268 instance DataflowSolverDirection ForwardTransfers ForwardFixedPoint
269 where zdfSolveFrom = solve_f
271 instance DataflowSolverDirection BackwardTransfers BackwardFixedPoint
272 where zdfSolveFrom = solve_b
275 -- | zdfRewriteFrom is an overloaded name that resolves to an
276 -- interleaved analysis and transformation. It too is instantiated in
277 -- forward and backward directions.
279 -- The type parameters of the class include not only transfer
280 -- functions and the fixed point but also rewrites and the type
281 -- constructor (here called 'graph') for making rewritten graphs. As
282 -- above, in the definitoins of the rewrites, it might simplify
283 -- matters if 'graph' were replaced with 'AGraph'.
285 -- The type signature of 'zdfRewriteFrom' is that of 'zdfSolveFrom'
286 -- with additional parameters and a different result. Of course the
287 -- rewrites are an additional parameter, but there are further
288 -- parameters which reflect the fact that rewriting consumes both
289 -- OptimizationFuel and Uniqs.
291 -- The result type is changed to reflect fuel consumption, and also
292 -- the resulting fixed point containts a rewritten graph.
294 -- John Dias is going to improve the management of Uniqs and Fuel so
295 -- that it doesn't make us sick to look at the types.
297 class DataflowSolverDirection transfers fixedpt =>
298 DataflowDirection transfers fixedpt rewrites
299 (graph :: * -> * -> *) where
300 zdfRewriteFrom :: (DebugNodes m l, Outputable a)
301 => RewritingDepth -- whether to rewrite a rewritten graph
302 -> BlockEnv a -- initial facts (unbound == botton)
306 -> rewrites m l a graph
307 -> a -- fact flowing in (at entry or exit)
309 -> FuelMonad (fixedpt m l a (Graph m l))
311 data RewritingDepth = RewriteShallow | RewriteDeep
312 -- When a transformation proposes to rewrite a node,
313 -- you can either ask the system to
314 -- * "shallow": accept the new graph, analyse it without further rewriting
315 -- * "deep": recursively analyse-and-rewrite the new graph
318 -- There are currently four instances, but there could be more
319 -- forward, backward (instantiates transfers, fixedpt, rewrites)
320 -- Graph, AGraph (instantiates graph)
322 instance DataflowDirection ForwardTransfers ForwardFixedPoint ForwardRewrites Graph
323 where zdfRewriteFrom = rewrite_f_graph
325 instance DataflowDirection ForwardTransfers ForwardFixedPoint ForwardRewrites AGraph
326 where zdfRewriteFrom = rewrite_f_agraph
328 instance DataflowDirection BackwardTransfers BackwardFixedPoint BackwardRewrites Graph
329 where zdfRewriteFrom = rewrite_b_graph
331 instance DataflowDirection BackwardTransfers BackwardFixedPoint BackwardRewrites AGraph
332 where zdfRewriteFrom = rewrite_b_agraph
335 {- =================== IMPLEMENTATIONS ===================== -}
338 -----------------------------------------------------------
339 -- solve_f: forward, pure
341 solve_f :: (DebugNodes m l, Outputable a)
342 => BlockEnv a -- initial facts (unbound == bottom)
344 -> DataflowLattice a -- lattice
345 -> ForwardTransfers m l a -- dataflow transfer functions
347 -> Graph m l -- graph to be analyzed
348 -> FuelMonad (ForwardFixedPoint m l a ()) -- answers
349 solve_f env name lattice transfers in_fact g =
350 runDFM lattice $ fwd_pure_anal name env transfers in_fact g
352 rewrite_f_graph :: (DebugNodes m l, Outputable a)
357 -> ForwardTransfers m l a
358 -> ForwardRewrites m l a Graph
359 -> a -- fact flowing in (at entry or exit)
361 -> FuelMonad (ForwardFixedPoint m l a (Graph m l))
362 rewrite_f_graph depth start_facts name lattice transfers rewrites in_fact g =
364 do fuel <- fuelRemaining
365 (fp, fuel') <- forward_rew maybeRewriteWithFuel return depth start_facts name
366 transfers rewrites in_fact g fuel
367 fuelDecrement name fuel fuel'
370 rewrite_f_agraph :: (DebugNodes m l, Outputable a)
375 -> ForwardTransfers m l a
376 -> ForwardRewrites m l a AGraph
377 -> a -- fact flowing in (at entry or exit)
379 -> FuelMonad (ForwardFixedPoint m l a (Graph m l))
380 rewrite_f_agraph depth start_facts name lattice transfers rewrites in_fact g =
382 do fuel <- fuelRemaining
383 (fp, fuel') <- forward_rew maybeRewriteWithFuel areturn depth start_facts name
384 transfers rewrites in_fact g fuel
385 fuelDecrement name fuel fuel'
388 areturn :: AGraph m l -> DFM a (Graph m l)
389 areturn g = liftToDFM $ liftUniq $ graphOfAGraph g
393 graphToLGraph :: LastNode l => Graph m l -> DFM a (LGraph m l)
394 graphToLGraph (Graph (ZLast (LastOther l)) blockenv)
395 | isBranchNode l = return $ LGraph (branchNodeTarget l) blockenv
396 graphToLGraph (Graph tail blockenv) =
397 do id <- freshBlockId "temporary entry label"
398 return $ LGraph id $ insertBlock (Block id tail) blockenv
401 -- | Here we prefer not simply to slap on 'goto eid' because this
402 -- introduces an unnecessary basic block at each rewrite, and we don't
403 -- want to stress out the finite map more than necessary
404 lgraphToGraph :: LastNode l => LGraph m l -> Graph m l
405 lgraphToGraph (LGraph eid blocks) =
406 if flip any (eltsUFM blocks) $ \block -> any (== eid) (succs block) then
407 Graph (ZLast (mkBranchNode eid)) blocks
408 else -- common case: entry is not a branch target
409 let Block _ entry = lookupBlockEnv blocks eid `orElse` panic "missing entry!"
410 in Graph entry (delFromUFM blocks eid)
413 class (Outputable m, Outputable l, LastNode l, Outputable (LGraph m l)) => DebugNodes m l
415 fwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
418 -> ForwardTransfers m l a
421 -> DFM a (ForwardFixedPoint m l a ())
423 fwd_pure_anal name env transfers in_fact g =
424 do (fp, _) <- anal_f name env transfers panic_rewrites in_fact g panic_fuel
426 where -- definitiely a case of "I love lazy evaluation"
427 anal_f = forward_sol (\_ _ -> Nothing) panic_return panic_depth
428 panic_rewrites = panic "pure analysis asked for a rewrite function"
429 panic_fuel = panic "pure analysis asked for fuel"
430 panic_return = panic "pure analysis tried to return a rewritten graph"
431 panic_depth = panic "pure analysis asked for a rewrite depth"
433 -----------------------------------------------------------------------
435 -- Here beginneth the super-general functions
437 -- Think of them as (typechecked) macros
438 -- * They are not exported
440 -- * They are called by the specialised wrappers
441 -- above, and always inlined into their callers
443 -- There are four functions, one for each combination of:
447 -- A "solver" produces a (DFM f (f, Fuel)),
448 -- where f is the fact at entry(Bwd)/exit(Fwd)
449 -- and from the DFM you can extract
454 -- A "rewriter" produces a rewritten *Graph* as well
456 -- Both constrain their rewrites by
458 -- b) RewritingDepth: shallow/deep
460 -----------------------------------------------------------------------
462 type Fuel = OptimizationFuel
464 {-# INLINE forward_sol #-}
467 (DebugNodes m l, LastNode l, Outputable a)
468 => (forall a . Fuel -> Maybe a -> Maybe a)
469 -- Squashes proposed rewrites if there is
470 -- no more fuel; OR if we are doing a pure
471 -- analysis, so totally ignore the rewrite
472 -- ie. For pure-analysis the fn is (\_ _ -> Nothing)
473 -> (g m l -> DFM a (Graph m l))
474 -- Transforms the kind of graph 'g' wanted by the
475 -- client (in ForwardRewrites) to the kind forward_sol likes
476 -> RewritingDepth -- Shallow/deep
478 -> BlockEnv a -- Initial set of facts
479 -> ForwardTransfers m l a
480 -> ForwardRewrites m l a g
484 -> DFM a (ForwardFixedPoint m l a (), Fuel)
485 forward_sol check_maybe return_graph = forw
487 forw :: RewritingDepth
490 -> ForwardTransfers m l a
491 -> ForwardRewrites m l a g
495 -> DFM a (ForwardFixedPoint m l a (), Fuel)
496 forw rewrite name start_facts transfers rewrites =
497 let anal_f :: DFM a b -> a -> Graph m l -> DFM a b
498 anal_f finish in' g =
499 do { fwd_pure_anal name emptyBlockEnv transfers in' g; finish }
501 solve :: DFM a b -> a -> Graph m l -> Fuel -> DFM a (b, Fuel)
502 solve finish in_fact (Graph entry blockenv) fuel =
503 let blocks = G.postorder_dfs_from blockenv entry
504 set_or_save = mk_set_or_save (isJust . lookupBlockEnv blockenv)
505 set_successor_facts (Block id tail) fuel =
506 do { idfact <- getFact id
507 ; (last_outs, fuel) <-
508 case check_maybe fuel $ fr_first rewrites idfact id of
509 Nothing -> solve_tail (ft_first_out transfers idfact id) tail fuel
511 do g <- return_graph g
512 (a, fuel) <- subAnalysis' $
514 RewriteDeep -> solve getExitFact idfact g (oneLessFuel fuel)
516 do { a <- anal_f getExitFact idfact g
517 ; return (a, oneLessFuel fuel) }
518 solve_tail a tail fuel
519 ; set_or_save last_outs
522 in do { (last_outs, fuel) <- solve_tail in_fact entry fuel
523 ; set_or_save last_outs
524 ; fuel <- run "forward" name set_successor_facts blocks fuel
529 solve_tail in' (G.ZTail m t) fuel =
530 case check_maybe fuel $ fr_middle rewrites in' m of
531 Nothing -> solve_tail (ft_middle_out transfers in' m) t fuel
533 do { g <- return_graph g
534 ; (a, fuel) <- subAnalysis' $
536 RewriteDeep -> solve getExitFact in' g (oneLessFuel fuel)
537 RewriteShallow -> do { a <- anal_f getExitFact in' g
538 ; return (a, oneLessFuel fuel) }
539 ; solve_tail a t fuel
541 solve_tail in' (G.ZLast l) fuel =
542 case check_maybe fuel $ either_last rewrites in' l of
544 case l of LastOther l -> return (ft_last_outs transfers in' l, fuel)
545 LastExit -> do { setExitFact (ft_exit_out transfers in')
546 ; return (LastOutFacts [], fuel) }
548 do { g <- return_graph g
549 ; (last_outs :: LastOutFacts a, fuel) <- subAnalysis' $
551 RewriteDeep -> solve lastOutFacts in' g (oneLessFuel fuel)
552 RewriteShallow -> do { los <- anal_f lastOutFacts in' g
553 ; return (los, fuel) }
554 ; return (last_outs, fuel)
557 fixed_point in_fact g fuel =
558 do { setAllFacts start_facts
559 ; (a, fuel) <- solve getExitFact in_fact g fuel
560 ; facts <- getAllFacts
561 ; last_outs <- lastOutFacts
562 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
563 ; let fp = FFP cfp last_outs
567 either_last rewrites in' (LastExit) = fr_exit rewrites in'
568 either_last rewrites in' (LastOther l) = fr_last rewrites in' l
575 mk_set_or_save :: (DataflowAnalysis df, Monad (df a), Outputable a) =>
576 (BlockId -> Bool) -> LastOutFacts a -> df a ()
577 mk_set_or_save is_local (LastOutFacts l) = mapM_ set_or_save_one l
578 where set_or_save_one (id, a) =
579 if is_local id then setFact id a else addLastOutFact (id, a)
584 {-# INLINE forward_rew #-}
587 (DebugNodes m l, LastNode l, Outputable a)
588 => (forall a . Fuel -> Maybe a -> Maybe a)
589 -> (g m l -> DFM a (Graph m l)) -- option on what to rewrite
593 -> ForwardTransfers m l a
594 -> ForwardRewrites m l a g
598 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
599 forward_rew check_maybe return_graph = forw
601 solve = forward_sol check_maybe return_graph
602 forw :: RewritingDepth
605 -> ForwardTransfers m l a
606 -> ForwardRewrites m l a g
610 -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
611 forw depth xstart_facts name transfers rewrites in_factx gx fuelx =
612 let rewrite :: BlockEnv a -> DFM a b
613 -> a -> Graph m l -> Fuel
614 -> DFM a (b, Graph m l, Fuel)
615 rewrite start finish in_fact g fuel =
616 let Graph entry blockenv = g
617 blocks = G.postorder_dfs_from blockenv entry
618 in do { solve depth name start transfers rewrites in_fact g fuel
619 ; eid <- freshBlockId "temporary entry id"
620 ; (rewritten, fuel) <-
621 rew_tail (ZFirst eid) in_fact entry emptyBlockEnv fuel
622 ; (rewritten, fuel) <- rewrite_blocks blocks rewritten fuel
624 ; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
626 don't_rewrite facts finish in_fact g fuel =
627 do { solve depth name facts transfers rewrites in_fact g fuel
629 ; return (a, g, fuel)
631 inner_rew :: DFM a f -> a -> Graph m l -> Fuel -> DFM a (f, Graph m l, Fuel)
632 inner_rew f i g fu = getAllFacts >>= \facts -> inner_rew' facts f i g fu
633 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
634 RewriteDeep -> rewrite
636 do { (a, g, fuel) <- rewrite xstart_facts getExitFact in_factx gx fuelx
637 ; facts <- getAllFacts
638 ; changed <- graphWasRewritten
639 ; last_outs <- lastOutFacts
640 ; let cfp = FP facts a changed (panic "no decoration?!") g
641 ; let fp = FFP cfp last_outs
644 rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
645 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
646 rewrite_blocks [] rewritten fuel = return (rewritten, fuel)
647 rewrite_blocks (G.Block id t : bs) rewritten fuel =
650 case check_maybe fuel $ fr_first rewrites a id of
651 Nothing -> do { (rewritten, fuel) <-
652 rew_tail h (ft_first_out transfers a id)
654 ; rewrite_blocks bs rewritten fuel }
655 Just g -> do { markGraphRewritten
656 ; g <- return_graph g
657 ; (outfact, g, fuel) <- inner_rew getExitFact a g fuel
658 ; let (blocks, h) = splice_head' (ZFirst id) g
659 ; (rewritten, fuel) <-
660 rew_tail h outfact t (blocks `plusUFM` rewritten) fuel
661 ; rewrite_blocks bs rewritten fuel }
663 rew_tail head in' (G.ZTail m t) rewritten fuel =
664 my_trace "Rewriting middle node" (ppr m) $
665 case check_maybe fuel $ fr_middle rewrites in' m of
666 Nothing -> rew_tail (G.ZHead head m) (ft_middle_out transfers in' m) t
668 Just g -> do { markGraphRewritten
669 ; g <- return_graph g
670 ; (a, g, fuel) <- inner_rew getExitFact in' g fuel
671 ; let (blocks, h) = G.splice_head' head g
672 ; rew_tail h a t (blocks `plusUFM` rewritten) fuel
674 rew_tail h in' (G.ZLast l) rewritten fuel =
675 my_trace "Rewriting last node" (ppr l) $
676 case check_maybe fuel $ either_last rewrites in' l of
677 Nothing -> do check_facts in' l
678 return (insertBlock (zipht h (G.ZLast l)) rewritten, fuel)
679 Just g -> do { markGraphRewritten
680 ; g <- return_graph g
681 ; ((), g, fuel) <- inner_rew (return ()) in' g fuel
682 ; let g' = G.splice_head_only' h g
683 ; return (G.lg_blocks g' `plusUFM` rewritten, fuel)
685 either_last rewrites in' (LastExit) = fr_exit rewrites in'
686 either_last rewrites in' (LastOther l) = fr_last rewrites in' l
687 check_facts in' (LastOther l) =
688 let LastOutFacts last_outs = ft_last_outs transfers in' l
689 in mapM (uncurry checkFactMatch) last_outs
690 check_facts _ LastExit = return []
693 --lastOutFacts :: (DataflowAnalysis m, Monad (m f)) => m f (LastOutFacts f)
694 lastOutFacts :: DFM f (LastOutFacts f)
695 lastOutFacts = bareLastOutFacts >>= return . LastOutFacts
697 {- ================================================================ -}
699 solve_b :: (DebugNodes m l, Outputable a)
700 => BlockEnv a -- initial facts (unbound == bottom)
702 -> DataflowLattice a -- lattice
703 -> BackwardTransfers m l a -- dataflow transfer functions
705 -> Graph m l -- graph to be analyzed
706 -> FuelMonad (BackwardFixedPoint m l a ()) -- answers
707 solve_b env name lattice transfers exit_fact g =
708 runDFM lattice $ bwd_pure_anal name env transfers g exit_fact
711 rewrite_b_graph :: (DebugNodes m l, Outputable a)
716 -> BackwardTransfers m l a
717 -> BackwardRewrites m l a Graph
718 -> a -- fact flowing in at exit
720 -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
721 rewrite_b_graph depth start_facts name lattice transfers rewrites exit_fact g =
723 do fuel <- fuelRemaining
724 (fp, fuel') <- backward_rew maybeRewriteWithFuel return depth start_facts name
725 transfers rewrites g exit_fact fuel
726 fuelDecrement name fuel fuel'
729 rewrite_b_agraph :: (DebugNodes m l, Outputable a)
734 -> BackwardTransfers m l a
735 -> BackwardRewrites m l a AGraph
736 -> a -- fact flowing in at exit
738 -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
739 rewrite_b_agraph depth start_facts name lattice transfers rewrites exit_fact g =
741 do fuel <- fuelRemaining
742 (fp, fuel') <- backward_rew maybeRewriteWithFuel areturn depth start_facts name
743 transfers rewrites g exit_fact fuel
744 fuelDecrement name fuel fuel'
749 {-# INLINE backward_sol #-}
752 (DebugNodes m l, LastNode l, Outputable a)
753 => (forall a . Fuel -> Maybe a -> Maybe a)
754 -> (g m l -> DFM a (Graph m l)) -- option on what to rewrite
758 -> BackwardTransfers m l a
759 -> BackwardRewrites m l a g
763 -> DFM a (BackwardFixedPoint m l a (), Fuel)
764 backward_sol check_maybe return_graph = back
766 back :: RewritingDepth
769 -> BackwardTransfers m l a
770 -> BackwardRewrites m l a g
774 -> DFM a (BackwardFixedPoint m l a (), Fuel)
775 back rewrite name start_facts transfers rewrites =
776 let anal_b :: Graph m l -> a -> DFM a a
778 do { fp <- bwd_pure_anal name emptyBlockEnv transfers g out
779 ; return $ zdfFpOutputFact fp }
781 subsolve :: g m l -> a -> Fuel -> DFM a (a, Fuel)
784 RewriteDeep -> \g a fuel ->
785 subAnalysis' $ do { g <- return_graph g; solve g a (oneLessFuel fuel) }
786 RewriteShallow -> \g a fuel ->
787 subAnalysis' $ do { g <- return_graph g; a <- anal_b g a
788 ; return (a, oneLessFuel fuel) }
790 solve :: Graph m l -> a -> Fuel -> DFM a (a, Fuel)
791 solve (Graph entry blockenv) exit_fact fuel =
792 let blocks = reverse $ G.postorder_dfs_from blockenv entry
793 last_in _env (LastExit) = exit_fact
794 last_in env (LastOther l) = bt_last_in transfers env l
795 last_rew _env (LastExit) = br_exit rewrites
796 last_rew env (LastOther l) = br_last rewrites env l
797 set_block_fact block fuel =
798 let (h, l) = G.goto_end (G.unzip block) in
801 case check_maybe fuel $ last_rew env l of
802 Nothing -> return (last_in env l, fuel)
803 Just g -> 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 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) $
818 setFact id $ bt_first_in transfers a id
820 Just g -> do { (a, fuel) <- subsolve g a fuel
824 set_head_fact (G.ZHead h m) a fuel =
825 case check_maybe fuel $ br_middle rewrites a m of
826 Nothing -> set_head_fact h (bt_middle_in transfers a m) fuel
827 Just g -> do { (a, fuel) <- subsolve g a fuel
828 ; set_head_fact h a fuel }
830 fixed_point g exit_fact fuel =
831 do { setAllFacts start_facts
832 ; (a, fuel) <- solve g exit_fact fuel
833 ; facts <- getAllFacts
834 ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
839 bwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
842 -> BackwardTransfers m l a
845 -> DFM a (BackwardFixedPoint m l a ())
847 bwd_pure_anal name env transfers g exit_fact =
848 do (fp, _) <- anal_b name env transfers panic_rewrites g exit_fact panic_fuel
850 where -- another case of "I love lazy evaluation"
851 anal_b = backward_sol (\_ _ -> Nothing) panic_return panic_depth
852 panic_rewrites = panic "pure analysis asked for a rewrite function"
853 panic_fuel = panic "pure analysis asked for fuel"
854 panic_return = panic "pure analysis tried to return a rewritten graph"
855 panic_depth = panic "pure analysis asked for a rewrite depth"
858 {- ================================================================ -}
860 {-# INLINE backward_rew #-}
863 (DebugNodes m l, LastNode l, Outputable a)
864 => (forall a . Fuel -> Maybe a -> Maybe a)
865 -> (g m l -> DFM a (Graph m l)) -- option on what to rewrite
869 -> BackwardTransfers m l a
870 -> BackwardRewrites m l a g
874 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
875 backward_rew check_maybe return_graph = back
877 solve = backward_sol check_maybe return_graph
878 back :: RewritingDepth
881 -> BackwardTransfers m l a
882 -> BackwardRewrites m l a g
886 -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
887 back depth xstart_facts name transfers rewrites gx exit_fact fuelx =
888 let rewrite :: BlockEnv a
889 -> Graph m l -> a -> Fuel
890 -> DFM a (a, Graph m l, Fuel)
891 rewrite start g exit_fact fuel =
892 let Graph entry blockenv = g
893 blocks = reverse $ G.postorder_dfs_from blockenv entry
894 in do { solve depth name start transfers rewrites g exit_fact fuel
896 ; my_trace "facts after solving" (ppr env) $ return ()
897 ; eid <- freshBlockId "temporary entry id"
898 ; (rewritten, fuel) <- rewrite_blocks True blocks emptyBlockEnv fuel
899 -- We can't have the fact check fail on the bogus entry, which _may_ change
900 ; (rewritten, fuel) <- rewrite_blocks False [Block eid entry] rewritten fuel
902 ; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
904 don't_rewrite facts g exit_fact fuel =
906 solve depth name facts transfers rewrites g exit_fact fuel
907 ; return (zdfFpOutputFact fp, g, fuel) }
908 inner_rew :: Graph m l -> a -> Fuel -> DFM a (a, Graph m l, Fuel)
909 inner_rew g a f = getAllFacts >>= \facts -> inner_rew' facts g a f
910 where inner_rew' = case depth of RewriteShallow -> don't_rewrite
911 RewriteDeep -> rewrite
913 do { (a, g, fuel) <- rewrite xstart_facts gx exit_fact fuelx
914 ; facts <- getAllFacts
915 ; changed <- graphWasRewritten
916 ; let fp = FP facts a changed (panic "no decoration?!") g
919 rewrite_blocks :: Bool -> [Block m l] -> (BlockEnv (Block m l))
920 -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
921 rewrite_blocks check bs rewritten fuel =
923 ; let rew [] r f = return (r, f)
925 do { (r, f) <- rewrite_block check env b r f; rew bs r f }
926 ; rew bs rewritten fuel }
927 rewrite_block check env b rewritten fuel =
928 let (h, l) = G.goto_end (G.unzip b) in
929 case maybeRewriteWithFuel fuel $ either_last env l of
930 Nothing -> propagate check fuel h (last_in env l) (ZLast l) rewritten
932 do { markGraphRewritten
933 ; g <- return_graph g
934 ; (a, g, fuel) <- inner_rew g exit_fact fuel
935 ; let G.Graph t new_blocks = g
936 ; let rewritten' = new_blocks `plusUFM` rewritten
937 ; propagate check fuel h a t rewritten' -- continue at entry of g
939 either_last _env (LastExit) = br_exit rewrites
940 either_last env (LastOther l) = br_last rewrites env l
941 last_in _env (LastExit) = exit_fact
942 last_in env (LastOther l) = bt_last_in transfers env l
943 propagate check fuel (ZHead h m) a tail rewritten =
944 case maybeRewriteWithFuel fuel $ br_middle rewrites a m of
946 propagate check fuel h (bt_middle_in transfers a m) (ZTail m tail) rewritten
948 do { markGraphRewritten
949 ; g <- return_graph g
950 ; my_trace "With Facts" (ppr a) $ return ()
951 ; my_trace " Rewrote middle node"
952 (f4sep [ppr m, text "to", pprGraph g]) $
954 ; (a, g, fuel) <- inner_rew g a fuel
955 ; let Graph t newblocks = G.splice_tail g tail
956 ; propagate check fuel h a t (newblocks `plusUFM` rewritten) }
957 propagate check fuel (ZFirst id) a tail rewritten =
958 case maybeRewriteWithFuel fuel $ br_first rewrites a id of
959 Nothing -> do { if check then checkFactMatch id $ bt_first_in transfers a id
961 ; return (insertBlock (Block id tail) rewritten, fuel) }
963 do { markGraphRewritten
964 ; g <- return_graph g
965 ; my_trace "Rewrote first node"
966 (f4sep [ppr id <> colon, text "to", pprGraph g]) $ return ()
967 ; (a, g, fuel) <- inner_rew g a fuel
968 ; if check then checkFactMatch id a else return ()
969 ; let Graph t newblocks = G.splice_tail g tail
970 ; let r = insertBlock (Block id t) (newblocks `plusUFM` rewritten)
974 {- ================================================================ -}
976 instance FixedPoint CommonFixedPoint where
977 zdfFpFacts = fp_facts
978 zdfFpOutputFact = fp_out
979 zdfGraphChanged = fp_changed
980 zdfDecoratedGraph = fp_dec_graph
981 zdfFpContents = fp_contents
982 zdfFpMap f (FP fs out ch dg a) = FP fs out ch dg (f a)
984 instance FixedPoint ForwardFixedPoint where
985 zdfFpFacts = fp_facts . ffp_common
986 zdfFpOutputFact = fp_out . ffp_common
987 zdfGraphChanged = fp_changed . ffp_common
988 zdfDecoratedGraph = fp_dec_graph . ffp_common
989 zdfFpContents = fp_contents . ffp_common
990 zdfFpMap f (FFP fp los) = FFP (zdfFpMap f fp) los
996 my_trace :: String -> SDoc -> a -> a
997 my_trace = if dump_things then pprTrace else \_ _ a -> a
1000 -- | Here's a function to run an action on blocks until we reach a fixed point.
1001 run :: (Outputable a, DebugNodes m l) =>
1002 String -> String -> (Block m l -> b -> DFM a b) -> [Block m l] -> b -> DFM a b
1003 run dir name do_block blocks b =
1004 do { show_blocks $ iterate (1::Int) }
1006 -- N.B. Each iteration starts with the same transaction limit;
1007 -- only the rewrites in the final iteration actually count
1008 trace_block b block =
1009 my_trace "about to do" (text name <+> text "on" <+> ppr (blockId block)) $
1012 do { markFactsUnchanged
1013 ; b <- foldM trace_block b blocks
1014 ; changed <- factsStatus
1015 ; facts <- getAllFacts
1016 ; let depth = 0 -- was nesting depth
1019 NoChange -> unchanged depth $ return b
1021 pprFacts depth n facts $
1022 if n < 1000 then iterate (n+1)
1025 msg n = concat [name, " didn't converge in ", show n, " " , dir,
1027 my_nest depth sdoc = my_trace "" $ nest (3*depth) sdoc
1028 ppIter depth n = my_nest depth (empty $$ text "*************** iteration" <+> pp_i n)
1029 pp_i n = int n <+> text "of" <+> text name <+> text "on" <+> graphId
1031 my_nest depth (text "facts for" <+> graphId <+> text "are unchanged")
1033 graphId = case blocks of { Block id _ : _ -> ppr id ; [] -> text "<empty>" }
1034 show_blocks = my_trace "Blocks:" (vcat (map pprBlock blocks))
1035 pprBlock (Block id t) = nest 2 (pprFact (id, t))
1036 pprFacts depth n env =
1037 my_nest depth (text "facts for iteration" <+> pp_i n <+> text "are:" $$
1038 (nest 2 $ vcat $ map pprFact $ ufmToList env))
1039 pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)
1042 f4sep :: [SDoc] -> SDoc
1044 f4sep (d:ds) = fsep (d : map (nest 4) ds)
1047 subAnalysis' :: (Monad (m f), DataflowAnalysis m, Outputable f) =>
1050 do { a <- subAnalysis $
1051 do { a <- m; facts <- getAllFacts
1052 ; my_trace "after sub-analysis facts are" (pprFacts facts) $
1054 ; facts <- getAllFacts
1055 ; my_trace "in parent analysis facts are" (pprFacts facts) $
1057 where pprFacts env = nest 2 $ vcat $ map pprFact $ ufmToList env
1058 pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)