Report UNKNOWN when the target never reaches main

symbolic-explorer/data/Database.py

@@ -145,6 +145,13 @@ def get_traces(self):
         lock.release()
         return ret
 
+    def trace_count(self) -> int:
+        """The number of traces received so far, over all endpoints."""
+        lock.acquire()
+        ret = len(self.traces)
+        lock.release()
+        return ret
+
     def get_trace(self, idx: int):
         lock.acquire()
         ret = copy.deepcopy(self.traces[idx])

symbolic-explorer/driver/SVCompDriver.py

@@ -161,8 +161,14 @@ def run_command_with_timeout(self, cmd: List[str]) -> Tuple[ExecutionStatus, Lis
                 return ExecutionStatus.ERROR, output + [str(e)]
 
 
-    def determine_next_step(self, status: ExecutionStatus, output: List[str] ) -> Action:
-        """Determines the next step based on the execution status."""
+    def determine_next_step(self, status: ExecutionStatus, output: List[str], received_trace: bool = True) -> Action:
+        """Determines the next step based on the execution status.
+
+        received_trace says whether the run sent a trace. The executor sends one whenever the entry
+        method was entered (also when it ends in an exception or System.exit), so a run without one
+        never reached it, e.g. because the JVM failed to start (VerifyError, missing main class) or
+        the agent failed: such a run proves nothing.
+        """
         if status == ExecutionStatus.SUCCESS:
 
 
@@ -190,6 +196,11 @@ def determine_next_step(self, status: ExecutionStatus, output: List[str] ) -> Ac
                     self.state.verdict = Verdict.UNKNOWN
                     return Action.REPORTVERDICT
 
+            if not received_trace:
+                logger.warning(f'[SVCOMP] The target sent no trace: it did not reach the entry method')
+                Database.instance().record_execution_error(ENDPOINT_ID, 'no_trace', 'the target sent no trace')
+                self.state.verdict = Verdict.UNKNOWN
+                return Action.REPORTVERDICT
 
             if len(Database.instance().get_tree(ENDPOINT_ID).symbolic_vars) == 0:
                 # No symbolic vars found, safe to assume no violation
@@ -246,20 +257,23 @@ def run_testcase(self, java_path, agentpath: str, configpath: str, z3path, port,
             # Run the target with DSE - Time the symbolic executor
             status: ExecutionStatus
             output: List[str]
+            traces_before = Database.instance().trace_count()
             executor_start = time.perf_counter()
             status, output = self.run_command_with_timeout(cmd=command)
             executor_duration = time.perf_counter() - executor_start
             TimingManager.instance().record_executor_time(executor_duration)
 
+            received_trace = Database.instance().trace_count() > traces_before
+
             # check if the target explored the branch as expected
-            if self.state.branch_to_explore:
+            if self.state.branch_to_explore and received_trace:
                 self.check_divergence(Database.instance().get_trace(-1)) # most recent trace
             self.state.branch_to_explore = None
             self.state.solution_is_guess = False
 
             self.log_output(output)
             logger.info(f'[STATUS] {status}')
-            next_step: Action = self.determine_next_step(status, output)
+            next_step: Action = self.determine_next_step(status, output, received_trace)
 
             # Visualize DB tree
             # print("Plotting DB Tree...", flush=True)

symbolic-explorer/tests/test_failed_start_e2e.py

@@ -0,0 +1,145 @@
+"""
+End-to-end reproducer: an SV-COMP run whose target JVM fails before main (a VerifyError from
+inconsistently compiled classes, or a missing main class) is UNKNOWN, while a non-symbolic program
+that runs to completion stays SAFE. Both through the explorer and through the competition package
+wrapper (scripts/svcomp-package/run_swat.py), which compiles the task first.
+
+It runs SymbolicExplorer.py with the executor jar (build it with `../gradlew copyJar` in
+symbolic-executor/) and the Z3 libraries in libs/java-library-path, and is skipped if either or
+javac is missing. Run it with the harness venv, from symbolic-explorer/:
+    ../targets/sv-comp/scripts/.venv/bin/python3 -m unittest tests.test_failed_start_e2e -v
+"""
+
+import json
+import os
+import re
+import shutil
+import socket
+import subprocess
+import sys
+import tempfile
+import unittest
+from pathlib import Path
+
+EXPLORER = Path(__file__).resolve().parent.parent
+ROOT = EXPLORER.parent
+AGENT = ROOT / 'symbolic-executor/lib/symbolic-executor.jar'
+Z3_DIR = ROOT / 'libs/java-library-path'
+Z3_JAR = Z3_DIR / 'com.microsoft.z3.jar'
+CONFIG = ROOT / 'targets/sv-comp/sv-comp.cfg'
+PACKAGE = ROOT / 'scripts/svcomp-package'
+
+
+def free_port():
+    with socket.socket() as s:
+        s.bind(('localhost', 0))
+        return s.getsockname()[1]
+
+
+def write(path: Path, text: str):
+    path.parent.mkdir(parents=True, exist_ok=True)
+    path.write_text(text)
+
+
+@unittest.skipUnless(AGENT.exists() and Z3_JAR.exists() and shutil.which('javac') and shutil.which('java'),
+                     'needs the executor jar, the Z3 libraries, java and javac')
+class FailedStartTest(unittest.TestCase):
+
+    def setUp(self):
+        self.tmp = Path(tempfile.mkdtemp())
+        self.addCleanup(shutil.rmtree, self.tmp, ignore_errors=True)
+
+    def javac(self, out: Path, *sources: Path):
+        subprocess.run(['javac', '-d', str(out)] + [str(s) for s in sources], check=True)
+
+    def verdict(self, target_dir: Path) -> dict:
+        logdir = self.tmp / 'run'
+        logdir.mkdir()
+        cmd = [sys.executable, '-u', str(EXPLORER / 'SymbolicExplorer.py'), '-prp', 'valid-assert.prp',
+               '--agent', str(AGENT), '--config', str(CONFIG), '-z3', str(Z3_DIR), '--logdir', str(logdir),
+               '--mode', 'sv-comp', '--port', str(free_port()), '--target', 'Main',
+               '--classpath', str(target_dir), str(Z3_JAR)]
+        # The explorer ends itself with SIGTERM once the verdict is written
+        subprocess.run(cmd, cwd=logdir, stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL, timeout=120)
+        return json.loads((logdir / 'stats.json').read_text())
+
+    def test_verify_error_is_unknown(self):
+        # B extends A when Main is compiled, but not at run time: verifying Main fails before main
+        src = self.tmp / 'src'
+        write(src / 'A.java', 'public class A { public int f() { return 1; } }')
+        write(src / 'B.java', 'public class B extends A { }')
+        write(src / 'Main.java', 'public class Main { public static void main(String[] args) { A a = new B(); assert a.f() == 1; } }')
+        write(src / 'v2/B.java', 'public class B { }')
+        out = self.tmp / 'classes'
+        self.javac(out, src / 'A.java', src / 'B.java', src / 'Main.java')
+        self.javac(out, src / 'v2/B.java')
+        stats = self.verdict(out)
+        self.assertEqual(stats['verdict'], 'UNKNOWN')
+        self.assertIn('no_trace', [e['kind'] for e in stats['execution_errors']])
+
+    def test_missing_main_class_is_unknown(self):
+        empty = self.tmp / 'empty'
+        empty.mkdir()
+        stats = self.verdict(empty)
+        self.assertEqual(stats['verdict'], 'UNKNOWN')
+
+    def test_non_symbolic_program_is_safe(self):
+        src = self.tmp / 'src'
+        write(src / 'Main.java', 'public class Main { public static void main(String[] args) { int x = 3; assert x == 3; } }')
+        out = self.tmp / 'classes'
+        self.javac(out, src / 'Main.java')
+        stats = self.verdict(out)
+        self.assertEqual(stats['verdict'], 'SAFE')
+        self.assertEqual(stats['execution_errors'], [])
+
+
+@unittest.skipUnless(AGENT.exists() and Z3_JAR.exists() and shutil.which('javac') and shutil.which('java'),
+                     'needs the executor jar, the Z3 libraries, java and javac')
+class PackageFailedStartTest(unittest.TestCase):
+    """The same through run_swat.py, in the layout of scripts/package-svcomp.sh."""
+
+    def setUp(self):
+        self.tmp = Path(tempfile.mkdtemp())
+        self.addCleanup(shutil.rmtree, self.tmp, ignore_errors=True)
+        pkg = self.tmp / 'pkg'
+        (pkg / 'symbolic-executor/lib').mkdir(parents=True)
+        (pkg / 'libs').mkdir()
+        shutil.copy(PACKAGE / 'compile-target.sh', pkg)
+        shutil.copy(CONFIG, pkg)
+        # The wrapper's fixed explorer port, replaced so that parallel runs do not collide
+        wrapper = (PACKAGE / 'run_swat.py').read_text()
+        self.assertIn("'--port', \"8000\"", wrapper)
+        (pkg / 'run_swat.py').write_text(wrapper.replace("'--port', \"8000\"", f"'--port', \"{free_port()}\""))
+        (pkg / 'symbolic-executor/lib/symbolic-executor.jar').symlink_to(AGENT)
+        (pkg / 'symbolic-explorer').symlink_to(EXPLORER)
+        (pkg / 'libs/java-library-path').symlink_to(Z3_DIR)
+        self.pkg = pkg
+
+    def verdict(self, main_java: str | None) -> str:
+        task = self.tmp / 'task'
+        task.mkdir()
+        if main_java is not None:
+            write(task / 'Main.java', main_java)
+        else:
+            write(task / 'Other.java', 'public class Other { public static void main(String[] args) { assert false; } }')
+        prp = self.tmp / 'valid-assert.prp'
+        prp.write_text('CHECK( init(main()), LTL(G assert) )\n')
+        out = subprocess.run([sys.executable, '-u', str(self.pkg / 'run_swat.py'), str(prp), str(task)],
+                             cwd=self.pkg, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, text=True, timeout=180).stdout
+        verdicts = [l for l in out.splitlines() if '[VERDICT valid-assert.prp]' in l]
+        self.assertTrue(verdicts, out[-2000:])
+        return re.search(r'== [A-Z-]+', verdicts[-1]).group(0)
+
+    def test_missing_main_class_is_unknown(self):
+        # Compiles, but there is no class Main: ClassNotFoundException before main
+        self.assertEqual(self.verdict(None), '== DONT-KNOW')
+
+    def test_task_that_does_not_compile_is_unknown(self):
+        self.assertEqual(self.verdict('public class Main { public static void main(String[] args) { int x = ; } }'), '== DONT-KNOW')
+
+    def test_non_symbolic_program_is_safe(self):
+        self.assertEqual(self.verdict('public class Main { public static void main(String[] args) { int x = 3; assert x == 3; } }'), '== OK')
+
+
+if __name__ == '__main__':
+    unittest.main()

symbolic-explorer/tests/test_no_trace.py

@@ -0,0 +1,117 @@
+"""
+Unit tests for SVCompDriver.determine_next_step on runs that sent no trace: the target never reached
+its entry method (e.g. a VerifyError or a missing main class), so the run must not count as a
+non-symbolic program that ran to completion.
+
+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/:
+    ../targets/sv-comp/scripts/.venv/bin/python3 -m unittest tests.test_no_trace -v
+"""
+
+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 driver import SVCompDriver as svcomp
+
+VERIFY_ERROR_OUTPUT = [
+    'Error: Unable to initialize main class Main',
+    'Caused by: java.lang.VerifyError: Bad type on operand stack',
+]
+
+
+class NoTraceTest(unittest.TestCase):
+
+    def setUp(self):
+        self.tree = SimpleNamespace(symbolic_vars=set(), execution_errors=[], uncaught_exceptions=0)
+        def record_execution_error(endpoint_id, kind, message):
+            self.tree.execution_errors.append({'kind': kind, 'message': message})
+        def record_uncaught_exception(endpoint_id):
+            self.tree.uncaught_exceptions += 1
+        db = SimpleNamespace(record_execution_error=record_execution_error,
+                             record_uncaught_exception=record_uncaught_exception,
+                             get_tree=lambda endpoint_id: self.tree)
+        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.state = svcomp.State()
+        self.driver.verification_category = svcomp.VerificationCategory.VALID_ASSERT_PRP
+
+    def step(self, output, received_trace):
+        return self.driver.determine_next_step(svcomp.ExecutionStatus.SUCCESS, output, received_trace)
+
+    def test_failed_start_is_unknown(self):
+        self.assertEqual(self.step(VERIFY_ERROR_OUTPUT, received_trace=False), svcomp.Action.REPORTVERDICT)
+        self.assertEqual(self.driver.state.verdict, svcomp.Verdict.UNKNOWN)
+        self.assertEqual([e['kind'] for e in self.tree.execution_errors], ['no_trace'])
+
+    def test_missing_trace_with_symbolic_vars_from_earlier_rounds_is_unknown(self):
+        self.tree.symbolic_vars = {'int_0'}
+        self.assertEqual(self.step([], received_trace=False), svcomp.Action.REPORTVERDICT)
+        self.assertEqual(self.driver.state.verdict, svcomp.Verdict.UNKNOWN)
+
+    def test_non_symbolic_program_that_ran_is_non_symbolic(self):
+        self.assertEqual(self.step([], received_trace=True), svcomp.Action.REPORTVERDICT)
+        self.assertEqual(self.driver.state.verdict, svcomp.Verdict.NO_SYMBOLIC_VARS)
+        self.assertEqual(self.tree.execution_errors, [])
+
+    def test_symbolic_program_that_ran_continues(self):
+        self.tree.symbolic_vars = {'int_0'}
+        self.assertEqual(self.step([], received_trace=True), svcomp.Action.SYMBOLICNEXT)
+
+    def test_assertion_error_in_output_is_still_a_violation(self):
+        # E.g. an assert in the static initializer of the main class: program code that failed
+        # before main, a genuine violation.
+        output = ['Exception in thread "main" java.lang.ExceptionInInitializerError',
+                  'Caused by: java.lang.AssertionError']
+        self.assertEqual(self.step(output, received_trace=False), svcomp.Action.REPORTVERDICT)
+        self.assertEqual(self.driver.state.verdict, svcomp.Verdict.VIOLATION)
+
+
+class ReceivedTraceTest(unittest.TestCase):
+    """run_testcase decides received_trace from the trace count around the target run."""
+
+    def run_round(self, traces_sent, branch_to_explore=None):
+        traces = {'n': 0}
+        tree = SimpleNamespace(symbolic_vars=set(), execution_errors=[])
+        def record_execution_error(endpoint_id, kind, message):
+            tree.execution_errors.append({'kind': kind, 'message': message})
+        db = SimpleNamespace(trace_count=lambda: traces['n'], clear_witness_data=lambda endpoint_id: None,
+                             record_execution_error=record_execution_error, get_tree=lambda endpoint_id: tree,
+                             get_trace=lambda idx: [])
+        driver = svcomp.SVCompDriver.__new__(svcomp.SVCompDriver)
+        driver.state = svcomp.State()
+        driver.state.branch_to_explore = branch_to_explore
+        driver.verification_category = svcomp.VerificationCategory.VALID_ASSERT_PRP
+        driver.args = SimpleNamespace(parallel_sa=True)
+        driver.sa = SimpleNamespace(start=lambda: None)
+        driver.build_command = lambda **kwargs: []
+        def run_command(cmd):
+            traces['n'] += traces_sent
+            return svcomp.ExecutionStatus.SUCCESS, []
+        driver.run_command_with_timeout = run_command
+        driver.check_divergence = mock.Mock()
+        with mock.patch.object(svcomp.Database, 'instance', return_value=db), \
+                mock.patch.object(svcomp.TimingManager, 'instance'):
+            verdict = driver.run_testcase(None, None, None, None, None, None)
+        return verdict, tree, driver
+
+    def test_round_with_trace(self):
+        verdict, tree, _ = self.run_round(traces_sent=1)
+        self.assertEqual(verdict, svcomp.Verdict.NO_SYMBOLIC_VARS)
+
+    def test_round_without_trace(self):
+        verdict, tree, driver = self.run_round(traces_sent=0, branch_to_explore=SimpleNamespace(id=1))
+        self.assertEqual(verdict, svcomp.Verdict.UNKNOWN)
+        self.assertEqual([e['kind'] for e in tree.execution_errors], ['no_trace'])
+        # The latest trace is one of an earlier round: no divergence check against it
+        driver.check_divergence.assert_not_called()
+
+
+if __name__ == '__main__':
+    unittest.main()