Skip to content

Commit

Permalink
Merge pull request #1093 from sosy-lab/handle-validation-tasks-valida…
Browse files Browse the repository at this point in the history
…tors

Update all validators to handle Validation tasks
  • Loading branch information
dbeyer authored Nov 20, 2024
2 parents 0b288c9 + ab4791f commit 638480c
Show file tree
Hide file tree
Showing 20 changed files with 504 additions and 44 deletions.
9 changes: 8 additions & 1 deletion benchexec/tools/concurrentwitness2test.py
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,10 @@
# SPDX-License-Identifier: Apache-2.0
import benchexec.result as result
import benchexec.tools.template
from benchexec.tools.sv_benchmarks_util import (
handle_witness_of_task,
TaskFilesConsidered,
)


class Tool(benchexec.tools.template.BaseTool2):
Expand All @@ -26,7 +30,10 @@ def version(self, executable):
return self._version_from_tool(executable)

def cmdline(self, executable, options, task, rlimits):
return [executable, task.single_input_file] + options
input_file, witness_options = handle_witness_of_task(
task, options, "--witness", TaskFilesConsidered.SINGLE_INPUT_FILE
)
return [executable] + input_file + options + witness_options

def determine_result(self, run):
for line in run.output:
Expand Down
6 changes: 5 additions & 1 deletion benchexec/tools/cpa-witness2test.py
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,9 @@
import benchexec.tools.cpachecker as cpachecker

from benchexec.tools.template import ToolNotFoundException
from benchexec.tools.sv_benchmarks_util import (
get_single_non_witness_input_file,
)


class Tool(cpachecker.Tool):
Expand Down Expand Up @@ -51,4 +54,5 @@ 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 = [get_single_non_witness_input_file(task)]
return [executable] + additional_options + options + input_files
17 changes: 9 additions & 8 deletions benchexec/tools/cpachecker.py
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,16 @@
# SPDX-License-Identifier: Apache-2.0

import logging
import sys
import os
import re
import sys

import benchexec.result as result
import benchexec.tools.template

from benchexec.tools.sv_benchmarks_util import (
get_non_witness_input_files_or_identifier,
get_witness_options,
)
from benchexec.tools.template import ToolNotFoundException


Expand Down Expand Up @@ -180,16 +183,14 @@ def option_present(option):
f"Unsupported data_model '{data_model}' defined for task '{task}'"
)

options += get_witness_options(options, task, [f"{prefix}witness"])

return options

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 = get_non_witness_input_files_or_identifier(task)
return [executable] + options + additional_options + input_files

def determine_result(self, run):
"""
Expand Down
9 changes: 8 additions & 1 deletion benchexec/tools/dartagnan.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,10 @@

import benchexec.tools.template
import benchexec.result as result
from benchexec.tools.sv_benchmarks_util import (
TaskFilesConsidered,
handle_witness_of_task,
)


class Tool(benchexec.tools.template.BaseTool2):
Expand All @@ -26,7 +30,10 @@ def project_url(self):
def cmdline(self, executable, options, task, rlimits):
if task.property_file:
options += [task.property_file]
return [executable] + options + list(task.input_files_or_identifier)
input_files, witness_options = handle_witness_of_task(
task, options, "-witness", TaskFilesConsidered.INPUT_FILES_OR_IDENTIFIER
)
return [executable] + options + witness_options + input_files

def version(self, executable):
return self._version_from_tool(executable)
Expand Down
16 changes: 14 additions & 2 deletions benchexec/tools/fshell-witness2test.py
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,13 @@

import benchexec.result as result
import benchexec.tools.template
from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
from benchexec.tools.sv_benchmarks_util import (
get_data_model_from_task,
ILP32,
LP64,
TaskFilesConsidered,
handle_witness_of_task,
)


class Tool(benchexec.tools.template.BaseTool2):
Expand Down Expand Up @@ -62,7 +68,13 @@ def cmdline(self, executable, options, task, rlimits):
if data_model_param and data_model_param not in options:
options += [data_model_param]

return [executable] + options + list(task.input_files_or_identifier)
input_files, witness_options = handle_witness_of_task(
task,
options,
"--graphml-witness",
TaskFilesConsidered.INPUT_FILES_OR_IDENTIFIER,
)
return [executable] + options + witness_options + input_files

def determine_result(self, run):
"""
Expand Down
20 changes: 15 additions & 5 deletions benchexec/tools/goblint.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,15 @@
#
# SPDX-License-Identifier: Apache-2.0

