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/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") 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