content: -----------------------------------------------------------------------
  -- |
  -- Module           : Lang.Crucible.Analysis.Fixpoint
  -- Description      : Abstract interpretation over SSA function CFGs
  -- Copyright        : (c) Galois, Inc 2015
  -- License          : BSD3
  -- Maintainer       : Tristan Ravitch <tristan@galois.com>
  -- Stability        : provisional
  --
  --  Abstract interpretation over the Crucible IR
  --
  --  Supports widening with an iteration order based on weak
  --  topological orderings.  Some basic tests on hand-written IR
  --  programs are included.
  ------------------------------------------------------------------------
  
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE StandaloneDeriving #-}
  {-# LANGUAGE TypeOperators #-}
  module Lang.Crucible.Analysis.Fixpoint (
    -- * Entry point
    forwardFixpoint,
    forwardFixpoint',
    ScopedReg(..),
    lookupAbstractScopedRegValue,
    lookupAbstractScopedRegValueByIndex,
    Ignore(..),
    -- * Abstract Domains
    Domain(..),
    IterationStrategy(..),
    Interpretation(..),
    PointAbstraction(..),
    RefSet,
    emptyRefSet,
    paGlobals,
    paRegisters,
    lookupAbstractRegValue,
    modifyAbstractRegValue,
    cfgWeakTopologicalOrdering,
    -- * Pointed domains
    -- $pointed
    Pointed(..),
    pointed
    ) where
  
  import           Control.Applicative
  import           Control.Lens.Operators ( (^.), (%=), (.~), (&), (%~) )
  import qualified Control.Monad.State.Strict as St
  import qualified Data.Functor.Identity as I
  import           Data.Kind
  import qualified Data.Set as S
  import           Text.Printf
  
  import           Prelude
  
  import           Data.Parameterized.Classes
  import qualified Data.Parameterized.Context as PU
  import qualified Data.Parameterized.Map as PM
  import qualified Data.Parameterized.TraversableFC as PU
  
  import           Lang.Crucible.CFG.Core
  import           Lang.Crucible.CFG.Extension
  import           Lang.Crucible.Analysis.Fixpoint.Components
  
  -- | A wrapper around widening strategies
  data WideningStrategy = WideningStrategy (Int -> Bool)
  
  -- | A wrapper around widening operators.  This is mostly here to
  -- avoid requiring impredicative types later.
  data WideningOperator dom = WideningOperator (forall tp . dom tp -> dom tp -> dom tp)
  
  -- | The iteration strategies available for computing fixed points.
  --
  -- Algorithmically, the best strategies seem to be based on Weak
  -- Topological Orders (WTOs).  The WTO approach also naturally
  -- supports widening (with a specified widening strategy and widening
  -- operator).
  --
  -- A simple worklist approach is also available.
  data IterationStrategy (dom :: CrucibleType -> Type) where
    WTO :: IterationStrategy dom
    WTOWidening :: (Int -> Bool) -> (forall tp . dom tp -> dom tp -> dom tp) -> IterationStrategy dom
    Worklist :: IterationStrategy dom
  
  -- | A domain of abstract values, parameterized by a term type
  data Domain (dom :: CrucibleType -> Type) =
    Domain { domTop    :: forall tp . dom tp
           , domBottom :: forall tp . dom tp
           , domJoin   :: forall tp . dom tp -> dom tp -> dom tp
           , domIter   :: IterationStrategy dom
           , domEq     :: forall tp . dom tp -> dom tp -> Bool
           }
  
  -- | Transfer functions for each statement type
  --
  -- Interpretation functions for some statement types --
  -- e.g. @interpExpr@ and @interpExt@ -- receive 'ScopedReg' arguments
  -- corresponding to the SSA tmp that the result of the interpreted
  -- statement get assigned to. Some interpretation functions that could
  -- receive this argument do not -- e.g. @interpCall@ -- because
  -- conathan didn't have a use for that.
  data Interpretation ext (dom :: CrucibleType -> Type) =
    Interpretation { interpExpr       :: forall blocks ctx tp
                                       . ScopedReg
                                      -> TypeRepr tp
                                      -> Expr ext ctx tp
                                      -> PointAbstraction blocks dom ctx
                                      -> (Maybe (PointAbstraction blocks dom ctx), dom tp)
                   , interpExt        :: forall blocks ctx tp
                                       . ScopedReg
                                      -> StmtExtension ext (Reg ctx) tp
                                      -> PointAbstraction blocks dom ctx
                                      -> (Maybe (PointAbstraction blocks dom ctx), dom tp)
                   , interpCall       :: forall blocks ctx args ret
                                       . CtxRepr args
                                      -> TypeRepr ret
                                      -> Reg ctx (FunctionHandleType args ret)
                                      -> dom (FunctionHandleType args ret)
                                      -> PU.Assignment dom args
                                      -> PointAbstraction blocks dom ctx
                                      -> (Maybe (PointAbstraction blocks dom ctx), dom ret)
                   , interpReadGlobal :: forall blocks ctx tp
                                       . GlobalVar tp
                                      -> PointAbstraction blocks dom ctx
                                      -> (Maybe (PointAbstraction blocks dom ctx), dom tp)
                   , interpWriteGlobal :: forall blocks ctx tp
                                        . GlobalVar tp
                                       -> Reg ctx tp
                                       -> PointAbstraction blocks dom ctx
                                       -> Maybe (PointAbstraction blocks dom ctx)
                   , interpBr         :: forall blocks ctx
                                       . Reg ctx BoolType
                                      -> dom BoolType
                                      -> JumpTarget blocks ctx
                                      -> JumpTarget blocks ctx
                                      -> PointAbstraction blocks dom ctx
                                      -> (Maybe (PointAbstraction blocks dom ctx), Maybe (PointAbstraction blocks dom ctx))
                   , interpMaybe      :: forall blocks ctx tp
                                       . TypeRepr tp
                                      -> Reg ctx (MaybeType tp)
                                      -> dom (MaybeType tp)
                                      -> PointAbstraction blocks dom ctx
                                      -> (Maybe (PointAbstraction blocks dom ctx), dom tp, Maybe (PointAbstraction blocks dom ctx))
                   }
  
  -- | This abstraction contains the abstract values of each register at
  -- the program point represented by the abstraction.  It also contains
  -- a map of abstractions for all of the global variables currently
  -- known.
  data PointAbstraction blocks dom ctx =
    PointAbstraction { _paGlobals :: PM.MapF GlobalVar dom
                     , _paRegisters :: PU.Assignment dom ctx
                     , _paRefs :: PM.MapF (RefStmtId blocks) dom
                     -- ^ In this map, the keys are really just the 'StmtId's in
                     -- '_paRegisterRefs', but with a newtype wrapper that unwraps
                     -- a level of their 'ReferenceType` type rep.
                     , _paRegisterRefs :: PU.Assignment (RefSet blocks) ctx
                     -- ^ This mapping records the *set* of references (named by
                     -- allocation site) that each register could hold.
                     }
  
  -- | This is a wrapper around 'StmtId' that exposes the underlying type of a
  -- 'ReferenceType', and is needed to define the abstract value we carry around.
  newtype RefStmtId blocks tp = RefStmtId (StmtId blocks (ReferenceType tp))
  
  -- | This type names an allocation site in a program.
  --
  -- Allocation sites are named by their basic block and their index into that
  -- containing basic block.  We have to carry around the type repr for inspection
  -- later (especially in instances).
  data StmtId blocks tp = StmtId (TypeRepr tp) (Some (BlockID blocks)) Int
    deriving (Show)
  
  instance Eq (StmtId blocks tp) where
    StmtId tp1 bid1 ix1 == StmtId tp2 bid2 ix2 =
      case testEquality tp1 tp2 of
        Nothing -> False
        Just Refl -> (bid1, ix1) == (bid2, ix2)
  
  instance Ord (StmtId blocks tp) where
    compare (StmtId tp1 bid1 ix1) (StmtId tp2 bid2 ix2) =
      case toOrdering (compareF tp1 tp2) of
        LT -> LT
        GT -> GT
        EQ -> compare (bid1, ix1) (bid2, ix2)
  
  instance TestEquality (RefStmtId blocks) where
    testEquality (RefStmtId (StmtId tp1 (Some bid1) idx1)) (RefStmtId (StmtId tp2 (Some bid2) idx2)) = do
      Refl <- testEquality tp1 tp2
      Refl <- testEquality bid1 bid2
      case idx1 == idx2 of
        True -> return $! Refl
        False -> Nothing
  
  instance OrdF (RefStmtId blocks) where
    compareF (RefStmtId (StmtId tp1 (Some bid1) idx1)) (RefStmtId (StmtId tp2 (Some bid2) idx2)) =
      case compareF tp1 tp2 of
        EQF ->
          case compareF bid1 bid2 of
            EQF ->
              case compare idx1 idx2 of
                LT -> LTF
                GT -> GTF
                EQ -> EQF
            LTF -> LTF
            GTF -> GTF
        LTF -> LTF
        GTF -> GTF
  
  -- | This is a wrapper around a set of 'StmtId's that name allocation sites of
  -- references.  We need the wrapper to correctly position the @tp@ type
  -- parameter so that we can put them in an 'PU.Assignment'.
  newtype RefSet blocks tp = RefSet (S.Set (StmtId blocks tp))
  
  emptyRefSet :: RefSet blocks tp
  emptyRefSet = RefSet S.empty
  
  unionRefSets :: RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp
  unionRefSets (RefSet s1) (RefSet s2) = RefSet (s1 `S.union` s2)
  
  instance ShowF dom => Show (PointAbstraction blocks dom ctx) where
    show pa = show (_paRegisters pa)
  
  instance ShowF dom => ShowF (PointAbstraction blocks dom)
  
  -- | Look up the abstract value of a register at a program point
  lookupAbstractRegValue :: PointAbstraction blocks dom ctx -> Reg ctx tp -> dom tp
  lookupAbstractRegValue pa (Reg ix) = (pa ^. paRegisters) PU.! ix
  
  -- | Modify the abstract value of a register at a program point
  modifyAbstractRegValue :: PointAbstraction blocks dom ctx
                         -> Reg ctx tp
                         -> (dom tp -> dom tp)
                         -> PointAbstraction blocks dom ctx
  modifyAbstractRegValue pa (Reg ix) f = pa & paRegisters . ixF ix %~ f
  
  -- | The `FunctionAbstraction` contains the abstractions for the entry
  -- point of each basic block in the function, as well as the final
  -- abstract value for the returned register.
  data FunctionAbstraction (dom :: CrucibleType -> Type) blocks ret =
    FunctionAbstraction { _faEntryRegs :: PU.Assignment (PointAbstraction blocks dom) blocks
                          -- ^ Mapping from blocks to point abstractions
                          -- at entry to blocks.
                        , _faExitRegs :: PU.Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
                          -- ^ Mapping from blocks to point abstractions
                          -- at exit from blocks. Blocks are indexed by
                          -- their entry context, but not by there exit
                          -- contexts, so we wrap the point abstraction
                          -- in @Ignore . Some@ to hide the context of
                          -- SSA tmps at exit.
                        , _faRet :: dom ret
                          -- ^ Abstract value at return from function.
                        }
  
  data IterationState (dom :: CrucibleType -> Type) blocks ret =
    IterationState { _isFuncAbstr :: FunctionAbstraction dom blocks ret
                   , _isRetAbstr  :: dom ret
                   , _processedOnce :: S.Set (Some (BlockID blocks))
                   }
  
  newtype M (dom :: CrucibleType -> Type) blocks ret a = M { runM :: St.State (IterationState dom blocks ret) a }
    deriving (St.MonadState (IterationState dom blocks ret), Monad, Applicative, Functor)
  
  -- | Extend the abstraction with a domain value for the next register.
  --
  -- The set of references that the register can point to is set to the empty set
  extendRegisters :: dom tp -> PointAbstraction blocks dom ctx -> PointAbstraction blocks dom (ctx ::> tp)
  extendRegisters domVal pa =
    pa { _paRegisters = PU.extend (_paRegisters pa) domVal
       , _paRegisterRefs = PU.extend (_paRegisterRefs pa) emptyRefSet
       }
  
  -- | Join two point abstractions using the join operation of the domain.
  --
  -- We join registers pointwise.  For globals, we explicitly call join
  -- when the global is in both maps.  If a global is only in one map,
  -- there is an implicit join with bottom, which always results in the
  -- same element.  Since it is a no-op, we just skip it and keep the
  -- one present element.
  joinPointAbstractions :: forall blocks (dom :: CrucibleType -> Type) ctx
                         . Domain dom
                        -> PointAbstraction blocks dom ctx
                        -> PointAbstraction blocks dom ctx
                        -> PointAbstraction blocks dom ctx
  joinPointAbstractions dom = zipPAWith (domJoin dom) unionRefSets
  
  zipPAWith :: forall blocks (dom :: CrucibleType -> Type) ctx
                         . (forall tp . dom tp -> dom tp -> dom tp)
                        -> (forall tp . RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp)
                        -> PointAbstraction blocks dom ctx
                        -> PointAbstraction blocks dom ctx
                        -> PointAbstraction blocks dom ctx
  zipPAWith domOp refSetOp pa1 pa2 =
    pa1 { _paRegisters = PU.zipWith domOp (pa1 ^. paRegisters) (pa2 ^. paRegisters)
        , _paGlobals = I.runIdentity $ do
            PM.mergeWithKeyM (\_ a b -> return (Just (domOp a b))) return return (pa1 ^. paGlobals) (pa2 ^. paGlobals)
        , _paRefs = I.runIdentity $ do
            PM.mergeWithKeyM (\_ a b -> return (Just (domOp a b))) return return (pa1 ^. paRefs) (pa2 ^. paRefs)
        , _paRegisterRefs = PU.zipWith refSetOp (pa1 ^. paRegisterRefs) (pa2 ^. paRegisterRefs)
        }
  
  -- | Compare two point abstractions for equality.
  --
  -- Note that the globals maps are converted to a list and the lists
  -- are checked for equality.  This should be safe if order is
  -- preserved properly in the list functions...
  equalPointAbstractions :: forall blocks (dom :: CrucibleType -> Type) ctx
                          . Domain dom
                         -> PointAbstraction blocks dom ctx
                         -> PointAbstraction blocks dom ctx
                         -> Bool
  equalPointAbstractions dom pa1 pa2 =
    PU.foldlFC (\a (Ignore b) -> a && b) True pointwiseEqualRegs && equalGlobals
    where
      checkGlobal (PM.Pair gv1 d1) (PM.Pair gv2 d2) =
        case PM.testEquality gv1 gv2 of
          Just Refl -> domEq dom d1 d2
          Nothing -> False
      equalGlobals = and $ zipWith checkGlobal (PM.toList (pa1 ^. paGlobals)) (PM.toList (pa2 ^. paGlobals))
      pointwiseEqualRegs = PU.zipWith (\a b -> Ignore (domEq dom a b)) (pa1 ^. paRegisters) (pa2 ^. paRegisters)
  
  ----------------------------------------------------------------
  
  -- | A CFG-scoped SSA temp register.
  --
  -- We don't care about the type params yet, hence the
  -- existential quantification. We may want to look up the instruction
  -- corresponding to a 'ScopedReg' after analysis though, and we'll
  -- surely want to compare 'ScopedReg's for equality, and use them to
  -- look up values in point abstractions after analysis.
  data ScopedReg where
    ScopedReg :: BlockID blocks ctx1 -> Reg ctx2 tp -> ScopedReg
  -- The pretty-show library can't parse the derived version, because it
  -- doesn't like bare "%" and/or "$" in atoms.
  {- deriving instance Show ScopedReg -}
  instance Show ScopedReg where
    show (ScopedReg b r) = printf "\"%s:%s\"" (show b) (show r)
  instance Eq ScopedReg where
    sr1 == sr2 =
      scopedRegIndexVals sr1 == scopedRegIndexVals sr2
  instance Ord ScopedReg where
    sr1 `compare` sr2 =
      scopedRegIndexVals sr1 `compare` scopedRegIndexVals sr2
  
  scopedRegIndexVals :: ScopedReg -> (Int, Int)
  scopedRegIndexVals (ScopedReg b r) = (blockIDIndexVal b, regIndexVal r)
  
  blockIDIndexVal :: BlockID ctx tp -> Int
  blockIDIndexVal = PU.indexVal . blockIDIndex
  
  regIndexVal :: Reg ctx tp -> Int
  regIndexVal = PU.indexVal . regIndex
  
  ----------------------------------------------------------------
  
  -- | Lookup the abstract value of scoped reg in an exit assignment.
  lookupAbstractScopedRegValue :: ScopedReg
    -> PU.Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
    -> Maybe (Some dom)
  lookupAbstractScopedRegValue sr ass =
    lookupAbstractScopedRegValueByIndex (scopedRegIndexVals sr) ass
  
  -- | Lookup the abstract value of scoped reg -- specified by 0-based
  -- int indices -- in an exit assignment.
  lookupAbstractScopedRegValueByIndex :: (Int, Int)
    -> PU.Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
    -> Maybe (Some dom)
  lookupAbstractScopedRegValueByIndex (b, r) ass = do
    Some (Ignore (Some pa)) <- assignmentLookupByIndex b ass
    assignmentLookupByIndex r (pa ^. paRegisters)
  
  -- | Lookup a value in an assignment based on it's 0-based int index.
  assignmentLookupByIndex :: Int -> PU.Assignment f ctx -> Maybe (Some f)
  assignmentLookupByIndex i ass =
    let sz = PU.size ass
    in case PU.intIndex i sz of
      Nothing -> Nothing
      Just (Some ix) -> Just (Some (ass PU.! ix))
  
  ----------------------------------------------------------------
  
  -- | Apply the transfer functions from an interpretation to a block,
  -- given a starting set of abstract values.
  --
  -- Return a set of blocks to visit later.
  transfer :: forall ext dom blocks ret ctx
            . Domain dom
           -> Interpretation ext dom
           -> TypeRepr ret
           -> Block ext blocks ret ctx
           -> PointAbstraction blocks dom ctx
           -> M dom blocks ret (S.Set (Some (BlockID blocks)))
  transfer dom interp retRepr blk = transferSeq blockInputSize (_blockStmts blk)
    where
      blockInputSize :: PU.Size ctx
      blockInputSize = PU.size $ blockInputs blk
  
      lookupReg = flip lookupAbstractRegValue
  
      -- We maintain the current 'Size' of the context so that we can
      -- compute the SSA temp register corresponding to the current
      -- statement.
      transferSeq :: forall ctx'
                   . PU.Size ctx'
                  -> StmtSeq ext blocks ret ctx'
                  -> PointAbstraction blocks dom ctx'
                  -> M dom blocks ret (S.Set (Some (BlockID blocks)))
      transferSeq sz (ConsStmt _loc stmt ss) =
        transferSeq (nextStmtHeight sz stmt) ss .
        transferStmt sz stmt
      transferSeq _sz (TermStmt _loc term) = transferTerm term
  
      transferStmt :: forall ctx1 ctx2
                    . PU.Size ctx1
                   -> Stmt ext ctx1 ctx2
                   -> PointAbstraction blocks dom ctx1
                   -> PointAbstraction blocks dom ctx2
      transferStmt sz s assignment =
        case s of
          SetReg (tp :: TypeRepr tp) ex ->
            let reg :: Reg (ctx1 ::> tp) tp
                reg = Reg (PU.nextIndex sz)
                scopedReg = ScopedReg (blockID blk) reg
                (assignment', absVal) = interpExpr interp scopedReg tp ex assignment
                assignment'' = maybe assignment (joinPointAbstractions dom assignment) assignment'
            in extendRegisters absVal assignment''
  
          ExtendAssign (estmt :: StmtExtension ext (Reg ctx1) tp) ->
            let reg :: Reg (ctx1 ::> tp) tp
                reg = Reg (PU.nextIndex sz)
                scopedReg = ScopedReg (blockID blk) reg
                (assignment', absVal) = interpExt interp scopedReg estmt assignment
                assignment'' = maybe assignment (joinPointAbstractions dom assignment) assignment'
            in extendRegisters absVal assignment''
  
          -- This statement aids in debugging the representation, but
          -- should not be a meaningful part of any analysis.  For now,
          -- skip it in the interpretation.  We could add a transfer
          -- function for it...
          --
          -- Note that this is not used to represent print statements in
          -- the language being represented.  This is a *crucible* level
          -- print.  This is actually apparent in the type of Print,
          -- which does not modify its context at all.
          Print _reg -> assignment
  
          CallHandle retTp funcHandle argTps actuals ->
            let actualsAbstractions = PU.zipWith (\_ act -> lookupReg act assignment) argTps actuals
                funcAbstraction = lookupReg funcHandle assignment
                (assignment', absVal) = interpCall interp argTps retTp funcHandle funcAbstraction actualsAbstractions assignment
                assignment'' = maybe assignment (joinPointAbstractions dom assignment) assignment'
            in extendRegisters absVal assignment''
  
          -- FIXME: This would actually potentially be nice to
          -- capture. We would need to extend the context,
          -- though... maybe with a unit type.
          Assert _ _ -> assignment
          Assume _ _ -> assignment
  
          ReadGlobal gv ->
            let (assignment', absVal) = interpReadGlobal interp gv assignment
                assignment'' = maybe assignment (joinPointAbstractions dom assignment) assignment'
            in extendRegisters absVal assignment''
          WriteGlobal gv reg ->
            let assignment' = interpWriteGlobal interp gv reg assignment
            in maybe assignment (joinPointAbstractions dom assignment) assignment'
  
          FreshConstant{} -> error "transferStmt: FreshConstant not supported"
          FreshFloat{} -> error "transferStmt: FreshFloat not supported"
          FreshNat{} -> error "transferStmt: FreshNat not supported"
          NewEmptyRefCell{} -> error "transferStmt: NewEmptyRefCell not supported"
          NewRefCell {} -> error "transferStmt: NewRefCell not supported"
          ReadRefCell {} -> error "transferStmt: ReadRefCell not supported"
          WriteRefCell {} -> error "transferStmt: WriteRefCell not supported"
          DropRefCell {} -> error "transferStmt: DropRefCell not supported"
  
      -- Transfer a block terminator statement.
      transferTerm :: forall ctx'
                    . TermStmt blocks ret ctx'
                   -> PointAbstraction blocks dom ctx'
                   -> M dom blocks ret (S.Set (Some (BlockID blocks)))
      transferTerm s assignment = do
        -- Save the current point abstraction as the exit point
        -- abstraction since we won't be defining any more SSA tmps in
        -- this block.
        let BlockID srcIdx = blockID blk
        isFuncAbstr %= (faExitRegs . ixF srcIdx .~ Ignore (Some assignment))
  
        case s of
          ErrorStmt {} -> return S.empty
          Jump target -> transferJump target assignment
          Br condReg target1 target2 -> do
            let condAbst = lookupReg condReg assignment
                (d1, d2) = interpBr interp condReg condAbst target1 target2 assignment
                d1' = maybe assignment (joinPointAbstractions dom assignment) d1
                d2' = maybe assignment (joinPointAbstractions dom assignment) d2
            s1 <- transferJump target1 d1'
            s2 <- transferJump target2 d2'
            return (S.union s1 s2)
          MaybeBranch tp mreg swTarget jmpTarget -> do
            let condAbst = lookupReg mreg assignment
                (d1, mAbstraction, d2) = interpMaybe interp tp mreg condAbst assignment
                d1' = maybe assignment (joinPointAbstractions dom assignment) d1
                d2' = maybe assignment (joinPointAbstractions dom assignment) d2
            s1 <- transferSwitch swTarget mAbstraction d1'
            s2 <- transferJump jmpTarget d2'
            return (S.union s1 s2)
          Return reg -> do
            let absVal = lookupReg reg assignment
            isRetAbstr %= domJoin dom absVal
            return S.empty
  
          TailCall fn callArgs actuals -> do
            let argAbstractions = PU.zipWith (\_tp act -> lookupReg act assignment) callArgs actuals
                callee = lookupReg fn assignment
                (_assignment', absVal) = interpCall interp callArgs retRepr fn callee argAbstractions assignment
                -- assignment'' = maybe assignment (joinPointAbstractions dom assignment) assignment'
  
            -- We don't really have a place to put a modified assignment
            -- here, which is interesting.  There is no next block...
            isRetAbstr %= domJoin dom absVal
            return S.empty
  
          VariantElim {} -> error "transferTerm: VariantElim terminator not supported"
  
  
      transferJump :: forall ctx'
                    . JumpTarget blocks ctx'
                   -> PointAbstraction blocks dom ctx'
                   -> M dom blocks ret (S.Set (Some (BlockID blocks)))
      transferJump (JumpTarget target argsTps actuals) assignment = do
        let blockAbstr0 = assignment { _paRegisters = PU.zipWith (\_tp act -> lookupReg act assignment) argsTps actuals
                                     , _paRegisterRefs = PU.zipWith (\_tp act -> lookupRegRefs act assignment) argsTps actuals
                                     }
        transferTarget target blockAbstr0
  
      transferSwitch :: forall ctx' tp
                      . SwitchTarget blocks ctx' tp
                     -> dom tp
                     -> PointAbstraction blocks dom ctx'
                     -> M dom blocks ret (S.Set (Some (BlockID blocks)))
      transferSwitch (SwitchTarget target argTps actuals) domVal assignment = do
        let argRegAbstractions = PU.zipWith (\_ act -> lookupReg act assignment) argTps actuals
            argRegRefAbstractions = PU.zipWith (\_ act -> lookupRegRefs act assignment) argTps actuals
            blockAbstr0 = assignment { _paRegisters = PU.extend argRegAbstractions domVal
                                     , _paRegisterRefs = PU.extend argRegRefAbstractions emptyRefSet
                                     }
        transferTarget target blockAbstr0
  
      -- Return the singleton set containing the target block if we
      -- haven't converged yet on the current block, and otherwise
      -- return an empty set while updating the function abstraction for
      -- the current block.
      transferTarget :: forall ctx'
                      . BlockID blocks ctx'
                     -> PointAbstraction blocks dom ctx'
                     -> M dom blocks ret (S.Set (Some (BlockID blocks)))
      transferTarget target@(BlockID idx) assignment = do
        old <- lookupAssignment idx
        haveVisited <- isVisited target
        let new = joinPointAbstractions dom old assignment
        case haveVisited && equalPointAbstractions dom old new of
          True -> return S.empty
          False -> do
            markVisited target
            isFuncAbstr %= (faEntryRegs . ixF idx .~ new)
            return (S.singleton (Some target))
  
  markVisited :: BlockID blocks ctx -> M dom blocks ret ()
  markVisited bid = do
    processedOnce %= S.insert (Some bid)
  
  isVisited :: BlockID blocks ctx -> M dom blocks ret Bool
  isVisited bid = do
    s <- St.gets _processedOnce
    return (Some bid `S.member` s)
  
  -- | Compute a fixed point via abstract interpretation over a control
  -- flow graph ('CFG') given 1) an interpretation + domain, 2) initial
  -- assignments of domain values to global variables, and 3) initial
  -- assignments of domain values to function arguments.
  --
  -- This is an intraprocedural analysis.  To handle function calls, the
  -- transfer function for call statements must know how to supply
  -- summaries or compute an appropriate conservative approximation.
  --
  -- There are two results from the fixed point computation:
  --
  -- 1) For each block in the CFG, the abstraction computed at the *entry* to the block
  --
  -- 2) For each block in the CFG, the abstraction computed at the
  -- *exit* from the block. The 'PU.Assignment' for these "exit"
  -- abstractions ignores the @ctx@ index on the blocks, since that
  -- context is for *entry* to the blocks.
  --
  -- 3) The final abstract value for the value returned by the function
  forwardFixpoint' :: forall ext dom blocks ret init
                   . Domain dom
                  -- ^ The domain of abstract values
                  -> Interpretation ext dom
                  -- ^ The transfer functions for each statement type
                  -> CFG ext blocks init ret
                  -- ^ The function to analyze
                  -> PM.MapF GlobalVar dom
                  -- ^ Assignments of abstract values to global variables at the function start
                  -> PU.Assignment dom init
                  -- ^ Assignments of abstract values to the function arguments
                  -> ( PU.Assignment (PointAbstraction blocks dom) blocks
                     , PU.Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
                     , dom ret )
  forwardFixpoint' dom interp cfg globals0 assignment0 =
    let BlockID idx = cfgEntryBlockID cfg
        pa0 = PointAbstraction { _paGlobals = globals0
                               , _paRegisters = assignment0
                               , _paRefs = PM.empty
                               , _paRegisterRefs = PU.fmapFC (const emptyRefSet) assignment0
                               }
        freshAssignment :: PU.Index blocks ctx -> PointAbstraction blocks dom ctx
        freshAssignment i =
          PointAbstraction { _paRegisters = PU.fmapFC (const (domBottom dom)) (blockInputs (getBlock (BlockID i) (cfgBlockMap cfg)))
                           , _paRegisterRefs = PU.fmapFC (const emptyRefSet) (blockInputs (getBlock (BlockID i) (cfgBlockMap cfg)))
                           , _paGlobals = PM.empty
                           , _paRefs = PM.empty
                           }
        emptyFreshAssignment :: PU.Index blocks ctx -> Ignore (Some (PointAbstraction blocks dom)) ctx
        emptyFreshAssignment _i =
          Ignore (Some (PointAbstraction { _paRegisters = PU.empty
                                         , _paGlobals = PM.empty
                                         , _paRefs = PM.empty
                                         , _paRegisterRefs = PU.empty
                                         }))
        s0 = IterationState { _isRetAbstr = domBottom dom
                            , _isFuncAbstr =
                              FunctionAbstraction { _faEntryRegs =
                                                      PU.generate (PU.size (cfgBlockMap cfg)) freshAssignment
                                                        & ixF idx .~ pa0
                                                  , _faExitRegs = PU.generate (PU.size (cfgBlockMap cfg)) emptyFreshAssignment
                                                  , _faRet = domBottom dom
                                                  }
                            , _processedOnce = S.empty
                            }
        iterStrat = iterationStrategy dom
        abstr' = St.execState (runM (iterStrat interp cfg)) s0
    in ( _faEntryRegs (_isFuncAbstr abstr')
       , _faExitRegs (_isFuncAbstr abstr')
       , _isRetAbstr abstr' )
  
  -- Preserve old interface for now; fix tests later if my generalization is the right one.
  forwardFixpoint :: forall ext dom blocks ret init
                  . Domain dom
                  -> Interpretation ext dom
                  -> CFG ext blocks init ret
                  -> PM.MapF GlobalVar dom
                  -> PU.Assignment dom init
                  -> (PU.Assignment (PointAbstraction blocks dom) blocks, dom ret)
  forwardFixpoint dom interp cfg globals0 assignment0 =
    let (ass, _, ret) = forwardFixpoint' dom interp cfg globals0 assignment0
    in (ass, ret)
  
  -- | Inspect the 'Domain' definition to determine which iteration
  -- strategy the caller requested.
  iterationStrategy :: Domain dom -> (Interpretation ext dom -> CFG ext blocks init ret -> M dom blocks ret ())
  iterationStrategy dom =
    case domIter dom of
      WTOWidening s op -> wtoIteration (Just (WideningStrategy s, WideningOperator op)) dom
      WTO -> wtoIteration Nothing dom
      Worklist -> worklistIteration dom
  
  -- | Iterate over blocks using a worklist (i.e., after a block is
  -- processed and abstract values change, put the block successors on
  -- the worklist).
  --
  -- The worklist is actually processed by taking the lowest-numbered
  -- block in a set as the next work item.
  worklistIteration :: forall ext dom blocks ret init
                     . Domain dom
                    -> Interpretation ext dom
                    -> CFG ext blocks init ret
                    -> M dom blocks ret ()
  worklistIteration dom interp cfg =
    loop (S.singleton (Some (cfgEntryBlockID cfg)))
    where
      loop worklist =
        case S.minView worklist of
          Nothing -> return ()
          Just (Some target@(BlockID idx), worklist') -> do
            assignment <- lookupAssignment idx
            visit (getBlock target (cfgBlockMap cfg)) assignment worklist'
  
      visit :: Block ext blocks ret ctx
            -> PointAbstraction blocks dom ctx
            -> S.Set (Some (BlockID blocks))
            -> M dom blocks ret ()
      visit blk startingAssignment worklist' = do
        s <- transfer dom interp (cfgReturnType cfg) blk startingAssignment
        loop (S.union s worklist')
  
  -- | Iterate over the blocks in the control flow graph in weak
  -- topological order until a fixed point is reached.
  --
  -- The weak topological order essentially formalizes the idea of
  -- breaking the graph on back edges and putting the result in
  -- topological order.  The blocks that serve as loop heads are the
  -- heads of their respective strongly connected components.  Those
  -- block heads are suitable locations to apply widening operators
  -- (which can be provided to this iterator).
  wtoIteration :: forall ext dom blocks ret init
                . Maybe (WideningStrategy, WideningOperator dom)
                -- ^ An optional widening operator
               -> Domain dom
               -> Interpretation ext dom
               -> CFG ext blocks init ret
               -> M dom blocks ret ()
  wtoIteration mWiden dom interp cfg = loop (cfgWeakTopologicalOrdering cfg)
    where
      loop [] = return ()
      loop (Vertex (Some bid@(BlockID idx)) : rest) = do
        assignment <- lookupAssignment idx
        let blk = getBlock bid (cfgBlockMap cfg)
        _ <- transfer dom interp (cfgReturnType cfg) blk assignment
        loop rest
      loop (SCC (SCCData { wtoHead = hbid, wtoComps = comps }) : rest) = do
        processSCC hbid comps 0
        loop rest
  
      -- Process a single SCC until the input to the head node of the
      -- SCC stabilizes.  Applies widening if requested.
      processSCC (Some hbid@(BlockID idx)) comps iterNum = do
        headInput0 <- lookupAssignment idx
        -- We process the SCC until the input to the head of the SCC stabilizes
        let headBlock = getBlock hbid (cfgBlockMap cfg)
        _ <- transfer dom interp (cfgReturnType cfg) headBlock headInput0
        loop comps
        headInput1 <- lookupAssignment idx
        case equalPointAbstractions dom headInput0 headInput1 of
          True -> return ()
          False -> do
            case mWiden of
              -- TODO(conathan): figure out if we need to do something
              -- here with 'faExitRegs'?
              Just (WideningStrategy strat, WideningOperator widen)
                | strat iterNum -> do
                    -- TODO: is unionRefSets the right thing below?
                    let headInputW = zipPAWith widen unionRefSets headInput0 headInput1
                    isFuncAbstr %= (faEntryRegs . ixF idx .~ headInputW)
              _ -> return ()
            processSCC (Some hbid) comps (iterNum + 1)
  
  lookupAssignment :: forall dom blocks ret tp
                    . PU.Index blocks tp
                   -> M dom blocks ret (PointAbstraction blocks dom tp)
  lookupAssignment idx = do
    abstr <- St.get
    return ((abstr ^. isFuncAbstr . faEntryRegs) PU.! idx)
  
  lookupRegRefs :: Reg ctx tp -> PointAbstraction blocks dom ctx -> RefSet blocks tp
  lookupRegRefs reg assignment = (assignment ^. paRegisterRefs) PU.! regIndex reg
  
  -- | Turn a non paramaterized type into a parameterized type.
  --
  -- For when you want to use a @parameterized-utils@ style data
  -- structure with a type that doesn't have a parameter.
  --
  -- The same definition as 'Control.Applicative.Const', but with a
  -- different 'Show' instance.
  newtype Ignore a (b::k) = Ignore { _ignoreOut :: a }
   deriving (Eq, Ord)
  
  instance Show a => Show (Ignore a tp) where
    show (Ignore x) = show x
  
  instance Show a => ShowF (Ignore a)
  
  -- Lenses
  
  paGlobals :: (Functor f)
            => (PM.MapF GlobalVar dom -> f (PM.MapF GlobalVar dom))
            -> PointAbstraction blocks dom ctx
            -> f (PointAbstraction blocks dom ctx)
  paGlobals f pa = (\a -> pa { _paGlobals = a }) <$> f (_paGlobals pa)
  
  paRegisters :: (Functor f)
              => (PU.Assignment dom ctx -> f (PU.Assignment dom ctx))
              -> PointAbstraction blocks dom ctx
              -> f (PointAbstraction blocks dom ctx)
  paRegisters f pa = (\a -> pa { _paRegisters = a }) <$> f (_paRegisters pa)
  
  paRegisterRefs :: (Functor f)
                 => (PU.Assignment (RefSet blocks) ctx -> f (PU.Assignment (RefSet blocks) ctx))
                 -> PointAbstraction blocks dom ctx
                 -> f (PointAbstraction blocks dom ctx)
  paRegisterRefs f pa = (\a -> pa { _paRegisterRefs = a }) <$> f (_paRegisterRefs pa)
  
  paRefs :: (Functor f)
         => (PM.MapF (RefStmtId blocks) dom -> f (PM.MapF (RefStmtId blocks) dom))
         -> PointAbstraction blocks dom ctx
         -> f (PointAbstraction blocks dom ctx)
  paRefs f pa = (\a -> pa { _paRefs = a }) <$> f (_paRefs pa)
  
  faEntryRegs :: (Functor f)
              => (PU.Assignment (PointAbstraction blocks dom) blocks -> f (PU.Assignment (PointAbstraction blocks dom) blocks))
              -> FunctionAbstraction dom blocks ret
              -> f (FunctionAbstraction dom blocks ret)
  faEntryRegs f fa = (\a -> fa { _faEntryRegs = a }) <$> f (_faEntryRegs fa)
  
  faExitRegs :: (Functor f)
             => (PU.Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks -> f (PU.Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks))
             -> FunctionAbstraction dom blocks ret
             -> f (FunctionAbstraction dom blocks ret)
  faExitRegs f fa = (\a -> fa { _faExitRegs = a }) <$> f (_faExitRegs fa)
  
  isFuncAbstr :: (Functor f)
              => (FunctionAbstraction dom blocks ret -> f (FunctionAbstraction dom blocks ret))
              -> IterationState dom blocks ret
              -> f (IterationState dom blocks ret)
  isFuncAbstr f is = (\a -> is { _isFuncAbstr = a }) <$> f (_isFuncAbstr is)
  
  isRetAbstr :: (Functor f) => (dom ret -> f (dom ret)) -> IterationState dom blocks ret -> f (IterationState dom blocks ret)
  isRetAbstr f is = (\a -> is { _isRetAbstr = a }) <$> f (_isRetAbstr is)
  
  processedOnce :: (Functor f)
                => (S.Set (Some (BlockID blocks)) -> f (S.Set (Some (BlockID blocks))))
                -> IterationState dom blocks ret
                -> f (IterationState dom blocks ret)
  processedOnce f is = (\a -> is { _processedOnce = a}) <$> f (_processedOnce is)
  
  -- $pointed
  --
  -- The 'Pointed' type is a wrapper around another 'Domain' that
  -- provides distinguished 'Top' and 'Bottom' elements.  Use of this
  -- type is never required (domains can always define their own top and
  -- bottom), but this1 wrapper can save some boring boilerplate.
  
  -- | The Pointed wrapper that adds Top and Bottom elements
  data Pointed dom (tp :: CrucibleType) where
    Top :: Pointed a tp
    Pointed :: dom tp -> Pointed dom tp
    Bottom :: Pointed dom tp
  
  deriving instance (Eq (dom tp)) => Eq (Pointed dom tp)
  
  instance ShowF dom => Show (Pointed dom tp) where
    show Top = "Top"
    show Bottom = "Bottom"
    show (Pointed p) = showF p
  
  instance ShowF dom => ShowF (Pointed dom)
  
  -- | Construct a 'Pointed' 'Domain' from a pointed join function and
  -- an equality test.
  pointed :: (forall tp . dom tp -> dom tp -> Pointed dom tp)
          -- ^ Join of contained domain elements
          -> (forall tp . dom tp -> dom tp -> Bool)
          -- ^ Equality for domain elements
          -> IterationStrategy (Pointed dom)
          -> Domain (Pointed dom)
  pointed j eq iterStrat =
    Domain { domTop = Top
           , domBottom = Bottom
           , domJoin = pointedJoin j
           , domEq = pointedEq eq
             -- TODO(conathan): test faExitRegs computation with WTO
             -- strategy. It was hardcoded to 'WTO' here before conathan
             -- added block-exit point abstractions.
           , domIter = iterStrat
           }
  
    where
      pointedJoin _ Top _ = Top
      pointedJoin _ _ Top = Top
      pointedJoin _ Bottom a = a
      pointedJoin _ a Bottom = a
      pointedJoin j' (Pointed p1) (Pointed p2) = j' p1 p2
  
      pointedEq _ Top Top = True
      pointedEq _ Bottom Bottom = True
      pointedEq eq' (Pointed p1) (Pointed p2) = eq' p1 p2
      pointedEq _ _ _ = False
  