Lang.Crucible.Simulator.ExecutionTree

Execution trees record the state of the simulator as it explores execution paths through a program. This module defines the collection of datatypes that record the state of a running simulator and basic lenses and accessors for these types. See Lang.Crucible.Simulator.Operations for the definitions of operations that manipulate these datastructures to drive them through the simulator state machine.

GlobalPair

data GlobalPair sym (v :: Type)

A value of some type v together with a global state.

Constructors

GlobalPair

Fields

• _gpValue :: !v
• _gpGlobals :: !(SymGlobalState sym)

gpValue :: Lens (GlobalPair sym u) (GlobalPair sym v) u v

Access the value stored in the global pair.

gpGlobals :: Simple Lens (GlobalPair sym u) (SymGlobalState sym)

Access the globals stored in the global pair.

TopFrame

type TopFrame sym ext f a = GlobalPair sym (SimFrame sym ext f a)

The currently-executing frame plus the global state associated with it.

crucibleTopFrame :: Lens (TopFrame sym ext (CrucibleLang blocks r) ('Just args)) (TopFrame sym ext (CrucibleLang blocks r) ('Just args')) (CallFrame sym ext blocks r args) (CallFrame sym ext blocks r args')

Access the Crucible call frame inside a TopFrame.

overrideTopFrame :: Lens (TopFrame sym ext (OverrideLang r) ('Just args)) (TopFrame sym ext (OverrideLang r') ('Just args')) (OverrideFrame sym r args) (OverrideFrame sym r' args')

CrucibleBranchTarget

data CrucibleBranchTarget f (args :: Maybe (Ctx CrucibleType)) where

A CrucibleBranchTarget identifies a program location that is a potential join point. Each label is a merge point, and there is an additional implicit join point at function returns.

Constructors

BlockTarget :: !(BlockID blocks args) -> CrucibleBranchTarget (CrucibleLang blocks r) ('Just args)

ReturnTarget :: CrucibleBranchTarget f 'Nothing

Instances

TestEquality (CrucibleBranchTarget f :: Maybe (Ctx CrucibleType) -> Type)

Defined in Lang.Crucible.Simulator.CallFrame

Methods

testEquality :: forall (a :: k) (b :: k). CrucibleBranchTarget f a -> CrucibleBranchTarget f b -> Maybe (a :~: b)

ppBranchTarget :: CrucibleBranchTarget f args -> String

AbortedResult

data AbortedResult sym ext where

An execution path that was prematurely aborted. Note, an abort does not necessarily indicate an error condition. An execution path might abort because it became infeasible (inconsistent path conditions), because the program called an exit primitive, or because of a true error condition (e.g., a failed assertion).

Constructors

AbortedExec :: !AbortExecReason -> !(GlobalPair sym (SimFrame sym ext l args)) -> AbortedResult sym ext

A single aborted execution with the execution state at time of the abort and the reason.

AbortedExit :: !ExitCode -> AbortedResult sym ext

An aborted execution that was ended by a call to exit.

AbortedBranch :: !ProgramLoc -> !(Pred sym) -> !(AbortedResult sym ext) -> !(AbortedResult sym ext) -> AbortedResult sym ext

Two separate threads of execution aborted after a symbolic branch, possibly for different reasons.

data SomeFrame (f :: fk -> argk -> Type)

This represents an execution frame where its frame type and arguments have been hidden.

Constructors

forall l a. SomeFrame !(f l a)

filterCrucibleFrames :: SomeFrame (SimFrame sym ext) -> Maybe ProgramLoc

Return the program locations of all the Crucible frames.

arFrames :: Simple Traversal (AbortedResult sym ext) (SomeFrame (SimFrame sym ext))

Iterate over frames in the result.

ppExceptionContext :: [SomeFrame (SimFrame sym ext)] -> Doc ann

Print an exception context

Partial result

data PartialResult sym ext (v :: Type)

A PartialResult represents the result of a computation that might be only partially defined. If the result is a TotalResult, the the result is fully defined; however if it is a PartialResult, then some of the computation paths that led to this result aborted for some reason, and the resulting value is only defined if the associated condition is true.

Constructors

TotalRes !(GlobalPair sym v)

A TotalRes indicates that the the global pair is always defined.

PartialRes !ProgramLoc !(Pred sym) !(GlobalPair sym v) !(AbortedResult sym ext)

PartialRes indicates that the global pair may be undefined under some circumstances. The predicate specifies under what conditions the GlobalPair is defined. The AbortedResult describes the circumstances under which the result would be partial.

type PartialResultFrame sym ext f args = PartialResult sym ext (SimFrame sym ext f args)

partialValue :: Lens (PartialResult sym ext u) (PartialResult sym ext v) (GlobalPair sym u) (GlobalPair sym v)

Access the value stored in the partial result.

Execution states

data ExecResult p sym ext (r :: Type)

Executions that have completed either due to (partial or total) successful completion or by some abort condition.

Constructors

FinishedResult !(SimContext p sym ext) !(PartialResult sym ext r)

At least one execution path resulted in some return result.

AbortedResult !(SimContext p sym ext) !(AbortedResult sym ext)

All execution paths resulted in an abort condition, and there is no result to return.

TimeoutResult !(ExecState p sym ext r)

An execution stopped somewhere in the middle of a run because a timeout condition occurred.

data ExecState p sym ext (rtp :: Type)

An ExecState represents an intermediate state of executing a Crucible program. The Crucible simulator executes by transitioning between these different states until it results in a ResultState, indicating the program has completed.

Constructors

ResultState !(ExecResult p sym ext rtp)

The ResultState is used to indicate that the program has completed.

forall f a. AbortState !AbortExecReason !(SimState p sym ext rtp f a)

An abort state indicates that the included SimState encountered an abort event while executing its next step. The state needs to be unwound to its nearest enclosing branch point and resumed.

forall f a r. UnwindCallState !(ValueFromValue p sym ext rtp r) !(AbortedResult sym ext) !(SimState p sym ext rtp f a)

An unwind call state occurs when we are about to leave the context of a function call because of an abort. The included ValueFromValue is the context of the call site we are about to unwind into, and the AbortedResult indicates the reason we are aborting.

forall f a ret. CallState !(ReturnHandler ret p sym ext rtp f a) !(ResolvedCall p sym ext ret) !(SimState p sym ext rtp f a)

A call state is entered when we are about to make a function call to the included call frame, which has already resolved the implementation and arguments to the function.

forall f a ret. TailCallState !(ValueFromValue p sym ext rtp ret) !(ResolvedCall p sym ext ret) !(SimState p sym ext rtp f a)

A tail-call state is entered when we are about to make a function call to the included call frame, and this is the last action we need to take in the current caller. Note, we can only enter a tail-call state if there are no pending merge points in the caller. This means that sometimes calls that appear to be in tail-call position may nonetheless have to be treated as ordinary calls.

forall f a ret. ReturnState !FunctionName !(ValueFromValue p sym ext rtp ret) !(RegEntry sym ret) !(SimState p sym ext rtp f a)

A return state is entered after the final return value of a function is computed, and just before we resolve injecting the return value back into the caller's context.

forall blocks r args. RunningState !(RunningStateInfo blocks args) !(SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))

A running state indicates the included SimState is ready to enter and execute a Crucible basic block, or to resume a basic block from a call site.

forall f args postdom_args. SymbolicBranchState !(Pred sym) !(PausedFrame p sym ext rtp f) !(PausedFrame p sym ext rtp f) !(CrucibleBranchTarget f postdom_args) !(SimState p sym ext rtp f ('Just args))

A symbolic branch state indicates that the execution needs to branch on a non-trivial symbolic condition. The included Pred is the condition to branch on. The first PausedFrame is the path that corresponds to the Pred being true, and the second is the false branch.

forall f a. ControlTransferState !(ControlResumption p sym ext rtp f) !(SimState p sym ext rtp f ('Just a))

A control transfer state is entered just prior to invoking a control resumption. Control resumptions are responsible for transitioning from the end of one basic block to another, although there are also some intermediate states related to resolving switch statements.

forall args ret. OverrideState !(Override p sym ext args ret) !(SimState p sym ext rtp (OverrideLang ret) ('Just args))

An override state indicates the included SimState is prepared to execute a code override.

forall f args. BranchMergeState !(CrucibleBranchTarget f args) !(SimState p sym ext rtp f args)

A branch merge state occurs when the included SimState is in the process of transferring control to the included CrucibleBranchTarget. We enter a BranchMergeState every time we need to _check_ if there is a pending branch, even if no branch is pending. During this process, paths may have to be merged. If several branches must merge at the same control point, this state may be entered several times in succession before returning to a RunningState.

forall ret.rtp ~ RegEntry sym ret => InitialState !(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))

An initial state indicates the state of a simulator just before execution begins. It specifies all the initial data necessary to begin simulating. The given ExecCont will be executed in a fresh SimState representing the default starting call frame.

type ExecCont p sym ext r f a = ReaderT (SimState p sym ext r f a) IO (ExecState p sym ext r)

An action which will construct an ExecState given a current SimState. Such continuations correspond to a single transition of the simulator transition system.

data RunningStateInfo blocks args

Some additional information attached to a RunningState that indicates how we got to this running state.

Constructors

RunBlockStart !(BlockID blocks args)

This indicates that we are now in a RunningState because we transferred execution to the start of a basic block.

RunBlockEnd !(Some (BlockID blocks))

This indicates that we are in a RunningState because we reached the terminal statement of a basic block.

RunReturnFrom !FunctionName

This indicates that we are in a RunningState because we returned from calling the named function.

RunPostBranchMerge !(BlockID blocks args)

This indicates that we are now in a RunningState because we finished branch merging prior to the start of a block.

data ResolvedCall p sym ext ret where

The result of resolving a function call.

Constructors

OverrideCall :: !(Override p sym ext args ret) -> !(OverrideFrame sym ret args) -> ResolvedCall p sym ext ret

A resolved function call to an override.

CrucibleCall :: !(BlockID blocks args) -> !(CallFrame sym ext blocks ret args) -> ResolvedCall p sym ext ret

A resolved function call to a Crucible function.

resolvedCallHandle :: ResolvedCall p sym ext ret -> SomeHandle

execResultContext :: ExecResult p sym ext r -> SimContext p sym ext

execStateContext :: ExecState p sym ext r -> SimContext p sym ext

execStateSimState :: ExecState p sym ext r -> Maybe (SomeSimState p sym ext r)

Simulator context trees

Main context data structures

data ValueFromValue p sym ext (ret :: Type) (top_return :: CrucibleType)

This type contains information about the current state of the exploration of the branching structure of a program. The ValueFromValue states correspond to stack call frames in a more traditional simulator environment.

The type parameters have the following meanings:

• p is the personality of the simulator (i.e., custom user state).
• sym is the simulator backend being used.
• ext specifies what extensions to the Crucible language are enabled
• ret is the global return type of the entire computation
• top_return is the return type of the top-most call on the stack.

Constructors

forall args caller. VFVCall !(ValueFromFrame p sym ext ret caller) !(SimFrame sym ext caller args) !(ReturnHandler top_return p sym ext ret caller args)

VFVCall denotes a call site in the outer context, and represents the point to which a function higher on the stack will eventually return. The three arguments are:

• The context in which the call happened.
• The frame of the caller
• How to modify the current sim frame and resume execution when we obtain the return value

VFVPartial !(ValueFromValue p sym ext ret top_return) !ProgramLoc !(Pred sym) !(AbortedResult sym ext)

A partial value. The predicate indicates what needs to hold to avoid the partiality. The AbortedResult describes what could go wrong if the predicate does not hold.

ret ~ RegEntry sym top_return => VFVEnd

The top return value, indicating the program termination point.

Instances

Pretty (ValueFromValue p ext sym root rp)

Defined in Lang.Crucible.Simulator.ExecutionTree

Methods

pretty :: ValueFromValue p ext sym root rp -> Doc ann

prettyList :: [ValueFromValue p ext sym root rp] -> Doc ann

data ValueFromFrame p sym ext (ret :: Type) (f :: Type)

This type contains information about the current state of the exploration of the branching structure of a program. The ValueFromFrame states correspond to the structure of symbolic branching that occurs within a single function call.

The type parameters have the following meanings:

• p is the personality of the simulator (i.e., custom user state).
• sym is the simulator backend being used.
• ext specifies what extensions to the Crucible language are enabled
• ret is the global return type of the entire execution.
• f is the type of the top frame.

Constructors

forall args. VFFBranch !(ValueFromFrame p sym ext ret f) !FrameIdentifier !ProgramLoc !(Pred sym) !(VFFOtherPath p sym ext ret f args) !(CrucibleBranchTarget f args)

We are working on a branch; this could be the first or the second of both branches (see the VFFOtherPath field).

VFFPartial !(ValueFromFrame p sym ext ret f) !ProgramLoc !(Pred sym) !(AbortedResult sym ext) !PendingPartialMerges

We are on a branch where the other branch was aborted before getting to the merge point.

VFFEnd !(ValueFromValue p sym ext ret (FrameRetType f))

When we are finished with this branch we should return from the function.

Instances

Pretty (ValueFromFrame p ext sym ret f)

Defined in Lang.Crucible.Simulator.ExecutionTree

Methods

pretty :: ValueFromFrame p ext sym ret f -> Doc ann

prettyList :: [ValueFromFrame p ext sym ret f] -> Doc ann

data PendingPartialMerges

Data about whether the surrounding context is expecting a merge to occur or not. If the context sill expects a merge, we need to take some actions to indicate that the merge will not occur; otherwise there is no special work to be done.

Constructors

NoNeedToAbort

Don't indicate an abort condition in the context

NeedsToBeAborted

Indicate an abort condition in the context when we get there again.

Paused Frames

data ResolvedJump sym blocks

A ResolvedJump is a block label together with a collection of actual arguments that are expected by that block. These data are sufficient to actually transfer control to the named label.

Constructors

forall args. ResolvedJump !(BlockID blocks args) !(RegMap sym args)

data ControlResumption p sym ext rtp f where

When a path of execution is paused by the symbolic simulator (while it first explores other paths), a ControlResumption indicates what actions must later be taken in order to resume execution of that path.

Constructors

ContinueResumption :: !(ResolvedJump sym blocks) -> ControlResumption p sym ext rtp (CrucibleLang blocks r)

When resuming a paused frame with a ContinueResumption, no special work needs to be done, simply begin executing statements of the basic block.

CheckMergeResumption :: !(ResolvedJump sym blocks) -> ControlResumption p sym ext rtp (CrucibleLang blocks r)

When resuming with a CheckMergeResumption, we must check for the presence of pending merge points before resuming.

SwitchResumption :: ![(Pred sym, ResolvedJump sym blocks)] -> ControlResumption p sym ext rtp (CrucibleLang blocks r)

When resuming a paused frame with a SwitchResumption, we must continue branching to possible alternatives in a variant elimination statement. In other words, we are still in the process of transferring control away from the current basic block (which is now at a final VariantElim terminal statement).

OverrideResumption :: ExecCont p sym ext rtp (OverrideLang r) ('Just args) -> !(RegMap sym args) -> ControlResumption p sym ext rtp (OverrideLang r)

When resuming a paused frame with an OverrideResumption, we simply return control to the included thunk, which represents the remaining computation for the override.

data PausedFrame p sym ext rtp f

A PausedFrame represents a path of execution that has been postponed while other paths are explored. It consists of a (potentially partial) SimFrame together with some information about how to resume execution of that frame.

Constructors

forall old_args. PausedFrame

Fields

• pausedFrame :: !(PartialResultFrame sym ext f ('Just old_args))
• resume :: !(ControlResumption p sym ext rtp f)
• pausedLoc :: !(Maybe ProgramLoc)

Sibling paths

data VFFOtherPath p sym ext ret f args

This describes the state of the sibling path at a symbolic branch point. A symbolic branch point starts with the sibling in the VFFActivePath state, which indicates that the sibling path still needs to be executed. After the first path to be explored has reached the merge point, the places of the two paths are exchanged, and the completed path is stored in the VFFCompletePath state until the second path also reaches its merge point. The two paths will then be merged, and execution will continue beyond the merge point.

Constructors

VFFActivePath !(PausedFrame p sym ext ret f)

This corresponds the a path that still needs to be analyzed.

VFFCompletePath !(Assumptions sym) !(PartialResultFrame sym ext f args)

This is a completed execution path.

Instances

Pretty (VFFOtherPath ctx sym ext r f a)

Defined in Lang.Crucible.Simulator.ExecutionTree

Methods

pretty :: VFFOtherPath ctx sym ext r f a -> Doc ann

prettyList :: [VFFOtherPath ctx sym ext r f a] -> Doc ann

type family FrameRetType (f :: Type) :: CrucibleType where ...

Equations

FrameRetType (CrucibleLang b r) = r

FrameRetType (OverrideLang r) = r

ReturnHandler

data ReturnHandler (ret :: CrucibleType) p sym ext root f args where

A ReturnHandler indicates what actions to take to resume executing in a caller's context once a function call has completed and the return value is available.

The type parameters have the following meanings:

• ret is the type of the return value that is expected.
• p is the personality of the simulator (i.e., custom user state).
• sym is the simulator backend being used.
• ext specifies what extensions to the Crucible language are enabled.
• root is the global return type of the entire computation.
• f is the stack type of the caller.
• args is the type of the local variables in scope prior to the call.

Constructors

ReturnToOverride :: (RegEntry sym ret -> SimState p sym ext root (OverrideLang r) ('Just args) -> IO (ExecState p sym ext root)) -> ReturnHandler ret p sym ext root (OverrideLang r) ('Just args)

The ReturnToOverride constructor indicates that the calling context is primitive code written directly in Haskell.

ReturnToCrucible :: TypeRepr ret -> StmtSeq ext blocks r (ctx ::> ret) -> ReturnHandler ret p sym ext root (CrucibleLang blocks r) ('Just ctx)

The ReturnToCrucible constructor indicates that the calling context is an ordinary function call position from within a Crucible basic block. The included StmtSeq is the remaining statements in the basic block to be executed following the return.

TailReturnToCrucible :: ret ~ r => ReturnHandler ret p sym ext root (CrucibleLang blocks r) ctx

The TailReturnToCrucible constructor indicates that the calling context is a tail call position from the end of a Crucible basic block. Upon receiving the return value, that value should be immediately returned in the caller's context as well.

ActiveTree

data ActiveTree p sym ext root (f :: Type) args

An active execution tree contains at least one active execution. The data structure is organized so that the current execution can be accessed rapidly.

Constructors

ActiveTree

Fields

• _actContext :: !(ValueFromFrame p sym ext root f)
• _actResult :: !(PartialResultFrame sym ext f args)

singletonTree :: TopFrame sym ext f args -> ActiveTree p sym ext (RegEntry sym (FrameRetType f)) f args

Create a tree with a single top frame.

activeFrames :: ActiveTree ctx sym ext root a args -> [SomeFrame (SimFrame sym ext)]

Return the call stack of all active frames, in reverse activation order (i.e., with callees appearing before callers).

actContext :: Lens (ActiveTree p sym ext root f args) (ActiveTree p sym ext root f args) (ValueFromFrame p sym ext root f) (ValueFromFrame p sym ext root f)

Access the calling context of the currently-active frame

actFrame :: Lens (ActiveTree p sym ext root f args) (ActiveTree p sym ext root f args') (TopFrame sym ext f args) (TopFrame sym ext f args')

Access the currently-active frame

Simulator context

Function bindings

data Override p sym ext (args :: Ctx CrucibleType) ret

A definition of a function's semantics, given as a Haskell action.

Constructors

Override

Fields

• overrideName :: FunctionName
• overrideHandler :: forall r. ExecCont p sym ext r (OverrideLang ret) ('Just args)

data FnState p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType)

State used to indicate what to do when function is called. A function may either be defined by writing a Haskell Override or by giving a Crucible control-flow graph representation.

Constructors

UseOverride !(Override p sym ext args ret)

forall blocks. UseCFG !(CFG ext blocks args ret) !(CFGPostdom blocks)

newtype FunctionBindings p sym ext

A map from function handles to their semantics.

Constructors

FnBindings

Fields

• fnBindings :: FnHandleMap (FnState p sym ext)

Extensions

data ExtensionImpl p sym ext

In order to start executing a simulator, one must provide an implementation of the extension syntax. This includes an evaluator for the added expression forms, and an evaluator for the added statement forms.

Constructors

ExtensionImpl

Fields

• extensionEval :: forall bak rtp blocks r ctx. IsSymBackend sym bak => bak -> IntrinsicTypes sym -> (Int -> String -> IO ()) -> CrucibleState p sym ext rtp blocks r ctx -> EvalAppFunc sym (ExprExtension ext)
• extensionExec :: EvalStmtFunc p sym ext

type EvalStmtFunc p sym ext = forall rtp blocks r ctx tp'. StmtExtension ext (RegEntry sym) tp' -> CrucibleState p sym ext rtp blocks r ctx -> IO (RegValue sym tp', CrucibleState p sym ext rtp blocks r ctx)

The type of functions that interpret extension statements. These have access to the main simulator state, and can make fairly arbitrary changes to it.

emptyExtensionImpl :: ExtensionImpl p sym ()

Trivial implementation for the "empty" extension, which adds no additional syntactic forms.

SimContext record

type IsSymInterfaceProof sym a = (IsSymInterface sym => a) -> a

data SimContext (personality :: Type) (sym :: Type) (ext :: Type)

Top-level state record for the simulator. The state contained in this record remains persistent across all symbolic simulator actions. In particular, it is not rolled back when the simulator returns previous program points to explore additional paths, etc.

Constructors

SimContext

Fields

• _ctxBackend :: !(SomeBackend sym)
• ctxSolverProof :: !(forall a. IsSymInterfaceProof sym a)

  Class dictionary for IsSymInterface sym

• ctxIntrinsicTypes :: !(IntrinsicTypes sym)
• simHandleAllocator :: !HandleAllocator

  Allocator for function handles

• printHandle :: !Handle

  Handle to write messages to.

• extensionImpl :: ExtensionImpl personality sym ext
• _functionBindings :: !(FunctionBindings personality sym ext)
• _cruciblePersonality :: !personality
• _profilingMetrics :: !(Map Text (Metric personality sym ext))

newtype Metric p sym ext

Constructors

Metric

Fields

• runMetric :: forall rtp f args. SimState p sym ext rtp f args -> IO Integer

initSimContext

Arguments

:: IsSymBackend sym bak

=> bak

Symbolic backend

-> IntrinsicTypes sym

Implementations of intrinsic types

-> HandleAllocator

Handle allocator for creating new function handles

-> Handle

Handle to write output to

-> FunctionBindings personality sym ext

Initial bindings for function handles

-> ExtensionImpl personality sym ext

Semantics for extension syntax

-> personality

Initial value for custom user state

-> SimContext personality sym ext

Create a new SimContext with the given bindings.

withBackend :: SimContext personality sym ext -> (forall bak. IsSymBackend sym bak => bak -> a) -> a

ctxSymInterface :: Getter (SimContext p sym ext) sym

Access the symbolic backend inside a SimContext.

functionBindings :: Lens' (SimContext p sym ext) (FunctionBindings p sym ext)

A map from function handles to their semantics.

cruciblePersonality :: Lens' (SimContext p sym ext) p

Access the custom user-state inside the SimContext.

profilingMetrics :: Lens' (SimContext p sym ext) (Map Text (Metric p sym ext))

SimState

data SimState p sym ext rtp f (args :: Maybe (Ctx CrucibleType))

A SimState contains the execution context, an error handler, and the current execution tree. It captures the entire state of the symbolic simulator.

Constructors

SimState

Fields

• _stateContext :: !(SimContext p sym ext)
• _abortHandler :: !(AbortHandler p sym ext rtp)
• _stateTree :: !(ActiveTree p sym ext rtp f args)

Instances

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

Defined in Lang.Crucible.Simulator.OverrideSim

Methods

get :: OverrideSim p sym ext rtp args ret (SimState p sym ext rtp (OverrideLang ret) ('Just args))

put :: SimState p sym ext rtp (OverrideLang ret) ('Just args) -> OverrideSim p sym ext rtp args ret ()

state :: (SimState p sym ext rtp (OverrideLang ret) ('Just args) -> (a, SimState p sym ext rtp (OverrideLang ret) ('Just args))) -> OverrideSim p sym ext rtp args ret a

data SomeSimState p sym ext rtp

Constructors

forall f args. SomeSimState !(SimState p sym ext rtp f args)

initSimState

Arguments

:: SimContext p sym ext

initial SimContext state

-> SymGlobalState sym

state of Crucible global variables

-> AbortHandler p sym ext (RegEntry sym ret)

initial abort handler

-> TypeRepr ret

-> IO (SimState p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx))

Create an initial SimState

stateLocation :: Getter (SimState p sym ext r f a) (Maybe ProgramLoc)

newtype AbortHandler p sym ext rtp

An abort handler indicates to the simulator what actions to take when an abort occurs. Usually, one should simply use the defaultAbortHandler from Lang.Crucible.Simulator, which unwinds the tree context to the nearest branch point and correctly resumes simulation. However, for some use cases, it may be desirable to take additional or alternate actions on abort events; in which case, the library user may replace the default abort handler with their own.

Constructors

AH

Fields

• runAH :: forall (l :: Type) args. AbortExecReason -> ExecCont p sym ext rtp l args

type CrucibleState p sym ext rtp blocks ret args = SimState p sym ext rtp (CrucibleLang blocks ret) ('Just args)

A simulator state that is currently executing Crucible instructions.

Lenses and accessors

stateTree :: Lens (SimState p sym ext rtp f a) (SimState p sym ext rtp g b) (ActiveTree p sym ext rtp f a) (ActiveTree p sym ext rtp g b)

Access the active tree associated with a state.

abortHandler :: Simple Lens (SimState p sym ext r f a) (AbortHandler p sym ext r)

Access the current abort handler of a state.

stateContext :: Simple Lens (SimState p sym ext r f a) (SimContext p sym ext)

Access the SimContext inside a SimState

stateCrucibleFrame :: Lens (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)) (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a')) (CallFrame sym ext blocks r a) (CallFrame sym ext blocks r a')

Access the Crucible call frame inside a SimState

stateSymInterface :: Getter (SimState p sym ext r f a) sym

Get the symbolic interface out of a SimState

stateSolverProof :: SimState p sym ext r f args -> forall a. IsSymInterfaceProof sym a

Provide the IsSymInterface typeclass dictionary from a SimState

stateIntrinsicTypes :: Getter (SimState p sym ext r f args) (IntrinsicTypes sym)

Get the intrinsic type map out of a SimState

stateOverrideFrame :: Lens (SimState p sym ext q (OverrideLang r) ('Just a)) (SimState p sym ext q (OverrideLang r) ('Just a')) (OverrideFrame sym r a) (OverrideFrame sym r a')

Access the override frame inside a SimState

stateGlobals :: Simple Lens (SimState p sym ext q f args) (SymGlobalState sym)

Access the globals inside a SimState

stateConfiguration :: Getter (SimState p sym ext r f args) Config

Get the configuration object out of a SimState