diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5d50d53a1..05113123e 100644 --- a/.github/workflows/ci.yml +++ b/.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 ' diff --git a/docs/TESTCOMP-CHECKLIST.md b/docs/TESTCOMP-CHECKLIST.md index 84f9f9e71..a29fa5d54 100644 --- a/docs/TESTCOMP-CHECKLIST.md +++ b/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) | diff --git a/modules/frontend/map2check.cpp b/modules/frontend/map2check.cpp index f092e8cb7..314309176 100644 --- a/modules/frontend/map2check.cpp +++ b/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 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 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) diff --git a/scripts/package-release.sh b/scripts/package-release.sh index a4bedec0a..1021388ed 100755 --- a/scripts/package-release.sh +++ b/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" diff --git a/tests/integration/test_benchexec_toolinfo.py b/tests/integration/test_benchexec_toolinfo.py new file mode 100644 index 000000000..bbb3b768b --- /dev/null +++ b/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()) diff --git a/utils/map2check-testcomp-wrapper.py b/utils/map2check-testcomp-wrapper.py new file mode 100755 index 000000000..54a61723a --- /dev/null +++ b/utils/map2check-testcomp-wrapper.py @@ -0,0 +1,132 @@ +#!/usr/bin/env python3 +"""Test-Comp entry point for Map2Check. + +Separate from map2check-wrapper.py on purpose. That wrapper answers an SV-COMP +question -- "does this program satisfy the property" -- and prints a verdict. +Test-Comp asks a different one: produce a test suite, and let TestCov decide +what it is worth. The verdict vocabulary, the exit codes and the artefact are +all different, and folding both into one script would mean a wrapper whose +behaviour depends on a property string in two unrelated ways. + +Contract with the competition harness: + + * the suite is written to ./test-suite/ in the current working directory + * the suite is written whether or not a violation was found -- an absent + directory reads as a crashed tool, an empty suite as an honest zero + * exit 0 means "I ran"; it does not claim the suite covers anything +""" + +import argparse +import os +import subprocess +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) + +# Resolved against this file rather than "./map2check". BenchExec's BaseTool2 +# dropped the working_directory() hook that the old wrapper relied on, so the +# process starts in the benchmark's directory, not the tool's. map2check itself +# derives MAP2CHECK_PATH from /proc/self/exe, so an absolute path is fine -- +# what is NOT fine is renaming the binary, which makes that derivation produce +# a garbage prefix. +MAP2CHECK = os.path.join(HERE, "map2check") + +# Test-Comp 2026 coverage properties. Matched on the FQL body rather than on +# the file name: the competition names these files differently across years and +# the body is what actually defines the goal. +COVER_ERROR = "COVER EDGES(@CALL(reach_error))" +COVER_BRANCHES = "COVER EDGES(@DECISIONEDGE)" + +# 900s is the Test-Comp per-task budget. The tool gets slightly less so that it +# is Map2Check that stops and writes its suite, rather than the harness killing +# it mid-write and leaving a truncated metadata.xml behind. +DEFAULT_BUDGET = 900 +SHUTDOWN_MARGIN = 20 + + +def parse_args(argv): + parser = argparse.ArgumentParser(add_help=True) + parser.add_argument("-v", "--version", action="store_true", + help="print Map2Check's version") + parser.add_argument("-p", "--propertyfile", help="path to the property file") + parser.add_argument("--data-model", choices=["ILP32", "LP64"], default="LP64", + help="machine model of the task (Test-Comp: ILP32 or LP64)") + parser.add_argument("--budget", type=int, default=DEFAULT_BUDGET, + help="total wall-clock budget in seconds") + parser.add_argument("benchmark", nargs="?", help="path to the C program") + return parser.parse_args(argv) + + +def read_property(path): + with open(path, "r") as handle: + return handle.read() + + +def main(argv): + args = parse_args(argv) + + if args.version: + return subprocess.call([MAP2CHECK, "--version"]) + + if args.propertyfile is None: + print("Please, specify a property file") + return 1 + if args.benchmark is None: + print("Please, specify a benchmark") + return 1 + + prop = read_property(args.propertyfile) + + if COVER_ERROR in prop: + goal_flags = ["--target-function", "--target-function-name", "reach_error"] + elif COVER_BRANCHES in prop: + # Not a silent zero. Branch coverage needs one test case per input + # vector, and the runtime currently writes a single nondet log per run + # (H1.3 in docs/TESTCOMP-CHECKLIST.md). Emitting a one-case suite here + # would look like participation while scoring nothing and hiding why. + print("Unsupported Property: cover-branches needs per-input test cases " + "(see H1.3 in docs/TESTCOMP-CHECKLIST.md)") + return 1 + else: + print("Unsupported Property") + return 1 + + architecture = "32bit" if args.data_model == "ILP32" else "64bit" + + # The inner budget is what Map2Check divides between LibFuzzer and KLEE; the + # outer one is the backstop for a shutdown that hangs. + inner = max(1, args.budget - SHUTDOWN_MARGIN) + + command = [MAP2CHECK] + goal_flags + [ + "--generate-test-suite", + "--property-file", args.propertyfile, + "--architecture", architecture, + "--timeout", str(inner), + args.benchmark, + ] + + print("Verifying with MAP2CHECK") + print("Command: " + " ".join(command)) + sys.stdout.flush() + + try: + completed = subprocess.run(command, timeout=args.budget) + rc = completed.returncode + except subprocess.TimeoutExpired: + print("Timed out") + rc = 0 + + suite = os.path.join(os.getcwd(), "test-suite") + if not os.path.isdir(suite): + # Reported, not repaired. Fabricating a metadata.xml here would hide a + # Map2Check that died before it could write one, and the whole point of + # always emitting the suite is that its absence means something. + print("ERROR: no test-suite/ directory was produced") + return 1 + + print("Test suite in " + suite) + return 0 if rc in (0, 1) else rc + + +if __name__ == "__main__": + sys.exit(main(sys.argv[1:])) diff --git a/utils/moduleBenchExec/map2check_testcomp.py b/utils/moduleBenchExec/map2check_testcomp.py new file mode 100644 index 000000000..63501015c --- /dev/null +++ b/utils/moduleBenchExec/map2check_testcomp.py @@ -0,0 +1,97 @@ +# This file is part of Map2Check . +# +# SPDX-License-Identifier: Apache-2.0 +"""BenchExec tool-info module for Map2Check as a Test-Comp test generator. + +Kept separate from map2check.py, which is the SV-COMP verification adaptor and +still targets the deprecated BaseTool (1.x) API. The two describe genuinely +different tools to BenchExec: one reports a verification verdict, the other +produces an artefact and lets TestCov score it. Merging them would mean a +determine_result whose meaning depends on a property string. +""" + +import benchexec.result as result +import benchexec.tools.template + +# The FQL bodies, matched rather than the file names -- the competition renames +# the property files between editions but the goal expression is what defines +# the task. +COVER_ERROR = "COVER EDGES(@CALL(reach_error))" +COVER_BRANCHES = "COVER EDGES(@DECISIONEDGE)" + + +class Tool(benchexec.tools.template.BaseTool2): + """Tool adaptor for Map2Check (https://github.com/hbgit/Map2Check).""" + + REQUIRED_PATHS = [ + "map2check", + "map2check-testcomp-wrapper.py", + "bin", + "include", + "lib", + ] + + def executable(self, tool_locator): + return tool_locator.find_executable("map2check-testcomp-wrapper.py") + + def name(self): + return "Map2Check" + + def project_url(self): + return "https://github.com/hbgit/Map2Check" + + def version(self, executable): + return self._version_from_tool(executable) + + def program_files(self, executable): + return self._program_files_from_executable(executable, self.REQUIRED_PATHS) + + def cmdline(self, executable, options, task, rlimits): + if task.property_file is None: + raise benchexec.tools.template.UnsupportedFeatureException( + "Map2Check needs a property file to know what to cover" + ) + + with open(task.property_file, "r") as handle: + spec = handle.read() + + if COVER_BRANCHES in spec: + # Declared, not faked. Branch coverage needs one test case per input + # vector and the runtime writes one nondet log per run (H1.3 in + # docs/TESTCOMP-CHECKLIST.md). Raising here makes BenchExec skip the + # task instead of recording a run that could only ever score zero. + raise benchexec.tools.template.UnsupportedFeatureException( + "cover-branches is not supported yet: it needs per-input test " + "cases (H1.3)" + ) + if COVER_ERROR not in spec: + raise benchexec.tools.template.UnsupportedFeatureException( + "unsupported property: " + spec.strip() + ) + + # LP64 is the Test-Comp default when a task definition says nothing. + data_model = (task.options or {}).get("data_model", "LP64") + + cmd = [executable, "-p", task.property_file, "--data-model", data_model] + if rlimits.walltime: + # Handing the tool its own budget is what lets it stop and finish + # writing the suite. Left to the harness's kill, metadata.xml can be + # truncated mid-write, which is worse than an empty suite. + cmd += ["--budget", str(rlimits.walltime)] + return cmd + list(options) + [task.single_input_file] + + def determine_result(self, run): + # Test-Comp scores the artefact, not a verdict, so the only thing this + # has to distinguish is "ran" from "broke". Saying anything stronger + # would be this module claiming to know whether the suite covers the + # error -- which is TestCov's job and precisely what the competition + # does not let the tool self-report. + # + # A timeout still counts as DONE: the tool budgets itself below the + # harness limit and writes the suite before returning, so a run killed + # at the wall clock has normally already produced one. + if run.was_timeout: + return result.RESULT_DONE + if run.exit_code.value == 0: + return result.RESULT_DONE + return result.RESULT_ERROR