{-|
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 { forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
OverrideSim p sym ext rtp args ret a
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
unSim :: StateContT (SimState p sym ext rtp (OverrideLang ret) ('Just args))
                                  (ExecState p sym ext rtp)
                                  IO
                                  a
            }
  deriving ( (forall a b.
 (a -> b)
 -> OverrideSim p sym ext rtp args ret a
 -> OverrideSim p sym ext rtp args ret b)
-> (forall a b.
    a
    -> OverrideSim p sym ext rtp args ret b
    -> OverrideSim p sym ext rtp args ret a)
-> Functor (OverrideSim p sym ext rtp args ret)
forall a b.
a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret a
forall a b.
(a -> b)
-> OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b.
a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b.
(a -> b)
-> OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b.
(a -> b)
-> OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
fmap :: forall a b.
(a -> b)
-> OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
$c<$ :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b.
a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret a
<$ :: forall a b.
a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret a
Functor
           , Functor (OverrideSim p sym ext rtp args ret)
Functor (OverrideSim p sym ext rtp args ret) =>
(forall a. a -> OverrideSim p sym ext rtp args ret a)
-> (forall a b.
    OverrideSim p sym ext rtp args ret (a -> b)
    -> OverrideSim p sym ext rtp args ret a
    -> OverrideSim p sym ext rtp args ret b)
-> (forall a b c.
    (a -> b -> c)
    -> OverrideSim p sym ext rtp args ret a
    -> OverrideSim p sym ext rtp args ret b
    -> OverrideSim p sym ext rtp args ret c)
-> (forall a b.
    OverrideSim p sym ext rtp args ret a
    -> OverrideSim p sym ext rtp args ret b
    -> OverrideSim p sym ext rtp args ret b)
-> (forall a b.
    OverrideSim p sym ext rtp args ret a
    -> OverrideSim p sym ext rtp args ret b
    -> OverrideSim p sym ext rtp args ret a)
-> Applicative (OverrideSim p sym ext rtp args ret)
forall a. a -> OverrideSim p sym ext rtp args ret a
forall a b.
OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret a
forall a b.
OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret b
forall a b.
OverrideSim p sym ext rtp args ret (a -> b)
-> OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
forall a b c.
(a -> b -> c)
-> OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret c
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
Functor (OverrideSim p sym ext rtp args ret)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
a -> OverrideSim p sym ext rtp args ret a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b.
OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b.
OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret b
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b.
OverrideSim p sym ext rtp args ret (a -> b)
-> OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b c.
(a -> b -> c)
-> OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
a -> OverrideSim p sym ext rtp args ret a
pure :: forall a. a -> OverrideSim p sym ext rtp args ret a
$c<*> :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b.
OverrideSim p sym ext rtp args ret (a -> b)
-> OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
<*> :: forall a b.
OverrideSim p sym ext rtp args ret (a -> b)
-> OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
$cliftA2 :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b c.
(a -> b -> c)
-> OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret c
liftA2 :: forall a b c.
(a -> b -> c)
-> OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret c
$c*> :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b.
OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret b
*> :: forall a b.
OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret b
$c<* :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b.
OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret a
<* :: forall a b.
OverrideSim p sym ext rtp args ret a
-> OverrideSim p sym ext rtp args ret b
-> OverrideSim p sym ext rtp args ret a
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 :: forall sym p ext rtp (args :: Ctx CrucibleType) (r :: CrucibleType)
       a.
IsSymInterface sym =>
ExitCode -> OverrideSim p sym ext rtp args r a
exitExecution ExitCode
ec = StateContT
  (SimState p sym ext rtp (OverrideLang r) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args r a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang r) ('Just args))
   (ExecState p sym ext rtp)
   IO
   a
 -> OverrideSim p sym ext rtp args r a)
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
-> OverrideSim p sym ext rtp args r a
forall a b. (a -> b) -> a -> b
$ ((a
  -> SimState p sym ext rtp (OverrideLang r) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> SimState p sym ext rtp (OverrideLang r) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((a
   -> SimState p sym ext rtp (OverrideLang r) ('Just args)
   -> IO (ExecState p sym ext rtp))
  -> SimState p sym ext rtp (OverrideLang r) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> StateContT
      (SimState p sym ext rtp (OverrideLang r) ('Just args))
      (ExecState p sym ext rtp)
      IO
      a)
-> ((a
     -> SimState p sym ext rtp (OverrideLang r) ('Just args)
     -> IO (ExecState p sym ext rtp))
    -> SimState p sym ext rtp (OverrideLang r) ('Just args)
    -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall a b. (a -> b) -> a -> b
$ \a
-> SimState p sym ext rtp (OverrideLang r) ('Just args)
-> IO (ExecState p sym ext rtp)
_c SimState p sym ext rtp (OverrideLang r) ('Just args)
s ->
  ExecState p sym ext rtp -> IO (ExecState p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecState p sym ext rtp -> IO (ExecState p sym ext rtp))
-> ExecState p sym ext rtp -> IO (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ ExecResult p sym ext rtp -> ExecState p sym ext rtp
forall p sym ext rtp.
ExecResult p sym ext rtp -> ExecState p sym ext rtp
ResultState (ExecResult p sym ext rtp -> ExecState p sym ext rtp)
-> ExecResult p sym ext rtp -> ExecState p sym ext rtp
forall a b. (a -> b) -> a -> b
$ SimContext p sym ext
-> AbortedResult sym ext -> ExecResult p sym ext rtp
forall p sym ext r.
SimContext p sym ext
-> AbortedResult sym ext -> ExecResult p sym ext r
AbortedResult (SimState p sym ext rtp (OverrideLang r) ('Just args)
sSimState p sym ext rtp (OverrideLang r) ('Just args)
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext rtp (OverrideLang r) ('Just args))
     (SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (OverrideLang r) ('Just args))
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext) (ExitCode -> AbortedResult sym ext
forall sym ext. ExitCode -> AbortedResult sym ext
AbortedExit ExitCode
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 :: forall p sym ext rtp (args :: Ctx CrucibleType) (r :: CrucibleType)
       a b.
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 StateContT
  (SimState p sym ext rtp (OverrideLang r) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
m) a -> OverrideSim p sym ext rtp args r b
h = StateContT
  (SimState p sym ext rtp (OverrideLang r) ('Just args))
  (ExecState p sym ext rtp)
  IO
  b
-> OverrideSim p sym ext rtp args r b
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang r) ('Just args))
   (ExecState p sym ext rtp)
   IO
   b
 -> OverrideSim p sym ext rtp args r b)
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just args))
     (ExecState p sym ext rtp)
     IO
     b
-> OverrideSim p sym ext rtp args r b
forall a b. (a -> b) -> a -> b
$ OverrideSim p sym ext rtp args r b
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just args))
     (ExecState p sym ext rtp)
     IO
     b
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
OverrideSim p sym ext rtp args ret a
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
unSim (OverrideSim p sym ext rtp args r b
 -> StateContT
      (SimState p sym ext rtp (OverrideLang r) ('Just args))
      (ExecState p sym ext rtp)
      IO
      b)
-> (a -> OverrideSim p sym ext rtp args r b)
-> a
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just args))
     (ExecState p sym ext rtp)
     IO
     b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> OverrideSim p sym ext rtp args r b
h (a
 -> StateContT
      (SimState p sym ext rtp (OverrideLang r) ('Just args))
      (ExecState p sym ext rtp)
      IO
      b)
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just args))
     (ExecState p sym ext rtp)
     IO
     b
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< StateContT
  (SimState p sym ext rtp (OverrideLang r) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
m
{-# INLINE bindOverrideSim #-}

instance Monad (OverrideSim p sym ext rtp args r) where
  >>= :: forall a b.
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
(>>=) = 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
forall p sym ext rtp (args :: Ctx CrucibleType) (r :: CrucibleType)
       a b.
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

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 :: forall a. String -> OverrideSim p sym ext rtp args ret a
fail String
msg = StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang ret) ('Just args))
   (ExecState p sym ext rtp)
   IO
   a
 -> OverrideSim p sym ext rtp args ret a)
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
-> OverrideSim p sym ext rtp args ret a
forall a b. (a -> b) -> a -> b
$ ((a
  -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((a
   -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
   -> IO (ExecState p sym ext rtp))
  -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> StateContT
      (SimState p sym ext rtp (OverrideLang ret) ('Just args))
      (ExecState p sym ext rtp)
      IO
      a)
-> ((a
     -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
     -> IO (ExecState p sym ext rtp))
    -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
    -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall a b. (a -> b) -> a -> b
$ \a
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> IO (ExecState p sym ext rtp)
_c -> String
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> IO (ExecState p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
String
-> SimState p sym ext rtp f args -> IO (ExecState p sym ext rtp)
runGenericErrorHandler String
msg


instance MonadIO (OverrideSim p sym ext rtp args ret) where
  liftIO :: forall a. IO a -> OverrideSim p sym ext rtp args ret a
liftIO IO a
m = do
     StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang ret) ('Just args))
   (ExecState p sym ext rtp)
   IO
   a
 -> OverrideSim p sym ext rtp args ret a)
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
-> OverrideSim p sym ext rtp args ret a
forall a b. (a -> b) -> a -> b
$ ((a
  -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((a
   -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
   -> IO (ExecState p sym ext rtp))
  -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> StateContT
      (SimState p sym ext rtp (OverrideLang ret) ('Just args))
      (ExecState p sym ext rtp)
      IO
      a)
-> ((a
     -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
     -> IO (ExecState p sym ext rtp))
    -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
    -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall a b. (a -> b) -> a -> b
$ \a
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> IO (ExecState p sym ext rtp)
c SimState p sym ext rtp (OverrideLang ret) ('Just args)
s -> do
       -- FIXME, should we be doing this exception handling here, or should
       -- we just continue to let it bubble upward?
       Either SomeException a
r <- IO a -> IO (Either SomeException a)
forall e a. Exception e => IO a -> IO (Either e a)
try IO a
m
       case Either SomeException a
r of
         Left SomeException
e0
           -- IO Exception
           | Just IOError
e <- SomeException -> Maybe IOError
forall e. Exception e => SomeException -> Maybe e
fromException SomeException
e0
           , IOError -> Bool
isUserError IOError
e ->
             String
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> IO (ExecState p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
String
-> SimState p sym ext rtp f args -> IO (ExecState p sym ext rtp)
runGenericErrorHandler (IOError -> String
ioeGetErrorString IOError
e) SimState p sym ext rtp (OverrideLang ret) ('Just args)
s
             -- AbortReason
           | Just AbortExecReason
e <- SomeException -> Maybe AbortExecReason
forall e. Exception e => SomeException -> Maybe e
fromException SomeException
e0 ->
             AbortExecReason
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> IO (ExecState p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
AbortExecReason
-> SimState p sym ext rtp f args -> IO (ExecState p sym ext rtp)
runAbortHandler AbortExecReason
e SimState p sym ext rtp (OverrideLang ret) ('Just args)
s
             -- Default case
           | Bool
otherwise ->
             SomeException -> IO (ExecState p sym ext rtp)
forall e a. Exception e => e -> IO a
throwIO SomeException
e0
         Right a
v -> a
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> IO (ExecState p sym ext rtp)
c a
v SimState p sym ext rtp (OverrideLang ret) ('Just args)
s

instance MonadST RealWorld (OverrideSim p sym ext rtp args ret) where
  liftST :: forall a. ST RealWorld a -> OverrideSim p sym ext rtp args ret a
liftST ST RealWorld a
m = IO a -> OverrideSim p sym ext rtp args ret a
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO a -> OverrideSim p sym ext rtp args ret a)
-> IO a -> OverrideSim p sym ext rtp args ret a
forall a b. (a -> b) -> a -> b
$ ST RealWorld a -> IO a
forall a. ST RealWorld a -> IO a
stToIO ST RealWorld a
m

instance MonadCont (OverrideSim p sym ext rtp args ret) where
  callCC :: forall a b.
((a -> OverrideSim p sym ext rtp args ret b)
 -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
callCC (a -> OverrideSim p sym ext rtp args ret b)
-> OverrideSim p sym ext rtp args ret a
f = StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang ret) ('Just args))
   (ExecState p sym ext rtp)
   IO
   a
 -> OverrideSim p sym ext rtp args ret a)
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
-> OverrideSim p sym ext rtp args ret a
forall a b. (a -> b) -> a -> b
$ ((a
  -> StateContT
       (SimState p sym ext rtp (OverrideLang ret) ('Just args))
       (ExecState p sym ext rtp)
       IO
       b)
 -> StateContT
      (SimState p sym ext rtp (OverrideLang ret) ('Just args))
      (ExecState p sym ext rtp)
      IO
      a)
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall a b.
((a
  -> StateContT
       (SimState p sym ext rtp (OverrideLang ret) ('Just args))
       (ExecState p sym ext rtp)
       IO
       b)
 -> StateContT
      (SimState p sym ext rtp (OverrideLang ret) ('Just args))
      (ExecState p sym ext rtp)
      IO
      a)
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall (m :: Type -> Type) a b.
MonadCont m =>
((a -> m b) -> m a) -> m a
callCC (\a
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     b
k -> OverrideSim p sym ext rtp args ret a
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
OverrideSim p sym ext rtp args ret a
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
unSim ((a -> OverrideSim p sym ext rtp args ret b)
-> OverrideSim p sym ext rtp args ret a
f (\a
a -> StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  b
-> OverrideSim p sym ext rtp args ret b
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (a
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     b
k a
a))))

instance X.MonadThrow (OverrideSim p sym ext rtp args ret) where
  throwM :: forall e a.
(HasCallStack, Exception e) =>
e -> OverrideSim p sym ext rtp args ret a
throwM = IO a -> OverrideSim p sym ext rtp args ret a
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO a -> OverrideSim p sym ext rtp args ret a)
-> (e -> IO a) -> e -> OverrideSim p sym ext rtp args ret a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> IO a
forall e a. Exception e => e -> IO a
throwIO

getContext :: OverrideSim p sym ext rtp args ret (SimContext p sym ext)
getContext :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (SimContext p sym ext)
getContext = Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SimContext p sym ext)
-> OverrideSim p sym ext rtp args ret (SimContext p sym ext)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext
{-# INLINE getContext #-}

getSymInterface :: OverrideSim p sym ext rtp args ret sym
getSymInterface :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface = Getting
  sym (SimState p sym ext rtp (OverrideLang ret) ('Just args)) sym
-> OverrideSim p sym ext rtp args ret sym
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  sym (SimState p sym ext rtp (OverrideLang ret) ('Just args)) sym
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(sym -> f2 sym)
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
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 :: forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend forall bak.
IsSymBackend sym bak =>
bak -> OverrideSim p sym ext rtp args ret a
k =
  do SimContext p sym ext
simCtx <- Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SimContext p sym ext)
-> OverrideSim p sym ext rtp args ret (SimContext p sym ext)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext
     SimContext p sym ext -> forall a. IsSymInterfaceProof sym a
forall personality sym ext.
SimContext personality sym ext
-> forall a. IsSymInterfaceProof sym a
ctxSolverProof SimContext p sym ext
simCtx (SimContext p sym ext
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimContext p sym ext
simCtx bak -> OverrideSim p sym ext rtp args ret a
forall bak.
IsSymBackend sym bak =>
bak -> OverrideSim p sym ext rtp args ret a
k)

instance MonadVerbosity (OverrideSim p sym ext rtp args ret) where
  getVerbosity :: OverrideSim p sym ext rtp args ret Int
getVerbosity =
    do SimContext p sym ext
ctx <- OverrideSim p sym ext rtp args ret (SimContext p sym ext)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (SimContext p sym ext)
getContext
       let cfg :: Config
cfg = SimContext p sym ext -> forall a. IsSymInterfaceProof sym a
forall personality sym ext.
SimContext personality sym ext
-> forall a. IsSymInterfaceProof sym a
ctxSolverProof SimContext p sym ext
ctx (sym -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration (SimContext p sym ext
ctxSimContext p sym ext
-> Getting sym (SimContext p sym ext) sym -> sym
forall s a. s -> Getting a s a -> a
^.Getting sym (SimContext p sym ext) sym
forall p sym ext (f :: Type -> Type).
(Contravariant f, Functor f) =>
(sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
ctxSymInterface))
       Integer
v <- IO Integer -> OverrideSim p sym ext rtp args ret Integer
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (OptionSetting BaseIntegerType -> IO Integer
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt (OptionSetting BaseIntegerType -> IO Integer)
-> IO (OptionSetting BaseIntegerType) -> IO Integer
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
verbosity Config
cfg)
       Int -> OverrideSim p sym ext rtp args ret Int
forall a. a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
v)

  getLogFunction :: OverrideSim p sym ext rtp args ret (Int -> String -> IO ())
getLogFunction =
    do Handle
h <- SimContext p sym ext -> Handle
forall personality sym ext.
SimContext personality sym ext -> Handle
printHandle (SimContext p sym ext -> Handle)
-> OverrideSim p sym ext rtp args ret (SimContext p sym ext)
-> OverrideSim p sym ext rtp args ret Handle
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> OverrideSim p sym ext rtp args ret (SimContext p sym ext)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (SimContext p sym ext)
getContext
       Int
verb <- OverrideSim p sym ext rtp args ret Int
forall (m :: Type -> Type). MonadVerbosity m => m Int
getVerbosity
       (Int -> String -> IO ())
-> OverrideSim p sym ext rtp args ret (Int -> String -> IO ())
forall a. a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Int -> String -> IO ())
 -> OverrideSim p sym ext rtp args ret (Int -> String -> IO ()))
-> (Int -> String -> IO ())
-> OverrideSim p sym ext rtp args ret (Int -> String -> IO ())
forall a b. (a -> b) -> a -> b
$ \Int
n String
msg -> do
         Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
verb) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
           Handle -> String -> IO ()
hPutStr Handle
h String
msg
           Handle -> IO ()
hFlush Handle
h
  showWarning :: String -> OverrideSim p sym ext rtp args ret ()
showWarning String
msg =
    do Handle
h <- SimContext p sym ext -> Handle
forall personality sym ext.
SimContext personality sym ext -> Handle
printHandle (SimContext p sym ext -> Handle)
-> OverrideSim p sym ext rtp args ret (SimContext p sym ext)
-> OverrideSim p sym ext rtp args ret Handle
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> OverrideSim p sym ext rtp args ret (SimContext p sym ext)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (SimContext p sym ext)
getContext
       IO () -> OverrideSim p sym ext rtp args ret ()
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim p sym ext rtp args ret ())
-> IO () -> OverrideSim p sym ext rtp args ret ()
forall a b. (a -> b) -> a -> b
$
         do Handle -> String -> IO ()
hPutStrLn Handle
h String
msg
            Handle -> IO ()
hFlush Handle
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 :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType) p sym ext
       rtp (a :: Ctx CrucibleType) (r :: CrucibleType).
FnHandle args ret
-> FnState p sym ext args ret -> OverrideSim p sym ext rtp a r ()
bindFnHandle FnHandle args ret
h FnState p sym ext args ret
s =
  (SimContext p sym ext -> Identity (SimContext p sym ext))
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> Identity (SimState p sym ext rtp (OverrideLang r) ('Just a))
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext ((SimContext p sym ext -> Identity (SimContext p sym ext))
 -> SimState p sym ext rtp (OverrideLang r) ('Just a)
 -> Identity (SimState p sym ext rtp (OverrideLang r) ('Just a)))
-> ((FunctionBindings p sym ext
     -> Identity (FunctionBindings p sym ext))
    -> SimContext p sym ext -> Identity (SimContext p sym ext))
-> (FunctionBindings p sym ext
    -> Identity (FunctionBindings p sym ext))
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> Identity (SimState p sym ext rtp (OverrideLang r) ('Just a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FunctionBindings p sym ext
 -> Identity (FunctionBindings p sym ext))
-> SimContext p sym ext -> Identity (SimContext p sym ext)
forall p sym ext (f :: Type -> Type).
Functor f =>
(FunctionBindings p sym ext -> f (FunctionBindings p sym ext))
-> SimContext p sym ext -> f (SimContext p sym ext)
functionBindings ((FunctionBindings p sym ext
  -> Identity (FunctionBindings p sym ext))
 -> SimState p sym ext rtp (OverrideLang r) ('Just a)
 -> Identity (SimState p sym ext rtp (OverrideLang r) ('Just a)))
-> (FunctionBindings p sym ext -> FunctionBindings p sym ext)
-> OverrideSim p sym ext rtp a r ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= FnHandleMap (FnState p sym ext) -> FunctionBindings p sym ext
forall p sym ext.
FnHandleMap (FnState p sym ext) -> FunctionBindings p sym ext
FnBindings (FnHandleMap (FnState p sym ext) -> FunctionBindings p sym ext)
-> (FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext))
-> FunctionBindings p sym ext
-> FunctionBindings p sym ext
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FnHandle args ret
-> FnState p sym ext args ret
-> FnHandleMap (FnState p sym ext)
-> FnHandleMap (FnState p sym ext)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (f :: Ctx CrucibleType -> CrucibleType -> Type).
FnHandle args ret -> f args ret -> FnHandleMap f -> FnHandleMap f
insertHandleMap FnHandle args ret
h FnState p sym ext args ret
s (FnHandleMap (FnState p sym ext)
 -> FnHandleMap (FnState p sym ext))
-> (FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext))
-> FunctionBindings p sym ext
-> FnHandleMap (FnState p sym ext)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
forall p sym ext.
FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
fnBindings

-- | Bind a CFG to its handle.
--
-- Computes postdominator information.
bindCFG :: CFG ext blocks args ret -> OverrideSim p sym ext rtp a r ()
bindCFG :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) (ret :: CrucibleType) p sym rtp
       (a :: Ctx CrucibleType) (r :: CrucibleType).
CFG ext blocks args ret -> OverrideSim p sym ext rtp a r ()
bindCFG CFG ext blocks args ret
c = FnHandle args ret
-> FnState p sym ext args ret -> OverrideSim p sym ext rtp a r ()
forall (args :: Ctx CrucibleType) (ret :: CrucibleType) p sym ext
       rtp (a :: Ctx CrucibleType) (r :: CrucibleType).
FnHandle args ret
-> FnState p sym ext args ret -> OverrideSim p sym ext rtp a r ()
bindFnHandle (CFG ext blocks args ret -> FnHandle args ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
cfgHandle CFG ext blocks args ret
c) (CFG ext blocks args ret
-> CFGPostdom blocks -> FnState p sym ext args ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
CFG ext blocks args ret
-> CFGPostdom blocks -> FnState p sym ext args ret
UseCFG CFG ext blocks args ret
c (CFG ext blocks args ret -> CFGPostdom blocks
forall ext (b :: Ctx (Ctx CrucibleType)) (i :: Ctx CrucibleType)
       (r :: CrucibleType).
CFG ext b i r -> CFGPostdom b
postdomInfo CFG ext blocks args ret
c))

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

-- | Read the whole sym global state.
readGlobals :: OverrideSim p sym ext rtp args ret (SymGlobalState sym)
readGlobals :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (SymGlobalState sym)
readGlobals = Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SymGlobalState sym)
-> OverrideSim p sym ext rtp args ret (SymGlobalState sym)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
  -> Const
       (SymGlobalState sym)
       (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym
     -> Const (SymGlobalState sym) (SymGlobalState sym))
    -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
    -> Const
         (SymGlobalState sym)
         (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (SymGlobalState sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame ((TopFrame sym ext (OverrideLang ret) ('Just args)
  -> Const
       (SymGlobalState sym)
       (TopFrame sym ext (OverrideLang ret) ('Just args)))
 -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym
     -> Const (SymGlobalState sym) (SymGlobalState sym))
    -> TopFrame sym ext (OverrideLang ret) ('Just args)
    -> Const
         (SymGlobalState sym)
         (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym
    -> Const (SymGlobalState sym) (SymGlobalState sym))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym
 -> Const (SymGlobalState sym) (SymGlobalState sym))
-> TopFrame sym ext (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (TopFrame sym ext (OverrideLang ret) ('Just args))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals)

-- | Overwrite the whole sym global state
writeGlobals :: SymGlobalState sym -> OverrideSim p sym ext rtp args ret ()
writeGlobals :: forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
SymGlobalState sym -> OverrideSim p sym ext rtp args ret ()
writeGlobals SymGlobalState sym
g = (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
  -> Identity
       (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
    -> Identity
         (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (OverrideLang ret) ('Just args)
 -> Identity (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame ((TopFrame sym ext (OverrideLang ret) ('Just args)
  -> Identity (TopFrame sym ext (OverrideLang ret) ('Just args)))
 -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> TopFrame sym ext (OverrideLang ret) ('Just args)
    -> Identity (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym -> Identity (SymGlobalState sym))
-> TopFrame sym ext (OverrideLang ret) ('Just args)
-> Identity (TopFrame sym ext (OverrideLang ret) ('Just args))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> SymGlobalState sym -> OverrideSim p sym ext rtp args ret ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= SymGlobalState sym
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 :: forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar tp
k =
  do SymGlobalState sym
globals <- Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SymGlobalState sym)
-> OverrideSim p sym ext rtp args ret (SymGlobalState sym)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
  -> Const
       (SymGlobalState sym)
       (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym
     -> Const (SymGlobalState sym) (SymGlobalState sym))
    -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
    -> Const
         (SymGlobalState sym)
         (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (SymGlobalState sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame ((TopFrame sym ext (OverrideLang ret) ('Just args)
  -> Const
       (SymGlobalState sym)
       (TopFrame sym ext (OverrideLang ret) ('Just args)))
 -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym
     -> Const (SymGlobalState sym) (SymGlobalState sym))
    -> TopFrame sym ext (OverrideLang ret) ('Just args)
    -> Const
         (SymGlobalState sym)
         (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym
    -> Const (SymGlobalState sym) (SymGlobalState sym))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym
 -> Const (SymGlobalState sym) (SymGlobalState sym))
-> TopFrame sym ext (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (TopFrame sym ext (OverrideLang ret) ('Just args))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals)
     case GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
lookupGlobal GlobalVar tp
k SymGlobalState sym
globals of
       Just RegValue sym tp
v  -> RegValue sym tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
forall a. a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return RegValue sym tp
v
       Maybe (RegValue sym tp)
Nothing -> String
-> [String] -> OverrideSim p sym ext rtp args ret (RegValue sym tp)
forall a. HasCallStack => String -> [String] -> a
panic String
"OverrideSim.readGlobal"
                          [ String
"Attempt to read undefined global."
                          , String
"*** Global name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ GlobalVar tp -> String
forall a. Show a => a -> String
show GlobalVar tp
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 :: forall (tp :: CrucibleType) sym p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
GlobalVar tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
writeGlobal GlobalVar tp
g RegValue sym tp
v = (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
  -> Identity
       (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
    -> Identity
         (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (OverrideLang ret) ('Just args)
 -> Identity (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame ((TopFrame sym ext (OverrideLang ret) ('Just args)
  -> Identity (TopFrame sym ext (OverrideLang ret) ('Just args)))
 -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> TopFrame sym ext (OverrideLang ret) ('Just args)
    -> Identity (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym -> Identity (SymGlobalState sym))
-> TopFrame sym ext (OverrideLang ret) ('Just args)
-> Identity (TopFrame sym ext (OverrideLang ret) ('Just args))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym -> SymGlobalState sym)
-> OverrideSim p sym ext rtp args ret ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
insertGlobal GlobalVar tp
g RegValue sym tp
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 :: forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar tp
gv RegValue sym tp
-> OverrideSim p sym ext rtp args ret (a, RegValue sym tp)
f =
  do RegValue sym tp
x <- GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar tp
gv
     (a
a, RegValue sym tp
x') <- RegValue sym tp
-> OverrideSim p sym ext rtp args ret (a, RegValue sym tp)
f RegValue sym tp
x
     GlobalVar tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
forall (tp :: CrucibleType) sym p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
GlobalVar tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
writeGlobal GlobalVar tp
gv RegValue sym tp
x'
     a -> OverrideSim p sym ext rtp args ret a
forall a. a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
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 :: forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
TypeRepr tp
-> RegValue sym tp
-> OverrideSim p sym ext rtp args ret (RefCell tp)
newRef TypeRepr tp
tpr RegValue sym tp
v =
  do RefCell tp
r <- TypeRepr tp -> OverrideSim p sym ext rtp args ret (RefCell tp)
forall (tp :: CrucibleType) p sym ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
TypeRepr tp -> OverrideSim p sym ext rtp args ret (RefCell tp)
newEmptyRef TypeRepr tp
tpr
     RefCell tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
RefCell tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
writeRef RefCell tp
r RegValue sym tp
v
     RefCell tp -> OverrideSim p sym ext rtp args ret (RefCell tp)
forall a. a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return RefCell tp
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 :: forall (tp :: CrucibleType) p sym ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
TypeRepr tp -> OverrideSim p sym ext rtp args ret (RefCell tp)
newEmptyRef TypeRepr tp
tpr =
  do HandleAllocator
halloc <- Getting
  HandleAllocator
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  HandleAllocator
-> OverrideSim p sym ext rtp args ret HandleAllocator
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use ((SimContext p sym ext
 -> Const HandleAllocator (SimContext p sym ext))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     HandleAllocator
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext ((SimContext p sym ext
  -> Const HandleAllocator (SimContext p sym ext))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      HandleAllocator
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((HandleAllocator -> Const HandleAllocator HandleAllocator)
    -> SimContext p sym ext
    -> Const HandleAllocator (SimContext p sym ext))
-> Getting
     HandleAllocator
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     HandleAllocator
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimContext p sym ext -> HandleAllocator)
-> (HandleAllocator -> Const HandleAllocator HandleAllocator)
-> SimContext p sym ext
-> Const HandleAllocator (SimContext p sym ext)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to SimContext p sym ext -> HandleAllocator
forall personality sym ext.
SimContext personality sym ext -> HandleAllocator
simHandleAllocator)
     IO (RefCell tp) -> OverrideSim p sym ext rtp args ret (RefCell tp)
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RefCell tp)
 -> OverrideSim p sym ext rtp args ret (RefCell tp))
-> IO (RefCell tp)
-> OverrideSim p sym ext rtp args ret (RefCell tp)
forall a b. (a -> b) -> a -> b
$ HandleAllocator -> TypeRepr tp -> IO (RefCell tp)
forall (tp :: CrucibleType).
HandleAllocator -> TypeRepr tp -> IO (RefCell tp)
freshRefCell HandleAllocator
halloc TypeRepr tp
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 :: forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
RefCell tp -> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readRef RefCell tp
r =
  do SymGlobalState sym
globals <- Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SymGlobalState sym)
-> OverrideSim p sym ext rtp args ret (SymGlobalState sym)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
  -> Const
       (SymGlobalState sym)
       (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym
     -> Const (SymGlobalState sym) (SymGlobalState sym))
    -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
    -> Const
         (SymGlobalState sym)
         (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (SymGlobalState sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame ((TopFrame sym ext (OverrideLang ret) ('Just args)
  -> Const
       (SymGlobalState sym)
       (TopFrame sym ext (OverrideLang ret) ('Just args)))
 -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym
     -> Const (SymGlobalState sym) (SymGlobalState sym))
    -> TopFrame sym ext (OverrideLang ret) ('Just args)
    -> Const
         (SymGlobalState sym)
         (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym
    -> Const (SymGlobalState sym) (SymGlobalState sym))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym
 -> Const (SymGlobalState sym) (SymGlobalState sym))
-> TopFrame sym ext (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (TopFrame sym ext (OverrideLang ret) ('Just args))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals)
     let msg :: SimErrorReason
msg = String -> SimErrorReason
ReadBeforeWriteSimError String
"Attempt to read undefined reference cell"
     (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret (RegValue sym tp))
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext rtp args ret (RegValue sym tp))
 -> OverrideSim p sym ext rtp args ret (RegValue sym tp))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext rtp args ret (RegValue sym tp))
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
       IO (RegValue sym tp)
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegValue sym tp)
 -> OverrideSim p sym ext rtp args ret (RegValue sym tp))
-> IO (RegValue sym tp)
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ bak
-> PartExpr (Pred sym) (RegValue sym tp)
-> SimErrorReason
-> IO (RegValue sym tp)
forall sym bak v.
IsSymBackend sym bak =>
bak -> PartExpr (Pred sym) v -> SimErrorReason -> IO v
readPartExpr bak
bak (RefCell tp
-> SymGlobalState sym -> PartExpr (Pred sym) (RegValue sym tp)
forall (tp :: CrucibleType) sym.
RefCell tp
-> SymGlobalState sym -> PartExpr (Pred sym) (RegValue sym tp)
lookupRef RefCell tp
r SymGlobalState sym
globals) SimErrorReason
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 :: forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
RefCell tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
writeRef RefCell tp
r RegValue sym tp
v =
  do sym
sym <- OverrideSim p sym ext rtp args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
  -> Identity
       (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
    -> Identity
         (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (OverrideLang ret) ('Just args)
 -> Identity (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame ((TopFrame sym ext (OverrideLang ret) ('Just args)
  -> Identity (TopFrame sym ext (OverrideLang ret) ('Just args)))
 -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> TopFrame sym ext (OverrideLang ret) ('Just args)
    -> Identity (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym -> Identity (SymGlobalState sym))
-> TopFrame sym ext (OverrideLang ret) ('Just args)
-> Identity (TopFrame sym ext (OverrideLang ret) ('Just args))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym -> SymGlobalState sym)
-> OverrideSim p sym ext rtp args ret ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= sym
-> RefCell tp
-> RegValue sym tp
-> SymGlobalState sym
-> SymGlobalState sym
forall sym (tp :: CrucibleType).
IsExprBuilder sym =>
sym
-> RefCell tp
-> RegValue sym tp
-> SymGlobalState sym
-> SymGlobalState sym
insertRef sym
sym RefCell tp
r RegValue sym tp
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 :: forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
RefCell tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyRef RefCell tp
ref RegValue sym tp
-> OverrideSim p sym ext rtp args ret (a, RegValue sym tp)
f =
  do RegValue sym tp
x <- RefCell tp -> OverrideSim p sym ext rtp args ret (RegValue sym tp)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
RefCell tp -> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readRef RefCell tp
ref
     (a
a, RegValue sym tp
x') <- RegValue sym tp
-> OverrideSim p sym ext rtp args ret (a, RegValue sym tp)
f RegValue sym tp
x
     RefCell tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
RefCell tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
writeRef RefCell tp
ref RegValue sym tp
x'
     a -> OverrideSim p sym ext rtp args ret a
forall a. a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
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 :: forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
TypeRepr tp
-> MuxTree sym (RefCell tp)
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readMuxTreeRef TypeRepr tp
tpr MuxTree sym (RefCell tp)
r =
  do IntrinsicTypes sym
iTypes <- SimContext p sym ext -> IntrinsicTypes sym
forall personality sym ext.
SimContext personality sym ext -> IntrinsicTypes sym
ctxIntrinsicTypes (SimContext p sym ext -> IntrinsicTypes sym)
-> OverrideSim p sym ext rtp args ret (SimContext p sym ext)
-> OverrideSim p sym ext rtp args ret (IntrinsicTypes sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SimContext p sym ext)
-> OverrideSim p sym ext rtp args ret (SimContext p sym ext)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext
     SymGlobalState sym
globals <- Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SymGlobalState sym)
-> OverrideSim p sym ext rtp args ret (SymGlobalState sym)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
  -> Const
       (SymGlobalState sym)
       (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym
     -> Const (SymGlobalState sym) (SymGlobalState sym))
    -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
    -> Const
         (SymGlobalState sym)
         (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (SymGlobalState sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame ((TopFrame sym ext (OverrideLang ret) ('Just args)
  -> Const
       (SymGlobalState sym)
       (TopFrame sym ext (OverrideLang ret) ('Just args)))
 -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym
     -> Const (SymGlobalState sym) (SymGlobalState sym))
    -> TopFrame sym ext (OverrideLang ret) ('Just args)
    -> Const
         (SymGlobalState sym)
         (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym
    -> Const (SymGlobalState sym) (SymGlobalState sym))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym
 -> Const (SymGlobalState sym) (SymGlobalState sym))
-> TopFrame sym ext (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (TopFrame sym ext (OverrideLang ret) ('Just args))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals)
     (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret (RegValue sym tp))
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext rtp args ret (RegValue sym tp))
 -> OverrideSim p sym ext rtp args ret (RegValue sym tp))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext rtp args ret (RegValue sym tp))
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
       IO (RegValue sym tp)
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegValue sym tp)
 -> OverrideSim p sym ext rtp args ret (RegValue sym tp))
-> IO (RegValue sym tp)
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ bak
-> IntrinsicTypes sym
-> TypeRepr tp
-> MuxTree sym (RefCell tp)
-> SymGlobalState sym
-> IO (RegValue sym tp)
forall sym bak (tp :: CrucibleType).
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> TypeRepr tp
-> MuxTree sym (RefCell tp)
-> SymGlobalState sym
-> IO (RegValue sym tp)
EvalStmt.readRef bak
bak IntrinsicTypes sym
iTypes TypeRepr tp
tpr MuxTree sym (RefCell tp)
r SymGlobalState sym
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 :: forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
TypeRepr tp
-> MuxTree sym (RefCell tp)
-> RegValue sym tp
-> OverrideSim p sym ext rtp args ret ()
writeMuxTreeRef TypeRepr tp
tpr MuxTree sym (RefCell tp)
r RegValue sym tp
v =
  do sym
sym <- OverrideSim p sym ext rtp args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
     IntrinsicTypes sym
iTypes <- SimContext p sym ext -> IntrinsicTypes sym
forall personality sym ext.
SimContext personality sym ext -> IntrinsicTypes sym
ctxIntrinsicTypes (SimContext p sym ext -> IntrinsicTypes sym)
-> OverrideSim p sym ext rtp args ret (SimContext p sym ext)
-> OverrideSim p sym ext rtp args ret (IntrinsicTypes sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SimContext p sym ext)
-> OverrideSim p sym ext rtp args ret (SimContext p sym ext)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext
     SymGlobalState sym
globals <- Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SymGlobalState sym)
-> OverrideSim p sym ext rtp args ret (SymGlobalState sym)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
  -> Const
       (SymGlobalState sym)
       (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym
     -> Const (SymGlobalState sym) (SymGlobalState sym))
    -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
    -> Const
         (SymGlobalState sym)
         (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (SymGlobalState sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame ((TopFrame sym ext (OverrideLang ret) ('Just args)
  -> Const
       (SymGlobalState sym)
       (TopFrame sym ext (OverrideLang ret) ('Just args)))
 -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (SymGlobalState sym)
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym
     -> Const (SymGlobalState sym) (SymGlobalState sym))
    -> TopFrame sym ext (OverrideLang ret) ('Just args)
    -> Const
         (SymGlobalState sym)
         (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym
    -> Const (SymGlobalState sym) (SymGlobalState sym))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym
 -> Const (SymGlobalState sym) (SymGlobalState sym))
-> TopFrame sym ext (OverrideLang ret) ('Just args)
-> Const
     (SymGlobalState sym)
     (TopFrame sym ext (OverrideLang ret) ('Just args))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals)
     SymGlobalState sym
globals' <- IO (SymGlobalState sym)
-> OverrideSim p sym ext rtp args ret (SymGlobalState sym)
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymGlobalState sym)
 -> OverrideSim p sym ext rtp args ret (SymGlobalState sym))
-> IO (SymGlobalState sym)
-> OverrideSim p sym ext rtp args ret (SymGlobalState sym)
forall a b. (a -> b) -> a -> b
$ sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> MuxTree sym (RefCell tp)
-> PartExpr (Pred sym) (RegValue sym tp)
-> SymGlobalState sym
-> IO (SymGlobalState sym)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> MuxTree sym (RefCell tp)
-> PartExpr (Pred sym) (RegValue sym tp)
-> SymGlobalState sym
-> IO (SymGlobalState sym)
EvalStmt.alterRef sym
sym IntrinsicTypes sym
iTypes TypeRepr tp
tpr MuxTree sym (RefCell tp)
r (sym -> RegValue sym tp -> PartExpr (Pred sym) (RegValue sym tp)
forall sym v.
IsExprBuilder sym =>
sym -> v -> PartExpr (Pred sym) v
justPartExpr sym
sym RegValue sym tp
v) SymGlobalState sym
globals
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
  -> Identity
       (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
    -> Identity
         (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (OverrideLang ret) ('Just args)
 -> Identity (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame ((TopFrame sym ext (OverrideLang ret) ('Just args)
  -> Identity (TopFrame sym ext (OverrideLang ret) ('Just args)))
 -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> TopFrame sym ext (OverrideLang ret) ('Just args)
    -> Identity (TopFrame sym ext (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym -> Identity (SymGlobalState sym))
-> TopFrame sym ext (OverrideLang ret) ('Just args)
-> Identity (TopFrame sym ext (OverrideLang ret) ('Just args))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> SymGlobalState sym -> OverrideSim p sym ext rtp args ret ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= SymGlobalState sym
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 :: forall (tp :: CrucibleType) p sym ext rtp
       (args :: Ctx CrucibleType).
TypeRepr tp
-> OverrideSim p sym ext rtp args tp (RegValue sym tp)
-> ExecCont p sym ext rtp (OverrideLang tp) ('Just args)
runOverrideSim TypeRepr tp
tp OverrideSim p sym ext rtp args tp (RegValue sym tp)
m = (SimState p sym ext rtp (OverrideLang tp) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang tp) ('Just args))
     IO
     (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT ((SimState p sym ext rtp (OverrideLang tp) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> ReaderT
      (SimState p sym ext rtp (OverrideLang tp) ('Just args))
      IO
      (ExecState p sym ext rtp))
-> (SimState p sym ext rtp (OverrideLang tp) ('Just args)
    -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang tp) ('Just args))
     IO
     (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ \SimState p sym ext rtp (OverrideLang tp) ('Just args)
s0 -> SimState p sym ext rtp (OverrideLang tp) ('Just args)
-> forall a. IsSymInterfaceProof sym a
forall p sym ext r f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext r f args -> forall a. IsSymInterfaceProof sym a
stateSolverProof SimState p sym ext rtp (OverrideLang tp) ('Just args)
s0 IsSymInterfaceProof sym (IO (ExecState p sym ext rtp))
-> IsSymInterfaceProof sym (IO (ExecState p sym ext rtp))
forall a b. (a -> b) -> a -> b
$
  StateContT
  (SimState p sym ext rtp (OverrideLang tp) ('Just args))
  (ExecState p sym ext rtp)
  IO
  (RegValue sym tp)
-> (RegValue sym tp
    -> SimState p sym ext rtp (OverrideLang tp) ('Just args)
    -> IO (ExecState p sym ext rtp))
-> SimState p sym ext rtp (OverrideLang tp) ('Just args)
-> IO (ExecState p sym ext rtp)
forall s r (m :: Type -> Type) a.
StateContT s r m a -> (a -> s -> m r) -> s -> m r
runStateContT (OverrideSim p sym ext rtp args tp (RegValue sym tp)
-> StateContT
     (SimState p sym ext rtp (OverrideLang tp) ('Just args))
     (ExecState p sym ext rtp)
     IO
     (RegValue sym tp)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
OverrideSim p sym ext rtp args ret a
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
unSim OverrideSim p sym ext rtp args tp (RegValue sym tp)
m) (\RegValue sym tp
v -> ReaderT
  (SimState p sym ext rtp (OverrideLang tp) ('Just args))
  IO
  (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang tp) ('Just args)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (RegEntry sym (FrameRetType (OverrideLang tp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang tp) ('Just args))
     IO
     (ExecState p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
RegEntry sym (FrameRetType f) -> ExecCont p sym ext rtp f args
returnValue (TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr tp
tp RegValue sym tp
v))) SimState p sym ext rtp (OverrideLang tp) ('Just args)
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' :: forall (ret :: CrucibleType) p sym ext (args :: Ctx CrucibleType).
FunctionName
-> TypeRepr ret
-> (forall r. OverrideSim p sym ext r args ret (RegValue sym ret))
-> Override p sym ext args ret
mkOverride' FunctionName
nm TypeRepr ret
tp forall r. OverrideSim p sym ext r args ret (RegValue sym ret)
f =
  Override { overrideName :: FunctionName
overrideName = FunctionName
nm
           , overrideHandler :: forall r. ExecCont p sym ext r (OverrideLang ret) ('Just args)
overrideHandler = TypeRepr ret
-> OverrideSim p sym ext r args ret (RegValue sym ret)
-> ExecCont p sym ext r (OverrideLang ret) ('Just args)
forall (tp :: CrucibleType) p sym ext rtp
       (args :: Ctx CrucibleType).
TypeRepr tp
-> OverrideSim p sym ext rtp args tp (RegValue sym tp)
-> ExecCont p sym ext rtp (OverrideLang tp) ('Just args)
runOverrideSim TypeRepr ret
tp OverrideSim p sym ext r args ret (RegValue sym ret)
forall r. OverrideSim p sym ext r args ret (RegValue sym ret)
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 :: forall (ret :: CrucibleType) p sym ext (args :: Ctx CrucibleType).
KnownRepr TypeRepr ret =>
FunctionName
-> (forall r. OverrideSim p sym ext r args ret (RegValue sym ret))
-> Override p sym ext args ret
mkOverride FunctionName
nm = FunctionName
-> TypeRepr ret
-> (forall r. OverrideSim p sym ext r args ret (RegValue sym ret))
-> Override p sym ext args ret
forall (ret :: CrucibleType) p sym ext (args :: Ctx CrucibleType).
FunctionName
-> TypeRepr ret
-> (forall r. OverrideSim p sym ext r args ret (RegValue sym ret))
-> Override p sym ext args ret
mkOverride' FunctionName
nm TypeRepr ret
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

-- | Return override arguments.
getOverrideArgs :: OverrideSim p sym ext rtp args ret (RegMap sym args)
getOverrideArgs :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (RegMap sym args)
getOverrideArgs = Getting
  (RegMap sym args)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (RegMap sym args)
-> OverrideSim p sym ext rtp args ret (RegMap sym args)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use ((OverrideFrame sym ret args
 -> Const (RegMap sym args) (OverrideFrame sym ret args))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Const
     (RegMap sym args)
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext q (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> SimState p sym ext q (OverrideLang r) ('Just a)
-> f (SimState p sym ext q (OverrideLang r) ('Just a'))
stateOverrideFrame((OverrideFrame sym ret args
  -> Const (RegMap sym args) (OverrideFrame sym ret args))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Const
      (RegMap sym args)
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> ((RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
    -> OverrideFrame sym ret args
    -> Const (RegMap sym args) (OverrideFrame sym ret args))
-> Getting
     (RegMap sym args)
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (RegMap sym args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
-> OverrideFrame sym ret args
-> Const (RegMap sym args) (OverrideFrame sym ret args)
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args'))
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args')
overrideRegMap)

withSimContext :: StateT (SimContext p sym ext) IO a -> OverrideSim p sym ext rtp args ret a
withSimContext :: forall p sym ext a rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
StateT (SimContext p sym ext) IO a
-> OverrideSim p sym ext rtp args ret a
withSimContext StateT (SimContext p sym ext) IO a
m =
  do SimContext p sym ext
ctx <- Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SimContext p sym ext)
-> OverrideSim p sym ext rtp args ret (SimContext p sym ext)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext
     (a
r,SimContext p sym ext
ctx') <- IO (a, SimContext p sym ext)
-> OverrideSim p sym ext rtp args ret (a, SimContext p sym ext)
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (a, SimContext p sym ext)
 -> OverrideSim p sym ext rtp args ret (a, SimContext p sym ext))
-> IO (a, SimContext p sym ext)
-> OverrideSim p sym ext rtp args ret (a, SimContext p sym ext)
forall a b. (a -> b) -> a -> b
$ StateT (SimContext p sym ext) IO a
-> SimContext p sym ext -> IO (a, SimContext p sym ext)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT StateT (SimContext p sym ext) IO a
m SimContext p sym ext
ctx
     (SimContext p sym ext -> Identity (SimContext p sym ext))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> Identity
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext ((SimContext p sym ext -> Identity (SimContext p sym ext))
 -> SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> SimContext p sym ext -> OverrideSim p sym ext rtp args ret ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= SimContext p sym ext
ctx'
     a -> OverrideSim p sym ext rtp args ret a
forall a. a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
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 :: forall sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType) p
       rtp (a :: Ctx CrucibleType) (r :: CrucibleType).
(IsExprBuilder sym, IsSyntaxExtension ext) =>
FnVal sym args ret
-> RegMap sym args
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
callFnVal FnVal sym args ret
cl RegMap sym args
args =
  StateContT
  (SimState p sym ext rtp (OverrideLang r) ('Just a))
  (ExecState p sym ext rtp)
  IO
  (RegEntry sym ret)
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang r) ('Just a))
   (ExecState p sym ext rtp)
   IO
   (RegEntry sym ret)
 -> OverrideSim p sym ext rtp a r (RegEntry sym ret))
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     (ExecState p sym ext rtp)
     IO
     (RegEntry sym ret)
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
forall a b. (a -> b) -> a -> b
$ ((RegEntry sym ret
  -> SimState p sym ext rtp (OverrideLang r) ('Just a)
  -> IO (ExecState p sym ext rtp))
 -> SimState p sym ext rtp (OverrideLang r) ('Just a)
 -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     (ExecState p sym ext rtp)
     IO
     (RegEntry sym ret)
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((RegEntry sym ret
   -> SimState p sym ext rtp (OverrideLang r) ('Just a)
   -> IO (ExecState p sym ext rtp))
  -> SimState p sym ext rtp (OverrideLang r) ('Just a)
  -> IO (ExecState p sym ext rtp))
 -> StateContT
      (SimState p sym ext rtp (OverrideLang r) ('Just a))
      (ExecState p sym ext rtp)
      IO
      (RegEntry sym ret))
-> ((RegEntry sym ret
     -> SimState p sym ext rtp (OverrideLang r) ('Just a)
     -> IO (ExecState p sym ext rtp))
    -> SimState p sym ext rtp (OverrideLang r) ('Just a)
    -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     (ExecState p sym ext rtp)
     IO
     (RegEntry sym ret)
forall a b. (a -> b) -> a -> b
$ \RegEntry sym ret
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
c -> ReaderT
  (SimState p sym ext rtp (OverrideLang r) ('Just a))
  IO
  (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (ReaderT
   (SimState p sym ext rtp (OverrideLang r) ('Just a))
   IO
   (ExecState p sym ext rtp)
 -> SimState p sym ext rtp (OverrideLang r) ('Just a)
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     IO
     (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ do
    sym
sym <- Getting sym (SimState p sym ext rtp (OverrideLang r) ('Just a)) sym
-> ReaderT
     (SimState p sym ext rtp (OverrideLang r) ('Just a)) IO sym
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting sym (SimState p sym ext rtp (OverrideLang r) ('Just a)) sym
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(sym -> f2 sym)
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateSymInterface
    ProgramLoc
loc <- IO ProgramLoc
-> ReaderT
     (SimState p sym ext rtp (OverrideLang r) ('Just a)) IO ProgramLoc
forall a.
IO a
-> ReaderT (SimState p sym ext rtp (OverrideLang r) ('Just a)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ProgramLoc
 -> ReaderT
      (SimState p sym ext rtp (OverrideLang r) ('Just a)) IO ProgramLoc)
-> IO ProgramLoc
-> ReaderT
     (SimState p sym ext rtp (OverrideLang r) ('Just a)) IO ProgramLoc
forall a b. (a -> b) -> a -> b
$ sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
    FnVal sym args ret
-> RegMap sym args
-> ReturnHandler ret p sym ext rtp (OverrideLang r) ('Just a)
-> ProgramLoc
-> ReaderT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     IO
     (ExecState p sym ext rtp)
forall sym (args :: Ctx CrucibleType) (ret :: CrucibleType) p ext
       rtp f (a :: Maybe (Ctx CrucibleType)).
IsExprBuilder sym =>
FnVal sym args ret
-> RegMap sym args
-> ReturnHandler ret p sym ext rtp f a
-> ProgramLoc
-> ExecCont p sym ext rtp f a
callFunction FnVal sym args ret
cl RegMap sym args
args ((RegEntry sym ret
 -> SimState p sym ext rtp (OverrideLang r) ('Just a)
 -> IO (ExecState p sym ext rtp))
-> ReturnHandler ret p sym ext rtp (OverrideLang r) ('Just a)
forall sym (ret :: CrucibleType) p ext root (r :: CrucibleType)
       (args1 :: Ctx CrucibleType).
(RegEntry sym ret
 -> SimState p sym ext root (OverrideLang r) ('Just args1)
 -> IO (ExecState p sym ext root))
-> ReturnHandler ret p sym ext root (OverrideLang r) ('Just args1)
ReturnToOverride RegEntry sym ret
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
c) ProgramLoc
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' :: forall sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType) p
       rtp (a :: Ctx CrucibleType) (r :: CrucibleType).
(IsExprBuilder sym, IsSyntaxExtension ext) =>
FnVal sym args ret
-> Assignment (RegValue' sym) args
-> OverrideSim p sym ext rtp a r (RegValue sym ret)
callFnVal' FnVal sym args ret
cl Assignment (RegValue' sym) args
args =
  do let FunctionHandleRepr Assignment TypeRepr args
CtxRepr ctx
tps TypeRepr ret
_ = FnVal sym args ret -> TypeRepr (FunctionHandleType args ret)
forall sym (args :: Ctx CrucibleType) (res :: CrucibleType).
FnVal sym args res -> TypeRepr (FunctionHandleType args res)
fnValType FnVal sym args ret
cl
     let args' :: Assignment (RegEntry sym) args
args' = (forall (x :: CrucibleType).
 TypeRepr x -> RegValue' sym x -> RegEntry sym x)
-> Assignment TypeRepr args
-> Assignment (RegValue' sym) args
-> Assignment (RegEntry sym) args
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
       (a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
Ctx.zipWith (\TypeRepr x
tp (RV RegValue sym x
x) -> TypeRepr x -> RegValue sym x -> RegEntry sym x
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr x
tp RegValue sym x
x) Assignment TypeRepr args
tps Assignment (RegValue' sym) args
args
     RegEntry sym ret -> RegValue sym ret
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue (RegEntry sym ret -> RegValue sym ret)
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
-> OverrideSim p sym ext rtp a r (RegValue sym ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> FnVal sym args ret
-> RegMap sym args
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
forall sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType) p
       rtp (a :: Ctx CrucibleType) (r :: CrucibleType).
(IsExprBuilder sym, IsSyntaxExtension ext) =>
FnVal sym args ret
-> RegMap sym args
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
callFnVal FnVal sym args ret
cl (Assignment (RegEntry sym) args -> RegMap sym args
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap Assignment (RegEntry sym) args
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 :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType) sym p rtp
       (a :: Ctx CrucibleType) (r :: CrucibleType).
IsSyntaxExtension ext =>
CFG ext blocks init ret
-> RegMap sym init
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
callCFG CFG ext blocks init ret
cfg = CFG ext blocks init ret
-> BlockID blocks init
-> RegMap sym init
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType)
       (args :: Ctx CrucibleType) sym p rtp (a :: Ctx CrucibleType)
       (r :: CrucibleType).
IsSyntaxExtension ext =>
CFG ext blocks init ret
-> BlockID blocks args
-> RegMap sym args
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
callBlock CFG ext blocks init ret
cfg (CFG ext blocks init ret -> BlockID blocks init
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockID blocks init
cfgEntryBlockID CFG ext blocks init ret
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 :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType)
       (args :: Ctx CrucibleType) sym p rtp (a :: Ctx CrucibleType)
       (r :: CrucibleType).
IsSyntaxExtension ext =>
CFG ext blocks init ret
-> BlockID blocks args
-> RegMap sym args
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
callBlock CFG ext blocks init ret
cfg BlockID blocks args
bid RegMap sym args
args =
  StateContT
  (SimState p sym ext rtp (OverrideLang r) ('Just a))
  (ExecState p sym ext rtp)
  IO
  (RegEntry sym ret)
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang r) ('Just a))
   (ExecState p sym ext rtp)
   IO
   (RegEntry sym ret)
 -> OverrideSim p sym ext rtp a r (RegEntry sym ret))
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     (ExecState p sym ext rtp)
     IO
     (RegEntry sym ret)
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
forall a b. (a -> b) -> a -> b
$ ((RegEntry sym ret
  -> SimState p sym ext rtp (OverrideLang r) ('Just a)
  -> IO (ExecState p sym ext rtp))
 -> SimState p sym ext rtp (OverrideLang r) ('Just a)
 -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     (ExecState p sym ext rtp)
     IO
     (RegEntry sym ret)
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((RegEntry sym ret
   -> SimState p sym ext rtp (OverrideLang r) ('Just a)
   -> IO (ExecState p sym ext rtp))
  -> SimState p sym ext rtp (OverrideLang r) ('Just a)
  -> IO (ExecState p sym ext rtp))
 -> StateContT
      (SimState p sym ext rtp (OverrideLang r) ('Just a))
      (ExecState p sym ext rtp)
      IO
      (RegEntry sym ret))
-> ((RegEntry sym ret
     -> SimState p sym ext rtp (OverrideLang r) ('Just a)
     -> IO (ExecState p sym ext rtp))
    -> SimState p sym ext rtp (OverrideLang r) ('Just a)
    -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     (ExecState p sym ext rtp)
     IO
     (RegEntry sym ret)
forall a b. (a -> b) -> a -> b
$ \RegEntry sym ret
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
c -> ReaderT
  (SimState p sym ext rtp (OverrideLang r) ('Just a))
  IO
  (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (ReaderT
   (SimState p sym ext rtp (OverrideLang r) ('Just a))
   IO
   (ExecState p sym ext rtp)
 -> SimState p sym ext rtp (OverrideLang r) ('Just a)
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     IO
     (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$
    let f :: CallFrame sym ext blocks ret args
f = CFG ext blocks init ret
-> BlockID blocks args
-> CFGPostdom blocks
-> RegMap sym args
-> CallFrame sym ext blocks ret args
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType)
       (args :: Ctx CrucibleType) sym.
CFG ext blocks init ret
-> BlockID blocks args
-> CFGPostdom blocks
-> RegMap sym args
-> CallFrame sym ext blocks ret args
mkBlockFrame CFG ext blocks init ret
cfg BlockID blocks args
bid (CFG ext blocks init ret -> CFGPostdom blocks
forall ext (b :: Ctx (Ctx CrucibleType)) (i :: Ctx CrucibleType)
       (r :: CrucibleType).
CFG ext b i r -> CFGPostdom b
postdomInfo CFG ext blocks init ret
cfg) RegMap sym args
args in
    (SimState p sym ext rtp (OverrideLang r) ('Just a)
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     IO
     (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT ((SimState p sym ext rtp (OverrideLang r) ('Just a)
  -> IO (ExecState p sym ext rtp))
 -> ReaderT
      (SimState p sym ext rtp (OverrideLang r) ('Just a))
      IO
      (ExecState p sym ext rtp))
-> (SimState p sym ext rtp (OverrideLang r) ('Just a)
    -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     IO
     (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp -> IO (ExecState p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecState p sym ext rtp -> IO (ExecState p sym ext rtp))
-> (SimState p sym ext rtp (OverrideLang r) ('Just a)
    -> ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReturnHandler ret p sym ext rtp (OverrideLang r) ('Just a)
-> ResolvedCall p sym ext ret
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> ExecState p sym ext rtp
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType))
       (ret :: CrucibleType).
ReturnHandler ret p sym ext rtp f a
-> ResolvedCall p sym ext ret
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
CallState ((RegEntry sym ret
 -> SimState p sym ext rtp (OverrideLang r) ('Just a)
 -> IO (ExecState p sym ext rtp))
-> ReturnHandler ret p sym ext rtp (OverrideLang r) ('Just a)
forall sym (ret :: CrucibleType) p ext root (r :: CrucibleType)
       (args1 :: Ctx CrucibleType).
(RegEntry sym ret
 -> SimState p sym ext root (OverrideLang r) ('Just args1)
 -> IO (ExecState p sym ext root))
-> ReturnHandler ret p sym ext root (OverrideLang r) ('Just args1)
ReturnToOverride RegEntry sym ret
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
c) (BlockID blocks args
-> CallFrame sym ext blocks ret args -> ResolvedCall p sym ext ret
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) sym ext (ret :: CrucibleType) p.
BlockID blocks args
-> CallFrame sym ext blocks ret args -> ResolvedCall p sym ext ret
CrucibleCall BlockID blocks args
bid CallFrame sym ext blocks ret args
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 :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType) p sym ext
       rtp (a :: Ctx CrucibleType) (r :: CrucibleType).
FnHandle args ret
-> Override p sym ext args ret
-> RegMap sym args
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
callOverride FnHandle args ret
h Override p sym ext args ret
ovr RegMap sym args
args =
  StateContT
  (SimState p sym ext rtp (OverrideLang r) ('Just a))
  (ExecState p sym ext rtp)
  IO
  (RegEntry sym ret)
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang r) ('Just a))
   (ExecState p sym ext rtp)
   IO
   (RegEntry sym ret)
 -> OverrideSim p sym ext rtp a r (RegEntry sym ret))
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     (ExecState p sym ext rtp)
     IO
     (RegEntry sym ret)
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
forall a b. (a -> b) -> a -> b
$ ((RegEntry sym ret
  -> SimState p sym ext rtp (OverrideLang r) ('Just a)
  -> IO (ExecState p sym ext rtp))
 -> SimState p sym ext rtp (OverrideLang r) ('Just a)
 -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     (ExecState p sym ext rtp)
     IO
     (RegEntry sym ret)
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((RegEntry sym ret
   -> SimState p sym ext rtp (OverrideLang r) ('Just a)
   -> IO (ExecState p sym ext rtp))
  -> SimState p sym ext rtp (OverrideLang r) ('Just a)
  -> IO (ExecState p sym ext rtp))
 -> StateContT
      (SimState p sym ext rtp (OverrideLang r) ('Just a))
      (ExecState p sym ext rtp)
      IO
      (RegEntry sym ret))
-> ((RegEntry sym ret
     -> SimState p sym ext rtp (OverrideLang r) ('Just a)
     -> IO (ExecState p sym ext rtp))
    -> SimState p sym ext rtp (OverrideLang r) ('Just a)
    -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     (ExecState p sym ext rtp)
     IO
     (RegEntry sym ret)
forall a b. (a -> b) -> a -> b
$ \RegEntry sym ret
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
c -> ReaderT
  (SimState p sym ext rtp (OverrideLang r) ('Just a))
  IO
  (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (ReaderT
   (SimState p sym ext rtp (OverrideLang r) ('Just a))
   IO
   (ExecState p sym ext rtp)
 -> SimState p sym ext rtp (OverrideLang r) ('Just a)
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     IO
     (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$
    let f :: OverrideFrame sym ret args
f = FunctionName
-> SomeHandle -> RegMap sym args -> OverrideFrame sym ret args
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType).
FunctionName
-> SomeHandle -> RegMap sym args -> OverrideFrame sym ret args
OverrideFrame (Override p sym ext args ret -> FunctionName
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Override p sym ext args ret -> FunctionName
overrideName Override p sym ext args ret
ovr) (FnHandle args ret -> SomeHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeHandle
SomeHandle FnHandle args ret
h) RegMap sym args
args in
    (SimState p sym ext rtp (OverrideLang r) ('Just a)
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     IO
     (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT ((SimState p sym ext rtp (OverrideLang r) ('Just a)
  -> IO (ExecState p sym ext rtp))
 -> ReaderT
      (SimState p sym ext rtp (OverrideLang r) ('Just a))
      IO
      (ExecState p sym ext rtp))
-> (SimState p sym ext rtp (OverrideLang r) ('Just a)
    -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang r) ('Just a))
     IO
     (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp -> IO (ExecState p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecState p sym ext rtp -> IO (ExecState p sym ext rtp))
-> (SimState p sym ext rtp (OverrideLang r) ('Just a)
    -> ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReturnHandler ret p sym ext rtp (OverrideLang r) ('Just a)
-> ResolvedCall p sym ext ret
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> ExecState p sym ext rtp
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType))
       (ret :: CrucibleType).
ReturnHandler ret p sym ext rtp f a
-> ResolvedCall p sym ext ret
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
CallState ((RegEntry sym ret
 -> SimState p sym ext rtp (OverrideLang r) ('Just a)
 -> IO (ExecState p sym ext rtp))
-> ReturnHandler ret p sym ext rtp (OverrideLang r) ('Just a)
forall sym (ret :: CrucibleType) p ext root (r :: CrucibleType)
       (args1 :: Ctx CrucibleType).
(RegEntry sym ret
 -> SimState p sym ext root (OverrideLang r) ('Just args1)
 -> IO (ExecState p sym ext root))
-> ReturnHandler ret p sym ext root (OverrideLang r) ('Just args1)
ReturnToOverride RegEntry sym ret
-> SimState p sym ext rtp (OverrideLang r) ('Just a)
-> IO (ExecState p sym ext rtp)
c) (Override p sym ext args ret
-> OverrideFrame sym ret args -> ResolvedCall p sym ext ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Override p sym ext args ret
-> OverrideFrame sym ret args -> ResolvedCall p sym ext ret
OverrideCall Override p sym ext args ret
ovr OverrideFrame sym ret args
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 :: forall sym p ext rtp (args :: Ctx CrucibleType)
       (res :: CrucibleType) a.
IsSymInterface sym =>
SimErrorReason -> OverrideSim p sym ext rtp args res a
overrideError SimErrorReason
err = StateContT
  (SimState p sym ext rtp (OverrideLang res) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args res a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang res) ('Just args))
   (ExecState p sym ext rtp)
   IO
   a
 -> OverrideSim p sym ext rtp args res a)
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
-> OverrideSim p sym ext rtp args res a
forall a b. (a -> b) -> a -> b
$ ((a
  -> SimState p sym ext rtp (OverrideLang res) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> SimState p sym ext rtp (OverrideLang res) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((a
   -> SimState p sym ext rtp (OverrideLang res) ('Just args)
   -> IO (ExecState p sym ext rtp))
  -> SimState p sym ext rtp (OverrideLang res) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> StateContT
      (SimState p sym ext rtp (OverrideLang res) ('Just args))
      (ExecState p sym ext rtp)
      IO
      a)
-> ((a
     -> SimState p sym ext rtp (OverrideLang res) ('Just args)
     -> IO (ExecState p sym ext rtp))
    -> SimState p sym ext rtp (OverrideLang res) ('Just args)
    -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall a b. (a -> b) -> a -> b
$ \a
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
_ -> SimErrorReason
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimErrorReason
-> SimState p sym ext rtp f args -> IO (ExecState p sym ext rtp)
runErrorHandler SimErrorReason
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 :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (res :: CrucibleType) a.
AbortExecReason -> OverrideSim p sym ext rtp args res a
overrideAbort AbortExecReason
abt = StateContT
  (SimState p sym ext rtp (OverrideLang res) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args res a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang res) ('Just args))
   (ExecState p sym ext rtp)
   IO
   a
 -> OverrideSim p sym ext rtp args res a)
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
-> OverrideSim p sym ext rtp args res a
forall a b. (a -> b) -> a -> b
$ ((a
  -> SimState p sym ext rtp (OverrideLang res) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> SimState p sym ext rtp (OverrideLang res) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((a
   -> SimState p sym ext rtp (OverrideLang res) ('Just args)
   -> IO (ExecState p sym ext rtp))
  -> SimState p sym ext rtp (OverrideLang res) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> StateContT
      (SimState p sym ext rtp (OverrideLang res) ('Just args))
      (ExecState p sym ext rtp)
      IO
      a)
-> ((a
     -> SimState p sym ext rtp (OverrideLang res) ('Just args)
     -> IO (ExecState p sym ext rtp))
    -> SimState p sym ext rtp (OverrideLang res) ('Just args)
    -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall a b. (a -> b) -> a -> b
$ \a
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
_ -> AbortExecReason
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
AbortExecReason
-> SimState p sym ext rtp f args -> IO (ExecState p sym ext rtp)
runAbortHandler AbortExecReason
abt

overrideReturn :: KnownRepr TypeRepr res => RegValue sym res -> OverrideSim p sym ext rtp args res a
overrideReturn :: forall (res :: CrucibleType) sym p ext rtp
       (args :: Ctx CrucibleType) a.
KnownRepr TypeRepr res =>
RegValue sym res -> OverrideSim p sym ext rtp args res a
overrideReturn RegValue sym res
v = StateContT
  (SimState p sym ext rtp (OverrideLang res) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args res a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang res) ('Just args))
   (ExecState p sym ext rtp)
   IO
   a
 -> OverrideSim p sym ext rtp args res a)
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
-> OverrideSim p sym ext rtp args res a
forall a b. (a -> b) -> a -> b
$ ((a
  -> SimState p sym ext rtp (OverrideLang res) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> SimState p sym ext rtp (OverrideLang res) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((a
   -> SimState p sym ext rtp (OverrideLang res) ('Just args)
   -> IO (ExecState p sym ext rtp))
  -> SimState p sym ext rtp (OverrideLang res) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> StateContT
      (SimState p sym ext rtp (OverrideLang res) ('Just args))
      (ExecState p sym ext rtp)
      IO
      a)
-> ((a
     -> SimState p sym ext rtp (OverrideLang res) ('Just args)
     -> IO (ExecState p sym ext rtp))
    -> SimState p sym ext rtp (OverrideLang res) ('Just args)
    -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall a b. (a -> b) -> a -> b
$ \a
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
_ -> ReaderT
  (SimState p sym ext rtp (OverrideLang res) ('Just args))
  IO
  (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (ReaderT
   (SimState p sym ext rtp (OverrideLang res) ('Just args))
   IO
   (ExecState p sym ext rtp)
 -> SimState p sym ext rtp (OverrideLang res) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ RegEntry sym (FrameRetType (OverrideLang res))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
RegEntry sym (FrameRetType f) -> ExecCont p sym ext rtp f args
returnValue (TypeRepr res -> RegValue sym res -> RegEntry sym res
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr res
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RegValue sym res
v)

overrideReturn' :: RegEntry sym res -> OverrideSim p sym ext rtp args res a
overrideReturn' :: forall sym (res :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) a.
RegEntry sym res -> OverrideSim p sym ext rtp args res a
overrideReturn' RegEntry sym res
v = StateContT
  (SimState p sym ext rtp (OverrideLang res) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args res a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang res) ('Just args))
   (ExecState p sym ext rtp)
   IO
   a
 -> OverrideSim p sym ext rtp args res a)
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
-> OverrideSim p sym ext rtp args res a
forall a b. (a -> b) -> a -> b
$ ((a
  -> SimState p sym ext rtp (OverrideLang res) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> SimState p sym ext rtp (OverrideLang res) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((a
   -> SimState p sym ext rtp (OverrideLang res) ('Just args)
   -> IO (ExecState p sym ext rtp))
  -> SimState p sym ext rtp (OverrideLang res) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> StateContT
      (SimState p sym ext rtp (OverrideLang res) ('Just args))
      (ExecState p sym ext rtp)
      IO
      a)
-> ((a
     -> SimState p sym ext rtp (OverrideLang res) ('Just args)
     -> IO (ExecState p sym ext rtp))
    -> SimState p sym ext rtp (OverrideLang res) ('Just args)
    -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall a b. (a -> b) -> a -> b
$ \a
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
_ -> ReaderT
  (SimState p sym ext rtp (OverrideLang res) ('Just args))
  IO
  (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (ReaderT
   (SimState p sym ext rtp (OverrideLang res) ('Just args))
   IO
   (ExecState p sym ext rtp)
 -> SimState p sym ext rtp (OverrideLang res) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ RegEntry sym (FrameRetType (OverrideLang res))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
RegEntry sym (FrameRetType f) -> ExecCont p sym ext rtp f args
returnValue RegEntry sym res
RegEntry sym (FrameRetType (OverrideLang res))
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 :: forall sym (then_args :: Ctx CrucibleType) p ext rtp
       (res :: CrucibleType) a (else_args :: Ctx CrucibleType)
       (args :: Ctx CrucibleType).
IsSymInterface sym =>
Pred sym
-> RegMap sym then_args
-> OverrideSim p sym ext rtp then_args res a
-> Maybe Position
-> RegMap sym else_args
-> OverrideSim p sym ext rtp else_args res a
-> Maybe Position
-> OverrideSim p sym ext rtp args res a
symbolicBranch Pred sym
p RegMap sym then_args
thn_args OverrideSim p sym ext rtp then_args res a
thn Maybe Position
thn_pos RegMap sym else_args
els_args OverrideSim p sym ext rtp else_args res a
els Maybe Position
els_pos =
  StateContT
  (SimState p sym ext rtp (OverrideLang res) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args res a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang res) ('Just args))
   (ExecState p sym ext rtp)
   IO
   a
 -> OverrideSim p sym ext rtp args res a)
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
-> OverrideSim p sym ext rtp args res a
forall a b. (a -> b) -> a -> b
$ ((a
  -> SimState p sym ext rtp (OverrideLang res) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> SimState p sym ext rtp (OverrideLang res) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((a
   -> SimState p sym ext rtp (OverrideLang res) ('Just args)
   -> IO (ExecState p sym ext rtp))
  -> SimState p sym ext rtp (OverrideLang res) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> StateContT
      (SimState p sym ext rtp (OverrideLang res) ('Just args))
      (ExecState p sym ext rtp)
      IO
      a)
-> ((a
     -> SimState p sym ext rtp (OverrideLang res) ('Just args)
     -> IO (ExecState p sym ext rtp))
    -> SimState p sym ext rtp (OverrideLang res) ('Just args)
    -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall a b. (a -> b) -> a -> b
$ \a
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
c -> ReaderT
  (SimState p sym ext rtp (OverrideLang res) ('Just args))
  IO
  (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (ReaderT
   (SimState p sym ext rtp (OverrideLang res) ('Just args))
   IO
   (ExecState p sym ext rtp)
 -> SimState p sym ext rtp (OverrideLang res) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$
    do RegMap sym args
old_args <- Getting
  (RegMap sym args)
  (SimState p sym ext rtp (OverrideLang res) ('Just args))
  (RegMap sym args)
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (RegMap sym args)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view ((ActiveTree p sym ext rtp (OverrideLang res) ('Just args)
 -> Const
      (RegMap sym args)
      (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> Const
     (RegMap sym args)
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree((ActiveTree p sym ext rtp (OverrideLang res) ('Just args)
  -> Const
       (RegMap sym args)
       (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
 -> SimState p sym ext rtp (OverrideLang res) ('Just args)
 -> Const
      (RegMap sym args)
      (SimState p sym ext rtp (OverrideLang res) ('Just args)))
-> ((RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
    -> ActiveTree p sym ext rtp (OverrideLang res) ('Just args)
    -> Const
         (RegMap sym args)
         (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> Getting
     (RegMap sym args)
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (RegMap sym args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TopFrame sym ext (OverrideLang res) ('Just args)
 -> Const
      (RegMap sym args)
      (TopFrame sym ext (OverrideLang res) ('Just args)))
-> ActiveTree p sym ext rtp (OverrideLang res) ('Just args)
-> Const
     (RegMap sym args)
     (ActiveTree p sym ext rtp (OverrideLang res) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame((TopFrame sym ext (OverrideLang res) ('Just args)
  -> Const
       (RegMap sym args)
       (TopFrame sym ext (OverrideLang res) ('Just args)))
 -> ActiveTree p sym ext rtp (OverrideLang res) ('Just args)
 -> Const
      (RegMap sym args)
      (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> ((RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
    -> TopFrame sym ext (OverrideLang res) ('Just args)
    -> Const
         (RegMap sym args)
         (TopFrame sym ext (OverrideLang res) ('Just args)))
-> (RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
-> ActiveTree p sym ext rtp (OverrideLang res) ('Just args)
-> Const
     (RegMap sym args)
     (ActiveTree p sym ext rtp (OverrideLang res) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(OverrideFrame sym res args
 -> Const (RegMap sym args) (OverrideFrame sym res args))
-> TopFrame sym ext (OverrideLang res) ('Just args)
-> Const
     (RegMap sym args)
     (TopFrame sym ext (OverrideLang res) ('Just args))
forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType)
       (r' :: CrucibleType) (args' :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> TopFrame sym ext (OverrideLang r) ('Just args)
-> f (TopFrame sym ext (OverrideLang r') ('Just args'))
overrideTopFrame((OverrideFrame sym res args
  -> Const (RegMap sym args) (OverrideFrame sym res args))
 -> TopFrame sym ext (OverrideLang res) ('Just args)
 -> Const
      (RegMap sym args)
      (TopFrame sym ext (OverrideLang res) ('Just args)))
-> ((RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
    -> OverrideFrame sym res args
    -> Const (RegMap sym args) (OverrideFrame sym res args))
-> (RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
-> TopFrame sym ext (OverrideLang res) ('Just args)
-> Const
     (RegMap sym args)
     (TopFrame sym ext (OverrideLang res) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
-> OverrideFrame sym res args
-> Const (RegMap sym args) (OverrideFrame sym res args)
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args'))
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args')
overrideRegMap)
       let thn' :: ReaderT
  (SimState p sym ext rtp (OverrideLang res) ('Just then_args))
  IO
  (ExecState p sym ext rtp)
thn' = (SimState p sym ext rtp (OverrideLang res) ('Just then_args)
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just then_args))
     IO
     (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT (StateContT
  (SimState p sym ext rtp (OverrideLang res) ('Just then_args))
  (ExecState p sym ext rtp)
  IO
  a
-> (a
    -> SimState p sym ext rtp (OverrideLang res) ('Just then_args)
    -> IO (ExecState p sym ext rtp))
-> SimState p sym ext rtp (OverrideLang res) ('Just then_args)
-> IO (ExecState p sym ext rtp)
forall s r (m :: Type -> Type) a.
StateContT s r m a -> (a -> s -> m r) -> s -> m r
runStateContT
                            (OverrideSim p sym ext rtp then_args res a
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just then_args))
     (ExecState p sym ext rtp)
     IO
     a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
OverrideSim p sym ext rtp args ret a
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
unSim OverrideSim p sym ext rtp then_args res a
thn)
                            (\a
x SimState p sym ext rtp (OverrideLang res) ('Just then_args)
st -> a
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
c a
x (SimState p sym ext rtp (OverrideLang res) ('Just then_args)
st SimState p sym ext rtp (OverrideLang res) ('Just then_args)
-> (SimState p sym ext rtp (OverrideLang res) ('Just then_args)
    -> SimState p sym ext rtp (OverrideLang res) ('Just args))
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
forall a b. a -> (a -> b) -> b
& (ActiveTree p sym ext rtp (OverrideLang res) ('Just then_args)
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> SimState p sym ext rtp (OverrideLang res) ('Just then_args)
-> Identity
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree((ActiveTree p sym ext rtp (OverrideLang res) ('Just then_args)
  -> Identity
       (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
 -> SimState p sym ext rtp (OverrideLang res) ('Just then_args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang res) ('Just args)))
-> ((RegMap sym then_args -> Identity (RegMap sym args))
    -> ActiveTree p sym ext rtp (OverrideLang res) ('Just then_args)
    -> Identity
         (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> (RegMap sym then_args -> Identity (RegMap sym args))
-> SimState p sym ext rtp (OverrideLang res) ('Just then_args)
-> Identity
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TopFrame sym ext (OverrideLang res) ('Just then_args)
 -> Identity (TopFrame sym ext (OverrideLang res) ('Just args)))
-> ActiveTree p sym ext rtp (OverrideLang res) ('Just then_args)
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang res) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame((TopFrame sym ext (OverrideLang res) ('Just then_args)
  -> Identity (TopFrame sym ext (OverrideLang res) ('Just args)))
 -> ActiveTree p sym ext rtp (OverrideLang res) ('Just then_args)
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> ((RegMap sym then_args -> Identity (RegMap sym args))
    -> TopFrame sym ext (OverrideLang res) ('Just then_args)
    -> Identity (TopFrame sym ext (OverrideLang res) ('Just args)))
-> (RegMap sym then_args -> Identity (RegMap sym args))
-> ActiveTree p sym ext rtp (OverrideLang res) ('Just then_args)
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang res) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(OverrideFrame sym res then_args
 -> Identity (OverrideFrame sym res args))
-> TopFrame sym ext (OverrideLang res) ('Just then_args)
-> Identity (TopFrame sym ext (OverrideLang res) ('Just args))
forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType)
       (r' :: CrucibleType) (args' :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> TopFrame sym ext (OverrideLang r) ('Just args)
-> f (TopFrame sym ext (OverrideLang r') ('Just args'))
overrideTopFrame((OverrideFrame sym res then_args
  -> Identity (OverrideFrame sym res args))
 -> TopFrame sym ext (OverrideLang res) ('Just then_args)
 -> Identity (TopFrame sym ext (OverrideLang res) ('Just args)))
-> ((RegMap sym then_args -> Identity (RegMap sym args))
    -> OverrideFrame sym res then_args
    -> Identity (OverrideFrame sym res args))
-> (RegMap sym then_args -> Identity (RegMap sym args))
-> TopFrame sym ext (OverrideLang res) ('Just then_args)
-> Identity (TopFrame sym ext (OverrideLang res) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(RegMap sym then_args -> Identity (RegMap sym args))
-> OverrideFrame sym res then_args
-> Identity (OverrideFrame sym res args)
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args'))
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args')
overrideRegMap ((RegMap sym then_args -> Identity (RegMap sym args))
 -> SimState p sym ext rtp (OverrideLang res) ('Just then_args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang res) ('Just args)))
-> RegMap sym args
-> SimState p sym ext rtp (OverrideLang res) ('Just then_args)
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ RegMap sym args
old_args)))
       let els' :: ReaderT
  (SimState p sym ext rtp (OverrideLang res) ('Just else_args))
  IO
  (ExecState p sym ext rtp)
els' = (SimState p sym ext rtp (OverrideLang res) ('Just else_args)
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just else_args))
     IO
     (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT (StateContT
  (SimState p sym ext rtp (OverrideLang res) ('Just else_args))
  (ExecState p sym ext rtp)
  IO
  a
-> (a
    -> SimState p sym ext rtp (OverrideLang res) ('Just else_args)
    -> IO (ExecState p sym ext rtp))
-> SimState p sym ext rtp (OverrideLang res) ('Just else_args)
-> IO (ExecState p sym ext rtp)
forall s r (m :: Type -> Type) a.
StateContT s r m a -> (a -> s -> m r) -> s -> m r
runStateContT
                            (OverrideSim p sym ext rtp else_args res a
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just else_args))
     (ExecState p sym ext rtp)
     IO
     a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
OverrideSim p sym ext rtp args ret a
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
unSim OverrideSim p sym ext rtp else_args res a
els)
                            (\a
x SimState p sym ext rtp (OverrideLang res) ('Just else_args)
st -> a
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
c a
x (SimState p sym ext rtp (OverrideLang res) ('Just else_args)
st SimState p sym ext rtp (OverrideLang res) ('Just else_args)
-> (SimState p sym ext rtp (OverrideLang res) ('Just else_args)
    -> SimState p sym ext rtp (OverrideLang res) ('Just args))
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
forall a b. a -> (a -> b) -> b
& (ActiveTree p sym ext rtp (OverrideLang res) ('Just else_args)
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> SimState p sym ext rtp (OverrideLang res) ('Just else_args)
-> Identity
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree((ActiveTree p sym ext rtp (OverrideLang res) ('Just else_args)
  -> Identity
       (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
 -> SimState p sym ext rtp (OverrideLang res) ('Just else_args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang res) ('Just args)))
-> ((RegMap sym else_args -> Identity (RegMap sym args))
    -> ActiveTree p sym ext rtp (OverrideLang res) ('Just else_args)
    -> Identity
         (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> (RegMap sym else_args -> Identity (RegMap sym args))
-> SimState p sym ext rtp (OverrideLang res) ('Just else_args)
-> Identity
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TopFrame sym ext (OverrideLang res) ('Just else_args)
 -> Identity (TopFrame sym ext (OverrideLang res) ('Just args)))
-> ActiveTree p sym ext rtp (OverrideLang res) ('Just else_args)
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang res) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame((TopFrame sym ext (OverrideLang res) ('Just else_args)
  -> Identity (TopFrame sym ext (OverrideLang res) ('Just args)))
 -> ActiveTree p sym ext rtp (OverrideLang res) ('Just else_args)
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> ((RegMap sym else_args -> Identity (RegMap sym args))
    -> TopFrame sym ext (OverrideLang res) ('Just else_args)
    -> Identity (TopFrame sym ext (OverrideLang res) ('Just args)))
-> (RegMap sym else_args -> Identity (RegMap sym args))
-> ActiveTree p sym ext rtp (OverrideLang res) ('Just else_args)
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang res) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(OverrideFrame sym res else_args
 -> Identity (OverrideFrame sym res args))
-> TopFrame sym ext (OverrideLang res) ('Just else_args)
-> Identity (TopFrame sym ext (OverrideLang res) ('Just args))
forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType)
       (r' :: CrucibleType) (args' :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> TopFrame sym ext (OverrideLang r) ('Just args)
-> f (TopFrame sym ext (OverrideLang r') ('Just args'))
overrideTopFrame((OverrideFrame sym res else_args
  -> Identity (OverrideFrame sym res args))
 -> TopFrame sym ext (OverrideLang res) ('Just else_args)
 -> Identity (TopFrame sym ext (OverrideLang res) ('Just args)))
-> ((RegMap sym else_args -> Identity (RegMap sym args))
    -> OverrideFrame sym res else_args
    -> Identity (OverrideFrame sym res args))
-> (RegMap sym else_args -> Identity (RegMap sym args))
-> TopFrame sym ext (OverrideLang res) ('Just else_args)
-> Identity (TopFrame sym ext (OverrideLang res) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(RegMap sym else_args -> Identity (RegMap sym args))
-> OverrideFrame sym res else_args
-> Identity (OverrideFrame sym res args)
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args'))
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args')
overrideRegMap ((RegMap sym else_args -> Identity (RegMap sym args))
 -> SimState p sym ext rtp (OverrideLang res) ('Just else_args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang res) ('Just args)))
-> RegMap sym args
-> SimState p sym ext rtp (OverrideLang res) ('Just else_args)
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ RegMap sym args
old_args)))
       Pred sym
-> RegMap sym then_args
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just then_args))
     IO
     (ExecState p sym ext rtp)
-> Maybe Position
-> RegMap sym else_args
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just else_args))
     IO
     (ExecState p sym ext rtp)
-> Maybe Position
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
forall sym (then_args :: Ctx CrucibleType) p ext rtp
       (r :: CrucibleType) (else_args :: Ctx CrucibleType)
       (args :: Ctx CrucibleType).
IsSymInterface sym =>
Pred sym
-> RegMap sym then_args
-> ExecCont p sym ext rtp (OverrideLang r) ('Just then_args)
-> Maybe Position
-> RegMap sym else_args
-> ExecCont p sym ext rtp (OverrideLang r) ('Just else_args)
-> Maybe Position
-> ExecCont p sym ext rtp (OverrideLang r) ('Just args)
overrideSymbolicBranch Pred sym
p RegMap sym then_args
thn_args ReaderT
  (SimState p sym ext rtp (OverrideLang res) ('Just then_args))
  IO
  (ExecState p sym ext rtp)
thn' Maybe Position
thn_pos RegMap sym else_args
els_args ReaderT
  (SimState p sym ext rtp (OverrideLang res) ('Just else_args))
  IO
  (ExecState p sym ext rtp)
els' Maybe Position
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 :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (new_args :: Ctx CrucibleType) (res :: CrucibleType) a.
IsSymInterface sym =>
RegMap sym new_args
-> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
     Maybe Position)]
-> OverrideSim p sym ext rtp args res a
symbolicBranches RegMap sym new_args
new_args [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
  Maybe Position)]
xs0 =
  StateContT
  (SimState p sym ext rtp (OverrideLang res) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args res a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
StateContT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  (ExecState p sym ext rtp)
  IO
  a
-> OverrideSim p sym ext rtp args ret a
Sim (StateContT
   (SimState p sym ext rtp (OverrideLang res) ('Just args))
   (ExecState p sym ext rtp)
   IO
   a
 -> OverrideSim p sym ext rtp args res a)
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
-> OverrideSim p sym ext rtp args res a
forall a b. (a -> b) -> a -> b
$ ((a
  -> SimState p sym ext rtp (OverrideLang res) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> SimState p sym ext rtp (OverrideLang res) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((a
   -> SimState p sym ext rtp (OverrideLang res) ('Just args)
   -> IO (ExecState p sym ext rtp))
  -> SimState p sym ext rtp (OverrideLang res) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> StateContT
      (SimState p sym ext rtp (OverrideLang res) ('Just args))
      (ExecState p sym ext rtp)
      IO
      a)
-> ((a
     -> SimState p sym ext rtp (OverrideLang res) ('Just args)
     -> IO (ExecState p sym ext rtp))
    -> SimState p sym ext rtp (OverrideLang res) ('Just args)
    -> IO (ExecState p sym ext rtp))
-> StateContT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
forall a b. (a -> b) -> a -> b
$ \a
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
c -> ReaderT
  (SimState p sym ext rtp (OverrideLang res) ('Just args))
  IO
  (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (ReaderT
   (SimState p sym ext rtp (OverrideLang res) ('Just args))
   IO
   (ExecState p sym ext rtp)
 -> SimState p sym ext rtp (OverrideLang res) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$
    do sym
sym <- Getting
  sym (SimState p sym ext rtp (OverrideLang res) ('Just args)) sym
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args)) IO sym
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting
  sym (SimState p sym ext rtp (OverrideLang res) ('Just args)) sym
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(sym -> f2 sym)
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateSymInterface
       ProgramLoc
top_loc <- IO ProgramLoc
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     ProgramLoc
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ProgramLoc
 -> ReaderT
      (SimState p sym ext rtp (OverrideLang res) ('Just args))
      IO
      ProgramLoc)
-> IO ProgramLoc
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     ProgramLoc
forall a b. (a -> b) -> a -> b
$ sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
       RegMap sym args
old_args <- Getting
  (RegMap sym args)
  (SimState p sym ext rtp (OverrideLang res) ('Just args))
  (RegMap sym args)
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (RegMap sym args)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view ((ActiveTree p sym ext rtp (OverrideLang res) ('Just args)
 -> Const
      (RegMap sym args)
      (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> Const
     (RegMap sym args)
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree((ActiveTree p sym ext rtp (OverrideLang res) ('Just args)
  -> Const
       (RegMap sym args)
       (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
 -> SimState p sym ext rtp (OverrideLang res) ('Just args)
 -> Const
      (RegMap sym args)
      (SimState p sym ext rtp (OverrideLang res) ('Just args)))
-> ((RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
    -> ActiveTree p sym ext rtp (OverrideLang res) ('Just args)
    -> Const
         (RegMap sym args)
         (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> Getting
     (RegMap sym args)
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     (RegMap sym args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TopFrame sym ext (OverrideLang res) ('Just args)
 -> Const
      (RegMap sym args)
      (TopFrame sym ext (OverrideLang res) ('Just args)))
-> ActiveTree p sym ext rtp (OverrideLang res) ('Just args)
-> Const
     (RegMap sym args)
     (ActiveTree p sym ext rtp (OverrideLang res) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame((TopFrame sym ext (OverrideLang res) ('Just args)
  -> Const
       (RegMap sym args)
       (TopFrame sym ext (OverrideLang res) ('Just args)))
 -> ActiveTree p sym ext rtp (OverrideLang res) ('Just args)
 -> Const
      (RegMap sym args)
      (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> ((RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
    -> TopFrame sym ext (OverrideLang res) ('Just args)
    -> Const
         (RegMap sym args)
         (TopFrame sym ext (OverrideLang res) ('Just args)))
-> (RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
-> ActiveTree p sym ext rtp (OverrideLang res) ('Just args)
-> Const
     (RegMap sym args)
     (ActiveTree p sym ext rtp (OverrideLang res) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(OverrideFrame sym res args
 -> Const (RegMap sym args) (OverrideFrame sym res args))
-> TopFrame sym ext (OverrideLang res) ('Just args)
-> Const
     (RegMap sym args)
     (TopFrame sym ext (OverrideLang res) ('Just args))
forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType)
       (r' :: CrucibleType) (args' :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> TopFrame sym ext (OverrideLang r) ('Just args)
-> f (TopFrame sym ext (OverrideLang r') ('Just args'))
overrideTopFrame((OverrideFrame sym res args
  -> Const (RegMap sym args) (OverrideFrame sym res args))
 -> TopFrame sym ext (OverrideLang res) ('Just args)
 -> Const
      (RegMap sym args)
      (TopFrame sym ext (OverrideLang res) ('Just args)))
-> ((RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
    -> OverrideFrame sym res args
    -> Const (RegMap sym args) (OverrideFrame sym res args))
-> (RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
-> TopFrame sym ext (OverrideLang res) ('Just args)
-> Const
     (RegMap sym args)
     (TopFrame sym ext (OverrideLang res) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
-> OverrideFrame sym res args
-> Const (RegMap sym args) (OverrideFrame sym res args)
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args'))
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args')
overrideRegMap)
       let all_args :: RegMap sym (args <+> new_args)
all_args = RegMap sym args
-> RegMap sym new_args -> RegMap sym (args <+> new_args)
forall sym (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
RegMap sym ctx -> RegMap sym ctx' -> RegMap sym (ctx <+> ctx')
appendRegs RegMap sym args
old_args RegMap sym new_args
new_args
       let c' :: a
-> SimState
     p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
-> IO (ExecState p sym ext rtp)
c' a
x SimState
  p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
st = a
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
c a
x (SimState
  p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
st SimState
  p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
-> (SimState
      p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
    -> SimState p sym ext rtp (OverrideLang res) ('Just args))
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
forall a b. a -> (a -> b) -> b
& (ActiveTree
   p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> SimState
     p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
-> Identity
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree((ActiveTree
    p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
  -> Identity
       (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
 -> SimState
      p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
 -> Identity
      (SimState p sym ext rtp (OverrideLang res) ('Just args)))
-> ((RegMap sym (args <+> new_args) -> Identity (RegMap sym args))
    -> ActiveTree
         p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
    -> Identity
         (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> (RegMap sym (args <+> new_args) -> Identity (RegMap sym args))
-> SimState
     p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
-> Identity
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TopFrame sym ext (OverrideLang res) ('Just (args <+> new_args))
 -> Identity (TopFrame sym ext (OverrideLang res) ('Just args)))
-> ActiveTree
     p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang res) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame((TopFrame sym ext (OverrideLang res) ('Just (args <+> new_args))
  -> Identity (TopFrame sym ext (OverrideLang res) ('Just args)))
 -> ActiveTree
      p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang res) ('Just args)))
-> ((RegMap sym (args <+> new_args) -> Identity (RegMap sym args))
    -> TopFrame sym ext (OverrideLang res) ('Just (args <+> new_args))
    -> Identity (TopFrame sym ext (OverrideLang res) ('Just args)))
-> (RegMap sym (args <+> new_args) -> Identity (RegMap sym args))
-> ActiveTree
     p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
-> Identity
     (ActiveTree p sym ext rtp (OverrideLang res) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(OverrideFrame sym res (args <+> new_args)
 -> Identity (OverrideFrame sym res args))
-> TopFrame sym ext (OverrideLang res) ('Just (args <+> new_args))
-> Identity (TopFrame sym ext (OverrideLang res) ('Just args))
forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType)
       (r' :: CrucibleType) (args' :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> TopFrame sym ext (OverrideLang r) ('Just args)
-> f (TopFrame sym ext (OverrideLang r') ('Just args'))
overrideTopFrame((OverrideFrame sym res (args <+> new_args)
  -> Identity (OverrideFrame sym res args))
 -> TopFrame sym ext (OverrideLang res) ('Just (args <+> new_args))
 -> Identity (TopFrame sym ext (OverrideLang res) ('Just args)))
-> ((RegMap sym (args <+> new_args) -> Identity (RegMap sym args))
    -> OverrideFrame sym res (args <+> new_args)
    -> Identity (OverrideFrame sym res args))
-> (RegMap sym (args <+> new_args) -> Identity (RegMap sym args))
-> TopFrame sym ext (OverrideLang res) ('Just (args <+> new_args))
-> Identity (TopFrame sym ext (OverrideLang res) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(RegMap sym (args <+> new_args) -> Identity (RegMap sym args))
-> OverrideFrame sym res (args <+> new_args)
-> Identity (OverrideFrame sym res args)
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args'))
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args')
overrideRegMap ((RegMap sym (args <+> new_args) -> Identity (RegMap sym args))
 -> SimState
      p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
 -> Identity
      (SimState p sym ext rtp (OverrideLang res) ('Just args)))
-> RegMap sym args
-> SimState
     p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ RegMap sym args
old_args)
       let go :: Integer
-> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
     Maybe Position)]
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
go Integer
_ [] = (SimState p sym ext rtp (OverrideLang res) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT ((SimState p sym ext rtp (OverrideLang res) ('Just args)
  -> IO (ExecState p sym ext rtp))
 -> ReaderT
      (SimState p sym ext rtp (OverrideLang res) ('Just args))
      IO
      (ExecState p sym ext rtp))
-> (SimState p sym ext rtp (OverrideLang res) ('Just args)
    -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ AbortExecReason
-> SimState p sym ext rtp (OverrideLang res) ('Just args)
-> IO (ExecState p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
AbortExecReason
-> SimState p sym ext rtp f args -> IO (ExecState p sym ext rtp)
runAbortHandler (ProgramLoc -> AbortExecReason
VariantOptionsExhausted ProgramLoc
top_loc)
           go !Integer
i ((Pred sym
p,OverrideSim p sym ext rtp (args <+> new_args) res a
m,Maybe Position
mpos):[(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
  Maybe Position)]
xs) =
             let msg :: Text
msg = String -> Text
T.pack (String
"after branch " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i)
                 m' :: ReaderT
  (SimState
     p sym ext rtp (OverrideLang res) ('Just (args <+> new_args)))
  IO
  (ExecState p sym ext rtp)
m'  = (SimState
   p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
 -> IO (ExecState p sym ext rtp))
-> ReaderT
     (SimState
        p sym ext rtp (OverrideLang res) ('Just (args <+> new_args)))
     IO
     (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT (StateContT
  (SimState
     p sym ext rtp (OverrideLang res) ('Just (args <+> new_args)))
  (ExecState p sym ext rtp)
  IO
  a
-> (a
    -> SimState
         p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
    -> IO (ExecState p sym ext rtp))
-> SimState
     p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
-> IO (ExecState p sym ext rtp)
forall s r (m :: Type -> Type) a.
StateContT s r m a -> (a -> s -> m r) -> s -> m r
runStateContT (OverrideSim p sym ext rtp (args <+> new_args) res a
-> StateContT
     (SimState
        p sym ext rtp (OverrideLang res) ('Just (args <+> new_args)))
     (ExecState p sym ext rtp)
     IO
     a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
OverrideSim p sym ext rtp args ret a
-> StateContT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     (ExecState p sym ext rtp)
     IO
     a
unSim OverrideSim p sym ext rtp (args <+> new_args) res a
m) a
-> SimState
     p sym ext rtp (OverrideLang res) ('Just (args <+> new_args))
-> IO (ExecState p sym ext rtp)
c')
              in Pred sym
-> RegMap sym (args <+> new_args)
-> ReaderT
     (SimState
        p sym ext rtp (OverrideLang res) ('Just (args <+> new_args)))
     IO
     (ExecState p sym ext rtp)
-> Maybe Position
-> RegMap sym args
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
-> Maybe Position
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
forall sym (then_args :: Ctx CrucibleType) p ext rtp
       (r :: CrucibleType) (else_args :: Ctx CrucibleType)
       (args :: Ctx CrucibleType).
IsSymInterface sym =>
Pred sym
-> RegMap sym then_args
-> ExecCont p sym ext rtp (OverrideLang r) ('Just then_args)
-> Maybe Position
-> RegMap sym else_args
-> ExecCont p sym ext rtp (OverrideLang r) ('Just else_args)
-> Maybe Position
-> ExecCont p sym ext rtp (OverrideLang r) ('Just args)
overrideSymbolicBranch Pred sym
p RegMap sym (args <+> new_args)
all_args ReaderT
  (SimState
     p sym ext rtp (OverrideLang res) ('Just (args <+> new_args)))
  IO
  (ExecState p sym ext rtp)
m' Maybe Position
mpos RegMap sym args
old_args (Integer
-> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
     Maybe Position)]
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
  Maybe Position)]
xs) (Position -> Maybe Position
forall a. a -> Maybe a
Just (Text -> Position
OtherPos Text
msg))
       Integer
-> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
     Maybe Position)]
-> ReaderT
     (SimState p sym ext rtp (OverrideLang res) ('Just args))
     IO
     (ExecState p sym ext rtp)
go (Integer
0::Integer) [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
  Maybe Position)]
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 :: forall p sym ext rtp (args :: Ctx CrucibleType)
       (new_args :: Ctx CrucibleType) (res :: CrucibleType) a.
IsSymInterface sym =>
RegMap sym new_args
-> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
     Maybe Position)]
-> OverrideSim p sym ext rtp args res a
nondetBranches RegMap sym new_args
new_args [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
  Maybe Position)]
xs0 =
  do sym
sym <- OverrideSim p sym ext rtp args res sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
     SymNat sym
z <- IO (SymNat sym) -> OverrideSim p sym ext rtp args res (SymNat sym)
forall a. IO a -> OverrideSim p sym ext rtp args res a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymNat sym)
 -> OverrideSim p sym ext rtp args res (SymNat sym))
-> IO (SymNat sym)
-> OverrideSim p sym ext rtp args res (SymNat sym)
forall a b. (a -> b) -> a -> b
$ sym -> SolverSymbol -> IO (SymNat sym)
forall sym.
IsSymExprBuilder sym =>
sym -> SolverSymbol -> IO (SymNat sym)
freshNat sym
sym (String -> SolverSymbol
safeSymbol String
"nondetBranchesZ")
     [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
  Maybe Position)]
xs <- [(Natural,
  (Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
   Maybe Position))]
-> ((Natural,
     (Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
      Maybe Position))
    -> OverrideSim
         p
         sym
         ext
         rtp
         args
         res
         (Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
          Maybe Position))
-> OverrideSim
     p
     sym
     ext
     rtp
     args
     res
     [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
       Maybe Position)]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for ([Natural]
-> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
     Maybe Position)]
-> [(Natural,
     (Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
      Maybe Position))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Natural
0 :: Natural)..] [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
  Maybe Position)]
xs0) (((Natural,
   (Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
    Maybe Position))
  -> OverrideSim
       p
       sym
       ext
       rtp
       args
       res
       (Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
        Maybe Position))
 -> OverrideSim
      p
      sym
      ext
      rtp
      args
      res
      [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
        Maybe Position)])
-> ((Natural,
     (Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
      Maybe Position))
    -> OverrideSim
         p
         sym
         ext
         rtp
         args
         res
         (Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
          Maybe Position))
-> OverrideSim
     p
     sym
     ext
     rtp
     args
     res
     [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
       Maybe Position)]
forall a b. (a -> b) -> a -> b
$ \(Natural
i, (Pred sym
p, OverrideSim p sym ext rtp (args <+> new_args) res a
v, Maybe Position
position)) ->
       do Pred sym
p' <- IO (Pred sym) -> OverrideSim p sym ext rtp args res (Pred sym)
forall a. IO a -> OverrideSim p sym ext rtp args res a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (Pred sym) -> OverrideSim p sym ext rtp args res (Pred sym))
-> IO (Pred sym) -> OverrideSim p sym ext rtp args res (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
z (SymNat sym -> IO (Pred sym)) -> IO (SymNat sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
i
          (Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
 Maybe Position)
-> OverrideSim
     p
     sym
     ext
     rtp
     args
     res
     (Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
      Maybe Position)
forall a. a -> OverrideSim p sym ext rtp args res a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
p', OverrideSim p sym ext rtp (args <+> new_args) res a
v, Maybe Position
position)
     RegMap sym new_args
-> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
     Maybe Position)]
-> OverrideSim p sym ext rtp args res a
forall p sym ext rtp (args :: Ctx CrucibleType)
       (new_args :: Ctx CrucibleType) (res :: CrucibleType) a.
IsSymInterface sym =>
RegMap sym new_args
-> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
     Maybe Position)]
-> OverrideSim p sym ext rtp args res a
symbolicBranches RegMap sym new_args
new_args [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
  Maybe Position)]
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 :: forall p sym ext.
FunctionBindings p sym ext
-> FnBinding p sym ext -> FunctionBindings p sym ext
insertFnBinding FunctionBindings p sym ext
m (FnBinding FnHandle args ret
h FnState p sym ext args ret
s) = FnHandleMap (FnState p sym ext) -> FunctionBindings p sym ext
forall p sym ext.
FnHandleMap (FnState p sym ext) -> FunctionBindings p sym ext
FnBindings (FnHandleMap (FnState p sym ext) -> FunctionBindings p sym ext)
-> FnHandleMap (FnState p sym ext) -> FunctionBindings p sym ext
forall a b. (a -> b) -> a -> b
$ FnHandle args ret
-> FnState p sym ext args ret
-> FnHandleMap (FnState p sym ext)
-> FnHandleMap (FnState p sym ext)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (f :: Ctx CrucibleType -> CrucibleType -> Type).
FnHandle args ret -> f args ret -> FnHandleMap f -> FnHandleMap f
insertHandleMap FnHandle args ret
h FnState p sym ext args ret
s (FnHandleMap (FnState p sym ext)
 -> FnHandleMap (FnState p sym ext))
-> FnHandleMap (FnState p sym ext)
-> FnHandleMap (FnState p sym ext)
forall a b. (a -> b) -> a -> b
$ FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
forall p sym ext.
FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
fnBindings FunctionBindings p sym ext
m

-- | Build a map of function bindings from a list of
--   handle/binding pairs.
fnBindingsFromList :: [FnBinding p sym ext] -> FunctionBindings p sym ext
fnBindingsFromList :: forall p sym ext.
[FnBinding p sym ext] -> FunctionBindings p sym ext
fnBindingsFromList = (FunctionBindings p sym ext
 -> FnBinding p sym ext -> FunctionBindings p sym ext)
-> FunctionBindings p sym ext
-> [FnBinding p sym ext]
-> FunctionBindings p sym ext
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' FunctionBindings p sym ext
-> FnBinding p sym ext -> FunctionBindings p sym ext
forall p sym ext.
FunctionBindings p sym ext
-> FnBinding p sym ext -> FunctionBindings p sym ext
insertFnBinding (FunctionBindings p sym ext
 -> [FnBinding p sym ext] -> FunctionBindings p sym ext)
-> FunctionBindings p sym ext
-> [FnBinding p sym ext]
-> FunctionBindings p sym ext
forall a b. (a -> b) -> a -> b
$ FnHandleMap (FnState p sym ext) -> FunctionBindings p sym ext
forall p sym ext.
FnHandleMap (FnState p sym ext) -> FunctionBindings p sym ext
FnBindings FnHandleMap (FnState p sym ext)
forall (f :: Ctx CrucibleType -> CrucibleType -> Type).
FnHandleMap f
emptyHandleMap

registerFnBinding :: FnBinding p sym ext
                   -> OverrideSim p sym ext rtp a r ()
registerFnBinding :: forall p sym ext rtp (a :: Ctx CrucibleType) (r :: CrucibleType).
FnBinding p sym ext -> OverrideSim p sym ext rtp a r ()
registerFnBinding (FnBinding FnHandle args ret
h FnState p sym ext args ret
s) = FnHandle args ret
-> FnState p sym ext args ret -> OverrideSim p sym ext rtp a r ()
forall (args :: Ctx CrucibleType) (ret :: CrucibleType) p sym ext
       rtp (a :: Ctx CrucibleType) (r :: CrucibleType).
FnHandle args ret
-> FnState p sym ext args ret -> OverrideSim p sym ext rtp a r ()
bindFnHandle FnHandle args ret
h FnState p sym ext args ret
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 :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType) p sym ext.
FnHandle args ret
-> (FnHandle args ret -> Override p sym ext args ret)
-> FnBinding p sym ext
useIntrinsic FnHandle args ret
hdl FnHandle args ret -> Override p sym ext args ret
impl = FnHandle args ret
-> FnState p sym ext args ret -> FnBinding p sym ext
forall (args :: Ctx CrucibleType) (ret :: CrucibleType) p sym ext.
FnHandle args ret
-> FnState p sym ext args ret -> FnBinding p sym ext
FnBinding FnHandle args ret
hdl (Override p sym ext args ret -> FnState p sym ext args ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Override p sym ext args ret -> FnState p sym ext args ret
UseOverride (FnHandle args ret -> Override p sym ext args ret
impl FnHandle args ret
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 :: forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
CurryAssignmentClass args =>
(forall r.
 Proxy r
 -> sym
 -> CurryAssignment
      args
      (RegEntry sym)
      (OverrideSim p sym ext r args ret (RegValue sym ret)))
-> FnHandle args ret -> Override p sym ext args ret
mkIntrinsic forall r.
Proxy r
-> sym
-> CurryAssignment
     args
     (RegEntry sym)
     (OverrideSim p sym ext r args ret (RegValue sym ret))
m FnHandle args ret
hdl = FunctionName
-> TypeRepr ret
-> (forall r. OverrideSim p sym ext r args ret (RegValue sym ret))
-> Override p sym ext args ret
forall (ret :: CrucibleType) p sym ext (args :: Ctx CrucibleType).
FunctionName
-> TypeRepr ret
-> (forall r. OverrideSim p sym ext r args ret (RegValue sym ret))
-> Override p sym ext args ret
mkOverride' (FnHandle args ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
handleName FnHandle args ret
hdl) (FnHandle args ret -> TypeRepr ret
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr ret
handleReturnType FnHandle args ret
hdl) OverrideSim p sym ext r args ret (RegValue sym ret)
forall r. OverrideSim p sym ext r args ret (RegValue sym ret)
ovr
 where
   ovr :: forall r. OverrideSim p sym ext r args ret (RegValue sym ret)
   ovr :: forall r. OverrideSim p sym ext r args ret (RegValue sym ret)
ovr = do
       sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
       (RegMap Assignment (RegEntry sym) args
args) <- OverrideSim p sym ext r args ret (RegMap sym args)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (RegMap sym args)
getOverrideArgs
       CurryAssignment
  args
  (RegEntry sym)
  (OverrideSim p sym ext r args ret (RegValue sym ret))
-> Assignment (RegEntry sym) args
-> OverrideSim p sym ext r args ret (RegValue sym ret)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment args f x -> Assignment f args -> x
Ctx.uncurryAssignment (Proxy r
-> sym
-> CurryAssignment
     args
     (RegEntry sym)
     (OverrideSim p sym ext r args ret (RegValue sym ret))
forall r.
Proxy r
-> sym
-> CurryAssignment
     args
     (RegEntry sym)
     (OverrideSim p sym ext r args ret (RegValue sym ret))
m (Proxy r
forall {k} (t :: k). Proxy t
Proxy :: Proxy r) sym
sym) Assignment (RegEntry sym) args
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
    { forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
TypedOverride p sym ext args ret
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   Assignment (RegValue' sym) args
   -> OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
typedOverrideHandler ::
        forall rtp args' ret'.
        Ctx.Assignment (RegValue' sym) args ->
        OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
    , forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
TypedOverride p sym ext args ret -> CtxRepr args
typedOverrideArgs :: CtxRepr args
    , forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
TypedOverride p sym ext args ret -> TypeRepr ret
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 :: forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
FunctionName
-> TypedOverride p sym ext args ret -> Override p sym ext args ret
runTypedOverride FunctionName
nm TypedOverride p sym ext args ret
typedOvr = FunctionName
-> TypeRepr ret
-> (forall {r}.
    OverrideSim p sym ext r args ret (RegValue sym ret))
-> Override p sym ext args ret
forall (ret :: CrucibleType) p sym ext (args :: Ctx CrucibleType).
FunctionName
-> TypeRepr ret
-> (forall r. OverrideSim p sym ext r args ret (RegValue sym ret))
-> Override p sym ext args ret
mkOverride' FunctionName
nm (TypedOverride p sym ext args ret -> TypeRepr ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
TypedOverride p sym ext args ret -> TypeRepr ret
typedOverrideRet TypedOverride p sym ext args ret
typedOvr) ((forall {r}. OverrideSim p sym ext r args ret (RegValue sym ret))
 -> Override p sym ext args ret)
-> (forall {r}.
    OverrideSim p sym ext r args ret (RegValue sym ret))
-> Override p sym ext args ret
forall a b. (a -> b) -> a -> b
$ do
  RegMap Assignment (RegEntry sym) args
args <- OverrideSim p sym ext r args ret (RegMap sym args)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (RegMap sym args)
getOverrideArgs
  TypedOverride p sym ext args ret
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   Assignment (RegValue' sym) args
   -> OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
TypedOverride p sym ext args ret
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   Assignment (RegValue' sym) args
   -> OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
typedOverrideHandler TypedOverride p sym ext args ret
typedOvr ((forall (x :: CrucibleType). RegEntry sym x -> RegValue' sym x)
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> Assignment (RegValue' sym) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC (RegValue sym x -> RegValue' sym x
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (RegValue sym x -> RegValue' sym x)
-> (RegEntry sym x -> RegValue sym x)
-> RegEntry sym x
-> RegValue' sym x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RegEntry sym x -> RegValue sym x
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue) Assignment (RegEntry sym) args
args)