solver: fix solving with reduced bitwith (1e071937) · Commits · Marek Chalupa / slowbeast

slowbeast/bse/bsestate.py

+2 −5

Original line number	Diff line number	Diff line
		@@ -6,7 +6,7 @@ from slowbeast.domains.pointer import Pointer
		from slowbeast.symexe.annotations import ExprAnnotation, execute_annotation
		from slowbeast.symexe.executionstate import LazySEState, Nondet
		from slowbeast.util.debugging import ldbgv, print_stdout
		from slowbeast.solvers.solver import try_solve_incrementally
		from slowbeast.solvers.solver import solve_incrementally


		def _subst_val(substitute, val, subs):
		@@ -381,12 +381,9 @@ class BSEState(LazySEState):
		r = self._solver.try_is_sat(500, self.constraints(), e)
		if r is not None:
		return r
		r = try_solve_incrementally(
		return solve_incrementally(
		self.constraints(), e, self.expr_manager(), 2000, 500
		)
		if r is None:
		return True
		return r

		def __repr__(self):
		s = f"BSEState [{self.get_id()}]"

slowbeast/domains/symbolic.py

+7 −16

Original line number	Diff line number	Diff line
		@@ -832,26 +832,17 @@ if _use_z3:

		def _rdw(expr, bw):
		oldbw = expr.size()
		if oldbw <= bw:
		return expr
		return BVZExt(oldbw - bw, BVExtract(bw-1, 0, expr))

		def _reduce_arith_bitwidth(expr, bw):
		if is_const(expr):
		return expr
		chld = expr.children()
		if is_app_of(expr, Z3_OP_BADD):
		return simplify(
		_rdw(_reduce_arith_bitwidth(chld[0], bw), bw) +\
		_rdw(_reduce_arith_bitwidth(chld[1], bw), bw))
		elif is_app_of(expr, Z3_OP_BSUB):
		return simplify(
		_rdw(_reduce_arith_bitwidth(chld[0], bw), bw) -\
		_rdw(_reduce_arith_bitwidth(chld[1], bw), bw))
		elif is_app_of(expr, Z3_OP_BMUL):
		return simplify(
		_rdw(_reduce_arith_bitwidth(chld[0], bw), bw) *\
		_rdw(_reduce_arith_bitwidth(chld[1], bw), bw))
		if is_bv(expr):
		return _rdw(expr, bw)
		#oldbw = expr.size()
		#return BVExtract(bw-1, 0, expr) if oldbw > bw else expr
		else:
		red = (_reduce_arith_bitwidth(c, bw) for c in chld)
		red = (_reduce_arith_bitwidth(c, bw) for c in expr.children())
		if is_and(expr): return And(*red)
		elif is_or(expr): return Or(*red)
		return expr.decl()(*red)

slowbeast/solvers/solver.py

+12 −10

Original line number	Diff line number	Diff line
		@@ -287,7 +287,7 @@ def _rewrite_poly(em, exprs, assumptions=None):
		return em.conjunction(*A, expr1)
		return em.conjunction(expr1)

		def try_solve_incrementally(assumptions, exprs, em, to1=3000, to2=1000):
		def solve_incrementally(assumptions, exprs, em, to1=3000, to2=1000):
		# check if we can evaluate some expression syntactically
		for a in assumptions:
		exprs = [em.substitute(e, (a, em.getTrue())) for e in exprs]
		@@ -315,16 +315,19 @@ def try_solve_incrementally(assumptions, exprs, em, to1=3000, to2=1000):
		else:
		expr = _rewrite_poly(em, list(expr.children()))

		# FIXME try reduced bitwidth with propagating back models instead of this
		solver = IncrementalSolver()
		for bw in (2, 4, 8, 16):
		solver.add(expr.reduce_arith_bitwidth(bw).rewrite_and_simplify())
		for bw in (1, 2, 4, 8, 16, 24):
		# FIXME: handle signed/unsinged correctly in reduce_arith_bitwidth
		# and use that
		solver.add(expr.reduce_eq_bitwidth(bw).rewrite_and_simplify())
		r = solver.try_is_sat(bw*500)
		if r is False: return False
		elif r is None:
		break
		assert r is True
		# the reduce formula is sat. Try to check the original formula
		# with the knowledge about the reduced formula stored in the solver
		# the reduced subformulas are sat. Try to check the original formula
		# with the knowledge about the reduced formulas stored in the solver
		r = solver.try_is_sat(bw*500, expr)
		if r is not None:
		return r
		@@ -333,13 +336,12 @@ def try_solve_incrementally(assumptions, exprs, em, to1=3000, to2=1000):
		#
		rexpr, subs = expr.replace_arith_ops()
		if rexpr:
		solver = IncrementalSolver()
		solver.push()
		solver.add(rexpr.rewrite_and_simplify())
		for placeholder, e in _sort_subs(subs):
		if solver.is_sat() is False:
		return False
		solver.add(em.Eq(e, placeholder))
		# solve the un-abstracted expression
		return solver.try_is_sat(to2)
		# FIXME try reduced bitwidth and propagating back models
		return None
		solver.pop()
		# fall-back to solving the un-abstracted expression
		return solver.is_sat(expr)

slowbeast/symexe/executionstate.py

+3 −9

Original line number	Diff line number	Diff line
		@@ -2,7 +2,7 @@ from slowbeast.core.executionstate import ExecutionState
		from slowbeast.util.debugging import warn, ldbgv
		from slowbeast.ir.instruction import Alloc, GlobalVariable, Load
		from .constraints import ConstraintsSet, IncrementalConstraintsSet
		from slowbeast.solvers.solver import try_solve_incrementally
		from slowbeast.solvers.solver import solve_incrementally
		from copy import copy
		from sys import stdout

		@@ -99,10 +99,7 @@ class SEState(ExecutionState):
		if r is not None:
		return r

		r = try_solve_incrementally(self.constraints(), e, self.expr_manager())
		if r is not None:
		return r
		return self._solver.is_sat(self.expr_manager().conjunction(*e))
		return solve_incrementally(self.constraints(), e, self.expr_manager())

		def try_is_sat(self, timeout, *e):
		return self._solver.try_is_sat(timeout, self.constraints(), e)
		@@ -120,10 +117,7 @@ class SEState(ExecutionState):
		return r

		em = self.expr_manager()
		r = try_solve_incrementally([], C, em)
		if r is not None:
		return r
		return self._solver.is_sat(em.conjunction(*C))
		return solve_incrementally([], C, em)

		def concretize(self, *e):
		return self._solver.concretize(self.constraints(), *e)

Admin message