{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}

module Lang.Crucible.Simulator.RecordAndReplay (
  HasRecordState(..),
  RecordState,
  mkRecordState,
  HasReplayState(..),
  ReplayState,
  mkReplayState,
  recordTraceLength,
  replayTraceLength,
  RecordedTrace,
  getRecordedTrace,
  recordFeature,
  replayFeature,
  initialTrace,
  traceGlobal,
  emptyRecordedTrace
) where

import Control.Exception qualified as X
import Control.Lens ((%~), (&), (^.))
import Control.Lens qualified as Lens
import Data.Foldable qualified as F
import Data.Kind (Type)
import Data.Text qualified as Text
import Data.Sequence qualified as Seq
import Lang.Crucible.Backend qualified as CB
import Lang.Crucible.CFG.Core qualified as C
import Lang.Crucible.FunctionHandle qualified as C
import Lang.Crucible.Panic (panic)
import Lang.Crucible.Simulator qualified as C
import Lang.Crucible.Simulator.EvalStmt qualified as C
import Lang.Crucible.Simulator.ExecutionTree qualified as C
import Lang.Crucible.Simulator.GlobalState qualified as C
import Lang.Crucible.Simulator.SymSequence qualified as CSSS
import Lang.Crucible.Types qualified as CT
import What4.Interface qualified as W4
import What4.Partial qualified as W4P

-- | A trace consists of the 'W4.ProgramLoc's returned by
-- 'W4.getCurrentProgramLoc' in 'C.RunningState's during symbolic execution.
--
-- Intentionally not part of the API so as to keep the implementation abstract.
type TraceType = CT.SequenceType (CT.StringType W4.Unicode)

-- | Type parameters:
--
-- * @p@: see 'C.cruciblePersonality'
-- * @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- * @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- * @rtp@: type of the simulator return value
type RecordState :: Type -> Type -> Type -> Type -> Type
newtype RecordState p sym ext rtp
  = RecordState (C.GlobalVar TraceType)
    -- ^ constructor intentionally not exported

{- | A trace from 'recordFeature', processed and ready for consumption by
'replayFeature'.
-}
newtype RecordedTrace sym
  = RecordedTrace (C.RegValue sym TraceType)

-- | Type parameters:
--
-- * @p@: see 'C.cruciblePersonality'
-- * @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- * @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- * @rtp@: type of the simulator return value
type ReplayState :: Type -> Type -> Type -> Type -> Type
data ReplayState p sym ext rtp
  = ReplayState
    { forall p sym ext rtp.
ReplayState p sym ext rtp -> GlobalVar TraceType
_traceGlobal :: (C.GlobalVar TraceType)
    , forall p sym ext rtp.
ReplayState p sym ext rtp -> RecordedTrace sym
_initialTrace :: (RecordedTrace sym)
    }
    -- ^ constructor intentionally not exported
Lens.makeLenses ''ReplayState

-- | Constructor for 'RecordState'
mkRecordState ::
  C.HandleAllocator -> IO (RecordState p sym ext rtp)
mkRecordState :: forall p sym ext rtp.
HandleAllocator -> IO (RecordState p sym ext rtp)
mkRecordState HandleAllocator
halloc =
  GlobalVar TraceType -> RecordState p sym ext rtp
