Crate isla_lib

Modules

cache
concrete
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
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
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.
type_check
value_parser
zencode

Macros

log
log_from
write_bits