Keep SV-COMP runs within the competition's memory and CPU budget

CLAUDE.md

@@ -87,6 +87,12 @@ cd targets/sv-comp && ./scripts/svcomp test run --mode parallel --no-witness --c
 
 - **Duration:** a full valid-assert run takes about 40 min with the default 900 s timeout, and
   much longer with `--testcase-timeout-s 3600`. Only compare runs made with the same timeout.
+- **Resource budget:** as in SV-COMP, the explorer and all executor JVMs share one memory and CPU
+  budget (`--memory-limit` MB, default 15000; `--cpu-limit` s, default 900; the harness passes
+  `--testcase-timeout-s` as the CPU limit). The executor heap is derived from the memory limit (a
+  lower cgroup limit wins). Close to a limit the explorer kills the executor run or interrupts the
+  Z3 query in progress; 20 s before the CPU limit it ends with UNKNOWN. Both rule out SAFE, see
+  `symbolic-explorer/svcomp/ResourceBudget.py` and `resources` in `stats.json`.
 - **Output:** results go to `targets/sv-comp/runs/run_<timestamp>/`. Per-task results are in
   `results/results_<prp>_*.json`, and per-task logs (`explorer.log`,
   `Main_main_interprocedural.json`, `stats.json`) are in `logs/<suite>/<task>_<prp>/`.

scripts/svcomp-package/run_swat.py

@@ -11,6 +11,8 @@
 # The explorer writes the violation witness (witness.yml, witness.graphml) here; BenchExec collects
 # it via the `**/witness.*` result-files pattern of the benchmark definition.
 WITNESS_DIR = os.path.join(SCRIPT_DIR, 'witness')
+# The explorer's logs and testcase statistics (stats.json)
+LOG_DIR = os.path.join(SCRIPT_DIR, 'logs')
 
 
 class ExecutionStatus(enum.Enum):
