From 9aad96794eb77e4dce59a8b15fcc0c2af23c870d Mon Sep 17 00:00:00 2001 From: passengerZ <904806153@qq.com> Date: Tue, 31 Oct 2023 22:51:34 -0700 Subject: [PATCH 1/8] FDSE: add tool info module --- benchexec/tools/fdse.py | 77 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) create mode 100755 benchexec/tools/fdse.py diff --git a/benchexec/tools/fdse.py b/benchexec/tools/fdse.py new file mode 100755 index 000000000..d8fdde918 --- /dev/null +++ b/benchexec/tools/fdse.py @@ -0,0 +1,77 @@ +# 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 +import benchexec.model +from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64 +import os + +class Tool(benchexec.tools.template.BaseTool2): + """ + Tool info for FDSE (https://github.com/zbchen/FDSE). + """ + + def executable(self, tool_locator): + return tool_locator.find_executable("fdse") + + def program_files(self, executable): + return self._program_files_from_executable( + executable, self.REQUIRED_PATHS, parent_dir=True + ) + + def version(self, executable): + return "fdse-testcomp" + + def cmdline(self, executable, options, task, rlimits): + new_option = ["--testcomp"] + if task.property_file: + new_option += [f"--property-file={task.property_file}"] + if rlimits.cputime: + new_option += [f"-mt={rlimits.cputime}"] + data_model_param = get_data_model_from_task(task, {ILP32: "32", LP64: "64"}) + + if data_model_param and "--arch" not in options: + new_option += ["--arch="+data_model_param] + + new_option += [f"-sf={task.single_input_file}"] + return [executable] + new_option + options + + def name(self): + return "FDSE" + + def determine_result(self, run): + """ + Parse the output of the tool and extract the verification result. + This method always needs to be overridden. + If the tool gave a result, this method needs to return one of the + benchexec.result.RESULT_* strings. + Otherwise an arbitrary string can be returned that will be shown to the user + and should give some indication of the failure reason + (e.g., "CRASH", "OUT_OF_MEMORY", etc.). + """ + for line in run.output: + if "[BUG]" in line: + if line.find("ASSERTION FAIL!") != -1: + return result.RESULT_FALSE_REACH + elif line.find("Index out-of-bound") != -1: + return result.RESULT_FALSE_DEREF + elif line.find("overflow") != -1: + return result.RESULT_FALSE_OVERFLOW + else: + return f"ERROR ({run.exit_code.value})" + if "Done : End analysis" in line: + return result.RESULT_DONE + return result.RESULT_UNKNOWN + + def get_value_from_output(self, run): + status = result.RESULT_UNKNOWN + + if run.output.any_line_contains("DONE"): + status = result.RESULT_DONE + + return status From b9cca4e95d4decb0802da3732064bd5dadfefd4e Mon Sep 17 00:00:00 2001 From: passengerZ <904806153@qq.com> Date: Tue, 31 Oct 2023 22:56:52 -0700 Subject: [PATCH 2/8] FDSE: adjust code format in tool info module --- benchexec/tools/fdse.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/benchexec/tools/fdse.py b/benchexec/tools/fdse.py index d8fdde918..3d9b1278a 100755 --- a/benchexec/tools/fdse.py +++ b/benchexec/tools/fdse.py @@ -9,7 +9,6 @@ import benchexec.tools.template import benchexec.model from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64 -import os class Tool(benchexec.tools.template.BaseTool2): """ @@ -36,7 +35,7 @@ def cmdline(self, executable, options, task, rlimits): data_model_param = get_data_model_from_task(task, {ILP32: "32", LP64: "64"}) if data_model_param and "--arch" not in options: - new_option += ["--arch="+data_model_param] + new_option += ["--arch=" + data_model_param] new_option += [f"-sf={task.single_input_file}"] return [executable] + new_option + options From c7cd5d1932831fecd7cfff3f65aa793535ec84f1 Mon Sep 17 00:00:00 2001 From: passengerZ <904806153@qq.com> Date: Tue, 31 Oct 2023 23:17:17 -0700 Subject: [PATCH 3/8] FDSE: refactor tool info module --- benchexec/tools/fdse.py | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/benchexec/tools/fdse.py b/benchexec/tools/fdse.py index 3d9b1278a..5ab10fc35 100755 --- a/benchexec/tools/fdse.py +++ b/benchexec/tools/fdse.py @@ -5,14 +5,14 @@ # # SPDX-License-Identifier: Apache-2.0 -import benchexec.result as result import benchexec.tools.template -import benchexec.model -from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64 +import benchexec.result as result + class Tool(benchexec.tools.template.BaseTool2): """ - Tool info for FDSE (https://github.com/zbchen/FDSE). + Tool info for FDSE. + https://github.com/zbchen/FDSE """ def executable(self, tool_locator): @@ -32,10 +32,6 @@ def cmdline(self, executable, options, task, rlimits): new_option += [f"--property-file={task.property_file}"] if rlimits.cputime: new_option += [f"-mt={rlimits.cputime}"] - data_model_param = get_data_model_from_task(task, {ILP32: "32", LP64: "64"}) - - if data_model_param and "--arch" not in options: - new_option += ["--arch=" + data_model_param] new_option += [f"-sf={task.single_input_file}"] return [executable] + new_option + options From a998c72e0ec3a99fd41aa7602bfae9c819e794f3 Mon Sep 17 00:00:00 2001 From: passengerZ <904806153@qq.com> Date: Wed, 1 Nov 2023 05:40:52 -0700 Subject: [PATCH 4/8] FDSE: refactor tool info module --- benchexec/tools/fdse.py | 37 ++++++++----------------------------- 1 file changed, 8 insertions(+), 29 deletions(-) diff --git a/benchexec/tools/fdse.py b/benchexec/tools/fdse.py index 5ab10fc35..422621787 100755 --- a/benchexec/tools/fdse.py +++ b/benchexec/tools/fdse.py @@ -12,22 +12,17 @@ class Tool(benchexec.tools.template.BaseTool2): """ Tool info for FDSE. - https://github.com/zbchen/FDSE + https://github.com/zbchen/FDSE (now is private) """ def executable(self, tool_locator): return tool_locator.find_executable("fdse") - def program_files(self, executable): - return self._program_files_from_executable( - executable, self.REQUIRED_PATHS, parent_dir=True - ) - def version(self, executable): - return "fdse-testcomp" + return self._version_from_tool(executable, "-v") def cmdline(self, executable, options, task, rlimits): - new_option = ["--testcomp"] + new_option = [] if task.property_file: new_option += [f"--property-file={task.property_file}"] if rlimits.cputime: @@ -40,33 +35,17 @@ def name(self): return "FDSE" def determine_result(self, run): - """ - Parse the output of the tool and extract the verification result. - This method always needs to be overridden. - If the tool gave a result, this method needs to return one of the - benchexec.result.RESULT_* strings. - Otherwise an arbitrary string can be returned that will be shown to the user - and should give some indication of the failure reason - (e.g., "CRASH", "OUT_OF_MEMORY", etc.). - """ for line in run.output: if "[BUG]" in line: - if line.find("ASSERTION FAIL!") != -1: + if "ASSERTION FAIL!" in line: return result.RESULT_FALSE_REACH - elif line.find("Index out-of-bound") != -1: + elif "Index out-of-bound" in line: return result.RESULT_FALSE_DEREF - elif line.find("overflow") != -1: + elif "overflow" in line: return result.RESULT_FALSE_OVERFLOW else: - return f"ERROR ({run.exit_code.value})" + return result.RESULT_ERROR if "Done : End analysis" in line: return result.RESULT_DONE return result.RESULT_UNKNOWN - - def get_value_from_output(self, run): - status = result.RESULT_UNKNOWN - - if run.output.any_line_contains("DONE"): - status = result.RESULT_DONE - - return status + From 83b0b9b1c5b19968297414aa386b4a5b7fe0c4d4 Mon Sep 17 00:00:00 2001 From: passengerZ <904806153@qq.com> Date: Wed, 1 Nov 2023 05:48:14 -0700 Subject: [PATCH 5/8] FDSE: fix format --- benchexec/tools/fdse.py | 1 - 1 file changed, 1 deletion(-) diff --git a/benchexec/tools/fdse.py b/benchexec/tools/fdse.py index 422621787..ed801655b 100755 --- a/benchexec/tools/fdse.py +++ b/benchexec/tools/fdse.py @@ -48,4 +48,3 @@ def determine_result(self, run): if "Done : End analysis" in line: return result.RESULT_DONE return result.RESULT_UNKNOWN - From 547a500934f97948f5ff72d624ad77a605f1de4f Mon Sep 17 00:00:00 2001 From: passengerZ <904806153@qq.com> Date: Thu, 2 Nov 2023 00:51:23 -0700 Subject: [PATCH 6/8] change the tool URL --- benchexec/tools/fdse.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/benchexec/tools/fdse.py b/benchexec/tools/fdse.py index ed801655b..a991e39da 100755 --- a/benchexec/tools/fdse.py +++ b/benchexec/tools/fdse.py @@ -12,7 +12,7 @@ class Tool(benchexec.tools.template.BaseTool2): """ Tool info for FDSE. - https://github.com/zbchen/FDSE (now is private) + https://github.com/passengerZ/FDSE """ def executable(self, tool_locator): From 783112c35c6db382c1a29ebcdce3a19d99e02475 Mon Sep 17 00:00:00 2001 From: passengerZ <904806153@qq.com> Date: Mon, 6 Nov 2023 00:35:01 -0800 Subject: [PATCH 7/8] FDSE: adjust output result --- benchexec/tools/fdse.py | 19 ++++++------------- 1 file changed, 6 insertions(+), 13 deletions(-) diff --git a/benchexec/tools/fdse.py b/benchexec/tools/fdse.py index a991e39da..8d74988e4 100755 --- a/benchexec/tools/fdse.py +++ b/benchexec/tools/fdse.py @@ -35,16 +35,9 @@ def name(self): return "FDSE" def determine_result(self, run): - for line in run.output: - if "[BUG]" in line: - if "ASSERTION FAIL!" in line: - return result.RESULT_FALSE_REACH - elif "Index out-of-bound" in line: - return result.RESULT_FALSE_DEREF - elif "overflow" in line: - return result.RESULT_FALSE_OVERFLOW - else: - return result.RESULT_ERROR - if "Done : End analysis" in line: - return result.RESULT_DONE - return result.RESULT_UNKNOWN + status = result.RESULT_UNKNOWN + + if run.output.any_line_contains("Done : End analysis"): + status = result.RESULT_DONE + + return status From bab344493c0342d335b1eb29725fb97d5e5a381c Mon Sep 17 00:00:00 2001 From: passengerZ <904806153@qq.com> Date: Mon, 6 Nov 2023 04:08:51 -0800 Subject: [PATCH 8/8] adjust output type --- benchexec/tools/fdse.py | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/benchexec/tools/fdse.py b/benchexec/tools/fdse.py index 8d74988e4..81dd8ce62 100755 --- a/benchexec/tools/fdse.py +++ b/benchexec/tools/fdse.py @@ -35,9 +35,12 @@ def name(self): return "FDSE" def determine_result(self, run): - status = result.RESULT_UNKNOWN + status = result.RESULT_ERROR - if run.output.any_line_contains("Done : End analysis"): - status = result.RESULT_DONE + for line in run.output: + if "Done : End analysis" in line: + status = result.RESULT_DONE + elif "HaltTimer invoked!!!" in line: + status = result.RESULT_TIMEOUT return status