add an FAQ file
[packages/hoopl.git] / prototypes / Hoopl5.hs
1 {-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs, EmptyDataDecls, PatternGuards, TypeFamilies #-}
2
3 {- Notes about the genesis of Hoopl5
4 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5 As well as addressing your concerns I had some of my own:
6
7 * In Hoopl4, a closed/closed graph starts with a distinguished
8 closed/closed block (the entry block). But this block is
9 *un-labelled*. That means that there is no way to branch back to
10 the entry point of a procedure, which seems a bit unclean.
11
12 * In general I have to admit that it does seem a bit unintuitive to
13 have block that is
14 a) closed on entry, but
15 b) does not have a label
16
17 * If you look at MkZipCfgCmm you'll see stuff like this:
18 mkCmmIfThen e tbranch
19 = withFreshLabel "end of if" $ \endif ->
20 withFreshLabel "start of then" $ \tid ->
21 mkCbranch e tid endif <*>
22 mkLabel tid <*> tbranch <*> mkBranch endif <*>
23 mkLabel endif
24
25 We are trying to present a user model *graphs* as
26 a sequence, connected by <*>,
27 of little graphs
28 Moreover, one of the little graphs is (mkLabel BlockId), and I
29 don't see how to make a graph for that in Hoopl4.
30
31 (Norman I know that this may be what you have been trying to say
32 about "graphs under construction" for some time, but looking at
33 MkZipCfgCmm made it far more concrete for me.)
34
35
36 Specifically, in Hoopl5:
37
38 * The ARF type is no longer overloaded over the LiftNode class.
39 It has a simple and beautiful type.
40
41 * I put the BlockId back in a first node, as John wanted.
42
43 * To make it possible to branch to the label of the entry block of a
44 Body it does make sense to put that block in the Body that is
45 the main payload of the graph
46
47 * That militates in favour of a Maybe-kind-of-thing on entry to a
48 Body, just as Norman wanted. It's called Entry, dual to Exit.
49
50 * However I am Very Very Keen to maintain the similar properties of
51 nodes, blocks, graphs; and in particular the single point of entry.
52 (For a multi-entry procedure, the procedure can be represented by a
53 Body plus a bunch of BlockIds, rather than a Body.) So I
54 made the Entry contain the BlockId of the entry point.
55
56 * The Body in a Body is a finite map, as you wanted. Notice
57 that this embodies an invariant: a BlockId must map to a block whose
58 entry point is that BlockId.
59
60 * I've added a layer, using arfBody/arbBlocks. Admittedly the
61 type doesn't fit the same pattern, but it's useful structuring
62
63 * You should think of a Body as a user-visible type; perhaps
64 this is the kind of graph that might form the body of a procedure.
65 Moreover, perhaps rewriteAndAnlyseForward should take a Body
66 rather than a Body, and call arbBlocks.
67
68 * With that in mind I was happy to introduce the analogous invariant
69 for the exit block in Exit; it is very very convenient to have that
70 BlockId (cached though it may be) to hand.
71
72 * Because graphs are made out of blocks, it's easy to have a
73 constructor for the empty ggraph, and we don't need any stinkikng
74 smart constructor to keep nil in its place. But if we moved nil to
75 blocks, we'd need a smart constructor for graphs *and* one for
76 blocks. (Because unlike graphs, blocks *are* made from other
77 blocks.
78
79 -}
80
81 module Hoopl5 where
82
83 import qualified Data.IntMap as M
84 import qualified Data.IntSet as S
85
86 -----------------------------------------------------------------------------
87 -- Graphs
88 -----------------------------------------------------------------------------
89
90 data O
91 data C
92
93 -- Blocks are always non-empty
94 data Block n e x where
95 BUnit :: n e x -> Block n e x
96 BCat :: Block n e O -> Block n O x -> Block n e x
97
98 type Body n = BlockMap (Block n C C)
99 -- Invariant: BlockId bid maps to a block whose entryBlockId is bid
100
101 data Graph n e x where
102 GNil :: Graph n O O
103 GUnit :: Block n O O -> Graph n O O
104 GMany :: Entry n e -> Body n
105 -> Exit n x -> Graph n e x
106 -- If Entry is EntryC, then Body is non-empty
107
108 data Entry n e where
109 EntryC :: BlockId -> Entry n C
110 EntryO :: Block n O C -> Entry n O
111
112 data Exit n x where
113 ExitC :: Exit n C
114 ExitO :: BlockId -> Block n C O -> Exit n O
115 -- Invariant: the BlockId is the entryBlockId of the block
116
117 -----------------------------------------------------------------------------
118 -- Defined here but not used
119 -----------------------------------------------------------------------------
120
121 -- Singletons
122 -- OO GUnit
123 -- CO GMany (EntryC l) [] (ExitO l b)
124 -- OC GMany (EntryO b) [] ExitC
125 -- CC GMany (EntryC l) [b] ExitC
126
127 bFilter :: forall n. (n O O -> Bool) -> Block n C C -> Block n C C
128 bFilter keep (BUnit n) = BUnit n
129 bFilter keep (BCat h t) = bFilterH h (bFilterT t)
130 where
131 bFilterH :: Block n C O -> Block n O C -> Block n C C
132 bFilterH (BUnit n) rest = BUnit n `BCat` rest
133 bFilterH (h `BCat` m) rest = bFilterH h (bFilterM m rest)
134
135 bFilterT :: Block n O C -> Block n O C
136 bFilterT (BUnit n) = BUnit n
137 bFilterT (m `BCat` t) = bFilterM m (bFilterT t)
138
139 bFilterM :: Block n O O -> Block n O C -> Block n O C
140 bFilterM (BUnit n) rest | keep n = BUnit n `BCat` rest
141 | otherwise = rest
142 bFilterM (b1 `BCat` b2) rest = bFilterM b1 (bFilterM b2 rest)
143
144 gCat :: Graph n e a -> Graph n a x -> Graph n e x
145 gCat GNil g2 = g2
146 gCat g1 GNil = g1
147
148 gCat (GUnit b1) (GUnit b2)
149 = GUnit (b1 `BCat` b2)
150
151 gCat (GUnit b) (GMany (EntryO e) bs x)
152 = GMany (EntryO (b `BCat` e)) bs x
153
154 gCat (GMany e bs (ExitO bid x)) (GUnit b2)
155 = GMany e bs (ExitO bid (x `BCat` b2))
156
157 gCat (GMany e1 bs1 (ExitO bid x1)) (GMany (EntryO e2) bs2 x2)
158 = GMany e1 (addBlock bid (x1 `BCat` e2) bs1 `unionBlocks` bs2) x2
159
160 gCat (GMany e1 bs1 ExitC) (GMany (EntryC _) bs2 x2)
161 = GMany e1 (bs1 `unionBlocks` bs2) x2
162
163 class Edges thing where
164 entryBlockId :: thing C x -> BlockId
165 successors :: thing e C -> [BlockId]
166
167 instance Edges n => Edges (Block n) where
168 entryBlockId (BUnit n) = entryBlockId n
169 entryBlockId (b `BCat` _) = entryBlockId b
170 successors (BUnit n) = successors n
171 successors (BCat _ b) = successors b
172
173 instance Edges n => Edges (Graph n) where
174 entryBlockId (GMany (EntryC bid) _ _) = bid
175 successors (GMany h bg ExitC)
176 = blockSetElems (all_succs `minusBlockSet` all_blk_ids)
177 where
178 (bids, blks) = unzip (blocksToList bg)
179 bg_succs = mkBlockSet [bid | b <- blks, bid <- successors b]
180 all_succs :: BlockSet
181 all_succs = case h of
182 EntryC _ -> bg_succs
183 EntryO b -> bg_succs `unionBlockSet` mkBlockSet (successors b)
184 all_blk_ids = mkBlockSet bids
185
186 data OCFlag oc where
187 IsOpen :: OCFlag O
188 IsClosed :: OCFlag C
189
190 class IsOC oc where
191 ocFlag :: OCFlag oc
192
193 instance IsOC O where
194 ocFlag = IsOpen
195 instance IsOC C where
196 ocFlag = IsClosed
197
198 mkIfThenElse :: forall n x. IsOC x
199 => (BlockId -> BlockId -> n O C) -- The conditional branch instruction
200 -> (BlockId -> n C O) -- Make a head node
201 -> (BlockId -> n O C) -- Make an unconditional branch
202 -> Graph n O x -> Graph n O x -- Then and else branches
203 -> [BlockId] -- Block supply
204 -> Graph n O x -- The complete thing
205 mkIfThenElse mk_cbranch mk_lbl mk_branch then_g else_g (tl:el:jl:_)
206 = case (ocFlag :: OCFlag x) of
207 IsOpen -> gUnitOC (mk_cbranch tl el)
208 `gCat` (mk_lbl_g tl `gCat` then_g `gCat` mk_branch_g jl)
209 `gCat` (mk_lbl_g el `gCat` else_g `gCat` mk_branch_g jl)
210 `gCat` (mk_lbl_g jl)
211 IsClosed -> gUnitOC (mk_cbranch tl el)
212 `gCat` (mk_lbl_g tl `gCat` then_g)
213 `gCat` (mk_lbl_g el `gCat` else_g)
214 where
215 mk_lbl_g :: BlockId -> Graph n C O
216 mk_lbl_g lbl = gUnitCO lbl (mk_lbl lbl)
217 mk_branch_g :: BlockId -> Graph n O C
218 mk_branch_g lbl = gUnitOC (mk_branch lbl)
219
220 gUnitCO :: BlockId -> n C O -> Graph n C O
221 gUnitCO lbl n = GMany (EntryC lbl) noBlocks (ExitO lbl (BUnit n))
222
223 gUnitOC :: n O C -> Graph n O C
224 gUnitOC n = GMany (EntryO (BUnit n)) noBlocks ExitC
225
226 -----------------------------------------------------------------------------
227 -- RG: an internal data type for graphs under construction
228 -- TOTALLY internal to Hoopl
229 -----------------------------------------------------------------------------
230
231 -- "RG" stands for "rewritten graph", and embodies
232 -- both the result graph and its internal facts
233
234 data RL n f x where
235 RL :: BlockId -> f -> RG n f C x -> RL n f x
236 RLMany :: GraphWithFacts n f -> RL n f C
237
238 data RG n f e x where -- Will have facts too in due course
239 RGNil :: RG n f a a
240 RGBlock :: Block n e x -> RG n f e x
241 RGCatO :: RG n f e O -> RG n f O x -> RG n f e x
242 RGCatC :: RG n f e C -> RL n f x -> RG n f e x
243
244 type GraphWithFacts n f = (Body n, FactBase f)
245 -- A Body together with the facts for that graph
246 -- The domains of the two maps should be identical
247
248 -- 'normalise' converts a closed/closed result graph into a Body
249 -- It uses three auxiliary functions,
250 -- specialised for various argument shapes
251 normRL :: RL n f C -> GraphWithFacts n f
252 normRL (RL l f b) = normRG l f b
253 normRL (RLMany bg) = bg
254
255 normRL_O :: RL n f O -> RG n f O C -> GraphWithFacts n f
256 normRL_O (RL l f b) rg = normRG_O l f b rg
257
258 normRG :: BlockId -> f -> RG n f C C -> GraphWithFacts n f
259 normRG l f (RGBlock b) = unitBWF l f b
260 normRG l f (RGCatO rg1 rg2) = normRG_O l f rg1 rg2
261 normRG l f (RGCatC rg1 rg2) = normRG l f rg1 `unionBWF` normRL rg2
262
263 normRG_O :: BlockId -> f -> RG n f C O -> RG n f O C -> GraphWithFacts n f
264 -- normalise (rg1 `RGCatO` rg2)
265 normRG_O l f (RGBlock b) rg = normB l f b rg
266 normRG_O l f (RGCatO rg1 rg2) rg3 = normRG_O l f rg1 (rg2 `RGCatO` rg3)
267 normRG_O l f (RGCatC rg1 rg2) rg3 = normRG l f rg1 `unionBWF` normRL_O rg2 rg3
268
269 normB :: BlockId -> f -> Block n C O -> RG n f O C -> GraphWithFacts n f
270 -- normalise (Block b `RGCatO` rg2)
271 normB l f b1 (RGBlock b2) = unitBWF l f (b1 `BCat` b2)
272 normB l f b (RGCatO rg1 rg2) = normB_O l f b rg1 rg2
273 normB l f b (RGCatC rg1 rg2) = normB l f b rg1 `unionBWF` normRL rg2
274
275 normB_O :: BlockId -> f -> Block n C O -> RG n f O O -> RG n f O C
276 -> GraphWithFacts n f
277 -- normalise (Block b `RGCatO` rg2 `RGCatO` rg3)
278 normB_O l f b RGNil rg = normB l f b rg
279 normB_O l f bh (RGBlock bt) rg = normB l f (bh `BCat` bt) rg
280 normB_O l f b (RGCatC rg1 rg2) rg3 = normB l f b rg1 `unionBWF` normRL_O rg2 rg3
281 normB_O l f b (RGCatO rg1 rg2) rg3 = normB_O l f b rg1 (rg2 `RGCatO` rg3)
282
283 noBWF :: GraphWithFacts n f
284 noBWF = (noBlocks, noFacts)
285
286 unitBWF :: BlockId -> f -> Block n C C -> GraphWithFacts n f
287 unitBWF lbl f b = (unitBlock lbl b, unitFactBase lbl f)
288
289 unionBWF :: GraphWithFacts n f -> GraphWithFacts n f -> GraphWithFacts n f
290 unionBWF (bg1, fb1) (bg2, fb2) = (bg1 `unionBlocks` bg2, fb1 `unionFactBase` fb2)
291
292 -----------------------------------------------------------------------------
293 -- DataflowLattice
294 -----------------------------------------------------------------------------
295
296 data DataflowLattice a = DataflowLattice {
297 fact_name :: String, -- Documentation
298 fact_bot :: a, -- Lattice bottom element
299 fact_extend :: a -> a -> (ChangeFlag,a), -- Lattice join plus change flag
300 fact_do_logging :: Bool -- log changes
301 }
302
303 data ChangeFlag = NoChange | SomeChange
304
305 -----------------------------------------------------------------------------
306 -- The main Hoopl API
307 -----------------------------------------------------------------------------
308
309 type ForwardTransfer n f
310 = forall e x. n e x -> f -> ExitFactF x f
311
312 type ForwardRewrite n f
313 = forall e x. n e x -> f -> Maybe (AGraph n e x)
314
315 type family ExitFactF x f :: *
316 type instance ExitFactF C f = [(BlockId, f)]
317 type instance ExitFactF O f = f
318
319 data AGraph n e x = AGraph -- Stub for now
320
321
322 -----------------------------------------------------------------------------
323 -- TxFactBase: a FactBase with ChangeFlag information
324 -----------------------------------------------------------------------------
325
326 -- The TxFactBase is an accumulating parameter, threaded through all
327 -- the analysis/transformation of each block in the g_blocks of a grpah.
328 -- It carries a ChangeFlag with it, and a set of BlockIds
329 -- to monitor. Updates to other BlockIds don't affect the ChangeFlag
330 data TxFactBase n f
331 = TxFB { tfb_fbase :: FactBase f
332
333 , tfb_cha :: ChangeFlag
334 , tfb_bids :: BlockSet -- Update change flag iff these blocks change
335 -- These are BlockIds of the *original*
336 -- (not transformed) blocks
337
338 , tfb_blks :: GraphWithFacts n f -- Transformed blocks
339 }
340
341 updateFact :: DataflowLattice f -> BlockSet
342 -> (BlockId, f)
343 -> (ChangeFlag, FactBase f)
344 -> (ChangeFlag, FactBase f)
345 -- Update a TxFactBase, setting the change flag iff
346 -- a) the new fact adds information...
347 -- b) for a block in the BlockSet in the TxFactBase
348 updateFact lat lbls (lbl, new_fact) (cha, fbase)
349 | NoChange <- cha2 = (cha, fbase)
350 | lbl `elemBlockSet` lbls = (SomeChange, new_fbase)
351 | otherwise = (cha, new_fbase)
352 where
353 old_fact = lookupFact lat fbase lbl
354 (cha2, res_fact) = fact_extend lat old_fact new_fact
355 new_fbase = extendFactBase fbase lbl res_fact
356
357 fixpoint :: forall n f.
358 DataflowLattice f
359 -> (BlockId -> Block n C C -> FactBase f
360 -> FuelMonad ([(BlockId,f)], RL n f C))
361 -> [(BlockId, Block n C C)]
362 -> FactBase f
363 -> FuelMonad (FactBase f, GraphWithFacts n f)
364 fixpoint lat do_block blocks init_fbase
365 = do { fuel <- getFuel
366 ; tx_fb <- loop fuel init_fbase
367 ; return (tfb_fbase tx_fb `deleteFromFactBase` blocks, tfb_blks tx_fb) }
368 -- The successors of the Graph are the the BlockIds for which
369 -- we have facts, that are *not* in the blocks of the graph
370 where
371 tx_blocks :: [(BlockId, Block n C C)]
372 -> TxFactBase n f -> FuelMonad (TxFactBase n f)
373 tx_blocks [] tx_fb = return tx_fb
374 tx_blocks ((lbl,blk):bs) tx_fb = do { tx_fb1 <- tx_block lbl blk tx_fb
375 ; tx_blocks bs tx_fb1 }
376
377 tx_block :: BlockId -> Block n C C
378 -> TxFactBase n f -> FuelMonad (TxFactBase n f)
379 tx_block lbl blk (TxFB { tfb_fbase = fbase, tfb_bids = lbls
380 , tfb_blks = blks, tfb_cha = cha })
381 = do { (out_facts, rg) <- do_block lbl blk fbase
382 ; let (cha',fbase') = foldr (updateFact lat lbls) (cha,fbase) out_facts
383 f = lookupFact lat fbase lbl
384 -- tfb_blks will be discarded unless we have
385 -- reached a fixed point, so it doesn't matter
386 -- whether we get f from fbase or fbase'
387 ; return (TxFB { tfb_bids = extendBlockSet lbls lbl
388 , tfb_blks = normRL rg `unionBWF` blks
389 , tfb_fbase = fbase', tfb_cha = cha' }) }
390
391 loop :: Fuel -> FactBase f -> FuelMonad (TxFactBase n f)
392 loop fuel fbase
393 = do { let init_tx_fb = TxFB { tfb_fbase = fbase
394 , tfb_cha = NoChange
395 , tfb_blks = noBWF
396 , tfb_bids = emptyBlockSet }
397 ; tx_fb <- tx_blocks blocks init_tx_fb
398 ; case tfb_cha tx_fb of
399 NoChange -> return tx_fb
400 SomeChange -> do { setFuel fuel; loop fuel (tfb_fbase tx_fb) } }
401
402 -----------------------------------------------------------------------------
403 -- Transfer functions
404 -----------------------------------------------------------------------------
405
406 -- Keys to the castle: a generic transfer function for each shape
407 -- Here's the idea: we start with single-n transfer functions,
408 -- move to basic-block transfer functions (we have exactly four shapes),
409 -- then finally to graph transfer functions (which requires iteration).
410
411 type ARF thing n f = forall e x. f -> thing e x -> FuelMonad (ExitFactF x f, RG n f e x)
412
413 type ARF_Node n f = ARF n n f
414 type ARF_Block n f = ARF (Block n) n f
415 type ARF_Graph n f = ARF (Graph n) n f
416 -----------------------------------------------------------------------------
417
418 arfNodeNoRW :: forall n f. ForwardTransfer n f -> ARF_Node n f
419 -- Lifts ForwardTransfer to ARF_Node; simple transfer only
420 arfNodeNoRW transfer_fn f node
421 = return (transfer_fn node f, RGBlock (BUnit node))
422
423 arfNode :: forall n f.
424 DataflowLattice f
425 -> ForwardTransfer n f
426 -> ForwardRewrite n f
427 -> ARF_Node n f
428 -> ARF_Node n f
429 -- Lifts (ForwardTransfer,ForwardRewrite) to ARF_Node;
430 -- this time we do rewriting as well.
431 -- The ARF_Graph parameters specifies what to do with the rewritten graph
432 arfNode lattice transfer_fn rewrite_fn arf_node f node
433 = do { mb_g <- withFuel (rewrite_fn node f)
434 ; case mb_g of
435 Nothing -> arfNodeNoRW transfer_fn f node
436 Just ag -> do { g <- graphOfAGraph ag
437 ; arfGraph lattice arf_node f g } }
438
439 arfBlock :: forall n f. ARF_Node n f -> ARF_Block n f
440 -- Lift from nodes to blocks
441 arfBlock arf_node f (BUnit node) = arf_node f node
442 arfBlock arf_node f (BCat hd mids) = do { (f1,g1) <- arfBlock arf_node f hd
443 ; (f2,g2) <- arfBlock arf_node f1 mids
444 ; return (f2, g1 `RGCatO` g2) }
445
446 arfBody :: forall n f. DataflowLattice f
447 -> ARF_Node n f -> FactBase f -> Body n
448 -> FuelMonad (FactBase f, GraphWithFacts n f)
449 -- Outgoing factbase is restricted to BlockIds *not* in
450 -- in the Body; the facts for BlockIds
451 -- *in* the Body are in the GraphWithFacts
452 arfBody lattice arf_node init_fbase blocks
453 = fixpoint lattice do_block
454 (forwardBlockList (factBaseBlockIds init_fbase) blocks)
455 init_fbase
456 where
457 do_block :: BlockId -> Block n C C -> FactBase f
458 -> FuelMonad ([(BlockId,f)], RL n f C)
459 do_block l blk fbase = do { let f = lookupFact lattice fbase l
460 ; (fs, rg) <- arfBlock arf_node f blk
461 ; return (fs, RL l f rg) }
462
463 arfGraph :: forall n f. DataflowLattice f -> ARF_Node n f -> ARF_Graph n f
464 -- Lift from blocks to graphs
465 arfGraph _ _ f GNil = return (f, RGNil)
466 arfGraph _ arf_node f (GUnit blk) = arfBlock arf_node f blk
467 arfGraph lattice arf_node f (GMany entry blks exit)
468 = do { (f1, entry') <- arf_entry f entry
469 ; (f2, blks') <- arfBody lattice arf_node (mkFactBase f1) blks
470 ; (f3, exit') <- arf_exit f2 exit
471 ; return (f3, entry' `RGCatC` RLMany blks' `RGCatC` exit') }
472 where
473 arf_entry :: f -> Entry n e
474 -> FuelMonad ([(BlockId,f)], RG n f e C)
475 arf_entry fh (EntryC lh) = return ([(lh,fh)], RGNil)
476 arf_entry fh (EntryO b) = arfBlock arf_node fh b
477
478 arf_exit :: FactBase f -> Exit n x
479 -> FuelMonad (ExitFactF x f, RL n f x)
480 arf_exit fb ExitC = return (factBaseList fb, RLMany noBWF)
481 arf_exit fb (ExitO lt blk) = do { let ft = lookupFact lattice fb lt
482 ; (f1, rg) <- arfBlock arf_node ft blk
483 ; return (f1, RL lt ft rg) }
484
485 forwardBlockList :: [BlockId] -> Body n -> [(BlockId,Block n C C)]
486 -- This produces a list of blocks in order suitable for forward analysis.
487 -- ToDo: Do a topological sort to improve convergence rate of fixpoint
488 -- This will require a (HavingSuccessors l) class constraint
489 forwardBlockList _ blks = blocksToList blks
490
491 ----------------------------------------------------------------
492 -- The pi├Ęce de resistance: cunning transfer functions
493 ----------------------------------------------------------------
494
495 pureAnalysis :: DataflowLattice f -> ForwardTransfer n f -> ARF_Graph n f
496 pureAnalysis lattice f = arfGraph lattice (arfNodeNoRW f)
497
498 analyseAndRewriteFwd
499 :: forall n f.
500 DataflowLattice f
501 -> ForwardTransfer n f
502 -> ForwardRewrite n f
503 -> RewritingDepth
504 -> FactBase f
505 -> Body n
506 -> FuelMonad (Body n, FactBase f)
507
508 data RewritingDepth = RewriteShallow | RewriteDeep
509 -- When a transformation proposes to rewrite a node,
510 -- you can either ask the system to
511 -- * "shallow": accept the new graph, analyse it without further rewriting
512 -- * "deep": recursively analyse-and-rewrite the new graph
513
514 analyseAndRewriteFwd lattice transfers rewrites depth facts graph
515 = do { (_, gwf) <- arfBody lattice arf_node facts graph
516 ; return gwf }
517 where
518 arf_node, rec_node :: ARF_Node n f
519 arf_node = arfNode lattice transfers rewrites rec_node
520
521 rec_node = case depth of
522 RewriteShallow -> arfNodeNoRW transfers
523 RewriteDeep -> arf_node
524
525 -----------------------------------------------------------------------------
526 -- Backward rewriting
527 -----------------------------------------------------------------------------
528
529 type BackwardTransfer n f
530 = forall e x. n e x -> ExitFactB x f -> f
531 type BackwardRewrite n f
532 = forall e x. n e x -> ExitFactB x f -> Maybe (AGraph n e x)
533
534 type ARB thing n f = forall e x. ExitFactB x f -> thing e x
535 -> FuelMonad (f, RG n f e x)
536
537 type family ExitFactB x f :: *
538 type instance ExitFactB C f = FactBase f
539 type instance ExitFactB O f = f
540
541 type ARB_Node n f = ARB n n f
542 type ARB_Block n f = ARB (Block n) n f
543 type ARB_Graph n f = ARB (Graph n) n f
544
545 arbNodeNoRW :: forall n f . BackwardTransfer n f -> ARB_Node n f
546 -- Lifts BackwardTransfer to ARB_Node; simple transfer only
547 arbNodeNoRW transfer_fn f node
548 = return (transfer_fn node f, RGBlock (BUnit node))
549
550 arbNode :: forall n f.
551 DataflowLattice f
552 -> BackwardTransfer n f
553 -> BackwardRewrite n f
554 -> ARB_Node n f
555 -> ARB_Node n f
556 -- Lifts (BackwardTransfer,BackwardRewrite) to ARB_Node;
557 -- this time we do rewriting as well.
558 -- The ARB_Graph parameters specifies what to do with the rewritten graph
559 arbNode lattice transfer_fn rewrite_fn arf_node f node
560 = do { mb_g <- withFuel (rewrite_fn node f)
561 ; case mb_g of
562 Nothing -> arbNodeNoRW transfer_fn f node
563 Just ag -> do { g <- graphOfAGraph ag
564 ; arbGraph lattice arf_node f g } }
565
566 arbBlock :: forall n f. ARB_Node n f -> ARB_Block n f
567 -- Lift from nodes to blocks
568 arbBlock arb_node f (BUnit node) = arb_node f node
569 arbBlock arb_node f (BCat b1 b2) = do { (f2,g2) <- arbBlock arb_node f b2
570 ; (f1,g1) <- arbBlock arb_node f2 b1
571 ; return (f1, g1 `RGCatO` g2) }
572
573
574 arbBlocks :: forall n f. DataflowLattice f
575 -> ARB_Node n f -> FactBase f
576 -> Body n -> FuelMonad (FactBase f, GraphWithFacts n f)
577 arbBlocks lattice arb_node init_fbase blocks
578 = fixpoint lattice do_block
579 (backwardBlockList (factBaseBlockIds init_fbase) blocks)
580 init_fbase
581 where
582 do_block :: BlockId -> Block n C C -> FactBase f
583 -> FuelMonad ([(BlockId,f)], RL n f C)
584 do_block l b fbase = do { (fb, rg) <- arbBlock arb_node fbase b
585 ; let f = lookupFact lattice fbase l
586 ; return ([(l,fb)], RL l f rg) }
587
588 arbGraph :: forall n f. DataflowLattice f -> ARB_Node n f -> ARB_Graph n f
589 arbGraph _ _ f GNil = return (f, RGNil)
590 arbGraph _ arb_node f (GUnit blk) = arbBlock arb_node f blk
591 arbGraph lattice arb_node f (GMany entry blks exit)
592 = do { (f1, exit') <- arb_exit f exit
593 ; (f2, blks') <- arbBlocks lattice arb_node f1 blks
594 ; (f3, entry') <- arb_entry f2 entry
595 ; return (f3, entry' `RGCatC` RLMany blks' `RGCatC` exit') }
596 where
597 arb_entry :: FactBase f -> Entry n e
598 -> FuelMonad (f, RG n f e C)
599 arb_entry fbase (EntryC l) = return (lookupFact lattice fbase l, RGNil)
600 arb_entry fbase (EntryO b) = arbBlock arb_node fbase b
601
602 arb_exit :: ExitFactB x f -> Exit n x
603 -> FuelMonad (FactBase f, RL n f x)
604 arb_exit ft ExitC = return (ft, RLMany noBWF)
605 arb_exit ft (ExitO lt blk) = do { (f1, rg) <- arbBlock arb_node ft blk
606 ; return (mkFactBase [(lt,f1)], RL lt f1 rg) }
607
608 backwardBlockList :: [BlockId] -> Body n -> [(BlockId,Block n C C)]
609 -- This produces a list of blocks in order suitable for backward analysis.
610 backwardBlockList _ blks = blocksToList blks
611
612 analyseAndRewriteBwd
613 :: forall n f.
614 DataflowLattice f
615 -> BackwardTransfer n f
616 -> BackwardRewrite n f
617 -> RewritingDepth
618 -> ARB_Graph n f
619
620 analyseAndRewriteBwd lattice transfers rewrites depth
621 = arbGraph lattice arb_node
622 where
623 arb_node, rec_node :: ARB_Node n f
624 arb_node = arbNode lattice transfers rewrites rec_node
625
626 rec_node = case depth of
627 RewriteShallow -> arbNodeNoRW transfers
628 RewriteDeep -> arb_node
629
630 -----------------------------------------------------------------------------
631 -- The fuel monad
632 -----------------------------------------------------------------------------
633
634 type Uniques = Int
635 type Fuel = Int
636
637 newtype FuelMonad a = FM { unFM :: Fuel -> Uniques -> (a, Fuel, Uniques) }
638
639 instance Monad FuelMonad where
640 return x = FM (\f u -> (x,f,u))
641 m >>= k = FM (\f u -> case unFM m f u of (r,f',u') -> unFM (k r) f' u')
642
643 withFuel :: Maybe a -> FuelMonad (Maybe a)
644 withFuel Nothing = return Nothing
645 withFuel (Just r) = FM (\f u -> if f==0 then (Nothing, f, u)
646 else (Just r, f-1, u))
647
648 getFuel :: FuelMonad Fuel
649 getFuel = FM (\f u -> (f,f,u))
650
651 setFuel :: Fuel -> FuelMonad ()
652 setFuel f = FM (\_ u -> ((), f, u))
653
654 graphOfAGraph :: AGraph node e x -> FuelMonad (Graph node e x)
655 graphOfAGraph = error "urk" -- Stub
656
657 -----------------------------------------------------------------------------
658 -- BlockId, FactBase, BlockSet
659 -----------------------------------------------------------------------------
660
661 type BlockId = Int
662
663 mkBlockId :: Int -> BlockId
664 mkBlockId uniq = uniq
665
666 ----------------------
667 type BlockMap a = M.IntMap a
668
669 noBlocks :: Body n
670 noBlocks = M.empty
671
672 unitBlock :: BlockId -> Block n C C -> Body n
673 unitBlock = M.singleton
674
675 addBlock :: BlockId -> Block n C C -> Body n -> Body n
676 addBlock = M.insert
677
678 unionBlocks :: Body n -> Body n -> Body n
679 unionBlocks = M.union
680
681 blocksToList :: Body n -> [(BlockId,Block n C C)]
682 blocksToList = M.toList
683
684 ----------------------
685 type FactBase a = M.IntMap a
686
687 noFacts :: FactBase f
688 noFacts = M.empty
689
690 mkFactBase :: [(BlockId, f)] -> FactBase f
691 mkFactBase prs = M.fromList prs
692
693 unitFactBase :: BlockId -> f -> FactBase f
694 unitFactBase = M.singleton
695
696 lookupFact :: DataflowLattice f -> FactBase f -> BlockId -> f
697 lookupFact lattice env blk_id
698 = case M.lookup blk_id env of
699 Just f -> f
700 Nothing -> fact_bot lattice
701
702 extendFactBase :: FactBase f -> BlockId -> f -> FactBase f
703 extendFactBase env blk_id f = M.insert blk_id f env
704
705 unionFactBase :: FactBase f -> FactBase f -> FactBase f
706 unionFactBase = M.union
707
708 factBaseBlockIds :: FactBase f -> [BlockId]
709 factBaseBlockIds = M.keys
710
711 factBaseList :: FactBase f -> [(BlockId, f)]
712 factBaseList = M.toList
713
714 deleteFromFactBase :: FactBase f -> [(BlockId,a)] -> FactBase f
715 deleteFromFactBase fb blks = foldr (M.delete . fst) fb blks
716
717 ----------------------
718 type BlockSet = S.IntSet
719
720 emptyBlockSet :: BlockSet
721 emptyBlockSet = S.empty
722
723 extendBlockSet :: BlockSet -> BlockId -> BlockSet
724 extendBlockSet bids bid = S.insert bid bids
725
726 elemBlockSet :: BlockId -> BlockSet -> Bool
727 elemBlockSet bid bids = S.member bid bids
728
729 blockSetElems :: BlockSet -> [BlockId]
730 blockSetElems = S.toList
731
732 minusBlockSet :: BlockSet -> BlockSet -> BlockSet
733 minusBlockSet = S.difference
734
735 unionBlockSet :: BlockSet -> BlockSet -> BlockSet
736 unionBlockSet = S.union
737
738 mkBlockSet :: [BlockId] -> BlockSet
739 mkBlockSet = S.fromList