Cover-Branches, engine measurement, and eleven defects the corpus found - #64
Merged
Conversation
Cover-Branches is the second scoreable Test-Comp category and Map2Check
scored nothing in it, because it had no source of per-path input vectors.
KLEE already had them. It writes klee-last/testNNNNNN.ktest per explored path,
each recording the symbolic objects in the order the program consumed them.
Nothing needed to be instrumented; the vectors were being computed and thrown
away.
The alternative was tried first and abandoned on measurement. Having the
instrumented program write one log per terminating state turned a 1-second run
that answered FALSE into a 100-second run that exhausted its budget and
answered TRUE: every write is an external call KLEE executes concretely, and
enough of them corrupt the result rather than merely slowing it. Reading
.ktest files after the search has finished costs the search nothing.
modules/frontend/test_suite/ktest_reader.{hpp,cpp}
Parses the format directly rather than shelling out to ktest-tool --
nine lines of big-endian counts, against putting a Python interpreter
between a verification run and its suite. Decoding is driven by the
object NAME, which is where the type lives: a .ktest records name, size
and bytes but no type, so signedness has nowhere else to come from. Read
as unsigned, -1 becomes 4294967295.
--cover-branches
Emits one test case per path, coversError false throughout: these are
paths, not violations. Capped at 500 -- the competition scores coverage,
not volume, and every test case costs the validator a compile-and-run.
The wrapper and the BenchExec tool-info stop refusing the property. Both used
to raise rather than accept it, deliberately, so that scoring zero could not be
mistaken for participating; that reason is gone.
Evaluation harness, for runs this repository could not do before:
tests/testcomp/fetch-benchmarks.sh shallow clone of sv-benchmarks (~13 GB,
gitignored, never committed)
tests/testcomp/build_corpus.py stratified manifest, quota per
subcategory and a deterministic stride
inside each -- a uniform sample of 33k
tasks would just report the shape of
the benchmark, where Floats and ECA
alone are 2.6k
tests/testcomp/run_testcomp_evaluation.sh
runs the corpus, hands every suite to
TestCov, resumes from its own CSV
Verified end to end: 7 test cases from KLEE paths on a six-branch program,
TestCov reporting 100.0% coverage over 6 goals. Unit tests 9/9 suites,
including 16 new ones pinning the .ktest parse against bytes built by hand --
a misparse yields plausible numbers, not a crash, and is silent all the way
down to a suite that covers nothing.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The first version mapped Result: DONE to FULL and Result: UNKNOWN to PARTIAL for cover-branches, on the inference that DONE meant 100% coverage. The running corpus disproved it within minutes: DONE appears at 77.78% and at 11.11% as readily as at 100%. What the Result line actually distinguishes is whether TestCov validated cleanly (DONE) or had to abort a test's execution (UNKNOWN). Neither says anything about how much was covered -- the coverage column beside it does, in both cases. FULL and PARTIAL read as a claim the line is not making, so they are now VALIDATED and VALIDATED_ABORTS. Replaced by rename rather than edited in place: nine containers have this script open, and truncating the inode under a running bash makes it execute whatever lands at its current offset. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The running containers hold the pre-fix inode of the evaluation script, so this run writes FULL/PARTIAL where the script now writes VALIDATED/VALIDATED_ABORTS. Recording the equivalence beside the data, because in five hours the CSV will be read by someone -- me -- who no longer has that in mind, and FULL reads as a coverage claim it never was. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
H1.3 is closed by a different route than the plan assumed. It asked for a per-input log from the runtime; that was built, measured, and thrown away (1s/FALSE became 100s/wrong-SUCCEEDED under KLEE). KLEE's own .ktest files are the same vectors at no cost, which is what the entry now records. H2.5 follows immediately: --cover-branches, accepted by the wrapper and the tool-info, validated by TestCov at 100% on a six-branch program. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…uota 150 Two defects in the corpus builder, both of which only bite when the corpus grows or a run is cut short -- which is exactly what happened. Sampling was not nested. An even stride recomputes every index when the quota changes, so raising it substitutes tasks rather than adding them. Measured on the real pool sizes: going from 40 to 150 per subcategory kept 12 of 40 tasks in Arrays and 10 of 40 in Loops, Floats and ECA -- 70% overall, but the large families almost entirely resampled, which would have thrown away measurements already taken. Replaced by a breadth-first recursive bisection order, whose prefixes both spread evenly over the family AND nest: the first 40 of the sequence are the first 40 of any longer one. Verified 40/40 preserved at 150. The manifest was grouped by subcategory. Every run here is deadline-bounded, and a truncated grouped manifest means the run finished Arrays and never reached XCSP -- discarding the stratification the sampling exists to provide. Rows are now written round-robin across subcategories, so any prefix is balanced. Quota raised to 150: 818 cover-error tasks (limited by availability in eight of the twelve subcategories) and 1522 cover-branches. sv-benchmarks checked against upstream while doing this: cd68d4ed3, current. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…h them free Running 2340 real Test-Comp tasks surfaced six defects that every existing test was blind to. Each produced well-formed output, a plausible verdict and a green run; what none produced was a suite a validator would accept. L. A Cover-Error suite came out with no <input> at all. The state that reaches the target aborts, an aborted KLEE state runs no exit handler, and the flush that writes klee_log.csv never happens. 290 of the 376 runs that reported FAILED emitted an empty test case: the tool had found the bug and could not prove it. KLEE marks the failing path with a .err beside its .ktest, so the vector is recoverable without the runtime's cooperation. M. --property-file was never read when relative, which is how BenchExec and every harness here pass it: resolveSpecification runs after the pipeline has chdir'd into the scratch directory. Invisible because the fallback guess happens to match the real property text for both categories -- no output differed, so no test could see it. The regression test uses a specification the fallback could not invent. N. --cover-branches fell through to the MEMTRACK default and instrumented memory tracking for a task that checks no property. There is now a COVER_BRANCHES_MODE whose pipeline is nondet-pass and nothing else. O. MemoryTrackPass registered map2check_malloc with an i64 size and passed the program's own operand through uncoerced. A program allocating with i32 -- what the CIL-processed sources in ProductLines and ECA do -- produced a call whose type did not match its signature, and LLVM rejected the module: 110 of 110 ProductLines tasks died two seconds into a sixty-second budget. It survived because Juliet and CASTLE allocate with i64. P. The 500-test-case cap made suites unvalidatable. Of 116 tasks whose validation failed outright, 115 had at least 100 test cases and the median was exactly 500. Lowered to 50. Q. KLEE lost its entire exploration when the budget ran out, which in a competition run is the normal case rather than an edge. It was bounded only by an external `timeout`, and the states still live at the kill were never written: "unable to write output test case, losing it", 3982 times, for a total of zero test cases from 3982 explored paths. Two changes: KLEE now gets its own --max-time below the external one so it halts rather than being killed, and Cover-Branches searches depth-first so states terminate in sequence and each writes its test as it goes, instead of thousands sitting live until a halt that cannot write them. tests/integration/test_testcomp_regressions.sh covers all six, wired into CI. Writing it caught one more thing worth keeping: the cap assertion first read "at most 50" and passed against a run that produced ZERO test cases. It asserts equality now -- an upper bound is satisfied by emptiness, which is the failure it was meant to detect. Also committed: the measurement data behind the findings. cover-error is the complete 818-task campaign; cover-branches is 1344 of 1522, stopped to implement these fixes. Partial is still balanced -- the manifest interleaves subcategories, so a prefix samples all twelve. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…turns 4 main() discarded the return value of map2check_execution() at all three call sites, so the process always exited 0 -- or SIGABRT from the --expected-result path, which used abort(). The Test-Comp tool-info decides DONE vs ERROR from exit_code == 0, so an internally failed run was reported DONE; and a --expected-result mismatch signalled with a signal, which BenchExec reads as "the tool crashed" -- the opposite of the truth. main() now returns the code from map2check_execution(), and a mismatch returns the new ERROR_EXPECTED_RESULT (4) instead of abort(). Exit 0 still means "the analysis ran to a verdict": SV-COMP parses the verdict from stdout, and any non-zero code is read as a crash by BenchExec, so the verdict must not migrate into the exit code. tests/integration/test_exit_codes.sh pins the contract: a FALSE verdict keeps exit 0 (verdict on stdout), a matching --expected-result exits 0, and a mismatch exits 4 rather than 134.
…lity mode Thirteen CWEs were mapped to `--target-function --target-function-name main`, which is degenerate (finding B): TargetPass instruments call sites whose callee is the named function, and a program never calls its own main, so nothing was instrumented and every vulnerable case was reported TRUE. On the v6 baseline that earned 12 fake true negatives and 5 guaranteed false negatives. 628/674/770/835 are termination/resource properties Map2Check does not model; the other nine are injection/crypto categories outside its scorable set. They now live in OUT_OF_SCOPE_CWES and are skipped outright (recorded N/A) instead of run under the degenerate mode and burning a full budget per case. tests/integration/test_cwe_mode_mapping.sh asserts no CWE maps to --target-function, that 628/674/770/835 are out of scope, and that every benchmark CWE is explicitly mapped or declared out of scope.
…is not one either
Three defects behind the Cover-Error recall of 13.9%, all found by following
one unconfirmed FAILED case down to its cause.
The verdict could come from uninitialised memory.
CheckViolatedProperty::propertyViolated had no initialiser. The constructor
assigns it on several paths but NOT when map2check_property exists and is
empty, nor when it holds a line the parser does not recognise -- the `else`
that would have caught that is commented out. Both cases left the field holding
whatever was on the stack, and that value decided the verdict. It is reachable:
a KLEE state that aborts early creates the file without writing to it. Observed
as the same program answering FAILED, SUCCEEDED and nothing at all across three
runs, and it is the best candidate for the ERROR/UNKNOWN churn that shows up in
every baseline comparison. Defaulted to UNKNOWN, and the unrecognised path now
says so instead of falling through in silence.
An assumption was being read as a violation. The SV-COMP idiom is
void assume_abort_if_not(int cond) { if (!cond) abort(); }
and KLEE runs here with --exit-on-error-type=Abort, so the first path that
violates an assumption halted the entire search AND left an abort.err that
looks exactly like a real violation. NonDetPass already renames
__VERIFIER_assume, which works because that one is only declared; these carry
their own body, so renaming would collide with the runtime's definition. The
body is replaced instead -- one rewrite reaches every call site.
Measured over the 818-task corpus, the categories saturated with this idiom are
exactly the ones with no recall: Sequentialized 86% of tasks and 0 confirmed,
Floats 82% and 0, Arrays 71% and 1.
And the .ktest fallback added yesterday was too permissive -- my own bug. It
accepted ANY .err as the violating path, so an assumption abort was recovered
and emitted with full confidence: one suite carried 25 inputs and covered 0.0%.
It now accepts only .abort.err, and only when the runtime actually recorded a
violation.
Verified against the two cases that motivated it:
pals_lcr.6_overflow v8: FAILED, 25 bogus inputs, not covered
v9: UNKNOWN, 0 inputs <- false positive gone
ps6-ll_unwindbound20 v8: FAILED, TestCov UNKNOWN
v9: FAILED, TestCov TRUE <- now confirmed
test_testcomp_regressions.sh is at 10 assertions; the new ones put the error
behind two assumptions, so a run that still halts on the first cannot reach it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… run The quota-40 corpus is an exact subset of the quota-150 one -- a property the nested-sampling fix bought -- so v9 compares pairwise against v8 on the same tasks at 44% of the cost. Split into treatment (the five categories saturated with assume_abort_if_not, 158 tasks) and control (the other seven, 214). The control group is what separates 'the fix worked' from 'the run varied'. Predictions written before launching, because last time I predicted 30-50% for cover-error and measured 13.9%. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Measured pairwise against v8 on 199 tasks, the previous commit's gate cost more than it saved: twelve tasks that HAD been covered stopped being covered, all twelve ERROR -> UNKNOWN with an empty suite. Every one was a case where the target really was reached and the runtime never wrote it down -- the state that reaches the target aborts, an aborted KLEE state runs no exit handler, and map2check_property is written by that handler. So foundViolation being false does not mean nothing was found; it means nothing was recorded, and it is false precisely in the case that matters. Requiring foundViolation was a defence against picking up an assumption failure, whose abort looks identical to a real one. That defence now lives upstream where it belongs: NonDetPass rewrites the abort-based assumptions into path pruning, so an abort.err can no longer BE an assumption. With the source of false aborts gone, the gate only blocked legitimate recoveries. The recovery therefore moves ahead of the early return, for reachability mode only, and says out loud when it fires -- a suite emitted on a run that reported no violation is worth a line in the log. Worth recording how this was caught: the control group. The run was split into categories saturated with the assumption idiom and categories without, and it was the CONTROL group moving -- 30 covered down to 19 -- that exposed the regression. A single-group run would have shown the treatment gain and hidden the cost underneath it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… is undecided
Two defects on the LibFuzzer path, both found while designing the seed
exchange, and the first of them is what made that exchange impossible.
Every generator took ONE byte and cast it to the type:
#define MAP2CHECK_NON_DET_GENERATOR(type) \
type map2check_non_det_##type() { return (type)get_next_input_from_fuzzer(); }
so a long, a short, a size_t or a pointer could only ever hold 0..255, and a
double could only be an integral value between 0.0 and 255.0. Nothing negative
was reachable at all: an unsigned byte cast to a signed type stays
non-negative. Half of every signed type was outside the fuzzer's reach. Only
int differed, and it read EIGHT bytes to build a value it then truncated to
four.
Measured on a short:
short s = nondet(); if (s < 0) before: not found after: FAILED
short s = nondet(); if (s == -4242) before: not found after: FAILED
The first of those is half of all values.
It also blocked what this was groundwork for. The byte layout IS the exchange
format between the engines, and a KLEE vector holding short x = 4242 cannot be
written into a slot one byte wide. sizeof(type) is exactly what
NonDetGeneratorKlee.c already passes to klee_make_symbolic, so both engines
now agree on what a vector means -- the prerequisite for seeding either from
the other.
While there: the fuzzer-chosen string length feeding malloc in
map2check_non_det_pchar is now bounded. With a full-width unsigned it could ask
for four billion bytes.
Second defect: the UNKNOWN branch was guarded on the generator being KLEE, so
an undecided LibFuzzer run printed no verdict line at all -- and every harness
here, plus the BenchExec tool-info, reads that silence as a crash. It is
finding G one layer up: the analysis concluded and did not say so. Whole
categories in the engine comparison were recorded as ERROR for this reason.
Worth recording a mistake of my own: my first three micro-benchmarks failed on
everything, including char == 65, and I nearly reported the fuzzer path as
broken. They only DECLARED reach_error. LibFuzzer detects a violation through
the crash file the abort produces, and the benchmarks define reach_error to
call __assert_fail; without a body that aborts there is no crash to catch. The
tool was right and the test was wrong -- caught by running the same case
against the previous build and seeing identical behaviour.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Every Test-Comp measurement in this repository forced --nondet-generator
symex, so all of them measured a mode nobody runs: the tool's own default,
with no generator flag, is LibFuzzer at 0.2x the budget and then KLEE.
Measured on the same 372-task corpus, paired:
symex 23% covered
fuzzer 35% covered
hybrid 47% covered
and the hybrid captured the entire UNION of what the two engines cover alone --
13 tasks only the fuzzer reaches, 6 only KLEE reaches, and the hybrid gets all
of them. Running the weaker engine first for a fifth of the budget costs almost
nothing and loses nothing.
Both harnesses now default to it, including the CI gate, which was exercising a
configuration the competition never sees.
Result directories written before this carry symex numbers. They are not
comparable to hybrid runs and must not be pooled.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The two engines cover almost disjoint sets. Measured over the same 372 tasks:
65 covered only by the fuzzer, 47 only by KLEE, and the hybrid takes the whole
union. Until now they shared nothing -- KLEE started from scratch after the
fuzzer had finished, knowing none of what it found.
LibFuzzer was not even keeping its own corpus. The command carried no corpus
directory, so everything discovered in its fifth of the budget lived in memory
and died with the process, every run.
seeds/ a directory both engines read and write, in the scratch
directory they already share as a working directory. A
directory rather than a value handed between phases,
because it has to survive between phases, between runs and
between alternations -- which is what time-slicing needs.
KLEE -> fuzzer each explored path's .ktest becomes a seed file.
Concatenating a .ktest's objects yields exactly the buffer
that drives the fuzzer down the same path -- sound only
since both engines started consuming sizeof(type) per read.
Before that fix most vectors had nowhere to go.
third phase the order is fuzzer then KLEE, so KLEE's vectors had no
consumer inside the same run and the exchange would only
have paid off on a later one. A short seeded fuzzer phase
now closes the loop: KLEE solves the guard mutation cannot
reach, and the fuzzer moves outward from there faster than
KLEE can fork.
Under a fixed budget this is not merely speed. Every second KLEE spends
rediscovering a path the fuzzer already walked is a second not spent going
deeper, so the exchange buys depth the run would not otherwise reach.
Behind --seed-exchange, off by default: the hybrid was measured at 44.6%
covered over 372 tasks in its current shape, and that figure has to keep
meaning what it means until this one is measured beside it.
Known limitation, stated rather than hidden: the fuzzer -> KLEE direction is
implemented but rarely fires. It reads the runtime's nondet log for the typed
vector, and that log is only written on a violating execution -- which is
precisely the case where KLEE is no longer needed. Carrying a fuzzer corpus
file back into a .ktest needs the type sequence of the reads, which the raw
bytes do not carry; recovering it means replaying each corpus entry through
the instrumented binary with logging on. Left for when the measurement says
the direction is worth that.
The tests assert the mechanism, not a coverage gain: that the channel exists,
stays off by default, and carries vectors in the direction it claims. Whether
cooperation finds more is a question for the corpus.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…alysing it Phase 2 of the migration plan, and the direct answer to finding K2: a nondeterministic read cost 1 -> 21 -> 114 -> 861 partial paths for 2 -> 4 reads, and most of that forking happens in code that cannot influence the target. Slicing removes it before KLEE ever sees it. Measured on the probe the image build runs: 126 lines of IR down to 66, "Sliced away 30 from 39 nodes", and the irrelevant 50-iteration loop -- one multiply in the original -- gone entirely from the slice. Getting DG to build against LLVM 16 took five obstacles, and two of them are worth writing down because the next person will hit them: master does not compile. It calls llvm::Function::getBasicBlockList(), which LLVM 16 made private. The maintained version is the llvm-latest branch, whose newest commit is literally "Fix build for LLVM < 18" -- the same shape as crab-llvm having been renamed to Clam, where the supported path existed under a name nothing referenced. DG must be built IN-SOURCE. sbt-slicer's CMakeLists documents DG_PATH as "a path to an in-source build of dg" and derives both include and library paths from it; an out-of-tree build satisfies neither, and the failure surfaces as a missing dg/tools/llvm-slicer-opts.h. Plus: both projects pin C++14 with a plain set() that overrides the command line, while LLVM 16's headers need C++17 (llvm-latest already ships 17); and sbt-slicer links dg's shared libraries without an rpath, so without LD_LIBRARY_PATH the binary builds and then dies on every invocation. Behind --slice, off by default, and for reachability only. This is not a neutral speed-up: a slice taken with respect to one error site can legitimately remove another, so a sliced run answers a NARROWER question. Right for a competition task with one property, wrong for a baseline scoring precision per CWE. Cover-Branches gets no criterion at all -- every branch is the goal -- and asking there is refused rather than ignored. The tests assert the unhappy paths, because that is where this class of feature fails: --add-invariants spent years accepted and silently ignored (issue #54), and a slicer that quietly does nothing would be the same defect renamed. An absent slicer must say so; a mode with no criterion must refuse. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… the image v11 answers "what do slicing and seed exchange buy", which is a comparison against v10 -- so the two cannot share a machine. The tool's LibFuzzer phase runs with -jobs=8, and ten containers already put this host at twice its core count (load 31 on 16 cores); a second campaign alongside would leave both numbers unattributable, which is the mistake that cost a day earlier this week when contention was read as a regression. The launcher waits for two things instead. The v10 containers to finish, and the republished image to actually carry sbt-slicer -- the second is not a formality, because --slice degrades gracefully when the slicer is absent, so launching too early would produce a full campaign that silently measures nothing. Two arms, so the features stay separable: slice against v10 isolates slicing, slice+seed against slice isolates the exchange. cover-error only, because slicing needs a criterion and Cover-Branches has none. EXTRA_FLAGS is how an opt-in capability gets measured against a run without it; it is kept apart from GENERATOR because --slice and --seed-exchange sit on top of whichever engine is running rather than replacing it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two arms measured the seed exchange only in the PRESENCE of slicing. If it helps alone and hurts combined -- or the reverse -- that design cannot see it. Four cells separate each feature and their interaction. The control cell runs inside v11 rather than reusing v10, even though v10 measures the same configuration on the same corpus. v10 ran with ten containers on a host already at twice its core count; v11 runs with twelve. Comparing across that difference carries contention into the result -- the exact confound the chaining was introduced to avoid, and the one that cost a day earlier this week when contention was read as a regression. One extra arm removes the question instead of arguing about it afterwards. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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
1 participant
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.
Fifteen commits. The through-line: running Map2Check over a real Test-Comp corpus for the first time, and fixing what that exposed.
The headline numbers
Cover-Branches went from unsupported to scoring. Effective branch coverage, paired over 1344 tasks:
TESTCOV_ERRORCover-Error confirmation nearly doubled, paired over 372 tasks: 12.6% → 13.9% → 27.2% across v7/v8/v9. FAILED verdicts fell from 145 to 93 while confirmations rose from 41 to 62 — fewer claims, more proof.
The hybrid is the best engine and nobody had measured it. Every Test-Comp measurement in this repository forced
--nondet-generator symex, a mode nobody runs:The two engines cover almost disjoint sets — 65 only the fuzzer reaches, 47 only KLEE — and the hybrid takes the whole union, for less wall clock than KLEE alone. Both harnesses now default to it.
The defects
Each was invisible to the tests that existed: they produced well-formed output, plausible verdicts, and green runs.
<input>— the aborting state runs no exit handler, so the nondet log is never written--property-filenever read when relative; the guess happened to match, so no output differed--cover-branchesfell through to the MEMTRACK defaultMemoryTrackPassemitted a type-mismatched call; LLVM rejected the modulemap2check_propertywas emptyassume_abort_if_notread as a violation — an assumption abort is indistinguishable from a real onedoublelimited to 0.0–255.0Plus G (exit code never propagated) and B's harness half (13 CWEs mapped to a degenerate mode), both from @OpenCode.
New capabilities
Cover-Branches (
--cover-branches) emits one test case per KLEE path, from its.ktestoutput. The alternative — having the runtime log each state — was built, measured and thrown away: it turned a 1s run answering FALSE into a 100s run that exhausted its budget and answered TRUE.Seed exchange (
--seed-exchange, off) gives the engines a shared seed corpus. Measured over 372 tasks: +2 covered, +15% time. That is noise, and it is not promoted. Stated plainly because only half the channel works — fuzzer→KLEE needs the type sequence that raw corpus bytes do not carry.Slicing (
--slice, off, reachability only) via DG + sbt-slicer. Probe: 126 → 66 lines of IR, 30 of 39 DG nodes removed. Not yet measured on the corpus — the image has to republish first.Evaluation infrastructure:
fetch-benchmarks.sh,build_corpus.py(nested sampling, category-interleaved manifest),run_testcomp_evaluation.sh(four engine arms, resumable).Integrating DG was five obstacles
Worth recording, because the next person hits them:
masterdoes not compile against LLVM 16 — it callsgetBasicBlockList(), made private. The maintained branch isllvm-latest, newest commit "Fix build for LLVM < 18". Same shape as crab-llvm having been renamed to Clam.sbt-slicerdocumentsDG_PATHas an in-source build and derives include and library paths from it.set()that overrides the command line, while LLVM 16 needs C++17.sbt-slicerlinks DG's shared libraries without an rpath.--add-invariantslesson (crabllvm (seahorn/crab-llvm) is incompatible with LLVM 16 —--add-invariantsis a no-op #54).Tests
tests/integration/test_testcomp_regressions.sh, 18 assertions, one per defect, wired into CI. Two are worth calling out:Unit tests 9 suites; the
.ktestparser is pinned against bytes built by hand, because a misparse yields plausible numbers rather than a crash.What is not settled
XCSP0/40,Sequentialized1/40,ECA2/40 — zero across all three engines. 120 tasks where the bottleneck is not the search.ERROR↔UNKNOWNchurn persists: 2.6%, 2.4%, 3.3% across the three baseline comparisons. I reported it fixed after a 532-case sample showed zero; the full 2108 says otherwise, and the cause is still open.