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

Type parameters:

• sym: instance of IsSymInterface
• v: type of the value

Access the value stored in the global pair.

Access the globals stored in the global pair.

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

Type parameters:

• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• f: the type of the top frame (CrucibleLang or OverrideLang)
• args: arguments to this frame (see SimFrame)

Access the Crucible call frame inside a TopFrame.

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.

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).

Type parameters:

• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension

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

The type parameter f is usually SimFrame.

Return the program locations of all the Crucible frames.

Iterate over frames in the result.

Print an exception context

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.

Type parameters:

• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• v: Type of the result of the computation

Access the value stored in the partial result.

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

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• rtp: type of the return value

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.

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• rtp: type of the return value

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

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• rtp: type of the return value
• f: the type of the top frame (CrucibleLang or OverrideLang)
• args: arguments to the current frame (see SimFrame)

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

Type parameters:

• blocks: types of variables in scope from previous blocks
• args: arguments to this block

The result of resolving a function call.

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• ret: CrucibleType of the return value

Extract the SymGlobalState from an ExecResult.

Extract the SymGlobalState from an ExecState.

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.

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• ret: global return type of the entire execution
• top_return: return type of the top-most call on the stack.

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.

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• ret: global return type of the entire execution
• f: the type of the top frame (CrucibleLang or OverrideLang)

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.

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.

Type parameters:

• sym: instance of IsSymInterface
• blocks: types of variables in scope from previous blocks

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.

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• rtp: type of the return value
• f: the type of the top frame (CrucibleLang or OverrideLang)

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.

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• rtp: type of the return value
• f: the type of the top frame (CrucibleLang or OverrideLang)

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.

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• rtp: type of the return value
• f: the type of the top frame (CrucibleLang or OverrideLang)
• args: arguments to this frame (see SimFrame)

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.

Type parameters:

• ret: the type of the return value that is expected
• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• root: global return type of the entire computation
• f: the frame type of the caller (CrucibleLang or OverrideLang)
• args: types of the local variables in scope prior to the call (see SimFrame)

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

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• root: global return type of the entire computation
• f: the frame type of the caller (CrucibleLang or OverrideLang) -- - args: arguments to the current frame (see SimFrame)

Create a tree with a single top frame.

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

Access the calling context of the currently-active frame

Access the currently-active frame

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

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• args: types of arguments to the override
• ret: return type of the override

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.

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• args: argument types
• ret: return type

A map from function handles to their semantics.

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension

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.

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension

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

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension

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

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.

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension

Some kind of Integer to be collected during execution.

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension

Create a new SimContext with the given bindings.

Access the symbolic backend inside a SimContext.

A map from function handles to their semantics.

Custom state inside the SimContext.

Crucible itself is entirely polymorphic over p. Downstream applications can instantiate it to any sort of state that they would like to associate with a SimContext.

For example, applications based on macaw-symbolic can instantiate this to a structure holding enough information to perform incremental code discovery. See ambient-verifier's AmbientSimulatorState.

Code that needs to store some state in the personality but doesn't wish to fix a particular type can use the "classy lenses" approach, e.g.,

class HasFooState p where
  fooState :: Lens' p FooState

For examples of this approach, see

• HasMacawLazySimulatorState
• HasGreaseSimulatorState

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

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• rtp: type of the return value
• f: the type of the top frame (CrucibleLang or OverrideLang)
• args: arguments to the current frame (see SimFrame)

Create an initial SimState

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.

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• rtp: type of the return value

A simulator state that is currently executing Crucible instructions.

Access the active tree associated with a state.

Access the current abort handler of a state.

Access the SimContext inside a SimState

Access the Crucible call frame inside a SimState

Get the symbolic interface out of a SimState

Provide the IsSymInterface typeclass dictionary from a SimState

Get the intrinsic type map out of a SimState

Access the override frame inside a SimState

Access the globals inside a SimState

Get the configuration object out of a SimState