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).
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.
