Cut per-round overhead of the executor and explorer

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());

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<String> 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);
     }
 }

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.
+ *
+ * <p>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.
+ *
+ * <p>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));
+        }
+    }
+}

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")

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.

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);
     }

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)

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()]

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:

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):