Merge branch 'sosy-lab:main' into btormc-tool-info

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())

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):

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:

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

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).