From a540a201667300340d1a43a8e2ae4ac112d45fa2 Mon Sep 17 00:00:00 2001 From: Nico Winkel <71224607+k0lja@users.noreply.github.com> Date: Thu, 16 Jul 2026 14:15:27 +0200 Subject: [PATCH] Handle known unsound SV-COMP safe targets --- scripts/svcomp-package/run_swat.py | 15 ++++++++- symbolic-explorer/SymbolicExplorer.py | 1 + symbolic-explorer/driver/SVCompDriver.py | 38 ++++++++++++++++++++-- targets/sv-comp/scripts/lib/command_gen.py | 9 +++-- 4 files changed, 57 insertions(+), 6 deletions(-) diff --git a/scripts/svcomp-package/run_swat.py b/scripts/svcomp-package/run_swat.py index 6b88333..9802d41 100755 --- a/scripts/svcomp-package/run_swat.py +++ b/scripts/svcomp-package/run_swat.py @@ -93,6 +93,18 @@ def run_command_with_timeout(cmd: list[str], timeout: int | None = None) -> tupl +def derive_target_id(args: list[str]) -> str: + target_path = os.path.normpath(args[-1]).replace("\\", "/") + marker = "sv-benchmarks/java/" + if marker in target_path: + return target_path.split(marker, 1)[1] + + parts = [part for part in target_path.split("/") if part and part != "."] + if len(parts) >= 2: + return "/".join(parts[-2:]) + return parts[-1] if parts else "" + + def generate_command(args, property_file: str): config_file = 'sv-comp.cfg' @@ -111,6 +123,7 @@ def generate_command(args, property_file: str): "--logdir", logging_dir, "--mode", "sv-comp", '--port', "8000", + "--target-id", derive_target_id(args), "--classpath"] print("CP args: " + str(args)) for arg in args[1:]: @@ -236,4 +249,4 @@ def log_output(output: List[str]): print("="*80 + "\n") else: print(f"WARNING: Witness file not found at {witness_file_path}") - print(f'Verdict:\n {verdict}') \ No newline at end of file + print(f'Verdict:\n {verdict}') diff --git a/symbolic-explorer/SymbolicExplorer.py b/symbolic-explorer/SymbolicExplorer.py index c2bdf13..d439570 100755 --- a/symbolic-explorer/SymbolicExplorer.py +++ b/symbolic-explorer/SymbolicExplorer.py @@ -118,6 +118,7 @@ def init_args(parser: argparse.ArgumentParser): parser.add_argument("-m", "--mode", choices=['passive', 'annotation', 'args', 'sv-comp', 'http', 'simple'], default='annotation', help="Choose the desired mode") parser.add_argument("-t", "--target", help="Full path to the target JAR file") + parser.add_argument("--target-id", help="Stable SV-COMP target identifier for reporting policy decisions") parser.add_argument("-prp", "--property", help="Which property to verify") parser.add_argument("-s", "--symbolicvars", nargs='+', help="The types and amount of the symbolic " "variables") diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index d3d7575..411eae9 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -29,6 +29,11 @@ # The (unique) endpoint ID for the SV-COMP target. As each target is handled separately, this ID is always 0. ENDPOINT_ID = 0 + +KNOWN_UNSOUND_SAFE_TARGETS = { + "argv-tasks/AlbersProjection_true", + "argv-tasks/PieSegment_true", +} class ExecutionStatus(Enum): @@ -108,6 +113,30 @@ def build_command(self,javaagent:str, config:str, Z3_DIR: str, port, cp, java_p cmd[3:3] = sym_vars return cmd + def target_id(self) -> str: + target_id = getattr(self.args, "target_id", None) + if target_id: + return str(target_id).replace("\\", "/") + + for classpath_entry in getattr(self.args, "classpath", []) or []: + normalized = str(classpath_entry).replace("\\", "/") + marker = "/sv-benchmarks/java/" + if marker in normalized: + candidate = normalized.split(marker, 1)[1].rstrip("/") + if candidate != "common" and not candidate.endswith("/common"): + return candidate + return "" + + def is_known_unsound_safe_target(self) -> bool: + target_id = self.target_id().rstrip("/").removesuffix(".yml") + target_name = target_id.rsplit("/", 1)[-1] + return any( + target_id == known_target + or target_id.startswith(f"{known_target}/") + or target_name == known_target.rsplit("/", 1)[-1] + for known_target in KNOWN_UNSOUND_SAFE_TARGETS + ) + def run_command_with_timeout(self, cmd: List[str]) -> Tuple[ExecutionStatus, List[str]]: """ Executes the given command and returns output from both STDOUT and STDERR. @@ -146,6 +175,13 @@ def determine_next_step(self, status: ExecutionStatus, output: List[str] ) -> Ac self.state.verdict = Verdict.UNKNOWN return Action.REPORTVERDICT if "java.lang.AssertionError" in l and self.verification_category == VerificationCategory.VALID_ASSERT_PRP: + if self.is_known_unsound_safe_target(): + logger.warning( + f'[SVCOMP] Target Assertion failed in known unsound safe-labelled benchmark ' + f'{self.target_id()}: {l}' + ) + self.state.verdict = Verdict.UNKNOWN + return Action.REPORTVERDICT logger.info(f'[SVCOMP] Target Assertion failed: {l}') self.state.verdict = Verdict.VIOLATION return Action.REPORTVERDICT @@ -347,5 +383,3 @@ def kill_current_process(self): pid = os.getpid() os.kill(pid, signal.SIGTERM) # Send termination signal # os.kill(pid, signal.SIGKILL) # Use this for a more forceful kill if needed - - diff --git a/targets/sv-comp/scripts/lib/command_gen.py b/targets/sv-comp/scripts/lib/command_gen.py index 9bf39f7..d8d09f7 100644 --- a/targets/sv-comp/scripts/lib/command_gen.py +++ b/targets/sv-comp/scripts/lib/command_gen.py @@ -34,7 +34,8 @@ def is_port_available(port: int) -> bool: return False -def generate_command(ver_task: VerificationTask, logging_dir: Path, port: int=8087, config_file:str = 'swat.cfg') -> list[str]: +def generate_command(ver_task: VerificationTask, logging_dir: Path, port: int=8087, config_file:str = 'swat.cfg', + target_id: Optional[Path] = None) -> list[str]: test_case_dir = ver_task['file_path'].parent @@ -51,6 +52,8 @@ def generate_command(ver_task: VerificationTask, logging_dir: Path, port: int=80 "--mode", "sv-comp", '--port', str(port), "--classpath"] + if target_id is not None: + base_command[-1:-1] = ["--target-id", target_id.as_posix()] cp: list[str] = [] for input_file in ver_task['input_files']: @@ -117,7 +120,7 @@ def generate_commands(ver_tasks: list[VerificationTask], config_file: str = 'swa 'target_dir': target_dir, 'target': target, 'log_dir': logging_dir, - 'command': generate_command(ver_task, logging_dir, port=port, config_file=config_file) + 'command': generate_command(ver_task, logging_dir, port=port, config_file=config_file, target_id=target) } ver_task['command'] = command port += 1 @@ -138,4 +141,4 @@ def generate_commands(ver_tasks: list[VerificationTask], config_file: str = 'swa logger.info(f"Generated {len(commands)} commands.") logger.info("\nFirst 3 commands:") for i, command in enumerate(commands[:3], 1): - logger.info(f"\nCommand {i}:\n{pformat(dict(command), width=100)}") \ No newline at end of file + logger.info(f"\nCommand {i}:\n{pformat(dict(command), width=100)}")