Crate isla_lib

Modules

bitvector	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.
cache
config	This module loads a TOML file containing configuration for a specific instruction set architecture.
error
executor	This module implements the core of the symbolic execution engine.
init	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.
ir	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.
ir_lexer
ir_parser
lexer
log
memory	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.
primop	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.
simplify	This module implements various routines for simplifying event traces, as well as printing the generated traces.
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.
value_parser
zencode	This module implements the name mangling scheme used by Sail

Macros

if_logging
log
log_from
write_bits