AeneasVerif/charon

# Charon Charon（发音为“Ka-ron”）将 Rust crate（及其依赖项）的完整内容提取到一个 JSON 文件中： ``` { "crate_name": "...", "type_decls": [ ... ], "fun_decls": [ ... ], "global_decls": [ ... ], "trait_decls": [ ... ], "trait_impls": [ ... ], } ``` 输出包含 crate 及其依赖项的类型、函数和 trait，简化的 MIR 函数体，每个 item 的源码信息，以及下文描述的其他语义信息。 我们**欢迎贡献**！如果您愿意做出贡献，请与我们联系以便协调。讨论在 [Zulip](https://aeneas-verif.zulipchat.com/) 上进行。 ## 用法 在目标 crate 中运行 `charon`，就像调用 `cargo build` 一样。它会生成一个 `crate_name.llbc` 文件。 `charon-lib` crate 可以读取此文件并让您操作其内容。使用 `serde_json::from_reader::(file)` 来解析文件。`charon-ml` 文件夹中也提供了 OCaml 绑定。 有关更详细的用法说明，请参阅[文档](./docs/usage.md)。 ## 为什么选择 Charon？ Charon 的输出看起来很简单，但构建相关信息却很困难。Charon 的目的是集中力量从 rustc 内部提取信息，并将其转化为统一且可用的形式。请参阅[文档](./docs/what_charon_does_for_you.md)以概述 Charon 目前必须完成的工作。 如果您正在编写 rustc driver，您很可能可以改用 Charon。然而，Charon 倾向于语义分析；对于像许多 lint 这样的语法分析，它可能无能为力。 在希腊神话中，Charon 是一位老人，负责将死者的灵魂运过分隔生者与死者世界的河流——冥河。在当前语境下，Charon 让我们能够跨越编译器内部机制的河流，从 Rust 程序的世界走向代码分析和验证的世界。 ## 限制 Charon 是 alpha 软件。虽然它在大量 crate 中运行良好，但它尚未达到我们预期的完整功能集，在某些边缘情况下会错误地翻译代码，并且计划在其 API 中进行大量破坏性更改。有关详细信息，请参阅[限制](./docs/limitations.md)。 ## 安装与构建 如果您使用 nix，可以直接运行 `nix run github:AeneasVerif/charon`。否则，请继续阅读。 您首先需要安装 [`rustup`](https://www.rust-lang.org/tools/install) 并卸载系统中先前安装的任何 `rust` 或 `cargo` 包（例如通过 `brew` 安装的），因为它们有时会与 `rustup` 冲突。 由于 Charon 是使用 cargo 设置的，因此在构建项目时，rustup 会自动下载并安装相应的包。如果您只想构建 Rust 项目（位于 `./charon` 中），请在根目录中运行 `make build-charon-rust`。生成的 `charon` 二进制文件可以在 `bin/charon` 中找到，您可以从那里使用它。 如果您还想构建 ML 库（位于 `./charon-ml` 中），您将需要安装 OCaml 和适当的依赖项。 我们建议您遵循这些[说明](https://ocaml.org/docs/install.html)，并在此过程中安装 OPAM（相同的说明）。 对于 Charon-ML，我们使用 **OCaml 4.14.0**（`opam switch create 4.14.0+options`），但任何最新版本都可以。特别是，**OCaml 5** 也能正常工作。 可以使用 `opam install . --deps-only` 安装依赖项。 然后您可以运行 `make build-charon-ml` 来构建 ML 库，甚至直接运行 `make` 来构建整个项目（Rust 和 OCaml）。最后，您可以使用 `make test` 运行测试。 或者，您可以使用 Nix 并执行 `nix develop`，所有依赖项都应该会自动可用。 ## 文档 您可以访问（正在开发中的）Rust 文档[在线版](https://aeneasverif.github.io/charon/charon_lib/index.html)。 您也可以运行 `make doc` 以在本地生成文档。 它将生成可从 [`doc-rust.html`](./doc-rust.html)（针对 Rust 项目）和 [`doc-ml.html`](./doc-ml.html)（针对 ML 库）访问的文档。

标签：AST提取, LLBC, Rust, 代码分析, 凭证管理, 可视化界面, 形式化验证, 漏洞数据库, 编译器前端, 网络流量审计, 通知系统