Preserve CS memory relations and reduce SV-COMP state

[shaobo-he]

Summary

This completes the context-sensitive memory-region pipeline on top of cs and addresses the state explosion observed in SV-COMP device-driver benchmarks.

• preserve complete one-to-many region relations across calls and globals instead of selecting one representative
• keep per-function SeaDsa graphs and repair region mappings after merges
• map cross-function state to entry or shared maps while retaining threadable relations in procedure interfaces
• remove caller-only foreign nodes after SeaDsa context-sensitive top-down propagation, compressing first to satisfy remove_dead()'s graph invariant
• eliminate memory maps used only by dead static-initializer stores
• keep proven function-private stack/heap maps procedure-local for SV-COMP runs
• sequence call-site region lookup before insertion so a merge cannot invalidate the destination set
• conservatively use a shared map when a local procedure-interface region has no counterpart at a call site, such as a null pointer actual

The private-map policy is enabled only for -x svcomp with context-sensitive DSA. Global-backed, external, unknown, and cross-function regions remain module-level. Context-insensitive DSA and ordinary cs invocations retain the existing map policy.

Memory-safety properties, concurrency, and contracts are outside this PR's scope.

Performance

Exact SV-COMP translations with the default Corral configuration:

Benchmark	Before	After	Result
ldv-linux-3.0/model0001.i/it913x	13,787 global maps; 4.3 MB BPL	130 global + 25 local maps	verified in 5.34 s
ldv-linux-3.0/model0001.i/i2c	state expansion previously dominated	95 global + 3 local maps	verified in 2.45 s
floppy2	prior CS configuration timed out	reduced state	verified in 4.5 s

DD unknown investigation

The first full DD run exposed two additional SMACK-side defects:

• mapping[i].insert(idx(...)) had unspecified operand evaluation order. idx() may merge regions and rebuild the mapping, invalidating the set selected by mapping[i]. This caused segmentation faults and allocator-corruption failures. Sequencing the lookup fixes the issue; 12 affected DD cases now verify, and the remaining long-running repro reaches Corral instead of crashing during translation.
• ET1310_PhyAccessMiBit has an output region mapped at calls that pass stack pointers but no caller region at calls that pass null. A single threaded Boogie procedure signature cannot represent that relation. The affected equivalence class now falls back to one conservative shared map. The old build fails during translation; the corrected build verifies the benchmark and emits no map argument at those calls.

The partial run was later killed by host OOM while extra targeted checks were running alongside its 11 workers. A clean run from commit 97fd8034 has been restarted with the same stock-Corral configuration.

Validation

• SMACK supported regression configurations: 1,152/1,152 passed with 11 workers before the audit follow-up
• final region-mapping follow-up: c/basic --all-configs --threads 1, 528/528 passed
• exact SV-COMP et131x differential: old build fails with a missing call-site mapping; corrected build verifies
• representative heap-corruption repro (i2c-diolan-u2c) verifies in 2.2 s after the sequencing fix
• updated SeaDsa follow-up with Debug SMACK: c/basic 528/528 configurations passed
• assertion-enabled SeaDsa build verified to contain no -DNDEBUG, with sanity checks enabled
• SeaDsa unit tests: 8/8 passed
• SeaDsa lit tests: 49/49 active tests passed, with the two existing expected failures unchanged
• verified directly that the private-map option yields local maps under CS DSA and no local maps under CI DSA
• git diff --check, C/C++ formatting checks, and Python bytecode compilation passed

Dependency

The submodule update is proposed upstream in seahorn/sea-dsa#179 at 23cd94a. The exact commit is fetchable through the existing upstream submodule URL, so .gitmodules remains unchanged.

[shaobo-he]

Audit report (543c2cc..76d7ad5 + sea-dsa 78db357→23cd94a)

Multi-agent review across six dimensions (region relations, DSAWrapper translation, private-map policy, dead-map elimination, sea-dsa bump, plumbing/tests/docs) with adversarial verification: 35 independent verdicts, each backed by line-level evidence or a live reproduction on A/B builds (this branch vs. cs @ 0d6524a). Follow-up fixes are pushed as 0c561228..c663534a.

What holds up

