From f809a0b7ab323bc0a31331ec80e433ea94ce8214 Mon Sep 17 00:00:00 2001
From: "maul.esel" <maul.esel@posteo.de>
Date: Thu, 19 Dec 2024 16:31:58 +0100
Subject: [PATCH] add support for task-defined options to ULTIMATE tool info
 module

For internal evaluations, we use task definition files that specify
ULTIMATE parameters pertaining to one particular program, e.g. custom
specifications (e.g preconditions) or assumptions about the program.

Specifying these in the task definition is useful, as the expected verdict
may differ depending on these parameters, and we can easily have multiple
task definition files with different parameters and verdicts for a program.

If an option is already present, we do not insert it again (or ULTIMATE
would fail). Thus, options specified in the benchexec XML take precedence,
which allows the same task definition files to be evaluated with multiple
run definitions.
---
 benchexec/tools/ultimate.py | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

diff --git a/benchexec/tools/ultimate.py b/benchexec/tools/ultimate.py
index e1a902f2f..c5c335c40 100644
--- a/benchexec/tools/ultimate.py
+++ b/benchexec/tools/ultimate.py
@@ -306,6 +306,7 @@ def _cmdline_no_wrapper(self, executable, options, task, resource_limits):
             TaskFilesConsidered.INPUT_FILES,
         )
 
+        cmdline += self._get_task_cmd_options(task, options)
         cmdline += witness_options
         cmdline += options
 
@@ -325,6 +326,7 @@ def _cmdline_default(self, executable, options, task):
             TaskFilesConsidered.INPUT_FILES,
         )
 
+        cmdline += self._get_task_cmd_options(task, options)
         cmdline += witness_options
         if task.input_files_or_empty:
             cmdline += ["--file", *input_files]
@@ -334,9 +336,10 @@ def _cmdline_default(self, executable, options, task):
 
     def _cmdline_svcomp17(self, executable, options, task):
         cmdline = [executable, task.property_file]
-        cmdline += [
+        filtered_options [
             option for option in options if option not in _SVCOMP17_FORBIDDEN_FLAGS
         ]
+        cmdline += filtered_options
         cmdline.append("--full-output")
 
         input_files, witness_options = handle_witness_of_task(
@@ -346,11 +349,28 @@ def _cmdline_svcomp17(self, executable, options, task):
             TaskFilesConsidered.INPUT_FILES,
         )
 
+        cmdline += self._get_task_cmd_options(task, filtered_options)
         cmdline += witness_options
         cmdline += input_files
         self.__assert_cmdline(cmdline, "SVCOMP17")
         return cmdline
 
+    def _get_task_cmd_options(task, existing_options):
+        if not task.options:
+            return []
+        task_options = []
+        for plugin, settings in task.options.items():
+            if plugin.startswith("de.uni_freiburg.informatik.ultimate."):
+                prefix = key.split(".")[-1]
+                for setting, value in settings.items():
+                    # The same conversion from human-readable setting names to parameters is performed by Ultimate.
+                    name = "--" + (prefix + " " + setting).replace(":", "").sub(r"[ ()\"'.]+", ".").lower().strip(".")
+
+                    # Avoid duplicating options (values in benchexec XML take precedence).
+                    if name not in existing_options:
+                        task_options += [name, value]
+        return task_options
+
     @staticmethod
     def __assert_cmdline(cmdline, mode):
         assert all(