java - z3:对 z3 位 vector 加法中的 Java 补码溢出和下溢进行建模

Question

我正在尝试对 Java 32 位 int 算术建模。我正在尝试使用 z3 位 vector 来实现此目的。我正在使用不稳定分支中的 Z3 Java API。

但是，我不知道如何从 z3 获得正确的溢出行为。我想模拟这种行为:

0b01111111111111111111111111111111 + 1 == 0b10000000000000000000000000000000
Integer.MAX_VALUE + 1 == Integer.MIN_VALUE

我可以创建一个值为 0b10000000000000000000000000000000 的位 vector ，但是当我使用 BitVecNum.getInt() 时出现异常。

我运行以下代码:

((BitVecNum) 
   ctx.mkBVAdd(ctx.mkBV(Integer.MAX_VALUE, 32), ctx.mkBV(1, 32))
   .simplify()).getInt()

我收到异常 com.microsoft.z3.Z3Exception: Numeral is not an int

如果我执行以下操作:

((int)((BitVecNum) 
    ctx.mkBVAdd(ctx.mkBV(Integer.MAX_VALUE, 32), ctx.mkBV(1, 32))
    .simplify()).getLong()); 

我得到了我想要的结果-2147483648。

有什么建议吗？

Answer 1

这种情况有点令人困惑，因为 Z3 将所有位 vector 视为无符号，但 getInt/getLong 函数看起来会返回有符号值。发生的情况是，MAX_VALUE+1 被正确计算，得到 2147483648(可以用 32 位无符号整数表示)，但是当调用 getInt 时，它发现这个无符号值不适合有符号整数。

此问题源于Java不支持无符号基本类型，因此相应的Z3函数(如getUInt和getULong)在Java API中不可用。我的建议是始终假设 Z3 中的位 vector 是无符号的，并使用更广泛的数据类型(例如通过 getLong 的技巧)来解决这个问题。这本质上也是其他 Java 程序员所做/建议的，例如 here和 there .