• Design premise verified: svcomp/utils.py:92 runs Corral with /trackAllVars, which disables the tracked-variable abstraction — so procedure-local maps for private regions are a legitimate state reduction in SV-COMP mode, and the policy is correctly scoped away from default runs (where locals are strictly worse than untracked globals).
• Verdict consistency: A/B sweep over 8 SV-COMP driver benchmarks (floppy2/3, hid-waltop, it913x-v2, dp83640, mousedev, cpia2, sm_ftl) under the exact SV-COMP invocation: no verdict flips, with large map reductions (hid-waltop 249→50, cpia2 854→386, floppy3 623→251 module maps).
• Dead static-init map eliminator: fully clean under deep scrutiny — conservative by construction (whole-program occurrence counting can only over-approximate liveness; all statement forms of CodifyStaticInits enumerated; all post-elimination emitters guarded; pass scheduling safe). Verified empirically in both verdict directions with field-level elimination active.
• sea-dsa foreign-node cleanup: the safety claim in Clean up foreign nodes in CS top-down propagation seahorn/sea-dsa#179 checks out in code — NodeType::join ANDs the foreign bit, so nodes unified with native callee nodes survive removal.
• Soundness probes: static-init (scalar/array/struct), callee-write-through-escaped-pointer, recursion, function pointers (devirtualized pre-Regions), pthread, and five memory-safety probes all give correct two-sided verdicts; only the genuinely non-escaping region becomes a $M.L local.
• 97fd8034's idx() hoist fixes real UB (remapAfterMerge can rebuild the very call-site mapping being mutated mid-expression).

Fixed in 0c561228..c663534a

1. Crash regression (confirmed by 5 independent reproductions): __SMACK_INIT bodies using memory not rooted at a global (stack array, call result) hit report_fatal_error("cannot conservatively translate a global SeaDsa cell"); baseline verified the same inputs. Untranslatable non-global cells now anchor as ordinary regions; global-rooted translation failures keep the whole-node conservative fallback. Regression test init_func_locals.c.
2. Convergence cap regression (confirmed with reproduction): a valid 150-deep pointer-passing chain in caller-before-callee module order needs ~149 mapping passes; the fixed 100-pass cap aborted where baseline completed with the correct verdict. The bound now scales with the number of functions. Regression test deep_call_chain.c.
3. Plain-mode gap in 97fd803: the preliminary interface guard only ran under -local-private-memory-maps, but threading exists in every CS mode — the missing-mapping fatal remained reachable in default runs. The guard now applies whenever the analysis is context-sensitive.
4. Vacuous test: under -x svcomp, C assert maps to a bodiless __VERIFIER_assert, so svcomp_private_maps.c could never fail behaviorally (verified: a false assert still passes). Added --local-private-memory-maps to the CLI and switched the test to the regular frontend so its assertion is a real obligation.
5. Docs: cs-dsa-memory-plan.md said entry regions keep module-level declarations and omitted both new features; now aligned with the implementation.

Refuted during verification

• Quadratic translateGlobalCell cost: not reproduced — a 4,000-global statically-initialized chain (4,017 field maps) translates in identical time on this branch and baseline (0.71 s vs 0.71 s). The per-value mapper is not measurably worse than the old cached whole-graph mapper.
• --no-memory-splitting as a sea-dsa escape hatch: never existed — CodifyStaticInits has required DSAWrapper unconditionally since 3e27650. (The new head does run sea-dsa twice under that flag; harmless duplicate work.)

Notes on the PR description

