charon

Patinir、E.、1515-1524、 CharonがStyx [Oil on Wood]を越えた風景。マドリッドのデル・プラド博物館。ソース

チャロン

Charonは、RUSTCコンパイラとプログラム検証プロジェクトの間のインターフェースとして機能します。その目的は、錆びた木箱を処理し、プログラムの検証者によって簡単に処理できるファイルに変換することです。 RUSTCコンパイラのカスタムドライバーとして実装されています。

チャロンは、ギリシャ神話では、故人の魂を運ぶ老人であり、生計の世界を死者の世界から隔てる川を隔てる川です。現在の文脈では、チャロンは錆プログラムの世界から正式な検証の世界に行くことを許可しています。

私たちは貢献を受け入れています！あなたが喜んで貢献しているなら、私たちが自分自身を調整できるように私たちに連絡してください。この目的のために、Zulipに参加できます。

LLBC

CharonはMiRコードをUllBC（非構造化された低レベルの借用計算）に変換し、次にLLBCに変換します。両方のASTは、Charonによって出力できます。

ULLBCはわずかに単純化されたMIRであり、できるだけ多くの冗長性を除去しようとします。たとえば、Rustコンパイラから来る定数の表現を大幅に簡素化します。

LLBCはullbcでif ... then ... else ...コントロールフローをループで再構築しました。その結果、miRステートメントとターミネーターを単一のLLBCステートメントタイプに統合します。また、いくつかの追加の変更を実行しますが、その一部は以下にリストされています。

注：miRをullbcに変換する変換のほとんどは、マイクロパスによって実装されます。必要に応じて、それらをオプションにし、フラグで制御することができます。詳細について詳しく知りたい場合は、 src/driver.rsのtranslate参照してください。マイクロパスを次々と適用します。

注：（u）llbcの詳細を知りたい場合は、 types.rs 、 values.rs 、 expressions.rs 、 ullbc_ast.rs 、 llbc_ast.rsをご覧ください。

抽出されたASTは、 .ullbcおよび.llbcファイル（JSON形式を使用）でシリアル化されています。クレート全体を1つのファイルに抽出します。

プロジェクト構造

• charon ：錆の実装。
• charon-ml ：MLライブラリ。 OCAMLのASTを取得および操作するユーティリティを提供します（降下、印刷など）。
• testsとtests-polonius ：テストファイルディレクトリ。 tests-poloniusには、Polonius借入チェッカーが必要なコードが含まれています。

インストールとビルド

最初にrustupをインストールする必要があります。

Charonが貨物でセットアップされると、Rustupはプロジェクトの構築時に適切なパッケージを自動的にダウンロードしてインストールします。 Rustプロジェクト（ ./charon ）のみを構築したい場合は、単に上部ディレクトリにmake build-charon-rust実行するだけです。

MLライブラリ（ ./charon-ml ）も構築する場合は、OCAMLと適切な依存関係をインストールする必要があります。

これらの指示に従い、Opamを途中でインストールすることをお勧めします（同じ指示）。

Charon-MLの場合、 opam switch create 4.13.1+options 4.13.1を使用します。

依存関係は、次のコマンドでインストールできます。

 opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc menhir unionFind

その後、 make build-charon-mlを実行してMLライブラリを構築するか、単にプロジェクト全体（RustおよびOCAML）をmakeするだけでもできます。最後に、 make testでテストを実行できます。

または、Nixを使用してnix develop使用して（またはhttps://direnv.net/およびdirenv allow ）を使用することもできます。すべての依存関係を利用可能にする必要があります。

ドキュメント

オンラインでRustドキュメントにアクセスできます。

また、ドキュメントをローカルに生成するためにmakeすることもできます。 doc-rust.html （Rustプロジェクト用）およびdoc-ml.html （MLライブラリ用）からアクセス可能なドキュメントを生成します。

使用法

Charonを実行するには、 cargo buildで木枠を構築したいかのように、コンパイルしたい木枠内からCharonバイナリを実行する必要があります。 Charon実行可能ファイルはbin/charonにあります。

Charonは、木枠とその依存関係を構築し、ASTを抽出します。 Charonは、その動作を微調整するためにさまざまなオプションとフラグを提供します。- --helpで詳細なドキュメントを表示できます。特に、Charonによって生成されたLLBCを--print-llbcを印刷できます。

プロジェクトのルートにCharon.tomlファイルがある場合、Charonもそこからオプションを取得します。このファイルは、CLIインターフェイスで同じオプションをサポートしていますが、 --print-llbcなどの入力/出力に関連するオプションを除きます。例Charon.toml ：

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

注：CharonはNigthly（これはRUSTCドライバーを実装するための要件である）でコンパイルされているため、毎晩Rustで木枠を構築します。 rust-toolchain.templateでCharonにピン留めされた夜間バージョンを見つけることができます。