更改 z3 位向量操作的类型

Question

是否可以在创建 z3 位向量操作后更改参数类型和 return 值？

例如，给定：

x = BitVec('x', 32)
y = BitVec('y', 32)
mul = x * y`

有没有办法用不同大小的位向量替换 mul 中的 x 和 y 并使 mul return 的位向量新尺寸？

或者用更正式的术语来说，我可以通过编程方式将 mul 从：

转换为

 (declare-fun bvmul ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))

到

 (declare-fun bvmul ((_ BitVec 64) (_ BitVec 64)) (_ BitVec 64))

呼叫替代不起作用：

 x64 = BitVec('x64', 64)
 y64 = BitVec('y64', 64)
 substitute(mul, (x, x1), (y, y1))
 ...
 _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")
 Z3Exception: Z3 invalid substitution, expression pairs expected

错误消息很奇怪，但我认为它在 assert 的最后一部分失败了，因为 x64.sort() 与 mul 期望的不匹配。

看来我必须创建一个使用具有新大小的变量的新表达式。但是我需要能够在构建之后对任何二进制位向量操作执行此操作，并且事先不知道它是加法、乘法等。

我发现的唯一可行的解决方案是查看 decl().kind() 并使用它来创建新表达式。类似于：

(child1, child2) = target_op.children()
new_child1 = ZeroExt(64 - child1.size(), child1)
new_child2 = ZeroExt(64 - child2.size(), child2)

op_kind = target_op.decl().kind()
if op_kind == Z3_OP_BMUL:
     return new_child1 * new_child2
elif op_kind == Z3_OP_BADD:
     return new_child1 + new_child2
...

有没有更好的方法？谢谢。

PS: 我正在使用 z3 4.5。

Answer 1

类型一旦创建就无法以任何有意义的方式进行更改。如果要将 32 位值转换为 64 位值，则应该对其进行零扩展（如果无符号）或对其进行符号扩展。类似于：

 mul = ZeroExt(64, x) * ZeroExt(64, y)

看这里：ZeroExt and SignExt

更改 z3 位向量操作的类型

Change the type of a z3 bitvector operation

smt

z3

z3py