Monad for running symbolic simulator.

Type parameters:

• p see cruciblePersonality
• sym the symbolic backend
• ext the syntax extension (Lang.Crucible.CFG.Extension)
• rtp global return type
• args argument types for the current frame
• ret return type of the current frame
• a the value type

Turn an OverrideSim action into an ExecCont that can be executed using standard Crucible execution primitives like executeCrucible.

Associate a definition (either an Override or a CFG) with the given handle.

Bind a CFG to its handle.

Computes postdominator information.

Exit from the current execution by ignoring the continuation and immediately returning an aborted execution result.

Return override arguments.

Add a failed assertion. This aborts execution along the current evaluation path, and adds a proof obligation ensuring that we can't get here in the first place.

Abort the current thread of execution for the given reason. Unlike overrideError, this operation will not add proof obligation, even if the given abort reason is due to an assertion failure. Use overrideError instead if a proof obligation should be generated.

Perform a symbolic branch on the given predicate. If we can determine that the predicate must be either true or false, we will exeucte only the "then" or the "else" branch. Otherwise, both branches will be executed and the results merged when a value is returned from the override. NOTE! this means the code following this symbolic branch may be executed more than once; in particular, side effects may happen more than once.

In order to ensure that pushabortmux bookeeping is done properly, all symbolic values that will be used in the branches should be inserted into the RegMap argument of this function, and retrieved in the branches using the getOverrideArgs function. Otherwise mux errors may later occur, which will be very confusing. In other words, don't directly use symbolic values computed before calling this function; you must instead first put them into the RegMap and get them out again later.

Perform a series of symbolic branches. This operation will evaluate a series of branches, one for each element of the list. The semantics of this construct is that the predicates are evaluated in order, until the first one that evaluates true; this branch will be the taken branch. In other words, this operates like a chain of if-then-else statements; later branches assume that earlier branches were not taken.

If no predicate is true, the construct will abort with a VariantOptionsExhausted reason. If you wish to report an error condition instead, you should add a final default case with a true predicate that calls overrideError. As with symbolicBranch, be aware that code following this operation may be called several times, and side effects may occur more than once.

As with symbolicBranch, any symbolic values needed by the branches should be placed into the RegMap argument and retrieved when needed. See the comment on symbolicBranch.

Non-deterministically choose among several feasible branches.

Unlike symbolicBranches, this function does not take only the first branch with a predicate that evaluates to true; instead it takes all branches with predicates that are not syntactically false (or cannot be proved unreachable with path satisfiability checking, if enabled). Each branch will not assume that other branches weren't taken.

As with symbolicBranch, any symbolic values needed by the branches should be placed into the RegMap argument and retrieved when needed. See the comment on symbolicBranch.

Operationally, this works by by numbering all of the branches from 0 to n, inventing a symbolic integer variable z, and adding z = i (where i ranges from 0 to n) to the branch condition for each branch, and calling symbolicBranches on the result. Even though each branch given to symbolicBranches assumes earlier branches are not taken, each branch condition has the form (z = i) and p, so the negation ~((z = i) and p) is equivalent to (z != i) or ~p, so later branches don't assume the negation of the branch condition of earlier branches (i.e., ~p).

Call a function with the given arguments.

Call a function with the given arguments. Provide the arguments as an Assignment instead of as a RegMap.

Call a control flow graph from OverrideSim.

Note that this computes the postdominator information, so there is some performance overhead in the call.

Call a block of a control flow graph from OverrideSim.

Note that this computes the postdominator information, so there is some performance overhead in the call.

Call an override in a new call frame.

Read a particular global variable from the global variable state.

Set the value of a particular global variable.

Read the whole sym global state.

Overwrite the whole sym global state

Run an action to compute the new value of a global.

Create a new reference cell.

Create a new reference cell with no contents.

Read the current value of a reference cell.

Write a value into a reference cell.

Read the current value of a mux tree of reference cells.

Write a value into a mux tree of reference cells.

A pair containing a handle and the state associated to execute it.

Build a map of function bindings from a list of handle/binding pairs.

This quantifies over function bindings that can work for any symbolic interface.

Create an override from a statically inferrable return type and definition using OverrideSim.

Create an override from an explicit return type and definition using OverrideSim.

Make an IntrinsicImpl from an explicit implementation

An action in OverrideSim, together with TypeReprs for its arguments and return values. This type is used across several frontends to define overrides for built-in functions, e.g., malloc in the LLVM frontend.

For maximal reusability, frontends may define TypedOverrides that are polymorphic in (any of) p, sym, and ext.

Create a TypedOverride with a statically-known signature

A TypedOverride with the type parameters args, ret existentially quantified

Create an override from a TypedOverride.

Bind a TypedOverride to a FnHandle

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