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