feat(testcomp): BenchExec packaging, and always emit a test suite (H1.4)

.github/workflows/ci.yml

@@ -499,6 +499,10 @@ jobs:
               apt-get update -qq
               apt-get install -y -qq python3-pip zip gcc lcov
               pip3 install --quiet testcov
+              # The tool-info module is what BenchExec loads on competition
+              # infrastructure. Nothing else here exercises it, and a wrong one
+              # only shows up days after submission as every task erroring out.
+              python3 tests/integration/test_benchexec_toolinfo.py
               bash tests/testcomp/run_testcov_suite.sh
             '
 

docs/TESTCOMP-CHECKLIST.md

@@ -23,8 +23,8 @@ evidência que sustenta o estado declarado.
 |---|---|---|
 | **H1.1** Emissor de test suite XML | ✅ | `modules/frontend/test_suite/`. `--generate-test-suite` emite `metadata.xml` + `testcase-N.xml` no formato de intercâmbio. 13 testes unitários + 12 asserções de integração. **Custo real muito abaixo das 2 pw estimadas**: o runtime já registrava os valores em ordem de consumo, faltava só serializar |
 | **H1.2** Conversor ktest→XML | ✅ | **Colapsou dentro do H1.1.** O log é escrito pelo binário instrumentado em tempo de execução, então já carrega os valores concretos do KLEE. Não precisou de conversor separado |
-| **H1.3** Conversor corpus-LibFuzzer→XML | 🟡 | O emissor é agnóstico de engine por construção (`NonDetGeneratorLibFuzzy.c:47` descarrega o mesmo log). **Falta:** log por input, para suítes com múltiplos test cases |
-| **H1.4** Empacotamento BenchExec / fm-tools | ⬜ | `utils/moduleBenchExec/map2check.py` existe mas usa a API `BaseTool` (1.x, obsoleta; hoje é `BaseTool2`) e é voltado a verificação SV-COMP, não a geração de testes |
+| **H1.3** Conversor corpus-LibFuzzer→XML | 🟡 | O emissor é agnóstico de engine por construção (`NonDetGeneratorLibFuzzy.c:47` descarrega o mesmo log). **Falta:** log por input, para suítes com múltiplos test cases. **É o gargalo declarado**: bloqueia H2.5 e é o motivo pelo qual o tool-info recusa `cover-branches` |
+| **H1.4** Empacotamento BenchExec / fm-tools | ✅ | `utils/moduleBenchExec/map2check_testcomp.py` (`BaseTool2`) + `utils/map2check-testcomp-wrapper.py`, ambos no zip de release. 15 asserções contra o benchexec real em `tests/integration/test_benchexec_toolinfo.py`. **Falta:** registrar em `fm-tools` (fora deste repositório). O `map2check.py` SV-COMP segue em `BaseTool` 1.x — obsoleto mas ainda presente no benchexec 3.35, então não está morto |
 | **H1.5** E2E no CI com TestCov | ✅ | Job `Test-Comp Validation (TestCov)`, 6/6 contra manifesto medido. Ver `tests/testcomp/` |
 
 ## H2 — Eficácia
@@ -35,7 +35,7 @@ evidência que sustenta o estado declarado.
 | **H2.2** Orquestração com time-slicing | ⬜ | Default híbrido atual (LibFuzzer 0.2× → KLEE 0.8×) preservado |
 | **H2.3** Seed exchange fuzzer↔KLEE | ⬜ | — |
 | **H2.4** Slicing pré-simbólico | ⬜ | Ver nota de prioridade abaixo |
-| **H2.5** Modo Cover-Branches | ⬜ | Bloqueado por H1.3 (log por input) |
+| **H2.5** Modo Cover-Branches | ⬜ | Bloqueado por H1.3 (log por input). O módulo tool-info **recusa** a propriedade em vez de aceitá-la e pontuar zero |
 
 ### Nota de prioridade sobre H2
 
@@ -110,7 +110,7 @@ Todos com evidência em [findings](reports/2026-08-12-castle-juliet-findings.md)
 | O quê | Contagem |
 |---|---|
 | `ctest` (unitários) | 8 |
-| Integração | 82 asserções em 8 scripts |
+| Integração | 97 asserções em 9 scripts |
 | Conformidade Test-Comp | 6 programas |
 | Jobs de CI | 10, todos verdes na PR #59 (o 10º builda a imagem no próprio PR) |
 

modules/frontend/map2check.cpp

