0

我正在尝试使用基于 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 解决过程中发生错误，生成的错误日志如下所示。

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

4

1 回答 1

3

你没有告诉我们你得到了什么确切的错误，所以我假设它来自 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，第二个说不是，不是a0。显然，这两个断言相互冲突，这就是 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 的工具的开发人员以进行进一步调试。

于 2021-04-28T15:40:29.750 回答