Repository navigation
Conversation
The evaluation harnesses read map2check's output through `$( )`, which
deadlocks. Command substitution reads its pipe until EOF, and EOF only
arrives once every write end closes. map2check spawns KLEE and LibFuzzer as
grandchildren that inherit that pipe; when the outer `timeout` kills
map2check, they are orphaned but keep the write end open, and the harness
blocks forever.
Observed directly on a run stalled 18 minutes on its first file:
pipe:[472046]
pid=113 fd=3 <- harness subshell, blocked reading
pid=48538 fd=2 <- orphaned `timeout 48 klee`, write end held
pid=48539 fd=2 <- orphaned klee, write end held
map2check itself was already gone.
run_isolated redirects to a file instead, so nothing waits on a pipe, and
reaps every process whose cwd is inside the run's private temp directory --
`timeout` only signals its direct child, so KLEE would otherwise keep
burning CPU for the rest of the suite. Verified against a grandchild that
traps SIGTERM and outlives its parent: rc=124, no survivors.
The private cwd also fixes two pre-existing hazards in the CASTLE runner,
whose cwd was the repo root: map2check names its scratch by SHA-1 of the
input bitcode (caller.cpp:63), so pass 1 and the --add-invariants pass
collided on one directory, and a directory orphaned by an aborted run was
reused by the next run of the same input.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…MAX] Juliet routes its random inputs through std_testcase.h macros that expand inside each testcase, so rand() itself is the only interception point. Left unstubbed, rand() is an unresolved external: KLEE calls the real libc function and gets ONE concrete value. The program then has a single feasible path and map2check answers VERIFICATION SUCCEEDED -- not UNKNOWN, but a confident wrong TRUE. All 6 CWE190 int_rand_add false negatives in the v3 baseline were this. int_rand_square escaped only by luck: data*data overflows for |data| > 46340, so almost any concrete draw trips it, while int_rand_add needs data == INT_MAX exactly. Modelling an unknown external as nondeterministic is a sound over-approximation and the standard SV-COMP treatment; the concrete-value alternative is the unsound one. The range is constrained rather than left open, because that is where a naive stub creates false positives: rand() returns [0, RAND_MAX] and URAND31() depends on it, so an unconstrained int would hand the solver negative draws real rand() cannot produce. A static assert enforces that RAND_MAX+1 is a power of two, so the mask stays exact or the build fails loudly instead of silently biasing the input space. Verified on the known false negative: bad => VERIFICATION FAILED (was SUCCEEDED), good => VERIFICATION SUCCEEDED (no new false positive). Also records two known biases in the header so they are not mistaken for results: decodeHexChars returning 0 can turn a real bug into a trivially safe program, and printLine() as a no-op stops reading the buffer, which could mask an out-of-bounds read whose only sink is the print (1924 CWE121 testcases call printLine(data); zero do in CWE190/191/369). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… prefix LIMIT_PER_CWE took the first N files in alphabetical order. A Juliet family owns ~26 consecutive filenames, so 60 files collapsed into 2-3 families. Measured coverage of the previous baseline: CWE-190: 6 of 90 families (6.7%) CWE-191: 5 of 69 families (7.2%) CWE-369: 2 of 18 families (11.1%) The consequences were not subtle. Every int64_t family went untested, so the width-aware i64 overflow work the baseline existed to validate was never exercised once. In CWE-369 only float families were reached -- float division by zero yields IEEE infinity and is not undefined behaviour at all -- so every genuine integer divide-by-zero was missed. The resulting "0% recall on CWE-369" measured the sampler, not the tool. PER_FAMILY samples every family instead. Three per family is the default, justified by the previous run's data: grouping its rows by (family, variant) gave 26 groups and all 26 were perfectly homogeneous, with short_min_multiply covering 25 of its 26 flow variants and never disagreeing with itself. The three files are spread across the variant range rather than taken from the front: variants _01.._09 are the simple control-flow shapes and the hard ones live in the _1x/_2x range, so a prefix would reintroduce at the variant level the exact bias being removed at the family level. LIMIT_PER_CWE now aborts if set to a value that would have capped anything, so the bias cannot return by habit; 0 was the inert "unlimited" default and is still accepted. tests/integration/test_juliet_sampling.sh locks the invariants whose violation would repeat this silently -- a wrong sampler produces plausible output, which is why it went unnoticed across two full runs. The two assertions that execute the runner are sandboxed so the suite needs neither the 570MB Juliet submodule nor a working clang, and an assertion verifies nothing is written into the working tree. 18 tests, 0.2s. This commit also wires the runner to run_isolated (see previous commit). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A full scope-C run is hours long and unattended, and a disk that fills mid-write corrupts the CSV it was writing. Stopping is recoverable because both runners resume from their CSV; a truncated CSV is not. The watchdog samples free space, docker usage, results size, container log size and liveness every five minutes, and halts the run if free space falls under a floor. It reports container log sizes so a missing --log-opt rotation is visible rather than silent: docker's json-file driver is unbounded by default. Docker usage comes from `docker system df` rather than `du /var/lib/docker`, which needs root and silently under-reports without it -- a quietly wrong monitoring number is worse than none, which is the whole failure mode this script exists to prevent. Also fixes .gitignore, where an append landed on the previous line because the file did not end in a newline, breaking both patterns. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Full scope-C evaluation, 2,742 cases, run to completion: CASTLE 217/217 that compile, and Juliet at 421 of 421 families with PER_FAMILY=3. CASTLE precision 98.2% recall 74.0% undecided 16.7% Juliet precision 90.8% recall 46.8% undecided 28.0% Every false positive was traced to its raw output and its source, and the headline is that 33 of the 36 are correct answers to the wrong question. They all report FALSE-MEMTRACK on programs Juliet labels safe, and Juliet's CWE-416 good variants leak by construction -- goodG2B() mallocs and never frees, and says so in a comment. The harness maps CWE-416 to --memtrack, which checks leaks too. Excluding them, Juliet precision is 99.2%; the sole CASTLE false positive found its bug and only misreported the line, so real CASTLE precision is 100%. The 3 genuine false positives are all int64_t_rand_square good variants, where KLEE silently concretizes the imaxabs/sqrtl guard over a now-symbolic input and loses the constraint. Reported as a cost of the rand() fix, which converted 6 false negatives into true positives and introduced these 3. 98% of the 345 timeouts come from two sources: fscanf (242) and listen_socket (96). The same axis explains the false negatives -- input sources fgets, connect_socket, console and environment sit on exactly 50.0% correct among decided cases, the signature of proving the safe variant and missing the vulnerable one every time. The plan prioritises by measured cost: unresolved externals account for 575 lost cases across 887 that take input that way, which is larger than everything else combined. The undecided cluster in CWE-121/122 (252 cases) is filed as an investigation, not a fix -- the obvious hypothesis was tested and rejected, since 100% of UNKNOWN cases log an unresolved reference but so do 87% of decided ones. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…omp2026 The two benchmark harnesses now share one layout. CASTLE already lived in tests/castle/ with its benchmark as a submodule; Juliet's runner sat under test-comp2026/simulation/ purely for historical reasons. test-comp2026/simulation/run_juliet_evaluation.sh -> tests/juliet/run_juliet_evaluation.sh test-comp2026/simulation/juliet_stubs.c -> tests/juliet/juliet_stubs.c test-comp2026/juliet (submodule) -> tests/juliet/juliet-test-suite-c test-comp2026/ is a local workspace for Test-Comp preparation and paper material, so it is untracked and ignored from here on. The files stay on disk; only the tracking stops. Note this does not remove them from the history of master or develop, where they have been since before this branch. Two things were rescued rather than dropped: - README.md cited test-comp2026/.../juliet_wasm/wasm_results.csv as the evidence that the WASM pipeline detects all 15 seeded Juliet bugs. The file is 16 lines; it moves to docs/reports/wasm-juliet-validation.csv so the claim keeps its evidence instead of pointing at an untracked path. - test_wasm_pipeline.sh and test_wasm_entrypoint.sh defaulted MAP2CHECK_PATH to test-comp2026/simulation/release. CI always overrides it, so this was never exercised there, but it would have become a dead path for anyone running locally. Now defaults to install_e2e, which is what CI actually passes. Paths updated in the runner (JULIET_DIR, RESULTS_DIR, the tests/lib sources), in test_juliet_sampling.sh, and in baseline_watchdog.sh. RESULTS_DIR now defaults to tests/juliet/results, mirroring tests/castle/results. Verified after the move: shell syntax on all five touched scripts, the classifier (20) and sampling (18) suites, and an end-to-end run of the relocated runner on CWE-415 -- 6 TP, 6 TN, 0 compile failures. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Three documents, none of them changing behaviour yet. The Crab-LLVM review answers a question the issue #54 report left open: whether --add-invariants is worth reviving. It is. crab-llvm was renamed to Clam, not abandoned -- upstream pushed nine days ago, branch dev16 targets LLVM 16 explicitly, and the symbol our NonDetPass keys off (verifier.assume) is preserved. Exactly one flag was renamed. Our fork has been stale since 2019 and pins LLVM 6, which is the whole of the breakage. The review also records a hazard that decides the recommendation: an unsound invariant does not produce an error, it produces a wrong TRUE. Under KLEE it prunes a reachable state; under LibFuzzer nondet_assume calls pthread_exit and the execution dies in silence. With 35% of baseline cases taking input through unresolved externals, how Crab models those decides soundness. Hence: fix the silence now, and gate the port behind a CMake flag that is off until a differential run proves no detection is lost. The two implementation plans cover the conformance work that the development plan calls bloqueante. The emitter plan turned out smaller than its 2 pw estimate: the runtime already logs every nondet value in consumption order and flushes it for both engines (NonDetLog.c:17), and the frontend already parses that CSV. What is missing is serialization, so H1.2 collapses into H1.1. The plan is explicit that this covers Cover-Error only -- map2check_exit flushes once per process, so Cover-Branches needs per-input logs and stays out of scope. The TestCov plan makes the official validator a blocking check. Its corpus carries a negative control and an expected-results manifest, so the gate fails in both directions and cannot quietly become vacuous. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Phase A makes the missing capability loud on every input path; Phase B brings it back behind -DENABLE_CLAM=ON and promotes it only on differential evidence. The flag stays in all three call sites that request it today. They fail until Clam lands, which is the point: a request the tool cannot satisfy is the signal that should be visible, and withdrawing it would recreate exactly the silence issue #54 describes. One carve-out, for data integrity rather than for the flag -- CASTLE's pass 2 replaces pass 1's verdict, so an unhandled exit 3 would write ERROR over a legitimate UNKNOWN and corrupt the CSV instead of failing visibly. Recorded while investigating: because the flag was ignored on the .bc path, that second pass has been a byte-identical re-run of the first through the whole v5 baseline, burning a second timeout budget and writing used_invariants=yes for runs that used none. The capability test is one file asserting two contracts and printing which it checked, so it passes today in the ABSENT state and starts asserting verifier.assume injection the day the image carries Clam -- progress visible in the CI log rather than a red check nobody watches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The binary installs to the prefix root (CMake: DESTINATION .), not to bin/. Every existing harness uses $MAP2CHECK_DIR/map2check; three plans had invented a bin/ path that would have failed on the first run. Also declares the two harness deltas that cross the v5/v6 boundary, since v5 is now frozen as the 'before' of a before/after comparison: used_invariants changes meaning, and pass 2 stops being a duplicate run. With the attribution rule that follows from it -- the headline v6 run keeps invariants off, or the overflow, timeout, sampling and invariant fixes all become jointly uncreditable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Phase A of the Clam revival. The flag was accepted and silently ignored whenever the input was bitcode -- which is how every baseline run, the CASTLE harness and both BenchExec wrappers invoke the tool. The guard that was meant to warn lived inside `if (!is_llvmir_in)`, so the .bc path skipped it entirely and left no trace at all. map2check now refuses the run with a distinct exit code (3, ERROR_UNAVAILABLE_CAPABILITY) that separates "you typed it wrong" from "this binary cannot do that". The check sits in main() next to the other option validation, not in map2check_execution(), for two reasons: main() is the only place whose return becomes the process exit code, and it runs once instead of once per generator on the hybrid path. That second point surfaced a separate defect, filed as finding G rather than fixed here: main() discards map2check_execution()'s return value at all three call sites, so the exit code never reflects the analysis outcome -- the `return 1` behind --expected-result is swallowed too. The three call sites keep requesting invariants. They fail until Clam lands, which is the point: withdrawing the request would hide the gap and recreate exactly the silence this commit removes. One carve-out, for data integrity rather than for the flag -- CASTLE's pass 2 REPLACES pass 1's verdict, so an unhandled exit 3 would write ERROR over a legitimate UNKNOWN and corrupt the CSV instead of failing visibly. It now recognises exit 3, keeps pass 1's verdict, and records used_invariants=unavailable. Recorded in the findings report: because the flag was ignored on the .bc path, that second pass has been a byte-identical re-run of the first through the whole v5 baseline -- a second full timeout budget per UNKNOWN row, written down as used_invariants=yes for runs that used none. No published verdict changes; the column's meaning and the run times do. The test asserts two contracts and prints which one it checked. Today it reports CAPABILITY: ABSENT and asserts the refusal is loud, names the flag, explains itself and offers the remedy. Once the image carries Clam it will report PRESENT and instead assert that verifier.assume is really injected -- so the flag cannot come back as a no-op wearing a success exit code. No red check is parked in CI: one that is expected to be red gets ignored, and then nobody notices the day it turns green. Verified in the map2check-dev container: 5/5 on the new test, and 56/56 on the existing suite (verdict classifier 20, Juliet sampling 18, main argv 2, modes 16). clang-format deviations unchanged at 79, all pre-existing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Phase B. crab-llvm was renamed to Clam, not abandoned: branch dev16 pins CLAM_LLVM_VERSION 16, upstream pushed nine days ago, and the symbol NonDetPass keys off (verifier.assume) is preserved. Our fork had been stale since 2019 and pinned LLVM 6. The flag list is measured, not translated, and that measurement found a second bug underneath the first. Counting verifier.assume calls in the emitted bitcode on a loop program, against the legacy invocation: baseline (track=num, inter, opt=add-invariants, loc=block-entry) 5 + --crab-promote-assume 1 + --llvm-pp-loops 0 --llvm-pp-loops annihilates injection outright, and --crab-promote-assume rewrites verifier.assume into the llvm.assume intrinsic -- precisely the symbol NonDetPass.cpp:95 matches on, so promoting makes the invariants invisible to Map2Check. Both were in the legacy command line. The capability was dead twice over: even if crab-llvm had still built, it would have injected nothing Map2Check could see. Traced end to end on the fixed invocation: -compiled.bc (Clam output) verifier.assume=5 crab_assume=0 -output.bc (after NonDetPass) verifier.assume=0 crab_assume=5 -result.bc (linked) verifier.assume=0 crab_assume=5 so Clam -> verifier.assume -> map2check_crab_assume -> klee_assume is live from end to end. Off by default (-DENABLE_CLAM=ON), because an unsound invariant does not raise an error: under KLEE klee_assume prunes a reachable state, under LibFuzzer nondet_assume calls pthread_exit and the execution vanishes. Both read as "program is safe". Promotion to default waits on the differential run. Dockerfile.dev builds Clam into /opt/clam and then FAILS THE IMAGE BUILD if a probe program comes back with zero injected assumes -- a silent zero is exactly what hid this for years. libzstd-dev is required rather than optional: LLVM 16 from apt.llvm.org exports zstd::libzstd_shared, so find_package(LLVM) inside Clam fails without it. No optional Crab domain is enabled; --crab-track=num uses the default interval domain. --debug now keeps the scratch directory. Every intermediate of a run lives there and cleanGarbage() deleted it unconditionally, which made the pipeline impossible to inspect after the fact -- and made the injection assertion above unwritable until now. Retires the LLVM 6 machinery: FindCrabLlvm.cmake (unreferenced, no branch pinned) and build_crabllvm.py (hardcodes /llvm/release/llvm600 and g++-5). Also gitignores local agent material -- ai-memory skill installs, editor agent configs, CLAUDE.md backups and the local Test-Comp planning document -- for the same reason test-comp2026/ is ignored: preparation material, not product. Verified in the container, both capability states green from one test file: ABSENT 5/5 on the default build, PRESENT 2/2 on -DENABLE_CLAM=ON with Clam at CLAM_DIR. Rest of the suite unchanged at 56/56. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…that made it impossible --generate-test-suite writes a Test-Comp exchange-format suite -- metadata.xml plus one testcase-N.xml -- for the violation a run found. The format is https://gitlab.com/sosy-lab/software/test-format; the DTDs and public identifiers are transcribed from that repository, not guessed. Almost none of this was meant to be new code. The runtime already records every nondet value in consumption order and flushes it for both engines (NonDetLog.c), and the frontend already parses that CSV for counterexamples, so the plan was a serializer. Building it surfaced why nobody had noticed the log was broken: three defects that only a symbolic executor can see. 1. Use-after-scope in the nondet log. NONDET_CALL.value held the ADDRESS of the `value` parameter of the map2check_nondet_* wrapper -- a stack slot long dead by the time the log is written at exit. Natively the dead frame usually still held the value, so it looked fine. Under KLEE it was a pointer error inside nondet_log_to_file() itself, killing every state: completed paths = 0, and klee_log.csv came out ZERO BYTES on every symbolic run. No counterexample from KLEE has ever carried input values. Fixed by storing the value inline in a union. A pointer cannot work here even if it pointed into the row: the containers memcpy rows into a reallocated array, so any self-referential pointer is stale after the first append. The TODO asking for exactly this union dates from 2020. 2. map2check_nondet_double tagged its rows UNSIGNED, so every logged floating-point input was printed with %u over four bytes of the mantissa. 3. Every forked KLEE state writes the same klee_log.csv on exit and the last one wins -- and it is never the violating state, which aborts early. With (1) fixed the vector came back as [42, -1] on a program whose only violating path is [42, 7]: a sibling state that took the other branch had overwritten it. The nondet flush is now guarded on the violation flag. With all three fixed the emitter recovers the exact violating vector. Also in this commit: SHA-256 for the <programhash> field, pinned to FIPS 180-4 vectors (Map2Check only had SHA-1, which the format does not accept); --property-file so <specification> is copied verbatim from the property BenchExec passes rather than guessed; --test-suite-dir and --architecture. Scope, stated plainly: one test case per run, because map2check_exit() flushes once per process. That is all Cover-Error needs. Cover-Branches needs many test cases and therefore per-input logs, which is separate work, and no suite is emitted for a TRUE or UNKNOWN verdict yet (gap G4). Deliberately no type= or variable= attributes on <input>: Format.md says that if a variable is named and the sequence does not fit it, "the interpretation is undefined". Bare inputs carry no such risk. Verified in the container: 8/8 ctest (Sha256Test 7, TestSuiteTest 13 are new) and 78/78 integration, including a new 12-assertion emission test that checks well-formedness with a real parser, that programhash equals sha256sum of the program, and that the recovered vector is [42, 7] in that order -- the assertion that would have caught all three bugs above. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Left over from building tests/unit/frontend in isolation; same class as the other per-purpose build prefixes already listed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Makes the official Test-Comp validator a blocking check. The structural test added with the emitter asks whether the XML is well formed; this asks the only question the competition scores -- whether the suite, executed, reaches the bug. The verdict parser is keyed to observed output, not to a guess, and the reason is in NOTES-testcov-output.md: TestCov 3.7 exits 0 whether the suite covers the error or not. The verdict lives in the "Result:" line -- TRUE for covered, UNKNOWN for not. A gate built on $? would have passed unconditionally and been worth nothing. Anything matching neither pattern becomes ERROR rather than NOT_COVERED, so a wording change in a future TestCov fails loudly instead of quietly reporting that nothing covers anything. Six programs, each isolating one thing the emitter can get wrong: the minimal path, ordering of two inputs, the empty test vector, a non-int nondet type, four reads in a loop, and an unreachable error as negative control. If unreachable.c ever reports COVERED the harness is lying and no other result here can be trusted. expected.txt is bidirectional. A program that stops being COVERED is a regression; one that STARTS being COVERED when the manifest says otherwise is also a failure, because an unrecorded improvement is indistinguishable from a broken harness. Every verdict in it was measured at BUDGET=120, not assumed. Measured 6/6 against the manifest. Five match the obvious expectation -- including no_input.c, which was the assumption most likely to be wrong: a program with no nondeterministic input yields an empty test vector, and TestCov accepts and covers it. loop_reads.c does not, and it is recorded rather than removed. Map2Check returns VERIFICATION UNKNOWN on it, so no suite is produced and the emitter is never reached. Four unconstrained symbolic reads summing to a constant is one linear constraint that KLEE should discharge instantly, yet it is UNKNOWN at 60s, 120s and 240s. Filed as finding K: if short accumulator loops are undecided, some part of the 45.6% UNKNOWN the development plan attributes to path explosion may have a more mundane cause, and that is worth knowing before any efficacy work. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A gate nobody has seen fail is a gate nobody should trust. Reversing the emitter's input order -- a change that leaves every suite structurally perfect and semantically worthless -- turns the gate red at exit 1, as it must. Recorded because of which program caught it: only two_guards.c. The rest are insensitive to ordering by construction (one input each, or none), and loop_reads.c, the other multi-input program, is currently undecided by the tool (finding K). The ordering guarantee therefore rests on one program right now -- so two_guards.c must not be removed without a replacement, and fixing finding K would restore a second independent witness. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The push filter listed 'feat-*' with a hyphen, which never matched the convention actually in use -- feat/castle-juliet-baseline, feat/testcomp-conformance. No branch push has been verified by CI; every green run so far came from the pull_request trigger alone. The pull_request filter matched only PRs TARGETING develop/main/master, so a stacked PR based on another feature branch triggered nothing. PR #56 opened with exactly one check on it: GitGuardian. The TestCov gate and the invariants contract added in that same PR would never have run on it -- a regression gate that does not execute is not a gate. Both filters now cover feat/**; push also covers fix/**. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The previous commit added feat/** to both triggers, which fires two identical runs for every push to a branch with an open PR -- doubling CI cost for no extra coverage. Push now covers only the integration branches; feature branches are covered by the pull_request trigger, which is where the review actually happens. Net effect versus before this pair of commits: stacked PRs are verified (they were not), and nothing runs twice. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The TestCov gate failed on PR #56 with six lines of the form FAIL single_int.c expected COVERED, observed COVERED Every verdict was correct. --verdict-only promises exactly one word on stdout and the caller captures it with $(...), but the KEEP_WORK trap printed "(work kept at ...)" there too, so the captured value was two lines and never compared equal. It passed locally and failed in CI for one reason: only the CI step sets KEEP_WORK, and I added that flag in the same commit that added the job. The notice moves to stderr, where every other diagnostic already goes. Two hardening changes, both prompted by how confusing this was to read: - run_testcov.sh now dumps the tail of testcov.log and map2check.log to stderr whenever the verdict is ERROR. Without that, an ERROR reaches the job log as the bare word "ERROR" with no way to find out why -- which is how this gate first failed and why diagnosing it needed a local reproduction against the published image. - run_testcov_suite.sh validates that the verdict is one of the three legal words and says so plainly otherwise, instead of letting stray output produce a mismatch between two values that print identically. Verified against ghcr.io/hbgit/map2check-dev with KEEP_WORK=1 set, which is the configuration that failed: single_int, two_guards, no_input, char_input and unreachable all match the manifest again. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Finding K was "a trivial 4-read accumulator loop returns UNKNOWN". The
investigation found something considerably more consequential.
Map2Check DOES find the violation. With --debug the log reads:
72: TARGET-REACHED found <- KLEE found it, property file written
75: Note: Forcing timeout
77: VERIFICATION UNKNOWN
KLEE keeps exploring other states after recording the error, gets killed by
the budget (exit 31744 = 124 << 8), and map2check.cpp then does
if (caller->isTimeout()) { propertyViolated = UNKNOWN; }
discarding a FALSE that already has its counterexample on disk. The budget ran
out AFTER the tool had done the work.
Fix proposed, not applied: consult the property before forcing UNKNOWN. Held
back because it shifts UNKNOWN->FALSE counts across the whole baseline, which
interacts with the attribution rule declared for the v6 run.
This matters well beyond the gate. The development plan attributes 45.6%/50.7%
UNKNOWN to path explosion and prices the remedy at 4-8 pw of orchestration and
slicing. Here is a cheap mechanism inflating UNKNOWN that has nothing to do
with path explosion, and "how many v5 UNKNOWNs are discarded violations" is
answerable from data we already have. That measurement should precede the
investment.
A bisection over six variants also isolated that the loop is irrelevant --
loop2_sum and straight2_sum give identical partial-path counts. What scales is
the number of nondet reads: 1 -> 21 -> 114 -> 861 partial paths, 147K -> 7.5M
instructions. No .err files, so those are not error terminations. Filed as K2.
Two of my own intermediate conclusions were wrong and are recorded as such:
I claimed budget was ruled out based on runs made while several KLEE containers
competed for CPU, and I claimed --debug flipped the verdict when in fact my
`grep | head -1` was matching the debug line "TARGET-REACHED found" ahead of the
verdict line. The second mistake is what exposed the root cause.
Also adds docs/TESTCOMP-CHECKLIST.md: per-item status of the development plan
with a pointer to the evidence behind each claim, including the items where the
plan's premises turned out to be stale (H1.2 collapsed into H1.1; H2.1 assumes
9 always-on passes that reachability has not used for some time).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Finding K. KLEE keeps exploring other states after recording an error, so it is
routinely killed by `timeout` on a run that already succeeded. The timeout check
ran first and overwrote the verdict, discarding a FALSE whose counterexample was
already written to map2check_property.
How much this happens, counted from the v5 raw logs without re-running anything:
corpus logs "Forcing timeout" fired final UNKNOWN
Juliet 2526 2031 (80%) 703
CASTLE 217 123 (57%) -
The gap between 2031 and 703 is the hybrid default: each case runs map2check
twice, and the LibFuzzer pass -- 0.2x the budget -- almost always overruns.
That number exposed a bug in the first version of this fix. Its comment claimed
the LibFuzzer arm was excluded, but the timeout branch runs first and applied to
both engines, so a LibFuzzer crash that could not be replayed (isVerified()
false) would have had its property file trusted -- the exact evidence the
comment said to distrust, across thousands of runs. The restriction now lives in
the condition:
bool evidenceIsTrustworthy =
recordedAViolation &&
(generator != NonDetGenerator::LibFuzzer || caller->isVerified());
Also hardens the scratch directory. It is named after the SHA-1 of the input, so
it is content-derived, and a plain mkdir over an existing one silently kept
whatever an aborted run had left -- including map2check_property. Now that a
recorded violation survives a timeout, a stale property file would fabricate a
FALSE. It is removed before being created.
What is NOT measured, and why: the raw logs record that the override fired but
not whether a violation was recorded, because map2check_property is not kept.
The UNKNOWN->FALSE count therefore stays open until the v6 run with both
binaries. CASTLE cannot answer it either -- 32 of its 38 undecided cases use the
degenerate reachability mode (finding B), where no violation is ever recorded,
so B masks K on that corpus entirely.
Four measurement mistakes of mine are recorded in the findings report rather
than quietly dropped: a "not a budget artefact" claim made while several KLEE
containers competed for CPU; a `grep | head -1` that matched a debug line ahead
of the verdict line and made me report that --debug flipped the verdict; a
segfault hypothesis retracted after 0/10 cases reproduced it; and four separate
bugs in the measurement harness itself. None were in the tool.
Verified: ctest 8/8, integration 73/73 across six scripts.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Width-aware overflow checking, a trustworthy evaluation harness, and the first full CASTLE/Juliet baseline
Test-Comp conformance: emit test suites, gate them on TestCov, and revive --add-invariants on Clam
The image build has been failing on develop since #57 merged. Clam's sea-dsa dependency defines seadsa::mkTLIGetter with a redundant namespace qualification inside its own namespace; clang reports that as -Wextra-qualification, GCC rejects it outright, and the build died at 34%. The Clam RUN was picking up GCC 11 because the ENV CC/CXX=clang-16 that the rest of the image relies on is declared in section 11, 88 lines *below* it, and a Docker ENV only applies to later instructions. Naming the compilers in CLAM_CFG fixes it without depending on instruction order, and matches what upstream's own docker/clam.Dockerfile passes. Neither dependency drifted: clam dev16 is at 302bf49a (2026-08-07) and sea-dsa dev16 at 661855a3 (2026-08-12), both older than the recipe. This never built -- it was written and merged without ever being compiled. That is the second defect, and the one worth fixing properly: the publish workflow only ran after a merge to develop, so no PR could have caught an unbuildable Dockerfile. It now also runs on pull requests that touch Dockerfile.dev, with push disabled so a branch never overwrites :latest. This PR touches Dockerfile.dev, so that new job validates the fix here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
fix(docker): build Clam with clang-16, and validate Dockerfile.dev on PRs
clam, sea-dsa and llvm-seahorn were cloned from dev16 and Crab from dev -- four moving branches. The contents of the published image could therefore change with no change in this repository, and the failure mode is the one that just cost a red develop: a build that worked yesterday breaks today for reasons no diff explains. crab@dev moved on 2026-08-21, one day before this. Clam's own crab/extra targets are plain `git clone -b dev<N>` custom commands with nowhere to pass a commit, so pinning means not using them. Its CMakeLists already prefers an in-tree dependency over cloning one, so placing all four by hand works -- and since everything is present before the first configure, the configure/clone/reconfigure sequence collapses to one `cmake ..`. Verified in the image before pushing this time: all four pinned checkouts resolve, and a single configure detects sea-dsa, Crab and llvm-seahorn with no "required but not found" warning. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
chore(docker): pin Clam and its three dependencies to SHAs
TargetPass instruments call sites whose callee matches the requested name. When the program never calls that function, nothing is instrumented and the reachability property holds trivially -- and nothing in the output says so. Zero call sites is not an error. A program that genuinely never calls reach_error IS safe with respect to reach_error, and TRUE is correct there. The defect is that such a TRUE is indistinguishable from a TRUE earned by exploring the program. So the fix is visibility, not a change of verdict: the pass scans the module once and, when the target has no call sites, says what the verdict is worth. Measured on the CASTLE v6 baseline, which is what moves this from a suspicion to a defect with a number. 98 of 217 runs used `--target-function-name main` -- a program does not call its own entry point: TRUE 57, TIMEOUT 22, UNKNOWN 10, ERROR 9, FALSE-* 0 Not one FALSE, while the other modes produce 49 across the same corpus. 59 of those 98 programs were known to be vulnerable and none was detected. Seventeen were scored: 5 FN, and 12 TN -- credit for answers an oracle that can only say "correct" could not have failed to give. Excluding the mode, recall goes from 74.0% to 79.4%; precision is unchanged at 98.2%, since the mode yields neither TP nor FP. Correcting my own earlier reading: the 61 N/A rows are N/A because the harness declares those CWEs out of scope, not because of finding B. B's real cost is the 17 scored cases. Still open, deliberately: the harness maps 13 CWEs onto this mode as an escape default. Fixing that changes baseline scoring, so it waits for the v6 run to finish rather than moving the criterion mid-run. Verified end to end against a full build, not just the pass in isolation: test_target_coverage.sh 4/4. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
fix(reachability): announce a target that is never called (finding B)
H1.4 was the last unstarted item in H1, and H1 is the front that decides
whether Map2Check can be submitted to Test-Comp at all.
Emit the suite for every outcome, not only for a violation. It used to live
inside `if (foundViolation)`, so a run that decided nothing left no
test-suite/ directory behind -- and the competition harness reads an absent
directory as a tool that crashed, not as an honest zero. metadata.xml is now
always written; foundViolation decides whether the suite carries a test case,
not whether the suite exists.
map2check-testcomp-wrapper.py is a separate entry point from the SV-COMP
wrapper on purpose. That one answers "does this program satisfy the property"
and prints a verdict; this one produces an artefact and lets TestCov score it.
The verdict vocabulary, the exit codes and the output are all different, and
folding both into one script would mean behaviour that depends on a property
string in two unrelated ways. It resolves the binary against its own path
rather than "./map2check", because BaseTool2 dropped the working_directory()
hook the old wrapper relied on: the process now starts in the benchmark's
directory, not the tool's.
utils/moduleBenchExec/map2check_testcomp.py is the tool-info module, written
against the introspected benchexec 3.35 API rather than from memory. It
refuses cover-branches instead of accepting it: branch coverage needs one test
case per input vector and the runtime writes one nondet log per run (H1.3), so
accepting it would look like participation while scoring zero and hiding why.
The harness walltime becomes the tool's own budget, so it is Map2Check that
stops and finishes writing metadata.xml rather than the harness killing it
mid-write.
The existing map2check.py is left alone. It is the SV-COMP adaptor and still
uses BaseTool 1.x -- deprecated, but still present in benchexec 3.35, so it is
legacy rather than dead, and migrating it is a separate change with its own
risk.
Verified against a full build and install, not in isolation:
- violation -> metadata.xml + testcase-1.xml, specification verbatim
- no violation -> metadata.xml, 0 test cases
- tool-info -> 15/15 against the real benchexec package
- TestCov corpus -> 6/6, including the two NOT_COVERED cases that now reach
TestCov with an empty suite instead of taking the old
"no suite produced" shortcut
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Owner
Author
|
@copilot resolve the merge conflicts in this pull request |
There was a problem hiding this comment.
🟡 Changes recommended
One or more issues must be addressed before approval.
4 open issues
What changed in this PR
Updates Map2Check’s verification runtime, AFL++ integration, and competition-oriented validation infrastructure.
Changes:
- Adds Test-Comp suite/hash build integration, nondeterministic-type interfaces, assertion handling, and runtime logging/checking changes.
- Expands unit tests and Test-Comp, CASTLE, and Juliet evaluation resources.
- Updates release packaging and migration documentation while removing obsolete simulation files and paper drafts.
| File | Description |
|---|---|
| utils/testcomp-archive/licenses/STP-2.3.4.LICENSE | Updated as part of this pull request. |
| utils/testcomp-archive/licenses/MiniSat.LICENSE | Updated as part of this pull request. |
| utils/testcomp-archive/examples/coverage-error-call.prp | Updated as part of this pull request. |
| utils/testcomp-archive/examples/coverage-branches.prp | Updated as part of this pull request. |
| utils/testcomp-archive/examples/cover_error.c | Updated as part of this pull request. |
| utils/testcomp-archive/examples/cover_branches.c | Updated as part of this pull request. |
| utils/moduleBenchExec/__init__.py | Updated as part of this pull request. |
| utils/map2check-wrapper.py | Updated as part of this pull request. |
| utils/map2check-wrapper-reg-test.py | Updated as part of this pull request. |
| tests/unit/HelloGTest.cpp | Updated as part of this pull request. |
| tests/unit/frontend/CMakeLists.txt | Updated as part of this pull request. |
| tests/unit/CMakeLists.txt | Updated as part of this pull request. |
| tests/unit/backend-library/CMakeLists.txt | Updated as part of this pull request. |
| tests/unit/backend-library/BTreeTest.cpp | Updated as part of this pull request. |
| tests/unit/backend-library/AllocationLogTest.cpp | Updated as part of this pull request. |
| tests/testcomp/programs/unreachable.c | Updated as part of this pull request. |
| tests/testcomp/programs/two_guards.c | Updated as part of this pull request. |
| tests/testcomp/programs/single_int.c | Updated as part of this pull request. |
| tests/testcomp/programs/no_input.c | Updated as part of this pull request. |
| tests/testcomp/programs/loop_reads.c | Updated as part of this pull request. |
| tests/testcomp/programs/char_input.c | Updated as part of this pull request. |
| tests/testcomp/official/init.sh | Updated as part of this pull request. |
| tests/testcomp/official/bench-defs/map2check.xml | Updated as part of this pull request. |
| tests/testcomp/launch-v12.sh | Updated as part of this pull request. |
| tests/testcomp/fetch-benchmarks.sh | Updated as part of this pull request. |
| tests/testcomp/expected.txt | Updated as part of this pull request. |
| tests/testcomp/cover-error-call.prp | Updated as part of this pull request. |
| tests/lib/memsafety_classifier.sh | Updated as part of this pull request. |
| tests/juliet/launch-v15-regression.sh | Updated as part of this pull request. |
| tests/juliet/launch-v12-regression.sh | Updated as part of this pull request. |
| tests/juliet/launch-juliet-cd-later.sh | Updated as part of this pull request. |
| tests/integration/test_wasm_pipeline.sh | Updated as part of this pull request. |
| tests/integration/test_wasm_entrypoint.sh | Updated as part of this pull request. |
| tests/integration/test_memsafety_classifier.sh | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/sets/castle-overflow.set | Updated as part of this pull request. |
| tests/castle/benchexec/sets/castle-memcleanup.set | Updated as part of this pull request. |
| tests/castle/benchexec/map2check_castle.xml | Updated as part of this pull request. |
| test-comp2026/simulation/map2check-v8.xml | Updated as part of this pull request. |
| test-comp2026/simulation/map2check-v8-heap.xml | Updated as part of this pull request. |
| test-comp2026/.gitignore | Updated as part of this pull request. |
| scripts/prepare-release.sh | Updated as part of this pull request. |
| scripts/package-release.sh | Updated as part of this pull request. |
| scripts/make-release.sh | Updated as part of this pull request. |
| modules/frontend/utils/sha256.hpp | Updated as part of this pull request. |
| modules/frontend/utils/log.cpp | Updated as part of this pull request. |
| modules/frontend/utils/gen_crypto_hash.cpp | Updated as part of this pull request. |
| modules/frontend/utils/CMakeLists.txt | Updated as part of this pull request. |
| modules/frontend/test_suite/CMakeLists.txt | Updated as part of this pull request. |
| modules/frontend/counter_example/counter_example.hpp | Updated as part of this pull request. |
| modules/frontend/CMakeLists.txt | Updated as part of this pull request. |
| modules/backend/pass/NonDetPass.hpp | Updated as part of this pull request. |
| modules/backend/pass/NonDetFunctions.hpp | Updated as part of this pull request. |
| modules/backend/pass/MemoryTrackPass.hpp | Updated as part of this pull request. |
| modules/backend/pass/AssertPass.hpp | Updated as part of this pull request. |
| modules/backend/pass/AssertPass.cpp | Updated as part of this pull request. |
| modules/backend/library/lib/WitnessGenerationNone.c | Updated as part of this pull request. |
| modules/backend/library/lib/WitnessGeneration.c | Updated as part of this pull request. |
| modules/backend/library/lib/PropertyGenerator.c | Updated as part of this pull request. |
| modules/backend/library/lib/NonDetGeneratorNone.c | Updated as part of this pull request. |
| modules/backend/library/lib/Map2CheckFunctions.c | Updated as part of this pull request. |
| modules/backend/library/lib/ListLog.c | Updated as part of this pull request. |
| modules/backend/library/lib/ContainerBTree.c | Updated as part of this pull request. |
| modules/backend/library/lib/CMakeLists.txt | Updated as part of this pull request. |
| modules/backend/library/lib/BTree.c | Updated as part of this pull request. |
| modules/backend/library/lib/AnalysisModeMemtrack.c | Updated as part of this pull request. |
| modules/backend/library/lib/AnalysisModeMemcleanup.c | Updated as part of this pull request. |
| modules/backend/library/lib/AllocationLog.c | Updated as part of this pull request. |
| modules/backend/library/header/WitnessGeneration.h | Updated as part of this pull request. |
| modules/backend/library/header/NonDetLog.h | Updated as part of this pull request. |
| modules/backend/library/header/NonDetGenerator.h | Updated as part of this pull request. |
| make-unit-test.sh | Updated as part of this pull request. |
| examples/use-after-free/sample_use_after_free.c | Updated as part of this pull request. |
| examples/use-after-free/README.md | Updated as part of this pull request. |
| docs/superpowers/specs/2026-09-29-tacas-3c-seed-ranking-design.md | Updated as part of this pull request. |
| docs/reports/wasm-juliet-validation.csv | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sections/06-conclusao.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sections/05-demonstracao.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sections/04-ciberseguranca.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sections/03-arquitetura.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sections/02-historia.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sections/01-introducao.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sbseg-article/img/README.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sbseg-article/img/fig5-cicd.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sbseg-article/img/fig4-testcomp2026.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sbseg-article/img/fig2-pipeline.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sbseg-article/img/fig1-timeline.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sbseg-article/.gitignore | Updated as part of this pull request. |
| docs/paper-sbseg-2026/references/references.bib | Updated as part of this pull request. |
| docs/paper-sbseg-2026/figures/fig5-cicd.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/figures/fig4-testcomp2026.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/figures/fig3-passes.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/figures/fig2-pipeline.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/figures/fig1-timeline.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/appendix/reprodutibilidade.md | Updated as part of this pull request. |
| docs/map2check_migration_plan.md | Updated as part of this pull request. |
| cmake/FindCrabLlvm.cmake | Updated as part of this pull request. |
| cmake/FindAFLPlusPlus.cmake | Updated as part of this pull request. |
| .gitmodules | Updated as part of this pull request. |
| .github/workflows/release.yml | Updated as part of this pull request. |
Review effort: Balanced
| <propertyfile>/home/bench/benchexec_files/tests/castle/benchexec/properties/valid-memcleanup.prp</propertyfile> | ||
| </tasks> | ||
|
|
||
| <tasks name="CASTLE-reachability"> |
| * a live allocation. Stops at the first invalid byte (ERROR_DEREF is set and | ||
| * the caller's map2check_check_deref reports it), before reading it. */ | ||
| void map2check_check_cstring(const char *string) { | ||
| if (string == NULL) return; |
Comment on lines
+9
to
+10
| <includesfile>/home/bench/benchexec_files/tests/castle/benchexec/sets/castle-memsafety.set</includesfile> | ||
| <propertyfile>/home/bench/benchexec_files/tests/castle/benchexec/properties/valid-memsafety.prp</propertyfile> |
Comment on lines
+8
to
+14
| int sum = 0; | ||
| for (int i = 0; i < 4; i++) { | ||
| sum += __VERIFIER_nondet_int(); | ||
| } | ||
| if (sum == 10) { | ||
| reach_error(); | ||
| } |
# Conflicts: # .github/workflows/ci.yml # TODO.md # modules/backend/library/lib/NonDetGeneratorKlee.c # modules/backend/library/lib/NonDetGeneratorLibFuzzy.c # modules/backend/library/lib/NonDetLog.c # modules/frontend/map2check.cpp # tests/unit/CMakeLists.txt Co-authored-by: hbgit <1494322+hbgit@users.noreply.github.com>
Co-authored-by: hbgit <1494322+hbgit@users.noreply.github.com>
Contributor
Merged |
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.
…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.
feat(testcomp): one wrapper and one tool-info module for SV-COMP and Test-Comp
Mirrors sosy-lab/benchexec#1352 after review: executable() reads the major version from the wrapper into self._version (the current version if the wrapper does not report one); _major_version is gone. The checklist's H1.4 still named the removed Test-Comp module and wrapper.
…ackage (Oct 21-24)
Test-Comp 2027 reported Map2Check runs ended by the OS OOM killer, the tool filling the disk. Under BenchExec what a tool writes sits in a tmpfs counted toward the run's memory limit, so the two are one symptom. Each .ktest carries every symbolic object whole: ~770 KB on the Intel-TDX havoc tasks. In Cover-Branches KLEE wrote one per terminated path and dumped every live state at the end of a phase -- 2651 tests (2.0 GB) for a suite that took 36, then 2470 that it took none of. A path that covers no new code adds nothing to a branch-coverage suite, so KLEE now gets --only-output-states-covering-new there; the filter also applies to the states dumped at halt. Property modes keep every test. Measured with the submitted archive against one that differs only in the map2check binary and wrapper (900 s, one run per arm): - TDX cover-branches: peak disk 2.31 -> 0.20 GB, memory 5.08 -> 1.64 GB, suite 50 -> 50; - TestCov 3.11 coverage: fermat1-ll_valuebound2 37.5 -> 37.5 %, Problem10_label22 37.81 -> 51.24 %, Problem05_label57 2.57 -> 3.85 %. The suite is filled first come, first served (#92): without the redundant paths, later KLEE phases find room. Test 40 pins the filter (64 paths over the same code: 64 tests before, 5 after). Test 5's program, which relied on those 64 redundant paths to reach the cap of 50, now has 64 paths through code of their own.
BenchExec leaves RLIMIT_CORE as it finds it -- unlimited in the containers measured -- and keeps what the tool writes in a tmpfs counted toward the memory limit. Map2Check replays vectors natively, and a replay that reaches abort() could drop a core the size of the process there. The wrapper lowers the soft limit to 0 before starting map2check, in both modes. test_wrapper_core_dumps.sh runs the wrapper against a fake map2check that records the limit it was started with; it runs in the Test-Comp CI job.
The comment added with the core-dump test said "the run's memory limit". The whole step is `bash -c '...'`, so that apostrophe closed the quote: the container script ended there, and the wrapper test, the Cover-Branches test and the TestCov suite ran in the runner's shell, outside the container, where testcov was never installed -- "testcov not found", exit 2.
fix(testcomp): KLEE writes only new-coverage paths in Cover-Branches; wrapper disables core dumps
chore(benchexec): one tool version in the tool-info module
docs(tacas): log the V99c wrap-up, the Rust ports and the Test-Comp package (Oct 21-24)
The Test-Comp 2027 pre-run (900 s, 3 GB) ended 1,747 runs as OUT OF MEMORY. BenchExec enforces the limit on the whole run, tmpfs included, and none of the engines knew it: - 821 runs died in KLEE's seeding loop, which never checks --max-memory; - about 200 with KLEE at its fixed 2,000 MB cap plus the files in tmpfs; - 239 in the first fuzzer phase: afl-fuzz runs its target unlimited. Map2Check now reads the run's limit from the cgroup (memory.max, visible inside the BenchExec container; MAP2CHECK_MEMORY_LIMIT_MB overrides it): - KLEE's --max-memory is 40% of the limit, at most KLEE's default 2,000 MB, so a 15 GB run keeps the cap it had (MAP2CHECK_KLEE_MAX_MEMORY still wins); - the KLEE watchdog reads memory.current every half second, seeding included: SIGINT at 80% of the limit (KLEE halts and writes its tests), SIGKILL at 92%. A phase stopped this way counts as incomplete; - the afl-fuzz target (-m) and the native replays (ulimit -v) get a third of the limit. With no limit found, nothing changes.
afl-fuzz starts each forkserver with setsid() (afl-forkserver.c, 4.40c), so its targets sit in sessions of their own, outside the process group `timeout` signals. When `timeout -k` SIGKILLs afl-fuzz, a running target survives and keeps spending the run's CPU time after Map2Check is done: a 900 s BenchExec run ended with 870 s of wall time, 908 s of CPU time and TIMEOUT. A persistent-mode target stopped in raise(SIGSTOP) is also left in an orphaned process group. When afl-fuzz returns, every process whose argv[0] is this program's fuzzing or CmpLog binary (the names carry the program's hash) is killed. test_fuzzer_leftovers.sh: a fake afl-fuzz leaves such a process in a new session and exits. RED: it is still running after map2check; GREEN: gone.
…limit Under BenchExec with one core a run's CPU time came out up to 22 s above its wall time (888 s of CPU for 866 s of wall, 900 s / 3 GB). With a 20 s margin the run ended 12 s from a TIMEOUT.
fix(testcomp): keep the run below its cgroup memory limit; no fuzzing target outlives afl-fuzz
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Update for new version.