为什么这个带有 Z3 的符号执行会导致错误？

如何解决为什么这个带有 Z3 的符号执行会导致错误？

我正在尝试使用基于 SMT Solver 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)

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

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

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

解决方法

您没有告诉我们您得到的确切错误是什么，所以我假设它来自 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 is not 0，第二个断言 not {{1 }} 不是 a。显然，这两个断言相互冲突，这就是 z3 告诉您 0 的原因。

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

unsat

如果你做算术，它会说：

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

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

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

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