Skip to content

Commit

Permalink
add support for task-defined options to ULTIMATE tool info module
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
maul-esel committed Dec 19, 2024
1 parent b2cb946 commit f809a0b
Showing 1 changed file with 21 additions and 1 deletion.
22 changes: 21 additions & 1 deletion benchexec/tools/ultimate.py
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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]
Expand All @@ -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(
Expand All @@ -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(
Expand Down

0 comments on commit f809a0b

Please sign in to comment.