Skip to content

Commit

Permalink
Add algorithm selection dependent on the property.
Browse files Browse the repository at this point in the history
While previously SV-COMP allowed the selection of the backend tool for MetaVal based on the property in the benchmark definition files, this changed with SV-COMP24.
Due to this, the selection needs to be moved either into MetaVal or into the benchmark definition module.
Since the BenchExec tool info module contains some necessary preprocessing to determine the backend tool to be executed, using the ToolLocator, it is probably for the best to implement the algorithm selection inside it.
  • Loading branch information
Marian Lingsch-Rosenfeld committed Nov 16, 2023
1 parent 2cd705d commit 2751363
Showing 1 changed file with 18 additions and 1 deletion.
19 changes: 18 additions & 1 deletion benchexec/tools/metaval.py
Original file line number Diff line number Diff line change
Expand Up @@ -77,18 +77,35 @@ def determine_result(self, run):
), "we expect that all wrapped tools extend BaseTool2"
return tool.determine_result(run)

def _select_verifier_from_property(self, property: str):
if "unreach-call" in property:
return "cpachecker"
elif "valid-memcleanup" in property:
return "symbiotic"
elif "valid-memsafety" in property:
return "symbiotic"
elif "no-overflow" in property:
return "ultimateautomizer"
elif "termination" in property:
return "ultimateautomizer"
else:
assert False, "Could not determine verifier from property file!"

def cmdline(self, executable, options, task, rlimits):
if not task.property_file:
raise UnsupportedFeatureException(
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("--metavalVerifierBackend", required=True)
parser.add_argument("--metavalVerifierBackend", default=None)
parser.add_argument("--metavalAdditionalPATH")
parser.add_argument("--metavalWitnessType")
(knownargs, options) = parser.parse_known_args(options)
verifierName = knownargs.metavalVerifierBackend.lower()
if verifierName is None:
verifierName = self._select_verifier_from_property(str(task.property_file))

witnessName = knownargs.metavalWitness
additionalPathArgument = (
["--additionalPATH", knownargs.metavalAdditionalPATH]
Expand Down

0 comments on commit 2751363

Please sign in to comment.