feat(testcomp): one wrapper and one tool-info module for SV-COMP and Test-Comp

docs/reports/tacas-experiment-log.md

@@ -988,3 +988,41 @@ com 300 s.
 - **Campanha:** em 13/10 às 00h43, o `v99c-campaign.sh` iniciou as 256 Intel-TDX `SKIPPED`
   no `install_v99c` (`v99c-ce-tdx-s0/1`). O Cover-Branches (4 shards, 3 500 tarefas,
   `install_v99c`) começa sozinho quando todo o CE terminar.
+
+## Um módulo tool-info só: o Test-Comp dentro do `map2check.py` (2026-10-26)
+
+**Motivação:** a revisão do benchexec#1352 (Philipp Wendler) e do fm-tools!1245 (Dirk Beyer)
+pediu que o suporte ao Test-Comp entrasse no módulo `benchexec/tools/map2check.py` que já
+existe, em vez de um `map2check-testcomp.py` à parte.
+
+**Mudança:**
+- `utils/map2check-wrapper.py` passa a ser o único wrapper. Ele despacha pela propriedade:
+  `COVER(...)` gera testes e termina com a linha `DONE`; `CHECK(...)` segue o caminho
+  SV-COMP de antes.
+- O wrapper agora usa o caminho absoluto do binário e repassa o `--data-model` também no
+  modo SV-COMP.
+- O `utils/map2check-testcomp-wrapper.py` e o `utils/moduleBenchExec/map2check_testcomp.py`
+  saem.
+- O módulo (cópia do upstream editado) faz quatro coisas novas:
+  - reconhece `DONE` como `RESULT_DONE`;
+  - troca o `assert` por `UnsupportedFeatureException`;
+  - passa `--data-model` e `--budget` só se `--version` do wrapper indicar v9 ou mais,
+    porque os wrappers v7 do SV-COMP 2018–2020 rejeitam essas flags;
+  - mantém o `working_directory` do upstream (diretório da ferramenta). Os `resultfiles`
+    são resolvidos relativos a ele, então a `test-suite/` é coletada.
+
+**Verificação:**
+- `tests/integration/test_benchexec_toolinfo.py`: 24/24. O teste cobre as versões v9, v7 e
+  sem versão, os veredictos do SV-COMP e DONE/ERROR/TIMEOUT.
+- Pacote regenerado do `install_v99c` (99 MB, 641 arquivos) e execução real do BenchExec
+  (`tests/testcomp/official/run.sh`), 120 s e 4 GB, em `simple_2-2` e `gcd_1` (ILP32):
+
+| propriedade | tarefa | status | casos | arquitetura no metadata |
+|---|---|---|---|---|
+| Cover-Error | simple_2-2 | done | 2 | 32bit |
+| Cover-Branches | simple_2-2 | done | 50 | 32bit |
+| Cover-Branches | gcd_1 | done | 7 | 32bit |
+
+- `32bit` mostra que o `--data-model ILP32` chegou ao wrapper (o padrão dele é LP64).
+- TestCov (gcc, formatado e não formatado) na suíte do Cover-Error de `simple_2-2`: `true`
+  nos dois, ou seja, a suíte pontua.

scripts/package-release.sh

@@ -13,14 +13,13 @@ cd "$REPO_ROOT"
   exit 1
 }
 
-# Composição do artefato: wrappers SV-COMP e Test-Comp + licença + documentação.
+# Composição do artefato: wrapper (SV-COMP e Test-Comp) + licença + documentação.
 #
-# O wrapper do Test-Comp entra aqui porque o módulo tool-info
-# (utils/moduleBenchExec/map2check_testcomp.py) o declara em REQUIRED_PATHS: o
+# O wrapper entra aqui porque o módulo tool-info
+# (utils/moduleBenchExec/map2check.py) o declara em REQUIRED_PATHS: o
 # BenchExec copia exatamente esses caminhos para o nó de execução, então um
 # arquivo ausente do zip vira um erro na infraestrutura da competição, não aqui.
 cp utils/map2check-wrapper.py release/
-cp utils/map2check-testcomp-wrapper.py release/
 cp LICENSE README.md release/
 
 ZIP="map2check-v${VERSION}-linux-x86_64.zip"

tests/integration/test_benchexec_toolinfo.py

@@ -1,13 +1,19 @@
 #!/usr/bin/env python3
-"""The BenchExec tool-info contract for Test-Comp.
+"""The BenchExec tool-info contract, for SV-COMP and Test-Comp.
 
