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