Handle validation tasks inside CPAchecker

benchexec/tools/cpa-witness2test.py

@@ -7,7 +7,7 @@
 
 import benchexec.tools.cpachecker as cpachecker
 
-from benchexec.tools.template import ToolNotFoundException
+from benchexec.tools.template import ToolNotFoundException, UnsupportedFeatureException
 
 
 class Tool(cpachecker.Tool):
@@ -51,4 +51,10 @@ def program_files(self, executable):
     def cmdline(self, executable, options, task, rlimits):
         additional_options = self._get_additional_options(options, task, rlimits)
         # Add additional options in front of existing ones, since -gcc-args ... must be last argument in front of task
-        return [executable] + additional_options + options + [task.single_input_file]
+        input_files = self._get_non_witness_input_files(task)
+        if len(input_files) != 1:
+            raise UnsupportedFeatureException(
+                f"{self.name()} does not support tasks with more than one non-witness input file"
+            )
+
+        return [executable] + additional_options + options + input_files

benchexec/tools/cpachecker.py

@@ -6,6 +6,7 @@
 # SPDX-License-Identifier: Apache-2.0
 
 import logging
+from pathlib import Path
 import sys
 import os
 import re
@@ -180,16 +181,47 @@ def option_present(option):
                         f"Unsupported data_model '{data_model}' defined for task '{task}'"
                     )
 
+        if isinstance(task.options, dict) and "witness" in task.options.keys():
+            if not option_present("witness"):
+                possible_witness_files = self._get_witness_input_files(task)
+
+                if len(possible_witness_files) != 1:
+                    raise benchexec.tools.template.UnsupportedFeatureException(
+                        f"Expected exactly one witness file, but found {len(possible_witness_files)}: {possible_witness_files}"
+                    )
+
+                options += [f"{prefix}witness", possible_witness_files[0]]
+            else:
+                raise benchexec.tools.template.UnsupportedFeatureException(
+                    "You are passing a witness as both an option and through the task definition. "
+                    "Please remove one of them."
+                )
+
         return options
 
+    def __partition_input_files(self, task):
+        input_files = task.input_files_or_identifier
+        witness_files = []
+        other_files = []
+        for file in input_files:
+            if Path(file).name == task.options.get("witness"):
+                witness_files.append(file)
+            else:
+                other_files.append(file)
+        return witness_files, other_files
+
+    def _get_witness_input_files(self, task):
+        witness_files, _ = self.__partition_input_files(task)
+        return witness_files
+
+    def _get_non_witness_input_files(self, task):
+        _, other_files = self.__partition_input_files(task)
+        return other_files
+
     def cmdline(self, executable, options, task, rlimits):
         additional_options = self._get_additional_options(options, task, rlimits)
-        return (
-            [executable]
-            + options
-            + additional_options
-            + list(task.input_files_or_identifier)
-        )
+        input_files = self._get_non_witness_input_files(task)
+        return [executable] + options + additional_options + input_files
 
     def determine_result(self, run):
         """