#!/usr/bin/env pypy # encoding: utf-8 """ The purpose of this test file is to check that the optimizeopt *test* cases are correct. It uses the z3 SMT solver to check the before/after optimization traces for equivalence. Only supports very few operations for now, but would have found the buggy tests in d9616aacbd02/issue #3832. It can also be used to do bounded model checking on the optimizer, by generating random traces.""" import sys import time, io import pytest import struct from rpython.rlib.rarithmetic import LONG_BIT, r_uint, intmask from rpython.rlib.longlong2float import float2longlong from rpython.jit.metainterp.optimizeopt.test.test_util import ( BaseTest, convert_old_style_to_targets, FakeJitDriverStaticData) from rpython.jit.metainterp.optimizeopt.test.test_optimizeintbound import ( TestOptimizeIntBounds as TOptimizeIntBounds) from rpython.jit.metainterp.optimizeopt.test.test_optimizeheap import ( TestOptimizeHeap as TOptimizeHeap) from rpython.rtyper import rclass from rpython.jit.metainterp import compile from rpython.jit.metainterp.resoperation import ( rop, ResOperation, InputArgInt, OpHelpers, InputArgRef, AbstractResOp) from rpython.jit.metainterp.history import ( JitCellToken, Const, ConstInt, ConstPtr, ConstFloat, get_const_ptr_for_string) from rpython.jit.tool.oparser import parse, convert_loop_to_trace from rpython.jit.backend.test.test_random import RandomLoop, Random, OperationBuilder, AbstractOperation from rpython.jit.backend.test.test_random import GuardPtrOperation from rpython.jit.backend.test import test_ll_random from rpython.jit.backend.llgraph.runner import LLGraphCPU from rpython.jit.codewriter.effectinfo import EffectInfo from rpython.jit.metainterp.optimizeopt.intutils import MININT, MAXINT from rpython.jit.metainterp.history import new_ref_dict from rpython.rtyper.lltypesystem import lltype try: import z3 from hypothesis import given, strategies except ImportError: pytest.skip("please install z3 (z3-solver on pypi) and hypothesis") TRUEBV = z3.BitVecVal(1, LONG_BIT) FALSEBV = z3.BitVecVal(0, LONG_BIT) class CheckError(Exception): pass def check_z3(beforeinputargs, beforeops, afterinputargs, afterops): c = Checker(beforeinputargs, beforeops, afterinputargs, afterops) c.check() return c.unsat_count, c.unknown_count def z3_pydiv(x, y): r = x / y psubx = r * y - x return z3.If( y == z3.BitVecVal(0, LONG_BIT), z3.BitVecVal(0xdeadbeef, LONG_BIT), # XXX model "undefined" better r + (z3.If(y < 0, psubx, -psubx) >> (LONG_BIT - 1))) def z3_pymod(x, y): r = x % y return z3.If( y == z3.BitVecVal(0, LONG_BIT), z3.BitVecVal(0xdeadbeef, LONG_BIT), r + (y & z3.If(y < 0, -r, r) >> (LONG_BIT - 1))) class Checker(object): def __init__(self, beforeinputargs, beforeops, afterinputargs, afterops): self.solver = z3.Solver() if pytest.config.option.z3timeout: self.solver.set("timeout", pytest.config.option.z3timeout) self.box_to_z3 = {} self.seen_names = {} self.constptr_to_z3 = new_ref_dict() self.beforeinputargs = beforeinputargs self.beforeops = beforeops self.afterinputargs = afterinputargs self.afterops = afterops self.unsat_count = self.unknown_count = 0 self.result_ovf = None self.heapindex = 0 self.arraycopyindex = 0 self.true_for_all_heaps = [] self.fresh_pointers = [] self._init_heap_types() def _init_heap_types(self): self.fielddescr_to_z3indexvar = {} self.nullpointer = z3.BitVec('NULL', LONG_BIT) self.solver_add(self.nullpointer == z3.BitVecVal(0, LONG_BIT)) self._lltype_to_index = {} def solver_add(self, cond): if z3.simplify(cond).eq(z3.BoolVal(True)): return res = self.solver.check(cond) # make sure that we don't add "False" to self.solver if res == z3.unsat: assert 0, "programming error, trying to add something to solver that is equivalent to False: " + str(cond) #z3res = self.solver.check(z3.Not(cond)) #if z3res == z3.unsat: # print "tautology, not adding:", cond # return self.solver.add(cond) def fielddescr_indexvar(self, descr): if descr in self.fielddescr_to_z3indexvar: return self.fielddescr_to_z3indexvar[descr] repr = "%s_%s" % (descr.S._name, descr.fieldname) var = z3.BitVec(repr, LONG_BIT) self.solver_add(var == len(self.fielddescr_to_z3indexvar)) self.fielddescr_to_z3indexvar[descr] = var return var def _lltype_heaptypes_index(self, T): if T in self._lltype_to_index: return self._lltype_to_index[T] # return negative numbers to not be confused with subclassrange_min values res = ~len(self._lltype_to_index) if isinstance(T, lltype.GcArray): varname = 'typeindex_array_%s' % (~res) else: varname = 'typeindex_struct_%s' % T._name z3heaptypeindex = z3.BitVec(self._unique_name(varname), LONG_BIT) self.solver_add(z3heaptypeindex == res) self._lltype_to_index[T] = z3heaptypeindex return z3heaptypeindex def convert(self, box): if isinstance(box, ConstInt): return z3.BitVecVal(box.getint(), LONG_BIT) if isinstance(box, ConstPtr): if not box.value: return self.nullpointer if box.value in self.constptr_to_z3: return self.constptr_to_z3[box.value] res = z3.BitVec('constPTR_%s' % len(self.constptr_to_z3), LONG_BIT) self.constptr_to_z3[box.value] = res is_array = False try: typeptr = lltype.cast_opaque_ptr(rclass.OBJECTPTR, box.value).typeptr except lltype.InvalidCast: T = lltype.typeOf(box.value._obj.container) typ = self._lltype_heaptypes_index(T) if isinstance(T, lltype.GcArray): is_array = True else: typ = typeptr.subclassrange_min self.solver_add(self.state.heaptypes[res] == typ) for freshptr in self.fresh_pointers: self.solver_add(freshptr != res) if is_array: self.solver_add(self.state.arraylength[res] == box.value._obj.container.getlength()) else: self.solver_add(self.state.arraylength[res] == -1) return res if isinstance(box, ConstFloat): if LONG_BIT != 64: pytest.skip("float checking not supported on 32-bit") return z3.BitVecVal(float2longlong(box.getfloat()), LONG_BIT) assert not isinstance(box, Const) # not supported return self.box_to_z3[box] def convertarg(self, box, arg): return self.convert(box.getarg(arg)) def newvar(self, box, repr=None): if repr is None: repr = box.repr_short(box._repr_memo) repr = self._unique_name(repr) result = z3.BitVec(repr, LONG_BIT) self.box_to_z3[box] = result return result def _unique_name(self, repr): while repr in self.seen_names: repr += "_" self.seen_names[repr] = None return repr def newheaptypes(self): pointersort = typesort = z3.BitVecSort(LONG_BIT) heaptypes = z3.Array('types', pointersort, typesort) self.solver_add(heaptypes[self.nullpointer] == -1) return heaptypes def newarraylength(self): pointersort = arraylengthsort = z3.BitVecSort(LONG_BIT) return z3.Array('arraylength', pointersort, arraylengthsort) def newheap(self): pointersort = z3.BitVecSort(LONG_BIT) heapobjectsort = z3.ArraySort(pointersort, pointersort) self.heapindex += 1 heap = z3.Array('heap%s'% self.heapindex, pointersort, heapobjectsort) for ptr, index, res in self.true_for_all_heaps: self.solver_add(heap[ptr][index] == res) return heap def print_chunk(self, chunk, label, model): print print "=============", label, "==================" for op in chunk: if op in self.box_to_z3: text = "-----> " + hex(intmask(r_uint(int(str(model[self.box_to_z3[op]]))))) else: text = "" print op, text def prove(self, cond, *ops): z3res = self.solver.check(z3.Not(cond)) if z3res == z3.unsat: self.unsat_count += 1 elif z3res == z3.unknown: self.unknown_count += 1 elif z3res == z3.sat: # not possible to prove! # print some nice stuff model = self.solver.model() print "ERROR counterexample:" print "inputs:" for beforeinput, afterinput in zip(self.beforeinputargs, self.afterinputargs): if model[self.box_to_z3[beforeinput]] is not None: print beforeinput, afterinput, hex(intmask(r_uint(int(str(model[self.box_to_z3[beforeinput]]))))) else: print beforeinput, afterinput, "unassigned in the model" print "chunks:" for i, chunk in enumerate(self.chunks): beforechunk, beforelast, afterchunk, afterlast = chunk if i == self.chunkindex: print "vvvvvvvvvvvvvvv Problem vvvvvvvvvvvvvvv" self.print_chunk(beforechunk + [beforelast], "before", model) self.print_chunk(afterchunk + [afterlast], "after", model) print if i == self.chunkindex: break print "END counterexample" # raise error l = [] if ops: l.append("in the following ops:") for op in ops: l.append(str(op)) l.append("the following SMT condition was not provable:") l.append(str(cond)) l.append("_________________") l.append("smt model:") l.append(str(self.solver)) l.append("_________________") l.append("counterexample:") l.append(str(model)) raise CheckError("\n".join(l)) def cond(self, z3expr): return z3.If(z3expr, TRUEBV, FALSEBV) def add_to_solver(self, ops, state): self.state = state for op in ops: if op.type != 'v': res = self.newvar(op) else: res = None opname = op.getopname() descr = op.getdescr() # clear state arg0 = arg1 = arg2 = None if not op.is_guard(): state.no_ovf = None else: assert state.before cond = self.guard_to_condition(op, state) # was optimized away, must be true self.prove(cond, op) continue # convert arguments if op.numargs() == 1: arg0 = self.convert(op.getarg(0)) elif op.numargs() == 2: arg0 = self.convert(op.getarg(0)) arg1 = self.convert(op.getarg(1)) elif op.numargs() == 3: arg0 = self.convert(op.getarg(0)) arg1 = self.convert(op.getarg(1)) arg2 = self.convert(op.getarg(2)) # compute results if opname == "int_add": expr = arg0 + arg1 elif opname == "int_sub": expr = arg0 - arg1 elif opname == "int_mul": expr = arg0 * arg1 elif opname == "int_and": expr = arg0 & arg1 elif opname == "int_or": expr = arg0 | arg1 elif opname == "int_xor": expr = arg0 ^ arg1 elif opname == "int_eq": expr = self.cond(arg0 == arg1) elif opname == "int_ne": expr = self.cond(arg0 != arg1) elif opname == "int_lt": expr = self.cond(arg0 < arg1) elif opname == "int_le": expr = self.cond(arg0 <= arg1) elif opname == "int_gt": expr = self.cond(arg0 > arg1) elif opname == "int_ge": expr = self.cond(arg0 >= arg1) elif opname == "int_is_true": expr = self.cond(arg0 != FALSEBV) elif opname == "uint_lt": expr = self.cond(z3.ULT(arg0, arg1)) elif opname == "uint_le": expr = self.cond(z3.ULE(arg0, arg1)) elif opname == "uint_gt": expr = self.cond(z3.UGT(arg0, arg1)) elif opname == "uint_ge": expr = self.cond(z3.UGE(arg0, arg1)) elif opname == "int_is_zero": expr = self.cond(arg0 == FALSEBV) elif opname == "int_neg": expr = -arg0 elif opname == "int_invert": expr = ~arg0 elif opname == "int_lshift": expr = arg0 << arg1 elif opname == "int_rshift": expr = arg0 >> arg1 elif opname == "uint_rshift": expr = z3.LShR(arg0, arg1) elif opname == "int_add_ovf": expr = arg0 + arg1 m = z3.SignExt(LONG_BIT, arg0) + z3.SignExt(LONG_BIT, arg1) state.no_ovf = m == z3.SignExt(LONG_BIT, expr) elif opname == "int_sub_ovf": expr = arg0 - arg1 m = z3.SignExt(LONG_BIT, arg0) - z3.SignExt(LONG_BIT, arg1) state.no_ovf = m == z3.SignExt(LONG_BIT, expr) elif opname == "int_mul_ovf": expr = arg0 * arg1 m = z3.SignExt(LONG_BIT, arg0) * z3.SignExt(LONG_BIT, arg1) state.no_ovf = m == z3.SignExt(LONG_BIT, expr) elif opname == "int_signext": numbits = op.getarg(1).getint() * 8 expr = z3.SignExt(64 - numbits, z3.Extract(numbits - 1, 0, arg0)) elif opname == "int_force_ge_zero": expr = z3.If(arg0 < 0, 0, arg0) elif opname == "uint_mul_high": # zero-extend args to 2*LONG_BIT bit, then multiply and extract # highest LONG_BIT bits zarg0 = z3.ZeroExt(LONG_BIT, arg0) zarg1 = z3.ZeroExt(LONG_BIT, arg1) expr = z3.Extract(LONG_BIT * 2 - 1, LONG_BIT, zarg0 * zarg1) elif opname == "same_as_i" or opname == "same_as_r": expr = arg0 # heap operations elif opname == "ptr_eq" or opname == "instance_ptr_eq": expr = self.cond(arg0 == arg1) elif opname == "ptr_ne" or opname == "instance_ptr_ne": expr = self.cond(arg0 != arg1) elif opname == "new_with_vtable": expr = res self.fresh_pointer(res) vtable = descr.get_vtable().adr.ptr self.solver_add(state.heaptypes[expr] == vtable.subclassrange_min) self.solver_add(state.heap[expr] == z3.K(z3.BitVecSort(LONG_BIT), z3.BitVecVal(0, LONG_BIT))) elif opname == "getfield_gc_i" or opname == "getfield_gc_r":# int and reference # we dont differentiate between struct and field in z3 heap structure # so a field is an array at a specific index # thus we need to set the types for array and field writes, so z3 knows they cant interfere index = self.fielddescr_indexvar(descr) parentdescr = descr.get_parent_descr() if parentdescr.is_object(): vtable = parentdescr.get_vtable().adr.ptr self.solver_add(state.heaptypes[arg0] >= vtable.subclassrange_min) self.solver_add(state.heaptypes[arg0] <= vtable.subclassrange_max) expr = state.heap[arg0][index] if descr.is_always_pure(): self.true_for_all_heaps.append((arg0, index, expr)) if isinstance(op.getarg(0), ConstPtr) and descr.is_always_pure(): ptr = lltype.cast_opaque_ptr(lltype.Ptr(descr.S), op.getarg(0).value) const_res = getattr(ptr, descr.fieldname) assert opname == "getfield_gc_i" self.solver_add(expr == const_res) if descr.is_integer_bounded(): self.solver_add(expr >= descr.get_integer_min()) self.solver_add(expr <= descr.get_integer_max()) elif opname == "setfield_gc": index = self.fielddescr_indexvar(descr) # copys old heap with new value inserted heapexpr = z3.Store(state.heap, arg0, z3.Store(state.heap[arg0], index, arg1)) parentdescr = descr.get_parent_descr() if parentdescr.is_object(): vtable = parentdescr.get_vtable().adr.ptr self.solver_add(state.heaptypes[arg0] >= vtable.subclassrange_min) self.solver_add(state.heaptypes[arg0] <= vtable.subclassrange_max) # create new heap state.heap = self.newheap() # set new heap to modified heap with constraint self.solver_add(state.heap == heapexpr) # mark arg1 as non-null if arg1 is const or constptr if self.is_const(op.getarg(1)): self.solver_add(arg0 != self.nullpointer) elif opname == "getarrayitem_gc_r" or opname == "getarrayitem_gc_i" or opname == "getarrayitem_gc_f": # TODO: immutable arrays z3typ = self._lltype_heaptypes_index(descr.A) self.solver_add(state.heaptypes[arg0] == z3typ) self.solver_add(arg1 >= 0) self.solver_add(arg1 < state.arraylength[arg0]) expr = state.heap[arg0][arg1] if descr.is_item_integer_bounded(): self.solver_add(expr >= descr.get_item_integer_min()) self.solver_add(expr <= descr.get_item_integer_max()) elif opname == "setarrayitem_gc": heapexpr = z3.Store(state.heap, arg0, z3.Store(state.heap[arg0], arg1, arg2)) z3typ = self._lltype_heaptypes_index(descr.A) self.solver_add(state.heaptypes[arg0] == z3typ) self.solver_add(arg1 >= 0) self.solver_add(arg1 < state.arraylength[arg0]) state.heap = self.newheap() self.solver_add(state.heap == heapexpr) if self.is_const(op.getarg(2)): self.solver_add(arg0 != self.nullpointer) elif opname == "arraylen_gc": expr = state.arraylength[arg0] self.solver_add(expr >= 0) elif opname == "new_array" or opname == "new_array_clear": expr = res self.fresh_pointer(res) z3typ = self._lltype_heaptypes_index(descr.A) self.solver_add(state.heaptypes[res] == z3typ) # new_array cant return null self.solver_add(res != self.nullpointer) # store array len self.solver_add(state.arraylength[res] == arg0) self.solver_add(state.heap[expr] == z3.K(z3.BitVecSort(LONG_BIT), z3.BitVecVal(0, LONG_BIT))) elif opname == "escape_n": # the heap is completely new, but it's the same between # the before and the after state state.heap = state.nextheap(self) # end heap operations elif opname in ["label", "escape_i", "debug_merge_point", "force_token"]: # TODO: handling escape this way probably is not correct continue # ignore for now elif opname == "call_n": effectinfo = op.getdescr().get_extra_info() oopspecindex = effectinfo.oopspecindex if oopspecindex == EffectInfo.OS_ARRAYCOPY or oopspecindex == EffectInfo.OS_ARRAYMOVE: array_from = self.convert(op.getarg(1)) # from array if oopspecindex == EffectInfo.OS_ARRAYCOPY: array_to = self.convert(op.getarg(2)) # to array index_from = self.convert(op.getarg(3)) # from index index_to = self.convert(op.getarg(4)) # to index len_arg = op.getarg(5) copy_len = self.convert(len_arg) # len else: array_to = array_from # to array index_from = self.convert(op.getarg(2)) # from index index_to = self.convert(op.getarg(3)) # to index len_arg = op.getarg(4) copy_len = self.convert(len_arg) # len z3typ = self._lltype_heaptypes_index(effectinfo.single_write_descr_array.A) # set types for both arrays self.solver_add(state.heaptypes[array_from] == z3typ) if oopspecindex == EffectInfo.OS_ARRAYCOPY: self.solver_add(state.heaptypes[array_to] == z3typ) if self.is_const(len_arg): len_arg_const = len_arg.getint() # do nothing on len=0 moves/copies if len_arg_const == 0: continue # do the copy manually, to not need a forall curr_heap = state.heap for i in range(len_arg_const): heapexpr = z3.Store(curr_heap, array_to, z3.Store(curr_heap[array_to], index_to + i, curr_heap[array_from][index_from + i])) new_heap = self.newheap() self.solver.add(new_heap == heapexpr) curr_heap = new_heap state.heap = curr_heap continue # general case, use forall #self.solver_add(state.heaptypes[array_from] == z3type) #if oopspecindex == EffectInfo.OS_ARRAYCOPY: #self.solver_add(state.heaptypes[array_to] == z3type) # create vars for copy ranges arr_range_from = z3.BitVec('__arr_index_from_%d' % self.arraycopyindex, LONG_BIT) arr_range_to = z3.BitVec('__arr_index_to_%d' % self.arraycopyindex, LONG_BIT) other_range = z3.BitVec('__arr_other_index_%d' % self.arraycopyindex, LONG_BIT) p = z3.BitVec('__arr_pointer_%d' % self.arraycopyindex, LONG_BIT) # create new heap, but dont set to state yet new_heap = self.newheap() # constraint copy ranges with index and len self.solver.add(z3.ForAll([arr_range_from, arr_range_to], # ∀ from_idx, to_idx: z3.Implies(z3.And( z3.And(arr_range_from >= index_from, arr_range_from < index_from + copy_len), # (index_from <= from_idx < index_from + copy_len && z3.And(arr_range_to >= index_to, arr_range_to < arr_range_to + copy_len)), # index_to <= to_idx < index_to + copy_len) => new_heap[array_to][arr_range_to] == state.heap[array_from][arr_range_from]))) # all other indexes of arg2 stay the same self.solver.add(z3.ForAll([other_range], z3.Implies(z3.And(other_range < index_to, other_range >= index_to + copy_len), new_heap[array_to][other_range] == state.heap[array_to][other_range]))) # new heap is same as old heap for all other pointers self.solver.add(z3.ForAll([p], z3.Implies(p != array_to, new_heap[p] == state.heap[p]))) state.heap = new_heap self.arraycopyindex += 1 else: assert 0, "unsupported" elif opname == "call_pure_i" or opname == "call_i": # only div and mod supported effectinfo = op.getdescr().get_extra_info() oopspecindex = effectinfo.oopspecindex if oopspecindex == EffectInfo.OS_INT_PY_DIV: arg0 = self.convert(op.getarg(1)) # arg 0 is the function arg1 = self.convert(op.getarg(2)) expr = z3_pydiv(arg0, arg1) elif oopspecindex == EffectInfo.OS_INT_PY_MOD: arg0 = self.convert(op.getarg(1)) # arg 0 is the function arg1 = self.convert(op.getarg(2)) expr = z3_pymod(arg0, arg1) else: assert 0, "unsupported" else: assert 0, "unsupported" if res is not None: self.solver_add(res == expr) def is_const(self, arg): return isinstance(arg, Const) or isinstance(arg, ConstPtr) def fresh_pointer(self, res): for box, var in self.box_to_z3.iteritems(): if box.type == "r" and res is not var: self.solver_add(res != var) for const, z3var in self.constptr_to_z3.iteritems(): self.solver_add(res != z3var) self.fresh_pointers.append(res) def guard_to_condition(self, guard, state): opname = guard.getopname() if opname == "guard_true": return self.convertarg(guard, 0) == TRUEBV elif opname == "guard_false": return self.convertarg(guard, 0) == FALSEBV elif opname == "guard_value": return self.convertarg(guard, 0) == self.convertarg(guard, 1) elif opname == "guard_no_overflow": assert state.no_ovf is not None return state.no_ovf elif opname == "guard_overflow": assert state.no_ovf is not None return z3.Not(state.no_ovf) elif opname == "guard_class": arg0 = self.convertarg(guard, 0) cls = guard.getarg(1) vtable = cls.value.adr.ptr return state.heaptypes[arg0] == vtable.subclassrange_min elif opname == "guard_nonnull": # returns z3 var, or returns nullptr if no val in box return self.convertarg(guard, 0) != self.nullpointer elif opname == "guard_isnull": return self.convertarg(guard, 0) == self.nullpointer else: assert 0, "unsupported " + opname def check_last(self, beforelast, state_before, afterlast, state_after): if beforelast.getopname() in ("jump", "finish"): assert beforelast.numargs() == afterlast.numargs() for i in range(beforelast.numargs()): beforearg = beforelast.getarg(i) if beforearg.type == 'r' and isinstance(beforearg, AbstractResOp): if beforearg.opnum in (rop.NEW_WITH_VTABLE, rop.NEW, rop.NEW_ARRAY, rop.NEW_ARRAY_CLEAR): continue # the pointer addresses might be different before = self.convertarg(beforelast, i) after = self.convertarg(afterlast, i) self.prove(before == after, beforelast, afterlast) return assert beforelast.is_guard() # first, check the failing case cond_before = self.guard_to_condition(beforelast, state_before) if afterlast is None: # beforelast was optimized away, must be true self.prove(cond_before, beforelast) else: cond_after = self.guard_to_condition(afterlast, state_after) equivalent = cond_before == cond_after self.prove(equivalent, beforelast, afterlast) # then assert the true case self.solver_add(cond_before) if afterlast: self.solver_add(cond_after) def check(self): for beforeinput, afterinput in zip(self.beforeinputargs, self.afterinputargs): self.box_to_z3[beforeinput] = self.newvar(afterinput, "input_%s_%s" % (beforeinput, afterinput)) state_before = State() state_after = State(state_before) state_before.heap = state_after.heap = self.newheap()# heap is created new on every write state_before.heaptypes = state_after.heaptypes = self.newheaptypes()# types 'set' by constraints state_before.arraylength = state_after.arraylength = self.newarraylength() self.chunks = list(chunk_ops(self.beforeops, self.afterops)) for chunkindex, (beforechunk, beforelast, afterchunk, afterlast) in enumerate(self.chunks): self.chunkindex = chunkindex self.add_to_solver(beforechunk, state_before) self.add_to_solver(afterchunk, state_after) self.check_last(beforelast, state_before, afterlast, state_after) class State(object): def __init__(self, state_before=None): self.before = state_before is None self.no_ovf = None if self.before: self.heap_sequence = [] else: self.heap_sequence = state_before.heap_sequence self.heap_index = 0 def nextheap(self, checker): if self.before: res = checker.newheap() self.heap_sequence.append(res) else: res = self.heap_sequence[self.heap_index] self.heap_index += 1 return res def chunk_ops(beforeops, afterops): beforeops = list(reversed(beforeops)) afterops = list(reversed(afterops)) while 1: if not beforeops: assert not afterops return beforechunk, beforelast = up_to_guard(beforeops) afterchunk, afterlast = up_to_guard(afterops) while (beforelast is not None and (afterlast is None or beforelast.rd_resume_position < afterlast.rd_resume_position)): beforechunk.append(beforelast) bc, beforelast = up_to_guard(beforeops) beforechunk.extend(bc) if beforelast is None: beforelast = beforechunk.pop() if afterlast is None and afterchunk: afterlast = afterchunk.pop() yield beforechunk, beforelast, afterchunk, afterlast def up_to_guard(oplist): res = [] while oplist: op = oplist.pop() if op.is_guard(): return res, op res.append(op) return res, None def test_solver_add_false_protection(): c = Checker(None, None, None, None) x = z3.BitVec('x', 64) c.solver_add(x == 1) with pytest.raises(AssertionError): c.solver_add(x != 1) # ____________________________________________________________ class BaseCheckZ3(BaseTest): enable_opts = "intbounds:rewrite:virtualize:string:earlyforce:pure:heap" def optimize_loop(self, ops, optops, call_pure_results=None): from rpython.jit.metainterp.opencoder import Trace, TraceIterator loop = self.parse(ops) token = JitCellToken() if loop.operations[-1].getopnum() == rop.JUMP: loop.operations[-1].setdescr(token) exp = parse(optops, namespace=self.namespace.copy()) expected = convert_old_style_to_targets(exp, jump=True) call_pure_results = self._convert_call_pure_results(call_pure_results) trace = convert_loop_to_trace(loop, self.metainterp_sd) compile_data = compile.SimpleCompileData( trace, call_pure_results=call_pure_results, enable_opts=self.enable_opts) compile_data.forget_optimization_info = lambda *args, **kwargs: None jitdriver_sd = FakeJitDriverStaticData() info, ops = compile_data.optimize_trace(self.metainterp_sd, jitdriver_sd, {}) beforeinputargs, beforeops = trace.unpack() # check that the generated trace is correct correct, timeout = check_z3(beforeinputargs, beforeops, info.inputargs, ops) print 'correct conditions:', correct, 'timed out conditions:', timeout class TestBuggyTestsFail(BaseCheckZ3): def check_z3_throws_error(self, ops, optops, call_pure_results=None): from rpython.jit.metainterp.opencoder import Trace, TraceIterator loop = self.parse(ops) token = JitCellToken() if loop.operations[-1].getopnum() == rop.JUMP: loop.operations[-1].setdescr(token) trace = convert_loop_to_trace(loop, self.metainterp_sd) beforeinputargs, beforeops = trace.unpack() loopopt = self.parse(optops) if loopopt.operations[-1].getopnum() == rop.JUMP: loopopt.operations[-1].setdescr(token) opttrace = convert_loop_to_trace(loopopt, self.metainterp_sd) afterinputargs, afterops = opttrace.unpack() for afterop in afterops: assert not afterop.is_guard() # we can't chunk the operations when running in this mode with pytest.raises(CheckError): check_z3(beforeinputargs, beforeops, afterinputargs, afterops) def test_duplicate_getarrayitem_after_setarrayitem_3(self): ops = """ [p1, p2, p3, i1] setarrayitem_gc(p1, i1, p2, descr=arraydescr2) setarrayitem_gc(p1, 0, p3, descr=arraydescr2) p5 = getarrayitem_gc_r(p1, i1, descr=arraydescr2) jump(p5) """ expected = """ [p1, p2, p3, i1] setarrayitem_gc(p1, i1, p2, descr=arraydescr2) setarrayitem_gc(p1, 0, p3, descr=arraydescr2) jump(p2) """ self.check_z3_throws_error(ops, expected) class CallIntPyModPyDiv(AbstractOperation): def produce_into(self, builder, r): from rpython.jit.backend.test.test_random import getint k = r.random() if k < 0.20: v_second = ConstInt(r.random_integer()) else: v_second = r.choice(builder.intvars) if k > 0.80 and type(v_second) is not ConstInt: v_first = ConstInt(r.random_integer()) else: v_first = r.choice(builder.intvars) # exclude overflow and div by zero while (( getint(v_second) == -1 and getint(v_first) == MININT) or getint(v_second) == 0 ): v_second = ConstInt(r.random_integer()) if r.random() > 0.5: descr = BaseTest.int_py_div_descr res = getint(v_first) // getint(v_second) func = 12 else: descr = BaseTest.int_py_mod_descr res = getint(v_first) % getint(v_second) func = 14 ops = builder.loop.operations op = ResOperation(rop.INT_EQ, [v_second, ConstInt(0)]) op._example_int = 0 ops.append(op) op = ResOperation(rop.GUARD_FALSE, [op]) op.setdescr(builder.getfaildescr()) op.setfailargs(builder.subset_of_intvars(r)) ops.append(op) op1 = ResOperation(rop.INT_EQ, [v_first, ConstInt(MININT)]) op1._example_int = int(getint(v_first) == MININT) ops.append(op1) op2 = ResOperation(rop.INT_EQ, [v_second, ConstInt(-1)]) op2._example_int = int(getint(v_second) == -1) ops.append(op2) op = ResOperation(rop.INT_AND, [op1, op2]) op._example_int = 0 # excluded above ops.append(op) op = ResOperation(rop.GUARD_FALSE, [op]) op.setdescr(builder.getfaildescr()) op.setfailargs(builder.subset_of_intvars(r)) ops.append(op) op = ResOperation(rop.CALL_PURE_I, [ConstInt(func), v_first, v_second], descr=descr) if not hasattr(builder, "call_pure_results"): builder.call_pure_results = {} builder.call_pure_results[(ConstInt(func), ConstInt(getint(v_first)), ConstInt(getint(v_second)))] = ConstInt(res) op._example_int = res ops.append(op) builder.intvars.append(op) class RangeCheck(AbstractOperation): def produce_into(self, builder, r): from rpython.jit.backend.test.test_random import getint v_int = r.choice(list(set(builder.intvars) - set(builder.boolvars))) val = getint(v_int) ops = builder.loop.operations bound = r.random_integer() if bound > val: op = ResOperation(rop.INT_LE, [v_int, ConstInt(bound)]) else: op = ResOperation(rop.INT_GE, [v_int, ConstInt(bound)]) op._example_int = 1 ops.append(op) op = ResOperation(rop.GUARD_TRUE, [op]) op.setdescr(builder.getfaildescr()) op.setfailargs(builder.subset_of_intvars(r)) ops.append(op) class KnownBitsCheck(AbstractOperation): def produce_into(self, builder, r): # inject knowledge about a random subset of the bits of an integer # variable from rpython.jit.backend.test.test_random import getint v_int = r.choice(list(set(builder.intvars) - set(builder.boolvars))) val = getint(v_int) ops = builder.loop.operations mask = r.random_integer() res = val & mask op = ResOperation(rop.INT_AND, [v_int, ConstInt(mask)]) op._example_int = res ops.append(op) op = ResOperation(rop.GUARD_VALUE, [op, ConstInt(res)]) op.setdescr(builder.getfaildescr()) op.setfailargs(builder.subset_of_intvars(r)) ops.append(op) OPERATIONS = [op for op in OperationBuilder.OPERATIONS if not isinstance(op, GuardPtrOperation)] + [ #CallIntPyModPyDiv(rop.CALL_PURE_I)] + [ RangeCheck(None), KnownBitsCheck(None)] * 10 for i in range(4): OPERATIONS.append(test_ll_random.GetFieldOperation(rop.GETFIELD_GC_I)) OPERATIONS.append(test_ll_random.GetFieldOperation(rop.GETFIELD_GC_I)) OPERATIONS.append(test_ll_random.SetFieldOperation(rop.SETFIELD_GC)) #OPERATIONS.append(test_ll_random.NewOperation(rop.NEW)) OPERATIONS.append(test_ll_random.NewOperation(rop.NEW_WITH_VTABLE)) OPERATIONS.append(test_ll_random.GetArrayItemOperation(rop.GETARRAYITEM_GC_I)) OPERATIONS.append(test_ll_random.GetArrayItemOperation(rop.GETARRAYITEM_GC_I)) OPERATIONS.append(test_ll_random.SetArrayItemOperation(rop.SETARRAYITEM_GC)) OPERATIONS.append(test_ll_random.NewArrayOperation(rop.NEW_ARRAY_CLEAR)) OPERATIONS.append(test_ll_random.ArrayLenOperation(rop.ARRAYLEN_GC)) for i in range(2): OPERATIONS.append(test_ll_random.GuardClassOperation(rop.GUARD_CLASS)) class Z3OperationBuilder(test_ll_random.LLtypeOperationBuilder): produce_failing_guards = False OPERATIONS = OPERATIONS floatvars = [] class TestOptimizeIntBoundsZ3(BaseCheckZ3, TOptimizeIntBounds): def check_random_function_z3(self, cpu, r, num=None, max=None): t1 = time.time() output = io.BytesIO() loop = RandomLoop(cpu, Z3OperationBuilder, r, output=output) trace = convert_loop_to_trace(loop.loop, self.metainterp_sd) compile_data = compile.SimpleCompileData( trace, call_pure_results=self._convert_call_pure_results(getattr(loop.builder, 'call_pure_results', None)), enable_opts=self.enable_opts) jitdriver_sd = FakeJitDriverStaticData() info, ops = compile_data.optimize_trace(self.metainterp_sd, jitdriver_sd, {}) print info.inputargs for op in ops: print op beforeinputargs, beforeops = trace.unpack() # check that the generated trace is correct t2 = time.time() try: correct, timeout = check_z3(beforeinputargs, beforeops, info.inputargs, ops) except CheckError: print "to reproduce:" print "_" * 60 print make_reproducer(output.getvalue()) print "_" * 60 raise t3 = time.time() print 'generation/optimization [s]:', t2 - t1, 'z3:', t3 - t2, "total:", t3 - t1 print 'correct conditions:', correct, 'timed out conditions:', timeout if num is not None: print ' # passed (%d/%s).' % (num + 1, max) else: print ' # passed.' print def test_random_z3(self): cpu = LLGraphCPU(None) cpu.supports_floats = False cpu.setup_once() r = Random() seed = pytest.config.option.randomseed try: if pytest.config.option.repeat == -1: i = 0 while 1: self.check_random_function_z3(cpu, r, i) i += 1 seed = r.randrange(sys.maxint) r.seed(seed) else: for i in range(pytest.config.option.repeat): r.seed(seed) self.check_random_function_z3(cpu, r, i, pytest.config.option.repeat) seed = r.randrange(sys.maxint) except Exception as e: print "_" * 60 print "got exception", e print "seed was", seed raise @given(strategies.randoms()) def DISABLED_test_random_loop_parses(r): # guard_class doesn't parse right now unfortunately cpu = LLGraphCPU(None) cpu.supports_floats = False cpu.setup_once() output = io.BytesIO() try: loop = RandomLoop(cpu, Z3OperationBuilder, Random(r), output=output) except Exception: raise s = output.getvalue() r = make_reproducer(s) try: check_via_reproducer_string(r) except Exception as e: print "error", e print "to reproduce" print "_" * 60 print r print "_" * 60 raise def check_via_reproducer_string(r): d = {} exec r in d loop = d['loop'] cpu = LLGraphCPU(None) cpu.supports_floats = False cpu.setup_once() t = TestOptimizeIntBoundsZ3() t.cls_attributes() trace = convert_loop_to_trace(loop, t.metainterp_sd) compile_data = compile.SimpleCompileData( trace, call_pure_results=None, enable_opts=t.enable_opts) compile_data.forget_optimization_info = lambda *args, **kwargs: None jitdriver_sd = FakeJitDriverStaticData() info, ops = compile_data.optimize_trace(t.metainterp_sd, jitdriver_sd, {}) beforeinputargs, beforeops = trace.unpack() # check that the generated trace is correct correct, timeout = check_z3(beforeinputargs, beforeops, info.inputargs, ops) @given(strategies.randoms()) def test_random_hypothesis(r): cpu = LLGraphCPU(None) cpu.supports_floats = False cpu.setup_once() t = TestOptimizeIntBoundsZ3() t.cls_attributes() t.check_random_function_z3(cpu, Random(r), 0) def make_reproducer(s): lines = s.splitlines() assert "cpu.execute_token" in lines[-1] lines.pop() assert "loop_args =" in lines[-1] lines.pop() assert "cpu.compile_loop" in lines[-1] lines.pop() assert "looptoken =" in lines[-1] lines.pop() preamble = """\ from rpython.rtyper.lltypesystem import lltype, rffi, llmemory from rpython.rtyper import rclass from rpython.jit.metainterp.resoperation import rop, ResOperation, \ InputArgInt, InputArgRef, InputArgFloat from rpython.jit.metainterp.history import TargetToken, TreeLoop from rpython.jit.metainterp.history import BasicFailDescr, BasicFinalDescr from rpython.jit.metainterp.history import ConstInt, ConstPtr from rpython.jit.backend.llgraph.runner import LLGraphCPU as CPU from rpython.jit.codewriter import heaptracker if 1: """ post = """ loop = TreeLoop('reproduce') loop.inputargs = inputargs loop.operations = operations """ return preamble + "\n".join(lines) + post class TestOptimizeHeapZ3(BaseCheckZ3, TOptimizeHeap): def dont_execute(self): pass # skip, can't work yet test_nonvirtual_later = dont_execute test_nonvirtual_write_null_fields_on_force = dont_execute test_nonvirtual_array_write_null_fields_on_force = dont_execute test_arraycopy_1 = dont_execute test_arraycopy_not_virtual = dont_execute test_arraycopy_invalidate_3 = dont_execute test_varray_negative_items_from_invalid_loop = dont_execute test_virtual_array_of_struct = dont_execute test_virtual_array_of_struct_forced = dont_execute test_virtual_array_of_struct_arraycopy = dont_execute test_nonvirtual_array_of_struct_arraycopy = dont_execute test_varray_struct_negative_items_from_invalid_loop = dont_execute test_varray_struct_too_large_items = dont_execute if __name__ == '__main__': # this code is there so we can use the file to automatically reduce crashes # with shrinkray. # 1) install shrinkray # 2) put the buggy (big) trace into crash.txt # 3) run shrinkray like this: # shrinkray test/test_z3checktests.py crash.txt --timeout=100 # this takes a while (can be hours) but it will happily turn the huge trace # into a tiny one with open(sys.argv[1], "r") as f: ops = f.read() import pytest, os class config: class option: z3timeout = 100000 pytest.config = config try: check_via_reproducer_string(ops) except CheckError as e: print e os._exit(0) except Exception as e: print e os._exit(-1) os._exit(-1)