{-|
Module      : Lang.Crucible.Simulator.OverrideSim
Description : The main simulation monad
Copyright   : (c) Galois, Inc 2014-2018
License     : BSD3
Maintainer  : Joe Hendrix <jhendrix@galois.com>

Define the main simulation monad 'OverrideSim' and basic operations on it.
-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.Simulator.OverrideSim
  ( -- * Monad definition
    OverrideSim(..)
  , runOverrideSim
    -- * Monad operations
  , withSimContext
  , getContext
  , getSymInterface
  , ovrWithBackend
  , bindFnHandle
  , bindCFG
  , exitExecution
  , getOverrideArgs
  , overrideError
  , overrideAbort
  , symbolicBranch
  , symbolicBranches
  , nondetBranches
  , overrideReturn
  , overrideReturn'
    -- * Function calls
  , callFnVal
  , callFnVal'
  , callCFG
  , callBlock
  , callOverride
    -- * Global variables
  , readGlobal
  , writeGlobal
  , readGlobals
  , writeGlobals
  , modifyGlobal
    -- * References
  , newRef
  , newEmptyRef
  , readRef
  , writeRef
  , modifyRef
  , readMuxTreeRef
  , writeMuxTreeRef
    -- * Function bindings
  , FnBinding(..)
  , fnBindingsFromList
  , registerFnBinding
  , AnyFnBindings(..)
    -- * Overrides
  , mkOverride
  , mkOverride'
    -- * Intrinsic implementations
  , IntrinsicImpl
  , mkIntrinsic
  , useIntrinsic
    -- * Typed overrides
  , TypedOverride(..)
  , SomeTypedOverride(..)
  , runTypedOverride
    -- * Re-exports
  , Lang.Crucible.Simulator.ExecutionTree.Override
  ) where

import           Control.Exception
import           Control.Lens
import           Control.Monad hiding (fail)
import qualified Control.Monad.Catch as X
import           Control.Monad.IO.Class (MonadIO(..))
import           Control.Monad.Reader (ReaderT(..))
import           Control.Monad.ST
import           Control.Monad.State.Strict (StateT(..))
import           Data.List (foldl')
import qualified Data.Parameterized.Context as Ctx
import           Data.Proxy
import qualified Data.Text as T
import           Data.Traversable (for)
import           Numeric.Natural (Natural)
import           System.Exit
import           System.IO
import           System.IO.Error

import           Data.Parameterized.TraversableFC (fmapFC)

import           What4.Config
import           What4.Interface
import           What4.FunctionName
import           What4.Partial (justPartExpr)
import           What4.ProgramLoc
import           What4.Utils.MonadST

import           Lang.Crucible.Analysis.Postdom
import           Lang.Crucible.CFG.Core
import           Lang.Crucible.CFG.Extension
import           Lang.Crucible.FunctionHandle
import           Lang.Crucible.Panic(panic)

import           Lang.Crucible.Backend
import           Lang.Crucible.Simulator.CallFrame
import qualified Lang.Crucible.Simulator.EvalStmt as EvalStmt (readRef, alterRef)
import           Lang.Crucible.Simulator.ExecutionTree
import           Lang.Crucible.Simulator.GlobalState
import           Lang.Crucible.Simulator.Operations
                   ( runGenericErrorHandler, runErrorHandler, runAbortHandler
                   , returnValue, callFunction, overrideSymbolicBranch )
import           Lang.Crucible.Simulator.RegMap
import           Lang.Crucible.Simulator.SimError
import           Lang.Crucible.Utils.MonadVerbosity
import           Lang.Crucible.Utils.MuxTree (MuxTree)
import           Lang.Crucible.Utils.StateContT

------------------------------------------------------------------------
-- OverrideSim

-- | Monad for running symbolic simulator.
--
-- Type parameters:
--
--   * 'p'    the "personality", i.e. user-defined state parameterized by @sym@
--   * 'sym'  the symbolic backend
--   * 'ext'  the syntax extension ("Lang.Crucible.CFG.Extension")
--   * 'rtp'  global return type
--   * 'args' argument types for the current frame
--   * 'ret'  return type of the current frame
--   * 'a'    the value type
--
newtype OverrideSim p sym ext rtp (args :: Ctx CrucibleType) (ret :: CrucibleType) a
      = Sim { unSim :: StateContT (SimState p sym ext rtp (OverrideLang ret) ('Just args))
                                  (ExecState p sym ext rtp)
                                  IO
                                  a
            }
  deriving ( Functor
           , Applicative
           )

-- | Exit from the current execution by ignoring the continuation
--   and immediately returning an aborted execution result.
exitExecution :: IsSymInterface sym => ExitCode -> OverrideSim p sym ext rtp args r a
exitExecution ec = Sim $ StateContT $ \_c s ->
  return $ ResultState $ AbortedResult (s^.stateContext) (AbortedExit ec)

bindOverrideSim ::
  OverrideSim p sym ext rtp args r a ->
  (a -> OverrideSim p sym ext rtp args r b) ->
  OverrideSim p sym ext rtp args r b
bindOverrideSim (Sim m) h = Sim $ unSim . h =<< m
{-# INLINE bindOverrideSim #-}

instance Monad (OverrideSim p sym ext rtp args r) where
  (>>=) = bindOverrideSim

deriving instance MonadState (SimState p sym ext rtp (OverrideLang ret) ('Just args))
                             (OverrideSim p sym ext rtp args ret)

instance MonadFail (OverrideSim p sym ext rtp args ret) where
  fail msg = Sim $ StateContT $ \_c -> runGenericErrorHandler msg


instance MonadIO (OverrideSim p sym ext rtp args ret) where
  liftIO m = do
     Sim $ StateContT $ \c s -> do
       -- FIXME, should we be doing this exception handling here, or should
       -- we just continue to let it bubble upward?
       r <- try m
       case r of
         Left e0
           -- IO Exception
           | Just e <- fromException e0
           , isUserError e ->
             runGenericErrorHandler (ioeGetErrorString e) s
             -- AbortReason
           | Just e <- fromException e0 ->
             runAbortHandler e s
             -- Default case
           | otherwise ->
             throwIO e0
         Right v -> c v s

instance MonadST RealWorld (OverrideSim p sym ext rtp args ret) where
  liftST m = liftIO $ stToIO m

instance MonadCont (OverrideSim p sym ext rtp args ret) where
  callCC f = Sim $ callCC (\k -> unSim (f (\a -> Sim (k a))))

instance X.MonadThrow (OverrideSim p sym ext rtp args ret) where
  throwM = liftIO . throwIO

getContext :: OverrideSim p sym ext rtp args ret (SimContext p sym ext)
getContext = use stateContext
{-# INLINE getContext #-}

getSymInterface :: OverrideSim p sym ext rtp args ret sym
getSymInterface = use stateSymInterface

ovrWithBackend ::
  (forall bak. IsSymBackend sym bak => bak -> OverrideSim p sym ext rtp args ret a) ->
  OverrideSim p sym ext rtp args ret a
ovrWithBackend k =
  do simCtx <- use stateContext
     ctxSolverProof simCtx (withBackend simCtx k)

instance MonadVerbosity (OverrideSim p sym ext rtp args ret) where
  getVerbosity =
    do ctx <- getContext
       let cfg = ctxSolverProof ctx (getConfiguration (ctx^.ctxSymInterface))
       v <- liftIO (getOpt =<< getOptionSetting verbosity cfg)
       return (fromInteger v)

  getLogFunction =
    do h <- printHandle <$> getContext
       verb <- getVerbosity
       return $ \n msg -> do
         when (n <= verb) $ do
           hPutStr h msg
           hFlush h
  showWarning msg =
    do h <- printHandle <$> getContext
       liftIO $
         do hPutStrLn h msg
            hFlush h

-- | Associate a definition (either an 'Override' or a 'CFG') with the given handle.
bindFnHandle ::
  FnHandle args ret ->
  FnState p sym ext args ret ->
  OverrideSim p sym ext rtp a r ()
bindFnHandle h s =
  stateContext . functionBindings %= FnBindings . insertHandleMap h s . fnBindings

-- | Bind a CFG to its handle.
--
-- Computes postdominator information.
bindCFG :: CFG ext blocks args ret -> OverrideSim p sym ext rtp a r ()
bindCFG c = bindFnHandle (cfgHandle c) (UseCFG c (postdomInfo c))

------------------------------------------------------------------------
-- Mutable variables

-- | Read the whole sym global state.
readGlobals :: OverrideSim p sym ext rtp args ret (SymGlobalState sym)
readGlobals = use (stateTree . actFrame . gpGlobals)

-- | Overwrite the whole sym global state
writeGlobals :: SymGlobalState sym -> OverrideSim p sym ext rtp args ret ()
writeGlobals g = stateTree . actFrame . gpGlobals .= g

-- | Read a particular global variable from the global variable state.
readGlobal ::
  IsSymInterface sym =>
  GlobalVar tp                                     {- ^ global variable -} ->
  OverrideSim p sym ext rtp args ret (RegValue sym tp) {- ^ current value   -}
readGlobal k =
  do globals <- use (stateTree . actFrame . gpGlobals)
     case lookupGlobal k globals of
       Just v  -> return v
       Nothing -> panic "OverrideSim.readGlobal"
                          [ "Attempt to read undefined global."
                          , "*** Global name: " ++ show k
                          ]

-- | Set the value of a particular global variable.
writeGlobal ::
  GlobalVar tp    {- ^ global variable -} ->
  RegValue sym tp {- ^ new value       -} ->
  OverrideSim p sym ext rtp args ret ()
writeGlobal g v = stateTree . actFrame . gpGlobals %= insertGlobal g v


-- | Run an action to compute the new value of a global.
modifyGlobal ::
  IsSymInterface sym =>
  GlobalVar tp    {- ^ global variable to modify -} ->
  (RegValue sym tp ->
    OverrideSim p sym ext rtp args ret (a, RegValue sym tp)) {- ^ modification action -} ->
  OverrideSim p sym ext rtp args ret a
modifyGlobal gv f =
  do x <- readGlobal gv
     (a, x') <- f x
     writeGlobal gv x'
     return a

-- | Create a new reference cell.
newRef ::
  IsSymInterface sym =>
  TypeRepr tp {- ^ Type of the reference cell -} ->
  RegValue sym tp {- ^ Initial value of the cell -} ->
  OverrideSim p sym ext rtp args ret (RefCell tp)
newRef tpr v =
  do r <- newEmptyRef tpr
     writeRef r v
     return r

-- | Create a new reference cell with no contents.
newEmptyRef ::
  TypeRepr tp {- ^ Type of the reference cell -} ->
  OverrideSim p sym ext rtp args ret (RefCell tp)
newEmptyRef tpr =
  do halloc <- use (stateContext . to simHandleAllocator)
     liftIO $ freshRefCell halloc tpr

-- | Read the current value of a reference cell.
readRef ::
  IsSymInterface sym =>
  RefCell tp {- ^ Reference cell to read -} ->
  OverrideSim p sym ext rtp args ret (RegValue sym tp)
readRef r =
  do globals <- use (stateTree . actFrame . gpGlobals)
     let msg = ReadBeforeWriteSimError "Attempt to read undefined reference cell"
     ovrWithBackend $ \bak ->
       liftIO $ readPartExpr bak (lookupRef r globals) msg

-- | Write a value into a reference cell.
writeRef ::
  IsSymInterface sym =>
  RefCell tp {- ^ Reference cell to write -} ->
  RegValue sym tp {- ^ Value to write into the cell -} ->
  OverrideSim p sym ext rtp args ret ()
writeRef r v =
  do sym <- getSymInterface
     stateTree . actFrame . gpGlobals %= insertRef sym r v

modifyRef ::
  IsSymInterface sym =>
  RefCell tp {- ^ Reference cell to modify -} ->
  (RegValue sym tp ->
    OverrideSim p sym ext rtp args ret (a, RegValue sym tp)) {- ^ modification action -} ->
  OverrideSim p sym ext rtp args ret a
modifyRef ref f =
  do x <- readRef ref
     (a, x') <- f x
     writeRef ref x'
     return a


-- | Read the current value of a mux tree of reference cells.
readMuxTreeRef ::
  IsSymInterface sym =>
  TypeRepr tp ->
  MuxTree sym (RefCell tp) {- ^ Reference cell to read -} ->
  OverrideSim p sym ext rtp args ret (RegValue sym tp)
readMuxTreeRef tpr r =
  do iTypes <- ctxIntrinsicTypes <$> use stateContext
     globals <- use (stateTree . actFrame . gpGlobals)
     ovrWithBackend $ \bak ->
       liftIO $ EvalStmt.readRef bak iTypes tpr r globals

-- | Write a value into a mux tree of reference cells.
writeMuxTreeRef ::
  IsSymInterface sym =>
  TypeRepr tp ->
  MuxTree sym (RefCell tp) {- ^ Reference cell to write -} ->
  RegValue sym tp {- ^ Value to write into the cell -} ->
  OverrideSim p sym ext rtp args ret ()
writeMuxTreeRef tpr r v =
  do sym <- getSymInterface
     iTypes <- ctxIntrinsicTypes <$> use stateContext
     globals <- use (stateTree . actFrame . gpGlobals)
     globals' <- liftIO $ EvalStmt.alterRef sym iTypes tpr r (justPartExpr sym v) globals
     stateTree . actFrame . gpGlobals .= globals'


-- | Turn an 'OverrideSim' action into an 'ExecCont' that can be executed
--   using standard Crucible execution primitives like 'executeCrucible'.
runOverrideSim ::
  TypeRepr tp {- ^ return type -} ->
  OverrideSim p sym ext rtp args tp (RegValue sym tp) {- ^ action to execute  -} ->
  ExecCont p sym ext rtp (OverrideLang tp) ('Just args)
runOverrideSim tp m = ReaderT $ \s0 -> stateSolverProof s0 $
  runStateContT (unSim m) (\v -> runReaderT (returnValue (RegEntry tp v))) s0


-- | Create an override from an explicit return type and definition using 'OverrideSim'.
mkOverride' ::
  FunctionName ->
  TypeRepr ret ->
  (forall r . OverrideSim p sym ext r args ret (RegValue sym ret)) ->
  Override p sym ext args ret
mkOverride' nm tp f =
  Override { overrideName = nm
           , overrideHandler = runOverrideSim tp f
           }

-- | Create an override from a statically inferrable return type and definition using 'OverrideSim'.
mkOverride ::
  KnownRepr TypeRepr ret =>
  FunctionName ->
  (forall r . OverrideSim p sym ext r args ret (RegValue sym ret)) ->
  Override p sym ext args ret
mkOverride nm = mkOverride' nm knownRepr

-- | Return override arguments.
getOverrideArgs :: OverrideSim p sym ext rtp args ret (RegMap sym args)
getOverrideArgs = use (stateOverrideFrame.overrideRegMap)

withSimContext :: StateT (SimContext p sym ext) IO a -> OverrideSim p sym ext rtp args ret a
withSimContext m =
  do ctx <- use stateContext
     (r,ctx') <- liftIO $ runStateT m ctx
     stateContext .= ctx'
     return r

-- | Call a function with the given arguments.
callFnVal ::
  (IsExprBuilder sym, IsSyntaxExtension ext) =>
  FnVal sym args ret {- ^ Function to call -} ->
  RegMap sym args {- ^ Arguments to the function -} ->
  OverrideSim p sym ext rtp a r (RegEntry sym ret)
callFnVal cl args =
  Sim $ StateContT $ \c -> runReaderT $ do
    sym <- view stateSymInterface
    loc <- liftIO $ getCurrentProgramLoc sym
    callFunction cl args (ReturnToOverride c) loc

-- | Call a function with the given arguments.  Provide the arguments as an
--   @Assignment@ instead of as a @RegMap@.
callFnVal' ::
  (IsExprBuilder sym, IsSyntaxExtension ext) =>
  FnVal sym args ret {- ^ Function to call -} ->
  Ctx.Assignment (RegValue' sym) args {- ^ Arguments to the function -} ->
  OverrideSim p sym ext rtp a r (RegValue sym ret)
callFnVal' cl args =
  do let FunctionHandleRepr tps _ = fnValType cl
     let args' = Ctx.zipWith (\tp (RV x) -> RegEntry tp x) tps args
     regValue <$> callFnVal cl (RegMap args')

-- | Call a control flow graph from 'OverrideSim'.
--
-- Note that this computes the postdominator information, so there is some
-- performance overhead in the call.
callCFG ::
  IsSyntaxExtension ext =>
  CFG ext blocks init ret {- ^ Function to run -} ->
  RegMap sym init {- ^ Arguments to the function -} ->
  OverrideSim p sym ext rtp a r (RegEntry sym ret)
callCFG cfg = callBlock cfg (cfgEntryBlockID cfg)

-- | Call a block of a control flow graph from 'OverrideSim'.
--
-- Note that this computes the postdominator information, so there is some
-- performance overhead in the call.
callBlock ::
  IsSyntaxExtension ext =>
  CFG ext blocks init ret {- ^ Function to run -} ->
  BlockID blocks args {- ^ Block to run -} ->
  RegMap sym args {- ^ Arguments to the block -} ->
  OverrideSim p sym ext rtp a r (RegEntry sym ret)
callBlock cfg bid args =
  Sim $ StateContT $ \c -> runReaderT $
    let f = mkBlockFrame cfg bid (postdomInfo cfg) args in
    ReaderT $ return . CallState (ReturnToOverride c) (CrucibleCall bid f)

-- | Call an override in a new call frame.
callOverride ::
  FnHandle args ret ->
  Override p sym ext args ret ->
  RegMap sym args ->
  OverrideSim p sym ext rtp a r (RegEntry sym ret)
callOverride h ovr args =
  Sim $ StateContT $ \c -> runReaderT $
    let f = OverrideFrame (overrideName ovr) (SomeHandle h) args in
    ReaderT $ return . CallState (ReturnToOverride c) (OverrideCall ovr f)


-- | Add a failed assertion.  This aborts execution along the current
-- evaluation path, and adds a proof obligation ensuring that we can't get here
-- in the first place.
overrideError :: IsSymInterface sym => SimErrorReason -> OverrideSim p sym ext rtp args res a
overrideError err = Sim $ StateContT $ \_ -> runErrorHandler err


-- | Abort the current thread of execution for the given reason.  Unlike @overrideError@,
--   this operation will not add proof obligation, even if the given abort reason
--   is due to an assertion failure.  Use @overrideError@ instead if a proof obligation
--   should be generated.
overrideAbort :: AbortExecReason -> OverrideSim p sym ext rtp args res a
overrideAbort abt = Sim $ StateContT $ \_ -> runAbortHandler abt

overrideReturn :: KnownRepr TypeRepr res => RegValue sym res -> OverrideSim p sym ext rtp args res a
overrideReturn v = Sim $ StateContT $ \_ -> runReaderT $ returnValue (RegEntry knownRepr v)

overrideReturn' :: RegEntry sym res -> OverrideSim p sym ext rtp args res a
overrideReturn' v = Sim $ StateContT $ \_ -> runReaderT $ returnValue v

-- | Perform a symbolic branch on the given predicate.  If we can determine
--   that the predicate must be either true or false, we will exeucte only
--   the "then" or the "else" branch.  Otherwise, both branches will be executed
--   and the results merged when a value is returned from the override.  NOTE!
--   this means the code following this symbolic branch may be executed more than
--   once; in particular, side effects may happen more than once.
--
--   In order to ensure that push/abort/mux bookeeping is done properly, all
--   symbolic values that will be used in the branches should be inserted into
--   the @RegMap@ argument of this function, and retrieved in the branches using
--   the @getOverrideArgs@ function.  Otherwise mux errors may later occur, which
--   will be very confusing.  In other words, don't directly use symbolic values
--   computed before calling this function; you must instead first put them into
--   the @RegMap@ and get them out again later.
symbolicBranch ::
  IsSymInterface sym =>
  Pred sym {- ^ Predicate to branch on -} ->

  RegMap sym then_args {- ^ argument values for the then branch -} ->
  OverrideSim p sym ext rtp then_args res a {- ^ then branch -} ->
  Maybe Position {- ^ optional location for then branch -} ->

  RegMap sym else_args {- ^ argument values for the else branch -} ->
  OverrideSim p sym ext rtp else_args res a {- ^ else branch -} ->
  Maybe Position {- ^ optional location for else branch -} ->

  OverrideSim p sym ext rtp args res a
symbolicBranch p thn_args thn thn_pos els_args els els_pos =
  Sim $ StateContT $ \c -> runReaderT $
    do old_args <- view (stateTree.actFrame.overrideTopFrame.overrideRegMap)
       let thn' = ReaderT (runStateContT
                            (unSim thn)
                            (\x st -> c x (st & stateTree.actFrame.overrideTopFrame.overrideRegMap .~ old_args)))
       let els' = ReaderT (runStateContT
                            (unSim els)
                            (\x st -> c x (st & stateTree.actFrame.overrideTopFrame.overrideRegMap .~ old_args)))
       overrideSymbolicBranch p thn_args thn' thn_pos els_args els' els_pos

-- | Perform a series of symbolic branches.  This operation will evaluate a
--   series of branches, one for each element of the list.  The semantics of
--   this construct is that the predicates are evaluated in order, until
--   the first one that evaluates true; this branch will be the taken branch.
--   In other words, this operates like a chain of if-then-else statements;
--   later branches assume that earlier branches were not taken.
--
--   If no predicate is true, the construct will abort with a @VariantOptionsExhausted@
--   reason.  If you wish to report an error condition instead, you should add a
--   final default case with a true predicate that calls @overrideError@.
--   As with @symbolicBranch@, be aware that code following this operation may be
--   called several times, and side effects may occur more than once.
--
--   As with @symbolicBranch@, any symbolic values needed by the branches should be
--   placed into the @RegMap@ argument and retrieved when needed.  See the comment
--   on @symbolicBranch@.
symbolicBranches :: forall p sym ext rtp args new_args res a.
  IsSymInterface sym =>
  RegMap sym new_args {- ^ argument values for the branches -} ->
  [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a, Maybe Position)]
   {- ^ Branches to consider -} ->
  OverrideSim p sym ext rtp args res a
symbolicBranches new_args xs0 =
  Sim $ StateContT $ \c -> runReaderT $
    do sym <- view stateSymInterface
       top_loc <- liftIO $ getCurrentProgramLoc sym
       old_args <- view (stateTree.actFrame.overrideTopFrame.overrideRegMap)
       let all_args = appendRegs old_args new_args
       let c' x st = c x (st & stateTree.actFrame.overrideTopFrame.overrideRegMap .~ old_args)
       let go _ [] = ReaderT $ runAbortHandler (VariantOptionsExhausted top_loc)
           go !i ((p,m,mpos):xs) =
             let msg = T.pack ("after branch " ++ show i)
                 m'  = ReaderT (runStateContT (unSim m) c')
              in overrideSymbolicBranch p all_args m' mpos old_args (go (i+1) xs) (Just (OtherPos msg))
       go (0::Integer) xs0

-- | Non-deterministically choose among several feasible branches.
--
-- Unlike 'symbolicBranches', this function does not take only the first branch
-- with a predicate that evaluates to true; instead it takes /all/ branches with
-- predicates that are not syntactically false (or cannot be proved unreachable
-- with path satisfiability checking, if enabled). Each branch will /not/ assume
-- that other branches weren't taken.
--
-- As with 'symbolicBranch', any symbolic values needed by the branches should be
-- placed into the @RegMap@ argument and retrieved when needed. See the comment
-- on 'symbolicBranch'.
--
-- Operationally, this works by by numbering all of the branches from 0 to n,
-- inventing a symbolic integer variable z, and adding z = i (where i ranges
-- from 0 to n) to the branch condition for each branch, and calling
-- 'symbolicBranches' on the result. Even though each branch given to
-- 'symbolicBranches' assumes earlier branches are not taken, each branch
-- condition has the form @(z = i) and p@, so the negation @~((z = i) and p)@
-- is equivalent to @(z != i) or ~p@, so later branches don't assume the
-- negation of the branch condition of earlier branches (i.e., @~p@).
nondetBranches :: forall p sym ext rtp args new_args res a.
  IsSymInterface sym =>
  RegMap sym new_args {- ^ argument values for the branches -} ->
  [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a, Maybe Position)]
   {- ^ Branches to consider -} ->
  OverrideSim p sym ext rtp args res a
nondetBranches new_args xs0 =
  do sym <- getSymInterface
     z <- liftIO $ freshNat sym (safeSymbol "nondetBranchesZ")
     xs <- for (zip [(0 :: Natural)..] xs0) $ \(i, (p, v, position)) ->
       do p' <- liftIO $ andPred sym p =<< natEq sym z =<< natLit sym i
          return (p', v, position)
     symbolicBranches new_args xs

--------------------------------------------------------------------------------
-- FnBinding

-- | A pair containing a handle and the state associated to execute it.
data FnBinding p sym ext where
  FnBinding :: FnHandle args ret
            -> FnState p sym ext args ret
            -> FnBinding p sym ext

-- | Add function binding to map.
insertFnBinding :: FunctionBindings p sym ext
                -> FnBinding p sym ext
                -> FunctionBindings p sym ext
insertFnBinding m (FnBinding h s) = FnBindings $ insertHandleMap h s $ fnBindings m

-- | Build a map of function bindings from a list of
--   handle/binding pairs.
fnBindingsFromList :: [FnBinding p sym ext] -> FunctionBindings p sym ext
fnBindingsFromList = foldl' insertFnBinding $ FnBindings emptyHandleMap

registerFnBinding :: FnBinding p sym ext
                   -> OverrideSim p sym ext rtp a r ()
registerFnBinding (FnBinding h s) = bindFnHandle h s

--------------------------------------------------------------------------------
-- AnyFnBindings

-- | This quantifies over function bindings that can work for any symbolic interface.
data AnyFnBindings ext = AnyFnBindings (forall p sym . IsSymInterface sym => [FnBinding p sym ext])

--------------------------------------------------------------------------------
-- Intrinsic utility definitions

type IntrinsicImpl p sym ext args ret =
  IsSymInterface sym => FnHandle args ret -> Override p sym ext args ret

useIntrinsic ::
  FnHandle args ret ->
  (FnHandle args ret -> Override p sym ext args ret) ->
  FnBinding p sym ext
useIntrinsic hdl impl = FnBinding hdl (UseOverride (impl hdl))

-- | Make an IntrinsicImpl from an explicit implementation
mkIntrinsic :: forall p sym ext args ret.
  Ctx.CurryAssignmentClass args =>
  (forall r. Proxy r
               -> sym
               -> Ctx.CurryAssignment args
                    (RegEntry sym)
                    (OverrideSim p sym ext r args ret (RegValue sym ret)))
    {- ^ Override implementation, given a proxy value to fix the type, a
         reference to the symbolic engine, and a curried arguments -} ->
  FnHandle args ret ->
  Override p sym ext args ret
mkIntrinsic m hdl = mkOverride' (handleName hdl) (handleReturnType hdl) ovr
 where
   ovr :: forall r. OverrideSim p sym ext r args ret (RegValue sym ret)
   ovr = do
       sym <- getSymInterface
       (RegMap args) <- getOverrideArgs
       Ctx.uncurryAssignment (m (Proxy :: Proxy r) sym) args

--------------------------------------------------------------------------------
-- Typed overrides

-- | An action in 'OverrideSim', together with 'TypeRepr's for its arguments
-- and return values. This type is used across several frontends to define
-- overrides for built-in functions, e.g., @malloc@ in the LLVM frontend.
--
-- For maximal reusability, frontends may define 'TypedOverride's that are
-- polymorphic in (any of) @p@, @sym@, and @ext@.
data TypedOverride p sym ext args ret
  = TypedOverride
    { typedOverrideHandler ::
        forall rtp args' ret'.
        Ctx.Assignment (RegValue' sym) args ->
        OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
    , typedOverrideArgs :: CtxRepr args
    , typedOverrideRet :: TypeRepr ret
    }

-- | A 'TypedOverride' with the type parameters @args@, @ret@ existentially
-- quantified
data SomeTypedOverride p sym ext =
  forall args ret. SomeTypedOverride (TypedOverride p sym ext args ret)

-- | Create an override from a 'TypedOverride'.
runTypedOverride ::
  FunctionName ->
  TypedOverride p sym ext args ret ->
  Override p sym ext args ret
runTypedOverride nm typedOvr = mkOverride' nm (typedOverrideRet typedOvr) $ do
  RegMap args <- getOverrideArgs
  typedOverrideHandler typedOvr (fmapFC (RV . regValue) args)