• "1,152/1,152 regression configurations" corresponds to --all-configs, which excludes the 257 skip-with-reason tests; CI's --exhaustive matrix on this checkout is 457 tests / 2,377 configurations (which CI runs and passes).
• Attribution caveat: toggling the foreign-node cleanup off (-sea-dsa-no-td-copying-opt) produced byte-identical map declarations on all probe-scale inputs — at that scale the map reduction comes from the SMACK-side changes. The sea-dsa cleanup may only matter at driver scale (the it913x input wasn't available locally to check).
• -local-private-memory-maps fires for all -x svcomp properties, including memory-safety/memcleanup, which the text scopes out. Empirically fine (the $alloc bookkeeping is orthogonal; five memsafety probes pass), but gate and prose should agree.

Pre-existing cs-branch issues surfaced (not caused here — suggest separate issues)

• va_arg writeback is unsound (confirmed both modes, both builds): memory reached only through va_arg gets no call-site mapping, so callee writes land in a map disjoint from the caller's — demonstrated FALSE VERIFIED on a reachable-error probe. 97fd8034's forced sharing does not couple the two sides.
• llvm.global_ctors is never lowered: __attribute__((constructor)) functions are emitted but never called; wrong verdicts in both directions demonstrated.
• Threaded-class attribute merging: under --integer-encoding=bit-vector, a threaded class mixing bytewise and type-safe members produces ill-typed Boogie (shared classes merge attributes; threaded classes don't).
• mousedev still crashes llvm2bpl identically on both builds (upstream sea-dsa Cloner null-deref on zero-index-GEP-of-inttoptr) — the fix exists locally from the PR 810 work and could ride along in Clean up foreign nodes in CS top-down propagation seahorn/sea-dsa#179.

[shaobo-he]

Optimization suggestions from the audit — none blocking. Prioritization context: in the round-1 A/B sweep, floppy2/dp83640/cpia2 still time out at 600 s under the real SV-COMP Corral configuration on both builds, so at driver scale the bottleneck is tracked-state size under /trackAllVars, not translation time. The two suggestions that shrink the tracked-global set (write-only-region elimination, one-function shared classes) are therefore the ones most likely to move SV-COMP results; the call-graph-ordering one is the clean translation-time win.

[shaobo-he]

Suggestion (translation time): process call sites in bottom-up call-graph order instead of module order. Information currently propagates one call-graph level per pass — that is why a 150-deep chain needs ~149 passes and this bound has to scale with module size. Walking call sites callee-first (llvm::scc_iterator over CallGraph, the same order sea-dsa's BU pass uses) converges in one or two passes regardless of depth, cuts Phase-3 time by the chain-depth factor on driver benchmarks, and turns maxIters back into a true divergence detector.

[shaobo-he]

Suggestion (SV-COMP state): generalize dead-map elimination from static-init stores to write-only region classes, computed semantically. After the Phase-4 closure, any class absent from every function's readRegions is write-only memory (status registers, log buffers — common in the ldv drivers): its map declaration and stores can be dropped for reach-safety properties (must stay off for memory safety). Under /trackAllVars every eliminated map is a tracked global removed, so this compounds directly with this PR's headline mechanism — and it would subsume this textual eliminator, retiring the whole-program string scan and its implicit naming invariants.

[shaobo-he]

Suggestion (SV-COMP state): classNeedsShared classes whose members all belong to one non-entry function (and hold no global) currently bind to a module-level $M.S map, but the representational requirement is only one backing map — it could be a single procedure-local map under -local-private-memory-maps. Merging the members into one $M.L index removes another tracked global per such class; the relation-preservation argument is identical to the shared-map case.

[shaobo-he]

Suggestion (robustness at scale): memoize the mapper per (global, src graph, dst graph). A 4,000-global probe showed the fresh-mapper cost is invisible at that scale, so this is insurance rather than a measured win — but static initializers of large arrays re-seed the same global's mapper once per field store, and driver-scale graphs are both bigger and probed more often. A small cache keyed on the underlying global keeps the exact-identity semantics that motivated dropping the old all-globals mapper.

[shaobo-he]

Suggestion (encoding): the !isStaticInitd exclusion may be liftable now. The comment it came with predates SmackRep::store's direct-assignment handling for singleton regions; if __SMACK_static_init stores route through the same emission, statically initialized scalar globals (drivers have many) become plain Boogie variables instead of maps — the cheapest possible encoding under /trackAllVars. One experiment decides it: lift the guard, confirm static init emits $M.k := v rather than $store, and run two-sided static-init probes.

[shaobo-he]

Note (minor): this preliminary pass runs the whole-module access closure twice per CS run. The second run starts from saturated sets so it converges quickly, but if profiling ever shows it, snapshotting the access sets here and propagating only the unification-induced delta in Phase 4 is straightforward.