如何使用 z3-solver 注释程序以检测死代码？

Question

简介

给定一个用 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中对程序进行注解？

1. 检测死码。 (x = x + 4)
2. 生成测试用例（代码覆盖率）。
3. 分析不变量。
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 代码。

感谢您的帮助

Answer 1

如果您只关注一个问题，Stack-overflow 效果最好。所有这些都可以使用 z3 实现，但要问的重要问题是您是否只对这个给定程序感兴趣，或者您是否有兴趣构建适用于任意 C 程序的东西？

如果您对后者感兴趣，那么这是一项更难解决的任务，您应该真正查看符号执行/分析论文。如果你只对这个程序感兴趣，那么你应该跟进一个路径分析：对于死代码，你想知道是否有任何代码路径不可达，即，如果一个特定的 if 语句永远不会占用它的then 或else 分支。请注意，您应该只使用一个求解器，而不是为每条路径使用不同的求解器。您可以逐步使用求解器，就像对控制流进行深度优先搜索一样。

您所追求的技术通常被视为 DART 研究的一部分，该研究还包括测试用例生成。从阅读本文开始：https://web.eecs.umich.edu/~weimerw/2014-6610/reading/p213-godefroid.pdf

同样，如果您针对某个特定方面提出非常具体且非常集中的问题，则堆栈溢出效果最好。一旦您查看了上述论文，我相信您会有更好的问题！