🔮
Rust で預言を使ったプログラム検証器を自作しよう 2/3
Rust で預言を使ったプログラム検証器を自作しようブログの第2回になります。
読む前に第1回の内容を読んでいただけると幸いです。
各回のリンク
- 第1回: Rust で預言を使ったプログラム検証器を自作しよう 1/3
- 第2回: Rust で預言を使ったプログラム検証器を自作しよう 2/3
- 第3回: Rust で預言を使ったプログラム検証器を自作しよう 3/3
この記事の目的
この回は、第1回で作成した一言語機能のみサポートした検証器に機能を追加することを目的としています。
前回の実装で、検証器は、"変数の宣言"、"アサイン"、"外部関数の呼び出し"、言語機能をサポートしています。
これに、"ユーザ定義関数の呼び出し"、"関数の戻り値"、"If"、"If のアサイン"のサポートを追加します。
それでは、始めましょう。
"ユーザ定義関数の呼び出し"のサポート
ここでは、ユーザ定義関数の呼び出しを解析し、検証できるようにします。
次のようなコードを処理できることを目指します。
user_function.rs
extern crate t3modules;
use t3modules::*;
fn test_function(n: i32) { t3assert(n * n > 0); }
fn main() {
let a = rand_int::<i32>();
t3assume(a > 0);
test_function(a);
}
第1回で保留していた以下の local 関数の処理部分を実装していきましょう。
sub.rs
match ty.kind() {
TyKind::FnDef(def_id, ..) => {
if let Some(fun) = self.get_local_fn(def_id) {
// local 関数の処理
} else {
let fn_info = self.get_fn_info(def_id);
self.analyze_external_fn(fn_info, args, env)
}
}
関数の RTHIR と args(引数) を用いて local 関数を処理します。
local 関数を処理する方法を示します。
- params と args を対応付ける
- body を処理
形的には次のようになります。
main 関数の処理の際は params は存在しませんでしたが、その他の関数には params が存在する可能性があるので、それを処理します。
body の処理は同じです。
なので、params を処理する機能を実装します。
まず、params と args を対応づけます。
params と args をイテレートしましょう。
Pat はまだ Binding のみでも大丈夫です。
core.rs
// params と args を zip でイテレートする
for (param, arg) in params.iter().zip(args.iter()) {
// param から pattern を取り出す
if let Some(pattern) = ¶m.pat {
// pattern を Pat であるあることを前提に処理
if let RExpr { kind: Pat { kind }, .. } = pattern.as_ref() {
// pattern の処理
}
}
}
PatKind を match で処理します
core.rs
use RPatKind::*;
match kind {
Binding { ty, var, .. } => {
// Binding の処理
}
}
Binding の処理は、LetStmt の initializer の処理と同じです。
pattern と、arg を initialier として、ty、var を LetStmt の処理に与えましょう。
これで params と arg の対応付け処理の実装が終わりました。
短い実装でしたが、これで完了です。
実際に実行してみましょう。
検証成功です！
(declare-const rand_user_function_L7_C9 Int)
(assert (> rand_user_function_L7_C9 0))
(assert (not (> (* rand_user_function_L7_C9 rand_user_function_L7_C9) 0)))
(check-sat)
Verification success!
"関数の戻り値"のサポート
ここでは、関数の戻り値を解析し、検証できるようにします。
この章では、次のようなコードを処理できることを目指します。
return_value.rs
extern crate t3modules;
use t3modules::*;
fn test_function(n: i32) -> i32 {
t3assert(n > 0);
let m = n * n;
t3assert(m > 0);
m
}
fn main() {
let a = rand_int::<i32>();
t3assume(a > 0);
let b = test_function(x);
t3assert(b > 0);
}
関数の戻り値は値の式の生成を目的としているので、rand 関数のサポートの際に保留していた以下の local 関数の処理を実装していきましょう。
gen_cstr.rs
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"),
}
local 関数の処理についてです。
params に関しては、ユーザ定義関数の呼び出しの時と同じです。
body は値の式の生成に使用します。
body から値の式を生成する方法を示します。
- 戻り値を初期化
- stmts をイテレートし、それぞれ処理
- expr から値の式を生成し戻り値に代入する。
return 式は今回サポートしません。
まず戻り値を初期化します。
gen_cstr.rs
// return_value 戻り値 を初期化
let mut return_value = LirKind::new(TyKind::Int(IntTy::I32), String::new());
gen_cstr.rs
// expr を Block であることを前提に処理
if let RExpr { kind: RExprKind::Block { stmts, expr }, .. } = body.as_ref() {
// stmts をそれぞれ処理します。
for stmt in stmts {
// stmt を処理
}
// expr をアンラップし、関数から返却される値の式として使用します。
if let Some(expr) = expr {
return_value = // expr から値の式を生成する処理
}
}
Ok(return_value)
これで実装終了です。
では実際に実行してみましょう。
検証成功です！
(declare-const rand_return_value_L14_C9 Int)
(assert (> rand_return_value_L14_C9 0))
(assert (not (> rand_return_value_L14_C9 0)))
(check-sat)
Verification success!
(declare-const rand_return_value_L14_C9 Int)
(assert (> rand_return_value_L14_C9 0))
(assert (not (> (* rand_return_value_L14_C9 rand_return_value_L14_C9) 0)))
(check-sat)
Verification success!
(declare-const rand_return_value_L14_C9 Int)
(assert (> rand_return_value_L14_C9 0))
(assert (not (> (* rand_return_value_L14_C9 rand_return_value_L14_C9) 0)))
(check-sat)
Verification success!
"If"のサポート
ここでは、If を解析し、検証できるようにします。
この章では、次のようなコードを処理できることを目指します。
if.rs
extern crate t3modules;
use t3modules::*;
fn main() {
let a = rand_int::<i32>();
let b;
if a >= 0 {
let c = rand_int::<i32>();
t3assume(c > 0);
b = a + c;
t3assert(b > 0);
} else {
let c = rand_int::<i32>();
t3assume(c < 0);
b = a + c;
t3assert(b < 0);
}
t3assert(b * b > 0);
}
まず If の前に、まず Assign をサポートします。
RExprKind に If を追加します。
thir.rs
Assign {
lhs: Rc<RExpr<'tcx>>,
rhs: Rc<RExpr<'tcx>>,
}
match に Assign を追加します。
プリント関数や、Expr からの変換関数も適当に実装してください。
core.rs
Assign { lhs, rhs } => // Assign の処理
AssignOp { op, lhs, rhs } => // AssignOp の処理
Assign の処理です。
sub.rs
let constraint = // rhs から値の式を生成する処理
// lhs に対応する Lir を取得
let var = env.var_map.get_mut(&Analyzer::expr_to_id(lhs)).expect("Assign target not found");
// Lir に対して値の式を設定
var.set_var_expr(constraint.get_var_expr().into());
Ok(())
これで Assign のサポートは終了です。
それでは、If をサポートします。
REprKind に If を追加します。
rthir.rs
If {
cond: Rc<RExpr<'tcx>>,
then: Rc<RExpr<'tcx>>,
else_opt: Option<Rc<RExpr<'tcx>>>,
}
プリント関数や、Expr からの変換関数も適当に実装してください。
Expr からの変換関数に関しては、ExprKind::Use が含まれるので取り除いた方がいいです。
次のように表示されるよう変換します。
if.rs tree
Tautrust!
DefId(0:5 ~ if[30c5]::main), params: [
]
body:
Expr {
span: if.rs:4:11: 21:2 (#0)
kind:
Block {
stmts: [
Expr {
span: if.rs:5:5: 5:30 (#0)
kind:
LetStmt {
pattern:
Expr {
span: if.rs:5:9: 5:10 (#0)
kind:
Pat {
PatKind {
Binding {
var: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).8))
ty: i32
subpattern: None
}
}
}
}
,
initializer: Some(
Expr {
span: if.rs:5:13: 5:30 (#0)
kind:
Call {
ty: FnDef(DefId(20:7 ~ t3modules[ddc1]::rand_int), [i32])
from_hir_call: true
fn_span: if.rs:5:13: 5:30 (#0)
fun:
Expr {
span: if.rs:5:13: 5:28 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: []
}
}
)
}
}
Expr {
span: if.rs:6:5: 6:11 (#0)
kind:
LetStmt {
pattern:
Expr {
span: if.rs:6:9: 6:10 (#0)
kind:
Pat {
PatKind {
Binding {
var: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).11))
ty: i32
subpattern: None
}
}
}
}
,
initializer: None
}
}
Expr {
span: if.rs:8:5: 18:6 (#0)
kind:
If {
cond:
Expr {
span: if.rs:8:8: 8:14 (#5)
kind:
Binary {
op: Ge
lhs:
Expr {
span: if.rs:8:8: 8:9 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).8))
}
}
rhs:
Expr {
span: if.rs:8:13: 8:14 (#0)
kind:
Literal( lit: Spanned { node: Int(Pu128(0), Unsuffixed), span: if.rs:8:13: 8:14 (#0) }, neg: false)
}
}
}
then:
Expr {
span: if.rs:8:15: 13:6 (#0)
kind:
Block {
stmts: [
Expr {
span: if.rs:9:9: 9:34 (#0)
kind:
LetStmt {
pattern:
Expr {
span: if.rs:9:13: 9:14 (#0)
kind:
Pat {
PatKind {
Binding {
var: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).25))
ty: i32
subpattern: None
}
}
}
}
,
initializer: Some(
Expr {
span: if.rs:9:17: 9:34 (#0)
kind:
Call {
ty: FnDef(DefId(20:7 ~ t3modules[ddc1]::rand_int), [i32])
from_hir_call: true
fn_span: if.rs:9:17: 9:34 (#0)
fun:
Expr {
span: if.rs:9:17: 9:32 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: []
}
}
)
}
}
Expr {
span: if.rs:10:9: 10:24 (#0)
kind:
Call {
ty: FnDef(DefId(20:4 ~ t3modules[ddc1]::t3assume), [])
from_hir_call: true
fn_span: if.rs:10:9: 10:24 (#0)
fun:
Expr {
span: if.rs:10:9: 10:17 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: if.rs:10:18: 10:23 (#0)
kind:
Binary {
op: Gt
lhs:
Expr {
span: if.rs:10:18: 10:19 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).25))
}
}
rhs:
Expr {
span: if.rs:10:22: 10:23 (#0)
kind:
Literal( lit: Spanned { node: Int(Pu128(0), Unsuffixed), span: if.rs:10:22: 10:23 (#0) }, neg: false)
}
}
}
]
}
}
Expr {
span: if.rs:11:9: 11:18 (#0)
kind:
Assign {
lhs:
Expr {
span: if.rs:11:9: 11:10 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).11))
}
}
rhs:
Expr {
span: if.rs:11:13: 11:18 (#0)
kind:
Binary {
op: Add
lhs:
Expr {
span: if.rs:11:13: 11:14 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).8))
}
}
rhs:
Expr {
span: if.rs:11:17: 11:18 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).25))
}
}
}
}
}
}
Expr {
span: if.rs:12:9: 12:25 (#0)
kind:
Call {
ty: FnDef(DefId(20:3 ~ t3modules[ddc1]::t3assert), [])
from_hir_call: true
fn_span: if.rs:12:9: 12:25 (#0)
fun:
Expr {
span: if.rs:12:9: 12:17 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: if.rs:12:18: 12:24 (#0)
kind:
Binary {
op: Ge
lhs:
Expr {
span: if.rs:12:18: 12:19 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).11))
}
}
rhs:
Expr {
span: if.rs:12:23: 12:24 (#0)
kind:
Literal( lit: Spanned { node: Int(Pu128(0), Unsuffixed), span: if.rs:12:23: 12:24 (#0) }, neg: false)
}
}
}
]
}
}
]
expr: []
}
}
else:
Expr {
span: if.rs:13:12: 18:6 (#0)
kind:
Block {
stmts: [
Expr {
span: if.rs:14:9: 14:34 (#0)
kind:
LetStmt {
pattern:
Expr {
span: if.rs:14:13: 14:14 (#0)
kind:
Pat {
PatKind {
Binding {
var: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).61))
ty: i32
subpattern: None
}
}
}
}
,
initializer: Some(
Expr {
span: if.rs:14:17: 14:34 (#0)
kind:
Call {
ty: FnDef(DefId(20:7 ~ t3modules[ddc1]::rand_int), [i32])
from_hir_call: true
fn_span: if.rs:14:17: 14:34 (#0)
fun:
Expr {
span: if.rs:14:17: 14:32 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: []
}
}
)
}
}
Expr {
span: if.rs:15:9: 15:24 (#0)
kind:
Call {
ty: FnDef(DefId(20:4 ~ t3modules[ddc1]::t3assume), [])
from_hir_call: true
fn_span: if.rs:15:9: 15:24 (#0)
fun:
Expr {
span: if.rs:15:9: 15:17 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: if.rs:15:18: 15:23 (#0)
kind:
Binary {
op: Lt
lhs:
Expr {
span: if.rs:15:18: 15:19 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).61))
}
}
rhs:
Expr {
span: if.rs:15:22: 15:23 (#0)
kind:
Literal( lit: Spanned { node: Int(Pu128(0), Unsuffixed), span: if.rs:15:22: 15:23 (#0) }, neg: false)
}
}
}
]
}
}
Expr {
span: if.rs:16:9: 16:18 (#0)
kind:
Assign {
lhs:
Expr {
span: if.rs:16:9: 16:10 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).11))
}
}
rhs:
Expr {
span: if.rs:16:13: 16:18 (#0)
kind:
Binary {
op: Add
lhs:
Expr {
span: if.rs:16:13: 16:14 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).8))
}
}
rhs:
Expr {
span: if.rs:16:17: 16:18 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).61))
}
}
}
}
}
}
Expr {
span: if.rs:17:9: 17:24 (#0)
kind:
Call {
ty: FnDef(DefId(20:3 ~ t3modules[ddc1]::t3assert), [])
from_hir_call: true
fn_span: if.rs:17:9: 17:24 (#0)
fun:
Expr {
span: if.rs:17:9: 17:17 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: if.rs:17:18: 17:23 (#0)
kind:
Binary {
op: Lt
lhs:
Expr {
span: if.rs:17:18: 17:19 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).11))
}
}
rhs:
Expr {
span: if.rs:17:22: 17:23 (#0)
kind:
Literal( lit: Spanned { node: Int(Pu128(0), Unsuffixed), span: if.rs:17:22: 17:23 (#0) }, neg: false)
}
}
}
]
}
}
]
expr: []
}
}
}
}
Expr {
span: if.rs:20:5: 20:24 (#0)
kind:
Call {
ty: FnDef(DefId(20:3 ~ t3modules[ddc1]::t3assert), [])
from_hir_call: true
fn_span: if.rs:20:5: 20:24 (#0)
fun:
Expr {
span: if.rs:20:5: 20:13 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: if.rs:20:14: 20:23 (#0)
kind:
Binary {
op: Gt
lhs:
Expr {
span: if.rs:20:14: 20:19 (#0)
kind:
Binary {
op: Mul
lhs:
Expr {
span: if.rs:20:14: 20:15 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).11))
}
}
rhs:
Expr {
span: if.rs:20:18: 20:19 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ if[30c5]::main).11))
}
}
}
}
rhs:
Expr {
span: if.rs:20:22: 20:23 (#0)
kind:
Literal( lit: Spanned { node: Int(Pu128(0), Unsuffixed), span: if.rs:20:22: 20:23 (#0) }, neg: false)
}
}
}
]
}
}
]
expr: []
}
}
では If の処理をしていきます。
match に If を追加しましょう。
core.rs
Assign { lhs, rhs } => // Assign の処理
AssignOp { op, lhs, rhs } => // AssignOp の処理
If { cond, then, else_opt } => // If の処理
RExprKind::If を処理する流れ
then を then ブロック、else_opt を Some(else ブロック) とし、If を処理する方法を示します。
現在の環境を current_env とします。
- If の条件式, cond を文字列に変換
- then ブロックを処理
- then ブロック用の Env, then_env を作成
- then_env に条件式を制約条件として追加
- then_env を使って then ブロックをシンボリック実行
- else_opt を処理
- else ブロックが存在すれば、else_env を作成
- else_env に (not 条件式) を制約条件として追加
- else_env を使って else ブロックをシンボリック実行
- current_env に、 then_env と else_env を条件 cond 下で結合する。
If の条件式, cond を文字列に変換
まず条件式を文字列に変換します。操作としては、値の式を生成する処理を行い、返却された Lir から var_expr を取り出す流れで良いです。
sub.rs
let cond_str: String = // cond から生成した値の式から get_var_expr()
then ブロックを処理
then ブロック用の Env, then_env を生成
current_env から then ブロック解析用の環境 then_env を生成します。env をそのまま clone すれば良いでしょう。
sub.rs
let mut then_env = env.clone()
then_env に cond_str を制約条件として追加
env の add_assum を使用しましょう。
sub.rs
then_env.add_assume(cond_str.clone());
then_env を使って then ブロックをシンボリック実行
then_env を用いて Body を解析する処理を行えば良いです。
else ブロックを処理
if let で else_opt を開いて then ブロックと同様の処理をすれば良いです。
current_env に、 then_env と else_env を条件 cond 下で結合する。
この時点で、then_env と else_env にはそれぞれのブロック内での操作が記録されています。
それらを、条件式を用いて current_env に結合することで、If を表現します。
env に then と else を 結合する処理を実装しましょう。
処理の流れを示します。
- SMT 変数リストを結合
- 各環境での操作に条件式を適応
- then ブロックの環境に対して、条件式をそのまま適応
- else ブロックの環境に対して、条件式の否定（not 条件式）を適応
- 各パスの制約条件に対して imply（=>）を追加
- 制約条件リストの結合
- 前処理済みの then ブロックと else ブロックそれぞれの制約条件リストを現在の環境に追加
- 変数辞書の結合
- 既存の変数に対して then ブロックと else ブロックでの状態を確認
- then ブロックと else ブロックがある場合
- 両方の値の式が同じであれば変更なし
- 異なる場合は if-then-else式（ite）を生成して結合
- then ブロックだけで、else ブロックがない場合
- 現在の状態とthen部の状態を結合
- それ以外の場合は現在の状態を維持
SMT 変数リストを結合
then, else ブロック内で新しく宣言された SMT 変数を current_env に追加します。
rnv.rs
// len を取得
len = current_env.smt_vars.len();
current_env.smt_vars.extend_from_slice(&then_env.smt_vars[len..]);
if let Some(else_env) = else_env {
current_env.smt_vars.extend_from_slice(&else_env.smt_vars[len..]);
}
各環境での操作に条件式を適応
まず、結合の前準備として then、else ブロック内で新たに追加された制約条件に、If の条件式を適応します。
env.rs
// len を取得
len = current_env.path.len();
// current_env の path の長さを len とし、len 番目以降の制約条件を、新たに追加された制約条件とする
// then_env の処理
for assume in &mut then_env.path[len..] {
*assume = format!("(=> {cond_str} {assume})");
}
// else_env の処理
if let Some(else_env) = &mut else_env {
for assume in &mut then_env.path[len..] {
*assume = format!("(=> {cond_str} {assume})");
}
}
制約条件リストの結合
次に前処理をした新たに追加された制約条件を current_env に追加します。
env.rs
// 分岐時に If の条件式が制約条件についかされているため len + 1
current_env.path.extend_from_slice(&then_env.path[len + 1..]);
if let Some(else_env) = else_env {
current_env.path.extend_from_slice(&else_env.path[len + 1..]);
}
変数辞書の結合
最後に変数辞書の結合を行います。
then ブロックと else ブロック内で、既存の変数に対して新しく行われた操作を結合します。
新しい変数辞書を作成し、結合処理を行った Lir を insert していきます。
env.rs
let mut new_var_map = Map::new();
for (var_id, current_lir) in current_env.var_map.iter_mut() {
new_lir // var_id, cond, current_lir, then_env, else_env を用いて Lir を結合
// 結合後の Lir を新しい変数辞書に登録
new_var_map.insert(*var_id, new_lir);
}
current_env.var_map = new_var_map;
Lir を結合します。
結合は then ブロックも else ブロック両方がある場合、then ブロックのみがある場合で別れます。
その状態を、current_var_map に含まれる VarId で各ブロックの var_env から get できるかで判断します。
env.rs
match (then_env.var_map.get(var_id), else_env.as_ref().and_then(|e| e.var_map.get(var_id)))
{
(Some(then_lir), Some(else_lir)) => {
// cond で then_lir, else_lir を current_lir に結合
}
(Some(then_lir), None) => // cond で then_lir を current_lir に 結合
_ => unreachable()!;
}
then_env, else_env がある場合の処理です。
まず新しく行われた操作があるかを、それぞれの値の式の比較により確かめます。
変更があった場合 if-then-else式（ite）を生成して結合します。
env.rs
if current_lir.get_var_expr() != then_lir.get_var_expr()
or current_lir.get_var_expr() != else_lir.get_var_expr()
{
let var_expr = format!("(ite {} {} {})",
cond, then_lir.get_var_expr(), else_lir.get_var_expr());
current_lir.set_var_expr(var_expr);
}
then_env のみがある場合の処理です。
先と同様に値の式を比較し、変更があれば、current_lir と else_lir を ite で繋ぎます。
env.rs
if current_lir.get_var_expr() != then_lir.get_var_expr() {
let var_expr = format!("(ite {} {} {})", cond, then_lir.get_var_expr(), current_lir.get_var_expr());
current_lir.set_var_expr(var_expr);
}
以上で、環境の結合処理が全て終わり、If が処理できるようになりました。
では検証していきましょう。
検証成功です！
(declare-const rand_if_L5_C9 Int)
(declare-const rand_if_L9_C13 Int)
(assert (>= rand_if_L5_C9 0))
(assert (> rand_if_L9_C13 0))
(assert (not (> (+ rand_if_L5_C9 rand_if_L9_C13) 0)))
(check-sat)
Verification success!
(declare-const rand_if_L5_C9 Int)
(declare-const rand_if_L14_C13 Int)
(assert (not (>= rand_if_L5_C9 0)))
(assert (< rand_if_L14_C13 0))
(assert (not (< (+ rand_if_L5_C9 rand_if_L14_C13) 0)))
(check-sat)
Verification success!
(declare-const rand_if_L5_C9 Int)
(declare-const rand_if_L9_C13 Int)
(declare-const rand_if_L14_C13 Int)
(assert (=> (>= rand_if_L5_C9 0) (> rand_if_L9_C13 0)))
(assert (=> (not (>= rand_if_L5_C9 0)) (< rand_if_L14_C13 0)))
(assert (not (> (* (ite (>= rand_if_L5_C9 0) (+ rand_if_L5_C9 rand_if_L9_C13) (+ rand_if_L5_C9 rand_if_L14_C13)) (ite (>= rand_if_L5_C9 0) (+ rand_if_L5_C9 rand_if_L9_C13) (+ rand_if_L5_C9 rand_if_L14_C13))) 0)))
(check-sat)
Verification success!
"If のアサイン"のサポート
ここでは、If を解析し、検証できるようにします。
この章では、次のようなコードを処理できることを目指します。
if.rs
extern crate t3modules;
use t3modules::*;
fn main() {
let a = rand_int::<i32>();
let c = if a >= 0 {
let b = a + 5;
t3assert(b >= 0);
b
} else {
let b = x - 5;
t3assert(b < 0);
b * -1
};
t3assert(c > 0);
}
If から値の式を生成します。
処理自体は else ブロックが必ず存在すること意外 If の時とあまり変わりません。
If アサインを処理する方法を示します。
- If の条件式, cond を文字列に変換
- then ブロックを処理
- then ブロック用の Env, then_env を作成
- then_env に条件式を assume として追加
- then_env を使って then ブロックから値の式を生成
- else_opt を処理
- else ブロック用の Env, else_env を作成
- else_env に (not 条件式) を assume として追加
- else_env を使って else ブロックから値の式を生成
- current_env に、 then_env と else_env を条件 cond 下で結合する。
- then と else の値の式を (ite) で結合し新しい値の式を生成し、Lir にして返却
次にコードを示します。
env.rs
let cond_str = // cond を文字列に変換
// then ブロックを処理する準備
let mut then_env = env.clone();
then_env.add_assume(cond_str.clone());
let mut then_value = // then ブロックから値の式を生成
// else ブロックを処理する準備
let else_block = else_opt.expect("Else block of if assign initializer not found");
let mut else_env = env.clone();
else_env.add_assume(format!("(not {cond_str})"));
let else_value = // else ブロックから値の式を生成
// env を結合
// 値の式をセット
then_value.set_assume(Analyzer::value_to_ite(
cond_str,
then_value.get_assume(),
else_value.get_assume(),
));
Ok(then_value)
これで準備が整いました。
検証しましょう。
検証成功です！
(declare-const rand_if_assign_L5_C9 Int)
(assert (>= rand_if_assign_L5_C9 0))
(assert (not (>= (+ rand_if_assign_L5_C9 5) 0)))
(check-sat)
Verification success!
(declare-const rand_if_assign_L5_C9 Int)
(assert (not (>= rand_if_assign_L5_C9 0)))
(assert (not (< (- rand_if_assign_L5_C9 5) 0)))
(check-sat)
Verification success!
(declare-const rand_if_assign_L5_C9 Int)
(assert (not (> (ite (>= rand_if_assign_L5_C9 0) (+ rand_if_assign_L5_C9 5) (* (- rand_if_assign_L5_C9 5) -1)) 0)))
(check-sat)
Verification success!
まとめ
お疲れ様でした。
"関数の戻り値"や"If"などをサポートし、検証器らしくなってきたと思います。
できることが増えていくことを楽しんでいただけたら嬉しいです。
この、第2回では、"関数の戻り値"と"If"を含むコードを検証できるようになりました。
次回の第3回は、ついに"予言を使った可変借用"をサポートします。
また次回でお会いしましょう。
Discussion