Bring the Test-Comp conformance work into develop (follow-up to #55/#56) - #57
Merged
Conversation
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>
Test-Comp conformance: emit test suites, gate them on TestCov, and revive --add-invariants on Clam
This was referenced Aug 22, 2026
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
2 participants
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.
Closes #54.
Why this PR exists
A stacking accident. #56 was based on
feat/castle-juliet-baseline, and the two merged in this order:developfeat/castle-juliet-baseline#56 landed on its base branch five minutes after that branch had already gone to
develop, so none of its 14 commits are ancestors ofdevelop. Verified commit by commit withgit merge-base --is-ancestor.This PR carries those 15 commits (14 + the merge of #56) the rest of the way. No new work — everything here was already reviewed in #56 and passed 9/9 CI there.
What it brings
Everything is described in detail in #56; the summary:
--generate-test-suiteproduces the artifact the competition scores (exchange format 1.1), plus--property-file,--test-suite-dir,--architecture, and SHA-256 for<programhash>.--add-invariantsrevived on Clamdev16— behind-DENABLE_CLAM=ON, off by default. This is option 1 of crabllvm (seahorn/crab-llvm) is incompatible with LLVM 16 —--add-invariantsis a no-op #54's desired outcome.map2check_nondet_doubletagged rowsUNSIGNEDklee_log.csv--add-invariantsaccepted and silently ignored on.bcinput (#54)Verification
ctest8/8, integration 73/73, TestCov conformance 6/6, and 9/9 CI green on #56 atc4ef3a355.Open items carried forward
Tracked in
docs/TESTCOMP-CHECKLIST.md, with findings B, G, K2 and gap G4 recorded in the findings report. TheInvariants (Clam)job reportsABSENTuntilghcr.io/hbgit/map2check-devis republished fromdevelopwith the newDockerfile.dev— which merging this PR triggers.Note on #54: the closing keyword only fires when a PR merges into the default branch (
master), so it will still need closing by hand or on the eventualdevelop→masterPR.🤖 Generated with Claude Code