Merge pull request #646 from sosy-lab/TI-update-to-BaseTool2-verifiers

benchexec/tools/brick.py

@@ -5,27 +5,31 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
+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.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Tool info for BRICK
     https://github.com/brick-tool-dev/brick-tool
     """
 
     REQUIRED_PATHS = ["bin", "lib"]
 
-    def executable(self):
-        return util.find_executable("bin/brick")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("brick", subdir="bin")
 
     def name(self):
         return "BRICK"
 
-    def cmdline(self, executable, options, tasks, propertyfile, rlimits):
-        return [executable] + options + tasks
+    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 data_model_param not in options:
+            options += [data_model_param]
+
+        return [executable] + options + list(task.input_files_or_identifier)
 
     def version(self, executable):
         return self._version_from_tool(executable, arg="--version")
@@ -36,20 +40,17 @@ def program_files(self, executable):
             executable, paths, parent_dir=True
         )
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def determine_result(self, run):
         status = result.RESULT_ERROR
 
-        for line in output:
-            if line == "VERIFICATION SUCCESSFUL\n":
+        for line in run.output:
+            if line == "VERIFICATION SUCCESSFUL":
                 status = result.RESULT_TRUE_PROP
                 break
-            elif line == "VERIFICATION FAILED\n":
+            elif line == "VERIFICATION FAILED":
                 status = result.RESULT_FALSE_REACH
                 break
-            elif (
-                line == "VERIFICATION UNKNOWN\n"
-                or line == "VERIFICATION BOUNDED TRUE\n"
-            ):
+            elif line == "VERIFICATION UNKNOWN" or line == "VERIFICATION BOUNDED TRUE":
                 status = result.RESULT_UNKNOWN
                 break
 

benchexec/tools/cbmc.py

@@ -8,12 +8,12 @@
 import logging
 from xml.etree import ElementTree
 
-import benchexec.util as util
+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.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Tool info for CBMC (http://www.cprover.org/cbmc/).
     It always adds --xml-ui to the command-line arguments for easier parsing of
@@ -23,26 +23,30 @@ class Tool(benchexec.tools.template.BaseTool):
 
     REQUIRED_PATHS = ["cbmc", "cbmc-binary", "goto-cc"]
 
-    def executable(self):
-        return util.find_executable("cbmc")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("cbmc")
 
     def version(self, executable):
         return self._version_from_tool(executable)
 
     def name(self):
         return "CBMC"
 
-    def cmdline(self, executable, options, tasks, propertyfile, rlimits):
-        if propertyfile:
-            options = options + ["--propertyfile", propertyfile]
+    def cmdline(self, executable, options, task, rlimits):
+        if task.property_file:
+            options = options + ["--propertyfile", task.property_file]
         elif "--xml-ui" not in options:
             options = options + ["--xml-ui"]
 
+        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 + tasks
+        return [executable] + options + list(task.input_files_or_identifier)
 
-    def parse_XML(self, output, returncode, isTimeout):
+    def parse_XML(self, output, exit_code, isTimeout):
         # an empty tag cannot be parsed into a tree
         def sanitizeXML(s):
             return s.replace("<>", "<emptyTag>").replace("</>", "</emptyTag>")
@@ -72,7 +76,7 @@ def isErrorMessage(msg):
                     status = "INVALID OUTPUT"
 
             elif status == "FAILURE":
-                assert returncode == 10
+                assert exit_code.value == 10
                 reason = tree.find("goto_trace").find("failure").findtext("reason")
                 if not reason:
                     reason = tree.find("goto_trace").find("failure").get("reason")
@@ -82,7 +86,7 @@ def isErrorMessage(msg):
                     status = result.RESULT_FALSE_REACH
 
             elif status == "SUCCESS":
-                assert returncode == 0
+                assert exit_code.value == 0
                 if "--unwinding-assertions" in self.options:
                     status = result.RESULT_TRUE_PROP
                 else:
@@ -97,17 +101,18 @@ def isErrorMessage(msg):
             else:
                 status = "INVALID OUTPUT"
                 logging.exception(
-                    "Error parsing CBMC output for returncode %d", returncode
+                    "Error parsing CBMC output for exit_code.value %d", exit_code.value
                 )
 
         return status
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def determine_result(self, run):
+        output = run.output
 
-        if returnsignal == 0 and ((returncode == 0) or (returncode == 10)):
+        if run.exit_code.value in [0, 10]:
             status = result.RESULT_ERROR
             if "--xml-ui" in self.options:
-                status = self.parse_XML(output, returncode, isTimeout)
+                status = self.parse_XML(output, run.exit_code, run.was_timeout)
             elif len(output) > 0:
                 # SV-COMP mode
                 result_str = output[-1].strip()
@@ -130,13 +135,13 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
                 elif "UNKNOWN" in output:
                     status = result.RESULT_UNKNOWN
 
-        elif returncode == 64 and "Usage error!\n" in output:
+        elif run.exit_code.value == 64 and "Usage error!" in output:
             status = "INVALID ARGUMENTS"
 
-        elif returncode == 6 and "Out of memory\n" in output:
+        elif run.exit_code.value == 6 and "Out of memory" in output:
             status = "OUT OF MEMORY"
 
-        elif returncode == 6 and "SAT checker ran out of memory\n" in output:
+        elif run.exit_code.value == 6 and "SAT checker ran out of memory" in output:
             status = "OUT OF MEMORY"
 
         else:

benchexec/tools/cseq.py

@@ -9,7 +9,7 @@
 import benchexec.result as result
 
 
-class CSeqTool(benchexec.tools.template.BaseTool):
+class CSeqTool(benchexec.tools.template.BaseTool2):
     """
     Abstract tool info for CSeq-based tools (http://users.ecs.soton.ac.uk/gp4/cseq/cseq.html).
     """
@@ -19,7 +19,7 @@ def version(self, executable):
         first_line = output.splitlines()[0]
         return first_line.strip()
 
-    def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
+    def cmdline(self, executable, options, task, rlimits):
         """
         Compose the command line to execute from the name of the executable,
         the user-specified options, and the inputfile to analyze.
@@ -29,24 +29,20 @@ def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
         are either absolute or have been made relative to the designated working directory.
         @param executable: the path to the executable of the tool (typically the result of executable())
         @param options: a list of options, in the same order as given in the XML-file.
-        @param tasks: a list of tasks, that should be analysed with the tool in one run.
-                            In most cases we we have only _one_ inputfile.
-        @param propertyfile: contains a specification for the verifier.
+        @param task: instance of class Task containg the property and input file
+                            This tool info module only supports one input file.
         @param rlimits: This dictionary contains resource-limits for a run,
                         for example: time-limit, soft-time-limit, hard-time-limit, memory-limit, cpu-core-limit.
                         All entries in rlimits are optional, so check for existence before usage!
         """
-        assert len(tasks) == 1, "only one inputfile supported"
-        inputfile = ["--input", tasks[0]]
-        spec = ["--spec", propertyfile] if propertyfile is not None else []
-        return [executable] + options + spec + inputfile
+        spec = ["--spec", task.property_file] if task.property_file else []
+        return [executable] + options + spec + ["--input", task.single_input_file]
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
-        output = "\n".join(output)
+    def determine_result(self, run):
         status = result.RESULT_UNKNOWN
-        if "FALSE" in output:
+        if run.output.any_line_contains("FALSE"):
             status = result.RESULT_FALSE_REACH
-        elif "TRUE" in output:
+        elif run.output.any_line_contains("TRUE"):
             status = result.RESULT_TRUE_PROP
         else:
             status = result.RESULT_UNKNOWN

benchexec/tools/dartagnan.py

@@ -5,12 +5,11 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
 import benchexec.tools.template
 import benchexec.result as result
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Tool info for Dartagnan (https://github.com/hernanponcedeleon/Dat3M).
     """
@@ -24,22 +23,22 @@ class Tool(benchexec.tools.template.BaseTool):
         "output",
     ]
 
