Merge pull request #1133 from Po-Chun-Chien/add-moxi-tools

Add tool-info modules for MoXI model checkers

benchexec/tools/moxi-mc-flow.py

@@ -0,0 +1,56 @@
+# 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
+
+import benchexec.result as result
+import benchexec.tools.template
+
+
+class Tool(benchexec.tools.template.BaseTool2):
+    """
+    Tool info for MoXI-MC-Flow
+    """
+
+    REQUIRED_PATHS = [
+        "deps/",
+        "src/",
+        "json-schema/",
+        "sortcheck.py",
+        "translate.py",
+    ]
+
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("modelcheck.py")
+
+    def name(self):
+        return "MoXI-MC-Flow"
+
+    def project_url(self):
+        return "https://github.com/ModelChecker/moxi-mc-flow"
+
+    def cmdline(self, executable, options, task, rlimits):
+        if rlimits.cputime and "--timeout" not in options:
+            # The `--timeout` parameter must be passed to the tool
+            # to prevent it from using its default value,
+            # which could be shorter than the limit set by BenchExec
+            # and cause early termination.
+            # Moreover, in practice the tool sometimes terminates itself prematurely
+            # even when the exact time limit is passed.
+            # To prevent this and ensure the tool utilizes the full time limit,
+            # a factor of 2 is applied to the timeout value.
+            options += ["--timeout", str(rlimits.cputime * 2)]
+        return ["python3", executable, task.single_input_file, *options]
+
+    def determine_result(self, run):
+        """
+        @return: verification result obtained from MoXI-MC-Flow
+        """
+        for line in run.output[::-1]:
+            if line.startswith("unsat"):
+                return result.RESULT_TRUE_PROP
+            if line.startswith("sat"):
+                return result.RESULT_FALSE_PROP
+        return result.RESULT_ERROR

benchexec/tools/moxichecker.py

@@ -0,0 +1,46 @@
+# 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
+
+import benchexec.result as result
+import benchexec.tools.template
+
+
+class Tool(benchexec.tools.template.BaseTool2):
+    """
+    Tool info for MoXIchecker
+    """
+
+    REQUIRED_PATHS = ["moxichecker/", "lib/"]
+
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("moxichecker", subdir="bin")
+
+    def name(self):
+        return "MoXIchecker"
+
+    def project_url(self):
+        return "https://gitlab.com/sosy-lab/software/moxichecker"
+
+    def version(self, executable):
+        return self._version_from_tool(executable)
+
+    def program_files(self, executable):
+        return [executable] + self._program_files_from_executable(
+            executable, self.REQUIRED_PATHS, parent_dir=True
+        )
+
+    def cmdline(self, executable, options, task, rlimits):
+        return [executable, *options, task.single_input_file]
+
+    def determine_result(self, run):
+        for line in run.output[::-1]:
+            if line.startswith("[INFO] Model-checking result:"):
+                if "UNREACHABLE" in line:
+                    return result.RESULT_TRUE_PROP
+                if "REACHABLE" in line:
+                    return result.RESULT_FALSE_PROP
+        return result.RESULT_ERROR