Core.hs

{- |
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 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 Lens.Micro ((^.), Lens', lens)
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 :: 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)
         , cfgCutpoints :: !(Bimap CutpointName (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