Module isla_lib::smt

This module defines an interface with the SMT solver, primarily via the Solver type. It provides a safe abstraction over the z3_sys crate. In addition, all the interaction with the SMT solver is logged as a Trace in an SMTLIB-like format, expanded with additional events marking e.g. memory events, the start and end of processor cycles, etc (see the Event type). Points in these traces can be snapshotted and shared between threads via the Checkpoint type.

Modules

smtlib

This module defines a subset of the SMTLIB format we use to interact with the SMT solver, which mostly corresponds to the theory of quantifier-free bitvectors and arrays.

Structs

Checkpoint	Snapshot of interaction with underlying solver that can be efficiently cloned and shared between threads.
Config	Config is a wrapper around the Z3_config type from the C API. Z3_del_config is called when it is dropped.
Context	Context is a wrapper around Z3_context.
Model	Interface for extracting information from Z3 models.
Solver	The Solver type handles all interaction with Z3. It mimics interacting with Z3 via the subset of the SMTLIB 2.0 format we care about.
Sym	A newtype wrapper for symbolic variables, which are u32 under the hood.
Trace	Abstractly represents a sequence of events in such a way that checkpoints can be created and shared.

Enums

Accessor	For the concurrency models, register accesses must be logged at a subfield level granularity (e.g. for PSTATE in ARM ASL), which is what the Accessor type is for.
Event
SmtResult

Functions

checkpoint
finalize_solver⚠	This function just calls Z3_finalize_memory(). It’s useful because by calling it before we exit, we can check whether we are leaking memory while interacting with Z3 objects.
global_set_param_value

Type Definitions

EvPath