Rustverif

目的

• Verusやframa-cと同等の機能を持つ検証機を作成する
  • 事前条件
  • 事後条件
  • ループ普遍条件

処理フロー(過去)

1. 検証対象となるRustのソースコードファイルをコマンドライン引数として受け取る。
2. rustc_driverのrun_compilerを呼び出し、Callbackを登録してコンパイル処理を開始する。
3. コンパイラの解析後、after_analysisコールバック内で型情報コンテキスト(TyCtxt)を取得する。
4. TyCtxtを用いて、プログラムのエントリーポイントであるmain関数のDefId（定義ID）を特定する。
5. main関数のDefIdを基に、TyCtxtから型付き高水準中間表現（THIR）を取得する。
6. THIRから検証に不要な情報を削ぎ落とし、独自の中間表現（RTHIR）へと変換する。
7. RTHIRからmain関数の本体（Body）を抽出し、シンボリック実行を開始する。
8. 関数の本体に含まれる文(stmts)と式(expr)を先頭から順に評価し、プログラムの状態を論理的な中間表現（LIR）としてモデル化する。
9. シンボリック実行によって構築された論理式（LIR）を、SMT-LIB 2形式のテキストに変換する。
10. 生成したSMT-LIB 2クエリを、Z3(SMTソルバ)に入力として渡す。
11. Z3の証明結果を出力する。

処理フロー(現在)

1. 検証対象となるRustのソースコードファイルをコマンドライン引数として受け取る。
2. rustc_driverのrun_compilerを呼び出し、Callbackを登録してコンパイル処理を開始する。
3. コンパイラの解析後、after_analysisコールバック内で型情報コンテキスト(TyCtxt)を取得する。
4. TyCtxtを用いて、プログラムのエントリーポイントであるmain関数のDefId（定義ID）を特定する。
5. main関数のDefIdを基に、TyCtxtから型付き高水準中間表現（THIR）を取得する。
6. THIRから検証に不要な情報を削ぎ落とし、独自の中間表現（RTHIR）へと変換する。
7. RTHIRからmain関数の本体（Body）を抽出
8. Bodyからアノテーションやpureな関数を抽出
9. CHCに変換しそれをSMT-LIB 2クエリに変換
10. 生成したSMT-LIB 2クエリを、Z3(SMTソルバ)に入力として渡す。
11. Z3の証明結果を出力する。

最終目標

以下の関数プログラムを検証

fn seven(n: i64) -> i64 
// todo
// require: n <= i64::MAX - 3
// ensure: n == 7
{
if n <= 4 { n + 3 } else { seven(seven(n - 4)) }
}
fn main() {
    assert!(seven(42) == 7);
}