介绍
给定一个用 C++ 编写的简单函数，如下所示：
int func(int x, int y)
{
if (x < 3)
{
y = 4;
if (x < 4)
{
y = y + 2;
}
else
{
x = x + 4;
}
}
else
{
x = x + 1;
}
return x + y;
};
问题
如何注释程序以执行以下操作z3？
- 检测死代码。(x = x + 4)
- 生成测试用例（代码覆盖率）。
- 分析不变量。
Pre&Post代码检查。
我做了什么？
我知道我需要识别代码中每个块的每个路径：
PATH 1 for (y = 4) => (x < 3)
PATH 2 for (y = y + 2) => (x < 3) ^ (x < 4)
PATH 3 for (x = x + 4) => (x < 3) ^ (x >= 4)
PATH 4 for (x = x + 1) => (x >= 3)
然后，如果我使用 Z3，我可以检查这些路径中是否有任何一个unsat推断与它们相关的代码块将是Dead code.
我需要什么帮助？
- 对于死码检测：
我真的不知道如何在z3. 我应该为每条路径使用不同的求解器吗？像这样：
from z3 import *
x = Int('x')
y = Int('y)
s1 = Solver()
s2 = Solver()
s3 = Solver()
s4 = Solver()
s1.add(x < 3)
s2.add(x < 3, x < 4)
s3.add(x < 3, x >= 4)
s4.add(x >= 3)
s1.check() // sat
s2.check() // sat
s3.check() // unsat
s4.check() // sat
我认为这是检测死代码的低效方法。如果有一百种不同的路径怎么办？所以必须有更好的方法来做到这一点。
- 对于分析不变量：
同样，我应该为每个代码块使用不同的求解器吗？例如：
from z3 import *
s1 = Solver()
s2 = Solver()
s3 = Solver()
s4 = Solver()
x0 = Int('x0')
y0 = Int('y0)
x1 = Int('x1')
y1 = Int('y1')
// Path 1
s1.add(x0 < 3)
s1.add(y0 == 4)
s1.add(y1 == y0 + 2)
s1.check()
s1.model()
// Path 2
s2.add(x0 < 3)
s2.add(y0 == 4)
s2.add(x1 == x0 + 4);
s2.check()
s2.model()
// Path 3
s3.add(x0 < 3)
s3.add(y0 == 4)
s3.add(x1 == x0 + 4);
s3.check()
s3.model()
// Path 4
s3.add(x0 >= 3)
s3.add(x1 == x0 + 1);
s3.check()
s3.model()
- 而且我不知道如何
Generate test cases做Pre和Post代码检查
最后，我的问题实际上是，如何使用 z3 针对不同的场景分析程序，例如Dead Code Detection、Invariant analysis、Test-case generation等。更具体地说，我正在寻找这方面的最佳实践。中的示例代码z3-solver将有很大帮助。更优选地，我想看看如何改进z3我上面提供的示例代码。
谢谢你的帮助