content: {- |
  Module           : Lang.Crucible.CFG.Core
  Description      : SSA-based control flow graphs
  Copyright        : (c) Galois, Inc 2014-2016
  License          : BSD3
  Maintainer       : Joe Hendrix <jhendrix@galois.com>
  
  Define a SSA-based control flow graph data structure using a side-effect free
  expression syntax.
  
  Unlike usual SSA forms, we do not use phi-functions, but instead rely on an
  argument-passing formulation for basic blocks.  In this form, concrete values
  are bound to formal parameters instead of using phi-functions that switch
  on the place from which you jumped.
  -}
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE InstanceSigs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE ParallelListComp #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  module Lang.Crucible.CFG.Core
    ( -- * CFG
      CFG(..)
    , SomeCFG(..)
    , HasSomeCFG(..)
    , AnyCFG(..)
    , ppCFG
    , ppCFG'
    , cfgArgTypes
    , cfgReturnType
    , CFGPostdom
  
      -- * Blocks
    , BlockMap
    , getBlock
    , extendBlockMap
  
    , BlockID(..)
    , extendBlockID
    , extendBlockID'
  
    , Block(..)
    , blockLoc
    , blockStmts
    , withBlockTermStmt
    , nextBlocks
  
      -- * Jump targets
    , JumpTarget(..)
    , extendJumpTarget
    , jumpTargetID
    , SwitchTarget(..)
    , switchTargetID
    , extendSwitchTarget
  
      -- * Statements
    , StmtSeq(..)
    , firstStmtLoc
    , stmtSeqTermStmt
    , Stmt(..)
    , ppStmt
    , nextStmtHeight
  
    , applyEmbeddingStmt
  
    , TermStmt(..)
    , termStmtNextBlocks
  
      -- * Expressions
    , Expr(..)
    , Reg(..)
    , extendReg
    , lastReg
  
      -- * Re-exports
    , module Lang.Crucible.Types
    , module Lang.Crucible.CFG.Common
    , module Data.Parameterized.Classes
    , module Data.Parameterized.Some
    ) where
  
  import Control.Applicative
  import Control.Lens
  import Data.Bimap (Bimap)
  import Data.Maybe (fromMaybe)
  import Data.Kind (Type)
  import Data.Parameterized.Classes
  import Data.Parameterized.Map (Pair(..))
  import Data.Parameterized.Some
  import Data.Parameterized.TraversableFC
  import Data.String
  import Prettyprinter
  
  import What4.ProgramLoc
  import What4.Symbol
  
  import Lang.Crucible.CFG.Common
  import Lang.Crucible.CFG.Expr
  import Lang.Crucible.FunctionHandle
  import Lang.Crucible.Types
  import Lang.Crucible.Utils.PrettyPrint
  
  #ifdef UNSAFE_OPS
  -- We deliberately import Context.Unsafe as it is the only one that supports
  -- the unsafe coerces between an index and its extension.
  import Data.Parameterized.Context as Ctx hiding (Assignment)
  import Data.Parameterized.Context.Unsafe as Ctx (Assignment)
  import Unsafe.Coerce
  #else
  import Data.Parameterized.Context as Ctx
  #endif
  
  ------------------------------------------------------------------------
  -- Reg
  
  -- | A temporary register identifier introduced during translation.
  --   These are unique to the current function.  The `ctx` parameter
  --   is a context containing the types of all the temporary registers
  --   currently in scope, and the `tp` parameter indicates the type
  --   of this register (which necessarily appears somewhere in `ctx`)
  newtype Reg (ctx :: Ctx CrucibleType) (tp :: CrucibleType) = Reg { regIndex :: Ctx.Index ctx tp }
    deriving (Eq, TestEquality, Ord, OrdF)
  
  instance Show (Reg ctx tp) where
    show (Reg i) = '$' : show (indexVal i)
  
  instance ShowF (Reg ctx)
  
  instance Pretty (Reg ctx tp) where
    pretty (Reg i) = pretty '$' <> pretty (indexVal i)
  
  instance ApplyEmbedding' Reg where
    applyEmbedding' ctxe r = Reg $ applyEmbedding' ctxe (regIndex r)
  
  instance ExtendContext' Reg where
    extendContext' diff r = Reg $ extendContext' diff (regIndex r)
  
  -- | Finds the value of the most-recently introduced register in scope.
  lastReg :: KnownContext ctx => Reg (ctx ::> tp) tp
  lastReg = Reg (nextIndex knownSize)
  
  -- | Extend the set of registers in scope for a given register value
  --   without changing its index or type.
  extendReg :: Reg ctx tp -> Reg (ctx ::> r) tp
  extendReg = Reg . extendIndex . regIndex
  
  ------------------------------------------------------------------------
  -- Expr
  
  -- | An expression is just an App applied to some registers.
  newtype Expr ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType)
        = App (App ext (Reg ctx) tp)
  
  instance IsString (Expr ext ctx (StringType Unicode)) where
    fromString  = App . StringLit . fromString
  
  instance PrettyApp (ExprExtension ext) => Pretty (Expr ext ctx tp) where
    pretty (App a) = ppApp pretty a
  
  ppAssignment :: Assignment (Reg ctx) args -> [Doc ann]
  ppAssignment = toListFC pretty
  
  instance ( TraversableFC (ExprExtension ext)
           ) => ApplyEmbedding' (Expr ext) where
    applyEmbedding' ctxe (App e) = App (mapApp (applyEmbedding' ctxe) e)
  
  instance ( TraversableFC (ExprExtension ext)
           ) => ExtendContext' (Expr ext) where
    extendContext' diff (App e) = App (mapApp (extendContext' diff) e)
  
  ------------------------------------------------------------------------
  -- BlockID
  
  -- | A `BlockID` uniquely identifies a block in a control-flow graph.
  --   Each block has an associated context, indicating the formal arguments
  --   it expects to find in registers from its calling locations.
  newtype BlockID (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType)
        = BlockID { blockIDIndex :: Ctx.Index blocks tp }
    deriving (Eq, Ord)
  
  instance TestEquality (BlockID blocks) where
    testEquality (BlockID x) (BlockID y) = testEquality x y
  
  instance OrdF (BlockID blocks) where
    compareF (BlockID x) (BlockID y) = compareF x y
  
  instance Pretty (BlockID blocks tp) where
    pretty (BlockID i) = pretty '%' <> pretty (indexVal i)
  
  instance Show (BlockID blocks ctx) where
    show (BlockID i) = '%' : show (indexVal i)
  
  instance ShowF (BlockID blocks)
  
  extendBlockID :: KnownDiff l r => BlockID l tp -> BlockID r tp
  extendBlockID = BlockID . extendIndex . blockIDIndex
  
  extendBlockID' :: Diff l r -> BlockID l tp -> BlockID r tp
  extendBlockID' e = BlockID . extendIndex' e . blockIDIndex
  
  ------------------------------------------------------------------------
  -- JumpTarget
  
  -- | Target for jump and branch statements
  data JumpTarget blocks ctx where
       JumpTarget :: !(BlockID blocks args)            -- BlockID to jump to
                  -> !(CtxRepr args)                   -- expected argument types
                  -> !(Assignment (Reg ctx) args) -- jump target actual arguments
                  -> JumpTarget blocks ctx
  
  instance Pretty (JumpTarget blocks ctx) where
    pretty (JumpTarget tgt _ a) = pretty tgt <> parens (commas (ppAssignment a))
  
  jumpTargetID :: JumpTarget blocks ctx -> Some (BlockID blocks)
  jumpTargetID (JumpTarget tgt _ _) = Some tgt
  
  extendJumpTarget :: Diff blocks' blocks -> JumpTarget blocks' ctx -> JumpTarget blocks ctx
  extendJumpTarget diff (JumpTarget b tps a) = JumpTarget (extendBlockID' diff b) tps a
  
  instance ApplyEmbedding (JumpTarget blocks) where
    applyEmbedding ctxe (JumpTarget dest tys args) =
      JumpTarget dest tys (fmapFC (applyEmbedding' ctxe) args)
  
  instance ExtendContext (JumpTarget blocks) where
    extendContext diff (JumpTarget dest tys args) =
      JumpTarget dest tys (fmapFC (extendContext' diff) args)
  
  ------------------------------------------------------------------------
  -- SwitchTarget
  
  -- | Target for a switch statement.
  data SwitchTarget blocks ctx tp where
    SwitchTarget :: !(BlockID blocks (args ::> tp))   -- BlockID to jump to
                 -> !(CtxRepr args)                   -- expected argument types
                 -> !(Assignment (Reg ctx) args) -- switch target actual arguments
                 -> SwitchTarget blocks ctx tp
  
  switchTargetID :: SwitchTarget blocks ctx tp -> Some (BlockID blocks)
  switchTargetID (SwitchTarget tgt _ _) = Some tgt
  
  ppCase :: String -> SwitchTarget blocks ctx tp -> Doc ann
  ppCase nm (SwitchTarget tgt _ a) =
    pretty nm <+> pretty "->" <+> pretty tgt <> parens (commas (ppAssignment a))
  
  extendSwitchTarget :: Diff blocks' blocks
                     -> SwitchTarget blocks' ctx tp
                     -> SwitchTarget blocks ctx tp
  extendSwitchTarget diff (SwitchTarget b tps a) =
      SwitchTarget (extendBlockID' diff b) tps a
  
  instance ApplyEmbedding' (SwitchTarget blocks) where
    applyEmbedding' ctxe (SwitchTarget dest tys args) =
      SwitchTarget dest tys (fmapFC (applyEmbedding' ctxe) args)
  
  instance ExtendContext' (SwitchTarget blocks) where
    extendContext' diff (SwitchTarget dest tys args) =
      SwitchTarget dest tys (fmapFC (extendContext' diff) args)
  
  
  ------------------------------------------------------------------------
  -- Stmt
  
  -- | A sequential statement that does not affect the
  -- program location within the current block or leave the current
  -- block.
  data Stmt ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) where
    -- Assign the value of a register
    SetReg :: !(TypeRepr tp)
           -> !(Expr ext ctx tp)
           -> Stmt ext ctx (ctx ::> tp)
  
    -- Assign a register via an extension statement
    ExtendAssign :: !(StmtExtension ext (Reg ctx) tp)
                 -> Stmt ext ctx (ctx ::> tp)
  
    -- Statement used for evaluating function calls
    CallHandle :: !(TypeRepr ret)                          -- The type of the return value(s)
               -> !(Reg ctx (FunctionHandleType args ret)) -- The function handle to call
               -> !(CtxRepr args)                          -- The expected types of the arguments
               -> !(Assignment (Reg ctx) args)             -- The actual arguments to the call
               -> Stmt ext ctx (ctx ::> ret)
  
    -- Print a message out to the console
    Print :: !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
  
    -- Read a global variable.
    ReadGlobal :: !(GlobalVar tp)
               -> Stmt ext ctx (ctx ::> tp)
  
    -- Write to a global variable.
    WriteGlobal :: !(GlobalVar tp)
                -> !(Reg ctx tp)
                -> Stmt ext ctx ctx
  
    -- Create a fresh constant
    FreshConstant :: !(BaseTypeRepr bt)
                  -> !(Maybe SolverSymbol)
                  -> Stmt ext ctx (ctx ::> BaseToType bt)
  
    -- Create a fresh floating-point constant
    FreshFloat :: !(FloatInfoRepr fi)
               -> !(Maybe SolverSymbol)
               -> Stmt ext ctx (ctx ::> FloatType fi)
  
    -- Create a fresh natural number constant
    FreshNat :: !(Maybe SolverSymbol)
             -> Stmt  ext ctx (ctx ::> NatType)
  
    -- Allocate a new reference cell
    NewRefCell :: !(TypeRepr tp)
               -> !(Reg ctx tp)
               -> Stmt ext ctx (ctx ::> ReferenceType tp)
  
    -- Allocate a new, unassigned reference cell
    NewEmptyRefCell :: !(TypeRepr tp)
                    -> Stmt ext ctx (ctx ::> ReferenceType tp)
  
    -- Read the current value of a reference cell
    ReadRefCell :: !(Reg ctx (ReferenceType tp))
                -> Stmt ext ctx (ctx ::> tp)
  
    -- Write the current value of a reference cell
    WriteRefCell :: !(Reg ctx (ReferenceType tp))
                 -> !(Reg ctx tp)
                 -> Stmt ext ctx ctx
  
    -- Deallocate the storage associated with a reference cell
    DropRefCell  :: !(Reg ctx (ReferenceType tp))
                 -> Stmt ext ctx ctx
  
    -- Assert a boolean condition.  If the condition fails, print the given string.
    Assert :: !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
  
    -- Assume a boolean condition, remembering the given string as the 'reason' for this assumption.
    Assume :: !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
  
  ------------------------------------------------------------------------
  -- TermStmt
  
  data TermStmt blocks (ret :: CrucibleType) (ctx :: Ctx CrucibleType) where
    -- Jump to the given jump target
    Jump :: !(JumpTarget blocks ctx)
         -> TermStmt blocks ret ctx
  
    -- Branch on condition.  If true, jump to the first jump target; otherwise
    -- jump to the second jump target.
    Br :: !(Reg ctx BoolType)
       -> !(JumpTarget blocks ctx)
       -> !(JumpTarget blocks ctx)
       -> TermStmt blocks ret ctx
  
    -- Switch on whether this is a maybe value.  Jump to the switch target if
    -- the maybe value is a "Some".  Otherwise (if "Nothing"), jump to the jump target.
    MaybeBranch :: !(TypeRepr tp)
                -> !(Reg ctx (MaybeType tp))
                -> !(SwitchTarget blocks ctx tp)
                -> !(JumpTarget blocks ctx)
                -> TermStmt blocks rtp ctx
  
    -- Switch on a variant value.  Examine the tag of the variant
    -- and jump to the appropriate switch target.
    VariantElim :: !(CtxRepr varctx)
                -> !(Reg ctx (VariantType varctx))
                -> !(Assignment (SwitchTarget blocks ctx) varctx)
                -> TermStmt blocks ret ctx
  
    -- Return from function, providing the return value(s).
    Return :: !(Reg ctx ret)
           -> TermStmt blocks ret ctx
  
    -- End block with a tail call.
    TailCall :: !(Reg ctx (FunctionHandleType args ret))
             -> !(CtxRepr args)
             -> !(Assignment (Reg ctx) args)
             -> TermStmt blocks ret ctx
  
    -- Block ends with an error.
    ErrorStmt :: !(Reg ctx (StringType Unicode)) -> TermStmt blocks ret ctx
  
  #ifndef UNSAFE_OPS
  extendTermStmt :: Diff blocks' blocks -> TermStmt blocks' ret ctx -> TermStmt blocks ret ctx
  extendTermStmt diff (Jump tgt) = Jump (extendJumpTarget diff tgt)
  extendTermStmt diff (Br c x y) = Br c (extendJumpTarget diff x) (extendJumpTarget diff y)
  extendTermStmt diff (MaybeBranch tp c x y) =
    MaybeBranch tp c (extendSwitchTarget diff x) (extendJumpTarget diff y)
  extendTermStmt diff (VariantElim ctx e asgn) =
    VariantElim ctx e (fmapFC (extendSwitchTarget diff) asgn)
  extendTermStmt _diff (Return e) = Return e
  extendTermStmt _diff (TailCall h tps args) = TailCall h tps args
  extendTermStmt _diff (ErrorStmt e) = ErrorStmt e
  #endif
  
  -- | Return the set of possible next blocks from a TermStmt
  termStmtNextBlocks :: TermStmt b ret ctx -> Maybe [Some (BlockID b)]
  termStmtNextBlocks s0 =
    case s0 of
      Jump tgt             -> Just [ jumpTargetID tgt ]
      Br          _ x y    -> Just [ jumpTargetID x, jumpTargetID y ]
      MaybeBranch _ _ x y  -> Just [ switchTargetID x, jumpTargetID y ]
      VariantElim _ _ a    -> Just (toListFC switchTargetID a)
      Return      _        -> Nothing
      TailCall    _ _ _    -> Nothing
      ErrorStmt   _        -> Just []
  
  instance Pretty (TermStmt blocks ret ctx) where
   pretty s =
    case s of
      Jump b   -> pretty "jump" <+> pretty b
      Br e x y -> pretty "br"  <+> pretty e <+> pretty x <+> pretty y
      MaybeBranch _ e j n ->
        vcat
        [ pretty "maybeBranch" <+> pretty e <+> lbrace
        , indent 2 $
            vcat [ ppCase "Just" j
                 , pretty "Nothing ->" <+> pretty n
                 , rbrace
                 ]
        ]
      VariantElim _ e asgn ->
        let branches =
                [ f (show i) <> semi
                | i <- [(0::Int) .. ]
                | f <- toListFC (\tgt nm -> ppCase nm tgt) asgn
                ] in
        vcat
        [ pretty "vswitch" <+> pretty e <+> lbrace
        , indent 2 (vcat branches)
        , rbrace
        ]
      Return e ->
        pretty "return"
         <+> pretty e
      TailCall h _ args ->
        pretty "tailCall"
         <+> pretty h
         <+> parens (commas (ppAssignment args))
      ErrorStmt msg ->
        pretty "error" <+> pretty msg
  
  
  applyEmbeddingStmt :: forall ext ctx ctx' sctx.
                        TraverseExt ext =>
                        CtxEmbedding ctx ctx' ->
                        Stmt ext ctx sctx ->
                        Pair (Stmt ext ctx') (CtxEmbedding sctx)
  applyEmbeddingStmt ctxe stmt =
    case stmt of
      SetReg tp e -> Pair (SetReg tp (applyEmbedding' ctxe e))
                          (extendEmbeddingBoth ctxe)
  
      ExtendAssign estmt ->
         Pair (ExtendAssign (fmapFC (Ctx.applyEmbedding' ctxe) estmt))
              (Ctx.extendEmbeddingBoth ctxe)
  
      CallHandle ret hdl tys args ->
        Pair (CallHandle ret (reg hdl) tys (fmapFC reg args))
             (extendEmbeddingBoth ctxe)
  
      Print str -> Pair (Print (reg str)) ctxe
  
      ReadGlobal var -> Pair (ReadGlobal var)
                             (extendEmbeddingBoth ctxe)
  
      WriteGlobal var r -> Pair (WriteGlobal var (reg r)) ctxe
  
      FreshConstant bt nm -> Pair (FreshConstant bt nm)
                                  (Ctx.extendEmbeddingBoth ctxe)
  
      FreshFloat fi nm -> Pair (FreshFloat fi nm)
                               (Ctx.extendEmbeddingBoth ctxe)
  
      FreshNat nm -> Pair (FreshNat nm) (Ctx.extendEmbeddingBoth ctxe)
  
      NewRefCell tp r -> Pair (NewRefCell tp (reg r))
                              (Ctx.extendEmbeddingBoth ctxe)
      NewEmptyRefCell tp -> Pair (NewEmptyRefCell tp)
                                 (Ctx.extendEmbeddingBoth ctxe)
      ReadRefCell r     -> Pair (ReadRefCell (reg r))
                                (Ctx.extendEmbeddingBoth ctxe)
      WriteRefCell r r' -> Pair (WriteRefCell (reg r) (reg r')) ctxe
      DropRefCell r     -> Pair (DropRefCell (reg r)) ctxe
      Assert b str      -> Pair (Assert (reg b) (reg str)) ctxe
      Assume b str      -> Pair (Assume (reg b) (reg str)) ctxe
    where
      reg :: forall tp. Reg ctx tp -> Reg ctx' tp
      reg = applyEmbedding' ctxe
  
  
  instance ApplyEmbedding (TermStmt blocks ret) where
    applyEmbedding :: forall ctx ctx'.
                      CtxEmbedding ctx ctx'
                      -> TermStmt blocks ret ctx
                      -> TermStmt blocks ret ctx'
    applyEmbedding ctxe term =
      case term of
        Jump jt -> Jump (apC jt)
        Br b jtl jtr -> Br (apC' b) (apC jtl) (apC jtr)
        MaybeBranch tp b swt jt    -> MaybeBranch tp (apC' b) (apC' swt) (apC jt)
        VariantElim repr r targets -> VariantElim repr (apC' r) (fmapFC apC' targets)
        Return r -> Return (apC' r)
        TailCall hdl tys args -> TailCall (apC' hdl) tys (fmapFC apC' args)
        ErrorStmt r -> ErrorStmt (apC' r)
      where
        apC' :: forall f v. ApplyEmbedding' f => f ctx v -> f ctx' v
        apC' = applyEmbedding' ctxe
  
        apC :: forall f. ApplyEmbedding  f => f ctx -> f ctx'
        apC  = applyEmbedding  ctxe
  
  instance ExtendContext (TermStmt blocks ret) where
    extendContext :: forall ctx ctx'.
                      Diff ctx ctx'
                      -> TermStmt blocks ret ctx
                      -> TermStmt blocks ret ctx'
    extendContext diff term =
      case term of
        Jump jt -> Jump (extC jt)
        Br b jtl jtr -> Br (extC' b) (extC jtl) (extC jtr)
        MaybeBranch tp b swt jt    -> MaybeBranch tp (extC' b) (extC' swt) (extC jt)
        VariantElim repr r targets -> VariantElim repr (extC' r) (fmapFC extC' targets)
        Return r -> Return (extC' r)
        TailCall hdl tys args -> TailCall (extC' hdl) tys (fmapFC extC' args)
        ErrorStmt r -> ErrorStmt (extC' r)
      where
        extC' :: forall f v. ExtendContext' f => f ctx v -> f ctx' v
        extC' = extendContext' diff
  
        extC :: forall f. ExtendContext  f => f ctx -> f ctx'
        extC  = extendContext  diff
  
  
  ------------------------------------------------------------------------
  -- StmtSeq
  
  -- | A sequence of straight-line program statements that end with
  --   a terminating statement (return, jump, etc).
  data StmtSeq ext blocks (ret :: CrucibleType) ctx where
    ConsStmt :: !ProgramLoc
             -> !(Stmt ext ctx ctx')
             -> !(StmtSeq ext blocks ret ctx')
             -> StmtSeq ext blocks ret ctx
    TermStmt :: !ProgramLoc
             -> !(TermStmt blocks ret ctx)
             -> (StmtSeq ext blocks ret ctx)
  
  -- | Return the location of a statement.
  firstStmtLoc :: StmtSeq ext b r ctx -> ProgramLoc
  firstStmtLoc (ConsStmt pl _ _) = pl
  firstStmtLoc (TermStmt pl _) = pl
  
  -- | A lens-like operation that gives one access to program location and term statement,
  -- and allows the terminal statement to be replaced with an arbitrary sequence of
  -- statements.
  stmtSeqTermStmt :: Functor f
                  => (forall ctx
                      . (ProgramLoc, TermStmt b ret ctx)
                      -> f (StmtSeq ext b' ret ctx))
                  -> StmtSeq ext b ret args
                  -> f (StmtSeq ext b' ret args)
  stmtSeqTermStmt f (ConsStmt l s t) = ConsStmt l s <$> stmtSeqTermStmt f t
  stmtSeqTermStmt f (TermStmt p t) = f (p, t)
  
  ppReg :: Size ctx -> Doc ann
  ppReg h = pretty "$" <> pretty (sizeInt h)
  
  nextStmtHeight :: Size ctx -> Stmt ext ctx ctx' -> Size ctx'
  nextStmtHeight h s =
    case s of
      SetReg{} -> incSize h
      ExtendAssign{} -> incSize h
      CallHandle{} -> incSize h
      Print{} -> h
      ReadGlobal{} -> incSize h
      WriteGlobal{} -> h
      FreshConstant{} -> Ctx.incSize h
      FreshFloat{} -> Ctx.incSize h
      FreshNat{} -> Ctx.incSize h
      NewRefCell{} -> Ctx.incSize h
      NewEmptyRefCell{} ->Ctx.incSize h
      ReadRefCell{} -> Ctx.incSize h
      WriteRefCell{} -> h
      DropRefCell{}  -> h
      Assert{} -> h
      Assume{} -> h
  
  ppStmt :: PrettyExt ext => Size ctx -> Stmt ext ctx ctx' -> Doc ann
  ppStmt r s =
    case s of
      SetReg _ e -> ppReg r <+> pretty "=" <+> pretty e
      ExtendAssign s' -> ppReg r <+> pretty "=" <+> ppApp pretty s'
      CallHandle _ h _ args ->
        ppReg r <+> pretty "= call"
                <+> pretty h <> parens (commas (ppAssignment args))
                 <> pretty ";"
      Print msg -> ppFn "print" [ pretty msg ]
      ReadGlobal v -> pretty "read" <+> ppReg r <+> pretty v
      WriteGlobal v e -> pretty "write" <+> pretty v <+> pretty e
      -- TODO: replace viaShow once we have instance Pretty SolverSymbol
      FreshConstant bt nm -> ppReg r <+> pretty "=" <+> pretty "fresh" <+> pretty bt <+> maybe mempty viaShow nm
      FreshFloat fi nm -> ppReg r <+> pretty "=" <+> pretty "fresh-float" <+> pretty fi <+> maybe mempty viaShow nm
      FreshNat nm -> ppReg r <+> pretty "=" <+> pretty "fresh-nat" <+> maybe mempty viaShow nm
      NewRefCell _ e -> ppReg r <+> pretty "=" <+> ppFn "newref" [ pretty e ]
      NewEmptyRefCell tp -> ppReg r <+> pretty "=" <+> ppFn "emptyref" [ pretty tp ]
      ReadRefCell e -> ppReg r <+> pretty "= !" <> pretty e
      WriteRefCell r1 r2 -> pretty r1 <+> pretty ":=" <+> pretty r2
      DropRefCell r1 -> pretty "drop" <+> pretty r1
      Assert c e -> ppFn "assert" [ pretty c, pretty e ]
      Assume c e -> ppFn "assume" [ pretty c, pretty e ]
  
  prefixLineNum :: Bool -> ProgramLoc -> Doc ann -> Doc ann
  prefixLineNum True pl d = vcat [pretty "%" <+> ppNoFileName (plSourceLoc pl), d]
  prefixLineNum False _ d = d
  
  ppStmtSeq :: PrettyExt ext => Bool -> Size ctx -> StmtSeq ext blocks ret ctx -> Doc ann
  ppStmtSeq ppLineNum h (ConsStmt pl s r) =
    vcat
    [ prefixLineNum ppLineNum pl (ppStmt h s)
    , ppStmtSeq ppLineNum (nextStmtHeight h s) r
    ]
  ppStmtSeq ppLineNum _ (TermStmt pl s) =
    prefixLineNum ppLineNum pl (pretty s)
  
  
  #ifndef UNSAFE_OPS
  extendStmtSeq :: Diff blocks' blocks -> StmtSeq ext blocks' ret ctx -> StmtSeq ext blocks ret ctx
  extendStmtSeq diff (ConsStmt p s l) = ConsStmt p s (extendStmtSeq diff l)
  extendStmtSeq diff (TermStmt p s) = TermStmt p (extendTermStmt diff s)
  #endif
  
  
  instance TraverseExt ext => ApplyEmbedding (StmtSeq ext blocks ret) where
    applyEmbedding ctxe (ConsStmt loc stmt rest) =
      case applyEmbeddingStmt ctxe stmt of
        Pair stmt' ctxe' -> ConsStmt loc stmt' (applyEmbedding ctxe' rest)
    applyEmbedding ctxe (TermStmt loc term) =
      TermStmt loc (applyEmbedding ctxe term)
  
  
  
  ------------------------------------------------------------------------
  -- CFGPostdom
  
  -- | Postdominator information about a CFG.  The assignment maps each block
  --   to the postdominators of the given block.  The postdominators are ordered
  --   with nearest postdominator first.
  type CFGPostdom blocks = Assignment (Const [Some (BlockID blocks)]) blocks
  
  emptyCFGPostdomInfo :: Size blocks -> CFGPostdom blocks
  emptyCFGPostdomInfo sz = Ctx.replicate sz (Const [])
  
  
  ------------------------------------------------------------------------
  -- Block
  
  -- | A basic block within a function.
  data Block ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ctx
     = Block { blockID        :: !(BlockID blocks ctx)
               -- ^ The unique identifier of this block
             , blockInputs    :: !(CtxRepr ctx)
               -- ^ The expected types of the formal arguments to this block
             , _blockStmts    :: !(StmtSeq ext blocks ret ctx)
               -- ^ The sequence of statements in this block
             }
  
  blockStmts :: Simple Lens (Block ext b r c) (StmtSeq ext b r c)
  blockStmts = lens _blockStmts (\b s -> b { _blockStmts = s })
  
  -- | Return location of start of block.
  blockLoc :: Block ext blocks ret ctx -> ProgramLoc
  blockLoc b = firstStmtLoc (b^.blockStmts)
  
  -- | Get the terminal statement of a basic block.  This is implemented
  -- in a CPS style due to the block context.
  withBlockTermStmt :: Block ext blocks ret args
                    -> (forall ctx . ProgramLoc -> TermStmt blocks ret ctx -> r)
                    -> r
  withBlockTermStmt b f = getConst (stmtSeqTermStmt (Const . uncurry f) (b^.blockStmts))
  
  nextBlocks :: Block ext b r a -> [Some (BlockID b)]
  nextBlocks b =
    withBlockTermStmt b (\_ s -> fromMaybe [] (termStmtNextBlocks s))
  
  
  blockInputCount :: Block ext blocks ret ctx -> Size ctx
  blockInputCount b = size (blockInputs b)
  
  ppBlock :: PrettyExt ext
          => Bool
             -- ^ Print line numbers.
          -> Bool
             -- ^ Print block args. Note that you can infer the number
             -- of block args from the first SSA temp register assigned
             -- to in the block: if the block has @n@ args, then the
             -- first register it assigns to will be @$n@.
          -> Maybe (CFGPostdom blocks)
             -- ^ Optionally print postdom info.
          -> Block ext blocks ret ctx
             -- ^ Block to print.
          -> Doc ann
  ppBlock ppLineNumbers ppBlockArgs mPda b = do
    let stmts = ppStmtSeq ppLineNumbers (blockInputCount b) (b^.blockStmts)
    let mPostdom = flip fmap mPda $ \ pda ->
          let Const pd = pda ! blockIDIndex (blockID b)
          in if Prelude.null pd
             then pretty "% no postdom"
             else pretty "% postdom" <+> hsep (viewSome pretty <$> pd)
    let numArgs = lengthFC (blockInputs b)
    let argList = [ pretty '$' <> pretty n | n <- [0 .. numArgs-1] ]
    let args = encloseSep lparen rparen comma argList
    let block = pretty (blockID b) <>
                if ppBlockArgs then args else mempty
    let body = case mPostdom of
          Nothing -> stmts
          Just postdom -> vcat [stmts, postdom]
    vcat [block, indent 2 body]
  
  instance PrettyExt ext => Show (Block ext blocks ret args) where
    show blk = show $ ppBlock False False Nothing blk
  
  instance PrettyExt ext => ShowF (Block ext blocks ret)
  
  #ifndef UNSAFE_OPS
  extendBlock :: Block ext blocks ret ctx -> Block ext (blocks ::> new) ret ctx
  extendBlock b =
    Block { blockID = extendBlockID (blockID b)
          , blockInputs = blockInputs b
          , _blockStmts = extendStmtSeq knownDiff (b^.blockStmts)
          }
  #endif
  
  ------------------------------------------------------------------------
  -- BlockMap
  
  -- | A mapping from block indices to CFG blocks
  type BlockMap ext blocks ret = Assignment (Block ext blocks ret) blocks
  
  getBlock :: BlockID blocks args
           -> BlockMap ext blocks ret
           -> Block ext blocks ret args
  getBlock (BlockID i) m = m Ctx.! i
  
  extendBlockMap :: Assignment (Block ext blocks ret) b
                 -> Assignment (Block ext (blocks ::> args) ret) b
  #ifdef UNSAFE_OPS
  extendBlockMap = unsafeCoerce
  #else
  extendBlockMap = fmapFC extendBlock
  #endif
  ------------------------------------------------------------------------
  -- CFG
  
  -- | A CFG consists of:
  --
  -- * a function handle, uniquely identifying the function this CFG
  -- implements;
  --
  -- * a block map, representing the main CFG data structure;
  --
  -- * and the identifier of the function entry point.
  --
  -- The @blocks@ type parameter maps each block identifier to the
  -- formal arguments it expects.  The @init@ type parameter identifies
  -- the formal arguments of the function represented by this control-flow graph,
  -- which correspond to the formal arguments of the CFG entry point.
  -- The @ret@ type parameter indicates the return type of the function.
  data CFG (ext :: Type)
           (blocks :: Ctx (Ctx CrucibleType))
           (init :: Ctx CrucibleType)
           (ret :: CrucibleType)
     = CFG { cfgHandle :: FnHandle init ret
           , cfgBlockMap :: !(BlockMap ext blocks ret)
           , cfgEntryBlockID :: !(BlockID blocks init)
           , cfgBreakpoints :: !(Bimap BreakpointName (Some (BlockID blocks)))
           }
  
  cfgArgTypes :: CFG ext blocks init ret -> CtxRepr init
  cfgArgTypes g = handleArgTypes (cfgHandle g)
  
  cfgReturnType :: CFG ext blocks init ret -> TypeRepr ret
  cfgReturnType g = handleReturnType (cfgHandle g)
  
  -- | Class for types that embed a CFG of some sort.
  class HasSomeCFG f ext init ret | f -> ext, f -> init, f -> ret where
    getCFG :: f b -> SomeCFG ext init ret
  
  instance PrettyExt ext => Show (CFG ext blocks init ret) where
    show g = show (ppCFG True g)
  
  -- | Pretty print a CFG.
  ppCFG :: PrettyExt ext
        => Bool -- ^ Flag indicates if we should print line numbers
        -> CFG ext blocks init ret
        -> Doc ann
  ppCFG lineNumbers g = ppCFG' lineNumbers (emptyCFGPostdomInfo sz) g
    where sz = size (cfgBlockMap g)
  
  -- | Pretty print CFG with postdom information.
  ppCFG' :: PrettyExt ext
         => Bool -- ^ Flag indicates if we should print line numbers
         -> CFGPostdom blocks
         -> CFG ext blocks init ret
         -> Doc ann
  ppCFG' lineNumbers pdInfo g = vcat (toListFC (ppBlock lineNumbers blockArgs (Just pdInfo)) (cfgBlockMap g))
    where blockArgs = False
  
  -- | Control flow graph with some blocks.  This data type closes
  --   existentially over the @blocks@ type parameter.
  data SomeCFG ext (init :: Ctx CrucibleType) (ret :: CrucibleType) where
    SomeCFG :: CFG ext blocks init ret -> SomeCFG ext init ret
  
  instance PrettyExt ext => Show (SomeCFG ext i r)
    where show cfg = case cfg of SomeCFG c -> show c
  
  -- | Control flow graph.  This data type closes existentially
  --   over all the type parameters except @ext@.
  data AnyCFG ext where
    AnyCFG :: CFG ext blocks init ret
           -> AnyCFG ext
  
  instance PrettyExt ext => Show (AnyCFG ext) where
    show cfg = case cfg of AnyCFG c -> show c
  