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