diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java index 2f14df0e..62171982 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java @@ -275,50 +275,64 @@ public LongValue F2L() { } /** - * Compares two floats and returns: 0 if both values are equal; 1 if this float is greater or - * either float is NaN; -1 if the parameter is greater ToDo (Nils): This method is not validated + * FCMPG instruction implementation. Compares two floats and returns: 0 if both values are + * equal; 1 if this float is greater or either float is NaN; -1 if the parameter is greater. * * @param f The other FloatValue * @return The resulting IntValue with the boolean conditions */ public IntValue FCMPG(FloatValue f) { - if (concrete.isNaN() || f.concrete.isNaN()) { - return new IntValue(context, 1); - } - return FCMP(f); + return FCMP(f, 1); } /** - * Compares two floats and returns: 0 if both values are equal 1 if this float is greater -1 if - * the parameter is greater or either float is NaN ToDo (Nils): This method is not validated + * FCMPL instruction implementation. Compares two floats and returns: 0 if both values are + * equal; 1 if this float is greater; -1 if the parameter is greater or either float is NaN. * * @param f The other FloatValue * @return The resulting IntValue with the boolean conditions */ public IntValue FCMPL(FloatValue f) { - if (concrete.isNaN() || f.concrete.isNaN()) { - return new IntValue(context, -1); - } - return FCMP(f); + return FCMP(f, -1); } /** - * Compares two floats and returns: 0 if both values are equal 1 if this float is greater -1 if - * the parameter is greater + * Compares two floats with IEEE 754 semantics (as FCMPG/FCMPL do, unlike Float.compareTo): + * nanResult if either value is NaN, 0 if both are equal (so 0.0 == -0.0), 1 if this float is + * greater, -1 if the parameter is greater. The formula has the NaN case too, so that the + * solver cannot pick a NaN input for an ordered comparison. * * @param f The other FloatValue + * @param nanResult The result if either value is NaN * @return The resulting IntValue with the boolean conditions */ - private IntValue FCMP(FloatValue f) { - int c = concrete.compareTo(f.concrete); + private IntValue FCMP(FloatValue f, int nanResult) { + float a = concrete; + float b = f.concrete; + int c; + if (Float.isNaN(a) || Float.isNaN(b)) { + c = nanResult; + } else if (a > b) { + c = 1; + } else if (a == b) { + c = 0; + } else { + c = -1; + } BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager(); + BooleanFormula isNaN = bmgr.or(fmgr.isNaN(formula), fmgr.isNaN(f.formula)); BooleanFormula eqCond = fmgr.equalWithFPSemantics(formula, f.formula); BooleanFormula gtCond = fmgr.greaterThan(formula, f.formula); - NumeralFormula.IntegerFormula tmp = - bmgr.ifThenElse(gtCond, imgr.makeNumber(1), imgr.makeNumber(-1)); - NumeralFormula.IntegerFormula res = bmgr.ifThenElse(eqCond, imgr.makeNumber(0), tmp); + NumeralFormula.IntegerFormula res = + bmgr.ifThenElse( + isNaN, + imgr.makeNumber(nanResult), + bmgr.ifThenElse( + gtCond, + imgr.makeNumber(1), + bmgr.ifThenElse(eqCond, imgr.makeNumber(0), imgr.makeNumber(-1)))); return new IntValue(context, c, res); } diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/primitive/numeric/floatingpoint/FloatValueTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/primitive/numeric/floatingpoint/FloatValueTest.groovy index 1081d342..716f1ecb 100644 --- a/symbolic-executor/src/test/groovy/de/uzl/its/value/primitive/numeric/floatingpoint/FloatValueTest.groovy +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/primitive/numeric/floatingpoint/FloatValueTest.groovy @@ -337,6 +337,43 @@ class FloatValueTest extends Specification { ].transpose().collect { (it[0] == Float.NaN || it[1] == Float.NaN) ? -1 : (it[0] == it[1] ? 0 : (it[0] > it[1] ? 1 : -1)) } } + def "FCMPG/FCMPL: a symbolic NaN operand gives the unordered result"(boolean greater, int unordered) { + given: "0.0f compared with a symbolic x that is currently 1.0f" + def zero = new FloatValue(context, 0.0f) + def x = new FloatValue(context, 1.0f, fpmgr.makeVariable("x", FloatValue.precision)) + + when: + def cmp = greater ? zero.FCMPG(x) : zero.FCMPL(x) + prover.addConstraint(fpmgr.isNaN(x.formula)) + prover.addConstraint(bmgr.not(bvmgr.equal(cmp.formula, bvmgr.makeBitvector(32, unordered)))) + + then: "no NaN x gives another result" + cmp.concrete == -1 + prover.isUnsat() + + where: + greater | unordered + true | 1 + false | -1 + } + + def "FCMPG/FCMPL: signed zeros compare equal"(boolean greater) { + given: + def pos = new FloatValue(context, 0.0f) + def neg = new FloatValue(context, -0.0f) + + when: + def cmp = greater ? pos.FCMPG(neg) : pos.FCMPL(neg) + prover.addConstraint(bvmgr.equal(cmp.formula, bvmgr.makeBitvector(32, 0))) + + then: + cmp.concrete == 0 + !prover.isUnsat() + + where: + greater << [true, false] + } + // ======================================================================== // Float Narrowing Conversions - Testing fpToIntFormula Fix // ======================================================================== diff --git a/symbolic-explorer/SymbolicExplorer.py b/symbolic-explorer/SymbolicExplorer.py index be21affd..fd7440b3 100755 --- a/symbolic-explorer/SymbolicExplorer.py +++ b/symbolic-explorer/SymbolicExplorer.py @@ -137,6 +137,7 @@ def init_args(parser: argparse.ArgumentParser): parser.add_argument("--sa-no-callback-targets", action="store_true", help="Do not count library calls as possible asserts when application code that library code may call back (overrides of library methods, lambdas) can reach an assert. Unsound: an assert reached only through such a callback can then give a false SAFE", default=False) parser.add_argument("--sa-rank-distance", action="store_true", help="Try branches closest to an assert (by static pre-analysis graph distance) first, instead of in plain DFS order", default=False) parser.add_argument("--solver-rlimit", type=int, default=0, help="Z3 resource limit (rlimit) for the first query of each branch in sv-comp mode; a branch that runs out is retried later with a growing limit. 0 (default): unlimited") + parser.add_argument("--divergence-retries", type=int, default=3, help="How often a branch is re-solved (with the failed solutions excluded) when the run of its solution does not reach it, before it is given up on, which rules out SAFE (sv-comp mode)") parser.add_argument("--parallel-sa", action="store_true", help="Run the static pre-analysis in the background and use it once it is ready (sv-comp mode). By default exploration waits for it: running it in parallel makes runs nondeterministic", default=False) # SV-COMP witness arguments: the explorer writes the violation witness from the trace of the diff --git a/symbolic-explorer/data/Database.py b/symbolic-explorer/data/Database.py index 53bf1882..c6dc2d51 100755 --- a/symbolic-explorer/data/Database.py +++ b/symbolic-explorer/data/Database.py @@ -37,6 +37,8 @@ def __init__(self): self.solutions = {} self.new_solutions = [] self.unsat_branches = [] + # Branches whose solutions repeatedly did not lead the run to them, given up on (by gid) + self.retired_branches = set() self.endpoints = list() self.traces: list[list[Branch | Special]] = list() self.instr_coverage = {'total_executed': {}, 'total_instr_count': 0, 'endpoints': {}} @@ -58,6 +60,8 @@ def reset(self): self.solutions = {} self.new_solutions = [] self.unsat_branches = [] + # Branches whose solutions repeatedly did not lead the run to them, given up on (by gid) + self.retired_branches = set() self.endpoints = list() self.traces: list[list[Branch | Special]] = list() self.instr_coverage = {'total_executed': {}, 'total_instr_count': 0, 'endpoints': {}} @@ -233,6 +237,26 @@ def clear_new_solutions(self): self.new_solutions.clear() lock.release() + def drop_solution(self, branch_id: int): + """Forgets the solution of the branch, so that it becomes a candidate again.""" + lock.acquire() + self.solutions.pop(branch_id, None) + if branch_id in self.new_solutions: + self.new_solutions.remove(branch_id) + lock.release() + + def retire_branch(self, branch_id: int): + """Takes the branch out of the candidates for good, without claiming it is infeasible.""" + lock.acquire() + self.retired_branches.add(branch_id) + lock.release() + + def get_retired_branches(self): + lock.acquire() + ret = set(self.retired_branches) + lock.release() + return ret + def add_unsat_branch(self, branch_id: int): lock.acquire() self.unsat_branches.append(branch_id) diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index a6c70f11..fc3cfd04 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -8,7 +8,7 @@ from pathlib import Path -from solver.SolverHandler import SATResult +from solver.SolverHandler import SATResult, Z3Handler from data.Database import Database from data.BinaryExecutionTree.Node import Node @@ -35,6 +35,15 @@ RLIMIT_GROWTH = 5 MAX_RLIMIT = 2**32 - 1 +# A solution whose run does not reach the side of the branch it was solved for is re-solved up to +# this many times (by default), each time with the solutions that failed so far excluded. Only if +# all of them fail too is the branch given up on, which rules out SAFE (see run()). +DIVERGENCE_RETRIES = 3 +# A retry first looks for small values: every integral input is bounded by each of these magnitudes +# in turn, then left unbounded. The solver likes extreme values such as 2^31-1 for a size, and then +# the allocation fails (OutOfMemoryError) before the run gets to the branch. +RETRY_BOUNDS = (16, 256, 65536) + # The (unique) endpoint ID for the SV-COMP target. As each target is handled separately, this ID is always 0. ENDPOINT_ID = 0 @@ -71,6 +80,8 @@ class State: def __init__(self): self.verdict = Verdict.UNKNOWN self.branch_to_explore: Node | None = None + # The solution the next run executes (for branch_to_explore) + self.solution: dict | None = None # Whether the solution for branch_to_explore came from a trace with an approximate model, # so that the next run may legitimately diverge from it. self.solution_is_guess: bool = False @@ -98,6 +109,13 @@ def __init__(self, args): self.solver_limit_hits = 0 # queries that ran out of their resource limit # How often each branch (by gid) ran out of its resource limit; each time multiplies it. self.rlimit_level: dict[int, int] = {} + self.divergence_retries = getattr(args, 'divergence_retries', DIVERGENCE_RETRIES) + # The solutions of each branch (by gid) whose runs did not reach it + self.failed_solutions: dict[int, list[dict]] = {} + # Branches given up on after their solutions kept failing, with the side that was not reached + # (True: branched), unless the solutions were only guesses (see check_divergence) + self.given_up: list[tuple[Node, bool]] = [] + self.divergence_retry_count = 0 # branches scheduled to be re-solved @contextmanager def pushd(self, dirname): @@ -255,6 +273,7 @@ def run_testcase(self, java_path, agentpath: str, configpath: str, z3path, port, if self.state.branch_to_explore: self.check_divergence(Database.instance().get_trace(-1)) # most recent trace self.state.branch_to_explore = None + self.state.solution = None self.state.solution_is_guess = False self.log_output(output) @@ -297,9 +316,8 @@ def run_testcase(self, java_path, agentpath: str, configpath: str, z3path, port, def check_divergence(self, trace) -> None: """Checks that the last run took the side of branch_to_explore its solution was solved for. - A divergence is a bug, unless the solution relied on an approximate model: then it was only a - guess, and the divergence is expected. That is logged without the "SWAT Assertion failed" - marker the harness counts as an internal error, and counted in the tree's statistics. + If not, the branch is re-solved with the failed solutions excluded (see solve_retry), up to + divergence_retries times; only then is it given up on (give_up_branch). """ target = self.state.branch_to_explore # The tree has one level per trace element, so the target is at its depth in the trace. @@ -318,12 +336,60 @@ def check_divergence(self, trace) -> None: reason = 'Branch does not appear in trace.' if self.state.solution_is_guess: Database.instance().record_expected_divergence(ENDPOINT_ID) - logger.info(f'[SVCOMP] Diverged from branch {target.id}: its solution relied on an approximate model (expected). {reason}') - else: - logger.error(f'[SVCOMP] SWAT Assertion failed: Target did not explore branch {target.id} as expected! {reason}') - # The branch counts as solved now, so its unexplored side is never tried again: an - # exhausted search no longer proves anything (see run()). - Database.instance().record_execution_error(ENDPOINT_ID, 'unexpected_divergence', f'branch {target.id}: {reason}') + failed = self.failed_solutions.setdefault(target.gid, []) + failed.append(self.state.solution or {}) + if len(failed) <= self.divergence_retries: + logger.info(f'[SVCOMP] Diverged from branch {target.id}{" (approximate model)" if self.state.solution_is_guess else ""}: {reason} ' + f'Re-solving it without the failed solutions ({len(failed)}/{self.divergence_retries}).') + Database.instance().drop_solution(target.gid) + self.divergence_retry_count += 1 + return + self.give_up_branch(target, self.state.solution_is_guess, reason) + + def give_up_branch(self, target: Node, guess: bool, reason: str) -> None: + """Takes a branch whose solutions kept missing it out of the search. + + A divergence is a bug, unless the solution relied on an approximate model: then it was only a + guess, and the divergence is expected (that run has precision loss, so it cannot end SAFE + anyway). That is logged without the "SWAT Assertion failed" marker the harness counts as an + internal error. + """ + Database.instance().retire_branch(target.gid) + tries = len(self.failed_solutions.get(target.gid, [])) + if guess: + logger.info(f'[SVCOMP] Diverged from branch {target.id}: its solution relied on an approximate model (expected). {reason} Giving up after {tries} solutions.') + return + logger.error(f'[SVCOMP] SWAT Assertion failed: Target did not explore branch {target.id} as expected! {reason} Giving up after {tries} solutions.') + # Its unexplored side is never tried again: an exhausted search no longer proves anything, + # unless some other run reaches that side after all (see run()). + Database.instance().record_execution_error(ENDPOINT_ID, 'unexpected_divergence', f'branch {target.id}: {reason}') + self.given_up.append((target, target.branched is None)) + + def unreached_given_up_branches(self) -> list[Node]: + """The given-up branches whose unexplored side no run has reached by now. A side reached + later is in the tree, so the search covers what lies behind it like any other.""" + return [n for n, branched in self.given_up if (n.branched if branched else n.skipped) is None] + + def solve_retry(self, branch: Node, rlimit: int | None) -> tuple[SATResult, dict]: + """Re-solves a branch whose solutions so far did not lead the run to it, excluding them. + + Small values are tried first (RETRY_BOUNDS), then any value. A bounded query that fails in + any way only moves on to the next bound. UNSAT without a bound means that no other solution + is left: the branch is given up on, as the encoding was evidently imprecise for it, the + branch is not claimed infeasible. + """ + failed = self.failed_solutions[branch.gid] + for bound in RETRY_BOUNDS + (None,): + extra = Z3Handler.retry_constraints(failed, bound) + sat, sol = StrategyService.solve_branch(branch, solver_timeout_ms=None, solver_rlimit=rlimit, extra_exprs=extra) + self.nr_solver_calls += 1 + if sat == SATResult.SAT or bound is None: + break + logger.debug(f'[SYMBOLIC EXPLORATION] Retry of branch {branch.id}: no solution with inputs bounded by {bound} ({sat})') + if sat == SATResult.UNSAT: + self.give_up_branch(branch, Database.instance().is_approximate_trace(ENDPOINT_ID, branch.trace_id), + 'No other solution left.') + return sat, sol def adopt_sa_graph(self): """Switches branch selection to the pre-analysis graph once it is ready (at most once). @@ -368,8 +434,11 @@ def solve_candidates(self, candidates: list[Node]) -> tuple[Node | None, dict, b alone = retry and len(pending) == 1 for branch in pending: rlimit = None if alone else self.solver_rlimit_for(branch) - sat, sol = StrategyService.solve_branch(branch, solver_timeout_ms=None, solver_rlimit=rlimit) - self.nr_solver_calls += 1 + if branch.gid in self.failed_solutions: + sat, sol = self.solve_retry(branch, rlimit) + else: + sat, sol = StrategyService.solve_branch(branch, solver_timeout_ms=None, solver_rlimit=rlimit) + self.nr_solver_calls += 1 if sat == SATResult.SAT: return branch, sol, gave_up if sat == SATResult.LIMIT: @@ -411,6 +480,7 @@ def retrieve_solution(self): logger.info(f'[SYMBOLIC EXPLORATION] Found solution for branch {branch.id} {"skipped" if branch.skipped is None else "branched"}') # remember which branch we want to explore self.state.branch_to_explore = branch + self.state.solution = sol self.state.solution_is_guess = Database.instance().is_approximate_trace(ENDPOINT_ID, branch.trace_id) sol_viz = [f'{key}: {val["plain_value"]}' for key, val in sol.items()] @@ -450,10 +520,13 @@ def run(self): logger.warning(f'[SVCOMP] Found symbolic precision loss') verdict = Verdict.UNKNOWN - if (verdict == Verdict.SAFE) and any(e.get('kind') == 'unexpected_divergence' - for e in Database.instance().get_tree(ENDPOINT_ID).execution_errors): - logger.warning(f'[SVCOMP] A solution did not reach the side of the branch it was solved for') - verdict = Verdict.UNKNOWN + if self.given_up: + unreached = self.unreached_given_up_branches() + if (verdict == Verdict.SAFE) and unreached: + logger.warning(f'[SVCOMP] No solution reached the side of branch(es) {[n.id for n in unreached]} it was solved for') + verdict = Verdict.UNKNOWN + elif not unreached: + logger.info(f'[SVCOMP] Other runs reached the sides of all given-up branches') if (verdict == Verdict.SAFE) and any(e.get('kind') == 'sa_desync' for e in Database.instance().get_tree(ENDPOINT_ID).execution_errors): @@ -490,7 +563,7 @@ def run(self): stats_file = os.path.join(log_dir, 'stats.json') write_testcase_stats(Path(stats_file), verdict, self.verification_category, Database.instance().get_tree(ENDPOINT_ID), self.round_idx, self.nr_solver_calls, self.sa.stats(self.sa_adopted_round), - self.solver_limit_hits) + self.solver_limit_hits, self.divergence_retry_count) self.kill_current_process() diff --git a/symbolic-explorer/solver/SolverHandler.py b/symbolic-explorer/solver/SolverHandler.py index 8e781a72..688cc530 100755 --- a/symbolic-explorer/solver/SolverHandler.py +++ b/symbolic-explorer/solver/SolverHandler.py @@ -380,7 +380,8 @@ def write_optimizer_to_file(optimizer: Optimize, output_dir: str = "smt_files") return filepath @staticmethod - def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000, rlimit: int | None = None) -> Tuple[SATResult, Dict[str, Any]]: + def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000, rlimit: int | None = None, + extra_exprs: list | None = None) -> Tuple[SATResult, Dict[str, Any]]: """ Solve for the given node and path constraints using ConstraintCache (modern approach). @@ -393,6 +394,8 @@ def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000, - timeout_ms: Wall-clock limit for the check, or None. - rlimit: Z3 resource limit for the check, or None. Unlike a timeout it is deterministic: the same query gets as far regardless of machine load. Running out of it gives LIMIT. + - extra_exprs: Further Z3 constraints (in the cache's shared context) on the inputs, e.g. + from retry_constraints(). Returns: - Tuple[SATResult, Dict[str, Any]]: Tuple containing SAT result and solution dictionary. @@ -434,6 +437,9 @@ def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000, for i, path_expr in enumerate(all_exprs[len(node_exprs):]): solver.add(path_expr) + for expr in extra_exprs or []: + solver.add(expr) + # Building the solver is Z3 work (SMT-LIB parsing on cache misses, assertion # construction), so it counts towards the SMT solver stage rather than the # explorer residual. It is not a query, hence count=False. @@ -521,6 +527,43 @@ def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000, logger.debug(f"[SOLVER] unknown: {reason}") return SATResult.UNKNOWN, {} + @staticmethod + def solution_values(sol: Dict[str, Any]) -> Dict[str, Any]: + """The scalar input values of a solution (from extract_and_encode_values) as Z3 values, + by name. Arrays are left out: their plain value is only a description.""" + return {name: val['plain_value'] for name, val in sol.items() if z3.is_expr(val.get('plain_value'))} + + @staticmethod + def retry_constraints(failed: list, bound: int | None = None, ctx=None) -> list: + """Constraints for re-solving a branch whose earlier solutions `failed` did not lead the + run to it: each of them is excluded (by its scalar inputs), and with `bound`, every + integral input is restricted to [-bound, bound] (chars: [0, bound]). + + Both only remove models, so UNSAT under them proves nothing about the branch. + """ + if ctx is None: + from solver.ConstraintCache import get_constraint_cache + ctx = get_constraint_cache().shared_context + exprs = [] + consts = {} + for sol in failed: + values = Z3Handler.solution_values(sol) + pairs = [(z3.Const(name, v.sort()), v) for name, v in values.items()] + consts.update((name, c) for (c, _), name in zip(pairs, values)) + # With no scalar input to tell models apart, the failed one cannot be excluded alone. + exprs.append(z3.Or([c != v for c, v in pairs]) if pairs else z3.BoolVal(False, ctx=ctx)) + if bound is not None: + for name, c in consts.items(): + if z3.is_bv(c): + width = c.size() + if name.startswith(DataTypes.CHAR.value + '_'): + exprs.append(z3.ULE(c, z3.BitVecVal(min(bound, 2**width - 1), width, ctx=c.ctx))) + elif bound < 2**(width - 1): + exprs.append(z3.And(c >= -bound, c <= bound)) + elif z3.is_int(c): + exprs.append(z3.And(c >= -bound, c <= bound)) + return exprs + @staticmethod def solve_with_optimization(node: Any, path_constraints: list) -> Tuple[SATResult, Dict[str, Any]]: """ diff --git a/symbolic-explorer/strategy/StrategyService.py b/symbolic-explorer/strategy/StrategyService.py index 9afe6927..4280a945 100755 --- a/symbolic-explorer/strategy/StrategyService.py +++ b/symbolic-explorer/strategy/StrategyService.py @@ -25,7 +25,9 @@ def select_branch(**kwargs): # changes, so which branches exist, and hence the verdict, does not. The sort is stable: # ties, and branches without SA information (ranked last), keep their DFS order. distances = {} if kwargs.get("rank_by_distance", False) else None - possible_branches = dfs(visited, tree, tree.root, db.get_solutions().keys(), db.get_unsat_branches(), kwargs.get("sa_node", None), distances=distances) + # A branch is not offered again once it is solved, or retired (its solutions kept missing it). + solved = db.get_solutions().keys() | db.get_retired_branches() + possible_branches = dfs(visited, tree, tree.root, solved, db.get_unsat_branches(), kwargs.get("sa_node", None), distances=distances) if distances: possible_branches.sort(key=lambda n: distances.get(n, math.inf)) # dfs records where the SA walk fell out of step on its tree, which is a copy. @@ -96,9 +98,12 @@ def collect_uf_definitions(node: Node) -> list(): @staticmethod def solve_branch(possible_branch: Node, endpoint_id=None, solver_timeout_ms: int | None = 60 * 1000, - solver_rlimit: int | None = None): + solver_rlimit: int | None = None, extra_exprs: list | None = None): """Solves for the unexplored side of the branch. LIMIT (the rlimit ran out) records nothing, - so the branch stays a candidate and can be retried with a larger limit.""" + so the branch stays a candidate and can be retried with a larger limit. + + extra_exprs further restrict the inputs (see Z3Handler.retry_constraints). UNSAT under them + does not make the branch infeasible, so it is not recorded either.""" db = Database.instance() path_constraints = StrategyService.collect_path_constrains(possible_branch) @@ -109,12 +114,13 @@ def solve_branch(possible_branch: Node, endpoint_id=None, solver_timeout_ms: int inputs = possible_branch.inputs - sat, sol = Z3Handler.solve(possible_branch, path_constraints, timeout_ms=solver_timeout_ms, rlimit=solver_rlimit) + sat, sol = Z3Handler.solve(possible_branch, path_constraints, timeout_ms=solver_timeout_ms, rlimit=solver_rlimit, + extra_exprs=extra_exprs) if sat == SATResult.SAT: db.add_solution(branch_id=possible_branch.gid, sol=sol, inputs=inputs, endpoint_id=endpoint_id) - elif sat == SATResult.UNSAT: + elif sat == SATResult.UNSAT and not extra_exprs: db.add_unsat_branch(possible_branch.gid) return sat, sol diff --git a/symbolic-explorer/svcomp/TestcaseStats.py b/symbolic-explorer/svcomp/TestcaseStats.py index 6f129eaa..e377481d 100644 --- a/symbolic-explorer/svcomp/TestcaseStats.py +++ b/symbolic-explorer/svcomp/TestcaseStats.py @@ -25,7 +25,7 @@ def _signature(inv: dict) -> str: def build_testcase_stats(verdict, category, tree, symbolic_exec_iterations: int, nr_solver_calls: int, static_analysis: dict, - solver_limit_hits: int = 0) -> dict: + solver_limit_hits: int = 0, divergence_retries: int = 0) -> dict: """ Assemble the consolidated per-testcase statistics dictionary. @@ -71,15 +71,18 @@ def build_testcase_stats(verdict, category, tree, symbolic_exec_iterations: int, 'solver_limit_hits': solver_limit_hits, # Runs that took another path than a solution based on an approximate model predicted. 'expected_divergences': tree.expected_divergences, + # Branches re-solved because the run of their previous solution did not reach them. + 'divergence_retries': divergence_retries, }, 'static_analysis': static_analysis, } def write_testcase_stats(filepath: Path, verdict, category, tree, symbolic_exec_iterations: int, nr_solver_calls: int, static_analysis: dict, - solver_limit_hits: int = 0): + solver_limit_hits: int = 0, divergence_retries: int = 0): """Write the consolidated per-testcase statistics to ``filepath`` as JSON.""" - data = build_testcase_stats(verdict, category, tree, symbolic_exec_iterations, nr_solver_calls, static_analysis, solver_limit_hits) + data = build_testcase_stats(verdict, category, tree, symbolic_exec_iterations, nr_solver_calls, static_analysis, solver_limit_hits, + divergence_retries) filepath.parent.mkdir(parents=True, exist_ok=True) with open(filepath, 'w') as f: diff --git a/symbolic-explorer/tests/test_divergence.py b/symbolic-explorer/tests/test_divergence.py index 3b543bc3..a338a9d8 100644 --- a/symbolic-explorer/tests/test_divergence.py +++ b/symbolic-explorer/tests/test_divergence.py @@ -1,6 +1,8 @@ """ -Unit tests for SVCompDriver.check_divergence: a run that does not take the side a solution was -solved for is an internal error, unless the solution relied on an approximate model. +Unit tests for the handling of divergences in SVCompDriver: a run that does not take the side a +solution was solved for gets the branch re-solved with the failed solutions excluded, up to +divergence_retries times. Only then is the branch given up on, which is an internal error (and rules +out SAFE) unless the solution relied on an approximate model. It imports the driver, which needs the explorer's dependencies (z3, fastapi, ...) that the system Python lacks, so run it with the harness venv, from symbolic-explorer/: @@ -13,74 +15,294 @@ from types import SimpleNamespace from unittest import mock +import z3 + sys.path.insert(0, os.path.join(os.path.dirname(__file__), '..')) from driver import SVCompDriver as svcomp +from solver.SolverHandler import SATResult, Z3Handler +from strategy.StrategyService import StrategyService def trace_branch(id, has_branched): return SimpleNamespace(id=id, has_branched=has_branched) -class CheckDivergenceTest(unittest.TestCase): +def int_solution(ctx, **values): + """A solution as Z3Handler.extract_and_encode_values builds it, for 32-bit int inputs.""" + return {name: {'encoded_value': str(v), 'plain_value': z3.BitVecVal(v, 32, ctx=ctx), 'index': name.split('_')[1]} + for name, v in values.items()} + + +class DivergenceTestBase(unittest.TestCase): def setUp(self): self.tree = SimpleNamespace(expected_divergences=0, execution_errors=[]) + self.dropped, self.retired = [], set() + self.approximate = False def record_expected_divergence(endpoint_id): self.tree.expected_divergences += 1 def record_execution_error(endpoint_id, kind, message): self.tree.execution_errors.append({'kind': kind, 'message': message}) db = SimpleNamespace(record_expected_divergence=record_expected_divergence, - record_execution_error=record_execution_error) + record_execution_error=record_execution_error, + drop_solution=self.dropped.append, + retire_branch=self.retired.add, + is_approximate_trace=lambda endpoint_id, trace_id: self.approximate) patcher = mock.patch.object(svcomp.Database, 'instance', return_value=db) patcher.start() self.addCleanup(patcher.stop) self.driver = svcomp.SVCompDriver.__new__(svcomp.SVCompDriver) + self.driver.args = SimpleNamespace(solver_rlimit=0) self.driver.state = svcomp.State() + self.driver.divergence_retries = 2 + self.driver.failed_solutions = {} + self.driver.given_up = [] + self.driver.divergence_retry_count = 0 + self.driver.nr_solver_calls = 0 + self.driver.solver_limit_hits = 0 + self.driver.rlimit_level = {} + self.ctx = z3.Context() # Solved to take the branched side, which the tree has not explored yet. - self.driver.state.branch_to_explore = SimpleNamespace(id=7, branched=None) + self.target = SimpleNamespace(id=7, gid=70, trace_id='t', branched=None, skipped=object(), parent=None) + self.aim(self.target, {'I_0': 1}) + + def aim(self, target, values): + self.driver.state.branch_to_explore = target + self.driver.state.solution = int_solution(self.ctx, **values) + self.driver.state.solution_is_guess = self.approximate def check(self, trace): with self.assertLogs(svcomp.logger, level='INFO') as logs: self.driver.check_divergence(trace) return '\n'.join(logs.output) + +class CheckDivergenceTest(DivergenceTestBase): + def test_taking_the_predicted_side_is_silent(self): with self.assertNoLogs(svcomp.logger, level='INFO'): self.driver.check_divergence([trace_branch(7, True)]) self.assertEqual(self.tree.expected_divergences, 0) + self.assertEqual(self.driver.failed_solutions, {}) def test_repeated_id_is_matched_by_position(self): # The target is at depth 2; the same id also occurs at depth 0 (e.g. a switch whose case # numbers wrap), taken the other way. Only the element at the target's depth counts. root = SimpleNamespace(parent=None) middle = SimpleNamespace(parent=root) - self.driver.state.branch_to_explore = SimpleNamespace(id=7, branched=None, parent=middle) + self.target.parent = middle with self.assertNoLogs(svcomp.logger, level='INFO'): self.driver.check_divergence([trace_branch(7, False), trace_branch(3, True), trace_branch(7, True)]) self.assertEqual(self.tree.execution_errors, []) - def test_divergence_of_an_exact_solution_is_an_error(self): + def test_divergence_is_retried_first(self): + out = self.check([trace_branch(7, False)]) + self.assertNotIn('SWAT Assertion failed', out) + self.assertIn('Re-solving', out) + # The branch becomes a candidate again, with the failed solution remembered. + self.assertEqual(self.dropped, [70]) + self.assertEqual(len(self.driver.failed_solutions[70]), 1) + self.assertEqual(self.tree.execution_errors, []) + self.assertEqual(self.retired, set()) + self.assertEqual(self.driver.divergence_retry_count, 1) + + def test_exact_solutions_that_keep_diverging_are_an_error(self): + for i in range(2): + self.aim(self.target, {'I_0': i}) + self.check([trace_branch(8, True)]) + self.assertEqual(self.tree.execution_errors, []) + self.aim(self.target, {'I_0': 2}) out = self.check([trace_branch(7, False)]) self.assertIn('ERROR', out) self.assertIn('SWAT Assertion failed', out) self.assertEqual(self.tree.expected_divergences, 0) - # Recorded, so that the run cannot end SAFE + # Recorded, so that the run cannot end SAFE, and out of the search for good self.assertEqual([e['kind'] for e in self.tree.execution_errors], ['unexpected_divergence']) + self.assertEqual(self.retired, {70}) + self.assertEqual(self.driver.unreached_given_up_branches(), [self.target]) + self.assertEqual(len(self.driver.failed_solutions[70]), 3) + + def test_no_retries(self): + self.driver.divergence_retries = 0 + out = self.check([trace_branch(7, False)]) + self.assertIn('SWAT Assertion failed', out) + self.assertEqual(self.dropped, []) + self.assertEqual(self.retired, {70}) def test_divergence_of_a_guess_is_expected(self): - self.driver.state.solution_is_guess = True + self.approximate = True + self.driver.divergence_retries = 0 + self.aim(self.target, {'I_0': 1}) out = self.check([trace_branch(7, False)]) self.assertNotIn('SWAT Assertion failed', out) self.assertNotIn('ERROR', out) self.assertEqual(self.tree.expected_divergences, 1) self.assertEqual(self.tree.execution_errors, []) + # Given up on, but no SAFE downgrade of its own: the approximate model already rules SAFE out. + self.assertEqual(self.retired, {70}) + self.assertEqual(self.driver.given_up, []) - def test_missing_branch_of_a_guess_is_expected(self): - self.driver.state.solution_is_guess = True + def test_guess_is_retried_too(self): + self.approximate = True + self.aim(self.target, {'I_0': 1}) out = self.check([trace_branch(8, True)]) self.assertNotIn('SWAT Assertion failed', out) self.assertEqual(self.tree.expected_divergences, 1) + self.assertEqual(self.dropped, [70]) + + def test_side_reached_later_lifts_the_downgrade(self): + self.driver.divergence_retries = 0 + self.check([trace_branch(7, False)]) + self.assertEqual(self.driver.unreached_given_up_branches(), [self.target]) + # Another run reaches the branched side after all: what lies behind it is in the tree now. + self.target.branched = object() + self.assertEqual(self.driver.unreached_given_up_branches(), []) + + def test_skipped_side(self): + target = SimpleNamespace(id=9, gid=90, trace_id='t', branched=object(), skipped=None, parent=None) + self.driver.divergence_retries = 0 + self.aim(target, {'I_0': 1}) + self.check([trace_branch(9, True)]) + self.assertEqual(self.driver.unreached_given_up_branches(), [target]) + target.skipped = object() + self.assertEqual(self.driver.unreached_given_up_branches(), []) + + +class SolveRetryTest(DivergenceTestBase): + """solve_retry tries the bounds in RETRY_BOUNDS, then no bound; only UNSAT without a bound + gives the branch up.""" + + def setUp(self): + super().setUp() + self.driver.failed_solutions[70] = [int_solution(self.ctx, I_0=2**31 - 1)] + self.calls = [] + + def solver(self, results): + def solve(b, solver_timeout_ms=None, solver_rlimit=None, extra_exprs=None): + self.calls.append((b.gid, solver_rlimit, len(extra_exprs or []))) + result = results[len(self.calls) - 1] + return result, ({'I_0': 3} if result == SATResult.SAT else {}) + return mock.patch.object(svcomp.StrategyService, 'solve_branch', side_effect=solve) + + def test_smallest_bound_first(self): + with self.solver([SATResult.SAT]): + sat, sol = self.driver.solve_retry(self.target, None) + self.assertEqual(sat, SATResult.SAT) + # The exclusion plus the bound on I_0 + self.assertEqual(self.calls, [(70, None, 2)]) + self.assertEqual(self.retired, set()) + + def test_bounded_failures_move_on(self): + results = [SATResult.UNSAT, SATResult.LIMIT, SATResult.UNKNOWN, SATResult.SAT] + with self.solver(results): + sat, _ = self.driver.solve_retry(self.target, 1000) + self.assertEqual(sat, SATResult.SAT) + self.assertEqual(self.calls, [(70, 1000, 2)] * 3 + [(70, 1000, 1)]) + self.assertEqual(self.driver.nr_solver_calls, 4) + self.assertEqual(self.retired, set()) + + def test_no_other_solution_gives_up(self): + with self.solver([SATResult.UNSAT] * 4): + with self.assertLogs(svcomp.logger, level='INFO') as logs: + sat, _ = self.driver.solve_retry(self.target, None) + self.assertEqual(sat, SATResult.UNSAT) + self.assertIn('SWAT Assertion failed', '\n'.join(logs.output)) + self.assertEqual(self.retired, {70}) + self.assertEqual([e['kind'] for e in self.tree.execution_errors], ['unexpected_divergence']) + + def test_unbounded_limit_is_passed_on(self): + # The caller escalates the resource limit; the branch is not given up on. + with self.solver([SATResult.UNSAT] * 3 + [SATResult.LIMIT]): + sat, _ = self.driver.solve_retry(self.target, 1000) + self.assertEqual(sat, SATResult.LIMIT) + self.assertEqual(self.retired, set()) + + def test_solve_candidates_routes_retries(self): + other = SimpleNamespace(id=8, gid=80, trace_id='t') + with self.solver([SATResult.UNSAT] * 4 + [SATResult.SAT]): + found, _, gave_up = self.driver.solve_candidates([self.target, other]) + self.assertIs(found, other) + self.assertFalse(gave_up) + self.assertEqual(self.retired, {70}) + + +class RetryConstraintsTest(unittest.TestCase): + """Z3Handler.retry_constraints on a real solver.""" + + def setUp(self): + self.ctx = z3.Context() + self.x = z3.BitVec('I_0', 32, ctx=self.ctx) + self.y = z3.BitVec('I_1', 32, ctx=self.ctx) + + def model(self, *exprs): + s = z3.Solver(ctx=self.ctx) + s.add(*exprs) + if s.check() != z3.sat: + return None + m = s.model() + return {str(d.name()): m[d].as_signed_long() for d in m.decls()} + + def test_failed_solutions_are_excluded(self): + failed = [int_solution(self.ctx, I_0=5), int_solution(self.ctx, I_0=6)] + extra = Z3Handler.retry_constraints(failed, ctx=self.ctx) + self.assertEqual(self.model(self.x >= 5, self.x <= 7, *extra), {'I_0': 7}) + self.assertIsNone(self.model(self.x >= 5, self.x <= 6, *extra)) + + def test_exclusion_is_by_the_whole_solution(self): + # Excluding (I_0=1, I_1=2) still allows I_0=1 with another I_1. + extra = Z3Handler.retry_constraints([int_solution(self.ctx, I_0=1, I_1=2)], ctx=self.ctx) + m = self.model(self.x == 1, self.y >= 2, self.y <= 3, *extra) + self.assertEqual(m, {'I_0': 1, 'I_1': 3}) + + def test_bound_gives_small_values(self): + failed = [int_solution(self.ctx, I_0=2**31 - 1)] + extra = Z3Handler.retry_constraints(failed, 16, ctx=self.ctx) + m = self.model(self.x > 1, *extra) + self.assertLessEqual(m['I_0'], 16) + self.assertGreater(m['I_0'], 1) + # Bounds are signed: negative values are bounded below as well. + m = self.model(self.x < 0, *extra) + self.assertGreaterEqual(m['I_0'], -16) + self.assertIsNone(self.model(self.x > 16, *extra)) + + def test_bound_beyond_the_type_is_left_out(self): + b = z3.BitVec('B_0', 8, ctx=self.ctx) + failed = [{'B_0': {'encoded_value': '5', 'plain_value': z3.BitVecVal(5, 8, ctx=self.ctx), 'index': '0'}}] + self.assertEqual(len(Z3Handler.retry_constraints(failed, 256, ctx=self.ctx)), 1) + self.assertEqual(len(Z3Handler.retry_constraints(failed, 16, ctx=self.ctx)), 2) + + def test_arrays_and_empty_solutions(self): + # Array entries carry no Z3 value; with nothing to tell models apart, all are excluded. + failed = [{'[I_0': {'encoded_value': '[1]', 'plain_value': 'K(Int, 1)', 'index': '0'}}] + extra = Z3Handler.retry_constraints(failed, ctx=self.ctx) + self.assertIsNone(self.model(*extra)) + + def test_strings_and_doubles_are_excluded_exactly(self): + s = z3.String('java/lang/String_0', ctx=self.ctx) + d = z3.FP('D_1', z3.Float64(self.ctx)) + failed = [{'java/lang/String_0': {'encoded_value': 'a', 'plain_value': z3.StringVal('a', ctx=self.ctx), 'index': '0'}, + 'D_1': {'encoded_value': '0', 'plain_value': z3.FPVal(-0.0, z3.Float64(self.ctx)), 'index': '1'}}] + extra = Z3Handler.retry_constraints(failed, 16, ctx=self.ctx) + sol = z3.Solver(ctx=self.ctx) + sol.add(s == z3.StringVal('a', ctx=self.ctx), z3.Or(d == z3.FPVal(0.0, z3.Float64(self.ctx)), d == z3.FPVal(-0.0, z3.Float64(self.ctx))), *extra) + self.assertEqual(sol.check(), z3.sat) + # Only the other zero is left: the exclusion is by bit pattern, not by FP equality. + self.assertEqual(sol.model().eval(d).as_string(), z3.FPVal(0.0, z3.Float64(self.ctx)).as_string()) + + +class SolveBranchTest(unittest.TestCase): + """UNSAT under retry constraints does not make the branch infeasible.""" + + def test_unsat_with_extra_constraints_is_not_recorded(self): + db = mock.Mock() + branch = SimpleNamespace(gid=1, id=1, trace_id='t', parent=None, inputs=[], ufs=[]) + with mock.patch('strategy.StrategyService.Database.instance', return_value=db), \ + mock.patch('strategy.StrategyService.Z3Handler.solve', return_value=(SATResult.UNSAT, {})): + StrategyService.solve_branch(branch, extra_exprs=['x']) + db.add_unsat_branch.assert_not_called() + StrategyService.solve_branch(branch) + db.add_unsat_branch.assert_called_once_with(1) if __name__ == '__main__': diff --git a/symbolic-explorer/tests/test_solver_rlimit.py b/symbolic-explorer/tests/test_solver_rlimit.py index 288d0e7f..a77da0e1 100644 --- a/symbolic-explorer/tests/test_solver_rlimit.py +++ b/symbolic-explorer/tests/test_solver_rlimit.py @@ -46,6 +46,7 @@ def driver(self, rlimit=BASE): d.nr_solver_calls = 0 d.solver_limit_hits = 0 d.rlimit_level = {} + d.failed_solutions = {} return d def solve(self, d, candidates, solver):