diff --git a/docs/cs-dsa-memory-plan.md b/docs/cs-dsa-memory-plan.md index 53a7f26d5..c977573bf 100644 --- a/docs/cs-dsa-memory-plan.md +++ b/docs/cs-dsa-memory-plan.md @@ -2,125 +2,171 @@ ## 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 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 + +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. 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 + +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. 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 -## 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. In the default mode: -### 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 get module-level maps of their own. -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. +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. -### Phase 3: Call-Site Mappings +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. -**`computeOneCallSiteMapping(CI, caller, callee)`** builds a map from callee region indices to caller region indices through: +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. -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. +### 6a. Dead Static-Initializer Maps -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. +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. -**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. +### 7. Access Closure and Interfaces -### Phase 3.5: Region Merge Propagation +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. -**`propagateRegionMerges(M)`** enforces the soundness invariant: **regions must not alias**. Uses SCCs for proper ordering. +## Failure Policy -**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. +SMACK aborts translation instead of continuing when: -**Bottom-up pass:** When a callee has collapsed regions that the caller keeps separate, the caller's regions are merged to match. +- 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 non-unique relation reaches a code path that requires one owner. -**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. +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. -### Phase 4: Transitive Closure +These failures are preferable to proving a program against disconnected or +incomplete memory state. -**`computeFunctionRegions(M)`** propagates callee region accesses to callers through call-site mappings until convergence. Only mapped regions are propagated. +## Regression Coverage -### Phase 5: Procedure Memory Interfaces +- `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. -**`computeInterfaceRegions(M)`** separates local memory from caller-visible memory: +## Main Files -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/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 9de9cd34b..7f24bc821 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,17 +61,16 @@ 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. + bool isContextSensitive() const; seadsa::Graph &getGraph(const llvm::Function &F); bool hasGraph(const llvm::Function &F) const; }; 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/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/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 68fdb2af3..9d5cd4aad 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; + } } } } @@ -177,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)) @@ -193,21 +201,21 @@ 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; } + // 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. } - const Value *base = getUnderlyingObject(v); - if (base != v && graph.hasCell(*base)) - return graph.getCell(*base).getOffset(); return 0; } @@ -220,24 +228,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 +263,17 @@ 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; + // 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; } @@ -413,6 +422,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/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/Regions.cpp b/lib/smack/Regions.cpp index 15548b497..4f58b9831 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -7,6 +7,8 @@ #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" #include "llvm/IR/IntrinsicInst.h" @@ -34,11 +36,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 +66,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 +113,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 +123,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 +159,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 +173,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 +194,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; @@ -365,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; @@ -374,10 +397,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 " + + Twine(maxIters) + " passes"); mappingsFinal = true; dumpPhase("3-mappings", funcRegionVecs); @@ -386,11 +407,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 +416,24 @@ 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. + 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); + } + + // 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 +447,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 +492,30 @@ 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. + // 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)) + return -1; + auto dst = dstG.getCell(*GV); + auto *node = dst.getNode(); + if (!node) + return -1; + 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 +822,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 +847,12 @@ 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); + // 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); } } @@ -858,15 +904,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 +950,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 +1070,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,67 +1168,54 @@ 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(); } - } } } 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() && @@ -1220,6 +1248,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 +1258,85 @@ 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 (DSA->isContextSensitive()) { + 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) - 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::map classSize; + for (auto &kv : ids) + classSize[find(kv.second)]++; + std::set classThreaded; { - std::map classSizePre; - for (auto &kv : ids) - classSizePre[find(kv.second)]++; - std::map, unsigned> mult; + 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 +1344,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]); @@ -1304,6 +1362,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 && !classNeedsShared.count(root) && + 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 @@ -1314,6 +1379,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 +1389,9 @@ 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 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) @@ -1340,16 +1406,18 @@ 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; } } - // 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. - if (entryF) + // Preserve the branch's declaration policy: all entry regions are + // module-level maps, whether or not the access closure reaches them. + if (entryF && !localPrivateMaps) for (auto &R : funcRegionVecs[entryF]) R.markGlobalScope(); } @@ -1383,14 +1451,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 +1488,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 +1525,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/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/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/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 7828c35be..c0959461a 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,22 @@ 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()) { + std::string callText; + raw_string_ostream callStream(callText); + ci.print(callStream); + callStream.flush(); report_fatal_error( "missing SeaDsa call-site memory-region mapping for call to " + - f->getName()); - return it->second; + 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(); }; auto &info = regions->getFunctionRegionInfo(f); @@ -1390,21 +1405,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())); } } diff --git a/sea-dsa b/sea-dsa index 78db35706..23cd94a78 160000 --- a/sea-dsa +++ b/sea-dsa @@ -1 +1 @@ -Subproject commit 78db35706f1bed40758ae47b03b82eac5c5e9d39 +Subproject commit 23cd94a78912b2f12bf058364c89c41d7b2b0a74 diff --git a/share/smack/top.py b/share/smack/top.py index 28174e6ee..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=[ @@ -764,6 +771,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' or args.local_private_memory_maps: + 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/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; +} 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; +} 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; +} diff --git a/test/c/basic/svcomp_private_maps.c b/test/c/basic/svcomp_private_maps.c new file mode 100644 index 000000000..17d5099dd --- /dev/null +++ b/test/c/basic/svcomp_private_maps.c @@ -0,0 +1,22 @@ +#include "smack.h" +#include + +// @expect verified +// @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; + local[1] = value + 1; + return local[0]; +} + +int main(void) { + assert(read_local(42) == 42); + return 0; +}