From a0edc1205bace14e7303aab00645e010f4c46df4 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Fri, 12 Jul 2024 20:38:12 +0200 Subject: [PATCH 1/8] Create a tool-info module for MoXI-MC-Flow --- benchexec/tools/moxi-mc-flow.py | 51 +++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 benchexec/tools/moxi-mc-flow.py diff --git a/benchexec/tools/moxi-mc-flow.py b/benchexec/tools/moxi-mc-flow.py new file mode 100644 index 000000000..a83cedc12 --- /dev/null +++ b/benchexec/tools/moxi-mc-flow.py @@ -0,0 +1,51 @@ +# 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 + + +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 program_files(self, executable): + return self._program_files_from_executable(executable, self.REQUIRED_PATHS) + + def cmdline(self, executable, options, task, rlimits): + if rlimits.cputime and "--timeout" not in options: + options += ["--timeout", str(rlimits.cputime)] + return ["python3", executable, *options, task.single_input_file] + + 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 From 6fb44c1264af4d147ebe51d8ec023e31dc538213 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Fri, 12 Jul 2024 20:45:03 +0200 Subject: [PATCH 2/8] Add a tool-info module for MoXIchecker --- benchexec/tools/moxichecker.py | 46 ++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 benchexec/tools/moxichecker.py diff --git a/benchexec/tools/moxichecker.py b/benchexec/tools/moxichecker.py new file mode 100644 index 000000000..06fc12a65 --- /dev/null +++ b/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 +# +# 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/"] + + 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 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 From ded94a46ae9a40e0fc24c24ef67bf9c2e677d556 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Sun, 14 Jul 2024 11:28:37 +0200 Subject: [PATCH 3/8] Reorder command-line arguments for MoXI-MC-Flow - task first, then options --- benchexec/tools/moxi-mc-flow.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/benchexec/tools/moxi-mc-flow.py b/benchexec/tools/moxi-mc-flow.py index a83cedc12..cb4aa2e15 100644 --- a/benchexec/tools/moxi-mc-flow.py +++ b/benchexec/tools/moxi-mc-flow.py @@ -37,7 +37,7 @@ def program_files(self, executable): def cmdline(self, executable, options, task, rlimits): if rlimits.cputime and "--timeout" not in options: options += ["--timeout", str(rlimits.cputime)] - return ["python3", executable, *options, task.single_input_file] + return ["python3", executable, task.single_input_file, *options] def determine_result(self, run): """ From 288d86b633df26fcbdfc972738b56a336f942edf Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Tue, 16 Jul 2024 15:19:13 +0200 Subject: [PATCH 4/8] Add 5% more runtime to MoXI-MC-Flow's time-limit option - otherwise it usually kills the underlying model checker before actually reaching the time limit --- benchexec/tools/moxi-mc-flow.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/benchexec/tools/moxi-mc-flow.py b/benchexec/tools/moxi-mc-flow.py index cb4aa2e15..f4f3b0c92 100644 --- a/benchexec/tools/moxi-mc-flow.py +++ b/benchexec/tools/moxi-mc-flow.py @@ -7,6 +7,7 @@ import benchexec.result as result import benchexec.tools.template +from math import ceil class Tool(benchexec.tools.template.BaseTool2): @@ -36,7 +37,7 @@ def program_files(self, executable): def cmdline(self, executable, options, task, rlimits): if rlimits.cputime and "--timeout" not in options: - options += ["--timeout", str(rlimits.cputime)] + options += ["--timeout", str(ceil(rlimits.cputime * 1.05))] return ["python3", executable, task.single_input_file, *options] def determine_result(self, run): From c35f6adb7064305712e93f816b26982e2249dfa3 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Wed, 4 Dec 2024 13:32:40 +0100 Subject: [PATCH 5/8] Add lib/ to MoXIchecker's required paths --- benchexec/tools/moxichecker.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/benchexec/tools/moxichecker.py b/benchexec/tools/moxichecker.py index 06fc12a65..0764f511f 100644 --- a/benchexec/tools/moxichecker.py +++ b/benchexec/tools/moxichecker.py @@ -14,7 +14,7 @@ class Tool(benchexec.tools.template.BaseTool2): Tool info for MoXIchecker """ - REQUIRED_PATHS = ["moxichecker/"] + REQUIRED_PATHS = ["moxichecker/", "lib/"] def executable(self, tool_locator): return tool_locator.find_executable("moxichecker", subdir="bin") From e1fee24061e5502be6831348347e5be977af96a3 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Thu, 5 Dec 2024 17:12:36 +0100 Subject: [PATCH 6/8] Refine the collections of required program files for MoXI model checkers --- benchexec/tools/moxi-mc-flow.py | 3 --- benchexec/tools/moxichecker.py | 2 +- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/benchexec/tools/moxi-mc-flow.py b/benchexec/tools/moxi-mc-flow.py index f4f3b0c92..ce29d226d 100644 --- a/benchexec/tools/moxi-mc-flow.py +++ b/benchexec/tools/moxi-mc-flow.py @@ -32,9 +32,6 @@ def name(self): def project_url(self): return "https://github.com/ModelChecker/moxi-mc-flow" - def program_files(self, executable): - return self._program_files_from_executable(executable, self.REQUIRED_PATHS) - def cmdline(self, executable, options, task, rlimits): if rlimits.cputime and "--timeout" not in options: options += ["--timeout", str(ceil(rlimits.cputime * 1.05))] diff --git a/benchexec/tools/moxichecker.py b/benchexec/tools/moxichecker.py index 0764f511f..11621f37d 100644 --- a/benchexec/tools/moxichecker.py +++ b/benchexec/tools/moxichecker.py @@ -29,7 +29,7 @@ def version(self, executable): return self._version_from_tool(executable) def program_files(self, executable): - return self._program_files_from_executable( + return [executable] + self._program_files_from_executable( executable, self.REQUIRED_PATHS, parent_dir=True ) From bac42d573a0826e58630bb9e1fcbf79a5b883457 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Thu, 5 Dec 2024 18:05:43 +0100 Subject: [PATCH 7/8] Increase the timeout value passed to MoXI-MC-Flow and add explanation as comments --- benchexec/tools/moxi-mc-flow.py | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/benchexec/tools/moxi-mc-flow.py b/benchexec/tools/moxi-mc-flow.py index ce29d226d..1cafeafa5 100644 --- a/benchexec/tools/moxi-mc-flow.py +++ b/benchexec/tools/moxi-mc-flow.py @@ -34,7 +34,15 @@ def project_url(self): def cmdline(self, executable, options, task, rlimits): if rlimits.cputime and "--timeout" not in options: - options += ["--timeout", str(ceil(rlimits.cputime * 1.05))] + # 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): From e04800a471d6747713241750b2215862ae3d8468 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Thu, 5 Dec 2024 18:07:43 +0100 Subject: [PATCH 8/8] Remove an unused import --- benchexec/tools/moxi-mc-flow.py | 1 - 1 file changed, 1 deletion(-) diff --git a/benchexec/tools/moxi-mc-flow.py b/benchexec/tools/moxi-mc-flow.py index 1cafeafa5..97d133c44 100644 --- a/benchexec/tools/moxi-mc-flow.py +++ b/benchexec/tools/moxi-mc-flow.py @@ -7,7 +7,6 @@ import benchexec.result as result import benchexec.tools.template -from math import ceil class Tool(benchexec.tools.template.BaseTool2):