Maps register types to the runtime representation.

A newtype wrapper around RegValue. This is wrapper necessary because RegValue is a type family and, as such, cannot be partially applied.

Construct a VariantType value by identifying which branch of the variant to construct, and providing a value of the correct type.

Represents a function closure.

Extract the runtime representation of the type of the given FnVal

The value of a register.

A set of registers in an execution frame.

Create a new set of registers.

Class for exceptions generated by simulator.

A global variable.

A map from global variables to their value.

The empty set of global variable bindings.

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.

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

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)

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

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

The default abort handler calls abortExecAndLog.

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 SimContext inside a SimState

Type family for intrinsic type representations. Intrinsic types are identified by a type-level Symbol, and this typeclass allows backends to define implementations for these types.

An instance of this class defines both an instance for the Intrinsic type family (which defines the runtime representation for this intrinsic type) and also the muxIntrinsic method (which defines how to merge to intrinsic values when the simulator reaches a merge point).

Note: Instances of this will typically end up as orphan instances. This warning is normally quite important, as orphan instances allow one to define multiple instances for a particular class. However, in this case, IntrinsicClass contains a type family, and GHC will globally check consistency of all type family instances. Consequently, there can be at most one implementation of IntrinsicClass in a program.

The IntrinsicMuxFn datatype allows an IntrinsicClass instance to be packaged up into a value. This allows us to get access to IntrinsicClass instance methods (the muxIntrinsic method in particular) at runtime even for symbol names that are not known statically.

By packaging up a type class instance (rather than just providing some method with the same signature as muxIntrinsic) we get the compiler to ensure that a single distinguished implementation is always used for each backend/symbol name combination. This prevents any possible confusion between different parts of the system.

IntrinsicTypes is a map from symbol name representatives to IntrinsicMuxFn values. Such a map is useful for providing access to intrinsic type implementations that are not known statically at compile time.

An empty collection of intrinsic types, for cases where no additional types are required

Given a SimState and an execution continuation, apply the continuation and execute the resulting computation until completion.

This function is responsible for catching AbortExecReason exceptions and UserError exceptions and invoking the errorHandler contained in the state.

Run a single step of the Crucible symbolic simulator.

Retrieve the value of a register.

Evaluate the actual arguments for a function call or block transfer.

Evaluation operation for evaluating a single straight-line statement of the Crucible evaluator.

This is allowed to throw user exceptions or SimError.

Evaluation operation for evaluating a single block-terminator statement of the Crucible evaluator.

This is allowed to throw user exceptions or SimError.

Main evaluation operation for running a single step of basic block evaluation.

This is allowed to throw user exceptions or SimError.

An execution feature represents a computation that is allowed to intercept the processing of execution states to perform additional processing at each intermediate state. A list of execution features is accepted by executeCrucible. After each step of the simulator, the execution features are consulted, each in turn. After all the execution features have run, the main simulator code is executed to advance the simulator one step.

If an execution feature wishes to make changes to the execution state before further execution happens, the return value can be used to return a modified state. If this happens, the current stack of execution features is abandoned and a fresh step starts over immediately from the top of the execution features. In essence, each execution feature can preempt all following execution features and the main simulator loop. In other words, the main simulator only gets reached if every execution feature returns Nothing. It is important, therefore, that execution features make only a bounded number of modification in a row, or the main simulator loop will be starved out.

A generic execution feature is an execution feature that is agnostic to the execution environment, and is therefore polymorphic over the p, ext and rtp variables.

This feature will terminate the execution of a crucible simulator with a TimeoutResult after a given interval of wall-clock time has elapsed.