Module executor

Expand description

This module implements the core of the symbolic execution engine.

Structs§

Frame: A Frame is an immutable snapshot of the program state while it is being symbolically executed.
LocalFrame: A LocalFrame is a mutable frame which is used by a currently executing thread. It is turned into an immutable Frame when the control flow forks on a choice, which can be shared by threads.
Task: A Task is a suspended point in the symbolic execution of a program. It consists of a frame, which is a snapshot of the program variables, a checkpoint which allows us to reconstruct the SMT solver state, and finally an option SMTLIB definiton which is added to the solver state when the task is resumed.
TaskState

all_unsat_collector: This Collector is used for boolean Sail functions. It returns true via an AtomicBool if all reachable paths through the program are unsatisfiable, which implies that the function always returns true.
footprint_collector
freeze_frame
start_multi: Start symbolically executing a Task across num_threads new threads, collecting the results using the given collector.
start_single: Start symbolically executing a Task using just the current thread, collecting the results using the given collector.
symbolic: Create a Symbolic value of a specified type. Can return a concrete value if the type only permits a single value, such as for the unit type or the zero-length bitvector type (which is ideal because SMT solvers don’t allow zero-length bitvectors). Compound types like structs will be a concrete structure with symbolic values for each field. Returns the NoSymbolicType error if the type cannot be represented in the SMT solver.
trace_collector
trace_result_collector
trace_value_collector
unfreeze_frame

Backtrace
Collector: A collector is run on the result of each path found via symbolic execution through the code. It takes the result of the execution, which is either a combination of the return value and local state at the end of the execution or an error, as well as the shared state and the SMT solver state associated with that execution. It build a final result for all the executions by collecting the results into a type R.
TraceQueue
TraceResultQueue
TraceValueQueue