[GuilhermeBn198]

The full 9.0 campaign (the v15 corpora, paired task by task) is complete, and the assume-pruning defect it found is fixed and re-measured: see Full 9.0 campaign below.

Summary

This PR merges the whole TACAS line into one branch and sets the version to Map2Check 9.0.0. It covers:

• smart seeds;
• slicing optimizations;
• engine alternation;
• the fixes that made TRUE sound again;
• a study of --add-invariants.

Nine stacked branches are merged, plus the release and default commits on top of develop:

branch	scope
feat/tacas-smart-seeds	3a: seed store and typed seed exchange, plus the verdict fixes
feat/tacas-2d-slicing	2d: slice once per run, faster criteria, experiment knobs
feat/tacas-3b-alternation	3b: --alternate-engines, AFL++ build cache, fixes from review
feat/tacas-memtrack-intrinsics	memset/memcpy/memmove checked under LLVM 16
feat/tacas-3c-seed-ranking	3c v1: new-edge entries first
feat/tacas-memtrack-strings	%s/puts string checks (off by default)
feat/tacas-fuzzer-suite	the fuzzer corpus as Cover-Branches cases (off by default)
feat/tacas-klee-vector-replay	KLEE vectors replayed natively; harness and input fixes
feat/tacas-invariants	Clam profiles, invariant count, MAP2CHECK_PREOPT=ssa

New defaults (measured in R26)

• The hybrid is the alternation (--alternate-engines, with seed exchange) whenever --timeout is given.
  • On Cover-Error it ties the seed-exchange hybrid (157/213 each).
  • On Cover-Branches it leads (53.5% vs 46.5%, partial).
  • --fixed-hybrid keeps the 8.x schedule.
• The fuzzer's corpus joins Cover-Branches suites (MAP2CHECK_FUZZER_SUITE=0 drops it).
• Everything else stays off, and each knob is documented in the README with what it was measured to do:
  • --add-invariants (optional and under study, see docs/backlog.md);
  • MAP2CHECK_PREOPT=ssa;
  • MAP2CHECK_CHECK_CSTRINGS;
  • the slice knobs.

Why 9.0.0 and not 8.2

• The engine changed, from LibFuzzer to AFL++ 4.40c. --nondet-generator fuzzer is now --nondet-generator afl.
• Several verdicts change meaning, so the same program can get a different answer than under 8.x:
  • a KLEE run that did not explore every path is no longer TRUE;
  • the program's own abort() prunes the path instead of ending KLEE's search.

Changes

Verdict soundness (these fixes affect every mode)

• The program's abort() prunes the path. NonDetPass rewrites the program's abort() into map2check_assume(0). SV-COMP benchmarks use abort() as an assumption, both inline and through assume_abort_if_not. With --exit-on-error-type=Abort, KLEE used to end its whole search on the first such path and answer TRUE. This was the cause of every wrong TRUE of the control arm in R15: the pals_* family and sin_interpolated_index-1.
• KLEE's exit 0 is not a proof unless it explored every path. The following now make the run incomplete, and so UNKNOWN:
  • the HaltTimer;
  • a concretized input ("silently concretizing", for example a symbolic double pinned to 0);
  • any *.err or *.early state;
  • the memory cap ("skipping fork", "over memory cap");
  • a KLEE run with no done lines, meaning it crashed.
• Assumptions under KLEE prune with klee_silent_exit. A failed klee_assume(0) is a KLEE user error, and it counted as a dropped path. An intermediate version of this PR had that bug: it read partially completed paths and could not prove any program that contains an assumption. Fixed and covered by a test.

Engines and seeds

• Seed store <hash>.seeds/ (3a). The store lives beside the scratch directory, so it survives the phases. Exchange works in both directions:
  • the AFL++ queue is replayed through the witness binary into typed .ktest seeds for KLEE;
  • KLEE's vectors go back to the fuzzer, all of them, uncapped.
• --alternate-engines (3b). AFL++ and KLEE take turns:
  • a turn ends when its engine stagnates: AFL_EXIT_ON_TIME for AFL++, and for KLEE the covered instructions read from run.stats (SQLite is optional at build time; SIGINT goes to the KLEE pid);
  • windows (0.1T for the fuzzer, 0.3T for KLEE) and the stagnation patience double every round;
  • each phase measures its own setup time and deducts it from the budget.
• KLEE's vectors replayed natively. After a KLEE phase that found nothing, KLEE's vectors are completed with zeros past their end and run through the witness binary. KLEE's partial paths often go on to the error. The seed-exchange hybrid used to find these only by accident, in its last fuzzer dry run.
• AFL++ binaries built once per run (<hash>.build/), and the three builds share one budget.
• 3c v1: AFL++ queue entries marked +cov are sent to KLEE first.