@@ -108,10 +108,7 @@ std::string resolveSpecification(const std::string &propertyFile,
 void emitTestSuite(const std::string &outputDir, const std::string &programFile,
                    const std::string &entryFunction,
                    const std::string &architecture,
-                   const std::string &specification, bool coversError) {
-  std::vector<std::string> inputs =
-      Map2Check::readNonDetLog(Map2Check::kleeLogCSV);
-
+                   const std::string &specification, bool foundViolation) {
   Map2Check::TestSuiteMetadata metadata;
   metadata.producer = std::string("Map2Check ") + Map2CheckVersion;
   metadata.specification = specification;
@@ -127,7 +124,19 @@ void emitTestSuite(const std::string &outputDir, const std::string &programFile,
                             outputDir);
     return;
   }
-  if (!writer.writeTestCase(inputs, coversError)) {
+  // No violation means no test case, but the suite still has to exist. A
+  // missing test-suite/ directory reads to the competition harness as a tool
+  // that crashed; a suite carrying metadata and zero test cases says the tool
+  // ran and found nothing, which is a legitimate and scoreable outcome.
+  if (!foundViolation) {
+    Map2Check::Log::Info("Test suite written to " + outputDir +
+                         " (no violation found -- 0 test cases)");
+    return;
+  }
+
+  std::vector<std::string> inputs =
+      Map2Check::readNonDetLog(Map2Check::kleeLogCSV);
+  if (!writer.writeTestCase(inputs, true)) {
     Map2Check::Log::Warning("could not write test case to " + outputDir);
     return;
   }
@@ -421,18 +430,25 @@ int map2check_execution(map2check_args args) {
     if (args.generateTestCase) counterExample->generateTestCase();
     if (args.generateWitness)
       generate_witness(args.inputFile, propertyViolated, args.spectTrue);
-    if (args.generateTestSuite) {
-      // Relative paths resolve against the directory map2check was invoked
-      // from, not the scratch directory the pipeline chdir'd into -- the suite
-      // has to outlive cleanGarbage().
-      std::string outputDir = args.testSuiteDir;
-      if (!fs::path(outputDir).is_absolute()) {
-        outputDir = caller->getOriginalPath() + "/" + outputDir;
-      }
-      emitTestSuite(outputDir, caller->c_program_fullpath, args.entryFunction,
-                    args.architecture,
-                    resolveSpecification(args.propertyFile, args.mode), true);
+  }
+
+  // Emitted for every outcome, not only for a violation. Test-Comp scores the
+  // suite, and a run that decides nothing still has to hand one over: the
+  // competition harness reads an absent test-suite/ as a crashed tool rather
+  // than as an empty result. The `foundViolation` flag decides whether the
+  // suite carries a test case, not whether the suite exists.
+  if (args.generateTestSuite) {
+    // Relative paths resolve against the directory map2check was invoked
+    // from, not the scratch directory the pipeline chdir'd into -- the suite
+    // has to outlive cleanGarbage().
+    std::string outputDir = args.testSuiteDir;
+    if (!fs::path(outputDir).is_absolute()) {
+      outputDir = caller->getOriginalPath() + "/" + outputDir;
     }
+    emitTestSuite(outputDir, caller->c_program_fullpath, args.entryFunction,
+                  args.architecture,
+                  resolveSpecification(args.propertyFile, args.mode),
+                  foundViolation);
   }
 
   // (6) Clean map2check execution (folders and temp files)

scripts/package-release.sh

@@ -13,8 +13,14 @@ cd "$REPO_ROOT"
   exit 1
 }
 
-# Composição do artefato: wrapper SV-COMP + licença + documentação
+# Composição do artefato: wrappers 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
+# 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

@@ -0,0 +1,155 @@
+#!/usr/bin/env python3
+"""The BenchExec tool-info contract for Test-Comp.
+
+Map2Check cannot be submitted to Test-Comp 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.
+
+Run with: python3 tests/integration/test_benchexec_toolinfo.py
+Requires: pip3 install benchexec (already present wherever testcov is).
+"""
+
+import os
+import sys
+import tempfile
+
+REPO = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
+sys.path.insert(0, os.path.join(REPO, "utils", "moduleBenchExec"))
+
+import benchexec.result as result                       # noqa: E402
+import benchexec.tools.template as template             # noqa: E402
+import benchexec.util as util                           # noqa: E402
+
+import map2check_testcomp                               # noqa: E402
+
+PASSED = 0
+FAILED = 0
+
+
+def ok(what):
+    global PASSED
+    print("  PASS %s" % what)
+    PASSED += 1
+
+
+def fail(what, why):
+    global FAILED
+    print("  FAIL %s: %s" % (what, why))
+    FAILED += 1
+
+
+def check(what, condition, why=""):
+    ok(what) if condition else fail(what, why)
+
+
+def raises(what, fn, exc=template.UnsupportedFeatureException):
+    try:
+        fn()
+    except exc:
+        ok(what)
+    except Exception as other:                          # noqa: BLE001
+        fail(what, "raised %s instead of %s" % (type(other).__name__, exc.__name__))
+    else:
+        fail(what, "did not raise")
+
+
+def write(directory, name, text):
+    path = os.path.join(directory, name)
+    with open(path, "w") as handle:
+        handle.write(text)
+    return path
+
+
+def run_with(exit_value):
+    return template.BaseTool2.Run(
+        cmdline=["map2check"],
+        exit_code=util.ProcessExitCode(raw=exit_value << 8, value=exit_value, signal=None),
+        output=[],
+        termination_reason=None,
+    )
+
+
+def main():
+    tool = map2check_testcomp.Tool()
+
+    print("=== BenchExec tool-info (Test-Comp) ===")
+
+    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())
+
+    work = tempfile.mkdtemp()
+    cover_error = write(work, "coverage-error-call.prp",
+                        "COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )\n")
+    cover_branches = write(work, "coverage-branches.prp",
+                           "COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )\n")
+    unreachability = write(work, "unreach-call.prp",
+                           "CHECK( init(main()), LTL(G ! call(reach_error())) )\n")
+    program = write(work, "prog.c", "int main(void) { return 0; }\n")
+
+    limits = template.BaseTool2.ResourceLimits(walltime=900)
+
+    # --- cover-error: the one property Map2Check claims to support -----------
+    task = template.BaseTool2.Task.with_files([program], property_file=cover_error)
+    cmd = tool.cmdline("/opt/m2c/map2check-testcomp-wrapper.py", [], 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.
+    raises("cover-branches is refused rather than faked",
+           lambda: tool.cmdline("x", [], template.BaseTool2.Task.with_files(
+               [program], property_file=cover_branches), limits))
+    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))
+    raises("a task with no property file is refused",
+           lambda: tool.cmdline("x", [], template.BaseTool2.Task.with_files(
+               [program]), limits))
+
+    # --- 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)
+
+    print("  ---")
+    print("  Results: %d passed, %d failed" % (PASSED, FAILED))
+    return 1 if FAILED else 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())