简介
给定一个用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(
- 生成测试用例(代码覆盖率(
- 分析不变量
- CCD_ 2&
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代码。
感谢您的帮助
如果只关注一个问题，堆栈溢出效果最好。使用z3，所有这些都是可行的，但要问的重要问题是，你是否只对这一个给定的程序感兴趣，或者你是否对构建适用于任意C程序的东西感兴趣？
如果你对后者感兴趣，那么这是一项更难解决的任务，你真的应该看看符号执行/分析论文。如果你只对这个程序感兴趣，那么你应该进行路径分析：对于死代码，你想知道是否有任何代码路径是不可访问的，即特定的If语句是否从不接受其then或else分支。请注意，应该只使用一个解算器，而不是为每条路径使用不同的解算器。可以增量使用解算器，就像对控制流进行深度优先搜索一样。
您所追求的技术通常被视为DART研究的一部分，DART研究还包括测试用例生成。从阅读本文开始：https://web.eecs.umich.edu/~weimerw/2014-6610/reading/p23-godefroid.pdf
同样，如果你在一个特定的方面提出非常具体和集中的问题，堆栈溢出效果最好。一旦你复习了上面的论文，我相信你会有更好的问题！