From cf70848ebb264f6b102f8a9d8ac4fee42032129c Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Fri, 7 Jun 2024 12:07:13 +0200 Subject: [PATCH 01/33] Update SeaHorn's executable paths --- benchexec/tools/seahorn.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/benchexec/tools/seahorn.py b/benchexec/tools/seahorn.py index ae2670304..0c09e9b2a 100644 --- a/benchexec/tools/seahorn.py +++ b/benchexec/tools/seahorn.py @@ -17,10 +17,10 @@ class Tool(benchexec.tools.template.BaseTool): - REQUIRED_PATHS = ["bin", "include", "lib", "share"] + REQUIRED_PATHS = ["bin", "crab", "include", "lib", "share"] - def executable(self): - return util.find_executable("sea_svcomp", os.path.join("bin", "sea_svcomp")) + def executable(self, tool_locator): + return tool_locator.find_executable("sea", subdir="bin") def program_files(self, executable): return self._program_files_from_executable( From 7e799a90cb320cbbe9651cd5cb9885f3f837b356 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Fri, 7 Jun 2024 12:08:14 +0200 Subject: [PATCH 02/33] Update name and add project URL of SeaHorn --- benchexec/tools/seahorn.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/benchexec/tools/seahorn.py b/benchexec/tools/seahorn.py index 0c09e9b2a..bebe08fdf 100644 --- a/benchexec/tools/seahorn.py +++ b/benchexec/tools/seahorn.py @@ -28,7 +28,10 @@ def program_files(self, executable): ) def name(self): - return "SeaHorn-F16" + return "SeaHorn" + + def project_url(self): + return "https://github.com/seahorn/seahorn" def cmdline(self, executable, options, tasks, propertyfile, rlimits): assert len(tasks) == 1 From 9cabfc9045122564a533472866b2616d91f2c6fc Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Fri, 7 Jun 2024 12:13:50 +0200 Subject: [PATCH 03/33] Get version from SeaHorn 14 The wrapper script (executable) of SeaHorn `sea` does not support `--version`, but the binary `seahorn` does. --- benchexec/tools/seahorn.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/benchexec/tools/seahorn.py b/benchexec/tools/seahorn.py index bebe08fdf..a91bed329 100644 --- a/benchexec/tools/seahorn.py +++ b/benchexec/tools/seahorn.py @@ -40,7 +40,9 @@ def cmdline(self, executable, options, tasks, propertyfile, rlimits): return [executable] + options + spec + tasks def version(self, executable): - return self._version_from_tool(executable) + return self._version_from_tool( + f"{str(executable)}horn", line_prefix=" SeaHorn version" + ) def determine_result(self, returncode, returnsignal, output, isTimeout): output = "\n".join(output) From 925d4e2cf0f1da13faee9fb8eedbca09cc5b574c Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Fri, 7 Jun 2024 13:00:40 +0200 Subject: [PATCH 04/33] Update command line to run SeaHorn - SeaHorn 14 does not support SV-COMP properties --- benchexec/tools/seahorn.py | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/benchexec/tools/seahorn.py b/benchexec/tools/seahorn.py index a91bed329..2a3eb98c4 100644 --- a/benchexec/tools/seahorn.py +++ b/benchexec/tools/seahorn.py @@ -16,7 +16,7 @@ import os -class Tool(benchexec.tools.template.BaseTool): +class Tool(benchexec.tools.template.BaseTool2): REQUIRED_PATHS = ["bin", "crab", "include", "lib", "share"] def executable(self, tool_locator): @@ -33,11 +33,8 @@ def name(self): def project_url(self): return "https://github.com/seahorn/seahorn" - def cmdline(self, executable, options, tasks, propertyfile, rlimits): - assert len(tasks) == 1 - assert propertyfile is not None - spec = ["--spec=" + propertyfile] - return [executable] + options + spec + tasks + def cmdline(self, executable, options, task, rlimits): + return [executable] + options + [task.single_input_file] def version(self, executable): return self._version_from_tool( From b5d4bacf4df85a34cc2a8a09a3a9e915a0a057b6 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Fri, 7 Jun 2024 13:13:01 +0200 Subject: [PATCH 05/33] Determine verification result for SeaHorn 14 --- benchexec/tools/seahorn.py | 26 ++++++-------------------- 1 file changed, 6 insertions(+), 20 deletions(-) diff --git a/benchexec/tools/seahorn.py b/benchexec/tools/seahorn.py index 2a3eb98c4..34ce310c4 100644 --- a/benchexec/tools/seahorn.py +++ b/benchexec/tools/seahorn.py @@ -41,23 +41,9 @@ def version(self, executable): f"{str(executable)}horn", line_prefix=" SeaHorn version" ) - def determine_result(self, returncode, returnsignal, output, isTimeout): - output = "\n".join(output) - if "BRUNCH_STAT Result TRUE" in output: - status = result.RESULT_TRUE_PROP - elif "BRUNCH_STAT Result FALSE" in output: - if "BRUNCH_STAT Termination" in output: - status = result.RESULT_FALSE_TERMINATION - else: - status = result.RESULT_FALSE_REACH - elif returnsignal == 9 or returnsignal == (128 + 9): - if isTimeout: - status = result.RESULT_TIMEOUT - else: - status = "KILLED BY SIGNAL 9" - elif returncode != 0: - status = f"ERROR ({returncode})" - else: - status = "FAILURE" - - return status + def determine_result(self, run): + if run.output[-1].startswith("sat"): + return result.RESULT_FALSE_PROP + if run.output[-1].startswith("unsat"): + return result.RESULT_TRUE_PROP + return result.RESULT_ERROR From 94af94b7ef45ef61b3aa607d3913c9e6ba8fa562 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Fri, 7 Jun 2024 19:04:50 +0200 Subject: [PATCH 06/33] Remove unused import --- benchexec/tools/seahorn.py | 3 --- 1 file changed, 3 deletions(-) diff --git a/benchexec/tools/seahorn.py b/benchexec/tools/seahorn.py index 34ce310c4..8bb1f3723 100644 --- a/benchexec/tools/seahorn.py +++ b/benchexec/tools/seahorn.py @@ -9,12 +9,9 @@ # SeaHorn Verification Framework # DM-0002198 -import benchexec.util as util import benchexec.tools.template import benchexec.result as result -import os - class Tool(benchexec.tools.template.BaseTool2): REQUIRED_PATHS = ["bin", "crab", "include", "lib", "share"] From 0fc2c9398c9683106d551b520c526ebe864c1619 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Tue, 11 Jun 2024 17:09:46 +0200 Subject: [PATCH 07/33] Use groupadd instead of addgroup in our .deb-package installation script addgroup is a user-friendly high-level command, whereas groupadd is a low-level command. I noticed out that not in all containers addgroup is available, and then the installation script reports an error. AFAIS there should be no difference between "addgroup --system" and "groupadd --force --system", so we can switch to the latter, which exists everywhere. --- debian/benchexec.postinst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/debian/benchexec.postinst b/debian/benchexec.postinst index 7fab8891e..b804eff9d 100644 --- a/debian/benchexec.postinst +++ b/debian/benchexec.postinst @@ -12,7 +12,7 @@ set -e GROUP=benchexec add_group() { - addgroup --system "${GROUP}" + groupadd --force --system "${GROUP}" if [ ! -f /sys/fs/cgroup/cgroup.controllers ]; then echo echo "Please add those user accounts that should be able to use BenchExec to the group ${GROUP}." From ef831c5aa0943a3aa3f78928cf481a981fabd5ae Mon Sep 17 00:00:00 2001 From: younghojan Date: Fri, 24 May 2024 14:30:21 +0800 Subject: [PATCH 08/33] Add helpful error message on Ubuntu 24.04 if namespaces are restricted --- benchexec/container.py | 8 ++++++++ benchexec/containerexecutor.py | 7 +++++++ benchexec/containerized_tool.py | 8 ++++++++ doc/INSTALL.md | 4 ++++ doc/container.md | 2 +- 5 files changed, 28 insertions(+), 1 deletion(-) diff --git a/benchexec/container.py b/benchexec/container.py index ca49ed4dd..e1bba2e5f 100644 --- a/benchexec/container.py +++ b/benchexec/container.py @@ -115,6 +115,14 @@ ) """Whether we use generated native code for clone or an unsafe Python fallback""" +_ERROR_MSG_USER_NS_RESTRICTION = ( + "Unprivileged user namespaces forbidden on this system, please " + "enable them with 'sysctl -w kernel.apparmor_restrict_unprivileged_userns=0'. " + "Ubuntu disables them by default since 24.04, refer to " + "https://ubuntu.com/blog/ubuntu-23-10-restricted-unprivileged-user-namespaces " + "for more information." +) + @contextlib.contextmanager def allocate_stack(size=DEFAULT_STACK_SIZE): diff --git a/benchexec/containerexecutor.py b/benchexec/containerexecutor.py index ff2a31641..bf442d6cf 100644 --- a/benchexec/containerexecutor.py +++ b/benchexec/containerexecutor.py @@ -754,6 +754,13 @@ def child(): traceback.extract_tb(e.__traceback__, limit=-1)[0].line, e, ) + if util.try_read_file( + "/proc/sys/kernel/apparmor_restrict_unprivileged_userns" + ) == "1" and e.errno in [ + errno.EPERM, + errno.EACCES, + ]: + logging.critical(container._ERROR_MSG_USER_NS_RESTRICTION) return CHILD_OSERROR try: diff --git a/benchexec/containerized_tool.py b/benchexec/containerized_tool.py index bcd0259b7..59fa90345 100644 --- a/benchexec/containerized_tool.py +++ b/benchexec/containerized_tool.py @@ -124,6 +124,14 @@ def _init_container_and_load_tool(tool_module, *args, **kwargs): try: _init_container(*args, **kwargs) except OSError as e: + if ( + util.try_read_file("/proc/sys/kernel/apparmor_restrict_unprivileged_userns") + == "1" + ) and e.errno in [ + errno.EPERM, + errno.EACCES, + ]: + raise BenchExecException(container._ERROR_MSG_USER_NS_RESTRICTION) raise BenchExecException(f"Failed to configure container: {e}") return _load_tool(tool_module) diff --git a/doc/INSTALL.md b/doc/INSTALL.md index b5c90ce26..4f3a16c88 100644 --- a/doc/INSTALL.md +++ b/doc/INSTALL.md @@ -169,6 +169,10 @@ that are not usable on all distributions by default: On CentOS it can be necessary to enable this feature with `sudo sysctl -w user.max_user_namespaces=10000` or a respective entry in `/etc/sysctl.conf` (the exact value is not important). + On Ubuntu 24.04 (or newer versions) it can be necessary to enable this feature with + `sysctl -w kernel.apparmor_restrict_unprivileged_userns=0` or a respective entry + in `/etc/sysctl.conf`. + - **Unprivileged Overlay Filesystem**: This is only available since Linux 5.11 (kernel option `CONFIG_OVERLAY_FS`), diff --git a/doc/container.md b/doc/container.md index a01b40b27..fe81c5354 100644 --- a/doc/container.md +++ b/doc/container.md @@ -211,7 +211,7 @@ in a container with `containerexec` than using `benchexec` or `runexec`. #### `Cannot execute ...: Unprivileged user namespaces forbidden on this system...` Unprivileged user namespaces are forbidden on your system -(this is the default on some distributions like Debian, Arch Linux, and CentOS). +(this is the default on some distributions like Debian, Arch Linux, CentOS, and Ubuntu since 24.04). Please check the [system requirements](INSTALL.md#kernel-requirements) how to enable them. From fb6a54a90e0da9a2f778591311cd5bfb7f521cb5 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Thu, 13 Jun 2024 13:26:10 +0200 Subject: [PATCH 09/33] Refactoring: remove duplicate code into utility function --- benchexec/container.py | 15 +++++++++++++++ benchexec/containerexecutor.py | 7 +------ benchexec/containerized_tool.py | 8 +------- 3 files changed, 17 insertions(+), 13 deletions(-) diff --git a/benchexec/container.py b/benchexec/container.py index e1bba2e5f..9c80055d2 100644 --- a/benchexec/container.py +++ b/benchexec/container.py @@ -44,6 +44,7 @@ "CONTAINER_GID", "CONTAINER_HOME", "CONTAINER_HOSTNAME", + "check_apparmor_userns_restriction", ] @@ -124,6 +125,20 @@ ) +def check_apparmor_userns_restriction(error: OSError): + """Check whether the passed OSError was likely caused by Ubuntu's AppArmor-based + restriction of user namespaces.""" + return ( + error.errno + in [ + errno.EPERM, + errno.EACCES, + ] + and util.try_read_file("/proc/sys/kernel/apparmor_restrict_unprivileged_userns") + == "1" + ) + + @contextlib.contextmanager def allocate_stack(size=DEFAULT_STACK_SIZE): """Allocate some memory that can be used as a stack. diff --git a/benchexec/containerexecutor.py b/benchexec/containerexecutor.py index bf442d6cf..eb6d08393 100644 --- a/benchexec/containerexecutor.py +++ b/benchexec/containerexecutor.py @@ -754,12 +754,7 @@ def child(): traceback.extract_tb(e.__traceback__, limit=-1)[0].line, e, ) - if util.try_read_file( - "/proc/sys/kernel/apparmor_restrict_unprivileged_userns" - ) == "1" and e.errno in [ - errno.EPERM, - errno.EACCES, - ]: + if container.check_apparmor_userns_restriction(e): logging.critical(container._ERROR_MSG_USER_NS_RESTRICTION) return CHILD_OSERROR diff --git a/benchexec/containerized_tool.py b/benchexec/containerized_tool.py index 59fa90345..3ab1c005e 100644 --- a/benchexec/containerized_tool.py +++ b/benchexec/containerized_tool.py @@ -124,13 +124,7 @@ def _init_container_and_load_tool(tool_module, *args, **kwargs): try: _init_container(*args, **kwargs) except OSError as e: - if ( - util.try_read_file("/proc/sys/kernel/apparmor_restrict_unprivileged_userns") - == "1" - ) and e.errno in [ - errno.EPERM, - errno.EACCES, - ]: + if container.check_apparmor_userns_restriction(e): raise BenchExecException(container._ERROR_MSG_USER_NS_RESTRICTION) raise BenchExecException(f"Failed to configure container: {e}") return _load_tool(tool_module) From 7753c4af03f7212a9602425830f5bc8eadae6782 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Tue, 11 Jun 2024 16:48:06 +0200 Subject: [PATCH 10/33] Add an AppArmor profile for BenchExec to its .deb package On Ubuntu since 24.04, user namespaces are forbidden for regular users (cf. #1041 and #1042). There is a global sysctl switch to enable them again, but applications whose AppArmor profile allows this can also use it. (Typically, AppArmor only restricts application, but in this case an AppArmor profile can actually provide a privilege than an unconfined application does not have.) More explanations are at https://ubuntu.com/blog/ubuntu-23-10-restricted-unprivileged-user-namespaces In order to make BenchExec usable out-of-the-box after installing the .deb package we want to ship such an AppArmor profile. This is made complicated by the fact that the AppArmor profile that is necessary on Ubuntu 24.04+ breaks AppArmor on previous Ubuntu versions. So we have to install this profile conditionally. I found a way to do so using ucf (a tool for handling config files) and this seems to work in my tests on Ubuntu 22.04 (old AppArmor), Ubuntu 24.04 (new AppArmor), and Debian 12 (old AppArmor), as well as installation without AppArmor present. There are two known remaining problems: - If one upgrades from Ubuntu 22.04 to Ubuntu 24.04 while having BenchExec installed, the AppArmor profile will not be installed, so BenchExec will not work. Upgrading or reinstalling the BenchExec package makes it work. - The command "python3 -m benchexec.test_tool_info" will not work, because the AppArmor profile won't match it. One has to either disable container mode or temporarily allow the use of user namespaces for the whole system. If we implement #1053 this would just work. Part of #1041. --- .../usr/share/benchexec/apparmor.d/benchexec | 22 +++++++++++++++ debian/benchexec.postinst | 10 ++++++- debian/benchexec.postrm | 27 +++++++++++++++++++ debian/control | 3 ++- debian/install | 1 + debian/rules | 4 +++ doc/INSTALL.md | 13 ++++----- 7 files changed, 72 insertions(+), 8 deletions(-) create mode 100644 debian/additional_files/usr/share/benchexec/apparmor.d/benchexec create mode 100644 debian/benchexec.postrm diff --git a/debian/additional_files/usr/share/benchexec/apparmor.d/benchexec b/debian/additional_files/usr/share/benchexec/apparmor.d/benchexec new file mode 100644 index 000000000..a0f5f5de4 --- /dev/null +++ b/debian/additional_files/usr/share/benchexec/apparmor.d/benchexec @@ -0,0 +1,22 @@ +#!/bin/sh + +# This file is part of BenchExec, a framework for reliable benchmarking: +# https://github.com/sosy-lab/benchexec +# +# SPDX-FileCopyrightText: 2024 Dirk Beyer +# +# SPDX-License-Identifier: Apache-2.0 + +# based on example in +# https://ubuntu.com/blog/ubuntu-23-10-restricted-unprivileged-user-namespaces + +abi , + +include + +profile benchexec /usr/bin/{bench,container,run}exec flags=(default_allow) { + userns, + + # Site-specific additions and overrides. See local/README for details. + include if exists +} diff --git a/debian/benchexec.postinst b/debian/benchexec.postinst index b804eff9d..b61945ee6 100644 --- a/debian/benchexec.postinst +++ b/debian/benchexec.postinst @@ -3,7 +3,7 @@ # This file is part of BenchExec, a framework for reliable benchmarking: # https://github.com/sosy-lab/benchexec # -# SPDX-FileCopyrightText: 2019-2020 Dirk Beyer +# SPDX-FileCopyrightText: 2019-2024 Dirk Beyer # # SPDX-License-Identifier: Apache-2.0 @@ -26,4 +26,12 @@ case "$1" in ;; esac +if [ "$1" = "configure" ] || [ "$1" = "abort-upgrade" ]; then + # Our AppArmor profiles depend on abi/4.0, so install only if this is available. + if [ -f "/etc/apparmor.d/abi/4.0" ]; then + ucf "/usr/share/benchexec/apparmor.d/benchexec" "/etc/apparmor.d/benchexec" + ucfr benchexec "/etc/apparmor.d/benchexec" + fi +fi + #DEBHELPER# diff --git a/debian/benchexec.postrm b/debian/benchexec.postrm new file mode 100644 index 000000000..bbd41cb3a --- /dev/null +++ b/debian/benchexec.postrm @@ -0,0 +1,27 @@ +#!/bin/sh + +# This file is part of BenchExec, a framework for reliable benchmarking: +# https://github.com/sosy-lab/benchexec +# +# SPDX-FileCopyrightText: 2024 Dirk Beyer +# +# SPDX-License-Identifier: Apache-2.0 + +set -e + +# Only relevant for Ubuntu 24.04+, but works safely everywhere. +# Based on what dh_ucf/13.6ubuntu1 would produce. +if [ "$1" = "purge" ]; then + for ext in .ucf-new .ucf-old .ucf-dist ""; do + rm -f "/etc/apparmor.d/benchexec$ext" + done + + if [ -x "`command -v ucf`" ]; then + ucf --purge "/etc/apparmor.d/benchexec" + fi + if [ -x "`command -v ucfr`" ]; then + ucfr --purge benchexec "/etc/apparmor.d/benchexec" + fi +fi + +#DEBHELPER# diff --git a/debian/control b/debian/control index 7078ead5c..768b0f5a0 100644 --- a/debian/control +++ b/debian/control @@ -3,6 +3,7 @@ Section: utils Priority: optional Maintainer: Philipp Wendler Build-Depends: debhelper (>= 11), + dh-apparmor, dh-python, python3 (>= 3.7), python3-setuptools, @@ -17,7 +18,7 @@ Vcs-Browser: https://github.com/sosy-lab/benchexec Package: benchexec Architecture: all -Depends: ${python3:Depends}, python3-pkg-resources, ${misc:Depends} +Depends: ${python3:Depends}, python3-pkg-resources, ${misc:Depends}, ucf Recommends: cpu-energy-meter, libseccomp2, lxcfs, python3-coloredlogs, python3-pystemd Description: Framework for Reliable Benchmarking and Resource Measurement BenchExec allows benchmarking non-interactive tools on Linux systems. diff --git a/debian/install b/debian/install index 23e5a64a3..6cab75f37 100644 --- a/debian/install +++ b/debian/install @@ -1 +1,2 @@ debian/additional_files/lib/* lib/ +debian/additional_files/usr/* usr/ diff --git a/debian/rules b/debian/rules index 7ce8d46ad..85c6a887e 100755 --- a/debian/rules +++ b/debian/rules @@ -29,6 +29,10 @@ override_dh_auto_install: dh_auto_install python3 setup.py install --root=$(CURDIR)/debian/$(DEB_SOURCE) --install-layout=deb +override_dh_install: + dh_install + dh_apparmor --profile-name=benchexec + override_dh_installchangelogs: dh_installchangelogs CHANGELOG.md diff --git a/doc/INSTALL.md b/doc/INSTALL.md index 06cb567d7..98db33727 100644 --- a/doc/INSTALL.md +++ b/doc/INSTALL.md @@ -170,17 +170,18 @@ that are not usable on all distributions by default: - **User Namespaces**: This is available on most distros (the kernel option is `CONFIG_USER_NS`), - but Debian and Arch Linux disable this feature for regular users, - so the system administrator needs to enable it - with `sudo sysctl -w kernel.unprivileged_userns_clone=1` or a respective entry + but many distributions disable this feature for regular users, + so the system administrator needs to enable it. + On *Debian* or *Arch* it can be necessary to enable this feature with + `sudo sysctl -w kernel.unprivileged_userns_clone=1` or a respective entry in `/etc/sysctl.conf`. - On CentOS it can be necessary to enable this feature with + On *CentOS* it can be necessary to enable this feature with `sudo sysctl -w user.max_user_namespaces=10000` or a respective entry in `/etc/sysctl.conf` (the exact value is not important). - On Ubuntu 24.04 (or newer versions) it can be necessary to enable this feature with + On *Ubuntu*, we recommend to use our Ubuntu package, which takes care of this. + Alternatively, on 24.04 or newer one can enable this feature with `sysctl -w kernel.apparmor_restrict_unprivileged_userns=0` or a respective entry in `/etc/sysctl.conf`. - - **Unprivileged Overlay Filesystem**: This is only available since Linux 5.11 (kernel option `CONFIG_OVERLAY_FS`), From 6879cfc19ba20bcc6dbcf0ffdf40972d0c6d519a Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Fri, 14 Jun 2024 15:28:26 +0200 Subject: [PATCH 11/33] Adapt CPAchecker's tool-info module to change of executable CPAchecker will use bin/cpachecker instead of scripts/cpa.sh soon (cf. https://gitlab.com/sosy-lab/software/cpachecker/-/issues/632). We will support both in the tool-info module. Same change is also done for CPA-Witness2Test, which also has its executable renamed. --- benchexec/tools/cpa-witness2test.py | 21 ++++++++++++++++++++- benchexec/tools/cpachecker.py | 29 +++++++++++++++++++++++++---- 2 files changed, 45 insertions(+), 5 deletions(-) diff --git a/benchexec/tools/cpa-witness2test.py b/benchexec/tools/cpa-witness2test.py index 2b522babe..e84e5344a 100644 --- a/benchexec/tools/cpa-witness2test.py +++ b/benchexec/tools/cpa-witness2test.py @@ -7,6 +7,8 @@ import benchexec.tools.cpachecker as cpachecker +from benchexec.tools.template import ToolNotFoundException + class Tool(cpachecker.Tool): """ @@ -16,7 +18,24 @@ class Tool(cpachecker.Tool): def executable(self, tool_locator): # Makes sure that CPAchecker can be called, shows a warning otherwise super(Tool, self).executable(tool_locator) - return tool_locator.find_executable("cpa_witness2test.py", subdir="scripts") + # The following will perform these lookups (if --tool-directory is not given) + # and pick the first one that is found: + # 1. cpa-witness2test in PATH + # 2. cpa-witness2test in ./ and bin/ + # 3. cpa_witness2test.py in PATH + # 4. cpa_witness2test.py in ./ and scripts/ + # This follows the BenchExec logic of "look up first in PATH, then ./" + # except for the case "cpa_witness2test.py in PATH and cpa-witness2test in bin/", + # which should be ok. + try: + return tool_locator.find_executable("cpa-witness2test", subdir="bin") + except ToolNotFoundException as e1: + try: + return tool_locator.find_executable( + "cpa_witness2test.py", subdir="scripts" + ) + except ToolNotFoundException: + raise e1 def version(self, executable): stdout = self._version_from_tool(executable, "-version") diff --git a/benchexec/tools/cpachecker.py b/benchexec/tools/cpachecker.py index 19b3981b1..408bd47c6 100644 --- a/benchexec/tools/cpachecker.py +++ b/benchexec/tools/cpachecker.py @@ -13,6 +13,8 @@ import benchexec.result as result import benchexec.tools.template +from benchexec.tools.template import ToolNotFoundException + class Tool(benchexec.tools.template.BaseTool2): """ @@ -31,6 +33,7 @@ class Tool(benchexec.tools.template.BaseTool2): """ REQUIRED_PATHS = [ + "bin/cpachecker", "lib/java/runtime", "lib/*.jar", "lib/native/x86_64-linux", @@ -40,10 +43,28 @@ class Tool(benchexec.tools.template.BaseTool2): ] def executable(self, tool_locator): - executable = tool_locator.find_executable("cpa.sh", subdir="scripts") + # The following will perform these lookups (if --tool-directory is not given) + # and pick the first one that is found: + # 1. cpachecker in PATH + # 2. cpachecker in ./ and bin/ + # 3. cpa.sh in PATH + # 4. cpa.sh in ./ and scripts/ + # This follows the BenchExec logic of "look up first in PATH, then ./" + # except for the case of "cpa.sh in PATH and cpachecker in bin/", + # which should be ok. + try: + executable = tool_locator.find_executable("cpachecker", subdir="bin") + except ToolNotFoundException as e1: + try: + executable = tool_locator.find_executable("cpa.sh", subdir="scripts") + except ToolNotFoundException: + raise e1 + base_dir = os.path.join(os.path.dirname(executable), os.path.pardir) jar_file = os.path.join(base_dir, "cpachecker.jar") - bin_dir = os.path.join(base_dir, "bin") + cls_dir = os.path.join( + base_dir, "bin" if executable.endswith("cpa.sh") else "classes" + ) src_dir = os.path.join(base_dir, "src") # If this is a source checkout of CPAchecker, we heuristically check that @@ -55,8 +76,8 @@ def executable(self, tool_locator): if src_mtime > os.stat(jar_file).st_mtime: sys.exit("CPAchecker JAR is not uptodate, run 'ant jar'!") - elif os.path.isdir(bin_dir): - if src_mtime > self._find_newest_mtime(bin_dir): + elif os.path.isdir(cls_dir): + if src_mtime > self._find_newest_mtime(cls_dir): sys.exit("CPAchecker build is not uptodate, run 'ant'!") return executable From 8fc72af84fcef4387989eb8a7ac437c19f42607e Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Fri, 14 Jun 2024 15:37:18 +0200 Subject: [PATCH 12/33] Refactoring: introduce utility function in CPAchecker's tool-info module This is a preparation for the next commit. --- benchexec/tools/cpachecker.py | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/benchexec/tools/cpachecker.py b/benchexec/tools/cpachecker.py index 408bd47c6..4cfb4e435 100644 --- a/benchexec/tools/cpachecker.py +++ b/benchexec/tools/cpachecker.py @@ -142,11 +142,15 @@ def project_url(self): return "https://cpachecker.sosy-lab.org/" def _get_additional_options(self, existing_options, task, rlimits): + + def option_present(option): + return f"-{option}" in existing_options + options = [] - if rlimits.cputime and "-timelimit" not in existing_options: + if rlimits.cputime and not option_present("timelimit"): options += ["-timelimit", f"{rlimits.cputime}s"] - if "-stats" not in existing_options: + if not option_present("stats"): options += ["-stats"] if task.property_file: @@ -155,10 +159,10 @@ def _get_additional_options(self, existing_options, task, rlimits): if isinstance(task.options, dict) and task.options.get("language") == "C": data_model = task.options.get("data_model") if data_model: - data_model_option = {"ILP32": "-32", "LP64": "-64"}.get(data_model) + data_model_option = {"ILP32": "32", "LP64": "64"}.get(data_model) if data_model_option: - if data_model_option not in existing_options: - options += [data_model_option] + if not option_present(data_model_option): + options += [f"-{data_model_option}"] else: raise benchexec.tools.template.UnsupportedFeatureException( f"Unsupported data_model '{data_model}' defined for task '{task}'" From 9717254aa976f270f7a436b62a93622062484c36 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Fri, 14 Jun 2024 16:34:03 +0200 Subject: [PATCH 13/33] Adapt tool-info module to new option style of CPAchecker CPAchecker will soon use command-line arguments with "--" as prefix. The old arguments will continue to be supported, but we want to use the new ones in the tool-info module when possible in order to not confuse users. So let's let the tool-info module adapt to the options that the user specified in the benchmark definition. Cf. https://gitlab.com/sosy-lab/software/cpachecker/-/issues/1218 --- benchexec/tools/cpachecker.py | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/benchexec/tools/cpachecker.py b/benchexec/tools/cpachecker.py index 4cfb4e435..3a30c6b75 100644 --- a/benchexec/tools/cpachecker.py +++ b/benchexec/tools/cpachecker.py @@ -142,19 +142,23 @@ def project_url(self): return "https://cpachecker.sosy-lab.org/" def _get_additional_options(self, existing_options, task, rlimits): + # If at least one option uses "--" style, we use that for options added here. + # Otherwise use "-" to be safe for old versions of CPAchecker. + new_option_style = any(option.startswith("--") for option in existing_options) + prefix = "--" if new_option_style else "-" def option_present(option): - return f"-{option}" in existing_options + return f"-{option}" in existing_options or f"--{option}" in existing_options options = [] if rlimits.cputime and not option_present("timelimit"): - options += ["-timelimit", f"{rlimits.cputime}s"] + options += [f"{prefix}timelimit", f"{rlimits.cputime}s"] if not option_present("stats"): - options += ["-stats"] + options += [f"{prefix}stats"] if task.property_file: - options += ["-spec", task.property_file] + options += [f"{prefix}spec", task.property_file] if isinstance(task.options, dict) and task.options.get("language") == "C": data_model = task.options.get("data_model") @@ -162,7 +166,7 @@ def option_present(option): data_model_option = {"ILP32": "32", "LP64": "64"}.get(data_model) if data_model_option: if not option_present(data_model_option): - options += [f"-{data_model_option}"] + options += [f"{prefix}{data_model_option}"] else: raise benchexec.tools.template.UnsupportedFeatureException( f"Unsupported data_model '{data_model}' defined for task '{task}'" From 31ad021bfc8d01d418ea44bb8ae8c7eab2e89cad Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Fri, 14 Jun 2024 20:28:43 +0200 Subject: [PATCH 14/33] Add --architecture flag to theta --- benchexec/tools/theta.py | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/benchexec/tools/theta.py b/benchexec/tools/theta.py index a39a90b2e..cc5e1f7ee 100644 --- a/benchexec/tools/theta.py +++ b/benchexec/tools/theta.py @@ -34,10 +34,18 @@ def cmdline(self, executable, options, task, rlimits): # Theta supports data race and unreach call if task.property_file: options += ["--property", task.property_file] + if isinstance(task.options, dict) and task.options.get("language") == "C": + data_model = task.options.get("data_model") + if data_model: + options += ["--architecture", data_model] + return [executable, task.single_input_file] + options def determine_result(self, run): + if run.was_timeout: + return result.RESULT_TIMEOUT status = result.RESULT_UNKNOWN + for line in run.output: if "SafetyResult Unsafe" in line: status = result.RESULT_FALSE_REACH From 4036a88591e5b1b21e8f6496d41d32b88f2bcf70 Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Fri, 14 Jun 2024 20:30:35 +0200 Subject: [PATCH 15/33] Update theta.py --- benchexec/tools/theta.py | 1 - 1 file changed, 1 deletion(-) diff --git a/benchexec/tools/theta.py b/benchexec/tools/theta.py index cc5e1f7ee..beda5dafa 100644 --- a/benchexec/tools/theta.py +++ b/benchexec/tools/theta.py @@ -45,7 +45,6 @@ def determine_result(self, run): if run.was_timeout: return result.RESULT_TIMEOUT status = result.RESULT_UNKNOWN - for line in run.output: if "SafetyResult Unsafe" in line: status = result.RESULT_FALSE_REACH From a4fb31f8c9afdc5bbaf789e71144e08d37d9ffb5 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Tue, 18 Jun 2024 09:09:33 +0200 Subject: [PATCH 16/33] Fix crash with FileNotFoundError in cgroups v2 fallback case. This was a race condition if a process in the same cgroup as BenchExec stopped while we check its status. --- benchexec/util.py | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/benchexec/util.py b/benchexec/util.py index 0c0d7a5d7..43827c16e 100644 --- a/benchexec/util.py +++ b/benchexec/util.py @@ -830,11 +830,14 @@ def is_child_process_of_us(pid: int) -> bool: return True ppid = None - with open(f"/proc/{pid}/status") as status_file: - for line in status_file: - if line.startswith("PPid:"): - ppid = int(line.split(":", maxsplit=1)[1].strip()) - break + try: + with open(f"/proc/{pid}/status") as status_file: + for line in status_file: + if line.startswith("PPid:"): + ppid = int(line.split(":", maxsplit=1)[1].strip()) + break + except FileNotFoundError: + pass # Process terminated in the meantime. if ppid: return is_child_process_of_us(ppid) From 1ea185657e470e31d96ed452fc30a511bbdeff69 Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Tue, 18 Jun 2024 11:47:21 +0200 Subject: [PATCH 17/33] Add was_terminated check --- benchexec/tools/theta.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/benchexec/tools/theta.py b/benchexec/tools/theta.py index beda5dafa..60696808b 100644 --- a/benchexec/tools/theta.py +++ b/benchexec/tools/theta.py @@ -44,6 +44,8 @@ def cmdline(self, executable, options, task, rlimits): def determine_result(self, run): if run.was_timeout: return result.RESULT_TIMEOUT + if run.was_terminated: + return result.RESULT_ERROR status = result.RESULT_UNKNOWN for line in run.output: if "SafetyResult Unsafe" in line: From ea3fd0f22e9cc6e6f9fef4de5da72e634d3dac0f Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Tue, 18 Jun 2024 12:17:53 +0200 Subject: [PATCH 18/33] Update theta.py --- benchexec/tools/theta.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/benchexec/tools/theta.py b/benchexec/tools/theta.py index 60696808b..c1a7d1c47 100644 --- a/benchexec/tools/theta.py +++ b/benchexec/tools/theta.py @@ -42,8 +42,6 @@ def cmdline(self, executable, options, task, rlimits): return [executable, task.single_input_file] + options def determine_result(self, run): - if run.was_timeout: - return result.RESULT_TIMEOUT if run.was_terminated: return result.RESULT_ERROR status = result.RESULT_UNKNOWN From fa218eb3ebc6fd8928d7747443ba154ad8dca093 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Tue, 18 Jun 2024 17:39:48 +0200 Subject: [PATCH 19/33] Adapt SeaHorn's tool-info module such that it is compatible with its default and SV-COMP wrapper In `executable()`, we look for `bin/sea_svcomp` (the SV-COMP wrapper) first. If it does not exist, then we look for `bin/sea` (the default wrapper). --- benchexec/tools/seahorn.py | 48 +++++++++++++++++++++++++++++++------- 1 file changed, 39 insertions(+), 9 deletions(-) diff --git a/benchexec/tools/seahorn.py b/benchexec/tools/seahorn.py index 8bb1f3723..c008ab843 100644 --- a/benchexec/tools/seahorn.py +++ b/benchexec/tools/seahorn.py @@ -9,6 +9,8 @@ # SeaHorn Verification Framework # DM-0002198 +import logging +import os import benchexec.tools.template import benchexec.result as result @@ -17,7 +19,16 @@ class Tool(benchexec.tools.template.BaseTool2): REQUIRED_PATHS = ["bin", "crab", "include", "lib", "share"] def executable(self, tool_locator): - return tool_locator.find_executable("sea", subdir="bin") + self.use_svcomp_wrapper = False + try: + # try to find the SV-COMP wrapper script + ret = tool_locator.find_executable("sea_svcomp", subdir="bin") + self.use_svcomp_wrapper = True + logging.debug("Using SeaHorn's SV-COMP wrapper") + return ret + except benchexec.tools.template.ToolNotFoundException: + # find the default wrapper script + return tool_locator.find_executable("sea", subdir="bin") def program_files(self, executable): return self._program_files_from_executable( @@ -31,16 +42,35 @@ def project_url(self): return "https://github.com/seahorn/seahorn" def cmdline(self, executable, options, task, rlimits): + if self.use_svcomp_wrapper and task.property_file: + options += [f"--spec={task.property_file}"] return [executable] + options + [task.single_input_file] def version(self, executable): - return self._version_from_tool( - f"{str(executable)}horn", line_prefix=" SeaHorn version" - ) + seahorn_exe = os.path.join(os.path.dirname(executable), "seahorn") + return self._version_from_tool(seahorn_exe, line_prefix=" SeaHorn version") def determine_result(self, run): - if run.output[-1].startswith("sat"): - return result.RESULT_FALSE_PROP - if run.output[-1].startswith("unsat"): - return result.RESULT_TRUE_PROP - return result.RESULT_ERROR + if self.use_svcomp_wrapper: + if run.output.any_line_contains("BRUNCH_STAT Result TRUE"): + return result.RESULT_TRUE_PROP + elif run.output.any_line_contains("BRUNCH_STAT Result FALSE"): + if run.output.any_line_contains("BRUNCH_STAT Termination"): + return result.RESULT_FALSE_TERMINATION + else: + return result.RESULT_FALSE_REACH + elif run.exit_code.signal == 9 or run.exit_code.signal == (128 + 9): + if run.was_timeout: + return result.RESULT_TIMEOUT + else: + return "KILLED BY SIGNAL 9" + elif run.exit_code.value != 0: + return f"ERROR ({run.exit_code.value})" + else: + return "FAILURE" + else: + if run.output[-1].startswith("sat"): + return result.RESULT_FALSE_PROP + if run.output[-1].startswith("unsat"): + return result.RESULT_TRUE_PROP + return result.RESULT_ERROR From 8ee78e116b6ecf6c8dc97e773bef9b9b81870325 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Tue, 18 Jun 2024 22:38:54 +0200 Subject: [PATCH 20/33] Remove a redundant required path --- benchexec/tools/seahorn.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/benchexec/tools/seahorn.py b/benchexec/tools/seahorn.py index c008ab843..0fd686fc5 100644 --- a/benchexec/tools/seahorn.py +++ b/benchexec/tools/seahorn.py @@ -16,7 +16,7 @@ class Tool(benchexec.tools.template.BaseTool2): - REQUIRED_PATHS = ["bin", "crab", "include", "lib", "share"] + REQUIRED_PATHS = ["bin", "include", "lib", "share"] def executable(self, tool_locator): self.use_svcomp_wrapper = False From 6725bda9627d23e044e6298b109c51d77a3c1f68 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Wed, 19 Jun 2024 08:35:21 +0200 Subject: [PATCH 21/33] Fix tool-info module of CPA-witness2test: executable is required Previously, the tool-info module of CPAchecker ensured that the executable of CPA-witness2test is covered by program_files(), because the scripts/ directory is part of the program files. But for new versions of CPAchecker we do not add all of bin/ to the program files, so we need to explicitly add cpa-witness2test. --- benchexec/tools/cpa-witness2test.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/benchexec/tools/cpa-witness2test.py b/benchexec/tools/cpa-witness2test.py index e84e5344a..191defd40 100644 --- a/benchexec/tools/cpa-witness2test.py +++ b/benchexec/tools/cpa-witness2test.py @@ -45,6 +45,9 @@ def version(self, executable): def name(self): return "CPA-witness2test" + def program_files(self, executable): + return [executable] + super().program_files(executable) + def cmdline(self, executable, options, task, rlimits): additional_options = self._get_additional_options(options, task, rlimits) # Add additional options in front of existing ones, since -gcc-args ... must be last argument in front of task From 8e94a7013613345be530ddb6a0030a8dab79acbc Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Wed, 19 Jun 2024 10:27:40 +0200 Subject: [PATCH 22/33] Changelog and contributors for BenchExec 3.22 --- CHANGELOG.md | 60 ++++++++++++++++++++++++++++++++++++++++++++++++++++ README.md | 7 +++++- 2 files changed, 66 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0059f4d7a..23d1eb6a1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,66 @@ SPDX-License-Identifier: Apache-2.0 # BenchExec Changelog +## BenchExec 3.22 + +**This will be the last release of BenchExec to support Python 3.7.** +Future versions will require Python 3.8, +and in 2025 we are planning to drop support for Python 3.8 and 3.9. +Please [comment here](https://github.com/sosy-lab/benchexec/issues/986) +if these plans would create problems for you. + +BenchExec is now available as an +[official package in the NixOS distribution](https://github.com/sosy-lab/benchexec/blob/main/doc/INSTALL.md#nixos). +Thank you [@lorenzleutgeb](https://github.com/lorenzleutgeb)! + +- BenchExec now handles new restrictions imposed by Ubuntu 24.04. + Our Ubuntu package is recommended for installation + because it automatically does everything for making BenchExec work out of the box. + Users of other installation methods need to tweak their system config, + and both our documentation and the error message of BenchExec + now inform about what is necessary. Thank you [@younghojan](https://github.com/younghojan)! +- BenchExec is now easier to use on systems without systemd but with cgroups v2. + This is a common situation in containers, + and BenchExec will now automatically use the `/benchexec` cgroup + if it exists and has no running processes. + This makes it unnecessary to manually start BenchExec in a fresh cgroup, + but the `/benchexec` cgroup still needs to be created upfront. + We give examples how to do this in our + [documentation](https://github.com/sosy-lab/benchexec/blob/main/doc/benchexec-in-container.md). +- Several robustness improvements to BenchExec's container mode for non-standard environments. + This covers for example containers with invalid cgroup mounts, + systems with procfs mounts in several places, missing DBus, and Docker Desktop. +- Several fixes and improvements for the HTML tables produced by `table-generator`. + Thank you [@EshaanAgg](https://github.com/EshaanAgg) and [@JawHawk](https://github.com/JawHawk)! + - Filters for text columns are now case insensitive. + - Plots now have a reset button for clearing configuration changes. + - Text filters now work even if special characters like `_` or parentheses are used. + - Changes to the plot configuration no longer break the application + if it was opened from paths with spaces and other special characters. + - The drop-down area for status filters now immediately shows the correct value + when opening a table via a link with preconfigured filters. + - The filter for the left-most column is now correctly usable again + after a task-id filter in the filter sidebar was set and cleared. +- Fix handling of tools that read from stdin when asked to print their version. + In such a case, the tool (and thus BenchExec) would previously hang + but now stdin of the tool is connected to `/dev/null` + (just like during the actual execution) and the tool immediately gets EOF. +- Improvements to our documentation. + We now have a [quickstart tutorial for `runexec`](https://github.com/sosy-lab/benchexec/blob/main/doc/quickstart.md) + and a [guide specifically for executing BenchExec in containers](https://github.com/sosy-lab/benchexec/blob/main/doc/benchexec-in-container.md). + Thank you [@incaseoftrouble](https://github.com/incaseoftrouble)! +- Improvements for several tool-info modules. +- Integration of BenchExec and the cluster management tool SLURM. + It is not officially part of BenchExec and we do not provide any guarantees related to it, + but our repository now contains an + [integration of BenchExec and SLURM](https://github.com/sosy-lab/benchexec/tree/main/contrib/slurm) + that users of SLURM might find helpful. Thank you [@leventeBajczi](https://github.com/leventeBajczi)! + Further contributions in this area are also welcome. + +We celebrate that this release +sets a new record for contributions from non-maintainers +and thank all contributors! + ## BenchExec 3.21 - `table-generator` computes scores according to SV-COMP'24 scoring scheme. diff --git a/README.md b/README.md index 95d2a495b..e69b61817 100644 --- a/README.md +++ b/README.md @@ -129,6 +129,7 @@ which are available under several other free licenses Maintainer: [Philipp Wendler](https://www.philippwendler.de) Contributors: +- [Eshaan Aggarwal](https://github.com/EshaanAgg) - [Aditya Arora](https://github.com/alohamora) - [Levente Bajczi](https://github.com/leventeBajczi) - [Dirk Beyer](https://www.sosy-lab.org/people/beyer/) @@ -138,22 +139,26 @@ Contributors: - [Andreas Donig](https://github.com/adonig) - [Karlheinz Friedberger](https://www.sosy-lab.org/people/friedberger) - [Robin Gloster](https://github.com/globin) +- [Sam Grayson](https://github.com/charmoniumQ) - Peter Häring - [Florian Heck](https://github.com/fheck) -- [Hugo](https://github.com/hugovk) - [George Karpenkov](http://metaworld.me/) - [Mike Kazantsev](http://fraggod.net/) +- [Hugo van Kemenade](https://github.com/hugovk) - [Michael Lachner](https://github.com/lachnerm) - [Thomas Lemberger](https://www.sosy-lab.org/people/lemberger/) +- [Lorenz Leutgeb](https://github.com/lorenzleutgeb) - [Sebastian Ott](https://github.com/ottseb) - Stefan Löwe - [Stephan Lukasczyk](https://github.com/stephanlukasczyk) +- [Tobias Meggendorfer](https://github.com/incaseoftrouble) - [Alexander von Rhein](http://www.infosun.fim.uni-passau.de/se/people-rhein.php) - [Alexander Schremmer](https://www.xing.com/profile/Alexander_Schremmer) - [Dennis Simon](https://github.com/DennisSimon) - [Andreas Stahlbauer](http://stahlbauer.net/) - [Thomas Stieglmaier](https://stieglmaier.me/) - [Martin Yankov](https://github.com/marto97) +- [Hojan Young](https://github.com/younghojan) - [Ilja Zakharov](https://github.com/IljaZakharov) - and [lots of more people who integrated tools into BenchExec](https://github.com/sosy-lab/benchexec/graphs/contributors) From 57f5f402f287fce6c68ce132256c1404aba6ddfa Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Wed, 19 Jun 2024 10:58:02 +0200 Subject: [PATCH 23/33] Pin version of setuptools to older one for our build system Since version 69.3.0 the names of the produced build artifacts changes, but we prefer to keep the old names for compatibility. --- pyproject.toml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pyproject.toml b/pyproject.toml index 87d2cbaf7..fbc51a7fb 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -8,7 +8,8 @@ [build-system] requires = [ # Require versions that support our license files - 'setuptools >= 42.0.0', + # but produce the same names for artifacts as we always had. + 'setuptools == 69.2.0', 'wheel >= 0.32.0', ] build-backend = 'setuptools.build_meta' From cd0cad00673cdf1a5c7f034f4f9bf9fb904a2587 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Wed, 19 Jun 2024 15:09:48 +0200 Subject: [PATCH 24/33] Release 3.22 --- benchexec/__init__.py | 2 +- debian/changelog | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/benchexec/__init__.py b/benchexec/__init__.py index 2cd0b1d83..2e1c92cba 100644 --- a/benchexec/__init__.py +++ b/benchexec/__init__.py @@ -34,7 +34,7 @@ Variables ending with "tag" contain references to XML tag objects created by the XML parser. """ -__version__ = "3.22-dev" +__version__ = "3.22" class BenchExecException(Exception): # noqa: N818 backwards compatibility diff --git a/debian/changelog b/debian/changelog index ddeadd9a4..2b438a862 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,9 @@ +benchexec (3.22-1) jammy; urgency=medium + + * New upstream version. + + -- Philipp Wendler Wed, 19 Jun 2024 15:09:48 +0200 + benchexec (3.21-1) jammy; urgency=medium * New upstream version. From f4bd0f3917176046a83a2a525523bafc8cfa7e51 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Wed, 19 Jun 2024 15:17:16 +0200 Subject: [PATCH 25/33] Prepare version number for next development cycle. --- benchexec/__init__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/benchexec/__init__.py b/benchexec/__init__.py index 2e1c92cba..e872a0a0a 100644 --- a/benchexec/__init__.py +++ b/benchexec/__init__.py @@ -34,7 +34,7 @@ Variables ending with "tag" contain references to XML tag objects created by the XML parser. """ -__version__ = "3.22" +__version__ = "3.23-dev" class BenchExecException(Exception): # noqa: N818 backwards compatibility From 089ccf66551b89e35fad61940f7003ad936fc726 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Thu, 20 Jun 2024 08:34:33 +0200 Subject: [PATCH 26/33] Update users of BenchExec: SMT-COMP and Termination Competition SMT-COMP started to use BenchExec this year, and for Termination Competition is an important part of their measurement setup: https://lists.rwth-aachen.de/hyperkitty/list/termtools@lists.rwth-aachen.de/thread/6RTY4BDARIS74HSSUDJQYYQNURHIZ7IR/ --- README.md | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index e69b61817..0cd1a0bd3 100644 --- a/README.md +++ b/README.md @@ -164,11 +164,16 @@ Contributors: ### Users of BenchExec -BenchExec was successfully used for benchmarking in all instances -of the international competitions on [Software Verification](https://sv-comp.sosy-lab.org) -and [Software Testing](https://test-comp.sosy-lab.org) -with a wide variety of benchmarked tools and hundreds of thousands benchmark runs. -It is integrated into the cluster-based logic-solving service +Several well-known international competitions use BenchExec, +such as [SMT-COMP](https://smt-comp.github.io/), +[SV-COMP](https://sv-comp.sosy-lab.org) (software verification), +the [Termination Competition](https://termination-portal.org/wiki/Termination_Competition), +and +[Test-Comp](https://test-comp.sosy-lab.org). +In particular in SV-COMP +BenchExec was used successfully for benchmarking in all instances of the competition +and with a wide variety of benchmarked tools and millions of benchmark runs per year. +BenchExec is also integrated into the cluster-based logic-solving service [StarExec](https://www.starexec.org/starexec/public/about.jsp) ([GitHub](https://github.com/StarExec/StarExec)). The developers of the following tools use BenchExec: From 0e7c0f73f258c09a04a8423d45c0b2f9365c5239 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Thu, 20 Jun 2024 09:01:25 +0200 Subject: [PATCH 27/33] Drop support for Python 3.7 As announced in the changelog of BenchExec 3.22 and on the issue tracker. Part of #986. --- .gitlab-ci.yml | 11 ----------- benchexec/container.py | 6 +----- debian/control | 4 ++-- doc/INSTALL.md | 2 +- pyproject.toml | 2 +- test/Dockerfile.python-3.7 | 32 -------------------------------- 6 files changed, 5 insertions(+), 52 deletions(-) delete mode 100644 test/Dockerfile.python-3.7 diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index bfc92edd8..464ee1595 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -61,11 +61,6 @@ stages: paths: - coverage.xml -unit-tests:python-3.7: - <<: *unit-tests - variables: - PYTHON_VERSION: '3.7' - unit-tests:python-3.8: <<: *unit-tests variables: @@ -210,12 +205,6 @@ reuse: - schedules - web -build-docker:test:python-3.7: - extends: .build-docker - variables: - DOCKERFILE: test/Dockerfile.python-3.7 - IMAGE: test:python-3.7 - build-docker:test:python-3.8: extends: .build-docker variables: diff --git a/benchexec/container.py b/benchexec/container.py index 9c80055d2..c71af30b4 100644 --- a/benchexec/container.py +++ b/benchexec/container.py @@ -859,11 +859,7 @@ def setup_seccomp_filter(): logging.info("Could not enable seccomp filter for container isolation: %s", e) -try: - _ALL_SIGNALS = signal.valid_signals() # pytype: disable=module-attr -except AttributeError: - # Only exists on Python 3.8+ - _ALL_SIGNALS = range(1, signal.NSIG) +_ALL_SIGNALS = signal.valid_signals() def block_all_signals(): diff --git a/debian/control b/debian/control index 768b0f5a0..751d5092a 100644 --- a/debian/control +++ b/debian/control @@ -5,13 +5,13 @@ Maintainer: Philipp Wendler Build-Depends: debhelper (>= 11), dh-apparmor, dh-python, - python3 (>= 3.7), + python3 (>= 3.8), python3-setuptools, python3-lxml, python3-yaml (>= 3.12), python3-nose Standards-Version: 3.9.6.1 -X-Python3-Version: >= 3.7 +X-Python3-Version: >= 3.8 Homepage: https://github.com/sosy-lab/benchexec Vcs-Git: https://github.com/sosy-lab/benchexec.git Vcs-Browser: https://github.com/sosy-lab/benchexec diff --git a/doc/INSTALL.md b/doc/INSTALL.md index 98db33727..522f1592a 100644 --- a/doc/INSTALL.md +++ b/doc/INSTALL.md @@ -13,7 +13,7 @@ SPDX-License-Identifier: Apache-2.0 ### Requirements -- Python 3.7 or newer +- Python 3.8 or newer - Linux (cf. [Kernel Requirements](#kernel-requirements) below for details) - Access to cgroups (cf. [Setting up Cgroups](#setting-up-cgroups) below for details) - x86 or ARM machine (please [contact us](https://github.com/sosy-lab/benchexec/issues/new) for other architectures) diff --git a/pyproject.toml b/pyproject.toml index fbc51a7fb..5e4b78ba9 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -17,7 +17,7 @@ build-backend = 'setuptools.build_meta' [tool.black] include = 'bin|\.py$' exclude = 'node_modules|\.eggs' -target-version = ['py37'] +target-version = ['py38'] [tool.coverage.run] branch = true diff --git a/test/Dockerfile.python-3.7 b/test/Dockerfile.python-3.7 deleted file mode 100644 index 4002b6f67..000000000 --- a/test/Dockerfile.python-3.7 +++ /dev/null @@ -1,32 +0,0 @@ -# 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 - -# This is a Docker image for running the tests. -# It should be pushed to registry.gitlab.com/sosy-lab/software/benchexec/test -# and will be used by CI as declared in .gitlab-ci.yml. -# -# Commands for updating the image: -# docker build --pull -t registry.gitlab.com/sosy-lab/software/benchexec/test:python-3.7 - < test/Dockerfile.python-3.7 -# docker push registry.gitlab.com/sosy-lab/software/benchexec/test - -FROM python:3.7 - -# Cannot use apt package python3-pystemd here -# because these images do not use the Python installed via apt. - -RUN apt-get update && apt-get install -y \ - libsystemd-dev \ - lxcfs \ - sudo - -RUN pip install \ - coloredlogs \ - "coverage[toml] >= 5.0" \ - lxml \ - nose \ - pystemd \ - pyyaml From 98d0ad167ef644059443fec08b5353cd7e5e21e5 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Thu, 20 Jun 2024 14:55:39 +0200 Subject: [PATCH 28/33] Remove Python 3.7 from AppVeyor CI as well --- .appveyor.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.appveyor.yml b/.appveyor.yml index 203854d2a..57fb43606 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -7,7 +7,6 @@ environment: matrix: - - PYTHON: "C:\\Python37" - PYTHON: "C:\\Python38" - PYTHON: "C:\\Python39" From bc85102111a21ff1ac598fb26f01316ebe3247ee Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Fri, 21 Jun 2024 13:23:26 +0200 Subject: [PATCH 29/33] Use compatibility level 12 for building Debian packages According to the man page debhelper-compat-upgrade-checklist level 11 is deprecated and not recommended. A test build on level 12 produces an identical .deb package (same hash), so it seems we can safely upgrade. Also switch how we specify the compatibility level: In debian/control instead of debian/compat, because right now we need to specify it in two places. --- debian/compat | 1 - debian/control | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) delete mode 100644 debian/compat diff --git a/debian/compat b/debian/compat deleted file mode 100644 index b4de39476..000000000 --- a/debian/compat +++ /dev/null @@ -1 +0,0 @@ -11 diff --git a/debian/control b/debian/control index 751d5092a..725f611dd 100644 --- a/debian/control +++ b/debian/control @@ -2,7 +2,7 @@ Source: benchexec Section: utils Priority: optional Maintainer: Philipp Wendler -Build-Depends: debhelper (>= 11), +Build-Depends: debhelper-compat (= 12), dh-apparmor, dh-python, python3 (>= 3.8), From 165697282e968297f7a2f45375aa5f33035e97e7 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Fri, 21 Jun 2024 13:25:11 +0200 Subject: [PATCH 30/33] Use Podman instead of Docker in release.sh This makes it work without requiring sudo. --- release.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/release.sh b/release.sh index 1d2e33926..7982915f1 100755 --- a/release.sh +++ b/release.sh @@ -107,7 +107,7 @@ cd "BenchExec-$VERSION" dh_make -p "benchexec_$VERSION" --createorig -f "../$TAR" -i -c apache || true dpkg-buildpackage --build=source -sa "--sign-key=$DEBKEY" -sudo docker run --rm -w "$(pwd)" -v "$TEMP_DEB:$TEMP_DEB:rw" ubuntu:20.04 bash -c ' +podman run --rm -w "$(pwd)" -v "$TEMP_DEB:$TEMP_DEB:rw" ubuntu:20.04 bash -c ' apt-get update apt-get install -y --no-install-recommends dpkg-dev TZ=UTC DEBIAN_FRONTEND=noninteractive apt-get install -y $(dpkg-checkbuilddeps 2>&1 | grep -o "Unmet build dependencies:.*" | cut -d: -f2- | sed "s/([^)]*)//g") @@ -115,7 +115,7 @@ sudo docker run --rm -w "$(pwd)" -v "$TEMP_DEB:$TEMP_DEB:rw" ubuntu:20.04 bash - ' popd cp "$TEMP_DEB/benchexec_$VERSION"{.orig.tar.gz,-1_all.deb,-1.dsc,-1.debian.tar.xz,-1_source.buildinfo,-1_source.changes} "$DIST_DIR" -sudo rm -rf "$TEMP_DEB" +rm -rf "$TEMP_DEB" for f in "$DIST_DIR/BenchExec-$VERSION"*.{whl,tar.gz} "$DIST_DIR/benchexec_$VERSION"*.deb; do gpg --detach-sign -a -u "$DEBKEY" "$f" From 25df61b46d24c701163a84acd8877d4e007276c4 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Fri, 21 Jun 2024 13:36:00 +0200 Subject: [PATCH 31/33] Add Pre-Depends to .deb package as recommended for level 12 --- debian/control | 1 + 1 file changed, 1 insertion(+) diff --git a/debian/control b/debian/control index 725f611dd..798ccc835 100644 --- a/debian/control +++ b/debian/control @@ -18,6 +18,7 @@ Vcs-Browser: https://github.com/sosy-lab/benchexec Package: benchexec Architecture: all +Pre-Depends: ${misc:Pre-Depends} Depends: ${python3:Depends}, python3-pkg-resources, ${misc:Depends}, ucf Recommends: cpu-energy-meter, libseccomp2, lxcfs, python3-coloredlogs, python3-pystemd Description: Framework for Reliable Benchmarking and Resource Measurement From ead3fbaf1ab2b84ee6ea3de165d08baa04a23643 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Thu, 27 Jun 2024 07:50:41 +0200 Subject: [PATCH 32/33] Fix crash in CPAchecker's tool-info module We have a heuristic that checks if CPAchecker is used from source but misses a rebuild. This would crash if broken symlinks or other file-access problems occur. As it is just an optional feature, we can ignore such problems and print a warning. An example where this happened was for example system-wide installation of CPAchecker with the executable being /usr/bin/cpachecker and /usr/src existing. --- benchexec/tools/cpachecker.py | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/benchexec/tools/cpachecker.py b/benchexec/tools/cpachecker.py index 3a30c6b75..07044226f 100644 --- a/benchexec/tools/cpachecker.py +++ b/benchexec/tools/cpachecker.py @@ -69,16 +69,21 @@ def executable(self, tool_locator): # If this is a source checkout of CPAchecker, we heuristically check that # sources are not newer than binaries (cpachecker.jar or files in bin/). - if os.path.isdir(src_dir): - src_mtime = self._find_newest_mtime(src_dir) - - if os.path.isfile(jar_file): - if src_mtime > os.stat(jar_file).st_mtime: - sys.exit("CPAchecker JAR is not uptodate, run 'ant jar'!") - - elif os.path.isdir(cls_dir): - if src_mtime > self._find_newest_mtime(cls_dir): - sys.exit("CPAchecker build is not uptodate, run 'ant'!") + try: + if os.path.isdir(src_dir): + src_mtime = self._find_newest_mtime(src_dir) + + if os.path.isfile(jar_file): + if src_mtime > os.stat(jar_file).st_mtime: + sys.exit("CPAchecker JAR is not uptodate, run 'ant jar'!") + + elif os.path.isdir(cls_dir): + if src_mtime > self._find_newest_mtime(cls_dir): + sys.exit("CPAchecker build is not uptodate, run 'ant'!") + except OSError as e: + logging.warning( + "Could not determine whether CPAchecker needs to be rebuilt: %s", e + ) return executable From 2c4643f56fb2b2d10213a7fd298df3c1d41b28f6 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Thu, 27 Jun 2024 07:54:04 +0200 Subject: [PATCH 33/33] Optimization of CPAchecker's tool-info module We do not need to scan through the src directory of CPAchecker if we are not going to use the information anyway. So check this first. --- benchexec/tools/cpachecker.py | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/benchexec/tools/cpachecker.py b/benchexec/tools/cpachecker.py index 07044226f..041f24879 100644 --- a/benchexec/tools/cpachecker.py +++ b/benchexec/tools/cpachecker.py @@ -70,14 +70,17 @@ def executable(self, tool_locator): # If this is a source checkout of CPAchecker, we heuristically check that # sources are not newer than binaries (cpachecker.jar or files in bin/). try: - if os.path.isdir(src_dir): + has_jar = os.path.isfile(jar_file) + has_cls = os.path.isdir(cls_dir) + + if os.path.isdir(src_dir) and (has_jar or has_cls): src_mtime = self._find_newest_mtime(src_dir) - if os.path.isfile(jar_file): + if has_jar: if src_mtime > os.stat(jar_file).st_mtime: sys.exit("CPAchecker JAR is not uptodate, run 'ant jar'!") - elif os.path.isdir(cls_dir): + elif has_cls: if src_mtime > self._find_newest_mtime(cls_dir): sys.exit("CPAchecker build is not uptodate, run 'ant'!") except OSError as e: