From 8e56628481ead07cee9b706e87196d39261e1636 Mon Sep 17 00:00:00 2001 From: Henrik Wachowitz Date: Tue, 15 Oct 2024 16:20:44 +0200 Subject: [PATCH 1/6] add nacpa ti module --- benchexec/tools/nacpa.py | 85 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 benchexec/tools/nacpa.py diff --git a/benchexec/tools/nacpa.py b/benchexec/tools/nacpa.py new file mode 100644 index 000000000..9e9b97311 --- /dev/null +++ b/benchexec/tools/nacpa.py @@ -0,0 +1,85 @@ +from benchexec import result +from benchexec.tools import template + + +class Tool(template.BaseTool2): + """ + This tool-info module runs nacpa, a parallel portfolio + of natively compiled CPAchecker instances. + """ + + REQUIRED_PATHS = ["bin", "lib"] + + def executable(self, tool_locator): + return tool_locator.find_executable("nacpa", subdir="bin") + + def version(self, executable): + return self._version_from_tool( + executable, "--version", line_prefix="nacpa version" + ) + + def program_files(self, executable): + return self._program_files_from_executable( + executable, self.REQUIRED_PATHS, parent_dir=True + ) + + def name(self): + return "nacpa" + + def cmdline(self, executable, options, task, rlimits): + if "--spec" not in options and task.property_file: + options = options + ["--spec", task.property_file] + + if ( + "--data-model" not in options + and isinstance(task.options, dict) + and task.options.get("language") == "C" + ): + data_model = task.options.get("data_model") + if data_model: + options = options + ["--data-model", data_model] + + return super().cmdline(executable, options, task, rlimits) + + def determine_result(self, run): + for line in reversed(run.output): + if line.startswith("VERDICT: "): + verdict = line.partition(":")[-1].strip().lower() + if verdict.lower().startswith("true"): + return result.RESULT_TRUE_PROP + elif verdict.lower().startswith("false(unreach-call)"): + return result.RESULT_FALSE_REACH + elif verdict.lower().startswith("false(termination)"): + return result.RESULT_FALSE_TERMINATION + elif verdict.lower().startswith("false(no-overflow)"): + return result.RESULT_FALSE_OVERFLOW + elif verdict.lower().startswith("false(no-deadlock)"): + return result.RESULT_FALSE_DEADLOCK + elif verdict.lower().startswith("false(valid-deref)"): + return result.RESULT_FALSE_DEREF + elif verdict.lower().startswith("false(valid-free)"): + return result.RESULT_FALSE_FREE + elif verdict.lower().startswith("false(valid-memtrack)"): + return result.RESULT_FALSE_MEMTRACK + elif verdict.lower().startswith("false(valid-memcleanup)"): + return result.RESULT_FALSE_MEMCLEANUP + elif verdict.lower().startswith("false"): + return result.RESULT_FALSE_PROP + return result.RESULT_UNKNOWN + + def get_value_from_output(self, output, identifier): + # search for the text in output and get its value, + # search the first line, that starts with the searched text + # warn if there are more lines (multiple statistics from sequential analysis?) + match = None + for line in output: + if line.lstrip().startswith(identifier): + startPosition = line.find(":") + 1 + endPosition = line.find("(", startPosition) + if endPosition == -1: + endPosition = len(line) + if match is None: + match = line[startPosition:endPosition].strip() + break + + return match From aca22f9937a701c7ef7d95d9d403598cb5cfac3a Mon Sep 17 00:00:00 2001 From: Henrik Wachowitz Date: Tue, 15 Oct 2024 16:24:14 +0200 Subject: [PATCH 2/6] add license header --- benchexec/tools/nacpa.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/benchexec/tools/nacpa.py b/benchexec/tools/nacpa.py index 9e9b97311..f7c2baba8 100644 --- a/benchexec/tools/nacpa.py +++ b/benchexec/tools/nacpa.py @@ -1,3 +1,10 @@ +# This file is part of BenchExec, a framework for reliable benchmarking: +# https://github.com/sosy-lab/benchexec +# +# SPDX-FileCopyrightText: 2007-2020 Dirk Beyer +# +# SPDX-License-Identifier: Apache-2.0 + from benchexec import result from benchexec.tools import template From fa33c8e3a8fed767ade1acb56fe016c314908ffa Mon Sep 17 00:00:00 2001 From: Henrik Wachowitz <35438508+ricffb@users.noreply.github.com> Date: Wed, 16 Oct 2024 11:18:42 +0200 Subject: [PATCH 3/6] change wording in docstring Co-authored-by: Philipp Wendler <2545335+PhilippWendler@users.noreply.github.com> --- benchexec/tools/nacpa.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/benchexec/tools/nacpa.py b/benchexec/tools/nacpa.py index f7c2baba8..26c421ed1 100644 --- a/benchexec/tools/nacpa.py +++ b/benchexec/tools/nacpa.py @@ -11,7 +11,7 @@ class Tool(template.BaseTool2): """ - This tool-info module runs nacpa, a parallel portfolio + Tool-info module for nacpa, a parallel portfolio of natively compiled CPAchecker instances. """ From bd2286e3f7b3fa59b6098c0ff7d1c77cf8f28ce8 Mon Sep 17 00:00:00 2001 From: Henrik Wachowitz Date: Wed, 16 Oct 2024 11:36:24 +0200 Subject: [PATCH 4/6] add project url --- benchexec/tools/nacpa.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/benchexec/tools/nacpa.py b/benchexec/tools/nacpa.py index 26c421ed1..fe037329c 100644 --- a/benchexec/tools/nacpa.py +++ b/benchexec/tools/nacpa.py @@ -33,6 +33,9 @@ def program_files(self, executable): def name(self): return "nacpa" + def project_url(self): + return "https://gitlab.com/sosy-lab/software/nacpa" + def cmdline(self, executable, options, task, rlimits): if "--spec" not in options and task.property_file: options = options + ["--spec", task.property_file] From 50322cc12cfdb37e5691c4b8d466c35251440e4a Mon Sep 17 00:00:00 2001 From: Henrik Wachowitz Date: Wed, 16 Oct 2024 11:36:45 +0200 Subject: [PATCH 5/6] explicitly require a single input file --- benchexec/tools/nacpa.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/benchexec/tools/nacpa.py b/benchexec/tools/nacpa.py index fe037329c..a62dae380 100644 --- a/benchexec/tools/nacpa.py +++ b/benchexec/tools/nacpa.py @@ -49,7 +49,7 @@ def cmdline(self, executable, options, task, rlimits): if data_model: options = options + ["--data-model", data_model] - return super().cmdline(executable, options, task, rlimits) + return [executable, *options, task.single_input_file] def determine_result(self, run): for line in reversed(run.output): From f7bf0105d68456f61ebd8d01ebba56da24e6d29a Mon Sep 17 00:00:00 2001 From: Henrik Wachowitz Date: Wed, 16 Oct 2024 11:37:20 +0200 Subject: [PATCH 6/6] refactor get_value_from_output --- benchexec/tools/nacpa.py | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/benchexec/tools/nacpa.py b/benchexec/tools/nacpa.py index a62dae380..16823d0f3 100644 --- a/benchexec/tools/nacpa.py +++ b/benchexec/tools/nacpa.py @@ -78,18 +78,14 @@ def determine_result(self, run): return result.RESULT_UNKNOWN def get_value_from_output(self, output, identifier): - # search for the text in output and get its value, - # search the first line, that starts with the searched text - # warn if there are more lines (multiple statistics from sequential analysis?) - match = None for line in output: if line.lstrip().startswith(identifier): startPosition = line.find(":") + 1 endPosition = line.find("(", startPosition) + if endPosition == -1: endPosition = len(line) - if match is None: - match = line[startPosition:endPosition].strip() - break - return match + return line[startPosition:endPosition].strip() + + return None