From 69329c27d7d12a6e95e0dde65b175c19f162a7dd Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 22 Aug 2026 17:37:56 -0400 Subject: [PATCH] feat(testcomp): BenchExec packaging, and always emit a test suite (H1.4) H1.4 was the last unstarted item in H1, and H1 is the front that decides whether Map2Check can be submitted to Test-Comp at all. Emit the suite for every outcome, not only for a violation. It used to live inside `if (foundViolation)`, so a run that decided nothing left no test-suite/ directory behind -- and the competition harness reads an absent directory as a tool that crashed, not as an honest zero. metadata.xml is now always written; foundViolation decides whether the suite carries a test case, not whether the suite exists. map2check-testcomp-wrapper.py is a separate entry point from the SV-COMP wrapper on purpose. That one answers "does this program satisfy the property" and prints a verdict; this one produces an artefact and lets TestCov score it. The verdict vocabulary, the exit codes and the output are all different, and folding both into one script would mean behaviour that depends on a property string in two unrelated ways. It resolves the binary against its own path rather than "./map2check", because BaseTool2 dropped the working_directory() hook the old wrapper relied on: the process now starts in the benchmark's directory, not the tool's. utils/moduleBenchExec/map2check_testcomp.py is the tool-info module, written against the introspected benchexec 3.35 API rather than from memory. It refuses cover-branches instead of accepting it: branch coverage needs one test case per input vector and the runtime writes one nondet log per run (H1.3), so accepting it would look like participation while scoring zero and hiding why. The harness walltime becomes the tool's own budget, so it is Map2Check that stops and finishes writing metadata.xml rather than the harness killing it mid-write. The existing map2check.py is left alone. It is the SV-COMP adaptor and still uses BaseTool 1.x -- deprecated, but still present in benchexec 3.35, so it is legacy rather than dead, and migrating it is a separate change with its own risk. Verified against a full build and install, not in isolation: - violation -> metadata.xml + testcase-1.xml, specification verbatim - no violation -> metadata.xml, 0 test cases - tool-info -> 15/15 against the real benchexec package - TestCov corpus -> 6/6, including the two NOT_COVERED cases that now reach TestCov with an empty suite instead of taking the old "no suite produced" shortcut Co-Authored-By: Claude Opus 5 (1M context) --- .github/workflows/ci.yml | 4 + docs/TESTCOMP-CHECKLIST.md | 8 +- modules/frontend/map2check.cpp | 48 ++++-- scripts/package-release.sh | 8 +- tests/integration/test_benchexec_toolinfo.py | 155 +++++++++++++++++++ utils/map2check-testcomp-wrapper.py | 132 ++++++++++++++++ utils/moduleBenchExec/map2check_testcomp.py | 97 ++++++++++++ 7 files changed, 431 insertions(+), 21 deletions(-) create mode 100644 tests/integration/test_benchexec_toolinfo.py create mode 100755 utils/map2check-testcomp-wrapper.py create mode 100644 utils/moduleBenchExec/map2check_testcomp.py 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