z3 - 用 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]。

我究竟做错了什么？

Answer 1

我认为您没有做错任何事情，看起来像 BV2Int错误：

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

Z3py 证明了第一个，但给出了第二个的反例x=0。这听起来不对。（唯一的解释可能是一些奇怪的 Python 东西，但我不明白如何。）

另请注意，您获得的模型将取决于是否+将位向量视为 Python 绑定中的有符号数，我相信是这种情况。但是，BV2Int可能不会这样做，将其视为无符号值。这会使事情进一步复杂化。

无论如何，看起来BV2Int不太干净；在 Z3 人员给出正式答复之前，我会远离它。

Answer 2

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