blackify (90843ca3) · Commits · Marek Chalupa / slowbeast

slowbeast/analysis/scc.py

+1 −1

Original line number	Diff line number	Diff line
		@@ -303,6 +303,7 @@ class StronglyConnectedComponents:
		edges = {l: [succ.target() for succ in l.successors()] for l in G.locations()}
		yield from strongly_connected_components_iterative(G.locations(), edges)


		class SCCCondensation:
		class SCC:
		def __init__(self, nodes):
		@@ -350,4 +351,3 @@ class SCCCondensation:

		def get(self, n):
		return self._node_to_scc[n]

slowbeast/bse/bself.py

+22 −20

Original line number	Diff line number	Diff line
		@@ -135,10 +135,14 @@ def _overapprox_with_assumptions(E, L, S, executor, s, target):
		P = create_set(p)
		rels = [r0 for r0 in R0 if not intersection(P, r0).is_empty()]
		yielded \|= bool(rels)
		yield from _yield_overapprox_with_assumption(E, L, S, executor, rels, s, target)
		yield from _yield_overapprox_with_assumption(
		E, L, S, executor, rels, s, target
		)
		# try constant relations too - if they hold in more steps, they may be invariant
		rels = [rc for rc in Rc if not intersection(P, rc).is_empty()]
		yield from _yield_overapprox_with_assumption(E, L, S, executor, rels, s, target)
		yield from _yield_overapprox_with_assumption(
		E, L, S, executor, rels, s, target
		)

		if not yielded:
		yield from _yield_overapprox_with_assumption(E, L, S, executor, R0, s, target)
		@@ -162,11 +166,11 @@ def _yield_overapprox_with_assumption(E, L, S, executor, rels, s, target):
		def is_seq_inductive(seq, executor, L: LoopInfo):
		return L.set_is_inductive(seq.as_set())


		def is_set_inductive(S, executor, L: LoopInfo):
		return L.set_is_inductive(S)



		class BSELFChecker(BaseBSE):
		"""
		An executor that recursively checks the validity of one particular assertion.
		@@ -566,11 +570,7 @@ class BSELFChecker(BaseBSE):
		yield InductiveSequence(A)

		# try without relations
		seq = InductiveSequence(
		overapprox_set(
		self, EM, S, unsafe, target, None, L
		)
		)
		seq = InductiveSequence(overapprox_set(self, EM, S, unsafe, target, None, L))

		if is_seq_inductive(seq, self, L):
		# check if seq is a subset of some previously yielded sequence
		@@ -639,9 +639,7 @@ class BSELFChecker(BaseBSE):
		for s in sets:
		# gather the sets that subsume 's' and are disjunctive with unsafe
		# states
		cov = [
		I for I in isets if intersection(E, s).is_empty() and I.includes(s)
		]
		cov = [I for I in isets if intersection(E, s).is_empty() and I.includes(s)]
		if cov:
		dbg("Matched stored inductive sequences")
		S = create_set() if union_matched else None
		@@ -739,7 +737,9 @@ class BSELFChecker(BaseBSE):

		if __debug__:
		for seq0 in seqs0:
		assert intersection(seq0.as_set(), E).is_empty(), "Initial sequence contains error states"
		assert intersection(
		seq0.as_set(), E
		).is_empty(), "Initial sequence contains error states"

		# now we do not support empty sequences
		assert all(map(lambda s: s is not None, seqs0)), "A sequence is none"
		@@ -793,7 +793,9 @@ class BSELFChecker(BaseBSE):
		dbg(f"{seq}", color="dark_blue")

		if __debug__:
		assert intersection( seq.as_set(), E ).is_empty(), "Sequence is not safe"
		assert intersection(
		seq.as_set(), E
		).is_empty(), "Sequence is not safe"

		if len(seq) >= max_seq_len:
		dbg("Give up extending the sequence, it is too long")

slowbeast/bse/bsestate.py

+9 −3

Original line number	Diff line number	Diff line
		@@ -136,9 +136,15 @@ class BSEState(LazySEState):
		if mo.is_global() and mo.is_zeroed():
		constraints.append(em.Eq(val[0], ConcreteInt(0, val[0].bitwidth())))
		else:
		for g, ptr in ((g, ptr) for (g, ptr) in IM.bound_globals() if g.is_zeroed()):
		constraints.append(em.Or(em.Ne(obj, ptr.object()),
		em.Eq(val[0], ConcreteInt(0, val[0].bitwidth()))))
		for g, ptr in (
		(g, ptr) for (g, ptr) in IM.bound_globals() if g.is_zeroed()
		):
		constraints.append(
		em.Or(
		em.Ne(obj, ptr.object()),
		em.Eq(val[0], ConcreteInt(0, val[0].bitwidth())),
		)
		)
		return constraints

		def _memory_constraints(self):

slowbeast/bse/inductivesequence.py

+0 −1

Original line number	Diff line number	Diff line
		@@ -121,4 +121,3 @@ class InductiveSequence:

		def check_ind_on_paths(self, executor, paths, target=None):
		return self.check_on_paths(executor, paths, target=target, self_as_pre=True)

slowbeast/domains/symbolic.py

+18 −15

Original line number	Diff line number	Diff line
		@@ -751,7 +751,6 @@ if _use_z3:
		except ValueError:
		return None


		def get_eqs_from_ineqs(expr):
		###
		# check for equalities from inequalities:
		@@ -773,11 +772,11 @@ if _use_z3:
		if nc in clauses:
		eqs.append((clause, nc, chld[0] == chld[1]))
		continue
		nc = (chld[1] <= chld[0])
		nc = chld[1] <= chld[0]
		if nc in clauses:
		eqs.append((clause, nc, chld[0] == chld[1]))
		continue
		nc = (chld[0] >= chld[1])
		nc = chld[0] >= chld[1]
		if nc in clauses:
		eqs.append((clause, nc, chld[0] == chld[1]))
		continue
		@@ -850,8 +849,10 @@ if _use_z3:
		return expr
		else:
		red = [_reduce_eq_bitwidth(c, bw) for c in chld]
		if is_and(expr): return mk_and(*red)
		elif is_or(expr): return mk_or(*red)
		if is_and(expr):
		return mk_and(*red)
		elif is_or(expr):
		return mk_or(*red)
		else:
		return expr.decl()(*red)

		@@ -865,7 +866,6 @@ if _use_z3:
		except ValueError:
		return None


		def _rdw(expr, bw):
		oldbw = expr.size()
		if oldbw <= bw:
		@@ -879,11 +879,12 @@ if _use_z3:
		# return BVExtract(bw-1, 0, expr) if oldbw > bw else expr
		else:
		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)
		if is_and(expr):
		return And(*red)
		elif is_or(expr):
		return Or(*red)
		return expr.decl()(*red)


		def reduce_arith_bitwidth(expr, bw):
		# return _reduce_arith_bitwidth(expr, bw, variables)
		try:
		@@ -1078,7 +1079,9 @@ class Expr(Value):
		return Expr(expr, ty)

		def rewrite_polynomials(self, from_exprs):
		expr = rewrite_polynomials(self.unwrap(), map(lambda x: x.unwrap(), from_exprs) if from_exprs else None)
		expr = rewrite_polynomials(
		self.unwrap(), map(lambda x: x.unwrap(), from_exprs) if from_exprs else None
		)
		if expr is None:
		return self
		return Expr(expr, self.type())