@@ -104,15 +106,14 @@ def generate_command(args, property_file: str, property_path: str, input_paths:
     agent_path = os.path.join(SCRIPT_DIR, 'symbolic-executor', 'lib', 'symbolic-executor.jar')
     config_path = os.path.join(SCRIPT_DIR, config_file)
     library_path = os.path.join(SCRIPT_DIR, 'libs', 'java-library-path')
-    logging_dir =  os.path.join(SCRIPT_DIR, 'logs')
 
     # Same interpreter (and PYTHONPATH, via the inherited environment) as run-swat.sh set up.
     base_command = [ sys.executable, "-u", os.path.join(SCRIPT_DIR, 'symbolic-explorer', 'SymbolicExplorer.py'),
                      "-prp", property_file,
                      "--agent", agent_path,
                      "--config", config_path,
                      "-z3", library_path,
-                     "--logdir", logging_dir,
+                     "--logdir", LOG_DIR,
                      "--mode", "sv-comp",
                      '--port', "8000",
                      "--witness-dir", WITNESS_DIR,
@@ -149,20 +150,6 @@ def compile_target(args, local_target_dir):
     log_output(output)
 
 
-def extract_last_round(out, marker="============================== ROUND"):
-
-    return "\n ".join(out).split(marker)[-1]
-
-
-def extract_markers(out, markers):
-    if isinstance(markers, str):
-        markers = (markers,)
-    res = []
-    for line in out.split("\n"):
-        if any(marker in line for marker in markers):
-            res.append(line)
-    return res
-
 def swat_version():
     """The package version from BUILD_INFO.txt, written by scripts/package-svcomp.sh."""
     try:
@@ -221,29 +208,41 @@ def log_output(output: List[str]):
     cmd = generate_command(sys.argv[1:], property_file, property_path, input_paths)
     # Exactly one witness per run: drop whatever an earlier run left behind
     shutil.rmtree(WITNESS_DIR, ignore_errors=True)
+    if os.path.exists(os.path.join(LOG_DIR, 'stats.json')):
+        os.remove(os.path.join(LOG_DIR, 'stats.json'))
     local_target_dir = copy_target(target_dir)
     compile_target(sys.argv[1:], local_target_dir)
 
     path = local_target_dir
     log_dir = f'{path}/logs'
 
     cmd[-1] = os.path.join(SCRIPT_DIR, local_target_dir, 'build') #f"{local_target_dir}/build"
+    # The CPU time limit covers the whole run, so the explorer's budget starts with what copying
+    # and compiling the task took (the memory and CPU limits are the explorer's defaults).
+    t = os.times()
+    cmd[cmd.index('--classpath'):cmd.index('--classpath')] = [
+        '--cpu-used', f'{t.user + t.system + t.children_user + t.children_system:.1f}']
     #delete the dir if it exists
     if os.path.exists(log_dir):
         os.system(f'rm -rf {log_dir}')
     os.makedirs(log_dir)
     with pushd(path):
-        execution_status, output = run_command_with_timeout(cmd)
-        log_output(output)
-        print(f"Execution status: {execution_status}")
-        if execution_status == ExecutionStatus.TIMEOUT or execution_status == ExecutionStatus.ERROR:
-            print(f'Error: {output}')
-            exit(1)
-
-
-        out = extract_last_round(output)
-        verdict = extract_markers(out, f'[VERDICT {property_file}]')
-        if "== ERROR" in str(verdict):
+        # The explorer's output goes straight to ours: on long runs it is hundreds of MB, and
+        # collecting and re-logging it here took tens of seconds of CPU time and as much memory,
+        # after the explorer had already stopped in time for the limits.
+        logger.info(f'[TARGET EXECUTION]: Running command: {cmd}')
+        sys.stdout.flush()
+        sys.stderr.flush()
+        returncode = subprocess.run(cmd, stderr=subprocess.STDOUT).returncode
+        print(f"Execution status: {returncode}")
+
+        # The explorer records its verdict in the testcase statistics
+        try:
+            with open(os.path.join(LOG_DIR, 'stats.json')) as f:
+                verdict = json.load(f)['verdict_raw']
+        except (OSError, ValueError, KeyError):
+            verdict = None
+        if verdict == Verdict.VIOLATION.value:
             # The explorer wrote the witness from the trace of the violating execution
             print_witness()
         print(f'Verdict:\n {verdict}')

symbolic-explorer/SymbolicExplorer.py

@@ -139,6 +139,15 @@ def init_args(parser: argparse.ArgumentParser):
     parser.add_argument("--solver-rlimit", type=int, default=0, help="Z3 resource limit (rlimit) for the first query of each branch in sv-comp mode; a branch that runs out is retried later with a growing limit. 0 (default): unlimited")
     parser.add_argument("--parallel-sa", action="store_true", help="Run the static pre-analysis in the background and use it once it is ready (sv-comp mode). By default exploration waits for it: running it in parallel makes runs nondeterministic", default=False)
 
+    # SV-COMP resource budget, shared by the explorer and all executor JVMs (sv-comp mode). The
+    # defaults are the competition's limits (bench-defs swat.xml); a lower cgroup memory limit wins.
+    parser.add_argument("--memory-limit", type=int, default=15000,
+                        help="Memory limit of the whole run in MB (10^6 bytes); the executor heap is derived from it")
+    parser.add_argument("--cpu-limit", type=float, default=900,
+                        help="CPU time limit of the whole run in seconds; exploration stops with UNKNOWN shortly before it")
+    parser.add_argument("--cpu-used", type=float, default=0.0,
+                        help="CPU seconds the run used before the explorer started (e.g. compiling the task)")
+
     # SV-COMP witness arguments: the explorer writes the violation witness from the trace of the
     # violating execution (needs the task's input files and property file as given to the verifier)
     parser.add_argument("--witness-dir", default="witness",
@@ -166,6 +175,11 @@ def init_args(parser: argparse.ArgumentParser):
 
     # Initialize loggers
     log.initialize_loggers(args.logdir)
+    if args.mode == 'sv-comp':
+        # The module loggers' DEBUG/INFO lines on stdout (several per branch and query) were 500 MB
+        # in 900 s on MinePump: CPU time, and memory in a BenchExec container. The explorer's own
+        # log (explorer.log) is not affected.
+        logging.getLogger().setLevel(logging.WARNING)
 
     # Set configuration flags in Database
     from data.Database import Database