Prustiを使ってRustでプログラム検証をしよう

導入に際し、ドキュメントに書いてないこととか色々あってつらかったため、軽くメモ代わりに投稿しておきます。
また、Prusti を使う最も簡単な方法は VSCode の拡張である Prusti-Assistant を使うことですが、Vimの使用を見越しコマンドだけで使えるようにアレコレ設定しました。

Prusti の紹介

プログラミングにおいて、関数に対してプログラマが明示的に制約を課すことはよくあります。
例えば、次のような単純な関数 max を考えます。

fn max(x: i32, y: i32) -> i32 {
    let result = if x > y { x } else { y };

    result
}

さて、この関数は次のような性質を持つことが期待されます。

• resultはx以上かつy以上
• resultはxまたはy

そういった情報は多くの場合ライブラリのドキュメントなどに書いてあることが多いと思いますが、Prusti では、そういった関数の情報をコードで表現できます。

extern crate prusti_contracts;
use prusti_contracts::*;

#[ensures(result == x || result == y)]
#[ensures(result >= x && result >= y)]
fn max(x: i32, y: i32) -> i32 {
    if x > y {
        x
    } else {
        y
    }
}

コードを見ればおおよその予想はつくと思いますが、ensures という属性に期待される関数の性質を記述できます。(resultというのは返り値で、暗黙に使用できます。)

これだけでは、ただコードにコメントを書くのと変わらず、何が嬉しいのかよくわかりません。そこで、max 関数を次のように変更してみます。

#[ensures(result == x || result == y)]
#[ensures(result >= x && result >= y)]
fn max(x: i32, y: i32) -> i32 {
    if x > y {
        y // 入れ替えた
    } else {
        x // 
    }
}

これは実装ミスですね。maxを実装するつもりが、小さい方の値を返しています。ここで Prusti が活躍します。このコードを Prusti のツールで検証すると、次のようなエラーが出てコンパイルできません。

error: [Prusti: verification error] postcondition might not hold.
  --> src/lib.rs:4:11
   |
4  | #[ensures(result == x || result == y)]
   |           ^^^^^^^^^^^^^^^^^^^^^^^^^^
5  | #[ensures(result >= x && result >= y)]
   |           ^^^^^^^^^^^^^^^^^^^^^^^^^^
   |

このように、Prusti は渡されたプログラムが本当に条件を満たしているか検証してくれるのです。
ちなみに、Prusti 内部では Rust プログラムを Viper というバックエンド用の中間表現に変換し、最後に z3 という高速な SMT ソルバを使っています。

max 関数のような単純な例だけでなく、ヒープを使ったリストといったデータ構造にも、多少不安定ですが使えます。

導入

Prusti の Developer Guide に大体まとまっていますが、いくつか落とし穴があるので進めていきます。

Java11 を導入した状態で、prusti-dev リポジトリを手元に clone し、setup と build をします。

git clone https://github.com/viperproject/prusti-dev
cd prusti-dev

./x.py setup # Viper 関連のツールが viper_tools に入る。z3等もここ
./x.py build --release

ここで、build の途中で失敗する場合は JAVA_HOME の設定ができていない可能性があります。archlinuxの場合、次のように設定するとうまく行くと思います。

export JAVA_HOME=/usr/lib/jvm/default-runtime

/usr/lib/jvm/default-runtime の下には bin や lib があり、他のディストリビューションでも同じような場所を設定すればいいと思います。

ビルドが終わると、target/release 下に実行ファイルができます。その中の prusti-driver を試しに実行してみてください。
libjvm.so がなくて実行できないと表示される場合は、$JAVA_HOME/lib/server 下に libjvm.so があるので、そこを LD_LIBRARY_PATH に追加するか、patchelf 等で編集してください。前者をおすすめします。

また、librustc_driver-e70f935d0865b673.so が見つからない場合は(ハッシュは多分ランダム)、rustup component 内の rustc-dev か rustc が壊れている可能性があります。
面倒な場合は、 rustup self uninstall して入れ直すと症状が改善することがあります。~/.cargo や ~/.rustup が消えるため、バックアップを取ると良いです。

正常にビルドが成功したあとは、リポジトリ内で次のコマンドを実行してください。

ln -s $(pwd)/viper_tools $(pwd)/target/release/
ln -s $(pwd)/rust-toolchain $(pwd)/target/release/

最後に、target/release を PATH に追加すれば導入完了です。ビルド成果物内に PATH を通すのが嫌な方は、適当なディレクトリに実行ファイルをコピーし、同様に symlink を張れば、多分大丈夫です。

使い方

基本的に、prusti-server-driver がサーバーを立ち上げます。
次に、cargo-prusti がプロジェクト内から検証すべき問題を抽出してサーバーへ投げ、帰ってきた結果を整形して表示します。

まずサーバーを立ち上げます。後述する方法を使えば、一応このステップを省略できます。

Z3_EXE=/foo/bar/z3/bin/z3 BOOGIE_PATH=/foo/bar/Boogie/Binaries/Boogie prusti-server-driver --port=12345

Z3_EXE と BOOGIE に関しては、viper_tools 内に実行ファイルがあるため、それを指定してください。
ポートは何でもいいです。0を指定するとランダムなポートで Listen してくれます。

