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