Isla

Isla是Sail指令集架构规范以及一个词谜游戏。

它可以使用由herd7工具使用的cat语言子集指定的公理内存模型来评估Sail中指定的指令集架构的放松内存行为。例如

这里有一个在线Web界面

https://isla-axiomatic.cl.cam.ac.uk

它还可以用于测试生成，为具体的操作码生成简化的语义（摘要），以及许多其他可能的用例。

构建

目前使用（稳定）Rust 1.39进行测试

cargo build --release

默认情况下，我们要求z3作为共享库可用。在Ubuntu 20.04 LTS及以上版本中，只需运行apt install libz3-dev即可。然而，在较旧的Ubuntu LTS版本（以及可能的其他Linux发行版）中可用的z3版本相当旧，因此您可能会遇到链接错误。build.rs脚本已配置为可以使用放在此存储库根目录中的libz3.so共享库。如果这样做，则在执行时也必须设置LD_LIBRARY_PATH，以便使用较新的z3库。

Isla解释由Sail生成的IR。要生成正确格式的IR，在isla-sail目录中有一个工具可用。构建此工具需要各种神秘的OCaml咒语，但主要可以遵循Sail安装指南在此处，然后遵循此处的说明。它只能与Sail存储库中sail2分支的最新HEAD一起使用。

对于使用herd7（https://github.com/herd/herdtools7）的.litmus格式的酸碱测试，在isla-litmus目录下有一个基于herd7本身解析代码的OCaml工具，它将此格式转换为简单的TOML表示。此OCaml程序是独立的，不依赖于任何库，并且应该使用dune >= 1.2构建。

模型快照

Isla执行Sail生成的IR。为了避免生成此IR，以下存储库中提供了我们ISA模型的预编译快照：

https://github.com/rems-project/isla-snapshots

示例

编译Isla后，要使用上面的aarch64快照计算加法指令的footprint，可以使用以下命令

target/release/isla-footprint -A aarch64.ir -C configs/aarch64.toml -i "add x0, x1, #3" -s

参数包括编译后的Sail模型、控制初始状态和其他选项的配置文件以及我们想要运行的指令。-s标志执行一些基本的死代码消除以简化生成的footprint。

项目结构

• isla-lib是一个Rust库，其中包含核心符号执行引擎以及与之交互的API。

• isla-axiomatic包含处理isla-lib上特定于检查算术并发模型的rust代码，例如解析litmus测试、分析指令footprint以及定义运行litmus测试的高级接口。

• isla-cat是将herdtools使用的（猫内存模型的一部分）转换为SMTLIB定义的翻译器。它有自己的README在这里。

• isla-litmus是一个（可选的）OCaml实用工具，将herdtools使用的.litmus文件映射为我们能读取的格式。

• isla-sail是一个（可选的）OCaml实用工具，将Sail规范映射为我们能符号执行的IR。

• web包含用于axiomatic并发工具的Web界面的服务器和客户端。

• src定义了基于isla-lib的多个小型可执行实用工具。

资金

此软件由剑桥大学计算机实验室（计算机科学与技术系）开发，部分由DARPA/AFRL合同FA8650-18-C-7809（“CIFV”）资助，部分由EPSRC项目资助EP/K008528/1“REMS：面向主流系统的严谨工程”，部分由欧洲研究委员会（ERC）根据欧盟的Horizon 2020研究和创新计划（协议号789108，“ELVER”）资助，部分由英国政府的工业战略挑战基金（ISCF）在数字安全设计（DSbD）计划下资助，以实现DSbDtech数字平台，根据Innovate UK赠款105694。