From 543c2cc26e236677c9a0ebc38ff5a5eab4d7cb1c Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Sun, 12 Jul 2026 22:25:05 -0700 Subject: [PATCH 01/12] Preserve context-sensitive region relations --- docs/cs-dsa-memory-plan.md | 209 ++++++++++----------- include/smack/DSAWrapper.h | 16 +- include/smack/Regions.h | 35 ++-- lib/smack/DSAWrapper.cpp | 74 ++++---- lib/smack/Regions.cpp | 359 +++++++++++++++++++------------------ lib/smack/SmackRep.cpp | 29 +-- 6 files changed, 382 insertions(+), 340 deletions(-) diff --git a/docs/cs-dsa-memory-plan.md b/docs/cs-dsa-memory-plan.md index 53a7f26d5..5f3a8da51 100644 --- a/docs/cs-dsa-memory-plan.md +++ b/docs/cs-dsa-memory-plan.md @@ -2,125 +2,134 @@ ## Overview -SMACK uses **context-sensitive** sea-dsa analysis (`-sea-dsa=cs`) with **per-function memory regions**. Each function gets its own region vector computed from its CS graph, and memory maps are threaded through procedure signatures as parameters (reads) and returns (writes). - -```boogie -// Memory maps are local in/out parameters, not globals -procedure foo(x: ref, $M.0.in: [ref]i8) returns ($M.0.out: [ref]i8) -{ var $M.0: [ref]i8; - $M.0 := $M.0.in; - $M.0 := $store.i8($M.0, x, 42); - $M.0.out := $M.0; } - -procedure main() - modifies $M.0; -{ call $M.0 := foo(x, $M.0); } +SMACK runs SeaDsa in context-sensitive mode (`-sea-dsa=cs`) and constructs a +region vector for each LLVM function. Region indices are local to a function; +they are never compared across functions without a SeaDsa mapping. + +The existing `cs` branch uses a hybrid backing policy. Entry-function regions +and larger cross-function classes use module-level maps, while selected small +classes are threaded through procedure inputs and outputs. The soundness fixes +below preserve that policy and its map declarations. + +## Soundness Invariants + +1. A region mapping is a relation, not necessarily a function. One callee + region can correspond to several caller regions after DSA or region merges. +2. Every association in that relation is preserved. Selecting one target can + disconnect caller state and is an unsound under-approximation. +3. A relation with several targets cannot be represented by one threaded map + argument. Its complete equivalence class must use shared backing storage. +4. Region construction and call-site mapping must converge before translation + continues. Hitting the iteration limit is a translation error. +5. A nonfunctional SeaDsa `SimulationMapper` is a translation error until its + complete relation can be consumed through a SeaDsa API. +6. Cross-graph global translation is either exact and offset-preserving or + conservative. It never silently falls back to an unrelated cell or offset + zero. + +## Analysis Phases + +### 1. Per-Function Regions + +Loads, stores, atomics, and memory intrinsics create field-granular regions in +the DSA graph of the function containing the access. Regions are not pre-seeded +from whole formals, actuals, or globals because whole-object probes collapse +otherwise disjoint fields. + +`__SMACK_static_init` and `__SMACK_init_func*` are emitted in the entry +function's memory context. Their cells are translated through the identity of +the exact underlying global. If exact field translation is unavailable, SMACK +uses a whole-node bytewise region in the entry graph. + +### 2. Direct Access Sets + +Each function records directly read and modified regions: + +- load: read +- store: modified +- atomic read-modify-write: read and modified +- `memset`: modified +- `memcpy`/`memmove`: source read and destination modified + +### 3. Call-Site Relations + +`Graph::computeCalleeCallerMapping` supplies SeaDsa's authoritative mapping for +globals, return values, formal/actual parameters, and reachable links. SMACK +maps every callee region cell into the caller and records: + +```text +callee region -> { caller region, ... } ``` -Entry points (`main`) keep globals with `modifies` clauses. Non-entry procedures use local in/out parameters. +The computation runs to a structural fixpoint because mapping a reachable cell +can create or merge caller regions. Failure to converge after 100 passes aborts +translation. ---- +### 4. Merge Propagation and Normalization -## Architecture +If several callee regions map to one caller region, the callee regions are +merged. All index-based tables are repaired after every erase. Mapping-key +collisions union their target sets instead of discarding one mapping. -### Phase 1: Per-Function Region Construction +Normalization retains the branch's pairwise merge algorithm for incomplete, +complicated, collapsed, and interval-overlapping regions. -**Files:** `Regions.cpp` (runOnModule) +### 5. Global Relations -Each function's region vector is built from: -1. **Formal pointer parameters** -- `idx(&formalArg, &F)` -2. **Instructions** -- load/store/atomic/memcpy pointer operands via `visit(F)` -3. **Call-site actual pointer arguments** -- `idx(actualArg, &F)` for each call in the function -4. **Globals** -- `idx(&GV, &F)` for globals present in the function's DSA graph -5. **Pointer-returning calls** -- `idx(&callInst, &F)` for calls that return pointers (both declarations and definitions) -6. **Link-following** -- for each existing region, follow DSA pointer links to discover reachable nodes and create regions for them using `Region(Node*, ctx)`. This ensures callers have regions for data accessible through pointer indirection (e.g., `**arg`). +For each ordinary function, global-backed regions are related to every matching +entry-function region. This table is relational. Exact global identity is also +tracked when preserving singleton scalar regions; merging views from different +globals demotes the result to a map. -The `Region(Node*, LLVMContext&)` constructor creates a region directly from a DSA node without needing a Value*. This is needed because callers may not have LLVM values for data they never directly access but their callees do. +Statically initialized globals retain the branch's conservative map encoding. -### Phase 2: Read/Write Sets +### 6. Backing Maps -Direct memory accesses in each function are recorded: -- `LoadInst` -> readRegions -- `StoreInst` -> modifiedRegions -- `AtomicCmpXchgInst`, `AtomicRMWInst` -> both -- `MemSetInst` -> modifiedRegions -- `MemTransferInst` -> readRegions (source) + modifiedRegions (dest) +A union-find structure links region pairs through call-site and global +relations. The branch's existing backing policy is retained: -### Phase 2.5: Global Memory Mappings +- entry regions keep their module-level declarations; +- small classes with two same-function regions and at most eight members can + remain threaded through procedure interfaces; +- other cross-function classes use entry-owned or shared module-level maps; +- accessed regions outside mapped classes use the existing shared-map + fallback. -For non-entry `usesGlobalMemory` functions (e.g., `__SMACK_static_init`), compute mappings from their region indices to the entry function's indices via shared globals. +Classes containing a non-unique relation are excluded from threading. If a +non-threaded class contains several regions from one function, selecting one +of them as its owner would disconnect the others, so that class uses one shared +map. This is a representational soundness requirement, not a memory-splitting +or map-count optimization. -### Phase 3: Call-Site Mappings +### 7. Access Closure and Interfaces -**`computeOneCallSiteMapping(CI, caller, callee)`** builds a map from callee region indices to caller region indices through: +Callee reads and modifications propagate through every caller target in the +call-site relation until no access set changes. Procedure inputs and outputs +are then computed for classes retained by the existing threading policy. -1. Build the authoritative SeaDsa call-site simulation with `Graph::computeCalleeCallerMapping`. -2. For each callee region, ask the `SimulationMapper` for the corresponding caller `Cell`. -3. Translate the mapped caller `Cell` back into the caller's local region index, creating a caller region if the caller has no LLVM `Value*` for that reachable node. +## Failure Policy -SMACK does not reimplement SeaDsa's mapping rules. SeaDsa owns the root matching for globals, return values, and pointer formal/actual pairs, plus recursive link following with offset/collapsed-node handling. If SeaDsa cannot map the call site, the translation fails instead of falling back to equal numeric region indices. +SMACK aborts translation instead of continuing when: -**Iteration:** `computeCallSiteMappings` runs iteratively (up to 10 passes) because link-following may create new regions in callers, which then need mappings computed for their own callers. +- SeaDsa cannot compute a call-site mapping; +- SeaDsa returns a nonfunctional simulation relation that its public lookup API + cannot enumerate; +- call-site region construction does not converge; +- a required global cell cannot be translated or conservatively represented; +- a non-unique relation reaches a code path that requires one owner. -### Phase 3.5: Region Merge Propagation +These failures are preferable to proving a program against disconnected or +incomplete memory state. -**`propagateRegionMerges(M)`** enforces the soundness invariant: **regions must not alias**. Uses SCCs for proper ordering. +## Regression Coverage -**Top-down pass:** When a caller maps two callee regions to the same caller region, the callee regions are merged (they alias from the caller's perspective). `mergeCalleeRegion` handles the merge and updates all affected call-site mappings. +- `cs_dsa_region_threading.c`: nested heap and pointer flow across calls. +- `strings.c` and `strings1.c`: offset-preserving static-initializer mapping. -**Bottom-up pass:** When a callee has collapsed regions that the caller keeps separate, the caller's regions are merged to match. +## Main Files -**Key invariant in `mergeCalleeRegion`:** When shifting callee-side keys in call-site mappings, existing entries (typically from parameter mappings) take priority over entries from merged-away regions. This prevents global mapping collisions from overwriting call-site-specific parameter mappings. - -### Phase 4: Transitive Closure - -**`computeFunctionRegions(M)`** propagates callee region accesses to callers through call-site mappings until convergence. Only mapped regions are propagated. - -### Phase 5: Procedure Memory Interfaces - -**`computeInterfaceRegions(M)`** separates local memory from caller-visible memory: - -1. **Input regions** are accessed regions reachable from formal pointer parameters or globals. -2. **Output regions** are modified regions reachable from formal pointer parameters, globals, or the function return cell. - -Only input regions become `$M.r.in` parameters, and only output regions become `$M.r.out` returns. Private stack/heap regions remain local Boogie variables; they are not threaded through callers. - ---- - -## Key Design Decisions - -### SeaDsa-Owned Mapping -The call-site mapping must follow SeaDsa's `SimulationMapper`; function-local region numbers are not comparable across functions. Falling back from an unmapped callee region to the same numeric caller region is unsound and is intentionally rejected. - -### Interface Reachability -DSA graphs encode which nodes are reachable from parameters, globals, and return values. Procedure signatures expose only those regions. This avoids requiring callers to provide memory maps for callee-private allocas or heap objects that do not escape. - -### Region Creation from DSA Nodes -The `Region(const seadsa::Node*, LLVMContext&)` constructor enables creating regions for DSA nodes that have no corresponding LLVM Value in the function. This is needed when: -- A caller passes a pointer and the callee accesses through multiple levels of indirection -- Phase 1 link-following discovers reachable nodes -- Phase 3 link-following creates regions during mapping computation - -### Return Value Mapping -Call-site mappings include the callee's SeaDsa return cell and the caller's call-result cell. This is critical for function pointer dispatch patterns like `devirtbounce`, where data flows through return values rather than parameters. - ---- - -## Test Notes - -The `smack_code_call` tests use `__SMACK_code` to emit inline BPL calls that bypass the memory map threading. This is a pre-existing limitation of inline BPL with per-function memory maps. - ---- - -## File Summary - -| File | Change | -|------|--------| -| `DSAWrapper.h/cpp` | Function-aware `getNode`/`getOffset`/`isTypeSafe` with per-function graph lookup | -| `Regions.h/cpp` | Per-function region vectors, call-site mappings, link-following, merge propagation, `Region(Node*)` constructor | -| `SmackRep.h/cpp` | Memory map params/returns in procedure signatures, call-site mapping for threading | -| `SmackInstGenerator.cpp` | Prologue/epilogue for local memory shadows, entry block initialization | -| `SmackModuleGenerator.cpp` | Local var declarations for non-entry functions, global-scope region handling | -| `Prelude.cpp` | Per-function region types in prelude generation | -| `SmackOptions.h/cpp` | `usesGlobalMemory`, `isEntryPoint` helpers | -| `top.py` | Switch to `-sea-dsa=cs`, fix `VProperty.__members__` for `--check` flag | +| File | Responsibility | +|------|----------------| +| `DSAWrapper.h/cpp` | Function graph lookup and exact global-cell translation | +| `Regions.h/cpp` | Regions, relational mappings, merge repair, and backing classes | +| `SmackRep.cpp` | Resolve local indices and validate threaded mappings | diff --git a/include/smack/DSAWrapper.h b/include/smack/DSAWrapper.h index 9de9cd34b..74c4ed63a 100644 --- a/include/smack/DSAWrapper.h +++ b/include/smack/DSAWrapper.h @@ -30,6 +30,8 @@ class DSAWrapper : public llvm::ModulePass { // Mapping from the DSNodes associated with globals to the numbers of // globals associated with them. std::unordered_map globalRefCount; + std::unordered_map + uniqueGlobalRefs; const llvm::DataLayout *dataLayout; void collectStaticInits(llvm::Module &M); @@ -59,15 +61,13 @@ class DSAWrapper : public llvm::ModulePass { bool isTypeSafe(const llvm::Value *v); bool isTypeSafe(const llvm::Value *v, const llvm::Function &F); unsigned getNumGlobals(const seadsa::Node *n); + const llvm::GlobalValue *getUniqueGlobal(const seadsa::Node *n) const; - // Simulation mappers between graphs, seeded on their shared globals; used - // to translate cells of one function's values into another function's - // graph (e.g., __SMACK_static_init expressions into the entry graph). - std::map, - std::unique_ptr> - globalMappers; - seadsa::SimulationMapper &globalMapper(seadsa::Graph &src, - seadsa::Graph &dst); + // Translate one value through the identity of its underlying global. + // Using one mapper seeded with every global can become nonfunctional and + // silently lose otherwise valid translations. + bool translateGlobalCell(const llvm::Value *v, seadsa::Graph &src, + seadsa::Graph &dst, seadsa::Cell &result) const; // Per-function graph access for context-sensitive analysis. seadsa::Graph &getGraph(const llvm::Function &F); diff --git a/include/smack/Regions.h b/include/smack/Regions.h index 05f9d1e4b..00325c8d9 100644 --- a/include/smack/Regions.h +++ b/include/smack/Regions.h @@ -30,6 +30,7 @@ class Region { unsigned length; bool singleton; + const llvm::GlobalValue *singletonGlobal; bool allocated; bool bytewise; bool incomplete; @@ -55,7 +56,8 @@ class Region { Region(const seadsa::Node *node, unsigned offset, unsigned length, LLVMContext &ctx); Region(const seadsa::Node *node, unsigned offset, unsigned length, - const llvm::Type *type, bool bytewise, LLVMContext &ctx); + const llvm::Type *type, bool bytewise, + const llvm::GlobalValue *singletonGlobal, LLVMContext &ctx); static void init(Module &M, Pass &P); @@ -74,7 +76,14 @@ class Region { // Force module-level emission (used when another function's region is // unified with this one, so the map must be visible module-wide). void markGlobalScope() { globalScope = true; } + void markNonSingleton() { + singleton = false; + singletonGlobal = nullptr; + } const Type *getType() const { return type; } + const llvm::GlobalValue *getSingletonGlobal() const { + return singletonGlobal; + } const seadsa::Node *getRepresentative() const { return representative; } unsigned getOffset() const { return offset; } unsigned getLength() const { return length; } @@ -89,6 +98,12 @@ struct FunctionRegionInfo { std::set outputRegions; }; +// A callee region may correspond to more than one caller region after either +// graph mapping or region merging. Keep the full relation: selecting one +// target disconnects the remaining caller state from the callee. +using RegionRelation = std::map>; +using CallSiteRegionMapping = RegionRelation; + class Regions : public ModulePass, public InstVisitor { private: // Per-function region vectors (each function has its own local numbering). @@ -102,14 +117,12 @@ class Regions : public ModulePass, public InstVisitor { // Per-function read/write sets (using function-local region indices). std::map funcRegions; - // Call-site mapping: callee region index -> caller region index. - std::map> - callSiteMappings; + // Call-site relation: callee region index -> caller region indices. + std::map callSiteMappings; // For non-entry functions: mapping from their region indices to the entry // function's region indices (matched via globals and call-site mappings). - std::map> - globalMemoryMappings; + std::map globalMemoryMappings; // Module-level maps for memory shared across functions without touching // the entry function's regions (e.g., heap passed between siblings). @@ -147,11 +160,6 @@ class Regions : public ModulePass, public InstVisitor { // recomputed, so information lost in later merges cannot be recovered. bool mappingsFinal = false; - // Number of callee->caller associations dropped by key collisions in - // remapAfterMerge after Phase 3 convergence (see the warning emitted in - // runOnModule). - unsigned droppedMappings = 0; - // Per-function idx: find or create a region in F's vector. unsigned idx(Region &R, const llvm::Function *F); int idxTranslated(const llvm::Value *V, const llvm::Function *F, @@ -195,10 +203,9 @@ class Regions : public ModulePass, public InstVisitor { const FunctionRegionInfo & getFunctionRegionInfo(const llvm::Function *F) const; std::set getAccessedRegions(const llvm::Function *F) const; - const std::map & + const CallSiteRegionMapping & getCallSiteMapping(const llvm::CallBase *CI) const; - const std::map & - getGlobalMemoryMapping(const llvm::Function *F) const; + const RegionRelation &getGlobalMemoryMapping(const llvm::Function *F) const; // Shared (module-level) maps for cross-function memory that does not // reach the entry function's regions. Returns -1 if F's region r is not // backed by a shared map. diff --git a/lib/smack/DSAWrapper.cpp b/lib/smack/DSAWrapper.cpp index 68fdb2af3..50fdb72a2 100644 --- a/lib/smack/DSAWrapper.cpp +++ b/lib/smack/DSAWrapper.cpp @@ -102,6 +102,7 @@ void DSAWrapper::collectMemOpds(llvm::Module &M) { void DSAWrapper::countGlobalRefs() { globalRefCount.clear(); + uniqueGlobalRefs.clear(); std::set seenGraphs; for (auto &F : *module) { @@ -115,10 +116,13 @@ void DSAWrapper::countGlobalRefs() { auto &cellRef = g.second; auto *node = cellRef->getNode(); assert(node && "Global values should have DSNodes."); - if (!globalRefCount.count(node)) + if (!globalRefCount.count(node)) { globalRefCount[node] = 1; - else + uniqueGlobalRefs[node] = dyn_cast(g.first); + } else { globalRefCount[node]++; + uniqueGlobalRefs[node] = nullptr; + } } } } @@ -193,21 +197,19 @@ unsigned DSAWrapper::getOffset(const Value *v, const Function &F) { // Translate through shared globals first (preserves field offsets). auto &src = getGraphForValue(v); if (&src != &graph && src.hasCell(*v)) { - seadsa::Cell srcCell = src.getCell(*v); - seadsa::Cell c = globalMapper(src, graph).get(*srcCell.getNode()); - if (!c.isNull()) { + seadsa::Cell c; + if (translateGlobalCell(v, src, graph, c)) { auto *n = c.getNode(); - unsigned long rawOff = (unsigned long)c.getOffset() + srcCell.getOffset(); + unsigned long rawOff = c.getOffset(); if (n->isOffsetCollapsed()) return 0; if (n->isArray() && n->size() > 0) return (unsigned)(rawOff % n->size()); return (unsigned)rawOff; } + report_fatal_error( + "cannot translate a global memory cell between SeaDsa graphs"); } - const Value *base = getUnderlyingObject(v); - if (base != v && graph.hasCell(*base)) - return graph.getCell(*base).getOffset(); return 0; } @@ -220,24 +222,24 @@ const seadsa::Node *DSAWrapper::getNode(const Value *v) { return node; } -seadsa::SimulationMapper &DSAWrapper::globalMapper(seadsa::Graph &src, - seadsa::Graph &dst) { - auto key = - std::make_pair((const seadsa::Graph *)&src, (const seadsa::Graph *)&dst); - auto it = globalMappers.find(key); - if (it != globalMappers.end()) - return *it->second; - auto &sm = - *(globalMappers[key] = std::make_unique()); - for (auto &GV : module->globals()) { - if (!src.hasCell(GV) || !dst.hasCell(GV)) - continue; - seadsa::Cell from = src.getCell(GV); - seadsa::Cell to = dst.getCell(GV); - // Best effort: an incompatible pair just stays untranslated. - sm.insert(from, to); - } - return sm; +bool DSAWrapper::translateGlobalCell(const Value *v, seadsa::Graph &src, + seadsa::Graph &dst, + seadsa::Cell &result) const { + if (!src.hasCell(*v)) + return false; + + const auto *GV = dyn_cast(getUnderlyingObject(v)); + if (!GV || !src.hasCell(*GV) || !dst.hasCell(*GV)) + return false; + + seadsa::Cell from = src.getCell(*GV); + seadsa::Cell to = dst.getCell(*GV); + seadsa::SimulationMapper mapper; + if (!mapper.insert(from, to) || !mapper.isFunction()) + return false; + + result = mapper.get(src.getCell(*v)); + return !result.isNull(); } const seadsa::Node *DSAWrapper::getNode(const Value *v, const Function &F) { @@ -255,16 +257,11 @@ const seadsa::Node *DSAWrapper::getNode(const Value *v, const Function &F) { // preserves field offsets, unlike stripping to the underlying object. auto &src = getGraphForValue(v); if (&src != &graph && src.hasCell(*v)) { - seadsa::Cell c = globalMapper(src, graph).get(*src.getCell(*v).getNode()); - if (!c.isNull()) + seadsa::Cell c; + if (translateGlobalCell(v, src, graph, c)) return c.getNode(); - } - // Fall back to the underlying object (the global variable) itself. - const Value *base = getUnderlyingObject(v); - if (base != v && graph.hasCell(*base)) { - auto node = graph.getCell(*base).getNode(); - assert(node && "Values should have nodes if they have cells."); - return node; + report_fatal_error( + "cannot translate a global memory cell between SeaDsa graphs"); } return nullptr; } @@ -413,6 +410,11 @@ unsigned DSAWrapper::getNumGlobals(const seadsa::Node *n) { return 0; } +const GlobalValue *DSAWrapper::getUniqueGlobal(const seadsa::Node *n) const { + auto it = uniqueGlobalRefs.find(n); + return it == uniqueGlobalRefs.end() ? nullptr : it->second; +} + } // namespace smack char smack::DSAWrapper::ID = 0; diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 15548b497..5ebf6fe72 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -7,6 +7,7 @@ #include "smack/DSAWrapper.h" #include "smack/Debug.h" #include "smack/SmackOptions.h" +#include "llvm/Analysis/ValueTracking.h" #include "llvm/IR/GetElementPtrTypeIterator.h" #include "llvm/IR/InstIterator.h" #include "llvm/IR/IntrinsicInst.h" @@ -34,11 +35,7 @@ bool Region::isSingleton(const Value *v, unsigned length, const Function *F) { return node && !isAllocated(node) && DSA->getNumGlobals(node) == 1 && !node->isArray() && (F ? DSA->isTypeSafe(v, *F) : DSA->isTypeSafe(v)) && - !DSA->isMemOpd(v) && - // Statically initialized globals cannot be singletons because - // CodifyStaticInits generates pointer-based stores ($store) for them - // in __SMACK_static_init, which requires map-typed $M variables. - !DSA->isStaticInitd(node); + !DSA->isMemOpd(v) && !DSA->isStaticInitd(node); } bool Region::isAllocated(const seadsa::Node *N) { @@ -68,6 +65,8 @@ void Region::init(const Value *V, unsigned length, const Function *F) { this->length = std::max(length, 1u); singleton = DL && representative && isSingleton(V, length, F); + singletonGlobal = singleton ? DSA->getUniqueGlobal(representative) : nullptr; + singleton = singletonGlobal != nullptr; allocated = !representative || isAllocated(representative); bytewise = DSA && SmackOptions::BitPrecise && (SmackOptions::NoByteAccessInference || @@ -113,6 +112,7 @@ Region::Region(const seadsa::Node *node, unsigned offset, unsigned length, this->offset = offset; this->length = length; singleton = false; + singletonGlobal = nullptr; allocated = !representative || isAllocated(representative); bytewise = true; incomplete = !representative || representative->isIncomplete(); @@ -122,13 +122,21 @@ Region::Region(const seadsa::Node *node, unsigned offset, unsigned length, } Region::Region(const seadsa::Node *node, unsigned offset, unsigned length, - const Type *type, bool bytewise, LLVMContext &ctx) { + const Type *type, bool bytewise, + const GlobalValue *singletonGlobal, LLVMContext &ctx) { context = &ctx; representative = node; this->type = type; this->offset = offset; this->length = length; - singleton = false; + const GlobalValue *targetGlobal = + representative ? DSA->getUniqueGlobal(representative) : nullptr; + this->singletonGlobal = singletonGlobal && singletonGlobal == targetGlobal && + !isAllocated(representative) && + !representative->isArray() + ? singletonGlobal + : nullptr; + singleton = this->singletonGlobal != nullptr; allocated = !representative || isAllocated(representative); this->bytewise = bytewise; incomplete = !representative || representative->isIncomplete(); @@ -150,6 +158,11 @@ bool Region::merge(Region &R) { std::make_tuple(offset, length, singleton, allocated, bytewise, incomplete, complicated, collapsed, globalScope, type); bool collapse = type != R.type; + const GlobalValue *mergedSingleton = + singleton && R.singleton && singletonGlobal == R.singletonGlobal && + offset == R.offset + ? singletonGlobal + : nullptr; unsigned long low = std::min(offset, R.offset); unsigned long high = std::max((unsigned long)offset + length, (unsigned long)R.offset + R.length); @@ -159,7 +172,8 @@ bool Region::merge(Region &R) { // which lets the Phase 3 fixpoint oscillate (merge, then re-create). length = (unsigned)std::min( high - low, (unsigned long)std::numeric_limits::max() - low); - singleton = singleton && R.singleton; + singletonGlobal = mergedSingleton; + singleton = singletonGlobal != nullptr; allocated = allocated || R.allocated; bytewise = SmackOptions::BitPrecise && (bytewise || R.bytewise || collapse); incomplete = incomplete || R.incomplete; @@ -179,7 +193,11 @@ void Region::mergeAttributes(const Region &R) { // Region::overlaps; absorbing them from another node's region would arm // spurious cross-node matches after the normalization pass has run. bool collapse = type != R.type; - singleton = singleton && R.singleton; + singletonGlobal = + singleton && R.singleton && singletonGlobal == R.singletonGlobal + ? singletonGlobal + : nullptr; + singleton = singletonGlobal != nullptr; allocated = allocated || R.allocated; bytewise = SmackOptions::BitPrecise && (bytewise || R.bytewise || collapse); globalScope = globalScope || R.globalScope; @@ -374,10 +392,8 @@ bool Regions::runOnModule(Module &M) { break; } if (iter == maxIters) - errs() << "SMACK warning: call-site region mappings did not stabilize " - "after " - << maxIters - << " passes; some memory-region mappings may be incomplete\n"; + report_fatal_error( + "call-site region mappings did not stabilize after 100 passes"); mappingsFinal = true; dumpPhase("3-mappings", funcRegionVecs); @@ -386,11 +402,6 @@ bool Regions::runOnModule(Module &M) { // caller region), the callee must merge them to preserve the invariant // that regions never alias. propagateRegionMerges(M); - if (droppedMappings) - errs() << "SMACK warning: " << droppedMappings - << " call-site region mapping(s) dropped during region merge " - "propagation; callers may see stale memory for the affected " - "regions (-debug-only=regions for details)\n"; dumpPhase("3.5-merges", funcRegionVecs); // Phase 3.6: Map global-backed regions of every function to the entry @@ -400,13 +411,13 @@ bool Regions::runOnModule(Module &M) { computeGlobalMemoryMappings(M); dumpPhase("3.6-globals", funcRegionVecs); - // Phase 3.7: Unify all remaining cross-function memory into - // module-level maps by taking the transitive closure of the call-site - // mappings. Threading memory maps through procedure signatures places - // them beyond Corral's variable-tracking abstraction and inflates - // every inlined instance with map parameters and copies; emitting - // shared memory as globals keeps the encoding within the abstraction. - // Only function-private regions remain procedure-local. + // Phase 3.7: Bind cross-function equivalence classes to entry-owned or + // shared module-level maps, except for the small classes retained by the + // branch's existing procedure-interface threading policy. + // Threading memory maps through procedure signatures places them beyond + // Corral's variable-tracking abstraction and inflates every inlined + // instance with map parameters and copies; emitting shared memory as + // globals keeps the encoding within the abstraction. unifySharedRegions(M); // Phase 3.8: Final normalization. Merges in Phases 3.5-3.7 can widen @@ -420,9 +431,7 @@ bool Regions::runOnModule(Module &M) { // Phase 4: Transitive closure of region access sets. computeFunctionRegions(M); - // Phase 5: Procedure memory interfaces. Private regions stay local; only - // regions reachable from formals/globals/returns are threaded through - // calls. + // Phase 5: Procedure memory interfaces for the retained threaded classes. computeInterfaceRegions(M); } @@ -467,16 +476,27 @@ int Regions::idxTranslated(const Value *V, const Function *F, unsigned length) { auto sc = srcG.getCell(*V); if (!sc.getNode()) return -1; - auto tc = DSA->globalMapper(srcG, dstG).get(*sc.getNode()); - if (tc.isNull()) - return -1; - const Type *T = V->getType()->isPointerTy() - ? V->getType()->getPointerElementType() - : nullptr; - Region R(tc.getNode(), - composeOffset(tc.getNode(), - (unsigned long)tc.getOffset() + sc.getOffset()), - length, T, SmackOptions::BitPrecise, V->getContext()); + seadsa::Cell tc; + if (!DSA->translateGlobalCell(V, srcG, dstG, tc)) { + // If field-sensitive translation is unavailable, use the entire target + // global node. This loses precision but makes every access through that + // node share one backing region instead of silently using offset zero. + const auto *GV = dyn_cast(getUnderlyingObject(V)); + if (!GV || !dstG.hasCell(*GV)) + report_fatal_error( + "cannot conservatively translate a global SeaDsa cell"); + auto dst = dstG.getCell(*GV); + auto *node = dst.getNode(); + if (!node) + report_fatal_error("global SeaDsa cell has no target node"); + Region R(node, 0, std::max(node->size(), 1u), nullptr, + SmackOptions::BitPrecise, nullptr, V->getContext()); + return (int)idx(R, F); + } + Region source(V, translationSource, length); + Region R(tc.getNode(), composeOffset(tc.getNode(), tc.getOffset()), length, + source.getType(), source.bytewiseAccess(), + source.getSingletonGlobal(), V->getContext()); return (int)idx(R, F); } @@ -783,6 +803,9 @@ void Regions::computeOneCallSiteMapping(CallBase *CI, const Function *caller, if (!mapped) report_fatal_error( "SeaDsa failed to map callee regions to caller regions."); + if (!simMap.isFunction()) + report_fatal_error( + "SeaDsa produced a nonfunctional callee-to-caller memory mapping"); // Iterate by index over the live callee region vector: idx() below can // merge regions (in the caller, or in the callee itself for recursive @@ -805,8 +828,9 @@ void Regions::computeOneCallSiteMapping(CallBase *CI, const Function *caller, Region callerRegion(callerCell.getNode(), callerCell.getOffset(), std::max(calleeRegion.getLength(), 1u), calleeRegion.getType(), calleeRegion.bytewiseAccess(), + calleeRegion.getSingletonGlobal(), caller->getContext()); - mapping[i] = idx(callerRegion, caller); + mapping[i].insert(idx(callerRegion, caller)); } } @@ -858,15 +882,21 @@ void Regions::remapAfterMerge(const Function *F, unsigned keep, { auto it = globalMemoryMappings.find(F); if (it != globalMemoryMappings.end()) { - std::map newMapping; - for (auto &m : it->second) - newMapping[remapRegionIndex(m.first, keep, remove)] = m.second; + RegionRelation newMapping; + for (auto &m : it->second) { + unsigned key = remapRegionIndex(m.first, keep, remove); + newMapping[key].insert(m.second.begin(), m.second.end()); + } it->second = newMapping; } if (F->hasName() && SmackOptions::isEntryPoint(F->getName())) for (auto &gm : globalMemoryMappings) - for (auto &m : gm.second) - m.second = remapRegionIndex(m.second, keep, remove); + for (auto &m : gm.second) { + std::set values; + for (unsigned value : m.second) + values.insert(remapRegionIndex(value, keep, remove)); + m.second = values; + } } // Shift F-local indices in the shared-region table. @@ -898,29 +928,17 @@ void Regions::remapAfterMerge(const Function *F, unsigned keep, if (csCallee != F && csCaller != F) continue; - // When the `remove` key collapses into `keep`, prefer the existing - // `keep` entry (typically from parameter mapping, which is - // call-site-specific and more precise than globals). - std::map newMapping; + // When the `remove` key collapses into `keep`, union every caller target + // so no association is lost to the key collision. + CallSiteRegionMapping newMapping; for (auto &m : mapping) { unsigned k = m.first; - unsigned v = m.second; if (csCallee == F) k = remapRegionIndex(k, keep, remove); - if (csCaller == F) - v = remapRegionIndex(v, keep, remove); - auto ins = newMapping.insert({k, v}); - // Dropping a colliding entry whose caller region differs loses the - // association between the merged callee region and that caller - // region. During Phase 3 the next pass recomputes the mapping; after - // Phase 3 (propagateRegionMerges) it is not recomputed, so count the - // loss and report it once instead of failing silently. - if (!ins.second && ins.first->second != v && mappingsFinal) { - droppedMappings++; - SDEBUG(errs() << "[regions] dropped call-site mapping " << remove - << " -> " << v << " (kept " << keep << " -> " - << ins.first->second << ") merging regions of " - << F->getName() << "\n"); + for (unsigned v : m.second) { + if (csCaller == F) + v = remapRegionIndex(v, keep, remove); + newMapping[k].insert(v); } } mapping = newMapping; @@ -1030,7 +1048,8 @@ void Regions::propagateRegionMerges(Module &M) { // region. std::map> callerToCallees; for (auto &m : mapping) - callerToCallees[m.second].push_back(m.first); + for (unsigned callerR : m.second) + callerToCallees[callerR].push_back(m.first); for (auto &entry : callerToCallees) { auto &calleeIndices = entry.second; @@ -1127,63 +1146,48 @@ void Regions::computeGlobalMemoryMappings(Module &M) { if (!entryF || !DSA->hasGraph(*entryF)) return; - // Map each function's global-backed regions to the entry function's - // region holding the same global. When one function-level region covers - // globals that the entry function keeps in separate regions, those entry - // regions alias through this function and must be merged; - // mergeCalleeRegion repairs all bookkeeping (including these mappings), - // and merges strictly decrease the entry region count, so iterating to a - // fixpoint terminates. - bool changed = true; - while (changed) { - changed = false; - for (auto &F : M) { - if (F.isDeclaration() || &F == entryF) - continue; - // usesGlobalMemory functions (e.g., __SMACK_static_init) are emitted - // in the entry function's region context and need no mapping. - if (F.hasName() && SmackOptions::usesGlobalMemory(F.getName())) + // Map each function's global-backed regions to every entry-function region + // holding the same global. The relation is unified into one backing map in + // unifySharedRegions; selecting or physically merging one entry region here + // would either lose state or unnecessarily collapse field intervals. + for (auto &F : M) { + if (F.isDeclaration() || &F == entryF) + continue; + // usesGlobalMemory functions (e.g., __SMACK_static_init) are emitted + // in the entry function's region context and need no mapping. + if (F.hasName() && SmackOptions::usesGlobalMemory(F.getName())) + continue; + if (!DSA->hasGraph(F)) + continue; + auto &fGraph = DSA->getGraph(F); + auto &entryGraph = DSA->getGraph(*entryF); + // Lookups must not create regions: probing a global with its whole extent + // would merge away the per-field regions created from actual accesses. + auto &mapping = globalMemoryMappings[&F]; + for (auto &GV : M.globals()) { + if (!fGraph.hasCell(GV) || !entryGraph.hasCell(GV)) continue; - if (!DSA->hasGraph(F)) + auto fCell = fGraph.getCell(GV); + auto entryCell = entryGraph.getCell(GV); + int fR = findRegion(&F, fCell.getNode(), fCell.getOffset()); + int entryR = + findRegion(entryF, entryCell.getNode(), entryCell.getOffset()); + if (fR < 0 || entryR < 0) continue; - auto &fGraph = DSA->getGraph(F); - auto &entryGraph = DSA->getGraph(*entryF); - // Build in place: entry-side merges triggered below remap the values - // of every registered mapping, including this one. Lookups must not - // create regions: probing a global with its whole extent would merge - // away the per-field regions created from the actual accesses. - auto &mapping = globalMemoryMappings[&F]; - for (auto &GV : M.globals()) { - if (!fGraph.hasCell(GV) || !entryGraph.hasCell(GV)) - continue; - auto fCell = fGraph.getCell(GV); - auto entryCell = entryGraph.getCell(GV); - int fR = findRegion(&F, fCell.getNode(), fCell.getOffset()); - int entryR = - findRegion(entryF, entryCell.getNode(), entryCell.getOffset()); - if (fR < 0 || entryR < 0) - continue; - auto it = mapping.find((unsigned)fR); - if (it == mapping.end()) { - mapping[(unsigned)fR] = (unsigned)entryR; - changed = true; - } else if (it->second != (unsigned)entryR) { - mergeCalleeRegion(entryF, it->second, (unsigned)entryR); - changed = true; - } - } - // The entry region's declared map type must cover this function's - // view of the memory (relevant under bit-precise encodings), and the - // map must be module-level since other functions reference it. - auto &entryRegions = funcRegionVecs[entryF]; - auto &fRegions = funcRegionVecs[&F]; - for (auto &m : mapping) { - assert(m.first < fRegions.size() && m.second < entryRegions.size() && + mapping[(unsigned)fR].insert((unsigned)entryR); + } + // The entry region's declared map type must cover this function's + // view of the memory (relevant under bit-precise encodings), and the + // map must be module-level since other functions reference it. + auto &entryRegions = funcRegionVecs[entryF]; + auto &fRegions = funcRegionVecs[&F]; + for (auto &m : mapping) + for (unsigned entryR : m.second) { + assert(m.first < fRegions.size() && entryR < entryRegions.size() && "region indices must be repaired by remapAfterMerge"); - entryRegions[m.second].mergeAttributes(fRegions[m.first]); - entryRegions[m.second].markGlobalScope(); + entryRegions[entryR].mergeAttributes(fRegions[m.first]); + entryRegions[entryR].markGlobalScope(); } - } } } @@ -1220,6 +1224,7 @@ void Regions::unifySharedRegions(Module &M) { }; auto unite = [&](unsigned a, unsigned b) { parent[find(a)] = find(b); }; + std::vector forceSharedIds; for (auto &cs : callSiteMappings) { auto *CB = const_cast(cs.first); Function *callee = CB->getCalledFunction(); @@ -1229,52 +1234,70 @@ void Regions::unifySharedRegions(Module &M) { if (!callee) continue; const Function *caller = CB->getParent()->getParent(); - for (auto &m : cs.second) - unite(id(callee, m.first), id(caller, m.second)); + for (auto &m : cs.second) { + unsigned calleeId = id(callee, m.first); + if (m.second.size() > 1) + forceSharedIds.push_back(calleeId); + for (unsigned callerR : m.second) + unite(calleeId, id(caller, callerR)); + } } if (entryF) for (auto &gm : globalMemoryMappings) - for (auto &m : gm.second) - unite(id(gm.first, m.first), id(entryF, m.second)); - - // A small class containing exactly two distinct regions of some function - // keeps the per-call-site threading instead of binding to one - // module-level map: two regions of one function are distinct objects in - // that context (e.g. two arrays passed to the same callee), and folding - // them into one map loses separation that both the threading scheme and - // the context-insensitive baseline preserve (measured 4x slower on - // test/c/data/two_arrays1.c). Large classes or classes where some - // function has three or more regions are collapse artifacts spanning - // dozens of regions on driver benchmarks; threading those costs far more - // than the separation is worth, so they still merge. + for (auto &m : gm.second) { + unsigned localId = id(gm.first, m.first); + if (m.second.size() > 1) + forceSharedIds.push_back(localId); + for (unsigned entryR : m.second) + unite(localId, id(entryF, entryR)); + } + + std::set forceShared; + for (unsigned i : forceSharedIds) + forceShared.insert(find(i)); + + // Preserve the branch's existing policy for small classes with exactly + // two regions in one function: keep threading those maps through calls. + // A relation with more than one target cannot be threaded through a single + // call argument and is therefore forced onto one shared backing map. std::set classThreaded; { - std::map classSizePre; + std::map classSize; for (auto &kv : ids) - classSizePre[find(kv.second)]++; - std::map, unsigned> mult; + classSize[find(kv.second)]++; + std::map, unsigned> multiplicity; for (auto &kv : ids) - mult[{find(kv.second), kv.first.first}]++; - std::map maxMult; - for (auto &m : mult) { - auto &cur = maxMult[m.first.first]; - cur = std::max(cur, m.second); + multiplicity[{find(kv.second), kv.first.first}]++; + std::map maxMultiplicity; + for (auto &m : multiplicity) { + auto ¤t = maxMultiplicity[m.first.first]; + current = std::max(current, m.second); } - for (auto &m : maxMult) - if (m.second == 2 && classSizePre.at(m.first) <= 8) + for (auto &m : maxMultiplicity) + if (m.second == 2 && classSize.at(m.first) <= 8 && + !forceShared.count(m.first)) classThreaded.insert(m.first); } + // Non-threaded classes with several regions from one function cannot choose + // one of those regions as their owner without disconnecting the others. + std::set classNeedsShared; + std::map, unsigned> multiplicity; + for (auto &kv : ids) + multiplicity[{find(kv.second), kv.first.first}]++; + for (auto &m : multiplicity) + if (m.second > 1 && !classThreaded.count(m.first.first)) + classNeedsShared.insert(m.first.first); + classNeedsShared.insert(forceShared.begin(), forceShared.end()); + std::map classEntry; if (entryF) for (auto &kv : ids) - if (kv.first.first == entryF) + if (kv.first.first == entryF && + !classNeedsShared.count(find(kv.second)) && + !classThreaded.count(find(kv.second))) classEntry[find(kv.second)] = kv.first.second; - std::map classSize; - for (auto &kv : ids) - classSize[find(kv.second)]++; - std::set> threadedPairs; std::map classShared; for (auto &kv : ids) { @@ -1282,20 +1305,16 @@ void Regions::unifySharedRegions(Module &M) { unsigned r = kv.first.second; unsigned root = find(kv.second); if (classThreaded.count(root)) { - // Members bound by globals identity in Phase 3.6 keep their binding - // (sea-dsa propagates global symbols along call chains, so a bound - // callee implies a bound caller and the mix stays consistent); the - // remaining members thread. threadedPairs.insert({F, r}); continue; } - if (F == entryF) + if (F == entryF && !classNeedsShared.count(root)) continue; assert(r < funcRegionVecs[F].size() && "region indices must be repaired by remapAfterMerge"); auto ce = classEntry.find(root); if (ce != classEntry.end()) { - globalMemoryMappings[F][r] = ce->second; + globalMemoryMappings[F][r] = {ce->second}; assert(ce->second < funcRegionVecs[entryF].size() && "region indices must be repaired by remapAfterMerge"); funcRegionVecs[entryF][ce->second].mergeAttributes(funcRegionVecs[F][r]); @@ -1314,6 +1333,8 @@ void Regions::unifySharedRegions(Module &M) { if (cs == classShared.end()) { s = sharedRegions.size(); sharedRegions.push_back(funcRegionVecs[F][r]); + if (classNeedsShared.count(root)) + sharedRegions.back().markNonSingleton(); classShared[root] = s; } else { s = cs->second; @@ -1322,10 +1343,8 @@ void Regions::unifySharedRegions(Module &M) { sharedRegionIndex[{F, r}] = s; } - // Regions never mentioned by any call-site or global mapping (e.g. in - // functions that are never called through a mapped call site) get - // module-level maps of their own, for the same Corral-abstraction - // reason as above. + // Regions never mentioned by any call-site or global mapping get + // module-level maps of their own, preserving the branch's existing policy. for (auto &fr : funcRegions) { const Function *F = fr.first; if (F == entryF) @@ -1346,9 +1365,8 @@ void Regions::unifySharedRegions(Module &M) { } } - // The entry function's own maps are all module-level too: an untracked - // global costs Corral nothing, while a procedure-local map is always - // precise. + // Preserve the branch's declaration policy: all entry regions are + // module-level maps, whether or not the access closure reaches them. if (entryF) for (auto &R : funcRegionVecs[entryF]) R.markGlobalScope(); @@ -1383,14 +1401,16 @@ void Regions::computeFunctionRegions(Module &M) { for (unsigned calleeR : calleeInfo.readRegions) { if (mapping.count(calleeR)) { - if (info.readRegions.insert(mapping.at(calleeR)).second) - changed = true; + for (unsigned callerR : mapping.at(calleeR)) + if (info.readRegions.insert(callerR).second) + changed = true; } } for (unsigned calleeR : calleeInfo.modifiedRegions) { if (mapping.count(calleeR)) { - if (info.modifiedRegions.insert(mapping.at(calleeR)).second) - changed = true; + for (unsigned callerR : mapping.at(calleeR)) + if (info.modifiedRegions.insert(callerR).second) + changed = true; } } } @@ -1418,7 +1438,7 @@ void Regions::computeInterfaceRegions(Module &M) { // Regions mapped to module-level maps (entry or shared) are accessed // directly and are not threaded through the procedure signature. auto gmIt = globalMemoryMappings.find(&F); - const std::map *gm = + const RegionRelation *gm = gmIt != globalMemoryMappings.end() ? &gmIt->second : nullptr; auto accessed = getAccessedRegions(&F); @@ -1455,18 +1475,17 @@ std::set Regions::getAccessedRegions(const Function *F) const { return result; } -const std::map & +const CallSiteRegionMapping & Regions::getCallSiteMapping(const CallBase *CB) const { - static const std::map emptyMapping; + static const CallSiteRegionMapping emptyMapping; auto it = callSiteMappings.find(CB); if (it != callSiteMappings.end()) return it->second; return emptyMapping; } -const std::map & -Regions::getGlobalMemoryMapping(const Function *F) const { - static const std::map emptyMapping; +const RegionRelation &Regions::getGlobalMemoryMapping(const Function *F) const { + static const RegionRelation emptyMapping; auto it = globalMemoryMappings.find(F); if (it != globalMemoryMappings.end()) return it->second; diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 7828c35be..075a4f363 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -322,15 +322,19 @@ std::string SmackRep::memSharedReg(unsigned idx) { // currentFunction before resolving. std::pair SmackRep::resolveRegion(unsigned region) { + if (currentFunction) { + int s = regions->getSharedRegionIndex(currentFunction, region); + if (s >= 0) + return {nullptr, (unsigned)s}; + } if (currentFunction && currentFunction->hasName() && !SmackOptions::usesGlobalMemory(currentFunction->getName())) { auto &gm = regions->getGlobalMemoryMapping(currentFunction); auto it = gm.find(region); - if (it != gm.end() && entryFunction) - return {entryFunction, it->second}; - int s = regions->getSharedRegionIndex(currentFunction, region); - if (s >= 0) - return {nullptr, (unsigned)s}; + if (it != gm.end() && it->second.size() == 1 && entryFunction) + return {entryFunction, *it->second.begin()}; + if (it != gm.end()) + report_fatal_error("non-unique global memory mapping was not shared"); } return {currentFunction, region}; } @@ -1235,11 +1239,12 @@ const Stmt *SmackRep::call(llvm::Function *f, const llvm::User &ci) { auto mapRegion = [&](unsigned calleeR) -> unsigned { auto it = mapping.find(calleeR); - if (it == mapping.end()) + if (it == mapping.end() || it->second.size() != 1) report_fatal_error( - "missing SeaDsa call-site memory-region mapping for call to " + + "missing or non-unique SeaDsa call-site memory-region mapping " + "for call to " + f->getName()); - return it->second; + return *it->second.begin(); }; auto &info = regions->getFunctionRegionInfo(f); @@ -1390,21 +1395,21 @@ std::string SmackRep::code(llvm::CallInst &ci) { for (unsigned calleeR : info.inputRegions) { auto it = mapping.find(calleeR); - if (it == mapping.end()) { + if (it == mapping.end() || it->second.size() != 1) { complete = false; break; } - memArgs.push_back(memPath(it->second)); + memArgs.push_back(memPath(*it->second.begin())); } if (complete) { for (unsigned calleeR : info.outputRegions) { auto it = mapping.find(calleeR); - if (it == mapping.end()) { + if (it == mapping.end() || it->second.size() != 1) { complete = false; break; } - memRets.push_back(memPath(it->second)); + memRets.push_back(memPath(*it->second.begin())); } } From d660a6c1793f0852259cb5e415d1d7df30221b1c Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 13 Jul 2026 09:11:58 -0700 Subject: [PATCH 02/12] Eliminate unused static-initializer memory maps --- include/smack/BoogieAst.h | 1 + include/smack/DSAWrapper.h | 1 + include/smack/SmackRep.h | 8 ++ lib/smack/DSAWrapper.cpp | 4 + lib/smack/Prelude.cpp | 32 ++++++-- lib/smack/SmackModuleGenerator.cpp | 115 +++++++++++++++++++++++++++ test/c/basic/static_init_dead_maps.c | 18 +++++ 7 files changed, 172 insertions(+), 7 deletions(-) create mode 100644 test/c/basic/static_init_dead_maps.c diff --git a/include/smack/BoogieAst.h b/include/smack/BoogieAst.h index 06e77157c..6aaf47fc3 100644 --- a/include/smack/BoogieAst.h +++ b/include/smack/BoogieAst.h @@ -354,6 +354,7 @@ class AssignStmt : public Stmt { public: AssignStmt(std::list lhs, std::list rhs) : Stmt(ASSIGN), lhs(lhs), rhs(rhs) {} + const std::list &getLhs() const { return lhs; } void print(std::ostream &os) const override; static bool classof(const Stmt *S) { return S->getKind() == ASSIGN; } }; diff --git a/include/smack/DSAWrapper.h b/include/smack/DSAWrapper.h index 74c4ed63a..7f24bc821 100644 --- a/include/smack/DSAWrapper.h +++ b/include/smack/DSAWrapper.h @@ -70,6 +70,7 @@ class DSAWrapper : public llvm::ModulePass { seadsa::Graph &dst, seadsa::Cell &result) const; // Per-function graph access for context-sensitive analysis. + bool isContextSensitive() const; seadsa::Graph &getGraph(const llvm::Function &F); bool hasGraph(const llvm::Function &F) const; }; diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index 1fb4add9f..a2e247736 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -13,6 +13,7 @@ #include "llvm/Support/Regex.h" #include #include +#include #include namespace smack { @@ -59,6 +60,7 @@ class SmackRep { std::vector initFuncs; std::map auxDecls; + std::set deadMemoryMaps; public: // Current function being processed (set by SmackModuleGenerator). @@ -69,6 +71,12 @@ class SmackRep { SmackRep(const llvm::DataLayout *L, Naming *N, Program *P, Regions *R); Program *getProgram() { return program; } Regions *getRegions() { return regions; } + void markDeadMemoryMap(const std::string &name) { + deadMemoryMaps.insert(name); + } + bool isDeadMemoryMap(const std::string &name) const { + return deadMemoryMaps.count(name) != 0; + } private: unsigned storageSize(llvm::Type *T); diff --git a/lib/smack/DSAWrapper.cpp b/lib/smack/DSAWrapper.cpp index 50fdb72a2..038566a53 100644 --- a/lib/smack/DSAWrapper.cpp +++ b/lib/smack/DSAWrapper.cpp @@ -181,6 +181,10 @@ seadsa::Graph &DSAWrapper::getGraph(const Function &F) { bool DSAWrapper::hasGraph(const Function &F) const { return SD->hasGraph(F); } +bool DSAWrapper::isContextSensitive() const { + return SD && SD->kind() == seadsa::GlobalAnalysisKind::CONTEXT_SENSITIVE; +} + unsigned DSAWrapper::getOffset(const Value *v) { auto &graph = getGraphForValue(v); if (!graph.hasCell(*v)) diff --git a/lib/smack/Prelude.cpp b/lib/smack/Prelude.cpp index ed86a60f8..7c4cb1f08 100644 --- a/lib/smack/Prelude.cpp +++ b/lib/smack/Prelude.cpp @@ -1116,21 +1116,39 @@ void ConstDeclGen::generate(std::stringstream &s) const { void MemDeclGen::generateMemoryMaps(std::stringstream &s) const { auto *entryF = prelude.rep.entryFunction; unsigned numRegions = entryF ? prelude.rep.regions->size(entryF) : 0; - describe("Memory maps (" + std::to_string(numRegions) + " regions)", s); + unsigned numMemoryMaps = 0; if (entryF) { for (unsigned i = 0; i < numRegions; i++) { - if (prelude.rep.regions->get(entryF, i).isGlobalScope()) - s << "var " << prelude.rep.memReg(i) << ": " - << prelude.rep.memType(entryF, i) << ";\n"; + auto name = prelude.rep.memReg(i); + if (prelude.rep.regions->get(entryF, i).isGlobalScope() && + !prelude.rep.isDeadMemoryMap(name)) + numMemoryMaps++; + } + } + for (unsigned i = 0; i < prelude.rep.regions->numSharedRegions(); i++) + if (!prelude.rep.isDeadMemoryMap(prelude.rep.memSharedReg(i))) + numMemoryMaps++; + + describe("Memory maps (" + std::to_string(numMemoryMaps) + " maps)", s); + + if (entryF) { + for (unsigned i = 0; i < numRegions; i++) { + auto name = prelude.rep.memReg(i); + if (prelude.rep.regions->get(entryF, i).isGlobalScope() && + !prelude.rep.isDeadMemoryMap(name)) + s << "var " << name << ": " << prelude.rep.memType(entryF, i) << ";\n"; } } // Shared maps for cross-function memory outside the entry function's // regions. - for (unsigned i = 0; i < prelude.rep.regions->numSharedRegions(); i++) - s << "var " << prelude.rep.memSharedReg(i) << ": " - << prelude.rep.memTypeOf(prelude.rep.regions->getShared(i)) << ";\n"; + for (unsigned i = 0; i < prelude.rep.regions->numSharedRegions(); i++) { + auto name = prelude.rep.memSharedReg(i); + if (!prelude.rep.isDeadMemoryMap(name)) + s << "var " << name << ": " + << prelude.rep.memTypeOf(prelude.rep.regions->getShared(i)) << ";\n"; + } s << "\n"; } diff --git a/lib/smack/SmackModuleGenerator.cpp b/lib/smack/SmackModuleGenerator.cpp index 865d6b7c6..9bafec0f9 100644 --- a/lib/smack/SmackModuleGenerator.cpp +++ b/lib/smack/SmackModuleGenerator.cpp @@ -4,6 +4,7 @@ #define DEBUG_TYPE "smack-mod-gen" #include "smack/SmackModuleGenerator.h" #include "smack/BoogieAst.h" +#include "smack/DSAWrapper.h" #include "smack/Debug.h" #include "smack/Naming.h" #include "smack/Prelude.h" @@ -12,8 +13,118 @@ #include "smack/SmackOptions.h" #include "smack/SmackRep.h" +#include +#include +#include +#include + namespace smack { +namespace { + +using NameCounts = std::map; + +bool isBoogieIdentifierChar(char c) { + unsigned char uc = static_cast(c); + return std::isalnum(uc) || c == '_' || c == '.' || c == '$' || c == '#' || + c == '\'' || c == '~' || c == '^' || c == '?'; +} + +NameCounts countMemoryMapNames(const std::string &text) { + NameCounts counts; + const std::string prefix = Naming::MEMORY + "."; + + for (size_t pos = 0; (pos = text.find(prefix, pos)) != std::string::npos;) { + size_t end = pos + prefix.size(); + if (text.compare(end, 2, "S.") == 0) + end += 2; + + size_t digits = end; + while (end < text.size() && + std::isdigit(static_cast(text[end]))) + end++; + + if (end != digits && + (end == text.size() || !isBoogieIdentifierChar(text[end]))) + counts[text.substr(pos, end - pos)]++; + + pos += prefix.size(); + } + return counts; +} + +NameCounts countMemoryMapNames(const Stmt *stmt) { + std::ostringstream os; + stmt->print(os); + return countMemoryMapNames(os.str()); +} + +void eliminateDeadStaticInitMaps(Program &program, SmackRep &rep) { + std::map candidates; + NameCounts initializerCounts; + + for (auto *decl : program) { + auto *proc = dyn_cast(decl); + if (!proc || proc->getName() != Naming::STATIC_INIT_PROC) + continue; + + for (auto *block : proc->getBlocks()) { + for (auto *stmt : block->getStatements()) { + auto *assign = dyn_cast(stmt); + if (!assign || assign->getLhs().size() != 1) + continue; + + std::ostringstream lhs; + assign->getLhs().front()->print(lhs); + + NameCounts names = countMemoryMapNames(stmt); + if (names.size() != 1 || names.begin()->first != lhs.str()) + continue; + + candidates.emplace(stmt, lhs.str()); + initializerCounts[lhs.str()] += names.begin()->second; + } + } + } + + if (candidates.empty()) + return; + + std::ostringstream os; + program.print(os); + NameCounts allCounts = countMemoryMapNames(os.str()); + std::set deadMaps; + for (const auto &entry : initializerCounts) { + if (allCounts[entry.first] == entry.second) + deadMaps.insert(entry.first); + } + + if (deadMaps.empty()) + return; + + for (auto *decl : program) { + auto *proc = dyn_cast(decl); + if (!proc || proc->getName() != Naming::STATIC_INIT_PROC) + continue; + + for (auto *block : proc->getBlocks()) { + auto &statements = block->getStatements(); + statements.remove_if([&](const Stmt *stmt) { + auto it = candidates.find(stmt); + return it != candidates.end() && deadMaps.count(it->second) != 0; + }); + } + } + + for (const auto &name : deadMaps) + rep.markDeadMemoryMap(name); + + SDEBUG(errs() << "Eliminated " << deadMaps.size() + << " dead static-initializer memory maps.\n"); +} + +} // namespace + llvm::RegisterPass X("smack", "SMACK generator pass"); char SmackModuleGenerator::ID = 0; @@ -24,6 +135,7 @@ SmackModuleGenerator::SmackModuleGenerator() : ModulePass(ID) { void SmackModuleGenerator::getAnalysisUsage(llvm::AnalysisUsage &AU) const { AU.setPreservesAll(); AU.addRequired(); + AU.addRequired(); AU.addRequired(); } @@ -145,6 +257,9 @@ void SmackModuleGenerator::generateProgram(llvm::Module &M) { decls.insert(decls.end(), ds.begin(), ds.end()); decls.insert(decls.end(), rep.getInitFuncs()); + if (getAnalysis().isContextSensitive()) + eliminateDeadStaticInitMaps(*program, rep); + // NOTE we must do this after instruction generation, since we would not // otherwise know how many regions to declare. Prelude prelude(rep); diff --git a/test/c/basic/static_init_dead_maps.c b/test/c/basic/static_init_dead_maps.c new file mode 100644 index 000000000..81701242c --- /dev/null +++ b/test/c/basic/static_init_dead_maps.c @@ -0,0 +1,18 @@ +#include "smack.h" +#include + +// @expect verified +// @checkbpl awk 'index($0, "123456789") { found=1 } END { exit found }' +// @checkbpl grep -q '123456788' + +struct values { + int used; + int unused; +}; + +struct values data = {123456788, 123456789}; + +int main(void) { + assert(data.used == 123456788); + return 0; +} From a7e27200cb3dec548e1a34982843a056b0515c78 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 13 Jul 2026 09:12:03 -0700 Subject: [PATCH 03/12] Keep private memory maps local for SV-COMP --- include/smack/SmackOptions.h | 1 + lib/smack/Regions.cpp | 26 ++++++++++++++++++++------ lib/smack/SmackOptions.cpp | 5 +++++ share/smack/top.py | 3 +++ test/c/basic/svcomp_private_maps.c | 18 ++++++++++++++++++ 5 files changed, 47 insertions(+), 6 deletions(-) create mode 100644 test/c/basic/svcomp_private_maps.c diff --git a/include/smack/SmackOptions.h b/include/smack/SmackOptions.h index b073debbf..5b9eb7e23 100644 --- a/include/smack/SmackOptions.h +++ b/include/smack/SmackOptions.h @@ -28,6 +28,7 @@ class SmackOptions { static const llvm::cl::opt BitPrecisePointers; static const llvm::cl::opt RewriteBitwiseOps; static const llvm::cl::opt NoMemoryRegionSplitting; + static const llvm::cl::opt LocalPrivateMemoryMaps; static const llvm::cl::opt NoByteAccessInference; static const llvm::cl::opt FloatEnabled; static const llvm::cl::opt MemorySafety; diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 5ebf6fe72..ad717f7b4 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -1192,6 +1192,8 @@ void Regions::computeGlobalMemoryMappings(Module &M) { } void Regions::unifySharedRegions(Module &M) { + const bool localPrivateMaps = + SmackOptions::LocalPrivateMemoryMaps && DSA->isContextSensitive(); const Function *entryF = nullptr; for (auto &F : M) { if (!F.isDeclaration() && F.hasName() && @@ -1260,11 +1262,12 @@ void Regions::unifySharedRegions(Module &M) { // two regions in one function: keep threading those maps through calls. // A relation with more than one target cannot be threaded through a single // call argument and is therefore forced onto one shared backing map. + std::map classSize; + for (auto &kv : ids) + classSize[find(kv.second)]++; + std::set classThreaded; { - std::map classSize; - for (auto &kv : ids) - classSize[find(kv.second)]++; std::map, unsigned> multiplicity; for (auto &kv : ids) multiplicity[{find(kv.second), kv.first.first}]++; @@ -1323,6 +1326,13 @@ void Regions::unifySharedRegions(Module &M) { funcRegionVecs[entryF][ce->second].markGlobalScope(); continue; } + // SV-COMP runs Corral with /trackAllVars, which removes the abstraction + // advantage of globals. Keep genuinely private classes local in that mode + // so they do not enlarge Corral's tracked state. + if (localPrivateMaps && classSize[root] == 1 && + funcRegionVecs[F][r].isAllocated() && + !funcRegionVecs[F][r].isGlobalScope()) + continue; // Function-private classes get module-level maps as well: Corral's // variable-tracking abstraction applies to globals only, so an // untracked global map is havoced for free while a procedure-local map @@ -1343,8 +1353,9 @@ void Regions::unifySharedRegions(Module &M) { sharedRegionIndex[{F, r}] = s; } - // Regions never mentioned by any call-site or global mapping get - // module-level maps of their own, preserving the branch's existing policy. + // Regions never mentioned by any call-site or global mapping follow the + // same policy: module-level normally, but procedure-local under SV-COMP + // when they do not contain global objects. for (auto &fr : funcRegions) { const Function *F = fr.first; if (F == entryF) @@ -1359,6 +1370,9 @@ void Regions::unifySharedRegions(Module &M) { auto gm = globalMemoryMappings.find(F); if (gm != globalMemoryMappings.end() && gm->second.count(r)) continue; + if (localPrivateMaps && funcRegionVecs[F][r].isAllocated() && + !funcRegionVecs[F][r].isGlobalScope()) + continue; unsigned s = sharedRegions.size(); sharedRegions.push_back(funcRegionVecs[F][r]); sharedRegionIndex[{F, r}] = s; @@ -1367,7 +1381,7 @@ void Regions::unifySharedRegions(Module &M) { // Preserve the branch's declaration policy: all entry regions are // module-level maps, whether or not the access closure reaches them. - if (entryF) + if (entryF && !localPrivateMaps) for (auto &R : funcRegionVecs[entryF]) R.markGlobalScope(); } diff --git a/lib/smack/SmackOptions.cpp b/lib/smack/SmackOptions.cpp index 3fca4a6f3..cb5c9156a 100644 --- a/lib/smack/SmackOptions.cpp +++ b/lib/smack/SmackOptions.cpp @@ -64,6 +64,11 @@ const llvm::cl::opt SmackOptions::NoMemoryRegionSplitting( "no-memory-splitting", llvm::cl::desc("Disable splitting memory into regions.")); +const llvm::cl::opt SmackOptions::LocalPrivateMemoryMaps( + "local-private-memory-maps", + llvm::cl::desc("Keep function-private memory maps procedure-local."), + llvm::cl::Hidden); + const llvm::cl::opt SmackOptions::NoByteAccessInference( "no-byte-access-inference", llvm::cl::desc("Optimize bit-precision with DSA.")); diff --git a/share/smack/top.py b/share/smack/top.py index 28174e6ee..4dcf5840a 100644 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -764,6 +764,9 @@ def llvm_to_bpl(args): cmd += ['-rewrite-bitwise-ops'] if args.no_memory_splitting: cmd += ['-no-memory-splitting'] + # SV-COMP's Corral configuration tracks every global variable. + if args.language == 'svcomp': + cmd += ['-local-private-memory-maps'] if args.check.contains_mem_safe_props(): cmd += ['-memory-safety'] if VProperty.INTEGER_OVERFLOW in args.check: diff --git a/test/c/basic/svcomp_private_maps.c b/test/c/basic/svcomp_private_maps.c new file mode 100644 index 000000000..1e7e82b18 --- /dev/null +++ b/test/c/basic/svcomp_private_maps.c @@ -0,0 +1,18 @@ +#include "smack.h" +#include + +// @expect verified +// @flag -x svcomp +// @checkbpl grep -q 'var \$M\.L\.' + +static int read_local(int value) { + int local[2]; + local[0] = value; + local[1] = value + 1; + return local[0]; +} + +int main(void) { + assert(read_local(42) == 42); + return 0; +} From 696896c50711ea2debb7b60bf3753dac5b8afcbc Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 13 Jul 2026 09:12:28 -0700 Subject: [PATCH 04/12] Update SeaDsa CS top-down propagation --- sea-dsa | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sea-dsa b/sea-dsa index 78db35706..5a281ac8c 160000 --- a/sea-dsa +++ b/sea-dsa @@ -1 +1 @@ -Subproject commit 78db35706f1bed40758ae47b03b82eac5c5e9d39 +Subproject commit 5a281ac8c818760ba13329b99681ad362615316f From be981603911a0745c46fed05d189b17f534ef115 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 13 Jul 2026 14:49:49 -0700 Subject: [PATCH 05/12] Update SeaDsa cleanup after audit --- sea-dsa | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sea-dsa b/sea-dsa index 5a281ac8c..23cd94a78 160000 --- a/sea-dsa +++ b/sea-dsa @@ -1 +1 @@ -Subproject commit 5a281ac8c818760ba13329b99681ad362615316f +Subproject commit 23cd94a78912b2f12bf058364c89c41d7b2b0a74 From 97fd80341a8fabb2cfff5c25e9c24715d27639bf Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 13 Jul 2026 20:43:50 -0700 Subject: [PATCH 06/12] Fix CS call-site region mapping failures --- lib/smack/Regions.cpp | 31 +++++++++++++++++++++++++++++-- lib/smack/SmackRep.cpp | 18 ++++++++++++++---- 2 files changed, 43 insertions(+), 6 deletions(-) diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index ad717f7b4..fdea72a24 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -411,6 +411,15 @@ bool Regions::runOnModule(Module &M) { computeGlobalMemoryMappings(M); dumpPhase("3.6-globals", funcRegionVecs); + if (SmackOptions::LocalPrivateMemoryMaps && DSA->isContextSensitive()) { + // Compute a preliminary procedure interface before choosing local maps. + // If an interface region lacks a caller counterpart at even one call + // site (for example, a pointer formal receives null), it cannot be + // threaded through one fixed Boogie signature and must be shared. + computeFunctionRegions(M); + computeInterfaceRegions(M); + } + // Phase 3.7: Bind cross-function equivalence classes to entry-owned or // shared module-level maps, except for the small classes retained by the // branch's existing procedure-interface threading policy. @@ -830,7 +839,10 @@ void Regions::computeOneCallSiteMapping(CallBase *CI, const Function *caller, calleeRegion.getType(), calleeRegion.bytewiseAccess(), calleeRegion.getSingletonGlobal(), caller->getContext()); - mapping[i].insert(idx(callerRegion, caller)); + // idx() can merge regions and rebuild this call-site mapping. Complete it + // before looking up mapping[i], or insert() may use an invalidated set. + unsigned callerRegionIndex = idx(callerRegion, caller); + mapping[i].insert(callerRegionIndex); } } @@ -1243,6 +1255,20 @@ void Regions::unifySharedRegions(Module &M) { for (unsigned callerR : m.second) unite(calleeId, id(caller, callerR)); } + + if (localPrivateMaps) { + auto hasCallerMapping = [&](unsigned calleeR) { + auto it = cs.second.find(calleeR); + return it != cs.second.end() && !it->second.empty(); + }; + auto &calleeInfo = funcRegions[callee]; + for (unsigned calleeR : calleeInfo.inputRegions) + if (!hasCallerMapping(calleeR)) + forceSharedIds.push_back(id(callee, calleeR)); + for (unsigned calleeR : calleeInfo.outputRegions) + if (!hasCallerMapping(calleeR)) + forceSharedIds.push_back(id(callee, calleeR)); + } } if (entryF) for (auto &gm : globalMemoryMappings) @@ -1329,7 +1355,8 @@ void Regions::unifySharedRegions(Module &M) { // SV-COMP runs Corral with /trackAllVars, which removes the abstraction // advantage of globals. Keep genuinely private classes local in that mode // so they do not enlarge Corral's tracked state. - if (localPrivateMaps && classSize[root] == 1 && + if (localPrivateMaps && !classNeedsShared.count(root) && + classSize[root] == 1 && funcRegionVecs[F][r].isAllocated() && !funcRegionVecs[F][r].isGlobalScope()) continue; diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 075a4f363..d5119319c 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -1239,11 +1239,21 @@ const Stmt *SmackRep::call(llvm::Function *f, const llvm::User &ci) { auto mapRegion = [&](unsigned calleeR) -> unsigned { auto it = mapping.find(calleeR); - if (it == mapping.end() || it->second.size() != 1) + if (it == mapping.end()) { + std::string callText; + raw_string_ostream callStream(callText); + ci.print(callStream); + callStream.flush(); report_fatal_error( - "missing or non-unique SeaDsa call-site memory-region mapping " - "for call to " + - f->getName()); + "missing SeaDsa call-site memory-region mapping for call to " + + f->getName() + " (callee region " + Twine(calleeR) + "): " + + callText); + } + if (it->second.size() != 1) + report_fatal_error( + "non-unique SeaDsa call-site memory-region mapping for call to " + + f->getName() + " (callee region " + Twine(calleeR) + ", " + + Twine(it->second.size()) + " caller regions)"); return *it->second.begin(); }; From 76d7ad574f1dab8e195767915fb2803db4c5400b Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 13 Jul 2026 20:52:21 -0700 Subject: [PATCH 07/12] Apply clang-format to region fixes --- lib/smack/Regions.cpp | 3 +-- lib/smack/SmackRep.cpp | 4 ++-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index fdea72a24..9cb72dd23 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -1356,8 +1356,7 @@ void Regions::unifySharedRegions(Module &M) { // advantage of globals. Keep genuinely private classes local in that mode // so they do not enlarge Corral's tracked state. if (localPrivateMaps && !classNeedsShared.count(root) && - classSize[root] == 1 && - funcRegionVecs[F][r].isAllocated() && + classSize[root] == 1 && funcRegionVecs[F][r].isAllocated() && !funcRegionVecs[F][r].isGlobalScope()) continue; // Function-private classes get module-level maps as well: Corral's diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index d5119319c..c0959461a 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -1246,8 +1246,8 @@ const Stmt *SmackRep::call(llvm::Function *f, const llvm::User &ci) { callStream.flush(); report_fatal_error( "missing SeaDsa call-site memory-region mapping for call to " + - f->getName() + " (callee region " + Twine(calleeR) + "): " + - callText); + f->getName() + " (callee region " + Twine(calleeR) + + "): " + callText); } if (it->second.size() != 1) report_fatal_error( From 0c5612281388b57c2b361f8c3143d36924aa38d1 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Thu, 16 Jul 2026 18:48:12 -0700 Subject: [PATCH 08/12] Anchor untranslatable init-function cells as ordinary regions Init-function bodies may use memory that is not rooted at any global (a stack array, a call result). Cross-graph translation cannot apply to such values because they are not shared global memory; aborting on them was a regression against the baseline, which anchored them as ordinary regions. idxTranslated now reports no translation for values without an underlying global, letting the caller fall back to an ordinary (unknown) region in the target context. DSAWrapper's translated getNode/getOffset follow the same policy: global-rooted values whose field-sensitive translation fails degrade to the whole target node (matching idxTranslated's conservative fallback) and non-global-rooted values report no node. Co-Authored-By: Claude Fable 5 --- lib/smack/DSAWrapper.cpp | 16 ++++++++++++---- lib/smack/Regions.cpp | 9 ++++++--- test/c/basic/init_func_locals.c | 23 +++++++++++++++++++++++ 3 files changed, 41 insertions(+), 7 deletions(-) create mode 100644 test/c/basic/init_func_locals.c diff --git a/lib/smack/DSAWrapper.cpp b/lib/smack/DSAWrapper.cpp index 038566a53..9d5cd4aad 100644 --- a/lib/smack/DSAWrapper.cpp +++ b/lib/smack/DSAWrapper.cpp @@ -211,8 +211,10 @@ unsigned DSAWrapper::getOffset(const Value *v, const Function &F) { return (unsigned)(rawOff % n->size()); return (unsigned)rawOff; } - report_fatal_error( - "cannot translate a global memory cell between SeaDsa graphs"); + // Values not rooted at a global (e.g., allocas in init functions) are + // not shared global memory; global-rooted values whose field-sensitive + // translation fails fall back to the whole target node at offset zero, + // matching Regions::idxTranslated's conservative fallback. } return 0; } @@ -264,8 +266,14 @@ const seadsa::Node *DSAWrapper::getNode(const Value *v, const Function &F) { seadsa::Cell c; if (translateGlobalCell(v, src, graph, c)) return c.getNode(); - report_fatal_error( - "cannot translate a global memory cell between SeaDsa graphs"); + // Global-rooted values whose field-sensitive translation fails fall + // back to the whole target node, matching Regions::idxTranslated's + // conservative fallback; values not rooted at a global are not shared + // global memory, so report no node and let the caller treat them as an + // unknown region. + const auto *GV = dyn_cast(getUnderlyingObject(v)); + if (GV && graph.hasCell(*GV)) + return graph.getCell(*GV).getNode(); } return nullptr; } diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 9cb72dd23..4c7cce144 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -490,14 +490,17 @@ int Regions::idxTranslated(const Value *V, const Function *F, unsigned length) { // If field-sensitive translation is unavailable, use the entire target // global node. This loses precision but makes every access through that // node share one backing region instead of silently using offset zero. + // Values not rooted at a global (e.g., an alloca or a call result in an + // init function) are not shared global memory at all: report no + // translation so the caller anchors them as an ordinary (unknown) + // region in F's context instead of aborting. const auto *GV = dyn_cast(getUnderlyingObject(V)); if (!GV || !dstG.hasCell(*GV)) - report_fatal_error( - "cannot conservatively translate a global SeaDsa cell"); + return -1; auto dst = dstG.getCell(*GV); auto *node = dst.getNode(); if (!node) - report_fatal_error("global SeaDsa cell has no target node"); + return -1; Region R(node, 0, std::max(node->size(), 1u), nullptr, SmackOptions::BitPrecise, nullptr, V->getContext()); return (int)idx(R, F); diff --git a/test/c/basic/init_func_locals.c b/test/c/basic/init_func_locals.c new file mode 100644 index 000000000..08a6a05da --- /dev/null +++ b/test/c/basic/init_func_locals.c @@ -0,0 +1,23 @@ +#include "smack.h" +#include + +// @expect verified + +// Init functions run in the entry function's memory-region context; their +// bodies may still use memory that is not rooted at any global (here, a +// stack array). Region translation must fall back to an ordinary region +// for such values instead of aborting. + +int g; + +__SMACK_INIT(stack_probe) { + int a[2]; + a[0] = 4; + a[1] = 5; + g = a[0] + a[1]; +} + +int main(void) { + assert(g == 9); + return 0; +} From f3c11d3f0313fc47f2c01b0522233acca8c653d7 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Thu, 16 Jul 2026 18:48:40 -0700 Subject: [PATCH 09/12] Scale the call-site mapping convergence bound with module size Call-site mapping propagates one call-graph level per pass when callers precede callees in module order, so a valid pointer-passing chain deeper than the fixed 100-pass cap aborted translation while the analysis was converging normally. Allow one pass per function plus slack; genuine divergence still aborts. Co-Authored-By: Claude Fable 5 --- lib/smack/Regions.cpp | 11 +- test/c/basic/deep_call_chain.c | 256 +++++++++++++++++++++++++++++++++ 2 files changed, 264 insertions(+), 3 deletions(-) create mode 100644 test/c/basic/deep_call_chain.c diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 4c7cce144..997633157 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -7,6 +7,7 @@ #include "smack/DSAWrapper.h" #include "smack/Debug.h" #include "smack/SmackOptions.h" +#include "llvm/ADT/Twine.h" #include "llvm/Analysis/ValueTracking.h" #include "llvm/IR/GetElementPtrTypeIterator.h" #include "llvm/IR/InstIterator.h" @@ -383,7 +384,11 @@ bool Regions::runOnModule(Module &M) { // merges) so that every mapping reflects the final region numbering; // comparing region counts is not enough since one merge plus one // creation in the same pass cancel out. - const unsigned maxIters = 100; + // Deep pointer-passing call chains propagate one level per pass under + // adverse module order, so the bound must scale with the number of + // functions; a fixed cap aborts on valid deep call chains. + const unsigned maxIters = + std::max(100u, (unsigned)M.getFunctionList().size() + 16); unsigned iter; for (iter = 0; iter < maxIters; iter++) { unsigned version = structuralVersion; @@ -392,8 +397,8 @@ bool Regions::runOnModule(Module &M) { break; } if (iter == maxIters) - report_fatal_error( - "call-site region mappings did not stabilize after 100 passes"); + report_fatal_error("call-site region mappings did not stabilize after " + + Twine(maxIters) + " passes"); mappingsFinal = true; dumpPhase("3-mappings", funcRegionVecs); diff --git a/test/c/basic/deep_call_chain.c b/test/c/basic/deep_call_chain.c new file mode 100644 index 000000000..112a0e7e5 --- /dev/null +++ b/test/c/basic/deep_call_chain.c @@ -0,0 +1,256 @@ +#include "smack.h" +#include + +// @expect verified + +// Pointer-passing call chains deeper than the old fixed 100-pass cap must +// still translate: the Phase-3 bound now scales with the number of +// functions. Callers are defined before callees so call-site mapping +// propagates one level per pass (the adverse order). + +static void f1(int *p); +static void f2(int *p); +static void f3(int *p); +static void f4(int *p); +static void f5(int *p); +static void f6(int *p); +static void f7(int *p); +static void f8(int *p); +static void f9(int *p); +static void f10(int *p); +static void f11(int *p); +static void f12(int *p); +static void f13(int *p); +static void f14(int *p); +static void f15(int *p); +static void f16(int *p); +static void f17(int *p); +static void f18(int *p); +static void f19(int *p); +static void f20(int *p); +static void f21(int *p); +static void f22(int *p); +static void f23(int *p); +static void f24(int *p); +static void f25(int *p); +static void f26(int *p); +static void f27(int *p); +static void f28(int *p); +static void f29(int *p); +static void f30(int *p); +static void f31(int *p); +static void f32(int *p); +static void f33(int *p); +static void f34(int *p); +static void f35(int *p); +static void f36(int *p); +static void f37(int *p); +static void f38(int *p); +static void f39(int *p); +static void f40(int *p); +static void f41(int *p); +static void f42(int *p); +static void f43(int *p); +static void f44(int *p); +static void f45(int *p); +static void f46(int *p); +static void f47(int *p); +static void f48(int *p); +static void f49(int *p); +static void f50(int *p); +static void f51(int *p); +static void f52(int *p); +static void f53(int *p); +static void f54(int *p); +static void f55(int *p); +static void f56(int *p); +static void f57(int *p); +static void f58(int *p); +static void f59(int *p); +static void f60(int *p); +static void f61(int *p); +static void f62(int *p); +static void f63(int *p); +static void f64(int *p); +static void f65(int *p); +static void f66(int *p); +static void f67(int *p); +static void f68(int *p); +static void f69(int *p); +static void f70(int *p); +static void f71(int *p); +static void f72(int *p); +static void f73(int *p); +static void f74(int *p); +static void f75(int *p); +static void f76(int *p); +static void f77(int *p); +static void f78(int *p); +static void f79(int *p); +static void f80(int *p); +static void f81(int *p); +static void f82(int *p); +static void f83(int *p); +static void f84(int *p); +static void f85(int *p); +static void f86(int *p); +static void f87(int *p); +static void f88(int *p); +static void f89(int *p); +static void f90(int *p); +static void f91(int *p); +static void f92(int *p); +static void f93(int *p); +static void f94(int *p); +static void f95(int *p); +static void f96(int *p); +static void f97(int *p); +static void f98(int *p); +static void f99(int *p); +static void f100(int *p); +static void f101(int *p); +static void f102(int *p); +static void f103(int *p); +static void f104(int *p); +static void f105(int *p); +static void f106(int *p); +static void f107(int *p); +static void f108(int *p); +static void f109(int *p); +static void f110(int *p); +static void f111(int *p); +static void f112(int *p); +static void f113(int *p); +static void f114(int *p); +static void f115(int *p); +static void f116(int *p); +static void f117(int *p); +static void f118(int *p); +static void f119(int *p); +static void f120(int *p) { *p = 42; } +static void f1(int *p) { f2(p); } +static void f2(int *p) { f3(p); } +static void f3(int *p) { f4(p); } +static void f4(int *p) { f5(p); } +static void f5(int *p) { f6(p); } +static void f6(int *p) { f7(p); } +static void f7(int *p) { f8(p); } +static void f8(int *p) { f9(p); } +static void f9(int *p) { f10(p); } +static void f10(int *p) { f11(p); } +static void f11(int *p) { f12(p); } +static void f12(int *p) { f13(p); } +static void f13(int *p) { f14(p); } +static void f14(int *p) { f15(p); } +static void f15(int *p) { f16(p); } +static void f16(int *p) { f17(p); } +static void f17(int *p) { f18(p); } +static void f18(int *p) { f19(p); } +static void f19(int *p) { f20(p); } +static void f20(int *p) { f21(p); } +static void f21(int *p) { f22(p); } +static void f22(int *p) { f23(p); } +static void f23(int *p) { f24(p); } +static void f24(int *p) { f25(p); } +static void f25(int *p) { f26(p); } +static void f26(int *p) { f27(p); } +static void f27(int *p) { f28(p); } +static void f28(int *p) { f29(p); } +static void f29(int *p) { f30(p); } +static void f30(int *p) { f31(p); } +static void f31(int *p) { f32(p); } +static void f32(int *p) { f33(p); } +static void f33(int *p) { f34(p); } +static void f34(int *p) { f35(p); } +static void f35(int *p) { f36(p); } +static void f36(int *p) { f37(p); } +static void f37(int *p) { f38(p); } +static void f38(int *p) { f39(p); } +static void f39(int *p) { f40(p); } +static void f40(int *p) { f41(p); } +static void f41(int *p) { f42(p); } +static void f42(int *p) { f43(p); } +static void f43(int *p) { f44(p); } +static void f44(int *p) { f45(p); } +static void f45(int *p) { f46(p); } +static void f46(int *p) { f47(p); } +static void f47(int *p) { f48(p); } +static void f48(int *p) { f49(p); } +static void f49(int *p) { f50(p); } +static void f50(int *p) { f51(p); } +static void f51(int *p) { f52(p); } +static void f52(int *p) { f53(p); } +static void f53(int *p) { f54(p); } +static void f54(int *p) { f55(p); } +static void f55(int *p) { f56(p); } +static void f56(int *p) { f57(p); } +static void f57(int *p) { f58(p); } +static void f58(int *p) { f59(p); } +static void f59(int *p) { f60(p); } +static void f60(int *p) { f61(p); } +static void f61(int *p) { f62(p); } +static void f62(int *p) { f63(p); } +static void f63(int *p) { f64(p); } +static void f64(int *p) { f65(p); } +static void f65(int *p) { f66(p); } +static void f66(int *p) { f67(p); } +static void f67(int *p) { f68(p); } +static void f68(int *p) { f69(p); } +static void f69(int *p) { f70(p); } +static void f70(int *p) { f71(p); } +static void f71(int *p) { f72(p); } +static void f72(int *p) { f73(p); } +static void f73(int *p) { f74(p); } +static void f74(int *p) { f75(p); } +static void f75(int *p) { f76(p); } +static void f76(int *p) { f77(p); } +static void f77(int *p) { f78(p); } +static void f78(int *p) { f79(p); } +static void f79(int *p) { f80(p); } +static void f80(int *p) { f81(p); } +static void f81(int *p) { f82(p); } +static void f82(int *p) { f83(p); } +static void f83(int *p) { f84(p); } +static void f84(int *p) { f85(p); } +static void f85(int *p) { f86(p); } +static void f86(int *p) { f87(p); } +static void f87(int *p) { f88(p); } +static void f88(int *p) { f89(p); } +static void f89(int *p) { f90(p); } +static void f90(int *p) { f91(p); } +static void f91(int *p) { f92(p); } +static void f92(int *p) { f93(p); } +static void f93(int *p) { f94(p); } +static void f94(int *p) { f95(p); } +static void f95(int *p) { f96(p); } +static void f96(int *p) { f97(p); } +static void f97(int *p) { f98(p); } +static void f98(int *p) { f99(p); } +static void f99(int *p) { f100(p); } +static void f100(int *p) { f101(p); } +static void f101(int *p) { f102(p); } +static void f102(int *p) { f103(p); } +static void f103(int *p) { f104(p); } +static void f104(int *p) { f105(p); } +static void f105(int *p) { f106(p); } +static void f106(int *p) { f107(p); } +static void f107(int *p) { f108(p); } +static void f108(int *p) { f109(p); } +static void f109(int *p) { f110(p); } +static void f110(int *p) { f111(p); } +static void f111(int *p) { f112(p); } +static void f112(int *p) { f113(p); } +static void f113(int *p) { f114(p); } +static void f114(int *p) { f115(p); } +static void f115(int *p) { f116(p); } +static void f116(int *p) { f117(p); } +static void f117(int *p) { f118(p); } +static void f118(int *p) { f119(p); } +static void f119(int *p) { f120(p); } + +int main(void) { + int x = 0; + f1(&x); + assert(x == 42); + return 0; +} From 9bea2386bca1d2085ad4f703ef5bb523b6bdb90d Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Thu, 16 Jul 2026 18:49:03 -0700 Subject: [PATCH 10/12] Guard threaded interfaces against unmapped regions in every CS mode The preliminary interface pass and the shared-map fallback for callee interface regions lacking a caller counterpart were gated on the SV-COMP private-map policy, but procedure-interface threading applies in every context-sensitive mode. A threaded region with no mapping at some call site would still reach the missing-mapping translation error in ordinary runs; apply the guard whenever the analysis is context-sensitive. Co-Authored-By: Claude Fable 5 --- lib/smack/Regions.cpp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 997633157..4f58b9831 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -416,11 +416,13 @@ bool Regions::runOnModule(Module &M) { computeGlobalMemoryMappings(M); dumpPhase("3.6-globals", funcRegionVecs); - if (SmackOptions::LocalPrivateMemoryMaps && DSA->isContextSensitive()) { - // Compute a preliminary procedure interface before choosing local maps. - // If an interface region lacks a caller counterpart at even one call - // site (for example, a pointer formal receives null), it cannot be - // threaded through one fixed Boogie signature and must be shared. + if (DSA->isContextSensitive()) { + // Compute a preliminary procedure interface before binding backing + // maps. If an interface region lacks a caller counterpart at even one + // call site (for example, a pointer formal receives null), it cannot + // be threaded through one fixed Boogie signature and must be shared. + // Threading is not specific to the private-map policy, so this guard + // applies in every context-sensitive mode. computeFunctionRegions(M); computeInterfaceRegions(M); } @@ -1264,7 +1266,7 @@ void Regions::unifySharedRegions(Module &M) { unite(calleeId, id(caller, callerR)); } - if (localPrivateMaps) { + if (DSA->isContextSensitive()) { auto hasCallerMapping = [&](unsigned calleeR) { auto it = cs.second.find(calleeR); return it != cs.second.end() && !it->second.empty(); From f3d3ca596822dc9e343dbe8ce007021d6f99805e Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Thu, 16 Jul 2026 18:49:24 -0700 Subject: [PATCH 11/12] Expose the private-map policy as a CLI option and test it non-vacuously Under '-x svcomp' the C assert maps to a bodiless __VERIFIER_assert, so svcomp_private_maps.c's 'verified' expectation could never fail and only its BPL check had teeth. Add --local-private-memory-maps to the smack CLI (the SVCOMP language mode still enables it automatically) and switch the test to the flag with the regular frontend, making its assertion a real verification obligation alongside the local-map BPL check. Co-Authored-By: Claude Fable 5 --- share/smack/top.py | 9 ++++++++- test/c/basic/svcomp_private_maps.c | 6 +++++- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/share/smack/top.py b/share/smack/top.py index 4dcf5840a..8ee941f46 100644 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -411,6 +411,13 @@ def arguments(): default=False, help='disable region-based memory splitting') + translate_group.add_argument( + '--local-private-memory-maps', + action="store_true", + default=False, + help='''keep function-private memory maps procedure-local + (enabled automatically for SV-COMP)''') + translate_group.add_argument( '--mem-mod', choices=[ @@ -765,7 +772,7 @@ def llvm_to_bpl(args): if args.no_memory_splitting: cmd += ['-no-memory-splitting'] # SV-COMP's Corral configuration tracks every global variable. - if args.language == 'svcomp': + if args.language == 'svcomp' or args.local_private_memory_maps: cmd += ['-local-private-memory-maps'] if args.check.contains_mem_safe_props(): cmd += ['-memory-safety'] diff --git a/test/c/basic/svcomp_private_maps.c b/test/c/basic/svcomp_private_maps.c index 1e7e82b18..17d5099dd 100644 --- a/test/c/basic/svcomp_private_maps.c +++ b/test/c/basic/svcomp_private_maps.c @@ -2,9 +2,13 @@ #include // @expect verified -// @flag -x svcomp +// @flag --local-private-memory-maps // @checkbpl grep -q 'var \$M\.L\.' +// Uses the CLI flag rather than -x svcomp so the assertion is actually +// checked: under the SVCOMP language mode, assert maps to a bodiless +// __VERIFIER_assert and the verification verdict is vacuous. + static int read_local(int value) { int local[2]; local[0] = value; From c663534a2ea8a1506d21776f528cf495752008dd Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Thu, 16 Jul 2026 18:49:24 -0700 Subject: [PATCH 12/12] Align the CS memory-plan document with the implementation Document the SV-COMP private-map policy (which skips the blanket module-level promotion of entry regions), the preliminary interface guard, the dead static-initializer map elimination, the scaled convergence bound, and the non-aborting fallbacks for untranslatable cells; the previous text described the pre-policy declaration rules as unchanged. Co-Authored-By: Claude Fable 5 --- docs/cs-dsa-memory-plan.md | 53 ++++++++++++++++++++++++++++++++------ 1 file changed, 45 insertions(+), 8 deletions(-) diff --git a/docs/cs-dsa-memory-plan.md b/docs/cs-dsa-memory-plan.md index 5f3a8da51..c977573bf 100644 --- a/docs/cs-dsa-memory-plan.md +++ b/docs/cs-dsa-memory-plan.md @@ -9,7 +9,10 @@ they are never compared across functions without a SeaDsa mapping. The existing `cs` branch uses a hybrid backing policy. Entry-function regions and larger cross-function classes use module-level maps, while selected small classes are threaded through procedure inputs and outputs. The soundness fixes -below preserve that policy and its map declarations. +below preserve that policy for ordinary runs; under +`-local-private-memory-maps` (enabled automatically for SV-COMP, where Corral +runs with `/trackAllVars`), provably function-private stack/heap regions stay +procedure-local instead (see Backing Maps). ## Soundness Invariants @@ -39,7 +42,10 @@ otherwise disjoint fields. `__SMACK_static_init` and `__SMACK_init_func*` are emitted in the entry function's memory context. Their cells are translated through the identity of the exact underlying global. If exact field translation is unavailable, SMACK -uses a whole-node bytewise region in the entry graph. +uses a whole-node bytewise region in the entry graph. Values in init bodies +that are not rooted at any global (stack arrays, call results) are not shared +global memory; they anchor as ordinary regions in the entry context rather +than aborting translation. ### 2. Direct Access Sets @@ -62,8 +68,9 @@ callee region -> { caller region, ... } ``` The computation runs to a structural fixpoint because mapping a reachable cell -can create or merge caller regions. Failure to converge after 100 passes aborts -translation. +can create or merge caller regions. Deep pointer-passing call chains propagate +one level per pass under adverse module order, so the iteration bound scales +with the number of functions; exceeding it aborts translation. ### 4. Merge Propagation and Normalization @@ -86,14 +93,19 @@ Statically initialized globals retain the branch's conservative map encoding. ### 6. Backing Maps A union-find structure links region pairs through call-site and global -relations. The branch's existing backing policy is retained: +relations. In the default mode: - entry regions keep their module-level declarations; - small classes with two same-function regions and at most eight members can remain threaded through procedure interfaces; - other cross-function classes use entry-owned or shared module-level maps; -- accessed regions outside mapped classes use the existing shared-map - fallback. +- accessed regions outside mapped classes get module-level maps of their own. + +Before backing maps are chosen, a preliminary procedure-interface pass runs in +every context-sensitive mode: a callee interface region that lacks a caller +counterpart at even one call site (for example, a pointer formal receiving +null) cannot be threaded through one fixed Boogie signature and is forced onto +a shared map. Classes containing a non-unique relation are excluded from threading. If a non-threaded class contains several regions from one function, selecting one @@ -101,6 +113,23 @@ of them as its owner would disconnect the others, so that class uses one shared map. This is a representational soundness requirement, not a memory-splitting or map-count optimization. +Under `-local-private-memory-maps` (automatic for `-x svcomp`, where Corral's +`/trackAllVars` removes the abstraction advantage of globals), the policy +changes for provably private memory: singleton classes and unmapped leftover +regions that are allocated (stack/heap) and hold no global stay +procedure-local, and the blanket module-level promotion of entry regions is +skipped. Global-backed, external, unknown, and cross-function regions remain +module-level in both modes. + +### 6a. Dead Static-Initializer Maps + +After translation, `__SMACK_static_init` stores whose target map has no other +occurrence anywhere in the printed program are removed and the map's +declaration is suppressed. The liveness check counts every textual occurrence +of each entry/shared map name over the whole program, so any reference outside +the candidate stores conservatively keeps the map. This runs only under +context-sensitive DSA. + ### 7. Access Closure and Interfaces Callee reads and modifications propagate through every caller target in the @@ -115,9 +144,12 @@ SMACK aborts translation instead of continuing when: - SeaDsa returns a nonfunctional simulation relation that its public lookup API cannot enumerate; - call-site region construction does not converge; -- a required global cell cannot be translated or conservatively represented; - a non-unique relation reaches a code path that requires one owner. +Global-rooted cells whose field-sensitive translation fails degrade to a +whole-node conservative region; cells not rooted at any global are anchored as +ordinary regions in the target context. Neither aborts translation. + These failures are preferable to proving a program against disconnected or incomplete memory state. @@ -125,6 +157,11 @@ incomplete memory state. - `cs_dsa_region_threading.c`: nested heap and pointer flow across calls. - `strings.c` and `strings1.c`: offset-preserving static-initializer mapping. +- `svcomp_private_maps.c`: private regions become procedure-local maps under + `--local-private-memory-maps`, with a checked (non-vacuous) assertion. +- `static_init_dead_maps.c`: unused initializer field maps are eliminated. +- `init_func_locals.c`: init-function bodies using non-global-rooted memory. +- `deep_call_chain.c`: call-site mapping convergence beyond 100 passes. ## Main Files