[−][src]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 |