diff --git a/CHANGES b/CHANGES --- a/CHANGES +++ b/CHANGES @@ -1,3 +1,22 @@ +3.7.12.1 + + - Added a bunch of zipper experiments. + - Existing clients should not be affected. + + +3.7.12.0 + + - More expressive debugging support + - retract arfGraph and normalization; export analyzeAndRewriterFwd' + +3.7.11.1 + + - Expose arfGraph and normalization functions + +3.7.11.0 + + - Debugging support + 3.7.8.0 - Rationalized AGraph splicing functions. diff --git a/Compiler/Hoopl.hs b/Compiler/Hoopl.hs --- a/Compiler/Hoopl.hs +++ b/Compiler/Hoopl.hs @@ -1,14 +1,20 @@ module Compiler.Hoopl - ( module Compiler.Hoopl.Dataflow + ( module Compiler.Hoopl.Combinators + , module Compiler.Hoopl.Dataflow + , module Compiler.Hoopl.Debug , module Compiler.Hoopl.Fuel , module Compiler.Hoopl.Graph , module Compiler.Hoopl.Label , module Compiler.Hoopl.MkGraph + , module Compiler.Hoopl.Show ) where +import Compiler.Hoopl.Combinators import Compiler.Hoopl.Dataflow +import Compiler.Hoopl.Debug import Compiler.Hoopl.Fuel hiding (withFuel, getFuel, setFuel) import Compiler.Hoopl.Graph hiding (BodyEmpty, BodyUnit, BodyCat) import Compiler.Hoopl.Label hiding (allLabels) import Compiler.Hoopl.MkGraph +import Compiler.Hoopl.Show diff --git a/Compiler/Hoopl/Combinators.hs b/Compiler/Hoopl/Combinators.hs new file mode 100644 --- /dev/null +++ b/Compiler/Hoopl/Combinators.hs @@ -0,0 +1,79 @@ +{-# LANGUAGE RankNTypes #-} + +module Compiler.Hoopl.Combinators + ( SimpleFwdRewrite, noFwdRewrite, thenFwdRw, shallowFwdRw, deepFwdRw, iterFwdRw + , SimpleBwdRewrite, noBwdRewrite, thenBwdRw, shallowBwdRw, deepBwdRw, iterBwdRw + ) + +where + +import Compiler.Hoopl.Dataflow +import Compiler.Hoopl.MkGraph + +type SimpleFwdRewrite n f + = forall e x. n e x -> Fact e f + -> Maybe (AGraph n e x) + +noFwdRewrite :: FwdRewrite n f +noFwdRewrite _ _ = Nothing + +shallowFwdRw :: SimpleFwdRewrite n f -> FwdRewrite n f +shallowFwdRw rw n f = case (rw n f) of + Nothing -> Nothing + Just ag -> Just (FwdRes ag noFwdRewrite) + +deepFwdRw :: SimpleFwdRewrite n f -> FwdRewrite n f +deepFwdRw r = iterFwdRw (shallowFwdRw r) + +thenFwdRw :: FwdRewrite n f -> FwdRewrite n f -> FwdRewrite n f +thenFwdRw rw1 rw2 n f + = case rw1 n f of + Nothing -> rw2 n f + Just (FwdRes ag rw1a) -> Just (FwdRes ag (rw1a `thenFwdRw` rw2)) + +iterFwdRw :: FwdRewrite n f -> FwdRewrite n f +iterFwdRw rw = + \ n f -> case rw n f of + Just (FwdRes g rw2) -> Just $ FwdRes g (rw2 `thenFwdRw` iterFwdRw rw) + Nothing -> Nothing + +---------------------------------------------------------------- + +type SimpleBwdRewrite n f + = forall e x. n e x -> Fact x f + -> Maybe (AGraph n e x) + +noBwdRewrite :: BwdRewrite n f +noBwdRewrite _ _ = Nothing + +shallowBwdRw :: SimpleBwdRewrite n f -> BwdRewrite n f +shallowBwdRw rw n f = case (rw n f) of + Nothing -> Nothing + Just ag -> Just (BwdRes ag noBwdRewrite) + +deepBwdRw :: SimpleBwdRewrite n f -> BwdRewrite n f +deepBwdRw r = iterBwdRw (shallowBwdRw r) + + +thenBwdRw :: BwdRewrite n f -> BwdRewrite n f -> BwdRewrite n f +thenBwdRw rw1 rw2 n f + = case rw1 n f of + Nothing -> rw2 n f + Just (BwdRes ag rw1a) -> Just (BwdRes ag (rw1a `thenBwdRw` rw2)) + +iterBwdRw :: BwdRewrite n f -> BwdRewrite n f +iterBwdRw rw = + \ n f -> case rw n f of + Just (BwdRes g rw2) -> Just $ BwdRes g (rw2 `thenBwdRw` iterBwdRw rw) + Nothing -> Nothing + +{- +productFwd :: FwdPass n f -> FwdPass n f' -> FwdPass n (f, f') +productFwd pass pass' = FwdPass lattice transfer rewrite + where -- can't tell if I have a FactBase of pairs or a pair of facts + transfer n fb = (fp_transfer pass $ factBaseMap fst fb, + fp_transfer pass' $ factBaseMap snd fb) + transfer n (f, f') = (fp_transfer pass f, fp_transfer pass' f') + ... + +-} diff --git a/Compiler/Hoopl/Dataflow.hs b/Compiler/Hoopl/Dataflow.hs --- a/Compiler/Hoopl/Dataflow.hs +++ b/Compiler/Hoopl/Dataflow.hs @@ -58,12 +58,11 @@ module Compiler.Hoopl.Dataflow ( DataflowLattice(..), JoinFun, OldFact(..), NewFact(..) , ChangeFlag(..), changeIf - , FwdPass(..), FwdTransfer, FwdRewrite, SimpleFwdRewrite, FwdRes(..) - , noFwdRewrite, thenFwdRw, shallowFwdRw, deepFwdRw, iterFwdRw - , BwdPass(..), BwdTransfer, BwdRewrite, SimpleBwdRewrite, BwdRes(..) - , noBwdRewrite, thenBwdRw, shallowBwdRw, deepBwdRw, iterBwdRw + , FwdPass(..), FwdTransfer, FwdRewrite, FwdRes(..) + , BwdPass(..), BwdTransfer, BwdRewrite, BwdRes(..) , Fact - , analyzeAndRewriteFwd, analyzeAndRewriteBwd + , analyzeAndRewriteFwd, analyzeAndRewriteBwd + , analyzeAndRewriteFwd', analyzeAndRewriteBwd' ) where @@ -71,8 +70,8 @@ import Compiler.Hoopl.Graph import qualified Compiler.Hoopl.GraphUtil as U import Compiler.Hoopl.Label -import Compiler.Hoopl.MkGraph (AGraph) - +import Compiler.Hoopl.MkGraph (AGraph, graphOfAGraph) +import Compiler.Hoopl.Util ----------------------------------------------------------------------------- -- DataflowLattice @@ -86,11 +85,12 @@ , fact_do_logging :: Bool -- log changes } -type JoinFun a = OldFact a -> NewFact a -> (ChangeFlag, a) +type JoinFun a = Label -> OldFact a -> NewFact a -> (ChangeFlag, a) + -- the label argument is for debugging purposes only newtype OldFact a = OldFact a newtype NewFact a = NewFact a -data ChangeFlag = NoChange | SomeChange +data ChangeFlag = NoChange | SomeChange deriving (Eq, Ord) changeIf :: Bool -> ChangeFlag changeIf changed = if changed then SomeChange else NoChange @@ -115,33 +115,6 @@ type instance Fact C f = FactBase f type instance Fact O f = f -type SimpleFwdRewrite n f - = forall e x. n e x -> Fact e f - -> Maybe (AGraph n e x) - -noFwdRewrite :: FwdRewrite n f -noFwdRewrite _ _ = Nothing - -shallowFwdRw :: SimpleFwdRewrite n f -> FwdRewrite n f -shallowFwdRw rw n f = case (rw n f) of - Nothing -> Nothing - Just ag -> Just (FwdRes ag noFwdRewrite) - -deepFwdRw :: SimpleFwdRewrite n f -> FwdRewrite n f -deepFwdRw r = iterFwdRw (shallowFwdRw r) - -thenFwdRw :: FwdRewrite n f -> FwdRewrite n f -> FwdRewrite n f -thenFwdRw rw1 rw2 n f - = case rw1 n f of - Nothing -> rw2 n f - Just (FwdRes ag rw1a) -> Just (FwdRes ag (rw1a `thenFwdRw` rw2)) - -iterFwdRw :: FwdRewrite n f -> FwdRewrite n f -iterFwdRw rw = - \ n f -> case rw n f of - Just (FwdRes g rw2) -> Just $ FwdRes g (rw2 `thenFwdRw` iterFwdRw rw) - Nothing -> Nothing - analyzeAndRewriteFwd :: forall n f. Edges n => FwdPass n f @@ -152,6 +125,35 @@ = do { (rg, _) <- arfBody pass body facts ; return (normaliseBody rg) } +-- | if the graph being analyzed is open at the entry, there must +-- be no other entry point, or all goes horribly wrong... +analyzeAndRewriteFwd' + :: forall n f e x. Edges n + => FwdPass n f + -> Graph n e x -> Fact e f + -> FuelMonad (Graph n e x, FactBase f, MaybeO x f) +analyzeAndRewriteFwd' pass g f = + do (rg, fout) <- arfGraph pass g f + let (g', fb) = normalizeGraph g rg + return (g', fb, distinguishedExitFact g' fout) + +distinguishedExitFact :: forall n e x f . Graph n e x -> Fact x f -> MaybeO x f +distinguishedExitFact g f = maybe g + where maybe :: Graph n e x -> MaybeO x f + maybe GNil = JustO f + maybe (GUnit {}) = JustO f + maybe (GMany _ _ x) = case x of NothingO -> NothingO + JustO _ -> JustO f + +normalizeGraph :: Edges n => Graph n e x -> RG n f e x -> GraphWithFacts n f e x +normalizeGraph GNil = normOO +normalizeGraph (GUnit {}) = normOO +normalizeGraph (GMany NothingO _ NothingO) = normCC +normalizeGraph (GMany (JustO _) _ NothingO) = normOC +normalizeGraph (GMany NothingO _ (JustO _)) = normCO +normalizeGraph (GMany (JustO _) _ (JustO _)) = normOO + + ---------------------------------------------------------------- -- Forward Implementation ---------------------------------------------------------------- @@ -209,13 +211,11 @@ ; (exit', fx) <- arfBlock pass exit fb ; return (entry' `RGCatC` body' `RGCatC` exit', fx) } -forwardBlockList :: Edges n => [Label] -> Body n -> [((Label,Block n C C), [Label])] +forwardBlockList :: (Edges n, LabelsPtr entry) + => entry -> Body n -> [Block n C C] -- This produces a list of blocks in order suitable for forward analysis, -- along with the list of Labels it may depend on for facts. --- ToDo: Do a topological sort to improve convergence rate of fixpoint --- This will require a (HavingSuccessors l) class constraint -forwardBlockList _ blks = map withLbl $ bodyList blks - where withLbl (l, b) = ((l, b), [l]) +forwardBlockList entries blks = postorder_dfs_from (bodyMap blks) entries ----------------------------------------------------------------------------- -- Backward analysis and rewriting: the interface @@ -232,34 +232,6 @@ = forall e x. n e x -> Fact x f -> Maybe (BwdRes n f e x) data BwdRes n f e x = BwdRes (AGraph n e x) (BwdRewrite n f) -type SimpleBwdRewrite n f - = forall e x. n e x -> Fact x f - -> Maybe (AGraph n e x) - -noBwdRewrite :: BwdRewrite n f -noBwdRewrite _ _ = Nothing - -shallowBwdRw :: SimpleBwdRewrite n f -> BwdRewrite n f -shallowBwdRw rw n f = case (rw n f) of - Nothing -> Nothing - Just ag -> Just (BwdRes ag noBwdRewrite) - -deepBwdRw :: SimpleBwdRewrite n f -> BwdRewrite n f -deepBwdRw r = iterBwdRw (shallowBwdRw r) - - -thenBwdRw :: BwdRewrite n f -> BwdRewrite n f -> BwdRewrite n f -thenBwdRw rw1 rw2 n f - = case rw1 n f of - Nothing -> rw2 n f - Just (BwdRes ag rw1a) -> Just (BwdRes ag (rw1a `thenBwdRw` rw2)) - -iterBwdRw :: BwdRewrite n f -> BwdRewrite n f -iterBwdRw rw = - \ n f -> case rw n f of - Just (BwdRes g rw2) -> Just $ BwdRes g (rw2 `thenBwdRw` iterBwdRw rw) - Nothing -> Nothing - ----------------------------------------------------------------------------- -- Backward implementation ----------------------------------------------------------------------------- @@ -294,7 +266,7 @@ -> FuelMonad (RG n f C C, FactBase f) arbBody pass blocks init_fbase = fixpoint False (bp_lattice pass) (arbBlock pass) init_fbase $ - backwardBlockList (factBaseLabels init_fbase) blocks + backwardBlockList blocks arbGraph :: Edges n => ARB (Graph n) n arbGraph _ GNil f = return (RGNil, f) @@ -316,12 +288,52 @@ ; (entry', fe) <- arbBlock pass entry fb ; return (entry' `RGCatC` body' `RGCatC` exit', fe) } -backwardBlockList :: Edges n => [Label] -> Body n -> [((Label, Block n C C), [Label])] +backwardBlockList :: Edges n => Body n -> [Block n C C] -- This produces a list of blocks in order suitable for backward analysis, -- along with the list of Labels it may depend on for facts. -backwardBlockList _ blks = map withSuccs $ bodyList blks - where withSuccs (l, b) = ((l, b), successors b) +backwardBlockList body = reachable ++ missing + where reachable = reverse $ forwardBlockList entries body + entries = externalEntryLabels body + all = bodyList body + missingLabels = + mkLabelSet (map fst all) `minusLabelSet` + mkLabelSet (map entryLabel reachable) + missing = map snd $ filter (flip elemLabelSet missingLabels . fst) all +{- + +The forward and backward dataflow analyses now use postorder depth-first +order for faster convergence. + +The forward and backward cases are not dual. In the forward case, the +entry points are known, and one simply traverses the body blocks from +those points. In the backward case, something is known about the exit +points, but this information is essentially useless, because we don't +actually have a dual graph (that is, one with edges reversed) to +compute with. (Even if we did have a dual graph, it would not avail +us---a backward analysis must include reachable blocks that don't +reach the exit, as in a procedure that loops forever and has side +effects.) + +Since in the general case, no information is available about entry +points, I have put in a horrible hack. First, I assume that every +label defined but not used is an entry point. Then, because an entry +point might also be a loop header, I add, in arbitrary order, all the +remaining "missing" blocks. Needless to say, I am not pleased. +I am not satisfied. I am not Senator Morgan. + +Wait! I believe that the Right Thing here is to require that anyone +wishing to analyze a graph closed at the entry provide a way of +determining the entry points, if any, of that graph. This requirement +can apply equally to forward and backward analyses; I believe that +using the input FactBase to determine the entry points of a closed +graph is *also* a hack. + +NR + +-} + + analyzeAndRewriteBwd :: forall n f. Edges n => BwdPass n f @@ -332,7 +344,27 @@ = do { (rg, _) <- arbBody pass body facts ; return (normaliseBody rg) } +-- | if the graph being analyzed is open at the exit, I don't +-- quite understand the implications of possible other exits +analyzeAndRewriteBwd' + :: forall n f e x. Edges n + => BwdPass n f + -> Graph n e x -> Fact x f + -> FuelMonad (Graph n e x, FactBase f, MaybeO e f) +analyzeAndRewriteBwd' pass g f = + do (rg, fout) <- arbGraph pass g f + let (g', fb) = normalizeGraph g rg + return (g', fb, distinguishedEntryFact g' fout) +distinguishedEntryFact :: forall n e x f . Graph n e x -> Fact e f -> MaybeO e f +distinguishedEntryFact g f = maybe g + where maybe :: Graph n e x -> MaybeO e f + maybe GNil = JustO f + maybe (GUnit {}) = JustO f + maybe (GMany e _ _) = case e of NothingO -> NothingO + JustO _ -> JustO f + + ----------------------------------------------------------------------------- -- fixpoint: finding fixed points ----------------------------------------------------------------------------- @@ -359,10 +391,11 @@ | lbl `elemLabelSet` lbls = (SomeChange, new_fbase) | otherwise = (cha, new_fbase) where - (cha2, res_fact) + (cha2, res_fact) -- Note [Unreachable blocks] = case lookupFact fbase lbl of - Nothing -> (SomeChange, new_fact) -- Note [Unreachable blocks] - Just old_fact -> fact_extend lat (OldFact old_fact) (NewFact new_fact) + Nothing -> (SomeChange, snd $ join $ fact_bot lat) -- Note [Unreachable blocks] + Just old_fact -> join old_fact + where join old_fact = fact_extend lat lbl (OldFact old_fact) (NewFact new_fact) new_fbase = extendFactBase fbase lbl res_fact fixpoint :: forall n f. Edges n @@ -370,9 +403,10 @@ -> DataflowLattice f -> (Block n C C -> FactBase f -> FuelMonad (RG n f C C, FactBase f)) - -> FactBase f -> [((Label, Block n C C), [Label])] + -> FactBase f + -> [Block n C C] -> FuelMonad (RG n f C C, FactBase f) -fixpoint is_fwd lat do_block init_fbase blocks +fixpoint is_fwd lat do_block init_fbase untagged_blocks = do { fuel <- getFuel ; tx_fb <- loop fuel init_fbase ; return (tfb_rg tx_fb, @@ -380,7 +414,10 @@ -- The successors of the Graph are the the Labels for which -- we have facts, that are *not* in the blocks of the graph where - tx_blocks :: [((Label, Block n C C), [Label])] + blocks = map tag untagged_blocks + where tag b = ((entryLabel b, b), if is_fwd then [entryLabel b] else successors b) + + tx_blocks :: [((Label, Block n C C), [Label])] -- I do not understand this type -> TxFactBase n f -> FuelMonad (TxFactBase n f) tx_blocks [] tx_fb = return tx_fb tx_blocks (((lbl,blk), deps):bs) tx_fb = tx_block lbl blk deps tx_fb >>= tx_blocks bs @@ -439,6 +476,10 @@ bottom the points above bottom +* Even if the fact is going from UNR to bottom, we still call the + client's fact_extend function because it might give the client + some useful debugging information. + * All of this only applies for *forward* fixpoints. For the backward case we must treat every block as reachable; it might finish with a 'return', and therefore have no successors, for example. @@ -503,9 +544,3 @@ bwfUnion :: BodyWithFacts n f -> BodyWithFacts n f -> BodyWithFacts n f bwfUnion (bg1, fb1) (bg2, fb2) = (bg1 `BodyCat` bg2, fb1 `unionFactBase` fb2) -} - ------------------------------------------------------------------------------ - -graphOfAGraph :: AGraph node e x -> FuelMonad (Graph node e x) -graphOfAGraph ag = ag - diff --git a/Compiler/Hoopl/Debug.hs b/Compiler/Hoopl/Debug.hs new file mode 100644 --- /dev/null +++ b/Compiler/Hoopl/Debug.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE RankNTypes, GADTs, ScopedTypeVariables, FlexibleContexts #-} + +module Compiler.Hoopl.Debug + ( TraceFn , debugFwdJoins , debugBwdJoins + ) +where + +import Compiler.Hoopl.Dataflow + +-------------------------------------------------------------------------------- +-- | Debugging combinators: +-- Each combinator takes a dataflow pass and produces +-- a dataflow pass that can output debugging messages. +-- You provide the function, we call it with the applicable message. +-- +-- The most common use case is probably to: +-- +-- 1. import 'Debug.Trace' +-- +-- 2. pass 'trace' as the 1st argument to the debug combinator +-- +-- 3. pass 'const true' as the 2nd argument to the debug combinator +-------------------------------------------------------------------------------- + + +debugFwdJoins :: forall n f . Show f => TraceFn -> ChangePred -> FwdPass n f -> FwdPass n f +debugBwdJoins :: forall n f . Show f => TraceFn -> ChangePred -> BwdPass n f -> BwdPass n f + +type TraceFn = forall a . String -> a -> a +type ChangePred = ChangeFlag -> Bool + +debugFwdJoins trace pred p = p { fp_lattice = debugJoins trace pred $ fp_lattice p } +debugBwdJoins trace pred p = p { bp_lattice = debugJoins trace pred $ bp_lattice p } + +debugJoins :: Show f => TraceFn -> ChangePred -> DataflowLattice f -> DataflowLattice f +debugJoins trace showOutput l@(DataflowLattice {fact_extend = extend}) = l {fact_extend = extend'} + where + extend' l f1@(OldFact of1) f2@(NewFact nf2) = + if showOutput c then trace output res else res + where res@(c, f') = extend l f1 f2 + output = case c of + SomeChange -> "+ Join@" ++ show l ++ ": " ++ show of1 ++ " |_| " + ++ show nf2 ++ " = " ++ show f' + NoChange -> "_ Join@" ++ show l ++ ": " ++ show nf2 ++ " <= " ++ show of1 + +-------------------------------------------------------------------------------- +-- Functions we'd like to have, but don't know how to implement generically: +-------------------------------------------------------------------------------- + +-- type Showing n = forall e x . n e x -> String +-- debugFwdTransfers, debugFwdRewrites, debugFwdAll :: +-- forall n f . Show f => TraceFn -> Showing n -> FwdPass n f -> FwdPass n f +-- debugBwdTransfers, debugBwdRewrites, debugBwdAll :: +-- forall n f . Show f => TraceFn -> Showing n -> BwdPass n f -> BwdPass n f + diff --git a/Compiler/Hoopl/Graph.hs b/Compiler/Hoopl/Graph.hs --- a/Compiler/Hoopl/Graph.hs +++ b/Compiler/Hoopl/Graph.hs @@ -1,7 +1,7 @@ {-# LANGUAGE GADTs, EmptyDataDecls #-} module Compiler.Hoopl.Graph - ( O, C, Block(..), Body(..), bodyMap, Graph(..), MaybeO(..) + ( O, C, Block(..), Body, Body'(..), bodyMap, Graph, Graph'(..), MaybeO(..) , Edges(entryLabel, successors) , addBlock, bodyList ) @@ -21,23 +21,29 @@ BUnit :: n e x -> Block n e x BCat :: Block n e O -> Block n O x -> Block n e x -data Body n where - BodyEmpty :: Body n - BodyUnit :: Block n C C -> Body n - BodyCat :: Body n -> Body n -> Body n +type Body = Body' Block +data Body' block n where + BodyEmpty :: Body' block n + BodyUnit :: block n C C -> Body' block n + BodyCat :: Body' block n -> Body' block n -> Body' block n -data Graph n e x where - GNil :: Graph n O O - GUnit :: Block n O O -> Graph n O O - GMany :: MaybeO e (Block n O C) - -> Body n - -> MaybeO x (Block n C O) - -> Graph n e x +type Graph = Graph' Block +data Graph' block n e x where + GNil :: Graph' block n O O + GUnit :: block n O O -> Graph' block n O O + GMany :: MaybeO e (block n O C) + -> Body' block n + -> MaybeO x (block n C O) + -> Graph' block n e x data MaybeO ex t where JustO :: t -> MaybeO O t NothingO :: MaybeO C t +instance Functor (MaybeO ex) where + fmap f NothingO = NothingO + fmap f (JustO a) = JustO (f a) + ------------------------------- class Edges thing where entryLabel :: thing C x -> Label @@ -50,16 +56,16 @@ successors (BCat _ b) = successors b ------------------------------ -addBlock :: Block n C C -> Body n -> Body n +addBlock :: block n C C -> Body' block n -> Body' block n addBlock b body = BodyUnit b `BodyCat` body -bodyList :: Edges n => Body n -> [(Label,Block n C C)] +bodyList :: Edges (block n) => Body' block n -> [(Label,block n C C)] bodyList body = go body [] where go BodyEmpty bs = bs go (BodyUnit b) bs = (entryLabel b, b) : bs go (BodyCat b1 b2) bs = go b1 (go b2 bs) -bodyMap :: Edges n => Body n -> LabelMap (Block n C C) +bodyMap :: Edges (block n) => Body' block n -> LabelMap (block n C C) bodyMap = mkFactBase . bodyList diff --git a/Compiler/Hoopl/GraphUtil.hs b/Compiler/Hoopl/GraphUtil.hs --- a/Compiler/Hoopl/GraphUtil.hs +++ b/Compiler/Hoopl/GraphUtil.hs @@ -1,38 +1,65 @@ -{-# LANGUAGE GADTs #-} +{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables #-} {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} -- bug in GHC -- N.B. addBasicBlocks won't work on OO without a Node (branch/label) constraint module Compiler.Hoopl.GraphUtil - ( gSplice + ( splice, gSplice, zSplice + , zCat , bodyGraph ) where import Compiler.Hoopl.Graph +import Compiler.Hoopl.Zipper bodyGraph :: Body n -> Graph n C C bodyGraph b = GMany NothingO b NothingO +splice :: forall block n e a x . + (forall e x . block n e O -> block n O x -> block n e x) + -> (Graph' block n e a -> Graph' block n a x -> Graph' block n e x) +splice bcat = sp + where sp :: forall e a x . + Graph' block n e a -> Graph' block n a x -> Graph' block n e x -gSplice :: Graph n e a -> Graph n a x -> Graph n e x + sp GNil g2 = g2 + sp g1 GNil = g1 -gSplice GNil g2 = g2 -gSplice g1 GNil = g1 + sp (GUnit b1) (GUnit b2) = GUnit (b1 `bcat` b2) -gSplice (GUnit b1) (GUnit b2) - = GUnit (b1 `BCat` b2) + sp (GUnit b) (GMany (JustO e) bs x) = GMany (JustO (b `bcat` e)) bs x -gSplice (GUnit b) (GMany (JustO e) bs x) - = GMany (JustO (b `BCat` e)) bs x + sp (GMany e bs (JustO x)) (GUnit b2) = GMany e bs (JustO (x `bcat` b2)) -gSplice (GMany e bs (JustO x)) (GUnit b2) - = GMany e bs (JustO (x `BCat` b2)) + sp (GMany e1 bs1 (JustO x1)) (GMany (JustO e2) bs2 x2) + = GMany e1 (addBlock (x1 `bcat` e2) bs1 `BodyCat` bs2) x2 -gSplice (GMany e1 bs1 (JustO x1)) (GMany (JustO e2) bs2 x2) - = GMany e1 (addBlock (x1 `BCat` e2) bs1 `BodyCat` bs2) x2 + sp (GMany e1 bs1 NothingO) (GMany NothingO bs2 x2) + = GMany e1 (bs1 `BodyCat` bs2) x2 -gSplice (GMany e1 bs1 NothingO) (GMany NothingO bs2 x2) - = GMany e1 (bs1 `BodyCat` bs2) x2 + +gSplice :: Graph n e a -> Graph n a x -> Graph n e x +zSplice :: ZGraph n e a -> ZGraph n a x -> ZGraph n e x + +gSplice = splice BCat +zSplice = splice zCat + +zCat :: ZBlock n e O -> ZBlock n O x -> ZBlock n e x +zCat b1@(ZFirst {}) (ZMiddle n) = ZHead b1 n +zCat b1@(ZFirst {}) b2@(ZLast{}) = ZClosed b1 b2 +zCat b1@(ZFirst {}) b2@(ZTail{}) = ZClosed b1 b2 +zCat b1@(ZFirst {}) (ZCat b2 b3) = (b1 `zCat` b2) `zCat` b3 +zCat b1@(ZHead {}) (ZCat b2 b3) = (b1 `zCat` b2) `zCat` b3 +zCat b1@(ZHead {}) (ZMiddle n) = ZHead b1 n +zCat b1@(ZHead {}) b2@(ZLast{}) = ZClosed b1 b2 +zCat b1@(ZHead {}) b2@(ZTail{}) = ZClosed b1 b2 +zCat (ZMiddle n) b2@(ZLast{}) = ZTail n b2 +zCat b1@(ZMiddle {}) b2@(ZCat{}) = ZCat b1 b2 +zCat (ZMiddle n) b2@(ZTail{}) = ZTail n b2 +zCat (ZCat b1 b2) b3@(ZLast{}) = b1 `zCat` (b2 `zCat` b3) +zCat (ZCat b1 b2) b3@(ZTail{}) = b1 `zCat` (b2 `zCat` b3) +zCat b1@(ZCat {}) b2@(ZCat{}) = ZCat b1 b2 + diff --git a/Compiler/Hoopl/Label.hs b/Compiler/Hoopl/Label.hs --- a/Compiler/Hoopl/Label.hs +++ b/Compiler/Hoopl/Label.hs @@ -74,36 +74,40 @@ delFromFactBase fb blks = foldr (M.delete . unLabel . fst) fb blks ---------------------- -type LabelSet = S.IntSet -- ought to be a newtype or we expose the rep... +newtype LabelSet = LS { unLS :: S.IntSet } emptyLabelSet :: LabelSet -emptyLabelSet = S.empty +emptyLabelSet = LS S.empty extendLabelSet :: LabelSet -> Label -> LabelSet -extendLabelSet lbls (Label bid) = S.insert bid lbls +extendLabelSet lbls (Label bid) = LS $ S.insert bid $ unLS lbls reduceLabelSet :: LabelSet -> Label -> LabelSet -reduceLabelSet lbls (Label bid) = S.delete bid lbls +reduceLabelSet lbls (Label bid) = LS $ S.delete bid $ unLS lbls elemLabelSet :: Label -> LabelSet -> Bool -elemLabelSet (Label bid) lbls = S.member bid lbls +elemLabelSet (Label bid) lbls = S.member bid (unLS lbls) labelSetElems :: LabelSet -> [Label] -labelSetElems = map Label . S.toList +labelSetElems = map Label . S.toList . unLS +set2 :: (S.IntSet -> S.IntSet -> S.IntSet) + -> (LabelSet -> LabelSet -> LabelSet) +set2 f (LS ls) (LS ls') = LS (f ls ls') + minusLabelSet :: LabelSet -> LabelSet -> LabelSet -minusLabelSet = S.difference +minusLabelSet = set2 S.difference unionLabelSet :: LabelSet -> LabelSet -> LabelSet -unionLabelSet = S.union +unionLabelSet = set2 S.union interLabelSet :: LabelSet -> LabelSet -> LabelSet -interLabelSet = S.intersection +interLabelSet = set2 S.intersection sizeLabelSet :: LabelSet -> Int -sizeLabelSet = S.size +sizeLabelSet = S.size . unLS mkLabelSet :: [Label] -> LabelSet -mkLabelSet = S.fromList . map unLabel +mkLabelSet = LS . S.fromList . map unLabel diff --git a/Compiler/Hoopl/MkGraph.hs b/Compiler/Hoopl/MkGraph.hs --- a/Compiler/Hoopl/MkGraph.hs +++ b/Compiler/Hoopl/MkGraph.hs @@ -1,6 +1,7 @@ {-# LANGUAGE ScopedTypeVariables, GADTs #-} module Compiler.Hoopl.MkGraph - ( AGraph, (<*>), catAGraphs, addEntrySeq, addExitSeq, addBlocks, unionBlocks + ( AGraph, graphOfAGraph + , (<*>), (|*><*|), catAGraphs, addEntrySeq, addExitSeq, addBlocks, unionBlocks , emptyAGraph, emptyClosedAGraph, withFreshLabels , mkFirst, mkMiddle, mkMiddles, mkLast, mkBranch, mkLabel, mkWhileDo , IfThenElseable(mkIfThenElse) @@ -16,16 +17,16 @@ import Control.Monad (liftM2) -type AGraph n e x = FuelMonad (Graph n e x) +newtype AGraph n e x = A { graphOfAGraph :: FuelMonad (Graph n e x) } class Labels l where withFreshLabels :: (l -> AGraph n e x) -> AGraph n e x emptyAGraph :: AGraph n O O -emptyAGraph = return GNil +emptyAGraph = A $ return GNil emptyClosedAGraph :: AGraph n C C -emptyClosedAGraph = return $ GMany NothingO BodyEmpty NothingO +emptyClosedAGraph = A $ return $ GMany NothingO BodyEmpty NothingO {-| As noted in the paper, we can define a single, polymorphic type of @@ -55,6 +56,17 @@ redundant with 'addBlocks', because 'addBlocks' requires a 'HooplNode' constraint but 'unionBlocks' does not. + * The operator |*><*| splices two graphs at a closed point. The + vertical bar stands for "closed point" just as the angle brackets + above stand for "open point". Unlike the <*> operator, the |*><*| + can create a control-flow graph with dangling outedges or + unreachable blocks. The operator must be used carefully, so we + have chosen a long name on purpose, to help call people's + attention to what they're doing. + + * We have discussed a dynamic assertion about dangling outedges and + unreachable blocks, but nothing is implemented yet. + There is some redundancy in this representation (any instance of 'addEntrySeq' is also an instance of either 'addExitSeq' or 'addBlocks'), but because the different operators restrict polymorphism in different ways, @@ -65,7 +77,9 @@ infixl 3 <*> -(<*>) :: AGraph n e O -> AGraph n O x -> AGraph n e x +infixl 2 |*><*| +(<*>) :: AGraph n e O -> AGraph n O x -> AGraph n e x +(|*><*|) :: AGraph n e C -> AGraph n C x -> AGraph n e x addEntrySeq :: AGraph n O C -> AGraph n C x -> AGraph n O x @@ -74,19 +88,24 @@ => AGraph n e x -> AGraph n C C -> AGraph n e x unionBlocks :: AGraph n C C -> AGraph n C C -> AGraph n C C -addEntrySeq = liftM2 U.gSplice -addExitSeq = liftM2 U.gSplice -unionBlocks = liftM2 U.gSplice +liftA2 :: (Graph n a b -> Graph n c d -> Graph n e f) + -> (AGraph n a b -> AGraph n c d -> AGraph n e f) -addBlocks g blocks = g >>= \g -> blocks >>= add g - where add :: HooplNode n => Graph n e x -> Graph n C C -> AGraph n e x +liftA2 f (A g) (A g') = A (liftM2 f g g') + +addEntrySeq = liftA2 U.gSplice +addExitSeq = liftA2 U.gSplice +unionBlocks = liftA2 U.gSplice + +addBlocks (A g) (A blocks) = A $ g >>= \g -> blocks >>= add g + where add :: HooplNode n => Graph n e x -> Graph n C C -> FuelMonad (Graph n e x) add (GMany e body x) (GMany NothingO body' NothingO) = return $ GMany e (body `BodyCat` body') x add g@GNil blocks = spliceOO g blocks add g@(GUnit _) blocks = spliceOO g blocks - spliceOO :: HooplNode n => Graph n O O -> Graph n C C -> AGraph n O O - spliceOO g blocks = withFreshLabels $ \l -> - return g <*> mkBranch l `addEntrySeq` return blocks `addExitSeq` mkLabel l + spliceOO :: HooplNode n => Graph n O O -> Graph n C C -> FuelMonad(Graph n O O) + spliceOO g blocks = graphOfAGraph $ withFreshLabels $ \l -> + A (return g) <*> mkBranch l |*><*| A (return blocks) |*><*| mkLabel l mkFirst :: n C O -> AGraph n C O @@ -126,7 +145,8 @@ -- IMPLEMENTATION -- ================================================================ -(<*>) = liftM2 U.gSplice +(<*>) = liftA2 U.gSplice +(|*><*|) = liftA2 U.gSplice catAGraphs :: [AGraph n O O] -> AGraph n O O catAGraphs = foldr (<*>) emptyAGraph @@ -136,16 +156,13 @@ mkLabel id = mkFirst $ mkLabelNode id mkBranch target = mkLast $ mkBranchNode target -mkMiddles ms = foldr (<*>) (return GNil) (map mkMiddle ms) +mkMiddles ms = foldr (<*>) emptyAGraph (map mkMiddle ms) instance IfThenElseable O where - mkIfThenElse cbranch tbranch fbranch = do - endif <- freshLabel - ltrue <- freshLabel - lfalse <- freshLabel - cbranch ltrue lfalse `addEntrySeq` - (mkLabel ltrue <*> tbranch <*> mkBranch endif) `addBlocks` - (mkLabel lfalse <*> fbranch <*> mkBranch endif) `addExitSeq` + mkIfThenElse cbranch tbranch fbranch = withFreshLabels $ \(endif, ltrue, lfalse) -> + cbranch ltrue lfalse |*><*| + mkLabel ltrue <*> tbranch <*> mkBranch endif |*><*| + mkLabel lfalse <*> fbranch <*> mkBranch endif |*><*| mkLabel endif {- @@ -153,24 +170,19 @@ -} instance IfThenElseable C where - mkIfThenElse cbranch tbranch fbranch = do - ltrue <- freshLabel - lfalse <- freshLabel - cbranch ltrue lfalse `addEntrySeq` - (mkLabel ltrue <*> tbranch) `addBlocks` - (mkLabel lfalse <*> fbranch) + mkIfThenElse cbranch tbranch fbranch = withFreshLabels $ \(ltrue, lfalse) -> + cbranch ltrue lfalse |*><*| + mkLabel ltrue <*> tbranch |*><*| + mkLabel lfalse <*> fbranch {- fallThroughTo _ g = g -} -mkWhileDo cbranch body = do - test <- freshLabel - head <- freshLabel - endwhile <- freshLabel +mkWhileDo cbranch body = withFreshLabels $ \(test, head, endwhile) -> -- Forrest Baskett's while-loop layout - mkBranch test `addEntrySeq` - (mkLabel head <*> body <*> mkBranch test) `addBlocks` - (mkLabel test <*> cbranch head endwhile) `addExitSeq` + mkBranch test |*><*| + mkLabel head <*> body <*> mkBranch test |*><*| + mkLabel test <*> cbranch head endwhile |*><*| mkLabel endwhile ------------------------------------- @@ -194,7 +206,7 @@ instance Labels Label where - withFreshLabels f = freshLabel >>= f + withFreshLabels f = A $ freshLabel >>= (graphOfAGraph . f) instance (Labels l1, Labels l2) => Labels (l1, l2) where withFreshLabels f = withFreshLabels $ \l1 -> @@ -215,9 +227,9 @@ f (l1, l2, l3, l4) -mkExit block = return $ GMany NothingO BodyEmpty (JustO block) -mkEntry block = return $ GMany (JustO block) BodyEmpty NothingO +mkExit block = A $ return $ GMany NothingO BodyEmpty (JustO block) +mkEntry block = A $ return $ GMany (JustO block) BodyEmpty NothingO mkFirst = mkExit . BUnit mkLast = mkEntry . BUnit -mkMiddle = return . GUnit . BUnit +mkMiddle = A . return . GUnit . BUnit diff --git a/Compiler/Hoopl/Show.hs b/Compiler/Hoopl/Show.hs new file mode 100644 --- /dev/null +++ b/Compiler/Hoopl/Show.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE RankNTypes, GADTs, ScopedTypeVariables, FlexibleContexts #-} + +module Compiler.Hoopl.Show + ( showGraph + ) +where + +import Compiler.Hoopl.Graph + +-------------------------------------------------------------------------------- +-- Prettyprinting +-------------------------------------------------------------------------------- + +type Showing n = forall e x . n e x -> String + + +showGraph :: forall n e x . (Edges n) => Showing n -> Graph n e x -> String +showGraph node = g + where g :: (Edges n) => Graph n e x -> String + g GNil = "" + g (GUnit block) = b block + g (GMany g_entry g_blocks g_exit) = + open b g_entry ++ body g_blocks ++ open b g_exit + body blocks = concatMap b (map snd $ bodyList blocks) + b :: forall e x . Block n e x -> String + b (BUnit n) = node n ++ "\n" + b (BCat b1 b2) = b b1 ++ b b2 + +open :: (a -> String) -> MaybeO z a -> String +open _ NothingO = "" +open p (JustO n) = p n diff --git a/Compiler/Hoopl/Util.hs b/Compiler/Hoopl/Util.hs --- a/Compiler/Hoopl/Util.hs +++ b/Compiler/Hoopl/Util.hs @@ -1,14 +1,216 @@ +{-# LANGUAGE GADTs, ScopedTypeVariables, FlexibleInstances, RankNTypes #-} + module Compiler.Hoopl.Util ( gUnitOO, gUnitOC, gUnitCO, gUnitCC + , graphMapBlocks + , zblockGraph + , postorder_dfs, postorder_dfs_from, postorder_dfs_from_except + , preorder_dfs, preorder_dfs_from_except + , labelsDefined, labelsUsed, externalEntryLabels + , LabelsPtr(..) ) where +import Control.Monad + import Compiler.Hoopl.Graph -gUnitOO :: Block n O O -> Graph n O O -gUnitOC :: Block n O C -> Graph n O C -gUnitCO :: Block n C O -> Graph n C O -gUnitCC :: Block n C C -> Graph n C C +import Compiler.Hoopl.Label +import Compiler.Hoopl.Zipper + +gUnitOO :: block n O O -> Graph' block n O O +gUnitOC :: block n O C -> Graph' block n O C +gUnitCO :: block n C O -> Graph' block n C O +gUnitCC :: block n C C -> Graph' block n C C gUnitOO b = GUnit b gUnitOC b = GMany (JustO b) BodyEmpty NothingO gUnitCO b = GMany NothingO BodyEmpty (JustO b) gUnitCC b = GMany NothingO (BodyUnit b) NothingO + +zblockGraph :: ZBlock n e x -> ZGraph n e x +zblockGraph b@(ZFirst {}) = gUnitCO b +zblockGraph b@(ZMiddle {}) = gUnitOO b +zblockGraph b@(ZLast {}) = gUnitOC b +zblockGraph b@(ZCat {}) = gUnitOO b +zblockGraph b@(ZHead {}) = gUnitCO b +zblockGraph b@(ZTail {}) = gUnitOC b +zblockGraph b@(ZClosed {}) = gUnitCC b + + +graphMapBlocks :: forall block n block' n' e x . + (forall e x . block n e x -> block' n' e x) + -> (Graph' block n e x -> Graph' block' n' e x) +bodyMapBlocks :: forall block n block' n' . + (block n C C -> block' n' C C) + -> (Body' block n -> Body' block' n') + +graphMapBlocks f = map + where map :: Graph' block n e x -> Graph' block' n' e x + map GNil = GNil + map (GUnit b) = GUnit (f b) + map (GMany e b x) = GMany (fmap f e) (bodyMapBlocks f b) (fmap f x) + +bodyMapBlocks f = map + where map BodyEmpty = BodyEmpty + map (BodyUnit b) = BodyUnit (f b) + map (BodyCat b1 b2) = BodyCat (map b1) (map b2) + + +---------------------------------------------------------------- + +class LabelsPtr l where + targetLabels :: l -> [Label] + +instance Edges n => LabelsPtr (n e C) where + targetLabels n = successors n + +instance LabelsPtr Label where + targetLabels l = [l] + +instance LabelsPtr LabelSet where + targetLabels = labelSetElems + +instance LabelsPtr l => LabelsPtr [l] where + targetLabels = concatMap targetLabels + + +-- | Traversal: 'postorder_dfs' returns a list of blocks reachable +-- from the entry of enterable graph. The entry and exit are *not* included. +-- The list has the following property: +-- +-- Say a "back reference" exists if one of a block's +-- control-flow successors precedes it in the output list +-- +-- Then there are as few back references as possible +-- +-- The output is suitable for use in +-- a forward dataflow problem. For a backward problem, simply reverse +-- the list. ('postorder_dfs' is sufficiently tricky to implement that +-- one doesn't want to try and maintain both forward and backward +-- versions.) + +postorder_dfs :: Edges (block n) => Graph' block n O x -> [block n C C] +preorder_dfs :: Edges (block n) => Graph' block n O x -> [block n C C] + +-- | This is the most important traversal over this data structure. It drops +-- unreachable code and puts blocks in an order that is good for solving forward +-- dataflow problems quickly. The reverse order is good for solving backward +-- dataflow problems quickly. The forward order is also reasonably good for +-- emitting instructions, except that it will not usually exploit Forrest +-- Baskett's trick of eliminating the unconditional branch from a loop. For +-- that you would need a more serious analysis, probably based on dominators, to +-- identify loop headers. +-- +-- The ubiquity of 'postorder_dfs' is one reason for the ubiquity of the 'LGraph' +-- representation, when for most purposes the plain 'Graph' representation is +-- more mathematically elegant (but results in more complicated code). +-- +-- Here's an easy way to go wrong! Consider +-- @ +-- A -> [B,C] +-- B -> D +-- C -> D +-- @ +-- Then ordinary dfs would give [A,B,D,C] which has a back ref from C to D. +-- Better to get [A,B,C,D] + + +graphDfs :: (Edges (block n)) + => (LabelMap (block n C C) -> block n O C -> LabelSet -> [block n C C]) + -> (Graph' block n O x -> [block n C C]) +graphDfs _ (GNil) = [] +graphDfs _ (GUnit{}) = [] +graphDfs order (GMany (JustO entry) body _) = order blockenv entry emptyLabelSet + where blockenv = bodyMap body + +postorder_dfs = graphDfs postorder_dfs_from_except +preorder_dfs = graphDfs preorder_dfs_from_except + +postorder_dfs_from_except :: forall block e . (Edges block, LabelsPtr e) + => LabelMap (block C C) -> e -> LabelSet -> [block C C] +postorder_dfs_from_except blocks b visited = + vchildren (get_children b) (\acc _visited -> acc) [] visited + where + vnode :: block C C -> ([block C C] -> LabelSet -> a) -> [block C C] -> LabelSet -> a + vnode block cont acc visited = + if elemLabelSet id visited then + cont acc visited + else + let cont' acc visited = cont (block:acc) visited in + vchildren (get_children block) cont' acc (extendLabelSet visited id) + where id = entryLabel block + vchildren bs cont acc visited = next bs acc visited + where next children acc visited = + case children of [] -> cont acc visited + (b:bs) -> vnode b (next bs) acc visited + get_children block = foldr add_id [] $ targetLabels block + add_id id rst = case lookupFact blocks id of + Just b -> b : rst + Nothing -> rst + +postorder_dfs_from + :: (Edges block, LabelsPtr b) => LabelMap (block C C) -> b -> [block C C] +postorder_dfs_from blocks b = postorder_dfs_from_except blocks b emptyLabelSet + + +---------------------------------------------------------------- + +data VM a = VM { unVM :: LabelSet -> (a, LabelSet) } +marked :: Label -> VM Bool +mark :: Label -> VM () +instance Monad VM where + return a = VM $ \visited -> (a, visited) + m >>= k = VM $ \visited -> let (a, v') = unVM m visited in unVM (k a) v' +marked l = VM $ \v -> (elemLabelSet l v, v) +mark l = VM $ \v -> ((), extendLabelSet v l) + +preorder_dfs_from_except :: forall block e . (Edges block, LabelsPtr e) + => LabelMap (block C C) -> e -> LabelSet -> [block C C] +preorder_dfs_from_except blocks b visited = + (fst $ unVM (children (get_children b)) visited) [] + where children [] = return id + children (b:bs) = liftM2 (.) (visit b) (children bs) + visit :: block C C -> VM (HL (block C C)) + visit b = do already <- marked (entryLabel b) + if already then return id + else do mark (entryLabel b) + bs <- children $ get_children b + return $ b `cons` bs + get_children block = foldr add_id [] $ targetLabels block + add_id id rst = case lookupFact blocks id of + Just b -> b : rst + Nothing -> rst + +type HL a = [a] -> [a] -- Hughes list (constant-time concatenation) +cons :: a -> HL a -> HL a +cons a as tail = a : as tail + +---------------------------------------------------------------- + +labelsDefined :: forall block n e x . Edges (block n) => Graph' block n e x -> LabelSet +labelsDefined GNil = emptyLabelSet +labelsDefined (GUnit{}) = emptyLabelSet +labelsDefined (GMany _ body x) = foldBodyBlocks addEntry body $ exitLabel x + where addEntry block labels = extendLabelSet labels (entryLabel block) + exitLabel :: MaybeO x (block n C O) -> LabelSet + exitLabel NothingO = emptyLabelSet + exitLabel (JustO b) = mkLabelSet [entryLabel b] + +labelsUsed :: forall block n e x. Edges (block n) => Graph' block n e x -> LabelSet +labelsUsed GNil = emptyLabelSet +labelsUsed (GUnit{}) = emptyLabelSet +labelsUsed (GMany e body _) = foldBodyBlocks addTargets body $ entryTargets e + where addTargets block labels = foldl extendLabelSet labels (successors block) + entryTargets :: MaybeO e (block n O C) -> LabelSet + entryTargets NothingO = emptyLabelSet + entryTargets (JustO b) = addTargets b emptyLabelSet + +foldBodyBlocks :: (block n C C -> a -> a) -> Body' block n -> a -> a +foldBodyBlocks _ BodyEmpty = id +foldBodyBlocks f (BodyUnit b) = f b +foldBodyBlocks f (BodyCat b b') = foldBodyBlocks f b . foldBodyBlocks f b' + +externalEntryLabels :: Edges (block n) => Body' block n -> LabelSet +externalEntryLabels body = defined `minusLabelSet` used + where defined = labelsDefined g + used = labelsUsed g + g = GMany NothingO body NothingO diff --git a/Compiler/Hoopl/ZipDataflow.hs b/Compiler/Hoopl/ZipDataflow.hs new file mode 100644 --- /dev/null +++ b/Compiler/Hoopl/ZipDataflow.hs @@ -0,0 +1,568 @@ +{-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs, EmptyDataDecls, PatternGuards, TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} -- bug in GHC + +{- Notes about the genesis of Hoopl7 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Hoopl7 has the following major chages + +a) GMany has symmetric entry and exit +b) GMany closed-entry does not record a BlockId +c) GMany open-exit does not record a BlockId +d) The body of a GMany is called Body +e) A Body is just a list of blocks, not a map. I've argued + elsewhere that this is consistent with (c) + +A consequence is that Graph is no longer an instance of Edges, +but nevertheless I managed to keep the ARF and ARB signatures +nice and uniform. + +This was made possible by + +* FwdTransfer looks like this: + type FwdTransfer n f + = forall e x. n e x -> Fact e f -> Fact x f + type family Fact x f :: * + type instance Fact C f = FactBase f + type instance Fact O f = f + + Note that the incoming fact is a Fact (not just 'f' as in Hoopl5,6). + It's up to the *transfer function* to look up the appropriate fact + in the FactBase for a closed-entry node. Example: + constProp (Label l) fb = lookupFact fb l + That is how Hoopl can avoid having to know the block-id for the + first node: it defers to the client. + + [Side note: that means the client must know about + bottom, in case the looupFact returns Nothing] + +* Note also that FwdTransfer *returns* a Fact too; + that is, the types in both directions are symmetrical. + Previously we returned a [(BlockId,f)] but I could not see + how to make everything line up if we do this. + + Indeed, the main shortcoming of Hoopl7 is that we are more + or less forced into this uniform representation of the facts + flowing into or out of a closed node/block/graph, whereas + previously we had more flexibility. + + In exchange the code is neater, with fewer distinct types. + And morally a FactBase is equivalent to [(BlockId,f)] and + nearly equivalent to (BlockId -> f). + +* I've realised that forwardBlockList and backwardBlockList + both need (Edges n), and that goes everywhere. + +* I renamed BlockId to Label +-} + +module Compiler.Hoopl.ZipDataflow + ( FwdPass(..), FwdTransfer, FwdRewrite, FwdRes(..) + , BwdPass(..), BwdTransfer, BwdRewrite, BwdRes(..) + , analyzeAndRewriteFwd, analyzeAndRewriteBwd + , analyzeAndRewriteFwd', analyzeAndRewriteBwd' + ) +where + +import Compiler.Hoopl.Dataflow + ( DataflowLattice(..), OldFact(..), NewFact(..) + , ChangeFlag(..) + , Fact + ) +import Compiler.Hoopl.Fuel +import Compiler.Hoopl.Graph +import qualified Compiler.Hoopl.GraphUtil as U +import Compiler.Hoopl.Label +import Compiler.Hoopl.Util +import Compiler.Hoopl.Zipper + +type AGraph n e x = FuelMonad (ZGraph n e x) +graphOfAGraph :: AGraph n e x -> FuelMonad (ZGraph n e x) +graphOfAGraph = id + +----------------------------------------------------------------------------- +-- Analyze and rewrite forward: the interface +----------------------------------------------------------------------------- + +data FwdPass n f + = FwdPass { fp_lattice :: DataflowLattice f + , fp_transfer :: FwdTransfer n f + , fp_rewrite :: FwdRewrite n f } + +type FwdTransfer n f + = forall e x. n e x -> Fact e f -> Fact x f + +type FwdRewrite n f + = forall e x. n e x -> Fact e f -> Maybe (FwdRes n f e x) +data FwdRes n f e x = FwdRes (AGraph n e x) (FwdRewrite n f) + -- result of a rewrite is a new graph and a (possibly) new rewrite function + +analyzeAndRewriteFwd + :: forall n f. Edges n + => FwdPass n f + -> ZBody n -> FactBase f + -> FuelMonad (ZBody n, FactBase f) + +analyzeAndRewriteFwd pass body facts + = do { (rg, _) <- arfBody pass body facts + ; return (normaliseBody rg) } + +-- | if the graph being analyzed is open at the entry, there must +-- be no other entry point, or all goes horribly wrong... +analyzeAndRewriteFwd' + :: forall n f e x. Edges n + => FwdPass n f + -> ZGraph n e x -> Fact e f + -> FuelMonad (ZGraph n e x, FactBase f, MaybeO x f) +analyzeAndRewriteFwd' pass g f = + do (rg, fout) <- arfGraph pass g f + let (g', fb) = normalizeGraph g rg + return (g', fb, distinguishedExitFact g' fout) + +distinguishedExitFact :: forall n e x f . ZGraph n e x -> Fact x f -> MaybeO x f +distinguishedExitFact g f = maybe g + where maybe :: ZGraph n e x -> MaybeO x f + maybe GNil = JustO f + maybe (GUnit {}) = JustO f + maybe (GMany _ _ x) = case x of NothingO -> NothingO + JustO _ -> JustO f + +normalizeGraph :: Edges n => ZGraph n e x -> RG n f e x -> GraphWithFacts n f e x +normalizeGraph GNil = normOO +normalizeGraph (GUnit {}) = normOO +normalizeGraph (GMany NothingO _ NothingO) = normCC +normalizeGraph (GMany (JustO _) _ NothingO) = normOC +normalizeGraph (GMany NothingO _ (JustO _)) = normCO +normalizeGraph (GMany (JustO _) _ (JustO _)) = normOO + + +---------------------------------------------------------------- +-- Forward Implementation +---------------------------------------------------------------- + + +type ARF' n f thing e x + = FwdPass n f -> thing e x -> Fact e f -> FuelMonad (RG n f e x, Fact x f) + +type ARF thing n = forall f e x . ARF' n f thing e x + + +arfNode :: Edges n + => (n e x -> ZBlock n e x) + -> ARF' n f n e x +arfNode bunit pass node f + = do { mb_g <- withFuel (fp_rewrite pass node f) + ; case mb_g of + Nothing -> return (RGUnit f (bunit node), + fp_transfer pass node f) + Just (FwdRes ag rw) -> do { g <- graphOfAGraph ag + ; let pass' = pass { fp_rewrite = rw } + ; arfGraph pass' g f } } + +-- type demonstration +_arfBlock :: Edges n => ARF' n f (ZBlock n) e x +_arfBlock = arfBlock +_arfGraph :: Edges n => ARF' n f (ZGraph n) e x +_arfGraph = arfGraph + + +arfMiddle :: Edges n => ARF' n f n O O +arfMiddle = arfNode ZMiddle + + +arfBlock :: Edges n => ARF (ZBlock n) n +-- Lift from nodes to blocks +arfBlock pass (ZFirst node) = arfNode ZFirst pass node +arfBlock pass (ZMiddle node) = arfNode ZMiddle pass node +arfBlock pass (ZLast node) = arfNode ZLast pass node +arfBlock pass (ZCat b1 b2) = arfCat arfBlock arfBlock pass b1 b2 +arfBlock pass (ZHead h n) = arfCat arfBlock arfMiddle pass h n +arfBlock pass (ZTail n t) = arfCat arfMiddle arfBlock pass n t +arfBlock pass (ZClosed h t) = arfCat arfBlock arfBlock pass h t + +arfCat :: Edges n => ARF' n f thing1 e O -> ARF' n f thing2 O x + -> FwdPass n f -> thing1 e O -> thing2 O x + -> Fact e f -> FuelMonad (RG n f e x, Fact x f) +arfCat arf1 arf2 pass thing1 thing2 f = do { (g1,f1) <- arf1 pass thing1 f + ; (g2,f2) <- arf2 pass thing2 f1 + ; return (g1 `RGCatO` g2, f2) } +arfBody :: Edges n + + => FwdPass n f -> ZBody n -> FactBase f + -> FuelMonad (RG n f C C, FactBase f) + -- Outgoing factbase is restricted to Labels *not* in + -- in the Body; the facts for Labels *in* + -- the Body are in the BodyWithFacts +arfBody pass blocks init_fbase + = fixpoint True (fp_lattice pass) (arfBlock pass) init_fbase $ + forwardBlockList (factBaseLabels init_fbase) blocks + +arfGraph :: Edges n => ARF (ZGraph n) n +-- Lift from blocks to graphs +arfGraph _ GNil f = return (RGNil, f) +arfGraph pass (GUnit blk) f = arfBlock pass blk f +arfGraph pass (GMany NothingO body NothingO) f + = do { (body', fb) <- arfBody pass body f + ; return (body', fb) } +arfGraph pass (GMany NothingO body (JustO exit)) f + = do { (body', fb) <- arfBody pass body f + ; (exit', fx) <- arfBlock pass exit fb + ; return (body' `RGCatC` exit', fx) } +arfGraph pass (GMany (JustO entry) body NothingO) f + = do { (entry', fe) <- arfBlock pass entry f + ; (body', fb) <- arfBody pass body fe + ; return (entry' `RGCatC` body', fb) } +arfGraph pass (GMany (JustO entry) body (JustO exit)) f + = do { (entry', fe) <- arfBlock pass entry f + ; (body', fb) <- arfBody pass body fe + ; (exit', fx) <- arfBlock pass exit fb + ; return (entry' `RGCatC` body' `RGCatC` exit', fx) } + +forwardBlockList :: (Edges n, LabelsPtr entry) + => entry -> ZBody n -> [ZBlock n C C] +-- This produces a list of blocks in order suitable for forward analysis, +-- along with the list of Labels it may depend on for facts. +forwardBlockList entries blks = postorder_dfs_from (bodyMap blks) entries + +----------------------------------------------------------------------------- +-- Backward analysis and rewriting: the interface +----------------------------------------------------------------------------- + +data BwdPass n f + = BwdPass { bp_lattice :: DataflowLattice f + , bp_transfer :: BwdTransfer n f + , bp_rewrite :: BwdRewrite n f } + +type BwdTransfer n f + = forall e x. n e x -> Fact x f -> Fact e f +type BwdRewrite n f + = forall e x. n e x -> Fact x f -> Maybe (BwdRes n f e x) +data BwdRes n f e x = BwdRes (AGraph n e x) (BwdRewrite n f) + +----------------------------------------------------------------------------- +-- Backward implementation +----------------------------------------------------------------------------- + +type ARB' n f thing e x + = BwdPass n f -> thing e x -> Fact x f -> FuelMonad (RG n f e x, Fact e f) + +type ARB thing n = forall f e x. ARB' n f thing e x + +arbNode :: Edges n + => (n e x -> ZBlock n e x) + -> ARB' n f n e x +-- Lifts (BwdTransfer,BwdRewrite) to ARB_Node; +-- this time we do rewriting as well. +-- The ARB_Graph parameters specifies what to do with the rewritten graph +arbNode bunit pass node f + = do { mb_g <- withFuel (bp_rewrite pass node f) + ; case mb_g of + Nothing -> return (RGUnit entry_f (bunit node), entry_f) + where + entry_f = bp_transfer pass node f + Just (BwdRes ag rw) -> do { g <- graphOfAGraph ag + ; let pass' = pass { bp_rewrite = rw } + ; arbGraph pass' g f} } + +arbMiddle :: Edges n => ARB' n f n O O +arbMiddle = arbNode ZMiddle + +arbBlock :: Edges n => ARB (ZBlock n) n +-- Lift from nodes to blocks +arbBlock pass (ZFirst node) = arbNode ZFirst pass node +arbBlock pass (ZMiddle node) = arbNode ZMiddle pass node +arbBlock pass (ZLast node) = arbNode ZLast pass node +arbBlock pass (ZCat b1 b2) = arbCat arbBlock arbBlock pass b1 b2 +arbBlock pass (ZHead h n) = arbCat arbBlock arbMiddle pass h n +arbBlock pass (ZTail n t) = arbCat arbMiddle arbBlock pass n t +arbBlock pass (ZClosed h t) = arbCat arbBlock arbBlock pass h t + +arbCat :: Edges n => ARB' n f thing1 e O -> ARB' n f thing2 O x + -> BwdPass n f -> thing1 e O -> thing2 O x + -> Fact x f -> FuelMonad (RG n f e x, Fact e f) +arbCat arb1 arb2 pass thing1 thing2 f = do { (g2,f2) <- arb2 pass thing2 f + ; (g1,f1) <- arb1 pass thing1 f2 + ; return (g1 `RGCatO` g2, f1) } + +arbBody :: Edges n + => BwdPass n f -> ZBody n -> FactBase f + -> FuelMonad (RG n f C C, FactBase f) +arbBody pass blocks init_fbase + = fixpoint False (bp_lattice pass) (arbBlock pass) init_fbase $ + backwardBlockList blocks + +arbGraph :: Edges n => ARB (ZGraph n) n +arbGraph _ GNil f = return (RGNil, f) +arbGraph pass (GUnit blk) f = arbBlock pass blk f +arbGraph pass (GMany NothingO body NothingO) f + = do { (body', fb) <- arbBody pass body f + ; return (body', fb) } +arbGraph pass (GMany NothingO body (JustO exit)) f + = do { (exit', fx) <- arbBlock pass exit f + ; (body', fb) <- arbBody pass body fx + ; return (body' `RGCatC` exit', fb) } +arbGraph pass (GMany (JustO entry) body NothingO) f + = do { (body', fb) <- arbBody pass body f + ; (entry', fe) <- arbBlock pass entry fb + ; return (entry' `RGCatC` body', fe) } +arbGraph pass (GMany (JustO entry) body (JustO exit)) f + = do { (exit', fx) <- arbBlock pass exit f + ; (body', fb) <- arbBody pass body fx + ; (entry', fe) <- arbBlock pass entry fb + ; return (entry' `RGCatC` body' `RGCatC` exit', fe) } + +backwardBlockList :: Edges n => ZBody n -> [ZBlock n C C] +-- This produces a list of blocks in order suitable for backward analysis, +-- along with the list of Labels it may depend on for facts. +backwardBlockList body = reachable ++ missing + where reachable = reverse $ forwardBlockList entries body + entries = externalEntryLabels body + all = bodyList body + missingLabels = + mkLabelSet (map fst all) `minusLabelSet` + mkLabelSet (map entryLabel reachable) + missing = map snd $ filter (flip elemLabelSet missingLabels . fst) all + +{- + +The forward and backward dataflow analyses now use postorder depth-first +order for faster convergence. + +The forward and backward cases are not dual. In the forward case, the +entry points are known, and one simply traverses the body blocks from +those points. In the backward case, something is known about the exit +points, but this information is essentially useless, because we don't +actually have a dual graph (that is, one with edges reversed) to +compute with. (Even if we did have a dual graph, it would not avail +us---a backward analysis must include reachable blocks that don't +reach the exit, as in a procedure that loops forever and has side +effects.) + +Since in the general case, no information is available about entry +points, I have put in a horrible hack. First, I assume that every +label defined but not used is an entry point. Then, because an entry +point might also be a loop header, I add, in arbitrary order, all the +remaining "missing" blocks. Needless to say, I am not pleased. +I am not satisfied. I am not Senator Morgan. + +Wait! I believe that the Right Thing here is to require that anyone +wishing to analyze a graph closed at the entry provide a way of +determining the entry points, if any, of that graph. This requirement +can apply equally to forward and backward analyses; I believe that +using the input FactBase to determine the entry points of a closed +graph is *also* a hack. + +NR + +-} + + +analyzeAndRewriteBwd + :: forall n f. Edges n + => BwdPass n f + -> ZBody n -> FactBase f + -> FuelMonad (ZBody n, FactBase f) + +analyzeAndRewriteBwd pass body facts + = do { (rg, _) <- arbBody pass body facts + ; return (normaliseBody rg) } + +-- | if the graph being analyzed is open at the exit, I don't +-- quite understand the implications of possible other exits +analyzeAndRewriteBwd' + :: forall n f e x. Edges n + => BwdPass n f + -> ZGraph n e x -> Fact x f + -> FuelMonad (ZGraph n e x, FactBase f, MaybeO e f) +analyzeAndRewriteBwd' pass g f = + do (rg, fout) <- arbGraph pass g f + let (g', fb) = normalizeGraph g rg + return (g', fb, distinguishedEntryFact g' fout) + +distinguishedEntryFact :: forall n e x f . ZGraph n e x -> Fact e f -> MaybeO e f +distinguishedEntryFact g f = maybe g + where maybe :: ZGraph n e x -> MaybeO e f + maybe GNil = JustO f + maybe (GUnit {}) = JustO f + maybe (GMany e _ _) = case e of NothingO -> NothingO + JustO _ -> JustO f + +----------------------------------------------------------------------------- +-- fixpoint: finding fixed points +----------------------------------------------------------------------------- + +data TxFactBase n f + = TxFB { tfb_fbase :: FactBase f + , tfb_rg :: RG n f C C -- Transformed blocks + , tfb_cha :: ChangeFlag + , tfb_lbls :: LabelSet } + -- Note [TxFactBase change flag] + -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + -- Set the tfb_cha flag iff + -- (a) the fact in tfb_fbase for or a block L changes + -- (b) L is in tfb_lbls. + -- The tfb_lbls are all Labels of the *original* + -- (not transformed) blocks + +updateFact :: DataflowLattice f -> LabelSet -> (Label, f) + -> (ChangeFlag, FactBase f) + -> (ChangeFlag, FactBase f) +-- See Note [TxFactBase change flag] +updateFact lat lbls (lbl, new_fact) (cha, fbase) + | NoChange <- cha2 = (cha, fbase) + | lbl `elemLabelSet` lbls = (SomeChange, new_fbase) + | otherwise = (cha, new_fbase) + where + (cha2, res_fact) -- Note [Unreachable blocks] + = case lookupFact fbase lbl of + Nothing -> (SomeChange, snd $ join $ fact_bot lat) -- Note [Unreachable blocks] + Just old_fact -> join old_fact + where join old_fact = fact_extend lat lbl (OldFact old_fact) (NewFact new_fact) + new_fbase = extendFactBase fbase lbl res_fact + +fixpoint :: forall block n f. Edges (block n) + => Bool -- Going forwards? + -> DataflowLattice f + -> (block n C C -> FactBase f + -> FuelMonad (RG n f C C, FactBase f)) + -> FactBase f + -> [block n C C] + -> FuelMonad (RG n f C C, FactBase f) +fixpoint is_fwd lat do_block init_fbase untagged_blocks + = do { fuel <- getFuel + ; tx_fb <- loop fuel init_fbase + ; return (tfb_rg tx_fb, + tfb_fbase tx_fb `delFromFactBase` map fst blocks) } + -- The successors of the ZGraph are the the Labels for which + -- we have facts, that are *not* in the blocks of the graph + where + blocks = map tag untagged_blocks + where tag b = ((entryLabel b, b), if is_fwd then [entryLabel b] else successors b) + + tx_blocks :: [((Label, block n C C), [Label])] -- I do not understand this type + -> TxFactBase n f -> FuelMonad (TxFactBase n f) + tx_blocks [] tx_fb = return tx_fb + tx_blocks (((lbl,blk), deps):bs) tx_fb = tx_block lbl blk deps tx_fb >>= tx_blocks bs + -- "deps" == Labels the block may _depend_ upon for facts + + tx_block :: Label -> block n C C -> [Label] + -> TxFactBase n f -> FuelMonad (TxFactBase n f) + tx_block lbl blk deps tx_fb@(TxFB { tfb_fbase = fbase, tfb_lbls = lbls + , tfb_rg = blks, tfb_cha = cha }) + | is_fwd && not (lbl `elemFactBase` fbase) + = return tx_fb {tfb_lbls = lbls `unionLabelSet` mkLabelSet deps} -- Note [Unreachable blocks] + | otherwise + = do { (rg, out_facts) <- do_block blk fbase + ; let (cha',fbase') + = foldr (updateFact lat lbls) (cha,fbase) + (factBaseList out_facts) + lbls' = lbls `unionLabelSet` mkLabelSet deps + ; return (TxFB { tfb_lbls = lbls' + , tfb_rg = rg `RGCatC` blks + , tfb_fbase = fbase', tfb_cha = cha' }) } + + loop :: Fuel -> FactBase f -> FuelMonad (TxFactBase n f) + loop fuel fbase + = do { let init_tx_fb = TxFB { tfb_fbase = fbase + , tfb_cha = NoChange + , tfb_rg = RGNil + , tfb_lbls = emptyLabelSet } + ; tx_fb <- tx_blocks blocks init_tx_fb + ; case tfb_cha tx_fb of + NoChange -> return tx_fb + SomeChange -> do { setFuel fuel + ; loop fuel (tfb_fbase tx_fb) } } + +{- Note [Unreachable blocks] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A block that is not in the domain of tfb_fbase is "currently unreachable". +A currently-unreachable block is not even analyzed. Reason: consider +constant prop and this graph, with entry point L1: + L1: x:=3; goto L4 + L2: x:=4; goto L4 + L4: if x>3 goto L2 else goto L5 +Here L2 is actually unreachable, but if we process it with bottom input fact, +we'll propagate (x=4) to L4, and nuke the otherwise-good rewriting of L4. + +* If a currently-unreachable block is not analyzed, then its rewritten + graph will not be accumulated in tfb_rg. And that is good: + unreachable blocks simply do not appear in the output. + +* Note that clients must be careful to provide a fact (even if bottom) + for each entry point. Otherwise useful blocks may be garbage collected. + +* Note that updateFact must set the change-flag if a label goes from + not-in-fbase to in-fbase, even if its fact is bottom. In effect the + real fact lattice is + UNR + bottom + the points above bottom + +* Even if the fact is going from UNR to bottom, we still call the + client's fact_extend function because it might give the client + some useful debugging information. + +* All of this only applies for *forward* fixpoints. For the backward + case we must treat every block as reachable; it might finish with a + 'return', and therefore have no successors, for example. +-} + +----------------------------------------------------------------------------- +-- RG: an internal data type for graphs under construction +-- TOTALLY internal to Hoopl +----------------------------------------------------------------------------- + +-- this type exists because we have not yet found a way to write arfNode +-- to return a Graph; the invariants of ZGraph seem too strong + +data RG' block n f e x where + RGNil :: RG' block n f a a + RGUnit :: Fact e f -> block n e x -> RG' block n f e x + RGCatO :: RG' block n f e O -> RG' block n f O x -> RG' block n f e x + RGCatC :: RG' block n f e C -> RG' block n f C x -> RG' block n f e x +type RG = RG' ZBlock + +type BodyWithFacts n f = (ZBody n, FactBase f) +type GraphWithFacts n f e x = (ZGraph n e x, FactBase f) + -- A ZGraph together with the facts for that graph + -- The domains of the two maps should be identical + +normaliseBody :: Edges n => RG n f C C -> BodyWithFacts n f +normaliseBody rg = (body, fact_base) + where + (GMany _ body _, fact_base) = normCC rg + +normOO :: Edges n => RG n f O O -> GraphWithFacts n f O O +normOO RGNil = (GNil, noFacts) +normOO (RGUnit _ b) = (GUnit b, noFacts) +normOO (RGCatO g1 g2) = normOO g1 `gwfCat` normOO g2 +normOO (RGCatC g1 g2) = normOC g1 `gwfCat` normCO g2 + +normOC :: Edges n => RG n f O C -> GraphWithFacts n f O C +normOC (RGUnit _ b) = (GMany (JustO b) BodyEmpty NothingO, noFacts) +normOC (RGCatO g1 g2) = normOO g1 `gwfCat` normOC g2 +normOC (RGCatC g1 g2) = normOC g1 `gwfCat` normCC g2 + +normCO :: Edges n => RG n f C O -> GraphWithFacts n f C O +normCO (RGUnit f b) = (GMany NothingO BodyEmpty (JustO b), unitFact l f) + where + l = entryLabel b +normCO (RGCatO g1 g2) = normCO g1 `gwfCat` normOO g2 +normCO (RGCatC g1 g2) = normCC g1 `gwfCat` normCO g2 + +normCC :: Edges n => RG n f C C -> GraphWithFacts n f C C +normCC RGNil = (GMany NothingO BodyEmpty NothingO, noFacts) +normCC (RGUnit f b) = (GMany NothingO (BodyUnit b) NothingO, unitFact l f) + where + l = entryLabel b +normCC (RGCatO g1 g2) = normCO g1 `gwfCat` normOC g2 +normCC (RGCatC g1 g2) = normCC g1 `gwfCat` normCC g2 + +gwfCat :: Edges n => GraphWithFacts n f e a + -> GraphWithFacts n f a x + -> GraphWithFacts n f e x +gwfCat (g1, fb1) (g2, fb2) = (g1 `U.zSplice` g2, fb1 `unionFactBase` fb2) + +{- +bwfUnion :: BodyWithFacts n f -> BodyWithFacts n f -> BodyWithFacts n f +bwfUnion (bg1, fb1) (bg2, fb2) = (bg1 `BodyCat` bg2, fb1 `unionFactBase` fb2) +-} diff --git a/Compiler/Hoopl/ZipDataflowNoRG.hs b/Compiler/Hoopl/ZipDataflowNoRG.hs new file mode 100644 --- /dev/null +++ b/Compiler/Hoopl/ZipDataflowNoRG.hs @@ -0,0 +1,556 @@ +{-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs, EmptyDataDecls, PatternGuards, TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} -- bug in GHC + +{- Notes about the genesis of Hoopl7 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Hoopl7 has the following major chages + +a) GMany has symmetric entry and exit +b) GMany closed-entry does not record a BlockId +c) GMany open-exit does not record a BlockId +d) The body of a GMany is called Body +e) A Body is just a list of blocks, not a map. I've argued + elsewhere that this is consistent with (c) + +A consequence is that Graph is no longer an instance of Edges, +but nevertheless I managed to keep the ARF and ARB signatures +nice and uniform. + +This was made possible by + +* FwdTransfer looks like this: + type FwdTransfer n f + = forall e x. n e x -> Fact e f -> Fact x f + type family Fact x f :: * + type instance Fact C f = FactBase f + type instance Fact O f = f + + Note that the incoming fact is a Fact (not just 'f' as in Hoopl5,6). + It's up to the *transfer function* to look up the appropriate fact + in the FactBase for a closed-entry node. Example: + constProp (Label l) fb = lookupFact fb l + That is how Hoopl can avoid having to know the block-id for the + first node: it defers to the client. + + [Side note: that means the client must know about + bottom, in case the looupFact returns Nothing] + +* Note also that FwdTransfer *returns* a Fact too; + that is, the types in both directions are symmetrical. + Previously we returned a [(BlockId,f)] but I could not see + how to make everything line up if we do this. + + Indeed, the main shortcoming of Hoopl7 is that we are more + or less forced into this uniform representation of the facts + flowing into or out of a closed node/block/graph, whereas + previously we had more flexibility. + + In exchange the code is neater, with fewer distinct types. + And morally a FactBase is equivalent to [(BlockId,f)] and + nearly equivalent to (BlockId -> f). + +* I've realised that forwardBlockList and backwardBlockList + both need (Edges n), and that goes everywhere. + +* I renamed BlockId to Label +-} + +module Compiler.Hoopl.ZipDataflowNoRG + ( FwdPass(..), FwdTransfer, FwdRewrite, FwdRes(..) + , BwdPass(..), BwdTransfer, BwdRewrite, BwdRes(..) + , analyzeAndRewriteFwd, analyzeAndRewriteBwd + , analyzeAndRewriteFwd', analyzeAndRewriteBwd' + ) +where + +import Compiler.Hoopl.Dataflow + ( DataflowLattice(..), OldFact(..), NewFact(..) + , ChangeFlag(..) + , Fact + ) +import Compiler.Hoopl.Fuel +import Compiler.Hoopl.Graph +import qualified Compiler.Hoopl.GraphUtil as U +import Compiler.Hoopl.Label +import Compiler.Hoopl.Util +import Compiler.Hoopl.Zipper + +type AGraph n e x = FuelMonad (ZGraph n e x) +graphOfAGraph :: AGraph n e x -> FuelMonad (ZGraph n e x) +graphOfAGraph = id + +----------------------------------------------------------------------------- +-- Analyze and rewrite forward: the interface +----------------------------------------------------------------------------- + +data FwdPass n f + = FwdPass { fp_lattice :: DataflowLattice f + , fp_transfer :: FwdTransfer n f + , fp_rewrite :: FwdRewrite n f } + +type FwdTransfer n f + = forall e x. n e x -> Fact e f -> Fact x f + +type FwdRewrite n f + = forall e x. n e x -> Fact e f -> Maybe (FwdRes n f e x) +data FwdRes n f e x = FwdRes (AGraph n e x) (FwdRewrite n f) + -- result of a rewrite is a new graph and a (possibly) new rewrite function + +analyzeAndRewriteFwd + :: forall n f. Edges n + => FwdPass n f + -> ZBody n -> FactBase f + -> FuelMonad (ZBody n, FactBase f) + +analyzeAndRewriteFwd pass body facts + = do { (rg, _) <- arfBody pass body facts + ; return (normaliseBody rg) } + +-- | if the graph being analyzed is open at the entry, there must +-- be no other entry point, or all goes horribly wrong... +analyzeAndRewriteFwd' + :: forall n f e x. Edges n + => FwdPass n f + -> ZGraph n e x -> Fact e f + -> FuelMonad (ZGraph n e x, FactBase f, MaybeO x f) +analyzeAndRewriteFwd' pass g f = + do (rg, fout) <- arfGraph pass g f + let (g', fb) = normalizeGraph rg + return (g', fb, distinguishedExitFact g' fout) + +distinguishedExitFact :: forall n e x f . ZGraph n e x -> Fact x f -> MaybeO x f +distinguishedExitFact g f = maybe g + where maybe :: ZGraph n e x -> MaybeO x f + maybe GNil = JustO f + maybe (GUnit {}) = JustO f + maybe (GMany _ _ x) = case x of NothingO -> NothingO + JustO _ -> JustO f + +---------------------------------------------------------------- +-- Forward Implementation +---------------------------------------------------------------- + + +type ARF' n f thing e x + = FwdPass n f -> thing e x -> Fact e f -> FuelMonad (RG f n e x, Fact x f) + +type ARF thing n = forall f e x . ARF' n f thing e x + + +arfNode :: Edges n + => (n e x -> ZBlock n e x) + -> ARF' n f n e x +arfNode bunit pass node f + = do { mb_g <- withFuel (fp_rewrite pass node f) + ; case mb_g of + Nothing -> return (rgunit f (bunit node), + fp_transfer pass node f) + Just (FwdRes ag rw) -> do { g <- graphOfAGraph ag + ; let pass' = pass { fp_rewrite = rw } + ; arfGraph pass' g f } } + +-- type demonstration +_arfBlock :: Edges n => ARF' n f (ZBlock n) e x +_arfBlock = arfBlock +_arfGraph :: Edges n => ARF' n f (ZGraph n) e x +_arfGraph = arfGraph + + +arfMiddle :: Edges n => ARF' n f n O O +arfMiddle = arfNode ZMiddle + + +arfBlock :: Edges n => ARF (ZBlock n) n +-- Lift from nodes to blocks +arfBlock pass (ZFirst node) = arfNode ZFirst pass node +arfBlock pass (ZMiddle node) = arfNode ZMiddle pass node +arfBlock pass (ZLast node) = arfNode ZLast pass node +arfBlock pass (ZCat b1 b2) = arfCat arfBlock arfBlock pass b1 b2 +arfBlock pass (ZHead h n) = arfCat arfBlock arfMiddle pass h n +arfBlock pass (ZTail n t) = arfCat arfMiddle arfBlock pass n t +arfBlock pass (ZClosed h t) = arfCat arfBlock arfBlock pass h t + +arfCat :: Edges n => ARF' n f thing1 e O -> ARF' n f thing2 O x + -> FwdPass n f -> thing1 e O -> thing2 O x + -> Fact e f -> FuelMonad (RG f n e x, Fact x f) +arfCat arf1 arf2 pass thing1 thing2 f = do { (g1,f1) <- arf1 pass thing1 f + ; (g2,f2) <- arf2 pass thing2 f1 + ; return (g1 `rgCat` g2, f2) } +arfBody :: Edges n + + => FwdPass n f -> ZBody n -> FactBase f + -> FuelMonad (RG f n C C, FactBase f) + -- Outgoing factbase is restricted to Labels *not* in + -- in the Body; the facts for Labels *in* + -- the Body are in the BodyWithFacts +arfBody pass blocks init_fbase + = fixpoint True (fp_lattice pass) (arfBlock pass) init_fbase $ + forwardBlockList (factBaseLabels init_fbase) blocks + +arfGraph :: Edges n => ARF (ZGraph n) n +-- Lift from blocks to graphs +arfGraph _ GNil f = return (rgnil, f) +arfGraph pass (GUnit blk) f = arfBlock pass blk f +arfGraph pass (GMany NothingO body NothingO) f + = do { (body', fb) <- arfBody pass body f + ; return (body', fb) } +arfGraph pass (GMany NothingO body (JustO exit)) f + = do { (body', fb) <- arfBody pass body f + ; (exit', fx) <- arfBlock pass exit fb + ; return (body' `rgCat` exit', fx) } +arfGraph pass (GMany (JustO entry) body NothingO) f + = do { (entry', fe) <- arfBlock pass entry f + ; (body', fb) <- arfBody pass body fe + ; return (entry' `rgCat` body', fb) } +arfGraph pass (GMany (JustO entry) body (JustO exit)) f + = do { (entry', fe) <- arfBlock pass entry f + ; (body', fb) <- arfBody pass body fe + ; (exit', fx) <- arfBlock pass exit fb + ; return (entry' `rgCat` body' `rgCat` exit', fx) } + +forwardBlockList :: (Edges n, LabelsPtr entry) + => entry -> ZBody n -> [ZBlock n C C] +-- This produces a list of blocks in order suitable for forward analysis, +-- along with the list of Labels it may depend on for facts. +forwardBlockList entries blks = postorder_dfs_from (bodyMap blks) entries + +----------------------------------------------------------------------------- +-- Backward analysis and rewriting: the interface +----------------------------------------------------------------------------- + +data BwdPass n f + = BwdPass { bp_lattice :: DataflowLattice f + , bp_transfer :: BwdTransfer n f + , bp_rewrite :: BwdRewrite n f } + +type BwdTransfer n f + = forall e x. n e x -> Fact x f -> Fact e f +type BwdRewrite n f + = forall e x. n e x -> Fact x f -> Maybe (BwdRes n f e x) +data BwdRes n f e x = BwdRes (AGraph n e x) (BwdRewrite n f) + +----------------------------------------------------------------------------- +-- Backward implementation +----------------------------------------------------------------------------- + +type ARB' n f thing e x + = BwdPass n f -> thing e x -> Fact x f -> FuelMonad (RG f n e x, Fact e f) + +type ARB thing n = forall f e x. ARB' n f thing e x + +arbNode :: Edges n + => (n e x -> ZBlock n e x) + -> ARB' n f n e x +-- Lifts (BwdTransfer,BwdRewrite) to ARB_Node; +-- this time we do rewriting as well. +-- The ARB_Graph parameters specifies what to do with the rewritten graph +arbNode bunit pass node f + = do { mb_g <- withFuel (bp_rewrite pass node f) + ; case mb_g of + Nothing -> return (rgunit entry_f (bunit node), entry_f) + where + entry_f = bp_transfer pass node f + Just (BwdRes ag rw) -> do { g <- graphOfAGraph ag + ; let pass' = pass { bp_rewrite = rw } + ; arbGraph pass' g f} } + +arbMiddle :: Edges n => ARB' n f n O O +arbMiddle = arbNode ZMiddle + +arbBlock :: Edges n => ARB (ZBlock n) n +-- Lift from nodes to blocks +arbBlock pass (ZFirst node) = arbNode ZFirst pass node +arbBlock pass (ZMiddle node) = arbNode ZMiddle pass node +arbBlock pass (ZLast node) = arbNode ZLast pass node +arbBlock pass (ZCat b1 b2) = arbCat arbBlock arbBlock pass b1 b2 +arbBlock pass (ZHead h n) = arbCat arbBlock arbMiddle pass h n +arbBlock pass (ZTail n t) = arbCat arbMiddle arbBlock pass n t +arbBlock pass (ZClosed h t) = arbCat arbBlock arbBlock pass h t + +arbCat :: Edges n => ARB' n f thing1 e O -> ARB' n f thing2 O x + -> BwdPass n f -> thing1 e O -> thing2 O x + -> Fact x f -> FuelMonad (RG f n e x, Fact e f) +arbCat arb1 arb2 pass thing1 thing2 f = do { (g2,f2) <- arb2 pass thing2 f + ; (g1,f1) <- arb1 pass thing1 f2 + ; return (g1 `rgCat` g2, f1) } + +arbBody :: Edges n + => BwdPass n f -> ZBody n -> FactBase f + -> FuelMonad (RG f n C C, FactBase f) +arbBody pass blocks init_fbase + = fixpoint False (bp_lattice pass) (arbBlock pass) init_fbase $ + backwardBlockList blocks + +arbGraph :: Edges n => ARB (ZGraph n) n +arbGraph _ GNil f = return (rgnil, f) +arbGraph pass (GUnit blk) f = arbBlock pass blk f +arbGraph pass (GMany NothingO body NothingO) f + = do { (body', fb) <- arbBody pass body f + ; return (body', fb) } +arbGraph pass (GMany NothingO body (JustO exit)) f + = do { (exit', fx) <- arbBlock pass exit f + ; (body', fb) <- arbBody pass body fx + ; return (body' `rgCat` exit', fb) } +arbGraph pass (GMany (JustO entry) body NothingO) f + = do { (body', fb) <- arbBody pass body f + ; (entry', fe) <- arbBlock pass entry fb + ; return (entry' `rgCat` body', fe) } +arbGraph pass (GMany (JustO entry) body (JustO exit)) f + = do { (exit', fx) <- arbBlock pass exit f + ; (body', fb) <- arbBody pass body fx + ; (entry', fe) <- arbBlock pass entry fb + ; return (entry' `rgCat` body' `rgCat` exit', fe) } + +backwardBlockList :: Edges n => ZBody n -> [ZBlock n C C] +-- This produces a list of blocks in order suitable for backward analysis, +-- along with the list of Labels it may depend on for facts. +backwardBlockList body = reachable ++ missing + where reachable = reverse $ forwardBlockList entries body + entries = externalEntryLabels body + all = bodyList body + missingLabels = + mkLabelSet (map fst all) `minusLabelSet` + mkLabelSet (map entryLabel reachable) + missing = map snd $ filter (flip elemLabelSet missingLabels . fst) all + +{- + +The forward and backward dataflow analyses now use postorder depth-first +order for faster convergence. + +The forward and backward cases are not dual. In the forward case, the +entry points are known, and one simply traverses the body blocks from +those points. In the backward case, something is known about the exit +points, but this information is essentially useless, because we don't +actually have a dual graph (that is, one with edges reversed) to +compute with. (Even if we did have a dual graph, it would not avail +us---a backward analysis must include reachable blocks that don't +reach the exit, as in a procedure that loops forever and has side +effects.) + +Since in the general case, no information is available about entry +points, I have put in a horrible hack. First, I assume that every +label defined but not used is an entry point. Then, because an entry +point might also be a loop header, I add, in arbitrary order, all the +remaining "missing" blocks. Needless to say, I am not pleased. +I am not satisfied. I am not Senator Morgan. + +Wait! I believe that the Right Thing here is to require that anyone +wishing to analyze a graph closed at the entry provide a way of +determining the entry points, if any, of that graph. This requirement +can apply equally to forward and backward analyses; I believe that +using the input FactBase to determine the entry points of a closed +graph is *also* a hack. + +NR + +-} + + +analyzeAndRewriteBwd + :: forall n f. Edges n + => BwdPass n f + -> ZBody n -> FactBase f + -> FuelMonad (ZBody n, FactBase f) + +analyzeAndRewriteBwd pass body facts + = do { (rg, _) <- arbBody pass body facts + ; return (normaliseBody rg) } + +-- | if the graph being analyzed is open at the exit, I don't +-- quite understand the implications of possible other exits +analyzeAndRewriteBwd' + :: forall n f e x. Edges n + => BwdPass n f + -> ZGraph n e x -> Fact x f + -> FuelMonad (ZGraph n e x, FactBase f, MaybeO e f) +analyzeAndRewriteBwd' pass g f = + do (rg, fout) <- arbGraph pass g f + let (g', fb) = normalizeGraph rg + return (g', fb, distinguishedEntryFact g' fout) + +distinguishedEntryFact :: forall n e x f . ZGraph n e x -> Fact e f -> MaybeO e f +distinguishedEntryFact g f = maybe g + where maybe :: ZGraph n e x -> MaybeO e f + maybe GNil = JustO f + maybe (GUnit {}) = JustO f + maybe (GMany e _ _) = case e of NothingO -> NothingO + JustO _ -> JustO f + +----------------------------------------------------------------------------- +-- fixpoint: finding fixed points +----------------------------------------------------------------------------- + +data TxFactBase n f + = TxFB { tfb_fbase :: FactBase f + , tfb_rg :: RG f n C C -- Transformed blocks + , tfb_cha :: ChangeFlag + , tfb_lbls :: LabelSet } + -- Note [TxFactBase change flag] + -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + -- Set the tfb_cha flag iff + -- (a) the fact in tfb_fbase for or a block L changes + -- (b) L is in tfb_lbls. + -- The tfb_lbls are all Labels of the *original* + -- (not transformed) blocks + +updateFact :: DataflowLattice f -> LabelSet -> (Label, f) + -> (ChangeFlag, FactBase f) + -> (ChangeFlag, FactBase f) +-- See Note [TxFactBase change flag] +updateFact lat lbls (lbl, new_fact) (cha, fbase) + | NoChange <- cha2 = (cha, fbase) + | lbl `elemLabelSet` lbls = (SomeChange, new_fbase) + | otherwise = (cha, new_fbase) + where + (cha2, res_fact) -- Note [Unreachable blocks] + = case lookupFact fbase lbl of + Nothing -> (SomeChange, snd $ join $ fact_bot lat) -- Note [Unreachable blocks] + Just old_fact -> join old_fact + where join old_fact = fact_extend lat lbl (OldFact old_fact) (NewFact new_fact) + new_fbase = extendFactBase fbase lbl res_fact + +fixpoint :: forall block n f. Edges (block n) + => Bool -- Going forwards? + -> DataflowLattice f + -> (block n C C -> FactBase f + -> FuelMonad (RG f n C C, FactBase f)) + -> FactBase f + -> [block n C C] + -> FuelMonad (RG f n C C, FactBase f) +fixpoint is_fwd lat do_block init_fbase untagged_blocks + = do { fuel <- getFuel + ; tx_fb <- loop fuel init_fbase + ; return (tfb_rg tx_fb, + tfb_fbase tx_fb `delFromFactBase` map fst blocks) } + -- The successors of the ZGraph are the the Labels for which + -- we have facts, that are *not* in the blocks of the graph + where + blocks = map tag untagged_blocks + where tag b = ((entryLabel b, b), if is_fwd then [entryLabel b] else successors b) + + tx_blocks :: [((Label, block n C C), [Label])] -- I do not understand this type + -> TxFactBase n f -> FuelMonad (TxFactBase n f) + tx_blocks [] tx_fb = return tx_fb + tx_blocks (((lbl,blk), deps):bs) tx_fb = tx_block lbl blk deps tx_fb >>= tx_blocks bs + -- "deps" == Labels the block may _depend_ upon for facts + + tx_block :: Label -> block n C C -> [Label] + -> TxFactBase n f -> FuelMonad (TxFactBase n f) + tx_block lbl blk deps tx_fb@(TxFB { tfb_fbase = fbase, tfb_lbls = lbls + , tfb_rg = blks, tfb_cha = cha }) + | is_fwd && not (lbl `elemFactBase` fbase) + = return tx_fb {tfb_lbls = lbls `unionLabelSet` mkLabelSet deps} -- Note [Unreachable blocks] + | otherwise + = do { (rg, out_facts) <- do_block blk fbase + ; let (cha',fbase') + = foldr (updateFact lat lbls) (cha,fbase) + (factBaseList out_facts) + lbls' = lbls `unionLabelSet` mkLabelSet deps + ; return (TxFB { tfb_lbls = lbls' + , tfb_rg = rg `rgCat` blks + , tfb_fbase = fbase', tfb_cha = cha' }) } + + loop :: Fuel -> FactBase f -> FuelMonad (TxFactBase n f) + loop fuel fbase + = do { let init_tx_fb = TxFB { tfb_fbase = fbase + , tfb_cha = NoChange + , tfb_rg = rgnilC + , tfb_lbls = emptyLabelSet } + ; tx_fb <- tx_blocks blocks init_tx_fb + ; case tfb_cha tx_fb of + NoChange -> return tx_fb + SomeChange -> do { setFuel fuel + ; loop fuel (tfb_fbase tx_fb) } } + +{- Note [Unreachable blocks] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A block that is not in the domain of tfb_fbase is "currently unreachable". +A currently-unreachable block is not even analyzed. Reason: consider +constant prop and this graph, with entry point L1: + L1: x:=3; goto L4 + L2: x:=4; goto L4 + L4: if x>3 goto L2 else goto L5 +Here L2 is actually unreachable, but if we process it with bottom input fact, +we'll propagate (x=4) to L4, and nuke the otherwise-good rewriting of L4. + +* If a currently-unreachable block is not analyzed, then its rewritten + graph will not be accumulated in tfb_rg. And that is good: + unreachable blocks simply do not appear in the output. + +* Note that clients must be careful to provide a fact (even if bottom) + for each entry point. Otherwise useful blocks may be garbage collected. + +* Note that updateFact must set the change-flag if a label goes from + not-in-fbase to in-fbase, even if its fact is bottom. In effect the + real fact lattice is + UNR + bottom + the points above bottom + +* Even if the fact is going from UNR to bottom, we still call the + client's fact_extend function because it might give the client + some useful debugging information. + +* All of this only applies for *forward* fixpoints. For the backward + case we must treat every block as reachable; it might finish with a + 'return', and therefore have no successors, for example. +-} + +----------------------------------------------------------------------------- +-- RG: an internal data type for graphs under construction +-- TOTALLY internal to Hoopl; each block carries its fact +----------------------------------------------------------------------------- + +type RG f n e x = Graph' (FZBlock f) n e x +data FZBlock f n e x = FZBlock (Fact e f) (ZBlock n e x) + +--- constructors + +rgnil :: RG f n O O +rgnilC :: RG f n C C +rgunit :: Fact e f -> ZBlock n e x -> RG f n e x +rgCat :: RG f n e a -> RG f n a x -> RG f n e x + +---- observers + +type BodyWithFacts n f = (ZBody n, FactBase f) +type GraphWithFacts n f e x = (ZGraph n e x, FactBase f) + -- A ZGraph together with the facts for that graph + -- The domains of the two maps should be identical + +normalizeGraph :: forall n f e x . + Edges n => RG f n e x -> GraphWithFacts n f e x +normaliseBody :: Edges n => RG f n C C -> BodyWithFacts n f + +normalizeGraph g = (graphMapBlocks dropFact g, facts g) + where dropFact (FZBlock _ b) = b + facts :: RG f n e x -> FactBase f + facts GNil = noFacts + facts (GUnit _) = noFacts + facts (GMany _ body exit) = bodyFacts body `unionFactBase` exitFacts exit + exitFacts :: MaybeO x (FZBlock f n C O) -> FactBase f + exitFacts NothingO = noFacts + exitFacts (JustO (FZBlock f b)) = unitFact (entryLabel b) f + bodyFacts :: Body' (FZBlock f) n -> FactBase f + bodyFacts (BodyUnit (FZBlock f b)) = unitFact (entryLabel b) f + bodyFacts (b1 `BodyCat` b2) = bodyFacts b1 `unionFactBase` bodyFacts b2 + +normaliseBody rg = (body, fact_base) + where (GMany _ body _, fact_base) = normalizeGraph rg + +--- implementation of the constructors (boring) + +rgnil = GNil +rgnilC = GMany NothingO BodyEmpty NothingO + +rgunit f b@(ZFirst {}) = gUnitCO (FZBlock f b) +rgunit f b@(ZMiddle {}) = gUnitOO (FZBlock f b) +rgunit f b@(ZLast {}) = gUnitOC (FZBlock f b) +rgunit f b@(ZCat {}) = gUnitOO (FZBlock f b) +rgunit f b@(ZHead {}) = gUnitCO (FZBlock f b) +rgunit f b@(ZTail {}) = gUnitOC (FZBlock f b) +rgunit f b@(ZClosed {}) = gUnitCC (FZBlock f b) + +rgCat = U.splice fzCat + where fzCat (FZBlock f b1) (FZBlock _ b2) = FZBlock f (b1 `U.zCat` b2) diff --git a/Compiler/Hoopl/Zipper.hs b/Compiler/Hoopl/Zipper.hs new file mode 100644 --- /dev/null +++ b/Compiler/Hoopl/Zipper.hs @@ -0,0 +1,90 @@ +{-# LANGUAGE GADTs #-} + +module Compiler.Hoopl.Zipper + ( ZBlock(..), ZGraph, ZBody + , frontBiasBlock, backBiasBlock + ) +where + +import Compiler.Hoopl.Graph + +data ZBlock n e x where + -- nodes + ZFirst :: n C O -> ZBlock n C O + ZMiddle :: n O O -> ZBlock n O O + ZLast :: n O C -> ZBlock n O C + + -- concatenation operations + ZCat :: ZBlock n O O -> ZBlock n O O -> ZBlock n O O -- non-list-like + ZHead :: ZBlock n C O -> n O O -> ZBlock n C O + ZTail :: n O O -> ZBlock n O C -> ZBlock n O C + + ZClosed :: ZBlock n C O -> ZBlock n O C -> ZBlock n C C -- the zipper + +type ZGraph = Graph' ZBlock +type ZBody = Body' ZBlock + +instance Edges n => Edges (ZBlock n) where + entryLabel (ZFirst n) = entryLabel n + entryLabel (ZHead h _) = entryLabel h + entryLabel (ZClosed h _) = entryLabel h + successors (ZLast n) = successors n + successors (ZTail _ t) = successors t + successors (ZClosed _ t) = successors t + + +---------------------------------------------------------------- + +-- | A block is "front biased" if the left child of every +-- concatenation operation is a node, not a general block; a +-- front-biased block is analogous to an ordinary list. If a block is +-- front-biased, then its nodes can be traversed from front to back +-- without general recusion; tail recursion suffices. Not all shapes +-- can be front-biased; a closed/open block is inherently back-biased. + +frontBiasBlock :: ZBlock n e x -> ZBlock n e x +frontBiasBlock b@(ZFirst {}) = b +frontBiasBlock b@(ZMiddle {}) = b +frontBiasBlock b@(ZLast {}) = b +frontBiasBlock b@(ZCat {}) = rotate b + where -- rotate and append ensure every left child of ZCat is ZMiddle + -- provided 2nd argument to append already has this property + rotate :: ZBlock n O O -> ZBlock n O O + append :: ZBlock n O O -> ZBlock n O O -> ZBlock n O O + rotate (ZCat h t) = append h (rotate t) + rotate b@(ZMiddle {}) = b + append b@(ZMiddle {}) t = b `ZCat` t + append (ZCat b1 b2) b3 = b1 `append` (b2 `append` b3) +frontBiasBlock b@(ZHead {}) = b -- back-biased by nature; cannot fix +frontBiasBlock b@(ZTail {}) = b -- statically front-biased +frontBiasBlock (ZClosed h t) = shiftRight h t + where shiftRight :: ZBlock n C O -> ZBlock n O C -> ZBlock n C C + shiftRight (ZHead b1 b2) b3 = shiftRight b1 (ZTail b2 b3) + shiftRight b1@(ZFirst {}) b2 = ZClosed b1 b2 + +-- | A block is "back biased" if the right child of every +-- concatenation operation is a node, not a general block; a +-- back-biased block is analogous to a snoc-list. If a block is +-- back-biased, then its nodes can be traversed from back to back +-- without general recusion; tail recursion suffices. Not all shapes +-- can be back-biased; an open/closed block is inherently front-biased. + +backBiasBlock :: ZBlock n e x -> ZBlock n e x +backBiasBlock b@(ZFirst {}) = b +backBiasBlock b@(ZMiddle {}) = b +backBiasBlock b@(ZLast {}) = b +backBiasBlock b@(ZCat {}) = rotate b + where -- rotate and append ensure every right child of ZCat is ZMiddle + -- provided 1st argument to append already has this property + rotate :: ZBlock n O O -> ZBlock n O O + append :: ZBlock n O O -> ZBlock n O O -> ZBlock n O O + rotate (ZCat h t) = append (rotate h) t + rotate b@(ZMiddle {}) = b + append h b@(ZMiddle {}) = h `ZCat` b + append b1 (ZCat b2 b3) = (b1 `append` b2) `append` b3 +backBiasBlock b@(ZHead {}) = b -- statically back-biased +backBiasBlock b@(ZTail {}) = b -- front-biased by nature; cannot fix +backBiasBlock (ZClosed h t) = shiftLeft h t + where shiftLeft :: ZBlock n C O -> ZBlock n O C -> ZBlock n C C + shiftLeft b1 (ZTail b2 b3) = shiftLeft (ZHead b1 b2) b3 + shiftLeft b1 b2@(ZLast {}) = ZClosed b1 b2 diff --git a/README b/README --- a/README +++ b/README @@ -23,4 +23,13 @@ git clone -o tufts git://ghc.cs.tufts.edu/hoopl/hoopl.git If you are not familiar with git, we recommend the tutorial 'Git Magic' -by Ben Lynn. +by Ben Lynn. To get some ideas about how to use git effectively, + + http://whygitisbetterthanx.com/ + +is also useful. + +If you've been given an account at Tufts with write privileges to the +git repository, you'll want to use a different URL: + + git clone -o tufts linux.cs.tufts.edu:/r/ghc/www/hoopl/hoopl.git diff --git a/hoopl.cabal b/hoopl.cabal --- a/hoopl.cabal +++ b/hoopl.cabal @@ -1,5 +1,5 @@ Name: hoopl -Version: 3.7.8.0 +Version: 3.7.12.1 Description: Higher-order optimization library License: BSD3 License-file: LICENSE @@ -15,14 +15,20 @@ Library Build-Depends: base >= 3 && < 5, containers - Exposed-modules: Compiler.Hoopl + Exposed-modules: Compiler.Hoopl, + Compiler.Hoopl.Zipper, + Compiler.Hoopl.ZipDataflowNoRG Other-modules: Compiler.Hoopl.GraphUtil, -- GraphUtil should *never* be seen by clients. -- The remaining modules are hidden *provisionally* - Compiler.Hoopl.Dataflow, Compiler.Hoopl.Graph, + Compiler.Hoopl.Combinators, + Compiler.Hoopl.Dataflow, + Compiler.Hoopl.Debug, + Compiler.Hoopl.Graph, Compiler.Hoopl.MkGraph, Compiler.Hoopl.Fuel, Compiler.Hoopl.Label, - Compiler.Hoopl.Util + Compiler.Hoopl.Show, Compiler.Hoopl.Util + Compiler.Hoopl.ZipDataflow ghc-options: -Wall -fno-warn-name-shadowing diff --git a/hoopl.pdf b/hoopl.pdf Binary files a/hoopl.pdf and b/hoopl.pdf differ