From 693ef5ac0964d24fea1947309e1643d199bf8a57 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Wed, 1 Nov 2023 15:21:03 +0100 Subject: [PATCH 1/5] Collect version information of ABC --- benchexec/tools/abc.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/benchexec/tools/abc.py b/benchexec/tools/abc.py index 2af3f974f..1f61dc1c7 100644 --- a/benchexec/tools/abc.py +++ b/benchexec/tools/abc.py @@ -24,6 +24,11 @@ def executable(self, tool_locator): def name(self): return "ABC" + def version(self, executable): + return self._version_from_tool( + executable, arg="-q version", line_prefix="UC Berkeley, ABC" + ) + def cmdline(self, executable, options, task, rlimits): # The default read method in ABC cannot process uninitialized registers properly. # Therefore, a new read method `&r` (`&read`) is invoked here. From 4072488312420ad51b011afa67a1ec7ca815fa0c Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Wed, 1 Nov 2023 15:31:49 +0100 Subject: [PATCH 2/5] Add required paths for ABC and AVR --- benchexec/tools/abc.py | 7 +++++++ benchexec/tools/avr.py | 2 ++ 2 files changed, 9 insertions(+) diff --git a/benchexec/tools/abc.py b/benchexec/tools/abc.py index 1f61dc1c7..57a694dcd 100644 --- a/benchexec/tools/abc.py +++ b/benchexec/tools/abc.py @@ -18,6 +18,8 @@ class Tool(benchexec.tools.template.BaseTool2): URL: https://people.eecs.berkeley.edu/~alanmi/abc/ """ + REQUIRED_PATHS = ["bin/", "abc.rc"] + def executable(self, tool_locator): return tool_locator.find_executable("abc", subdir="bin") @@ -29,6 +31,11 @@ def version(self, executable): executable, arg="-q version", line_prefix="UC Berkeley, ABC" ) + 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): # The default read method in ABC cannot process uninitialized registers properly. # Therefore, a new read method `&r` (`&read`) is invoked here. diff --git a/benchexec/tools/avr.py b/benchexec/tools/avr.py index b5aeaaed2..350f8155a 100644 --- a/benchexec/tools/avr.py +++ b/benchexec/tools/avr.py @@ -15,6 +15,8 @@ class Tool(benchexec.tools.template.BaseTool2): URL: https://github.com/aman-goel/avr """ + REQUIRED_PATHS = ["build/"] + def executable(self, tool_locator): return tool_locator.find_executable("avr.py") From 267e03709fdabbf0d1a5c8117f32bb774422823b Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Wed, 1 Nov 2023 15:39:29 +0100 Subject: [PATCH 3/5] Pass resource limits to AVR command lines --- benchexec/tools/avr.py | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/benchexec/tools/avr.py b/benchexec/tools/avr.py index 350f8155a..7565d28d4 100644 --- a/benchexec/tools/avr.py +++ b/benchexec/tools/avr.py @@ -24,6 +24,12 @@ def name(self): return "AVR" def cmdline(self, executable, options, task, rlimits): + from math import ceil + + if rlimits.cputime and "--timeout" not in options: + options += ["--timeout", str(rlimits.cputime)] + if rlimits.memory and "--memout" not in options: + options += ["--memout", str(ceil(rlimits.memory / 1000000.0))] return [executable] + options + [task.single_input_file] def determine_result(self, run): From 61b379ba198ee3828e92e22fe994d28f9264b63a Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Wed, 1 Nov 2023 15:44:02 +0100 Subject: [PATCH 4/5] Parse results from console logs backward - verification results are usually printed at the last line of an execution log --- benchexec/tools/abc.py | 2 +- benchexec/tools/avr.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/benchexec/tools/abc.py b/benchexec/tools/abc.py index 57a694dcd..c00c013a4 100644 --- a/benchexec/tools/abc.py +++ b/benchexec/tools/abc.py @@ -51,7 +51,7 @@ def determine_result(self, run): """ if run.was_timeout: return result.RESULT_TIMEOUT - for line in run.output: + for line in run.output[::-1]: if line.startswith("Property proved") or line.startswith( "Networks are equivalent" ): diff --git a/benchexec/tools/avr.py b/benchexec/tools/avr.py index 7565d28d4..a19510efb 100644 --- a/benchexec/tools/avr.py +++ b/benchexec/tools/avr.py @@ -38,7 +38,7 @@ def determine_result(self, run): """ if run.was_timeout: return result.RESULT_TIMEOUT - for line in run.output: + for line in run.output[::-1]: # skip the lines that do not contain verification result if not line.startswith("Verification result:"): continue From a37525be1aa2bf96c56d70b7263e80cdea16908c Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Thu, 2 Nov 2023 11:46:09 +0100 Subject: [PATCH 5/5] Refactor import --- benchexec/tools/avr.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/benchexec/tools/avr.py b/benchexec/tools/avr.py index a19510efb..01c5bd35a 100644 --- a/benchexec/tools/avr.py +++ b/benchexec/tools/avr.py @@ -7,6 +7,7 @@ import benchexec.result as result import benchexec.tools.template +from math import ceil class Tool(benchexec.tools.template.BaseTool2): @@ -24,8 +25,6 @@ def name(self): return "AVR" def cmdline(self, executable, options, task, rlimits): - from math import ceil - if rlimits.cputime and "--timeout" not in options: options += ["--timeout", str(rlimits.cputime)] if rlimits.memory and "--memout" not in options: