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固定的​​夜間版本。