From 18200f55edf14e5360c9095736710ae689032f6d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Nov 2017 15:14:49 -0800 Subject: [PATCH] add bit-vector over/underflow checks to Python API, #1364 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 59 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index a247d0a3a..5ccab92dd 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -3993,6 +3993,65 @@ def BVRedOr(a): _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx) +def BVAddNoOverflow(a, b, signed): + """A predicate the determines that bit-vector addition does not overflow""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) + +def BVAddNoUnderflow(a, b, signed): + """A predicate the determines that signed bit-vector addition does not underflow""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) + +def BVSubNoOverflow(a, b): + """A predicate the determines that bit-vector subtraction does not overflow""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) + + +def BVSubNoUnderflow(a, b, signed): + """A predicate the determines that bit-vector subtraction does not underflow""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) + +def BVSDivNoOverflow(a, b): + """A predicate the determines that bit-vector signed division does not overflow""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) + +def BVSNegNoOverflow(a): + """A predicate the determines that bit-vector unary negation does not overflow""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx) + +def BVMulNoOverflow(a, b, signed): + """A predicate the determines that bit-vector multiplication does not overflow""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) + + +def BVMulNoUnderflow(a, b, signed): + """A predicate the determines that bit-vector signed multiplication does not underflow""" + if __debug__: + _z3_assert(is_bv(a), "Arguments should be bit-vectors") + _z3_assert(is_bv(b), "Arguments should be bit-vectors") + return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) + + + ######################################### # # Arrays