Is it possible to change the argument types and the return value of a z3 bitvector operation after it has been created?
For example, given:
x = BitVec('x', 32)
y = BitVec('y', 32)
mul = x * y`
Is there a way to substitute x and y in mul with bitvectors of a different size and have mul return a bitvector of the new size?
Or in more formal terms, can I programatically convert mul from:
(declare-fun bvmul ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
to
(declare-fun bvmul ((_ BitVec 64) (_ BitVec 64)) (_ BitVec 64))
Calling substitute doesn't work:
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
The error message is odd but I think it's failing on the last part of the assert, because x64.sort() doesn't match what mul expects.
It seems like I would have to create a new expression which uses the variables with the new size. But I need to be able to do this to any binary bitvector operation after it has been constructed and without knowing ahead of time if it's an add, multiply, etc.
The only plausible solution I've found is looking at decl().kind() and use that to create the new expression. Something like:
(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
...
Is there a better way? Thanks.
PS: I'm using z3 4.5.
You cannot change the types in any meaningful way once they are created. If you want to convert a 32-bit value to a 64-bit value, then you should either zero-extend it (if unsigned), or sign-extend it. Something like:
mul = ZeroExt(64, x) * ZeroExt(64, y)