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