forall p sym ext rtp.
GlobalVar TraceType -> RecordState p sym ext rtp
RecordState (GlobalVar TraceType -> RecordState p sym ext rtp)
-> IO (GlobalVar TraceType) -> IO (RecordState p sym ext rtp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> HandleAllocator
-> Text -> TypeRepr TraceType -> IO (GlobalVar TraceType)
forall (tp :: CrucibleType).
HandleAllocator -> Text -> TypeRepr tp -> IO (GlobalVar tp)
C.freshGlobalVar HandleAllocator
halloc Text
"recordState" TypeRepr TraceType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
W4.knownRepr

-- | Constructor for 'ReplayState'
mkReplayState ::
  C.HandleAllocator -> RecordedTrace sym  -> IO (ReplayState p sym ext rtp)
mkReplayState :: forall sym p ext rtp.
HandleAllocator
-> RecordedTrace sym -> IO (ReplayState p sym ext rtp)
mkReplayState HandleAllocator
halloc RecordedTrace sym
rt =
  GlobalVar TraceType
-> RecordedTrace sym -> ReplayState p sym ext rtp
forall p sym ext rtp.
GlobalVar TraceType
-> RecordedTrace sym -> ReplayState p sym ext rtp
ReplayState (GlobalVar TraceType
 -> RecordedTrace sym -> ReplayState p sym ext rtp)
-> IO (GlobalVar TraceType)
-> IO (RecordedTrace sym -> ReplayState p sym ext rtp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> HandleAllocator
-> Text -> TypeRepr TraceType -> IO (GlobalVar TraceType)
forall (tp :: CrucibleType).
HandleAllocator -> Text -> TypeRepr tp -> IO (GlobalVar tp)
C.freshGlobalVar HandleAllocator
halloc Text
"replayState" TypeRepr TraceType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
W4.knownRepr IO (RecordedTrace sym -> ReplayState p sym ext rtp)
-> IO (RecordedTrace sym) -> IO (ReplayState p sym ext rtp)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> RecordedTrace sym -> IO (RecordedTrace sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RecordedTrace sym
rt

-- | A class for Crucible personality types @p@ which contain a
-- 'RecordState'. This execution feature is polymorphic over
-- 'RecordState' so that downstream users can supply their own
-- personality types that extend 'RecordState' further.
class HasRecordState p r sym ext rtp | p -> r sym ext rtp where
  recordState :: Lens.Lens' p (RecordState r sym ext rtp)

instance HasRecordState (RecordState p sym ext rtp) p sym ext rtp where
  recordState :: Lens' (RecordState p sym ext rtp) (RecordState p sym ext rtp)
recordState = (RecordState p sym ext rtp -> f (RecordState p sym ext rtp))
-> RecordState p sym ext rtp -> f (RecordState p sym ext rtp)
forall a. a -> a
id
  {-# INLINE recordState #-}

-- | A class for Crucible personality types @p@ which contain a
-- 'ReplayState'. This execution feature is polymorphic over
-- 'ReplayState' so that downstream users can supply their own
-- personality types that extend 'ReplayState' further.
class HasReplayState p r sym ext rtp | p -> r sym ext rtp where
  replayState :: Lens.Lens' p (ReplayState r sym ext rtp)

instance HasReplayState (ReplayState p sym ext rtp) p sym ext rtp where
  replayState :: Lens' (ReplayState p sym ext rtp) (ReplayState p sym ext rtp)
replayState = (ReplayState p sym ext rtp -> f (ReplayState p sym ext rtp))
-> ReplayState p sym ext rtp -> f (ReplayState p sym ext rtp)
forall a. a -> a
id
  {-# INLINE replayState #-}

data TraceGlobalNotDefined = TraceGlobalNotDefined

instance Show TraceGlobalNotDefined where
  show :: TraceGlobalNotDefined -> String
show TraceGlobalNotDefined
_ = String
"record and replay trace global not defined"

instance X.Exception TraceGlobalNotDefined

locAsStr ::
  W4.IsExprBuilder sym =>
  sym ->
  IO (C.RegValue sym (CT.StringType W4.Unicode))
locAsStr :: forall sym.
IsExprBuilder sym =>
sym -> IO (RegValue sym ('BaseToType (BaseStringType Unicode)))
locAsStr sym
sym = do
  ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
W4.getCurrentProgramLoc sym
sym
  let txtLoc :: Text
txtLoc = String -> Text
Text.pack (ProgramLoc -> String
forall a. Show a => a -> String
show ProgramLoc
loc)
  sym
-> StringLiteral Unicode
-> IO (SymExpr sym (BaseStringType Unicode))
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
forall (si :: StringInfo).
sym -> StringLiteral si -> IO (SymString sym si)
W4.stringLit sym
sym (Text -> StringLiteral Unicode
W4.UnicodeLiteral Text
txtLoc)

emptyRecordedTrace :: sym -> IO (RecordedTrace sym)
emptyRecordedTrace :: forall sym. sym -> IO (RecordedTrace sym)
emptyRecordedTrace sym
sym = SymSequence sym (SymExpr sym (BaseStringType Unicode))
-> RecordedTrace sym
RegValue sym TraceType -> RecordedTrace sym
forall sym. RegValue sym TraceType -> RecordedTrace sym
RecordedTrace (SymSequence sym (SymExpr sym (BaseStringType Unicode))
 -> RecordedTrace sym)
-> IO (SymSequence sym (SymExpr sym (BaseStringType Unicode)))
-> IO (RecordedTrace sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> IO (SymSequence sym (SymExpr sym (BaseStringType Unicode)))
forall sym a. sym -> IO (SymSequence sym a)
CSSS.nilSymSequence sym
sym

getRecordTrace ::
  HasRecordState p p sym ext rtp =>
  C.SimState p sym ext rtp f args ->
  Maybe (C.RegValue sym TraceType)
getRecordTrace :: forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasRecordState p p sym ext rtp =>
SimState p sym ext rtp f args -> Maybe (RegValue sym TraceType)
getRecordTrace SimState p sym ext rtp f args
simState = do
  let ctx :: SimContext p sym ext
ctx = SimState p sym ext rtp f args
simState SimState p sym ext rtp f args
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext rtp f 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 f 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)
C.stateContext
  let RecordState GlobalVar TraceType
g = SimContext p sym ext
ctx SimContext p sym ext
-> Getting
     (RecordState p sym ext rtp)
     (SimContext p sym ext)
     (RecordState p sym ext rtp)
-> RecordState p sym ext rtp
forall s a. s -> Getting a s a -> a
^. (p -> Const (RecordState p sym ext rtp) p)
-> SimContext p sym ext
-> Const (RecordState p sym ext rtp) (SimContext p sym ext)
forall p sym ext (f :: Type -> Type).
Functor f =>
(p -> f p) -> SimContext p sym ext -> f (SimContext p sym ext)
C.cruciblePersonality ((p -> Const (RecordState p sym ext rtp) p)
 -> SimContext p sym ext
 -> Const (RecordState p sym ext rtp) (SimContext p sym ext))
-> ((RecordState p sym ext rtp
     -> Const (RecordState p sym ext rtp) (RecordState p sym ext rtp))
    -> p -> Const (RecordState p sym ext rtp) p)
-> Getting
     (RecordState p sym ext rtp)
     (SimContext p sym ext)
     (RecordState p sym ext rtp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RecordState p sym ext rtp
 -> Const (RecordState p sym ext rtp) (RecordState p sym ext rtp))
-> p -> Const (RecordState p sym ext rtp) p
forall p r sym ext rtp.
HasRecordState p r sym ext rtp =>
Lens' p (RecordState r sym ext rtp)
Lens' p (RecordState p sym ext rtp)
recordState
  GlobalVar TraceType
-> SymGlobalState sym -> Maybe (RegValue sym TraceType)
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
C.lookupGlobal GlobalVar TraceType
g (SimState p sym ext rtp f args
simState SimState p sym ext rtp f args
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp f args)
     (SymGlobalState sym)
-> SymGlobalState sym
forall s a. s -> Getting a s a -> a
^. Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp f args)
  (SymGlobalState sym)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
C.stateGlobals)

-- | Get the length of the currently recorded trace
recordTraceLength ::
  W4.IsExprBuilder sym =>
  HasRecordState p p sym ext rtp =>
  C.SimState p sym ext rtp f args ->
  IO (Maybe (W4.SymNat sym))
recordTraceLength :: forall sym p ext rtp f (args :: Maybe (Ctx CrucibleType)).
(IsExprBuilder sym, HasRecordState p p sym ext rtp) =>
SimState p sym ext rtp f args -> IO (Maybe (SymNat sym))
recordTraceLength SimState p sym ext rtp f args
simState = do
  let sym :: sym
sym = SimState p sym ext rtp f args
simState SimState p sym ext rtp f args
-> Getting sym (SimState p sym ext rtp f args) sym -> sym
forall s a. s -> Getting a s a -> a
^. Getting sym (SimState p sym ext rtp f 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)
C.stateSymInterface
  case SimState p sym ext rtp f args -> Maybe (RegValue sym TraceType)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasRecordState p p sym ext rtp =>
SimState p sym ext rtp f args -> Maybe (RegValue sym TraceType)
getRecordTrace SimState p sym ext rtp f args
simState of
    Maybe (RegValue sym TraceType)
Nothing -> Maybe (SymNat sym) -> IO (Maybe (SymNat sym))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (SymNat sym)
forall a. Maybe a
Nothing
    Just RegValue sym TraceType
s -> SymNat sym -> Maybe (SymNat sym)
forall a. a -> Maybe a
Just (SymNat sym -> Maybe (SymNat sym))
-> IO (SymNat sym) -> IO (Maybe (SymNat sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymSequence sym (SymExpr sym (BaseStringType Unicode))
-> IO (SymNat sym)
forall sym a.
IsExprBuilder sym =>
sym -> SymSequence sym a -> IO (SymNat sym)
CSSS.lengthSymSequence sym
sym SymSequence sym (SymExpr sym (BaseStringType Unicode))
RegValue sym TraceType
s

getReplayTrace ::
  HasReplayState p p sym ext rtp =>
  C.SimState p sym ext rtp f args ->
  Maybe (C.RegValue sym TraceType)
getReplayTrace :: forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasReplayState p p sym ext rtp =>
SimState p sym ext rtp f args -> Maybe (RegValue sym TraceType)
getReplayTrace SimState p sym ext rtp f args
simState = do
  let ctx :: SimContext p sym ext
ctx = SimState p sym ext rtp f args
simState SimState p sym ext rtp f args
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext rtp f 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 f 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)
C.stateContext
  let g :: GlobalVar TraceType
g = SimContext p sym ext
ctx SimContext p sym ext
-> Getting
     (GlobalVar TraceType) (SimContext p sym ext) (GlobalVar TraceType)
-> GlobalVar TraceType
forall s a. s -> Getting a s a -> a
^. (p -> Const (GlobalVar TraceType) p)
-> SimContext p sym ext
-> Const (GlobalVar TraceType) (SimContext p sym ext)
forall p sym ext (f :: Type -> Type).
Functor f =>
(p -> f p) -> SimContext p sym ext -> f (SimContext p sym ext)
C.cruciblePersonality ((p -> Const (GlobalVar TraceType) p)
 -> SimContext p sym ext
 -> Const (GlobalVar TraceType) (SimContext p sym ext))
-> ((GlobalVar TraceType
     -> Const (GlobalVar TraceType) (GlobalVar TraceType))
    -> p -> Const (GlobalVar TraceType) p)
-> Getting
     (GlobalVar TraceType) (SimContext p sym ext) (GlobalVar TraceType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReplayState p sym ext rtp
 -> Const (GlobalVar TraceType) (ReplayState p sym ext rtp))
-> p -> Const (GlobalVar TraceType) p
forall p r sym ext rtp.
HasReplayState p r sym ext rtp =>
Lens' p (ReplayState r sym ext rtp)
Lens' p (ReplayState p sym ext rtp)
replayState ((ReplayState p sym ext rtp
  -> Const (GlobalVar TraceType) (ReplayState p sym ext rtp))
 -> p -> Const (GlobalVar TraceType) p)
-> ((GlobalVar TraceType
     -> Const (GlobalVar TraceType) (GlobalVar TraceType))
    -> ReplayState p sym ext rtp
    -> Const (GlobalVar TraceType) (ReplayState p sym ext rtp))
-> (GlobalVar TraceType
    -> Const (GlobalVar TraceType) (GlobalVar TraceType))
-> p
-> Const (GlobalVar TraceType) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GlobalVar TraceType
 -> Const (GlobalVar TraceType) (GlobalVar TraceType))
-> ReplayState p sym ext rtp
-> Const (GlobalVar TraceType) (ReplayState p sym ext rtp)
forall p sym ext rtp p ext rtp (f :: Type -> Type).
Functor f =>
(GlobalVar TraceType -> f (GlobalVar TraceType))
-> ReplayState p sym ext rtp -> f (ReplayState p sym ext rtp)
traceGlobal
  GlobalVar TraceType
-> SymGlobalState sym -> Maybe (RegValue sym TraceType)
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
C.lookupGlobal GlobalVar TraceType
g (SimState p sym ext rtp f args
simState SimState p sym ext rtp f args
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp f args)
     (SymGlobalState sym)
-> SymGlobalState sym
forall s a. s -> Getting a s a -> a
^. Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp f args)
  (SymGlobalState sym)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
C.stateGlobals)

-- | Get the length of the trace being replayed
replayTraceLength ::
  W4.IsExprBuilder sym =>
  HasReplayState p p sym ext rtp =>
  C.SimState p sym ext rtp f args ->
  IO (Maybe (W4.SymNat sym))
replayTraceLength :: forall sym p ext rtp f (args :: Maybe (Ctx CrucibleType)).
(IsExprBuilder sym, HasReplayState p p sym ext rtp) =>
SimState p sym ext rtp f args -> IO (Maybe (SymNat sym))
replayTraceLength SimState p sym ext rtp f args
simState = do
  let sym :: sym
sym = SimState p sym ext rtp f args
simState SimState p sym ext rtp f args
-> Getting sym (SimState p sym ext rtp f args) sym -> sym
forall s a. s -> Getting a s a -> a
^. Getting sym (SimState p sym ext rtp f 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)
C.stateSymInterface
  case SimState p sym ext rtp f args -> Maybe (RegValue sym TraceType)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasReplayState p p sym ext rtp =>
SimState p sym ext rtp f args -> Maybe (RegValue sym TraceType)
getReplayTrace SimState p sym ext rtp f args
simState of
    Maybe (RegValue sym TraceType)
Nothing -> Maybe (SymNat sym) -> IO (Maybe (SymNat sym))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (SymNat sym)
forall a. Maybe a
Nothing
    Just RegValue sym TraceType
s -> SymNat sym -> Maybe (SymNat sym)
forall a. a -> Maybe a
Just (SymNat sym -> Maybe (SymNat sym))
-> IO (SymNat sym) -> IO (Maybe (SymNat sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymSequence sym (SymExpr sym (BaseStringType Unicode))
-> IO (SymNat sym)
forall sym a.
IsExprBuilder sym =>
sym -> SymSequence sym a -> IO (SymNat sym)
CSSS.lengthSymSequence sym
sym SymSequence sym (SymExpr sym (BaseStringType Unicode))
RegValue sym TraceType
s

-- | An 'C.ExecutionFeature' to record traces.
--
-- During execution this logs program locations to a Crucible global variable.
-- After execution, this variable may be read with 'getRecordedTrace' and the
-- 'RecordedTrace' can be passed to 'replayFeature' to \"replay\" it, i.e., to
-- abort all branches that deviate from it.
--
-- If this is not called with 'C.InitialState' before any other 'C.ExecState',
-- it may throw a 'TraceGlobalNotDefined' exception.
recordFeature ::
  ( HasRecordState p p sym ext rtp
  , W4.IsExprBuilder sym
  ) =>
  C.ExecutionFeature p sym ext rtp
recordFeature :: forall p sym ext rtp.
(HasRecordState p p sym ext rtp, IsExprBuilder sym) =>
ExecutionFeature p sym ext rtp
recordFeature =
  (ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
forall p sym ext rtp.
(ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
C.ExecutionFeature ((ExecState p sym ext rtp
  -> IO (ExecutionFeatureResult p sym ext rtp))
 -> ExecutionFeature p sym ext rtp)
-> (ExecState p sym ext rtp
    -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
forall a b. (a -> b) -> a -> b
$
    \case
      C.InitialState SimContext p sym ext
simCtx SymGlobalState sym
globals AbortHandler p sym ext (RegEntry sym ret)
abortHandler TypeRepr ret
retTy ExecCont
  p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
cont -> do
        SymGlobalState sym
globals' <- SimContext p sym ext
-> SymGlobalState sym -> IO (SymGlobalState sym)
forall p sym ext rtp.
HasRecordState p p sym ext rtp =>
SimContext p sym ext
-> SymGlobalState sym -> IO (SymGlobalState sym)
insertNewTrace SimContext p sym ext
simCtx SymGlobalState sym
globals
        let iState :: ExecState p sym ext rtp
iState = SimContext p sym ext
-> SymGlobalState sym
-> AbortHandler p sym ext (RegEntry sym ret)
-> TypeRepr ret
-> ExecCont
     p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
-> ExecState p sym ext rtp
forall p sym ext rtp (ret :: CrucibleType).
(rtp ~ RegEntry sym ret) =>
SimContext p sym ext
-> SymGlobalState sym
-> AbortHandler p sym ext (RegEntry sym ret)
-> TypeRepr ret
-> ExecCont
     p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
-> ExecState p sym ext rtp
C.InitialState SimContext p sym ext
simCtx SymGlobalState sym
globals' AbortHandler p sym ext (RegEntry sym ret)
abortHandler TypeRepr ret
retTy ExecCont
  p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
cont
        ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecutionFeatureResult p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureModifiedState ExecState p sym ext rtp
iState
      C.RunningState RunningStateInfo blocks args
runStateInfo SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st -> do
        SymExpr sym (BaseStringType Unicode)
loc <- sym -> IO (RegValue sym ('BaseToType (BaseStringType Unicode)))
forall sym.
IsExprBuilder sym =>
sym -> IO (RegValue sym ('BaseToType (BaseStringType Unicode)))
locAsStr (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     sym
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     sym
-> sym
forall s a. s -> Getting a s a -> a
^. Getting
  sym
  (SimState p sym ext rtp (CrucibleLang blocks r) ('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)
C.stateSymInterface)
        SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st' <- SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> RegValue sym ('BaseToType (BaseStringType Unicode))
-> IO (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasRecordState p p sym ext rtp =>
SimState p sym ext rtp f args
-> RegValue sym ('BaseToType (BaseStringType Unicode))
-> IO (SimState p sym ext rtp f args)
consTrace SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st SymExpr sym (BaseStringType Unicode)
RegValue sym ('BaseToType (BaseStringType Unicode))
loc
        let rState :: ExecState p sym ext rtp
rState = RunningStateInfo blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (args :: Ctx CrucibleType).
RunningStateInfo blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
C.RunningState RunningStateInfo blocks args
runStateInfo SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st'
        ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecutionFeatureResult p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureModifiedState ExecState p sym ext rtp
rState
      ExecState p sym ext rtp
_ -> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange
  where
    insertNewTrace ::
      HasRecordState p p sym ext rtp =>
      C.SimContext p sym ext ->
      C.SymGlobalState sym ->
      IO (C.SymGlobalState sym)
    insertNewTrace :: forall p sym ext rtp.
HasRecordState p p sym ext rtp =>
SimContext p sym ext
-> SymGlobalState sym -> IO (SymGlobalState sym)
insertNewTrace SimContext p sym ext
simCtx SymGlobalState sym
globals = do
      let RecordState GlobalVar TraceType
g = SimContext p sym ext
simCtx SimContext p sym ext
-> Getting
     (RecordState p sym ext rtp)
     (SimContext p sym ext)
     (RecordState p sym ext rtp)
-> RecordState p sym ext rtp
forall s a. s -> Getting a s a -> a
^. (p -> Const (RecordState p sym ext rtp) p)
-> SimContext p sym ext
-> Const (RecordState p sym ext rtp) (SimContext p sym ext)
forall p sym ext (f :: Type -> Type).
Functor f =>
(p -> f p) -> SimContext p sym ext -> f (SimContext p sym ext)
C.cruciblePersonality ((p -> Const (RecordState p sym ext rtp) p)
 -> SimContext p sym ext
 -> Const (RecordState p sym ext rtp) (SimContext p sym ext))
-> ((RecordState p sym ext rtp
     -> Const (RecordState p sym ext rtp) (RecordState p sym ext rtp))
    -> p -> Const (RecordState p sym ext rtp) p)
-> Getting
     (RecordState p sym ext rtp)
     (SimContext p sym ext)
     (RecordState p sym ext rtp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RecordState p sym ext rtp
 -> Const (RecordState p sym ext rtp) (RecordState p sym ext rtp))
-> p -> Const (RecordState p sym ext rtp) p
forall p r sym ext rtp.
HasRecordState p r sym ext rtp =>
Lens' p (RecordState r sym ext rtp)
Lens' p (RecordState p sym ext rtp)
recordState
      let sym :: sym
sym = SimContext p sym ext
simCtx SimContext 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)
C.ctxSymInterface
      SymSequence sym (SymExpr sym (BaseStringType Unicode))
nil <- sym -> IO (SymSequence sym (SymExpr sym (BaseStringType Unicode)))
forall sym a. sym -> IO (SymSequence sym a)
CSSS.nilSymSequence sym
sym
      SymGlobalState sym -> IO (SymGlobalState sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GlobalVar TraceType
-> RegValue sym TraceType
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
C.insertGlobal GlobalVar TraceType
g SymSequence sym (SymExpr sym (BaseStringType Unicode))
RegValue sym TraceType
nil SymGlobalState sym
globals)

    getTraceOrThrow ::
      HasRecordState p p sym ext rtp =>
      C.SimState p sym ext rtp f args ->
      IO (C.RegValue sym TraceType)
    getTraceOrThrow :: forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasRecordState p p sym ext rtp =>
SimState p sym ext rtp f args -> IO (RegValue sym TraceType)
getTraceOrThrow SimState p sym ext rtp f args
st =
      case SimState p sym ext rtp f args -> Maybe (RegValue sym TraceType)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasRecordState p p sym ext rtp =>
SimState p sym ext rtp f args -> Maybe (RegValue sym TraceType)
getRecordTrace SimState p sym ext rtp f args
st of
        Maybe (RegValue sym TraceType)
Nothing -> TraceGlobalNotDefined
-> IO (SymSequence sym (SymExpr sym (BaseStringType Unicode)))
forall a e. Exception e => e -> a
X.throw TraceGlobalNotDefined
TraceGlobalNotDefined
        Just RegValue sym TraceType
t -> SymSequence sym (SymExpr sym (BaseStringType Unicode))
-> IO (SymSequence sym (SymExpr sym (BaseStringType Unicode)))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymSequence sym (SymExpr sym (BaseStringType Unicode))
RegValue sym TraceType
t

    insertTrace ::
      HasRecordState p p sym ext rtp =>
      C.SimState p sym ext rtp f args ->
      C.RegValue sym TraceType ->
      C.SimState p sym ext rtp f args
    insertTrace :: forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasRecordState p p sym ext rtp =>
SimState p sym ext rtp f args
-> RegValue sym TraceType -> SimState p sym ext rtp f args
insertTrace SimState p sym ext rtp f args
st RegValue sym TraceType
v = do
      let simCtx :: SimContext p sym ext
simCtx = SimState p sym ext rtp f args
st SimState p sym ext rtp f args
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext rtp f 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 f 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)
C.stateContext
      let RecordState GlobalVar TraceType
g = SimContext p sym ext
simCtx SimContext p sym ext
-> Getting
     (RecordState p sym ext rtp)
     (SimContext p sym ext)
     (RecordState p sym ext rtp)
-> RecordState p sym ext rtp
forall s a. s -> Getting a s a -> a
^. (p -> Const (RecordState p sym ext rtp) p)
-> SimContext p sym ext
-> Const (RecordState p sym ext rtp) (SimContext p sym ext)
forall p sym ext (f :: Type -> Type).
Functor f =>
(p -> f p) -> SimContext p sym ext -> f (SimContext p sym ext)
C.cruciblePersonality ((p -> Const (RecordState p sym ext rtp) p)
 -> SimContext p sym ext
 -> Const (RecordState p sym ext rtp) (SimContext p sym ext))
-> ((RecordState p sym ext rtp
     -> Const (RecordState p sym ext rtp) (RecordState p sym ext rtp))
    -> p -> Const (RecordState p sym ext rtp) p)
-> Getting
     (RecordState p sym ext rtp)
     (SimContext p sym ext)
     (RecordState p sym ext rtp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RecordState p sym ext rtp
 -> Const (RecordState p sym ext rtp) (RecordState p sym ext rtp))
-> p -> Const (RecordState p sym ext rtp) p
forall p r sym ext rtp.
HasRecordState p r sym ext rtp =>
Lens' p (RecordState r sym ext rtp)
Lens' p (RecordState p sym ext rtp)
recordState
      SimState p sym ext rtp f args
st SimState p sym ext rtp f args
-> (SimState p sym ext rtp f args -> SimState p sym ext rtp f args)
-> SimState p sym ext rtp f args
forall a b. a -> (a -> b) -> b
& (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp f args
-> Identity (SimState p sym ext rtp f args)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
C.stateGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp f args
 -> Identity (SimState p sym ext rtp f args))
-> (SymGlobalState sym -> SymGlobalState sym)
-> SimState p sym ext rtp f args
-> SimState p sym ext rtp f args
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ GlobalVar TraceType
-> RegValue sym TraceType
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
C.insertGlobal GlobalVar TraceType
g RegValue sym TraceType
v

    consTrace ::
      HasRecordState p p sym ext rtp =>
      C.SimState p sym ext rtp f args ->
      C.RegValue sym (CT.StringType W4.Unicode) ->
      IO (C.SimState p sym ext rtp f args)
    consTrace :: forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasRecordState p p sym ext rtp =>
SimState p sym ext rtp f args
-> RegValue sym ('BaseToType (BaseStringType Unicode))
-> IO (SimState p sym ext rtp f args)
consTrace SimState p sym ext rtp f args
st RegValue sym ('BaseToType (BaseStringType Unicode))
v = do
      SymSequence sym (SymExpr sym (BaseStringType Unicode))
s <- SimState p sym ext rtp f args -> IO (RegValue sym TraceType)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasRecordState p p sym ext rtp =>
SimState p sym ext rtp f args -> IO (RegValue sym TraceType)
getTraceOrThrow SimState p sym ext rtp f args
st
      let sym :: sym
sym = SimState p sym ext rtp f args
st SimState p sym ext rtp f args
-> Getting sym (SimState p sym ext rtp f args) sym -> sym
forall s a. s -> Getting a s a -> a
^. Getting sym (SimState p sym ext rtp f 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)
C.stateSymInterface
      SymSequence sym (SymExpr sym (BaseStringType Unicode))
s' <- sym
-> SymExpr sym (BaseStringType Unicode)
-> SymSequence sym (SymExpr sym (BaseStringType Unicode))
-> IO (SymSequence sym (SymExpr sym (BaseStringType Unicode)))
forall sym a.
sym -> a -> SymSequence sym a -> IO (SymSequence sym a)
CSSS.consSymSequence sym
sym SymExpr sym (BaseStringType Unicode)
RegValue sym ('BaseToType (BaseStringType Unicode))
v SymSequence sym (SymExpr sym (BaseStringType Unicode))
s
      SimState p sym ext rtp f args -> IO (SimState p sym ext rtp f args)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SimState p sym ext rtp f args
-> RegValue sym TraceType -> SimState p sym ext rtp f args
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasRecordState p p sym ext rtp =>
SimState p sym ext rtp f args
-> RegValue sym TraceType -> SimState p sym ext rtp f args
insertTrace SimState p sym ext rtp f args
st SymSequence sym (SymExpr sym (BaseStringType Unicode))
RegValue sym TraceType
s')


    -- ^ constructor intentionally not exported to keep 'TraceType' out of the
    -- API, but it could be exported in the future if necessary.

-- | Obtain a 'RecordedTrace' after execution.
--
-- This currently requires concretizing the trace, because there is no efficient
-- reverse operation for 'CSSS.SymSequence'.
getRecordedTrace ::
  W4.IsExprBuilder sym =>
  C.SymGlobalState sym ->
  RecordState p sym ext rtp ->
  sym ->
  -- | Evaluation for booleans, usually a 'What4.Expr.GroundEval.GroundEvalFn'
  (W4.Pred sym -> IO Bool) ->
  IO (RecordedTrace sym)
getRecordedTrace :: forall sym p ext rtp.
IsExprBuilder sym =>
SymGlobalState sym
-> RecordState p sym ext rtp
-> sym
-> (Pred sym -> IO Bool)
-> IO (RecordedTrace sym)
getRecordedTrace SymGlobalState sym
globals (RecordState GlobalVar TraceType
g) sym
sym Pred sym -> IO Bool
evalBool = do
  case GlobalVar TraceType
-> SymGlobalState sym -> Maybe (RegValue sym TraceType)
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
C.lookupGlobal GlobalVar TraceType
g SymGlobalState sym
globals of
    Maybe (RegValue sym TraceType)
Nothing -> TraceGlobalNotDefined -> IO (RecordedTrace sym)
forall a e. Exception e => e -> a
X.throw TraceGlobalNotDefined
TraceGlobalNotDefined
    Just RegValue sym TraceType
s -> SymSequence sym (SymExpr sym (BaseStringType Unicode))
-> RecordedTrace sym
RegValue sym TraceType -> RecordedTrace sym
forall sym. RegValue sym TraceType -> RecordedTrace sym
RecordedTrace (SymSequence sym (SymExpr sym (BaseStringType Unicode))
 -> RecordedTrace sym)
-> IO (SymSequence sym (SymExpr sym (BaseStringType Unicode)))
-> IO (RecordedTrace sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym (SymExpr sym (BaseStringType Unicode))
-> IO (SymSequence sym (SymExpr sym (BaseStringType Unicode)))
concretizeAndReverseTrace SymSequence sym (SymExpr sym (BaseStringType Unicode))
RegValue sym TraceType
s
  where
    concretizeAndReverseTrace :: SymSequence sym (SymExpr sym (BaseStringType Unicode))
-> IO (SymSequence sym (SymExpr sym (BaseStringType Unicode)))
concretizeAndReverseTrace SymSequence sym (SymExpr sym (BaseStringType Unicode))
s = do
      Seq Text
concretized <- (Pred sym -> IO Bool)
-> (SymExpr sym (BaseStringType Unicode) -> IO Text)
-> SymSequence sym (SymExpr sym (BaseStringType Unicode))
-> IO (Seq Text)
forall sym a b.
(Pred sym -> IO Bool)
-> (a -> IO b) -> SymSequence sym a -> IO (Seq b)
CSSS.concretizeSymSequence Pred sym -> IO Bool
evalBool (sym -> SymExpr sym (BaseStringType Unicode) -> IO Text
forall sym.
IsExpr (SymExpr sym) =>
sym -> SymString sym Unicode -> IO Text
evalStr sym
sym) SymSequence sym (SymExpr sym (BaseStringType Unicode))
s
      let reversed :: Seq Text
reversed = Seq Text -> Seq Text
forall a. Seq a -> Seq a
Seq.reverse Seq Text
concretized
      Seq (SymExpr sym (BaseStringType Unicode))
symbolized <- (Text -> IO (SymExpr sym (BaseStringType Unicode)))
-> Seq Text -> IO (Seq (SymExpr sym (BaseStringType Unicode)))
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Seq a -> m (Seq b)
mapM (sym
-> StringLiteral Unicode
-> IO (SymExpr sym (BaseStringType Unicode))
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
forall (si :: StringInfo).
sym -> StringLiteral si -> IO (SymString sym si)
W4.stringLit sym
sym (StringLiteral Unicode
 -> IO (SymExpr sym (BaseStringType Unicode)))
-> (Text -> StringLiteral Unicode)
-> Text
-> IO (SymExpr sym (BaseStringType Unicode))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> StringLiteral Unicode
W4.UnicodeLiteral) Seq Text
reversed
      sym
-> [SymExpr sym (BaseStringType Unicode)]
-> IO (SymSequence sym (SymExpr sym (BaseStringType Unicode)))
forall sym a. sym -> [a] -> IO (SymSequence sym a)
CSSS.fromListSymSequence sym
sym (Seq (SymExpr sym (BaseStringType Unicode))
-> [SymExpr sym (BaseStringType Unicode)]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
F.toList Seq (SymExpr sym (BaseStringType Unicode))
symbolized)

    evalStr ::
      W4.IsExpr (W4.SymExpr sym) =>
      sym ->
      W4.SymString sym W4.Unicode ->
      IO Text.Text
    evalStr :: forall sym.
IsExpr (SymExpr sym) =>
sym -> SymString sym Unicode -> IO Text
evalStr sym
_sym SymString sym Unicode
s =
      case SymString sym Unicode -> Maybe (StringLiteral Unicode)
forall (si :: StringInfo).
SymExpr sym (BaseStringType si) -> Maybe (StringLiteral si)
forall (e :: BaseType -> Type) (si :: StringInfo).
IsExpr e =>
e (BaseStringType si) -> Maybe (StringLiteral si)
W4.asString SymString sym Unicode
s of
        Just (W4.UnicodeLiteral Text
s') -> Text -> IO Text
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Text
s'
        Maybe (StringLiteral Unicode)
Nothing -> String -> [String] -> IO Text
forall a. HasCallStack => String -> [String] -> a
panic String
"getRecordedTrace" [String
"Non-literal trace element?"]

{- | Inserts a recorded trace into the state's replay trace variable
The replay feature will follow this trace if it is enabled
-}
insertReplayTrace ::
  (HasReplayState p p sym ext rtp) =>
  C.SimState p sym ext rtp f args ->
  C.RegValue sym TraceType ->
  C.SimState p sym ext rtp f args
insertReplayTrace :: forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasReplayState p p sym ext rtp =>
SimState p sym ext rtp f args
-> RegValue sym TraceType -> SimState p sym ext rtp f args
insertReplayTrace SimState p sym ext rtp f args
st RegValue sym TraceType
v = do
  let simCtx :: SimContext p sym ext
simCtx = SimState p sym ext rtp f args
st SimState p sym ext rtp f args
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext rtp f 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 f 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)
C.stateContext
  let g :: GlobalVar TraceType
g = SimContext p sym ext
simCtx SimContext p sym ext
-> Getting
     (GlobalVar TraceType) (SimContext p sym ext) (GlobalVar TraceType)
-> GlobalVar TraceType
forall s a. s -> Getting a s a -> a
^. (p -> Const (GlobalVar TraceType) p)
-> SimContext p sym ext
-> Const (GlobalVar TraceType) (SimContext p sym ext)
forall p sym ext (f :: Type -> Type).
Functor f =>
(p -> f p) -> SimContext p sym ext -> f (SimContext p sym ext)
C.cruciblePersonality ((p -> Const (GlobalVar TraceType) p)
 -> SimContext p sym ext
 -> Const (GlobalVar TraceType) (SimContext p sym ext))
-> ((GlobalVar TraceType
     -> Const (GlobalVar TraceType) (GlobalVar TraceType))
    -> p -> Const (GlobalVar TraceType) p)
-> Getting
     (GlobalVar TraceType) (SimContext p sym ext) (GlobalVar TraceType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReplayState p sym ext rtp
 -> Const (GlobalVar TraceType) (ReplayState p sym ext rtp))
-> p -> Const (GlobalVar TraceType) p
forall p r sym ext rtp.
HasReplayState p r sym ext rtp =>
Lens' p (ReplayState r sym ext rtp)
Lens' p (ReplayState p sym ext rtp)
replayState ((ReplayState p sym ext rtp
  -> Const (GlobalVar TraceType) (ReplayState p sym ext rtp))
 -> p -> Const (GlobalVar TraceType) p)
-> ((GlobalVar TraceType
     -> Const (GlobalVar TraceType) (GlobalVar TraceType))
    -> ReplayState p sym ext rtp
    -> Const (GlobalVar TraceType) (ReplayState p sym ext rtp))
-> (GlobalVar TraceType
    -> Const (GlobalVar TraceType) (GlobalVar TraceType))
-> p
-> Const (GlobalVar TraceType) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GlobalVar TraceType
 -> Const (GlobalVar TraceType) (GlobalVar TraceType))
-> ReplayState p sym ext rtp
-> Const (GlobalVar TraceType) (ReplayState p sym ext rtp)
forall p sym ext rtp p ext rtp (f :: Type -> Type).
Functor f =>
(GlobalVar TraceType -> f (GlobalVar TraceType))
-> ReplayState p sym ext rtp -> f (ReplayState p sym ext rtp)
traceGlobal
  SimState p sym ext rtp f args
st SimState p sym ext rtp f args
-> (SimState p sym ext rtp f args -> SimState p sym ext rtp f args)
-> SimState p sym ext rtp f args
forall a b. a -> (a -> b) -> b
& (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp f args
-> Identity (SimState p sym ext rtp f args)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
C.stateGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp f args
 -> Identity (SimState p sym ext rtp f args))
-> (SymGlobalState sym -> SymGlobalState sym)
-> SimState p sym ext rtp f args
-> SimState p sym ext rtp f args
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ GlobalVar TraceType
-> RegValue sym TraceType
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
C.insertGlobal GlobalVar TraceType
g RegValue sym TraceType
v

-- | An 'C.ExecutionFeature' to replay traces recorded with 'recordFeature'.
--
-- Branches that deviate from the given trace will be aborted with
-- 'C.InfeasibleBranch'.
--
-- If this is not called with 'C.InitialState' before any other 'C.ExecState',
-- it may throw a 'TraceGlobalNotDefined' exception.
replayFeature ::
  ( HasReplayState p p sym ext rtp
  , W4.IsExprBuilder sym
  ) =>
  -- | Whether to stop at the end of the trace. If this is 'True' and execution
  -- has exhausted the trace, then any further execution will be aborted via
  -- 'C.InfeasibleBranch'.
  Bool ->
  C.ExecutionFeature p sym ext rtp
replayFeature :: forall p sym ext rtp.
(HasReplayState p p sym ext rtp, IsExprBuilder sym) =>
Bool -> ExecutionFeature p sym ext rtp
replayFeature Bool
stop =
  (ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
forall p sym ext rtp.
(ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
C.ExecutionFeature ((ExecState p sym ext rtp
  -> IO (ExecutionFeatureResult p sym ext rtp))
 -> ExecutionFeature p sym ext rtp)
-> (ExecState p sym ext rtp
    -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
forall a b. (a -> b) -> a -> b
$
    \case
      C.InitialState SimContext p sym ext
simCtx SymGlobalState sym
globals AbortHandler p sym ext (RegEntry sym ret)
abortHandler TypeRepr ret
retTy ExecCont
  p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
cont -> do
        let rstate :: ReplayState p sym ext (RegEntry sym ret)
rstate = SimContext p sym ext
simCtx SimContext p sym ext
-> Getting
     (ReplayState p sym ext (RegEntry sym ret))
     (SimContext p sym ext)
     (ReplayState p sym ext (RegEntry sym ret))
-> ReplayState p sym ext (RegEntry sym ret)
forall s a. s -> Getting a s a -> a
^. (p -> Const (ReplayState p sym ext (RegEntry sym ret)) p)
-> SimContext p sym ext
-> Const
     (ReplayState p sym ext (RegEntry sym ret)) (SimContext p sym ext)
forall p sym ext (f :: Type -> Type).
Functor f =>
(p -> f p) -> SimContext p sym ext -> f (SimContext p sym ext)
C.cruciblePersonality ((p -> Const (ReplayState p sym ext (RegEntry sym ret)) p)
 -> SimContext p sym ext
 -> Const
      (ReplayState p sym ext (RegEntry sym ret)) (SimContext p sym ext))
-> ((ReplayState p sym ext (RegEntry sym ret)
     -> Const
          (ReplayState p sym ext (RegEntry sym ret))
          (ReplayState p sym ext (RegEntry sym ret)))
    -> p -> Const (ReplayState p sym ext (RegEntry sym ret)) p)
-> Getting
     (ReplayState p sym ext (RegEntry sym ret))
     (SimContext p sym ext)
     (ReplayState p sym ext (RegEntry sym ret))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReplayState p sym ext (RegEntry sym ret)
 -> Const
      (ReplayState p sym ext (RegEntry sym ret))
      (ReplayState p sym ext (RegEntry sym ret)))
-> p -> Const (ReplayState p sym ext (RegEntry sym ret)) p
forall p r sym ext rtp.
HasReplayState p r sym ext rtp =>
Lens' p (ReplayState r sym ext rtp)
Lens' p (ReplayState p sym ext (RegEntry sym ret))
replayState
        let g :: GlobalVar TraceType
g =  ReplayState p sym ext (RegEntry sym ret)
rstate ReplayState p sym ext (RegEntry sym ret)
-> Getting
     (GlobalVar TraceType)
     (ReplayState p sym ext (RegEntry sym ret))
     (GlobalVar TraceType)
-> GlobalVar TraceType
forall s a. s -> Getting a s a -> a
^. Getting
  (GlobalVar TraceType)
  (ReplayState p sym ext (RegEntry sym ret))
  (GlobalVar TraceType)
forall p sym ext rtp p ext rtp (f :: Type -> Type).
Functor f =>
(GlobalVar TraceType -> f (GlobalVar TraceType))
-> ReplayState p sym ext rtp -> f (ReplayState p sym ext rtp)
traceGlobal
        let RecordedTrace RegValue sym TraceType
trace = ReplayState p sym ext (RegEntry sym ret)
rstate ReplayState p sym ext (RegEntry sym ret)
-> Getting
     (RecordedTrace sym)
     (ReplayState p sym ext (RegEntry sym ret))
     (RecordedTrace sym)
-> RecordedTrace sym
forall s a. s -> Getting a s a -> a
^. Getting
  (RecordedTrace sym)
  (ReplayState p sym ext (RegEntry sym ret))
  (RecordedTrace sym)
forall p sym ext rtp p sym ext rtp (f :: Type -> Type).
Functor f =>
(RecordedTrace sym -> f (RecordedTrace sym))
-> ReplayState p sym ext rtp -> f (ReplayState p sym ext rtp)
initialTrace
        let globals' :: SymGlobalState sym
globals' = GlobalVar TraceType
-> RegValue sym TraceType
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
C.insertGlobal GlobalVar TraceType
g RegValue sym TraceType
trace SymGlobalState sym
globals
        let iState :: ExecState p sym ext rtp
iState = SimContext p sym ext
-> SymGlobalState sym
-> AbortHandler p sym ext (RegEntry sym ret)
-> TypeRepr ret
-> ExecCont
     p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
-> ExecState p sym ext rtp
forall p sym ext rtp (ret :: CrucibleType).
(rtp ~ RegEntry sym ret) =>
SimContext p sym ext
-> SymGlobalState sym
-> AbortHandler p sym ext (RegEntry sym ret)
-> TypeRepr ret
-> ExecCont
     p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
-> ExecState p sym ext rtp
C.InitialState SimContext p sym ext
simCtx SymGlobalState sym
globals' AbortHandler p sym ext (RegEntry sym ret)
abortHandler TypeRepr ret
retTy ExecCont
  p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
cont
        ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecutionFeatureResult p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureModifiedState ExecState p sym ext rtp
iState
      C.RunningState RunningStateInfo blocks args
runStateInfo SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st -> do
        let sym :: sym
sym = SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     sym
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     sym
-> sym
forall s a. s -> Getting a s a -> a
^. Getting
  sym
  (SimState p sym ext rtp (CrucibleLang blocks r) ('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)
C.stateSymInterface
        SymSequence sym (SymExpr sym (BaseStringType Unicode))
s <- SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> IO (RegValue sym TraceType)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasReplayState p p sym ext rtp =>
SimState p sym ext rtp f args -> IO (RegValue sym TraceType)
getTraceOrThrow SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st
        PartExpr
  (SymExpr sym BaseBoolType)
  (SymExpr sym (BaseStringType Unicode),
   SymSequence sym (SymExpr sym (BaseStringType Unicode)))
partExpr <- sym
-> (SymExpr sym BaseBoolType
    -> SymExpr sym (BaseStringType Unicode)
    -> SymExpr sym (BaseStringType Unicode)
    -> IO (SymExpr sym (BaseStringType Unicode)))
-> SymSequence sym (SymExpr sym (BaseStringType Unicode))
-> IO
     (PartExpr
        (SymExpr sym BaseBoolType)
        (SymExpr sym (BaseStringType Unicode),
         SymSequence sym (SymExpr sym (BaseStringType Unicode))))
forall sym a.
IsExprBuilder sym =>
sym
-> (Pred sym -> a -> a -> IO a)
-> SymSequence sym a
-> IO (PartExpr (Pred sym) (a, SymSequence sym a))
CSSS.unconsSymSequence sym
sym (sym
-> SymExpr sym BaseBoolType
-> SymExpr sym (BaseStringType Unicode)
-> SymExpr sym (BaseStringType Unicode)
-> IO (SymExpr sym (BaseStringType Unicode))
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymString sym si
-> SymString sym si
-> IO (SymString sym si)
forall (si :: StringInfo).
sym
-> SymExpr sym BaseBoolType
-> SymString sym si
-> SymString sym si
-> IO (SymString sym si)
W4.stringIte sym
sym) SymSequence sym (SymExpr sym (BaseStringType Unicode))
s
        let badPath :: IO (ExecutionFeatureResult p sym ext rtp)
badPath = do
              ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
W4.getCurrentProgramLoc sym
sym
              let st' :: ExecState p sym ext rtp
st' = AbortExecReason
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)).
AbortExecReason
-> SimState p sym ext rtp f a -> ExecState p sym ext rtp
C.AbortState (ProgramLoc -> AbortExecReason
CB.InfeasibleBranch ProgramLoc
loc) SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st
              ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNewState ExecState p sym ext rtp
st')
        case PartExpr
  (SymExpr sym BaseBoolType)
  (SymExpr sym (BaseStringType Unicode),
   SymSequence sym (SymExpr sym (BaseStringType Unicode)))
partExpr of
          PartExpr
  (SymExpr sym BaseBoolType)
  (SymExpr sym (BaseStringType Unicode),
   SymSequence sym (SymExpr sym (BaseStringType Unicode)))
W4P.Unassigned
            | Bool
stop -> IO (ExecutionFeatureResult p sym ext rtp)
badPath
            | Bool
otherwise -> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange
          W4P.PE SymExpr sym BaseBoolType
valid (SymExpr sym (BaseStringType Unicode)
expectedLoc, SymSequence sym (SymExpr sym (BaseStringType Unicode))
rest) ->
            SimContext p sym ext
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (ExecutionFeatureResult p sym ext rtp))
-> IO (ExecutionFeatureResult p sym ext rtp)
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
C.withBackend (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext rtp (CrucibleLang blocks 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 (CrucibleLang blocks 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)
C.stateContext) ((forall {bak}.
  IsSymBackend sym bak =>
  bak -> IO (ExecutionFeatureResult p sym ext rtp))
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (ExecutionFeatureResult p sym ext rtp))
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
              let msg :: String
msg = String
"Trace must be valid"
              bak -> SymExpr sym BaseBoolType -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
CB.assert bak
bak SymExpr sym BaseBoolType
valid (String -> String -> SimErrorReason
C.AssertFailureSimError String
msg String
"")

              SymExpr sym (BaseStringType Unicode)
currLoc <- sym -> IO (RegValue sym ('BaseToType (BaseStringType Unicode)))
forall sym.
IsExprBuilder sym =>
sym -> IO (RegValue sym ('BaseToType (BaseStringType Unicode)))
locAsStr sym
sym
              SymExpr sym BaseBoolType
atExpectedLoc <- sym
-> SymExpr sym (BaseStringType Unicode)
-> SymExpr sym (BaseStringType Unicode)
-> IO (SymExpr sym BaseBoolType)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
forall (si :: StringInfo).
sym
-> SymString sym si
-> SymString sym si
-> IO (SymExpr sym BaseBoolType)
W4.stringEq sym
sym SymExpr sym (BaseStringType Unicode)
currLoc SymExpr sym (BaseStringType Unicode)
expectedLoc
              case SymExpr sym BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred SymExpr sym BaseBoolType
atExpectedLoc of
                Just Bool
False -> IO (ExecutionFeatureResult p sym ext rtp)
badPath
                Maybe Bool
_ -> do
                  let msg' :: String
msg' = String
"Execution deviated from trace"
                  bak -> SymExpr sym BaseBoolType -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
CB.assert bak
bak SymExpr sym BaseBoolType
atExpectedLoc (String -> String -> SimErrorReason
C.AssertFailureSimError String
msg' String
"")
                  let st' :: SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st' = SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> RegValue sym TraceType
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasReplayState p p sym ext rtp =>
SimState p sym ext rtp f args
-> RegValue sym TraceType -> SimState p sym ext rtp f args
insertReplayTrace SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st SymSequence sym (SymExpr sym (BaseStringType Unicode))
RegValue sym TraceType
rest
                  let rState :: ExecState p sym ext rtp
rState = RunningStateInfo blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (args :: Ctx CrucibleType).
RunningStateInfo blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
C.RunningState RunningStateInfo blocks args
runStateInfo SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st'
                  ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureModifiedState ExecState p sym ext rtp
rState)

      ExecState p sym ext rtp
_ -> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange
  where
    getTraceOrThrow ::
      HasReplayState p p sym ext rtp =>
      C.SimState p sym ext rtp f args ->
      IO (C.RegValue sym TraceType)
    getTraceOrThrow :: forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasReplayState p p sym ext rtp =>
SimState p sym ext rtp f args -> IO (RegValue sym TraceType)
getTraceOrThrow SimState p sym ext rtp f args
st =
      case SimState p sym ext rtp f args -> Maybe (RegValue sym TraceType)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
HasReplayState p p sym ext rtp =>
SimState p sym ext rtp f args -> Maybe (RegValue sym TraceType)
getReplayTrace SimState p sym ext rtp f args
st of
        Maybe (RegValue sym TraceType)
Nothing -> TraceGlobalNotDefined
-> IO (SymSequence sym (SymExpr sym (BaseStringType Unicode)))
forall a e. Exception e => e -> a
X.throw TraceGlobalNotDefined
TraceGlobalNotDefined
        Just RegValue sym TraceType
t -> SymSequence sym (SymExpr sym (BaseStringType Unicode))
-> IO (SymSequence sym (SymExpr sym (BaseStringType Unicode)))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymSequence sym (SymExpr sym (BaseStringType Unicode))
RegValue sym TraceType
t