Slicing

• Slice once per run (<hash>.slice/, keyed by content). A slicer failure is cached too.
• Criteria collected by a plain scan instead of std::regex: on the eca-* programs the regex took about 45 s.
• Experiment knobs: MAP2CHECK_SLICE_CLEANUP=light|o2 and MAP2CHECK_SLICER_FLAGS. None was promoted: every variant stayed within ±3 tasks.

Memory safety

• Memory intrinsics are checked. MemoryTrackPass matched llvm.memset/memcpy by their LLVM 6 names, so under LLVM 16 no intrinsic was checked and memmove never was. It now dispatches on MemSetInst / MemTransferInst.
• MAP2CHECK_CHECK_CSTRINGS=1, off by default. Under KLEE, printf runs as an external call, so a %s read of an unterminated buffer was never checked.
  • It fixes a wrong TRUE in Juliet CWE121 CWE193 cpy bad.
  • It creates a wrong FALSE in the matching good task. There the terminator is an uninitialized byte, which SV-COMP counts as zero.
  • It stays off until a larger Juliet sample decides between the two.

Test suites

• The Cover-Branches cap of 50 and the deduplication apply across phases, and every run starts from an empty suite.
• MAP2CHECK_FUZZER_SUITE=1, off by default: the fuzzer corpus becomes Cover-Branches test cases, up to half of the suite.

--add-invariants (INV-1 in the log)

• The history of the old engine:
  • The SV-COMP 2019/2020 builds (v7.3.x) ran crab-llvm with --crab-promote-assume. That flag emits llvm.assume, which NonDetPass does not map and which KLEE ignores. I tested this on the release's KLEE 2.1 and on KLEE 3.1, with and without --optimize. In those builds the invariants had no effect.
  • Before October 2018 the configuration was --crab-track=arr --crab-add-invariants=after-load, and the invariants did reach KLEE.
• Where the gain actually came from. On a probe loop program, a safe variant and a buggy one, compiling through Clam decided both even with no invariant inserted. The gain came from the SSA preprocessing, not from the invariants.
• What this PR adds:
  • MAP2CHECK_CLAM_PROFILE=default|memory|none;
  • the number of invariants inserted, in the log;
  • a fallback when Clam fails;
  • MAP2CHECK_PREOPT=ssa (mem2reg + simplifycfg), for reachability and assert only. With it on, the memory modes produced FALSE-FREE on safe programs.

