""" The purpose of this test file is to do bounded model checking of the IntBound methods with Z3. The approach is to generate random bounds, then perform operations on them, and ask Z3 whether the resulting bound is a sound approximation of the result. """ import pytest import sys import gc from rpython.rlib.rarithmetic import LONG_BIT, r_uint, intmask, ovfcheck from rpython.jit.metainterp.optimizeopt.intutils import ( IntBound, unmask_one, unmask_zero, next_pow2_m1, lowest_set_bit_only, leading_zeros_mask, flip_msb, msbonly, ) from rpython.jit.metainterp.optimize import InvalidLoop from rpython.jit.metainterp.optimizeopt.test.test_intbound import knownbits_and_bound_with_contained_number from rpython.jit.metainterp.optimizeopt.test.test_z3checktests import z3_pymod, z3_pydiv try: import z3 from hypothesis import given, strategies, assume, example except ImportError: pytest.skip("please install z3 (z3-solver on pypi) and hypothesis") def BitVecVal(value): return z3.BitVecVal(value, LONG_BIT) def BitVec(name): return z3.BitVec(name, LONG_BIT) def z3_with_reduced_bitwidth(width): def dec(test): assert test.func_name.endswith("logic") # doesn't work for code in intutils.py def newtest(*args, **kwargs): global LONG_BIT old_value = LONG_BIT LONG_BIT = width try: return test(*args, **kwargs) finally: LONG_BIT = old_value return newtest return dec MAXINT = sys.maxint MININT = -sys.maxint - 1 uints = strategies.builds( r_uint, strategies.integers(min_value=0, max_value=2**LONG_BIT - 1) ) ints = strategies.builds( lambda x: intmask(r_uint(x)), strategies.integers(min_value=0, max_value=2**LONG_BIT - 1) ) bounds = strategies.builds( lambda tup: tup[0], knownbits_and_bound_with_contained_number ) varname_counter = 0 def z3_tnum_condition(variable, tvalue, tmask): if isinstance(tvalue, r_uint): tvalue = BitVecVal(tvalue) if isinstance(tmask, r_uint): tmask = BitVecVal(tmask) return variable & ~tmask == tvalue def z3_tvalue_tmask_are_valid(tvalue, tmask): return tvalue & ~tmask == tvalue def to_z3(bound, variable=None): global varname_counter if variable is None: variable = BitVec("bv%s" % (varname_counter, )) varname_counter += 1 components = [] if bound.upper < MAXINT: components.append(variable <= BitVecVal(bound.upper)) if bound.lower > MININT: components.append(variable >= BitVecVal(bound.lower)) if bound.tmask != r_uint(-1): # all unknown: components.append(z3_tnum_condition(variable, bound.tvalue, bound.tmask)) if len(components) == 1: return variable, components[0] if len(components) == 0: return variable, z3.BoolVal(True) return variable, z3.And(*components) class CheckError(Exception): pass def prove_implies(*args, **kwargs): last = args[-1] prev = args[:-1] return prove(z3.Implies(z3.And(*prev), last), **kwargs) def teardown_function(function): # z3 doesn't add enough memory pressure, just collect after every function # to counteract gc.collect() def prove(cond, use_timeout=True): solver = z3.Solver() if use_timeout and pytest.config.option.z3timeout: solver.set("timeout", pytest.config.option.z3timeout) z3res = solver.check(z3.Not(cond)) if z3res == z3.unsat: pass elif z3res == z3.unknown: print "timeout", cond assert use_timeout elif z3res == z3.sat: # not possible to prove! global model model = solver.model() raise CheckError(cond, model) @given(bounds, bounds) def test_add(b1, b2): b3 = b1.add_bound(b2) var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) var3, formula3 = to_z3(b3, var1 + var2) prove_implies(formula1, formula2, formula3) @given(bounds, bounds) def test_add_bound_cannot_overflow(b1, b2): bound = b1.add_bound_cannot_overflow(b2) assume(bound) var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) m = z3.SignExt(LONG_BIT, var1) + z3.SignExt(LONG_BIT, var2) no_ovf = m == z3.SignExt(LONG_BIT, var1 + var2) prove_implies(formula1, formula2, no_ovf) @given(bounds, bounds) def test_add_bound_no_overflow(b1, b2): b3 = b1.add_bound_no_overflow(b2) var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) var3, formula3 = to_z3(b3, var1 + var2) m = z3.SignExt(LONG_BIT, var1) + z3.SignExt(LONG_BIT, var2) no_ovf = m == z3.SignExt(LONG_BIT, var1 + var2) prove_implies(formula1, formula2, no_ovf, formula3) @given(bounds, bounds) def test_sub(b1, b2): b3 = b1.sub_bound(b2) var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) var3, formula3 = to_z3(b3, var1 - var2) prove_implies(formula1, formula2, formula3) @given(bounds, bounds) def test_sub_bound_cannot_overflow(b1, b2): bound = b1.sub_bound_cannot_overflow(b2) assume(bound) var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) m = z3.SignExt(LONG_BIT, var1) - z3.SignExt(LONG_BIT, var2) no_ovf = m == z3.SignExt(LONG_BIT, var1 - var2) prove_implies(formula1, formula2, no_ovf) @given(bounds, bounds) def test_sub_bound_no_overflow(b1, b2): b3 = b1.sub_bound_no_overflow(b2) var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) var3, formula3 = to_z3(b3, var1 - var2) m = z3.SignExt(LONG_BIT, var1) - z3.SignExt(LONG_BIT, var2) no_ovf = m == z3.SignExt(LONG_BIT, var1 - var2) prove_implies(formula1, formula2, no_ovf, formula3) @given(bounds, bounds) def test_mul(b1, b2): b3 = b1.mul_bound(b2) var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) var3, formula3 = to_z3(b3, var1 * var2) prove_implies(formula1, formula2, formula3) @given(bounds, bounds) def test_mul_bound_cannot_overflow(b1, b2): bound = b1.mul_bound_cannot_overflow(b2) if bound: var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) m = z3.SignExt(LONG_BIT, var1) * z3.SignExt(LONG_BIT, var2) no_ovf = m == z3.SignExt(LONG_BIT, var1 * var2) prove_implies(formula1, formula2, no_ovf) @given(bounds, bounds) def test_mul_bound_no_overflow(b1, b2): b3 = b1.mul_bound_no_overflow(b2) var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) var3, formula3 = to_z3(b3, var1 * var2) m = z3.SignExt(LONG_BIT, var1) * z3.SignExt(LONG_BIT, var2) no_ovf = m == z3.SignExt(LONG_BIT, var1 * var2) prove_implies(formula1, formula2, no_ovf, formula3) @given(bounds) def test_neg(b1): b2 = b1.neg_bound() var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2, -var1) prove_implies(formula1, formula2) @given(bounds, bounds) def test_known(b1, b2): var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) if b1.known_lt(b2): prove_implies(formula1, formula2, var1 < var2) if b1.known_gt(b2): prove_implies(formula1, formula2, var1 > var2) if b1.known_le(b2): prove_implies(formula1, formula2, var1 <= var2) if b1.known_ge(b2): prove_implies(formula1, formula2, var1 >= var2) if b1.known_ne(b2): prove_implies(formula1, formula2, var1 != var2) @given(bounds, bounds) def test_mod(b1, b2): b3 = b1.mod_bound(b2) print b1, b2, b3 var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) var3, nonzero = z3_pymod_nonzero(var1, var2) _, formula3 = to_z3(b3, var3) prove_implies(formula1, formula2, nonzero, formula3) # ____________________________________________________________ # boolean operations @given(bounds, bounds) def test_and(b1, b2): b3 = b1.and_bound(b2) var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) var3, formula3 = to_z3(b3, var1 & var2) prove_implies(formula1, formula2, formula3) @given(bounds, bounds) def test_or(b1, b2): b3 = b1.or_bound(b2) var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) var3, formula3 = to_z3(b3, var1 | var2) prove_implies(formula1, formula2, formula3) @given(bounds, bounds) def test_xor(b1, b2): b3 = b1.xor_bound(b2) var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2) var3, formula3 = to_z3(b3, var1 ^ var2) prove_implies(formula1, formula2, formula3) @given(bounds) def test_invert(b1): b2 = b1.invert_bound() var1, formula1 = to_z3(b1) var2, formula2 = to_z3(b2, ~var1) prove_implies(formula1, formula2) # ____________________________________________________________ # shrinking @given(ints, ints) def test_shrink_bounds_to_knownbits(x, y): x, y = sorted([x, y]) b = IntBound(x, y, do_shrinking=False) var1, formula1 = to_z3(b) b.shrink() var1, formula2 = to_z3(b, var1) prove_implies(formula1, formula2) @given(uints, uints) def test_shrink_knownbits_to_bounds(x, y): b = IntBound(tvalue=x & ~y, tmask=y, do_shrinking=False) var1, formula1 = to_z3(b) b.shrink() var1, formula2 = to_z3(b, var1) prove_implies(formula1, formula2) @given(ints, ints, uints, uints) def test_shrink_mixed(x, y, value, tmask): x, y = sorted([x, y]) b = IntBound(x, y, value & ~tmask, tmask, do_shrinking=False) var1, formula1 = to_z3(b) # check that b contains values before we shrink solver = z3.Solver() assume(solver.check(formula1) == z3.sat) b.shrink() var1, formula2 = to_z3(b, var1) prove_implies(formula1, formula2) # ____________________________________________________________ # explicit proofs of some of the helpers def test_prove_next_pow2_m1(): x = BitVec('x') res = next_pow2_m1(x) # it's a power of 2 - 1 prove(res & (res + 1) == 0) # it's bigger than x prove( z3.BV2Int(res) + 1 >= z3.BV2Int(x) ) def test_prove_lowest_set_bit_only(): x = BitVec('x') res = lowest_set_bit_only(x) prove_implies( x != 0, popcount64(res) == 1 ) prove_implies( x == 0, res == 0, ) # do it the pedestrian way: if a bit is set, then the bits with lower # indexes must be 0 conditions = [] for i in range(LONG_BIT): for j in range(i): cond = z3.Implies(z3.Extract(i, i, res) == 1, z3.Extract(j, j, res) == 0) conditions.append(cond) prove( z3.And(*conditions) ) # ____________________________________________________________ # explicit proofs of IntBound logic/code def make_z3_bound_and_tnum(name): """ make a z3 knownbits number and bounds. return values are: - variable, corresponding to the concrete value - lower, a variable corresponding to the lower bound - upper, a variable corresponding to the upper bound - tvalue and tmask, corresponding to the abstract value - formula, which is the precondition that tvalue and tmask are well-formed, that lower <= upper, and that the four variables are a valid abstraction of the concrete value """ variable = BitVec(name) tvalue = BitVec(name + "_tvalue") tmask = BitVec(name + "_tmask") upper = BitVec(name + "_upper") lower = BitVec(name + "_lower") formula = z3.And( z3_tnum_condition(variable, tvalue, tmask), lower <= variable, variable <= upper ) return variable, lower, upper, tvalue, tmask, formula def popcount64(w): w -= (w >> 1) & 0x5555555555555555 w = (w & 0x3333333333333333) + ((w >> 2) & 0x3333333333333333) w = (w + (w >> 4)) & 0x0f0f0f0f0f0f0f0f return ((w * 0x0101010101010101) >> 56) & 0xff def test_popcount64(): assert popcount64(1 << 60) == 1 assert popcount64((1 << 60) + 5) == 3 assert popcount64((1 << 63) + 0b11010110111) == 9 def z3_add_overflow(a, b): result = a + b result_wide = z3.SignExt(LONG_BIT, a) + z3.SignExt(LONG_BIT, b) no_ovf = result_wide == z3.SignExt(LONG_BIT, result) return result, no_ovf def z3_sub_overflow(a, b): result = a - b result_wide = z3.SignExt(LONG_BIT, a) - z3.SignExt(LONG_BIT, b) no_ovf = result_wide == z3.SignExt(LONG_BIT, result) return result, no_ovf def z3_mul_overflow(a, b): result = a * b result_wide = z3.SignExt(LONG_BIT, a) * z3.SignExt(LONG_BIT, b) no_ovf = result_wide == z3.SignExt(LONG_BIT, result) return result, no_ovf # debugging functions to understand the counterexamples def s(p): if p.sort() == z3.BoolSort(): print model.evaluate(p) else: print hex(model.evaluate(p).as_signed_long()) def u(p): print "r_uint(%s)" % bin(model.evaluate(p).as_long()) class Z3IntBound(IntBound): def __init__(self, lower, upper, tvalue, tmask, concrete_variable=None): self.lower = lower self.upper = upper self.tvalue = tvalue self.tmask = tmask self.concrete_variable = concrete_variable @staticmethod def new(lower, upper, tvalue, tmask): return Z3IntBound(lower, upper, tvalue, tmask) @staticmethod def from_knownbits(tvalue, tmask): # compute lower and upper bound like shrinking does it res = Z3IntBound(None, None, tvalue, tmask) res.lower = res._get_minimum_signed_by_knownbits() res.upper = res._get_maximum_signed_by_knownbits() return res @staticmethod def from_constant(const): if isinstance(const, int): const = BitVecVal(const) res = Z3IntBound(const, const, const, 0) return res @staticmethod def intmask(x): # casts from unsigned to signed don't actually matter to Z3 return x @staticmethod def r_uint(x): # casts from unsigned to signed don't actually matter to Z3 return x @staticmethod def _add_check_overflow(a, b, default): result, no_ovf = z3_add_overflow(a, b) return z3.If(no_ovf, result, default) @staticmethod def _sub_check_overflow(a, b, default): result, no_ovf = z3_sub_overflow(a, b) return z3.If(no_ovf, result, default) @staticmethod def _urshift(a, b): return z3.LShR(a, b) def __repr__(self): more = '' if self.concrete_variable is not None: more = ', concrete_variable=%s' % (self.concrete_variable, ) return "" % ( self.lower, self.upper, self.tvalue, self.tmask, more) __str__ = __repr__ # ____________________________________________________________ # reimplementations of methods with control flow that Z3 doesn't support def add_bound(self, other): lower, no_ovf_lower = z3_add_overflow(self.lower, other.lower) upper, no_ovf_upper = z3_add_overflow(self.upper, other.upper) result_lower = z3.If(z3.And(no_ovf_lower, no_ovf_upper), lower, MININT) result_upper = z3.If(z3.And(no_ovf_lower, no_ovf_upper), upper, MAXINT) tvalue, tmask = self._tnum_add(other) return Z3IntBound(result_lower, result_upper, tvalue, tmask) def sub_bound(self, other): result = self.concrete_variable - other.concrete_variable lower, no_ovf_lower = z3_sub_overflow(self.lower, other.upper) upper, no_ovf_upper = z3_sub_overflow(self.upper, other.lower) result_lower = z3.If(z3.And(no_ovf_lower, no_ovf_upper), lower, MININT) result_upper = z3.If(z3.And(no_ovf_lower, no_ovf_upper), upper, MAXINT) tvalue, tmask = self._tnum_sub(other) return Z3IntBound(result_lower, result_upper, tvalue, tmask) def add_bound_cannot_overflow(self, other): lower, no_ovf_lower = z3_add_overflow(self.lower, other.lower) upper, no_ovf_upper = z3_add_overflow(self.upper, other.upper) return z3.And(no_ovf_lower, no_ovf_upper) def sub_bound_cannot_overflow(self, other): lower, no_ovf_lower = z3_sub_overflow(self.lower, other.upper) upper, no_ovf_upper = z3_sub_overflow(self.upper, other.lower) return z3.And(no_ovf_lower, no_ovf_upper) def and_bound(self, other): pos1 = self.known_nonnegative() pos2 = other.known_nonnegative() # the next three if-conditions are proven by test_prove_and_bound_logic lower = z3.If(z3.Or(pos1, pos2), z3.BitVecVal(0, LONG_BIT), MININT) upper = z3.If( pos1, z3.If( pos2, z3_min(self.upper, other.upper), self.upper), z3.If( pos2, other.upper, MAXINT)) res_tvalue, res_tmask = self._tnum_and(other) return self.new(lower, upper, res_tvalue, res_tmask) def lshift_bound_cannot_overflow(self, other): _, no_ovf1 = z3_lshift_overflow(self.lower, other.lower) _, no_ovf2 = z3_lshift_overflow(self.lower, other.upper) _, no_ovf3 = z3_lshift_overflow(self.upper, other.lower) _, no_ovf4 = z3_lshift_overflow(self.upper, other.upper) return z3.And(no_ovf1, no_ovf2, no_ovf3, no_ovf4) def rshift_bound(self, other): result = self.concrete_variable >> other.concrete_variable result1 = self.lower >> other.lower result2 = self.lower >> other.upper result3 = self.upper >> other.lower result4 = self.upper >> other.upper min1 = z3_min(result1, result2, result3, result4) max1 = z3_max(result1, result2, result3, result4) cond = z3.And(other.lower >= 0, other.upper < LONG_BIT) min1 = z3.If(cond, min1, MININT) max1 = z3.If(cond, max1, MAXINT) tvalue, tmask = self._tnum_rshift(other.lower) cond2 = z3.And(other.is_constant(), cond) tvalue = z3.If(cond2, tvalue, 0) tmask = z3.If(cond2, tmask, -1) return Z3IntBound(min1, max1, tvalue, tmask) def urshift_bound(self, other): tvalue_if_const, tmask_if_const = self._tnum_urshift(other.lower) tvalue = z3.If(other.is_constant(), tvalue_if_const, 0) tmask = z3.If(other.is_constant(), tmask_if_const, -1) lower = z3.If(z3.And(other.is_constant(), self.lower >= 0), self.lower >> other.lower, MININT) upper = z3.If(z3.And(other.is_constant(), self.lower >= 0), self.upper >> other.lower, MAXINT) return Z3IntBound.from_knownbits(tvalue, tmask) def is_constant(self): return z3.And(self.lower == self.upper, self.tmask == 0) def is_bool(self): return z3.And(0 <= self.lower, self.upper <= 1) def known_eq_const(self, value): return z3.If(self.is_constant(), self.lower == value, False) def get_constant_int(self): return z3.If(self.is_constant(), self.lower, 0xdeadbeef) # ____________________________________________________________ def z3_formula(self, variable=None, must_be_minimal=False): """ return the Z3 condition that: - self is well-formed - variable (or self.concrete_variable) is an element of the set described by self """ if variable is None: variable = self.concrete_variable assert variable is not None result = z3.And( # is the tnum well-formed? ie are the unknown bits in tvalue set to 0? self.tvalue & ~self.tmask == self.tvalue, # does variable fulfill the conditions imposed by tvalue and tmask? z3_tnum_condition(variable, self.tvalue, self.tmask), # does variable fulfill the conditions of the bounds? self.lower <= variable, variable <= self.upper, ) if must_be_minimal: tvalue, tmask, valid = self._tnum_improve_knownbits_by_bounds() result = z3.And( valid, self.tvalue == tvalue, self.tmask == tmask, result ) return result def convert_to_concrete(self, model): """ A helper function that can be used to turn a Z3 counterexample into an IntBound instance to understand it better. """ v = r_uint(model.evaluate(self.tvalue).as_long()) m = r_uint(model.evaluate(self.tmask).as_long()) l = model.evaluate(self.lower).as_signed_long() u = model.evaluate(self.upper).as_signed_long() return IntBound(l, u, v, m, do_shrinking=False) def prove_implies(self, *args): formula_args = [(arg.z3_formula() if isinstance(arg, Z3IntBound) else arg) for arg in (self, ) + args] try: prove_implies( *formula_args, use_timeout=False ) except CheckError as e: model = e.args[1] example_self = self.convert_to_concrete(model) print "ERROR", args print "COUNTEREXAMPLE", example_self assert 0 def make_z3_intbounds_instance(name, concrete_variable=None): if concrete_variable is None: variable = BitVec(name + "_concrete") else: variable = concrete_variable tvalue = BitVec(name + "_tvalue") tmask = BitVec(name + "_tmask") upper = BitVec(name + "_upper") lower = BitVec(name + "_lower") return Z3IntBound(lower, upper, tvalue, tmask, variable) def test_prove_invert(): bound = make_z3_intbounds_instance('self') b2 = bound.invert_bound() bound.prove_implies( b2.z3_formula(~bound.concrete_variable), ) def test_prove_min_max_unsigned_by_knownbits(): bound = make_z3_intbounds_instance('self') minimum = bound.get_minimum_unsigned_by_knownbits() bound.prove_implies( z3.ULE(minimum, bound.concrete_variable), ) maximum = bound.get_maximum_unsigned_by_knownbits() bound.prove_implies( z3.ULE(bound.concrete_variable, maximum), ) def test_prove_min_max_signed_by_knownbits(): bound = make_z3_intbounds_instance('self') minimum = bound._get_minimum_signed_by_knownbits() bound.prove_implies( minimum <= bound.concrete_variable ) bound.prove_implies( z3_tnum_condition(minimum, bound.tvalue, bound.tmask), ) maximum = bound._get_maximum_signed_by_knownbits() bound.prove_implies( bound.concrete_variable <= maximum, ) bound.prove_implies( z3_tnum_condition(maximum, bound.tvalue, bound.tmask), ) def test_prove_or(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') b3 = b1.or_bound(b2) b3.concrete_variable = b1.concrete_variable | b2.concrete_variable b1.prove_implies( b2, b3 ) def test_prove_or_bounds_implied_by_knownbits(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') b3 = b1.or_bound(b2) # similar to test_prove_xor_bounds_implied_by_knownbits, the following # logic was used to give explicit bounds for or of two nonnegative numbers. mostsignificant = b1.upper | b2.upper upper = next_pow2_m1(mostsignificant) result = b1.concrete_variable | b2.concrete_variable b1.prove_implies( b1.z3_formula(must_be_minimal=True), b2.z3_formula(must_be_minimal=True), b1.lower >= 0, b2.lower >= 0, z3.And(b3.upper <= upper, b3.lower >= 0), ) def test_prove_xor(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') b3 = b1.xor_bound(b2) b3.concrete_variable = b1.concrete_variable ^ b2.concrete_variable b1.prove_implies( b2, b3, ) def test_prove_xor_bounds_implied_by_knownbits(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') # for non-negative b1 and b2, xor_bound used to contain code that set the # lower bound to 0, and an upper bound to: mostsignificant = b1.upper | b2.upper upper = next_pow2_m1(mostsignificant) # this is unnecessary, because the information is implied by the knownbits, # which we prove here result = b1.concrete_variable ^ b2.concrete_variable b3 = b1.xor_bound(b2) b3.concrete_variable = result b1.prove_implies( b1.z3_formula(must_be_minimal=True), b2.z3_formula(must_be_minimal=True), b1.lower >= 0, b2.lower >= 0, # check that the maximum implied by the known bits is not worse than # the maximum computed by the expression above z3.And(b3.upper <= upper, b3.lower >= 0), ) def test_prove_and(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') tvalue, tmask = b1._tnum_and(b2) b1.prove_implies( b2, z3_tnum_condition(b1.concrete_variable & b2.concrete_variable, tvalue, tmask), ) def test_prove_and_bound_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') res = b1.concrete_variable & b2.concrete_variable b3 = b1.and_bound(b2) b3.concrete_variable = res b1.prove_implies( b2, b3 ) def test_prove_add_knownbits(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') result = b1.concrete_variable + b2.concrete_variable res_tvalue, res_tmask = b1._tnum_add(b2) b1.prove_implies( b2, z3_tnum_condition(result, res_tvalue, res_tmask), ) def test_prove_add_bound_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') result = b1.concrete_variable + b2.concrete_variable b3 = b1.add_bound(b2) b3.concrete_variable = result b1.prove_implies( b2, b3 ) def test_prove_add_bound_cannot_overflow_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') result, no_ovf_result = z3_add_overflow(b1.concrete_variable, b2.concrete_variable) b1.prove_implies( b2, b1.add_bound_cannot_overflow(b2), no_ovf_result, ) def test_prove_add_bound_no_overflow(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') result, no_ovf = z3_add_overflow(b1.concrete_variable, b2.concrete_variable) b3 = b1.add_bound_no_overflow(b2) b3.concrete_variable = result b1.prove_implies( b2, no_ovf, b3 ) def test_prove_neg_logic(): b1 = make_z3_intbounds_instance('self') one = Z3IntBound(BitVecVal(1), BitVecVal(1), BitVecVal(1), BitVecVal(0)) b2 = b1.neg_bound() b2.concrete_variable = -b1.concrete_variable b1.prove_implies(b2) def test_prove_sub_knownbits(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') result = b1.concrete_variable - b2.concrete_variable res_tvalue, res_tmask = b1._tnum_sub(b2) b1.prove_implies( b2, z3_tnum_condition(result, res_tvalue, res_tmask), ) def test_prove_sub_bound_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') b3 = b1.sub_bound(b2) b3.concrete_variable = b1.concrete_variable - b2.concrete_variable b1.prove_implies( b2, b3 ) def test_prove_sub_bound_cannot_overflow_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') result, no_ovf_result = z3_sub_overflow(b1.concrete_variable, b2.concrete_variable) b1.prove_implies( b2, b1.sub_bound_cannot_overflow(b2), no_ovf_result, ) def test_prove_sub_bound_no_overflow(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') result, no_ovf = z3_sub_overflow(b1.concrete_variable, b2.concrete_variable) b3 = b1.sub_bound_no_overflow(b2) b1.prove_implies( b2, no_ovf, b3.z3_formula(result) ) def test_prove_and_backwards(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') b3 = make_z3_intbounds_instance('result') res = b1.concrete_variable & b2.concrete_variable b3.concrete_variable = res better_tvalue, better_tmask, valid = b2._tnum_and_backwards(b3) b1.prove_implies( b2, b3, z3.And( valid, z3_tnum_condition(b1.concrete_variable, better_tvalue, better_tmask) ), ) def test_prove_and_backwards_inconsistent(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') b3 = make_z3_intbounds_instance('result') res = b1.concrete_variable & b2.concrete_variable better_tvalue, better_tmask, valid = b2._tnum_and_backwards(b3) # hm, this is just the contraposition of test_prove_and_backwards, so # trivially true? b1.prove_implies( b2, b3, # if we aren't consistent z3.Not(valid), # then the result must be different than the result of the & b3.concrete_variable != res ) def test_prove_or_backwards(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') b3 = make_z3_intbounds_instance('result') res = b1.concrete_variable | b2.concrete_variable b3.concrete_variable = res better_tvalue, better_tmask, valid = b2._tnum_or_backwards(b3) b1.prove_implies( b2, b3, z3.And( valid, z3_tnum_condition(b1.concrete_variable, better_tvalue, better_tmask) ), ) def test_prove_known_unsigned_lt_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') max_self = b1.get_maximum_unsigned_by_knownbits() min_other = b2.get_minimum_unsigned_by_knownbits() b1.prove_implies( b2, z3.ULT(max_self, min_other), z3.ULT(b1.concrete_variable, b2.concrete_variable), ) def test_prove_known_unsigned_lt_from_signed_lt_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') b1.prove_implies( b2, b1.lower >= 0, b2.lower < b2.lower, z3.ULT(b1.concrete_variable, b2.concrete_variable), ) b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') b1.prove_implies( b2, b1.lower < 0, b2.lower < b2.lower, z3.ULT(b1.concrete_variable, b2.concrete_variable), ) def test_prove_known_eq_const_logic(): b1 = make_z3_intbounds_instance('self') x = BitVec('x') b1.prove_implies( b1.known_eq_const(x), b1.concrete_variable == x ) def test_prove_uint_less_nonnegative_implies_nonnegative(): index = BitVec('index') length = BitVec('length') prove_implies( length >= 0, z3.ULT(index, length), z3.And(index >= 0, index < length), ) prove_implies( length >= 0, z3.ULT(index, length), z3.And(index >= 0, index <= length - 1), ) prove_implies( length >= 0, z3.ULE(index, length), z3.And(index >= 0, index <= length), ) def test_prove_uint_greater_negative_implies_negative(): a = BitVec('a') b = BitVec('b') prove_implies( b < 0, z3.UGE(a, b), z3.And(a < 0, a >= b), ) prove_implies( b < 0, z3.UGT(a, b), z3.And(a < 0, a > b), ) # an example prove_implies( b <= -3, b >= -4, z3.UGT(a, b), z3.And(a <= -1, a >= -3), ) def test_prove_known_cmp(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') b1.prove_implies( b2, b1.known_lt(b2), b1.concrete_variable < b2.concrete_variable, ) b1.prove_implies( b2, b1.known_le(b2), b1.concrete_variable <= b2.concrete_variable, ) b1.prove_implies( b2, b1.known_gt(b2), b1.concrete_variable > b2.concrete_variable, ) b1.prove_implies( b2, b1.known_ge(b2), b1.concrete_variable >= b2.concrete_variable, ) def test_prove_tnum_intersect(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') tvalue, tmask, valid = b1._tnum_intersect(b2.tvalue, b2.tmask) b1.prove_implies( b2.z3_formula(b1.concrete_variable), z3.And( valid, z3_tnum_condition(b1.concrete_variable, tvalue, tmask) ) ) # check that if valid if false, there are no values in the intersection b1.prove_implies( z3.Not(valid), z3.Not(b2.z3_formula(b1.concrete_variable)), ) # and also that we only gain information b1.prove_implies( b2.z3_formula(b1.concrete_variable), valid, popcount64(~tmask) >= popcount64(~b1.tmask), ) def test_prove_tnum_intersect_idempotent(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') b2.concrete_variable = b1.concrete_variable tvalue1, tmask1, valid1 = b1._tnum_intersect(b2.tvalue, b2.tmask) tvalue2, tmask2, valid2 = b1._tnum_intersect(tvalue1, tmask1) b1.prove_implies( b2, z3.And( tvalue1 == tvalue2, tmask1 == tmask2, valid1, valid2, ) ) # ____________________________________________________________ # prove things about _shrink_knownbits_by_bounds def test_prove_tnum_implied_by_bounds(): self = make_z3_intbounds_instance('self') bounds_tvalue, bounds_tmask = self._tnum_implied_by_bounds() val = BitVec('val') self.prove_implies( val >= self.lower, val <= self.upper, z3_tnum_condition(val, bounds_tvalue, bounds_tmask) ) def test_prove_shrink_knownbits_by_bounds(): self = make_z3_intbounds_instance('self') tvalue, tmask, valid = self._tnum_improve_knownbits_by_bounds() self.prove_implies( z3_tnum_condition(self.concrete_variable, self.tvalue, self.tmask), z3.And(valid, z3_tnum_condition(self.concrete_variable, tvalue, tmask)), ) # ____________________________________________________________ # prove things about _shrink_bounds_by_knownbits def test_prove_shrink_bounds_by_knownbits_min_case1(): # case 1, cl2set > set2cl b1 = make_z3_intbounds_instance('self') threshold = b1.lower working_min, cl2set, set2cl = b1._helper_min_max_prepare(threshold) new_threshold = b1._helper_min_case1(working_min, cl2set) # show that the new_threshold is larger than threshold b1.prove_implies( b1._get_minimum_signed_by_knownbits() < threshold, working_min != threshold, z3.UGT(cl2set, set2cl), new_threshold > threshold, ) # correctness: show that there are no elements x in b1 with # threshold <= x < new_threshold b1.prove_implies( b1._get_minimum_signed_by_knownbits() < threshold, working_min != threshold, z3.UGT(cl2set, set2cl), z3.Not(b1.concrete_variable < new_threshold), ) # precision: new_threshold is an element in the set, ie we # couldn't have increased the bound further b1.prove_implies( b1._get_minimum_signed_by_knownbits() < threshold, working_min != threshold, z3.UGT(cl2set, set2cl), z3_tnum_condition(new_threshold, b1.tvalue, b1.tmask), ) def test_prove_shrink_bounds_by_knownbits_correctness_min_case2(): # case 2) cl2set <= set2cl b1 = make_z3_intbounds_instance('self') threshold = b1.lower working_min, cl2set, set2cl = b1._helper_min_max_prepare(threshold) working_min_ne_threshold = working_min != threshold new_threshold = b1._helper_min_case2(working_min, set2cl) # check that the bound is not getting worse b1.prove_implies( b1._get_minimum_signed_by_knownbits() < threshold, working_min_ne_threshold, z3.ULE(cl2set, set2cl), new_threshold > threshold ) # correctness: show that there are no elements x in b1 with # threshold <= x < new_threshold b1.prove_implies( b1._get_minimum_signed_by_knownbits() < threshold, working_min_ne_threshold, z3.ULE(cl2set, set2cl), z3.Not(b1.concrete_variable < new_threshold), ) # precision: new_threshold is an element in the set, ie we # couldn't have increased the bound further b1.prove_implies( b1._get_minimum_signed_by_knownbits() < threshold, working_min_ne_threshold, z3.ULE(cl2set, set2cl), z3_tnum_condition(new_threshold, b1.tvalue, b1.tmask), ) def test_prove_shrink_bounds_by_knownbits_max_case1(): # case 1, cl2set < set2cl b1 = make_z3_intbounds_instance('self') threshold = b1.upper working_min, cl2set, set2cl = b1._helper_min_max_prepare(threshold) new_threshold = b1._helper_max_case1(working_min, set2cl) # show that the new_threshold is smaller than threshold b1.prove_implies( b1._get_maximum_signed_by_knownbits() > threshold, working_min != threshold, z3.ULT(cl2set, set2cl), new_threshold < threshold, ) # correctness: show that there are no elements x in b1 with # new_threshold <= x < threshold b1.prove_implies( b1._get_maximum_signed_by_knownbits() > threshold, working_min != threshold, z3.ULT(cl2set, set2cl), z3.Not(b1.concrete_variable > new_threshold), ) # precision: new_threshold is an element in the set, ie we # couldn't have increased the bound further b1.prove_implies( b1._get_maximum_signed_by_knownbits() > threshold, working_min != threshold, z3.ULT(cl2set, set2cl), z3_tnum_condition(new_threshold, b1.tvalue, b1.tmask), ) def test_prove_shrink_bounds_by_knownbits_correctness_max_case2(): # case 2) cl2set >= set2cl b1 = make_z3_intbounds_instance('self') threshold = b1.upper working_max, cl2set, set2cl = b1._helper_min_max_prepare(threshold) working_max_ne_threshold = working_max != threshold new_threshold = b1._helper_max_case2(working_max, cl2set) # check that the bound is not getting worse b1.prove_implies( b1._get_maximum_signed_by_knownbits() > threshold, working_max_ne_threshold, z3.UGE(cl2set, set2cl), new_threshold < threshold ) # correctness: show that there are no elements x in b1 with # threshold <= x < new_threshold b1.prove_implies( b1._get_maximum_signed_by_knownbits() > threshold, working_max_ne_threshold, z3.UGE(cl2set, set2cl), z3.Not(b1.concrete_variable > new_threshold), ) # precision: new_threshold is an element in the set, ie we # couldn't have increased the bound further b1.prove_implies( b1._get_maximum_signed_by_knownbits() > threshold, working_max_ne_threshold, z3.UGE(cl2set, set2cl), z3_tnum_condition(new_threshold, b1.tvalue, b1.tmask), ) # ____________________________________________________________ def z3_lshift_overflow(a, b): res = a << b return res, (res >> b) == a def z3_min(*args): res = args[0] for x in args[1:]: res = z3.If(res < x, res, x) return res def z3_max(*args): res = args[0] for x in args[1:]: res = z3.If(res > x, res, x) return res @z3_with_reduced_bitwidth(16) def test_prove_lshift_bound_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') # bounds logic result, no_ovf = z3_lshift_overflow(b1.concrete_variable, b2.concrete_variable) result1, no_ovf1 = z3_lshift_overflow(b1.lower, b2.lower) result2, no_ovf2 = z3_lshift_overflow(b1.lower, b2.upper) result3, no_ovf3 = z3_lshift_overflow(b1.upper, b2.lower) result4, no_ovf4 = z3_lshift_overflow(b1.upper, b2.upper) min1 = z3_min(result1, result2, result3, result4) max1 = z3_max(result1, result2, result3, result4) b1.prove_implies( b2, z3.And(no_ovf1, no_ovf2, no_ovf3, no_ovf4), z3.And(min1 <= result, result <= max1, no_ovf), ) def test_prove_lshift_knownbits(): b1 = make_z3_intbounds_instance('self') c = BitVec('const') result = b1.concrete_variable << c tvalue, tmask = b1._tnum_lshift(c) b1.prove_implies( c >= 0, c < LONG_BIT, z3_tnum_condition(result, tvalue, tmask) ) def test_prove_lshift_bound_cannot_overflow_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') res = b1.lshift_bound_cannot_overflow(b2) result, no_ovf = z3_lshift_overflow(b1.concrete_variable, b2.concrete_variable) b1.prove_implies( b2, res, no_ovf ) def test_prove_rshift_knownbits(): b1 = make_z3_intbounds_instance('self') c = BitVec('const') result = b1.concrete_variable >> c tvalue, tmask = b1._tnum_rshift(c) b1.prove_implies( c >= 0, z3_tnum_condition(result, tvalue, tmask), ) def test_prove_rshift_bound_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') # bounds logic result = b1.concrete_variable >> b2.concrete_variable result1 = b1.lower >> b2.lower result2 = b1.lower >> b2.upper result3 = b1.upper >> b2.lower result4 = b1.upper >> b2.upper min1 = z3_min(result1, result2, result3, result4) max1 = z3_max(result1, result2, result3, result4) b1.prove_implies( b2, b2.lower >= 0, min1 <= result, result <= max1, ) @z3_with_reduced_bitwidth(32) def test_2_prove_rshift_bound_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') b3 = b1.rshift_bound(b2) b3.concrete_variable = result = b1.concrete_variable >> b2.concrete_variable b1.prove_implies( b2, b2.lower >= 0, b2.upper < LONG_BIT, b3, ) def test_prove_urshift_knownbits(): b1 = make_z3_intbounds_instance('self') c = BitVec('const') result = z3.LShR(b1.concrete_variable, c) tvalue, tmask = b1._tnum_urshift(c) b1.prove_implies( c >= 0, z3_tnum_condition(result, tvalue, tmask), ) def test_prove_urshift_knownbits_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') result = z3.LShR(b1.concrete_variable, b2.concrete_variable) b3 = b1.urshift_bound(b2) b3.concrete_variable = result b1.prove_implies( b2, b3, ) def test_prove_lshift_bound_backwards_logic(): b1 = make_z3_intbounds_instance('self') c_other = BitVec('const') res = b1.concrete_variable << c_other bresult = make_z3_intbounds_instance('result', res) tvalue = z3.LShR(bresult.tvalue, c_other) tmask = z3.LShR(bresult.tmask, c_other) s_tmask = ~z3.LShR(-1, c_other) valid = (bresult.tvalue & ((1 << c_other) - 1)) == 0 tmask |= s_tmask b1.prove_implies( bresult, 0 <= c_other, c_other <= LONG_BIT, z3.And( valid, z3_tnum_condition(b1.concrete_variable, tvalue, tmask) ), ) def test_prove_rshift_bound_backwards_logic(): b1 = make_z3_intbounds_instance('self') c_other = BitVec('const') res = b1.concrete_variable >> c_other bresult = make_z3_intbounds_instance('result', res) tvalue = bresult.tvalue << c_other tmask = bresult.tmask << c_other tmask |= (1 << c_other) - 1 b1.prove_implies( bresult, 0 <= c_other, c_other < LONG_BIT, z3_tnum_condition(b1.concrete_variable, tvalue, tmask) ) def test_prove_rshift_bound_backwards_logic2(): b1 = make_z3_intbounds_instance('self') c_other = BitVec('const') res = b1.concrete_variable >> c_other bresult = make_z3_intbounds_instance('result', res) power = 1 << c_other lower_shifted, no_ovf1 = z3_mul_overflow(bresult.lower, power) upper_shifted, no_ovf2 = z3_mul_overflow(bresult.upper, power) lower = z3_min(lower_shifted, lower_shifted | (power - 1), upper_shifted, upper_shifted | (power - 1)) upper = z3_max(lower_shifted, lower_shifted | (power - 1), upper_shifted, upper_shifted | (power - 1)) b1.prove_implies( bresult, 0 <= c_other, c_other < LONG_BIT, no_ovf1, no_ovf2, z3.And(lower <= b1.concrete_variable, b1.concrete_variable <= upper), ) @z3_with_reduced_bitwidth(8) def test_prove_mul_bound_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') result, no_ovf = z3_mul_overflow(b1.concrete_variable, b2.concrete_variable) result1, no_ovf1 = z3_mul_overflow(b1.lower, b2.lower) result2, no_ovf2 = z3_mul_overflow(b1.lower, b2.upper) result3, no_ovf3 = z3_mul_overflow(b1.upper, b2.lower) result4, no_ovf4 = z3_mul_overflow(b1.upper, b2.upper) min1 = z3_min(result1, result2, result3, result4) max1 = z3_max(result1, result2, result3, result4) b1.prove_implies( b2, z3.And(no_ovf1, no_ovf2, no_ovf3, no_ovf4), z3.And(min1 <= result, result <= max1, no_ovf), ) @z3_with_reduced_bitwidth(8) def test_prove_mul_bound_cannot_overflow_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') result, no_ovf_result = z3_mul_overflow(b1.concrete_variable, b2.concrete_variable) result1, no_ovf1 = z3_mul_overflow(b1.lower, b2.lower) result2, no_ovf2 = z3_mul_overflow(b1.lower, b2.upper) result3, no_ovf3 = z3_mul_overflow(b1.upper, b2.lower) result4, no_ovf4 = z3_mul_overflow(b1.upper, b2.upper) b1.prove_implies( b2, z3.And(no_ovf1, no_ovf2, no_ovf3, no_ovf4), no_ovf_result, ) def z3_pymod_nonzero(x, y): r = x % y res = r + (y & z3.If(y < 0, -r, r) >> (LONG_BIT - 1)) return res, y != 0 @z3_with_reduced_bitwidth(16) def test_prove_mod_bound_logic(): b1 = make_z3_intbounds_instance('self') b2 = make_z3_intbounds_instance('other') result, nonzero = z3_pymod_nonzero(b1.concrete_variable, b2.concrete_variable) b1.prove_implies( b2, nonzero, z3.And(result <= z3_max(b2.upper - 1, 0), z3_min(b2.lower + 1, 0) <= result) ) # ____________________________________________________________ # proofs for rewrite rules def test_int_xor_neg_one_is_invert(): x = BitVec('x') prove(x ^ -1 == ~x) def test_uint_cmp_equivalent_int_cmp_if_same_sign(): x = BitVec('x') y = BitVec('y') prove_implies( (x >= 0) == (y >= 0), z3.ULT(x, y) == (x < y), ) prove_implies( (x >= 0) == (y >= 0), z3.ULE(x, y) == (x <= y), ) prove_implies( (x >= 0) == (y >= 0), z3.UGT(x, y) == (x > y), ) prove_implies( (x >= 0) == (y >= 0), z3.UGE(x, y) == (x >= y), ) def test_prove_int_mul_1_lshift_rewrite(): x = BitVec('x') y = BitVec('y') prove_implies( 0 <= y, y < LONG_BIT, x * (1 << y) == x << y )