This class provides operations that interact with the symbolic simulator. It allows for logical assumptions/assertions to be added to the current path condition, and allows queries to be asked about branch conditions.

The bak type contains all the datastructures necessary to maintain the current program path conditions, and keep track of assumptions and assertions made during program execution. The sym type is expected to satisfy the IsSymInterface constraints, which provide access to the What4 expression language. A sym is uniquely determined by a bak.

Note [Pushes and pops]

This class provides methods for pushing (pushAssumptionFrame) and popping (popAssumptionFrame, popUntilAssumptionFrame, popAssumptionFrameAndObligations) frames. Pushes and pops must be well-bracketed. In particular, popAssumptionFrame* are required to throw an exception if the provided frame identifier does not match the top of the stack.

It is relatively easy to end up with ill-bracketed pushes and pops in the presence of exceptions. When diagnosing such issues, consider popping frames using methods such as try.

Class for backend type that can retrieve sym values.

This is separate from IsSymBackend specifically to avoid the need for additional class constraints on the backendGetSym operation, which is occasionally useful.

Add a proof obligation using the current program location. Afterwards, assume the given fact.

If an assumption is clearly impossible, return an abort reason that can be used to unwind the execution of this branch.

This type describes assumptions made at some point during program execution.

This type describes events we can track during program execution.

This type tracks both logical assumptions and program events that are relevant when evaluating proof obligations arising from simulation.

Given a ground evaluation function, compute a linear, ground-valued sequence of events corresponding to this program run.

Pretty print an event

Check if an assumption is trivial (always true)

Return the program location associated with an assumption

Return the program location associated with an event

Merge the assumptions collected from the branches of a conditional.

Get the predicate associated with this assumption

Compute the logical predicate corresponding to this collection of assumptions.

Given a CrucibleAssumptions structure, flatten all the muxed assumptions into a flat sequence of assumptions that have been appropriately weakened. Note, once these assumptions have been flattened, their order might no longer strictly correspond to any concrete program run.

Collect the program locations of all assumptions and events that did not occur in the context of a symbolic branch. These are locations that every program path represented by this CrucibleAssumptions structure must have passed through.

Information about an assertion that was previously made.

Predicate that was asserted.

Message added when assumption/assertion was made.

An assumption stack is a data structure for tracking logical assumptions and proof obligations. Assumptions can be added to the current stack frame, and stack frames may be pushed (to remember a previous state) or popped to restore a previous state.

A FrameIdentifier is a value that identifies an an assumption frame. These are expected to be unique when a new frame is pushed onto the stack. This is primarily a debugging aid, to ensure that stack management remains well-bracketed.

A proof goal consists of a collection of assumptions that were in scope when an assertion was made, together with the given assertion.

A collection of goals, which can represent shared assumptions.

Render the tree of goals as a list instead, duplicating shared assumptions over each goal as necessary.

This is used to signal that current execution path is infeasible.

Throw an exception, thus aborting the current execution path.

Add a proof obligation for the given predicate, and then assume it (when the assertThenAssume option is true). Note that assuming the prediate might cause the current execution path to abort, if we happened to assume something that is obviously false.

Add a durable proof obligation for the given predicate, and then assume it (when the assertThenAssume option is true). Note that assuming the prediate might cause the current execution path to abort, if we happened to assume something that is obviously false.

Run the given action to compute a predicate, and assert it.

Add a proof obligation for False. This always aborts execution of the current path, because after asserting false, we get to assume it, and so there is no need to check anything after. This is why the resulting IO computation can have the fully polymorphic type.

Assert that the given real-valued expression is an integer.

Given a partial expression, assert that it is defined and return the underlying value.

Run the CHC solver on the current proof obligations, and return the solution as a substitution from the uninterpreted functions to their definitions.

Get proof obligations as What4 implications.

Convert proof obligations to What4 implications.

Get the set of uninterpreted constants that appear in the proof obligations.

Get the set of uninterpreted constants that appear in the path condition.