charon

Patinir，E.，1515-1524，景观与Charon越过Styx [木材上的油]。马德里博物馆Del Prado。来源

夏隆

Charon充当Rustc编译器和程序验证项目之间的接口。其目的是处理锈蚀箱，并将其转换为易于通过程序验证器处理的文件。它是作为Rustc编译器的自定义驱动程序实现的。

在希腊神话中，夏隆（Charon）是一个老人，载着死者的灵魂，使施特克斯（Styx）累积了一条河，将生活与死者世界分开。在当前的情况下，夏隆使我们可以从锈计划的世界转变为正式验证的世界。

我们愿意做出贡献！如果您愿意做出贡献，请与我们联系，以便我们可以协调自己。为此，您可以加入Zulip。

LLBC

Charon将mir代码转换为ULLBC（非结构化的低级借用微积分），然后转换为LLBC。两种AST可以通过Charon输出。

ULLBC是一个稍微简化的mir，我们尝试删除尽可能多的冗余。例如，我们大大简化了来自Rust编译器的常数的表示。

LLBC是ULLBC，我们在其中用循环重组控制流， if ... then ... else ...等。而不是gotos。因此，我们将mir语句和终止器合并到单个LLBC语句类型中。我们还执行一些其他修改，其中一些列出了下面：

备注：大多数转化miR到ULLBC然后LLBC的转换都是通过微型填充来实现的。根据需求，我们可以使它们可选并用标志控制它们。如果您想了解有关详细信息的更多信息，请参见src/driver.rs中的translate ，该transpate又一个又一个地应用了微型填充。

说明：如果您想知道（u）llbc的全部详细信息，请查看： types.rs ， values.rs ， expressions.rs ， ullbc_ast.rs和llbc_ast.rs 。

提取的AST在.ullbc和.llbc文件（使用JSON格式）中序列化。我们在一个文件中提取整个板条箱。

项目结构

• charon ：生锈实施。
• charon-ml ：ML库。提供实用程序来检索和操纵OCAML中的AST（避难，打印等）。
• tests和tests-polonius ：测试文件目录。 tests-polonius包含需要Polonius借用检查器的代码。

安装和构建

您首先需要安装rustup 。

随着Charon的货物设置，Rusup将在构建项目时自动下载并安装适当的软件包。如果您只想构建Rust Project（in ./charon ），则只需在顶级目录中运行make build-charon-rust 。

如果您还想构建ML库（in ./charon-ml ），则需要安装OCAML和适当的依赖项。

我们建议您遵循这些说明，并在途中安装OPAM（相同的说明）。

对于Charon-ML，我们使用OCAML 4.13.1 ： opam switch create 4.13.1+options

依赖项可以通过以下命令安装：

 opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc menhir unionFind

然后，您可以运行make build-charon-ml以构建ML库，甚至简单地make整个项目（Rust和Ocaml）。最后，您可以通过make test进行测试。

另外，您可以使用NIX并进行nix develop （或使用https://direnv.net/和direnv allow ），并且应提供所有依赖关系。

文档

您可以在线访问Rust文档。

您还可以运行以本地生成文档的make 。它将生成可从doc-rust.html （生锈项目）和doc-ml.html （用于ML库）访问的文档。

用法

要运行Charon，您应该从要编译的板条箱中运行Charon二进制文件，就好像您想用cargo build板条箱一样。 Charon可执行文件位于bin/charon 。

Charon将建立​​板条箱及其依赖关系，然后提取AST。 Charon提供了各种选项和标志来调整其行为：您可以使用--help显示详细的文档。特别是，您可以使用--print-llbc生成的Charon生成的LLBC。

如果您的项目根部有一个Charon.toml文件，则Charon还将从中获得选项。该文件在CLI接口上支持相同的选项，除了与输入/输出（如--print-llbc相关的选项。示例Charon.toml ：

[ charon ]
extract_opaque_bodies = true
[ rustc ]
flags = [ " --cfg " , " abc " ]

备注：由于Charon是用Rust Nigthly编译的（这是实施Rustc驾驶员的必要条件），所以它将用Rust Nightly构建您的板条箱。您可以在rust-toolchain.template中找到为Charon固定的​​夜间版本。