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

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.

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

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

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.

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.

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.

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

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

The result of resolving a function call.

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

A map from function handles to their semantics.

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.

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

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.

Create a new SimContext with the given bindings.

Access the symbolic backend inside a SimContext.

A map from function handles to their semantics.

Access the custom user-state inside the SimContext.

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

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.

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