[−][src]Module isla_lib::executor

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.

all_unsat_collector	This `Collector` is used for boolean Sail functions. It returns true via the mutex 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.
trace_collector
trace_result_collector
unfreeze_frame

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, protected by a lock.
TraceQueue
TraceResultQueue