From 275136326b0f7537ab7ed204f148e49711285b72 Mon Sep 17 00:00:00 2001 From: Marian Lingsch-Rosenfeld Date: Thu, 16 Nov 2023 13:23:22 +0100 Subject: [PATCH] Add algorithm selection dependent on the property. 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. --- benchexec/tools/metaval.py | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/benchexec/tools/metaval.py b/benchexec/tools/metaval.py index 8e52c7c23..b681951b9 100644 --- a/benchexec/tools/metaval.py +++ b/benchexec/tools/metaval.py @@ -77,6 +77,20 @@ 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( @@ -84,11 +98,14 @@ def cmdline(self, executable, options, task, rlimits): ) 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]