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