diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java index f280c9ba..523ba5bc 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java @@ -150,7 +150,12 @@ public static void terminate() { } SymbolicInstructionDispatcher.flush(); // TODO WTF does that do? calls log(null) <- I think what this does is removing that last symbolic instruction from the pipeline as symbolic execution is always one behind. - ThreadHandler.removeSolverContext(currentThread().getId()); + // An SV-COMP run is one execution per JVM, which exits right after it. Closing the + // solver context there only costs time: Z3 frees the terms of the trace one by one, + // which takes minutes after a long trace. + if (!config.getInstrumentationTransformer().equals(TransformerType.SV_COMP)) { + ThreadHandler.removeSolverContext(currentThread().getId()); + } ThreadHandler.removeThreadContext(currentThread().getId()); } catch (NoThreadContextException | ThreadAlreadyDisabledException e) { logger.warn(e.toString()); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java index e272cf71..696640b7 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java @@ -13,6 +13,8 @@ import de.uzl.its.swat.common.logging.GlobalLogger; import de.uzl.its.swat.common.logging.StatsStorage; import de.uzl.its.swat.common.logging.records.InvocationEntry; +import de.uzl.its.swat.config.Config; +import de.uzl.its.swat.solver.SolverMode; import de.uzl.its.swat.coverage.InstrCoverage; import de.uzl.its.swat.symbolic.trace.dto.*; import de.uzl.its.swat.thread.ThreadHandler; @@ -22,6 +24,7 @@ import java.util.Set; import java.util.List; import java.util.Map; +import java.util.regex.Pattern; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Formula; @@ -33,6 +36,7 @@ */ class DTOBuilder { private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger(); + private static final Pattern INPUT_NAME = Pattern.compile("[A-Z].*_[0-9].*"); /** * Encodes the symbolic trace as a JSON string. * @@ -85,9 +89,10 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage FormulaManager fmgr = ThreadHandler.getSolverContext(threadId).getFormulaManager(); + FormulaDumper dumper = FormulaDumper.of(fmgr); for (InputElement ie : symbolicTrace.getInputs()) { - String lowerBound = String.valueOf(fmgr.dumpFormula(ie.getValue().getBounds(false))); - String upperBound = String.valueOf(fmgr.dumpFormula(ie.getValue().getBounds(true))); + String lowerBound = dumper.dump(ie.getValue().getBounds(false)); + String upperBound = dumper.dump(ie.getValue().getBounds(true)); InputDTO iDto = new InputDTO( ie.getName(), @@ -98,7 +103,7 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage inputs.add(iDto); } for (BooleanFormula uf : symbolicTrace.getConstraints()) { - String formula = String.valueOf(fmgr.dumpFormula(uf)); + String formula = dumper.dump(uf); ufs.add(new UFDTO(formula)); } logger.trace("Parsing constraints..."); @@ -110,7 +115,7 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage inputNames.add(ie.getName()); } java.util.function.Predicate isInput = - name -> inputNames.contains(name) || name.matches("[A-Z].*_[0-9].*"); + name -> inputNames.contains(name) || INPUT_NAME.matcher(name).matches(); boolean symbolicPrecisionLoss = symbolicTrace.isSymbolicPrecisionLoss(); for (Element el : symbolicTrace.getTrace()) { if (el instanceof BranchElement be) { @@ -121,9 +126,9 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage if(fmgr.getBooleanFormulaManager().isTrue(f) || fmgr.getBooleanFormulaManager().isFalse(f)){ constraint = "(assert true)"; } else { - constraint = String.valueOf(fmgr.dumpFormula(f)); - if (!fmgr.extractVariablesAndUFs(f).isEmpty() && - !fmgr.extractVariablesAndUFs(f).keySet().stream().allMatch(isInput)) { + constraint = dumper.dump(f); + if (!symbolicPrecisionLoss + && !fmgr.extractVariablesAndUFs(f).keySet().stream().allMatch(isInput)) { symbolicPrecisionLoss = true; } } @@ -134,11 +139,12 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage } catch (InterruptedException e) { BooleanFormula f = be.getConstraint(); logger.warn("Error while simplifying formula", e); - constraint = String.valueOf(fmgr.dumpFormula(f)); + constraint = dumper.dump(f); //fmgr.extractVariablesAndUFs(f).keySet().forEach(System.out::println); // assert fmgr.extractVariablesAndUFs(f).keySet().stream() // .allMatch(s -> s.matches("[A-Z].*_[0-9].*")): "[SWAT] UF introduced in: " + constraint; - if (!fmgr.extractVariablesAndUFs(f).keySet().stream().allMatch(isInput)) { + if (!symbolicPrecisionLoss + && !fmgr.extractVariablesAndUFs(f).keySet().stream().allMatch(isInput)) { symbolicPrecisionLoss = true; } } @@ -179,6 +185,10 @@ private static String buildRequestBody(Object payload) throws JsonProcessingExce ObjectMapper objectMapper = new ObjectMapper(); objectMapper.setVisibility(PropertyAccessor.FIELD, JsonAutoDetect.Visibility.ANY); - return objectMapper.writerWithDefaultPrettyPrinter().writeValueAsString(payload); + // Indented only where a person reads it (PRINT); the explorer gets the compact form. + if (Config.instance().getSolverMode() == SolverMode.PRINT) { + return objectMapper.writerWithDefaultPrettyPrinter().writeValueAsString(payload); + } + return objectMapper.writeValueAsString(payload); } } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/FormulaDumper.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/FormulaDumper.java new file mode 100644 index 00000000..51204d84 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/FormulaDumper.java @@ -0,0 +1,103 @@ +package de.uzl.its.swat.symbolic.trace; + +import ch.qos.logback.classic.Logger; +import com.microsoft.z3.Native; +import de.uzl.its.swat.common.logging.GlobalLogger; +import java.lang.reflect.Method; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator; + +/** + * Dumps formulas as SMT-LIB like {@link FormulaManager#dumpFormula}, with the same output, but + * faster for many formulas. For Z3, java-smt creates a new solver for every formula, asserts the + * formula in it and prints the solver, and initialising that solver costs more than printing a + * small formula. This dumper keeps one solver and asserts each formula in its own scope. + * + *

