From 6e3eacbb604194f47d419f52ee2aaf305402ec02 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sun, 18 Oct 2026 14:40:36 -0400 Subject: [PATCH 1/2] test(testcomp): sweep per-task work dirs left by killed runs A task killed by a reboot never reached the rm -rf at the end of the loop, so its mktemp directory stayed in /tmp. Over the V99c campaign a few reboots left 11 GB in one shard container and filled the Windows disk behind the WSL vhdx. Work directories now live under one root per results dir and shard, emptied when the harness starts. --- tests/testcomp/run_testcomp_evaluation.sh | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/tests/testcomp/run_testcomp_evaluation.sh b/tests/testcomp/run_testcomp_evaluation.sh index 9838ccbb9..879dfba49 100755 --- a/tests/testcomp/run_testcomp_evaluation.sh +++ b/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") From 9fb37184029760898c8613ef86993a33b0e2b920 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Mon, 26 Oct 2026 13:36:35 -0400 Subject: [PATCH 2/2] feat(testcomp): one wrapper and one tool-info module for SV-COMP and Test-Comp The BenchExec maintainers asked for Test-Comp support in the existing tool-info module instead of a second one (sosy-lab/benchexec#1352, sosy-lab/benchmarking/fm-tools!1245). So: - utils/map2check-wrapper.py now dispatches on the property file: COVER(...) generates tests and ends with DONE, CHECK(...) verifies as before. It calls map2check by absolute path, passes --data-model to both modes and points map2check at the bundled AFL++ when present. - map2check-testcomp-wrapper.py and moduleBenchExec/map2check_testcomp.py are gone; moduleBenchExec/map2check.py mirrors the updated upstream module (DONE -> RESULT_DONE, --data-model/--budget only for v9+, UnsupportedFeatureException, version without the "v" prefix). - The archive (make-archive.sh, smoketest.sh, README, licenses table), package-release.sh, the bench-def and the tool-info test follow. --- docs/reports/tacas-experiment-log.md | 38 ++ scripts/package-release.sh | 7 +- tests/integration/test_benchexec_toolinfo.py | 150 ++++--- tests/integration/test_exit_codes.sh | 7 +- .../official/bench-defs/map2check.xml | 4 +- utils/map2check-testcomp-wrapper.py | 160 ------- utils/map2check-wrapper.py | 394 ++++++++++++------ utils/moduleBenchExec/map2check.py | 187 +++++---- utils/moduleBenchExec/map2check_testcomp.py | 97 ----- utils/testcomp-archive/README.txt | 9 +- utils/testcomp-archive/licenses/README.md | 2 +- utils/testcomp-archive/make-archive.sh | 6 +- utils/testcomp-archive/smoketest.sh | 2 +- 13 files changed, 518 insertions(+), 545 deletions(-) delete mode 100755 utils/map2check-testcomp-wrapper.py delete mode 100644 utils/moduleBenchExec/map2check_testcomp.py diff --git a/docs/reports/tacas-experiment-log.md b/docs/reports/tacas-experiment-log.md index 151569d04..bf97c71fc 100644 --- a/docs/reports/tacas-experiment-log.md +++ b/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. diff --git a/scripts/package-release.sh b/scripts/package-release.sh index 1021388ed..6e5098f8a 100755 --- a/scripts/package-release.sh +++ b/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" diff --git a/tests/integration/test_benchexec_toolinfo.py b/tests/integration/test_benchexec_toolinfo.py index bfea6f0ce..6a4472450 100644 --- a/tests/integration/test_benchexec_toolinfo.py +++ b/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,19 +69,35 @@ 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)) @@ -83,6 +105,10 @@ def main(): "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)) diff --git a/tests/integration/test_exit_codes.sh b/tests/integration/test_exit_codes.sh index a315d4742..ef5bb384e 100644 --- a/tests/integration/test_exit_codes.sh +++ b/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. # diff --git a/tests/testcomp/official/bench-defs/map2check.xml b/tests/testcomp/official/bench-defs/map2check.xml index 14dfc0cc3..5eaacd1c1 100644 --- a/tests/testcomp/official/bench-defs/map2check.xml +++ b/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. --> - + module is utils/moduleBenchExec/map2check.py. --> + diff --git a/utils/map2check-testcomp-wrapper.py b/utils/map2check-testcomp-wrapper.py deleted file mode 100755 index 006f9ef53..000000000 --- a/utils/map2check-testcomp-wrapper.py +++ /dev/null @@ -1,160 +0,0 @@ -#!/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 - -Both Test-Comp goals are supported, with AFL++ and KLEE taking turns: - - cover-error one test case, the violating input vector of whichever - engine reached reach_error first - cover-branches up to 50 test cases: the fuzzer's corpus (at most half) and - one input vector per path KLEE explored -""" - -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 tool_environment(): - """The environment map2check runs with. - - In the Test-Comp archive (utils/testcomp-archive/make-archive.sh) AFL++ - travels inside the tool directory, since the competition machines do not - have it: map2check is pointed at the bundled afl-fuzz and afl-clang-fast, - afl-cc at its passes and runtime objects (AFL_PATH) and at the bundled - LLVM 16 clang (AFL_CC). Outside the archive -- a development install -- - none of these exist and the defaults (/usr/local) stay in force.""" - env = dict(os.environ) - bundled = { - "MAP2CHECK_AFL_FUZZ": os.path.join(HERE, "bin", "afl-fuzz"), - "MAP2CHECK_AFL_CC": os.path.join(HERE, "bin", "afl-clang-fast"), - "AFL_PATH": os.path.join(HERE, "lib", "afl"), - "AFL_CC": os.path.join(HERE, "bin", "clang"), - } - if os.path.exists(bundled["MAP2CHECK_AFL_FUZZ"]): - for key, value in bundled.items(): - env.setdefault(key, value) - return env - - -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: - # One test case: the violating vector. - goal_flags = ["--target-function", "--target-function-name", "reach_error"] - elif COVER_BRANCHES in prop: - # The fuzzer's corpus and one test case per path KLEE explored. - # No target function: the goal is to cover branches, and asking the - # tool to hunt for reach_error would make it stop at the first error - # instead of exploring. - goal_flags = ["--cover-branches"] - else: - print("Unsupported Property") - return 1 - - architecture = "32bit" if args.data_model == "ILP32" else "64bit" - - # The inner budget is what Map2Check divides between AFL++ 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, env=tool_environment()) - 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/map2check-wrapper.py b/utils/map2check-wrapper.py index c6b2fd2fc..0f12ff50a 100755 --- a/utils/map2check-wrapper.py +++ b/utils/map2check-wrapper.py @@ -1,152 +1,282 @@ #!/usr/bin/env python3 +"""Competition entry point for Map2Check, for both SV-COMP and Test-Comp. + +One wrapper, because BenchExec has one tool-info module per tool +(benchexec/tools/map2check.py): the property file decides what is asked. + + CHECK(...) SV-COMP verification. Prints a verdict as the last line + (TRUE, FALSE, FALSE_DEREF, ..., UNKNOWN). + COVER(...) Test-Comp test generation. Writes ./test-suite/ and prints + DONE as the last line. 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 -- and DONE does not + claim the suite covers anything; the validators decide that. + +Both Test-Comp goals are supported, with AFL++ and KLEE taking turns: + + cover-error one test case, the violating input vector of whichever + engine reached reach_error first + cover-branches up to 50 test cases: the fuzzer's corpus (at most half) and + one input vector per path KLEE explored +""" -import os import argparse +import os import shlex import subprocess +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) + +# Resolved against this file rather than "./map2check", so that the wrapper +# does not depend on the directory BenchExec starts it in. 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") + +# --- SV-COMP ------------------------------------------------------------------ + +SVCOMP_OUTER_TIMEOUT = "897s" +SVCOMP_TIMEOUT = "895" + +# --- Test-Comp ---------------------------------------------------------------- + +# Test-Comp 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 (ILP32 or LP64)") + parser.add_argument("--budget", type=int, default=DEFAULT_BUDGET, + help="total wall-clock budget in seconds (Test-Comp)") + parser.add_argument("benchmark", nargs="?", help="path to the C program") + return parser.parse_args(argv) + + +def tool_environment(): + """The environment map2check runs with. + + In the competition archive (utils/testcomp-archive/make-archive.sh) AFL++ + travels inside the tool directory, since the competition machines do not + have it: map2check is pointed at the bundled afl-fuzz and afl-clang-fast, + afl-cc at its passes and runtime objects (AFL_PATH) and at the bundled + LLVM 16 clang (AFL_CC). Outside the archive -- a development install -- + none of these exist and the defaults (/usr/local) stay in force.""" + env = dict(os.environ) + bundled = { + "MAP2CHECK_AFL_FUZZ": os.path.join(HERE, "bin", "afl-fuzz"), + "MAP2CHECK_AFL_CC": os.path.join(HERE, "bin", "afl-clang-fast"), + "AFL_PATH": os.path.join(HERE, "lib", "afl"), + "AFL_CC": os.path.join(HERE, "bin", "clang"), + } + if os.path.exists(bundled["MAP2CHECK_AFL_FUZZ"]): + for key, value in bundled.items(): + env.setdefault(key, value) + return env + -tool_path = "./map2check " -# default args -extra_tool = "timeout 897s " -command_line = extra_tool + tool_path -timemapsplit = "895" - -# Options -parser = argparse.ArgumentParser() -parser.add_argument("-v", "--version", help="Prints Map2check's version", action='store_true') -parser.add_argument("-p", "--propertyfile", help="Path to the property file") -parser.add_argument("benchmark", nargs='?', help="Path to the benchmark") - -args = parser.parse_args() - -# ARG options -version = args.version -property_file = args.propertyfile -benchmark = args.benchmark - -if version == True: - os.system(tool_path + "--version") - exit(0) - -if property_file is None: - print("Please, specify a property file") - exit(1) - -if benchmark is None: - print("Please, specify a benchmark to verify") - exit(1) - -is_memsafety = False -is_reachability = False -is_overflow = False -is_memcleanup = False - -f = open(property_file, 'r') -property_file_content = f.read() - -if "CHECK( init(main()), LTL(G valid-free) )" in property_file_content: - is_memsafety = True -elif "CHECK( init(main()), LTL(G valid-deref) )" in property_file_content: - is_memsafety = True -elif "CHECK( init(main()), LTL(G valid-memtrack) )" in property_file_content: - is_memsafety = True -elif "CHECK( init(main()), LTL(G valid-memcleanup) )" in property_file_content: - is_memcleanup = True -elif "CHECK( init(main()), LTL(G ! overflow) )" in property_file_content: - is_overflow = True -elif "CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )" in property_file_content: - is_reachability = True -else: - # We don't support termination - print("Unsupported Property") - exit(1) - - -# Set options -command_line_bkp = "" -if is_memsafety: - command_line += " --timeout "+timemapsplit+" --memtrack --smt-solver yices2 --generate-witness " -elif is_memcleanup: - command_line += " --timeout "+timemapsplit+" --memcleanup-property --smt-solver yices2 --generate-witness " -elif is_reachability: - # --add-invariants needs Clam (the renamed crab-llvm), which this build does - # not ship. map2check now exits 3 rather than ignoring the flag, so this - # branch fails until Clam lands -- deliberately. Do not drop the flag to - # silence it: the request is what makes the gap visible, and hiding it is how - # the flag stayed dead through an entire baseline (issue #54). - # - # command_line_bkp below is the pre-existing no-invariants fallback, and it is - # intentionally NOT wired to exit 3: it fires only on the Crab-specific - # 'failed external call' signal further down. Wiring it here would restore the - # silence this change exists to remove. - # See docs/reports/2026-08-16-crabllvm-review.md. - command_line_bkp = command_line + " --timeout "+timemapsplit+" --smt-solver yices2 --target-function --generate-witness " - command_line += " --timeout "+timemapsplit+" --smt-solver yices2 --add-invariants --target-function --generate-witness " -elif is_overflow: - command_line += " --timeout "+timemapsplit+" --check-overflow --smt-solver yices2 --generate-witness " - -print("Verifying with MAP2CHECK ") - -# Call MAP2CHECK -command_line += benchmark -command_line_bkp += benchmark - -print("Command: " + command_line) -args = shlex.split(command_line) -p = subprocess.Popen(args, stdout=subprocess.PIPE, stderr=subprocess.PIPE) -(stdout, stderr) = p.communicate() - -# Check invariant conflict -if b'failed external call: __map2check_main__' in stderr: - if is_reachability: - args = shlex.split(command_line_bkp) - p = subprocess.Popen(args, stdout=subprocess.PIPE, stderr=subprocess.PIPE) +def architecture(data_model): + return "32bit" if data_model == "ILP32" else "64bit" + + +def generate_tests(args, prop): + """Test-Comp: write ./test-suite/ and end with DONE.""" + if COVER_ERROR in prop: + # One test case: the violating vector. + goal_flags = ["--target-function", "--target-function-name", "reach_error"] + else: + # The fuzzer's corpus and one test case per path KLEE explored. + # No target function: the goal is to cover branches, and asking the + # tool to hunt for reach_error would make it stop at the first error + # instead of exploring. + goal_flags = ["--cover-branches"] + + # The inner budget is what Map2Check divides between AFL++ 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(args.data_model), + "--timeout", str(inner), + args.benchmark, + ] + + print("Generating tests with MAP2CHECK") + print("Command: " + " ".join(command)) + sys.stdout.flush() + + try: + completed = subprocess.run(command, timeout=args.budget, env=tool_environment()) + 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) + if rc not in (0, 1): + print("ERROR: map2check exited with %d" % rc) + return rc + print("DONE") + return 0 + + +def verify(args, prop): + """SV-COMP: print a verdict as the last line.""" + is_memsafety = False + is_reachability = False + is_overflow = False + is_memcleanup = False + + if "CHECK( init(main()), LTL(G valid-free) )" in prop: + is_memsafety = True + elif "CHECK( init(main()), LTL(G valid-deref) )" in prop: + is_memsafety = True + elif "CHECK( init(main()), LTL(G valid-memtrack) )" in prop: + is_memsafety = True + elif "CHECK( init(main()), LTL(G valid-memcleanup) )" in prop: + is_memcleanup = True + elif "CHECK( init(main()), LTL(G ! overflow) )" in prop: + is_overflow = True + elif "CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )" in prop: + is_reachability = True + else: + # We don't support termination + print("Unsupported Property") + return 1 + + command_line = ("timeout " + SVCOMP_OUTER_TIMEOUT + " " + shlex.quote(MAP2CHECK) + + " --architecture " + architecture(args.data_model)) + + # Set options + command_line_bkp = "" + if is_memsafety: + command_line += " --timeout " + SVCOMP_TIMEOUT + " --memtrack --smt-solver yices2 --generate-witness " + elif is_memcleanup: + command_line += " --timeout " + SVCOMP_TIMEOUT + " --memcleanup-property --smt-solver yices2 --generate-witness " + elif is_reachability: + # --add-invariants needs Clam (the renamed crab-llvm), which this build does + # not ship. map2check now exits 3 rather than ignoring the flag, so this + # branch fails until Clam lands -- deliberately. Do not drop the flag to + # silence it: the request is what makes the gap visible, and hiding it is how + # the flag stayed dead through an entire baseline (issue #54). + # + # command_line_bkp below is the pre-existing no-invariants fallback, and it is + # intentionally NOT wired to exit 3: it fires only on the Crab-specific + # 'failed external call' signal further down. Wiring it here would restore the + # silence this change exists to remove. + # See docs/reports/2026-08-16-crabllvm-review.md. + command_line_bkp = command_line + " --timeout " + SVCOMP_TIMEOUT + " --smt-solver yices2 --target-function --generate-witness " + command_line += " --timeout " + SVCOMP_TIMEOUT + " --smt-solver yices2 --add-invariants --target-function --generate-witness " + elif is_overflow: + command_line += " --timeout " + SVCOMP_TIMEOUT + " --check-overflow --smt-solver yices2 --generate-witness " + + print("Verifying with MAP2CHECK ") + + # Call MAP2CHECK + command_line += shlex.quote(args.benchmark) + command_line_bkp += shlex.quote(args.benchmark) + + print("Command: " + command_line) + env = tool_environment() + p = subprocess.Popen(shlex.split(command_line), stdout=subprocess.PIPE, + stderr=subprocess.PIPE, env=env) (stdout, stderr) = p.communicate() + # Check invariant conflict + if b'failed external call: __map2check_main__' in stderr: + if is_reachability: + p = subprocess.Popen(shlex.split(command_line_bkp), stdout=subprocess.PIPE, + stderr=subprocess.PIPE, env=env) + (stdout, stderr) = p.communicate() + + output = stdout.decode() + + # Parse output + if 'Timed out' in output: + print("Timed out") + return 1 -# Parse output -if b'Timed out' in stdout: - print("Timed out") - exit(1) + # Error messages + free_offset = "\tFALSE-FREE: Operand of free must have zero pointer offset" + deref_offset = "\tFALSE-DEREF: Reference to pointer was lost" + memtrack_offset = "\tFALSE-MEMTRACK" + memcleanup_offset = "\tFALSE-MEMCLEANUP" + target_offset = "\tFALSE: Target Reached" + overflow_offset = "\tOVERFLOW" + if "VERIFICATION FAILED" in output: + if free_offset in output: + print("FALSE_FREE") + return 0 + if deref_offset in output: + print("FALSE_DEREF") + return 0 + if memtrack_offset in output: + print("FALSE_MEMTRACK") + return 0 + if memcleanup_offset in output: + print("FALSE_MEMCLEANUP") + return 0 + if target_offset in output: + print("FALSE") + return 0 + if overflow_offset in output: + print("FALSE_OVERFLOW") + return 0 -# Error messages -free_offset = "\tFALSE-FREE: Operand of free must have zero pointer offset" -deref_offset = "\tFALSE-DEREF: Reference to pointer was lost" -memtrack_offset = "\tFALSE-MEMTRACK" -memcleanup_offset = "\tFALSE-MEMCLEANUP" -target_offset = "\tFALSE: Target Reached" -overflow_offset = "\tOVERFLOW" + if "VERIFICATION SUCCEEDED" in output: + print("TRUE") + return 0 -if "VERIFICATION FAILED" in stdout.decode(): - if free_offset in stdout.decode(): - print("FALSE_FREE") - exit(0) + print("UNKNOWN") + return 0 - if deref_offset in stdout.decode(): - print("FALSE_DEREF") - exit(0) - if memtrack_offset in stdout.decode(): - print("FALSE_MEMTRACK") - exit(0) +def main(argv): + args = parse_args(argv) - if memcleanup_offset in stdout.decode(): - print("FALSE_MEMCLEANUP") - exit(0) + if args.version: + return subprocess.call([MAP2CHECK, "--version"]) - if target_offset in stdout.decode(): - print("FALSE") - exit(0) + 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 - if overflow_offset in stdout.decode(): - print("FALSE_OVERFLOW") - exit(0) + with open(args.propertyfile, "r") as handle: + prop = handle.read() + if COVER_ERROR in prop or COVER_BRANCHES in prop: + return generate_tests(args, prop) + return verify(args, prop) -if "VERIFICATION SUCCEEDED" in stdout.decode(): - print("TRUE") - exit(0) -print("UNKNOWN") -exit(0) +if __name__ == "__main__": + sys.exit(main(sys.argv[1:])) diff --git a/utils/moduleBenchExec/map2check.py b/utils/moduleBenchExec/map2check.py index 7dba57fa1..c5a52456f 100644 --- a/utils/moduleBenchExec/map2check.py +++ b/utils/moduleBenchExec/map2check.py @@ -1,110 +1,121 @@ -""" -BenchExec is a framework for reliable benchmarking. -This file is part of BenchExec. +# This file is part of BenchExec, a framework for reliable benchmarking: +# https://github.com/sosy-lab/benchexec +# +# SPDX-FileCopyrightText: 2007-2020 Dirk Beyer +# +# SPDX-License-Identifier: Apache-2.0 + +import functools +import os +import re -Copyright (C) 2007-2015 Dirk Beyer +import benchexec.tools.template +from benchexec import result +from benchexec.tools.sv_benchmarks_util import ILP32, LP64, get_data_model_from_task +from benchexec.tools.template import ToolNotFoundException -All rights reserved. -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at +class Tool(benchexec.tools.template.BaseTool2): + """ + This class serves as tool adaptor for Map2Check + (https://github.com/hbgit/Map2Check). - http://www.apache.org/licenses/LICENSE-2.0 + Map2Check is both a verifier and a test generator; its wrapper decides from + the property file which one is asked for. For a coverage property it + writes the test suite to ./test-suite/ and prints DONE. -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. -""" -import os -import benchexec.util as Util -import benchexec.tools.template -import benchexec.result as result - -class Tool(benchexec.tools.template.BaseTool): - """ - This class serves as tool adaptor for Map2Check (https://github.com/hbgit/Map2Check) + Since Map2Check 9, the task's data model (--data-model) and the time limit + (--budget, the tool stops shortly before it so that the test suite is + complete) are passed to the wrapper. Older wrappers do not accept them. """ REQUIRED_PATHS_6 = [ - "__init__.py", - "map2check.py", - "map2check-wrapper.sh", - "modules" - ] - - REQUIRED_PATHS_7_1 = [ - "map2check", - "map2check-wrapper.py", - "bin", - "include", - "lib" - ] - - def executable(self): - #Relative path to map2check wrapper - if self._get_version() == 6: - return Util.find_executable('map2check-wrapper.sh') - elif self._get_version() > 6: - return Util.find_executable('map2check-wrapper.py') + "__init__.py", + "map2check.py", + "map2check-wrapper.sh", + "modules", + ] + + REQUIRED_PATHS_7_1 = ["map2check", "map2check-wrapper.py", "bin", "include", "lib"] + + def executable(self, tool_locator): + try: + executable = tool_locator.find_executable("map2check-wrapper.sh") + self._version = 6 + except ToolNotFoundException: + executable = tool_locator.find_executable("map2check-wrapper.py") + self._version = 7 + return executable def program_files(self, executable): """ Determine the file paths to be adopted """ - if self._get_version() == 6: + if self._version == 6: paths = self.REQUIRED_PATHS_6 - elif self._get_version() > 6: + elif self._version > 6: paths = self.REQUIRED_PATHS_7_1 return paths - def _get_version(self): - """ - Determine the version based on map2check-wrapper.sh file - """ - exe_v6 = Util.find_executable('map2check-wrapper.sh', exitOnError=False) - if exe_v6: - return 6 - else: - return 7 - - def working_directory(self, executable): executableDir = os.path.dirname(executable) return executableDir def version(self, executable): - return self._version_from_tool(executable) + # Map2Check prints "v9.0.0-Songbirds:2026-10-13". + return self._version_from_tool(executable).removeprefix("v") def name(self): - return 'Map2Check' - - def cmdline(self, executable, options, sourcefiles, propertyfile, rlimits): - assert len(sourcefiles) == 1, "only one sourcefile supported" - assert propertyfile, "property file required" - sourcefile = sourcefiles[0] - if self._get_version() == 6: - return [executable] + options + ['-c', propertyfile, sourcefile] - elif self._get_version() > 6: - return [executable] + options + ['-p', propertyfile, sourcefile] - - - def determine_result(self, returncode, returnsignal, output, isTimeout): + return "Map2Check" + + def project_url(self): + return "https://github.com/hbgit/Map2Check" + + def cmdline(self, executable, options, task, rlimits): + if task.property_file is None: + raise benchexec.tools.template.UnsupportedFeatureException( + "Map2Check requires a property file" + ) + + if self._version == 6: + return ( + [executable] + + options + + ["-c", task.property_file, task.single_input_file] + ) + elif self._version > 6: + cmd = [executable] + options + ["-p", task.property_file] + if _major_version(executable) >= 9: + data_model = get_data_model_from_task( + task, {ILP32: "ILP32", LP64: "LP64"} + ) + if data_model: + cmd += ["--data-model", data_model] + budget = rlimits.walltime or rlimits.cputime + if budget: + cmd += ["--budget", str(budget)] + return cmd + [task.single_input_file] + assert False, f"Unexpected version {self._version}" + + def determine_result(self, run): + output = run.output if not output: return result.RESULT_UNKNOWN output = output[-1].strip() status = result.RESULT_UNKNOWN - if self._get_version() > 6: - if output.endswith('TRUE'): + if self._version > 6: + if output == "DONE": + status = result.RESULT_DONE + elif output.endswith("TRUE"): status = result.RESULT_TRUE_PROP - elif 'FALSE' in output: + elif "FALSE" in output: if "FALSE_MEMTRACK" in output: status = result.RESULT_FALSE_MEMTRACK + elif "FALSE_MEMCLEANUP" in output: + status = result.RESULT_FALSE_MEMCLEANUP elif "FALSE_DEREF" in output: status = result.RESULT_FALSE_DEREF elif "FALSE_FREE" in output: @@ -113,28 +124,36 @@ def determine_result(self, returncode, returnsignal, output, isTimeout): status = result.RESULT_FALSE_OVERFLOW else: status = result.RESULT_FALSE_REACH - elif output.endswith('UNKNOWN'): + elif output.endswith("UNKNOWN"): status = result.RESULT_UNKNOWN - elif isTimeout: - status = 'TIMEOUT' + elif run.was_timeout: + status = result.RESULT_TIMEOUT else: - status = 'ERROR' + status = "ERROR" - elif self._get_version() == 6: - if output.endswith('TRUE'): + elif self._version == 6: + if output.endswith("TRUE"): status = result.RESULT_TRUE_PROP - elif 'FALSE' in output: + elif "FALSE" in output: if "FALSE(valid-memtrack)" in output: status = result.RESULT_FALSE_MEMTRACK elif "FALSE(valid-deref)" in output: status = result.RESULT_FALSE_DEREF elif "FALSE(valid-free)" in output: status = result.RESULT_FALSE_FREE - elif output.endswith('UNKNOWN'): + elif output.endswith("UNKNOWN"): status = result.RESULT_UNKNOWN - elif isTimeout: - status = 'TIMEOUT' + elif run.was_timeout: + status = result.RESULT_TIMEOUT else: - status = 'ERROR' + status = "ERROR" return status + + +@functools.lru_cache +def _major_version(executable): + """The major version of Map2Check, or 0 if the wrapper does not tell.""" + version = Tool._version_from_tool(executable) + match = re.match(r"v?(\d+)\.", version) + return int(match.group(1)) if match else 0 diff --git a/utils/moduleBenchExec/map2check_testcomp.py b/utils/moduleBenchExec/map2check_testcomp.py deleted file mode 100644 index b34fe4e0f..000000000 --- a/utils/moduleBenchExec/map2check_testcomp.py +++ /dev/null @@ -1,97 +0,0 @@ -# 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). - - Both Test-Comp goals are supported. The wrapper picks the source of test - vectors from the property: cover-error takes the single violating vector - from the runtime's nondet log, cover-branches takes one vector per path - from KLEE's own .ktest output. - """ - - 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_ERROR not in spec and COVER_BRANCHES 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] - # 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. Test-Comp - # limits CPU time (15 min) and sets no wall-time limit; the hybrid runs - # one engine at a time, so its CPU time tracks its wall time. - budget = rlimits.walltime or rlimits.cputime - if budget: - cmd += ["--budget", str(budget)] - 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 diff --git a/utils/testcomp-archive/README.txt b/utils/testcomp-archive/README.txt index e4d6976d3..91e8569dc 100644 --- a/utils/testcomp-archive/README.txt +++ b/utils/testcomp-archive/README.txt @@ -10,16 +10,17 @@ License: GPL-2.0 (LICENSE); third-party components under licenses/ Usage (Test-Comp) ----------------- - ./map2check-testcomp-wrapper.py -p [--data-model ILP32|LP64] \ + ./map2check-wrapper.py -p [--data-model ILP32|LP64] \ [--budget ] The test suite is written to ./test-suite/ in the current directory, in the Test-Comp exchange format. Supported properties: coverage-error-call and coverage-branches. --budget defaults to 900 s; the tool stops shortly before -it so that the suite is complete. +it so that the suite is complete. The same wrapper verifies when given an +SV-COMP property (CHECK(...)) and then prints a verdict instead. - ./map2check-testcomp-wrapper.py --version prints the version - ./smoketest.sh runs the two examples in examples/ + ./map2check-wrapper.py --version prints the version + ./smoketest.sh runs the two examples in examples/ The archive runs on x86_64 Ubuntu 24.04: it carries LLVM 16 (clang, opt, llvm-link), KLEE 3.1 with klee-uclibc, AFL++ 4.40c and every shared library diff --git a/utils/testcomp-archive/licenses/README.md b/utils/testcomp-archive/licenses/README.md index 1a0b77aa8..9e3e32c21 100644 --- a/utils/testcomp-archive/licenses/README.md +++ b/utils/testcomp-archive/licenses/README.md @@ -7,7 +7,7 @@ with a license file of a row missing. | Component | Version / source | Files in the archive | License | Texts in `licenses/` | |---|---|---|---|---| -| Map2Check | this repository | `map2check`, `map2check-testcomp-wrapper.py`, `smoketest.sh`, `examples/`, `README`, `lib/lib*Pass.so`, `lib/libMap2CheckLibrary.so`, `lib/*.bc` (runtime) | GPL-2.0 | `../LICENSE` | +| Map2Check | this repository | `map2check`, `map2check-wrapper.py`, `smoketest.sh`, `examples/`, `README`, `lib/lib*Pass.so`, `lib/libMap2CheckLibrary.so`, `lib/*.bc` (runtime) | GPL-2.0 | `../LICENSE` | | KLEE | 3.1 (`fe22b90`) | `bin/klee`, `bin/kleaver`, `bin/ktest-tool` | NCSA | `KLEE-3.1.LICENSE.TXT` | | KLEE runtime | 3.1 (`runtime/`) | `lib/klee/runtime/libkleeRuntime*.bca`, `libkleeUBSan64*.bca` | NCSA; 9 files of klee-libc and Freestanding under BSD (University of California, FreeBSD); the UBSan runtime from LLVM compiler-rt | `KLEE-3.1.LICENSE.TXT`, `KLEE-3.1-runtime-NOTICES.txt` (the 9 notices, verbatim), `LLVM-16.LICENSE.TXT` | | klee-uclibc | `klee/klee-uclibc` | `lib/klee/runtime/klee-uclibc.bca` | LGPL-2.1 | `klee-uclibc.COPYING.LIB` | diff --git a/utils/testcomp-archive/make-archive.sh b/utils/testcomp-archive/make-archive.sh index 21a137d3f..28be155e2 100755 --- a/utils/testcomp-archive/make-archive.sh +++ b/utils/testcomp-archive/make-archive.sh @@ -49,8 +49,8 @@ mkdir -p "$T"/{bin,lib,include,lib/afl} cp -a "$INSTALL/map2check" "$T/" cp -aL "$INSTALL/lib/." "$T/lib/" 2>/dev/null || true rm -rf "$T/lib/clang" "$T/lib/klee" "$T/lib/libz3*" -cp "$HERE/../map2check-testcomp-wrapper.py" "$T/" -chmod +x "$T/map2check-testcomp-wrapper.py" +cp "$HERE/../map2check-wrapper.py" "$T/" +chmod +x "$T/map2check-wrapper.py" # --- LLVM 16 --------------------------------------------------------------- for tool in clang opt llvm-link; do cp -L "$LLVM/bin/$tool" "$T/bin/"; done @@ -162,7 +162,7 @@ while IFS= read -r -d '' file; do rel=${file#"$T"/} case "$rel" in licenses/*) continue ;; - LICENSE|README|smoketest.sh|map2check|map2check-testcomp-wrapper.py|examples/*|lib/*Pass.so|lib/libMap2CheckLibrary.so|lib/*.bc) + LICENSE|README|smoketest.sh|map2check|map2check-wrapper.py|examples/*|lib/*Pass.so|lib/libMap2CheckLibrary.so|lib/*.bc) need LICENSE ;; bin/klee|bin/kleaver|bin/ktest-tool) need licenses/KLEE-3.1.LICENSE.TXT ;; diff --git a/utils/testcomp-archive/smoketest.sh b/utils/testcomp-archive/smoketest.sh index f074d95e1..aa1e123ec 100755 --- a/utils/testcomp-archive/smoketest.sh +++ b/utils/testcomp-archive/smoketest.sh @@ -11,7 +11,7 @@ set -eu HERE=$(cd "$(dirname "$0")" && pwd) -TOOL="$HERE/map2check-testcomp-wrapper.py" +TOOL="$HERE/map2check-wrapper.py" "$TOOL" --version