z3 bitvector overflow checking from python?

Question

The C API for z3 has functions such as Z3_mk_bvadd_no_overflow, but these do not seem to be available from the Python API. Before I start hacking to solve this I'd just like to verify that this is the case and also request that these be added to the official version.

I'm trying adding things like this to z3.py, but so far haven't managed to get the details right. Suggestions about where I'm going wrong would be appreciated. I'm working on the contrib branch.

def Bvadd_no_overflow(a, b, si, ctx=None):
    """Create a Z3 bvadd_no_overflow expression.

    """
    ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
    # argh can't hard-code the 32
    s = BitVecSort(32,ctx)
    a = s.cast(a)
    b = s.cast(b)
    # this function requires a bool as the last argument but is it a python bool, a
    # z3 bool, or what?
    return BitVecRef(Z3_mk_bvadd_no_overflow(ctx.ref(), a.as_ast(), b.as_ast(), 1), ctx) 

Answer 1

Indeed, it seems those functions not available in the higher level API yet. Something along these lines may do the job for you:

def bvadd_no_overflow(x, y, signed=False):
    assert x.ctx_ref()==y.ctx_ref()
    a, b = z3._coerce_exprs(x, y)
    return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed))

Here's an example of using this function, which works for me:

q = BitVec('q', 32)
r = BitVec('r', 32)
s.add(bvadd_no_overflow(q, r))
print(s)

which prints

[Extract(32, 32, ZeroExt(1, q) + ZeroExt(1, r)) == 0]

(Internally, this is represented as taking the + of two bit-vectors and then extracting the most significant bit.)

Answer 2

I encountered the same problem 8 years after the last answer was posted. So here is an update:

The Z3 Python API now has a function BVAddNoOverflow which is defined as such:

def BVAddNoOverflow(a, b, signed):
    """A predicate the determines that bit-vector addition does not overflow"""
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(),
                   b.as_ast(), signed), a.ctx)

Equivalent functions also exist for overflow and underflow on other arithmetic operations: BVSubNoOverflow, BVMulNoUnderflow, etc.

I post this here for posterity as this is where I landed when trying to answer a similar question.