Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proton tool info module proton.py #952

Merged
merged 9 commits into from
Nov 3, 2023
70 changes: 70 additions & 0 deletions benchexec/tools/proton.py
Original file line number Diff line number Diff line change
@@ -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 <https://www.sosy-lab.org>
#
# 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
PhilippWendler marked this conversation as resolved.
Show resolved Hide resolved
"""

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
PhilippWendler marked this conversation as resolved.
Show resolved Hide resolved

return [executable] + options + list(task.input_files_or_identifier)
PhilippWendler marked this conversation as resolved.
Show resolved Hide resolved

def determine_result(self, run):
output = run.output

if run.exit_code.value in [0, 10]:
status = result.RESULT_ERROR
if len(output) > 0:
PhilippWendler marked this conversation as resolved.
Show resolved Hide resolved
# 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:
PhilippWendler marked this conversation as resolved.
Show resolved Hide resolved
status = "OUT OF MEMORY"

elif run.exit_code.value == 6:
status = "OUT-OF-MEMORY or INTERNAL-ERROR"

else:
status = result.RESULT_ERROR

return status
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not have a return everywhere instead of the status variable? Seems easier to follow that way.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems this was overlooked?