Unmodeled nondet types (#74)

• The fix. NonDetPass instrumented only 16 __VERIFIER_nondet_* types. A call to float, longlong, ulonglong, u8/u16/u32 or __VERIFIER_nondet_memory was an external call: KLEE killed every state and the task was UNKNOWN by construction.
• What each type now has:
  • a KLEE and an AFL++ generator of the right width;
  • a full-width log entry: 64-bit and float values no longer pass through the int logger, and floats print as %.9g so they round-trip;
  • decoding in the ktest reader.
• nondet_memory gives one uchar input per byte, which is how the validators' harness reads it.
• Tests: 8 new unit tests, and synthetic programs for each type: UNKNOWN before the fix, FAILED after, Result: TRUE on TestCov 3.11.
• What the fix uncovered: the KLEE nondet-log explosion (KLEE: gravar o klee_log.csv com valores simbólicos explode os estados no fim de cada caminho #75), fixed below.

KLEE nondet-log explosion (#75)

• Cause. At the end of each violating path, the KLEE runtime wrote klee_log.csv with fprintf, and the values were still symbolic. uClibc's vfprintf forks on every digit it converts. KLEE reached the target, then multiplied states while writing the log and never finished.

• The fix, each part driven by run.istats:

  • the logged values are pinned to one model before printing (klee_get_value + klee_assume, in order, so the row stays one consistent vector);
  • the rows are formatted without printf. Even with concrete values, vfprintf was 93% of a 1,000-read path. The file is byte for byte the same (NonDetLogTest);
  • a log past 1,024 rows is not written. The violating .ktest carries the same vector, and the frontend already falls back to it;
  • the log container grows geometrically, and the heap copy that leaked one row per read is gone.

• Measured on a straight-line program with N nondet reads and the target at the end, KLEE only:

  N	before	after
  5	FAILED, 28 s	FAILED, 1 s
  10	UNKNOWN	FAILED, 1 s
  1,000	UNKNOWN	FAILED, 6 s
  10,000	UNKNOWN	FAILED, 31 s

• Intel-TDX is still 0/8 on the 300 s probe, with KLEE's default cap and with MAP2CHECK_KLEE_MAX_MEMORY=6000 (new knob, default unchanged). The log no longer blocks KLEE: it now completes about 850 paths per task, where it completed 0 before. What remains is the programs' own path explosion: thousands of havoc reads followed by a long validity precondition.

• Tests: integration 51/51; section 38 checks KLEE alone behind 12 nondet reads.

Official Test-Comp 2026 validation

• tests/testcomp/official/run.sh generate|validate runs the competition's own validators under BenchExec: TestCov gcc/clang unformatted and TestCoCa clang formatted. Each task gets its own property files, and each validator's scratch is dropped so a full corpus fits on disk.
• Official corpora (build_corpus_official.py), drawn from the Test-Comp 2026 task set with proportional stratification:
  • Cover-Error;
  • Cover-Branches, 3,500 tasks.
• The AFL++ toolchain ships as a self-contained archive for the validation image.

Smaller fixes

• AFL++ input past its end reads as zeros. Before, it wrapped around, so a while (nondet()) loop never ended and afl-fuzz aborted in its dry run.
• A fuzzer link error is reported with its cause, and an unreadable input program is reported clearly.
• Evaluation harnesses:
  • children no longer inherit the manifest descriptor (the program under test was moving the loop's file offset);
  • a crash replayed from the fuzzer is no longer classified as a tool failure.

Results

Full 9.0 campaign, paired with v15 (2026-10-05)

Setup. Both versions ran on the same tasks under the same conditions: the corpora of the v15 campaign, 300 s and 4 GB per task, compared task by task. 9.0 ran with its defaults: alternating hybrid, seed exchange, and the fuzzer corpus in Cover-Branches suites. The campaign build is 76eedfc75. The assume fix (e4e0b74c7, 6848d2395) came after the campaign; its rerun is reported separately below.

At a glance

corpus	what it measures	v15	9.0	change
Test-Comp Cover-Error (1,087 tasks)	tasks whose suite reaches the error, confirmed by TestCov (1 point each)	470	722	+252 (+54%)
Test-Comp Cover-Branches (2,765 tasks)	mean branch coverage of the suite, measured by TestCov	41.4%	45.1% (≈47.0% with the fix)	+3.7 p.p. (≈+5.6)
Juliet C (8,060 cases)	bugs found in the vulnerable variants (4,030 cases)	1,154 (28.6%)	1,808 (44.9%)	+654
	false alarms on the fixed variants (4,030 cases)	120 (3.0%)	120 (3.0%)	=
CASTLE (119 cases in scope)	bugs found / false alarms	54 / 1	54 / 1	=

Cover-Error: finding the error and proving its absence

A task counts only when TestCov runs the suite and confirms the error is reached. A wrong TRUE means the tool claimed the error unreachable on a task where it is reachable. The competition penalises that heavily, and it is what this line set out to remove.

	v15	9.0
covered (TestCov confirms the error)	470	722	+265 gained, −13 lost
wrong TRUE	175	0	soundness: a TRUE now needs an exhaustive KLEE run
ERROR (tool crash)	9	0
median time per task	176 s	72 s	the alternation stops early once it finds the error

By category (covered): ECA 58 → 146, ProductLines 111 → 169, Sequentialized 9 → 78, XCSP 22 → 38, Arrays 84 → 92, Loops 102 → 109. No category loses.

Cover-Branches: how much of the program the suite exercises

Score: the branch coverage TestCov measures when it runs the suite. A task with no validated suite counts as 0%.

	v15	9.0 (campaign)	9.0 + assume fix
mean coverage	41.4%	45.1%	≈47.0% (projected)
median coverage	38.5%	47.6%
tasks better / worse / equal vs v15	—	932 / 381 / 1,452
XCSP mean	77.6%	54.6% ⚠️	96.6%
TestCov failed to validate (TESTCOV_ERROR)	110	140	109 of them fail on v15 too; almost all ECA, where TestCov exceeds 300 s
median time per task	114 s	274 s	the alternation keeps working while the suite still grows

By category (mean coverage, v15 → 9.0): Arrays 60.7 → 76.2, BitVectors 60.6 → 70.0, ControlFlow 44.9 → 53.1, Recursive 57.8 → 65.3, Heap 40.6 → 47.3, Loops 70.5 → 73.8, LinkedLists 75.8 → 78.5, Sequentialized 56.0 → 58.7, Floats 5.4 → 6.7, ProductLines 20.3 → 20.7, ECA 10.5 → 10.6. XCSP was the only category that lost, and the fix below recovers it.

The assume fix. In the campaign build, a path that a failed assumption pruned under KLEE wrote no test. 50 tasks (43 XCSP, 7 Floats) ended with an empty suite. The fix has two parts:

• the pruned path ends normally (_exit), so KLEE writes its test;
• the test is marked, and when the suite reaches its cap of 50 a deeper path replaces it, even in a later phase. Without that, on xcsp/AllInterval the shallow pruned tests filled the suite first, and coverage fell from 95% to 9%.

Rerun with the fix (mean coverage, same conditions):

set	tasks	v15	9.0 (campaign)	9.0 + fix
tasks left with no test	50	88.8%	0%	88.8%
XCSP tasks that already had tests	76	64.9%	85.5%	94.7%
random control	100	46.9%	54.4%	55.0%
Cover-Error random sample (tasks covered)	100	—	63	63, still 0 wrong TRUE

The projected ≈47.0% replaces these 226 tasks in the campaign result; the other tasks were not rerun.

Re-run of the categories #74 affected (official corpus, 2026-10-12)

Same conditions as the V99 campaign on the official corpus: 900 s, 8 GB, 4 cores. All suites were validated by the three official validators.

category	tasks	before the fix	with the fix	official score
Floats	33	11	33	33.0 (22 UNKNOWN → FAILED, from ~830 s to 0–92 s)
regression guard (ProductLines, Loops, Sequentialized, Hardware, Arrays, Heap)	15	15	15	15.0
Intel-TDX (sample)	12	0	0	— (#75)

Report: docs/reports/2026-10-12-issue74-rerodada.md.

Juliet C and CASTLE: memory-safety and overflow bugs

Each Juliet test comes in a bad variant, which has the bug, and a good variant, which has it fixed. Finding the bug in a bad variant is a TP. Saying it is safe is an FN. Reporting a bug in a good variant is an FP.

	v15	9.0
bad variants: bug found (TP)	1,154	1,808	+654
bad variants: claimed safe (FN)	1,145	1,084	−61
bad variants: no answer (UNKNOWN / TIMEOUT)	1,351	1,138
bad variants: tool crash (ERROR)	380	0
good variants: confirmed safe (TN)	3,290	3,262	−28, moved to UNKNOWN / TIMEOUT
good variants: false alarm (FP)	120	120	=
good variants: tool crash (ERROR)	0	4	KLEE core dumps

CASTLE is unchanged: TP 54, TN 44, FN 14, FP 1 on the 119 cases in scope.

Caveats

• The corpora are the v15 sample, not the Test-Comp 2026 task set. The official set has 1,895 Cover-Error and 14,322 Cover-Branches tasks, including Hardware and Intel-TDX subcategories the sample lacks, and it normalises scores per subcategory. These numbers compare 9.0 with v15. They do not predict a competition score (docs/backlog.md).
• Per-task data and every round are in docs/reports/tacas-experiment-log.md.

Development rounds (samples)

All rounds use the Test-Comp samples r15-ce.tsv (Cover-Error, 213 tasks) and r15-cb.tsv (Cover-Branches, 120 tasks), which are nested inside the v15 campaign, with 300 s per task. The per-round data is in docs/reports/tacas-experiment-log.md.

v15 baseline (full campaign, before this line)

Cover-Error, 1,087 tasks	control 470 covered, slice 412
Cover-Branches	53.0%
Juliet	TP 1154, FP 120
CASTLE	TP 54, FN 14, FP 1

Cover-Error, 213-task sample

round	build / arm	covered	wrong TRUE	median time
R15	v15 control	111	27	43 s
R15	develop after #68–#71	129	5	5 s
R16	+ smart seeds, before the verdict fixes	148	7	6 s
R19	control, with all verdict fixes	128	0	3 s
R19	--seed-exchange	151 (+23 −0 vs control)	0	5 s
R19	--alternate-engines, before its fix	148 (+20 −0)	0	9 s
R19	--slice and its 4 variants	127–128 (±3)	0	4–5 s
R24	control + KLEE vector replay	146 (+20 −2 vs R19 control)	0	4 s
R20	seeds + 3c ranking	150 (+2 −3 vs R19 seeds)	0	4 s
R23	seeds, intermediate build	154	0	4 s
R24	seeds + KLEE vector replay	155	0	5 s
R26	--seed-exchange, this branch	157 (+29 −0 vs R19 control)	0	3 s
R26	--alternate-engines (the new default), this branch	157 (+30 −1)	0	9 s

• v15 → this branch, same 213 tasks: 111 → 157 covered (+41%), wrong TRUE 27 → 0.
• Wrong TRUE is 0 in every arm since R19, confirmed at scale.
• Seed exchange gives +23 −0 over the fixed control. The KLEE-vector replay gives most of that gain to the plain hybrid as well: 146 against 151.

Cover-Branches, 120-task sample

round	arm	mean coverage
R15	v15 / develop	48.0% / 47.7%
R16	seeds	49.7% (26 better, 9 worse)
R19	control / seeds / alternate	44.7% / 46.1% / 50.3% (alternate: 43 better, 5 worse)
R22	control + fuzzer corpus in the suite	49.7% vs 44.7% (40 better, 3 worse)
R26 (partial, 107)	alternate + fuzzer corpus (the new default), this branch	52.9% vs 46.0% (40 better, 7 worse)
R26 (partial, 97)	seeds + fuzzer corpus, this branch	49.0% vs 44.5% (30 better, 11 worse)

R19 ran under heavier machine load than R15: 11 containers at once, and memory ran out at the end. That is why the R19 control scored lower on the same sample.

--add-invariants and SSA (R25, 71 Cover-Error + 50 MemSafety tasks)

arm	Cover-Error covered	ERROR	MemSafety correct / wrong-true / wrong-false
off	51	0	28 / 2 / 2
MAP2CHECK_PREOPT=ssa	50	0	—
Clam, no invariants	50	2	25 / 1 / 4
Clam, default profile	49	4	27 / 1 / 4
Clam, memory profile	44	7	25 / 2 / 4

• No gain in the hybrid, and more wrong FALSE on MemSafety.
• The ERRORs came from Clam running unbounded; it is now bounded at 0.2T and falls back to the plain compile.
• The option stays optional. A dedicated study is in the backlog.
• The history of the old engine is in the "--add-invariants" section above.

SV-COMP (R17 and R21, 120 s per task)

	control	seeds	alternate
MemSafety (50): correct	29	30	29
MemSafety: wrong TRUE	2	1	1
MemCleanup (10): correct	6	6	6
NoOverflows (20): correct / unknown	2 / 17	2 / 17	2 / 17

• The 6 MemSafety error results in R17 came from the harness classifier, not from Map2Check (fixed).
• The %s check (R21) fixes one wrong TRUE and introduces one wrong FALSE. On CASTLE it raised FP from 1 to 4 (a scanf buffer, argv[0]). It is off by default.
• CASTLE (R21, %s check on): TP 54, TN 44, FN 12, FP 4. Baseline R14: TP 53, FN 14, FP 1.

Tests

• Unit tests: 12/12 (ctest). New: AlternationTest, plus new cases in KtestReaderTest, SlicerTest, SeedStoreTest and TestSuiteTest.
• Integration (tests/integration/test_testcomp_regressions.sh): 50/50 with the new defaults; section 11 now checks the 8.x behaviour through --fixed-hybrid. Also 50/50 with MAP2CHECK_PREOPT=ssa. New sections 29–37 cover the abort rewrite, dropped paths, the slice cache, the AFL++ nondet loop, alternation, intrinsics, %s, the fuzzer suite and the link error.
• Verdict classifier: 21/21 (tests/integration/test_verdict_classifier.sh).

Documentation

• README: a new section on the engines, the options and the verdict semantics, plus a table of the environment knobs with what each was measured to do.
• CLAUDE.md: the hybrid, and the state kept beside the scratch directory.
• docs/backlog.md:
  • the --add-invariants study;
  • the KLEE memory limit for parallel rounds;
  • the pitfalls of the campaign harness.
• Addendum to docs/reports/2026-08-16-crabllvm-review.md.
• docs/reports/tacas-experiment-log.md: every round, R1–R26, plus the official-environment rounds and NonDetPass: tipos __VERIFIER_nondet_* não modelados zeram tarefas (Intel-TDX, Floats) para UNKNOWN #74.
• docs/reports/2026-10-06-ambiente-testcomp-oficial.md and docs/reports/2026-10-12-issue74-rerodada.md.

🤖 Generated with Claude Code

[Copilot]

🟡 Changes recommended

Unresolved instrumentation and output-consumer defects can break analysis or replay, with additional correctness issues in packaging and crash classification.

6 open issues

• Handle new nondet CSV type IDs across parsing and witness generation · New
• Avoid renaming assumptions to an occupied runtime function name · New
• Recover violating .ktest data when klee_log.csv is absent · New
• Do not advance printf argument index for %m conversion · New
• Detect outer crashes before suppressing replay crash messages · New
• Resolve relative output paths before staging and archiving · New

What changed in this PR

This PR prepares Map2Check 9.0, combining AFL++/KLEE engine coordination, safer verdict handling, expanded nondeterministic input support, and competition validation infrastructure.

Changes:

• Adds persistent seed exchange, engine alternation, slice caching, and cross-phase test-suite management.
• Expands nondet and memory instrumentation while reducing KLEE logging overhead.
• Adds Test-Comp packaging, evaluation support, regression tests, and release documentation.

File	Description
utils/​testcomp-archive/​make-archive.sh	Packages Map2Check and its engine dependencies.
utils/​moduleBenchExec/​map2check_testcomp.py	Uses CPU limits when no wall-time budget exists.
utils/​moduleBenchExec/​__init__.py	Adds the BenchExec module package marker.
utils/​map2check-testcomp-wrapper.py	Configures bundled AFL++ tools.
tests/​unit/​frontend/​TestSuiteTest.cpp	Tests cross-phase suite persistence and eviction.
tests/​unit/​frontend/​SlicerTest.cpp	Tests nondet criteria and slice-cache helpers.
tests/​unit/​frontend/​SeedStoreTest.cpp	Tests seed filtering and coverage ranking.
tests/​unit/​frontend/​CMakeLists.txt	Registers seed-store and alternation tests.
tests/​unit/​frontend/​AlternationTest.cpp	Tests engine windows and stagnation tracking.
tests/​unit/​backend-library/​NonDetLogTest.cpp	Checks nondet CSV formatting.
tests/​unit/​backend-library/​CMakeLists.txt	Registers nondet-log tests.
tests/​testcomp/​run_testcomp_evaluation.sh	Preserves suites and isolates manifest descriptors.
tests/​testcomp/​official/​run.sh	Launches containerized generation and validation.
tests/​testcomp/​official/​init.sh	Initializes BenchExec cgroups.
tests/​testcomp/​official/​Dockerfile	Defines the competition validation image.
tests/​testcomp/​official/​bench-defs/​testcov-validate-test-suites-gcc-unformatted.xml	Defines unformatted GCC validation.
tests/​testcomp/​official/​bench-defs/​testcov-validate-test-suites-gcc-formatted.xml	Defines formatted GCC validation.
tests/​testcomp/​official/​bench-defs/​testcov-validate-test-suites-clang-unformatted.xml	Defines unformatted Clang validation.
tests/​testcomp/​official/​bench-defs/​testcoca-validate-test-suites-clang-formatted.xml	Defines formatted TestCoCa validation.
tests/​testcomp/​official/​bench-defs/​map2check.xml	Defines competition-style generation limits.
tests/​testcomp/​expected.txt	Updates the loop-input coverage expectation.
tests/​testcomp/​build_corpus_official.py	Builds proportionally stratified official corpora.
tests/​memsafety/​run_memsafety_evaluation.sh	Prevents child access to the manifest descriptor.
tests/​lib/​verdict_classifier.sh	Separates replay crashes from tool failures.
tests/​integration/​test_verdict_classifier.sh	Adds replay-crash classification coverage.
README.md	Documents engines, verdicts, and experimental options.
modules/​frontend/​utils/​slicer.hpp	Adds faster criteria scanning and cache helpers.
modules/​frontend/​utils/​seed_store.hpp	Defines persistent seed paths and ranking.
modules/​frontend/​utils/​gen_crypto_hash.cpp	Rejects unreadable input files early.
modules/​frontend/​utils/​alternation.hpp	Defines scheduling and stagnation helpers.
modules/​frontend/​test_suite/​test_suite.hpp	Extends cross-phase suite-management APIs.
modules/​frontend/​test_suite/​test_suite.cpp	Preserves cases and tracks pruned paths.
modules/​frontend/​test_suite/​ktest_reader.hpp	Extends decoding and exploration-status interfaces.
modules/​frontend/​CMakeLists.txt	Adds threading and optional SQLite support.
modules/​frontend/​caller.hpp	Declares caching, seed exchange, and engine controls.
modules/​backend/​pass/​NonDetPass.hpp	Declares additional nondet instrumentation types.
modules/​backend/​pass/​NonDetPass.cpp	Rewrites abort calls and instruments new types.
modules/​backend/​pass/​NonDetFunctions.hpp	Declares typed logging functions.
modules/​backend/​pass/​MemoryTrackPass.hpp	Declares string-read instrumentation.
modules/​backend/​pass/​MemoryTrackPass.cpp	Recognizes memory intrinsics and optional string checks.
modules/​backend/​library/​lib/​WitnessGeneration.c	Enables nondet logs during seed replay.
modules/​backend/​library/​lib/​NonDetLog.c	Optimizes formatting and supports wider values.
modules/​backend/​library/​lib/​NonDetGeneratorNone.c	Adds constant implementations of new nondet types.
modules/​backend/​library/​lib/​NonDetGeneratorKlee.c	Adds types, bounded logging, and pruned-path markers.
modules/​backend/​library/​lib/​NonDetGeneratorAFL.c	Adds types and zero-fills exhausted inputs.
modules/​backend/​library/​lib/​ContainerRealloc.c	Grows log containers geometrically.
modules/​backend/​library/​lib/​AnalysisModeMemtrack.c	Checks string reads against tracked allocations.
modules/​backend/​library/​lib/​AnalysisModeMemcleanup.c	Adds the string-check stub.
modules/​backend/​library/​header/​NonDetLog.h	Declares new typed logging APIs.
modules/​backend/​library/​header/​NonDetGenerator.h	Declares new nondet generators.
modules/​backend/​library/​header/​Map2CheckTypes.h	Adds nondet tags and 64-bit value storage.
docs/​superpowers/​specs/​2026-09-29-tacas-3c-seed-ranking-design.md	Describes coverage-based seed ranking.
docs/​superpowers/​specs/​2026-09-29-tacas-3b-engine-alternation-design.md	Describes engine scheduling and safeguards.
docs/​superpowers/​specs/​2026-09-29-tacas-2d-slicing-optimizations-design.md	Describes slice caching and experiments.
docs/​superpowers/​specs/​2026-09-28-tacasv3a-smart-seeds-plumbing-design.md	Describes bidirectional seed exchange.
docs/​reports/​2026-10-12-issue74-rerodada.md	Reports nondet-type fixes and validation results.
docs/​reports/​2026-10-11-handoff-v99-campanha.md	Records official campaign status and follow-ups.
docs/​reports/​2026-10-06-ambiente-testcomp-oficial.md	Documents the official validation environment.
docs/​reports/​2026-09-30-plano-campanha-completa.md	Defines full-campaign evaluation criteria.
docs/​reports/​2026-08-16-crabllvm-review.md	Adds historical invariant-engine findings.
docs/​backlog.md	Tracks deferred studies and known limitations.
Dockerfile.dev	Clarifies Clam domain choices in comments only.
CMakeLists.txt	Sets the project version to 9.0.0.
CLAUDE.md	Documents hybrid state and invariant-study status.
CHANGELOG.md	Summarizes 9.0 behavior changes and fixes.

_{Review effort: Balanced}

[GuilhermeBn198]

Confirmed and fixed in 7db6dd5. It was wider than the new IDs: the parser knew 0–5 only, so 6–15 already left row.type uninitialized, and generateWitnessFunctionName() fell off the end of a non-void function. KleeLogType now mirrors enum NONDET_TYPE (0–22, same order) plus UNKNOWN for any other number or a non-numeric column; the generator name is a full table that always returns ("" for UNKNOWN). New unit test KleeLogTest (all 23 types, plus 23, -1, abc).

[GuilhermeBn198]

Confirmed and fixed in 9c14229. Reproduced on the PR head: a function with abort() and __VERIFIER_assume produced map2check_assume.1, the native link failed (undefined reference to 'map2check_assume.1') and a reachable target answered UNKNOWN. adoptRuntimeName() now redirects the calls to the existing function when one of the same type already holds the runtime name, and renames otherwise; the nondet generators and the Crab assume use it too. The repro answers FAILED with input 42. Integration section 39.

[GuilhermeBn198]

Confirmed and fixed in c2bcc6c. Reproduced with 1100 nondet reads under --nondet-generator symex --generate-testcase: the PR head wrote long map2check_input_array[] = {}; (not even valid C). generateTestCase() now falls back to the violating .ktest (readViolatingKtest, as emitTestSuite does) when the log is empty, and writes {0} if nothing at all is recovered; the same repro writes all 1100 values. The costly symbolic CSV formatting stays off.

[GuilhermeBn198]

Confirmed and fixed in 223194e. With MAP2CHECK_CHECK_CSTRINGS=1, printf("%m %s %p", buf, (void *)&byte) on a safe program was a FALSE-DEREF on the PR head (it checked &byte as the string). %m now advances no argument; * width/precision are still counted. The safe program of integration section 36 now includes that call and stays TRUE.

[GuilhermeBn198]

Confirmed and fixed in b25e6af. The outer exit status 139 (SIGSEGV) or 134 (SIGABRT) is now ERROR before the replay filter; definitive verdicts keep precedence. Three new cases in test_verdict_classifier.sh: tool SIGSEGV and SIGABRT after "Exited fuzzer with 0" are ERROR (both fail on the previous classifier), and the same log with exit 0 stays UNKNOWN.

[GuilhermeBn198]

Confirmed and fixed in deea32a. Both arguments are resolved to absolute paths before anything else, and a missing output directory is an error up front (exit 2). Checked: a relative rel.zip is now written in the caller's directory, and /nonexistent/x.zip stops with "no such directory" without touching anything.

[hbgit]

Revise tambem os comentarios do Github Pilot

[hbgit]

Confirmar se ao final da verificação o DB é deletado

[GuilhermeBn198]

Confirmado: sim. O banco SQLite é o run.stats que o KLEE grava no próprio diretório de saída (klee-out-N), dentro do diretório de trabalho <hash>.map2check; o Map2Check só o lê, durante a alternância, para detectar estagnação. No fim, Caller::cleanGarbage() apaga o diretório de trabalho inteiro (com o klee-out-N e o run.stats dentro), e o SeedStoreCleanup do main() apaga as pastas que ficam ao lado dele entre as fases (<hash>.seeds, <hash>.slice, <hash>.build) em qualquer saída, inclusive exceção. Só o --debug mantém tudo, de propósito.

Verifiquei em duas execuções do modo padrão (alternância AFL++/KLEE, sem --debug): ao final só sobram o programa, o log e test-suite/, e não há nenhum run.stats em todo o sistema de arquivos. A exceção é uma execução morta por fora (por exemplo, pelo timeout do BenchExec), em que a limpeza não chega a rodar; na competição isso não pesa, porque o contêiner da execução é descartado.

[hbgit]

0 klee suporta este tipo ?

[GuilhermeBn198]

Sim, para unsigned long long o KLEE tem suporte completo: o valor vira um objeto simbólico de 8 bytes (non_det_ulonglong), e o solver trabalha com vetores de bits de 64 bits. Testei com o KLEE sozinho (--nondet-generator symex) num programa que só alcança o erro com x == 18446744073709551000ULL: ele encontra o valor exato.

O tipo vizinho, float (linha 84), é o caso delicado: o KLEE 3.1 não raciocina sobre ponto flutuante simbólico (silently concretizing (reason: floating point) ... to value 0). Por isso, nas tarefas de Floats, quem acha os erros é o AFL++ dentro do híbrido; o KLEE só reaproveita os valores concretos. A linha 84 continua necessária para decodificar os .ktest e as sementes.

[hbgit]

sugiro documentar este formato

[GuilhermeBn198]

Feito em fb2423b: docs/test-suite-format.md documenta o formato das suítes como o Map2Check as escreve — arquivos, metadata.xml, ordem e codificação das entradas, o marcador <!-- map2check: assumption-pruned path --> (o que significa, por que os validadores o ignoram, e como a remoção de casos podados funciona quando a suíte enche), o limite de 50 casos e as duas fontes dos vetores (klee_log.csv, com a tabela de tipos, e o .ktest). O comentário do código e o cabeçalho de test_suite.hpp (que ainda dizia que Cover-Branches era trabalho futuro) apontam para lá.

[hbgit]

como este foi criado ?

[GuilhermeBn198]

Gerado pelo tests/testcomp/build_corpus_official.py --property cover-branches --total 3500 (commit 0149e22): ele lê as categorias, com seus includesfile/excludesfile, da definição oficial da Test-Comp 2026, e sorteia de forma determinística e proporcional ao tamanho de cada categoria (ordem de bissecção aninhada, linhas intercaladas entre categorias).

Em fb2423b documentei a origem de todos os manifestos em tests/testcomp/corpus/README.md, com o comando e o commit de cada um. Conferi hoje: os oito regeneram idênticos, byte a byte, a partir do sv-benchmarks 7efe28dd2 (o commit fixado pela Test-Comp 2026).

[GuilhermeBn198]

Todas as 10 observações da revisão foram tratadas em 7 commits (7db6dd5..fb2423b); cada comentário tem a resposta com o commit e a evidência.

Verificação do head atualizado (fb2423b68), contra a 9.0 anterior (install_v99c, 3 repetições da rodada controlada):

• testes unitários: 14/14 (inclui o novo KleeLogTest);
• regressão de integração da Test-Comp: 52/52 (inclui a nova seção 39, abort() + __VERIFIER_assume);
• classificador de vereditos: 24/24 (3 casos novos);
• 30 sondas de Cover-Error, confirmadas pelos validadores oficiais (TestCov 3.11 gcc e clang + TestCoCa): 28, contra 26/27/28 da 9.0 anterior; tempo nas 25 tarefas comuns: 457 s × 496 s;
• 20 sondas de Cover-Branches, cobertura oficial: 68,1 %, contra 70,3–71,1 %. A diferença vem de relax-2-2, e não é regressão (verificado depois deste comentário, edição de 23/out):
  • o código instrumentado da tarefa é idêntico byte a byte nos dois builds (módulo dos passes, módulo linkado e binário de testemunha), e as mudanças do frontend não estão no caminho de geração das suítes;
  • repetida nas mesmas condições, a tarefa oscila nos dois builds: 9.0 anterior em 12 execuções, mediana 83,3 % (com quedas a 41,7 / 41,7 / 66,7 %); este head em 10 execuções, mediana 83,3 % (quedas a 38,9 / 63,9 / 75,0 %). Médias de 75,0 % e 76,7 %.

Três defeitos foram reproduzidos na 9.0 anterior e corrigidos aqui: falha de link com abort() + __VERIFIER_assume (UNKNOWN num alvo alcançável), caso de teste C vazio acima de 1024 leituras e FALSE-DEREF falso com %m.

🤖 Generated with Claude Code