import benchexec.tools.template
import benchexec.result as result

import re
import logging
import re

import benchexec.result as result
import benchexec.tools.template
from benchexec.tools.sv_benchmarks_util import (
get_witness_options,
get_non_witness_input_files,
)


class Tool(benchexec.tools.template.BaseTool2):
Expand Down Expand Up @@ -63,11 +67,17 @@ def cmdline(self, executable, options, task, rlimits):
f"Unsupported data_model '{data_model}'"
)

witness_options = get_witness_options(
options, task, ["--witness.yaml.validate", "--witness.yaml.unassume"]
)
input_files = get_non_witness_input_files(task)

return [
executable,
*options,
*additional_options,
*task.input_files,
*witness_options,
*input_files,
]

def determine_result(self, run):
Expand Down
15 changes: 13 additions & 2 deletions benchexec/tools/gwit.py
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,10 @@
# SPDX-License-Identifier: Apache-2.0

import benchexec.result as result
from benchexec.tools.sv_benchmarks_util import (
handle_witness_of_task,
TaskFilesConsidered,
)
from benchexec.tools.template import BaseTool2


Expand All @@ -28,10 +32,17 @@ def project_url(self):
return "https://github.com/tudo-aqua/gwit"

def cmdline(self, executable, options, task, rlimits):
cmd = [executable] + options
input_files, witness_options = handle_witness_of_task(
task,
options,
"--witness",
TaskFilesConsidered.INPUT_FILES,
)

cmd = [executable] + options + witness_options
if task.property_file:
cmd.append(task.property_file)
return cmd + list(task.input_files)
return cmd + input_files

def determine_result(self, run):
status = result.RESULT_ERROR
Expand Down
15 changes: 13 additions & 2 deletions benchexec/tools/jcwit.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,12 @@
#
# SPDX-License-Identifier: Apache-2.0

import benchexec.tools.template
import benchexec.result as result
import benchexec.tools.template
from benchexec.tools.sv_benchmarks_util import (
TaskFilesConsidered,
handle_witness_of_task,
)


class Tool(benchexec.tools.template.BaseTool2):
Expand All @@ -27,7 +31,14 @@ def project_url(self):
return "https://github.com/Chriszai/JCWIT"

def cmdline(self, executable, options, task, rlimits):
return [executable] + options + list(task.input_files)
input_files, witness_options = handle_witness_of_task(
task,
options,
"--witness",
TaskFilesConsidered.INPUT_FILES,
)

return [executable] + options + witness_options + input_files

def determine_result(self, run):
for line in run.output:
Expand Down
18 changes: 15 additions & 3 deletions benchexec/tools/liv.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,10 +7,15 @@

import logging
import re

import benchexec.result
from benchexec.tools.sv_benchmarks_util import ILP32, LP64, get_data_model_from_task
from benchexec.tools.template import BaseTool2
from benchexec.tools.sv_benchmarks_util import (
ILP32,
LP64,
get_data_model_from_task,
TaskFilesConsidered,
handle_witness_of_task,
)


class Tool(BaseTool2):
Expand Down Expand Up @@ -48,7 +53,14 @@ def cmdline(self, executable, options, task, rlimits):
if data_model_param and "--data-model" not in options:
options += ["--data-model", data_model_param]

return [executable] + options + list(task.input_files_or_identifier)
input_files, witness_options = handle_witness_of_task(
task,
options,
"--witness",
TaskFilesConsidered.INPUT_FILES_OR_IDENTIFIER,
)

