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 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 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.