Miri未定義動作 (UB: Undefined Behavior) の検出ツールである。
unsafe を含むコードの検証やその健全性の確認に使われる。

現状と必要性

、Miri はまだ実験段階のため、ナイトリー版でのみ動作する。

とはいえ、unsafe なコードを扱う場合、筆者はこのツールはほぼ必須だと考えている。

なぜなら、未定義動作にはエラーの発生有無が偶然に左右される物があり、見逃されやすい。また、Rust のバージョンアップなどで最適化方法が変更されると、その影響を受ける可能性もある。Miri はこれらの問題の対策となる。

実行方法

それぞれ以下のコマンドから実行できる。

インストール


> rustup +nightly component add miri

バイナリの実行


> cargo +nightly miri run

テストの実行


> cargo +nightly miri test

注意点

偽陽性なし

エラーがあればそれは何らかの未定義動作がある事を示している。

ただし、の重要な点として、後述のモデルによる差異がある。

偽陰性あり

ツールの性質上、偽陰性は避けられない。

なぜなら、UB になるパターンがテストされていないだけの可能性は常にある。

モデル

、Rust のエイリアシングルールは unsafe まわりにまだ曖昧さがある。

これに対して、Miri は二つのモデル Stacked BorrowsTree Borrows を用意している。どちらでもメモリ安全性は守られるが、後者は制限がより少ない。現在の既定は前者だが、将来的には後者が有力である。後者に切り替える場合、環境変数 MIRIFLAGS-Zmiri-tree-borrows を指定するとよい。

ちなみに、将来的に Stacked Borrows より Tree Borrows が有力とする根拠は、前者が現状の多くのクレートの実情にそぐわないからである (参考: arraydeque での実例)。

事例集