1c4b091d7995c0bb4ac1d728d9a889d13cc5753a
[packages/hoopl.git] / src / Compiler / Hoopl / DataflowFold.hs
1 {-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs, EmptyDataDecls, PatternGuards, TypeFamilies, MultiParamTypeClasses #-}
2 #if __GLASGOW_HASKELL__ >= 701
3 {-# LANGUAGE Safe #-}
4 #endif
5
6 {- Notes about the genesis of Hoopl7
7 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
8 Hoopl7 has the following major chages
9
10 a) GMany has symmetric entry and exit
11 b) GMany closed-entry does not record a BlockId
12 c) GMany open-exit does not record a BlockId
13 d) The body of a GMany is called Body
14 e) A Body is just a list of blocks, not a map. I've argued
15 elsewhere that this is consistent with (c)
16
17 A consequence is that Graph is no longer an instance of NonLocal,
18 but nevertheless I managed to keep the ARF and ARB signatures
19 nice and uniform.
20
21 This was made possible by
22
23 * FwdTransfer looks like this:
24 type FwdTransfer n f
25 = forall e x. n e x -> Fact e f -> Fact x f
26 type family Fact x f :: *
27 type instance Fact C f = FactBase f
28 type instance Fact O f = f
29
30 Note that the incoming fact is a Fact (not just 'f' as in Hoopl5,6).
31 It's up to the *transfer function* to look up the appropriate fact
32 in the FactBase for a closed-entry node. Example:
33 constProp (Label l) fb = lookupFact fb l
34 That is how Hoopl can avoid having to know the block-id for the
35 first node: it defers to the client.
36
37 [Side note: that means the client must know about
38 bottom, in case the looupFact returns Nothing]
39
40 * Note also that FwdTransfer *returns* a Fact too;
41 that is, the types in both directions are symmetrical.
42 Previously we returned a [(BlockId,f)] but I could not see
43 how to make everything line up if we do this.
44
45 Indeed, the main shortcoming of Hoopl7 is that we are more
46 or less forced into this uniform representation of the facts
47 flowing into or out of a closed node/block/graph, whereas
48 previously we had more flexibility.
49
50 In exchange the code is neater, with fewer distinct types.
51 And morally a FactBase is equivalent to [(BlockId,f)] and
52 nearly equivalent to (BlockId -> f).
53
54 * I've realised that forwardBlockList and backwardBlockList
55 both need (NonLocal n), and that goes everywhere.
56
57 * I renamed BlockId to Label
58 -}
59
60 module Compiler.Hoopl.DataflowFold
61 ( DataflowLattice(..), JoinFun, OldFact(..), NewFact(..), Fact
62 , ChangeFlag(..), changeIf
63 , FwdPass(..), FwdTransfer, mkFTransfer, mkFTransfer', getFTransfers
64 , FwdRes(..), FwdRewrite, mkFRewrite, mkFRewrite', getFRewrites
65 , BwdPass(..), BwdTransfer, mkBTransfer, mkBTransfer', getBTransfers
66 , BwdRes(..), BwdRewrite, mkBRewrite, mkBRewrite', getBRewrites
67 , analyzeAndRewriteFwd, analyzeAndRewriteBwd
68 )
69 where
70
71 import Data.Maybe
72
73 import Compiler.Hoopl.Fuel
74 import Compiler.Hoopl.Graph
75 import Compiler.Hoopl.MkGraph
76 import qualified Compiler.Hoopl.GraphUtil as U
77 import Compiler.Hoopl.Label
78 import Compiler.Hoopl.Util
79
80 -----------------------------------------------------------------------------
81 -- DataflowLattice
82 -----------------------------------------------------------------------------
83
84 data DataflowLattice a = DataflowLattice
85 { fact_name :: String -- Documentation
86 , fact_bot :: a -- Lattice bottom element
87 , fact_join :: JoinFun a -- Lattice join plus change flag
88 -- (changes iff result > old fact)
89 }
90 -- ^ A transfer function might want to use the logging flag
91 -- to control debugging, as in for example, it updates just one element
92 -- in a big finite map. We don't want Hoopl to show the whole fact,
93 -- and only the transfer function knows exactly what changed.
94
95 type JoinFun a = Label -> OldFact a -> NewFact a -> (ChangeFlag, a)
96 -- the label argument is for debugging purposes only
97 newtype OldFact a = OldFact a
98 newtype NewFact a = NewFact a
99
100 data ChangeFlag = NoChange | SomeChange deriving (Eq, Ord)
101 changeIf :: Bool -> ChangeFlag
102 changeIf changed = if changed then SomeChange else NoChange
103
104
105 -----------------------------------------------------------------------------
106 -- Analyze and rewrite forward: the interface
107 -----------------------------------------------------------------------------
108
109 data FwdPass n f
110 = FwdPass { fp_lattice :: DataflowLattice f
111 , fp_transfer :: FwdTransfer n f
112 , fp_rewrite :: FwdRewrite n f }
113
114 newtype FwdTransfer n f
115 = FwdTransfers { getFTransfers ::
116 ( n C O -> f -> f
117 , n O O -> f -> f
118 , n O C -> f -> FactBase f
119 ) }
120
121 newtype FwdRewrite n f
122 = FwdRewrites { getFRewrites ::
123 ( n C O -> f -> Maybe (FwdRes n f C O)
124 , n O O -> f -> Maybe (FwdRes n f O O)
125 , n O C -> f -> Maybe (FwdRes n f O C)
126 ) }
127 data FwdRes n f e x = FwdRes (AGraph n e x) (FwdRewrite n f)
128 -- result of a rewrite is a new graph and a (possibly) new rewrite function
129
130 mkFTransfer :: (n C O -> f -> f)
131 -> (n O O -> f -> f)
132 -> (n O C -> f -> FactBase f)
133 -> FwdTransfer n f
134 mkFTransfer f m l = FwdTransfers (f, m, l)
135
136 mkFTransfer' :: (forall e x . n e x -> f -> Fact x f) -> FwdTransfer n f
137 mkFTransfer' f = FwdTransfers (f, f, f)
138
139 mkFRewrite :: (n C O -> f -> Maybe (FwdRes n f C O))
140 -> (n O O -> f -> Maybe (FwdRes n f O O))
141 -> (n O C -> f -> Maybe (FwdRes n f O C))
142 -> FwdRewrite n f
143 mkFRewrite f m l = FwdRewrites (f, m, l)
144
145 mkFRewrite' :: (forall e x . n e x -> f -> Maybe (FwdRes n f e x)) -> FwdRewrite n f
146 mkFRewrite' f = FwdRewrites (f, f, f)
147
148
149 type family Fact x f :: *
150 type instance Fact C f = FactBase f
151 type instance Fact O f = f
152
153 -- | if the graph being analyzed is open at the entry, there must
154 -- be no other entry point, or all goes horribly wrong...
155 analyzeAndRewriteFwd
156 :: forall n f e x entries. (NonLocal n, LabelsPtr entries)
157 => FwdPass n f
158 -> MaybeC e entries
159 -> Graph n e x -> Fact e f
160 -> FuelMonad (Graph n e x, FactBase f, MaybeO x f)
161 analyzeAndRewriteFwd pass entries g f =
162 do (rg, fout) <- arfGraph pass (nilBefore g) (fmap targetLabels entries) g f
163 let (g', fb) = normalizeGraph rg
164 return (g', fb, distinguishedExitFact g' fout)
165 where nilBefore (GMany NothingO _ _) = rgnilC
166 nilBefore (GMany (JustO _) _ _) = rgnil
167 nilBefore GNil = rgnil
168 nilBefore (GUnit _) = rgnil
169 nilBefore :: Graph n e x -> RG f n e e
170
171 distinguishedExitFact :: forall n e x f . Graph n e x -> Fact x f -> MaybeO x f
172 distinguishedExitFact g f = maybe g
173 where maybe :: Graph n e x -> MaybeO x f
174 maybe GNil = JustO f
175 maybe (GUnit {}) = JustO f
176 maybe (GMany _ _ x) = case x of NothingO -> NothingO
177 JustO _ -> JustO f
178
179 ----------------------------------------------------------------
180 -- Forward Implementation
181 ----------------------------------------------------------------
182
183
184 type FM = FuelMonad
185
186 type Entries e = MaybeC e [Label]
187
188 type RGPair f n e x = (RG f n e x, Fact x f)
189
190
191 arfGraph :: forall n f e a x .
192 (NonLocal n)
193 => FwdPass n f
194 -> RG f n e a
195 -> Entries a -> Graph n a x -> Fact a f -> FM (RG f n e x, Fact x f)
196 arfGraph pass head entries g f = graph g (head, f)
197 where
198 graph :: Graph n a x -> RGPair f n e a -> FM (RGPair f n e x)
199 block :: forall e a x . Block n a x -> (RG f n e a, f) -> FM (RGPair f n e x)
200 node :: forall e a x . (ShapeLifter a x)
201 => n a x -> (RG f n e a, f) -> FM (RGPair f n e x)
202 body :: forall e . [Label] -> Body n -> (RGPair f n e C) -> FM (RGPair f n e C)
203 -- Outgoing factbase is restricted to Labels *not* in
204 -- in the Body; the facts for Labels *in*
205 -- the Body are in the 'RG f n C C'
206
207 cat :: forall e a b x info info' info''.
208 ((RG f n e a, info) -> FuelMonad (RG f n e b, info'))
209 -> ((RG f n e b, info') -> FuelMonad (RG f n e x, info''))
210 -> ((RG f n e a, info) -> FuelMonad (RG f n e x, info''))
211
212 cat ft1 ft2 (g, f) = ft1 (g, f) >>= ft2
213
214 graph GNil = return
215 graph (GUnit blk) = block blk
216 graph (GMany e bdy x) = eb e bdy `cat` exit x
217 where
218 eb :: MaybeO a (Block n O C) -> Body n -> (RGPair f n e a) -> FM (RGPair f n e C)
219 exit :: MaybeO x (Block n C O) -> (RGPair f n e C) -> FM (RGPair f n e x)
220 exit (JustO blk) = arfx block blk
221 exit NothingO = return
222 eb entry bdy = c entries entry
223 where c :: MaybeC a [Label] -> MaybeO a (Block n O C)
224 -> (RGPair f n e a) -> FM (RGPair f n e C)
225 c NothingC (JustO entry) = block entry `cat` body (successors entry) bdy
226 c (JustC entries) NothingO = body entries bdy
227
228 -- Lift from nodes to blocks
229 block (BFirst n) = node n
230 block (BMiddle n) = node n
231 block (BLast n) = node n
232 block (BCat b1 b2) = block b1 `cat` block b2
233 block (BHead h n) = block h `cat` node n
234 block (BTail n t) = node n `cat` block t
235 block (BClosed h t)= block h `cat` block t
236
237 node thenode (head, f)
238 = do { mb_g <- withFuel (frewrite pass thenode f)
239 ; case mb_g of
240 Nothing -> return (spliceRgNode head f thenode,
241 ftransfer pass thenode f)
242 Just (FwdRes ag rw) ->
243 do { g <- graphOfAGraph ag
244 ; let pass' = pass { fp_rewrite = rw }
245 ; arfGraph pass' head (entry thenode) g (elift thenode f) } }
246
247 -- | Compose fact transformers and concatenate the resulting
248 -- rewritten graphs.
249 {-# INLINE cat #-}
250
251 arfx :: forall thing e x .
252 NonLocal thing
253 => (thing C x -> (RG f n e C, f) -> FM (RGPair f n e x))
254 -> (thing C x -> (RG f n e C, Fact C f) -> FM (RGPair f n e x))
255 arfx arf thing (h, fb) =
256 arf thing (h, fromJust $ lookupFact (joinInFacts lattice fb) $ entryLabel thing)
257 where lattice = fp_lattice pass
258 -- joinInFacts adds debugging information
259
260
261 -- Outgoing factbase is restricted to Labels *not* in
262 -- in the Body; the facts for Labels *in*
263 -- the Body are in the 'RG f n C C'
264 body entries blocks (h, init_fbase)
265 = do { (body', fb) <- fix; return (h `rgCat` body', fb) }
266 where
267 fix = fixpoint True (fp_lattice pass) do_block init_fbase $
268 forwardBlockList entries blocks
269 do_block b f = do (g, fb) <- block b (rgnilC, lookupF pass (entryLabel b) f)
270 return (g, factBaseList fb)
271
272
273 -- Join all the incoming facts with bottom.
274 -- We know the results _shouldn't change_, but the transfer
275 -- functions might, for example, generate some debugging traces.
276 joinInFacts :: DataflowLattice f -> FactBase f -> FactBase f
277 joinInFacts (DataflowLattice {fact_bot = bot, fact_join = fj}) fb =
278 mkFactBase $ map botJoin $ factBaseList fb
279 where botJoin (l, f) = (l, snd $ fj l (OldFact bot) (NewFact f))
280
281
282 forwardBlockList :: (NonLocal n, LabelsPtr entry)
283 => entry -> Body n -> [Block n C C]
284 -- This produces a list of blocks in order suitable for forward analysis,
285 -- along with the list of Labels it may depend on for facts.
286 forwardBlockList entries (Body blks) = postorder_dfs_from blks entries
287
288 -----------------------------------------------------------------------------
289 -- Backward analysis and rewriting: the interface
290 -----------------------------------------------------------------------------
291
292 data BwdPass n f
293 = BwdPass { bp_lattice :: DataflowLattice f
294 , bp_transfer :: BwdTransfer n f
295 , bp_rewrite :: BwdRewrite n f }
296
297 newtype BwdTransfer n f
298 = BwdTransfers { getBTransfers ::
299 ( n C O -> f -> f
300 , n O O -> f -> f
301 , n O C -> FactBase f -> f
302 ) }
303 newtype BwdRewrite n f
304 = BwdRewrites { getBRewrites ::
305 ( n C O -> f -> Maybe (BwdRes n f C O)
306 , n O O -> f -> Maybe (BwdRes n f O O)
307 , n O C -> FactBase f -> Maybe (BwdRes n f O C)
308 ) }
309 data BwdRes n f e x = BwdRes (AGraph n e x) (BwdRewrite n f)
310
311 mkBTransfer :: (n C O -> f -> f) -> (n O O -> f -> f) ->
312 (n O C -> FactBase f -> f) -> BwdTransfer n f
313 mkBTransfer f m l = BwdTransfers (f, m, l)
314
315 mkBTransfer' :: (forall e x . n e x -> Fact x f -> f) -> BwdTransfer n f
316 mkBTransfer' f = BwdTransfers (f, f, f)
317
318 mkBRewrite :: (n C O -> f -> Maybe (BwdRes n f C O))
319 -> (n O O -> f -> Maybe (BwdRes n f O O))
320 -> (n O C -> FactBase f -> Maybe (BwdRes n f O C))
321 -> BwdRewrite n f
322 mkBRewrite f m l = BwdRewrites (f, m, l)
323
324 mkBRewrite' :: (forall e x . n e x -> Fact x f -> Maybe (BwdRes n f e x)) -> BwdRewrite n f
325 mkBRewrite' f = BwdRewrites (f, f, f)
326
327
328 -----------------------------------------------------------------------------
329 -- Backward implementation
330 -----------------------------------------------------------------------------
331
332 type ARB' n f thing e x
333 = BwdPass n f -> thing e x -> Fact x f -> FuelMonad (RG f n e x, f)
334
335 type ARB thing n = forall f e x. ARB' n f thing e x
336
337 arbNode :: (NonLocal n, ShapeLifter e x) => ARB' n f n e x
338 -- Lifts (BwdTransfer,BwdRewrite) to ARB_Node;
339 -- this time we do rewriting as well.
340 -- The ARB_Graph parameters specifies what to do with the rewritten graph
341 arbNode pass node f
342 = do { mb_g <- withFuel (brewrite pass node f)
343 ; case mb_g of
344 Nothing -> return (rgunit entry_f (unit node), entry_f)
345 where entry_f = btransfer pass node f
346 Just (BwdRes ag rw) -> do { g <- graphOfAGraph ag
347 ; let pass' = pass { bp_rewrite = rw }
348 ; (g, f) <- arbGraph pass' g f
349 ; return (g, elower (bp_lattice pass) node f)} }
350
351 arbBlock :: NonLocal n => ARB (Block n) n
352 -- Lift from nodes to blocks
353 arbBlock pass (BFirst node) = arbNode pass node
354 arbBlock pass (BMiddle node) = arbNode pass node
355 arbBlock pass (BLast node) = arbNode pass node
356 arbBlock pass (BCat b1 b2) = arbCat arbBlock arbBlock pass b1 b2
357 arbBlock pass (BHead h n) = arbCat arbBlock arbNode pass h n
358 arbBlock pass (BTail n t) = arbCat arbNode arbBlock pass n t
359 arbBlock pass (BClosed h t) = arbCat arbBlock arbBlock pass h t
360
361 arbCat :: NonLocal n => ARB' n f thing1 e O -> ARB' n f thing2 O x
362 -> BwdPass n f -> thing1 e O -> thing2 O x
363 -> Fact x f -> FuelMonad (RG f n e x, f)
364 arbCat arb1 arb2 pass thing1 thing2 f = do { (g2,f2) <- arb2 pass thing2 f
365 ; (g1,f1) <- arb1 pass thing1 f2
366 ; return (g1 `rgCat` g2, f1) }
367
368 arbBody :: NonLocal n
369 => BwdPass n f -> Body n -> FactBase f
370 -> FuelMonad (RG f n C C, FactBase f)
371 arbBody pass blocks init_fbase
372 = fixpoint False (bp_lattice pass) do_block init_fbase $
373 backwardBlockList blocks
374 where
375 do_block b f = do (g, f) <- arbBlock pass b f
376 return (g, [(entryLabel b, f)])
377
378 arbGraph :: NonLocal n
379 => BwdPass n f -> Graph n e x -> Fact x f
380 -> FuelMonad (RG f n e x, Fact e f)
381 arbGraph _ GNil f = return (rgnil, f)
382 arbGraph pass (GUnit blk) f = arbBlock pass blk f
383 arbGraph pass (GMany NothingO body NothingO) f
384 = do { (body', fb) <- arbBody pass body f
385 ; return (body', fb) }
386 arbGraph pass (GMany NothingO body (JustO exit)) f
387 = do { (exit', fx) <- arbBlock pass exit f
388 ; (body', fb) <- arbBody pass body $
389 joinInFacts (bp_lattice pass) $ mkFactBase [(entryLabel exit, fx)]
390 ; return (body' `rgCat` exit', fb) }
391 arbGraph pass (GMany (JustO entry) body NothingO) f
392 = do { (body', fb) <- arbBody pass body f
393 ; (entry', fe) <- arbBlock pass entry fb
394 ; return (entry' `rgCat` body', fe) }
395 arbGraph pass (GMany (JustO entry) body (JustO exit)) f
396 = do { (exit', fx) <- arbBlock pass exit f
397 ; (body', fb) <- arbBody pass body $
398 joinInFacts (bp_lattice pass) $ mkFactBase [(entryLabel exit, fx)]
399 ; (entry', fe) <- arbBlock pass entry fb
400 ; return (entry' `rgCat` body' `rgCat` exit', fe) }
401
402 backwardBlockList :: NonLocal n => Body n -> [Block n C C]
403 -- This produces a list of blocks in order suitable for backward analysis,
404 -- along with the list of Labels it may depend on for facts.
405 backwardBlockList body = reachable ++ missing
406 where reachable = reverse $ forwardBlockList entries body
407 entries = externalEntryLabels body
408 all = bodyList body
409 missingLabels =
410 mkLabelSet (map fst all) `minusLabelSet`
411 mkLabelSet (map entryLabel reachable)
412 missing = map snd $ filter (flip elemLabelSet missingLabels . fst) all
413
414 {-
415
416 The forward and backward dataflow analyses now use postorder depth-first
417 order for faster convergence.
418
419 The forward and backward cases are not dual. In the forward case, the
420 entry points are known, and one simply traverses the body blocks from
421 those points. In the backward case, something is known about the exit
422 points, but this information is essentially useless, because we don't
423 actually have a dual graph (that is, one with edges reversed) to
424 compute with. (Even if we did have a dual graph, it would not avail
425 us---a backward analysis must include reachable blocks that don't
426 reach the exit, as in a procedure that loops forever and has side
427 effects.)
428
429 Since in the general case, no information is available about entry
430 points, I have put in a horrible hack. First, I assume that every
431 label defined but not used is an entry point. Then, because an entry
432 point might also be a loop header, I add, in arbitrary order, all the
433 remaining "missing" blocks. Needless to say, I am not pleased.
434 I am not satisfied. I am not Senator Morgan.
435
436 Wait! I believe that the Right Thing here is to require that anyone
437 wishing to analyze a graph closed at the entry provide a way of
438 determining the entry points, if any, of that graph. This requirement
439 can apply equally to forward and backward analyses; I believe that
440 using the input FactBase to determine the entry points of a closed
441 graph is *also* a hack.
442
443 NR
444
445 -}
446
447
448 -- | if the graph being analyzed is open at the exit, I don't
449 -- quite understand the implications of possible other exits
450 analyzeAndRewriteBwd
451 :: forall n f e x. NonLocal n
452 => BwdPass n f
453 -> Graph n e x -> Fact x f
454 -> FuelMonad (Graph n e x, FactBase f, MaybeO e f)
455 analyzeAndRewriteBwd pass g f =
456 do (rg, fout) <- arbGraph pass g f
457 let (g', fb) = normalizeGraph rg
458 return (g', fb, distinguishedEntryFact g' fout)
459
460 distinguishedEntryFact :: forall n e x f . Graph n e x -> Fact e f -> MaybeO e f
461 distinguishedEntryFact g f = maybe g
462 where maybe :: Graph n e x -> MaybeO e f
463 maybe GNil = JustO f
464 maybe (GUnit {}) = JustO f
465 maybe (GMany e _ _) = case e of NothingO -> NothingO
466 JustO _ -> JustO f
467
468 -----------------------------------------------------------------------------
469 -- fixpoint: finding fixed points
470 -----------------------------------------------------------------------------
471
472 data TxFactBase n f
473 = TxFB { tfb_fbase :: FactBase f
474 , tfb_rg :: RG f n C C -- Transformed blocks
475 , tfb_cha :: ChangeFlag
476 , tfb_lbls :: LabelSet }
477 -- Note [TxFactBase change flag]
478 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
479 -- Set the tfb_cha flag iff
480 -- (a) the fact in tfb_fbase for or a block L changes
481 -- (b) L is in tfb_lbls.
482 -- The tfb_lbls are all Labels of the *original*
483 -- (not transformed) blocks
484
485 updateFact :: DataflowLattice f -> LabelSet -> (Label, f)
486 -> (ChangeFlag, FactBase f)
487 -> (ChangeFlag, FactBase f)
488 -- See Note [TxFactBase change flag]
489 updateFact lat lbls (lbl, new_fact) (cha, fbase)
490 | NoChange <- cha2 = (cha, fbase)
491 | lbl `elemLabelSet` lbls = (SomeChange, new_fbase)
492 | otherwise = (cha, new_fbase)
493 where
494 (cha2, res_fact) -- Note [Unreachable blocks]
495 = case lookupFact fbase lbl of
496 Nothing -> (SomeChange, snd $ join $ fact_bot lat) -- Note [Unreachable blocks]
497 Just old_fact -> join old_fact
498 where join old_fact = fact_join lat lbl (OldFact old_fact) (NewFact new_fact)
499 new_fbase = extendFactBase fbase lbl res_fact
500
501 fixpoint :: forall block n f. (NonLocal n, NonLocal (block n))
502 => Bool -- Going forwards?
503 -> DataflowLattice f
504 -> (block n C C -> FactBase f
505 -> FuelMonad (RG f n C C, [(Label, f)]))
506 -> FactBase f
507 -> [block n C C]
508 -> FuelMonad (RG f n C C, FactBase f)
509 fixpoint is_fwd lat do_block init_fbase untagged_blocks
510 = do { fuel <- getFuel
511 ; tx_fb <- loop fuel init_fbase
512 ; return (tfb_rg tx_fb,
513 tfb_fbase tx_fb `delFromFactBase` map fst blocks) }
514 -- The successors of the Graph are the the Labels for which
515 -- we have facts, that are *not* in the blocks of the graph
516 where
517 blocks = map tag untagged_blocks
518 where tag b = ((entryLabel b, b), if is_fwd then [entryLabel b] else successors b)
519
520 tx_blocks :: [((Label, block n C C), [Label])] -- I do not understand this type
521 -> TxFactBase n f -> FuelMonad (TxFactBase n f)
522 tx_blocks [] tx_fb = return tx_fb
523 tx_blocks (((lbl,blk), deps):bs) tx_fb = tx_block lbl blk deps tx_fb >>= tx_blocks bs
524 -- "deps" == Labels the block may _depend_ upon for facts
525
526 tx_block :: Label -> block n C C -> [Label]
527 -> TxFactBase n f -> FuelMonad (TxFactBase n f)
528 tx_block lbl blk deps tx_fb@(TxFB { tfb_fbase = fbase, tfb_lbls = lbls
529 , tfb_rg = blks, tfb_cha = cha })
530 | is_fwd && not (lbl `elemFactBase` fbase)
531 = return tx_fb {tfb_lbls = lbls `unionLabelSet` mkLabelSet deps} -- Note [Unreachable blocks]
532 | otherwise
533 = do { (rg, out_facts) <- do_block blk fbase
534 ; let (cha',fbase')
535 = foldr (updateFact lat lbls) (cha,fbase) out_facts
536 lbls' = lbls `unionLabelSet` mkLabelSet deps
537 ; return (TxFB { tfb_lbls = lbls'
538 , tfb_rg = rg `rgCat` blks
539 , tfb_fbase = fbase', tfb_cha = cha' }) }
540
541 loop :: Fuel -> FactBase f -> FuelMonad (TxFactBase n f)
542 loop fuel fbase
543 = do { let init_tx_fb = TxFB { tfb_fbase = fbase
544 , tfb_cha = NoChange
545 , tfb_rg = rgnilC
546 , tfb_lbls = emptyLabelSet }
547 ; tx_fb <- tx_blocks blocks init_tx_fb
548 ; case tfb_cha tx_fb of
549 NoChange -> return tx_fb
550 SomeChange -> do { setFuel fuel
551 ; loop fuel (tfb_fbase tx_fb) } }
552
553 {- Note [Unreachable blocks]
554 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
555 A block that is not in the domain of tfb_fbase is "currently unreachable".
556 A currently-unreachable block is not even analyzed. Reason: consider
557 constant prop and this graph, with entry point L1:
558 L1: x:=3; goto L4
559 L2: x:=4; goto L4
560 L4: if x>3 goto L2 else goto L5
561 Here L2 is actually unreachable, but if we process it with bottom input fact,
562 we'll propagate (x=4) to L4, and nuke the otherwise-good rewriting of L4.
563
564 * If a currently-unreachable block is not analyzed, then its rewritten
565 graph will not be accumulated in tfb_rg. And that is good:
566 unreachable blocks simply do not appear in the output.
567
568 * Note that clients must be careful to provide a fact (even if bottom)
569 for each entry point. Otherwise useful blocks may be garbage collected.
570
571 * Note that updateFact must set the change-flag if a label goes from
572 not-in-fbase to in-fbase, even if its fact is bottom. In effect the
573 real fact lattice is
574 UNR
575 bottom
576 the points above bottom
577
578 * Even if the fact is going from UNR to bottom, we still call the
579 client's fact_join function because it might give the client
580 some useful debugging information.
581
582 * All of this only applies for *forward* fixpoints. For the backward
583 case we must treat every block as reachable; it might finish with a
584 'return', and therefore have no successors, for example.
585 -}
586
587 -----------------------------------------------------------------------------
588 -- RG: an internal data type for graphs under construction
589 -- TOTALLY internal to Hoopl; each block carries its fact
590 -----------------------------------------------------------------------------
591
592 type RG f n e x = Graph' (FBlock f) n e x
593 data FBlock f n e x = FBlock f (Block n e x)
594 instance NonLocal n => NonLocal (FBlock f n) where
595 entryLabel (FBlock _ b) = entryLabel b
596 successors (FBlock _ b) = successors b
597
598 --- constructors
599
600 rgnil :: RG f n O O
601 rgnilC :: RG f n C C
602 rgunit :: NonLocal n => f -> Block n e x -> RG f n e x
603 rgCat :: NonLocal n => RG f n e a -> RG f n a x -> RG f n e x
604
605 ---- observers
606
607 type GraphWithFacts n f e x = (Graph n e x, FactBase f)
608 -- A Graph together with the facts for that graph
609 -- The domains of the two maps should be identical
610
611 normalizeGraph :: forall n f e x .
612 NonLocal n => RG f n e x -> GraphWithFacts n f e x
613
614 normalizeGraph g = (graphMapBlocks dropFact g, facts g)
615 where dropFact (FBlock _ b) = b
616 facts :: RG f n e x -> FactBase f
617 facts GNil = noFacts
618 facts (GUnit _) = noFacts
619 facts (GMany _ body exit) = bodyFacts body `unionFactBase` exitFacts exit
620 exitFacts :: MaybeO x (FBlock f n C O) -> FactBase f
621 exitFacts NothingO = noFacts
622 exitFacts (JustO (FBlock f b)) = mkFactBase [(entryLabel b, f)]
623 bodyFacts :: Body' (FBlock f) n -> FactBase f
624 bodyFacts (Body body) = foldLabelMap f noFacts body
625 where f (FBlock f b) fb = extendFactBase fb (entryLabel b) f
626
627 --- implementation of the constructors (boring)
628
629 rgnil = GNil
630 rgnilC = GMany NothingO emptyMap NothingO
631
632 rgunit f b@(BFirst {}) = gUnitCO (FBlock f b)
633 rgunit f b@(BMiddle {}) = gUnitOO (FBlock f b)
634 rgunit f b@(BLast {}) = gUnitOC (FBlock f b)
635 rgunit f b@(BCat {}) = gUnitOO (FBlock f b)
636 rgunit f b@(BHead {}) = gUnitCO (FBlock f b)
637 rgunit f b@(BTail {}) = gUnitOC (FBlock f b)
638 rgunit f b@(BClosed {}) = gUnitCC (FBlock f b)
639
640 rgCat = U.splice fzCat
641 where fzCat (FBlock f b1) (FBlock _ b2) = FBlock f (b1 `U.cat` b2)
642
643 ----------------------------------------------------------------
644 -- Utilities
645 ----------------------------------------------------------------
646
647 -- Lifting based on shape:
648 -- - from nodes to blocks
649 -- - from facts to fact-like things
650 -- Lowering back:
651 -- - from fact-like things to facts
652 -- Note that the latter two functions depend only on the entry shape.
653 class ShapeLifter e x where
654 unit :: n e x -> Block n e x
655 elift :: NonLocal n => n e x -> f -> Fact e f
656 elower :: NonLocal n => DataflowLattice f -> n e x -> Fact e f -> f
657 ftransfer :: FwdPass n f -> n e x -> f -> Fact x f
658 btransfer :: BwdPass n f -> n e x -> Fact x f -> f
659 frewrite :: FwdPass n f -> n e x -> f -> Maybe (FwdRes n f e x)
660 brewrite :: BwdPass n f -> n e x -> Fact x f -> Maybe (BwdRes n f e x)
661 spliceRgNode :: NonLocal n => RG f n a e -> f -> n e x -> RG f n a x
662 entry :: NonLocal n => n e x -> Entries e
663
664 instance ShapeLifter C O where
665 unit = BFirst
666 elift n f = mkFactBase [(entryLabel n, f)]
667 elower lat n fb = getFact lat (entryLabel n) fb
668 ftransfer (FwdPass {fp_transfer = FwdTransfers (ft, _, _)}) n f = ft n f
669 btransfer (BwdPass {bp_transfer = BwdTransfers (bt, _, _)}) n f = bt n f
670 frewrite (FwdPass {fp_rewrite = FwdRewrites (fr, _, _)}) n f = fr n f
671 brewrite (BwdPass {bp_rewrite = BwdRewrites (br, _, _)}) n f = br n f
672 spliceRgNode (GMany e body NothingO) f n = GMany e body x
673 where x = JustO $ FBlock f $ BFirst n
674 entry n = JustC [entryLabel n]
675
676 instance ShapeLifter O O where
677 unit = BMiddle
678 elift _ f = f
679 elower _ _ f = f
680 ftransfer (FwdPass {fp_transfer = FwdTransfers (_, ft, _)}) n f = ft n f
681 btransfer (BwdPass {bp_transfer = BwdTransfers (_, bt, _)}) n f = bt n f
682 frewrite (FwdPass {fp_rewrite = FwdRewrites (_, fr, _)}) n f = fr n f
683 brewrite (BwdPass {bp_rewrite = BwdRewrites (_, br, _)}) n f = br n f
684 spliceRgNode (GMany e body (JustO (FBlock f x))) _ n = GMany e body (JustO x')
685 where x' = FBlock f $ BHead x n
686 spliceRgNode (GNil) f n = GUnit $ FBlock f $ BMiddle n
687 spliceRgNode (GUnit (FBlock f b)) _ n = GUnit $ FBlock f $ b `BCat` BMiddle n
688 entry _ = NothingC
689
690 instance ShapeLifter O C where
691 unit = BLast
692 elift _ f = f
693 elower _ _ f = f
694 ftransfer (FwdPass {fp_transfer = FwdTransfers (_, _, ft)}) n f = ft n f
695 btransfer (BwdPass {bp_transfer = BwdTransfers (_, _, bt)}) n f = bt n f
696 frewrite (FwdPass {fp_rewrite = FwdRewrites (_, _, fr)}) n f = fr n f
697 brewrite (BwdPass {bp_rewrite = BwdRewrites (_, _, br)}) n f = br n f
698 spliceRgNode (GMany e b1 (JustO (FBlock f x))) _ n = GMany e body' NothingO
699 where body' = unionLabelMap b1 b2
700 b2 = addBlock (FBlock f $ BClosed x $ BLast n) emptyMap
701 spliceRgNode (GNil) f n = GMany e emptyMap NothingO
702 where e = JustO $ FBlock f $ BLast n
703 spliceRgNode (GUnit (FBlock f b)) _ n = GMany e emptyMap NothingO
704 where e = JustO $ FBlock f (b `U.cat` BLast n)
705 entry _ = NothingC
706
707 -- Fact lookup: the fact `orelse` bottom
708 lookupF :: FwdPass n f -> Label -> FactBase f -> f
709 lookupF = getFact . fp_lattice
710
711 getFact :: DataflowLattice f -> Label -> FactBase f -> f
712 getFact lat l fb = case lookupFact fb l of Just f -> f
713 Nothing -> fact_bot lat