5826d0f0924417639d95ab07332bc7c6ea03a213
[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 = fixpoint_anal 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 = fixpoint_anal 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 = fixpoint_anal 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 (analysis only)
503 -----------------------------------------------------------------------------
504
505 data Direction = Fwd | Bwd
506
507 fixpoint_anal :: forall n f. NonLocal n
508 => Direction
509 -> DataflowLattice f
510 -> (Block n C C -> Fact C f -> Fact C f)
511 -> [Label]
512 -> LabelMap (Block n C C)
513 -> Fact C f -> FactBase f
514
515 fixpoint_anal direction DataflowLattice{ fact_bot = bot, fact_join = join }
516 do_block entries blockmap init_fbase
517 = loop start init_fbase
518 where
519 blocks = forwardBlockList entries blockmap
520 n = length blocks
521
522 ordered_blocks = case direction of
523 Fwd -> blocks
524 Bwd -> reverse blocks
525
526 block_arr = {-# SCC "block_arr" #-} listArray (0,n-1) ordered_blocks
527
528 start = {-# SCC "start" #-} [0 .. n-1]
529
530 -- mapping from L -> blocks. If the fact for L changes, re-analyse blocks.
531 dep_blocks :: LabelMap [Int]
532 dep_blocks = {-# SCC "dep_blocks" #-} mapFromListWith (++)
533 [ (l, [ix])
534 | (b,ix) <- zip ordered_blocks [0..]
535 , l <- case direction of
536 Fwd -> [entryLabel b]
537 Bwd -> successors b
538 ]
539
540 loop
541 :: [Int] -- blocks still to analyse
542 -> FactBase f -- current factbase (increases monotonically)
543 -> FactBase f
544
545 loop [] fbase = fbase
546 loop (ix:todo) fbase =
547 let
548 blk = block_arr ! ix
549
550 out_facts = {-# SCC "do_block" #-} do_block blk fbase
551
552 !(todo', fbase') = {-# SCC "mapFoldWithKey" #-}
553 mapFoldWithKey (updateFact bot join dep_blocks)
554 (todo,fbase) out_facts
555 in
556 -- trace ("analysing: " ++ show (entryLabel blk)) $
557 -- trace ("fbase': " ++ show (mapKeys fbase')) $ return ()
558 -- trace ("changed: " ++ show changed) $ return ()
559 -- trace ("to analyse: " ++ show to_analyse) $ return ()
560
561 loop todo' fbase'
562
563
564
565 -----------------------------------------------------------------------------
566 -- fixpoint: finding fixed points
567 -----------------------------------------------------------------------------
568
569 -- Shared by fixpoint and fixpoint_anal:
570 --
571 updateFact :: f -> JoinFun f -> LabelMap [Int]
572 -> Label -> f -- out fact
573 -> ([Int], FactBase f)
574 -> ([Int], FactBase f)
575
576 updateFact bot fact_join dep_blocks lbl new_fact (todo, fbase)
577 = case lookupFact lbl fbase of
578 Nothing -> let !z = mapInsert lbl new_fact fbase in (changed, z)
579 -- Note [no old fact]
580 Just old_fact ->
581 case fact_join lbl (OldFact old_fact) (NewFact new_fact) of
582 (NoChange, _) -> (todo, fbase)
583 (_, f) -> let !z = mapInsert lbl f fbase in (changed, z)
584 where
585 changed = foldr insertIntHeap todo $
586 mapFindWithDefault [] lbl dep_blocks
587
588 {-
589 Note [no old fact]
590
591 We know that the new_fact is >= _|_, so we don't need to join. However,
592 if the new fact is also _|_, and we have already analysed its block,
593 we don't need to record a change. So there's a tradeoff here. It turns
594 out that always recording a change is faster.
595 -}
596
597
598 fixpoint :: forall n f. NonLocal n
599 => Direction
600 -> DataflowLattice f
601 -> (Block n C C -> Fact C f -> FuelUniqSM (DG f n C C, Fact C f))
602 -> [Label]
603 -> LabelMap (Block n C C)
604 -> (Fact C f -> FuelUniqSM (DG f n C C, Fact C f))
605
606 fixpoint direction DataflowLattice{ fact_bot = bot, fact_join = join }
607 do_block entries blockmap init_fbase
608 = do
609 -- trace ("fixpoint: " ++ show (case direction of Fwd -> True; Bwd -> False) ++ " " ++ show (mapKeys blockmap) ++ show entries ++ " " ++ show (mapKeys init_fbase)) $ return()
610 (fbase, newblocks) <- loop start init_fbase mapEmpty
611 -- trace ("fixpoint DONE: " ++ show (mapKeys fbase) ++ show (mapKeys newblocks)) $ return()
612 return (GMany NothingO newblocks NothingO,
613 mapDeleteList (mapKeys blockmap) fbase)
614 -- The successors of the Graph are the the Labels
615 -- for which we have facts and which are *not* in
616 -- the blocks of the graph
617 where
618 blocks = forwardBlockList entries blockmap
619 ordered_blocks = case direction of
620 Fwd -> blocks
621 Bwd -> reverse blocks
622 block_arr = listArray (0,n-1) ordered_blocks
623
624 start = [0 .. n-1]
625 n = length blocks
626
627 -- mapping from L -> blocks. If the fact for L changes, re-analyse blocks.
628 dep_blocks :: LabelMap [Int]
629 dep_blocks = mapFromListWith (++)
630 [ (l, [ix])
631 | (b,ix) <- zip ordered_blocks [0..]
632 , l <- case direction of
633 Fwd -> [entryLabel b]
634 Bwd -> successors b
635 ]
636
637 loop
638 :: IntHeap
639 -> FactBase f -- current factbase (increases monotonically)
640 -> LabelMap (DBlock f n C C) -- transformed graph
641 -> FuelUniqSM (FactBase f, LabelMap (DBlock f n C C))
642
643 loop [] fbase newblocks = return (fbase, newblocks)
644 loop (ix:todo) fbase !newblocks = do
645 let blk = block_arr ! ix
646
647 -- trace ("analysing: " ++ show (entryLabel blk)) $ return ()
648 (rg, out_facts) <- do_block blk fbase
649 let !(todo', fbase') =
650 mapFoldWithKey (updateFact bot join dep_blocks)
651 (todo,fbase) out_facts
652
653 -- trace ("fbase': " ++ show (mapKeys fbase')) $ return ()
654 -- trace ("changed: " ++ show changed) $ return ()
655 -- trace ("to analyse: " ++ show to_analyse) $ return ()
656
657 let newblocks' = case rg of
658 GMany _ blks _ -> mapUnion blks newblocks
659
660 loop todo' fbase' newblocks'
661
662
663 {- Note [TxFactBase invariants]
664 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
665 The TxFactBase is used only during a fixpoint iteration (or "sweep"),
666 and accumulates facts (and the transformed code) during the fixpoint
667 iteration.
668
669 * tfb_fbase increases monotonically, across all sweeps
670
671 * At the beginning of each sweep
672 tfb_cha = NoChange
673 tfb_lbls = {}
674
675 * During each sweep we process each block in turn. Processing a block
676 is done thus:
677 1. Read from tfb_fbase the facts for its entry label (forward)
678 or successors labels (backward)
679 2. Transform those facts into new facts for its successors (forward)
680 or entry label (backward)
681 3. Augment tfb_fbase with that info
682 We call the labels read in step (1) the "in-labels" of the sweep
683
684 * The field tfb_lbls is the set of in-labels of all blocks that have
685 been processed so far this sweep, including the block that is
686 currently being processed. tfb_lbls is initialised to {}. It is a
687 subset of the Labels of the *original* (not transformed) blocks.
688
689 * The tfb_cha field is set to SomeChange iff we decide we need to
690 perform another iteration of the fixpoint loop. It is initialsed to NoChange.
691
692 Specifically, we set tfb_cha to SomeChange in step (3) iff
693 (a) The fact in tfb_fbase for a block L changes
694 (b) L is in tfb_lbls
695 Reason: until a label enters the in-labels its accumuated fact in tfb_fbase
696 has not been read, hence cannot affect the outcome
697
698 Note [Unreachable blocks]
699 ~~~~~~~~~~~~~~~~~~~~~~~~~
700 A block that is not in the domain of tfb_fbase is "currently unreachable".
701 A currently-unreachable block is not even analyzed. Reason: consider
702 constant prop and this graph, with entry point L1:
703 L1: x:=3; goto L4
704 L2: x:=4; goto L4
705 L4: if x>3 goto L2 else goto L5
706 Here L2 is actually unreachable, but if we process it with bottom input fact,
707 we'll propagate (x=4) to L4, and nuke the otherwise-good rewriting of L4.
708
709 * If a currently-unreachable block is not analyzed, then its rewritten
710 graph will not be accumulated in tfb_rg. And that is good:
711 unreachable blocks simply do not appear in the output.
712
713 * Note that clients must be careful to provide a fact (even if bottom)
714 for each entry point. Otherwise useful blocks may be garbage collected.
715
716 * Note that updateFact must set the change-flag if a label goes from
717 not-in-fbase to in-fbase, even if its fact is bottom. In effect the
718 real fact lattice is
719 UNR
720 bottom
721 the points above bottom
722
723 * Even if the fact is going from UNR to bottom, we still call the
724 client's fact_join function because it might give the client
725 some useful debugging information.
726
727 * All of this only applies for *forward* ixpoints. For the backward
728 case we must treat every block as reachable; it might finish with a
729 'return', and therefore have no successors, for example.
730 -}
731
732 -----------------------------------------------------------------------------
733 -- DG: an internal data type for 'decorated graphs'
734 -- TOTALLY internal to Hoopl; each block is decorated with a fact
735 -----------------------------------------------------------------------------
736
737 type Graph = Graph' Block
738 type DG f = Graph' (DBlock f)
739 data DBlock f n e x = DBlock f (Block n e x) -- ^ block decorated with fact
740
741 instance NonLocal n => NonLocal (DBlock f n) where
742 entryLabel (DBlock _ b) = entryLabel b
743 successors (DBlock _ b) = successors b
744
745 --- constructors
746
747 dgnil :: DG f n O O
748 dgnilC :: DG f n C C
749 dgSplice :: NonLocal n => DG f n e a -> DG f n a x -> DG f n e x
750
751 ---- observers
752
753 normalizeGraph :: forall n f e x .
754 NonLocal n => DG f n e x
755 -> (Graph n e x, FactBase f)
756 -- A Graph together with the facts for that graph
757 -- The domains of the two maps should be identical
758
759 normalizeGraph g = (graphMapBlocks dropFact g, facts g)
760 where dropFact :: DBlock t t1 t2 t3 -> Block t1 t2 t3
761 dropFact (DBlock _ b) = b
762 facts :: DG f n e x -> FactBase f
763 facts GNil = noFacts
764 facts (GUnit _) = noFacts
765 facts (GMany _ body exit) = bodyFacts body `mapUnion` exitFacts exit
766 exitFacts :: MaybeO x (DBlock f n C O) -> FactBase f
767 exitFacts NothingO = noFacts
768 exitFacts (JustO (DBlock f b)) = mapSingleton (entryLabel b) f
769 bodyFacts :: LabelMap (DBlock f n C C) -> FactBase f
770 bodyFacts body = mapFoldWithKey f noFacts body
771 where f :: forall t a x. (NonLocal t) => Label -> DBlock a t C x -> LabelMap a -> LabelMap a
772 f lbl (DBlock f _) fb = mapInsert lbl f fb
773
774 --- implementation of the constructors (boring)
775
776 dgnil = GNil
777 dgnilC = GMany NothingO emptyBody NothingO
778
779 dgSplice = U.splice fzCat
780 where fzCat :: DBlock f n e O -> DBlock t n O x -> DBlock f n e x
781 fzCat (DBlock f b1) (DBlock _ b2) = DBlock f $! b1 `U.cat` b2
782 -- NB. strictness, this function is hammered.
783
784 ----------------------------------------------------------------
785 -- Utilities
786 ----------------------------------------------------------------
787
788 -- Lifting based on shape:
789 -- - from nodes to blocks
790 -- - from facts to fact-like things
791 -- Lowering back:
792 -- - from fact-like things to facts
793 -- Note that the latter two functions depend only on the entry shape.
794 class ShapeLifter e x where
795 singletonDG :: f -> n e x -> DG f n e x
796 fwdEntryFact :: NonLocal n => n e x -> f -> Fact e f
797 fwdEntryLabel :: NonLocal n => n e x -> MaybeC e [Label]
798 ftransfer :: FwdTransfer n f -> n e x -> f -> Fact x f
799 frewrite :: FwdRewrite m n f -> n e x
800 -> f -> m (Maybe (Graph n e x, FwdRewrite m n f))
801 -- @ end node.tex
802 bwdEntryFact :: NonLocal n => DataflowLattice f -> n e x -> Fact e f -> f
803 btransfer :: BwdTransfer n f -> n e x -> Fact x f -> f
804 brewrite :: BwdRewrite m n f -> n e x
805 -> Fact x f -> m (Maybe (Graph n e x, BwdRewrite m n f))
806
807 instance ShapeLifter C O where
808 singletonDG f n = gUnitCO (DBlock f (BlockCO n BNil))
809 fwdEntryFact n f = mapSingleton (entryLabel n) f
810 bwdEntryFact lat n fb = getFact lat (entryLabel n) fb
811 ftransfer (FwdTransfer3 (ft, _, _)) n f = ft n f
812 btransfer (BwdTransfer3 (bt, _, _)) n f = bt n f
813 frewrite (FwdRewrite3 (fr, _, _)) n f = fr n f
814 brewrite (BwdRewrite3 (br, _, _)) n f = br n f
815 fwdEntryLabel n = JustC [entryLabel n]
816
817 instance ShapeLifter O O where
818 singletonDG f = gUnitOO . DBlock f . BMiddle
819 fwdEntryFact _ f = f
820 bwdEntryFact _ _ f = f
821 ftransfer (FwdTransfer3 (_, ft, _)) n f = ft n f
822 btransfer (BwdTransfer3 (_, bt, _)) n f = bt n f
823 frewrite (FwdRewrite3 (_, fr, _)) n f = fr n f
824 brewrite (BwdRewrite3 (_, br, _)) n f = br n f
825 fwdEntryLabel _ = NothingC
826
827 instance ShapeLifter O C where
828 singletonDG f n = gUnitOC (DBlock f (BlockOC BNil n))
829 fwdEntryFact _ f = f
830 bwdEntryFact _ _ f = f
831 ftransfer (FwdTransfer3 (_, _, ft)) n f = ft n f
832 btransfer (BwdTransfer3 (_, _, bt)) n f = bt n f
833 frewrite (FwdRewrite3 (_, _, fr)) n f = fr n f
834 brewrite (BwdRewrite3 (_, _, br)) n f = br n f
835 fwdEntryLabel _ = NothingC
836
837 {-
838 class ShapeLifter e x where
839 singletonDG :: f -> n e x -> DG f n e x
840
841 instance ShapeLifter C O where
842 singletonDG f n = gUnitCO (DBlock f (BlockCO n BNil))
843
844 instance ShapeLifter O O where
845 singletonDG f = gUnitOO . DBlock f . BMiddle
846
847 instance ShapeLifter O C where
848 singletonDG f n = gUnitOC (DBlock f (BlockOC BNil n))
849 -}
850
851 -- Fact lookup: the fact `orelse` bottom
852 getFact :: DataflowLattice f -> Label -> FactBase f -> f
853 getFact lat l fb = case lookupFact l fb of Just f -> f
854 Nothing -> fact_bot lat
855
856
857
858 {- Note [Respects fuel]
859 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
860 -}
861 -- $fuel
862 -- A value of type 'FwdRewrite' or 'BwdRewrite' /respects fuel/ if
863 -- any function contained within the value satisfies the following properties:
864 --
865 -- * When fuel is exhausted, it always returns 'Nothing'.
866 --
867 -- * When it returns @Just g rw@, it consumes /exactly/ one unit
868 -- of fuel, and new rewrite 'rw' also respects fuel.
869 --
870 -- Provided that functions passed to 'mkFRewrite', 'mkFRewrite3',
871 -- 'mkBRewrite', and 'mkBRewrite3' are not aware of the fuel supply,
872 -- the results respect fuel.
873 --
874 -- It is an /unchecked/ run-time error for the argument passed to 'wrapFR',
875 -- 'wrapFR2', 'wrapBR', or 'warpBR2' to return a function that does not respect fuel.
876
877 -- -----------------------------------------------------------------------------
878 -- a Heap of Int
879
880 -- We should really use a proper Heap here, but my attempts to make
881 -- one have not succeeded in beating the simple ordered list. Another
882 -- alternative is IntSet (using deleteFindMin), but that was also
883 -- slower than the ordered list in my experiments --SDM 25/1/2012
884
885 type IntHeap = [Int] -- ordered
886
887 insertIntHeap :: Int -> [Int] -> [Int]
888 insertIntHeap x [] = [x]
889 insertIntHeap x (y:ys)
890 | x < y = x : y : ys
891 | x == y = x : ys
892 | otherwise = y : insertIntHeap x ys