Skip to content

Commit

Permalink
updated tracerx-wp.py using inherited code from tracerx.py
Browse files Browse the repository at this point in the history
  • Loading branch information
ArpitaDutta committed Nov 4, 2023
1 parent bb3b539 commit 18cd963
Showing 1 changed file with 3 additions and 75 deletions.
78 changes: 3 additions & 75 deletions benchexec/tools/tracerx-wp.py
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 18cd963

Please sign in to comment.