From 9e916edcb04e35bb39a43a42911f3e062f003bcc Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 7 Jun 2018 15:40:04 +0100 Subject: [PATCH] z3.py: add overflow checks to PB API --- src/api/python/z3/z3.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 7657fb347..ab2217e13 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -90,6 +90,9 @@ def _z3_assert(cond, msg): if not cond: raise Z3Exception(msg) +def _z3_check_cint_overflow(n, name): + _z3_assert(ctypes.c_int(n).value == n, name + " is too large") + def open_log(fname): """Log interaction to a file. This function must be invoked immediately after init(). """ Z3_open_log(fname) @@ -8128,6 +8131,7 @@ def _pb_args_coeffs(args, default_ctx = None): _args, sz = _to_ast_array(args) _coeffs = (ctypes.c_int * len(coeffs))() for i in range(len(coeffs)): + _z3_check_cint_overflow(coeffs[i], "coefficient") _coeffs[i] = coeffs[i] return ctx, sz, _args, _coeffs @@ -8137,6 +8141,7 @@ def PbLe(args, k): >>> a, b, c = Bools('a b c') >>> f = PbLe(((a,1),(b,3),(c,2)), 3) """ + _z3_check_cint_overflow(k, "k") ctx, sz, _args, _coeffs = _pb_args_coeffs(args) return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx) @@ -8146,6 +8151,7 @@ def PbGe(args, k): >>> a, b, c = Bools('a b c') >>> f = PbGe(((a,1),(b,3),(c,2)), 3) """ + _z3_check_cint_overflow(k, "k") ctx, sz, _args, _coeffs = _pb_args_coeffs(args) return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx) @@ -8155,6 +8161,7 @@ def PbEq(args, k, ctx = None): >>> a, b, c = Bools('a b c') >>> f = PbEq(((a,1),(b,3),(c,2)), 3) """ + _z3_check_cint_overflow(k, "k") ctx, sz, _args, _coeffs = _pb_args_coeffs(args) return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)