This module defines the bitvector trait BV, and includes modules for concrete bitvectors of up to 64-bits, or up to 129-bits. The 129-bit bitvectors are intended for CHERI architectures as it allows capabilities to be represented without involving the SMT solver. Most functions in isla-lib, and dependent libraries will be parametric over the BV trait.
This module loads a TOML file containing configuration for a specific instruction set architecture.
This module implements the core of the symbolic execution engine.
This module defines a function to initialize a Sail architecture specification. The function initialize_architecture takes a mutable reference to some parsed IR with it’s symbols interned into a Symtab, and produces a SharedState struct, along with Bindings environments for both the registers and the global let bindings.
This module defines and implements functions for working with the Jib IR (intermediate representation) that is produced by Sail. It is a simple goto/conditional branch language, where each function can declare and use an arbitrary amount of variables.
The memory is split up into various regions defined by a half-open range between two addresses [base, top). This is done because we want to give different semantics to various parts of memory, e.g. program memory should be concrete, whereas the memory used for loads and stores in litmus tests need to be totally symbolic so the bevhaior can be imposed later as part of the concurrency model.
This module is a big set of primitive operations and builtins which are implemented over the crate::ir::Val type. Most are not exported directly but instead are exposed via the Primops struct which contains all the primops. During initialization (via the crate::init module) textual references to primops in the IR are replaced with direct function pointers to their implementation in this module. The Unary, Binary, and Variadic types are function pointers to unary, binary, and other primops, which are contained within Primops.
This module implements various routines for simplifying event traces, as well as printing the generated traces.
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.
This module implements the name mangling scheme used by Sail