Rust で預言を使ったプログラム検証器を自作しよう 1/3
この記事は筆者がセキュリティ・キャンプ全国大会 2024 にて作成したプログラム検証器を元に作成しました。
記事は全部で3回まであります。
各回へはこちらからどうぞ。
各回のリンク
- 第1回: Rust で預言を使ったプログラム検証器を自作しよう 1/3
- 第2回: Rust で預言を使ったプログラム検証器を自作しよう 2/3
- 第3回: Rust で預言を使ったプログラム検証器を自作しよう 3/3
この記事の目的
この記事は、プログラム検証器自作に関する情報が少なすぎる現状を改善し、初学者がより楽に基本的な機能を持つ検証器を完成させ、より早く各々がサポートしたい機能の追加のフェーズに入れるようにすることを目的としています。
全3記事で作成します。今回は、検証器の説明とそれに用いる中間表現の生成、検証器の実行まで行います。
また、この記事は“このやり方で検証機を作成しよう”というものではなく、検証器完成までのタスクを紹介することを目的として作成されています。そのタスクをどう解決するか、それぞれのタスクをどう繋ぎ合わせるかは、自分の趣味に合わせてください。基本的に処理をそのまま載せているので、関数に分けるなども自分のやり方に合わせてください。
しかし、作成する検証器の元となるプログラムはGitHubのリポジトリ(使用している toolchain は"nightly-2024-06-18")にありますので、困った場合には、そちらをご参照ください。
また検証器では、Microsoft が提供している SAT ソルバ Z3 を使用します。リポジトリからインストール方法を確認してインストールしておいてください。
プログラム検証器とは
一応内容に入る前に、簡単にプログラム検証器とは何か説明します。
ソフトウェアには仕様があり、それぞれのソフトウェアには想定された正しい動作というものがあります。開発者がそのソフトウェアを実装した時に、仕様に沿っているのか逆に仕様以外の動作をする可能性はないのかという、その"プログラムの正しさ"を数学的に証明することをプログラム検証といい、それをシステム的に実行するソフトウェアをプログラム検証器と呼びます。
詳しく書く記事も書きたいかも。
この記事のゴール
この記事では、次のような"変数の宣言"、"アサイン"、"If"、"関数呼び出し"、"関数の戻り値"、"可変借用"の要素と main 関数を必ず含む Rust プログラムを検証できる検証器の作成をゴールとしています。
記事としては次の全 3 回に分かれ、今回はその第 1 回となります。
- 第1回: 短いコードを実際に Z3 を呼び出し検証するまで。
- 第2回: 関数呼び出し、if 文が含まれるコードの検証
- 第3回: 預言を用いた可変借用の検証
extern crate t3modules;
use t3modules::*;
fn take_max<'a>(n: &'a mut i32, m: &'a mut i32) -> &'a mut i32 {
let l = if *n >= *m {
t3assert(*n >= *m);
t3drop(m);
n
} else {
t3assert(*n < *m);
t3drop(n);
m
};
l
}
fn main() {
let mut a = rand_int::<i32>();
let mut b = rand_int::<i32>();
let ma = &mut a;
let mb = &mut b;
let mc = take_max(ma, mb);
*mc += 1;
t3drop(mc);
t3drop(ma);
t3drop(mb);
t3assert(a != b);
}
検証器の出力
作成するプログラム検証器の設計
単にプログラム検証器といっても様々ありますが[1]、今回は形式検証を用いた自動検証器をフルスクラッチで作成します。
ベースはシンボリック実行であり、処理内容は次のようなものになります。
- Rust プログラムを Rust の中間表現のひとつである THIR[2] に変換する。
- THIR を SMT 論理式 に変換する。
- SMT 論理式を入力として Z3[3] を実行し、検証する。
- 2~3 を繰り返す。
図では簡略化のため省いていますが、THIR をそのまま SMT 論理式に変換するのではなく、要素を減らした RTHIR(Reduced THIR) そして、シンボリック実行中に変数と値の式を持ち回るための LIR(Logical IR) を挟んで SMT 論理式に変換しています。
色々説明しましたが後でまた説明するので大丈夫です!
では、早速作っていきましょう！！
※ リポジトリの構成は以下のようになっているので、ファイルの置き場所に困りましたら参考にしてください。
リポジトリの構造
tautrust
├── Cargo.toml
├── LICENSE
├── Makefile
├── README.md
├── rust-toolchain.toml
├── rustfmt.toml
├── src
│ ├── analyze.rs
│ ├── analyze
│ │ ├── core.rs
│ │ ├── env.rs
│ │ ├── gen_cstr.rs
│ │ ├── helper_struct.rs
│ │ ├── lir.rs
│ │ ├── special.rs
│ │ ├── sub.rs
│ │ └── util.rs
│ ├── drive.rs
│ ├── main.rs
│ ├── run.rs
│ ├── thir.rs
│ ├── thir
│ │ ├── rthir.rs
│ │ ├── thir_printer.rs
│ │ └── thir_reducer.rs
│ └── util.rs
├── t3modules
│ ├── Cargo.toml
│ └── src
│ └── lib.rs
├── rthir-tree-samples
│ ├── let_m.rs
│ ├── let_m.tree
│ ├── test_t3module.rs
│ └── test_t3module.tree
└── tests
├── should_error.rs
├── test01_simple_assertion.rs
└── test_t3modules.rs
検証器作成のステップ
本記事では、Rust のコンパイラ内部の中間表現（THIR）を解析し、検証器を作成する手順を解説します。
最終目標: Rust のプログラムを SMT 論理式に変換し、簡単な検証を行う
ステップ 1: 中間表現(THIR) を取得する
- Rust のコンパイラ
rustcから THIR（中間表現） を取得します。 -
TyCtxtを使って THIR を取得する方法を解説します。
ステップ 2: THIR を RTHIR(別の中間表現)に変換する
- THIR から解析しやすい形（木構造）に変換します。
ステップ 3: シンボリック実行を行う
- RTHIR をシンボリック実行し、各変数に値の式を紐づけます。
ステップ 4: SMT の出力と検証
- 検証のための関数を実装します。
- SMT ソルバーで扱える形に変換し、論理的な検証を行います。
まずは、次のシンプルなコードを解析していきます。
fn main() {
let x = 0;
}
前準備
実装を始める前に前準備を行います。
今回はプログラムからコンパイラを呼び出します。
そのため、検証対象のプログラム内で std やクレートなどを使用する方法が少し特殊なので Makefile を作成しておきましょう。
RUST_LIB_PATH=$(rustc --print target-libdir)
file = "sample.rs"
cargo run $file -L "$RUST_LIB_PATH"
プログラムを事項する際は以下のコマンドで実行してください
./Makefile
ステップ 1: 中間表現(THIR) を取得する
rustc から THIRを取得する方法を示します.
- TyCtxt という構造体を取得する。[4]
- TyCtxt の関数を呼びだし、THIR を取得する。
以上になります。
では実際にコードを書いていきましょう。
TyCtxt を取得する
ファイルのパスを入れた args とコールバックを与え、 rustc を呼び出し TyCtxt の取得をします。rustc_driver::Callbacks を使用すると、 rustc のコンパイルを止め、コールバック時の TyCtxt を返してくれるのでこれを利用します。
TyCtxt を取得する Rust コンパイラの rustc_driver を使い、THIR を取得する準備をします。
RunCompiler::new() を使うことで、コンパイル処理のフックを提供する Callbacks を設定できます。
RunCompiler::new(&args, &mut MyCallbacks {}).run().unwrap();
コードの解説:
- args: コンパイル時の引数（例えば sample.rs を指定）
- MyCallbacks {}: rustc_driver::Callbacks を実装した構造体
- run().unwrap(); で rustc のコンパイルを実行
次のステップ: MyCallbacks に after_crate_root_parsing() を実装し、TyCtxt を取得します。
この MyCallbacks には次のように rustc_driver::Callbacks::after_crate_root_parsing() を実装します。
コールバックにより TyCtxt が返却されるため、それを tcx という変数名に格納します。
struct MyCallbacks {}
impl Callbacks for MyCallbacks {
fn after_crate_root_parsing<'tcx>(
&mut self, _compiler: &Compiler, queries: &'tcx Queries<'tcx>,
) -> Compilation {
queries.global_ctxt().unwrap().enter(|tcx| {
~~~
});
Compilation::Stop
}
}
コードの解説:
- global_ctxt().unwrap().enter(|tcx|): コンテキストを取得
以上で TyCtxt を取得することができました。
これ以降コードは、このクロージャ内で進めていきます。
THIR を取得する
Rust のコンパイラ rustc は、プログラムを解析するために THIR（Typed High-Level Intermediate Representation） を生成します。
TyCtxt はコンパイル時の情報を管理しており、各関数や変数は DefId（Definition ID）で識別されています。
これを用いて、 TyCtxt に実装されている thir_body[5] 関数から THIR を取得できます。
tcx.mir_keys(()).iter().for_each(|&key| {
let (thir, _) = tcx.thir_body(key).unwrap();
// この記事を書いているときは戻り値が Steal で包まれていた。
let thir = thir.steal();
~~~
});
コードの解説:
- tcx.mir_keys(()): これは各関数に紐付けられた DefId のリストを返します。
- 各 DefId に対して tcx.thir_body(def_id) を呼び出す: これにより、その関数の THIR を取得できます。
- 取得した THIR を steal() で展開: thir_body の戻り値は Steal 型でラップされているため、steal() を呼び出して中身を取り出します。
これで THIR も取得できました。
検証器作成の入り口に立ちましたね！
ここまでのまとめ
- rustc_driver を使って TyCtxt を取得
- TyCtxt から thir_body() を呼び出し、THIR を取得
- THIR の構造を理解し、変換準備完了
ステップ 2: THIR を RTHIR に変換する
これから THIR を RTHIR に変換していきます。
と、その前に、RTHIR へ変換する理由について説明します。
なぜ RTHIR へ変換するのか
- サポートしない式の削減:
THIR は Rust の全ての表現をサポートしています。解析時に不要な式が多く、パターンマッチで除外するのが面倒になります。そのため、それらを先に処理し、解析のしやすい中間表現を作る方が楽です。 - 不要な情報の削除
検証では使用しない情報もたくさん保持されています。なので、それらも消しておいた方が楽です。 - 木構造への変換:
この THIR はプログラムの各要素をベクタで管理しており、式は式のベクタ、関数は関数の、変数は変数の、という感じで情報を保持しています。そのため、関連要素にアクセスする際は、その要素のベクタからインデックスを指定してアクセスするというような方法を取ります。検証では木構造の方が楽なので、木構造の RTHIR にします。
これらをここで行っておくと、検証のための解析が非常に楽になります。
実装に際しては、rustc に THIR をプリントする関数[6]があるのでそちらを参考にすると良いです。(筆者はそのように実装しました。)
RTHIR の構造
解析で用いる RTHIR 構造体の定義です。
この先持ち回りやすいように ExprKind がフィールドに Expr を持つようなものは Rc で包んでおくと良いです。
- RThir
フィールド 説明 params: Vec<RParam<'tcx>> 関数の引数の一覧 body: Option<Rc<RExpr<'tcx>>> 関数内の式の一覧 - RParam
フィールド 説明 pat: Option<Rc<RExpr<'tcx>>> 引数の情報 - RExpr
フィールド 説明 kind: RExprKind<'tcx> 式の種類 span: Span プログラムにおける位置情報
sample.rs を解析するために、サポートする式の一覧です。
THIR には Pat と Expr という構造体があり、それぞれ PatKind、ExprKind という Enum のフィールドを持っていますが、RTHIR では Expr の中に Pat を取り込みます。
全ての表現は 1 つずつ Scoped という表現で包まれているので、取り除きます。
それ以外は unimplemented でエラーを起こすようにします。
| RExprKind |
|---|
| Block { stmts, expr } |
| VarRef { id } |
| Literal { lit, neg } |
| LetStmt { pattern, initializer } |
| Pat { kind } |
| PatKind |
|---|
| Binding { var, ty, subpattern } |
この変換を行う関数を reduce_thir などと名付けておき、呼び出します。
tcx.mir_keys(()).iter().for_each(|&key| {
let (thir, _) = tcx.thir_body(key).unwrap();
let thir = thir.steal();
rthir = reduce_thir(thir);
});
print して、次のように表示できるようになれば、RTHIR の作成完了です。
fn main() {
let x = 0;
}
DefId(0:3 ~ sample[2cf1]::main), params: [
]
body:
Expr {
span: sample.rs:1:11: 1:25 (#0)
kind:
Block {
stmts: [
Expr {
span: sample.rs:1:13: 1:22 (#0)
kind:
LetStmt {
pattern:
Expr {
span: sample.rs:1:17: 1:18 (#0)
kind:
Pat {
PatKind {
Binding {
name: "x"
mode: BindingMode(No, Not)
var: LocalVarId(HirId(DefId(0:3 ~ sample[2cf1]::main).4))
ty: i32
is_primary: true
subpattern: None
}
}
}
}
,
initializer: Some(
Expr {
span: sample.rs:1:21: 1:22 (#0)
kind:
Literal(
lit: Spanned {
node: Int(Pu128(0), Unsuffixed),
span: sample.rs:1:21: 1:22 (#0)
},
neg: false
)
}
)
}
}
]
expr: []
}
}
ここまでのまとめ
- THIR の無駄な部分を除いた RThir を宣言。
- 必要最小限の Expr 、RExpr を宣言。
ステップ 3: シンボリック実行を行う
これから、検証器のメインの動作の実装に入っていきます。
ここで実装する機能は、先ほど作成した RTHIR をシンボリック実行をベースに解析していき、SMT へ変換していくものです。
main 関数を取り出す
Rust のプログラム解析では、main 関数をエントリーポイントとして解析を開始します。
Rust のコンパイラ rustc では、関数ごとに DefId（Definition ID）を持ち、それをキーとして THIR（Typed High-Level Intermediate Representation）や MIR（Middle Intermediate Representation）を管理しています。
main 関数の RTHIR（Reduced THIR）を取得する方法を示します。
- get_fn_map() を作成し、RTHIR のマップを構築
- 各関数の DefId を取得し、対応する RTHIR を生成する。
- tcx.entry_fn() を用いて main 関数の DefId を取得
- get_fn_map() から main 関数の RTHIR を取得する
THIR を取得する。のコードを編集して main 関数を取り出すまでのコードを書きましょう。
関数ごとの RTHIR を取得する
まず、プログラム内のすべての関数について RTHIR を作成し、LocalDefId をキーとして HashMap に格納します。
以下の get_fn_map() 関数は、mir_keys() で関数ごとの DefId を取得し、それに対応する RTHIR を生成します。
pub fn get_fn_map<'tcx>(tcx: &TyCtxt<'tcx>) -> Map<LocalDefId, Rc<RThir<'tcx>>> {
let mut map: Map<LocalDefId, Rc<RThir<'tcx>>> = Map::new();
tcx.mir_keys(()).iter().for_each(|&key| {
let rthir = generate_rthir(&tcx, key).expect("failed to generate Reduced-THIR");
println!("{:?}, {:?}", key, rthir);
map.insert(key, Rc::new(rthir));
});
map
}
コードの解説:
- tcx.mir_keys(()): すべての関数の DefId のリストを取得する。fn main() などのユーザー定義関数の ID を含む。
- generate_rthir(&tcx, key): 各 DefId に対して THIR を RTHIR に変換する関数を呼び出す。
- map.insert(key, Rc::new(rthir)): LocalDefId をキーとして RTHIR を格納する。
main 関数の RTHR を取得する。
次に、get_fn_map から返却された fn_map から、main 関数を取得します。
main関数の DefId は、tcx.entry_fn() [7]関数を用いて取得することができます。
if let Some((main_id, ..)) = tcx.entry_fn(()) {
let fn_map = get_fn_map(&tcx);
// expect_local は DefId 型を LocalDefId 型にキャストし、
// HashMap::<LocalDefId, RThir<'tcx>> のキーとして
// 使用できるようにするための操作。
let main = fn_map.get(&main_id.expect_local());
~
}
コードの解説:
- tcx.entry_fn(()): エントリポイント（main 関数）の DefId を取得する。
- expect_local(): DefId はグローバルな識別子だが、ローカルスコープの LocalDefId に変換することで HashMap のキーとして使えるようにする。
- fn_map.get(&main_id.expect_local()): get_fn_map() で作成した関数マップから main 関数の RTHIR を取得する。
以上で main 関数の RTHIR が取得できました。
Env 構造体の作成
シンボリック実行を用いた解析では、プログラム内の変数が具体的な値を持たないまま処理が進むため、変数とその演算履歴を記録・管理する環境（Env） を構築する必要があります。
この Env 構造体は、条件分岐（if, match 等）やループ（loop, for 等）ごとに新しいインスタンスが生成され、現在の解析状態を保持します。
Env 構造体
| フィールド | 説明 |
|---|---|
| smt_vars: Vec<(String, TyKind<'tcx>)> | SMT 論理式における変数の宣言の一覧。変数の名前と型を持つ。 |
| path: Vec<String> | 解析中の制約条件のリスト（条件分岐などの情報を保持）。 |
| var_map: Map<LocalVarId, Lir<'tcx>> | 検証器における変数と SMT 論理式の値の式を対応づける辞書。変数IDをキー、値の式をバリューとする。 |
宣言と new 関数の実装をしておきます。
#[derive(Clone)]
pub struct Env<'tcx> {
pub smt_vars: Vec<(String, TyKind<'tcx>)>,
pub path: Vec<String>,
pub var_map: HashMap<LocalVarId, Lir<'tcx>>,
}
impl<'tcx> Env<'tcx> {
pub fn new() -> Self { Self { smt_vars: Vec::new(), path: Vec::new(), var_map: HashMap::new() } }
}
Lir 構造体の作成
シンボリック実行では、変数や計算式を具体的な値ではなく、論理式として扱います。
そこで、値の式を表現するための LIR（Logical Intermediate Representation） を定義し、プログラムの解析を進めやすくします。
Lir 構造体
Lir は、解析対象の値を論理式（SMT 形式）として扱うための構造体 です。
各変数の式がどのような値を持つかを記録し、操作を蓄積していきます。
| フィールド | 説明 |
|---|---|
| kind: LirKind<'tcx> | 値の式の持ち方の種類 |
| expr: Rc<RExpr<'tcx>> | Span 情報を取得するために持っておく |
#[derive(Clone)]
pub struct Lir<'tcx> {
pub kind: LirKind<'tcx>,
pub expr: Rc<RExpr<'tcx>>,
}
impl<'tcx> Lir<'tcx> {
pub fn new(
ty: TyKind<'tcx>, var_expr: Vec<String>, expr: Rc<RExpr<'tcx>>,
) -> Result<Self, AnalysisError> {
let kind = match ty {
TyKind::Bool | TyKind::Int(_) | TyKind::Float(_) => LirKind::new(ty, var_expr[0].clone()),
_ => return Err(AnalysisError::UnsupportedPattern(format!("Unknown TyKind: {ty:?}"))),
};
Ok(Self { kind, expr })
}
pub fn get_var_expr(&self) -> &String { self.kind.get_var_expr() }
pub fn set_var_expr(&mut self, constraint: String) { self.kind.set_var_expr(constraint) }
}
LirKind 構造体
LIR の kind には、今後さまざまな種類の式（加算、乗算、条件式など）を拡張できるように Enum を用います。
現在は VarExpr（変数の式）のみを実装しています。
var_expr が値の式であり、値に対して行われた操作を溜めておきます。
| LirKind | 説明 |
|---|---|
| VarExpr { var_expr: String, ty: TyKind<'tcx> } | var_expr が値の式であり、値に対して行われた操作を溜めておきます。 |
Lir の宣言とnew関数を作成しておきます。
また、後ほど使用する、値の式(var_expr)のセッタ、ゲッタも実装しておきます。
#[derive(Clone)]
pub enum LirKind<'tcx> {
VarExpr { var_expr: String, ty: TyKind<'tcx> },
}
impl<'tcx> LirKind<'tcx> {
pub fn new(ty: TyKind<'tcx>, var_expr: String) -> Self { LirKind::VarExpr { var_expr, ty } }
pub fn get_ty(&self) -> TyKind<'tcx> {
match self {
LirKind::VarExpr { ty, .. } => ty.clone()
}
}
pub fn get_var_expr(&self) -> &String {
match self {
LirKind::VarExpr { var_expr, .. } => var_expr,
}
}
pub fn set_var_expr(&mut self, new_var_expr: String) {
match self {
LirKind::VarExpr { var_expr, .. } => *var_expr = new_var_expr
}
}
エラー構造体の作成
実行中にエラーが起きた際のために検証エラー用の構造体を作成しておきます。
match 文などで使用してください。
pub enum AnalysisError {
UnsupportedPattern(String)
}
main 関数の RTHIR を取得できたので、ここからシンボリック実行を行い、変数の値を論理式(SMT 形式)として解析していきます。
シンボリック実行では、各変数の状態を追跡しながらプログラムの動作をシミュレーションします。
解析の流れ
- main 関数の body を取得
- body が Block であることを確認し、stmts（文）と expr（式）を解析
- 各 stmt を match で処理
- シンボリック変数を Env に格納または、変数の値を更新
- LetStmt（変数の宣言）を処理
- initializer（初期化式）を LIR に変換
- 変数を Env に登録
- LetStmt（変数の宣言）を処理
- この処理を再帰的に行い、RTHIR 全体を解析
関数を移動する際には、Env オブジェクトを持ち回します。
main 関数の body を取得
main 関数には引数(Param)がないので、body から解析を始めます。
if let Some(body) = &rthir.body {
let mut main_env = Env::new();
// 解析処理へ
}
body が Block であることを確認
次に、body がブロックであるという前提のもと、フィールドを取得します。
Block には stmts と expr が含まれており、それぞれ解析します。
もし、Block でなければ、AnalysisError を返すようにします。
if let RExpr { kind: RExprKind::Block { stmts, expr }, .. } = body {
/// stmts の解析
if let Some(expr) = expr {
/// expr の解析
}
}
stmts は 式の一覧で、expr は戻り値[8]と考えていただいて問題ないです。
各 stmt を match で処理
stmts は Vec<Rc<RExpr<'tcx>>> 型です。for 文でイテレートし、match を用いてそれぞれのステートメントを処理します。
今回の例では、値の宣言 "let x = 0;" に対応する LetStmt が含まれており、変数をシンボリックな値（SMT 変数）として登録します。
for stmt in stmts {
~
match expr.kind.clone() {
LetStmt { pattern, initializer } => {
// LetStmt の処理へ
}
~
_ => return Err(AnalysisError::UnsupportedPattern("Unsupported statement".to_string())),
}
~
}
LetStmt を解析し、変数を登録
LetStmt では、変数の登録と値の式を生成します。
変数の宣言（let x = 0; など）では、以下の処理を行います：
- パターン pattern から変数情報を抽出
- 初期化式 initializer を解析し、論理式に変換
- シンボリック変数として Env に登録
// pattern は、 kind が Pat であるという前提のものと中身を確認します。
// また、Pat の kind も今は Binding のみであることも使いましょう。
if let RExprKind::Pat { kind: RPatKind::Binding { ty, var, .. } } = &pattern.clone().kind {
let lir = Lir::new(*ty.kind(), vec![String::new()], pat);
// 変数を登録する。
env.var_map.insert(*var_id, lir);
initializer の解析
initializer は Option 型なので、Someの場合は取り出し、式に変換します。
この処理は頻繁に行うため、関数として分離すると良いでしょう。
if let Some(expr) = initializer {
let value = // expr から値の式を生成する;
env.assign_new_value(var, value.get_var_expr().into())
}
Literal（リテラル）から値の式を生成する処理
今回、initializer は Literal なので、Literal を値の式に変換する処理を書きます。
match &expr.kind {
Literal { lit, neg } => match lit.node {
// Int の場合は、n が実数値です。
// neg の値によって、正負を判断しています。
// 一旦 I32 型のみサポートします。
LitKind::Int(n, _) => Ok(LirKind::new(
TyKind::Int(IntTy::I32),
if neg { format!("-{n}") } else { format!("{n}") },
)),
// Float も Int と同様です。
LitKind::Float(symbol, _) => Ok(LirKind::new(
TyKind::Float(FloatTy::F64),
if neg { format!("-{symbol}") } else { format!("{symbol}") },
)),
// 後のために bool もサポートします。
LitKind::Bool(b) => Ok(LirKind::new(TyKind::Bool, b.to_string())),
_ => Err(AnalysisError::UnsupportedPattern(format!(
"Unsupported literal pattern: {}",
lit.node
))),
},
}
変数の値を Env に登録
解析が完了した変数の論理式を Env に保存し、シンボリック実行を続行します。
assign_new_value は変数に値の式を登録します。LIR に実装してある、var_expr 関連の関数を使用して作成します。
pub fn assign_new_value(&mut self, target_id: &LocalVarId, constraint: String) {
// 対象の Lir を取得
let target = self.var_map.get_mut(target_id).expect("target value not found");
// 新規の値の式をセット
target.set_var_expr(constraint);
}
コードの解説:
- self.var_map.get_mut(target_id): 変数(Lir)の可変借用を取得する。
- target.set_var_expr(constraint): target に値の式を追加する。
このように、木構造である RTHIR を再起的に処理していき、変数と値の式を Env 関数に保存する、この繰り返しで解析していきます。
シンボリックイグゼキューションで処理を流れを追う方法を掴んできたでしょうか?
ここまでのまとめ
- 変数の論理式と制約条件を保持し、シンボリック実行の基盤を提供する Env を宣言
- 変数や値の論理式を管理し、SMT ソルバー用の式を保持する Lir, LirKind を宣言。
- main 関数の body を取得し、解析を開始。
- stmts を match で処理し、LetStmt の解析を実装。
- initializer を LIR に変換し、変数を Env に登録。
- 変数の値を assign_new_value() で更新。
ステップ 4: SMT の出力と検証
では、実際に検証が絡むコードを処理できるように機能を追加していきましょう。
が、その前に SMT の記法について説明します。
SMT の記法
-
変数の宣言
Z3 では変数の宣言を次の式で行います。この検証器では、type は Bool, Int, Real を使います。(declare-const [var name] [type]) -
二項演算
Z3 では二項演算は次のように記述します。例: +: (+ x y), not: (distinct x y)([operation] [left] [right]) -
assume と assert
Z3 ではそれぞれ次のように記述します。
assume に相当するのは、(assert A) です。制約条件を追加します。
assert に相当するのは、(assert (not A)) です。(assert (not constraint)) で検証を行います。# assume (assert [constraint]) # assert (assert (not [constraint])) -
検証実行
(check-sat)
以上が今回の検証で用いる基本的な SMT の記法です。
その他の機能など、詳しくは Z3 のドキュメントを確認してください
さて、戻って検証が絡むコードを実装する流れを示します。
SMT の出力と検証をするまでの流れを示します。
- 検証用のモジュールを実装
- RExprKind に Call(関数呼び出し) を追加
- 検証用モジュールのシンボリック実行をサポート
- Env から SMT の出力を実装
- プログラムから Z3 の呼び出しを実装
検証用のモジュールを実装
検証時に役に立つ、assert, assume 等の関数と、任意の値を表現するための rand を提供するクレートを作成します。
プロジェクトのルートで、次のコマンドを実行します。
cargo new --lib t3modules
次のように実装しましょう。
検証用の関数であるため、中身は不必要です。
pub fn t3assert(_: bool) {}
pub fn t3assume(_: bool) {}
pub fn rand_bool() -> bool { false }
pub fn rand_int<T: From<i8>>() -> T { T::from(0) }
pub fn rand_float<T: From<f32>>() -> T { T::from(0.0) }
関数の返却値を表現する ExprKind::ZstLiteral が必要になるので、RExprKind にも追加します。これは検証には直接関わりません。消しても良いです。
Literal {
lit: &'tcx hir::Lit,
neg: bool,
},
ZstLiteral {
user_ty: UserTy<'tcx>,
},
~
ExprKind::ZstLiteral { user_ty } => RExprKind::ZstLiteral { user_ty: user_ty.clone() },
検証対象のプログラム内で t3module を使用できるように Makefile を編集します。
cargo build --manifest-path=t3modules/Cargo.toml --release
RUST_LIB_PATH=$(rustc --print target-libdir)
T3MODULES="./t3modules/target/release/libt3modules.rlib"
file = "sample.rs"
cargo run $file -L "$RUST_LIB_PATH" --extern t3modules="$T3MODULES"
RExprKind に Call(関数呼び出し)を追加
REprKind に Call を追加します。
Call {
ty: Ty<'tcx>,
fun: Rc<RExpr<'tcx>>,
args: Box<[Rc<RExpr<'tcx>>]>,
from_hir_call: bool,
fn_span: Span,
},
プリント関数や、Expr からの変換関数も適当に実装してください。
ここで、次のようなコードがRTHIRで出力できることを確認しておくと良いでしょう。
extern crate t3modules;
use t3modules::*;
fn main() {
let x = 0;
t3assert(true);
}
sample.rs tree
params: [
]
body:
Expr {
ty: ()
temp_lifetime: Some(Node(11))
span: sample.rs:4:11: 7:2 (#0)
kind:
Scope {
region_scope: Node(11)
lint_level: Explicit(HirId(DefId(0:5 ~ sample[c8d0]::main).11))
value:
Expr {
ty: ()
temp_lifetime: Some(Node(11))
span: sample.rs:4:11: 7:2 (#0)
kind:
Block {
targeted_by_break: false
span: sample.rs:4:11: 7:2 (#0)
region_scope: Node(10)
safety_mode: Safe
stmts: [
Stmt {
kind: Let {
remainder_scope: Remainder { block: 10, first_statement_index: 0}
init_scope: Node(1)
pattern:
Pat: {
ty: i32
span: sample.rs:5:9: 5:10 (#0)
kind: PatKind {
Binding {
name: "x"
mode: BindingMode(No, Not)
var: LocalVarId(HirId(DefId(0:5 ~ sample[c8d0]::main).4))
ty: i32
is_primary: true
subpattern: None
}
}
}
,
initializer: Some(
Expr {
ty: i32
temp_lifetime: Some(Node(1))
span: sample.rs:5:13: 5:14 (#0)
kind:
Scope {
region_scope: Node(2)
lint_level: Explicit(HirId(DefId(0:5 ~ sample[c8d0]::main).2))
value:
Expr {
ty: i32
temp_lifetime: Some(Node(1))
span: sample.rs:5:13: 5:14 (#0)
kind:
Literal( lit: Spanned { node: Int(Pu128(0), Unsuffixed), span: sample.rs:5:13: 5:14 (#0) }, neg: false)
}
}
}
)
else_block: None
lint_level: Explicit(HirId(DefId(0:5 ~ sample[c8d0]::main).3))
span: sample.rs:5:5: 5:14 (#0)
}
}
Stmt {
kind: Expr {
scope: Node(9)
expr:
Expr {
ty: ()
temp_lifetime: Some(Node(9))
span: sample.rs:6:5: 6:19 (#0)
kind:
Scope {
region_scope: Node(5)
lint_level: Explicit(HirId(DefId(0:5 ~ sample[c8d0]::main).5))
value:
Expr {
ty: ()
temp_lifetime: Some(Node(9))
span: sample.rs:6:5: 6:19 (#0)
kind:
Call {
ty: FnDef(DefId(20:3 ~ t3modules[ddc1]::t3assert), [])
from_hir_call: true
fn_span: sample.rs:6:5: 6:19 (#0)
fun:
Expr {
ty: FnDef(DefId(20:3 ~ t3modules[ddc1]::t3assert), [])
temp_lifetime: Some(Node(9))
span: sample.rs:6:5: 6:13 (#0)
kind:
Scope {
region_scope: Node(6)
lint_level: Explicit(HirId(DefId(0:5 ~ sample[c8d0]::main).6))
value:
Expr {
ty: FnDef(DefId(20:3 ~ t3modules[ddc1]::t3assert), [])
temp_lifetime: Some(Node(9))
span: sample.rs:6:5: 6:13 (#0)
kind:
ZstLiteral(user_ty: None)
}
}
}
args: [
Expr {
ty: bool
temp_lifetime: Some(Node(9))
span: sample.rs:6:14: 6:18 (#0)
kind:
Scope {
region_scope: Node(8)
lint_level: Explicit(HirId(DefId(0:5 ~ sample[c8d0]::main).8))
value:
Expr {
ty: bool
temp_lifetime: Some(Node(9))
span: sample.rs:6:14: 6:18 (#0)
kind:
Literal( lit: Spanned { node: Bool(true), span: sample.rs:6:14: 6:18 (#0) }, neg: false)
}
}
}
]
}
}
}
}
}
}
]
expr: []
}
}
}
}
検証用モジュールのシンボリック実行のサポート
検証用モジュールを処理し、環境へ保存する機能を実装します。
関数呼び出しの処理の実装
関数呼び出しを処理する流れを示します。
- stmts で Call にマッチ
- ty から関数の DefId を取得し、local 関数か external 関数かを判別
- それぞれの関数にあった処理を実行
- local 関数: 関数内の環境に移動
- external 関数: Path から関数を判別し、その関数にあった処理を実行
まず、stmts の解析関数内で Call をサポートします。
stmts で Call にマッチ
match 文に Call を追加しましょう。一旦使用する要素は ty, args のみです。
LetStmt { pattern, initializer } => ...
Call { ty, args, .. } => // 関数を解析
ty から 関数のDefId を取得し、
match ty.kind() {
TyKind::FnDef(def_id, ..) => {
if let Some(_fun) = {
if def_id.is_local() {
Some(
self.fn_map
.get(&def_id.expect_local())
.expect("Get local fn failed")
.clone(),
)
} else {
None
}
} {
// local 関数の処理
unimplemented!();
} else {
let fn_info = // 関数情報を取得;
// extern 関数の処理
}
}
_ => panic!("Call does not have FnDef"),
}
コードの解説:
- def_id.is_local(): DefId が local なものかを確認。
- def_id.expect_Local(): DefId を LocalDefId にキャストして返却する。失敗すると panic する。
関数情報を取得
関数の def_id を使って tcx から関数名を含む def_path を取得します。
(def_path の例: t3modules::t3assert)
この def_path を ':', '"', "\" で分割した Vec を関数情報とします。
let def_path = tcx.def_path_str(*def_id);
def_path
.split(|c| c == ':' || c == '"' || c == '\\')
.filter(|s| !s.is_empty())
.map(String::from)
.collect()
コードの解説:
- map(String::from): 各変数に対して String::from() を呼び出す。
extern 関数の処理
extern 関数を処理します。
今 extern 関数は t3modules 内の関数のみであるため、決め内で解析します。
if fn_info[0] == "t3modules" {
match fn_info[1].as_str() {
"t3assert" => // t3assert の処理,
"t3assume" => // t3assume の処理,
_ => unreachable!(),
}
}
t3assume の処理の実装
extern 関数が t3assume であった場合環境に制約条件を追加します。
let constraint = // 関数の引数 args[0].clone() を Lir に変換する処理;
env.add_assume(constraint.get_assume().into());
コードの解説:
- env.add_assume(cosntraint): env に制約条件を追加する。path に制約条件が追加される。
t3assert の処理の実装
extern 関数が t3assert であった場合環境に制約条件を検証します。
let constraint = // 関数の引数 args[0].clone() を Lir に変換する処理;
// constraint の検証を実行
Env から SMT を出力
Env から SMT を出力する機能を実装します。
Env から SMT 文字列へ
Env を SMT 文字列に変換する方法を示します。
- Env に登録された変数の宣言を生成
- Env に記録された制約条件を生成
pub fn get_assumptions(&self) -> Result<String, AnalysisError> {
let mut smt = String::new();
// Env に登録された変数の宣言を生成
for smt_var in self.smt_vars.iter() {
smt.push_str(&self.to_smt(smt_var)?);
}
// Env に記録された制約条件を生成
for constraint in self.path.iter() {
smt.push_str(&format!("(assert {constraint})\n"));
}
Ok(smt)
}
pub fn to_smt(&self, var: &(String, TyKind<'tcx>)) -> Result<String, AnalysisError> {
match var.1 {
TyKind::Bool => Ok(format!("(declare-const {} Bool)\n", var.0)),
TyKind::Int(_) => Ok(format!("(declare-const {} Int)\n", var.0)),
TyKind::Float(_) => Ok(format!("(declare-const {} Real)\n", var.0)),
_ => Err(AnalysisError::UnsupportedPattern(format!(
"Unknown TyKind: {:?} in to_smt",
var.1
))),
}
}
コードの解説:
- smt.push_str(): String に文字列を連結する。
プログラムから Z3 の呼び出し
プログラムから Z3 を呼び出し、検証する方法を示します。
- Command を用いて Z3 実行
- Env から現在までの SMT 文字列を生成
- SMT 文字列に対し、今回検証する条件を追加
- SMT文字列に、検証のための (check-sat) 式を追加
- Z3 の stdin に SMT 文字列を書き込み
- Z3 の stdout から 検証結果を読み込み
- unsat であれば検証成功
Z3 を用いたプログラム検証において、unsat が返された場合、検証成功と判断します。
検証失敗した時のために、AnalysisError に VerifyError を追加します。これは失敗したコードの Span を持ちます。
pub enum AnalysisError {
UnsupportedPattern(String),
VerifyError(Span),
}
なぜ unsat が検証成功なのか？
Z3 は、与えられた制約条件を満たす変数の組み合わせが存在するかを検証するソルバーです。
通常、プログラムの動作を検証する際には、その正しさを保証するための制約条件を Z3 に入力し、
制約条件を満たす変数の組み合わせが存在する (sat) かどうかを確認します。
しかし、プログラムが特定の条件を必ず満たすことを証明するには、その条件が破られる可能性がないことを確認する必要があります。
これを実現するために、検証したい条件の否定 (not) を Z3 に与えて検証します。
- sat が返った場合 → 否定の条件を満たす解が存在する → 元の条件が破られる可能性がある（検証失敗）
- unsat が返った場合 → 否定の条件を満たす解が存在しない → 元の条件が必ず成り立つ（検証成功）
つまり、Z3 に not (検証したい条件) を与えて check-sat を実行し、unsat が返ってくれば、
その条件は必ず満たされることが証明されたことになります。
pub fn verify(&mut self, constraint: &String, span: Span) -> Result<(), AnalysisError> {
let mut child = Command::new("z3")
.args(["-in", "-model"])
.stdin(std::process::Stdio::piped())
.stdout(std::process::Stdio::piped())
.spawn()
.expect("Run Z3 failed");
let mut smt = String::new();
// Env から現在までの SMT 文字列を生成
smt.push_str(&self.get_assumptions()?);
// SMT 文字列に対し、今回検証する条件を追加
smt.push_str(&format!("(assert (not {constraint}))\n"));
let mut stdin = child.stdin.take().expect("Open stdin failed");
// SMT文字列に、検証のための (check-sat) 式を追加
smt += "(check-sat)\n";
println!("{smt}");
// Z3 の stdin に SMT 文字列を書き込み
stdin.write_all(smt.as_bytes()).expect("Write smt failed");
drop(stdin);
// Z3 の stdout から 検証結果を読み込み
let output = child.wait_with_output().expect("Get stdout failed");
let result = String::from_utf8(output.stdout).expect("Load result failed");
// unsat であれば検証成功
if &result != "unsat\n" {
return Err(AnalysisError::VerifyError(span));
}
println!("Verification success!\n");
Ok(())
}
コードの解説:
- Command::new(): 外部のコマンド実行します。
- child.stdin.take(): コマンドの stdin を取得します。
- stdin.write_all(): stdin に byte 列を書き込みます。
- drop(): 借用をドロップします。
- child.wait_with_output(): コマンドの stdout を取得します。
- String::from_utf8(): 有効な utf8 である byte 列から String を作成します。
では、sample を実行してみましょう。
extern crate t3modules;
use t3modules::*;
fn main() {
let x = 0;
t3assert(true);
}
検証も実装できました。
(assert (not true))
(check-sat)
Verification success!
ここまでのまとめ
- 検証用モジュールの実装。
- 検証用モジュールのシンボリック実行
- Env から var_map, path を含めた、SMT 文字列を出力
- verify() で Z3 を呼び出し検証を行う。
ここまでの章で、検証までに必要な機能を一通り確認することができました。
次がこの第1回記事の最後の章です。
実際に短いコードを検証してみる
お疲れ様です。これが最後の章です。
次のコードを検証できるようになることを目指します。
extern crate t3modules;
use t3modules::*;
fn main() {
let x = rand_int::<i32>();
t3assume(x != 0);
x *= x;
t3assert(x > 0);
}
必要な要素の洗い出し
まず power.rs を検証するために必要な要素を考えてみましょう。
RTHIR 眺めながら確認しましょう。
power.rs tree
DefId(0:5 ~ sample[c8d0]::main), params: [
]
body:
Expr {
span: tests/sample.rs:4:11: 12:2 (#0)
kind:
Block {
stmts: [
Expr {
span: tests/sample.rs:5:5: 5:30 (#0)
kind:
LetStmt {
pattern:
Expr {
span: tests/sample.rs:5:9: 5:10 (#0)
kind:
Pat {
PatKind {
Binding {
name: "x"
mode: BindingMode(No, Not)
var: LocalVarId(HirId(DefId(0:5 ~ sample[c8d0]::main).8))
ty: i32
is_primary: true
subpattern: None
}
}
}
}
,
initializer: Some(
Expr {
span: tests/sample.rs:5:13: 5:30 (#0)
kind:
Call {
ty: FnDef(DefId(20:7 ~ t3modules[ddc1]::rand_int), [i32])
from_hir_call: true
fn_span: tests/sample.rs:5:13: 5:30 (#0)
fun:
Expr {
span: tests/sample.rs:5:13: 5:28 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: []
}
}
)
}
}
Expr {
span: tests/sample.rs:7:5: 7:21 (#0)
kind:
Call {
ty: FnDef(DefId(20:4 ~ t3modules[ddc1]::t3assume), [])
from_hir_call: true
fn_span: tests/sample.rs:7:5: 7:21 (#0)
fun:
Expr {
span: tests/sample.rs:7:5: 7:13 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: tests/sample.rs:7:14: 7:20 (#0)
kind:
Binary {
op: Ne
lhs:
Expr {
span: tests/sample.rs:7:14: 7:15 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ sample[c8d0]::main).8))
}
}
rhs:
Expr {
span: tests/sample.rs:7:19: 7:20 (#0)
kind:
Literal( lit: Spanned { node: Int(Pu128(0), Unsuffixed), span: tests/sample.rs:7:19: 7:20 (#0) }, neg: false)
}
}
}
]
}
}
Expr {
span: tests/sample.rs:9:5: 9:11 (#0)
kind:
AssignOp {
op: Mul
lhs:
Expr {
span: tests/sample.rs:9:5: 9:6 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ sample[c8d0]::main).8))
}
}
rhs:
Expr {
span: tests/sample.rs:9:10: 9:11 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ sample[c8d0]::main).8))
}
}
}
}
Expr {
span: tests/sample.rs:11:5: 11:20 (#0)
kind:
Call {
ty: FnDef(DefId(20:3 ~ t3modules[ddc1]::t3assert), [])
from_hir_call: true
fn_span: tests/sample.rs:11:5: 11:20 (#0)
fun:
Expr {
span: tests/sample.rs:11:5: 11:13 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: tests/sample.rs:11:14: 11:19 (#0)
kind:
Binary {
op: Gt
lhs:
Expr {
span: tests/sample.rs:11:14: 11:15 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ sample[c8d0]::main).8))
}
}
rhs:
Expr {
span: tests/sample.rs:11:18: 11:19 (#0)
kind:
Literal( lit: Spanned { node: Int(Pu128(0), Unsuffixed), span: tests/sample.rs:11:18: 11:19 (#0) }, neg: false)
}
}
}
]
}
}
]
expr: []
}
}
どうですか、全部出せましたか?このコードには、以下の対応しなければいけない要素があります。
- rand_int: まず rand_int ですね。これは、x には指定された型が取りうる全ての値が入るというものになります。
- x: これは x に対する参照(VarRef)です。VarRef への対応が必要です。
- !=: 次に x != 0 です。二項演算子(Binary)への対応が必要です。
- *=: 次に x *= x です。複合代入演算子(AssignOp)への対応が必要です。
ではさっそくやっていきましょう。
rand_int のサポート
rand_int のサポートです。改めて言いますが、これは、指定された型が取りうる全ての値が入るというものを表します。そのため、値の式はなんらかの変数となります。
では、rand_int の処理を実装しましょう。
rand_int は let の initializer として使用されています。
そのため、値の式を生成する処理に Call(関数呼び出し)を追加しましょう。
Literal { lit, neg } => // Literal から値の式を生成する処理,
Call { ty, args, .. } => // 関数から値の式を生成する処理。
次に、関数が local であるか external であるかを判断するコードを書きます。
t3assert などの処理とあまり違いありません。
match ty.kind() {
TyKind::FnDef(def_id, ..) => {
let fn_info = self.get_fn_info(def_id);
if let Some(fun) = self.get_local_fn(def_id) {
// local 関数から値の式を生成する処理
} else {
// external 関数から値の式を生成する処理
}
}
_ => panic!("Call has not have FnDef"),
}
次に、external 関数を処理するコードを書きます。こちらも t3assert とあまり変わりません。が、私のコードは変わらないように勤めようとしたせいで、あまり綺麗ではないので、綺麗に書けるよう工夫してみると良いかもしれません。
私のコードを載せます。
まず、AnalysisError に RandFunctions を追加します。
pub enum AnalysisError {
UnsupportedPattern(String),
RandFunctions,
VerifyError(Span),
そして、rand を AnalysisError::RandFunctions として処理します。
if fn_info[0] == "t3modules" {
match fn_info[1].as_str() {
"rand_bool" => Err(AnalysisError::RandFunctions),
"rand_int" => Err(AnalysisError::RandFunctions),
"rand_float" => Err(AnalysisError::RandFunctions),
_ => unreachable!(),
}
}
Error で initializer のところまで戻り、RandFunctions についてハンドリングします。
値の式として用いる SMT 変数の名前を作成します。変数名は一意になるように span を名前に含めます。
match // initializer から値の式を生成する処理
{
Ok(value) => env.assign_new_value(var, value.get_var_expr().into()),
Err(AnalysisError::RandFunctions) => {
let rand = format!("rand_{}", Analyzer::span_to_str(&pattern.span));
env.add_rand(rand.clone(), ty.kind());
env.assign_new_value(var, rand)
},
Err(err) => return Err(err),
}
コードの解説:
- Command::new(): 外部のコマンド実行します。
- env.add_rand(): env の smt_vars に SMT 変数を追加します。
- env.assign_new_value(): env に変数を追加します。
VarRef から値の式を生成
今回引数は VarRef を含むので、それのサポートをしましょう。
VarRef の RTHIR はすでに実装してあるはずなので、値の式を生成する処理だけ実装すれば良いです。
match に VarRef 追加します。
Literal => // Literal から値の式
VarRef { id } => // VarRef から値の式を生成する処理,
処理はシンプルで、var_map から id を get して LirKind をクローンすれば良いです。
match env.var_map.get(id) {
Some(lir) => Ok(lir.kind.clone()),
None => Err(AnalysisError::UnsupportedPattern(format!(
"given var id {:?} is not found",
id
))),
}
二項演算(Binary)のサポート
二項演算のサポートです。
REprKind に Binary を追加します。
Binary {
op: BinOp,
lhs: Rc<RExpr<'tcx>>,
rhs: Rc<RExpr<'tcx>>,
},
プリント関数や、Expr からの変換関数も適当に実装してください。
では Binary から値の式を生成します。
match に Binary を追加しましょう。
Literal => // Literal から値の式
Binary { op, lhs, rhs } => Binary から値の式を生成する。
Call => // Call から値の式
Binary から値の式を生成する流れを示します。
- 左側の引数から値の式(LirKind)を生成
- 右側の引数から値の式(LirKind)を生成
- 演算子から SMT 演算子を生成
- 左側の値の式に演算子と右側の値の式を適応する
まず、lhs と rhs を先ほど実装した VarRef で値の式に変換します。
let mut lir = // lhs から値の式を生成
let rhs = // rhs から値の式を生成
次に演算子から SMT 演算子を生成します。
ここではこれからを見据えて、使いそうな二項演算子もサポートしておきます。
pub fn bin_op_to_smt(op: BinOp) -> Result<String, AnalysisError> {
use BinOp::*;
let op_str = match op {
Add => "+",
Sub => "-",
Mul => "*",
Rem => "mod",
Div => "div",
BitXor => "^",
BitAnd => "&",
BitOr => "|",
Eq => "=",
Lt => "<",
Le => "<=",
Ne => "distinct",
Ge => ">=",
Gt => ">",
_ => return Err(AnalysisError::UnsupportedPattern(format!("{op:?}"))),
};
Ok(op_str.into())
}
そして、左側の値の式に、右側の値の式と演算子を適応します。
lir.adapt_var_expr(&op_str, rhs.get_var_expr());
Lir と LirKind に adapt_var_expr() を実装しましょう。
impl<'tcx> Lir<'tcx> {
pub fn adapt_var_expr(&mut self, operation: &String, arg: &String, expr: Rc<RExpr<'tcx>>) {
self.kind.adapt_var_expr(operation, arg);
self.expr = expr;
}
}
impl<'tcx> LirKind<'tcx> {
pub fn adapt_var_expr(&mut self, operation: &String, arg: &String) {
self.set_var_expr(format!("({} {} {})", operation, self.get_var_expr(), arg));
}
}
複合代入演算(AssignOp)のサポート
複合代入演算子のサポートです。
REprKind に AssignOp を追加します。
AssignOp {
op: BinOp,
lhs: Rc<RExpr<'tcx>>,
rhs: Rc<RExpr<'tcx>>,
},
プリント関数や、Expr からの変換関数も適当に実装してください。
では AssignOp をシンボリック実行する処理を書きます。
match に AssignOp を追加しましょう。
LetStmt { pattern, initializer } => // LetStmt の処理
AssignOp { op, lhs, rhs } => // AssignOp の処理
AssignOp を処理する流れを示します。
- 右側の引数から値の式(LirKind)を生成
- 演算子から SMT 演算子を生成
- 左側の引数から VarId を取得
- VarId に対応する Lir に演算操作を適応
AssignOp は SMT 変数に対する処理の追加として扱います。
代入対象の変数は VarRef なので、左側の引数から id を取得します。
let rhs = // 右側の引数から値の式を生成
let op_str = Analyzer::bin_op_to_smt(op)?;
let id = // 左側の引数から VarId を取得
id を取得します。
match &expr.kind {
RExprKind::VarRef { id } => id.clone(),
_ => {
eprintln!("{expr:?}");
unreachable!()
}
}
取得した VarId に対応する変数に演算を適応します。
まず、env.var_map から Lir を取得します。
その後、LirKind::adapt_var_expr を呼び出します。
pub fn add_assumption(
&mut self, var_id: &LocalVarId, operation: String, arg: String, expr: Rc<RExpr<'tcx>>,
) {
let var = self.var_map.get_mut(var_id).expect("Variable not found");
var.adapt_var_expr(&operation, &arg, expr);
}
以上で、power.rs を検証するのに必要な全ての要素を実装できました。
Makefile を次のように修正し、実行していきましょう。
cargo build --manifest-path=t3modules/Cargo.toml --release
RUST_LIB_PATH=$(rustc --print target-libdir)
T3MODULES="./t3modules/target/release/libt3modules.rlib"
file = "power.rs"
cargo run $file -L "$RUST_LIB_PATH" --extern t3modules="$T3MODULES"
検証成功です！
(declare-const rand_power_L5_C9 Int)
(assert (distinct rand_power_L5_C9 0))
(assert (not (> (* rand_power_L5_C9 rand_power_L5_C9) 0)))
(check-sat)
Verification success!
まとめ
お疲れ様でした。
初めてのプログラム検証器実装どうでしたか？
検証器の全体像の確認、コードを検証するためにどう機能を追加したら良いのか、などなどわかるようになっていてくだされば幸いです。
この第1回では、"変数の宣言"、"アサイン"、"外部関数の呼び出し"を含むコードを、検証できるようになりました。
次回、第2回の目的は、"関数の戻り値"と"If"を含むコードを検証できるようになる。です。
今回で検証器に興味を持っていただいた方はまた、第2回でお会いしましょう。
-
プログラム検証器の種類とそれぞれの Rust で実装されている例が紹介されているサイト Rust verification tools ↩︎
-
rustc のドキュメントに Typed High-level Intermediate Representaion の説明が記載されている。 ↩︎
-
今回使用している Microsoft Research 作成の SMT ソルバ Z3 SMT solver ↩︎
-
TyCtxtとは: rustc はクエリシステムという形態を採用しているようです。TyCtxt は、コンパイルすべての情報を保持している、クエリシステムのコアとなる構造体であり、その構造体から関数を呼び出すことでコンパイルを進めているようです。 ↩︎
-
thir_body: 与えられた DefId に対応した THIR を取得することができる関数。バージョンによっては戻り値の方が異なっていたり、引数の型が異なっているため、最新のドキュメントを参考にして作成してください。 ↩︎
-
entry_fn()エントリの関数を取得する関数 ↩︎
-
あとでサポートしますが return は式ですので stmts の方に含まれます。 ↩︎
Discussion