8bf2ec7707a7e58d86bd1d729666861982f8932a
[packages/hoopl.git] / src / Compiler / Hoopl / Dataflow.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.Dataflow
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 m n f
109 = FwdPass { fp_lattice :: DataflowLattice f
110 , fp_transfer :: FwdTransfer n f
111 , fp_rewrite :: FwdRewrite m 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 m n f
121 = FwdRewrites { getFRewrites ::
122 ( n C O -> f -> Maybe (FwdRes m n f C O)
123 , n O O -> f -> Maybe (FwdRes m n f O O)
124 , n O C -> f -> Maybe (FwdRes m n f O C)
125 ) }
126 data FwdRes m n f e x = FwdRes (AGraph m n e x) (FwdRewrite m 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 m n f C O))
139 -> (n O O -> f -> Maybe (FwdRes m n f O O))
140 -> (n O C -> f -> Maybe (FwdRes m n f O C))
141 -> FwdRewrite m n f
142 mkFRewrite f m l = FwdRewrites (f, m, l)
143
144 mkFRewrite' :: (forall e x . n e x -> f -> Maybe (FwdRes m n f e x)) -> FwdRewrite m 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 m n f e x entries. (FuelMonad m, Edges n, LabelsPtr entries)
156 => FwdPass m n f
157 -> MaybeC e entries
158 -> Graph n e x -> Fact e f
159 -> m (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 Entries e = MaybeC e [Label]
178
179 arfGraph :: forall m n f e x .
180 (Edges n, FuelMonad m) => FwdPass m n f ->
181 Entries e -> Graph n e x -> Fact e f -> m (RG f n e x, Fact x f)
182 arfGraph pass entries = graph
183 where
184 {- nested type synonyms would be so lovely here
185 type ARF thing = forall e x . thing e x -> f -> m (RG f n e x, Fact x f)
186 type ARFX thing = forall e x . thing e x -> Fact e f -> m (RG f n e x, Fact x f)
187 -}
188 graph :: Graph n e x -> Fact e f -> m (RG f n e x, Fact x f)
189 block :: forall e x . Block n e x -> f -> m (RG f n e x, Fact x f)
190 node :: forall e x . (ShapeLifter e x)
191 => n e x -> f -> m (RG f n e x, Fact x f)
192 body :: [Label] -> Body n -> Fact C f -> m (RG f n C C, Fact C f)
193 -- Outgoing factbase is restricted to Labels *not* in
194 -- in the Body; the facts for Labels *in*
195 -- the Body are in the 'RG f n C C'
196 cat :: forall m e a x info info' info''. Monad m =>
197 (info -> m (RG f n e a, info'))
198 -> (info' -> m (RG f n a x, info''))
199 -> (info -> m (RG f n e x, info''))
200
201 graph GNil = \f -> return (rgnil, f)
202 graph (GUnit blk) = block blk
203 graph (GMany e bdy x) = (e `ebcat` bdy) `cat` exit x
204 where
205 ebcat :: MaybeO e (Block n O C) -> Body n -> Fact e f -> m (RG f n e C, Fact C f)
206 exit :: MaybeO x (Block n C O) -> Fact C f -> m (RG f n C x, Fact x f)
207 exit (JustO blk) = arfx block blk
208 exit NothingO = \fb -> return (rgnilC, fb)
209 ebcat entry bdy = c entries entry
210 where c :: MaybeC e [Label] -> MaybeO e (Block n O C)
211 -> Fact e f -> m (RG f n e C, Fact C f)
212 c NothingC (JustO entry) = block entry `cat` body (successors entry) bdy
213 c (JustC entries) NothingO = body entries bdy
214
215 -- Lift from nodes to blocks
216 block (BFirst n) = node n
217 block (BMiddle n) = node n
218 block (BLast n) = node n
219 block (BCat b1 b2) = block b1 `cat` block b2
220 block (BHead h n) = block h `cat` node n
221 block (BTail n t) = node n `cat` block t
222 block (BClosed h t)= block h `cat` block t
223
224 node thenode f
225 = do { mb_g <- withFuel (frewrite pass thenode f)
226 ; case mb_g of
227 Nothing -> return (rgunit f (unit thenode),
228 ftransfer pass thenode f)
229 Just (FwdRes ag rw) ->
230 do { g <- graphOfAGraph ag
231 ; let pass' = pass { fp_rewrite = rw }
232 ; arfGraph pass' (entry thenode) g (elift thenode f) } }
233
234 -- | Compose fact transformers and concatenate the resulting
235 -- rewritten graphs.
236 {-# INLINE cat #-}
237 cat ft1 ft2 f = do { (g1,f1) <- ft1 f
238 ; (g2,f2) <- ft2 f1
239 ; return (g1 `rgCat` g2, f2) }
240
241 arfx :: forall thing x .
242 Edges thing
243 => (thing C x -> f -> m (RG f n C x, Fact x f))
244 -> (thing C x -> Fact C f -> m (RG f n C x, Fact x f))
245 arfx arf thing fb =
246 arf thing $ fromJust $ lookupFact (joinInFacts lattice fb) $ entryLabel thing
247 where lattice = fp_lattice pass
248 -- joinInFacts adds debugging information
249
250
251 -- Outgoing factbase is restricted to Labels *not* in
252 -- in the Body; the facts for Labels *in*
253 -- the Body are in the 'RG f n C C'
254 body entries blocks init_fbase
255 = fixpoint True (fp_lattice pass) do_block init_fbase $
256 forwardBlockList entries blocks
257 where
258 do_block b f = do (g, fb) <- block b $ lookupF pass (entryLabel b) f
259 return (g, factBaseList fb)
260
261
262
263 -- Join all the incoming facts with bottom.
264 -- We know the results _shouldn't change_, but the transfer
265 -- functions might, for example, generate some debugging traces.
266 joinInFacts :: DataflowLattice f -> FactBase f -> FactBase f
267 joinInFacts (DataflowLattice {fact_bot = bot, fact_extend = fe}) fb =
268 mkFactBase $ map botJoin $ factBaseList fb
269 where botJoin (l, f) = (l, snd $ fe l (OldFact bot) (NewFact f))
270
271 forwardBlockList :: (Edges n, LabelsPtr entry)
272 => entry -> Body n -> [Block n C C]
273 -- This produces a list of blocks in order suitable for forward analysis,
274 -- along with the list of Labels it may depend on for facts.
275 forwardBlockList entries (Body blks) = postorder_dfs_from blks entries
276
277 -----------------------------------------------------------------------------
278 -- Backward analysis and rewriting: the interface
279 -----------------------------------------------------------------------------
280
281 data BwdPass m n f
282 = BwdPass { bp_lattice :: DataflowLattice f
283 , bp_transfer :: BwdTransfer n f
284 , bp_rewrite :: BwdRewrite m n f }
285
286 newtype BwdTransfer n f
287 = BwdTransfers { getBTransfers ::
288 ( n C O -> f -> f
289 , n O O -> f -> f
290 , n O C -> FactBase f -> f
291 ) }
292 newtype BwdRewrite m n f
293 = BwdRewrites { getBRewrites ::
294 ( n C O -> f -> Maybe (BwdRes m n f C O)
295 , n O O -> f -> Maybe (BwdRes m n f O O)
296 , n O C -> FactBase f -> Maybe (BwdRes m n f O C)
297 ) }
298 data BwdRes m n f e x = BwdRes (AGraph m n e x) (BwdRewrite m n f)
299
300 mkBTransfer :: (n C O -> f -> f) -> (n O O -> f -> f) ->
301 (n O C -> FactBase f -> f) -> BwdTransfer n f
302 mkBTransfer f m l = BwdTransfers (f, m, l)
303
304 mkBTransfer' :: (forall e x . n e x -> Fact x f -> f) -> BwdTransfer n f
305 mkBTransfer' f = BwdTransfers (f, f, f)
306
307 mkBRewrite :: (n C O -> f -> Maybe (BwdRes m n f C O))
308 -> (n O O -> f -> Maybe (BwdRes m n f O O))
309 -> (n O C -> FactBase f -> Maybe (BwdRes m n f O C))
310 -> BwdRewrite m n f
311 mkBRewrite f m l = BwdRewrites (f, m, l)
312
313 mkBRewrite' :: (forall e x . n e x -> Fact x f -> Maybe (BwdRes m n f e x))
314 -> BwdRewrite m n f
315 mkBRewrite' f = BwdRewrites (f, f, f)
316
317
318 -----------------------------------------------------------------------------
319 -- Backward implementation
320 -----------------------------------------------------------------------------
321
322 arbGraph :: forall m n f e x .
323 (Edges n, FuelMonad m) => BwdPass m n f ->
324 Entries e -> Graph n e x -> Fact x f -> m (RG f n e x, Fact e f)
325 arbGraph pass entries = graph
326 where
327 {- nested type synonyms would be so lovely here
328 type ARB thing = forall e x . thing e x -> Fact x f -> m (RG f n e x, f)
329 type ARBX thing = forall e x . thing e x -> Fact x f -> m (RG f n e x, Fact e f)
330 -}
331 graph :: Graph n e x -> Fact x f -> m (RG f n e x, Fact e f)
332 block :: forall e x . Block n e x -> Fact x f -> m (RG f n e x, f)
333 node :: forall e x . (ShapeLifter e x)
334 => n e x -> Fact x f -> m (RG f n e x, f)
335 body :: [Label] -> Body n -> Fact C f -> m (RG f n C C, Fact C f)
336 cat :: forall e a x info info' info''.
337 (info' -> m (RG f n e a, info''))
338 -> (info -> m (RG f n a x, info'))
339 -> (info -> m (RG f n e x, info''))
340
341 graph GNil = \f -> return (rgnil, f)
342 graph (GUnit blk) = block blk
343 graph (GMany e bdy x) = (e `ebcat` bdy) `cat` exit x
344 where
345 ebcat :: MaybeO e (Block n O C) -> Body n -> Fact C f -> m (RG f n e C, Fact e f)
346 exit :: MaybeO x (Block n C O) -> Fact x f -> m (RG f n C x, Fact C f)
347 exit (JustO blk) = arbx block blk
348 exit NothingO = \fb -> return (rgnilC, fb)
349 ebcat entry bdy = c entries entry
350 where c :: MaybeC e [Label] -> MaybeO e (Block n O C)
351 -> Fact C f -> m (RG f n e C, Fact e f)
352 c NothingC (JustO entry) = block entry `cat` body (successors entry) bdy
353 c (JustC entries) NothingO = body entries bdy
354
355 -- Lift from nodes to blocks
356 block (BFirst n) = node n
357 block (BMiddle n) = node n
358 block (BLast n) = node n
359 block (BCat b1 b2) = block b1 `cat` block b2
360 block (BHead h n) = block h `cat` node n
361 block (BTail n t) = node n `cat` block t
362 block (BClosed h t)= block h `cat` block t
363
364 node thenode f
365 = do { mb_g <- withFuel (brewrite pass thenode f)
366 ; case mb_g of
367 Nothing -> return (rgunit entry_f (unit thenode), entry_f)
368 where entry_f = btransfer pass thenode f
369 Just (BwdRes ag rw) ->
370 do { g <- graphOfAGraph ag
371 ; let pass' = pass { bp_rewrite = rw }
372 ; (g, f) <- arbGraph pass' (entry thenode) g f
373 ; return (g, elower (bp_lattice pass) thenode f)} }
374
375 -- | Compose fact transformers and concatenate the resulting
376 -- rewritten graphs.
377 {-# INLINE cat #-}
378 cat ft1 ft2 f = do { (g2,f2) <- ft2 f
379 ; (g1,f1) <- ft1 f2
380 ; return (g1 `rgCat` g2, f1) }
381
382 arbx :: forall thing x .
383 Edges thing
384 => (thing C x -> Fact x f -> m (RG f n C x, f))
385 -> (thing C x -> Fact x f -> m (RG f n C x, Fact C f))
386
387 arbx arb thing f = do { (rg, f) <- arb thing f
388 ; let fb = joinInFacts (bp_lattice pass) $
389 mkFactBase [(entryLabel thing, f)]
390 ; return (rg, fb) }
391 -- joinInFacts adds debugging information
392
393 -- Outgoing factbase is restricted to Labels *not* in
394 -- in the Body; the facts for Labels *in*
395 -- the Body are in the 'RG f n C C'
396 body entries blocks init_fbase
397 = fixpoint False (bp_lattice pass) do_block init_fbase $
398 backwardBlockList entries blocks
399 where
400 do_block b f = do (g, f) <- block b f
401 return (g, [(entryLabel b, f)])
402
403
404 backwardBlockList :: (LabelsPtr entries, Edges n) => entries -> Body n -> [Block n C C]
405 -- This produces a list of blocks in order suitable for backward analysis,
406 -- along with the list of Labels it may depend on for facts.
407 backwardBlockList entries body = reverse $ forwardBlockList entries body
408
409 {-
410
411 The forward and backward cases are not dual. In the forward case, the
412 entry points are known, and one simply traverses the body blocks from
413 those points. In the backward case, something is known about the exit
414 points, but this information is essentially useless, because we don't
415 actually have a dual graph (that is, one with edges reversed) to
416 compute with. (Even if we did have a dual graph, it would not avail
417 us---a backward analysis must include reachable blocks that don't
418 reach the exit, as in a procedure that loops forever and has side
419 effects.)
420
421 -}
422
423
424 -- | if the graph being analyzed is open at the exit, I don't
425 -- quite understand the implications of possible other exits
426 analyzeAndRewriteBwd
427 :: (FuelMonad m, Edges n, LabelsPtr entries)
428 => BwdPass m n f
429 -> MaybeC e entries -> Graph n e x -> Fact x f
430 -> m (Graph n e x, FactBase f, MaybeO e f)
431 analyzeAndRewriteBwd pass entries g f =
432 do (rg, fout) <- arbGraph pass (fmap targetLabels entries) g f
433 let (g', fb) = normalizeGraph rg
434 return (g', fb, distinguishedEntryFact g' fout)
435
436 distinguishedEntryFact :: forall n e x f . Graph n e x -> Fact e f -> MaybeO e f
437 distinguishedEntryFact g f = maybe g
438 where maybe :: Graph n e x -> MaybeO e f
439 maybe GNil = JustO f
440 maybe (GUnit {}) = JustO f
441 maybe (GMany e _ _) = case e of NothingO -> NothingO
442 JustO _ -> JustO f
443
444 -----------------------------------------------------------------------------
445 -- fixpoint: finding fixed points
446 -----------------------------------------------------------------------------
447
448 data TxFactBase n f
449 = TxFB { tfb_fbase :: FactBase f
450 , tfb_rg :: RG f n C C -- Transformed blocks
451 , tfb_cha :: ChangeFlag
452 , tfb_lbls :: LabelSet }
453 -- Note [TxFactBase change flag]
454 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
455 -- Set the tfb_cha flag iff
456 -- (a) the fact in tfb_fbase for or a block L changes
457 -- (b) L is in tfb_lbls.
458 -- The tfb_lbls are all Labels of the *original*
459 -- (not transformed) blocks
460
461 updateFact :: DataflowLattice f -> LabelSet -> (Label, f)
462 -> (ChangeFlag, FactBase f)
463 -> (ChangeFlag, FactBase f)
464 -- See Note [TxFactBase change flag]
465 updateFact lat lbls (lbl, new_fact) (cha, fbase)
466 | NoChange <- cha2 = (cha, fbase)
467 | lbl `elemLabelSet` lbls = (SomeChange, new_fbase)
468 | otherwise = (cha, new_fbase)
469 where
470 (cha2, res_fact) -- Note [Unreachable blocks]
471 = case lookupFact fbase lbl of
472 Nothing -> (SomeChange, snd $ join $ fact_bot lat) -- Note [Unreachable blocks]
473 Just old_fact -> join old_fact
474 where join old_fact = fact_extend lat lbl (OldFact old_fact) (NewFact new_fact)
475 new_fbase = extendFactBase fbase lbl res_fact
476
477 fixpoint :: forall m block n f. (FuelMonad m, Edges n, Edges (block n))
478 => Bool -- Going forwards?
479 -> DataflowLattice f
480 -> (block n C C -> FactBase f -> m (RG f n C C, [(Label, f)]))
481 -> FactBase f
482 -> [block n C C]
483 -> m (RG f n C C, FactBase f)
484 fixpoint is_fwd lat do_block init_fbase untagged_blocks
485 = do { fuel <- getFuel
486 ; tx_fb <- loop fuel init_fbase
487 ; return (tfb_rg tx_fb,
488 tfb_fbase tx_fb `delFromFactBase` map fst blocks) }
489 -- The successors of the Graph are the the Labels for which
490 -- we have facts, that are *not* in the blocks of the graph
491 where
492 blocks = map tag untagged_blocks
493 where tag b = ((entryLabel b, b), if is_fwd then [entryLabel b] else successors b)
494
495 tx_blocks :: [((Label, block n C C), [Label])] -- I do not understand this type
496 -> TxFactBase n f -> m (TxFactBase n f)
497 tx_blocks [] tx_fb = return tx_fb
498 tx_blocks (((lbl,blk), deps):bs) tx_fb = tx_block lbl blk deps tx_fb >>= tx_blocks bs
499 -- "deps" == Labels the block may _depend_ upon for facts
500
501 tx_block :: Label -> block n C C -> [Label]
502 -> TxFactBase n f -> m (TxFactBase n f)
503 tx_block lbl blk deps tx_fb@(TxFB { tfb_fbase = fbase, tfb_lbls = lbls
504 , tfb_rg = blks, tfb_cha = cha })
505 | is_fwd && not (lbl `elemFactBase` fbase)
506 = return tx_fb {tfb_lbls = lbls `unionLabelSet` mkLabelSet deps} -- Note [Unreachable blocks]
507 | otherwise
508 = do { (rg, out_facts) <- do_block blk fbase
509 ; let (cha',fbase')
510 = foldr (updateFact lat lbls) (cha,fbase) out_facts
511 lbls' = lbls `unionLabelSet` mkLabelSet deps
512 ; return (TxFB { tfb_lbls = lbls'
513 , tfb_rg = rg `rgCat` blks
514 , tfb_fbase = fbase', tfb_cha = cha' }) }
515
516 loop :: Fuel -> FactBase f -> m (TxFactBase n f)
517 loop fuel fbase
518 = do { let init_tx_fb = TxFB { tfb_fbase = fbase
519 , tfb_cha = NoChange
520 , tfb_rg = rgnilC
521 , tfb_lbls = emptyLabelSet }
522 ; tx_fb <- tx_blocks blocks init_tx_fb
523 ; case tfb_cha tx_fb of
524 NoChange -> return tx_fb
525 SomeChange -> do { setFuel fuel
526 ; loop fuel (tfb_fbase tx_fb) } }
527
528 {- Note [Unreachable blocks]
529 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
530 A block that is not in the domain of tfb_fbase is "currently unreachable".
531 A currently-unreachable block is not even analyzed. Reason: consider
532 constant prop and this graph, with entry point L1:
533 L1: x:=3; goto L4
534 L2: x:=4; goto L4
535 L4: if x>3 goto L2 else goto L5
536 Here L2 is actually unreachable, but if we process it with bottom input fact,
537 we'll propagate (x=4) to L4, and nuke the otherwise-good rewriting of L4.
538
539 * If a currently-unreachable block is not analyzed, then its rewritten
540 graph will not be accumulated in tfb_rg. And that is good:
541 unreachable blocks simply do not appear in the output.
542
543 * Note that clients must be careful to provide a fact (even if bottom)
544 for each entry point. Otherwise useful blocks may be garbage collected.
545
546 * Note that updateFact must set the change-flag if a label goes from
547 not-in-fbase to in-fbase, even if its fact is bottom. In effect the
548 real fact lattice is
549 UNR
550 bottom
551 the points above bottom
552
553 * Even if the fact is going from UNR to bottom, we still call the
554 client's fact_extend function because it might give the client
555 some useful debugging information.
556
557 * All of this only applies for *forward* fixpoints. For the backward
558 case we must treat every block as reachable; it might finish with a
559 'return', and therefore have no successors, for example.
560 -}
561
562 -----------------------------------------------------------------------------
563 -- RG: an internal data type for graphs under construction
564 -- TOTALLY internal to Hoopl; each block carries its fact
565 -----------------------------------------------------------------------------
566
567 type RG f n e x = Graph' (FBlock f) n e x
568 data FBlock f n e x = FBlock f (Block n e x)
569 instance Edges n => Edges (FBlock f n) where
570 entryLabel (FBlock _ b) = entryLabel b
571 successors (FBlock _ b) = successors b
572
573 --- constructors
574
575 rgnil :: RG f n O O
576 rgnilC :: RG f n C C
577 rgunit :: Edges n => f -> Block n e x -> RG f n e x
578 rgCat :: Edges n => RG f n e a -> RG f n a x -> RG f n e x
579
580 ---- observers
581
582 type GraphWithFacts n f e x = (Graph n e x, FactBase f)
583 -- A Graph together with the facts for that graph
584 -- The domains of the two maps should be identical
585
586 normalizeGraph :: forall n f e x .
587 Edges n => RG f n e x -> GraphWithFacts n f e x
588
589 normalizeGraph g = (graphMapBlocks dropFact g, facts g)
590 where dropFact (FBlock _ b) = b
591 facts :: RG f n e x -> FactBase f
592 facts GNil = noFacts
593 facts (GUnit _) = noFacts
594 facts (GMany _ body exit) = bodyFacts body `unionFactBase` exitFacts exit
595 exitFacts :: MaybeO x (FBlock f n C O) -> FactBase f
596 exitFacts NothingO = noFacts
597 exitFacts (JustO (FBlock f b)) = mkFactBase [(entryLabel b, f)]
598 bodyFacts :: Body' (FBlock f) n -> FactBase f
599 bodyFacts (Body body) = foldLabelMap f noFacts body
600 where f (FBlock f b) fb = extendFactBase fb (entryLabel b) f
601
602 --- implementation of the constructors (boring)
603
604 rgnil = GNil
605 rgnilC = GMany NothingO emptyBody NothingO
606
607 rgunit f b@(BFirst {}) = gUnitCO (FBlock f b)
608 rgunit f b@(BMiddle {}) = gUnitOO (FBlock f b)
609 rgunit f b@(BLast {}) = gUnitOC (FBlock f b)
610 rgunit f b@(BCat {}) = gUnitOO (FBlock f b)
611 rgunit f b@(BHead {}) = gUnitCO (FBlock f b)
612 rgunit f b@(BTail {}) = gUnitOC (FBlock f b)
613 rgunit f b@(BClosed {}) = gUnitCC (FBlock f b)
614
615 rgCat = U.splice fzCat
616 where fzCat (FBlock f b1) (FBlock _ b2) = FBlock f (b1 `U.cat` b2)
617
618 ----------------------------------------------------------------
619 -- Utilities
620 ----------------------------------------------------------------
621
622 -- Lifting based on shape:
623 -- - from nodes to blocks
624 -- - from facts to fact-like things
625 -- Lowering back:
626 -- - from fact-like things to facts
627 -- Note that the latter two functions depend only on the entry shape.
628 class ShapeLifter e x where
629 unit :: n e x -> Block n e x
630 elift :: Edges n => n e x -> f -> Fact e f
631 elower :: Edges n => DataflowLattice f -> n e x -> Fact e f -> f
632 ftransfer :: FwdPass m n f -> n e x -> f -> Fact x f
633 btransfer :: BwdPass m n f -> n e x -> Fact x f -> f
634 frewrite :: FwdPass m n f -> n e x -> f -> Maybe (FwdRes m n f e x)
635 brewrite :: BwdPass m n f -> n e x -> Fact x f -> Maybe (BwdRes m n f e x)
636 entry :: Edges n => n e x -> Entries e
637
638 instance ShapeLifter C O where
639 unit = BFirst
640 elift n f = mkFactBase [(entryLabel n, f)]
641 elower lat n fb = getFact lat (entryLabel n) fb
642 ftransfer (FwdPass {fp_transfer = FwdTransfers (ft, _, _)}) n f = ft n f
643 btransfer (BwdPass {bp_transfer = BwdTransfers (bt, _, _)}) n f = bt n f
644 frewrite (FwdPass {fp_rewrite = FwdRewrites (fr, _, _)}) n f = fr n f
645 brewrite (BwdPass {bp_rewrite = BwdRewrites (br, _, _)}) n f = br n f
646 entry n = JustC [entryLabel n]
647
648 instance ShapeLifter O O where
649 unit = BMiddle
650 elift _ f = f
651 elower _ _ f = f
652 ftransfer (FwdPass {fp_transfer = FwdTransfers (_, ft, _)}) n f = ft n f
653 btransfer (BwdPass {bp_transfer = BwdTransfers (_, bt, _)}) n f = bt n f
654 frewrite (FwdPass {fp_rewrite = FwdRewrites (_, fr, _)}) n f = fr n f
655 brewrite (BwdPass {bp_rewrite = BwdRewrites (_, br, _)}) n f = br n f
656 entry _ = NothingC
657
658 instance ShapeLifter O C where
659 unit = BLast
660 elift _ f = f
661 elower _ _ f = f
662 ftransfer (FwdPass {fp_transfer = FwdTransfers (_, _, ft)}) n f = ft n f
663 btransfer (BwdPass {bp_transfer = BwdTransfers (_, _, bt)}) n f = bt n f
664 frewrite (FwdPass {fp_rewrite = FwdRewrites (_, _, fr)}) n f = fr n f
665 brewrite (BwdPass {bp_rewrite = BwdRewrites (_, _, br)}) n f = br n f
666 entry _ = NothingC
667
668 -- Fact lookup: the fact `orelse` bottom
669 lookupF :: FwdPass m n f -> Label -> FactBase f -> f
670 lookupF = getFact . fp_lattice
671
672 getFact :: DataflowLattice f -> Label -> FactBase f -> f
673 getFact lat l fb = case lookupFact fb l of Just f -> f
674 Nothing -> fact_bot lat