Make Hoopl work with MonoLocalBinds.
[packages/hoopl.git] / src / Compiler / Hoopl / Dataflow.hs
1 {-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs, EmptyDataDecls, PatternGuards, TypeFamilies, MultiParamTypeClasses #-}
2
3 module Compiler.Hoopl.Dataflow
4 ( DataflowLattice(..), JoinFun, OldFact(..), NewFact(..), Fact, mkFactBase
5 , ChangeFlag(..), changeIf
6 , FwdPass(..), FwdTransfer, mkFTransfer, mkFTransfer3, getFTransfer3
7 -- * Respecting Fuel
8
9 -- $fuel
10 , FwdRewrite, mkFRewrite, mkFRewrite3, getFRewrite3, noFwdRewrite
11 , wrapFR, wrapFR2
12 , BwdPass(..), BwdTransfer, mkBTransfer, mkBTransfer3, getBTransfer3
13 , wrapBR, wrapBR2
14 , BwdRewrite, mkBRewrite, mkBRewrite3, getBRewrite3, noBwdRewrite
15 , analyzeAndRewriteFwd, analyzeAndRewriteBwd
16 )
17 where
18
19 import Control.Monad
20 import Data.Maybe
21
22 import Compiler.Hoopl.Checkpoint
23 import Compiler.Hoopl.Collections
24 import Compiler.Hoopl.Fuel
25 import Compiler.Hoopl.Graph hiding (Graph) -- hiding so we can redefine
26 -- and include definition in paper
27 import qualified Compiler.Hoopl.GraphUtil as U
28 import Compiler.Hoopl.Label
29 import Compiler.Hoopl.Util
30
31 -----------------------------------------------------------------------------
32 -- DataflowLattice
33 -----------------------------------------------------------------------------
34
35 data DataflowLattice a = DataflowLattice
36 { fact_name :: String -- Documentation
37 , fact_bot :: a -- Lattice bottom element
38 , fact_join :: JoinFun a -- Lattice join plus change flag
39 -- (changes iff result > old fact)
40 }
41 -- ^ A transfer function might want to use the logging flag
42 -- to control debugging, as in for example, it updates just one element
43 -- in a big finite map. We don't want Hoopl to show the whole fact,
44 -- and only the transfer function knows exactly what changed.
45
46 type JoinFun a = Label -> OldFact a -> NewFact a -> (ChangeFlag, a)
47 -- the label argument is for debugging purposes only
48 newtype OldFact a = OldFact a
49 newtype NewFact a = NewFact a
50
51 data ChangeFlag = NoChange | SomeChange deriving (Eq, Ord)
52 changeIf :: Bool -> ChangeFlag
53 changeIf changed = if changed then SomeChange else NoChange
54
55
56 -- | 'mkFactBase' creates a 'FactBase' from a list of ('Label', fact)
57 -- pairs. If the same label appears more than once, the relevant facts
58 -- are joined.
59
60 mkFactBase :: forall f. DataflowLattice f -> [(Label, f)] -> FactBase f
61 mkFactBase lattice = foldl add mapEmpty
62 where add :: FactBase f -> (Label, f) -> FactBase f
63 add map (lbl, f) = mapInsert lbl newFact map
64 where newFact = case mapLookup lbl map of
65 Nothing -> f
66 Just f' -> snd $ join lbl (OldFact f') (NewFact f)
67 join = fact_join lattice
68
69
70 -----------------------------------------------------------------------------
71 -- Analyze and rewrite forward: the interface
72 -----------------------------------------------------------------------------
73
74 data FwdPass m n f
75 = FwdPass { fp_lattice :: DataflowLattice f
76 , fp_transfer :: FwdTransfer n f
77 , fp_rewrite :: FwdRewrite m n f }
78
79 newtype FwdTransfer n f
80 = FwdTransfer3 { getFTransfer3 ::
81 ( n C O -> f -> f
82 , n O O -> f -> f
83 , n O C -> f -> FactBase f
84 ) }
85
86 newtype FwdRewrite m n f -- see Note [Respects Fuel]
87 = FwdRewrite3 { getFRewrite3 ::
88 ( n C O -> f -> m (Maybe (Graph n C O, FwdRewrite m n f))
89 , n O O -> f -> m (Maybe (Graph n O O, FwdRewrite m n f))
90 , n O C -> f -> m (Maybe (Graph n O C, FwdRewrite m n f))
91 ) }
92
93 wrapFR :: (forall e x. (n e x -> f -> m (Maybe (Graph n e x, FwdRewrite m n f )))
94 -> (n' e x -> f' -> m' (Maybe (Graph n' e x, FwdRewrite m' n' f')))
95 )
96 -- ^ This argument may assume that any function passed to it
97 -- respects fuel, and it must return a result that respects fuel.
98 -> FwdRewrite m n f
99 -> FwdRewrite m' n' f' -- see Note [Respects Fuel]
100 wrapFR wrap (FwdRewrite3 (f, m, l)) = FwdRewrite3 (wrap f, wrap m, wrap l)
101 wrapFR2
102 :: (forall e x . (n1 e x -> f1 -> m1 (Maybe (Graph n1 e x, FwdRewrite m1 n1 f1))) ->
103 (n2 e x -> f2 -> m2 (Maybe (Graph n2 e x, FwdRewrite m2 n2 f2))) ->
104 (n3 e x -> f3 -> m3 (Maybe (Graph n3 e x, FwdRewrite m3 n3 f3)))
105 )
106 -- ^ This argument may assume that any function passed to it
107 -- respects fuel, and it must return a result that respects fuel.
108 -> FwdRewrite m1 n1 f1
109 -> FwdRewrite m2 n2 f2
110 -> FwdRewrite m3 n3 f3 -- see Note [Respects Fuel]
111 wrapFR2 wrap2 (FwdRewrite3 (f1, m1, l1)) (FwdRewrite3 (f2, m2, l2)) =
112 FwdRewrite3 (wrap2 f1 f2, wrap2 m1 m2, wrap2 l1 l2)
113
114
115 mkFTransfer3 :: (n C O -> f -> f)
116 -> (n O O -> f -> f)
117 -> (n O C -> f -> FactBase f)
118 -> FwdTransfer n f
119 mkFTransfer3 f m l = FwdTransfer3 (f, m, l)
120
121 mkFTransfer :: (forall e x . n e x -> f -> Fact x f) -> FwdTransfer n f
122 mkFTransfer f = FwdTransfer3 (f, f, f)
123
124 -- | Functions passed to 'mkFRewrite3' should not be aware of the fuel supply.
125 -- The result returned by 'mkFRewrite3' respects fuel.
126 mkFRewrite3 :: forall m n f. FuelMonad m
127 => (n C O -> f -> m (Maybe (Graph n C O)))
128 -> (n O O -> f -> m (Maybe (Graph n O O)))
129 -> (n O C -> f -> m (Maybe (Graph n O C)))
130 -> FwdRewrite m n f
131 mkFRewrite3 f m l = FwdRewrite3 (lift f, lift m, lift l)
132 where lift :: forall t t1 a. (t -> t1 -> m (Maybe a)) -> t -> t1 -> m (Maybe (a, FwdRewrite m n f))
133 lift rw node fact = liftM (liftM asRew) (withFuel =<< rw node fact)
134 asRew :: forall t. t -> (t, FwdRewrite m n f)
135 asRew g = (g, noFwdRewrite)
136
137 noFwdRewrite :: Monad m => FwdRewrite m n f
138 noFwdRewrite = FwdRewrite3 (noRewrite, noRewrite, noRewrite)
139
140 noRewrite :: Monad m => a -> b -> m (Maybe c)
141 noRewrite _ _ = return Nothing
142
143
144
145 -- | Functions passed to 'mkFRewrite' should not be aware of the fuel supply.
146 -- The result returned by 'mkFRewrite' respects fuel.
147 mkFRewrite :: FuelMonad m => (forall e x . n e x -> f -> m (Maybe (Graph n e x)))
148 -> FwdRewrite m n f
149 mkFRewrite f = mkFRewrite3 f f f
150
151
152 type family Fact x f :: *
153 type instance Fact C f = FactBase f
154 type instance Fact O f = f
155
156 -- | if the graph being analyzed is open at the entry, there must
157 -- be no other entry point, or all goes horribly wrong...
158 analyzeAndRewriteFwd
159 :: forall m n f e x entries. (CheckpointMonad m, NonLocal n, LabelsPtr entries)
160 => FwdPass m n f
161 -> MaybeC e entries
162 -> Graph n e x -> Fact e f
163 -> m (Graph n e x, FactBase f, MaybeO x f)
164 analyzeAndRewriteFwd pass entries g f =
165 do (rg, fout) <- arfGraph pass (fmap targetLabels entries) g f
166 let (g', fb) = normalizeGraph rg
167 return (g', fb, distinguishedExitFact g' fout)
168
169 distinguishedExitFact :: forall n e x f . Graph n e x -> Fact x f -> MaybeO x f
170 distinguishedExitFact g f = maybe g
171 where maybe :: Graph n e x -> MaybeO x f
172 maybe GNil = JustO f
173 maybe (GUnit {}) = JustO f
174 maybe (GMany _ _ x) = case x of NothingO -> NothingO
175 JustO _ -> JustO f
176
177 ----------------------------------------------------------------
178 -- Forward Implementation
179 ----------------------------------------------------------------
180
181 type Entries e = MaybeC e [Label]
182
183 arfGraph :: forall m n f e x .
184 (NonLocal n, CheckpointMonad m) => FwdPass m n f ->
185 Entries e -> Graph n e x -> Fact e f -> m (DG f n e x, Fact x f)
186 arfGraph pass entries = graph
187 where
188 {- nested type synonyms would be so lovely here
189 type ARF thing = forall e x . thing e x -> f -> m (DG f n e x, Fact x f)
190 type ARFX thing = forall e x . thing e x -> Fact e f -> m (DG f n e x, Fact x f)
191 -}
192 graph :: Graph n e x -> Fact e f -> m (DG f n e x, Fact x f)
193 -- @ start block.tex -2
194 block :: forall e x .
195 Block n e x -> f -> m (DG f n e x, Fact x f)
196 -- @ end block.tex
197 -- @ start node.tex -4
198 node :: forall e x . (ShapeLifter e x)
199 => n e x -> f -> m (DG f n e x, Fact x f)
200 -- @ end node.tex
201 -- @ start bodyfun.tex
202 body :: [Label] -> LabelMap (Block n C C)
203 -> Fact C f -> m (DG f n C C, Fact C f)
204 -- @ end bodyfun.tex
205 -- Outgoing factbase is restricted to Labels *not* in
206 -- in the Body; the facts for Labels *in*
207 -- the Body are in the 'DG f n C C'
208 -- @ start cat.tex -2
209 cat :: forall e a x f1 f2 f3.
210 (f1 -> m (DG f n e a, f2))
211 -> (f2 -> m (DG f n a x, f3))
212 -> (f1 -> m (DG f n e x, f3))
213 -- @ end cat.tex
214
215 graph GNil = \f -> return (dgnil, f)
216 graph (GUnit blk) = block blk
217 graph (GMany e bdy x) = (e `ebcat` bdy) `cat` exit x
218 where
219 ebcat :: MaybeO e (Block n O C) -> Body n -> Fact e f -> m (DG f n e C, Fact C f)
220 exit :: MaybeO x (Block n C O) -> Fact C f -> m (DG f n C x, Fact x f)
221 exit (JustO blk) = arfx block blk
222 exit NothingO = \fb -> return (dgnilC, fb)
223 ebcat entry bdy = c entries entry
224 where c :: MaybeC e [Label] -> MaybeO e (Block n O C)
225 -> Fact e f -> m (DG f n e C, Fact C f)
226 c NothingC (JustO entry) = block entry `cat` body (successors entry) bdy
227 c (JustC entries) NothingO = body entries bdy
228 c _ _ = error "bogus GADT pattern match failure"
229
230 -- Lift from nodes to blocks
231 -- @ start block.tex -2
232 block (BFirst n) = node n
233 block (BMiddle n) = node n
234 block (BLast n) = node n
235 block (BCat b1 b2) = block b1 `cat` block b2
236 -- @ end block.tex
237 block (BHead h n) = block h `cat` node n
238 block (BTail n t) = node n `cat` block t
239 block (BClosed h t)= block h `cat` block t
240
241 -- @ start node.tex -4
242 node n f
243 = do { grw <- frewrite pass n f
244 ; case grw of
245 Nothing -> return ( singletonDG f n
246 , ftransfer pass n f )
247 Just (g, rw) ->
248 let pass' = pass { fp_rewrite = rw }
249 f' = fwdEntryFact n f
250 in arfGraph pass' (fwdEntryLabel n) g f' }
251
252 -- @ end node.tex
253
254 -- | Compose fact transformers and concatenate the resulting
255 -- rewritten graphs.
256 {-# INLINE cat #-}
257 -- @ start cat.tex -2
258 cat ft1 ft2 f = do { (g1,f1) <- ft1 f
259 ; (g2,f2) <- ft2 f1
260 ; return (g1 `dgSplice` g2, f2) }
261 -- @ end cat.tex
262 arfx :: forall thing x .
263 NonLocal thing
264 => (thing C x -> f -> m (DG f n C x, Fact x f))
265 -> (thing C x -> Fact C f -> m (DG f n C x, Fact x f))
266 arfx arf thing fb =
267 arf thing $ fromJust $ lookupFact (entryLabel thing) $ joinInFacts lattice fb
268 where lattice = fp_lattice pass
269 -- joinInFacts adds debugging information
270
271
272 -- Outgoing factbase is restricted to Labels *not* in
273 -- in the Body; the facts for Labels *in*
274 -- the Body are in the 'DG f n C C'
275 -- @ start bodyfun.tex
276 body entries blockmap init_fbase
277 = fixpoint Fwd lattice do_block blocks init_fbase
278 where
279 blocks = forwardBlockList entries blockmap
280 lattice = fp_lattice pass
281 do_block :: forall x. Block n C x -> FactBase f -> m (DG f n C x, Fact x f)
282 do_block b fb = block b entryFact
283 where entryFact = getFact lattice (entryLabel b) fb
284 -- @ end bodyfun.tex
285
286
287 -- Join all the incoming facts with bottom.
288 -- We know the results _shouldn't change_, but the transfer
289 -- functions might, for example, generate some debugging traces.
290 joinInFacts :: DataflowLattice f -> FactBase f -> FactBase f
291 joinInFacts (lattice @ DataflowLattice {fact_bot = bot, fact_join = fj}) fb =
292 mkFactBase lattice $ map botJoin $ mapToList fb
293 where botJoin (l, f) = (l, snd $ fj l (OldFact bot) (NewFact f))
294
295 forwardBlockList :: (NonLocal n, LabelsPtr entry)
296 => entry -> Body n -> [Block n C C]
297 -- This produces a list of blocks in order suitable for forward analysis,
298 -- along with the list of Labels it may depend on for facts.
299 forwardBlockList entries blks = postorder_dfs_from blks entries
300
301 -----------------------------------------------------------------------------
302 -- Backward analysis and rewriting: the interface
303 -----------------------------------------------------------------------------
304
305 data BwdPass m n f
306 = BwdPass { bp_lattice :: DataflowLattice f
307 , bp_transfer :: BwdTransfer n f
308 , bp_rewrite :: BwdRewrite m n f }
309
310 newtype BwdTransfer n f
311 = BwdTransfer3 { getBTransfer3 ::
312 ( n C O -> f -> f
313 , n O O -> f -> f
314 , n O C -> FactBase f -> f
315 ) }
316 newtype BwdRewrite m n f
317 = BwdRewrite3 { getBRewrite3 ::
318 ( n C O -> f -> m (Maybe (Graph n C O, BwdRewrite m n f))
319 , n O O -> f -> m (Maybe (Graph n O O, BwdRewrite m n f))
320 , n O C -> FactBase f -> m (Maybe (Graph n O C, BwdRewrite m n f))
321 ) }
322
323 wrapBR :: (forall e x .
324 Shape x
325 -> (n e x -> Fact x f -> m (Maybe (Graph n e x, BwdRewrite m n f )))
326 -> (n' e x -> Fact x f' -> m' (Maybe (Graph n' e x, BwdRewrite m' n' f')))
327 )
328 -- ^ This argument may assume that any function passed to it
329 -- respects fuel, and it must return a result that respects fuel.
330 -> BwdRewrite m n f
331 -> BwdRewrite m' n' f' -- see Note [Respects Fuel]
332 wrapBR wrap (BwdRewrite3 (f, m, l)) =
333 BwdRewrite3 (wrap Open f, wrap Open m, wrap Closed l)
334
335 wrapBR2 :: (forall e x . Shape x
336 -> (n1 e x -> Fact x f1 -> m1 (Maybe (Graph n1 e x, BwdRewrite m1 n1 f1)))
337 -> (n2 e x -> Fact x f2 -> m2 (Maybe (Graph n2 e x, BwdRewrite m2 n2 f2)))
338 -> (n3 e x -> Fact x f3 -> m3 (Maybe (Graph n3 e x, BwdRewrite m3 n3 f3))))
339 -- ^ This argument may assume that any function passed to it
340 -- respects fuel, and it must return a result that respects fuel.
341 -> BwdRewrite m1 n1 f1
342 -> BwdRewrite m2 n2 f2
343 -> BwdRewrite m3 n3 f3 -- see Note [Respects Fuel]
344 wrapBR2 wrap2 (BwdRewrite3 (f1, m1, l1)) (BwdRewrite3 (f2, m2, l2)) =
345 BwdRewrite3 (wrap2 Open f1 f2, wrap2 Open m1 m2, wrap2 Closed l1 l2)
346
347
348
349 mkBTransfer3 :: (n C O -> f -> f) -> (n O O -> f -> f) ->
350 (n O C -> FactBase f -> f) -> BwdTransfer n f
351 mkBTransfer3 f m l = BwdTransfer3 (f, m, l)
352
353 mkBTransfer :: (forall e x . n e x -> Fact x f -> f) -> BwdTransfer n f
354 mkBTransfer f = BwdTransfer3 (f, f, f)
355
356 -- | Functions passed to 'mkBRewrite3' should not be aware of the fuel supply.
357 -- The result returned by 'mkBRewrite3' respects fuel.
358 mkBRewrite3 :: forall m n f. FuelMonad m
359 => (n C O -> f -> m (Maybe (Graph n C O)))
360 -> (n O O -> f -> m (Maybe (Graph n O O)))
361 -> (n O C -> FactBase f -> m (Maybe (Graph n O C)))
362 -> BwdRewrite m n f
363 mkBRewrite3 f m l = BwdRewrite3 (lift f, lift m, lift l)
364 where lift :: forall t t1 a. (t -> t1 -> m (Maybe a)) -> t -> t1 -> m (Maybe (a, BwdRewrite m n f))
365 lift rw node fact = liftM (liftM asRew) (withFuel =<< rw node fact)
366 asRew :: t -> (t, BwdRewrite m n f)
367 asRew g = (g, noBwdRewrite)
368
369 noBwdRewrite :: Monad m => BwdRewrite m n f
370 noBwdRewrite = BwdRewrite3 (noRewrite, noRewrite, noRewrite)
371
372 -- | Functions passed to 'mkBRewrite' should not be aware of the fuel supply.
373 -- The result returned by 'mkBRewrite' respects fuel.
374 mkBRewrite :: FuelMonad m
375 => (forall e x . n e x -> Fact x f -> m (Maybe (Graph n e x)))
376 -> BwdRewrite m n f
377 mkBRewrite f = mkBRewrite3 f f f
378
379
380 -----------------------------------------------------------------------------
381 -- Backward implementation
382 -----------------------------------------------------------------------------
383
384 arbGraph :: forall m n f e x .
385 (NonLocal n, CheckpointMonad m) => BwdPass m n f ->
386 Entries e -> Graph n e x -> Fact x f -> m (DG f n e x, Fact e f)
387 arbGraph pass entries = graph
388 where
389 {- nested type synonyms would be so lovely here
390 type ARB thing = forall e x . thing e x -> Fact x f -> m (DG f n e x, f)
391 type ARBX thing = forall e x . thing e x -> Fact x f -> m (DG f n e x, Fact e f)
392 -}
393 graph :: Graph n e x -> Fact x f -> m (DG f n e x, Fact e f)
394 block :: forall e x . Block n e x -> Fact x f -> m (DG f n e x, f)
395 node :: forall e x . (ShapeLifter e x)
396 => n e x -> Fact x f -> m (DG f n e x, f)
397 body :: [Label] -> Body n -> Fact C f -> m (DG f n C C, Fact C f)
398 cat :: forall e a x info info' info''.
399 (info' -> m (DG f n e a, info''))
400 -> (info -> m (DG f n a x, info'))
401 -> (info -> m (DG f n e x, info''))
402
403 graph GNil = \f -> return (dgnil, f)
404 graph (GUnit blk) = block blk
405 graph (GMany e bdy x) = (e `ebcat` bdy) `cat` exit x
406 where
407 ebcat :: MaybeO e (Block n O C) -> Body n -> Fact C f -> m (DG f n e C, Fact e f)
408 exit :: MaybeO x (Block n C O) -> Fact x f -> m (DG f n C x, Fact C f)
409 exit (JustO blk) = arbx block blk
410 exit NothingO = \fb -> return (dgnilC, fb)
411 ebcat entry bdy = c entries entry
412 where c :: MaybeC e [Label] -> MaybeO e (Block n O C)
413 -> Fact C f -> m (DG f n e C, Fact e f)
414 c NothingC (JustO entry) = block entry `cat` body (successors entry) bdy
415 c (JustC entries) NothingO = body entries bdy
416 c _ _ = error "bogus GADT pattern match failure"
417
418 -- Lift from nodes to blocks
419 block (BFirst n) = node n
420 block (BMiddle n) = node n
421 block (BLast n) = node n
422 block (BCat b1 b2) = block b1 `cat` block b2
423 block (BHead h n) = block h `cat` node n
424 block (BTail n t) = node n `cat` block t
425 block (BClosed h t)= block h `cat` block t
426
427 node n f
428 = do { bwdres <- brewrite pass n f
429 ; case bwdres of
430 Nothing -> return (singletonDG entry_f n, entry_f)
431 where entry_f = btransfer pass n f
432 Just (g, rw) ->
433 do { let pass' = pass { bp_rewrite = rw }
434 ; (g, f) <- arbGraph pass' (fwdEntryLabel n) g f
435 ; return (g, bwdEntryFact (bp_lattice pass) n f)} }
436
437 -- | Compose fact transformers and concatenate the resulting
438 -- rewritten graphs.
439 {-# INLINE cat #-}
440 cat ft1 ft2 f = do { (g2,f2) <- ft2 f
441 ; (g1,f1) <- ft1 f2
442 ; return (g1 `dgSplice` g2, f1) }
443
444 arbx :: forall thing x .
445 NonLocal thing
446 => (thing C x -> Fact x f -> m (DG f n C x, f))
447 -> (thing C x -> Fact x f -> m (DG f n C x, Fact C f))
448
449 arbx arb thing f = do { (rg, f) <- arb thing f
450 ; let fb = joinInFacts (bp_lattice pass) $
451 mapSingleton (entryLabel thing) f
452 ; return (rg, fb) }
453 -- joinInFacts adds debugging information
454
455 -- Outgoing factbase is restricted to Labels *not* in
456 -- in the Body; the facts for Labels *in*
457 -- the Body are in the 'DG f n C C'
458 body entries blockmap init_fbase
459 = fixpoint Bwd (bp_lattice pass) do_block blocks init_fbase
460 where
461 blocks = backwardBlockList entries blockmap
462 do_block :: forall x. Block n C x -> Fact x f -> m (DG f n C x, LabelMap f)
463 do_block b f = do (g, f) <- block b f
464 return (g, mapSingleton (entryLabel b) f)
465
466
467 backwardBlockList :: (LabelsPtr entries, NonLocal n) => entries -> Body n -> [Block n C C]
468 -- This produces a list of blocks in order suitable for backward analysis,
469 -- along with the list of Labels it may depend on for facts.
470 backwardBlockList entries body = reverse $ forwardBlockList entries body
471
472 {-
473
474 The forward and backward cases are not dual. In the forward case, the
475 entry points are known, and one simply traverses the body blocks from
476 those points. In the backward case, something is known about the exit
477 points, but this information is essentially useless, because we don't
478 actually have a dual graph (that is, one with edges reversed) to
479 compute with. (Even if we did have a dual graph, it would not avail
480 us---a backward analysis must include reachable blocks that don't
481 reach the exit, as in a procedure that loops forever and has side
482 effects.)
483
484 -}
485
486
487 -- | if the graph being analyzed is open at the exit, I don't
488 -- quite understand the implications of possible other exits
489 analyzeAndRewriteBwd
490 :: (CheckpointMonad m, NonLocal n, LabelsPtr entries)
491 => BwdPass m n f
492 -> MaybeC e entries -> Graph n e x -> Fact x f
493 -> m (Graph n e x, FactBase f, MaybeO e f)
494 analyzeAndRewriteBwd pass entries g f =
495 do (rg, fout) <- arbGraph pass (fmap targetLabels entries) g f
496 let (g', fb) = normalizeGraph rg
497 return (g', fb, distinguishedEntryFact g' fout)
498
499 distinguishedEntryFact :: forall n e x f . Graph n e x -> Fact e f -> MaybeO e f
500 distinguishedEntryFact g f = maybe g
501 where maybe :: Graph n e x -> MaybeO e f
502 maybe GNil = JustO f
503 maybe (GUnit {}) = JustO f
504 maybe (GMany e _ _) = case e of NothingO -> NothingO
505 JustO _ -> JustO f
506
507 -----------------------------------------------------------------------------
508 -- fixpoint: finding fixed points
509 -----------------------------------------------------------------------------
510 -- @ start txfb.tex
511 data TxFactBase n f
512 = TxFB { tfb_fbase :: FactBase f
513 , tfb_rg :: DG f n C C -- Transformed blocks
514 , tfb_cha :: ChangeFlag
515 , tfb_lbls :: LabelSet }
516 -- @ end txfb.tex
517 -- See Note [TxFactBase invariants]
518 -- @ start update.tex
519 updateFact :: DataflowLattice f -> LabelSet
520 -> Label -> f -> (ChangeFlag, FactBase f)
521 -> (ChangeFlag, FactBase f)
522 -- See Note [TxFactBase change flag]
523 updateFact lat lbls lbl new_fact (cha, fbase)
524 | NoChange <- cha2 = (cha, fbase)
525 | lbl `setMember` lbls = (SomeChange, new_fbase)
526 | otherwise = (cha, new_fbase)
527 where
528 (cha2, res_fact) -- Note [Unreachable blocks]
529 = case lookupFact lbl fbase of
530 Nothing -> (SomeChange, new_fact_debug) -- Note [Unreachable blocks]
531 Just old_fact -> join old_fact
532 where join old_fact =
533 fact_join lat lbl
534 (OldFact old_fact) (NewFact new_fact)
535 (_, new_fact_debug) = join (fact_bot lat)
536 new_fbase = mapInsert lbl res_fact fbase
537 -- @ end update.tex
538
539
540 {-
541 -- this doesn't work because it can't be implemented
542 class Monad m => FixpointMonad m where
543 observeChangedFactBase :: m (Maybe (FactBase f)) -> Maybe (FactBase f)
544 -}
545
546 -- @ start fptype.tex
547 data Direction = Fwd | Bwd
548 fixpoint :: forall m n f. (CheckpointMonad m, NonLocal n)
549 => Direction
550 -> DataflowLattice f
551 -> (Block n C C -> Fact C f -> m (DG f n C C, Fact C f))
552 -> [Block n C C]
553 -> (Fact C f -> m (DG f n C C, Fact C f))
554 -- @ end fptype.tex
555 -- @ start fpimp.tex
556 fixpoint direction lat do_block blocks init_fbase
557 = do { tx_fb <- loop init_fbase
558 ; return (tfb_rg tx_fb,
559 map (fst . fst) tagged_blocks
560 `mapDeleteList` tfb_fbase tx_fb ) }
561 -- The successors of the Graph are the the Labels
562 -- for which we have facts and which are *not* in
563 -- the blocks of the graph
564 where
565 tagged_blocks = map tag blocks
566 is_fwd = case direction of { Fwd -> True;
567 Bwd -> False }
568 tag :: NonLocal t => t C C -> ((Label, t C C), [Label])
569 tag b = ((entryLabel b, b),
570 if is_fwd then [entryLabel b]
571 else successors b)
572 -- 'tag' adds the in-labels of the block;
573 -- see Note [TxFactBase invairants]
574
575 tx_blocks :: [((Label, Block n C C), [Label])] -- I do not understand this type
576 -> TxFactBase n f -> m (TxFactBase n f)
577 tx_blocks [] tx_fb = return tx_fb
578 tx_blocks (((lbl,blk), in_lbls):bs) tx_fb
579 = tx_block lbl blk in_lbls tx_fb >>= tx_blocks bs
580 -- "in_lbls" == Labels the block may
581 -- _depend_ upon for facts
582
583 tx_block :: Label -> Block n C C -> [Label]
584 -> TxFactBase n f -> m (TxFactBase n f)
585 tx_block lbl blk in_lbls
586 tx_fb@(TxFB { tfb_fbase = fbase, tfb_lbls = lbls
587 , tfb_rg = blks, tfb_cha = cha })
588 | is_fwd && not (lbl `mapMember` fbase)
589 = return (tx_fb {tfb_lbls = lbls'}) -- Note [Unreachable blocks]
590 | otherwise
591 = do { (rg, out_facts) <- do_block blk fbase
592 ; let (cha', fbase') = mapFoldWithKey
593 (updateFact lat lbls)
594 (cha,fbase) out_facts
595 ; return $
596 TxFB { tfb_lbls = lbls'
597 , tfb_rg = rg `dgSplice` blks
598 , tfb_fbase = fbase'
599 , tfb_cha = cha' } }
600 where
601 lbls' = lbls `setUnion` setFromList in_lbls
602
603
604 loop :: FactBase f -> m (TxFactBase n f)
605 loop fbase
606 = do { s <- checkpoint
607 ; let init_tx :: TxFactBase n f
608 init_tx = TxFB { tfb_fbase = fbase
609 , tfb_cha = NoChange
610 , tfb_rg = dgnilC
611 , tfb_lbls = setEmpty }
612 ; tx_fb <- tx_blocks tagged_blocks init_tx
613 ; case tfb_cha tx_fb of
614 NoChange -> return tx_fb
615 SomeChange
616 -> do { restart s
617 ; loop (tfb_fbase tx_fb) } }
618 -- @ end fpimp.tex
619
620
621 {- Note [TxFactBase invariants]
622 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
623 The TxFactBase is used only during a fixpoint iteration (or "sweep"),
624 and accumulates facts (and the transformed code) during the fixpoint
625 iteration.
626
627 * tfb_fbase increases monotonically, across all sweeps
628
629 * At the beginning of each sweep
630 tfb_cha = NoChange
631 tfb_lbls = {}
632
633 * During each sweep we process each block in turn. Processing a block
634 is done thus:
635 1. Read from tfb_fbase the facts for its entry label (forward)
636 or successors labels (backward)
637 2. Transform those facts into new facts for its successors (forward)
638 or entry label (backward)
639 3. Augment tfb_fbase with that info
640 We call the labels read in step (1) the "in-labels" of the sweep
641
642 * The field tfb_lbls is the set of in-labels of all blocks that have
643 been processed so far this sweep, including the block that is
644 currently being processed. tfb_lbls is initialised to {}. It is a
645 subset of the Labels of the *original* (not transformed) blocks.
646
647 * The tfb_cha field is set to SomeChange iff we decide we need to
648 perform another iteration of the fixpoint loop. It is initialsed to NoChange.
649
650 Specifically, we set tfb_cha to SomeChange in step (3) iff
651 (a) The fact in tfb_fbase for a block L changes
652 (b) L is in tfb_lbls
653 Reason: until a label enters the in-labels its accumuated fact in tfb_fbase
654 has not been read, hence cannot affect the outcome
655
656 Note [Unreachable blocks]
657 ~~~~~~~~~~~~~~~~~~~~~~~~~
658 A block that is not in the domain of tfb_fbase is "currently unreachable".
659 A currently-unreachable block is not even analyzed. Reason: consider
660 constant prop and this graph, with entry point L1:
661 L1: x:=3; goto L4
662 L2: x:=4; goto L4
663 L4: if x>3 goto L2 else goto L5
664 Here L2 is actually unreachable, but if we process it with bottom input fact,
665 we'll propagate (x=4) to L4, and nuke the otherwise-good rewriting of L4.
666
667 * If a currently-unreachable block is not analyzed, then its rewritten
668 graph will not be accumulated in tfb_rg. And that is good:
669 unreachable blocks simply do not appear in the output.
670
671 * Note that clients must be careful to provide a fact (even if bottom)
672 for each entry point. Otherwise useful blocks may be garbage collected.
673
674 * Note that updateFact must set the change-flag if a label goes from
675 not-in-fbase to in-fbase, even if its fact is bottom. In effect the
676 real fact lattice is
677 UNR
678 bottom
679 the points above bottom
680
681 * Even if the fact is going from UNR to bottom, we still call the
682 client's fact_join function because it might give the client
683 some useful debugging information.
684
685 * All of this only applies for *forward* fixpoints. For the backward
686 case we must treat every block as reachable; it might finish with a
687 'return', and therefore have no successors, for example.
688 -}
689
690 -----------------------------------------------------------------------------
691 -- DG: an internal data type for 'decorated graphs'
692 -- TOTALLY internal to Hoopl; each block is decorated with a fact
693 -----------------------------------------------------------------------------
694
695 -- @ start dg.tex
696 type Graph = Graph' Block
697 type DG f = Graph' (DBlock f)
698 data DBlock f n e x = DBlock f (Block n e x) -- ^ block decorated with fact
699 -- @ end dg.tex
700 instance NonLocal n => NonLocal (DBlock f n) where
701 entryLabel (DBlock _ b) = entryLabel b
702 successors (DBlock _ b) = successors b
703
704 --- constructors
705
706 dgnil :: DG f n O O
707 dgnilC :: DG f n C C
708 dgSplice :: NonLocal n => DG f n e a -> DG f n a x -> DG f n e x
709
710 ---- observers
711
712 type GraphWithFacts n f e x = (Graph n e x, FactBase f)
713 -- A Graph together with the facts for that graph
714 -- The domains of the two maps should be identical
715
716 normalizeGraph :: forall n f e x .
717 NonLocal n => DG f n e x -> GraphWithFacts n f e x
718
719 normalizeGraph g = (graphMapBlocks dropFact g, facts g)
720 where dropFact :: DBlock t t1 t2 t3 -> Block t1 t2 t3
721 dropFact (DBlock _ b) = b
722 facts :: DG f n e x -> FactBase f
723 facts GNil = noFacts
724 facts (GUnit _) = noFacts
725 facts (GMany _ body exit) = bodyFacts body `mapUnion` exitFacts exit
726 exitFacts :: MaybeO x (DBlock f n C O) -> FactBase f
727 exitFacts NothingO = noFacts
728 exitFacts (JustO (DBlock f b)) = mapSingleton (entryLabel b) f
729 bodyFacts :: LabelMap (DBlock f n C C) -> FactBase f
730 bodyFacts body = mapFold f noFacts body
731 where f :: forall t a x. (NonLocal t) => DBlock a t C x -> LabelMap a -> LabelMap a
732 f (DBlock f b) fb = mapInsert (entryLabel b) f fb
733
734 --- implementation of the constructors (boring)
735
736 dgnil = GNil
737 dgnilC = GMany NothingO emptyBody NothingO
738
739 dgSplice = U.splice fzCat
740 where fzCat :: DBlock f n e O -> DBlock t n O x -> DBlock f n e x
741 fzCat (DBlock f b1) (DBlock _ b2) = DBlock f (b1 `U.cat` b2)
742
743 ----------------------------------------------------------------
744 -- Utilities
745 ----------------------------------------------------------------
746
747 -- Lifting based on shape:
748 -- - from nodes to blocks
749 -- - from facts to fact-like things
750 -- Lowering back:
751 -- - from fact-like things to facts
752 -- Note that the latter two functions depend only on the entry shape.
753 -- @ start node.tex
754 class ShapeLifter e x where
755 singletonDG :: f -> n e x -> DG f n e x
756 fwdEntryFact :: NonLocal n => n e x -> f -> Fact e f
757 fwdEntryLabel :: NonLocal n => n e x -> MaybeC e [Label]
758 ftransfer :: FwdPass m n f -> n e x -> f -> Fact x f
759 frewrite :: FwdPass m n f -> n e x
760 -> f -> m (Maybe (Graph n e x, FwdRewrite m n f))
761 -- @ end node.tex
762 bwdEntryFact :: NonLocal n => DataflowLattice f -> n e x -> Fact e f -> f
763 btransfer :: BwdPass m n f -> n e x -> Fact x f -> f
764 brewrite :: BwdPass m n f -> n e x
765 -> Fact x f -> m (Maybe (Graph n e x, BwdRewrite m n f))
766
767 instance ShapeLifter C O where
768 singletonDG f = gUnitCO . DBlock f . BFirst
769 fwdEntryFact n f = mapSingleton (entryLabel n) f
770 bwdEntryFact lat n fb = getFact lat (entryLabel n) fb
771 ftransfer (FwdPass {fp_transfer = FwdTransfer3 (ft, _, _)}) n f = ft n f
772 btransfer (BwdPass {bp_transfer = BwdTransfer3 (bt, _, _)}) n f = bt n f
773 frewrite (FwdPass {fp_rewrite = FwdRewrite3 (fr, _, _)}) n f = fr n f
774 brewrite (BwdPass {bp_rewrite = BwdRewrite3 (br, _, _)}) n f = br n f
775 fwdEntryLabel n = JustC [entryLabel n]
776
777 instance ShapeLifter O O where
778 singletonDG f = gUnitOO . DBlock f . BMiddle
779 fwdEntryFact _ f = f
780 bwdEntryFact _ _ f = f
781 ftransfer (FwdPass {fp_transfer = FwdTransfer3 (_, ft, _)}) n f = ft n f
782 btransfer (BwdPass {bp_transfer = BwdTransfer3 (_, bt, _)}) n f = bt n f
783 frewrite (FwdPass {fp_rewrite = FwdRewrite3 (_, fr, _)}) n f = fr n f
784 brewrite (BwdPass {bp_rewrite = BwdRewrite3 (_, br, _)}) n f = br n f
785 fwdEntryLabel _ = NothingC
786
787 instance ShapeLifter O C where
788 singletonDG f = gUnitOC . DBlock f . BLast
789 fwdEntryFact _ f = f
790 bwdEntryFact _ _ f = f
791 ftransfer (FwdPass {fp_transfer = FwdTransfer3 (_, _, ft)}) n f = ft n f
792 btransfer (BwdPass {bp_transfer = BwdTransfer3 (_, _, bt)}) n f = bt n f
793 frewrite (FwdPass {fp_rewrite = FwdRewrite3 (_, _, fr)}) n f = fr n f
794 brewrite (BwdPass {bp_rewrite = BwdRewrite3 (_, _, br)}) n f = br n f
795 fwdEntryLabel _ = NothingC
796
797 -- Fact lookup: the fact `orelse` bottom
798 getFact :: DataflowLattice f -> Label -> FactBase f -> f
799 getFact lat l fb = case lookupFact l fb of Just f -> f
800 Nothing -> fact_bot lat
801
802
803
804 {- Note [Respects fuel]
805 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
806 -}
807 -- $fuel
808 -- A value of type 'FwdRewrite' or 'BwdRewrite' /respects fuel/ if
809 -- any function contained within the value satisfies the following properties:
810 --
811 -- * When fuel is exhausted, it always returns 'Nothing'.
812 --
813 -- * When it returns @Just g rw@, it consumes /exactly/ one unit
814 -- of fuel, and new rewrite 'rw' also respects fuel.
815 --
816 -- Provided that functions passed to 'mkFRewrite', 'mkFRewrite3',
817 -- 'mkBRewrite', and 'mkBRewrite3' are not aware of the fuel supply,
818 -- the results respect fuel.
819 --
820 -- It is an /unchecked/ run-time error for the argument passed to 'wrapFR',
821 -- 'wrapFR2', 'wrapBR', or 'warpBR2' to return a function that does not respect fuel.