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