🔮
Rust で預言を使ったプログラム検証器を自作しよう 3/3
Rust で預言を使ったプログラム検証器を自作しようブログの第3回になります。
読む前に第1回]、第2回の内容を読んでいただけると幸いです。
各回のリンク
- 第1回: Rust で預言を使ったプログラム検証器を自作しよう 1/3
- 第2回: Rust で預言を使ったプログラム検証器を自作しよう 2/3
- 第3回: Rust で預言を使ったプログラム検証器を自作しよう 3/3
この記事の目的
私たちは、第1回、第2回を通して検証器に "変数の宣言"、"アサイン"、"外部関数の呼び出し"、"ユーザ定義関数の呼び出し"、"関数の戻り値"、"If"、"If のアサイン" をサポートさせてきました。
今回は、"可変借用"のサポートを追加し、
以下のような可変借用を含むコードを検証できるようになることが目的です。
prophecy.rs
extern crate t3modules;
use t3modules::*;
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);
}
可変借用のサポートをするために預言というアプローチについて説明します。
預言とは
予言については、セキュリティキャンプ 2024 全国大会で講師を務めてくださった松下博士のスライドがわかりやすいです。
可変借用を預言で処理する流れを示します。
- 変数の可変借用を作成
- 変数の値の式を可変借用に継承
- 変数の値の式に預言をセットし、凍結
- 可変借用を操作
- 可変借用を開放
- 預言を確定
変数の可変借用を作成
まず、可変借用を行う対象の変数を特定し、その変数を可変借用（mutable reference）として扱えるようにします。
可変借用の作成時には、次の2つの処理を行います。
変数の値の式を可変借用に継承
可変借用を作成する際、対象の変数の現在の値の式を、可変借用 mut_ref に継承します。
let mut_ref = &mut var;
検証器の視点では、mut_ref に var の値の式をコピーしします。
- var_expr : 変数 var の現在の値を表す式
- mut_ref_expr : mut_ref に対応する値の式
次のように継承します。
mut_ref_expr = var_expr
変数の値の式に預言をセットし、凍結
預言は、変数の未来の値を表す未確定の値の式です。
可変借用中の変数は直接変更されず、預言をセットすることで「借用が解放された後に値がどうなるか」をシミュレートできます。
以下のような操作を行います。
- prophecy_var を作成（未来の値のプレースホルダー）
- 変数の値の式を prophecy_var に更新
- 変数を凍結（borrow による一時的な不変化）
// 預言用の新しい SMT 変数を生成
prophecy_var = new_symbolic_value()
// 変数の値を預言にセット
var_expr = prophecy_var
この時点で、変数は借用中のため変更できませんが、
prophecy_var により、将来の値をシミュレートできます。
可変借用を操作
可変借用 mut_ref に対して、通常の可変変数と同様に演算を行います。
*mut_ref = *mut_ref + 1;
可変借用を開放
元の変数に変更を反映するために、可変借用を開放します。
drop(mut_ref);
預言を確定
最後に、prophecy_var と var_expr の間に、(assert (=)) の制約条件を追加し、変数の最終的な値を決定します。
(assert (= prophecy_var var_expr))
この一連の預言による処理のアイデアにより、
これにより「借用期間中にもとの変数を書き換えずに変更する。」ことを再現することができます。
また、「Rust では可変借用が解除されると、その変数は新しい値を持つ。」ということを、「SMT で (assert (= prophecy_var var_expr)) という制約条件を追加する。」ことで再現できます。
"可変借用"のサポート
ここでは、可変借用を解析し、検証できるようにします。
可変借用を表現するために、LirKind に種類を追加します。
lir.rs
Aggregate { _ty: Ty<'tcx>, fields: Vec<LirKind<'tcx>> },
この LirKind は値の式を複数持つことができます。
この LirKind の値の式のインデックス 0 に元の変数の値の式を、インデックス 1 に預言をいれることで、可変借用とします。
set_var_expr や get_var_expr に加え、index で set と get をする関数を実装します。
Lir と LirKind の実装
lir.rs
#[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())
}
TyKind::Ref(_, ty, _) => LirKind::new_aggregate(ty, var_expr),
_ => return Err(AnalysisError::UnsupportedPattern(format!("Unknown TyKind: {ty:?}"))),
};
Ok(Self { kind, expr })
}
pub fn get_span(&self) -> Span { self.expr.span }
pub fn to_smt(&self) -> &String { self.kind.get_var_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) }
pub fn get_var_expr_by_index(&self, indices: Vec<usize>) -> &String {
self.kind.get_var_expr_by_index(indices)
}
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;
}
pub fn get_ty(&self) -> TyKind<'tcx> { self.kind.get_ty() }
}
#[derive(Clone)]
pub enum LirKind<'tcx> {
VarExpr { var_expr: String, ty: TyKind<'tcx> },
Aggregate { _ty: Ty<'tcx>, fields: Vec<LirKind<'tcx>> },
}
impl<'tcx> LirKind<'tcx> {
pub fn new(ty: TyKind<'tcx>, var_expr: String) -> Self { LirKind::VarExpr { var_expr, ty } }
pub fn new_aggregate(ty: Ty<'tcx>, args: Vec<String>) -> Self {
LirKind::Aggregate {
_ty: ty,
fields: args.iter().map(|arg| LirKind::new(*ty.kind(), arg.to_string())).collect(),
}
}
pub fn get_ty(&self) -> TyKind<'tcx> {
match self {
LirKind::VarExpr { ty, .. } => ty.clone(),
LirKind::Aggregate { fields, .. } => fields[0].get_ty(),
}
}
pub fn get_var_expr(&self) -> &String {
match self {
LirKind::VarExpr { var_expr, .. } => var_expr,
LirKind::Aggregate { fields, .. } => fields[0].get_var_expr(),
}
}
pub fn get_var_expr_by_index(&self, mut indices: Vec<usize>) -> &String {
match self {
LirKind::Aggregate { fields, .. } => {
fields[indices.remove(0)].get_var_expr_by_index(indices)
}
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,
LirKind::Aggregate { fields, .. } => fields[0].set_var_expr(new_var_expr),
}
}
pub fn set_var_expr_by_index(&mut self, new_var_expr: String, mut indices: Vec<usize>) {
match self {
LirKind::VarExpr { var_expr, .. } => *var_expr = new_var_expr,
LirKind::Aggregate { fields, .. } => {
fields[indices.remove(0)].set_var_expr_by_index(new_var_expr, indices)
}
}
}
pub fn adapt_var_expr(&mut self, operation: &String, arg: &String) {
self.set_var_expr(format!("({} {} {})", operation, self.get_var_expr(), arg));
}
}
また、可変借用のために対応が必要な ExprKind があるため RExprKind に追加します。
*var に対応する Deref、&, &mut に対応する Borrow を追加します。
rthir.rs
Deref {
arg: Rc<RExpr<'tcx>>,
},
Borrow {
arg: Rc<RExpr<'tcx>>,
}
変換する処理を書きます。
Deref は VarRef とあまり変わりません。
thir_reducer.rs
Deref { arg } => RExprKind::Deref { arg: // arg を RExprKind に変換する処理 },
Borrow { borrow_kind, arg } => // borrow_kind と arg から RExprKind に変換する処理
Borrow は borrow_kind の中身を処理する必要があります。
thir_reducer.rs
use rustc_middle::mir::MutBorrowKind;
match borrow_kind {
rustc_middle::mir::BorrowKind::Mut { kind } => match kind {
// TwoPhaseBorrow 検証に関係ないので中身を取り出す
MutBorrowKind::TwoPhaseBorrow => // TwoPhaseBrrow の取り出し RExprKind に変換する処理
MutBorrowKind::Default => RExprKind::Borrow { arg: // arg を RExprKind を変換する処理 },
_ => unimplemented!("MutBorrowKind::ClosureCpature is not supported"),
},
_ => {
unimplemented!("Other BorrowKind {borrow_kind:?} are not supported!")
}
}
TwoPhaseBorrow が何か気になる方は Rust Compiler Development Guide をどうぞ。
値の式の生成に使用するため、値の式を生成する処理の match に追加します。
gen_cstr.rs
Call { ty, args, .. } => // 関数の戻り値から値の式を生成
If { cond, then, else_opt } => // If から値の式を生成
Deref { arg } => // arg から値の式を生成
Borrow { arg } => // arg から値の式を生成
また、RExpr から変数の VarId を取得する処理に Deref を追加します。
util.rs
match &expr.kind {
RExprKind::VarRef { id } => id.clone(),
RExprKind::Deref { arg, .. } => {
if let RExprKind::VarRef { id } = &arg.kind {
*id
}
}
_ => unreachable!("{expr:?} is supplied to get id")
}
先ほどのコードが次のように表示できるようにしましょう。
prophecy.rs tree
DefId(0:5 ~ prophecy[f6f2]::take_max), params: [
Param {
param: Some(
Expr {
span: prophecy.rs:4:17: 4:18 (#0)
kind:
Pat {
PatKind {
Binding {
var: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).2))
ty: &'{erased} mut i32
subpattern: None
}
}
}
}
)
}
Param {
param: Some(
Expr {
span: prophecy.rs:4:33: 4:34 (#0)
kind:
Pat {
PatKind {
Binding {
var: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).4))
ty: &'{erased} mut i32
subpattern: None
}
}
}
}
)
}
]
body:
Expr {
span: prophecy.rs:14:5: 14:6 (#0)
kind:
Block {
stmts: [
Expr {
span: prophecy.rs:5:5: 13:6 (#0)
kind:
LetStmt {
pattern:
Expr {
span: prophecy.rs:5:9: 5:10 (#0)
kind:
Pat {
PatKind {
Binding {
var: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).58))
ty: &'{erased} mut i32
subpattern: None
}
}
}
}
,
initializer: Some(
Expr {
span: prophecy.rs:5:13: 13:6 (#0)
kind:
If {
cond:
Expr {
span: prophecy.rs:5:16: 5:24 (#5)
kind:
Binary {
op: Ge
lhs:
Expr {
span: prophecy.rs:5:16: 5:18 (#0)
kind:
Deref {
Expr {
span: prophecy.rs:5:17: 5:18 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).2))
}
}
}
}
rhs:
Expr {
span: prophecy.rs:5:22: 5:24 (#0)
kind:
Deref {
Expr {
span: prophecy.rs:5:23: 5:24 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).4))
}
}
}
}
}
}
then:
Expr {
span: prophecy.rs:5:25: 9:6 (#0)
kind:
Block {
stmts: [
Expr {
span: prophecy.rs:6:9: 6:27 (#0)
kind:
Call {
ty: FnDef(DefId(20:3 ~ t3modules[ddc1]::t3assert), [])
from_hir_call: true
fn_span: prophecy.rs:6:9: 6:27 (#0)
fun:
Expr {
span: prophecy.rs:6:9: 6:17 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: prophecy.rs:6:18: 6:26 (#0)
kind:
Binary {
op: Ge
lhs:
Expr {
span: prophecy.rs:6:18: 6:20 (#0)
kind:
Deref {
Expr {
span: prophecy.rs:6:19: 6:20 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).2))
}
}
}
}
rhs:
Expr {
span: prophecy.rs:6:24: 6:26 (#0)
kind:
Deref {
Expr {
span: prophecy.rs:6:25: 6:26 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).4))
}
}
}
}
}
}
]
}
}
Expr {
span: prophecy.rs:7:9: 7:18 (#0)
kind:
Call {
ty: FnDef(DefId(20:11 ~ t3modules[ddc1]::t3drop), [&'{erased} mut i32])
from_hir_call: true
fn_span: prophecy.rs:7:9: 7:18 (#0)
fun:
Expr {
span: prophecy.rs:7:9: 7:15 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: prophecy.rs:7:16: 7:17 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).4))
}
}
]
}
}
]
expr:
Expr {
span: prophecy.rs:8:9: 8:10 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).2))
}
}
}
}
else:
Expr {
span: prophecy.rs:12:9: 12:10 (#0)
kind:
Block {
stmts: [
Expr {
span: prophecy.rs:10:9: 10:26 (#0)
kind:
Call {
ty: FnDef(DefId(20:3 ~ t3modules[ddc1]::t3assert), [])
from_hir_call: true
fn_span: prophecy.rs:10:9: 10:26 (#0)
fun:
Expr {
span: prophecy.rs:10:9: 10:17 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: prophecy.rs:10:18: 10:25 (#0)
kind:
Binary {
op: Lt
lhs:
Expr {
span: prophecy.rs:10:18: 10:20 (#0)
kind:
Deref {
Expr {
span: prophecy.rs:10:19: 10:20 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).2))
}
}
}
}
rhs:
Expr {
span: prophecy.rs:10:23: 10:25 (#0)
kind:
Deref {
Expr {
span: prophecy.rs:10:24: 10:25 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).4))
}
}
}
}
}
}
]
}
}
Expr {
span: prophecy.rs:11:9: 11:18 (#0)
kind:
Call {
ty: FnDef(DefId(20:11 ~ t3modules[ddc1]::t3drop), [&'{erased} mut i32])
from_hir_call: true
fn_span: prophecy.rs:11:9: 11:18 (#0)
fun:
Expr {
span: prophecy.rs:11:9: 11:15 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: prophecy.rs:11:16: 11:17 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).2))
}
}
]
}
}
]
expr:
Expr {
span: prophecy.rs:12:9: 12:10 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).4))
}
}
}
}
}
}
)
}
}
]
expr:
Expr {
span: prophecy.rs:14:5: 14:6 (#0)
kind:
Borrow (
arg:
Expr {
span: prophecy.rs:14:5: 14:6 (#0)
kind:
Deref {
Expr {
span: prophecy.rs:14:5: 14:6 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:5 ~ prophecy[f6f2]::take_max).58))
}
}
}
}
)
}
}
}
DefId(0:7 ~ prophecy[f6f2]::main), params: [
]
body:
Expr {
span: prophecy.rs:17:11: 32:2 (#0)
kind:
Block {
stmts: [
Expr {
span: prophecy.rs:18:5: 18:34 (#0)
kind:
LetStmt {
pattern:
Expr {
span: prophecy.rs:18:9: 18:14 (#0)
kind:
Pat {
PatKind {
Binding {
var: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).8))
ty: i32
subpattern: None
}
}
}
}
,
initializer: Some(
Expr {
span: prophecy.rs:18:17: 18:34 (#0)
kind:
Call {
ty: FnDef(DefId(20:7 ~ t3modules[ddc1]::rand_int), [i32])
from_hir_call: true
fn_span: prophecy.rs:18:17: 18:34 (#0)
fun:
Expr {
span: prophecy.rs:18:17: 18:32 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: []
}
}
)
}
}
Expr {
span: prophecy.rs:19:5: 19:34 (#0)
kind:
LetStmt {
pattern:
Expr {
span: prophecy.rs:19:9: 19:14 (#0)
kind:
Pat {
PatKind {
Binding {
var: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).16))
ty: i32
subpattern: None
}
}
}
}
,
initializer: Some(
Expr {
span: prophecy.rs:19:17: 19:34 (#0)
kind:
Call {
ty: FnDef(DefId(20:7 ~ t3modules[ddc1]::rand_int), [i32])
from_hir_call: true
fn_span: prophecy.rs:19:17: 19:34 (#0)
fun:
Expr {
span: prophecy.rs:19:17: 19:32 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: []
}
}
)
}
}
Expr {
span: prophecy.rs:21:5: 21:20 (#0)
kind:
LetStmt {
pattern:
Expr {
span: prophecy.rs:21:9: 21:11 (#0)
kind:
Pat {
PatKind {
Binding {
var: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).22))
ty: &'{erased} mut i32
subpattern: None
}
}
}
}
,
initializer: Some(
Expr {
span: prophecy.rs:21:14: 21:20 (#0)
kind:
Borrow (
arg:
Expr {
span: prophecy.rs:21:19: 21:20 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).8))
}
}
)
}
)
}
}
Expr {
span: prophecy.rs:22:5: 22:20 (#0)
kind:
LetStmt {
pattern:
Expr {
span: prophecy.rs:22:9: 22:11 (#0)
kind:
Pat {
PatKind {
Binding {
var: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).28))
ty: &'{erased} mut i32
subpattern: None
}
}
}
}
,
initializer: Some(
Expr {
span: prophecy.rs:22:14: 22:20 (#0)
kind:
Borrow (
arg:
Expr {
span: prophecy.rs:22:19: 22:20 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).16))
}
}
)
}
)
}
}
Expr {
span: prophecy.rs:24:5: 24:30 (#0)
kind:
LetStmt {
pattern:
Expr {
span: prophecy.rs:24:9: 24:11 (#0)
kind:
Pat {
PatKind {
Binding {
var: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).38))
ty: &'{erased} mut i32
subpattern: None
}
}
}
}
,
initializer: Some(
Expr {
span: prophecy.rs:24:14: 24:30 (#0)
kind:
Call {
ty: FnDef(DefId(0:5 ~ prophecy[f6f2]::take_max), [])
from_hir_call: true
fn_span: prophecy.rs:24:14: 24:30 (#0)
fun:
Expr {
span: prophecy.rs:24:14: 24:22 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: prophecy.rs:24:23: 24:25 (#0)
kind:
Deref {
Expr {
span: prophecy.rs:24:23: 24:25 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).22))
}
}
}
}
Expr {
span: prophecy.rs:24:27: 24:29 (#0)
kind:
Deref {
Expr {
span: prophecy.rs:24:27: 24:29 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).28))
}
}
}
}
]
}
}
)
}
}
Expr {
span: prophecy.rs:25:5: 25:13 (#0)
kind:
AssignOp {
op: Add
lhs:
Expr {
span: prophecy.rs:25:5: 25:8 (#0)
kind:
Deref {
Expr {
span: prophecy.rs:25:6: 25:8 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).38))
}
}
}
}
rhs:
Expr {
span: prophecy.rs:25:12: 25:13 (#0)
kind:
Literal( lit: Spanned { node: Int(Pu128(1), Unsuffixed), span: prophecy.rs:25:12: 25:13 (#0) }, neg: false)
}
}
}
Expr {
span: prophecy.rs:27:5: 27:15 (#0)
kind:
Call {
ty: FnDef(DefId(20:11 ~ t3modules[ddc1]::t3drop), [&'{erased} mut i32])
from_hir_call: true
fn_span: prophecy.rs:27:5: 27:15 (#0)
fun:
Expr {
span: prophecy.rs:27:5: 27:11 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: prophecy.rs:27:12: 27:14 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).38))
}
}
]
}
}
Expr {
span: prophecy.rs:28:5: 28:15 (#0)
kind:
Call {
ty: FnDef(DefId(20:11 ~ t3modules[ddc1]::t3drop), [&'{erased} mut i32])
from_hir_call: true
fn_span: prophecy.rs:28:5: 28:15 (#0)
fun:
Expr {
span: prophecy.rs:28:5: 28:11 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: prophecy.rs:28:12: 28:14 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).22))
}
}
]
}
}
Expr {
span: prophecy.rs:29:5: 29:15 (#0)
kind:
Call {
ty: FnDef(DefId(20:11 ~ t3modules[ddc1]::t3drop), [&'{erased} mut i32])
from_hir_call: true
fn_span: prophecy.rs:29:5: 29:15 (#0)
fun:
Expr {
span: prophecy.rs:29:5: 29:11 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: prophecy.rs:29:12: 29:14 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).28))
}
}
]
}
}
Expr {
span: prophecy.rs:31:5: 31:21 (#0)
kind:
Call {
ty: FnDef(DefId(20:3 ~ t3modules[ddc1]::t3assert), [])
from_hir_call: true
fn_span: prophecy.rs:31:5: 31:21 (#0)
fun:
Expr {
span: prophecy.rs:31:5: 31:13 (#0)
kind:
ZstLiteral(user_ty: None)
}
args: [
Expr {
span: prophecy.rs:31:14: 31:20 (#0)
kind:
Binary {
op: Ne
lhs:
Expr {
span: prophecy.rs:31:14: 31:15 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).8))
}
}
rhs:
Expr {
span: prophecy.rs:31:19: 31:20 (#0)
kind:
VarRef {
id: LocalVarId(HirId(DefId(0:7 ~ prophecy[f6f2]::main).16))
}
}
}
}
]
}
}
]
expr: []
}
}
可変借用と預言の作成
可変借用と預言の作成の処理を実装します。
まず、LetStmt やアサインの Binding パターンの種類が借用であるか確認します。
借用である場合、かつ Mutability が Mut であれば、可変借用であると判断します。
sub.rs
match ty.kind() {
TyKind::Ref(_region, ref_ty, mutability) => match mutability {
Mutability::Not => // 今まで通りの処理
Mutability::Mut => // 可変借用の処理
},
_ => // 今まで通りの処理
}
LetStmt や アサインの initializer が可変借用であることがわかった後、initializer の種類を match で処理します。
sub.rs
if let Some(init) = initializer {
let name = Analyzer::span_to_str(&pattern.span);
match &init.kind {
~
}
}
可変借用の initializer ついては、処理が異なるので、
それぞれ処理を順番でサポートします。
- Borrow
- VarRef
- Deref
- Call
- If のアサイン
Borrow のサポート
Borrow が可変借用の initializer となっているのは、可変借用を作成する場合です。
まず、Borrow でマッチしましょう。
sub.rs
RExprKind::Borrow { arg } => {
// 預言の変数名を宣言
let prophecy_var = // Span から名前を作成
// Borrow から値の式を生成する
}
可変借用を作成するための処理なので、arg が変数への参照を表す VarRef であることを前提に処理します。
sub.rs
if let RExprKind::VarRef { id } = arg.kind {
// 預言を作成する処理
}
次の順番で預言の値を作成します。
- 対象の変数を取得
- 変数から現在の値の式を取得
- 預言を SMT 変数として登録
- 変数の値の式に預言をセット
- 可変借用を作成
- 値の式のインデックス 0 に変数の値の式
- 値の式のインデックス 1 に預言
- 可変借用を登録
そのまま実装します。
sub.rs
// 対象の変数を取得
let mut_init = env.var_map.get_mut(&id).expect("var not found in Mutable");
// 変数から現在の値の式を取得
let var_expr = mut_init.get_var_expr().clone();
// 預言を SMT 変数として登録
env.smt_vars.push((prophecy_var.clone(), *ty.kind()));
// 変数の値の式に預言をセット
mut_init.set_var_expr(prophecy_var.clone());
// 可変借用を作成
let lir = Lir { kind: LirKind::Aggregate { _ty: ty, fields: vec![var_expr, prophecy_var] }, expr: pattern) };
// 可変借用を登録
self.var_map.insert(*var_id, lir);
これで、Borrow のサポートができました。
VarRef のサポート
VarRef が可変借用の initializer となっているのは、関数の引数が &mut となっている時です、可変借用が移動します。
可変借用が移動する時も預言を追加します。
そのため、処理は Borrow と変わず、預言を作成します。
Borrow の時に使っていた arg の代わりに、init を使います。
match を少し編集します。
sub.rs
RExprKind::Borrow { .. } | RExprKind::VarRef { .. } => {
let var_ref = if let RExprKind::Borrow { arg } = &init.kind { arg } else { &init };
// VarRef から値の式を生成する処理
}
Deref のサポート
Deref については可変借用が移動します。
Deref を match に追加します。
arg は基本的に VarRef なので、Some(arg)を initializer として、もう一度可変借用を作成する処理を呼び出します。
sub.rs
RExprKind::Deref { arg } => {
// Some(arg) を initializer として可変借用の処理
}
Call のサポート
Call が可変借用の initializer となっているのは、可変借用が返却値である場合です。
関数の戻り値は今まで通り処理し、値の式を生成します。
可変借用を作成しますが、値の式は関数の返却値の値の式を引き継ぎます。
sub.rs
let return_value = // 関数から値の式を生成
// 可変借用を作成
let lir = Lir { kind: return_value, expr: pattern };
// 可変借用を登録
self.var_map.insert(*var_id, lir);
これで、Call のサポートができました。
If のアサインのサポート
If が可変借用の initializer となっているのは、可変借用がアサインされる場合です。
通常の If のアサインの処理との違いは、預言の値の結合も含まれることだけです。
If のアサインの処理の最後にインデックス 1 を (ite) で結合する処理を追加すれば完了です。
sub.rs
then_value.set_var_expr_by_index(
Analyzer::value_to_ite(
cond_str,
then_value.get_var_expr_by_index(vec![1]),
else_value.get_var_expr_by_index(vec![1]),
),
vec![1],
);
これで、Call のサポートができました。
以上で、可変借用への対応は終わりです。
可変借用の開放をする関数 t3drop の実装
検証用クレート t3modules に t3drop を実装します。
中身は特にいりません。
lib.rs
pub fn t3drop<T>(_: T) {}
t3drop で可変借用を開放し預言を確定させる
t3drop を処理します。
t3drop で行うことは、可変借用を開放し、預言を確定させることです。
もとの Rust のコードでは、スコープを抜けると借用が開放されますが、drop() を用いて明示的に解放することもできます。
この検証器では借用の開放方法に drop() の方を採用し、可変借用の解除をしつつ、予言を確定するという役割を持たせます。
では、external 関数の処理に t3drop も追加しましょう。
sub.rs
if fn_info[0] == "t3modules" {
match fn_info[1].as_str() {
"t3assert" => // t3assert だった時の処理
"t3assume" => // t3assume だった時の処理
// t3drop を追加
"t3drop" => // t3drop だった時の処理
_ => unreachable!(),
}
行うことは、env へ制約条件の追加です。
可変借用の値の式と預言をイコールとする制約条件を追加することで、予言を確定させます。
special.rs
if let RExprKind::VarRef { id } = args[0].kind {
let arg = env.var_map.get(&id).expect("Var not found in t3drop");
env.add_assume(format!(
"(= {} {})",
arg.get_var_expr(),
arg.get_var_expr_by_index(vec![1])
))
}
以上で、可変借用と預言の作成、可変借用の開放、預言の確定を実装しました。
これで、預言を用いて可変借用を検証する準備が整いました。
では、検証してみましょう。
検証成功です！
(declare-const rand_prophecy_L18_C9 Int)
(declare-const rand_prophecy_L19_C9 Int)
(declare-const prophecy_L21_C9 Int)
(declare-const prophecy_L22_C9 Int)
(declare-const prophecy_L4_C17 Int)
(declare-const prophecy_L4_C33 Int)
(assert (>= rand_prophecy_L18_C9 rand_prophecy_L19_C9))
(assert (not (>= rand_prophecy_L18_C9 rand_prophecy_L19_C9)))
(check-sat)
Verification success!
(declare-const rand_prophecy_L18_C9 Int)
(declare-const rand_prophecy_L19_C9 Int)
(declare-const prophecy_L21_C9 Int)
(declare-const prophecy_L22_C9 Int)
(declare-const prophecy_L4_C17 Int)
(declare-const prophecy_L4_C33 Int)
(assert (not (>= rand_prophecy_L18_C9 rand_prophecy_L19_C9)))
(assert (not (< rand_prophecy_L18_C9 rand_prophecy_L19_C9)))
(check-sat)
Verification success!
(declare-const rand_prophecy_L18_C9 Int)
(declare-const rand_prophecy_L19_C9 Int)
(declare-const prophecy_L21_C9 Int)
(declare-const prophecy_L22_C9 Int)
(declare-const prophecy_L4_C17 Int)
(declare-const prophecy_L4_C33 Int)
(assert (=> (>= rand_prophecy_L18_C9 rand_prophecy_L19_C9) (= rand_prophecy_L19_C9 prophecy_L4_C33)))
(assert (=> (not (>= rand_prophecy_L18_C9 rand_prophecy_L19_C9)) (= rand_prophecy_L18_C9 prophecy_L4_C17)))
(assert (= prophecy_L4_C17 prophecy_L21_C9))
(assert (= prophecy_L4_C33 prophecy_L22_C9))
(assert (= (+ (ite (>= rand_prophecy_L18_C9 rand_prophecy_L19_C9) rand_prophecy_L18_C9 rand_prophecy_L19_C9) 1) (ite (>= rand_prophecy_L18_C9 rand_prophecy_L19_C9) prophecy_L4_C17 prophecy_L4_C33)))
(assert (not (distinct prophecy_L21_C9 prophecy_L22_C9)))
(check-sat)
Verification success!
まとめ
これで、3 回にも及ぶ「Rust で預言を使ったプログラム検証器を自作しよう」ブログは終わりとなります。お疲れ様でした。やはり「預言」を使ったプログラム検証器、ロマンがありませんか？
これを気に検証器の楽しさを感じていただけていれば幸いです。
拙い文章、拙いコードであったかと思われますが、最後までお付き合いいただきありがとうございました。
今後の学習について
ブログ自体はここで終わってしまいましたが、まだまだ追加できる機能があります。
ので、筆者が考える今後追加したら良い機能について紹介します。
loop
ひとつは loop です。プログラムといえば、逐次実行、条件分岐、繰り返しですよね。現在、この検証器は逐次実行と条件分岐をサポートしていますが繰り返しをサポートしていません。
そのため、次は繰り返しをサポートしてみてはどうでしょうか？
リスト
もうひとつは、配列です。可変借用をサポートするために、複数の値の式を持つことができる Aggregate をサポートしました。
これを発展させて、配列もサポートしてみてはどうでしょうか？
言語にはさまざまな機能があります。検証器に好きな機能を追加して楽しみましょう！
では、またどこかの記事でお会いしましょう！
Discussion