-Map2Check cannot be submitted to Test-Comp without a tool-info module that
+Map2Check cannot be submitted to a competition without a tool-info module that
 BenchExec accepts, and the failure mode of a wrong one is nasty: it surfaces on
 competition infrastructure, days after submission, as every task erroring out.
 Nothing else in this repository exercises that module, so this file does --
 against the real benchexec package, not a stub, because the whole risk is that
 the API is not what we assumed.
 
+There is one module, utils/moduleBenchExec/map2check.py, a copy of
+benchexec/tools/map2check.py: the BenchExec maintainers asked for Test-Comp
+support to live in the existing module rather than in a second one
+(sosy-lab/benchexec#1352). So the old archives must keep working with it too:
+the v7 wrapper of SV-COMP 2018-2020 rejects --data-model and --budget.
+
 Run with: python3 tests/integration/test_benchexec_toolinfo.py
 Requires: pip3 install benchexec (already present wherever testcov is).
 """
@@ -23,7 +29,7 @@
 import benchexec.tools.template as template             # noqa: E402
 import benchexec.util as util                           # noqa: E402
 
-import map2check_testcomp                               # noqa: E402
+import map2check                                        # noqa: E402
 
 PASSED = 0
 FAILED = 0
@@ -63,26 +69,46 @@ def write(directory, name, text):
     return path
 
 
-def run_with(exit_value):
+def fake_tool(version):
+    """A tool directory whose wrapper only answers --version."""
+    directory = tempfile.mkdtemp()
+    wrapper = write(directory, "map2check-wrapper.py",
+                    "#!/bin/sh\necho %s\n" % version)
+    os.chmod(wrapper, 0o755)
+    tool = map2check.Tool()
+    executable = tool.executable(template.BaseTool2.ToolLocator(
+        tool_directory=directory, use_path=False, use_current=False))
+    return tool, executable
+
+
+def run_with(exit_value, output, termination_reason=None):
+    if exit_value is None:
+        exit_code = util.ProcessExitCode(raw=9, value=None, signal=9)
+    else:
+        exit_code = util.ProcessExitCode(raw=exit_value << 8, value=exit_value, signal=None)
     return template.BaseTool2.Run(
-        cmdline=["map2check"],
-        exit_code=util.ProcessExitCode(raw=exit_value << 8, value=exit_value, signal=None),
-        output=[],
-        termination_reason=None,
+        cmdline=["map2check-wrapper.py"],
+        exit_code=exit_code,
+        output=template.BaseTool2.RunOutput(output),
+        termination_reason=termination_reason,
     )
 
 
 def main():
-    tool = map2check_testcomp.Tool()
+    print("=== BenchExec tool-info (SV-COMP and Test-Comp) ===")
 
-    print("=== BenchExec tool-info (Test-Comp) ===")
+    tool, executable = fake_tool("v9.0.0-Songbirds:2026-10-13")
 
     check("the module is a BaseTool2, not the deprecated BaseTool",
           isinstance(tool, template.BaseTool2))
     check("the tool names itself Map2Check", tool.name() == "Map2Check",
           "got %r" % tool.name())
     check("the tool publishes a project URL",
           tool.project_url().startswith("https://"), tool.project_url())
+    check("the wrapper is the executable, not the raw binary",
+          executable.endswith("map2check-wrapper.py"), executable)
+    check("the archive paths include the wrapper",
+          "map2check-wrapper.py" in tool.program_files(executable))
 
     work = tempfile.mkdtemp()
     cover_error = write(work, "coverage-error-call.prp",
@@ -95,65 +121,81 @@ def main():
 
     limits = template.BaseTool2.ResourceLimits(walltime=900)
 
-    # --- cover-error: the one property Map2Check claims to support -----------
+    # --- Map2Check 9: the task options reach the wrapper ---------------------
     task = template.BaseTool2.Task.with_files([program], property_file=cover_error)
-    cmd = tool.cmdline("/opt/m2c/map2check-testcomp-wrapper.py", [], task, limits)
+    cmd = tool.cmdline(executable, [], task, limits)
 
-    check("the wrapper is the executable, not the raw binary",
-          cmd[0].endswith("map2check-testcomp-wrapper.py"), cmd[0])
     check("the property file is passed through",
           "-p" in cmd and cmd[cmd.index("-p") + 1] == cover_error)
     check("the program is the last argument", cmd[-1] == program, cmd[-1])
     check("the walltime limit becomes the tool's own budget",
           "--budget" in cmd and cmd[cmd.index("--budget") + 1] == "900")
-    check("LP64 is the default machine model",
-          "--data-model" in cmd and cmd[cmd.index("--data-model") + 1] == "LP64")
-
-    # --- the machine model has to come from the task, not a guess ------------
-    task32 = template.BaseTool2.Task.with_files(
-        [program], property_file=cover_error, options={"data_model": "ILP32"})
-    cmd32 = tool.cmdline("/opt/m2c/map2check-testcomp-wrapper.py", [], task32, limits)
-    check("a task declaring ILP32 is honoured",
-          cmd32[cmd32.index("--data-model") + 1] == "ILP32")
-
-    # --- unsupported inputs must be refused, not quietly mishandled ----------
-    # A tool-info that accepts cover-branches would produce runs that score
-    # zero while looking like participation. Refusing makes BenchExec skip.
+    check("a task without a data model leaves the wrapper's default (LP64)",
+          "--data-model" not in cmd, cmd)
+
+    # The machine model has to come from the task, not a guess. BenchExec only
+    # reads it from a task that declares its language, as sv-benchmarks do.
+    for model in ("ILP32", "LP64"):
+        task_model = template.BaseTool2.Task.with_files(
+            [program], property_file=cover_error,
+            options={"language": "C", "data_model": model})
+        cmd_model = tool.cmdline(executable, [], task_model, limits)
+        check("a task declaring %s is honoured" % model,
+              "--data-model" in cmd_model
+              and cmd_model[cmd_model.index("--data-model") + 1] == model, cmd_model)
+
     # cover-branches used to be refused, because there was no source of
-    # per-path vectors. KLEE's .ktest output is now that source, so the module
-    # must accept it -- and a regression to the refusal would silently drop a
-    # whole competition category.
-    cmd_branches = tool.cmdline("/opt/m2c/map2check-testcomp-wrapper.py", [],
-                                template.BaseTool2.Task.with_files(
-                                    [program], property_file=cover_branches),
-                                limits)
-    check("cover-branches is accepted", cmd_branches[-1] == program)
+    # per-path vectors. KLEE's .ktest output is now that source, so a
+    # regression to the refusal would silently drop a whole category.
+    cmd_branches = tool.cmdline(executable, [], template.BaseTool2.Task.with_files(
+        [program], property_file=cover_branches), limits)
     check("cover-branches passes its own property file",
           cmd_branches[cmd_branches.index("-p") + 1] == cover_branches)
 
-    raises("an SV-COMP CHECK property is refused by the Test-Comp module",
-           lambda: tool.cmdline("x", [], template.BaseTool2.Task.with_files(
-               [program], property_file=unreachability), limits))
+    # One module now: an SV-COMP property is the wrapper's business, not a
+    # reason for the module to refuse the task.
+    cmd_check = tool.cmdline(executable, [], template.BaseTool2.Task.with_files(
+        [program], property_file=unreachability), limits)
+    check("an SV-COMP CHECK property is accepted", cmd_check[-1] == program)
+
     raises("a task with no property file is refused",
-           lambda: tool.cmdline("x", [], template.BaseTool2.Task.with_files(
+           lambda: tool.cmdline(executable, [], template.BaseTool2.Task.with_files(
                [program]), limits))
 
+    # --- older archives: no options their wrapper would reject --------------
+    old_tool, old_executable = fake_tool("v7.3.1-Flock")
+    old_cmd = old_tool.cmdline(old_executable, [], task, limits)
+    check("a Map2Check 7 wrapper gets neither --data-model nor --budget",
+          "--data-model" not in old_cmd and "--budget" not in old_cmd, old_cmd)
+    check("a Map2Check 7 command line is unchanged",
+          old_cmd == [old_executable, "-p", cover_error, program], old_cmd)
+
+    silent_tool, silent_executable = fake_tool("")
+    silent_cmd = silent_tool.cmdline(silent_executable, [], task, limits)
+    check("a wrapper that does not tell its version gets no new options",
+          "--budget" not in silent_cmd, silent_cmd)
+
     # --- determine_result ----------------------------------------------------
-    check("a clean exit is DONE",
-          tool.determine_result(run_with(0)) == result.RESULT_DONE)
-    check("a failing exit is ERROR",
-          tool.determine_result(run_with(1)) == result.RESULT_ERROR)
-
-    # A timeout is DONE because the wrapper budgets itself below the harness
-    # limit and writes the suite before returning.
-    timed_out = template.BaseTool2.Run(
-        cmdline=["map2check"],
-        exit_code=util.ProcessExitCode(raw=9, value=None, signal=9),
-        output=[],
-        termination_reason="walltime",
-    )
-    check("a timeout still counts as DONE, because the suite was written",
-          tool.determine_result(timed_out) == result.RESULT_DONE)
+    check("DONE as the last line is DONE",
+          tool.determine_result(run_with(0, ["Test suite in /x/test-suite", "DONE"]))
+          == result.RESULT_DONE)
+    check("a failed generation is ERROR",
+          tool.determine_result(run_with(1, ["ERROR: no test-suite/ directory was produced"]))
+          == "ERROR")
+    check("a crashed map2check is ERROR, not DONE",
+          tool.determine_result(run_with(2, ["Test suite in /x/test-suite",
+                                             "ERROR: map2check exited with 2"]))
+          == "ERROR")
+    check("a run killed by the harness is TIMEOUT",
+          tool.determine_result(run_with(None, ["Generating tests with MAP2CHECK"],
+                                         termination_reason="walltime"))
+          == result.RESULT_TIMEOUT)
+    check("SV-COMP verdicts are untouched: TRUE",
+          tool.determine_result(run_with(0, ["TRUE"])) == result.RESULT_TRUE_PROP)
+    check("SV-COMP verdicts are untouched: FALSE_DEREF",
+          tool.determine_result(run_with(0, ["FALSE_DEREF"])) == result.RESULT_FALSE_DEREF)
+    check("SV-COMP verdicts are untouched: FALSE",
+          tool.determine_result(run_with(0, ["FALSE"])) == result.RESULT_FALSE_REACH)
 
     print("  ---")
     print("  Results: %d passed, %d failed" % (PASSED, FAILED))

tests/integration/test_exit_codes.sh

@@ -5,9 +5,10 @@
 # three call sites, so the exit code was always 0 (or SIGABRT from the
 # --expected-result path). Two consequences:
 #
-#   1. The Test-Comp tool-info (utils/moduleBenchExec/map2check_testcomp.py)
-#      decides DONE vs ERROR from `exit_code == 0`, so an internally failed run
-#      was reported DONE.
+#   1. The Test-Comp tool-info (then utils/moduleBenchExec/map2check_testcomp.py)
+#      decided DONE vs ERROR from `exit_code == 0`, so an internally failed run
+#      was reported DONE. The wrapper now prints DONE only for an exit code it
+#      accepts, so the exit code still decides.
 #   2. --expected-result signalled a wrong answer with abort() (SIGABRT, 134),
 #      which BenchExec reads as "the tool crashed" -- the opposite of the truth.
 #

tests/testcomp/official/bench-defs/map2check.xml

@@ -4,8 +4,8 @@
      is no map2check.xml in the testcomp26 tag. Modelled on the definitions of
      the tools that are there (klee.xml, fusebmc.xml, symbiotic.xml): the same
      limits, the same result files and the same run definitions. The tool-info
-     module is utils/moduleBenchExec/map2check_testcomp.py. -->
-<benchmark tool="moduleBenchExec.map2check_testcomp" displayName="Map2Check" timelimit="15 min" memlimit="15 GB" cpuCores="4">
+     module is utils/moduleBenchExec/map2check.py. -->
+<benchmark tool="moduleBenchExec.map2check" displayName="Map2Check" timelimit="15 min" memlimit="15 GB" cpuCores="4">
 
   <require cpuModel="Intel Xeon E3-1230 v5 @ 3.40 GHz" />
 

tests/testcomp/run_testcomp_evaluation.sh

@@ -92,6 +92,16 @@ case "$PROPERTY" in
 esac
 
 mkdir -p "$RESULTS_DIR/raw"
+
+# Per-task work directories live under one root per results dir and shard, and
+# the root is emptied on start. A task killed by a reboot never reaches the
+# rm -rf at the end of the loop, so its directory -- KLEE output included, up to
+# 4 GB each -- used to stay in /tmp for good. Over the V99c campaign, a handful
+# of reboots left 11 GB in one container and filled the Windows disk under WSL.
+# Only this shard writes here, so nothing that is still running gets swept.
+WORK_ROOT="${TMPDIR:-/tmp}/m2c-eval.$(basename "$RESULTS_DIR").s$SHARD"
+rm -rf "$WORK_ROOT"
+mkdir -p "$WORK_ROOT"
 CSV="$RESULTS_DIR/results.csv"
 if [ ! -f "$CSV" ]; then
   echo "category,program,data_model,expected_unreach,verdict,testcov,coverage,goals,n_tests,elapsed_s" > "$CSV"
@@ -137,7 +147,7 @@ while IFS=$'\t' read -r category program data_model expected <&3; do
   # A private directory per task. map2check names its scratch by the hash of the
   # input, so two tasks with identical content would otherwise share -- and a
   # directory left behind by an aborted run would be reused with stale contents.
-  work=$(mktemp -d)
+  work=$(mktemp -d -p "$WORK_ROOT")
   cp "$src" "$work/" 2>/dev/null || { rm -rf "$work"; continue; }
   cp "$PRP" "$work/prop.prp"
   name=$(basename "$src")