The Z3 handles are only reachable through protected java-smt methods, so they are looked up + * reflectively; if that fails (another java-smt version or solver), every formula goes through + * {@link FormulaManager#dumpFormula} instead. + * + *

The dumper of the last formula manager is kept: there is one per solver context, and one + * context per thread. Its solver lives as long as the context. + */ +final class FormulaDumper { + private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger(); + + private final FormulaManager fmgr; + private final FormulaCreator creator; + private final Method extractInfo; + private final Method sanitize; + private final long context; + private final long solver; + + private FormulaDumper( + FormulaManager fmgr, + FormulaCreator creator, + Method extractInfo, + Method sanitize, + long context, + long solver) { + this.fmgr = fmgr; + this.creator = creator; + this.extractInfo = extractInfo; + this.sanitize = sanitize; + this.context = context; + this.solver = solver; + } + + private static volatile FormulaDumper last; + + /** The dumper for the formulas of the given manager. */ + static FormulaDumper of(FormulaManager fmgr) { + FormulaDumper dumper = last; + if (dumper == null || dumper.fmgr != fmgr) { + dumper = create(fmgr); + last = dumper; + } + return dumper; + } + + /** A dumper for the formulas of the given manager; one that falls back if Z3 is not reachable. */ + private static FormulaDumper create(FormulaManager fmgr) { + try { + if (fmgr instanceof AbstractFormulaManager afm + && afm.getFormulaCreator().getEnv() instanceof Long context + && afm.getClass().getSimpleName().equals("Z3FormulaManager")) { + Method extractInfo = FormulaCreator.class.getDeclaredMethod("extractInfo", Formula.class); + extractInfo.setAccessible(true); + Method sanitize = AbstractFormulaManager.class.getDeclaredMethod("sanitize", String.class); + sanitize.setAccessible(true); + long solver = Native.mkSolver(context); + Native.solverIncRef(context, solver); + return new FormulaDumper(fmgr, afm.getFormulaCreator(), extractInfo, sanitize, context, solver); + } + } catch (ReflectiveOperationException | RuntimeException e) { + logger.debug("Dumping formulas through java-smt: {}", e.toString()); + } + return new FormulaDumper(fmgr, null, null, null, 0, 0); + } + + /** The formula as SMT-LIB: its declarations and one assert, as {@link FormulaManager#dumpFormula}. */ + String dump(BooleanFormula f) { + if (creator == null) { + return String.valueOf(fmgr.dumpFormula(f)); + } + try { + long expr = (Long) extractInfo.invoke(creator, f); + String dumped; + Native.solverPush(context, solver); + try { + Native.solverAssert(context, solver, expr); + dumped = Native.solverToString(context, solver); + } finally { + Native.solverPop(context, solver, 1); + } + return (String) sanitize.invoke(fmgr, dumped); + } catch (ReflectiveOperationException e) { + return String.valueOf(fmgr.dumpFormula(f)); + } + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java index 5a917bb2..26e25c2d 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java @@ -5,6 +5,7 @@ public class BranchDTO { private final long iid; @SuppressWarnings("unused") + @com.fasterxml.jackson.annotation.JsonInclude(com.fasterxml.jackson.annotation.JsonInclude.Include.NON_NULL) private String constraint; @SuppressWarnings("unused") @@ -14,8 +15,10 @@ public class BranchDTO { private final String type; @SuppressWarnings("unused") + @com.fasterxml.jackson.annotation.JsonInclude(com.fasterxml.jackson.annotation.JsonInclude.Include.NON_NULL) private String inst; @SuppressWarnings("unused") + @com.fasterxml.jackson.annotation.JsonInclude(com.fasterxml.jackson.annotation.JsonInclude.Include.NON_DEFAULT) private boolean concreteOnly; // See BranchElement: the branch's key and the frame stack change since the previous branch. @SuppressWarnings("unused") diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java index 38c571d8..f43d764f 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java @@ -31,7 +31,6 @@ import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.ConfigurationBuilder; import org.sosy_lab.common.configuration.InvalidConfigurationException; -import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.SolverContextFactory; import org.sosy_lab.java_smt.api.SolverContext; @@ -116,7 +115,9 @@ public ThreadContext(long id, String endpointName, int endpointID) throws Invali logger.info(SMTConfig.asPropertiesString()); - LogManager logger = BasicLogManager.create(SMTConfig); + // java-smt's own log is not read; a BasicLogManager would also register a JMX bean, which + // loads the JMX classes in every run + LogManager logger = LogManager.createNullLogManager(); ShutdownManager shutdown = ShutdownManager.create(); // SolverContext is a class wrapping a solver context. diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java index b83a3e8d..aeadeb0e 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java @@ -27,7 +27,7 @@ import org.sosy_lab.common.ShutdownManager; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; -import org.sosy_lab.common.log.BasicLogManager; +import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.SolverContextFactory; import org.sosy_lab.java_smt.api.SolverContext; @@ -58,7 +58,7 @@ public static void init() throws InvalidConfigurationException { solverContext = SolverContextFactory.createSolverContext( Configuration.defaultConfiguration(), - BasicLogManager.create(Configuration.defaultConfiguration()), + LogManager.createNullLogManager(), ShutdownManager.create().getNotifier(), SolverContextFactory.Solvers.Z3); } diff --git a/symbolic-explorer/data/Database.py b/symbolic-explorer/data/Database.py index 53bf1882..f0858b64 100755 --- a/symbolic-explorer/data/Database.py +++ b/symbolic-explorer/data/Database.py @@ -158,6 +158,25 @@ def get_tree(self, endpoint_id: Union[str, int]) -> Tree: lock.release() return ret + def visit_tree(self, endpoint_id: Union[str, int], visit): + """Returns visit(tree, solved, unsat) for the endpoint's tree, with the gids of the solved + and of the unsat branches, all under the lock and without copying: a copy of the whole + tree in every round costs more than the walk itself. visit must not keep the sets, and + must not call back into the Database (the lock is held).""" + endpoint_id = str(endpoint_id) + lock.acquire() + try: + return visit(self.tree[endpoint_id], self.solutions.keys(), set(self.unsat_branches)) + finally: + lock.release() + + def count_symbolic_vars(self, endpoint_id: Union[str, int]) -> int: + endpoint_id = str(endpoint_id) + lock.acquire() + ret = len(self.tree[endpoint_id].symbolic_vars) + lock.release() + return ret + def get_witness_data(self, endpoint_id: Union[str, int]) -> dict | None: """The witness data of the latest trace of the endpoint (None if no trace arrived since the last clear).""" endpoint_id = str(endpoint_id) diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index a6c70f11..66aad50d 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -1,3 +1,4 @@ +import copy import glob import signal import subprocess @@ -116,6 +117,9 @@ def build_command(self,javaagent:str, config:str, Z3_DIR: str, port, cp, java_p cmd = [ java_path, f'-Xmx{mem}g', + # A round runs the target once, mostly for well under a second: C2 compilations + # would not pay off before the JVM exits, the C1 ones do. + '-XX:TieredStopAtLevel=1', f'-Dconfig.path={config}', f'-Dexplorer.port={port}', f'-javaagent:{javaagent}', @@ -191,13 +195,13 @@ def determine_next_step(self, status: ExecutionStatus, output: List[str] ) -> Ac return Action.REPORTVERDICT - if len(Database.instance().get_tree(ENDPOINT_ID).symbolic_vars) == 0: + if Database.instance().count_symbolic_vars(ENDPOINT_ID) == 0: # No symbolic vars found, safe to assume no violation logger.info(f'[SVCOMP] No symbolic vars found') self.state.verdict = Verdict.NO_SYMBOLIC_VARS return Action.REPORTVERDICT - logger.info(f'[SVCOMP] Found {len(Database.instance().get_tree(ENDPOINT_ID).symbolic_vars)} symbolic vars') + logger.info(f'[SVCOMP] Found {Database.instance().count_symbolic_vars(ENDPOINT_ID)} symbolic vars') # No assertion error found but symbolic variables present, continue with symbolic exploration return Action.SYMBOLICNEXT @@ -409,8 +413,9 @@ def retrieve_solution(self): return Action.REPORTVERDICT 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 + # remember which branch we want to explore, as it is now: the node itself is the tree's + # and gets its other side once the next trace arrives (check_divergence needs this one) + self.state.branch_to_explore = copy.copy(branch) 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()] diff --git a/symbolic-explorer/solver/ConstraintManager.py b/symbolic-explorer/solver/ConstraintManager.py index ba087d75..592b513f 100644 --- a/symbolic-explorer/solver/ConstraintManager.py +++ b/symbolic-explorer/solver/ConstraintManager.py @@ -202,21 +202,24 @@ def _extract_variables(self, expr: ExprRef) -> Set[str]: Set of variable names """ variables = set() - - def traverse(e): - """Recursively traverse the AST.""" + # Iterative, and each shared subterm once: an expression is a DAG that can be deeper than + # the recursion limit, and exponentially larger as a tree. + seen = set() + work = [expr] + while work: + e = work.pop() + key = e.get_id() + if key in seen: + continue + seen.add(key) if is_const(e) and e.decl().kind() == Z3_OP_UNINTERPRETED: # This is a variable (uninterpreted constant) variables.add(str(e)) elif is_app(e): - # Traverse all arguments - for i in range(e.num_args()): - traverse(e.arg(i)) + work.extend(e.arg(i) for i in range(e.num_args())) elif is_quantifier(e): - # Traverse quantifier body - traverse(e.body()) + work.append(e.body()) - traverse(expr) return variables def _classify_constraint(self, expr: ExprRef) -> str: diff --git a/symbolic-explorer/strategy/DFS.py b/symbolic-explorer/strategy/DFS.py index b8d52078..f6e97f7f 100755 --- a/symbolic-explorer/strategy/DFS.py +++ b/symbolic-explorer/strategy/DFS.py @@ -81,7 +81,8 @@ def dfs(visited: set[Node], tree, node: Node | Leaf | None, solved_branches: set skip_is_interesting = mask_sa_node or (sa_node is None) or is_interesting(sa_node.get_fallthrough_child(), sa_stack) branch_is_interesting = mask_sa_node or (sa_node is None) or is_interesting(sa_node.get_branched_child(), sa_stack) - logger.info(f"[DFS] @{node.id}/{("CALLBACK" if node.callback else "CLINIT") if mask_sa_node else sa_node and sa_node.id} ({"branched" if node.branched else ""}{"skipped" if node.skipped else ""}): skip_is_interesting={skip_is_interesting}, branch_is_interesting={branch_is_interesting}") + if sa_index is not None: # without a graph the line has nothing to say, at every node every round + logger.info(f"[DFS] @{node.id}/{("CALLBACK" if node.callback else "CLINIT") if mask_sa_node else sa_node and sa_node.id} ({"branched" if node.branched else ""}{"skipped" if node.skipped else ""}): skip_is_interesting={skip_is_interesting}, branch_is_interesting={branch_is_interesting}") # Add the node itself, if eligible if (node.skipped is None and skip_is_interesting) or (node.branched is None and branch_is_interesting): diff --git a/symbolic-explorer/strategy/StrategyService.py b/symbolic-explorer/strategy/StrategyService.py index 9afe6927..4c68a65c 100755 --- a/symbolic-explorer/strategy/StrategyService.py +++ b/symbolic-explorer/strategy/StrategyService.py @@ -14,24 +14,24 @@ class StrategyService: + # is_symbolic_branch per (node gid, trace id) + _symbolic_branches: dict[tuple[int, str], bool] = {} @staticmethod def select_branch(**kwargs): endpoint_id = kwargs.get('endpoint_id', None) db = Database.instance() - tree = db.get_tree(endpoint_id) visited = set() # With rank_by_distance, the branches are tried closest-to-an-assert first. Only the order # 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) + # The walk is on the Database's tree itself, so dfs records where the SA walk fell out of + # step there directly. The returned nodes are live: they gain children as traces arrive. + possible_branches = db.visit_tree(endpoint_id, lambda tree, solved, unsat: dfs( + visited, tree, tree.root, solved, unsat, 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. - for error in tree.execution_errors: - if error['kind'] == 'sa_desync': - db.record_execution_error(endpoint_id, error['kind'], error['message']) return possible_branches @@ -138,6 +138,13 @@ def is_symbolic_branch(node: Node) -> bool: """ from solver.ConstraintCache import get_constraint_cache + # The answer depends only on the node's constraint and inputs, which are fixed when the + # node is created; a branch not taken stays a candidate, so it is asked again every round. + key = (node.gid, node.trace_id) + known = StrategyService._symbolic_branches.get(key) + if known is not None: + return known + try: # Get cached parsed constraint (parse once, reuse many times). # On a cache miss this parses SMT-LIB via Z3 and walks the AST, which is @@ -174,6 +181,7 @@ def is_symbolic_branch(node: Node) -> bool: logger.info(f"[is_symbolic_branch] Branch {node.id} is_symbolic: {is_symbolic}") + StrategyService._symbolic_branches[key] = is_symbolic return is_symbolic except Exception as e: diff --git a/symbolic-explorer/tests/test_round_overhead.py b/symbolic-explorer/tests/test_round_overhead.py new file mode 100644 index 00000000..685f1bf5 --- /dev/null +++ b/symbolic-explorer/tests/test_round_overhead.py @@ -0,0 +1,121 @@ +""" +Unit tests for the per-round bookkeeping of the explorer: branch selection walks the Database's +tree without copying it, and the answers it reuses across rounds are the ones a fresh walk gives. + +Run with the harness venv, from symbolic-explorer/: + ../targets/sv-comp/scripts/.venv/bin/python3 -m unittest tests.test_round_overhead -v +""" + +import copy +import os +import sys +import unittest +from types import SimpleNamespace +from unittest import mock + +sys.path.insert(0, os.path.join(os.path.dirname(__file__), '..')) + +from data.Database import Database +from data.trace.Branch import Branch +from data.trace.Input import Input +from driver import SVCompDriver as svcomp +from strategy.StrategyService import StrategyService + +DECL = '(declare-fun I_0 () (_ BitVec 32))\n' + + +def branch(id, trace_id, taken, constraint='(assert (bvsgt I_0 #x00000000))'): + return Branch(id, trace_id, taken, DECL + constraint) + + +class SelectBranchTest(unittest.TestCase): + + def setUp(self): + Database.instance().reset() + self.inputs = [Input('I_0', '0', 'int', DECL + '(assert true)', DECL + '(assert true)')] + + def add(self, trace_id, trace): + Database.instance().add_trace(0, trace_id, trace, self.inputs, [], False, False) + + def test_candidates_are_the_open_sides_in_dfs_order(self): + self.add('t1', [branch(1, 't1', True), branch(2, 't1', False), branch(3, 't1', True)]) + self.add('t2', [branch(1, 't2', True), branch(2, 't2', True)]) + nodes = StrategyService.select_branch(endpoint_id=0) + self.assertEqual([n.id for n in nodes], [1, 3]) # 2 has both sides now + + def test_solved_and_unsat_branches_are_left_out(self): + self.add('t1', [branch(1, 't1', True), branch(2, 't1', False)]) + first, second = StrategyService.select_branch(endpoint_id=0) + Database.instance().add_unsat_branch(first.gid) + Database.instance().add_solution(second.gid, {}, self.inputs, 0) + self.assertEqual(StrategyService.select_branch(endpoint_id=0), []) + + def test_the_tree_is_not_copied(self): + self.add('t1', [branch(1, 't1', True)]) + with mock.patch.object(copy, 'deepcopy', side_effect=AssertionError('copied')): + nodes = StrategyService.select_branch(endpoint_id=0) + self.assertEqual([n.id for n in nodes], [1]) + + def test_symbolic_check_is_remembered_per_node(self): + self.add('t1', [branch(1, 't1', True), branch(2, 't1', False, '(assert (= #x00000001 #x00000001))')]) + nodes = StrategyService.select_branch(endpoint_id=0) + first = [StrategyService.is_symbolic_branch(n) for n in nodes] + self.assertEqual(first, [True, False]) + with mock.patch('solver.ConstraintCache.get_constraint_cache', side_effect=AssertionError('asked again')): + self.assertEqual([StrategyService.is_symbolic_branch(n) for n in nodes], first) + + +class BranchToExploreTest(unittest.TestCase): + """The driver keeps the target as it was when it was solved: the tree's node gets its other + side as soon as the next trace arrives, and check_divergence must not take that as taken.""" + + def test_target_keeps_its_open_side(self): + Database.instance().reset() + inputs = [Input('I_0', '0', 'int', DECL + '(assert true)', DECL + '(assert true)')] + Database.instance().add_trace(0, 't1', [branch(1, 't1', False)], inputs, [], False, False) + node, = StrategyService.select_branch(endpoint_id=0) + driver = svcomp.SVCompDriver.__new__(svcomp.SVCompDriver) + driver.state = svcomp.State() + driver.symbolicStorage = svcomp.SymbolicStorage() + with mock.patch.object(StrategyService, 'select_branch', return_value=[node]), \ + mock.patch.object(svcomp.SVCompDriver, 'solve_candidates', return_value=(node, {}, False)): + driver.sa_graph = SimpleNamespace(entry_node=None) + driver.sa = SimpleNamespace(take_graph=lambda: None) + driver.args = SimpleNamespace(sa_rank_distance=False) + driver.retrieve_solution() + # The next run takes the branched side, as solved for. + Database.instance().add_trace(0, 't2', [branch(1, 't2', True)], inputs, [], False, False) + self.assertIsNotNone(node.branched) + with self.assertNoLogs(svcomp.logger, level='ERROR'): + driver.check_divergence(Database.instance().get_trace(-1)) + + +class ExtractVariablesTest(unittest.TestCase): + """A formula is a DAG: with shared subterms it is exponentially larger as a tree, and it can + be deeper than the recursion limit.""" + + def test_shared_subterms_are_visited_once(self): + from z3 import BitVec, Context + from solver.ConstraintManager import ConstraintManager + ctx = Context() + x, y = BitVec('x', 64, ctx), BitVec('y', 64, ctx) + e = x + for _ in range(200): # 2^200 paths through the DAG + e = e + e + mgr = ConstraintManager(shared_context=ctx) + self.assertEqual(mgr._extract_variables(e == y), {'x', 'y'}) + + def test_deep_terms(self): + from z3 import BitVec, Context + from solver.ConstraintManager import ConstraintManager + ctx = Context() + x = BitVec('x', 32, ctx) + e = x + for i in range(5000): + e = e - (i % 7) + mgr = ConstraintManager(shared_context=ctx) + self.assertEqual(mgr._extract_variables(e == 0), {'x'}) + + +if __name__ == '__main__': + unittest.main()