次に cargo-prusti を使えるようにします。
いつも通り cargo new して、src/main.rs に次のように記述します。

extern crate prusti_contracts;
use prusti_contracts::*;

#[ensures(result == x || result == y)]
#[ensures(result >= x && result >= y)]
fn max(x: i32, y: i32) -> i32 {
    if x > y {
        x
    } else {
        y
    }
}

ここで使われている prusti_contracts のために、Cargo.toml に次を追加します。

[dependencies]

[dependencies.prusti-contracts]
path = "/foo/bar/prusti-dev/prusti-contracts/prusti-contracts"

[features]
prusti = ["prusti-contracts/prusti"]

ここで、prusti-contracts の path には、clone した prusti-dev を使います。内部にある prusti-contracts に合うように指定してください。

最後に、cargo-prusti を使ってプログラムの検証を行います。次のコマンドを実行してください。

PRUSTI_SERVER_ADDRESS=localhost:12345 cargo-prusti --features=prusti

prusti-server-driver の方にログが出て、cargo-prusti が正常に終了したら検証完了です。
返り値のxとyを入れ替え、実装ミスを埋め込んだバージョンでもちゃんと失敗することを確認してください。

失敗例 1: 条件が無視される

ミスがあるにも関わらず検証が成功してしまう場合は、features の設定が正常でない可能性があります。
prusti-contracts 内の features、prusti を有効にしないと #[ensure()]　や prusti_assert!() がすべて無視されます。
その場合、assert! 等は無視されずチェックされるので、うまく動かない方は次のようなコードを試してください。

fn test() {
    let x = 2;
    assert!(x == 3);
}

正常に失敗する場合は、Cargo.toml 内にミスがあると思われます。

失敗例 2: サーバーが 'please set the smt_solver_path configuration flag' と言い残してパニックする

Z3_EXE が正常でないと思われます。
ちゃんと実行ファイルの場所を指定しているか確認してみてください。

失敗例 3: unimplement! とか出る。

error: [Prusti: verification error] statement might panic
   --> /foo/bar/prusti-dev/prusti-contracts/prusti-contracts/src/lib.rs:395:5
    |
395 |     unimplemented!()
    |     ^^^^^^^^^^^^^^^^
    |
    = note: this error originates in the macro `unimplemented` (in Nightly builds, run with -Z macro-backtrace for more info)

これも失敗例1 と同様に、features の設定が正常でないと思われます。

prusti-contracts は 内部に prusti-contracts-impl と prusti-contracts-internal という２つの crate を持っています。
prusti-contracts-impl は proc-macro で、ensures などのマクロがあります。それらは受け取った TokenStream をそのまま返し、prusti-contracts-internal の方は prusti 用に色々な処理をしているみたいです。
これを prusti という features によって切り替えることで、普通に cargo build するときは何もしないのだと思われます。

この失敗例はおそらくバグですが、内部で切り替えがうまく行われていないため失敗しています。

失敗例 4: --json の指定でコンパイルエラーが出る。

prusti のバージョンが古いためだと思われます。
prusti-rustc --version と rustc --version を実行し、一致しているか確認してください。

一致していない場合は、./x.py setup が正常に終了していなかった可能性があります。

失敗例 5: failed to resolve: use of undeclared crate or module prusti

Cargo.toml の prusti-contracts を git = "https://github.com/viperproject/prusti-dev.git" と指定する。もしくは、cargo build --features=prusti とした時に発生します。

前者はよくわかりませんが、後者の場合は、通常のビルドで prusti を指定しないようにすることで回避できます。
筆者もよくわかっていないので、フラグの指定とかせずに回避する方法があれば教えていただきたいです。

失敗例 6: failed to run rustc to learn about target-specific information

クラッシュして、内部で undefined symbol: _ZN9hashbrown3raw11Fallibility17capacity_overflow17h52b24f50adb3934dE みたいなやつが出るパターンです。

これは prusti-rustc 内部で使われている rustc-driver の動的ライブラリと、ビルド時に参考にしたライブラリがずれています。
例えば、rustup default nightly としているおり、かつ prusti のビルドにそれ以下のバージョンの toolchain を使用したときに発生します。

この場合は、rust-toolchain を作り、作成時のバージョンを指定するとうまく動きます。つまり、

cp /foo/bar/prusti-dev/rust-toolchain ./

とすれば良いはずです。

Q&A 1: 毎回サーバーを起動するのが面倒なんだけど

基本的にサーバーを使ったほうが、検証キャッシュとかがいい感じらしくておすすめですが、面倒な方は RPUSTI_SERVER_ADDRESS を MOCK にすると内部でサーバーが立ち上がって自動的に使ってくれます。

Q&A 2: 環境変数が多すぎてわからん

List of Configuration Flags にまとまっています。
言及したもの以外にも、バックエンドをCarbonに変えたり、SMTソルバを変更したりできます。

Q&A 3: 試してみたけど、算術オーバーフローとかまで検出されてうざい

Prusti.toml というファイルをプロジェクト内に作ると、その設定を参考に検証をしてくれます。
例えば、

check_overflows=false

とすると、オーバーフローチェックを無効にできます。

終わりに

検証楽しい！ｗ

間違えや誤字・脱字、質問等あればお気軽にコメントをお願いします。

もしくは僕の Twitter でもOKです。