为什么使用 Z3 的符号执行会导致错误？

Question

我正在尝试使用基于 SMT 求解器 Z3 的符号执行逻辑生成测试用例。

我有以下代码。

void foo(int a, int b, int c){
    int x = 0, y = 0, z = 0;
    if(a){
        x = -2;
    }

    if (b < 5){
        if (!a && c) { y = 1; }
        z = 2;
    }

    assert(x + y + z != 3);
}

现在SMT Solving过程中出现错误，产生的错误日志如下。

(set-option :produce-unsat-cores true)
(set-option :produce-models true)
(set-option :produce-proofs true)
(define-sort bot () Int)

(declare-const sv_1 Int)
(declare-const sv_5 Int)
(define-fun strcmp ((a String) (b String)) Int (ite (= a b) 0 1))

(assert (! (not (= sv_1 0)) :named __a0))
(assert (! (< sv_5 5) :named __a1))
(assert (! (not (not (= sv_1 0))) :named __a2))
(assert (! (not (not (= (+ (+ (bvneg 2) 0) 2) 3))) :named __a3))
(check-sat)
(get-unsat-core)
(get-model)

我已经用这段代码做了一些测试。

如果我在断言函数中不使用x,y,z，就没有错误。

如果第一个'if statement'为真（即a != 0），那么程序永远不会进入'if (!a && c)语句。如果我删除其中一个 'if statements'，则没有错误。但我不明白为什么会出现此错误。谁能向我解释为什么 Z3 无法解决这个问题？谢谢。

Answer 1

您没有告诉我们您收到的确切错误是什么，所以我假设它来自 z3 而不是您工具链的其他部分。让我们运行您通过 z3 发布的 SMTLib 程序。当我这样做时，z3 告诉我有一个“排序不匹配：”

(error "line 13 column 38: operator is applied to arguments of the wrong sort")

这是因为你有这条线：

(assert (! (not (not (= (+ (+ (bvneg 2) 0) 2) 3))) :named __a3))

尤其是表达式 (bvneg 2)。函数 bvneg 是位向量取反，但 2 是一个整数，而不是位向量值。您想改用常规否定。因此，将该行更改为：

(assert (! (not (not (= (+ (+ (- 0 2) 0) 2) 3))) :named __a3))

随着这一变化，z3 说：

unsat
(__a3)
(error "line 16 column 10: model is not available")

太棒了；所以现在你有 unsat，unsat-core 是 __a3。最后一行的错误可以忽略，是因为你调用了get-model但是问题无法解决，所以没有模型显示

现在，您可能想知道为什么这是 unsat，也许您希望它是可满足的？您还没有告诉我们您是如何将 C 函数转换为 SMTLib 的，而且您似乎使用了一些未命名的工具来执行此操作，也许是您自己创建的工具之一。该工具显然有一个错误，因为它创建了我们上面修复的 bvneg 表达式，也许它不那么值得信任！但是我们看看为什么z3认为这个问题是unsat.

它归结为您的工具生成的这两行：

(assert (! (not (= sv_1 0)) :named __a0))
(assert (! (not (not (= sv_1 0))) :named __a2))

让我们通过删除注释来简化这些，为了清楚起见，我将 sv_1 重命名为 a，因为这似乎是变量的来源。这给了我们：

(assert (not (= a 0)))
(assert (not (not (= a 0))))

让我们简单一点：

(assert (distinct a 0))
(assert (not (distinct a 0)))

（在 SMTLib 中，(distinct x y) 表示 (not (= x y))。）

现在我们看到了问题；你有两个断言，第一个说 a 不是 0，第二个说 它是不是 a 不是 0 的情况。显然，这两个断言相互冲突，这就是为什么 z3 告诉你 unsat.

其实还有一个冲突的来源。另一个断言简化为：

(assert (not (not (= (+ (+ (- 0 2) 0) 2) 3)

其中，如果你做算术，说：

(assert (= 0 3))

这显然不是真的。（这就是为什么 z3 告诉您 unsat 核心是 __a3；这就是为什么整组假设无法满足的根本原因。请注意，unsat-cores 不是唯一的，而 z3不保证它会给你一个最小的集合。所以它可以告诉你 (__a0 __a2) 以及 unsat-core；但那是一个单独的讨论。）

因此，根据您生成的 SMTLib，z3 正在做正确的事情（在上述更正之后。）

为什么您的工具会为 C 程序生成此 SMTLib，这是我们无法帮助您解决的问题，除非您告诉我们更多有关您如何生成该输出或此中间工具实际执行的操作的信息。我的粗略猜测是它实际上生成了一堆测试用例，最终它说“我没有更多的测试用例要生成”，所以一切都很好；但是为什么它会生成 (get-model) 调用似乎存在一些问题；或者为什么它会执行不正确的 bvneg 调用。但除此之外，您必须咨询为您生成此 SMTLib 的工具的开发人员以进行进一步调试。

为什么使用 Z3 的符号执行会导致错误？

Why is this Symbolic Execution with Z3 resulting in an error?

c

z3

static-analysis

symbolic-execution