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