使用Z3检查溢出

Question

我是Z3的新手，正在查看在线Python教程。

然后我想检查BitVecs的溢出行为。

我写了这段代码：

x = BitVec('x', 3)
y = Int('y')

solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))

我原本期望的是 [y = 7, x = 7]（即当值相等但后继不同时，因为 x + 1 将为 0，y + 1 将为 8）。

但是 Z3 的答案是 [y = 0, x = 0]。

我做错了什么？

- Braulio Horta

Answer 1

我不认为你做错了什么，看起来 BV2Int 有bug：

 x = BitVec('x', 3)
 prove(x <= 3)
 prove(BV2Int(x) <= 3)

Z3py证明了第一个问题，但对于第二个问题给出了反例x=0。这听起来不太对。（唯一的解释可能是一些奇怪的Python问题，但我不知道是哪种情况。）此外，请注意所得到的模型将取决于在Python绑定中+是否将位向量作为带符号数字处理，我认为是这种情况。然而，BV2Int可能不这样做，将其视为无符号值。这会进一步复杂化事情。无论如何，看起来BV2Int不是很可靠，直到Z3团队有正式答案之前，最好避免使用它。

- alias

Answer 2

对于其他关注此事的人，这个问题似乎已经在某个时候得到了解决。我刚刚使用最新版本的z3重新运行了这个示例（在最初发布几年后），它确实返回了7,7。

- Owl Owl