src/Compiler/Hoopl/DataflowNest.hs

   1 {-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs, EmptyDataDecls, PatternGuards, TypeFamilies, MultiParamTypeClasses #-}
   2 {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} -- bug in GHC
   3
   4 {- Notes about the genesis of Hoopl7
   5 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   6 Hoopl7 has the following major chages
   7
   8 a) GMany has symmetric entry and exit
   9 b) GMany closed-entry does not record a BlockId
  10 c) GMany open-exit does not record a BlockId
  11 d) The body of a GMany is called Body
  12 e) A Body is just a list of blocks, not a map. I've argued
  13    elsewhere that this is consistent with (c)
  14
  15 A consequence is that Graph is no longer an instance of Edges,
  16 but nevertheless I managed to keep the ARF and ARB signatures
  17 nice and uniform.
  18
  19 This was made possible by
  20
  21 * FwdTransfer looks like this:
  22     type FwdTransfer n f
  23       = forall e x. n e x -> Fact e f -> Fact x f
  24     type family   Fact x f :: *
  25     type instance Fact C f = FactBase f
  26     type instance Fact O f = f
  27
  28   Note that the incoming fact is a Fact (not just 'f' as in Hoopl5,6).
  29   It's up to the *transfer function* to look up the appropriate fact
  30   in the FactBase for a closed-entry node.  Example:
  31         constProp (Label l) fb = lookupFact fb l
  32   That is how Hoopl can avoid having to know the block-id for the
  33   first node: it defers to the client.
  34
  35   [Side note: that means the client must know about
  36   bottom, in case the looupFact returns Nothing]
  37
  38 * Note also that FwdTransfer *returns* a Fact too;
  39   that is, the types in both directions are symmetrical.
  40   Previously we returned a [(BlockId,f)] but I could not see
  41   how to make everything line up if we do this.
  42
  43   Indeed, the main shortcoming of Hoopl7 is that we are more
  44   or less forced into this uniform representation of the facts
  45   flowing into or out of a closed node/block/graph, whereas
  46   previously we had more flexibility.
  47
  48   In exchange the code is neater, with fewer distinct types.
  49   And morally a FactBase is equivalent to [(BlockId,f)] and
  50   nearly equivalent to (BlockId -> f).
  51
  52 * I've realised that forwardBlockList and backwardBlockList
  53   both need (Edges n), and that goes everywhere.
  54
  55 * I renamed BlockId to Label
  56 -}
  57
  58 module Compiler.Hoopl.DataflowNest
  59   ( DataflowLattice(..), JoinFun, OldFact(..), NewFact(..), Fact
  60   , ChangeFlag(..), changeIf
  61   , FwdPass(..), FwdTransfer, mkFTransfer, mkFTransfer', getFTransfers
  62   , FwdRes(..),  FwdRewrite,  mkFRewrite,  mkFRewrite',  getFRewrites
  63   , BwdPass(..), BwdTransfer, mkBTransfer, mkBTransfer', getBTransfers
  64   , BwdRes(..),  BwdRewrite,  mkBRewrite,  mkBRewrite',  getBRewrites
  65   , analyzeAndRewriteFwd,  analyzeAndRewriteBwd
  66   )
  67 where
  68
  69 import Data.Maybe
  70
  71 import Compiler.Hoopl.Fuel
  72 import Compiler.Hoopl.Graph
  73 import Compiler.Hoopl.MkGraph
  74 import qualified Compiler.Hoopl.GraphUtil as U
  75 import Compiler.Hoopl.Label
  76 import Compiler.Hoopl.Util
  77
  78 -----------------------------------------------------------------------------
  79 --              DataflowLattice
  80 -----------------------------------------------------------------------------
  81
  82 data DataflowLattice a = DataflowLattice
  83  { fact_name       :: String          -- Documentation
  84  , fact_bot        :: a               -- Lattice bottom element
  85  , fact_extend     :: JoinFun a       -- Lattice join plus change flag
  86                                       -- (changes iff result > old fact)
  87  , fact_do_logging :: Bool            -- log changes
  88  }
  89 -- ^ A transfer function might want to use the logging flag
  90 -- to control debugging, as in for example, it updates just one element
  91 -- in a big finite map.  We don't want Hoopl to show the whole fact,
  92 -- and only the transfer function knows exactly what changed.
  93
  94 type JoinFun a = Label -> OldFact a -> NewFact a -> (ChangeFlag, a)
  95   -- the label argument is for debugging purposes only
  96 newtype OldFact a = OldFact a
  97 newtype NewFact a = NewFact a
  98
  99 data ChangeFlag = NoChange | SomeChange deriving (Eq, Ord)
 100 changeIf :: Bool -> ChangeFlag
 101 changeIf changed = if changed then SomeChange else NoChange
 102
 103
 104 -----------------------------------------------------------------------------
 105 --              Analyze and rewrite forward: the interface
 106 -----------------------------------------------------------------------------
 107
 108 data FwdPass n f
 109   = FwdPass { fp_lattice  :: DataflowLattice f
 110             , fp_transfer :: FwdTransfer n f
 111             , fp_rewrite  :: FwdRewrite n f }
 112
 113 newtype FwdTransfer n f
 114   = FwdTransfers { getFTransfers ::
 115                      ( n C O -> f -> f
 116                      , n O O -> f -> f
 117                      , n O C -> f -> FactBase f
 118                      ) }
 119
 120 newtype FwdRewrite n f
 121   = FwdRewrites { getFRewrites ::
 122                     ( n C O -> f -> Maybe (FwdRes n f C O)
 123                     , n O O -> f -> Maybe (FwdRes n f O O)
 124                     , n O C -> f -> Maybe (FwdRes n f O C)
 125                     ) }
 126 data FwdRes n f e x = FwdRes (AGraph n e x) (FwdRewrite n f)
 127   -- result of a rewrite is a new graph and a (possibly) new rewrite function
 128
 129 mkFTransfer :: (n C O -> f -> f)
 130             -> (n O O -> f -> f)
 131             -> (n O C -> f -> FactBase f)
 132             -> FwdTransfer n f
 133 mkFTransfer f m l = FwdTransfers (f, m, l)
 134
 135 mkFTransfer' :: (forall e x . n e x -> f -> Fact x f) -> FwdTransfer n f
 136 mkFTransfer' f = FwdTransfers (f, f, f)
 137
 138 mkFRewrite :: (n C O -> f -> Maybe (FwdRes n f C O))
 139            -> (n O O -> f -> Maybe (FwdRes n f O O))
 140            -> (n O C -> f -> Maybe (FwdRes n f O C))
 141            -> FwdRewrite n f
 142 mkFRewrite f m l = FwdRewrites (f, m, l)
 143
 144 mkFRewrite' :: (forall e x . n e x -> f -> Maybe (FwdRes n f e x)) -> FwdRewrite n f
 145 mkFRewrite' f = FwdRewrites (f, f, f)
 146
 147
 148 type family   Fact x f :: *
 149 type instance Fact C f = FactBase f
 150 type instance Fact O f = f
 151
 152 -- | if the graph being analyzed is open at the entry, there must
 153 --   be no other entry point, or all goes horribly wrong...
 154 analyzeAndRewriteFwd
 155    :: forall n f e x entries. (Edges n, LabelsPtr entries)
 156    => FwdPass n f
 157    -> entries
 158    -> Graph n e x -> Fact e f
 159    -> FuelMonad (Graph n e x, FactBase f, MaybeO x f)
 160 analyzeAndRewriteFwd pass entries g f =
 161   do (rg, fout) <- arfGraph pass (targetLabels entries) g f
 162      let (g', fb) = normalizeGraph rg
 163      return (g', fb, distinguishedExitFact g' fout)
 164
 165 distinguishedExitFact :: forall n e x f . Graph n e x -> Fact x f -> MaybeO x f
 166 distinguishedExitFact g f = maybe g
 167     where maybe :: Graph n e x -> MaybeO x f
 168           maybe GNil       = JustO f
 169           maybe (GUnit {}) = JustO f
 170           maybe (GMany _ _ x) = case x of NothingO -> NothingO
 171                                           JustO _  -> JustO f
 172
 173 ----------------------------------------------------------------
 174 --       Forward Implementation
 175 ----------------------------------------------------------------
 176
 177 type FM = FuelMonad
 178
 179 type Entries = [Label]
 180
 181 arfGraph :: forall n f e x .
 182             (Edges n) => FwdPass n f ->
 183             Entries -> Graph n e x -> Fact e f -> FM (RG f n e x, Fact x f)
 184 arfGraph pass entries = graph
 185   where
 186     {- nested type synonyms would be so lovely here
 187     type ARF  thing = forall e x . thing e x -> f        -> FM (RG f n e x, Fact x f)
 188     type ARFX thing = forall e x . thing e x -> Fact e f -> FM (RG f n e x, Fact x f)
 189     -}
 190     graph :: forall e x . Graph n e x -> Fact e f -> FM (RG f n e x, Fact x f)
 191     block :: forall e x . Block n e x -> f        -> FM (RG f n e x, Fact x f)
 192     node  :: forall e x . (ShapeLifter e x)
 193                        => n e x       -> f        -> FM (RG f n e x, Fact x f)
 194     body  :: Entries -> Body n -> Fact C f -> FuelMonad (RG f n C C, Fact C f)
 195                     -- Outgoing factbase is restricted to Labels *not* in
 196                     -- in the Body; the facts for Labels *in*
 197                     -- the Body are in the 'RG f n C C'
 198     cat :: forall e a x info info' info''.
 199            (info  -> FuelMonad (RG f n e a, info'))
 200         -> (info' -> FuelMonad (RG f n a x, info''))
 201         -> (info  -> FuelMonad (RG f n e x, info''))
 202
 203     graph GNil                              = \f -> return (rgnil, f)
 204     graph (GUnit blk)                       = block blk
 205     graph (GMany NothingO bdy NothingO)     = body entries bdy
 206     graph (GMany NothingO bdy (JustO exit)) = body entries bdy `cat` arfx block exit
 207     graph (GMany (JustO entry) bdy NothingO)
 208       = block entry `cat` body (successors entry) bdy
 209     graph (GMany (JustO entry) bdy (JustO exit))
 210       = (block entry `cat` body (successors entry) bdy) `cat` arfx block exit
 211
 212     -- Lift from nodes to blocks
 213     block (BFirst  n)  = node n
 214     block (BMiddle n)  = node n
 215     block (BLast   n)  = node n
 216     block (BCat b1 b2) = block b1 `cat` block b2
 217     block (BHead h n)  = block h  `cat` node n
 218     block (BTail n t)  = node  n  `cat` block t
 219     block (BClosed h t)= block h  `cat` block t
 220
 221     node thenode f
 222       = do { mb_g <- withFuel (frewrite pass thenode f)
 223            ; case mb_g of
 224                Nothing -> return (rgunit f (unit thenode),
 225                                   ftransfer pass thenode f)
 226                Just (FwdRes ag rw) ->
 227                    do { g <- graphOfAGraph ag
 228                       ; let pass' = pass { fp_rewrite = rw }
 229                       ; arfGraph pass' (entry thenode) g (elift thenode f) } }
 230
 231     -- | Compose fact transformers and concatenate the resulting
 232     -- rewritten graphs.
 233     {-# INLINE cat #-}
 234     cat ft1 ft2 f = do { (g1,f1) <- ft1 f
 235                        ; (g2,f2) <- ft2 f1
 236                        ; return (g1 `rgCat` g2, f2) }
 237
 238     arfx :: forall thing x .
 239             Edges thing
 240          => (thing C x ->        f -> FM (RG f n C x, Fact x f))
 241          -> (thing C x -> Fact C f -> FM (RG f n C x, Fact x f))
 242     arfx arf thing fb =
 243       arf thing $ fromJust $ lookupFact (joinInFacts lattice fb) $ entryLabel thing
 244      where lattice = fp_lattice pass
 245      -- joinInFacts adds debugging information
 246
 247
 248                     -- Outgoing factbase is restricted to Labels *not* in
 249                     -- in the Body; the facts for Labels *in*
 250                     -- the Body are in the 'RG f n C C'
 251     body entries blocks init_fbase
 252       = fixpoint True (fp_lattice pass) do_block init_fbase $
 253         forwardBlockList entries blocks
 254       where
 255         do_block b f = do (g, fb) <- block b $ lookupF pass (entryLabel b) f
 256                           return (g, factBaseList fb)
 257
 258
 259
 260 -- Join all the incoming facts with bottom.
 261 -- We know the results _shouldn't change_, but the transfer
 262 -- functions might, for example, generate some debugging traces.
 263 joinInFacts :: DataflowLattice f -> FactBase f -> FactBase f
 264 joinInFacts (DataflowLattice {fact_bot = bot, fact_extend = fe}) fb =
 265   mkFactBase $ map botJoin $ factBaseList fb
 266     where botJoin (l, f) = (l, snd $ fe l (OldFact bot) (NewFact f))
 267
 268 forwardBlockList :: (Edges n, LabelsPtr entry)
 269                  => entry -> Body n -> [Block n C C]
 270 -- This produces a list of blocks in order suitable for forward analysis,
 271 -- along with the list of Labels it may depend on for facts.
 272 forwardBlockList entries blks = postorder_dfs_from (bodyMap blks) entries
 273
 274 -----------------------------------------------------------------------------
 275 --              Backward analysis and rewriting: the interface
 276 -----------------------------------------------------------------------------
 277
 278 data BwdPass n f
 279   = BwdPass { bp_lattice  :: DataflowLattice f
 280             , bp_transfer :: BwdTransfer n f
 281             , bp_rewrite  :: BwdRewrite n f }
 282
 283 newtype BwdTransfer n f
 284   = BwdTransfers { getBTransfers ::
 285                      ( n C O -> f          -> f
 286                      , n O O -> f          -> f
 287                      , n O C -> FactBase f -> f
 288                      ) }
 289 newtype BwdRewrite n f
 290   = BwdRewrites { getBRewrites ::
 291                     ( n C O -> f          -> Maybe (BwdRes n f C O)
 292                     , n O O -> f          -> Maybe (BwdRes n f O O)
 293                     , n O C -> FactBase f -> Maybe (BwdRes n f O C)
 294                     ) }
 295 data BwdRes n f e x = BwdRes (AGraph n e x) (BwdRewrite n f)
 296
 297 mkBTransfer :: (n C O -> f -> f) -> (n O O -> f -> f) ->
 298                (n O C -> FactBase f -> f) -> BwdTransfer n f
 299 mkBTransfer f m l = BwdTransfers (f, m, l)
 300
 301 mkBTransfer' :: (forall e x . n e x -> Fact x f -> f) -> BwdTransfer n f
 302 mkBTransfer' f = BwdTransfers (f, f, f)
 303
 304 mkBRewrite :: (n C O -> f          -> Maybe (BwdRes n f C O))
 305            -> (n O O -> f          -> Maybe (BwdRes n f O O))
 306            -> (n O C -> FactBase f -> Maybe (BwdRes n f O C))
 307            -> BwdRewrite n f
 308 mkBRewrite f m l = BwdRewrites (f, m, l)
 309
 310 mkBRewrite' :: (forall e x . n e x -> Fact x f -> Maybe (BwdRes n f e x)) -> BwdRewrite n f
 311 mkBRewrite' f = BwdRewrites (f, f, f)
 312
 313
 314 -----------------------------------------------------------------------------
 315 --              Backward implementation
 316 -----------------------------------------------------------------------------
 317
 318 arbGraph :: forall n f e x .
 319             (Edges n) => BwdPass n f ->
 320             Entries -> Graph n e x -> Fact x f -> FM (RG f n e x, Fact e f)
 321 arbGraph pass entries = graph
 322   where
 323     {- nested type synonyms would be so lovely here
 324     type ARB  thing = forall e x . thing e x -> Fact x f -> FM (RG f n e x, f)
 325     type ARBX thing = forall e x . thing e x -> Fact x f -> FM (RG f n e x, Fact e f)
 326     -}
 327     graph :: forall e x . Graph n e x -> Fact x f -> FM (RG f n e x, Fact e f)
 328     block :: forall e x . Block n e x -> Fact x f -> FM (RG f n e x, f)
 329     node  :: forall e x . (ShapeLifter e x)
 330                        => n e x       -> Fact x f -> FM (RG f n e x, f)
 331     body  :: Entries -> Body n -> Fact C f -> FuelMonad (RG f n C C, Fact C f)
 332     cat :: forall e a x info info' info''.
 333            (info' -> FuelMonad (RG f n e a, info''))
 334         -> (info  -> FuelMonad (RG f n a x, info'))
 335         -> (info  -> FuelMonad (RG f n e x, info''))
 336
 337     graph GNil                              = \f -> return (rgnil, f)
 338     graph (GUnit blk)                       = block blk
 339     graph (GMany NothingO bdy NothingO)     = body entries bdy
 340     graph (GMany NothingO bdy (JustO exit)) = body entries bdy `cat` arbx block exit
 341     graph (GMany (JustO entry) bdy NothingO)
 342       = block entry `cat` body (successors entry) bdy
 343     graph (GMany (JustO entry) bdy (JustO exit))
 344       = (block entry `cat` body (successors entry) bdy) `cat` arbx block exit
 345
 346     -- Lift from nodes to blocks
 347     block (BFirst  n)  = node n
 348     block (BMiddle n)  = node n
 349     block (BLast   n)  = node n
 350     block (BCat b1 b2) = block b1 `cat` block b2
 351     block (BHead h n)  = block h  `cat` node n
 352     block (BTail n t)  = node  n  `cat` block t
 353     block (BClosed h t)= block h  `cat` block t
 354
 355     node thenode f
 356       = do { mb_g <- withFuel (brewrite pass thenode f)
 357            ; case mb_g of
 358                Nothing -> return (rgunit entry_f (unit thenode), entry_f)
 359                    where entry_f  = btransfer pass thenode f
 360                Just (BwdRes ag rw) ->
 361                           do { g <- graphOfAGraph ag
 362                              ; let pass' = pass { bp_rewrite = rw }
 363                              ; (g, f) <- arbGraph pass' (entry thenode) g f
 364                              ; return (g, elower (bp_lattice pass) thenode f)} }
 365
 366     -- | Compose fact transformers and concatenate the resulting
 367     -- rewritten graphs.
 368     {-# INLINE cat #-}
 369     cat ft1 ft2 f = do { (g2,f2) <- ft2 f
 370                        ; (g1,f1) <- ft1 f2
 371                        ; return (g1 `rgCat` g2, f1) }
 372
 373     arbx :: forall thing x .
 374             Edges thing
 375          => (thing C x -> Fact x f -> FM (RG f n C x, f))
 376          -> (thing C x -> Fact x f -> FM (RG f n C x, Fact C f))
 377
 378     arbx arb thing f = do { (rg, f) <- arb thing f
 379                           ; let fb = joinInFacts (bp_lattice pass) $
 380                                      mkFactBase [(entryLabel thing, f)]
 381                           ; return (rg, fb) }
 382      -- joinInFacts adds debugging information
 383
 384                     -- Outgoing factbase is restricted to Labels *not* in
 385                     -- in the Body; the facts for Labels *in*
 386                     -- the Body are in the 'RG f n C C'
 387     body entries blocks init_fbase
 388       = fixpoint False (bp_lattice pass) do_block init_fbase $
 389         backwardBlockList entries blocks
 390       where
 391         do_block b f = do (g, f) <- block b f
 392                           return (g, [(entryLabel b, f)])
 393
 394 {-
 395
 396
 397
 398
 399 type ARB' n f thing e x
 400   = BwdPass n f -> thing e x -> Fact x f -> FuelMonad (RG f n e x, f)
 401
 402 type ARBX' n f thing e x
 403   = BwdPass n f -> thing e x -> Fact x f -> FuelMonad (RG f n e x, Fact e f)
 404
 405 type ARB  thing n = forall f e x. ARB'  n f thing e x
 406 type ARBX thing n = forall f e x. ARBX' n f thing e x
 407
 408 arbx :: Edges thing => ARB' n f thing C x -> ARBX' n f thing C x
 409 arbx arb pass thing f = do { (rg, f) <- arb pass thing f
 410                            ; let fb = joinInFacts (bp_lattice pass) $
 411                                       mkFactBase [(entryLabel thing, f)]
 412                            ; return (rg, fb) }
 413
 414 arbNode :: (Edges n, ShapeLifter e x) => ARB' n f n e x
 415 -- Lifts (BwdTransfer,BwdRewrite) to ARB_Node;
 416 -- this time we do rewriting as well.
 417 -- The ARB_Graph parameters specifies what to do with the rewritten graph
 418 arbNode pass node f
 419   = do { mb_g <- withFuel (brewrite pass node f)
 420        ; case mb_g of
 421            Nothing -> return (rgunit entry_f (unit node), entry_f)
 422                     where entry_f  = btransfer pass node f
 423            Just (BwdRes ag rw) -> do { g <- graphOfAGraph ag
 424                                      ; let pass' = pass { bp_rewrite = rw }
 425                                      ; (g, f) <- arbGraph pass' g f
 426                                      ; return (g, elower (bp_lattice pass) node f)} }
 427
 428 arbBlock :: Edges n => ARB (Block n) n
 429 -- Lift from nodes to blocks
 430 arbBlock pass (BFirst  node)  = arbNode pass node
 431 arbBlock pass (BMiddle node)  = arbNode pass node
 432 arbBlock pass (BLast   node)  = arbNode pass node
 433 arbBlock pass (BCat b1 b2)    = arbCat arbBlock arbBlock pass b1 b2
 434 arbBlock pass (BHead h n)     = arbCat arbBlock arbNode  pass h n
 435 arbBlock pass (BTail n t)     = arbCat arbNode  arbBlock pass n t
 436 arbBlock pass (BClosed h t)   = arbCat arbBlock arbBlock pass h t
 437
 438 arbCat :: (pass -> thing1 -> info1 -> FuelMonad (RG f n e a, info1'))
 439        -> (pass -> thing2 -> info2 -> FuelMonad (RG f n a x, info1))
 440        -> (pass -> thing1 -> thing2 -> info2 -> FuelMonad (RG f n e x, info1'))
 441 {-# INLINE arbCat #-}
 442 arbCat arb1 arb2 pass thing1 thing2 f = do { (g2,f2) <- arb2 pass thing2 f
 443                                            ; (g1,f1) <- arb1 pass thing1 f2
 444                                            ; return (g1 `rgCat` g2, f1) }
 445
 446 arbBody :: Edges n
 447         => BwdPass n f -> Body n -> FactBase f
 448         -> FuelMonad (RG f n C C, FactBase f)
 449 arbBody pass blocks init_fbase
 450   = fixpoint False (bp_lattice pass) do_block init_fbase $
 451     backwardBlockList blocks
 452   where
 453     do_block b f = do (g, f) <- arbBlock pass b f
 454                       return (g, [(entryLabel b, f)])
 455
 456 arbGraph :: Edges n => ARBX (Graph n) n
 457 arbGraph _    GNil        = \f -> return (rgnil, f)
 458 arbGraph pass (GUnit blk) = arbBlock pass blk
 459 arbGraph pass (GMany NothingO body NothingO) = arbBody pass body
 460 arbGraph pass (GMany NothingO body (JustO exit)) =
 461   arbCat arbBody (arbx arbBlock) pass body exit
 462 arbGraph pass (GMany (JustO entry) body NothingO) =
 463   arbCat arbBlock arbBody pass entry body
 464 arbGraph pass (GMany (JustO entry) body (JustO exit)) =
 465   arbCat arbeb (arbx arbBlock) pass (entry, body) exit
 466  where arbeb pass = uncurry $ arbCat arbBlock arbBody pass
 467
 468 -}
 469
 470 backwardBlockList :: (LabelsPtr entries, Edges n) => entries -> Body n -> [Block n C C]
 471 -- This produces a list of blocks in order suitable for backward analysis,
 472 -- along with the list of Labels it may depend on for facts.
 473 backwardBlockList entries body = reverse $ forwardBlockList entries body
 474
 475 {-
 476
 477 The forward and backward cases are not dual.  In the forward case, the
 478 entry points are known, and one simply traverses the body blocks from
 479 those points.  In the backward case, something is known about the exit
 480 points, but this information is essentially useless, because we don't
 481 actually have a dual graph (that is, one with edges reversed) to
 482 compute with.  (Even if we did have a dual graph, it would not avail
 483 us---a backward analysis must include reachable blocks that don't
 484 reach the exit, as in a procedure that loops forever and has side
 485 effects.)
 486
 487 -}
 488
 489
 490 -- | if the graph being analyzed is open at the exit, I don't
 491 --   quite understand the implications of possible other exits
 492 analyzeAndRewriteBwd
 493    :: (Edges n, LabelsPtr entries)
 494    => BwdPass n f
 495    -> entries -> Graph n e x -> Fact x f
 496    -> FuelMonad (Graph n e x, FactBase f, MaybeO e f)
 497 analyzeAndRewriteBwd pass entries g f =
 498   do (rg, fout) <- arbGraph pass (targetLabels entries) g f
 499      let (g', fb) = normalizeGraph rg
 500      return (g', fb, distinguishedEntryFact g' fout)
 501
 502 distinguishedEntryFact :: forall n e x f . Graph n e x -> Fact e f -> MaybeO e f
 503 distinguishedEntryFact g f = maybe g
 504     where maybe :: Graph n e x -> MaybeO e f
 505           maybe GNil       = JustO f
 506           maybe (GUnit {}) = JustO f
 507           maybe (GMany e _ _) = case e of NothingO -> NothingO
 508                                           JustO _  -> JustO f
 509
 510 -----------------------------------------------------------------------------
 511 --      fixpoint: finding fixed points
 512 -----------------------------------------------------------------------------
 513
 514 data TxFactBase n f
 515   = TxFB { tfb_fbase :: FactBase f
 516          , tfb_rg  :: RG f n C C -- Transformed blocks
 517          , tfb_cha   :: ChangeFlag
 518          , tfb_lbls  :: LabelSet }
 519  -- Note [TxFactBase change flag]
 520  -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 521  -- Set the tfb_cha flag iff
 522  --   (a) the fact in tfb_fbase for or a block L changes
 523  --   (b) L is in tfb_lbls.
 524  -- The tfb_lbls are all Labels of the *original*
 525  -- (not transformed) blocks
 526
 527 updateFact :: DataflowLattice f -> LabelSet -> (Label, f)
 528            -> (ChangeFlag, FactBase f)
 529            -> (ChangeFlag, FactBase f)
 530 -- See Note [TxFactBase change flag]
 531 updateFact lat lbls (lbl, new_fact) (cha, fbase)
 532   | NoChange <- cha2        = (cha,        fbase)
 533   | lbl `elemLabelSet` lbls = (SomeChange, new_fbase)
 534   | otherwise               = (cha,        new_fbase)
 535   where
 536     (cha2, res_fact) -- Note [Unreachable blocks]
 537        = case lookupFact fbase lbl of
 538            Nothing -> (SomeChange, snd $ join $ fact_bot lat)  -- Note [Unreachable blocks]
 539            Just old_fact -> join old_fact
 540          where join old_fact = fact_extend lat lbl (OldFact old_fact) (NewFact new_fact)
 541     new_fbase = extendFactBase fbase lbl res_fact
 542
 543 fixpoint :: forall block n f. Edges (block n)
 544          => Bool        -- Going forwards?
 545          -> DataflowLattice f
 546          -> (block n C C -> FactBase f
 547               -> FuelMonad (RG f n C C, [(Label, f)]))
 548          -> FactBase f
 549          -> [block n C C]
 550          -> FuelMonad (RG f n C C, FactBase f)
 551 fixpoint is_fwd lat do_block init_fbase untagged_blocks
 552   = do { fuel <- getFuel
 553        ; tx_fb <- loop fuel init_fbase
 554        ; return (tfb_rg tx_fb,
 555                  tfb_fbase tx_fb `delFromFactBase` map fst blocks) }
 556              -- The successors of the Graph are the the Labels for which
 557              -- we have facts, that are *not* in the blocks of the graph
 558   where
 559     blocks = map tag untagged_blocks
 560      where tag b = ((entryLabel b, b), if is_fwd then [entryLabel b] else successors b)
 561
 562     tx_blocks :: [((Label, block n C C), [Label])]   -- I do not understand this type
 563               -> TxFactBase n f -> FuelMonad (TxFactBase n f)
 564     tx_blocks []              tx_fb = return tx_fb
 565     tx_blocks (((lbl,blk), deps):bs) tx_fb = tx_block lbl blk deps tx_fb >>= tx_blocks bs
 566      -- "deps" == Labels the block may _depend_ upon for facts
 567
 568     tx_block :: Label -> block n C C -> [Label]
 569              -> TxFactBase n f -> FuelMonad (TxFactBase n f)
 570     tx_block lbl blk deps tx_fb@(TxFB { tfb_fbase = fbase, tfb_lbls = lbls
 571                                       , tfb_rg = blks, tfb_cha = cha })
 572       | is_fwd && not (lbl `elemFactBase` fbase)
 573       = return tx_fb {tfb_lbls = lbls `unionLabelSet` mkLabelSet deps}  -- Note [Unreachable blocks]
 574       | otherwise
 575       = do { (rg, out_facts) <- do_block blk fbase
 576            ; let (cha',fbase')
 577                    = foldr (updateFact lat lbls) (cha,fbase) out_facts
 578                  lbls' = lbls `unionLabelSet` mkLabelSet deps
 579            ; return (TxFB { tfb_lbls  = lbls'
 580                           , tfb_rg    = rg `rgCat` blks
 581                           , tfb_fbase = fbase', tfb_cha = cha' }) }
 582
 583     loop :: Fuel -> FactBase f -> FuelMonad (TxFactBase n f)
 584     loop fuel fbase
 585       = do { let init_tx_fb = TxFB { tfb_fbase = fbase
 586                                    , tfb_cha   = NoChange
 587                                    , tfb_rg    = rgnilC
 588                                    , tfb_lbls  = emptyLabelSet }
 589            ; tx_fb <- tx_blocks blocks init_tx_fb
 590            ; case tfb_cha tx_fb of
 591                NoChange   -> return tx_fb
 592                SomeChange -> do { setFuel fuel
 593                                 ; loop fuel (tfb_fbase tx_fb) } }
 594
 595 {- Note [Unreachable blocks]
 596 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 597 A block that is not in the domain of tfb_fbase is "currently unreachable".
 598 A currently-unreachable block is not even analyzed.  Reason: consider
 599 constant prop and this graph, with entry point L1:
 600   L1: x:=3; goto L4
 601   L2: x:=4; goto L4
 602   L4: if x>3 goto L2 else goto L5
 603 Here L2 is actually unreachable, but if we process it with bottom input fact,
 604 we'll propagate (x=4) to L4, and nuke the otherwise-good rewriting of L4.
 605
 606 * If a currently-unreachable block is not analyzed, then its rewritten
 607   graph will not be accumulated in tfb_rg.  And that is good:
 608   unreachable blocks simply do not appear in the output.
 609
 610 * Note that clients must be careful to provide a fact (even if bottom)
 611   for each entry point. Otherwise useful blocks may be garbage collected.
 612
 613 * Note that updateFact must set the change-flag if a label goes from
 614   not-in-fbase to in-fbase, even if its fact is bottom.  In effect the
 615   real fact lattice is
 616        UNR
 617        bottom
 618        the points above bottom
 619
 620 * Even if the fact is going from UNR to bottom, we still call the
 621   client's fact_extend function because it might give the client
 622   some useful debugging information.
 623
 624 * All of this only applies for *forward* fixpoints.  For the backward
 625   case we must treat every block as reachable; it might finish with a
 626   'return', and therefore have no successors, for example.
 627 -}
 628
 629 -----------------------------------------------------------------------------
 630 --      RG: an internal data type for graphs under construction
 631 --          TOTALLY internal to Hoopl; each block carries its fact
 632 -----------------------------------------------------------------------------
 633
 634 type RG      f n e x = Graph' (FBlock f) n e x
 635 data FBlock f n e x = FBlock f (Block n e x)
 636
 637 --- constructors
 638
 639 rgnil  :: RG f n O O
 640 rgnilC :: RG f n C C
 641 rgunit :: f -> Block n e x -> RG f n e x
 642 rgCat  :: RG f n e a -> RG f n a x -> RG f n e x
 643
 644 ---- observers
 645
 646 type GraphWithFacts n f e x = (Graph n e x, FactBase f)
 647   -- A Graph together with the facts for that graph
 648   -- The domains of the two maps should be identical
 649
 650 normalizeGraph :: forall n f e x .
 651                   Edges n => RG f n e x -> GraphWithFacts n f e x
 652
 653 normalizeGraph g = (graphMapBlocks dropFact g, facts g)
 654     where dropFact (FBlock _ b) = b
 655           facts :: RG f n e x -> FactBase f
 656           facts GNil = noFacts
 657           facts (GUnit _) = noFacts
 658           facts (GMany _ body exit) = bodyFacts body `unionFactBase` exitFacts exit
 659           exitFacts :: MaybeO x (FBlock f n C O) -> FactBase f
 660           exitFacts NothingO = noFacts
 661           exitFacts (JustO (FBlock f b)) = mkFactBase [(entryLabel b, f)]
 662           bodyFacts :: Body' (FBlock f) n -> FactBase f
 663           bodyFacts (BodyUnit (FBlock f b)) = mkFactBase [(entryLabel b, f)]
 664           bodyFacts (b1 `BodyCat` b2) = bodyFacts b1 `unionFactBase` bodyFacts b2
 665
 666 --- implementation of the constructors (boring)
 667
 668 rgnil  = GNil
 669 rgnilC = GMany NothingO BodyEmpty NothingO
 670
 671 rgunit f b@(BFirst  {}) = gUnitCO (FBlock f b)
 672 rgunit f b@(BMiddle {}) = gUnitOO (FBlock f b)
 673 rgunit f b@(BLast   {}) = gUnitOC (FBlock f b)
 674 rgunit f b@(BCat {})    = gUnitOO (FBlock f b)
 675 rgunit f b@(BHead {})   = gUnitCO (FBlock f b)
 676 rgunit f b@(BTail {})   = gUnitOC (FBlock f b)
 677 rgunit f b@(BClosed {}) = gUnitCC (FBlock f b)
 678
 679 rgCat = U.splice fzCat
 680   where fzCat (FBlock f b1) (FBlock _ b2) = FBlock f (b1 `U.cat` b2)
 681
 682 ----------------------------------------------------------------
 683 --       Utilities
 684 ----------------------------------------------------------------
 685
 686 -- Lifting based on shape:
 687 --  - from nodes to blocks
 688 --  - from facts to fact-like things
 689 -- Lowering back:
 690 --  - from fact-like things to facts
 691 -- Note that the latter two functions depend only on the entry shape.
 692 class ShapeLifter e x where
 693   unit      :: n e x -> Block n e x
 694   elift     :: Edges n =>                      n e x -> f -> Fact e f
 695   elower    :: Edges n => DataflowLattice f -> n e x -> Fact e f -> f
 696   ftransfer :: FwdPass n f -> n e x -> f        -> Fact x f
 697   btransfer :: BwdPass n f -> n e x -> Fact x f -> f
 698   frewrite  :: FwdPass n f -> n e x -> f        -> Maybe (FwdRes n f e x)
 699   brewrite  :: BwdPass n f -> n e x -> Fact x f -> Maybe (BwdRes n f e x)
 700   entry     :: Edges n => n e x -> [Label]
 701
 702 instance ShapeLifter C O where
 703   unit            = BFirst
 704   elift      n f  = mkFactBase [(entryLabel n, f)]
 705   elower lat n fb = getFact lat (entryLabel n) fb
 706   ftransfer (FwdPass {fp_transfer = FwdTransfers (ft, _, _)}) n f = ft n f
 707   btransfer (BwdPass {bp_transfer = BwdTransfers (bt, _, _)}) n f = bt n f
 708   frewrite  (FwdPass {fp_rewrite  = FwdRewrites  (fr, _, _)}) n f = fr n f
 709   brewrite  (BwdPass {bp_rewrite  = BwdRewrites  (br, _, _)}) n f = br n f
 710   entry n = [entryLabel n]
 711
 712 instance ShapeLifter O O where
 713   unit         = BMiddle
 714   elift    _ f = f
 715   elower _ _ f = f
 716   ftransfer (FwdPass {fp_transfer = FwdTransfers (_, ft, _)}) n f = ft n f
 717   btransfer (BwdPass {bp_transfer = BwdTransfers (_, bt, _)}) n f = bt n f
 718   frewrite  (FwdPass {fp_rewrite  = FwdRewrites  (_, fr, _)}) n f = fr n f
 719   brewrite  (BwdPass {bp_rewrite  = BwdRewrites  (_, br, _)}) n f = br n f
 720   entry _ = []
 721
 722 instance ShapeLifter O C where
 723   unit         = BLast
 724   elift    _ f = f
 725   elower _ _ f = f
 726   ftransfer (FwdPass {fp_transfer = FwdTransfers (_, _, ft)}) n f = ft n f
 727   btransfer (BwdPass {bp_transfer = BwdTransfers (_, _, bt)}) n f = bt n f
 728   frewrite  (FwdPass {fp_rewrite  = FwdRewrites  (_, _, fr)}) n f = fr n f
 729   brewrite  (BwdPass {bp_rewrite  = BwdRewrites  (_, _, br)}) n f = br n f
 730   entry _ = []
 731
 732 -- Fact lookup: the fact `orelse` bottom
 733 lookupF :: FwdPass n f -> Label -> FactBase f -> f
 734 lookupF = getFact . fp_lattice
 735
 736 getFact  :: DataflowLattice f -> Label -> FactBase f -> f
 737 getFact lat l fb = case lookupFact fb l of Just  f -> f
 738                                            Nothing -> fact_bot lat