Handle wrong verdicts for known SV-COMP targets

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}')
+        print(f'Verdict:\n {verdict}')

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

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

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)}")
+        logger.info(f"\nCommand {i}:\n{pformat(dict(command), width=100)}")