用SMT solver驗證程序等價

02-02

過去十年，SMT(Satisfiability modulo theories)求解器在形式化方法、程序語言、軟體工程、以及計算機安全、計算機系統等領域得到了廣泛應用。。

本文以「驗證程序等價性」的例子，介紹SMT 求解器的簡單運用。這裡將等價性定義為「給定相同合法輸入，有相同輸出「。考慮如下2個函數：

int power3_A(int in) {n int i, out_a;n out_a = in; n for (i = 0; i < 2; i++) n out_a = out_a * in;n return out_a;n}nnint power3_B(int in) {n int out_b;n out_b = (in * in) * in; n return out_b; n}n

如何證明power3_A, power3_B幹了同一件事情？一個傳統方法是寫測試用例，但是這2個程序的輸入int型整數取值範圍很大....

我們考慮基於形式邏輯的程序驗證。這個例子比較簡單，可以對power3_A做循環展開，然後用邏輯公式分別編碼power3_A, power3_B的程序語義（需要引入中間變數）。以上兩個程序分別編碼為 $varphi_a, varphi_b$ ，也就是

$begin{align} out0_a &= in land out1_a &= out0_a * in land out2_a &= out1_a * in end{align}$

和 $out0_b = (in * in) * in$

下面是證明「給定相同輸入，有相同輸出」。等價性就轉化為判斷以下公式是永真的（VALID）

$varphi_a land varphi_b Rightarrow out2_a = out0_b$

而要證明任意命題 $F$ 永真，可以對 $F$ 取反，然後證明 $neg F$ 不可滿足(unsatisfiable)。

$F text{ valid} equiv neg F text { unsatisfiable }$

於是問題轉化為了判斷公式的可滿足性。SMT solver可以接受特定問題域公式如實數方程約束，判斷其可滿足性。我們需要建模整數(32位/64位)和乘法*，正巧很多SMT solver支持的bit-vector theory剛好適合。

附上代碼，使用z3 SMT solver的Python API的

from z3 import *n# 創建solver和邏輯變數nsolver = Solver()nout0a, out1a, out2a, out0b, In = BitVecs("out0a out1a out2a out0b In", 32)nn# 編碼A程序語義nfa = And(out0a == In, out1a == out0a * In, out2a == out1a * In)nn# 編碼B程序語義nfb = (out0b == In * In * In)nn# 證明程序等價，需要證明G永真(VALID)nG = Implies(And(fa, fb), out2a == out0b)nn# 轉化為可滿足性問題：將G取反後判斷其是否不可滿足(UNSAT)nsolver.add(Not(G))nprint solver.check()n

附錄：「假如我想使用SMT solver娛樂甚至做一些研究，「

需要學習數理邏輯么？ 不需要
需要懂得SAT問題么？ 不需要
需要了解CSP求解么？不需要
需要接觸符號計算么？ 不需要
...