return [executable] + options + witness_options + input_files

def determine_result(self, run):
if not run.output:
Expand Down
14 changes: 12 additions & 2 deletions benchexec/tools/metaval++.py
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,13 @@
import re

import benchexec.result
from benchexec.tools.sv_benchmarks_util import ILP32, LP64, get_data_model_from_task
from benchexec.tools.sv_benchmarks_util import (
ILP32,
LP64,
get_data_model_from_task,
TaskFilesConsidered,
handle_witness_of_task,
)
from benchexec.tools.template import BaseTool2


Expand Down Expand Up @@ -42,7 +48,11 @@ def cmdline(self, executable, options, task, rlimits):
if data_model_param and "--data-model" not in options:
options += ["--data-model", data_model_param]

return [executable] + options + [task.single_input_file]
input_file, witness_options = handle_witness_of_task(
task, options, "--witness", TaskFilesConsidered.SINGLE_INPUT_FILE
)

return [executable] + options + witness_options + [input_file]

def determine_result(self, run):
separator = ":"
Expand Down
13 changes: 11 additions & 2 deletions benchexec/tools/metaval.py
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,10 @@

from benchexec.tools.template import BaseTool2
from benchexec.tools.template import UnsupportedFeatureException
from benchexec.tools.sv_benchmarks_util import (
get_witness,
get_single_non_witness_input_file,
)


class Tool(benchexec.tools.template.BaseTool2):
Expand Down Expand Up @@ -83,13 +87,16 @@ def cmdline(self, executable, options, task, rlimits):
f"Execution without property file is not supported by {self.name()}!"
)
parser = argparse.ArgumentParser(add_help=False, usage=argparse.SUPPRESS)
parser.add_argument("--metavalWitness", required=True)
parser.add_argument("--metavalWitness", default=None)
parser.add_argument("--metavalVerifierBackend", required=True)
parser.add_argument("--metavalAdditionalPATH")
parser.add_argument("--metavalWitnessType")
(knownargs, options) = parser.parse_known_args(options)
verifierName = knownargs.metavalVerifierBackend.lower()
witnessName = knownargs.metavalWitness
if knownargs.metavalWitness is None:
witnessName = get_witness(task)

additionalPathArgument = (
["--additionalPATH", knownargs.metavalAdditionalPATH]
if knownargs.metavalAdditionalPATH
Expand Down Expand Up @@ -130,6 +137,8 @@ def cmdline(self, executable, options, task, rlimits):
rlimits,
)

input_file = get_single_non_witness_input_file(task)

return (
[
executable,
Expand All @@ -141,7 +150,7 @@ def cmdline(self, executable, options, task, rlimits):
+ additionalPathArgument
+ witnessTypeArgument
+ ["--property", task.property_file]
+ [task.single_input_file]
+ [input_file]
+ ["--"]
+ wrappedOptions
)
Expand Down
15 changes: 13 additions & 2 deletions benchexec/tools/mopsa.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,12 @@
#
# SPDX-License-Identifier: Apache-2.0

import benchexec.tools.template
import benchexec.result as result
import benchexec.tools.template
from benchexec.tools.sv_benchmarks_util import (
TaskFilesConsidered,
handle_witness_of_task,
)


class Tool(benchexec.tools.template.BaseTool2):
Expand All @@ -27,7 +31,14 @@ def project_url(self):
return "https://gitlab.com/mopsa/mopsa-analyzer/"

def cmdline(self, executable, options, task, rlimits):
cmd = [executable, "--program", *task.input_files]
input_files, witness_options = handle_witness_of_task(
task,
options,
"--validate_yaml_witness",
TaskFilesConsidered.INPUT_FILES,
)

cmd = [executable, "--program"] + input_files + witness_options
if task.options is not None and "data_model" in task.options:
cmd += ["--data_model", task.options.get("data_model")]
if task.property_file:
Expand Down
Loading

0 comments on commit 638480c

Please sign in to comment.