diff --git a/symbolic-explorer/data/Database.py b/symbolic-explorer/data/Database.py index 53bf1882..767c3441 100755 --- a/symbolic-explorer/data/Database.py +++ b/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]) diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index a6c70f11..a033919a 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/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) diff --git a/symbolic-explorer/tests/test_failed_start_e2e.py b/symbolic-explorer/tests/test_failed_start_e2e.py new file mode 100644 index 00000000..9675e92f --- /dev/null +++ b/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() diff --git a/symbolic-explorer/tests/test_no_trace.py b/symbolic-explorer/tests/test_no_trace.py new file mode 100644 index 00000000..1af5ab4b --- /dev/null +++ b/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()