From ac0f422e8db599a8ee68b95a0a0d28957e7cbaa0 Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Wed, 1 Nov 2023 16:25:02 +0100 Subject: [PATCH 1/3] Create concurrentwitness2test.py --- benchexec/tools/concurrentwitness2test.py | 43 +++++++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 benchexec/tools/concurrentwitness2test.py diff --git a/benchexec/tools/concurrentwitness2test.py b/benchexec/tools/concurrentwitness2test.py new file mode 100644 index 000000000..eaffdaa43 --- /dev/null +++ b/benchexec/tools/concurrentwitness2test.py @@ -0,0 +1,43 @@ +# 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 +import benchexec.result as result +import benchexec.tools.template + + +class Tool(benchexec.tools.template.BaseTool2): + + def executable(self, tool_locator): + return tool_locator.find_executable("start.sh") + + def name(self): + return "ConcurrentWitness2Test" + + def version(self, executable): + return self._version_from_tool(executable) + + def cmdline(self, executable, options, task, rlimits): + return [executable, task.single_input_file] + options + + def determine_result(self, run): + status = result.RESULT_UNKNOWN + for line in run.output: + if "Verdict: SOMETIMES" in line or "Verdict: ALWAYS" in line: + status = result.RESULT_FALSE_REACH + elif "Verdict: NEVER" in line: + status = result.RESULT_TRUE_PROP + elif "Verdict: TIMEOUT" in line: + status = result.RESULT_TIMEOUT + "(inner)" + elif "Verdict: Unknown error" in line: + status = result.RESULT_ERROR + elif "Verdict: Incompatible witness" in line: + status = result.RESULT_ERROR + "(Incompatible witness)" + elif "Verdict: Parsing failed" in line: + status = result.RESULT_ERROR + "(Parsing failed)" + elif "Verdict: Compilation error" in line: + status = result.RESULT_ERROR + "(Compilation error)" + + return status From 6e596d93097a31d6ad86bbea853f50609f421af0 Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Wed, 1 Nov 2023 16:30:10 +0100 Subject: [PATCH 2/3] Reformatted using Black --- benchexec/tools/concurrentwitness2test.py | 1 - 1 file changed, 1 deletion(-) diff --git a/benchexec/tools/concurrentwitness2test.py b/benchexec/tools/concurrentwitness2test.py index eaffdaa43..e3ef7d7a4 100644 --- a/benchexec/tools/concurrentwitness2test.py +++ b/benchexec/tools/concurrentwitness2test.py @@ -9,7 +9,6 @@ class Tool(benchexec.tools.template.BaseTool2): - def executable(self, tool_locator): return tool_locator.find_executable("start.sh") From 902e7db2686c4b7d6939f784f3a2b3869763b61c Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Thu, 2 Nov 2023 10:15:33 +0100 Subject: [PATCH 3/3] Update concurrentwitness2test.py from feedback on PR --- benchexec/tools/concurrentwitness2test.py | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/benchexec/tools/concurrentwitness2test.py b/benchexec/tools/concurrentwitness2test.py index e3ef7d7a4..273a32cae 100644 --- a/benchexec/tools/concurrentwitness2test.py +++ b/benchexec/tools/concurrentwitness2test.py @@ -9,6 +9,11 @@ class Tool(benchexec.tools.template.BaseTool2): + """ + Tool info for ConcurrentWitness2Test: A violation witness validator for concurrent programs + URL: https://github.com/ftsrg/ConcurrentWitness2Test + """ + def executable(self, tool_locator): return tool_locator.find_executable("start.sh") @@ -22,21 +27,20 @@ def cmdline(self, executable, options, task, rlimits): return [executable, task.single_input_file] + options def determine_result(self, run): - status = result.RESULT_UNKNOWN for line in run.output: if "Verdict: SOMETIMES" in line or "Verdict: ALWAYS" in line: - status = result.RESULT_FALSE_REACH + return result.RESULT_FALSE_REACH elif "Verdict: NEVER" in line: - status = result.RESULT_TRUE_PROP + return result.RESULT_TRUE_PROP elif "Verdict: TIMEOUT" in line: - status = result.RESULT_TIMEOUT + "(inner)" + return result.RESULT_TIMEOUT + "(inner)" elif "Verdict: Unknown error" in line: - status = result.RESULT_ERROR + return result.RESULT_ERROR elif "Verdict: Incompatible witness" in line: - status = result.RESULT_ERROR + "(Incompatible witness)" + return result.RESULT_ERROR + "(Incompatible witness)" elif "Verdict: Parsing failed" in line: - status = result.RESULT_ERROR + "(Parsing failed)" + return result.RESULT_ERROR + "(Parsing failed)" elif "Verdict: Compilation error" in line: - status = result.RESULT_ERROR + "(Compilation error)" + return result.RESULT_ERROR + "(Compilation error)" - return status + return result.RESULT_UNKNOWN