From 19236957d6fc9c15e37dbdf12f8e93468c3066af Mon Sep 17 00:00:00 2001 From: rmetta Date: Thu, 2 Nov 2023 16:11:31 +0530 Subject: [PATCH 1/7] Proton tool info module proton.py Proton tool info module. --- benchexec/tools/proton.py | 70 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 70 insertions(+) create mode 100644 benchexec/tools/proton.py diff --git a/benchexec/tools/proton.py b/benchexec/tools/proton.py new file mode 100644 index 000000000..ef95f47e7 --- /dev/null +++ b/benchexec/tools/proton.py @@ -0,0 +1,70 @@ +# 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.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64 +import benchexec.tools.template +import benchexec.result as result + + +class Tool(benchexec.tools.template.BaseTool2): + """ + PROTON + """ + + def executable(self, tool_locator): + return tool_locator.find_executable("proton") + + def version(self, executable): + return self._version_from_tool(executable, use_stderr=True) + + def name(self): + return "PROTON" + + def cmdline(self, executable, options, task, rlimits): + if task.property_file: + options = options + ["--propertyFile", task.property_file] + + data_model_param = get_data_model_from_task(task, {ILP32: "32", LP64: "64"}) + if data_model_param and data_model_param not in options: + options += [data_model_param] + + self.options = options + + return [executable] + options + list(task.input_files_or_identifier) + + def determine_result(self, run): + output = run.output + + if run.exit_code.value in [0, 10]: + status = result.RESULT_ERROR + if len(output) > 0: + # SV-COMP mode + result_str = output[-1].strip() + + if result_str == "TRUE": + status = result.RESULT_TRUE_PROP + elif "FALSE" in result_str: + if result_str == "FALSE(termination)": + status = result.RESULT_FALSE_TERMINATION + else: + status = result.RESULT_FALSE_REACH + elif "UNKNOWN" in output: + status = result.RESULT_UNKNOWN + + elif run.exit_code.value == 64 and "Usage error!" in output: + status = "INVALID ARGUMENTS" + + elif run.exit_code.value == 6 and "Out of memory" in output: + status = "OUT OF MEMORY" + + elif run.exit_code.value == 6 and "SAT or SMT checker error: out-of-memory or internal-error" in output: + status = "OUT-OF-MEMORY or INTERNAL-ERROR" + + else: + status = result.RESULT_ERROR + + return status From 2b45b894fe1c1a546e0d6c04684d7af7f5cff79b Mon Sep 17 00:00:00 2001 From: rmetta Date: Thu, 2 Nov 2023 16:25:21 +0530 Subject: [PATCH 2/7] Corrected the tool info for proton --- benchexec/tools/proton.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/benchexec/tools/proton.py b/benchexec/tools/proton.py index ef95f47e7..6bb3db041 100644 --- a/benchexec/tools/proton.py +++ b/benchexec/tools/proton.py @@ -61,7 +61,7 @@ def determine_result(self, run): elif run.exit_code.value == 6 and "Out of memory" in output: status = "OUT OF MEMORY" - elif run.exit_code.value == 6 and "SAT or SMT checker error: out-of-memory or internal-error" in output: + elif run.exit_code.value == 6: status = "OUT-OF-MEMORY or INTERNAL-ERROR" else: From c88b3ee62c2e1e02cc240b9a36b5256c8c5ea655 Mon Sep 17 00:00:00 2001 From: rmetta Date: Thu, 2 Nov 2023 17:46:35 +0530 Subject: [PATCH 3/7] Proton tool info module, Philipp Wendler comments Proton tool info module, incorporating most of Philipp Wendler comments. We only dodn't do replacing assignments to status with returns (as we find this to be a better) --- benchexec/tools/proton.py | 38 ++++++++++++++++---------------------- 1 file changed, 16 insertions(+), 22 deletions(-) diff --git a/benchexec/tools/proton.py b/benchexec/tools/proton.py index 6bb3db041..99b5ddd93 100644 --- a/benchexec/tools/proton.py +++ b/benchexec/tools/proton.py @@ -12,7 +12,7 @@ class Tool(benchexec.tools.template.BaseTool2): """ - PROTON + PROTON -- intended to be shared in future at : https://github.com/kumarmadhukar/term """ def executable(self, tool_locator): @@ -32,35 +32,29 @@ def cmdline(self, executable, options, task, rlimits): if data_model_param and data_model_param not in options: options += [data_model_param] - self.options = options - - return [executable] + options + list(task.input_files_or_identifier) + return [executable] + options + [task.single_input_file] def determine_result(self, run): output = run.output - if run.exit_code.value in [0, 10]: - status = result.RESULT_ERROR - if len(output) > 0: - # SV-COMP mode - result_str = output[-1].strip() - - if result_str == "TRUE": - status = result.RESULT_TRUE_PROP - elif "FALSE" in result_str: - if result_str == "FALSE(termination)": - status = result.RESULT_FALSE_TERMINATION - else: - status = result.RESULT_FALSE_REACH - elif "UNKNOWN" in output: - status = result.RESULT_UNKNOWN + status = result.RESULT_ERROR + if run.exit_code.value in [0, 10] and len(output) > 0: + # SV-COMP mode + result_str = output[-1].strip() + + if result_str == "TRUE": + status = result.RESULT_TRUE_PROP + elif "FALSE" in result_str: + if result_str == "FALSE(termination)": + status = result.RESULT_FALSE_TERMINATION + else: + status = result.RESULT_FALSE_REACH + elif "UNKNOWN" in output: + status = result.RESULT_UNKNOWN elif run.exit_code.value == 64 and "Usage error!" in output: status = "INVALID ARGUMENTS" - elif run.exit_code.value == 6 and "Out of memory" in output: - status = "OUT OF MEMORY" - elif run.exit_code.value == 6: status = "OUT-OF-MEMORY or INTERNAL-ERROR" From cfd1f0be80732796ef9a62ca301885e0c32aec4d Mon Sep 17 00:00:00 2001 From: rmetta Date: Thu, 2 Nov 2023 18:50:35 +0530 Subject: [PATCH 4/7] Updated with URL and removed the confusing comment The URL provided : https://github.com/kumarmadhukar/term : is currently private. We have plenty of errors to weed out in this initial version of Proton code. Once this is done, we will make the tool available at the above website. --- benchexec/tools/proton.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/benchexec/tools/proton.py b/benchexec/tools/proton.py index 99b5ddd93..b21af9901 100644 --- a/benchexec/tools/proton.py +++ b/benchexec/tools/proton.py @@ -12,7 +12,7 @@ class Tool(benchexec.tools.template.BaseTool2): """ - PROTON -- intended to be shared in future at : https://github.com/kumarmadhukar/term + PROTON --- https://github.com/kumarmadhukar/term """ def executable(self, tool_locator): @@ -39,7 +39,6 @@ def determine_result(self, run): status = result.RESULT_ERROR if run.exit_code.value in [0, 10] and len(output) > 0: - # SV-COMP mode result_str = output[-1].strip() if result_str == "TRUE": From bacb3d32100e12d69ba567871d76da2b323c7c0d Mon Sep 17 00:00:00 2001 From: rmetta Date: Thu, 2 Nov 2023 19:54:03 +0530 Subject: [PATCH 5/7] Corrected the error codes Made the error codes in sync with Proton's error codes and strings, to address Philipp Wendler's review comments, with many thanks. --- benchexec/tools/proton.py | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/benchexec/tools/proton.py b/benchexec/tools/proton.py index b21af9901..27955fb09 100644 --- a/benchexec/tools/proton.py +++ b/benchexec/tools/proton.py @@ -43,20 +43,22 @@ def determine_result(self, run): if result_str == "TRUE": status = result.RESULT_TRUE_PROP - elif "FALSE" in result_str: - if result_str == "FALSE(termination)": - status = result.RESULT_FALSE_TERMINATION - else: - status = result.RESULT_FALSE_REACH + + elif "FALSE(termination)" in result_str: + status = result.RESULT_FALSE_TERMINATION + elif "UNKNOWN" in output: status = result.RESULT_UNKNOWN + elif "INTERNAL-ERROR" in result_str: + status = "OUT-OF-MEMORY or INTERNAL-ERROR" + + elif "INCONCLUSIVE" in result_str: + status = "INCONCLUSIVE" + elif run.exit_code.value == 64 and "Usage error!" in output: status = "INVALID ARGUMENTS" - elif run.exit_code.value == 6: - status = "OUT-OF-MEMORY or INTERNAL-ERROR" - else: status = result.RESULT_ERROR From bb769a82dcc80466e5d4f7b8d0fadc6bd202ad9b Mon Sep 17 00:00:00 2001 From: rmetta Date: Thu, 2 Nov 2023 20:18:40 +0530 Subject: [PATCH 6/7] Fixed inconsistent usage of result_str and output Fixed inconsistent usage of result_str and output (pointed out by Philipp Wendler in his review). --- benchexec/tools/proton.py | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/benchexec/tools/proton.py b/benchexec/tools/proton.py index 27955fb09..c62308e0f 100644 --- a/benchexec/tools/proton.py +++ b/benchexec/tools/proton.py @@ -47,7 +47,7 @@ def determine_result(self, run): elif "FALSE(termination)" in result_str: status = result.RESULT_FALSE_TERMINATION - elif "UNKNOWN" in output: + elif "UNKNOWN" in result_str: status = result.RESULT_UNKNOWN elif "INTERNAL-ERROR" in result_str: @@ -59,7 +59,4 @@ def determine_result(self, run): elif run.exit_code.value == 64 and "Usage error!" in output: status = "INVALID ARGUMENTS" - else: - status = result.RESULT_ERROR - return status From 208bdd643f5e6b572f93ddfcac460bfd563528e2 Mon Sep 17 00:00:00 2001 From: rmetta Date: Thu, 2 Nov 2023 21:13:44 +0530 Subject: [PATCH 7/7] Replaced error codes with relvant error strings --- benchexec/tools/proton.py | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/benchexec/tools/proton.py b/benchexec/tools/proton.py index c62308e0f..05e388024 100644 --- a/benchexec/tools/proton.py +++ b/benchexec/tools/proton.py @@ -38,25 +38,31 @@ def determine_result(self, run): output = run.output status = result.RESULT_ERROR + + result_str = "UNKNOWN ERROR" + if run.exit_code.value in [0, 10] and len(output) > 0: result_str = output[-1].strip() - if result_str == "TRUE": - status = result.RESULT_TRUE_PROP + if result_str == "TRUE": + status = result.RESULT_TRUE_PROP + + elif "FALSE(termination)" in result_str: + status = result.RESULT_FALSE_TERMINATION - elif "FALSE(termination)" in result_str: - status = result.RESULT_FALSE_TERMINATION + elif "UNKNOWN" in result_str: + status = result.RESULT_UNKNOWN - elif "UNKNOWN" in result_str: - status = result.RESULT_UNKNOWN + elif "INTERNAL-ERROR" in result_str: + status = "INTERNAL-ERROR" - elif "INTERNAL-ERROR" in result_str: - status = "OUT-OF-MEMORY or INTERNAL-ERROR" + elif "OUT OF MEMORY" in result_str: + status = "OUT OF MEMORY" - elif "INCONCLUSIVE" in result_str: - status = "INCONCLUSIVE" + elif "INCONCLUSIVE" in result_str: + status = "INCONCLUSIVE" - elif run.exit_code.value == 64 and "Usage error!" in output: - status = "INVALID ARGUMENTS" + elif "UNRECOGNIZED PROPERTY" in result_str: + status = "UNSUPPORTED PROPERTY SPECIFIED" return status