程序等价

既然程序是一种语言,跟自然语言一样,同一个意思有可能会有两种表达方式。直觉上,如果把两个程序看做黑盒子,这样就可以用测试的方法来判断它们对于每个输入是否有一样的输出,但测试毕竟只能在有限的空间上,不能穷尽所有的可能性。类似的,用测试的方法来观察两对象的行为是否一致,经典的案例就是图灵测试了,在图灵测试中,相当于测试一个机器和其他人是否等价。

验证程序等价这个问题,是不可判定的。对于一些简单的程序来说,验证两个程序等价并不是难事。简单的说,验证两个程序等价,只要证明语义对等就行了。

我们用以下的例子来说明,对于简单的程序,我们可以将程序转换为命题逻辑里的公式,然后用求解器来求解,将验证程序等价问题转化为判断公式的可满足性。

1
2
3
4
5
6
7
8
9
// p1
if (!a && !b) h();
else if (!a) g();
else f();

// p2
if(a) f();
else if(b) g();
else h();

这两个程序片段(p1 和 p2)比较简单,如果需要验证它们是否等价,首先,需要将 if-else 语句转变成 f-then-else,这一步是为了跟命题逻辑对应起来。

1
2
3
4
5
6
7
8
9
// p1'
if (!a && !b) then h()
else if (!a) then g()
else f()

// p2'
if(a) then f()
else if(b) then g()
else h()

第二步,将程序中的变量和子函数看做布尔变量,这些布尔变量实际上就是符号变量,比如 p1 和 p2 程序中的变量和函数 a, b, h(), g(), f() 。我们分别用布尔变量 a,b,h,g,fa, b, h, g, f 来表示。程序中的if-then-else 语句,可以直接用命题逻辑来替代:

\it{if} \ x\ \it{then}\ y\ \it{else}\ z \equiv (x \land y) \lor (\neg x \land z)

因此上述的程序片段 p1 可以转换为

ϕp1=(¬a¬b)(¬(¬a¬b)((¬ag)(af)))\phi_{p_{1}} = (\neg a \land \neg b) \land (\neg(\neg a \land \neg b) \land ((\neg a \land g) \lor (a \land f)))

p2 可以转换为

ϕp2=(af)(¬a((bg)(¬bh)))\phi_{p_{2}} = (a \land f) \lor (\neg a \land((b \land g) \lor (\neg b \land h)))

验证程序 p1 和 p2 是否等价,只需要检查以下命题逻辑公式就行了:

\phi_{p_{1}} \iff \phi_{p_{2}}

用 SMT 来验证程序等价

我们利用提供 python 接口的 z3 求解器,来求解上述的公式。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
// equ.py
from z3 import *
a, b, g, h, f = Bools('a b g h f')
p1 = Bool('p1')
p2 = Bool('p2')

p1 = Or(And(Not(a),Not(b),h), And(Or(a,b),Or(And(a,f), And(Not(a),g))))

p2 = Or(And(a, f), And(Not(a), Or(And(b, g), And(Not(b), h))))

s = Solver()
s.add(p1 == p2)
print(s.check())
print(s.model())
--------------------------------
# 运行 z3 求解
$ ~python3 equ.py
$ sat
$ [h = False, b = False, a = False, f = False, g = False]

对于简单的程序,可以将其转化为 SMT 公式,对于复杂的程序,还需要将比较两个程序的在特定点的不等式。

验证程序等价算法

验证程序等价,往往被应用在验证编译器的安全性中。编译器里涉及到将高级语言转换为不同的低级中间语言,这就要求转换过程是正确的,也就是需要保证两种语言的行为一致,程序等价问题是不可判定的,这使得编译器的验证是个滚烫的山芋。

在现代等价分析器(equivalence checker)中,一般的框架是这样的。

  1. equivalence checking algorithm: generates proof obligations

  2. invariants infer algorithm: infer invariants that relate the intermediate states of the two programs being compared for equivalence

[sat18论文] Effective use of SMT solvers for Program
Equivalence Checking through Invariant
Sketching and Query Decomposition