diff --git a/benchexec/cgroupsv2.py b/benchexec/cgroupsv2.py index 258d0cce7..11aefcc41 100644 --- a/benchexec/cgroupsv2.py +++ b/benchexec/cgroupsv2.py @@ -102,16 +102,16 @@ def initialize(): cgroup = CgroupsV2.from_system() - if list(cgroup.get_all_tasks()) == [os.getpid()]: + if cgroup.path and list(cgroup.get_all_tasks()) == [os.getpid()]: # If we are the only process, somebody prepared a cgroup for us. Use it. # We might be able to relax this check and for example allow child processes, # but then we would also have to move them to another cgroup, # which might not be a good idea. logging.debug("BenchExec was started in its own cgroup: %s", cgroup) - elif _create_systemd_scope_for_us(): - # If we can create a systemd scope for us and move ourselves in it, - # we have a usable cgroup afterwards. + elif _create_systemd_scope_for_us() or _try_fallback_cgroup(): + # If we can create a systemd scope for us or find a usable fallback cgroup + # and move ourselves in it, we have a usable cgroup afterwards. cgroup = CgroupsV2.from_system() else: @@ -192,6 +192,32 @@ def _create_systemd_scope_for_us(): return False +def _try_fallback_cgroup(): + """ + Attempt to locate a usable fallback cgroup. + If it is found this process is moved into it. + + @return: a boolean indicating whether this succeeded + """ + # Attempt to use /benchexec cgroup. + # If it exists, some deliberately created it for us to use. + # The following does this by just faking a /proc/self/cgroup for this case. + cgroup = CgroupsV2.from_system(["0::/benchexec"]) + if cgroup.path and os.path.isdir(cgroup.path) and not list(cgroup.get_all_tasks()): + logging.debug("Found existing cgroup /benchexec, using it as fallback.") + + # Create cgroup for this execution of BenchExec. + cgroup = cgroup.create_fresh_child_cgroup( + cgroup.subsystems.keys(), prefix="benchexec_" + ) + # Move ourselves to it such that for the rest of the code this looks as usual. + cgroup.add_task(os.getpid()) + + return True + + return False + + def _find_cgroup_mount(): """ Return the mountpoint of the cgroupv2 unified hierarchy. @@ -229,6 +255,12 @@ def _parse_proc_pid_cgroup(cgroup_file): mountpoint = _find_cgroup_mount() for line in cgroup_file: own_cgroup = line.strip().split(":")[2][1:] + if own_cgroup.startswith("../"): + # Our cgroup is outside the root cgroup! + # Happens inside containers with a cgroup namespace + # and an inappropriate cgroup config, such as bind-mounting the host cgroup. + logging.debug("Process is in unusable out-of-tree cgroup '%s'", own_cgroup) + return None path = mountpoint / own_cgroup return path @@ -300,14 +332,17 @@ def __init__(self, subsystems): @classmethod def from_system(cls, cgroup_procinfo=None): - logging.debug( - "Analyzing /proc/mounts and /proc/self/cgroup to determine cgroups." - ) if cgroup_procinfo is None: + logging.debug( + "Analyzing /proc/mounts and /proc/self/cgroup to determine cgroups." + ) cgroup_path = _find_own_cgroups() else: cgroup_path = _parse_proc_pid_cgroup(cgroup_procinfo) + if not cgroup_path: + return cls({}) + try: with open(cgroup_path / "cgroup.controllers") as subsystems_file: subsystems = set(subsystems_file.readline().strip().split()) diff --git a/benchexec/tools/btor2c.py b/benchexec/tools/btor2c.py index 51c7f93f0..36d29f455 100644 --- a/benchexec/tools/btor2c.py +++ b/benchexec/tools/btor2c.py @@ -12,25 +12,28 @@ class Tool(benchexec.tools.template.BaseTool2): """ - Tool info for BTOR2C: A Converter from BTOR2 models to C programs + Tool info for Btor2C: A translator from Btor2 circuits to C programs """ def executable(self, tool_locator): - return tool_locator.find_executable("btor2code", subdir="build") + return tool_locator.find_executable("btor2c", subdir="build") def name(self): - return "BTOR2C" + return "Btor2C" def project_url(self): return "https://gitlab.com/sosy-lab/software/btor2c" + def version(self, executable): + return self._version_from_tool(executable, line_prefix="Btor2C version") + def cmdline(self, executable, options, task, rlimits): return [executable] + options + [task.single_input_file] def get_value_from_output(self, output, identifier): # search for the text in output and get its value, # search the first line, that starts with the searched text - # warn if there are more lines (multiple statistics from sequential analysis?) + # warn if there are more lines match = None for line in output: if line.lstrip().startswith(identifier): diff --git a/benchexec/tools/template.py b/benchexec/tools/template.py index 2309f95dd..35d7de2b2 100644 --- a/benchexec/tools/template.py +++ b/benchexec/tools/template.py @@ -155,6 +155,7 @@ def _version_from_tool( [executable, arg], stdout=subprocess.PIPE, stderr=subprocess.PIPE, + stdin=subprocess.DEVNULL, universal_newlines=True, ) except OSError as e: diff --git a/doc/INSTALL.md b/doc/INSTALL.md index b5c90ce26..3eabb5869 100644 --- a/doc/INSTALL.md +++ b/doc/INSTALL.md @@ -334,20 +334,49 @@ If you want to run BenchExec inside a container, we recommend Podman and systems with cgroups v2. Then use the following command-line arguments: - podman run --security-opt unmask=/sys/fs/cgroup --cgroups=split ... - -This will work if BenchExec is the main process inside the container, -otherwise you need to create an appropriate cgroup hierarchy inside the container, + podman run --security-opt unmask=/sys/fs/cgroup --cgroups=split --security-opt unmask=/proc/* --security-opt seccomp=unconfined ... + +This allows BenchExec to use cgroups and create its own containers inside the Podman container. + +Using Docker is also possible, but only using the `--privileged` argument. +However, this gives your Docker container *full root access* to the host, +so please also add the `--cap-drop=all` flag, +make sure to use this only with trusted images, +and configure your Docker container such that everything in it +is executed under a different user account, not as root. +BenchExec is not designed to run as root and does not provide +any safety guarantees regarding its container under this circumstances. + +For both Podman and Docker this will work +if BenchExec is the main process inside the container, +otherwise you need to manually create an appropriate cgroup hierarchy inside the container, i.e., one where BenchExec has its own separate cgroup. +You can either start BenchExec as the only process in a fresh cgroup +or create an empty cgroup named `/benchexec`, +which BenchExec will then automatically use. +This cgroup should have as many controllers enabled and delegated to sub-cgroups as possible, +for example like this: +``` +mkdir -p /sys/fs/cgroup/benchexec +for controller in $(cat /sys/fs/cgroup/cgroup.controllers); do + echo "+$controller" > /sys/fs/cgroup/cgroup.subtree_control +done +for controller in $(cat /sys/fs/cgroup/benchexec/cgroup.controllers); do + echo "+$controller" > /sys/fs/cgroup/benchexec/cgroup.subtree_control +done +``` +Note that if no other cgroups exist, +you first need to create a different child cgroup +for all existing processes in the container. -For other cases, e.g., with cgroups v1, +For systems with cgroups v1, please use the following command line argument to mount the cgroup hierarchy within the container when starting it (same for Podman): docker run -v /sys/fs/cgroup:/sys/fs/cgroup:rw ... -Note that you additionally need some flags for container mode, +Note that you need some additional flags for container mode, which are explained in the [container documentation](container.md#using-benchexec-in-a-dockerpodman-container). ### Testing Cgroups Setup and Known Problems diff --git a/doc/container.md b/doc/container.md index a01b40b27..72772799e 100644 --- a/doc/container.md +++ b/doc/container.md @@ -185,7 +185,7 @@ because it provides "rootless" containers To use BenchExec within Podman, start it as a regular user (not root) and use the following arguments: ``` -podman run --security-opt unmask=/proc/* --security-opt unmask=/sys/fs/cgroup --security-opt seccomp=unconfined ... +podman run --security-opt unmask=/proc/* --security-opt seccomp=unconfined ... ``` You may additionally need the arguments documented for [cgroup usage](INSTALL.md#setting-up-cgroups-in-a-dockerpodman-container).