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是 buggy :

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

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

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

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