用 Z3 检查溢出 [英] Check overflow with Z3

问题描述

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

I'm new to Z3 and I was checking the online python tutorial.

然后我想我可以检查 BitVecs 中的溢出行为.

Then I thought I could check overflow behavior in 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)

and I was expecting [y = 7, x = 7] (i.e. when values are equal but successors are not because x + 1 will be 0 and y + 1 will be 8)

但 Z3 回答 [y = 0, x = 0].

But Z3 answers [y = 0, x = 0].

我做错了什么?

推荐答案

我不认为你做错了什么，看起来 BV2Int 有问题:

I don't think you're doing anything wrong, looks like BV2Int is buggy:

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

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

Z3py proves the first one, but gives the counter-example x=0 for the second. That doesn't sound right. (The only explanation might be some weird Python thing, but I don't see how.)

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

Also note that the model you get will depend on whether + treats the bit-vector as a signed number in the Python bindings, which I believe is the case. However, BV2Int might not do so, treating it as an unsigned value. This would further complicate the matters.

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

In any case, looks like BV2Int is not quite kosher; I'd stay away from it until there's an official answer from the Z3 folks.

这篇关于用 Z3 检查溢出的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！