-    def executable(self):
-        return util.find_executable("./Dartagnan-SVCOMP.sh")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("Dartagnan-SVCOMP.sh")
 
     def name(self):
         return "Dartagnan"
 
-    def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
-        return [executable] + options + tasks
+    def cmdline(self, executable, options, task, rlimits):
+        return [executable] + options + list(task.input_files_or_identifier)
 
     def version(self, executable):
         return self._version_from_tool(executable)
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def determine_result(self, run):
         status = result.RESULT_ERROR
-        if output:
-            result_str = output[-1].strip()
+        if run.output:
+            result_str = run.output[-1].strip()
             if "FAIL" in result_str:
                 status = result.RESULT_FALSE_REACH
             elif "PASS" in result_str:

benchexec/tools/divine.py

@@ -5,14 +5,14 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 import benchexec.tools.template
 import benchexec.result as result
 
 import os
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     DIVINE info object
     """
@@ -33,14 +33,14 @@ class Tool(benchexec.tools.template.BaseTool):
         "libz.so.1",
     ]
 
-    def executable(self):
+    def executable(self, tool_locator):
         """
         Find the path to the executable file that will get executed.
         This method always needs to be overridden,
         and most implementations will look similar to this one.
         The path returned should be relative to the current directory.
         """
-        return util.find_executable(self.BINS[0], os.path.join("bin", self.BINS[0]))
+        return tool_locator.find_executable(self.BINS[0], subdir="bin")
 
     def version(self, executable):
         return self._version_from_tool(executable)
@@ -51,7 +51,7 @@ def name(self):
         """
         return "DIVINE"
 
-    def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
+    def cmdline(self, executable, options, task, rlimits):
         """
         Compose the command line to execute from the name of the executable,
         the user-specified options, and the inputfile to analyze.
@@ -70,13 +70,21 @@ def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
                         for example: time-limit, soft-time-limit, hard-time-limit, memory-limit, cpu-core-limit.
                         All entries in rlimits are optional, so check for existence before usage!
         """
+        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]
+
         directory = os.path.dirname(executable)
 
         # Ignore propertyfile since we run only reachability
-        run = [os.path.join(".", directory, self.BINS[1]), directory] + options + tasks
+        run = (
+            [os.path.join(".", directory, self.BINS[1]), directory]
+            + options
+            + list(task.input_files_or_identifier)
+        )
         return run
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def determine_result(self, run):
         """
         Parse the output of the tool and extract the verification result.
         This method always needs to be overridden.
@@ -86,21 +94,18 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
         and should give some indication of the failure reason
         (e.g., "CRASH", "OUT_OF_MEMORY", etc.).
         """
-
-        if not output:
+        if not run.output:
             return "ERROR - no output"
 
-        last = output[-1]
+        last = run.output[-1]
 
-        if isTimeout:
+        if run.was_timeout:
             return "TIMEOUT"
 
-        if returncode != 0:
+        if run.exit_code.value and run.exit_code.value != 0:
             return "ERROR - Pre-run"
 
-        if last is None:
-            return "ERROR - no output"
-        elif "result: true" in last:
+        if "result: true" in last:
             return result.RESULT_TRUE_PROP
         elif "result: false" in last:
             return result.RESULT_FALSE_REACH