From bb3b539fd5d57a80e30fb936435a9469ac71f152 Mon Sep 17 00:00:00 2001 From: Arpita Dutta Date: Thu, 2 Nov 2023 21:41:37 +0800 Subject: [PATCH 1/2] pushed files for TracerX-Del and TracerX-WP --- benchexec/tools/tracerx-wp.py | 92 +++++++++++++++++++++++++++++++++++ benchexec/tools/tracerx.py | 2 +- 2 files changed, 93 insertions(+), 1 deletion(-) create mode 100644 benchexec/tools/tracerx-wp.py diff --git a/benchexec/tools/tracerx-wp.py b/benchexec/tools/tracerx-wp.py new file mode 100644 index 000000000..3e616c597 --- /dev/null +++ b/benchexec/tools/tracerx-wp.py @@ -0,0 +1,92 @@ +# 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 + + +class Tool(benchexec.tools.template.BaseTool2): + """ + Tool info for Tracer-X (https://www.comp.nus.edu.sg/~tracerx/). + """ + + def executable(self, tool_locator): + return tool_locator.find_executable("tracerx-wp", subdir="bin") + + def program_files(self, executable): + return self._program_files_from_executable( + executable, self.REQUIRED_PATHS, parent_dir=True + ) + + def version(self, executable): + """ + The output looks like this: + Tracer-X 0.2.0 (https://www.comp.nus.edu.sg/~tracerx/) + Built August 19 2019 + Build mode: Release + Build revision: 60794e3eac58744548657500e425241b57f4bdb7 + LLVM (http://llvm.org/): + LLVM version 3.4.2 + Optimized build. + Built Oct 15 2014 (13:57:47). + Default target: x86_64-pc-linux-gnu + Host CPU: bdver1 + """ + version = self._version_from_tool(executable, line_prefix="KLEE") + return version.split("(")[0].strip() + + def cmdline(self, executable, options, task, rlimits): + if task.property_file: + options += [f"--property-file={task.property_file}"] + if rlimits.memory: + options += [f"--max-memory={rlimits.memory}"] + if rlimits.cputime: + options += [f"--max-cputime-soft={rlimits.cputime}"] + + 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] + + return [executable] + options + list(task.input_files_or_identifier) + + def name(self): + return "TracerX-WP" + + 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 line.startswith("KLEE: ERROR: "): + if "ASSERTION FAIL:" in line: + return result.RESULT_FALSE_REACH + elif "memory error: out of bound pointer" in line: + return result.RESULT_FALSE_DEREF + elif "overflow" in line: + return result.RESULT_FALSE_OVERFLOW + else: + return f"ERROR ({run.exit_code.value})" + if line.startswith("KLEE: done"): + return result.RESULT_DONE + return result.RESULT_UNKNOWN + + def get_value_from_output(self, lines, identifier): + # search for the text in output and get its value, + # stop after the first line, that contains the searched text + for line in lines: + if line.startswith("KLEE: done: ") and line.find(identifier + " = ") != -1: + splittedLine = line.split(" = ") + return splittedLine[1].strip() + return None diff --git a/benchexec/tools/tracerx.py b/benchexec/tools/tracerx.py index 97cb9e149..3b0d6c4ce 100644 --- a/benchexec/tools/tracerx.py +++ b/benchexec/tools/tracerx.py @@ -56,7 +56,7 @@ def cmdline(self, executable, options, task, rlimits): return [executable] + options + list(task.input_files_or_identifier) def name(self): - return "Tracer-X" + return "TracerX-Del" def determine_result(self, run): """ From 18cd9639c8bdf039fa3260fbd15bd8d227056589 Mon Sep 17 00:00:00 2001 From: Arpita Dutta Date: Sat, 4 Nov 2023 08:31:30 +0800 Subject: [PATCH 2/2] updated tracerx-wp.py using inherited code from tracerx.py --- benchexec/tools/tracerx-wp.py | 78 ++--------------------------------- 1 file changed, 3 insertions(+), 75 deletions(-) diff --git a/benchexec/tools/tracerx-wp.py b/benchexec/tools/tracerx-wp.py index 3e616c597..f8b14693a 100644 --- a/benchexec/tools/tracerx-wp.py +++ b/benchexec/tools/tracerx-wp.py @@ -5,88 +5,16 @@ # # 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.tools.tracerx as tracerx -class Tool(benchexec.tools.template.BaseTool2): +class Tool(tracerx.Tool): """ - Tool info for Tracer-X (https://www.comp.nus.edu.sg/~tracerx/). + Tool info for TracerX-WP (https://www.comp.nus.edu.sg/~tracerx/). """ def executable(self, tool_locator): return tool_locator.find_executable("tracerx-wp", subdir="bin") - def program_files(self, executable): - return self._program_files_from_executable( - executable, self.REQUIRED_PATHS, parent_dir=True - ) - - def version(self, executable): - """ - The output looks like this: - Tracer-X 0.2.0 (https://www.comp.nus.edu.sg/~tracerx/) - Built August 19 2019 - Build mode: Release - Build revision: 60794e3eac58744548657500e425241b57f4bdb7 - LLVM (http://llvm.org/): - LLVM version 3.4.2 - Optimized build. - Built Oct 15 2014 (13:57:47). - Default target: x86_64-pc-linux-gnu - Host CPU: bdver1 - """ - version = self._version_from_tool(executable, line_prefix="KLEE") - return version.split("(")[0].strip() - - def cmdline(self, executable, options, task, rlimits): - if task.property_file: - options += [f"--property-file={task.property_file}"] - if rlimits.memory: - options += [f"--max-memory={rlimits.memory}"] - if rlimits.cputime: - options += [f"--max-cputime-soft={rlimits.cputime}"] - - 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] - - return [executable] + options + list(task.input_files_or_identifier) - def name(self): return "TracerX-WP" - - 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 line.startswith("KLEE: ERROR: "): - if "ASSERTION FAIL:" in line: - return result.RESULT_FALSE_REACH - elif "memory error: out of bound pointer" in line: - return result.RESULT_FALSE_DEREF - elif "overflow" in line: - return result.RESULT_FALSE_OVERFLOW - else: - return f"ERROR ({run.exit_code.value})" - if line.startswith("KLEE: done"): - return result.RESULT_DONE - return result.RESULT_UNKNOWN - - def get_value_from_output(self, lines, identifier): - # search for the text in output and get its value, - # stop after the first line, that contains the searched text - for line in lines: - if line.startswith("KLEE: done: ") and line.find(identifier + " = ") != -1: - splittedLine = line.split(" = ") - return splittedLine[1].strip() - return None