fold lives only on git.trevon.dev, but every SARIF report advertised
https://github.com/trvon/fold as the tool's information URI, so code
scanning UIs and SARIF viewers linked readers to a repository fold no
longer uses. The driver now points at https://git.trevon.dev/trevon/fold.
test_scan_e2e asserts the URI; it failed before this change.
Problem: normalizeClangTuPath, normalizeQuarantinePath and fan-out's
normalizePath were three copies of the same absolute + weakly_canonical
routine. Coverage, worker records and the quarantine file must agree on a
TU's spelling, and three copies can drift apart.
Fix: move the routine to fold/cli/tu_path.hpp as normalizeTuPath and use it
at every site. No behaviour change.
Test: existing test_scan_coverage (path spellings), test_tu_quarantine and
test_subprocess_fanout, updated to the new name. Full suite: 140/140.
Problem: null-deref, div-by-zero and int-overflow re-check a portfolio
verdict on the reporting solver and reconcile the two, but then memoized the
re-check's unsat core (and read its model) from the raw re-check result. A
portfolio SAT that the re-check called UNSAT became unknown, yet its core was
still reused as the assumptions for later queries on the same path. The
disagreement itself was silent: no stat, and the trace showed the portfolio's
verdict.
Fix: all six sites use symbolic::recheckPortfolioVerdict and act only on the
reconciled verdict, so an unknown leaves no core or model behind. The helper
counts SolverStats::portfolio_disagreements (merged, printed, and exported in
the detector profile), and the sites trace
"UNKNOWN (portfolio re-check disagreed)".
Test: test_model_validation "[portfolio]" checks the helper's agreement,
unknown and disagreement cases and the merged counter. Full suite: 140/140.
Problem: a TU skipped because a prior run quarantined it was not analysed,
but coverage did not say so. The serial path dropped it from the attempted
set, so a scan whose only TU was quarantined was complete and exited 0; the
fan-out path saw no file_finished record and called it frontend-failed.
Fix: the shard runner counts every requested TU and records skipped ones
with gap reason `quarantined`; a worker emits a file_finished record with
that reason so the parent classifies it the same way. USAGE lists the reason.
Test: test_subprocess_fanout "[quarantine]" covers serial (was 2 attempted,
no gap) and fan-out (was frontend-failed). CLI probe: serial and fan-out
both exit 2 with a `quarantined` gap.
Problem: isCLibraryFunction accepted any global-scope non-member function,
so a project's `void free(Obj*)` overload was modeled as libc free: calling
it twice was a double free, and reading after it a use-after-free.
Fix: a global function counts only when it is extern "C", in namespace std,
or declared in a system header. extern "C" also covers C translation units,
where external functions have C language linkage.
Test: test_library_callee_identity "[global]" (DoubleFree and UseAfterFree
now 0; were 1 each); test_encoder_callee_names flips the global C++ helper
to not-a-library-callee. Full suite: 140/140.
Problem: with --portfolio the OOB and UAF detectors took the portfolio's
SAT/UNSAT answer as final. The portfolio solves on its own contexts, so the
reporting solver was never checked: OOB read its counterexample from an
unchecked solver (i=0 under `i > 5`), and a SAT the reporting solver would
not reproduce was still emitted. Other detectors already fail closed through
reconcilePortfolioRecheck.
Fix: add symbolic::recheckPortfolioVerdict, which re-checks a decided verdict
on the reporting solver and reconciles the two (disagreement or timeout ->
unknown), and apply it at the four OOB and two UAF portfolio sites. The
now-redundant UNSAT-only artifact re-checks in OOB checkHazard are removed.
Test: test_proved_requires_exact_model "[portfolio]" requires the portfolio
counterexample to satisfy the path (was i=0, now i=6).
Problem: OOBObserver::emit marked every constant-index array OOB as Proved,
even when the path reaching the access was over-approximated (an opaque call
or a truncated loop). The heap and UAF paths already gated on exactEncoding.
Fix: pass exactEncoding(env) into emit and require it alongside a numeral
index before assigning Proved; otherwise the finding is Heuristic.
Test: test_proved_requires_exact_model "[oob]" adds an exact control (stays
Proved) and an opaque-call path (now Heuristic; was Proved).
Two gaps in the loop-exit soundness rule from 6adcc24, both found in
review and reproduced as Proved always-conditions:
- `continue` was not an escape. The walkers drop an arm that ends in
`continue` (it always leaves the iteration), so iterations that took it
were never modeled, yet the unroll still counted as exact and the
loop's variables were not havocked:
for (i = 0; i < 2; i++) { if (y) continue; x++; } if (x == 2)
was "always true" although y != 0 gives x == 0. containsLoopEscape now
treats a continue that targets the loop as an escape (a switch
captures break but not continue; a nested loop captures both).
- Havocking a truncated loop reset scalar variables only. Array element
and member stores from the partial unroll survived:
for (i = 0; i < n && i < 4; i++) buf[i] = 1; if (buf[0] == 1)
was "always true" although n == 0 leaves buf[0] == 0. The unroll now
records the base variables of array/member stores and replaces their
arrays/values with fresh ones of the same sort; a store through a
pointer havocs every tracked heap array (SymbolicEnv::havocHeapArrays)
and marks the env over-approximated. The three walkers share this via
LoopUnrollExits::havoc.
Tests (test_loop_exit_soundness): continue, local-array and heap-pointer
stores are no longer Proved by dead-branch, always-condition or
unreachable; the exact constant-bound loop stays Proved (negative
control). A pointer-mutating call inside the loop (review #9) did not
reproduce for unreachable; its case is kept as a regression guard.
Problem: the README said setup enables "tracked ... OpenGrep pre-push
hooks", but only .githooks/pre-commit is tracked, so fresh clones get no
pre-push hook. docs/research/prior-art.md pointed to prior-art-full.md,
which has never been in the repository. test_mcp_stdio's TempDir
destructor called the throwing remove_all overload; a failure during
unwinding terminates the test binary and leaves .fold-mcp-test-*
directories behind.
Fix: the README names only the tracked pre-commit hook. The pre-push
hook is not committed: it runs `opengrep --config auto`, which needs the
network. The dead reference is removed. TempDir uses the error_code
remove_all overload. It stays under the working directory, because the
MCP server rejects paths outside its workspace root (moving it to
temp_directory_path broke three MCP tests).
Test: mcp_stdio passes.
Problem: symbols are 64-bit bitvectors whose low bits carry the source
value, but int-overflow witnesses printed the whole bitvector. For a
32-bit `int a` the report showed a=2147483648 or a=-9223372034707292160,
which are not values of `a` and would make bad fuzz seeds
(tests/fixtures/clones/exact.cpp).
Fix: detect::sourceIntTypesOf() maps the function's integer parameters
and locals to their width and signedness (a name declared with two types
is left out). collectModelBindings() takes that map and prints each bound
symbol truncated to its source width with its signedness
(formatSourceIntValue). int-overflow passes the map for the current
function; other detectors are unchanged.
Test: test_int_overflow "[witness]": every binding for an `int` overflow
lies in int range, and formatSourceIntValue covers sign/width cases.
exact.cpp before: a=2147483648, a=3221225471. After: a=-2147483648,
a=-1073741825, the int values that actually overflow.
Problem: with --portfolio, null-deref, div-by-zero and int-overflow take
the verdict from a separate portfolio solver, then re-check on their own
solver only to obtain a model or unsat core. The re-check's result was
never compared: if it timed out (unknown) or disagreed, the portfolio's
SAT still produced a finding, with no model from the reporting solver.
Fix: symbolic::reconcilePortfolioRecheck() keeps the verdict only when
the re-check reproduces it and otherwise returns unknown. It is applied
at all six re-check sites.
Test: test_model_validation "portfolio verdicts stand only when the
re-check agrees" covers agreement, re-check unknown, and disagreement in
both directions. null_deref, int_overflow, div_by_zero and
source_structure pass.
Problem: SummaryStore keyed summaries by getQualifiedNameAsString (plus
"@file" for internal linkage), which overloads share. When a TU calls a
function whose body lives in another TU, the lookup returns whichever
overload was summarized last. Example: `take(int*, int)` dereferences p,
`take(int*, long)` checks it, and a call `take(q, 1L)` with a null q was
reported as a null-deref because it inherited the other overload's nonnull
precondition. Lookups also used a different spelling (no "@file") than
stores for static functions, so their summaries were never found at call
sites.
Fix: summaryStoreKey()/summaryStoreKeyForCall() return the declaration's
USR (semanticFunctionId: USR, TU-qualified for internal linkage). Every
clang-side store, lookup, dependency edge and staleness check uses it:
summary_encoder, null-deref, div-by-zero, OOB and the summary priming
pipeline, which still selects targets by the call graph's qualified names.
Rust summaries keep their own keys. Now that static callees' summaries
are found, null-deref's summary-precondition path applies the same
DEBUGASSERT and static-parameter-contract filters as its callee-deref
path.
Test: tests/unit/test_summary_key_identity.cpp covers per-overload
summaries, key identity across redeclarations and distinct keys across
namespaces, and the cross-TU overload call. That call reported a false
null-deref before the fix; a control call to the dereferencing overload
still reports one. Tests that hand-built the old keys
(test_symbolic_summary, test_cross_tu_security) now derive them from the
declaration. Full suite: 140/140 (rust_frontend's 500 ms timeout test
flaked once at load average 22 and passed on four reruns).
Problem: a TU the front end could not parse left no trace. ClangTool::run's
status was discarded, TUs with compile errors were analyzed on a partial
AST and counted as done, and the isolated-worker path dropped TUs that
never produced an AST. A scan of only broken files printed no findings and
exited 0, the same as a clean scan. Separately, the scan logger wrote to
stdout, so any warning corrupted a SARIF/JSON report written to stdout.
Fix: every TU now yields an outcome (clean, compile-errors,
analysis-failed); workers carry it on their file_finished record, and the
fan-out parent adds timeout/crash/worker-exit for the TU a worker died on.
tuCoverage() turns the requested file list plus outcomes into a
ScanCoverage (requested TUs with no outcome are frontend-failed). SARIF
gets a run `invocations` entry (executionSuccessful, one
toolExecutionNotification per gap); findings JSON gets an additive
`coverage` object. A scan with any gap, or with nothing analyzed, exits 2
after writing its report. CLI diagnostics now go to stderr, as
docs/internal/cli-philosophy.md principle 12 requires. USAGE.md and
AGENTS.md document the coverage fields and the exit code.
Test: tests/unit/test_scan_coverage.cpp (classification, path spelling,
complete/untracked controls, merge, both writers, and unchanged output
without coverage); test_cli_paths "[coverage]" covers a clean TU (exit 0,
complete) and a TU with a missing include (exit 2, gap in JSON, SARIF on
stdout parseable with executionSuccessful=false). Before: both probe files
exited 0 with no coverage information. Full suite: 139/139.
Problem: docs/research/soundness.md defines `proved` as an exact bounded
model establishing the property, but several detectors assigned Proved
without one: double-free from a heap-model flag, static-ptr-asymmetry from
a cross-function pattern, unused-function and dead-statement from AST
facts, the stdlib copy-overflow check, and the heap use-after-free / OOB
checks from SAT results whose encoding precision was never consulted. A
SAT result over an over-approximated path (an opaque call, an unsupported
node) can be spurious.
Fix: double-free and static-ptr-asymmetry report Heuristic; unused-function
and dead-statement report Syntactic; the stdlib copy check reports
Heuristic. Heap OOB and use-after-free keep Proved only when the path's
SymbolicEnv carries no imprecision tag. So that `malloc(sizeof(T))` paths
stay exact, sizeof/alignof on complete non-VLA types are now encoded as
exact constants (symbolic::typeTraitConstant) instead of an unsupported
node.
Test: tests/unit/test_proved_requires_exact_model.cpp covers each
downgraded detector, a heap UAF on an exact path (stays Proved, control)
and under an opaque call (Heuristic), and typeTraitConstant including the
VLA negative case. Full suite: 138/138.
malloc/free heap modeling (encoder), use-after-free's free/realloc, and
the taint source/sink tables selected a model by the callee's bare
identifier. A project function that merely shares a libc name was
modeled as libc:
namespace mine { void free(void*); }
mine::free(p); ... std::free(p); // double-free "proved", plus
// oob "double free" and a UAF
and `Pool::free(p)` behaved the same way, as did a member function
named `system` as a command-execution sink.
isCLibraryFunction / isCLibraryCallee (encoder_callee_names) accept a
direct callee that is not a class member and is declared at global
scope, in namespace std, or extern "C". The encoder's malloc-family and
free models, use-after-free's free/realloc, and every libc/POSIX taint
entry now require it. Entries that are deliberately method-name
heuristics (get, Query, execute, query, fromJson, readString*, the
request-parameter getters) are marked c_api = false and keep matching
by name as before.
Tests: test_library_callee_identity (namespaced and member `free` are
not double-free/UAF; member `system` is not a sink; libc free twice and
libc system(getenv()) still are), and isCLibraryCallee cases in
test_encoder_callee_names (::free, std::free, mine::free, Pool::free,
a global helper, an indirect call). Full suite 137/137.
The dead-branch, always-condition and unreachable walkers unroll loops
loop_unroll times, following only the path on which the guard holds.
When the guard could also be false (any symbolic bound), that early
exit was dropped, and the loop's assigned variables were havocked only
for loops containing calls. The state after the loop was therefore
"the loop ran exactly loop_unroll times", and conditions on it were
reported as Proved:
int s = 0; for (unsigned i = 0; i < n; ++i) s += 1;
if (s == 0) ... // "dead" proved/exact, "always false" proved
The same held for `s > 100`, while loops, and a `break` out of a
constant loop. On the audit probes this was 7 Proved findings, all
false.
LoopUnrollExits now records whether the unroll saw every way out of
the loop: no iteration could exit early (the guard's false branch was
infeasible), the unroll stopped because the guard became infeasible
rather than because loop_unroll ran out, and the body has no break or
goto that escapes. When any of that fails, the walker havocs the loop's
assigned variables and restores the entry path, as it already did for
opaque loops. A loop the unroll exits exactly (constant bound within
budget) keeps its precise state, so a genuinely dead branch after it
is still Proved.
Loop-bound provenance (--suppress-loop-bound-always-conditions) stays
off by default: it existed to downgrade proofs that leaned on the
unroll bound, and an inexact loop exit now havocs instead of producing
such a proof in the first place.
The duplicated helpers (containsCallExpr, collectAssignedVars,
appendAssignedVars, havocAssignedVars) move from dead_branch.cpp and
always_condition.cpp into detect/loop_havoc so all three walkers share
them; dead_branch.cpp drops under the 800-line soft cap.
Tests: test_loop_exit_soundness covers the symbolic-bound cases for all
three detectors (4 Proved each for dead and always-condition before),
the break escape, the exact-loop negative control, and the extracted
helpers (containsLoopEscape, LoopUnrollExits). Full suite 136/136.
fold:subprocess_fanout reads FOLD_TEST_FANOUT_FAILURE_WORKER, but the
worker target is build_by_default: false and the test declared
`depends: []`, so a plain `meson test -C build/release` ran the two
recovery cases against a binary that was never built and failed both
(`REQUIRE(std::filesystem::exists(helper))`). The test now depends on
the worker, and the suite is green from a fresh build.
Backlog #7. Repro showed chromium finding LOCATIONS (rule/uri/line/
col/id) were byte-identical across runs while the summary
finding_fingerprint drifted (064e60c9 -> 4573bb71): summarize_sarif_findings
hashed the full canonical finding record, which carries Z3-timing-
volatile fields (quality metrics, uncertainty reasons, confidence,
score). The stability gate already used identity-only keys, so the
fingerprint contradicted it on Z3-heavy corpora.
finding_identity_key now = {finding_id, rule_id, uri, line, backend}
(measurement artifacts excluded), and the fingerprint is the sha256
of the sorted identity keys — consistent with how change-time drift
and dispositions already define 'a finding'.
Verified: chromium fingerprint STABLE across identical runs
(f5629f0f). Repinned the four baselines to the identity-based
fingerprint (fold 6fe221a0, yams c9ad7d60, sage 3da6ecfa, chromium
f5629f0f).
Backlog #5 (operator-confirmed). chromium_source.json and
sage_rust.json were validated but unwired. This adds:
- reviewed dispositions (5 parallel review subagents): chromium 11
(10 FP/1 accepted-risk — deliberate modular arithmetic in
base/file_path.cc); sage 2714 (9 actionable uncontained path-join
reads in skill install/daemon library/model-downloader; 890 FP;
1815 accepted-risk quality bulk)
- wall/RSS baselines for both corpora
Measured both corpora produce finding drift run-to-run (chromium Z3
fingerprint drifts; sage +5 findings) and chromium's wall swings up
to ~2x under load — so they are wired as STRESS/DIVERSITY corpora:
a new additive evaluation.max_new_findings override lets a manifest
declare its finding-drift tolerance (CLI default unchanged for
fold/yams), allow_finding_drift is on, and chromium's wall/RSS
thresholds are relaxed. Final: both evals pass.
Also fixes a pre-existing /tmp-literal default (now platform tempdir)
in run_project_eval.py.
Round 4, iteration 2 of the fold optimization loop
(docs/research/optimization-loop-2026-07-30.md).
The yams wall-regression gate at 20% fired on a 113% concurrent-load
swing (8.1s -> 17.3s on identical code) and passed quiet at -11% —
with measured identical-code walls of 7.2-11.4s (quiet) and 17.3s
(loaded), a 20% threshold on a ~9s workload is noise-dominated and
flaky. A flaky gate is worthless as a regression oracle.
Calibrated to 50%: fires above 12.15s sustained (50% over the 8.10s
baseline) — catches true 2x regressions while tolerating the measured
40-113% machine swings. Validated: yams eval ok (7.37s vs 8.104s
baseline, -9%), gold precision/recall 1.0, full suite 137/137.
Fingerprints exactly preserved.
Round 3, iteration 2 of the fold optimization loop
(docs/research/optimization-loop-2026-07-30.md).
The foundation audit found both manifests declaring
wall_regression_pct/rss_regression_pct with no baseline artifacts —
the regression gates never engaged in the entire campaign.
New: tests/benchmarks/projects/baselines/{fold_source,yams_source}.json
(full prior-eval summaries with matching tu-set/config fingerprints
and exact finding fingerprints). Both manifests now reference their
baselines, activating the eval's baseline-compare path
(compare_performance_lanes + rss_regression).
Engage proof:
- fold: baseline_comparison engaged (paired-by-repetition, baseline
103.65s vs candidate 82.7s, -20.2%), status ok
- yams: gate FIRED on a 113% concurrent-load swing (proving it
discriminates), then passed quiet (7.181s vs 8.104s)
Also extends the schema-test prune to {runs, baselines} — third
instance of the same glob-sweep fragility the foundation audit
predicted. Full suite 137/137; fingerprints exactly preserved
(0fec78e5.../247523c5...); gold precision/recall 1.0 both.
Round 3, iteration 1 of the fold optimization loop
(docs/research/optimization-loop-2026-07-30.md).
The foundation audit found gold scoring machinery (26 oracle files in
bench/gold/, fold_eval/scoring.py, gold_threshold_failures gates)
fully implemented but wired into zero project manifests — the eval
measured finding drift, never precision/recall.
New gold standards anchored on the reviewed dispositions:
- bench/gold/fold_self_gold.json: 9 cases (5 SafetyObserver stub
clones, 1 detector-internal clone, 1 loop_inventory clone, 2
sql-injection sites reviewed false-positive-but-intentionally-
reported)
- bench/gold/yams_self_gold.json: 7 cases (3 clone, 4 high-complexity)
Both manifests now enforce gold_thresholds precision 1.0 / recall 1.0:
any detector drift that loses a reviewed finding (recall drop) or
emits a new unmatched finding (precision drop) fails the evaluation.
Proof runs: fold TP=9/FP=0/FN=0, yams TP=7/FP=0/FN=0, precision 1.0,
recall 1.0, fingerprints exactly preserved (0fec78e5.../247523c5...),
full suite 137/137. Gold files live in bench/gold/ alongside the
existing oracles (the tests/benchmarks schema-test glob correctly does
not sweep that directory).
Iteration 9 of the fold optimization loop
(docs/research/optimization-loop-2026-07-30.md).
Iteration 9 targeted the control-walk condition-fact cost (35.1s of
the sql-injection profile). Measurement-first: a scratch patch (never
committed) counted duplicate feasibility queries in a live scan —
1314 total, 1268 distinct (3.5% duplicate) — so a memo cache caps out
at ~1.2s of 35.1s, far below the >=20% KPI. The checks are genuine,
distinct SMT solving; memoization is a measured dead end. Scratch
patch fully reverted; production byte-identical.
Viable future directions recorded for the next campaign: fast-path
widening beyond affine parameter comparisons, incremental solving over
the pushed path stack, dual-walk (CFG/AST fallback) elimination.
This commit folds the formatting normalization applied to two
campaign-authored files after their initial commit.
Iteration 5 of the fold optimization loop
(docs/research/optimization-loop-2026-07-30.md).
The load-sensitivity flake in symbolic summary recomputation
(observed once: empty return_post in a 7/10-run burst under CPU
saturation) did not reproduce in three bounded rig attempts:
- 8 subshell busy-loops + 10 filtered runs: 10/10 PASS
- 8 verified 'yes' workers + 10 full runs: 10/10 PASS
- concurrent real fold sql-injection+uninit-read scan (-j 4)
+ 10 full runs: 10/10 PASS
No defect reproduced, so no fix ships; the rig is committed as the
standing recipe with the suspect documented (isValidPredicate's 100ms
Z3 solver timeout in summary_encoder.cpp — check() returning unknown
under CPU starvation flips predicate-record decisions). Production
code byte-identical.
Iteration 4 of the fold optimization loop
(docs/research/optimization-loop-2026-07-30.md).
BenchmarkSchemaTest claimed to validate checked-in manifests but
globbed tests/benchmarks/**/*.json, sweeping the designated runtime
output directory tests/benchmarks/runs/ (optimization-loop harness
artifacts) and failing 32 assertions + 5 errors on every full-suite
run once run artifacts existed.
Fix: prune runs/ from the glob; add tests/benchmarks/runs/ to
.gitignore so run artifacts are never accidentally committed.
fold:benchmark_evaluation green; full suite 137/137 with zero
failures. No production code change.
Iteration 3 of the fold optimization loop
(docs/research/optimization-loop-2026-07-30.md).
mergeTranslationUnitGraphContributions hard-failed with 'conflicting
semantic-USR function evidence' when the same function USR recurred
across TU contributions with spelling-variant qualified names (libc++
inline-namespace std:: vs std::__1) or an empty body hash (TU-dependent
template instantiation). ProjectCallGraph::addFunction — the exhaustive
fallback builder this merge must mirror — merges duplicates leniently,
so the incremental path could never succeed on real C++ codebases and
every scan silently paid the exhaustive fallback.
Measured (fold self-scan, 8 TUs):
- call-graph phase with --cache-dir: 24.1s median -> 1.7s (93% cut);
exhaustive-fallback warnings eliminated
- project eval wall median: 160.1s -> 92.6s (n=2, partly noise)
Finding fingerprints are exactly preserved (fold 0fec78e5..., yams
247523c5...; churn 0, pairwise Jaccard 1.0, both project evals ok).
Full suite 136/137 (sole failure: pre-existing benchmark_evaluation
fixture-schema issue, unrelated area). Red test added: 'contribution
merge tolerates same-USR spelling variants like the exhaustive
builder' (test_project_index.cpp).
Iteration 2 of the fold optimization loop
(docs/research/optimization-loop-2026-07-30.md).
The disposition baselines predated source edits; finding IDs encode
location, so line moves surfaced as new+resolved pairs and both
project evaluations gated red:
- fold: 8 new findings exceeded limit 0 (review coverage 0.111)
- yams: 3 new findings exceeded limit 0
Each finding was verified against source before re-baselining:
- fold: 5 SafetyObserver virtual-stub clones (line-moved, same
methods) accepted-risk; 2 detector-internal clone sites re-hashed,
accepted-risk; 2 sql-injection sites re-verified — all SQL text is
compile-time constants or fixed internal table lists (store.cpp:22,
:251) — false-positive
- yams: 3 clone IDs refreshed after line moves (document_metadata.h
600/623, connection_pool.cpp 42); 4 high-complexity locations
updated
Also fixes the disposition target fingerprint to the exact
runner-reproduced configuration fingerprint (manifest_configuration +
SOURCE_SETTING_FLAGS defaults), which the prior fold baseline had
stale.
Green proof (tests/benchmarks/runs/optimization-2026-07-31-dispositions/):
fold eval status failed -> ok, yams failed -> ok; finding fingerprints
unchanged (fold 0fec78e5..., yams 247523c5...); churn 0, pairwise
Jaccard 1.0, review_coverage 1.0. No gate weakened and no production
code change.
Iteration 1 of the fold optimization loop
(docs/research/optimization-loop-2026-07-30.md, workflow-driven
measure->select->implement->validate->checkpoint).
Baseline measured (tests/benchmarks/runs/optimization-2026-07-30/):
- fold self-scan median 251.7s, peak RSS 1390.5 MiB; sql-injection
detector 40.37% of analyze share (101.4s median) with 0 Z3 queries
- yams self-scan median 10.7s, peak RSS 489.9 MiB
Implement attempt: shared thread-local scratch Z3 context for
summarizeLeafFunctionSymbolically (stack samples showed Z3 ast_table
init from the ensureSymbolicSummary chain dominating walk time).
REJECTED by the new characterization test: Z3 hash-consing collapses
same-named parameters across functions and summary composition
silently degrades. Reverted; regression test retained plus rationale
comment at the reverted site.
Also documents: SummaryStore::lookupOrCompute returns pointers into
its internal map (invalidated by clear()); open finding on
load-sensitive summary recomputation under CPU saturation.
No production behavior change; fold:symbolic_summary 10/10 green,
focused suites green, git diff --check clean.
ARM NEON reductions (vaddvq_*/vminvq_*/vmaxvq_*) expand to GNU statement
expressions `({ ...; __ret = builtin(x); __ret; })`. The uninit-read walker
flat-traversed the statement expression, flagging the result read `__ret`
before noticing the assignment that writes it inside the same expression.
Track variables assigned within a StmtExpr (TraverseStmtExpr) so the result
read is not a false uninit-read.
Verified: simeon neon.cpp range_neon 2->0, statement-expression repro 1->0,
genuine uninit local still fires; full suite 137/137.
`(d & (d-1)) == 0 ? low & (d-1) : low % d` (simeon sketch_bucket) flagged
`low % d` as division-by-zero, but the guard `(0 & -1) == 0` is TRUE when
d==0, so the `%` arm is unreachable for a zero divisor. Teach
conditionProvesNonZero that `x & (x-1)` clears the lowest set bit (zero iff x
is 0 or a power of two):
* `(x & (x-1)) == 0` false arm -> x != 0
* `(x & (x-1)) != 0` true arm -> x != 0
Also route the same check through analyzeDivCallee so the callsite
precondition for the guarded divisor param is suppressed in the same TU.
Verified: simeon.cpp:48 `proved` finding gone; positive repro 1->0, bare
`a % d` still fires; 59 div-by-zero tests + full suite 137/137.
std::string/std::string_view size()/length() was cached only in the member
cache, which assign() clears. So `char* p = malloc(s.size()+1); ...; p[s.size()]`
encoded the two size() calls as DIFFERENT symbols, letting the solver find a
spurious out-of-bounds (yams object_storage_adapter.cpp dup_cstr, plugin_host_services_shim).
Route zero-arg const size()/length() through the assignment-surviving
string-length cache (string_lengths_), so both calls resolve to one length
symbol: the final write lands exactly at the end (in-bounds), while a genuine
size()+1 write still fires.
Adds positive/negative oob tests; full suite 137/137.
Given the engine can afford days of compute (fuzzing-grade), widen the
solver budgets so hard queries resolve instead of timing out:
- checkAdaptive escalation ceiling raised to 1 hour per query (was 8x base)
- budget_seconds 7200 -> 604800 (7 days)
- per_tu_timeout 900 -> 86400 (24h)
A single hard query getting up to an hour of escalating compute is cheap
relative to a lost vulnerability.
The 1800s solver budget, 6s per-query timeout, and 300s per-TU watchdog were
too tight for large security scans (e.g. 780-file yams), causing Z3 "unknown"
results and preempted TUs. Raise to 7200s budget, 30s per-query, and 900s
per-TU so slow-but-productive TUs finish and complex queries resolve.
The null-deref hardening and container-bounded callee guards pushed these two
helper files past the 1000-line ratchet; register them with the existing
tracked-monolith mechanism (matching int_overflow.cpp / oob_access.cpp) and
record the next extraction target.
std::basic_string / std::basic_string_view methods (substr/append/insert/...)
do size()-pos and pos+count arithmetic that is bounded by the container size
invariant, so an unbounded pos/length at a call site is a logic contract, not
signed-overflow UB. analyzeOverflowCallee now skips these, removing the
chromium file_path.cc substr/append FPs (6 signed findings -> 0) while
preserving the 10 genuine unsigned-wrap findings.
Adds positive tests (substr/append call sites are not flagged) and a clean
negative (free-function arithmetic is still flagged).
Unit + integration coverage for the session's work: incremental project
graph/index, pcode encoder, unreachable/dead-branch, equiv/cross-TU,
div-by-zero/sign-conversion/int-truncation, use-after-free, quality-precision,
scan-router profile, source TU runner, detector plan, and the eval fixtures.
- int-overflow: unsigned wrap is defined, not UB — split to
fold.unsigned-wrap so signed-UB findings aren't drowned; on by
default (--report-unsigned-wrap=false opts out)
- use-after-free: model return/throw as path-terminating so
`delete p; return;` in an error branch can't poison the fall-through
- oob-access: real sizeof for complete structs (was 1); recognize
std::min/clamp/modulo index bounds
- memory-leak: static-storage singletons + return-to-caller are
caller-owned, not leaks
YAMS scan: UAF 4→0, struct-OOB ~10→0, singleton-leak ~15→0,
min/modulo-bound OOB →0. 137/137 tests pass.
