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