compiler/cmm/ZipDataflow.hs

   1 {-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables #-}
   2 {-# OPTIONS -fno-allow-overlapping-instances -fglasgow-exts #-}
   3 -- -fglagow-exts for kind signatures
   4
   5 module ZipDataflow
   6     ( zdfSolveFrom, zdfRewriteFrom
   7     , ForwardTransfers(..), BackwardTransfers(..)
   8     , ForwardRewrites(..),  BackwardRewrites(..)
   9     , ForwardFixedPoint, BackwardFixedPoint
  10     , zdfFpFacts
  11     , zdfFpOutputFact
  12     , zdfGraphChanged
  13     , zdfDecoratedGraph -- not yet implemented
  14     , zdfFpContents
  15     , zdfFpLastOuts
  16     )
  17 where
  18
  19 import CmmTx
  20 import DFMonad
  21 import MkZipCfg
  22 import ZipCfg
  23 import qualified ZipCfg as G
  24
  25 import Maybes
  26 import Outputable
  27 import Panic
  28 import UniqFM
  29 import UniqSupply
  30
  31 import Control.Monad
  32 import Maybe
  33
  34 {-
  35
  36 This module implements two useful tools:
  37
  38   1. An iterative solver for dataflow problems
  39
  40   2. The combined dataflow-analysis-and-transformation framework
  41      described by Lerner, Grove, and Chambers in their excellent
  42      2002 POPL paper (http://tinyurl.com/3zycbr or
  43      http://tinyurl.com/3pnscd).
  44
  45 Each tool comes in two flavors: one for forward dataflow problems
  46 and one for backward dataflow problems.
  47
  48 We quote the paper above:
  49
  50   Dataflow analyses can have mutually beneficial interactions.
  51   Previous efforts to exploit these interactions have either
  52   (1) iteratively performed each individual analysis until no
  53   further improvements are discovered or (2) developed "super-
  54   analyses" that manually combine conceptually separate anal-
  55   yses. We have devised a new approach that allows anal-
  56   yses to be defined independently while still enabling them
  57   to be combined automatically and profitably. Our approach
  58   avoids the loss of precision associated with iterating indi-
  59   vidual analyses and the implementation difficulties of man-
  60   ually writing a super-analysis.
  61
  62 The key idea is to provide at each CFG node not only a dataflow
  63 transfer function but also a rewriting function that has the option to
  64 replace the node with a new (possibly empty) graph.  The rewriting
  65 function takes a dataflow fact as input, and the fact is used to
  66 justify any rewriting.  For example, in a backward problem, the fact
  67 that variable x is dead can be used to justify rewriting node
  68   x := e
  69 to the empty graph.  In a forward problem, the fact that x == 7 can
  70 be used to justify rewriting node
  71   y := x + 1
  72 to
  73   y := 8
  74 which in turn will be analyzed and produce a new fact:
  75 x == 7 and y == 8.
  76
  77 In its most general form, this module takes as input graph, transfer
  78 equations, rewrites, and an initial set of dataflow facts, and
  79 iteratively computes a new graph and a new set of dataflow facts such
  80 that
  81   * The set of facts is a fixed point of the transfer equations
  82   * The graph has been rewritten as much as is consistent with
  83     the given facts and requested rewriting depth (see below)
  84 N.B. 'A set of facts' is shorthand for 'A finite map from CFG label to fact'.
  85
  86 The types of transfer equations, rewrites, and fixed points are
  87 different for forward and backward problems.  To avoid cluttering the
  88 name space with two versions of every names, other names such as
  89 zdfSolveFrom are overloaded to work in both forward or backward
  90 directions.  This design decision is based on experience with the
  91 predecessor module, now called ZipDataflow0 and destined for the bit bucket.
  92
  93
  94 This module is deliberately very abstract.  It is a completely general
  95 framework and well-nigh impossible to understand in isolation.  The
  96 cautious reader will begin with some concrete examples in the form of
  97 clients.  NR recommends
  98
  99   CmmLiveZ             A simple liveness analysis
 100
 101   CmmSpillReload.removeDeadAssignmentsAndReloads
 102                        A piece of spaghetti to pull on, which leads to
 103                          - a two-part liveness analysis that tracks
 104                            variables live in registers and live on the stack
 105                          - elimination of assignments to dead variables
 106                          - elimination of redundant reloads
 107
 108 Even hearty souls should avoid the CmmProcPointZ client, at least for
 109 the time being.
 110
 111 -}
 112
 113
 114 {- ============ TRANSFER FUNCTIONS AND REWRITES =========== -}
 115
 116 -- | For a backward transfer, you're given the fact on a node's
 117 -- outedge and you compute the fact on the inedge.  Facts have type 'a'.
 118 -- A last node may have multiple outedges, each pointing to a labelled
 119 -- block, so instead of a fact it is given a mapping from BlockId to fact.
 120
 121 data BackwardTransfers middle last a = BackwardTransfers
 122     { bt_first_in  :: a              -> BlockId -> a
 123     , bt_middle_in :: a              -> middle  -> a
 124     , bt_last_in   :: (BlockId -> a) -> last    -> a
 125     }
 126
 127 -- | For a forward transfer, you're given the fact on a node's
 128 -- inedge and you compute the fact on the outedge. Because a last node
 129 -- may have multiple outedges, each pointing to a labelled
 130 -- block, so instead of a fact it produces a list of (BlockId, fact) pairs.
 131
 132 data ForwardTransfers middle last a = ForwardTransfers
 133     { ft_first_out  :: a -> BlockId -> a
 134     , ft_middle_out :: a -> middle  -> a
 135     , ft_last_outs  :: a -> last    -> LastOutFacts a
 136     , ft_exit_out   :: a            -> a
 137     }
 138
 139 newtype LastOutFacts a = LastOutFacts [(BlockId, a)]
 140   -- ^ These are facts flowing out of a last node to the node's successors.
 141   -- They are either to be set (if they pertain to the graph currently
 142   -- under analysis) or propagated out of a sub-analysis
 143
 144
 145 -- | A backward rewrite takes the same inputs as a backward transfer,
 146 -- but instead of producing a fact, it produces a replacement graph or Nothing.
 147 -- The type of the replacement graph is given as a type parameter 'g'
 148 -- of kind * -> * -> *.  This design offers great flexibility to clients,
 149 -- but it might be worth simplifying this module by replacing this type
 150 -- parameter with AGraph everywhere (SLPJ 19 May 2008).
 151
 152 data BackwardRewrites middle last a g = BackwardRewrites
 153     { br_first  :: a              -> BlockId -> Maybe (g middle last)
 154     , br_middle :: a              -> middle  -> Maybe (g middle last)
 155     , br_last   :: (BlockId -> a) -> last    -> Maybe (g middle last)
 156     , br_exit   ::                              Maybe (g middle last)
 157     }
 158
 159 -- | A forward rewrite takes the same inputs as a forward transfer,
 160 -- but instead of producing a fact, it produces a replacement graph or Nothing.
 161
 162 data ForwardRewrites middle last a g = ForwardRewrites
 163     { fr_first  :: a -> BlockId -> Maybe (g middle last)
 164     , fr_middle :: a -> middle  -> Maybe (g middle last)
 165     , fr_last   :: a -> last    -> Maybe (g middle last)
 166     , fr_exit   :: a            -> Maybe (g middle last)
 167     }
 168
 169 {- ===================== FIXED POINTS =================== -}
 170
 171 -- | The result of combined analysis and transformation is a
 172 -- solution to the set of dataflow equations together with a 'contained value'.
 173 -- This solution is a member of type class 'FixedPoint', which is parameterized by
 174 --   * middle and last nodes 'm' and 'l'
 175 --   * data flow fact 'fact'
 176 --   * the type 'a' of the contained value
 177 --
 178 -- In practice, the contained value 'zdfFpContents' is either a
 179 -- rewritten graph, when rewriting, or (), when solving without
 180 -- rewriting.  A function 'zdfFpMap' allows a client to change
 181 -- the contents without changing other values.
 182 --
 183 -- To save space, we provide the solution 'zdfFpFacts' as a mapping
 184 -- from BlockId to fact; if necessary, facts on edges can be
 185 -- reconstructed using the transfer functions; this functionality is
 186 -- intended to be included as the 'zdfDecoratedGraph', but the code
 187 -- has not yet been implemented.
 188 --
 189 -- The solution may also includes a fact 'zdfFpOuputFact', which is
 190 -- not associated with any label:
 191 --   * for a backward problem, this is the fact at entry
 192 --   * for a forward problem, this is the fact at the distinguished exit node,
 193 --     if such a node is present
 194 --
 195 -- For a forward problem only, the solution includes 'zdfFpLastOuts',
 196 -- which is the set of facts on edges leaving the graph.
 197 --
 198 -- The flag 'zdfGraphChanged' tells whether the engine did any rewriting.
 199
 200 class FixedPoint fp where
 201     zdfFpContents     :: fp m l fact a -> a
 202     zdfFpFacts        :: fp m l fact a -> BlockEnv fact
 203     zdfFpOutputFact   :: fp m l fact a -> fact  -- entry for backward; exit for forward
 204     zdfDecoratedGraph :: fp m l fact a -> Graph (fact, m) (fact, l)
 205     zdfGraphChanged   :: fp m l fact a -> ChangeFlag
 206     zdfFpMap          :: (a -> b) -> (fp m l fact a -> fp m l fact b)
 207
 208 -- | The class 'FixedPoint' has two instances: one for forward problems and
 209 -- one for backward problems.  The 'CommonFixedPoint' defines all fields
 210 -- common to both.  (The instance declarations are uninteresting and appear below.)
 211
 212 data CommonFixedPoint m l fact a = FP
 213     { fp_facts     :: BlockEnv fact
 214     , fp_out       :: fact  -- entry for backward; exit for forward
 215     , fp_changed   :: ChangeFlag
 216     , fp_dec_graph :: Graph (fact, m) (fact, l)
 217     , fp_contents  :: a
 218     }
 219
 220 -- | The common fixed point is sufficient for a backward problem.
 221 type BackwardFixedPoint = CommonFixedPoint
 222
 223 -- | A forward problem needs the common fields, plus the facts on the outedges.
 224 data ForwardFixedPoint m l fact a = FFP
 225     { ffp_common    :: CommonFixedPoint m l fact a
 226     , zdfFpLastOuts :: LastOutFacts fact
 227     }
 228
 229
 230 {- ============== SOLVING AND REWRITING ============== -}
 231
 232 type PassName = String
 233
 234 -- | zdfSolveFrom is an overloaded name that resolves to a pure
 235 -- analysis with no rewriting.  It has only two instances: forward and
 236 -- backward.  Since it needs no rewrites, the type parameters of the
 237 -- class are transfer functions and the fixed point.
 238 --
 239 --
 240 -- An iterative solver normally starts with the bottom fact at every
 241 -- node, but it can be useful in other contexts as well.  For this
 242 -- reason the initial set of facts (at labelled blocks only) is a
 243 -- parameter to the solver.
 244 --
 245 -- The constraints on the type signature exist purely for debugging;
 246 -- they make it possible to prettyprint nodes and facts.  The parameter of
 247 -- type 'PassName' is also used just for debugging.
 248 --
 249 -- Note that the result is a fixed point with no contents, that is,
 250 -- the contents have type ().
 251 --
 252 -- The intent of the rest of the type signature should be obvious.
 253 -- If not, place a skype call to norman-ramsey or complain bitterly
 254 -- to norman-ramsey@acm.org.
 255
 256 class DataflowSolverDirection transfers fixedpt where
 257   zdfSolveFrom   :: (DebugNodes m l, Outputable a)
 258                  => BlockEnv a        -- Initial facts (unbound == bottom)
 259                  -> PassName
 260                  -> DataflowLattice a -- Lattice
 261                  -> transfers m l a   -- Dataflow transfer functions
 262                  -> a                 -- Fact flowing in (at entry or exit)
 263                  -> Graph m l         -- Graph to be analyzed
 264                  -> fixedpt m l a ()  -- Answers
 265
 266 -- There are exactly two instances: forward and backward
 267 instance DataflowSolverDirection ForwardTransfers ForwardFixedPoint
 268   where zdfSolveFrom = solve_f
 269
 270 instance DataflowSolverDirection BackwardTransfers BackwardFixedPoint
 271   where zdfSolveFrom = solve_b
 272
 273
 274 -- | zdfRewriteFrom is an overloaded name that resolves to an
 275 -- interleaved analysis and transformation.  It too is instantiated in
 276 -- forward and backward directions.
 277 --
 278 -- The type parameters of the class include not only transfer
 279 -- functions and the fixed point but also rewrites and the type
 280 -- constructor (here called 'graph') for making rewritten graphs.  As
 281 -- above, in the definitoins of the rewrites, it might simplify
 282 -- matters if 'graph' were replaced with 'AGraph'.
 283 --
 284 -- The type signature of 'zdfRewriteFrom' is that of 'zdfSolveFrom'
 285 -- with additional parameters and a different result.  Of course the
 286 -- rewrites are an additional parameter, but there are further
 287 -- parameters which reflect the fact that rewriting consumes both
 288 -- OptimizationFuel and Uniqs.
 289 --
 290 -- The result type is changed to reflect fuel consumption, and also
 291 -- the resulting fixed point containts a rewritten graph.
 292 --
 293 -- John Dias is going to improve the management of Uniqs and Fuel so
 294 -- that it doesn't make us sick to look at the types.
 295
 296 class DataflowSolverDirection transfers fixedpt =>
 297       DataflowDirection transfers fixedpt rewrites
 298                         (graph :: * -> * -> *) where
 299   zdfRewriteFrom :: (DebugNodes m l, Outputable a)
 300                  => RewritingDepth      -- whether to rewrite a rewritten graph
 301                  -> BlockEnv a          -- initial facts (unbound == botton)
 302                  -> PassName
 303                  -> DataflowLattice a
 304                  -> transfers m l a
 305                  -> rewrites m l a graph
 306                  -> a                   -- fact flowing in (at entry or exit)
 307                  -> Graph m l
 308                  -> UniqSupply
 309                  -> FuelMonad (fixedpt m l a (Graph m l))
 310
 311 data RewritingDepth = RewriteShallow | RewriteDeep
 312 -- When a transformation proposes to rewrite a node,
 313 -- you can either ask the system to
 314 --  * "shallow": accept the new graph, analyse it without further rewriting
 315 --  * "deep": recursively analyse-and-rewrite the new graph
 316
 317
 318 -- There are currently four instances, but there could be more
 319 --      forward, backward (instantiates transfers, fixedpt, rewrites)
 320 --      Graph, AGraph     (instantiates graph)
 321
 322 instance DataflowDirection ForwardTransfers ForwardFixedPoint ForwardRewrites Graph
 323   where zdfRewriteFrom = rewrite_f_graph
 324
 325 instance DataflowDirection ForwardTransfers ForwardFixedPoint ForwardRewrites AGraph
 326   where zdfRewriteFrom = rewrite_f_agraph
 327
 328 instance DataflowDirection BackwardTransfers BackwardFixedPoint BackwardRewrites Graph
 329   where zdfRewriteFrom = rewrite_b_graph
 330
 331 instance DataflowDirection BackwardTransfers BackwardFixedPoint BackwardRewrites AGraph
 332   where zdfRewriteFrom = rewrite_b_agraph
 333
 334
 335 {- =================== IMPLEMENTATIONS ===================== -}
 336
 337
 338 -----------------------------------------------------------
 339 --      solve_f: forward, pure
 340
 341 solve_f         :: (DebugNodes m l, Outputable a)
 342                 => BlockEnv a        -- initial facts (unbound == bottom)
 343                 -> PassName
 344                 -> DataflowLattice a -- lattice
 345                 -> ForwardTransfers m l a   -- dataflow transfer functions
 346                 -> a
 347                 -> Graph m l         -- graph to be analyzed
 348                 -> ForwardFixedPoint m l a ()  -- answers
 349 solve_f env name lattice transfers in_fact g =
 350    runWithInfiniteFuel $ runDFM panic_us lattice $
 351                          fwd_pure_anal name env transfers in_fact g
 352  where panic_us = panic "pure analysis pulled on a UniqSupply"
 353
 354 rewrite_f_graph  :: (DebugNodes m l, Outputable a)
 355                  => RewritingDepth
 356                  -> BlockEnv a
 357                  -> PassName
 358                  -> DataflowLattice a
 359                  -> ForwardTransfers m l a
 360                  -> ForwardRewrites m l a Graph
 361                  -> a                 -- fact flowing in (at entry or exit)
 362                  -> Graph m l
 363                  -> UniqSupply
 364                  -> FuelMonad (ForwardFixedPoint m l a (Graph m l))
 365 rewrite_f_graph depth start_facts name lattice transfers rewrites in_fact g u =
 366     runDFM u lattice $
 367     do fuel <- fuelRemaining
 368        (fp, fuel') <- forward_rew maybeRewriteWithFuel return depth start_facts name
 369                       transfers rewrites in_fact g fuel
 370        fuelDecrement name fuel fuel'
 371        return fp
 372
 373 rewrite_f_agraph :: (DebugNodes m l, Outputable a)
 374                  => RewritingDepth
 375                  -> BlockEnv a
 376                  -> PassName
 377                  -> DataflowLattice a
 378                  -> ForwardTransfers m l a
 379                  -> ForwardRewrites m l a AGraph
 380                  -> a                 -- fact flowing in (at entry or exit)
 381                  -> Graph m l
 382                  -> UniqSupply
 383                  -> FuelMonad (ForwardFixedPoint m l a (Graph m l))
 384 rewrite_f_agraph depth start_facts name lattice transfers rewrites in_fact g u =
 385     runDFM u lattice $
 386     do fuel <- fuelRemaining
 387        (fp, fuel') <- forward_rew maybeRewriteWithFuel areturn depth start_facts name
 388                       transfers rewrites in_fact g fuel
 389        fuelDecrement name fuel fuel'
 390        return fp
 391
 392 areturn :: AGraph m l -> DFM a (Graph m l)
 393 areturn g = liftUSM $ graphOfAGraph g
 394
 395
 396 {-
 397 graphToLGraph :: LastNode l => Graph m l -> DFM a (LGraph m l)
 398 graphToLGraph (Graph (ZLast (LastOther l)) blockenv)
 399     | isBranchNode l = return $ LGraph (branchNodeTarget l) blockenv
 400 graphToLGraph (Graph tail blockenv) =
 401     do id <- freshBlockId "temporary entry label"
 402        return $ LGraph id $ insertBlock (Block id tail) blockenv
 403 -}
 404
 405 -- | Here we prefer not simply to slap on 'goto eid' because this
 406 -- introduces an unnecessary basic block at each rewrite, and we don't
 407 -- want to stress out the finite map more than necessary
 408 lgraphToGraph :: LastNode l => LGraph m l -> Graph m l
 409 lgraphToGraph (LGraph eid blocks) =
 410     if flip any (eltsUFM blocks) $ \block -> any (== eid) (succs block) then
 411         Graph (ZLast (mkBranchNode eid)) blocks
 412     else -- common case: entry is not a branch target
 413         let Block _ entry = lookupBlockEnv blocks eid `orElse` panic "missing entry!"
 414         in  Graph entry (delFromUFM blocks eid)
 415
 416
 417 class (Outputable m, Outputable l, LastNode l, Outputable (LGraph m l)) => DebugNodes m l
 418
 419 fwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
 420              => PassName
 421              -> BlockEnv a
 422              -> ForwardTransfers m l a
 423              -> a
 424              -> Graph m l
 425              -> DFM a (ForwardFixedPoint m l a ())
 426
 427 fwd_pure_anal name env transfers in_fact g =
 428     do (fp, _) <- anal_f name env transfers panic_rewrites in_fact g panic_fuel
 429        return fp
 430   where -- definitiely a case of "I love lazy evaluation"
 431     anal_f = forward_sol (\_ _ -> Nothing) panic_return panic_depth
 432     panic_rewrites = panic "pure analysis asked for a rewrite function"
 433     panic_fuel     = panic "pure analysis asked for fuel"
 434     panic_return   = panic "pure analysis tried to return a rewritten graph"
 435     panic_depth    = panic "pure analysis asked for a rewrite depth"
 436
 437 -----------------------------------------------------------------------
 438 --
 439 --      Here beginneth the super-general functions
 440 --
 441 --  Think of them as (typechecked) macros
 442 --   *  They are not exported
 443 --
 444 --   *  They are called by the specialised wrappers
 445 --      above, and always inlined into their callers
 446 --
 447 -- There are four functions, one for each combination of:
 448 --      Forward, Backward
 449 --      Solver, Rewriter
 450 --
 451 -- A "solver" produces a (DFM f (f, Fuel)),
 452 --      where f is the fact at entry(Bwd)/exit(Fwd)
 453 --      and from the DFM you can extract
 454 --              the BlockId->f
 455 --              the change-flag
 456 --              and more besides
 457 --
 458 -- A "rewriter" produces a rewritten *Graph* as well
 459 --
 460 -- Both constrain their rewrites by
 461 --      a) Fuel
 462 --      b) RewritingDepth: shallow/deep
 463
 464 -----------------------------------------------------------------------
 465
 466 type Fuel = OptimizationFuel
 467
 468 {-# INLINE forward_sol #-}
 469 forward_sol
 470         :: forall m l g a .
 471            (DebugNodes m l, LastNode l, Outputable a)
 472         => (forall a . Fuel -> Maybe a -> Maybe a)
 473                 -- Squashes proposed rewrites if there is
 474                 -- no more fuel; OR if we are doing a pure
 475                 -- analysis, so totally ignore the rewrite
 476                 -- ie. For pure-analysis the fn is (\_ _ -> Nothing)
 477         -> (g m l -> DFM a (Graph m l))
 478                 -- Transforms the kind of graph 'g' wanted by the
 479                 -- client (in ForwardRewrites) to the kind forward_sol likes
 480         -> RewritingDepth       -- Shallow/deep
 481         -> PassName
 482         -> BlockEnv a           -- Initial set of facts
 483         -> ForwardTransfers m l a
 484         -> ForwardRewrites m l a g
 485         -> a                    -- Entry fact
 486         -> Graph m l
 487         -> Fuel
 488         -> DFM a (ForwardFixedPoint m l a (), Fuel)
 489 forward_sol check_maybe return_graph = forw
 490  where
 491   forw :: RewritingDepth
 492        -> PassName
 493        -> BlockEnv a
 494        -> ForwardTransfers m l a
 495        -> ForwardRewrites m l a g
 496        -> a
 497        -> Graph m l
 498        -> Fuel
 499        -> DFM a (ForwardFixedPoint m l a (), Fuel)
 500   forw rewrite name start_facts transfers rewrites =
 501    let anal_f :: DFM a b -> a -> Graph m l -> DFM a b
 502        anal_f finish in' g =
 503            do { fwd_pure_anal name emptyBlockEnv transfers in' g; finish }
 504
 505        solve :: DFM a b -> a -> Graph m l -> Fuel -> DFM a (b, Fuel)
 506        solve finish in_fact (Graph entry blockenv) fuel =
 507          let blocks = G.postorder_dfs_from blockenv entry
 508              set_or_save = mk_set_or_save (isJust . lookupBlockEnv blockenv)
 509              set_successor_facts (Block id tail) fuel =
 510                do { idfact <- getFact id
 511                   ; (last_outs, fuel) <-
 512                       case check_maybe fuel $ fr_first rewrites idfact id of
 513                         Nothing -> solve_tail idfact tail fuel
 514                         Just g ->
 515                           do g <- return_graph g
 516                              (a, fuel) <- subAnalysis' $
 517                                case rewrite of
 518                                  RewriteDeep -> solve getExitFact idfact g (oneLessFuel fuel)
 519                                  RewriteShallow ->
 520                                      do { a <- anal_f getExitFact idfact g
 521                                         ; return (a, oneLessFuel fuel) }
 522                              solve_tail a tail fuel
 523                   ; set_or_save last_outs
 524                   ; return fuel }
 525
 526          in do { (last_outs, fuel) <- solve_tail in_fact entry fuel
 527                ; set_or_save last_outs
 528                ; fuel <- run "forward" name set_successor_facts blocks fuel
 529                ; b <- finish
 530                ; return (b, fuel)
 531                }
 532
 533        solve_tail in' (G.ZTail m t) fuel =
 534          case check_maybe fuel $ fr_middle rewrites in' m of
 535            Nothing -> solve_tail (ft_middle_out transfers in' m) t fuel
 536            Just g ->
 537              do { g <- return_graph g
 538                 ; (a, fuel) <- subAnalysis' $
 539                      case rewrite of
 540                        RewriteDeep -> solve getExitFact in' g (oneLessFuel fuel)
 541                        RewriteShallow -> do { a <- anal_f getExitFact in' g
 542                                             ; return (a, oneLessFuel fuel) }
 543                 ; solve_tail a t fuel
 544                 }
 545        solve_tail in' (G.ZLast l) fuel =
 546          case check_maybe fuel $ either_last rewrites in' l of
 547            Nothing ->
 548                case l of LastOther l -> return (ft_last_outs transfers in' l, fuel)
 549                          LastExit -> do { setExitFact (ft_exit_out transfers in')
 550                                         ; return (LastOutFacts [], fuel) }
 551            Just g ->
 552              do { g <- return_graph g
 553                 ; (last_outs :: LastOutFacts a, fuel) <- subAnalysis' $
 554                     case rewrite of
 555                       RewriteDeep -> solve lastOutFacts in' g (oneLessFuel fuel)
 556                       RewriteShallow -> do { los <- anal_f lastOutFacts in' g
 557                                            ; return (los, fuel) }
 558                 ; return (last_outs, fuel)
 559                 }
 560
 561        fixed_point in_fact g fuel =
 562          do { setAllFacts start_facts
 563             ; (a, fuel) <- solve getExitFact in_fact g fuel
 564             ; facts <- getAllFacts
 565             ; last_outs <- lastOutFacts
 566             ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
 567             ; let fp = FFP cfp last_outs
 568             ; return (fp, fuel)
 569             }
 570
 571        either_last rewrites in' (LastExit) = fr_exit rewrites in'
 572        either_last rewrites in' (LastOther l) = fr_last rewrites in' l
 573
 574    in fixed_point
 575
 576
 577
 578
 579 mk_set_or_save :: (DataflowAnalysis df, Monad (df a), Outputable a) =>
 580                   (BlockId -> Bool) -> LastOutFacts a -> df a ()
 581 mk_set_or_save is_local (LastOutFacts l) = mapM_ set_or_save_one l
 582     where set_or_save_one (id, a) =
 583               if is_local id then setFact id a else addLastOutFact (id, a)
 584
 585
 586
 587
 588 {-# INLINE forward_rew #-}
 589 forward_rew
 590         :: forall m l g a .
 591            (DebugNodes m l, LastNode l, Outputable a)
 592         => (forall a . Fuel -> Maybe a -> Maybe a)
 593         -> (g m l -> DFM a (Graph m l))  -- option on what to rewrite
 594         -> RewritingDepth
 595         -> BlockEnv a
 596         -> PassName
 597         -> ForwardTransfers m l a
 598         -> ForwardRewrites m l a g
 599         -> a
 600         -> Graph m l
 601         -> Fuel
 602         -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
 603 forward_rew check_maybe return_graph = forw
 604   where
 605     solve = forward_sol check_maybe return_graph
 606     forw :: RewritingDepth
 607          -> BlockEnv a
 608          -> PassName
 609          -> ForwardTransfers m l a
 610          -> ForwardRewrites m l a g
 611          -> a
 612          -> Graph m l
 613          -> Fuel
 614          -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
 615     forw depth xstart_facts name transfers rewrites in_factx gx fuelx =
 616       let rewrite :: BlockEnv a -> DFM a b
 617                   -> a -> Graph m l -> Fuel
 618                   -> DFM a (b, Graph m l, Fuel)
 619           rewrite start finish in_fact g fuel =
 620             let Graph entry blockenv = g
 621                 blocks = G.postorder_dfs_from blockenv entry
 622             in do { solve depth name start transfers rewrites in_fact g fuel
 623                   ; eid <- freshBlockId "temporary entry id"
 624                   ; (rewritten, fuel) <-
 625                       rew_tail (ZFirst eid) in_fact entry emptyBlockEnv fuel
 626                   ; (rewritten, fuel) <- rewrite_blocks blocks rewritten fuel
 627                   ; a <- finish
 628                   ; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
 629                   }
 630           don't_rewrite finish in_fact g fuel =
 631               do  { solve depth name emptyBlockEnv transfers rewrites in_fact g fuel
 632                   ; a <- finish
 633                   ; return (a, g, fuel)
 634                   }
 635           inner_rew :: DFM a b
 636                     -> a -> Graph m l -> Fuel
 637                     -> DFM a (b, Graph m l, Fuel)
 638           inner_rew = case depth of RewriteShallow -> don't_rewrite
 639                                     RewriteDeep -> rewrite emptyBlockEnv
 640           fixed_pt_and_fuel =
 641               do { (a, g, fuel) <- rewrite xstart_facts getExitFact in_factx gx fuelx
 642                  ; facts <- getAllFacts
 643                  ; changed <- graphWasRewritten
 644                  ; last_outs <- lastOutFacts
 645                  ; let cfp = FP facts a changed (panic "no decoration?!") g
 646                  ; let fp = FFP cfp last_outs
 647                  ; return (fp, fuel)
 648                  }
 649           rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
 650                          -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
 651           rewrite_blocks [] rewritten fuel = return (rewritten, fuel)
 652           rewrite_blocks (G.Block id t : bs) rewritten fuel =
 653             do let h = ZFirst id
 654                a <- getFact id
 655                case check_maybe fuel $ fr_first rewrites a id of
 656                  Nothing -> do { (rewritten, fuel) <- rew_tail h a t rewritten fuel
 657                                ; rewrite_blocks bs rewritten fuel }
 658                  Just g  -> do { markGraphRewritten
 659                                ; g <- return_graph g
 660                                ; (outfact, g, fuel) <- inner_rew getExitFact a g fuel
 661                                ; let (blocks, h) = splice_head' (ZFirst id) g
 662                                ; (rewritten, fuel) <-
 663                                  rew_tail h outfact t (blocks `plusUFM` rewritten) fuel
 664                                ; rewrite_blocks bs rewritten fuel }
 665
 666           rew_tail head in' (G.ZTail m t) rewritten fuel =
 667             my_trace "Rewriting middle node" (ppr m) $
 668             case check_maybe fuel $ fr_middle rewrites in' m of
 669               Nothing -> rew_tail (G.ZHead head m) (ft_middle_out transfers in' m) t
 670                          rewritten fuel
 671               Just g -> do { markGraphRewritten
 672                            ; g <- return_graph g
 673                            ; (a, g, fuel) <- inner_rew getExitFact in' g fuel
 674                            ; let (blocks, h) = G.splice_head' head g
 675                            ; rew_tail h a t (blocks `plusUFM` rewritten) fuel
 676                            }
 677           rew_tail h in' (G.ZLast l) rewritten fuel =
 678             my_trace "Rewriting last node" (ppr l) $
 679             case check_maybe fuel $ either_last rewrites in' l of
 680               Nothing -> -- can throw away facts because this is the rewriting phase
 681                          return (insertBlock (zipht h (G.ZLast l)) rewritten, fuel)
 682               Just g -> do { markGraphRewritten
 683                            ; g <- return_graph g
 684                            ; ((), g, fuel) <- inner_rew (return ()) in' g fuel
 685                            ; let g' = G.splice_head_only' h g
 686                            ; return (G.lg_blocks g' `plusUFM` rewritten, fuel)
 687                            }
 688           either_last rewrites in' (LastExit) = fr_exit rewrites in'
 689           either_last rewrites in' (LastOther l) = fr_last rewrites in' l
 690       in  fixed_pt_and_fuel
 691
 692 --lastOutFacts :: (DataflowAnalysis m, Monad (m f)) => m f (LastOutFacts f)
 693 lastOutFacts :: DFM f (LastOutFacts f)
 694 lastOutFacts = bareLastOutFacts >>= return . LastOutFacts
 695
 696 {- ================================================================ -}
 697
 698 solve_b         :: (DebugNodes m l, Outputable a)
 699                 => BlockEnv a        -- initial facts (unbound == bottom)
 700                 -> PassName
 701                 -> DataflowLattice a -- lattice
 702                 -> BackwardTransfers m l a   -- dataflow transfer functions
 703                 -> a                 -- exit fact
 704                 -> Graph m l         -- graph to be analyzed
 705                 -> BackwardFixedPoint m l a ()  -- answers
 706 solve_b env name lattice transfers exit_fact g =
 707    runWithInfiniteFuel $ runDFM panic_us lattice $
 708                          bwd_pure_anal name env transfers g exit_fact
 709  where panic_us = panic "pure analysis pulled on a UniqSupply"
 710
 711
 712 rewrite_b_graph  :: (DebugNodes m l, Outputable a)
 713                  => RewritingDepth
 714                  -> BlockEnv a
 715                  -> PassName
 716                  -> DataflowLattice a
 717                  -> BackwardTransfers m l a
 718                  -> BackwardRewrites m l a Graph
 719                  -> a                 -- fact flowing in at exit
 720                  -> Graph m l
 721                  -> UniqSupply
 722                  -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
 723 rewrite_b_graph depth start_facts name lattice transfers rewrites exit_fact g u =
 724     runDFM u lattice $
 725     do fuel <- fuelRemaining
 726        (fp, fuel') <- backward_rew maybeRewriteWithFuel return depth start_facts name
 727                       transfers rewrites g exit_fact fuel
 728        fuelDecrement name fuel fuel'
 729        return fp
 730
 731 rewrite_b_agraph :: (DebugNodes m l, Outputable a)
 732                  => RewritingDepth
 733                  -> BlockEnv a
 734                  -> PassName
 735                  -> DataflowLattice a
 736                  -> BackwardTransfers m l a
 737                  -> BackwardRewrites m l a AGraph
 738                  -> a                 -- fact flowing in at exit
 739                  -> Graph m l
 740                  -> UniqSupply
 741                  -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
 742 rewrite_b_agraph depth start_facts name lattice transfers rewrites exit_fact g u =
 743     runDFM u lattice $
 744     do fuel <- fuelRemaining
 745        (fp, fuel') <- backward_rew maybeRewriteWithFuel areturn depth start_facts name
 746                       transfers rewrites g exit_fact fuel
 747        fuelDecrement name fuel fuel'
 748        return fp
 749
 750
 751
 752 {-# INLINE backward_sol #-}
 753 backward_sol
 754         :: forall m l g a .
 755            (DebugNodes m l, LastNode l, Outputable a)
 756         => (forall a . Fuel -> Maybe a -> Maybe a)
 757         -> (g m l -> DFM a (Graph m l))  -- option on what to rewrite
 758         -> RewritingDepth
 759         -> PassName
 760         -> BlockEnv a
 761         -> BackwardTransfers m l a
 762         -> BackwardRewrites m l a g
 763         -> Graph m l
 764         -> a
 765         -> Fuel
 766         -> DFM a (BackwardFixedPoint m l a (), Fuel)
 767 backward_sol check_maybe return_graph = back
 768  where
 769   back :: RewritingDepth
 770        -> PassName
 771        -> BlockEnv a
 772        -> BackwardTransfers m l a
 773        -> BackwardRewrites m l a g
 774        -> Graph m l
 775        -> a
 776        -> Fuel
 777        -> DFM a (BackwardFixedPoint m l a (), Fuel)
 778   back rewrite name start_facts transfers rewrites =
 779    let anal_b :: Graph m l -> a -> DFM a a
 780        anal_b g out =
 781            do { fp <- bwd_pure_anal name emptyBlockEnv transfers g out
 782               ; return $ zdfFpOutputFact fp }
 783
 784        subsolve :: g m l -> a -> Fuel -> DFM a (a, Fuel)
 785        subsolve =
 786          case rewrite of
 787            RewriteDeep    -> \g a fuel ->
 788                subAnalysis' $ do { g <- return_graph g; solve g a (oneLessFuel fuel) }
 789            RewriteShallow -> \g a fuel ->
 790                subAnalysis' $ do { g <- return_graph g; a <- anal_b g a
 791                                  ; return (a, oneLessFuel fuel) }
 792
 793        solve :: Graph m l -> a -> Fuel -> DFM a (a, Fuel)
 794        solve (Graph entry blockenv) exit_fact fuel =
 795          let blocks = reverse $ G.postorder_dfs_from blockenv entry
 796              last_in  _env (LastExit)    = exit_fact
 797              last_in   env (LastOther l) = bt_last_in transfers env l
 798              last_rew _env (LastExit)    = br_exit rewrites
 799              last_rew  env (LastOther l) = br_last rewrites env l
 800              set_block_fact block fuel =
 801                  let (h, l) = G.goto_end (G.unzip block) in
 802                  do { env <- factsEnv
 803                     ; (a, fuel) <-
 804                       case check_maybe fuel $ last_rew env l of
 805                         Nothing -> return (last_in env l, fuel)
 806                         Just g -> subsolve g exit_fact fuel
 807                     ; set_head_fact h a fuel
 808                     ; return fuel }
 809
 810          in do { fuel <- run "backward" name set_block_fact blocks fuel
 811                ; eid <- freshBlockId "temporary entry id"
 812                ; fuel <- set_block_fact (Block eid entry) fuel
 813                ; a <- getFact eid
 814                ; forgetFact eid
 815                ; return (a, fuel)
 816                }
 817
 818        set_head_fact (G.ZFirst id) a fuel =
 819          case check_maybe fuel $ br_first rewrites a id of
 820            Nothing -> do { setFact id a; return fuel }
 821            Just g  -> do { (a, fuel) <- subsolve g a fuel
 822                          ; setFact id a
 823                          ; return fuel
 824                          }
 825        set_head_fact (G.ZHead h m) a fuel =
 826          case check_maybe fuel $ br_middle rewrites a m of
 827            Nothing -> set_head_fact h (bt_middle_in transfers a m) fuel
 828            Just g -> do { (a, fuel) <- subsolve g a fuel
 829                         ; set_head_fact h a fuel }
 830
 831        fixed_point g exit_fact fuel =
 832          do { setAllFacts start_facts
 833             ; (a, fuel) <- solve g exit_fact fuel
 834             ; facts <- getAllFacts
 835             ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
 836             ; return (cfp, fuel)
 837             }
 838    in fixed_point
 839
 840 bwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
 841              => PassName
 842              -> BlockEnv a
 843              -> BackwardTransfers m l a
 844              -> Graph m l
 845              -> a
 846              -> DFM a (BackwardFixedPoint m l a ())
 847
 848 bwd_pure_anal name env transfers g exit_fact =
 849     do (fp, _) <- anal_b name env transfers panic_rewrites g exit_fact panic_fuel
 850        return fp
 851   where -- another case of "I love lazy evaluation"
 852     anal_b = backward_sol (\_ _ -> Nothing) panic_return panic_depth
 853     panic_rewrites = panic "pure analysis asked for a rewrite function"
 854     panic_fuel     = panic "pure analysis asked for fuel"
 855     panic_return   = panic "pure analysis tried to return a rewritten graph"
 856     panic_depth    = panic "pure analysis asked for a rewrite depth"
 857
 858
 859 {- ================================================================ -}
 860
 861 {-# INLINE backward_rew #-}
 862 backward_rew
 863         :: forall m l g a .
 864            (DebugNodes m l, LastNode l, Outputable a)
 865         => (forall a . Fuel -> Maybe a -> Maybe a)
 866         -> (g m l -> DFM a (Graph m l))  -- option on what to rewrite
 867         -> RewritingDepth
 868         -> BlockEnv a
 869         -> PassName
 870         -> BackwardTransfers m l a
 871         -> BackwardRewrites m l a g
 872         -> Graph m l
 873         -> a
 874         -> Fuel
 875         -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
 876 backward_rew check_maybe return_graph = back
 877   where
 878     solve = backward_sol check_maybe return_graph
 879     back :: RewritingDepth
 880          -> BlockEnv a
 881          -> PassName
 882          -> BackwardTransfers m l a
 883          -> BackwardRewrites m l a g
 884          -> Graph m l
 885          -> a
 886          -> Fuel
 887          -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
 888     back depth xstart_facts name transfers rewrites gx exit_fact fuelx =
 889       let rewrite :: BlockEnv a
 890                   -> Graph m l -> a -> Fuel
 891                   -> DFM a (a, Graph m l, Fuel)
 892           rewrite start g exit_fact fuel =
 893            let Graph entry blockenv = g
 894                blocks = reverse $ G.postorder_dfs_from blockenv entry
 895            in do { solve depth name start transfers rewrites g exit_fact fuel
 896                  ; eid <- freshBlockId "temporary entry id"
 897                  ; (rewritten, fuel) <- rewrite_blocks blocks emptyBlockEnv fuel
 898                  ; (rewritten, fuel) <- rewrite_blocks [Block eid entry] rewritten fuel
 899                  ; a <- getFact eid
 900                  ; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
 901                  }
 902           don't_rewrite g exit_fact fuel =
 903             do { (fp, _) <-
 904                      solve depth name emptyBlockEnv transfers rewrites g exit_fact fuel
 905                ; return (zdfFpOutputFact fp, g, fuel) }
 906           inner_rew = case depth of RewriteShallow -> don't_rewrite
 907                                     RewriteDeep    -> rewrite emptyBlockEnv
 908           inner_rew :: Graph m l -> a -> Fuel -> DFM a (a, Graph m l, Fuel)
 909           fixed_pt_and_fuel =
 910               do { (a, g, fuel) <- rewrite xstart_facts gx exit_fact fuelx
 911                  ; facts <- getAllFacts
 912                  ; changed <- graphWasRewritten
 913                  ; let fp = FP facts a changed (panic "no decoration?!") g
 914                  ; return (fp, fuel)
 915                  }
 916           rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
 917                          -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
 918           rewrite_blocks bs rewritten fuel =
 919               do { env <- factsEnv
 920                  ; let rew [] r f = return (r, f)
 921                        rew (b : bs) r f =
 922                            do { (r, f) <- rewrite_block env b r f; rew bs r f }
 923                  ; rew bs rewritten fuel }
 924           rewrite_block env b rewritten fuel =
 925             let (h, l) = G.goto_end (G.unzip b) in
 926             case maybeRewriteWithFuel fuel $ either_last env l of
 927               Nothing -> propagate fuel h (last_in env l) (ZLast l) rewritten
 928               Just g ->
 929                 do { markGraphRewritten
 930                    ; g <- return_graph g
 931                    ; (a, g, fuel) <- inner_rew g exit_fact fuel
 932                    ; let G.Graph t new_blocks = g
 933                    ; let rewritten' = new_blocks `plusUFM` rewritten
 934                    ; propagate fuel h a t rewritten' -- continue at entry of g
 935                    }
 936           either_last _env (LastExit)    = br_exit rewrites
 937           either_last  env (LastOther l) = br_last rewrites env l
 938           last_in _env (LastExit)    = exit_fact
 939           last_in  env (LastOther l) = bt_last_in transfers env l
 940           propagate fuel (ZHead h m) a tail rewritten =
 941             case maybeRewriteWithFuel fuel $ br_middle rewrites a m of
 942               Nothing ->
 943                 propagate fuel h (bt_middle_in transfers a m) (ZTail m tail) rewritten
 944               Just g  ->
 945                 do { markGraphRewritten
 946                    ; g <- return_graph g
 947                    ; my_trace "Rewrote middle node"
 948                                              (f4sep [ppr m, text "to", pprGraph g]) $
 949                      return ()
 950                    ; (a, g, fuel) <- inner_rew g a fuel
 951                    ; let Graph t newblocks = G.splice_tail g tail
 952                    ; propagate fuel h a t (newblocks `plusUFM` rewritten) }
 953           propagate fuel (ZFirst id) a tail rewritten =
 954             case maybeRewriteWithFuel fuel $ br_first rewrites a id of
 955               Nothing -> do { checkFactMatch id a
 956                             ; return (insertBlock (Block id tail) rewritten, fuel) }
 957               Just g ->
 958                 do { markGraphRewritten
 959                    ; g <- return_graph g
 960                    ; my_trace "Rewrote first node"
 961                      (f4sep [ppr id <> colon, text "to", pprGraph g]) $ return ()
 962                    ; (a, g, fuel) <- inner_rew g a fuel
 963                    ; checkFactMatch id a
 964                    ; let Graph t newblocks = G.splice_tail g tail
 965                    ; let r = insertBlock (Block id t) (newblocks `plusUFM` rewritten)
 966                    ; return (r, fuel) }
 967       in  fixed_pt_and_fuel
 968
 969 {- ================================================================ -}
 970
 971 instance FixedPoint CommonFixedPoint where
 972     zdfFpFacts        = fp_facts
 973     zdfFpOutputFact   = fp_out
 974     zdfGraphChanged   = fp_changed
 975     zdfDecoratedGraph = fp_dec_graph
 976     zdfFpContents     = fp_contents
 977     zdfFpMap f (FP fs out ch dg a) = FP fs out ch dg (f a)
 978
 979 instance FixedPoint ForwardFixedPoint where
 980     zdfFpFacts        = fp_facts     . ffp_common
 981     zdfFpOutputFact   = fp_out       . ffp_common
 982     zdfGraphChanged   = fp_changed   . ffp_common
 983     zdfDecoratedGraph = fp_dec_graph . ffp_common
 984     zdfFpContents     = fp_contents  . ffp_common
 985     zdfFpMap f (FFP fp los) = FFP (zdfFpMap f fp) los
 986
 987
 988 dump_things :: Bool
 989 dump_things = True
 990
 991 my_trace :: String -> SDoc -> a -> a
 992 my_trace = if dump_things then pprTrace else \_ _ a -> a
 993
 994
 995 -- | Here's a function to run an action on blocks until we reach a fixed point.
 996 run :: (Outputable a, DebugNodes m l) =>
 997        String -> String -> (Block m l -> b -> DFM a b) -> [Block m l] -> b -> DFM a b
 998 run dir name do_block blocks b =
 999    do { show_blocks $ iterate (1::Int) }
1000    where
1001      -- N.B. Each iteration starts with the same transaction limit;
1002      -- only the rewrites in the final iteration actually count
1003      trace_block b block =
1004          my_trace "about to do" (text name <+> text "on" <+> ppr (blockId block)) $
1005          do_block block b
1006      iterate n =
1007          do { markFactsUnchanged
1008             ; b <- foldM trace_block b blocks
1009             ; changed <- factsStatus
1010             ; facts <- getAllFacts
1011             ; let depth = 0 -- was nesting depth
1012             ; ppIter depth n $
1013               case changed of
1014                 NoChange -> unchanged depth $ return b
1015                 SomeChange ->
1016                     pprFacts depth n facts $
1017                     if n < 1000 then iterate (n+1)
1018                     else panic $ msg n
1019             }
1020      msg n = concat [name, " didn't converge in ", show n, " " , dir,
1021                      " iterations"]
1022      my_nest depth sdoc = my_trace "" $ nest (3*depth) sdoc
1023      ppIter depth n = my_nest depth (empty $$ text "*************** iteration" <+> pp_i n)
1024      pp_i n = int n <+> text "of" <+> text name <+> text "on" <+> graphId
1025      unchanged depth = my_nest depth (text "facts are unchanged")
1026
1027      pprFacts depth n env =
1028          my_nest depth (text "facts for iteration" <+> pp_i n <+> text "are:" $$
1029                         (nest 2 $ vcat $ map pprFact $ ufmToList env))
1030      pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)
1031      graphId = case blocks of { Block id _ : _ -> ppr id ; [] -> text "<empty>" }
1032      show_blocks = my_trace "Blocks:" (vcat (map pprBlock blocks))
1033      pprBlock (Block id t) = nest 2 (pprFact (id, t))
1034
1035
1036 f4sep :: [SDoc] -> SDoc
1037 f4sep [] = fsep []
1038 f4sep (d:ds) = fsep (d : map (nest 4) ds)
1039
1040
1041 subAnalysis' :: (Monad (m f), DataflowAnalysis m, Outputable f) =>
1042                 m f a -> m f a
1043 subAnalysis' m =
1044     do { a <- subAnalysis $
1045                do { a <- m; facts <- getAllFacts
1046                   ; my_trace "after sub-analysis facts are" (pprFacts facts) $
1047                     return a }
1048        ; facts <- getAllFacts
1049        ; my_trace "in parent analysis facts are" (pprFacts facts) $
1050          return a }
1051   where pprFacts env = nest 2 $ vcat $ map pprFact $ ufmToList env
1052         pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)