|0.2.0||Feb 25, 2021|
|0.1.0||Jun 5, 2020|
Isla is a symbolic execution engine for , as well as an anagram.
It can be used to evaluate the relaxed-memory behavior of instruction set architectures specified in Sail, using an axiomatic memory model specified in a subset of the cat language used by the herd7 tools. For example:
There is an online web interface here:
It can also be used for test generation, generating simplified semantics (summaries) for concrete opcodes, as well as many other possible use cases.
Currently tested with (stable) Rust 1.39:
cargo build --release
By default we require that z3 is
available as a shared library. On Ubuntu 20.04 LTS and above this
should be available by just running
apt install libz3-dev. However the
version of z3 that is available in older Ubuntu LTS versions (and
likely other linux distros) is quite old, so you may experience link
errors in that case. The build.rs script is configured so it can use a
libz3.so shared library placed in the root directory of this
repository. If this is done then
LD_LIBRARY_PATH must also be set when
executing so that the more recent z3 library is used.
Isla interprets IR produced by Sail. To generate this IR in the
correct format a tool is available in the isla-sail
directory. Building this requires various arcane OCaml incantations,
but mostly one can follow the Sail install guide
followed by the instructions here. It will only
work with the latest HEAD of the
sail2branch in the Sail repository.
For litmus tests in the
.litmus format used by
herd7 there is another OCaml
tool based on parsing code from herd7 itself in the isla-litmus
directory, which translates that format into a simple
TOML representation. This OCaml
program is standalone and does not depend on any libraries, and should
build with dune >= 1.2.
Isla executes IR produced by Sail. To avoid having to generate this IR, there are pre-compiled snapshots of our ISA models available in the following repository:
After compiling Isla, to compute the footprint of an add instruction using the aarch64 snapshot above, the following command can be used:
target/release/isla-footprint -A aarch64.ir -C configs/aarch64.toml -i "add x0, x1, #3" -s
The arguments are the compiled Sail model, a configuration file
controlling the initial state and other options, and the instruction
we want to run. The
-s flag performs some basic dead-code
elimination to simplify the generated footprint.
isla-lib Is a Rust library which contains the core symbolic execution engine and an API to interact with it.
isla-axiomatic Contains rust code to handle various aspects which are specific to checking axiomatic concurrency models on top of isla-lib, such as parsing litmus tests, analysing instruction footprints, and defining a high-level interface to run litmus tests.
isla-cat Is a translator from (a fragment of) the cat memory models used by herdtools into SMTLIB definitions. It has its own README here.
isla-litmus Is an (optional) OCaml utility that maps the
.litmusfiles that herdtools uses into a format we can read.
isla-sail Is an (optional) OCaml utility that maps Sail specifications into the IR we can symbolically execute.
web Contains a server and client for a web interface to the axiomatic concurrency tool
src Defines multiple small executable utilities based on isla-lib
This software was developed by the University of Cambridge Computer Laboratory (Department of Computer Science and Technology), in part under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), in part funded by EPSRC Programme Grant EP/K008528/1 "REMS: Rigorous Engineering for Mainstream Systems", in part funded from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 789108, "ELVER"), and in part funded by the UK Government’s Industrial Strategy Challenge Fund (ISCF) inder the Digital Security by Design (DSbD) Programme, to deliver a DSbDtech enabled digital platform, under Innovate UK grant 105694.