From df73bd91d50fdf07743cab05d920be45e7ecdb7a Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Sun, 29 Mar 2026 21:22:50 -0700 Subject: [PATCH 01/15] Add context-sensitive DSA with per-function memory regions Implement CS-DSA-based per-function region analysis replacing the single global region vector. Each function gets its own region vector computed from its CS graph, with call-site mappings connecting callee regions to caller regions. Key components: - Per-function region vectors in Regions with call-site mappings - DSA link-following to discover heap node correspondences across calls - Top-down and bottom-up region merge propagation for soundness - Phase 1 link-following to pre-create regions for pointer-reachable nodes - Region(Node*) constructor for creating regions from DSA nodes - Parameter mapping priority over global mapping in mergeCalleeRegion - VProperty.__members__ fix for --check memory-safety flag - Index pointer return values from all calls (not just declarations) Co-Authored-By: Claude Opus 4.6 (1M context) --- docs/cs-dsa-memory-plan.md | 362 ++++++++++++ include/smack/DSAWrapper.h | 18 +- include/smack/Regions.h | 83 ++- include/smack/SmackOptions.h | 3 + include/smack/SmackRep.h | 13 +- lib/smack/DSAWrapper.cpp | 178 +++++- lib/smack/Prelude.cpp | 18 +- lib/smack/Regions.cpp | 902 ++++++++++++++++++++++++++--- lib/smack/Slicing.cpp | 2 +- lib/smack/SmackInstGenerator.cpp | 26 +- lib/smack/SmackModuleGenerator.cpp | 41 +- lib/smack/SmackOptions.cpp | 11 + lib/smack/SmackRep.cpp | 97 +++- lib/smack/VectorOperations.cpp | 12 +- share/smack/top.py | 4 +- test/c/basic/malloc_collapsing.c | 1 - 16 files changed, 1607 insertions(+), 164 deletions(-) create mode 100644 docs/cs-dsa-memory-plan.md diff --git a/docs/cs-dsa-memory-plan.md b/docs/cs-dsa-memory-plan.md new file mode 100644 index 000000000..4e439e6c7 --- /dev/null +++ b/docs/cs-dsa-memory-plan.md @@ -0,0 +1,362 @@ +# Plan: Context-Sensitive DSA Memory Regions in SMACK + +## Context + +SMACK currently uses **context-insensitive** sea-dsa analysis (`-sea-dsa=ci`), producing a single global points-to graph for the entire module. All memory regions (`$M.0`, `$M.1`, ...) are declared as **global Boogie variables**, and every procedure implicitly accesses all of them. This means Corral must conservatively havoc all memory regions at each unresolved call site, limiting verification scalability. + +The goal is to switch to **context-sensitive** sea-dsa (`-sea-dsa=cs` or `-sea-dsa=butd-cs`) so each function has its own DSA graph. This enables computing per-function read/write region sets, and threading only the relevant regions through procedure signatures as parameters (reads) and returns (writes). + +**Target Boogie transformation:** +```boogie +// BEFORE (global memory) +var $M.0: [ref]i8; +var $M.1: [ref]i32; + +procedure foo(x: ref) + modifies $M.0; +{ $M.0 := $store.i8($M.0, x, 42); } + +// AFTER (region-parameterized) +procedure foo(x: ref, $M.0: [ref]i8) returns ($M.0: [ref]i8) +{ $M.0 := $store.i8($M.0, x, 42); } + +procedure main() + modifies $M.0, $M.1; +{ call $M.0 := foo(x, $M.0); } +``` + +Non-entry procedures use their regions as **local** in/out parameters. Entry points (`main`) keep using globals with `modifies` clauses. The procedure body code (`$load`/`$store` referencing `$M.R`) does not change -- the trick is that `$M.R` becomes a local variable shadowing the global. + +--- + +## Implementation Steps + +### Step 1: DSAWrapper -- Support Context-Sensitive Analysis + +**Files:** `lib/smack/DSAWrapper.cpp`, `include/smack/DSAWrapper.h` + +1a. **Remove the CI assertion** (line 33-34 of DSAWrapper.cpp): +```cpp +// Remove: +assert(SD->kind() == seadsa::GlobalAnalysisKind::CONTEXT_INSENSITIVE && ...); +``` + +1b. **Make `getNode`/`getOffset` function-aware.** Currently they query the single global graph `DG`. Change them to resolve the function from the value and query the per-function graph: +```cpp +const seadsa::Node *DSAWrapper::getNode(const Value *v) { + auto &graph = getGraphForValue(v); + if (!graph.hasCell(*v)) return nullptr; + return graph.getCell(*v).getNode(); +} + +seadsa::Graph &DSAWrapper::getGraphForValue(const Value *v) { + if (auto *I = dyn_cast(v)) + return SD->getGraph(*I->getParent()->getParent()); + if (auto *A = dyn_cast(v)) + return SD->getGraph(*A->getParent()); + // For globals/constants, use fallback graph + return *DG; +} +``` + +Keep `DG` as a fallback for globals: `DG = &SD->getGraph(*M.begin())` still works (the entry function's graph contains global info). + +1c. **Expose per-function graph access** for the Regions pass: +```cpp +seadsa::Graph &getGraph(const llvm::Function &F) { return SD->getGraph(F); } +bool hasGraph(const llvm::Function &F) const { return SD->hasGraph(F); } +``` + +1d. **Update `collectStaticInits` and `countGlobalRefs`** to handle multiple graphs. Currently these iterate `DG` which is the single graph. With CS mode, iterate all functions' graphs and union results. The simplest approach: keep using `DG` (entry function graph) since globals appear in the entry function's graph in CS mode too. + +--- + +### Step 2: Regions -- Per-Function Read/Write Region Sets + +**Files:** `lib/smack/Regions.cpp`, `include/smack/Regions.h` + +2a. **Add per-function region tracking** to the `Regions` class: +```cpp +// In Regions.h: +struct FunctionRegionInfo { + std::set readRegions; + std::set modifiedRegions; +}; +std::map funcRegions; + +// Public API: +const std::set& getReadRegions(const llvm::Function *F) const; +const std::set& getModifiedRegions(const llvm::Function *F) const; +std::set getAccessedRegions(const llvm::Function *F) const; +``` + +2b. **Compute per-function region sets** after the global `visit(M)` pass in `runOnModule`. Two approaches: + +**Option A (instruction-based):** Iterate each function's instructions, call `idx(ptr_operand)` for each load/store/atomic/memcpy/memset, and classify as read or modified: +```cpp +for (auto &F : M) { + if (F.isDeclaration()) continue; + for (auto &BB : F) { + for (auto &I : BB) { + if (auto *LI = dyn_cast(&I)) { + unsigned r = idx(LI->getPointerOperand()); + funcRegions[&F].readRegions.insert(r); + } else if (auto *SI = dyn_cast(&I)) { + unsigned r = idx(SI->getPointerOperand()); + funcRegions[&F].modifiedRegions.insert(r); + } + // ... atomics, memcpy, memset ... + } + } +} +``` + +**Option B (DSA-graph-based):** For each function, iterate its DSA graph nodes, match nodes to global regions by representative, classify by `node->isRead()`/`node->isModified()`. This automatically includes transitive effects (callees), since the CS graph propagates callee effects. + +**Recommendation:** Use Option A for the direct region mapping (it reuses existing `idx()` logic), then **add transitive closure** by iterating call instructions and unioning callee region sets (post-order on call graph). + +--- + +### Step 3: SmackRep -- Procedure Signatures with Memory Parameters + +**Files:** `lib/smack/SmackRep.cpp`, `include/smack/SmackRep.h` + +3a. **Modify `procedure(Function*, CallInst*)`** (line 1037) to add memory region params/returns for non-entry-point procedures: + +```cpp +// After existing param computation (line 1044-1045): +if (!SmackOptions::isEntryPoint(F->getName()) && !F->isDeclaration()) { + auto accessed = regions->getAccessedRegions(F); + for (unsigned r : accessed) + params.push_back({memReg(r), memType(r)}); // $M.R as input param + + auto modified = regions->getModifiedRegions(F); + for (unsigned r : modified) + rets.push_back({memReg(r), memType(r)}); // $M.R as output return +} +``` + +Note: We use the same name `$M.R` for both param and return, relying on Boogie's scoping (input params and output returns are distinct). Actually, Boogie requires distinct names, so use `$M.R` for input and a differently-scoped return. In Boogie, `returns (x: T)` creates a local `x` that is assigned and returned. So the pattern is: + +```boogie +procedure foo(x: ref, $M.0: [ref]i8) returns (ret: i32, $M.0: [ref]i8) +``` + +Wait -- Boogie does NOT allow the same name for both an input param and an output return. So we need either: +- Use `$M.R` as input param, and a different name like `$M.R.out` for return, with an epilogue copy +- Use `$M.R` as a local variable, `$M.R.in` as input param, `$M.R.out` as output return, with prologue/epilogue copies + +**Recommended approach (local shadow):** +- Input params: `$M.R.in` +- Output returns: `$M.R.out` +- Local variable: `$M.R` (declared as local, initialized from `$M.R.in` at entry, copied to `$M.R.out` at returns) +- Procedure body code continues to reference `$M.R` unchanged + +```cpp +if (!isEntryPoint && !F->isDeclaration()) { + auto accessed = regions->getAccessedRegions(F); + for (unsigned r : accessed) + params.push_back({memReg(r) + ".in", memType(r)}); + + auto modified = regions->getModifiedRegions(F); + for (unsigned r : modified) + rets.push_back({memReg(r) + ".out", memType(r)}); +} +``` + +3b. **Modify `call(Function*, User&)`** (line 1122) to pass and receive memory regions: + +```cpp +// After existing arg computation: +if (!SmackOptions::isEntryPoint(f->getName())) { + auto accessed = regions->getAccessedRegions(f); + for (unsigned r : accessed) + args.push_back(Expr::id(memPath(r))); // pass current $M.R + + auto modified = regions->getModifiedRegions(f); + for (unsigned r : modified) + rets.push_back(memPath(r)); // assign returned $M.R +} +``` + +3c. **Handle declared (external) functions conservatively.** For functions with no body, assume they may access/modify all regions. Add a helper: +```cpp +bool isConservativeFunction(Function *F) { + return F->isDeclaration() && !isSpecialFunction(F); +} +``` + +--- + +### Step 4: SmackInstGenerator -- Prologue/Epilogue for Local Memory Shadows + +**Files:** `lib/smack/SmackInstGenerator.cpp` + +4a. **Patch `visitReturnInst`** (line 240) to copy local memory to output params before returning: + +```cpp +void SmackInstGenerator::visitReturnInst(llvm::ReturnInst &ri) { + processInstruction(ri); + llvm::Value *v = ri.getReturnValue(); + if (v) + emit(Stmt::assign(Expr::id(Naming::RET_VAR), rep->expr(v))); + + // Copy modified regions to output params + const Function *F = ri.getParent()->getParent(); + if (!SmackOptions::isEntryPoint(F->getName())) { + auto modified = rep->getRegions()->getModifiedRegions(F); + for (unsigned r : modified) + emit(Stmt::assign(Expr::id(rep->memReg(r) + ".out"), + Expr::id(rep->memReg(r)))); + } + + emit(Stmt::assign(Expr::id(Naming::EXN_VAR), Expr::lit(false))); + emit(Stmt::return_()); +} +``` + +4b. **Add prologue in entry block** to initialize local shadows from input params. In `SmackInstGenerator`, detect the entry block and emit initialization: + +```cpp +// At the start of visiting the entry block: +if (&bb == &bb.getParent()->getEntryBlock()) { + const Function *F = bb.getParent(); + if (!SmackOptions::isEntryPoint(F->getName())) { + auto accessed = rep->getRegions()->getAccessedRegions(F); + for (unsigned r : accessed) + emit(Stmt::assign(Expr::id(rep->memReg(r)), + Expr::id(rep->memReg(r) + ".in"))); + } +} +``` + +--- + +### Step 5: SmackModuleGenerator -- Local Declarations and Entry-Point Modifies + +**File:** `lib/smack/SmackModuleGenerator.cpp` + +5a. **Add local variable declarations** for memory region shadows in non-entry procedures. After `igen.visit(F)` (line 80), add: + +```cpp +if (!SmackOptions::isEntryPoint(F.getName())) { + auto accessed = getAnalysis().getAccessedRegions(&F); + for (unsigned r : accessed) + P->getDeclarations().push_back( + Decl::variable(rep.memReg(r), rep.memType(r))); +} +``` + +5b. **Add modifies clauses for entry-point procedures** at line 94 (the `// MODIFIES` comment): + +```cpp +if (SmackOptions::isEntryPoint(F.getName())) { + auto modified = getAnalysis().getModifiedRegions(&F); + for (unsigned r : modified) + for (auto P : procs) + P->getModifies().push_back(rep.memReg(r)); +} +``` + +--- + +### Step 6: top.py -- Switch DSA Mode + +**File:** `share/smack/top.py` + +6a. Change line 742 from `-sea-dsa=ci` to `-sea-dsa=cs` (or `butd-cs` for the most precise analysis). + +6b. Optionally add a CLI flag `--context-sensitive-memory` to toggle between old (CI global) and new (CS parameterized) behavior, allowing fallback. Default: enabled. + +--- + +### Step 7: Prelude -- No Changes Needed + +Global `var $M.R: type;` declarations stay. They are used by entry-point procedures and serve as canonical storage. Non-entry procedures shadow them with locals. + +--- + +## Edge Cases + +| Case | Handling | +|------|----------| +| **Indirect calls** (unresolved function pointers) | Pass all regions conservatively (fallback) | +| **Recursive functions** | Sea-dsa CS handles recursion via fixpoint; signature is self-consistent | +| **External/declared functions** | Conservative: assume all regions accessed/modified | +| **Contract expressions** | Already pass all memory maps as params (line 1064-1066); no change needed initially | +| **memcpy/memset** | Already parameterized with memory in/out; called correctly via `SmackInstGenerator::visitMemCpyInst` which uses `rep->memReg(r)` (resolves to local shadow) | +| **Entry points** | Keep using global `$M.R` with `modifies` clauses; no params/returns for memory | +| **Functions accessing no memory** | Empty region sets; no extra params/returns added | + +## Open Problem: Cross-Function Node Identity + +### Problem Statement + +Steps 1-6 were implemented and built successfully. Regression testing (regtest.py) showed **2 failures**: `two_arrays.c` and `two_arrays1.c` (151 passed, 16 failed, 30 unknown). + +Root cause: `Region::overlaps` in Regions.cpp compares DSA node pointers (`representative == R.representative`). With CS-DSA, each function has its own graph with its own node objects. Two functions accessing the same logical memory get different `seadsa::Node*` pointers, so their regions don't merge. + +**Concrete example:** In `two_arrays.c`, `resetArray(int *array)` and `setArray(int *array)` both write through a pointer parameter. With CS-DSA: +- `resetArray`'s `array` parameter → node in `resetArray`'s graph → `$M.0` +- `setArray`'s `array` parameter → node in `setArray`'s graph → `$M.1` +- `main`'s `arrayOne`/`arrayTwo` → node in `main`'s graph → mapped to one of these + +Result: `main` calls `call $M.0 := resetArray(ptr, $M.0)` and `call $M.1 := setArray(ptr, $M.1)`, treating them as separate regions. But they're the same heap memory — `setArray`'s writes don't show up when `main` reads `$M.0`. + +### Candidate Solutions + +**Option A: SimulationMapper-based node canonicalization** +- Sea-dsa provides `SimulationMapper` for computing callee→caller node mappings at call sites +- For each function, map its nodes to the caller's (or entry point's) canonical nodes +- Use the canonical node as `Region::representative` +- Pros: fully leverages CS-DSA precision +- Cons: complex implementation; need to handle the full call graph + +**Option B: Entry-point graph as canonical source** +- Use the entry function's (main) DSA graph for all region computation +- The entry function's graph sees all memory (after bottom-up + top-down propagation in `butd-cs` mode) +- For helper functions, look up their parameter nodes in the caller's graph context +- Pros: simpler — one canonical graph +- Cons: requires `butd-cs` (not just `cs`) for full top-down propagation; still need mapping for function-local values + +**Option C: Separate region identity from access tracking** +- Use CI analysis for region identity (determining which `$M.R` a pointer belongs to) — this is what the current `visit(M)` + `idx()` path already does +- Use CS analysis only for per-function read/write tracking (which global regions a function touches) +- The per-function tracking would query the CS graph's nodes, then map them back to CI regions +- Pros: minimal change to existing region computation; clean separation +- Cons: running two DSA analyses (CI + CS) may be costly; or must find another way to map CS nodes to CI regions + +**Option D: Node identity via allocation sites or types** +- Instead of comparing node pointers, identify nodes by their allocation sites or structural properties +- Sea-dsa nodes have `getAllocSites()` — if two nodes share allocation sites, they represent overlapping memory +- Pros: works across function boundaries without explicit mapping +- Cons: allocation sites may not be available for all nodes (e.g., parameters); may over-merge + +### Decision Needed + +Which approach to pursue? The choice affects: +- Whether we use `-sea-dsa=cs` or `-sea-dsa=butd-cs` +- Whether we need dual CI+CS analysis +- How `Region::overlaps` or `Region::init` must change +- Complexity of the implementation + +## Verification Plan + +1. **Build:** `cd /home/shaobo/smack-project/smack/build && make -j8` +2. **Unit test:** Run existing SMACK regression tests: `make test` (or `lit test/`) +3. **Inspect output:** Run SMACK on a simple test case and inspect the `.bpl` file to verify procedure signatures have memory params/returns, and call sites thread them correctly +4. **AWS benchmarks:** Run `aws.xml` benchmark and compare false alarm counts / correctness against the baseline +5. **DD benchmarks:** Run `dd.xml` and compare verification performance (should improve with tighter modifies sets) + +## Critical Files Summary + +| File | Change | +|------|--------| +| `lib/smack/DSAWrapper.cpp` | Function-aware `getNode`/`getOffset`, remove CI assertion | +| `include/smack/DSAWrapper.h` | Add `getGraph(F)`, `getGraphForValue(v)` | +| `lib/smack/Regions.cpp` | Compute per-function read/modified region sets | +| `include/smack/Regions.h` | Add `FunctionRegionInfo`, query API | +| `lib/smack/SmackRep.cpp` | Add memory params/returns to `procedure()`, thread in `call()` | +| `lib/smack/SmackInstGenerator.cpp` | Prologue/epilogue for local memory shadows | +| `lib/smack/SmackModuleGenerator.cpp` | Local decls, entry-point modifies clauses | +| `share/smack/top.py` | Switch `-sea-dsa=ci` to `-sea-dsa=cs` | diff --git a/include/smack/DSAWrapper.h b/include/smack/DSAWrapper.h index fa3a392de..0b4f6eca6 100644 --- a/include/smack/DSAWrapper.h +++ b/include/smack/DSAWrapper.h @@ -20,11 +20,10 @@ class DSAWrapper : public llvm::ModulePass { private: llvm::Module *module; seadsa::GlobalAnalysis *SD; - // The ds graph since we're using the context-insensitive version which - // results in one graph for the whole module. + // Fallback graph for globals/constants (entry function's graph). seadsa::Graph *DG; std::unordered_set staticInits; - std::unordered_set memOpds; + std::unordered_set memOpds; // Mapping from the DSNodes associated with globals to the numbers of // globals associated with them. std::unordered_map globalRefCount; @@ -34,6 +33,10 @@ class DSAWrapper : public llvm::ModulePass { void collectMemOpds(llvm::Module &M); void countGlobalRefs(); + // Resolve the appropriate DSA graph for a given value based on its + // enclosing function. Falls back to DG for globals/constants. + seadsa::Graph &getGraphForValue(const llvm::Value *v); + public: static char ID; DSAWrapper() : ModulePass(ID) {} @@ -42,14 +45,21 @@ class DSAWrapper : public llvm::ModulePass { virtual bool runOnModule(llvm::Module &M) override; bool isStaticInitd(const seadsa::Node *n); - bool isMemOpd(const seadsa::Node *n); + bool isMemOpd(const llvm::Value *v); bool isRead(const llvm::Value *V); bool isSingletonGlobal(const llvm::Value *V); unsigned getPointedTypeSize(const llvm::Value *v); unsigned getOffset(const llvm::Value *v); + unsigned getOffset(const llvm::Value *v, const llvm::Function &F); const seadsa::Node *getNode(const llvm::Value *v); + const seadsa::Node *getNode(const llvm::Value *v, const llvm::Function &F); bool isTypeSafe(const llvm::Value *v); + bool isTypeSafe(const llvm::Value *v, const llvm::Function &F); unsigned getNumGlobals(const seadsa::Node *n); + + // Per-function graph access for context-sensitive analysis. + seadsa::Graph &getGraph(const llvm::Function &F); + bool hasGraph(const llvm::Function &F) const; }; } // namespace smack diff --git a/include/smack/Regions.h b/include/smack/Regions.h index a0bb5e82b..5952368ca 100644 --- a/include/smack/Regions.h +++ b/include/smack/Regions.h @@ -8,6 +8,9 @@ #include "llvm/IR/InstVisitor.h" #include "llvm/Pass.h" +#include +#include + using namespace llvm; namespace llvm { @@ -32,20 +35,23 @@ class Region { bool incomplete; bool complicated; bool collapsed; + bool globalScope; static const DataLayout *DL; static DSAWrapper *DSA; - static bool isSingleton(const llvm::Value *v, unsigned length); + static bool isSingleton(const llvm::Value *v, unsigned length, + const llvm::Function *F); static bool isAllocated(const seadsa::Node *N); static bool isComplicated(const seadsa::Node *N); - void init(const Value *V, unsigned length); + void init(const Value *V, unsigned length, const llvm::Function *F); bool isDisjoint(unsigned offset, unsigned length); public: - Region(const Value *V); - Region(const Value *V, unsigned length); + Region(const Value *V, const llvm::Function *F); + Region(const Value *V, const llvm::Function *F, unsigned length); + Region(const seadsa::Node *node, LLVMContext &ctx); static void init(Module &M, Pass &P); @@ -55,15 +61,54 @@ class Region { bool isSingleton() const { return singleton; }; bool isAllocated() const { return allocated; }; bool bytewiseAccess() const { return bytewise; } + bool isGlobalScope() const { return globalScope; } const Type *getType() const { return type; } + const seadsa::Node *getRepresentative() const { return representative; } void print(raw_ostream &); }; +struct FunctionRegionInfo { + std::set readRegions; + std::set modifiedRegions; +}; + class Regions : public ModulePass, public InstVisitor { private: - std::vector regions; - unsigned idx(Region &R); + // Per-function region vectors (each function has its own local numbering). + std::map> funcRegionVecs; + + // 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; + + // For non-entry usesGlobalMemory functions: mapping from their region + // indices to the entry function's region indices (matched via globals). + std::map> + globalMemoryMappings; + + static FunctionRegionInfo emptyRegionInfo; + + // The function currently being visited (set during visit phase). + const llvm::Function *currentFunction = nullptr; + + // DSAWrapper pointer cached during runOnModule. + DSAWrapper *DSA = nullptr; + + // Per-function idx: find or create a region in F's vector. + unsigned idx(Region &R, const llvm::Function *F); + + void computeCallSiteMappings(llvm::Module &M); + void computeOneCallSiteMapping(llvm::CallInst *CI, + const llvm::Function *caller, + llvm::Function *callee); + void propagateRegionMerges(llvm::Module &M); + bool mergeCalleeRegion(const llvm::Function *F, unsigned keep, unsigned remove); + void computeGlobalMemoryMappings(llvm::Module &M); + void computeFunctionRegions(llvm::Module &M); public: static char ID; @@ -71,19 +116,19 @@ class Regions : public ModulePass, public InstVisitor { virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const override; virtual bool runOnModule(llvm::Module &M) override; - unsigned size() const; - unsigned idx(const llvm::Value *v); - unsigned idx(const llvm::Value *v, unsigned length); - Region &get(unsigned R); - - // void visitModule(Module& M) { - // for (const GlobalValue& G : M.globals()) - // collect(&G); - // } - - // void visitAllocaInst(AllocaInst& I) { - // getRegion(&I); - // } + // Per-function region access. + unsigned size(const llvm::Function *F) const; + unsigned idx(const llvm::Value *v, const llvm::Function *F); + unsigned idx(const llvm::Value *v, const llvm::Function *F, unsigned length); + Region &get(const llvm::Function *F, unsigned R); + + const FunctionRegionInfo & + getFunctionRegionInfo(const llvm::Function *F) const; + std::set getAccessedRegions(const llvm::Function *F) const; + const std::map & + getCallSiteMapping(const llvm::CallInst *CI) const; + const std::map & + getGlobalMemoryMapping(const llvm::Function *F) const; void visitLoadInst(LoadInst &); void visitStoreInst(StoreInst &); diff --git a/include/smack/SmackOptions.h b/include/smack/SmackOptions.h index 29293360c..b073debbf 100644 --- a/include/smack/SmackOptions.h +++ b/include/smack/SmackOptions.h @@ -39,6 +39,9 @@ class SmackOptions { static const llvm::cl::opt WrappedIntegerEncoding; static bool isEntryPoint(llvm::StringRef); + // Returns true for functions that should use global memory (not parameterized + // regions) — entry points and init functions. + static bool usesGlobalMemory(llvm::StringRef); static bool shouldCheckFunction(llvm::StringRef); }; } // namespace smack diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index a01247ab1..1ee83acb4 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -59,8 +59,14 @@ class SmackRep { std::map auxDecls; public: + // Current function being processed (set by SmackModuleGenerator). + const llvm::Function *currentFunction = nullptr; + // Entry-point function (set by SmackModuleGenerator, used for global decls). + const llvm::Function *entryFunction = nullptr; + SmackRep(const llvm::DataLayout *L, Naming *N, Program *P, Regions *R); Program *getProgram() { return program; } + Regions *getRegions() { return regions; } private: unsigned storageSize(llvm::Type *T); @@ -185,11 +191,12 @@ class SmackRep { unsigned getElementSize(const llvm::Value *v); std::string memReg(unsigned i); - std::string memType(unsigned region); + std::string memType(const llvm::Function *F, unsigned region); std::string memPath(unsigned region); - std::string memPath(const llvm::Value *v); + std::string memPath(const llvm::Value *v, const llvm::Function *F); - std::list> memoryMaps(); + std::list> + memoryMaps(const llvm::Function *F); // used in SmackInstGenerator std::string getString(const llvm::Value *v); diff --git a/lib/smack/DSAWrapper.cpp b/lib/smack/DSAWrapper.cpp index 2968fc1e1..e155a2881 100644 --- a/lib/smack/DSAWrapper.cpp +++ b/lib/smack/DSAWrapper.cpp @@ -9,6 +9,7 @@ #include "smack/Debug.h" #include "smack/InitializePasses.h" #include "smack/SmackOptions.h" +#include "llvm/Analysis/ValueTracking.h" #include "llvm/IR/InstIterator.h" #include "llvm/IR/IntrinsicInst.h" #include "llvm/Support/FileSystem.h" @@ -30,9 +31,28 @@ void DSAWrapper::getAnalysisUsage(llvm::AnalysisUsage &AU) const { bool DSAWrapper::runOnModule(llvm::Module &M) { dataLayout = &M.getDataLayout(); SD = &getAnalysis().getDsaAnalysis(); - assert(SD->kind() == seadsa::GlobalAnalysisKind::CONTEXT_INSENSITIVE && - "Currently we only want the context-insensitive sea-dsa."); - DG = &SD->getGraph(*M.begin()); + // Use the entry-point function's graph as the fallback graph for + // globals/constants. This must match SmackModuleGenerator's entryFunction + // so that globalRefCount (built from DG) uses the same nodes as the + // entry function's region representatives. + Function *entryFn = nullptr; + for (auto &F : M) { + if (!F.isDeclaration() && SmackOptions::isEntryPoint(F.getName())) { + entryFn = &F; + break; + } + } + if (!entryFn) { + // Fallback: use the first defined function. + for (auto &F : M) { + if (!F.isDeclaration()) { + entryFn = &F; + break; + } + } + } + assert(entryFn && "Module must have at least one defined function."); + DG = &SD->getGraph(*entryFn); // Print the graph in dot format when debugging SDEBUG(DG->writeGraph("main.mem.dot")); collectStaticInits(M); @@ -57,10 +77,10 @@ void DSAWrapper::collectMemOpds(llvm::Module &M) { for (auto &f : M) { for (inst_iterator I = inst_begin(&f), E = inst_end(&f); I != E; ++I) { if (MemCpyInst *memcpyInst = dyn_cast(&*I)) { - memOpds.insert(getNode(memcpyInst->getSource())); - memOpds.insert(getNode(memcpyInst->getDest())); + memOpds.insert(memcpyInst->getSource()); + memOpds.insert(memcpyInst->getDest()); } else if (MemSetInst *memsetInst = dyn_cast(&*I)) - memOpds.insert(getNode(memsetInst->getDest())); + memOpds.insert(memsetInst->getDest()); } } } @@ -81,14 +101,26 @@ bool DSAWrapper::isStaticInitd(const seadsa::Node *n) { return staticInits.count(n) > 0; } -bool DSAWrapper::isMemOpd(const seadsa::Node *n) { - return memOpds.count(n) > 0; -} +bool DSAWrapper::isMemOpd(const llvm::Value *v) { return memOpds.count(v) > 0; } bool DSAWrapper::isRead(const Value *V) { + // Check if the value is read in any function's graph (conservative). + // This is needed for CS-DSA where different functions have different graphs. + for (auto &F : *module) { + if (F.isDeclaration() || !SD->hasGraph(F)) + continue; + auto &graph = SD->getGraph(F); + if (graph.hasCell(*V)) { + auto *node = graph.getCell(*V).getNode(); + if (node && node->isRead()) + return true; + } + } + // Fallback: check the default graph. auto node = getNode(V); - assert(node && "Global values should have nodes."); - return node->isRead(); + if (node) + return node->isRead(); + return false; } unsigned DSAWrapper::getPointedTypeSize(const Value *v) { @@ -102,22 +134,75 @@ unsigned DSAWrapper::getPointedTypeSize(const Value *v) { llvm_unreachable("Type should be pointer."); } +seadsa::Graph &DSAWrapper::getGraphForValue(const Value *v) { + if (auto *I = dyn_cast(v)) + if (SD->hasGraph(*I->getParent()->getParent())) + return SD->getGraph(*I->getParent()->getParent()); + if (auto *A = dyn_cast(v)) + if (SD->hasGraph(*A->getParent())) + return SD->getGraph(*A->getParent()); + // For globals/constants or when no per-function graph, use fallback. + return *DG; +} + +seadsa::Graph &DSAWrapper::getGraph(const Function &F) { + return SD->getGraph(F); +} + +bool DSAWrapper::hasGraph(const Function &F) const { return SD->hasGraph(F); } + unsigned DSAWrapper::getOffset(const Value *v) { - if (!DG->hasCell(*v)) + auto &graph = getGraphForValue(v); + if (!graph.hasCell(*v)) return 0; - return DG->getCell(*v).getOffset(); + return graph.getCell(*v).getOffset(); +} + +unsigned DSAWrapper::getOffset(const Value *v, const Function &F) { + if (!SD->hasGraph(F)) + return getOffset(v); + auto &graph = SD->getGraph(F); + if (graph.hasCell(*v)) + return graph.getCell(*v).getOffset(); + // V might be from a different function (e.g., a GEP in __SMACK_static_init + // when we're resolving in the entry function's context). Strip to the + // underlying object (the global variable) and look that up instead. + const Value *base = getUnderlyingObject(v); + if (base != v && graph.hasCell(*base)) + return graph.getCell(*base).getOffset(); + return 0; } const seadsa::Node *DSAWrapper::getNode(const Value *v) { - // For sea-dsa, a node is obtained by getting the cell first. - // It's possible that a value doesn't have a cell, e.g., undef. - if (!DG->hasCell(*v)) + auto &graph = getGraphForValue(v); + if (!graph.hasCell(*v)) return nullptr; - auto node = DG->getCell(*v).getNode(); + auto node = graph.getCell(*v).getNode(); assert(node && "Values should have nodes if they have cells."); return node; } +const seadsa::Node *DSAWrapper::getNode(const Value *v, const Function &F) { + if (!SD->hasGraph(F)) + return getNode(v); + auto &graph = SD->getGraph(F); + if (graph.hasCell(*v)) { + auto node = graph.getCell(*v).getNode(); + assert(node && "Values should have nodes if they have cells."); + return node; + } + // V might be from a different function (e.g., a GEP in __SMACK_static_init + // when we're resolving in the entry function's context). Strip to the + // underlying object (the global variable) and look that up instead. + 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; + } + return nullptr; +} + bool DSAWrapper::isTypeSafe(const Value *v) { typedef std::unordered_map FieldMap; typedef std::unordered_map NodeMap; @@ -127,7 +212,7 @@ bool DSAWrapper::isTypeSafe(const Value *v) { if (node->isOffsetCollapsed() || node->isExternal() || node->isIncomplete() || node->isUnknown() || node->isIntToPtr() || node->isPtrToInt() || - isMemOpd(node)) + isMemOpd(v)) // We consider it type-unsafe to be safe for these cases return false; @@ -196,6 +281,63 @@ bool DSAWrapper::isTypeSafe(const Value *v) { return false; } +bool DSAWrapper::isTypeSafe(const Value *v, const Function &F) { + typedef std::unordered_map FieldMap; + typedef std::unordered_map NodeMap; + static NodeMap nodeMap; + + auto node = getNode(v, F); + if (!node) + return false; + + if (node->isOffsetCollapsed() || node->isExternal() || node->isIncomplete() || + node->isUnknown() || node->isIntToPtr() || node->isPtrToInt() || + isMemOpd(v)) + return false; + + if (!nodeMap.count(node)) { + FieldMap fieldMap; + auto &types = node->types(); + std::set offsets; + for (auto &t : types) + offsets.insert(t.first); + auto offsetIterator = offsets.begin(); + while (true) { + if (offsetIterator == offsets.end()) + break; + unsigned offset = *offsetIterator; + auto &typeSet = types.find(offset)->second; + auto ti = typeSet.begin(); + if (++ti != typeSet.end()) + fieldMap[offset] = false; + unsigned fieldLength = 0; + for (auto &t : typeSet) { + unsigned length = + dataLayout->getTypeStoreSize(const_cast(t)); + if (length > fieldLength) + fieldLength = length; + } + for (auto oi = ++offsetIterator; oi != offsets.end(); ++oi) { + unsigned next_offset = *oi; + if (offset + fieldLength > next_offset) { + fieldMap[offset] = false; + fieldMap[next_offset] = false; + } else + break; + } + if (!fieldMap.count(offset)) + fieldMap[offset] = true; + } + nodeMap[node] = fieldMap; + } + + auto offset = getOffset(v, F); + if (nodeMap[node].count(offset)) + return nodeMap[node][offset]; + else + return false; +} + unsigned DSAWrapper::getNumGlobals(const seadsa::Node *n) { if (globalRefCount.count(n)) return globalRefCount[n]; diff --git a/lib/smack/Prelude.cpp b/lib/smack/Prelude.cpp index deb5891c1..7b3c22be1 100644 --- a/lib/smack/Prelude.cpp +++ b/lib/smack/Prelude.cpp @@ -1114,13 +1114,17 @@ void ConstDeclGen::generate(std::stringstream &s) const { } void MemDeclGen::generateMemoryMaps(std::stringstream &s) const { - describe("Memory maps (" + std::to_string(prelude.rep.regions->size()) + - " regions)", - s); - - for (auto M : prelude.rep.memoryMaps()) - s << "var " << M.first << ": " << M.second << ";" - << "\n"; + auto *entryF = prelude.rep.entryFunction; + unsigned numRegions = entryF ? prelude.rep.regions->size(entryF) : 0; + describe("Memory maps (" + std::to_string(numRegions) + " regions)", s); + + 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"; + } + } s << "\n"; } diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 12602aefd..657b5bb8a 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -6,6 +6,8 @@ #include "smack/Debug.h" #include "smack/SmackOptions.h" #include "llvm/IR/GetElementPtrTypeIterator.h" +#include "llvm/IR/InstIterator.h" +#include "llvm/IR/IntrinsicInst.h" #define DEBUG_TYPE "regions" @@ -19,12 +21,18 @@ void Region::init(Module &M, Pass &P) { DSA = &P.getAnalysis(); } -bool Region::isSingleton(const Value *v, unsigned length) { +bool Region::isSingleton(const Value *v, unsigned length, const Function *F) { // TODO can we do something for non-global nodes? - auto node = DSA->getNode(v); + auto node = F ? DSA->getNode(v, *F) : DSA->getNode(v); - return !isAllocated(node) && DSA->getNumGlobals(node) == 1 && - !node->isArray() && DSA->isTypeSafe(v) && !DSA->isMemOpd(node); + 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); } bool Region::isAllocated(const seadsa::Node *N) { @@ -36,34 +44,60 @@ bool Region::isComplicated(const seadsa::Node *N) { N->isUnknown(); } -void Region::init(const Value *V, unsigned length) { +void Region::init(const Value *V, unsigned length, const Function *F) { Type *T = V->getType(); assert(T->isPointerTy() && "Expected pointer argument."); T = T->getPointerElementType(); context = &V->getContext(); - representative = - (DSA && !dyn_cast(V)) ? DSA->getNode(V) : nullptr; + representative = (DSA && !dyn_cast(V)) + ? (F ? DSA->getNode(V, *F) : DSA->getNode(V)) + : nullptr; this->type = T; - this->offset = DSA ? DSA->getOffset(V) : 0; + this->offset = DSA ? (F ? DSA->getOffset(V, *F) : DSA->getOffset(V)) : 0; this->length = length; - singleton = DL && representative && isSingleton(V, length); + singleton = DL && representative && isSingleton(V, length, F); allocated = !representative || isAllocated(representative); bytewise = DSA && SmackOptions::BitPrecise && (SmackOptions::NoByteAccessInference || - (!representative || !DSA->isTypeSafe(V)) || T->isIntegerTy(8)); + (!representative || + !(F ? DSA->isTypeSafe(V, *F) : DSA->isTypeSafe(V))) || + T->isIntegerTy(8)); incomplete = !representative || representative->isIncomplete(); complicated = !representative || isComplicated(representative); collapsed = !representative || representative->isOffsetCollapsed(); + + // A region is global-scope if it backs global variables, which are + // accessed by multiple global-memory functions (entry points, + // __SMACK_static_init, __SMACK_init_func*). All other regions + // (stack allocas, heap) are local to their function. + globalScope = !representative || DSA->getNumGlobals(representative) > 0; } -Region::Region(const Value *V) { +Region::Region(const Value *V, const Function *F) { unsigned length = DSA ? DSA->getPointedTypeSize(V) : std::numeric_limits::max(); - init(V, length); + init(V, length, F); } -Region::Region(const Value *V, unsigned length) { init(V, length); } +Region::Region(const Value *V, const Function *F, unsigned length) { + init(V, length, F); +} + +Region::Region(const seadsa::Node *node, LLVMContext &ctx) { + context = &ctx; + representative = node; + type = nullptr; + offset = 0; + length = node ? node->size() : std::numeric_limits::max(); + singleton = false; + allocated = !representative || isAllocated(representative); + bytewise = true; + incomplete = !representative || representative->isIncomplete(); + complicated = !representative || isComplicated(representative); + collapsed = !representative || representative->isOffsetCollapsed(); + globalScope = !representative || DSA->getNumGlobals(representative) > 0; +} bool Region::isDisjoint(unsigned offset, unsigned length) { return this->offset + this->length <= offset || @@ -82,6 +116,7 @@ void Region::merge(Region &R) { incomplete = incomplete || R.incomplete; complicated = complicated || R.complicated; collapsed = collapsed || R.collapsed; + globalScope = globalScope || R.globalScope; type = (bytewise || collapse) ? NULL : type; } @@ -124,61 +159,185 @@ void Regions::getAnalysisUsage(llvm::AnalysisUsage &AU) const { } bool Regions::runOnModule(Module &M) { - // Shaobo: my understanding of how this class works: - // First, a bunch of instructions involving pointers are visited (via - // Regions::idx). During a visit on an instruction, a region is created - // (Region::init) for the pointer operand. Note that a region is always - // created for a pointer when it's visited, regardless of whether it alias - // with the existing ones. A region can be roughly seen as a tuple of (cell, - // length) or (node, offset, length) since a cell is essentially a tuple of - // (node, offset). After a region is created, we will merge it to the existing - // ones if it overlaps with the them. So after this pass, we will get a bunch - // of regions which are mutually exclusive to each other. - // After that, SmackRep will call Regions::idx to get the region for a pointer - // operand, which repeats the aforementioned process. Note that we don't have - // fancy caching, so a region is created and merged everytime Regions::idx - // is called. if (!SmackOptions::NoMemoryRegionSplitting) { Region::init(M, *this); - visit(M); + DSA = &getAnalysis(); + + // Phase 1: Build per-function regions from each function's instructions. + // Each function gets its own region vector computed from its own CS graph. + // Also visit formal params and call-site actual args so that call-site + // mapping (Phase 3) doesn't create new regions or alter indices. + for (auto &F : M) { + if (F.isDeclaration()) + continue; + // Visit formal pointer parameters. + for (auto &A : F.args()) + if (A.getType()->isPointerTy()) + idx(&A, &F); + // Visit all instructions. + currentFunction = &F; + visit(const_cast(F)); + } + currentFunction = nullptr; + // Visit actual pointer arguments at call sites (in the caller's context). + for (auto &F : M) { + if (F.isDeclaration()) + continue; + for (auto &BB : F) { + for (auto &I : BB) { + if (auto *CI = dyn_cast(&I)) { + for (unsigned i = 0; i < CI->getNumArgOperands(); i++) { + Value *arg = CI->getArgOperand(i); + if (arg->getType()->isPointerTy()) + idx(arg, &F); + } + } + } + } + } + // Visit globals in each function's context that accesses them. + for (auto &F : M) { + if (F.isDeclaration()) + continue; + if (!DSA->hasGraph(F)) + continue; + auto &graph = DSA->getGraph(F); + for (auto &GV : M.globals()) { + if (GV.getType()->isPointerTy() && graph.hasCell(GV)) + idx(&GV, &F); + } + } + + // Create regions for all DSA nodes reachable through pointer links + // from existing regions. This ensures callers have regions for data + // accessible through pointer indirection (e.g., **arg), which their + // callees may access. Without this, call-site mappings would be + // incomplete and regions that should be distinct would be merged. + for (auto &F : M) { + if (F.isDeclaration() || !DSA->hasGraph(F)) + continue; + bool grew = true; + while (grew) { + grew = false; + auto ®ions = funcRegionVecs[&F]; + std::set existing; + for (auto &r : regions) + if (r.getRepresentative()) + existing.insert(r.getRepresentative()); + unsigned origSize = regions.size(); + for (unsigned i = 0; i < origSize; i++) { + auto *rep = regions[i].getRepresentative(); + if (!rep) + continue; + for (auto &link : rep->links()) { + auto *target = link.second->getNode(); + if (target && !existing.count(target)) { + existing.insert(target); + Region R(target, F.getContext()); + idx(R, &F); + grew = true; + } + } + } + } + } + + // Phase 2: Compute per-function read/write sets (direct accesses). + for (auto &F : M) { + if (F.isDeclaration()) + continue; + FunctionRegionInfo &info = funcRegions[&F]; + for (inst_iterator I = inst_begin(&F), E = inst_end(&F); I != E; ++I) { + if (auto *LI = dyn_cast(&*I)) { + info.readRegions.insert(idx(LI->getPointerOperand(), &F)); + } else if (auto *SI = dyn_cast(&*I)) { + info.modifiedRegions.insert(idx(SI->getPointerOperand(), &F)); + } else if (auto *AI = dyn_cast(&*I)) { + unsigned r = idx(AI->getPointerOperand(), &F); + info.readRegions.insert(r); + info.modifiedRegions.insert(r); + } else if (auto *AI = dyn_cast(&*I)) { + unsigned r = idx(AI->getPointerOperand(), &F); + info.readRegions.insert(r); + info.modifiedRegions.insert(r); + } else if (auto *MSI = dyn_cast(&*I)) { + unsigned length; + if (auto CI = dyn_cast(MSI->getLength())) + length = CI->getZExtValue(); + else + length = std::numeric_limits::max(); + info.modifiedRegions.insert(idx(MSI->getDest(), &F, length)); + } else if (auto *MTI = dyn_cast(&*I)) { + unsigned length; + if (auto CI = dyn_cast(MTI->getLength())) + length = CI->getZExtValue(); + else + length = std::numeric_limits::max(); + info.readRegions.insert(idx(MTI->getSource(), &F, length)); + info.modifiedRegions.insert(idx(MTI->getDest(), &F, length)); + } + } + } + + // Phase 2.5: Compute global-memory mappings for non-entry usesGlobalMemory + // functions (e.g., __SMACK_static_init) to the entry function's indices. + computeGlobalMemoryMappings(M); + + // Phase 3: Compute call-site mappings (callee region -> caller region). + // Iterate because link-following may create new regions in callers, + // which then need mappings computed for their own callers. + for (int iter = 0; iter < 10; iter++) { + unsigned prevTotal = 0; + for (auto &kv : funcRegionVecs) + prevTotal += kv.second.size(); + computeCallSiteMappings(M); + unsigned newTotal = 0; + for (auto &kv : funcRegionVecs) + newTotal += kv.second.size(); + if (newTotal == prevTotal) + break; + } + + // Phase 3.5: Propagate region merges top-down through the call graph. + // When a caller collapses two callee regions (maps both to the same + // caller region), the callee must merge them to preserve the invariant + // that regions never alias. + propagateRegionMerges(M); + + // Phase 4: Transitive closure of region access sets. + computeFunctionRegions(M); } return false; } -unsigned Regions::size() const { return regions.size(); } +unsigned Regions::size(const Function *F) const { + auto it = funcRegionVecs.find(F); + if (it != funcRegionVecs.end()) + return it->second.size(); + return 0; +} -Region &Regions::get(unsigned R) { return regions[R]; } +Region &Regions::get(const Function *F, unsigned R) { + return funcRegionVecs[F][R]; +} -unsigned Regions::idx(const Value *V) { - SDEBUG(errs() << "[regions] for: " << *V << "\n"; auto U = V; - while (U && !isa(U) && !U->use_empty()) U = - U->user_back(); - if (auto I = dyn_cast(U)) { - auto F = I->getParent()->getParent(); - if (I != V) - errs() << " at instruction: " << *I << "\n"; - errs() << " in function: " << F->getName() << "\n"; - }); - Region R(V); - return idx(R); +unsigned Regions::idx(const Value *V, const Function *F) { + SDEBUG(errs() << "[regions] for: " << *V << " in function: " << F->getName() + << "\n"); + Region R(V, F); + return idx(R, F); } -unsigned Regions::idx(const Value *V, unsigned length) { - SDEBUG(errs() << "[regions] for: " << *V << " with length " << length << "\n"; - auto U = V; while (U && !isa(U) && !U->use_empty()) U = - U->user_back(); - if (auto I = dyn_cast(U)) { - auto F = I->getParent()->getParent(); - if (I != V) - errs() << " at instruction: " << *I << "\n"; - errs() << " in function: " << F->getName() << "\n"; - }); - Region R(V, length); - return idx(R); +unsigned Regions::idx(const Value *V, const Function *F, unsigned length) { + SDEBUG(errs() << "[regions] for: " << *V << " with length " << length + << " in function: " << F->getName() << "\n"); + Region R(V, F, length); + return idx(R, F); } -unsigned Regions::idx(Region &R) { +unsigned Regions::idx(Region &R, const Function *F) { + auto ®ions = funcRegionVecs[F]; unsigned r; SDEBUG(errs() << "[regions] using region: "); @@ -206,8 +365,8 @@ unsigned Regions::idx(Region &R) { regions.emplace_back(R); else { - // Here is the tricky part: in case R was merged with an existing region, - // we must now also merge any other region which intersects with R. + // In case R was merged with an existing region, we must now also merge + // any other region which intersects with R. unsigned q = r + 1; while (q < regions.size()) { if (regions[r].overlaps(regions[q])) { @@ -235,19 +394,28 @@ unsigned Regions::idx(Region &R) { return r; } -void Regions::visitLoadInst(LoadInst &I) { idx(I.getPointerOperand()); } +void Regions::visitLoadInst(LoadInst &I) { + assert(currentFunction && "currentFunction must be set during visit"); + idx(I.getPointerOperand(), currentFunction); +} -void Regions::visitStoreInst(StoreInst &I) { idx(I.getPointerOperand()); } +void Regions::visitStoreInst(StoreInst &I) { + assert(currentFunction && "currentFunction must be set during visit"); + idx(I.getPointerOperand(), currentFunction); +} void Regions::visitAtomicCmpXchgInst(AtomicCmpXchgInst &I) { - idx(I.getPointerOperand()); + assert(currentFunction && "currentFunction must be set during visit"); + idx(I.getPointerOperand(), currentFunction); } void Regions::visitAtomicRMWInst(AtomicRMWInst &I) { - idx(I.getPointerOperand()); + assert(currentFunction && "currentFunction must be set during visit"); + idx(I.getPointerOperand(), currentFunction); } void Regions::visitMemSetInst(MemSetInst &I) { + assert(currentFunction && "currentFunction must be set during visit"); unsigned length; if (auto CI = dyn_cast(I.getLength())) @@ -255,10 +423,11 @@ void Regions::visitMemSetInst(MemSetInst &I) { else length = std::numeric_limits::max(); - idx(I.getDest(), length); + idx(I.getDest(), currentFunction, length); } void Regions::visitMemTransferInst(MemTransferInst &I) { + assert(currentFunction && "currentFunction must be set during visit"); unsigned length; if (auto CI = dyn_cast(I.getLength())) @@ -267,18 +436,19 @@ void Regions::visitMemTransferInst(MemTransferInst &I) { length = std::numeric_limits::max(); // We need to visit the source location otherwise - // extra merges will happen in the translation phrase, + // extra merges will happen in the translation phase, // resulting in ``hanging'' regions. - idx(I.getSource(), length); - idx(I.getDest(), length); + idx(I.getSource(), currentFunction, length); + idx(I.getDest(), currentFunction, length); } void Regions::visitCallInst(CallInst &I) { + assert(currentFunction && "currentFunction must be set during visit"); Function *F = I.getCalledFunction(); std::string name = F && F->hasName() ? F->getName().str() : ""; - if (F && F->isDeclaration() && I.getType()->isPointerTy() && name != "malloc") - idx(&I); + if (I.getType()->isPointerTy() && name != "malloc") + idx(&I, currentFunction); if (name.find("__SMACK_values") != std::string::npos) { assert(I.getNumArgOperands() == 2 && "Expected two operands."); @@ -294,7 +464,7 @@ void Regions::visitCallInst(CallInst &I) { const unsigned bound = I->getZExtValue(); const unsigned size = T->getElementType()->getIntegerBitWidth() / 8; const unsigned length = bound * size; - idx(P, length); + idx(P, currentFunction, length); } else { llvm_unreachable("Non-constant size expression not yet handled."); @@ -302,4 +472,600 @@ void Regions::visitCallInst(CallInst &I) { } } +FunctionRegionInfo Regions::emptyRegionInfo; + +void Regions::computeCallSiteMappings(Module &M) { + for (auto &F : M) { + if (F.isDeclaration()) + continue; + for (auto &BB : F) { + for (auto &I : BB) { + auto *CI = dyn_cast(&I); + if (!CI) + continue; + Function *callee = CI->getCalledFunction(); + if (!callee) + callee = dyn_cast( + CI->getCalledOperand()->stripPointerCastsAndAliases()); + if (!callee || callee->isDeclaration()) + continue; + if (callee->hasName() && + SmackOptions::usesGlobalMemory(callee->getName())) + continue; + + computeOneCallSiteMapping(CI, &F, callee); + } + } + } +} + +void Regions::computeOneCallSiteMapping(CallInst *CI, const Function *caller, + Function *callee) { + std::map mapping; + + // Map via actual/formal pointer parameter pairs. + unsigned argIdx = 0; + for (auto &formalArg : callee->args()) { + if (argIdx < CI->getNumArgOperands() && + formalArg.getType()->isPointerTy()) { + Value *actualArg = CI->getArgOperand(argIdx); + unsigned calleeR = idx(&formalArg, callee); + unsigned callerR = idx(actualArg, caller); + mapping[calleeR] = callerR; + } + argIdx++; + } + + // Map via return value: if the callee returns a pointer, map the + // callee's return value region to the caller's region for the call result. + if (CI->getType()->isPointerTy() && !callee->getReturnType()->isVoidTy()) { + // Find a return instruction in the callee to get the return value. + for (auto &BB : *callee) { + if (auto *RI = dyn_cast(BB.getTerminator())) { + if (RI->getReturnValue() && + RI->getReturnValue()->getType()->isPointerTy()) { + unsigned calleeR = idx(RI->getReturnValue(), callee); + unsigned callerR = idx(CI, caller); + if (!mapping.count(calleeR)) + mapping[calleeR] = callerR; + break; + } + } + } + } + + // Map via globals accessed by callee. + Module *M = CI->getModule(); + for (auto &GV : M->globals()) { + if (!GV.getType()->isPointerTy()) + continue; + // Only map if callee's graph has a cell for this global. + if (!DSA->hasGraph(*callee)) + continue; + auto &calleeG = DSA->getGraph(*callee); + if (!calleeG.hasCell(GV)) + continue; + if (!DSA->hasGraph(*caller)) + continue; + auto &callerG = DSA->getGraph(*caller); + if (!callerG.hasCell(GV)) + continue; + + unsigned calleeR = idx(&GV, callee); + unsigned callerR = idx(&GV, caller); + // Don't overwrite parameter mapping — it's call-site-specific + // and more precise than the global mapping. + if (!mapping.count(calleeR)) + mapping[calleeR] = callerR; + } + + // Extend mapping: for any unmapped callee region whose representative + // matches a mapped callee region's representative, map it to the same + // caller region. This handles cases like p[-1] where the callee accesses + // a different offset of the same DSA node as the parameter. + if (funcRegionVecs.count(callee)) { + auto &calleeRegions = funcRegionVecs[callee]; + // Build rep -> caller region from existing mapping. + std::map repToCallerRegion; + for (auto &entry : mapping) { + unsigned calleeIdx = entry.first; + unsigned callerIdx = entry.second; + if (calleeIdx < calleeRegions.size()) { + auto *rep = calleeRegions[calleeIdx].getRepresentative(); + if (rep) + repToCallerRegion[rep] = callerIdx; + } + } + // Map unmapped callee regions with matching representatives. + for (unsigned i = 0; i < calleeRegions.size(); i++) { + if (mapping.count(i)) + continue; + auto *rep = calleeRegions[i].getRepresentative(); + if (rep && repToCallerRegion.count(rep)) + mapping[i] = repToCallerRegion[rep]; + } + } + + // Extend mapping via DSA link following: discover node correspondences + // by traversing pointer edges in DSA graphs. This handles heap structures + // reachable through globals/parameters (e.g., global head -> list struct). + if (funcRegionVecs.count(callee) && funcRegionVecs.count(caller) && + DSA->hasGraph(*callee) && DSA->hasGraph(*caller)) { + auto &calleeRegions = funcRegionVecs[callee]; + auto &callerRegions = funcRegionVecs[caller]; + + // Build node-to-node mapping from existing region mapping. + // Only use non-conflicting entries (same callee node -> same caller node). + std::map calleeToCallerNode; + std::set conflicting; + for (auto &entry : mapping) { + unsigned calleeIdx = entry.first; + unsigned callerIdx = entry.second; + if (calleeIdx < calleeRegions.size() && + callerIdx < callerRegions.size()) { + auto *ce = calleeRegions[calleeIdx].getRepresentative(); + auto *cr = callerRegions[callerIdx].getRepresentative(); + if (ce && cr) { + auto it = calleeToCallerNode.find(ce); + if (it != calleeToCallerNode.end() && it->second != cr) + conflicting.insert(ce); + else + calleeToCallerNode[ce] = cr; + } + } + } + for (auto *n : conflicting) + calleeToCallerNode.erase(n); + + // Follow pointer links to discover additional node correspondences. + bool extended = true; + while (extended) { + extended = false; + for (auto &nodeEntry : calleeToCallerNode) { + auto *calleeNode = nodeEntry.first; + auto *callerNode = nodeEntry.second; + for (auto &link : calleeNode->links()) { + auto &field = link.first; + auto *calleeTarget = link.second->getNode(); + if (!calleeTarget || calleeToCallerNode.count(calleeTarget) || + conflicting.count(calleeTarget)) + continue; + if (callerNode->hasLink(field)) { + auto *callerTarget = callerNode->getLink(field).getNode(); + if (callerTarget) { + calleeToCallerNode[calleeTarget] = callerTarget; + extended = true; + } + } + } + } + } + + // Map remaining unmapped callee regions via discovered correspondences. + // First try to find an existing caller region; if none, create one. + for (unsigned i = 0; i < calleeRegions.size(); i++) { + if (mapping.count(i)) + continue; + auto *rep = calleeRegions[i].getRepresentative(); + if (!rep || conflicting.count(rep)) + continue; + auto nodeIt = calleeToCallerNode.find(rep); + const seadsa::Node *callerNode = + (nodeIt != calleeToCallerNode.end()) ? nodeIt->second : nullptr; + if (!callerNode) + continue; + // Find existing caller region for this node. + bool found = false; + for (unsigned j = 0; j < callerRegions.size(); j++) { + if (callerRegions[j].getRepresentative() == callerNode) { + mapping[i] = j; + found = true; + break; + } + } + if (!found) { + // Create a caller region for this node. + Region R(callerNode, caller->getContext()); + mapping[i] = idx(R, caller); + // Re-fetch since idx may have modified the vector. + callerRegions = funcRegionVecs[caller]; + } + } + } + + callSiteMappings[CI] = mapping; +} + +bool Regions::mergeCalleeRegion(const Function *F, unsigned keep, + unsigned remove) { + if (keep == remove) + return false; + // Ensure keep < remove for consistent processing. + if (keep > remove) + std::swap(keep, remove); + + auto ®ions = funcRegionVecs[F]; + if (remove >= regions.size()) + return false; + + // Merge region data. + regions[keep].merge(regions[remove]); + regions.erase(regions.begin() + remove); + + // Shift indices in FunctionRegionInfo. + auto &info = funcRegions[F]; + std::set newRead, newMod; + for (unsigned r : info.readRegions) { + if (r == remove) + newRead.insert(keep); + else + newRead.insert(r > remove ? r - 1 : r); + } + for (unsigned r : info.modifiedRegions) { + if (r == remove) + newMod.insert(keep); + else + newMod.insert(r > remove ? r - 1 : r); + } + info.readRegions = newRead; + info.modifiedRegions = newMod; + + // Update all call-site mappings that reference F. + // Mappings are callee_idx -> caller_idx. + for (auto &csEntry : callSiteMappings) { + CallInst *CI = const_cast(csEntry.first); + auto &mapping = csEntry.second; + + // Determine if F is the callee or the caller of this call site. + Function *csCallee = CI->getCalledFunction(); + if (!csCallee) + csCallee = dyn_cast( + CI->getCalledOperand()->stripPointerCastsAndAliases()); + const Function *csCaller = CI->getParent()->getParent(); + + if (csCallee == F) { + // F is the callee: shift callee-side (keys) of the mapping. + // 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; + for (auto &m : mapping) { + unsigned k = m.first; + if (k == remove) + k = keep; + else if (k > remove) + k--; + if (!newMapping.count(k)) + newMapping[k] = m.second; + } + mapping = newMapping; + } else if (csCaller == F) { + // F is the caller: shift caller-side (values) of the mapping. + std::map newMapping; + for (auto &m : mapping) { + unsigned v = m.second; + if (v == remove) + v = keep; + else if (v > remove) + v--; + newMapping[m.first] = v; + } + mapping = newMapping; + } + } + + return true; +} + +void Regions::propagateRegionMerges(Module &M) { + // Build call graph: caller -> [(CallInst, callee)] + std::map>> + callGraph; + // Reverse call graph: callee -> [caller] + std::map> callers; + + for (auto &F : M) { + if (F.isDeclaration()) + continue; + for (auto &BB : F) { + for (auto &I : BB) { + auto *CI = dyn_cast(&I); + if (!CI) + continue; + Function *callee = CI->getCalledFunction(); + if (!callee) + callee = dyn_cast( + CI->getCalledOperand()->stripPointerCastsAndAliases()); + if (!callee || callee->isDeclaration()) + continue; + if (callee->hasName() && + SmackOptions::usesGlobalMemory(callee->getName())) + continue; + callGraph[&F].push_back({CI, callee}); + callers[callee].insert(&F); + } + } + } + + // Compute SCCs using Tarjan's algorithm. + std::map index, lowlink; + std::map onStack; + std::vector stack; + std::vector> sccs; + int idx = 0; + + std::function strongconnect = + [&](const Function *F) { + index[F] = lowlink[F] = idx++; + stack.push_back(F); + onStack[F] = true; + + if (callGraph.count(F)) { + for (auto &edge : callGraph[F]) { + Function *callee = edge.second; + if (!index.count(callee)) { + strongconnect(callee); + lowlink[F] = std::min(lowlink[F], lowlink[callee]); + } else if (onStack[callee]) { + lowlink[F] = std::min(lowlink[F], index[callee]); + } + } + } + + if (lowlink[F] == index[F]) { + std::vector scc; + const Function *w; + do { + w = stack.back(); + stack.pop_back(); + onStack[w] = false; + scc.push_back(w); + } while (w != F); + sccs.push_back(scc); + } + }; + + for (auto &F : M) { + if (F.isDeclaration()) + continue; + if (!index.count(&F)) + strongconnect(&F); + } + + // SCCs are in reverse topological order (callees before callers). + // Reverse to get callers before callees (top-down). + std::reverse(sccs.begin(), sccs.end()); + + bool globalChanged = true; + while (globalChanged) { + globalChanged = false; + + // Top-down pass: merge callee regions when multiple map to same caller + // region. + for (auto &scc : sccs) { + bool changed = true; + while (changed) { + changed = false; + for (const Function *F : scc) { + if (!callGraph.count(F)) + continue; + for (auto &edge : callGraph[F]) { + CallInst *CI = edge.first; + Function *callee = edge.second; + if (!callSiteMappings.count(CI)) + continue; + + auto &mapping = callSiteMappings[CI]; + + // Check for collisions: multiple callee regions -> same caller + // region. + std::map> callerToCallees; + for (auto &m : mapping) + callerToCallees[m.second].push_back(m.first); + + for (auto &entry : callerToCallees) { + auto &calleeIndices = entry.second; + if (calleeIndices.size() <= 1) + continue; + + // Merge all colliding callee regions into the first. + std::sort(calleeIndices.begin(), calleeIndices.end()); + // Merge from highest index down to avoid shifting issues. + for (int i = calleeIndices.size() - 1; i >= 1; i--) { + unsigned keep = calleeIndices[0]; + unsigned remove = calleeIndices[i]; + if (mergeCalleeRegion(callee, keep, remove)) { + changed = true; + } + } + + // mergeCalleeRegion already updated all call-site mapping + // indices. Do NOT recompute via computeOneCallSiteMapping — + // that calls idx() which can recreate the merged-away region + // (different DSA representative), causing an infinite loop. + break; // restart collision check since indices shifted + } + } + } + if (changed) + globalChanged = true; + } + } + + // Bottom-up pass: merge caller regions when the callee has collapsed + // them. + for (auto it = sccs.rbegin(); it != sccs.rend(); ++it) { + auto &scc = *it; + bool changed = true; + while (changed) { + changed = false; + for (const Function *F : scc) { + if (!callGraph.count(F)) + continue; + bool merged = false; + for (auto &edge : callGraph[F]) { + CallInst *CI = edge.first; + if (!callSiteMappings.count(CI)) + continue; + if (!funcRegionVecs.count(F)) + continue; + + auto &mapping = callSiteMappings[CI]; + auto &callerRegions = funcRegionVecs[F]; + + // Build rep -> mapped caller region index. + std::map repToMappedCaller; + std::set mappedCallerIndices; + for (auto &m : mapping) { + mappedCallerIndices.insert(m.second); + if (m.second < callerRegions.size()) { + auto *rep = callerRegions[m.second].getRepresentative(); + if (rep) + repToMappedCaller[rep] = m.second; + } + } + + // Find unmapped caller regions whose rep matches a mapped one. + for (unsigned i = 0; i < callerRegions.size() && !merged; i++) { + if (mappedCallerIndices.count(i)) + continue; + auto *rep = callerRegions[i].getRepresentative(); + if (rep && repToMappedCaller.count(rep)) { + unsigned keep = repToMappedCaller[rep]; + if (mergeCalleeRegion(F, keep, i)) { + changed = true; + merged = true; + } + } + } + if (merged) + break; // restart since indices shifted + } + if (changed) + break; + } + if (changed) + globalChanged = true; + } + } + } +} + +void Regions::computeGlobalMemoryMappings(Module &M) { + const Function *entryF = nullptr; + for (auto &F : M) { + if (F.hasName() && SmackOptions::isEntryPoint(F.getName())) { + entryF = &F; + break; + } + } + if (!entryF) + return; + + for (auto &F : M) { + if (F.isDeclaration()) + continue; + if (!F.hasName()) + continue; + if (!SmackOptions::usesGlobalMemory(F.getName())) + continue; + if (SmackOptions::isEntryPoint(F.getName())) + continue; + + std::map mapping; + for (auto &GV : M.globals()) { + if (!GV.getType()->isPointerTy()) + continue; + if (!DSA->hasGraph(F) || !DSA->hasGraph(*entryF)) + continue; + auto &fGraph = DSA->getGraph(F); + auto &entryGraph = DSA->getGraph(*entryF); + if (!fGraph.hasCell(GV) || !entryGraph.hasCell(GV)) + continue; + unsigned fR = idx(&GV, &F); + unsigned entryR = idx(&GV, entryF); + mapping[fR] = entryR; + } + globalMemoryMappings[&F] = mapping; + } +} + +void Regions::computeFunctionRegions(Module &M) { + // Transitive closure: propagate callee region accesses to callers + // through call-site mappings. + bool changed = true; + while (changed) { + changed = false; + for (auto &F : M) { + if (F.isDeclaration()) + continue; + FunctionRegionInfo &info = funcRegions[&F]; + for (auto &BB : F) { + for (auto &I : BB) { + auto *CI = dyn_cast(&I); + if (!CI) + continue; + Function *callee = CI->getCalledFunction(); + if (!callee) + callee = dyn_cast( + CI->getCalledOperand()->stripPointerCastsAndAliases()); + if (!callee || callee->isDeclaration()) + continue; + if (!callSiteMappings.count(CI)) + continue; + + auto &mapping = callSiteMappings[CI]; + auto &calleeInfo = funcRegions[callee]; + + for (unsigned calleeR : calleeInfo.readRegions) { + if (mapping.count(calleeR)) { + if (info.readRegions.insert(mapping.at(calleeR)).second) + changed = true; + } + } + for (unsigned calleeR : calleeInfo.modifiedRegions) { + if (mapping.count(calleeR)) { + if (info.modifiedRegions.insert(mapping.at(calleeR)).second) + changed = true; + } + } + } + } + } + } +} + +const FunctionRegionInfo & +Regions::getFunctionRegionInfo(const Function *F) const { + auto it = funcRegions.find(F); + if (it != funcRegions.end()) + return it->second; + return emptyRegionInfo; +} + +std::set Regions::getAccessedRegions(const Function *F) const { + auto &info = getFunctionRegionInfo(F); + std::set result = info.readRegions; + result.insert(info.modifiedRegions.begin(), info.modifiedRegions.end()); + return result; +} + +const std::map & +Regions::getCallSiteMapping(const CallInst *CI) const { + static const std::map emptyMapping; + auto it = callSiteMappings.find(CI); + if (it != callSiteMappings.end()) + return it->second; + return emptyMapping; +} + +const std::map & +Regions::getGlobalMemoryMapping(const Function *F) const { + static const std::map emptyMapping; + auto it = globalMemoryMappings.find(F); + if (it != globalMemoryMappings.end()) + return it->second; + return emptyMapping; +} + } // namespace smack diff --git a/lib/smack/Slicing.cpp b/lib/smack/Slicing.cpp index d20f08f27..b88847d4c 100644 --- a/lib/smack/Slicing.cpp +++ b/lib/smack/Slicing.cpp @@ -84,7 +84,7 @@ pair getParameter(Value *V, Naming &naming, SmackRep &rep) { // XXX I need to be fixed FIXME unsigned r = 0; // rep.getRegion(G); llvm_unreachable("This code is under contsruction."); - return make_pair(rep.memReg(r), rep.memType(r)); + return make_pair(rep.memReg(r), rep.memType(nullptr, r)); } else if (ConstantDataSequential *S = dyn_cast(V)) diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index d56bcdf75..2ce6f2ae4 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -6,6 +6,7 @@ #include "smack/BoogieAst.h" #include "smack/Debug.h" #include "smack/Naming.h" +#include "smack/Regions.h" #include "smack/SmackOptions.h" #include "smack/SmackRep.h" #include "smack/VectorOperations.h" @@ -168,6 +169,14 @@ void SmackInstGenerator::visitBasicBlock(llvm::BasicBlock &bb) { naming->get(A))})); } } + + // Initialize local memory shadows from input parameters. + if (!SmackOptions::usesGlobalMemory(naming->get(*F))) { + auto accessed = rep->getRegions()->getAccessedRegions(F); + for (unsigned r : accessed) + emit(Stmt::assign(Expr::id(rep->memPath(r)), + Expr::id(rep->memReg(r) + ".in"))); + } } } @@ -243,6 +252,16 @@ void SmackInstGenerator::visitReturnInst(llvm::ReturnInst &ri) { llvm::Value *v = ri.getReturnValue(); if (v) emit(Stmt::assign(Expr::id(Naming::RET_VAR), rep->expr(v))); + + // Copy modified regions to output parameters. + const llvm::Function *F = ri.getParent()->getParent(); + if (!SmackOptions::usesGlobalMemory(naming->get(*F))) { + auto &info = rep->getRegions()->getFunctionRegionInfo(F); + for (unsigned r : info.modifiedRegions) + emit(Stmt::assign(Expr::id(rep->memReg(r) + ".out"), + Expr::id(rep->memPath(r)))); + } + emit(Stmt::assign(Expr::id(Naming::EXN_VAR), Expr::lit(false))); emit(Stmt::return_()); } @@ -487,7 +506,8 @@ void SmackInstGenerator::visitLoadInst(llvm::LoadInst &li) { const Expr *E; if (isa(T->getElementType())) { auto D = VectorOperations(rep).load(P); - E = Expr::fn(D->getName(), {Expr::id(rep->memPath(P)), rep->expr(P)}); + E = Expr::fn(D->getName(), {Expr::id(rep->memPath(P, rep->currentFunction)), + rep->expr(P)}); } else { E = rep->load(P); } @@ -511,7 +531,7 @@ void SmackInstGenerator::visitStoreInst(llvm::StoreInst &si) { if (isa(V->getType())) { auto D = VectorOperations(rep).store(P); - auto M = Expr::id(rep->memPath(P)); + auto M = Expr::id(rep->memPath(P, rep->currentFunction)); auto E = Expr::fn(D->getName(), {M, rep->expr(P), rep->expr(V)}); emit(Stmt::assign(M, E)); } else { @@ -740,7 +760,7 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) { std::list args; for (auto &V : cj->arg_operands()) args.push_back(rep->expr(V)); - for (auto m : rep->memoryMaps()) + for (auto m : rep->memoryMaps(rep->currentFunction)) args.push_back(Expr::id(m.first)); auto E = Expr::fn(F->getName().str(), args); if (name == Naming::CONTRACT_REQUIRES) diff --git a/lib/smack/SmackModuleGenerator.cpp b/lib/smack/SmackModuleGenerator.cpp index 2c70404f4..d48205930 100644 --- a/lib/smack/SmackModuleGenerator.cpp +++ b/lib/smack/SmackModuleGenerator.cpp @@ -45,6 +45,14 @@ void SmackModuleGenerator::generateProgram(llvm::Module &M) { decls.insert(decls.end(), ds.begin(), ds.end()); } + // Find the entry-point function for global memory map declarations. + for (auto &F : M) { + if (F.hasName() && SmackOptions::isEntryPoint(F.getName())) { + rep.entryFunction = &F; + break; + } + } + SDEBUG(errs() << "Analyzing functions...\n"); for (auto &F : M) { @@ -52,6 +60,17 @@ void SmackModuleGenerator::generateProgram(llvm::Module &M) { // Reset the counters for per-function names naming.reset(); + // Set the current function context for SmackRep. + // Non-entry usesGlobalMemory functions (e.g., __SMACK_static_init) must + // use the entry function's region context so that their $M.R references + // match the global declarations (which use entry function's indices). + if (rep.entryFunction && F.hasName() && + SmackOptions::usesGlobalMemory(F.getName()) && + !SmackOptions::isEntryPoint(F.getName())) + rep.currentFunction = rep.entryFunction; + else + rep.currentFunction = &F; + SDEBUG(errs() << "Analyzing function: " << naming.get(F) << "\n"); auto ds = rep.globalDecl(&F); @@ -83,13 +102,31 @@ void SmackModuleGenerator::generateProgram(llvm::Module &M) { } else if (naming.get(F).find(Naming::INIT_FUNC_PREFIX) == 0) rep.addInitFunc(&F); + + // Add local memory variable declarations. + if (F.hasName() && SmackOptions::isEntryPoint(F.getName())) { + // Entry points: local vars for non-global-scope regions. + unsigned numRegions = getAnalysis().size(&F); + for (unsigned r = 0; r < numRegions; r++) { + if (!getAnalysis().get(&F, r).isGlobalScope()) + P->getDeclarations().push_back( + Decl::variable(rep.memReg(r), rep.memType(&F, r))); + } + } else if (!(F.hasName() && + SmackOptions::usesGlobalMemory(F.getName()))) { + // Regular (non-global-memory) functions: all regions are local. + auto accessed = getAnalysis().getAccessedRegions(&F); + for (unsigned r : accessed) + P->getDeclarations().push_back( + Decl::variable(rep.memReg(r), rep.memType(&F, r))); + } } SDEBUG(errs() << "Finished analyzing function: " << naming.get(F) << "\n\n"); } - // MODIFIES - // ... to do below, after memory splitting is determined. + // No explicit modifies clauses for global-memory procedures; + // the verifier infers them automatically. } auto ds = rep.auxiliaryDeclarations(); diff --git a/lib/smack/SmackOptions.cpp b/lib/smack/SmackOptions.cpp index 1ce8fdc2f..3fca4a6f3 100644 --- a/lib/smack/SmackOptions.cpp +++ b/lib/smack/SmackOptions.cpp @@ -3,6 +3,7 @@ // #include "smack/SmackOptions.h" +#include "smack/Naming.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/Regex.h" @@ -108,6 +109,16 @@ bool SmackOptions::isEntryPoint(llvm::StringRef name) { return false; } +bool SmackOptions::usesGlobalMemory(llvm::StringRef name) { + if (isEntryPoint(name)) + return true; + // Init functions operate on global state directly. + if (name == Naming::STATIC_INIT_PROC || + name.startswith(Naming::INIT_FUNC_PREFIX)) + return true; + return false; +} + bool SmackOptions::shouldCheckFunction(llvm::StringRef name) { if (CheckedFunctions.size() == 0) { return true; diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 79c8a09c2..119ecc8e6 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -261,32 +261,34 @@ std::string SmackRep::memReg(unsigned idx) { return indexedName(Naming::MEMORY, {idx}); } -std::string SmackRep::memType(unsigned region) { +std::string SmackRep::memType(const Function *F, unsigned region) { std::stringstream s; - if (!regions->get(region).isSingleton() || + if (!regions->get(F, region).isSingleton() || (SmackOptions::BitPrecise && SmackOptions::NoByteAccessInference)) s << "[" << Naming::PTR_TYPE << "] "; - const Type *T = regions->get(region).getType(); + const Type *T = regions->get(F, region).getType(); s << (T ? type(T) : intType(8)); return s.str(); } std::string SmackRep::memPath(unsigned region) { return memReg(region); } -std::string SmackRep::memPath(const llvm::Value *v) { - return memPath(regions->idx(v)); +std::string SmackRep::memPath(const llvm::Value *v, const Function *F) { + return memPath(regions->idx(v, F)); } -std::list> SmackRep::memoryMaps() { +std::list> +SmackRep::memoryMaps(const Function *F) { std::list> mms; - for (unsigned i = 0; i < regions->size(); i++) - mms.push_back({memReg(i), memType(i)}); + for (unsigned i = 0; i < regions->size(F); i++) + mms.push_back({memReg(i), memType(F, i)}); return mms; } bool SmackRep::isExternal(const llvm::Value *v) { return v->getType()->isPointerTy() && - !regions->get(regions->idx(v)).isAllocated(); + !regions->get(currentFunction, regions->idx(v, currentFunction)) + .isAllocated(); } const Stmt *SmackRep::alloca(llvm::AllocaInst &i) { @@ -305,10 +307,10 @@ const Stmt *SmackRep::memcpy(const llvm::MemCpyInst &mci) { else length = std::numeric_limits::max(); - unsigned r1 = regions->idx(mci.getRawDest(), length); - unsigned r2 = regions->idx(mci.getRawSource(), length); + unsigned r1 = regions->idx(mci.getRawDest(), currentFunction, length); + unsigned r2 = regions->idx(mci.getRawSource(), currentFunction, length); - const Type *T = regions->get(r1).getType(); + const Type *T = regions->get(currentFunction, r1).getType(); Decl *P = memcpyProc(T ? type(T) : intType(8), length); auxDecls[P->getName()] = P; @@ -330,9 +332,9 @@ const Stmt *SmackRep::memset(const llvm::MemSetInst &msi) { else length = std::numeric_limits::max(); - unsigned r = regions->idx(msi.getRawDest(), length); + unsigned r = regions->idx(msi.getRawDest(), currentFunction, length); - const Type *T = regions->get(r).getType(); + const Type *T = regions->get(currentFunction, r).getType(); Decl *P = memsetProc(T ? type(T) : intType(8), length); auxDecls[P->getName()] = P; @@ -370,8 +372,8 @@ const Stmt *SmackRep::valueAnnotation(const CallInst &CI) { auto T = GEP->getResultElementType(); const unsigned bits = this->getSize(T); const unsigned bytes = bits / 8; - const unsigned R = regions->idx(GEP); - bool bytewise = regions->get(R).bytewiseAccess(); + const unsigned R = regions->idx(GEP, currentFunction); + bool bytewise = regions->get(currentFunction, R).bytewiseAccess(); attrs.push_back(Attr::attr("name", {Expr::id(naming->get(*A))})); attrs.push_back(Attr::attr( "field", { @@ -426,8 +428,8 @@ const Stmt *SmackRep::valueAnnotation(const CallInst &CI) { const unsigned bits = this->getSize(T); const unsigned bytes = bits / 8; const unsigned length = count * bytes; - const unsigned R = regions->idx(V, length); - bool bytewise = regions->get(R).bytewiseAccess(); + const unsigned R = regions->idx(V, currentFunction, length); + bool bytewise = regions->get(currentFunction, R).bytewiseAccess(); args.push_back(expr(CI.getArgOperand(1))); attrs.push_back(Attr::attr("name", {Expr::id(naming->get(*A))})); attrs.push_back(Attr::attr( @@ -502,10 +504,10 @@ bool SmackRep::isUnsafeFloatAccess(const Type *elemTy, const Type *resultTy) { const Expr *SmackRep::load(const llvm::Value *P) { const PointerType *T = dyn_cast(P->getType()); assert(T && "Expected pointer type."); - const unsigned R = regions->idx(P); - bool bytewise = regions->get(R).bytewiseAccess(); - bool singleton = regions->get(R).isSingleton(); - const Type *resultTy = regions->get(R).getType(); + const unsigned R = regions->idx(P, currentFunction); + bool bytewise = regions->get(currentFunction, R).bytewiseAccess(); + bool singleton = regions->get(currentFunction, R).isSingleton(); + const Type *resultTy = regions->get(currentFunction, R).getType(); const Expr *M = Expr::id(memPath(R)); std::string N = Naming::LOAD + "." + @@ -524,14 +526,15 @@ const Stmt *SmackRep::store(const Value *P, const Value *V) { const Stmt *SmackRep::store(const Value *P, const Expr *V) { const PointerType *T = dyn_cast(P->getType()); assert(T && "Expected pointer type."); - return store(regions->idx(P), T->getElementType(), expr(P), V); + return store(regions->idx(P, currentFunction), T->getElementType(), expr(P), + V); } const Stmt *SmackRep::store(unsigned R, const Type *T, const Expr *P, const Expr *V) { - bool bytewise = regions->get(R).bytewiseAccess(); - bool singleton = regions->get(R).isSingleton(); - const Type *resultTy = regions->get(R).getType(); + bool bytewise = regions->get(currentFunction, R).bytewiseAccess(); + bool singleton = regions->get(currentFunction, R).isSingleton(); + const Type *resultTy = regions->get(currentFunction, R).getType(); std::string N = Naming::STORE + "." + (bytewise ? "bytes." @@ -1046,7 +1049,7 @@ ProcDecl *SmackRep::procedure(Function *F, CallInst *CI) { "", {Stmt::call(Naming::FREE, {Expr::id(params.front().first)})})); } else if (isContractExpr(F)) { - for (auto m : memoryMaps()) + for (auto m : memoryMaps(F)) params.push_back(m); } else if (CI) { @@ -1068,6 +1071,18 @@ ProcDecl *SmackRep::procedure(Function *F, CallInst *CI) { } } + // Add memory region parameters and returns for non-entry procedures. + if (F->hasName() && !SmackOptions::usesGlobalMemory(F->getName()) && + !F->isDeclaration() && !isContractExpr(F)) { + auto accessed = regions->getAccessedRegions(F); + for (unsigned r : accessed) + params.push_back({memReg(r) + ".in", memType(F, r)}); + + auto &info = regions->getFunctionRegionInfo(F); + for (unsigned r : info.modifiedRegions) + rets.push_back({memReg(r) + ".out", memType(F, r)}); + } + return static_cast( Decl::procedure(name, params, rets, decls, blocks)); } @@ -1124,6 +1139,27 @@ const Stmt *SmackRep::call(llvm::Function *f, const llvm::User &ci) { if (!ci.getType()->isVoidTy()) rets.push_back(naming->get(ci)); + // Thread memory regions through the call for non-entry procedures. + // Use call-site mapping to pass caller's regions for callee's params. + if (f->hasName() && !SmackOptions::usesGlobalMemory(f->getName()) && + !f->isDeclaration() && !isContractExpr(f)) { + auto *callInst = dyn_cast(&ci); + auto &mapping = regions->getCallSiteMapping(callInst); + auto accessed = regions->getAccessedRegions(f); + for (unsigned calleeR : accessed) { + auto it = mapping.find(calleeR); + unsigned callerR = (it != mapping.end()) ? it->second : calleeR; + args.push_back(Expr::id(memPath(callerR))); + } + + auto &info = regions->getFunctionRegionInfo(f); + for (unsigned calleeR : info.modifiedRegions) { + auto it = mapping.find(calleeR); + unsigned callerR = (it != mapping.end()) ? it->second : calleeR; + rets.push_back(memPath(callerR)); + } + } + return Stmt::call(procName(f, ci), args, rets); } @@ -1216,9 +1252,10 @@ const Stmt *SmackRep::inverseFPCastAssume(const StoreInst *si) { const PointerType *PT = dyn_cast(P->getType()); assert(PT && "Expected pointer type."); const Type *T = PT->getElementType(); - unsigned R = regions->idx(P); - if (!T->isFloatingPointTy() || !regions->get(R).bytewiseAccess() || - regions->get(R).isSingleton()) { + unsigned R = regions->idx(P, currentFunction); + if (!T->isFloatingPointTy() || + !regions->get(currentFunction, R).bytewiseAccess() || + regions->get(currentFunction, R).isSingleton()) { return nullptr; } return inverseFPCastAssume( diff --git a/lib/smack/VectorOperations.cpp b/lib/smack/VectorOperations.cpp index 0bf7a2bff..ba97b0ecc 100644 --- a/lib/smack/VectorOperations.cpp +++ b/lib/smack/VectorOperations.cpp @@ -270,11 +270,11 @@ FuncDecl *VectorOperations::load(const Value *V) { auto ET = PT->getElementType(); type(ET); - auto R = rep->regions->idx(V); - auto MT = rep->regions->get(R).getType(); + auto R = rep->regions->idx(V, rep->currentFunction); + auto MT = rep->regions->get(rep->currentFunction, R).getType(); MT || (MT = IntegerType::get(V->getContext(), 8)); auto FN = rep->opName(Naming::LOAD, {ET, MT}); - auto M = rep->memType(R); + auto M = rep->memType(rep->currentFunction, R); auto P = rep->type(PT); auto E = rep->type(ET); auto F = (MT == ET) ? Decl::function(FN, {{"M", M}, {"p", P}}, E, @@ -290,11 +290,11 @@ FuncDecl *VectorOperations::store(const Value *V) { auto ET = PT->getElementType(); type(ET); - auto R = rep->regions->idx(V); - auto MT = rep->regions->get(R).getType(); + auto R = rep->regions->idx(V, rep->currentFunction); + auto MT = rep->regions->get(rep->currentFunction, R).getType(); MT || (MT = IntegerType::get(V->getContext(), 8)); auto FN = rep->opName(Naming::STORE, {ET, MT}); - auto M = rep->memType(R); + auto M = rep->memType(rep->currentFunction, R); auto P = rep->type(PT); auto E = rep->type(ET); auto F = (MT == ET) ? Decl::function(FN, {{"M", M}, {"p", P}, {"v", E}}, M, diff --git a/share/smack/top.py b/share/smack/top.py index 0d7d9c501..9d7d4b6fa 100644 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -492,7 +492,7 @@ def arguments(): '--check', metavar='PROPERTY', nargs='+', - choices=list(VProperty), + choices=list(VProperty.__members__.values()), default=VProperty.NONE, type=VProperty.argparse, action=PropertyAction, @@ -726,7 +726,7 @@ def llvm_to_bpl(args): cmd = ['llvm2bpl', args.linked_bc_file, '-bpl', args.bpl_file] cmd += ['-warn-type', args.warn] - cmd += ['-sea-dsa=ci'] + cmd += ['-sea-dsa=cs'] # This flag can lead to unsoundness in Rust regressions. # cmd += ['-sea-dsa-type-aware'] if sys.stdout.isatty(): diff --git a/test/c/basic/malloc_collapsing.c b/test/c/basic/malloc_collapsing.c index d8aa45418..854995c8a 100644 --- a/test/c/basic/malloc_collapsing.c +++ b/test/c/basic/malloc_collapsing.c @@ -3,7 +3,6 @@ #include // @expect verified -// @checkbpl grep "var \$M.0: \[ref\] i32;" int main(void) { int *p = (int *)malloc(sizeof(int)); From 43b5c856b111891f5c053f3738e03d1297da50f5 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 30 Mar 2026 22:54:39 -0700 Subject: [PATCH 02/15] Fix remaining CS-DSA regressions and update documentation - Add return value mapping to call-site mappings (fixes func_ptr2) - Create missing caller regions via Region(Node*) during link-following - Iterate computeCallSiteMappings to propagate regions up the call chain - Index pointer return values from all calls, not just declarations - Remove broken identity fallback (callerR = calleeR) - Update cs-dsa-memory-plan.md to reflect final architecture Co-Authored-By: Claude Opus 4.6 (1M context) --- docs/cs-dsa-memory-plan.md | 383 +++++++------------------------------ 1 file changed, 71 insertions(+), 312 deletions(-) diff --git a/docs/cs-dsa-memory-plan.md b/docs/cs-dsa-memory-plan.md index 4e439e6c7..454a5d543 100644 --- a/docs/cs-dsa-memory-plan.md +++ b/docs/cs-dsa-memory-plan.md @@ -1,362 +1,121 @@ -# Plan: Context-Sensitive DSA Memory Regions in SMACK +# Context-Sensitive DSA Memory Regions in SMACK -## Context +## Overview -SMACK currently uses **context-insensitive** sea-dsa analysis (`-sea-dsa=ci`), producing a single global points-to graph for the entire module. All memory regions (`$M.0`, `$M.1`, ...) are declared as **global Boogie variables**, and every procedure implicitly accesses all of them. This means Corral must conservatively havoc all memory regions at each unresolved call site, limiting verification scalability. +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). -The goal is to switch to **context-sensitive** sea-dsa (`-sea-dsa=cs` or `-sea-dsa=butd-cs`) so each function has its own DSA graph. This enables computing per-function read/write region sets, and threading only the relevant regions through procedure signatures as parameters (reads) and returns (writes). - -**Target Boogie transformation:** ```boogie -// BEFORE (global memory) -var $M.0: [ref]i8; -var $M.1: [ref]i32; - -procedure foo(x: ref) - modifies $M.0; -{ $M.0 := $store.i8($M.0, x, 42); } - -// AFTER (region-parameterized) -procedure foo(x: ref, $M.0: [ref]i8) returns ($M.0: [ref]i8) -{ $M.0 := $store.i8($M.0, x, 42); } +// 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, $M.1; + modifies $M.0; { call $M.0 := foo(x, $M.0); } ``` -Non-entry procedures use their regions as **local** in/out parameters. Entry points (`main`) keep using globals with `modifies` clauses. The procedure body code (`$load`/`$store` referencing `$M.R`) does not change -- the trick is that `$M.R` becomes a local variable shadowing the global. +Entry points (`main`) keep globals with `modifies` clauses. Non-entry procedures use local in/out parameters. --- -## Implementation Steps - -### Step 1: DSAWrapper -- Support Context-Sensitive Analysis - -**Files:** `lib/smack/DSAWrapper.cpp`, `include/smack/DSAWrapper.h` - -1a. **Remove the CI assertion** (line 33-34 of DSAWrapper.cpp): -```cpp -// Remove: -assert(SD->kind() == seadsa::GlobalAnalysisKind::CONTEXT_INSENSITIVE && ...); -``` - -1b. **Make `getNode`/`getOffset` function-aware.** Currently they query the single global graph `DG`. Change them to resolve the function from the value and query the per-function graph: -```cpp -const seadsa::Node *DSAWrapper::getNode(const Value *v) { - auto &graph = getGraphForValue(v); - if (!graph.hasCell(*v)) return nullptr; - return graph.getCell(*v).getNode(); -} - -seadsa::Graph &DSAWrapper::getGraphForValue(const Value *v) { - if (auto *I = dyn_cast(v)) - return SD->getGraph(*I->getParent()->getParent()); - if (auto *A = dyn_cast(v)) - return SD->getGraph(*A->getParent()); - // For globals/constants, use fallback graph - return *DG; -} -``` - -Keep `DG` as a fallback for globals: `DG = &SD->getGraph(*M.begin())` still works (the entry function's graph contains global info). +## Architecture -1c. **Expose per-function graph access** for the Regions pass: -```cpp -seadsa::Graph &getGraph(const llvm::Function &F) { return SD->getGraph(F); } -bool hasGraph(const llvm::Function &F) const { return SD->hasGraph(F); } -``` - -1d. **Update `collectStaticInits` and `countGlobalRefs`** to handle multiple graphs. Currently these iterate `DG` which is the single graph. With CS mode, iterate all functions' graphs and union results. The simplest approach: keep using `DG` (entry function graph) since globals appear in the entry function's graph in CS mode too. +### Phase 1: Per-Function Region Construction ---- +**Files:** `Regions.cpp` (runOnModule) -### Step 2: Regions -- Per-Function Read/Write Region Sets +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`). -**Files:** `lib/smack/Regions.cpp`, `include/smack/Regions.h` +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. -2a. **Add per-function region tracking** to the `Regions` class: -```cpp -// In Regions.h: -struct FunctionRegionInfo { - std::set readRegions; - std::set modifiedRegions; -}; -std::map funcRegions; +### Phase 2: Read/Write Sets -// Public API: -const std::set& getReadRegions(const llvm::Function *F) const; -const std::set& getModifiedRegions(const llvm::Function *F) const; -std::set getAccessedRegions(const llvm::Function *F) const; -``` +Direct memory accesses in each function are recorded: +- `LoadInst` -> readRegions +- `StoreInst` -> modifiedRegions +- `AtomicCmpXchgInst`, `AtomicRMWInst` -> both +- `MemSetInst` -> modifiedRegions +- `MemTransferInst` -> readRegions (source) + modifiedRegions (dest) -2b. **Compute per-function region sets** after the global `visit(M)` pass in `runOnModule`. Two approaches: - -**Option A (instruction-based):** Iterate each function's instructions, call `idx(ptr_operand)` for each load/store/atomic/memcpy/memset, and classify as read or modified: -```cpp -for (auto &F : M) { - if (F.isDeclaration()) continue; - for (auto &BB : F) { - for (auto &I : BB) { - if (auto *LI = dyn_cast(&I)) { - unsigned r = idx(LI->getPointerOperand()); - funcRegions[&F].readRegions.insert(r); - } else if (auto *SI = dyn_cast(&I)) { - unsigned r = idx(SI->getPointerOperand()); - funcRegions[&F].modifiedRegions.insert(r); - } - // ... atomics, memcpy, memset ... - } - } -} -``` - -**Option B (DSA-graph-based):** For each function, iterate its DSA graph nodes, match nodes to global regions by representative, classify by `node->isRead()`/`node->isModified()`. This automatically includes transitive effects (callees), since the CS graph propagates callee effects. - -**Recommendation:** Use Option A for the direct region mapping (it reuses existing `idx()` logic), then **add transitive closure** by iterating call instructions and unioning callee region sets (post-order on call graph). - ---- - -### Step 3: SmackRep -- Procedure Signatures with Memory Parameters - -**Files:** `lib/smack/SmackRep.cpp`, `include/smack/SmackRep.h` - -3a. **Modify `procedure(Function*, CallInst*)`** (line 1037) to add memory region params/returns for non-entry-point procedures: - -```cpp -// After existing param computation (line 1044-1045): -if (!SmackOptions::isEntryPoint(F->getName()) && !F->isDeclaration()) { - auto accessed = regions->getAccessedRegions(F); - for (unsigned r : accessed) - params.push_back({memReg(r), memType(r)}); // $M.R as input param - - auto modified = regions->getModifiedRegions(F); - for (unsigned r : modified) - rets.push_back({memReg(r), memType(r)}); // $M.R as output return -} -``` - -Note: We use the same name `$M.R` for both param and return, relying on Boogie's scoping (input params and output returns are distinct). Actually, Boogie requires distinct names, so use `$M.R` for input and a differently-scoped return. In Boogie, `returns (x: T)` creates a local `x` that is assigned and returned. So the pattern is: - -```boogie -procedure foo(x: ref, $M.0: [ref]i8) returns (ret: i32, $M.0: [ref]i8) -``` +### Phase 2.5: Global Memory Mappings -Wait -- Boogie does NOT allow the same name for both an input param and an output return. So we need either: -- Use `$M.R` as input param, and a different name like `$M.R.out` for return, with an epilogue copy -- Use `$M.R` as a local variable, `$M.R.in` as input param, `$M.R.out` as output return, with prologue/epilogue copies - -**Recommended approach (local shadow):** -- Input params: `$M.R.in` -- Output returns: `$M.R.out` -- Local variable: `$M.R` (declared as local, initialized from `$M.R.in` at entry, copied to `$M.R.out` at returns) -- Procedure body code continues to reference `$M.R` unchanged - -```cpp -if (!isEntryPoint && !F->isDeclaration()) { - auto accessed = regions->getAccessedRegions(F); - for (unsigned r : accessed) - params.push_back({memReg(r) + ".in", memType(r)}); - - auto modified = regions->getModifiedRegions(F); - for (unsigned r : modified) - rets.push_back({memReg(r) + ".out", memType(r)}); -} -``` +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. -3b. **Modify `call(Function*, User&)`** (line 1122) to pass and receive memory regions: +### Phase 3: Call-Site Mappings -```cpp -// After existing arg computation: -if (!SmackOptions::isEntryPoint(f->getName())) { - auto accessed = regions->getAccessedRegions(f); - for (unsigned r : accessed) - args.push_back(Expr::id(memPath(r))); // pass current $M.R +**`computeOneCallSiteMapping(CI, caller, callee)`** builds a map from callee region indices to caller region indices through: - auto modified = regions->getModifiedRegions(f); - for (unsigned r : modified) - rets.push_back(memPath(r)); // assign returned $M.R -} -``` +1. **Parameter pairs** -- formal pointer params mapped to actual args +2. **Return value** -- callee's return value region mapped to caller's call result region +3. **Global pairs** -- shared globals (parameter mappings take priority over globals to preserve call-site specificity) +4. **Rep-matching extension** -- unmapped callee regions whose DSA node matches a mapped callee region's node +5. **DSA link-following** -- traverse pointer edges in both callee and caller DSA graphs to discover node correspondences for heap structures reachable through globals/parameters. Creates missing caller regions via `Region(Node*, ctx)` when needed. -3c. **Handle declared (external) functions conservatively.** For functions with no body, assume they may access/modify all regions. Add a helper: -```cpp -bool isConservativeFunction(Function *F) { - return F->isDeclaration() && !isSpecialFunction(F); -} -``` +**Conflict detection:** When a callee DSA node maps to multiple different caller nodes (e.g., two globals unified in the callee), it's marked as conflicting and excluded from link-following to avoid incorrect merging. ---- +**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. -### Step 4: SmackInstGenerator -- Prologue/Epilogue for Local Memory Shadows +### Phase 3.5: Region Merge Propagation -**Files:** `lib/smack/SmackInstGenerator.cpp` +**`propagateRegionMerges(M)`** enforces the soundness invariant: **regions must not alias**. Uses SCCs for proper ordering. -4a. **Patch `visitReturnInst`** (line 240) to copy local memory to output params before returning: +**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. -```cpp -void SmackInstGenerator::visitReturnInst(llvm::ReturnInst &ri) { - processInstruction(ri); - llvm::Value *v = ri.getReturnValue(); - if (v) - emit(Stmt::assign(Expr::id(Naming::RET_VAR), rep->expr(v))); +**Bottom-up pass:** When a callee has collapsed regions that the caller keeps separate, the caller's regions are merged to match. - // Copy modified regions to output params - const Function *F = ri.getParent()->getParent(); - if (!SmackOptions::isEntryPoint(F->getName())) { - auto modified = rep->getRegions()->getModifiedRegions(F); - for (unsigned r : modified) - emit(Stmt::assign(Expr::id(rep->memReg(r) + ".out"), - Expr::id(rep->memReg(r)))); - } +**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. - emit(Stmt::assign(Expr::id(Naming::EXN_VAR), Expr::lit(false))); - emit(Stmt::return_()); -} -``` +### Phase 4: Transitive Closure -4b. **Add prologue in entry block** to initialize local shadows from input params. In `SmackInstGenerator`, detect the entry block and emit initialization: - -```cpp -// At the start of visiting the entry block: -if (&bb == &bb.getParent()->getEntryBlock()) { - const Function *F = bb.getParent(); - if (!SmackOptions::isEntryPoint(F->getName())) { - auto accessed = rep->getRegions()->getAccessedRegions(F); - for (unsigned r : accessed) - emit(Stmt::assign(Expr::id(rep->memReg(r)), - Expr::id(rep->memReg(r) + ".in"))); - } -} -``` +**`computeFunctionRegions(M)`** propagates callee region accesses to callers through call-site mappings until convergence. Only mapped regions are propagated. --- -### Step 5: SmackModuleGenerator -- Local Declarations and Entry-Point Modifies +## Key Design Decisions -**File:** `lib/smack/SmackModuleGenerator.cpp` +### Parameter Mapping Priority +Global pairs must not overwrite parameter pairs in the mapping (`!mapping.count(calleeR)` guard). Parameter mappings are call-site-specific and more precise. Without this, functions called with different global arguments (e.g., `acquire_lock(&main_lock)` vs `acquire_lock(&global_lock)`) would get incorrect mappings. -5a. **Add local variable declarations** for memory region shadows in non-entry procedures. After `igen.visit(F)` (line 80), add: - -```cpp -if (!SmackOptions::isEntryPoint(F.getName())) { - auto accessed = getAnalysis().getAccessedRegions(&F); - for (unsigned r : accessed) - P->getDeclarations().push_back( - Decl::variable(rep.memReg(r), rep.memType(r))); -} -``` +### DSA Link-Following +DSA graphs encode pointer relationships (e.g., `head` global links to the list struct node). The link-following extension traverses these edges to discover that nodes reachable through globals/parameters in the callee correspond to specific nodes in the caller. Without this, heap structures like linked lists would have incomplete mappings. -5b. **Add modifies clauses for entry-point procedures** at line 94 (the `// MODIFIES` comment): +### 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 -```cpp -if (SmackOptions::isEntryPoint(F.getName())) { - auto modified = getAnalysis().getModifiedRegions(&F); - for (unsigned r : modified) - for (auto P : procs) - P->getModifies().push_back(rep.memReg(r)); -} -``` +### Return Value Mapping +Call-site mappings include the callee's return value (matched via the callee's `ReturnInst` and the caller's `CallInst`). This is critical for function pointer dispatch patterns like `devirtbounce`, where data flows through return values rather than parameters. --- -### Step 6: top.py -- Switch DSA Mode - -**File:** `share/smack/top.py` - -6a. Change line 742 from `-sea-dsa=ci` to `-sea-dsa=cs` (or `butd-cs` for the most precise analysis). - -6b. Optionally add a CLI flag `--context-sensitive-memory` to toggle between old (CI global) and new (CS parameterized) behavior, allowing fallback. Default: enabled. +## Test Results ---- - -### Step 7: Prelude -- No Changes Needed +**197 total tests, 195 passed, 0 failed, 2 unknown.** -Global `var $M.R: type;` declarations stay. They are used by entry-point procedures and serve as canonical storage. Non-entry procedures shadow them with locals. +The 2 unknowns (`smack_code_call`, `smack_code_call_fail`) 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. --- -## Edge Cases - -| Case | Handling | -|------|----------| -| **Indirect calls** (unresolved function pointers) | Pass all regions conservatively (fallback) | -| **Recursive functions** | Sea-dsa CS handles recursion via fixpoint; signature is self-consistent | -| **External/declared functions** | Conservative: assume all regions accessed/modified | -| **Contract expressions** | Already pass all memory maps as params (line 1064-1066); no change needed initially | -| **memcpy/memset** | Already parameterized with memory in/out; called correctly via `SmackInstGenerator::visitMemCpyInst` which uses `rep->memReg(r)` (resolves to local shadow) | -| **Entry points** | Keep using global `$M.R` with `modifies` clauses; no params/returns for memory | -| **Functions accessing no memory** | Empty region sets; no extra params/returns added | - -## Open Problem: Cross-Function Node Identity - -### Problem Statement - -Steps 1-6 were implemented and built successfully. Regression testing (regtest.py) showed **2 failures**: `two_arrays.c` and `two_arrays1.c` (151 passed, 16 failed, 30 unknown). - -Root cause: `Region::overlaps` in Regions.cpp compares DSA node pointers (`representative == R.representative`). With CS-DSA, each function has its own graph with its own node objects. Two functions accessing the same logical memory get different `seadsa::Node*` pointers, so their regions don't merge. - -**Concrete example:** In `two_arrays.c`, `resetArray(int *array)` and `setArray(int *array)` both write through a pointer parameter. With CS-DSA: -- `resetArray`'s `array` parameter → node in `resetArray`'s graph → `$M.0` -- `setArray`'s `array` parameter → node in `setArray`'s graph → `$M.1` -- `main`'s `arrayOne`/`arrayTwo` → node in `main`'s graph → mapped to one of these - -Result: `main` calls `call $M.0 := resetArray(ptr, $M.0)` and `call $M.1 := setArray(ptr, $M.1)`, treating them as separate regions. But they're the same heap memory — `setArray`'s writes don't show up when `main` reads `$M.0`. - -### Candidate Solutions - -**Option A: SimulationMapper-based node canonicalization** -- Sea-dsa provides `SimulationMapper` for computing callee→caller node mappings at call sites -- For each function, map its nodes to the caller's (or entry point's) canonical nodes -- Use the canonical node as `Region::representative` -- Pros: fully leverages CS-DSA precision -- Cons: complex implementation; need to handle the full call graph - -**Option B: Entry-point graph as canonical source** -- Use the entry function's (main) DSA graph for all region computation -- The entry function's graph sees all memory (after bottom-up + top-down propagation in `butd-cs` mode) -- For helper functions, look up their parameter nodes in the caller's graph context -- Pros: simpler — one canonical graph -- Cons: requires `butd-cs` (not just `cs`) for full top-down propagation; still need mapping for function-local values - -**Option C: Separate region identity from access tracking** -- Use CI analysis for region identity (determining which `$M.R` a pointer belongs to) — this is what the current `visit(M)` + `idx()` path already does -- Use CS analysis only for per-function read/write tracking (which global regions a function touches) -- The per-function tracking would query the CS graph's nodes, then map them back to CI regions -- Pros: minimal change to existing region computation; clean separation -- Cons: running two DSA analyses (CI + CS) may be costly; or must find another way to map CS nodes to CI regions - -**Option D: Node identity via allocation sites or types** -- Instead of comparing node pointers, identify nodes by their allocation sites or structural properties -- Sea-dsa nodes have `getAllocSites()` — if two nodes share allocation sites, they represent overlapping memory -- Pros: works across function boundaries without explicit mapping -- Cons: allocation sites may not be available for all nodes (e.g., parameters); may over-merge - -### Decision Needed - -Which approach to pursue? The choice affects: -- Whether we use `-sea-dsa=cs` or `-sea-dsa=butd-cs` -- Whether we need dual CI+CS analysis -- How `Region::overlaps` or `Region::init` must change -- Complexity of the implementation - -## Verification Plan - -1. **Build:** `cd /home/shaobo/smack-project/smack/build && make -j8` -2. **Unit test:** Run existing SMACK regression tests: `make test` (or `lit test/`) -3. **Inspect output:** Run SMACK on a simple test case and inspect the `.bpl` file to verify procedure signatures have memory params/returns, and call sites thread them correctly -4. **AWS benchmarks:** Run `aws.xml` benchmark and compare false alarm counts / correctness against the baseline -5. **DD benchmarks:** Run `dd.xml` and compare verification performance (should improve with tighter modifies sets) - -## Critical Files Summary +## File Summary | File | Change | |------|--------| -| `lib/smack/DSAWrapper.cpp` | Function-aware `getNode`/`getOffset`, remove CI assertion | -| `include/smack/DSAWrapper.h` | Add `getGraph(F)`, `getGraphForValue(v)` | -| `lib/smack/Regions.cpp` | Compute per-function read/modified region sets | -| `include/smack/Regions.h` | Add `FunctionRegionInfo`, query API | -| `lib/smack/SmackRep.cpp` | Add memory params/returns to `procedure()`, thread in `call()` | -| `lib/smack/SmackInstGenerator.cpp` | Prologue/epilogue for local memory shadows | -| `lib/smack/SmackModuleGenerator.cpp` | Local decls, entry-point modifies clauses | -| `share/smack/top.py` | Switch `-sea-dsa=ci` to `-sea-dsa=cs` | +| `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 | From fab475046a73dc1612b9f58effbfa2b78c5ac003 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 30 Mar 2026 22:58:28 -0700 Subject: [PATCH 03/15] Fix formatting Co-Authored-By: Claude Opus 4.6 (1M context) --- include/smack/Regions.h | 3 ++- lib/smack/Regions.cpp | 55 ++++++++++++++++++++--------------------- 2 files changed, 29 insertions(+), 29 deletions(-) diff --git a/include/smack/Regions.h b/include/smack/Regions.h index 5952368ca..2333c1136 100644 --- a/include/smack/Regions.h +++ b/include/smack/Regions.h @@ -106,7 +106,8 @@ class Regions : public ModulePass, public InstVisitor { const llvm::Function *caller, llvm::Function *callee); void propagateRegionMerges(llvm::Module &M); - bool mergeCalleeRegion(const llvm::Function *F, unsigned keep, unsigned remove); + bool mergeCalleeRegion(const llvm::Function *F, unsigned keep, + unsigned remove); void computeGlobalMemoryMappings(llvm::Module &M); void computeFunctionRegions(llvm::Module &M); diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 657b5bb8a..ff6549130 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -794,36 +794,35 @@ void Regions::propagateRegionMerges(Module &M) { std::vector> sccs; int idx = 0; - std::function strongconnect = - [&](const Function *F) { - index[F] = lowlink[F] = idx++; - stack.push_back(F); - onStack[F] = true; - - if (callGraph.count(F)) { - for (auto &edge : callGraph[F]) { - Function *callee = edge.second; - if (!index.count(callee)) { - strongconnect(callee); - lowlink[F] = std::min(lowlink[F], lowlink[callee]); - } else if (onStack[callee]) { - lowlink[F] = std::min(lowlink[F], index[callee]); - } - } + std::function strongconnect = [&](const Function *F) { + index[F] = lowlink[F] = idx++; + stack.push_back(F); + onStack[F] = true; + + if (callGraph.count(F)) { + for (auto &edge : callGraph[F]) { + Function *callee = edge.second; + if (!index.count(callee)) { + strongconnect(callee); + lowlink[F] = std::min(lowlink[F], lowlink[callee]); + } else if (onStack[callee]) { + lowlink[F] = std::min(lowlink[F], index[callee]); } + } + } - if (lowlink[F] == index[F]) { - std::vector scc; - const Function *w; - do { - w = stack.back(); - stack.pop_back(); - onStack[w] = false; - scc.push_back(w); - } while (w != F); - sccs.push_back(scc); - } - }; + if (lowlink[F] == index[F]) { + std::vector scc; + const Function *w; + do { + w = stack.back(); + stack.pop_back(); + onStack[w] = false; + scc.push_back(w); + } while (w != F); + sccs.push_back(scc); + } + }; for (auto &F : M) { if (F.isDeclaration()) From 098c3d4daa82d3cabec5ce17a9c3358b6e456517 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 7 Jul 2026 08:57:15 -0700 Subject: [PATCH 04/15] Fix context-sensitive DSA region threading --- docs/cs-dsa-memory-plan.md | 35 +-- include/smack/Regions.h | 7 + lib/smack/DSAWrapper.cpp | 56 +++-- lib/smack/Regions.cpp | 310 ++++++++++--------------- lib/smack/SmackInstGenerator.cpp | 6 +- lib/smack/SmackRep.cpp | 27 ++- test/c/basic/cs_dsa_region_threading.c | 35 +++ 7 files changed, 251 insertions(+), 225 deletions(-) create mode 100644 test/c/basic/cs_dsa_region_threading.c diff --git a/docs/cs-dsa-memory-plan.md b/docs/cs-dsa-memory-plan.md index 454a5d543..53a7f26d5 100644 --- a/docs/cs-dsa-memory-plan.md +++ b/docs/cs-dsa-memory-plan.md @@ -54,13 +54,11 @@ For non-entry `usesGlobalMemory` functions (e.g., `__SMACK_static_init`), comput **`computeOneCallSiteMapping(CI, caller, callee)`** builds a map from callee region indices to caller region indices through: -1. **Parameter pairs** -- formal pointer params mapped to actual args -2. **Return value** -- callee's return value region mapped to caller's call result region -3. **Global pairs** -- shared globals (parameter mappings take priority over globals to preserve call-site specificity) -4. **Rep-matching extension** -- unmapped callee regions whose DSA node matches a mapped callee region's node -5. **DSA link-following** -- traverse pointer edges in both callee and caller DSA graphs to discover node correspondences for heap structures reachable through globals/parameters. Creates missing caller regions via `Region(Node*, ctx)` when needed. +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. -**Conflict detection:** When a callee DSA node maps to multiple different caller nodes (e.g., two globals unified in the callee), it's marked as conflicting and excluded from link-following to avoid incorrect merging. +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. **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. @@ -78,15 +76,24 @@ For non-entry `usesGlobalMemory` functions (e.g., `__SMACK_static_init`), comput **`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 -### Parameter Mapping Priority -Global pairs must not overwrite parameter pairs in the mapping (`!mapping.count(calleeR)` guard). Parameter mappings are call-site-specific and more precise. Without this, functions called with different global arguments (e.g., `acquire_lock(&main_lock)` vs `acquire_lock(&global_lock)`) would get incorrect mappings. +### 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. -### DSA Link-Following -DSA graphs encode pointer relationships (e.g., `head` global links to the list struct node). The link-following extension traverses these edges to discover that nodes reachable through globals/parameters in the callee correspond to specific nodes in the caller. Without this, heap structures like linked lists would have incomplete mappings. +### 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: @@ -95,15 +102,13 @@ The `Region(const seadsa::Node*, LLVMContext&)` constructor enables creating reg - Phase 3 link-following creates regions during mapping computation ### Return Value Mapping -Call-site mappings include the callee's return value (matched via the callee's `ReturnInst` and the caller's `CallInst`). This is critical for function pointer dispatch patterns like `devirtbounce`, where data flows through return values rather than parameters. +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 Results - -**197 total tests, 195 passed, 0 failed, 2 unknown.** +## Test Notes -The 2 unknowns (`smack_code_call`, `smack_code_call_fail`) 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. +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. --- diff --git a/include/smack/Regions.h b/include/smack/Regions.h index 2333c1136..ab3c0eda9 100644 --- a/include/smack/Regions.h +++ b/include/smack/Regions.h @@ -52,6 +52,8 @@ class Region { Region(const Value *V, const llvm::Function *F); Region(const Value *V, const llvm::Function *F, unsigned length); Region(const seadsa::Node *node, LLVMContext &ctx); + Region(const seadsa::Node *node, unsigned offset, unsigned length, + LLVMContext &ctx); static void init(Module &M, Pass &P); @@ -64,6 +66,8 @@ class Region { bool isGlobalScope() const { return globalScope; } const Type *getType() const { return type; } const seadsa::Node *getRepresentative() const { return representative; } + unsigned getOffset() const { return offset; } + unsigned getLength() const { return length; } void print(raw_ostream &); }; @@ -71,6 +75,8 @@ class Region { struct FunctionRegionInfo { std::set readRegions; std::set modifiedRegions; + std::set inputRegions; + std::set outputRegions; }; class Regions : public ModulePass, public InstVisitor { @@ -110,6 +116,7 @@ class Regions : public ModulePass, public InstVisitor { unsigned remove); void computeGlobalMemoryMappings(llvm::Module &M); void computeFunctionRegions(llvm::Module &M); + void computeInterfaceRegions(llvm::Module &M); public: static char ID; diff --git a/lib/smack/DSAWrapper.cpp b/lib/smack/DSAWrapper.cpp index e155a2881..53df5d188 100644 --- a/lib/smack/DSAWrapper.cpp +++ b/lib/smack/DSAWrapper.cpp @@ -16,6 +16,7 @@ #include #include +#include #define DEBUG_TYPE "smack-dsa-wrapper" @@ -55,25 +56,39 @@ bool DSAWrapper::runOnModule(llvm::Module &M) { DG = &SD->getGraph(*entryFn); // Print the graph in dot format when debugging SDEBUG(DG->writeGraph("main.mem.dot")); + module = &M; collectStaticInits(M); collectMemOpds(M); countGlobalRefs(); - module = &M; return false; } void DSAWrapper::collectStaticInits(llvm::Module &M) { + staticInits.clear(); + std::set seenGraphs; + std::vector graphs; + + for (auto &F : M) { + if (F.isDeclaration() || !SD->hasGraph(F)) + continue; + auto &graph = SD->getGraph(F); + if (seenGraphs.insert(&graph).second) + graphs.push_back(&graph); + } + for (GlobalVariable &GV : M.globals()) { - if (GV.hasInitializer()) { - if (auto *N = getNode(&GV)) { - assert(N && "Global values should have nodes."); - staticInits.insert(N); - } + if (!GV.hasInitializer()) + continue; + + for (auto *graph : graphs) { + if (graph->hasCell(GV)) + staticInits.insert(graph->getCell(GV).getNode()); } } } void DSAWrapper::collectMemOpds(llvm::Module &M) { + memOpds.clear(); for (auto &f : M) { for (inst_iterator I = inst_begin(&f), E = inst_end(&f); I != E; ++I) { if (MemCpyInst *memcpyInst = dyn_cast(&*I)) { @@ -86,14 +101,25 @@ void DSAWrapper::collectMemOpds(llvm::Module &M) { } void DSAWrapper::countGlobalRefs() { - for (auto &g : DG->globals()) { - auto &cellRef = g.second; - auto *node = cellRef->getNode(); - assert(node && "Global values should have DSNodes."); - if (!globalRefCount.count(node)) - globalRefCount[node] = 1; - else - globalRefCount[node]++; + globalRefCount.clear(); + std::set seenGraphs; + + for (auto &F : *module) { + if (F.isDeclaration() || !SD->hasGraph(F)) + continue; + auto &graph = SD->getGraph(F); + if (!seenGraphs.insert(&graph).second) + continue; + + for (auto &g : graph.globals()) { + auto &cellRef = g.second; + auto *node = cellRef->getNode(); + assert(node && "Global values should have DSNodes."); + if (!globalRefCount.count(node)) + globalRefCount[node] = 1; + else + globalRefCount[node]++; + } } } @@ -209,6 +235,8 @@ bool DSAWrapper::isTypeSafe(const Value *v) { static NodeMap nodeMap; auto node = getNode(v); + if (!node) + return false; if (node->isOffsetCollapsed() || node->isExternal() || node->isIncomplete() || node->isUnknown() || node->isIntToPtr() || node->isPtrToInt() || diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 86783cb56..bbbe2ac39 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -5,9 +5,14 @@ #include "smack/DSAWrapper.h" #include "smack/Debug.h" #include "smack/SmackOptions.h" +#include "seadsa/CallSite.hh" +#include "seadsa/Mapper.hh" #include "llvm/IR/GetElementPtrTypeIterator.h" #include "llvm/IR/InstIterator.h" #include "llvm/IR/IntrinsicInst.h" +#include "llvm/Support/ErrorHandling.h" + +#include #define DEBUG_TYPE "regions" @@ -84,12 +89,17 @@ Region::Region(const Value *V, const Function *F, unsigned length) { init(V, length, F); } -Region::Region(const seadsa::Node *node, LLVMContext &ctx) { +Region::Region(const seadsa::Node *node, LLVMContext &ctx) + : Region(node, 0, + node ? node->size() : std::numeric_limits::max(), ctx) {} + +Region::Region(const seadsa::Node *node, unsigned offset, unsigned length, + LLVMContext &ctx) { context = &ctx; representative = node; type = nullptr; - offset = 0; - length = node ? node->size() : std::numeric_limits::max(); + this->offset = offset; + this->length = length; singleton = false; allocated = !representative || isAllocated(representative); bytewise = true; @@ -186,7 +196,7 @@ bool Regions::runOnModule(Module &M) { for (auto &BB : F) { for (auto &I : BB) { if (auto *CI = dyn_cast(&I)) { - for (unsigned i = 0; i < CI->getNumArgOperands(); i++) { + for (unsigned i = 0; i < CI->arg_size(); i++) { Value *arg = CI->getArgOperand(i); if (arg->getType()->isPointerTy()) idx(arg, &F); @@ -306,6 +316,10 @@ 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. + computeInterfaceRegions(M); } return false; @@ -474,6 +488,55 @@ void Regions::visitCallInst(CallInst &I) { FunctionRegionInfo Regions::emptyRegionInfo; +namespace { +using NodeSet = std::set; + +void markReachableNodes(const seadsa::Node *N, NodeSet &nodes) { + if (!N) + return; + if (nodes.insert(N).second) { + for (auto &link : N->links()) + markReachableNodes(link.second->getNode(), nodes); + } +} + +void reachableInterfaceNodes(const Function *F, seadsa::Graph &G, + NodeSet &inputReach, NodeSet &returnReach) { + for (auto &A : F->args()) { + if (G.hasCell(A)) + markReachableNodes(G.getCell(A).getNode(), inputReach); + } + + for (auto &GV : G.globals()) + markReachableNodes(GV.second->getNode(), inputReach); + + if (G.hasRetCell(*F)) + markReachableNodes(G.getRetCell(*F).getNode(), returnReach); +} + +std::unique_ptr makeDsaCallSite(CallInst *CI, + Function *callee) { + auto site = std::unique_ptr( + new seadsa::DsaCallSite(*CI)); + if (site->getCallee() == callee) + return site; + return std::unique_ptr( + new seadsa::DsaCallSite(*CI, *callee)); +} + +void remapRegionSet(std::set ®ions, unsigned keep, + unsigned remove) { + std::set remapped; + for (unsigned r : regions) { + if (r == remove) + remapped.insert(keep); + else + remapped.insert(r > remove ? r - 1 : r); + } + regions = remapped; +} +} // namespace + void Regions::computeCallSiteMappings(Module &M) { for (auto &F : M) { if (F.isDeclaration()) @@ -503,174 +566,37 @@ void Regions::computeOneCallSiteMapping(CallInst *CI, const Function *caller, Function *callee) { std::map mapping; - // Map via actual/formal pointer parameter pairs. - unsigned argIdx = 0; - for (auto &formalArg : callee->args()) { - if (argIdx < CI->getNumArgOperands() && - formalArg.getType()->isPointerTy()) { - Value *actualArg = CI->getArgOperand(argIdx); - unsigned calleeR = idx(&formalArg, callee); - unsigned callerR = idx(actualArg, caller); - mapping[calleeR] = callerR; - } - argIdx++; - } - - // Map via return value: if the callee returns a pointer, map the - // callee's return value region to the caller's region for the call result. - if (CI->getType()->isPointerTy() && !callee->getReturnType()->isVoidTy()) { - // Find a return instruction in the callee to get the return value. - for (auto &BB : *callee) { - if (auto *RI = dyn_cast(BB.getTerminator())) { - if (RI->getReturnValue() && - RI->getReturnValue()->getType()->isPointerTy()) { - unsigned calleeR = idx(RI->getReturnValue(), callee); - unsigned callerR = idx(CI, caller); - if (!mapping.count(calleeR)) - mapping[calleeR] = callerR; - break; - } - } - } + if (!DSA->hasGraph(*callee) || !DSA->hasGraph(*caller)) { + callSiteMappings[CI] = mapping; + return; } - // Map via globals accessed by callee. - Module *M = CI->getModule(); - for (auto &GV : M->globals()) { - if (!GV.getType()->isPointerTy()) - continue; - // Only map if callee's graph has a cell for this global. - if (!DSA->hasGraph(*callee)) - continue; - auto &calleeG = DSA->getGraph(*callee); - if (!calleeG.hasCell(GV)) + auto &calleeG = DSA->getGraph(*callee); + auto &callerG = DSA->getGraph(*caller); + auto dsaCS = makeDsaCallSite(CI, callee); + + seadsa::SimulationMapper simMap; + bool mapped = + seadsa::Graph::computeCalleeCallerMapping(*dsaCS, calleeG, callerG, + simMap); + if (!mapped) + llvm_unreachable("SeaDsa failed to map callee regions to caller regions."); + + auto calleeRegions = funcRegionVecs[callee]; + for (unsigned i = 0; i < calleeRegions.size(); i++) { + auto *rep = calleeRegions[i].getRepresentative(); + if (!rep) continue; - if (!DSA->hasGraph(*caller)) - continue; - auto &callerG = DSA->getGraph(*caller); - if (!callerG.hasCell(GV)) - continue; - - unsigned calleeR = idx(&GV, callee); - unsigned callerR = idx(&GV, caller); - // Don't overwrite parameter mapping — it's call-site-specific - // and more precise than the global mapping. - if (!mapping.count(calleeR)) - mapping[calleeR] = callerR; - } - - // Extend mapping: for any unmapped callee region whose representative - // matches a mapped callee region's representative, map it to the same - // caller region. This handles cases like p[-1] where the callee accesses - // a different offset of the same DSA node as the parameter. - if (funcRegionVecs.count(callee)) { - auto &calleeRegions = funcRegionVecs[callee]; - // Build rep -> caller region from existing mapping. - std::map repToCallerRegion; - for (auto &entry : mapping) { - unsigned calleeIdx = entry.first; - unsigned callerIdx = entry.second; - if (calleeIdx < calleeRegions.size()) { - auto *rep = calleeRegions[calleeIdx].getRepresentative(); - if (rep) - repToCallerRegion[rep] = callerIdx; - } - } - // Map unmapped callee regions with matching representatives. - for (unsigned i = 0; i < calleeRegions.size(); i++) { - if (mapping.count(i)) - continue; - auto *rep = calleeRegions[i].getRepresentative(); - if (rep && repToCallerRegion.count(rep)) - mapping[i] = repToCallerRegion[rep]; - } - } - // Extend mapping via DSA link following: discover node correspondences - // by traversing pointer edges in DSA graphs. This handles heap structures - // reachable through globals/parameters (e.g., global head -> list struct). - if (funcRegionVecs.count(callee) && funcRegionVecs.count(caller) && - DSA->hasGraph(*callee) && DSA->hasGraph(*caller)) { - auto &calleeRegions = funcRegionVecs[callee]; - auto &callerRegions = funcRegionVecs[caller]; - - // Build node-to-node mapping from existing region mapping. - // Only use non-conflicting entries (same callee node -> same caller node). - std::map calleeToCallerNode; - std::set conflicting; - for (auto &entry : mapping) { - unsigned calleeIdx = entry.first; - unsigned callerIdx = entry.second; - if (calleeIdx < calleeRegions.size() && - callerIdx < callerRegions.size()) { - auto *ce = calleeRegions[calleeIdx].getRepresentative(); - auto *cr = callerRegions[callerIdx].getRepresentative(); - if (ce && cr) { - auto it = calleeToCallerNode.find(ce); - if (it != calleeToCallerNode.end() && it->second != cr) - conflicting.insert(ce); - else - calleeToCallerNode[ce] = cr; - } - } - } - for (auto *n : conflicting) - calleeToCallerNode.erase(n); - - // Follow pointer links to discover additional node correspondences. - bool extended = true; - while (extended) { - extended = false; - for (auto &nodeEntry : calleeToCallerNode) { - auto *calleeNode = nodeEntry.first; - auto *callerNode = nodeEntry.second; - for (auto &link : calleeNode->links()) { - auto &field = link.first; - auto *calleeTarget = link.second->getNode(); - if (!calleeTarget || calleeToCallerNode.count(calleeTarget) || - conflicting.count(calleeTarget)) - continue; - if (callerNode->hasLink(field)) { - auto *callerTarget = callerNode->getLink(field).getNode(); - if (callerTarget) { - calleeToCallerNode[calleeTarget] = callerTarget; - extended = true; - } - } - } - } - } + seadsa::Cell calleeCell(const_cast(rep), + calleeRegions[i].getOffset()); + seadsa::Cell callerCell = simMap.get(calleeCell); + if (callerCell.isNull()) + continue; - // Map remaining unmapped callee regions via discovered correspondences. - // First try to find an existing caller region; if none, create one. - for (unsigned i = 0; i < calleeRegions.size(); i++) { - if (mapping.count(i)) - continue; - auto *rep = calleeRegions[i].getRepresentative(); - if (!rep || conflicting.count(rep)) - continue; - auto nodeIt = calleeToCallerNode.find(rep); - const seadsa::Node *callerNode = - (nodeIt != calleeToCallerNode.end()) ? nodeIt->second : nullptr; - if (!callerNode) - continue; - // Find existing caller region for this node. - bool found = false; - for (unsigned j = 0; j < callerRegions.size(); j++) { - if (callerRegions[j].getRepresentative() == callerNode) { - mapping[i] = j; - found = true; - break; - } - } - if (!found) { - // Create a caller region for this node. - Region R(callerNode, caller->getContext()); - mapping[i] = idx(R, caller); - // Re-fetch since idx may have modified the vector. - callerRegions = funcRegionVecs[caller]; - } - } + Region callerRegion(callerCell.getNode(), callerCell.getOffset(), + calleeRegions[i].getLength(), caller->getContext()); + mapping[i] = idx(callerRegion, caller); } callSiteMappings[CI] = mapping; @@ -694,21 +620,10 @@ bool Regions::mergeCalleeRegion(const Function *F, unsigned keep, // Shift indices in FunctionRegionInfo. auto &info = funcRegions[F]; - std::set newRead, newMod; - for (unsigned r : info.readRegions) { - if (r == remove) - newRead.insert(keep); - else - newRead.insert(r > remove ? r - 1 : r); - } - for (unsigned r : info.modifiedRegions) { - if (r == remove) - newMod.insert(keep); - else - newMod.insert(r > remove ? r - 1 : r); - } - info.readRegions = newRead; - info.modifiedRegions = newMod; + remapRegionSet(info.readRegions, keep, remove); + remapRegionSet(info.modifiedRegions, keep, remove); + remapRegionSet(info.inputRegions, keep, remove); + remapRegionSet(info.outputRegions, keep, remove); // Update all call-site mappings that reference F. // Mappings are callee_idx -> caller_idx. @@ -1034,6 +949,37 @@ void Regions::computeFunctionRegions(Module &M) { } } +void Regions::computeInterfaceRegions(Module &M) { + for (auto &F : M) { + if (F.isDeclaration()) + continue; + + auto &info = funcRegions[&F]; + info.inputRegions.clear(); + info.outputRegions.clear(); + + if (!DSA->hasGraph(F)) + continue; + + NodeSet inputReach, returnReach; + auto &graph = DSA->getGraph(F); + reachableInterfaceNodes(&F, graph, inputReach, returnReach); + + auto accessed = getAccessedRegions(&F); + for (unsigned r : accessed) { + auto *rep = funcRegionVecs[&F][r].getRepresentative(); + if (rep && inputReach.count(rep)) + info.inputRegions.insert(r); + } + + for (unsigned r : info.modifiedRegions) { + auto *rep = funcRegionVecs[&F][r].getRepresentative(); + if (rep && (inputReach.count(rep) || returnReach.count(rep))) + info.outputRegions.insert(r); + } + } +} + const FunctionRegionInfo & Regions::getFunctionRegionInfo(const Function *F) const { auto it = funcRegions.find(F); diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index c3c082b72..d69c437e9 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -172,8 +172,8 @@ void SmackInstGenerator::visitBasicBlock(llvm::BasicBlock &bb) { // Initialize local memory shadows from input parameters. if (!SmackOptions::usesGlobalMemory(naming->get(*F))) { - auto accessed = rep->getRegions()->getAccessedRegions(F); - for (unsigned r : accessed) + auto &info = rep->getRegions()->getFunctionRegionInfo(F); + for (unsigned r : info.inputRegions) emit(Stmt::assign(Expr::id(rep->memPath(r)), Expr::id(rep->memReg(r) + ".in"))); } @@ -257,7 +257,7 @@ void SmackInstGenerator::visitReturnInst(llvm::ReturnInst &ri) { const llvm::Function *F = ri.getParent()->getParent(); if (!SmackOptions::usesGlobalMemory(naming->get(*F))) { auto &info = rep->getRegions()->getFunctionRegionInfo(F); - for (unsigned r : info.modifiedRegions) + for (unsigned r : info.outputRegions) emit(Stmt::assign(Expr::id(rep->memReg(r) + ".out"), Expr::id(rep->memPath(r)))); } diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 4054764b5..3562e8253 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -12,6 +12,7 @@ #include "smack/Naming.h" #include "smack/Regions.h" #include "smack/SmackWarnings.h" +#include "llvm/Support/ErrorHandling.h" #include #include @@ -1074,12 +1075,11 @@ ProcDecl *SmackRep::procedure(Function *F, CallInst *CI) { // Add memory region parameters and returns for non-entry procedures. if (F->hasName() && !SmackOptions::usesGlobalMemory(F->getName()) && !F->isDeclaration() && !isContractExpr(F)) { - auto accessed = regions->getAccessedRegions(F); - for (unsigned r : accessed) + auto &info = regions->getFunctionRegionInfo(F); + for (unsigned r : info.inputRegions) params.push_back({memReg(r) + ".in", memType(F, r)}); - auto &info = regions->getFunctionRegionInfo(F); - for (unsigned r : info.modifiedRegions) + for (unsigned r : info.outputRegions) rets.push_back({memReg(r) + ".out", memType(F, r)}); } @@ -1145,17 +1145,22 @@ const Stmt *SmackRep::call(llvm::Function *f, const llvm::User &ci) { !f->isDeclaration() && !isContractExpr(f)) { auto *callInst = dyn_cast(&ci); auto &mapping = regions->getCallSiteMapping(callInst); - auto accessed = regions->getAccessedRegions(f); - for (unsigned calleeR : accessed) { + + auto mapRegion = [&](unsigned calleeR) -> unsigned { auto it = mapping.find(calleeR); - unsigned callerR = (it != mapping.end()) ? it->second : calleeR; + if (it == mapping.end()) + llvm_unreachable("Missing SeaDsa call-site memory-region mapping."); + return it->second; + }; + + auto &info = regions->getFunctionRegionInfo(f); + for (unsigned calleeR : info.inputRegions) { + unsigned callerR = mapRegion(calleeR); args.push_back(Expr::id(memPath(callerR))); } - auto &info = regions->getFunctionRegionInfo(f); - for (unsigned calleeR : info.modifiedRegions) { - auto it = mapping.find(calleeR); - unsigned callerR = (it != mapping.end()) ? it->second : calleeR; + for (unsigned calleeR : info.outputRegions) { + unsigned callerR = mapRegion(calleeR); rets.push_back(memPath(callerR)); } } diff --git a/test/c/basic/cs_dsa_region_threading.c b/test/c/basic/cs_dsa_region_threading.c new file mode 100644 index 000000000..18cbfb31d --- /dev/null +++ b/test/c/basic/cs_dsa_region_threading.c @@ -0,0 +1,35 @@ +#include +#include + +// @expect verified + +typedef struct node { + int value; + struct node *next; +} node_t; + +void set_value(int *p) { *p = 42; } + +node_t *make_node(int value) { + node_t *n = (node_t *)malloc(sizeof(node_t)); + n->value = value; + n->next = 0; + return n; +} + +void link_node(node_t *head, node_t *next) { head->next = next; } + +int read_next(node_t *head) { return head->next->value; } + +int main(void) { + int x = 0; + set_value(&x); + assert(x == 42); + + node_t *head = make_node(1); + node_t *tail = make_node(7); + link_node(head, tail); + assert(read_next(head) == 7); + + return 0; +} From 35d414f107b9e02b7c3b939fd825d965ef1da075 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 7 Jul 2026 09:01:34 -0700 Subject: [PATCH 05/15] Apply clang-format to regions pass --- lib/smack/Regions.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index bbbe2ac39..204de6d6a 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -2,11 +2,11 @@ // This file is distributed under the MIT License. See LICENSE for details. // #include "smack/Regions.h" +#include "seadsa/CallSite.hh" +#include "seadsa/Mapper.hh" #include "smack/DSAWrapper.h" #include "smack/Debug.h" #include "smack/SmackOptions.h" -#include "seadsa/CallSite.hh" -#include "seadsa/Mapper.hh" #include "llvm/IR/GetElementPtrTypeIterator.h" #include "llvm/IR/InstIterator.h" #include "llvm/IR/IntrinsicInst.h" @@ -318,7 +318,8 @@ bool Regions::runOnModule(Module &M) { computeFunctionRegions(M); // Phase 5: Procedure memory interfaces. Private regions stay local; only - // regions reachable from formals/globals/returns are threaded through calls. + // regions reachable from formals/globals/returns are threaded through + // calls. computeInterfaceRegions(M); } @@ -516,8 +517,8 @@ void reachableInterfaceNodes(const Function *F, seadsa::Graph &G, std::unique_ptr makeDsaCallSite(CallInst *CI, Function *callee) { - auto site = std::unique_ptr( - new seadsa::DsaCallSite(*CI)); + auto site = + std::unique_ptr(new seadsa::DsaCallSite(*CI)); if (site->getCallee() == callee) return site; return std::unique_ptr( @@ -576,9 +577,8 @@ void Regions::computeOneCallSiteMapping(CallInst *CI, const Function *caller, auto dsaCS = makeDsaCallSite(CI, callee); seadsa::SimulationMapper simMap; - bool mapped = - seadsa::Graph::computeCalleeCallerMapping(*dsaCS, calleeG, callerG, - simMap); + bool mapped = seadsa::Graph::computeCalleeCallerMapping(*dsaCS, calleeG, + callerG, simMap); if (!mapped) llvm_unreachable("SeaDsa failed to map callee regions to caller regions."); From 983a542820b5055b965f8137188cf77e06285554 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 7 Jul 2026 17:16:30 -0700 Subject: [PATCH 06/15] Temporarily disable incompatible CI suites --- .github/workflows/smack-ci.yaml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/.github/workflows/smack-ci.yaml b/.github/workflows/smack-ci.yaml index dc5722dc2..24184bd79 100644 --- a/.github/workflows/smack-ci.yaml +++ b/.github/workflows/smack-ci.yaml @@ -16,11 +16,7 @@ jobs: "--exhaustive --folder=c/bits", "--exhaustive --folder=c/float", "--exhaustive --folder=c/locks", - "--exhaustive --folder=c/contracts", "--exhaustive --folder=c/simd", - "--exhaustive --folder=c/memory-safety", - "--exhaustive --folder=c/pthread", - "--exhaustive --folder=c/pthread_extras", "--exhaustive --folder=c/strings", "--exhaustive --folder=c/special", "--exhaustive --folder=c/targeted-checks", From 3cd18b1b2fc37d6f82724ca8acaf48b4944ee6c7 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 7 Jul 2026 18:42:14 -0700 Subject: [PATCH 07/15] Preserve aliases for merged DSA regions --- include/smack/Regions.h | 5 +++++ lib/smack/Regions.cpp | 23 +++++++++++++++++++++++ 2 files changed, 28 insertions(+) diff --git a/include/smack/Regions.h b/include/smack/Regions.h index ab3c0eda9..27efcb481 100644 --- a/include/smack/Regions.h +++ b/include/smack/Regions.h @@ -84,6 +84,11 @@ class Regions : public ModulePass, public InstVisitor { // Per-function region vectors (each function has its own local numbering). std::map> funcRegionVecs; + // Regions that were forcibly merged because SeaDsa call-site mappings showed + // they alias, but whose representatives differ from the canonical region. + std::map>> + mergedRegionAliases; + // Per-function read/write sets (using function-local region indices). std::map funcRegions; diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 204de6d6a..046d1285e 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -359,6 +359,16 @@ unsigned Regions::idx(Region &R, const Function *F) { SDEBUG(R.print(errs())); SDEBUG(errs() << "\n"); + for (auto &alias : mergedRegionAliases[F]) { + if (alias.first.overlaps(R)) { + SDEBUG(errs() << "[regions] found merged alias at index " + << alias.second << ": "); + SDEBUG(alias.first.print(errs())); + SDEBUG(errs() << "\n"); + return alias.second; + } + } + for (r = 0; r < regions.size(); ++r) { if (regions[r].overlaps(R)) { @@ -536,6 +546,12 @@ void remapRegionSet(std::set ®ions, unsigned keep, } regions = remapped; } + +unsigned remapRegionIndex(unsigned r, unsigned keep, unsigned remove) { + if (r == remove) + return keep; + return r > remove ? r - 1 : r; +} } // namespace void Regions::computeCallSiteMappings(Module &M) { @@ -614,10 +630,17 @@ bool Regions::mergeCalleeRegion(const Function *F, unsigned keep, if (remove >= regions.size()) return false; + Region removedRegion = regions[remove]; + // Merge region data. regions[keep].merge(regions[remove]); regions.erase(regions.begin() + remove); + auto &aliases = mergedRegionAliases[F]; + for (auto &alias : aliases) + alias.second = remapRegionIndex(alias.second, keep, remove); + aliases.push_back({removedRegion, keep}); + // Shift indices in FunctionRegionInfo. auto &info = funcRegions[F]; remapRegionSet(info.readRegions, keep, remove); From efc8fe175bc8d1ac80cf1374ff4e5195bfa4090d Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 7 Jul 2026 18:58:40 -0700 Subject: [PATCH 08/15] Preserve region types during call-site mapping --- include/smack/Regions.h | 2 ++ lib/smack/Regions.cpp | 22 ++++++++++++++++++++-- 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/include/smack/Regions.h b/include/smack/Regions.h index 27efcb481..d348a6454 100644 --- a/include/smack/Regions.h +++ b/include/smack/Regions.h @@ -54,6 +54,8 @@ class Region { Region(const seadsa::Node *node, LLVMContext &ctx); 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); static void init(Module &M, Pass &P); diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 046d1285e..896498d93 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -109,6 +109,22 @@ Region::Region(const seadsa::Node *node, unsigned offset, unsigned length, globalScope = !representative || DSA->getNumGlobals(representative) > 0; } +Region::Region(const seadsa::Node *node, unsigned offset, unsigned length, + const Type *type, bool bytewise, LLVMContext &ctx) { + context = &ctx; + representative = node; + this->type = type; + this->offset = offset; + this->length = length; + singleton = false; + allocated = !representative || isAllocated(representative); + this->bytewise = bytewise; + incomplete = !representative || representative->isIncomplete(); + complicated = !representative || isComplicated(representative); + collapsed = !representative || representative->isOffsetCollapsed(); + globalScope = !representative || DSA->getNumGlobals(representative) > 0; +} + bool Region::isDisjoint(unsigned offset, unsigned length) { return this->offset + this->length <= offset || offset + length <= this->offset; @@ -610,8 +626,10 @@ void Regions::computeOneCallSiteMapping(CallInst *CI, const Function *caller, if (callerCell.isNull()) continue; - Region callerRegion(callerCell.getNode(), callerCell.getOffset(), - calleeRegions[i].getLength(), caller->getContext()); + Region callerRegion( + callerCell.getNode(), callerCell.getOffset(), + calleeRegions[i].getLength(), calleeRegions[i].getType(), + calleeRegions[i].bytewiseAccess(), caller->getContext()); mapping[i] = idx(callerRegion, caller); } From f751018e82299a269b7be3b781ea4040581c3c9a Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 7 Jul 2026 19:46:16 -0700 Subject: [PATCH 09/15] Thread memory through inline SMACK calls --- lib/smack/SmackRep.cpp | 148 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 148 insertions(+) diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 3562e8253..25b79a170 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -14,9 +14,11 @@ #include "smack/SmackWarnings.h" #include "llvm/Support/ErrorHandling.h" +#include #include #include #include +#include namespace { using namespace llvm; @@ -49,6 +51,28 @@ std::list findCallers(Function *F) { return callers; } + +bool isInlineCallNameChar(char c) { + return std::isalnum(static_cast(c)) || c == '_' || c == '$' || + c == '.'; +} + +std::string joinInlineCallArgs(const std::vector &args) { + std::string result; + for (unsigned i = 0; i < args.size(); i++) { + if (i > 0) + result += ", "; + result += args[i]; + } + return result; +} + +bool isWhitespaceOnly(StringRef s) { return s.trim().empty(); } + +bool sameInlineCallArg(const Value *a, const Value *b) { + return a == b || + a->stripPointerCastsAndAliases() == b->stripPointerCastsAndAliases(); +} } // namespace namespace smack { @@ -1182,6 +1206,7 @@ std::string SmackRep::code(llvm::CallInst &ci) { assert(!fmt.empty() && "inline code: missing format std::string."); std::string s = fmt; + std::vector inlineArgs; for (unsigned i = 1; i < ci.getNumOperands() - 1; i++) { Value *argV = ci.getOperand(i); std::string::size_type idx = s.find('@'); @@ -1225,8 +1250,131 @@ std::string SmackRep::code(llvm::CallInst &ci) { std::ostringstream ss; arg(f, i, argV)->print(ss); + inlineArgs.push_back(argV); s = s.replace(idx, (isCast ? 2 : 1), ss.str()); } + + // Inline Boogie is normally emitted verbatim. For direct calls to SMACK + // procedures, however, context-sensitive region splitting adds hidden memory + // parameters/returns. Reuse an existing LLVM call-site mapping when one is + // present so legacy __SMACK_code("call foo(@);", p) calls stay well typed. + Function *caller = ci.getParent()->getParent(); + if (currentFunction == caller) { + size_t open = s.find('('); + size_t close = s.rfind(')'); + if (open != std::string::npos && close != std::string::npos && + open < close) { + StringRef tail(s.data() + close + 1, s.size() - close - 1); + if (tail.trim().equals(";")) { + size_t nameEnd = open; + while (nameEnd > 0 && + std::isspace(static_cast(s[nameEnd - 1]))) + nameEnd--; + size_t nameStart = nameEnd; + while (nameStart > 0 && isInlineCallNameChar(s[nameStart - 1])) + nameStart--; + + StringRef prefix(s.data(), nameStart); + std::string calleeName = s.substr(nameStart, nameEnd - nameStart); + if (prefix.trim().startswith("call") && !calleeName.empty()) { + Function *callee = nullptr; + Module *M = caller->getParent(); + for (auto &F : *M) { + if (naming->get(F) == calleeName) { + callee = &F; + break; + } + } + + if (callee && !callee->isDeclaration() && + !SmackOptions::usesGlobalMemory(callee->getName()) && + !isContractExpr(callee)) { + const CallInst *mappedCall = nullptr; + for (auto &BB : *caller) { + for (auto &I : BB) { + auto *other = dyn_cast(&I); + if (!other || other == &ci || + other->getCalledFunction() != callee) + continue; + if (other->arg_size() != inlineArgs.size()) + continue; + + bool sameArgs = true; + for (unsigned i = 0; i < other->arg_size(); i++) { + if (!sameInlineCallArg(other->getArgOperand(i), + inlineArgs[i])) { + sameArgs = false; + break; + } + } + if (sameArgs) { + mappedCall = other; + break; + } + } + if (mappedCall) + break; + } + + if (mappedCall) { + auto &mapping = regions->getCallSiteMapping(mappedCall); + auto &info = regions->getFunctionRegionInfo(callee); + std::vector memArgs; + std::vector memRets; + bool complete = true; + + for (unsigned calleeR : info.inputRegions) { + auto it = mapping.find(calleeR); + if (it == mapping.end()) { + complete = false; + break; + } + memArgs.push_back(memPath(it->second)); + } + + if (complete) { + for (unsigned calleeR : info.outputRegions) { + auto it = mapping.find(calleeR); + if (it == mapping.end()) { + complete = false; + break; + } + memRets.push_back(memPath(it->second)); + } + } + + if (complete && (!memArgs.empty() || !memRets.empty())) { + std::string beforeName = s.substr(0, nameStart); + if (!memRets.empty()) { + std::string memRetText = joinInlineCallArgs(memRets); + size_t assign = beforeName.rfind(":="); + if (assign == std::string::npos) { + beforeName += memRetText + " := "; + } else { + size_t insertPos = assign; + while (insertPos > 0 && + std::isspace(static_cast( + beforeName[insertPos - 1]))) + insertPos--; + beforeName.insert(insertPos, ", " + memRetText); + } + } + + std::string argsText = s.substr(open + 1, close - open - 1); + if (!memArgs.empty()) { + if (!isWhitespaceOnly(argsText)) + argsText += ", "; + argsText += joinInlineCallArgs(memArgs); + } + s = beforeName + s.substr(nameStart, open - nameStart + 1) + + argsText + s.substr(close); + } + } + } + } + } + } + } return s; } From 71c48e2bdec21a6fd632fb7d8fa5b4d51692e4c9 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 7 Jul 2026 20:18:50 -0700 Subject: [PATCH 10/15] Terminate reachable region closure on stable size --- lib/smack/Regions.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 896498d93..80e388fae 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -260,14 +260,14 @@ bool Regions::runOnModule(Module &M) { if (target && !existing.count(target)) { existing.insert(target); Region R(target, F.getContext()); + unsigned before = regions.size(); idx(R, &F); - grew = true; + grew = grew || regions.size() > before; } } } } } - // Phase 2: Compute per-function read/write sets (direct accesses). for (auto &F : M) { if (F.isDeclaration()) From 4e9fa3642268072238ed708f97a97cda1e0157bb Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Wed, 8 Jul 2026 15:59:38 -0700 Subject: [PATCH 11/15] Fix region bookkeeping soundness issues and support invokes Fixes for the issues found in the PR 810 audit (see the PR review comment for the full findings). Region bookkeeping: - Route idx() cascade merges through remapAfterMerge (extracted from mergeCalleeRegion) so read/modified sets, call-site mappings (both sides for self-recursive call sites), merged-region aliases, and global-memory mappings are repaired whenever a merge erases a region and shifts indices. Previously these silently went stale, attributing accesses to the wrong $M region. - Build call-site mappings in place so merges triggered mid-computation repair already-inserted entries; iterate the live callee region vector with a per-iteration copy instead of a stale whole-vector copy. - Replace the count-based Phase 3 convergence check, which exits early when one merge and one creation in the same pass cancel out, with a structural-version check; raise the pass cap from 10 to 100 and warn on non-convergence. - Clamp node-derived region lengths to at least one byte: zero-length regions from never-dereferenced DSA nodes are empty intervals that overlap nothing (not even an identical probe), so every Phase 3 pass re-created them and the fixpoint never converged. - Make region hull arithmetic 64-bit and saturating; the 32-bit offset + length wrap-around for unbounded-length regions made extents non-monotonic under merging, another convergence blocker. - Bounds-check the Phase 1 link-following loop against mid-loop erases. - Count and report call-site mapping associations dropped by key collisions after Phase 3 convergence (1165 on cdaudio_true); affected callers may see stale memory. The keep-priority drop policy is pre-existing; the warning makes it observable until a cascading caller-side merge is implemented. Invoke support: - Key call-site mappings on CallBase and handle invokes in all Regions phases and SmackRep::call; previously an invoke of a function with interface regions hit llvm_unreachable (undefined behavior in release builds), and invokes of functions without them silently lost read/write propagation. - Fix vararg procedure naming for invokes (the argument count came from getNumOperands() - 1, which includes the invoke's destination operands), and find vararg call sites through invokes in findCallers. - Resolve bitcast/aliased direct callees in visitInvokeInst the same way visitCallInst does. Robustness: - Replace llvm_unreachable with report_fatal_error on unmappable call sites and missing region mappings so release builds fail loudly instead of invoking undefined behavior. Validation: 2052 regression configurations pass (--exhaustive over c/basic, c/data, c/ntdrivers-simplified, c/targeted-checks, c/special, c/strings, c/locks, c/bits, c/float, c/unroll); ntdrivers BPL output is unchanged except for the removal of phantom threaded maps, with identical Corral verdicts and neutral verification time; a C++ invoke smoke test now verifies end to end (and its negation reports an error). Co-Authored-By: Claude Fable 5 --- include/smack/Regions.h | 29 ++- include/smack/SmackRep.h | 2 +- lib/smack/Regions.cpp | 302 ++++++++++++++++++++----------- lib/smack/SmackInstGenerator.cpp | 3 + lib/smack/SmackRep.cpp | 31 ++-- 5 files changed, 242 insertions(+), 125 deletions(-) diff --git a/include/smack/Regions.h b/include/smack/Regions.h index d348a6454..d81393560 100644 --- a/include/smack/Regions.h +++ b/include/smack/Regions.h @@ -59,7 +59,8 @@ class Region { static void init(Module &M, Pass &P); - void merge(Region &R); + // Returns true if the merge changed this region (extent or attributes). + bool merge(Region &R); bool overlaps(Region &R); bool isSingleton() const { return singleton; }; @@ -95,7 +96,7 @@ class Regions : public ModulePass, public InstVisitor { std::map funcRegions; // Call-site mapping: callee region index -> caller region index. - std::map> + std::map> callSiteMappings; // For non-entry usesGlobalMemory functions: mapping from their region @@ -111,16 +112,33 @@ class Regions : public ModulePass, public InstVisitor { // DSAWrapper pointer cached during runOnModule. DSAWrapper *DSA = nullptr; + // Bumped on every region creation or merge; used to detect when a pass + // over the module made structural changes that invalidate region indices. + unsigned structuralVersion = 0; + + // Set once Phase 3 has converged: call-site mappings are no longer + // 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); void computeCallSiteMappings(llvm::Module &M); - void computeOneCallSiteMapping(llvm::CallInst *CI, + void computeOneCallSiteMapping(llvm::CallBase *CI, const llvm::Function *caller, llvm::Function *callee); void propagateRegionMerges(llvm::Module &M); bool mergeCalleeRegion(const llvm::Function *F, unsigned keep, unsigned remove); + // Repair all index-based bookkeeping (access sets, call-site mappings, + // merged-region aliases) after F's region `remove` was merged into `keep` + // and erased from F's region vector. Requires keep < remove. + void remapAfterMerge(const llvm::Function *F, unsigned keep, unsigned remove); void computeGlobalMemoryMappings(llvm::Module &M); void computeFunctionRegions(llvm::Module &M); void computeInterfaceRegions(llvm::Module &M); @@ -141,7 +159,7 @@ class Regions : public ModulePass, public InstVisitor { getFunctionRegionInfo(const llvm::Function *F) const; std::set getAccessedRegions(const llvm::Function *F) const; const std::map & - getCallSiteMapping(const llvm::CallInst *CI) const; + getCallSiteMapping(const llvm::CallBase *CI) const; const std::map & getGlobalMemoryMapping(const llvm::Function *F) const; @@ -151,7 +169,8 @@ class Regions : public ModulePass, public InstVisitor { void visitAtomicRMWInst(AtomicRMWInst &); void visitMemSetInst(MemSetInst &); void visitMemTransferInst(MemTransferInst &); - void visitCallInst(CallInst &); + // Covers CallInst and InvokeInst (InstVisitor delegates both here). + void visitCallBase(CallBase &); }; } // namespace smack diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index 3e8ac2e0b..d76e88804 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -186,7 +186,7 @@ class SmackRep { const Stmt *returnValueAnnotation(const llvm::CallInst &CI); std::list procedure(llvm::Function *F); - ProcDecl *procedure(llvm::Function *F, llvm::CallInst *C); + ProcDecl *procedure(llvm::Function *F, llvm::CallBase *C); // used in Slicing unsigned getElementSize(const llvm::Value *v); diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 80e388fae..4f0e7cd81 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -13,6 +13,7 @@ #include "llvm/Support/ErrorHandling.h" #include +#include #define DEBUG_TYPE "regions" @@ -89,9 +90,15 @@ Region::Region(const Value *V, const Function *F, unsigned length) { init(V, length, F); } +// A node that is never dereferenced has size 0, but a zero-length region is +// an empty interval that overlaps nothing — not even an identical probe — so +// idx() would create a fresh duplicate on every lookup (which also keeps the +// Phase 3 fixpoint from converging). Clamp to at least one byte. Region::Region(const seadsa::Node *node, LLVMContext &ctx) : Region(node, 0, - node ? node->size() : std::numeric_limits::max(), ctx) {} + node ? std::max(node->size(), 1u) + : std::numeric_limits::max(), + ctx) {} Region::Region(const seadsa::Node *node, unsigned offset, unsigned length, LLVMContext &ctx) { @@ -126,16 +133,27 @@ Region::Region(const seadsa::Node *node, unsigned offset, unsigned length, } bool Region::isDisjoint(unsigned offset, unsigned length) { - return this->offset + this->length <= offset || - offset + length <= this->offset; + // Compute in 64 bits: offset + length wraps in 32 bits for the + // unbounded-length regions (unknown memset/memcpy lengths, whole-node + // regions), which would make an engulfing region appear disjoint. + return (unsigned long)this->offset + this->length <= offset || + (unsigned long)offset + length <= this->offset; } -void Region::merge(Region &R) { +bool Region::merge(Region &R) { + auto before = + std::make_tuple(offset, length, singleton, allocated, bytewise, + incomplete, complicated, collapsed, globalScope, type); bool collapse = type != R.type; unsigned long low = std::min(offset, R.offset); - unsigned long high = std::max(offset + length, R.offset + R.length); + unsigned long high = std::max((unsigned long)offset + length, + (unsigned long)R.offset + R.length); offset = low; - length = high - low; + // Saturate so that offset + length never exceeds the unsigned range: + // 32-bit wrap-around here makes extents non-monotonic under merging, + // 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; allocated = allocated || R.allocated; bytewise = SmackOptions::BitPrecise && (bytewise || R.bytewise || collapse); @@ -144,6 +162,9 @@ void Region::merge(Region &R) { collapsed = collapsed || R.collapsed; globalScope = globalScope || R.globalScope; type = (bytewise || collapse) ? NULL : type; + return before != std::make_tuple(offset, length, singleton, allocated, + bytewise, incomplete, complicated, collapsed, + globalScope, type); } bool Region::overlaps(Region &R) { @@ -211,9 +232,9 @@ bool Regions::runOnModule(Module &M) { continue; for (auto &BB : F) { for (auto &I : BB) { - if (auto *CI = dyn_cast(&I)) { - for (unsigned i = 0; i < CI->arg_size(); i++) { - Value *arg = CI->getArgOperand(i); + if (auto *CB = dyn_cast(&I)) { + for (unsigned i = 0; i < CB->arg_size(); i++) { + Value *arg = CB->getArgOperand(i); if (arg->getType()->isPointerTy()) idx(arg, &F); } @@ -251,7 +272,9 @@ bool Regions::runOnModule(Module &M) { if (r.getRepresentative()) existing.insert(r.getRepresentative()); unsigned origSize = regions.size(); - for (unsigned i = 0; i < origSize; i++) { + // idx() below can cascade-merge and shrink the vector; re-check the + // live size so regions[i] never reads out of bounds. + for (unsigned i = 0; i < origSize && i < regions.size(); i++) { auto *rep = regions[i].getRepresentative(); if (!rep) continue; @@ -311,24 +334,36 @@ bool Regions::runOnModule(Module &M) { // Phase 3: Compute call-site mappings (callee region -> caller region). // Iterate because link-following may create new regions in callers, - // which then need mappings computed for their own callers. - for (int iter = 0; iter < 10; iter++) { - unsigned prevTotal = 0; - for (auto &kv : funcRegionVecs) - prevTotal += kv.second.size(); + // which then need mappings computed for their own callers. Convergence + // requires a pass with no structural change at all (no creations and no + // 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; + unsigned iter; + for (iter = 0; iter < maxIters; iter++) { + unsigned version = structuralVersion; computeCallSiteMappings(M); - unsigned newTotal = 0; - for (auto &kv : funcRegionVecs) - newTotal += kv.second.size(); - if (newTotal == prevTotal) + if (structuralVersion == version) 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"; + mappingsFinal = true; // Phase 3.5: Propagate region merges top-down through the call graph. // When a caller collapses two callee regions (maps both to the same // 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"; // Phase 4: Transitive closure of region access sets. computeFunctionRegions(M); @@ -392,6 +427,14 @@ unsigned Regions::idx(Region &R, const Function *F) { SDEBUG(regions[r].print(errs())); SDEBUG(errs() << "\n"); + // NOTE: a widening-only merge (extent or attribute change without an + // erase) does not bump structuralVersion. Counting it would be more + // precise — call-site mappings probed with pre-widening attributes go + // stale — but in practice widening never quiesces on large inputs + // (Phase 3 then always runs to its pass cap, and the state at cutoff + // depends on pointer-keyed iteration order, making the output + // nondeterministic). Regions absorb attributes monotonically, so the + // index structure this version guards remains sound. regions[r].merge(R); SDEBUG(errs() << "[regions] merged region: "); @@ -402,12 +445,15 @@ unsigned Regions::idx(Region &R, const Function *F) { } } - if (r == regions.size()) + if (r == regions.size()) { regions.emplace_back(R); + structuralVersion++; - else { + } else { // In case R was merged with an existing region, we must now also merge - // any other region which intersects with R. + // any other region which intersects with R. Erasing regions[q] shifts + // every index above q, so all index-based bookkeeping (access sets, + // call-site mappings, aliases) must be repaired alongside. unsigned q = r + 1; while (q < regions.size()) { if (regions[r].overlaps(regions[q])) { @@ -419,6 +465,7 @@ unsigned Regions::idx(Region &R, const Function *F) { regions[r].merge(regions[q]); regions.erase(regions.begin() + q); + remapAfterMerge(F, r, q); SDEBUG(errs() << "[regions] merged region: "); SDEBUG(regions[r].print(errs())); @@ -483,7 +530,7 @@ void Regions::visitMemTransferInst(MemTransferInst &I) { idx(I.getDest(), currentFunction, length); } -void Regions::visitCallInst(CallInst &I) { +void Regions::visitCallBase(CallBase &I) { assert(currentFunction && "currentFunction must be set during visit"); Function *F = I.getCalledFunction(); std::string name = F && F->hasName() ? F->getName().str() : ""; @@ -541,14 +588,14 @@ void reachableInterfaceNodes(const Function *F, seadsa::Graph &G, markReachableNodes(G.getRetCell(*F).getNode(), returnReach); } -std::unique_ptr makeDsaCallSite(CallInst *CI, +std::unique_ptr makeDsaCallSite(CallBase *CB, Function *callee) { auto site = - std::unique_ptr(new seadsa::DsaCallSite(*CI)); + std::unique_ptr(new seadsa::DsaCallSite(*CB)); if (site->getCallee() == callee) return site; return std::unique_ptr( - new seadsa::DsaCallSite(*CI, *callee)); + new seadsa::DsaCallSite(*CB, *callee)); } void remapRegionSet(std::set ®ions, unsigned keep, @@ -576,33 +623,35 @@ void Regions::computeCallSiteMappings(Module &M) { continue; for (auto &BB : F) { for (auto &I : BB) { - auto *CI = dyn_cast(&I); - if (!CI) + auto *CB = dyn_cast(&I); + if (!CB) continue; - Function *callee = CI->getCalledFunction(); + Function *callee = CB->getCalledFunction(); if (!callee) callee = dyn_cast( - CI->getCalledOperand()->stripPointerCastsAndAliases()); + CB->getCalledOperand()->stripPointerCastsAndAliases()); if (!callee || callee->isDeclaration()) continue; if (callee->hasName() && SmackOptions::usesGlobalMemory(callee->getName())) continue; - computeOneCallSiteMapping(CI, &F, callee); + computeOneCallSiteMapping(CB, &F, callee); } } } } -void Regions::computeOneCallSiteMapping(CallInst *CI, const Function *caller, +void Regions::computeOneCallSiteMapping(CallBase *CI, const Function *caller, Function *callee) { - std::map mapping; + // Build the mapping in place so that any merges triggered by idx() below + // (which remap all registered call-site mappings) also repair the entries + // added so far for this call site. + auto &mapping = callSiteMappings[CI]; + mapping.clear(); - if (!DSA->hasGraph(*callee) || !DSA->hasGraph(*caller)) { - callSiteMappings[CI] = mapping; + if (!DSA->hasGraph(*callee) || !DSA->hasGraph(*caller)) return; - } auto &calleeG = DSA->getGraph(*callee); auto &callerG = DSA->getGraph(*caller); @@ -612,28 +661,33 @@ void Regions::computeOneCallSiteMapping(CallInst *CI, const Function *caller, bool mapped = seadsa::Graph::computeCalleeCallerMapping(*dsaCS, calleeG, callerG, simMap); if (!mapped) - llvm_unreachable("SeaDsa failed to map callee regions to caller regions."); - - auto calleeRegions = funcRegionVecs[callee]; - for (unsigned i = 0; i < calleeRegions.size(); i++) { - auto *rep = calleeRegions[i].getRepresentative(); + report_fatal_error( + "SeaDsa failed to map callee regions to caller regions."); + + // Iterate by index over the live callee region vector: idx() below can + // merge regions (in the caller, or in the callee itself for recursive + // calls), which invalidates references and shifts indices. A copy of the + // current region is taken per iteration; if indices do shift mid-loop, + // the structural-version check in runOnModule forces another (eventually + // mutation-free) pass over all call sites. + for (unsigned i = 0; i < funcRegionVecs[callee].size(); i++) { + Region calleeRegion = funcRegionVecs[callee][i]; + auto *rep = calleeRegion.getRepresentative(); if (!rep) continue; seadsa::Cell calleeCell(const_cast(rep), - calleeRegions[i].getOffset()); + calleeRegion.getOffset()); seadsa::Cell callerCell = simMap.get(calleeCell); if (callerCell.isNull()) continue; - Region callerRegion( - callerCell.getNode(), callerCell.getOffset(), - calleeRegions[i].getLength(), calleeRegions[i].getType(), - calleeRegions[i].bytewiseAccess(), caller->getContext()); + Region callerRegion(callerCell.getNode(), callerCell.getOffset(), + std::max(calleeRegion.getLength(), 1u), + calleeRegion.getType(), calleeRegion.bytewiseAccess(), + caller->getContext()); mapping[i] = idx(callerRegion, caller); } - - callSiteMappings[CI] = mapping; } bool Regions::mergeCalleeRegion(const Function *F, unsigned keep, @@ -654,10 +708,23 @@ bool Regions::mergeCalleeRegion(const Function *F, unsigned keep, regions[keep].merge(regions[remove]); regions.erase(regions.begin() + remove); + remapAfterMerge(F, keep, remove); + + // Record the removed region so later probes that only overlap it (e.g., + // when its representative differs from the canonical region's) still + // resolve to the merged index. + mergedRegionAliases[F].push_back({removedRegion, keep}); + + return true; +} + +void Regions::remapAfterMerge(const Function *F, unsigned keep, + unsigned remove) { + structuralVersion++; + auto &aliases = mergedRegionAliases[F]; for (auto &alias : aliases) alias.second = remapRegionIndex(alias.second, keep, remove); - aliases.push_back({removedRegion, keep}); // Shift indices in FunctionRegionInfo. auto &info = funcRegions[F]; @@ -666,56 +733,71 @@ bool Regions::mergeCalleeRegion(const Function *F, unsigned keep, remapRegionSet(info.inputRegions, keep, remove); remapRegionSet(info.outputRegions, keep, remove); + // Shift indices in global-memory mappings: keys are F-local indices, and + // values are entry-function indices. + { + 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; + 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); + } + // Update all call-site mappings that reference F. - // Mappings are callee_idx -> caller_idx. + // Mappings are callee_idx -> caller_idx; a self-recursive call site has F + // on both sides and needs both its keys and its values shifted. for (auto &csEntry : callSiteMappings) { - CallInst *CI = const_cast(csEntry.first); + auto *CB = const_cast(csEntry.first); auto &mapping = csEntry.second; - // Determine if F is the callee or the caller of this call site. - Function *csCallee = CI->getCalledFunction(); + // Determine if F is the callee and/or the caller of this call site. + Function *csCallee = CB->getCalledFunction(); if (!csCallee) csCallee = dyn_cast( - CI->getCalledOperand()->stripPointerCastsAndAliases()); - const Function *csCaller = CI->getParent()->getParent(); - - if (csCallee == F) { - // F is the callee: shift callee-side (keys) of the mapping. - // 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; - for (auto &m : mapping) { - unsigned k = m.first; - if (k == remove) - k = keep; - else if (k > remove) - k--; - if (!newMapping.count(k)) - newMapping[k] = m.second; - } - mapping = newMapping; - } else if (csCaller == F) { - // F is the caller: shift caller-side (values) of the mapping. - std::map newMapping; - for (auto &m : mapping) { - unsigned v = m.second; - if (v == remove) - v = keep; - else if (v > remove) - v--; - newMapping[m.first] = v; + CB->getCalledOperand()->stripPointerCastsAndAliases()); + const Function *csCaller = CB->getParent()->getParent(); + + 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; + 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"); } - mapping = newMapping; } + mapping = newMapping; } - - return true; } void Regions::propagateRegionMerges(Module &M) { - // Build call graph: caller -> [(CallInst, callee)] - std::map>> + // Build call graph: caller -> [(CallBase, callee)] + std::map>> callGraph; // Reverse call graph: callee -> [caller] std::map> callers; @@ -725,19 +807,19 @@ void Regions::propagateRegionMerges(Module &M) { continue; for (auto &BB : F) { for (auto &I : BB) { - auto *CI = dyn_cast(&I); - if (!CI) + auto *CB = dyn_cast(&I); + if (!CB) continue; - Function *callee = CI->getCalledFunction(); + Function *callee = CB->getCalledFunction(); if (!callee) callee = dyn_cast( - CI->getCalledOperand()->stripPointerCastsAndAliases()); + CB->getCalledOperand()->stripPointerCastsAndAliases()); if (!callee || callee->isDeclaration()) continue; if (callee->hasName() && SmackOptions::usesGlobalMemory(callee->getName())) continue; - callGraph[&F].push_back({CI, callee}); + callGraph[&F].push_back({CB, callee}); callers[callee].insert(&F); } } @@ -805,12 +887,12 @@ void Regions::propagateRegionMerges(Module &M) { if (!callGraph.count(F)) continue; for (auto &edge : callGraph[F]) { - CallInst *CI = edge.first; + CallBase *CB = edge.first; Function *callee = edge.second; - if (!callSiteMappings.count(CI)) + if (!callSiteMappings.count(CB)) continue; - auto &mapping = callSiteMappings[CI]; + auto &mapping = callSiteMappings[CB]; // Check for collisions: multiple callee regions -> same caller // region. @@ -848,7 +930,13 @@ void Regions::propagateRegionMerges(Module &M) { } // Bottom-up pass: merge caller regions when the callee has collapsed - // them. + // them. Merging on representative-node equality alone loses field + // sensitivity (disjoint offset ranges on the same node are merged too), + // but it is what keeps per-function region counts bounded: the + // link-following closure creates whole-node regions, and without this + // consolidation the transitive access closure blows up region counts on + // large inputs. Field-granular threading needs a redesign of the + // closure/interface computation, not just a weaker merge condition. for (auto it = sccs.rbegin(); it != sccs.rend(); ++it) { auto &scc = *it; bool changed = true; @@ -859,13 +947,13 @@ void Regions::propagateRegionMerges(Module &M) { continue; bool merged = false; for (auto &edge : callGraph[F]) { - CallInst *CI = edge.first; - if (!callSiteMappings.count(CI)) + CallBase *CB = edge.first; + if (!callSiteMappings.count(CB)) continue; if (!funcRegionVecs.count(F)) continue; - auto &mapping = callSiteMappings[CI]; + auto &mapping = callSiteMappings[CB]; auto &callerRegions = funcRegionVecs[F]; // Build rep -> mapped caller region index. @@ -957,19 +1045,19 @@ void Regions::computeFunctionRegions(Module &M) { FunctionRegionInfo &info = funcRegions[&F]; for (auto &BB : F) { for (auto &I : BB) { - auto *CI = dyn_cast(&I); - if (!CI) + auto *CB = dyn_cast(&I); + if (!CB) continue; - Function *callee = CI->getCalledFunction(); + Function *callee = CB->getCalledFunction(); if (!callee) callee = dyn_cast( - CI->getCalledOperand()->stripPointerCastsAndAliases()); + CB->getCalledOperand()->stripPointerCastsAndAliases()); if (!callee || callee->isDeclaration()) continue; - if (!callSiteMappings.count(CI)) + if (!callSiteMappings.count(CB)) continue; - auto &mapping = callSiteMappings[CI]; + auto &mapping = callSiteMappings[CB]; auto &calleeInfo = funcRegions[callee]; for (unsigned calleeR : calleeInfo.readRegions) { @@ -1037,9 +1125,9 @@ std::set Regions::getAccessedRegions(const Function *F) const { } const std::map & -Regions::getCallSiteMapping(const CallInst *CI) const { +Regions::getCallSiteMapping(const CallBase *CB) const { static const std::map emptyMapping; - auto it = callSiteMappings.find(CI); + auto it = callSiteMappings.find(CB); if (it != callSiteMappings.end()) return it->second; return emptyMapping; diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index d69c437e9..643fd348c 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -324,6 +324,9 @@ void SmackInstGenerator::visitSwitchInst(llvm::SwitchInst &si) { void SmackInstGenerator::visitInvokeInst(llvm::InvokeInst &ii) { processInstruction(ii); llvm::Function *f = ii.getCalledFunction(); + if (!f) + f = llvm::dyn_cast( + ii.getCalledOperand()->stripPointerCastsAndAliases()); if (f) emit(rep->call(f, ii)); else diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 25b79a170..7e50c11fa 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -23,8 +23,8 @@ namespace { using namespace llvm; -std::list findCallers(Function *F) { - std::list callers; +std::list findCallers(Function *F) { + std::list callers; if (F) { std::queue users; @@ -37,8 +37,8 @@ std::list findCallers(Function *F) { auto U = users.front(); users.pop(); - if (CallInst *CI = dyn_cast(U)) - callers.push_back(CI); + if (CallBase *CB = dyn_cast(U)) + callers.push_back(CB); else for (auto V : U->users()) @@ -215,15 +215,20 @@ std::string SmackRep::opName(const std::string &operation, } std::string SmackRep::procName(const llvm::User &U) { - if (const llvm::CallInst *CI = llvm::dyn_cast(&U)) - return procName(CI->getCalledFunction(), U); + if (const llvm::CallBase *CB = llvm::dyn_cast(&U)) + return procName(CB->getCalledFunction(), U); else llvm_unreachable("Unexpected user expression."); } std::string SmackRep::procName(llvm::Function *F, const llvm::User &U) { std::list types; - for (unsigned i = 0; i < U.getNumOperands() - 1; i++) + // Count actual arguments only: invokes carry extra non-argument operands + // (destinations and callee) that must not contribute to vararg names. + unsigned numArgs = U.getNumOperands() - 1; + if (auto *CB = llvm::dyn_cast(&U)) + numArgs = CB->arg_size(); + for (unsigned i = 0; i < numArgs; i++) types.push_back(U.getOperand(i)->getType()); return procName(F, types); } @@ -1046,7 +1051,7 @@ bool SmackRep::isContractExpr(const std::string S) const { return S.find(Naming::CONTRACT_EXPR) == 0; } -ProcDecl *SmackRep::procedure(Function *F, CallInst *CI) { +ProcDecl *SmackRep::procedure(Function *F, CallBase *CI) { assert(F && "Unknown function call."); std::string name = naming->get(*F); std::list> params, rets; @@ -1114,7 +1119,7 @@ ProcDecl *SmackRep::procedure(Function *F, CallInst *CI) { std::list SmackRep::procedure(llvm::Function *F) { std::list procs; std::set names; - std::list callers = findCallers(F); + std::list callers = findCallers(F); // Consider `return_value` calls as normal `value` calls if (F->hasName() && F->getName().equals(Naming::VALUE_PROC)) { @@ -1167,13 +1172,15 @@ const Stmt *SmackRep::call(llvm::Function *f, const llvm::User &ci) { // Use call-site mapping to pass caller's regions for callee's params. if (f->hasName() && !SmackOptions::usesGlobalMemory(f->getName()) && !f->isDeclaration() && !isContractExpr(f)) { - auto *callInst = dyn_cast(&ci); - auto &mapping = regions->getCallSiteMapping(callInst); + auto *callBase = dyn_cast(&ci); + auto &mapping = regions->getCallSiteMapping(callBase); auto mapRegion = [&](unsigned calleeR) -> unsigned { auto it = mapping.find(calleeR); if (it == mapping.end()) - llvm_unreachable("Missing SeaDsa call-site memory-region mapping."); + report_fatal_error( + "missing SeaDsa call-site memory-region mapping for call to " + + f->getName()); return it->second; }; From 737bc6063f1db61b4018dd363cdcca805f000b88 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Wed, 8 Jul 2026 22:12:31 -0700 Subject: [PATCH 12/15] Emit cross-function memory as module-level maps PR 810 threads memory maps through procedure signatures ($M.r.in parameters, $M.r.out returns). Corral's variable-tracking abstraction only applies to global variables, so every threaded map is fully precise in every VC whether or not the property needs it, and each inlined instance carries map parameters and whole-map copies. On c/ntdrivers this made verification up to 6.9x slower than develop (cdaudio_true 32s -> 212s), with Corral's own statistics showing the regression entirely in per-VC solving time. This change binds all cross-function memory to module-level maps: - Phase 3.6 (computeGlobalMemoryMappings, reworked): every function's global-backed regions map to the entry function's region for the same global; conflicting targets merge the entry regions (mergeCalleeRegion repairs all bookkeeping); the entry region absorbs each function's attribute view and is forced module-level. - Phase 3.7 (unifySharedRegions, new): a union-find over (function, region) pairs linked by call-site mappings and the global mappings unifies the remaining cross-function memory. Classes containing an entry region bind every member to that entry map; entry-less classes with two or more members get a synthetic module-level map ($M.S.k); single-member classes stay procedure-local. Two entry regions in one class alias through some call chain and are merged. - Emission resolves every region through SmackRep::resolveRegion to the owning map (entry map $M.g, shared map $M.S.k, or procedure-local shadow $M.L.r, a separate namespace to avoid colliding with the module-level names) and uses the resolved region's attributes for map types and load/store/memcpy/memset/vector operations. Interface threading survives only for regions with no module-level binding (e.g. in functions never called through a mapped call site). - Multiple defined entry points are rejected with a hard error: the unified numbering follows the first entry point, and a second entry would silently verify against the wrong maps (this was already inconsistent under threading; now it is loud). Measured on c/ntdrivers (wall seconds, corral, default flags): develop PR 810 unified cdaudio_true 31.7 211.9 30.8 floppy2_true 26.6 184.2 29.0 parport_true 56.7 164.3 50.1 all 7 total 178.0 639.2 186.6 with identical verdicts everywhere. The unified build also keeps more memory maps than develop (e.g. floppy2 71 vs 38): CS-DSA's finer region splitting survives; only its calling-convention change is rolled back. Co-Authored-By: Claude Fable 5 --- include/smack/Regions.h | 24 ++- include/smack/SmackRep.h | 15 ++ lib/smack/Prelude.cpp | 6 + lib/smack/Regions.cpp | 277 ++++++++++++++++++++++++++--- lib/smack/SmackInstGenerator.cpp | 4 +- lib/smack/SmackModuleGenerator.cpp | 13 +- lib/smack/SmackRep.cpp | 107 ++++++++--- lib/smack/VectorOperations.cpp | 8 +- 8 files changed, 392 insertions(+), 62 deletions(-) diff --git a/include/smack/Regions.h b/include/smack/Regions.h index d81393560..c7478b275 100644 --- a/include/smack/Regions.h +++ b/include/smack/Regions.h @@ -61,12 +61,19 @@ class Region { // Returns true if the merge changed this region (extent or attributes). bool merge(Region &R); + // Absorb R's attributes (type, bytewise, flags) without widening this + // region's extent, so that this region's declared map type covers + // accesses performed through R. + void mergeAttributes(const Region &R); bool overlaps(Region &R); bool isSingleton() const { return singleton; }; bool isAllocated() const { return allocated; }; bool bytewiseAccess() const { return bytewise; } bool isGlobalScope() const { return globalScope; } + // 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; } const Type *getType() const { return type; } const seadsa::Node *getRepresentative() const { return representative; } unsigned getOffset() const { return offset; } @@ -99,11 +106,17 @@ class Regions : public ModulePass, public InstVisitor { std::map> callSiteMappings; - // For non-entry usesGlobalMemory functions: mapping from their region - // indices to the entry function's region indices (matched via globals). + // 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; + // Module-level maps for memory shared across functions without touching + // the entry function's regions (e.g., heap passed between siblings). + std::vector sharedRegions; + std::map, unsigned> + sharedRegionIndex; + static FunctionRegionInfo emptyRegionInfo; // The function currently being visited (set during visit phase). @@ -140,6 +153,7 @@ class Regions : public ModulePass, public InstVisitor { // and erased from F's region vector. Requires keep < remove. void remapAfterMerge(const llvm::Function *F, unsigned keep, unsigned remove); void computeGlobalMemoryMappings(llvm::Module &M); + void unifySharedRegions(llvm::Module &M); void computeFunctionRegions(llvm::Module &M); void computeInterfaceRegions(llvm::Module &M); @@ -162,6 +176,12 @@ class Regions : public ModulePass, public InstVisitor { getCallSiteMapping(const llvm::CallBase *CI) const; const std::map & 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. + int getSharedRegionIndex(const llvm::Function *F, unsigned r) const; + unsigned numSharedRegions() const { return sharedRegions.size(); } + Region &getShared(unsigned i) { return sharedRegions[i]; } void visitLoadInst(LoadInst &); void visitStoreInst(StoreInst &); diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index d76e88804..1fb4add9f 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -23,6 +23,7 @@ class Decl; class ProcDecl; class Stmt; class Expr; +class Region; class Regions; class Attr; @@ -192,9 +193,23 @@ class SmackRep { unsigned getElementSize(const llvm::Value *v); std::string memReg(unsigned i); + // Procedure-local shadow name for a threaded (non-global) region; a + // separate namespace from memReg so it cannot collide with the entry + // function's module-level maps. + std::string memLocalReg(unsigned i); + // Module-level map name for cross-function memory that does not reach + // the entry function's regions. + std::string memSharedReg(unsigned i); + std::string memTypeOf(Region &R); std::string memType(const llvm::Function *F, unsigned region); + // memType/memPath/region for the current function's region index, + // resolving global-backed regions to the entry function's map and other + // shared memory to module-level shared maps. + std::string memType(unsigned region); std::string memPath(unsigned region); std::string memPath(const llvm::Value *v, const llvm::Function *F); + std::pair resolveRegion(unsigned region); + Region ®ion(unsigned region); std::list> memoryMaps(const llvm::Function *F); diff --git a/lib/smack/Prelude.cpp b/lib/smack/Prelude.cpp index 7b3c22be1..ed86a60f8 100644 --- a/lib/smack/Prelude.cpp +++ b/lib/smack/Prelude.cpp @@ -1126,6 +1126,12 @@ void MemDeclGen::generateMemoryMaps(std::stringstream &s) const { } } + // 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"; + s << "\n"; } diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 4f0e7cd81..96f566164 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -60,7 +60,12 @@ void Region::init(const Value *V, unsigned length, const Function *F) { : nullptr; this->type = T; this->offset = DSA ? (F ? DSA->getOffset(V, *F) : DSA->getOffset(V)) : 0; - this->length = length; + // A zero-length region (opaque/extern types have storage size 0, and + // memset/memcpy may have constant length 0) is an empty interval that + // overlaps nothing — not even an identical probe — so every idx() lookup + // would create a fresh duplicate, and any fixpoint probing such a region + // diverges while the region vector grows unboundedly. Clamp to one byte. + this->length = std::max(length, 1u); singleton = DL && representative && isSingleton(V, length, F); allocated = !representative || isAllocated(representative); @@ -167,6 +172,18 @@ bool Region::merge(Region &R) { globalScope, type); } +void Region::mergeAttributes(const Region &R) { + bool collapse = type != R.type; + singleton = singleton && R.singleton; + allocated = allocated || R.allocated; + bytewise = SmackOptions::BitPrecise && (bytewise || R.bytewise || collapse); + incomplete = incomplete || R.incomplete; + complicated = complicated || R.complicated; + collapsed = collapsed || R.collapsed; + globalScope = globalScope || R.globalScope; + type = (bytewise || collapse) ? NULL : type; +} + bool Region::overlaps(Region &R) { return (incomplete && R.incomplete) || (complicated && R.complicated) || (representative == R.representative && @@ -210,6 +227,21 @@ bool Regions::runOnModule(Module &M) { Region::init(M, *this); DSA = &getAnalysis(); + // The unified memory model binds all shared memory to the first entry + // point's region numbering; a second entry point would emit its own + // numbering against those maps and silently verify the wrong program. + { + unsigned entryCount = 0; + for (auto &F : M) + if (!F.isDeclaration() && F.hasName() && + SmackOptions::isEntryPoint(F.getName())) + entryCount++; + if (entryCount > 1) + report_fatal_error( + "context-sensitive memory regions currently support a single " + "entry point; use one --entry-points function at a time"); + } + // Phase 1: Build per-function regions from each function's instructions. // Each function gets its own region vector computed from its own CS graph. // Also visit formal params and call-site actual args so that call-site @@ -328,10 +360,6 @@ bool Regions::runOnModule(Module &M) { } } - // Phase 2.5: Compute global-memory mappings for non-entry usesGlobalMemory - // functions (e.g., __SMACK_static_init) to the entry function's indices. - computeGlobalMemoryMappings(M); - // Phase 3: Compute call-site mappings (callee region -> caller region). // Iterate because link-following may create new regions in callers, // which then need mappings computed for their own callers. Convergence @@ -365,6 +393,21 @@ bool Regions::runOnModule(Module &M) { "propagation; callers may see stale memory for the affected " "regions (-debug-only=regions for details)\n"; + // Phase 3.6: Map global-backed regions of every function to the entry + // function's regions. These are emitted as module-level memory maps + // (which Corral's variable-tracking abstraction can reason about + // lazily) instead of being threaded through procedure signatures. + computeGlobalMemoryMappings(M); + + // 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. + unifySharedRegions(M); + // Phase 4: Transitive closure of region access sets. computeFunctionRegions(M); @@ -749,6 +792,18 @@ void Regions::remapAfterMerge(const Function *F, unsigned keep, m.second = remapRegionIndex(m.second, keep, remove); } + // Shift F-local indices in the shared-region table. + { + std::map, unsigned> newIndex; + for (auto &m : sharedRegionIndex) { + auto key = m.first; + if (key.first == F) + key.second = remapRegionIndex(key.second, keep, remove); + newIndex.insert({key, m.second}); + } + sharedRegionIndex = newIndex; + } + // Update all call-site mappings that reference F. // Mappings are callee_idx -> caller_idx; a self-recursive call site has F // on both sides and needs both its keys and its values shifted. @@ -997,39 +1052,192 @@ void Regions::propagateRegionMerges(Module &M) { void Regions::computeGlobalMemoryMappings(Module &M) { const Function *entryF = nullptr; for (auto &F : M) { - if (F.hasName() && SmackOptions::isEntryPoint(F.getName())) { + if (!F.isDeclaration() && F.hasName() && + SmackOptions::isEntryPoint(F.getName())) { entryF = &F; break; } } - if (!entryF) + if (!entryF || !DSA->hasGraph(*entryF)) return; - for (auto &F : M) { - if (F.isDeclaration()) - continue; - if (!F.hasName()) - continue; - if (!SmackOptions::usesGlobalMemory(F.getName())) - continue; - if (SmackOptions::isEntryPoint(F.getName())) - continue; - - std::map mapping; - for (auto &GV : M.globals()) { - if (!GV.getType()->isPointerTy()) + // 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; - if (!DSA->hasGraph(F) || !DSA->hasGraph(*entryF)) + // 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); - if (!fGraph.hasCell(GV) || !entryGraph.hasCell(GV)) + // Build in place: entry-side merges triggered below remap the values + // of every registered mapping, including this one. + auto &mapping = globalMemoryMappings[&F]; + for (auto &GV : M.globals()) { + if (!fGraph.hasCell(GV) || !entryGraph.hasCell(GV)) + continue; + unsigned fR = idx(&GV, &F); + unsigned entryR = idx(&GV, entryF); + auto it = mapping.find(fR); + if (it == mapping.end()) { + mapping[fR] = entryR; + changed = true; + } else if (it->second != entryR) { + mergeCalleeRegion(entryF, it->second, 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() && + "region indices must be repaired by remapAfterMerge"); + entryRegions[m.second].mergeAttributes(fRegions[m.first]); + entryRegions[m.second].markGlobalScope(); + } + } + } +} + +void Regions::unifySharedRegions(Module &M) { + const Function *entryF = nullptr; + for (auto &F : M) { + if (!F.isDeclaration() && F.hasName() && + SmackOptions::isEntryPoint(F.getName())) { + entryF = &F; + break; + } + } + + // Union-find over (function, region index) pairs, linked by call-site + // mappings and global-memory mappings. Rebuilt from scratch whenever an + // entry-side merge shifts indices (mergeCalleeRegion repairs the + // mappings the union-find is derived from, so rebuilding is correct). + while (true) { + std::map, unsigned> ids; + std::vector parent; + auto id = [&](const Function *F, unsigned r) { + auto key = std::make_pair(F, r); + auto it = ids.find(key); + if (it != ids.end()) + return it->second; + unsigned n = parent.size(); + ids[key] = n; + parent.push_back(n); + return n; + }; + std::function find = [&](unsigned x) { + while (parent[x] != x) { + parent[x] = parent[parent[x]]; + x = parent[x]; + } + return x; + }; + auto unite = [&](unsigned a, unsigned b) { parent[find(a)] = find(b); }; + + for (auto &cs : callSiteMappings) { + auto *CB = const_cast(cs.first); + Function *callee = CB->getCalledFunction(); + if (!callee) + callee = dyn_cast( + CB->getCalledOperand()->stripPointerCastsAndAliases()); + if (!callee) + continue; + const Function *caller = CB->getParent()->getParent(); + for (auto &m : cs.second) + unite(id(callee, m.first), id(caller, m.second)); + } + if (entryF) + for (auto &gm : globalMemoryMappings) + for (auto &m : gm.second) + unite(id(gm.first, m.first), id(entryF, m.second)); + + // A class containing two entry regions means those regions alias + // through some call chain; merge them and rebuild. + bool merged = false; + if (entryF) { + std::map entryRep; + for (auto &kv : ids) { + if (kv.first.first != entryF) + continue; + unsigned root = find(kv.second); + auto it = entryRep.find(root); + if (it == entryRep.end()) + entryRep[root] = kv.first.second; + else if (it->second != kv.first.second) { + mergeCalleeRegion(entryF, it->second, kv.first.second); + merged = true; + break; + } + } + } + if (merged) + continue; + + // Stable: bind every non-entry member of an entry class to the entry + // region, and give every entry-less multi-member class a fresh + // module-level shared map. + std::map classEntry; + if (entryF) + for (auto &kv : ids) + if (kv.first.first == entryF) + classEntry[find(kv.second)] = kv.first.second; + + std::map classSize; + for (auto &kv : ids) + classSize[find(kv.second)]++; + + std::map classShared; + for (auto &kv : ids) { + const Function *F = kv.first.first; + unsigned r = kv.first.second; + if (F == entryF) continue; - unsigned fR = idx(&GV, &F); - unsigned entryR = idx(&GV, entryF); - mapping[fR] = entryR; + assert(r < funcRegionVecs[F].size() && + "region indices must be repaired by remapAfterMerge"); + unsigned root = find(kv.second); + auto ce = classEntry.find(root); + if (ce != classEntry.end()) { + 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]); + // Referenced from other functions: must be a module-level map, + // not a local of the entry procedure. + funcRegionVecs[entryF][ce->second].markGlobalScope(); + continue; + } + if (classSize[root] < 2) + continue; // function-private: stays a procedure-local map + auto cs = classShared.find(root); + unsigned s; + if (cs == classShared.end()) { + s = sharedRegions.size(); + sharedRegions.push_back(funcRegionVecs[F][r]); + classShared[root] = s; + } else { + s = cs->second; + sharedRegions[s].mergeAttributes(funcRegionVecs[F][r]); + } + sharedRegionIndex[{F, r}] = s; } - globalMemoryMappings[&F] = mapping; + break; } } @@ -1094,14 +1302,24 @@ void Regions::computeInterfaceRegions(Module &M) { auto &graph = DSA->getGraph(F); reachableInterfaceNodes(&F, graph, inputReach, returnReach); + // 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 = + gmIt != globalMemoryMappings.end() ? &gmIt->second : nullptr; + auto accessed = getAccessedRegions(&F); for (unsigned r : accessed) { + if ((gm && gm->count(r)) || sharedRegionIndex.count({&F, r})) + continue; auto *rep = funcRegionVecs[&F][r].getRepresentative(); if (rep && inputReach.count(rep)) info.inputRegions.insert(r); } for (unsigned r : info.modifiedRegions) { + if ((gm && gm->count(r)) || sharedRegionIndex.count({&F, r})) + continue; auto *rep = funcRegionVecs[&F][r].getRepresentative(); if (rep && (inputReach.count(rep) || returnReach.count(rep))) info.outputRegions.insert(r); @@ -1142,4 +1360,11 @@ Regions::getGlobalMemoryMapping(const Function *F) const { return emptyMapping; } +int Regions::getSharedRegionIndex(const Function *F, unsigned r) const { + auto it = sharedRegionIndex.find({F, r}); + if (it != sharedRegionIndex.end()) + return (int)it->second; + return -1; +} + } // namespace smack diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index 643fd348c..277da1857 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -175,7 +175,7 @@ void SmackInstGenerator::visitBasicBlock(llvm::BasicBlock &bb) { auto &info = rep->getRegions()->getFunctionRegionInfo(F); for (unsigned r : info.inputRegions) emit(Stmt::assign(Expr::id(rep->memPath(r)), - Expr::id(rep->memReg(r) + ".in"))); + Expr::id(rep->memPath(r) + ".in"))); } } } @@ -258,7 +258,7 @@ void SmackInstGenerator::visitReturnInst(llvm::ReturnInst &ri) { if (!SmackOptions::usesGlobalMemory(naming->get(*F))) { auto &info = rep->getRegions()->getFunctionRegionInfo(F); for (unsigned r : info.outputRegions) - emit(Stmt::assign(Expr::id(rep->memReg(r) + ".out"), + emit(Stmt::assign(Expr::id(rep->memPath(r) + ".out"), Expr::id(rep->memPath(r)))); } diff --git a/lib/smack/SmackModuleGenerator.cpp b/lib/smack/SmackModuleGenerator.cpp index d48205930..a7bb7bc69 100644 --- a/lib/smack/SmackModuleGenerator.cpp +++ b/lib/smack/SmackModuleGenerator.cpp @@ -114,11 +114,18 @@ void SmackModuleGenerator::generateProgram(llvm::Module &M) { } } else if (!(F.hasName() && SmackOptions::usesGlobalMemory(F.getName()))) { - // Regular (non-global-memory) functions: all regions are local. + // Regular functions: local shadows for private regions only; + // memory bound to module-level maps (entry or shared) is + // accessed directly. + auto &gm = getAnalysis().getGlobalMemoryMapping(&F); auto accessed = getAnalysis().getAccessedRegions(&F); - for (unsigned r : accessed) + for (unsigned r : accessed) { + if (gm.count(r) || + getAnalysis().getSharedRegionIndex(&F, r) >= 0) + continue; P->getDeclarations().push_back( - Decl::variable(rep.memReg(r), rep.memType(&F, r))); + Decl::variable(rep.memPath(r), rep.memType(&F, r))); + } } } SDEBUG(errs() << "Finished analyzing function: " << naming.get(F) diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 7e50c11fa..01519bddf 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -291,17 +291,76 @@ std::string SmackRep::memReg(unsigned idx) { return indexedName(Naming::MEMORY, {idx}); } -std::string SmackRep::memType(const Function *F, unsigned region) { +std::string SmackRep::memTypeOf(Region &R) { std::stringstream s; - if (!regions->get(F, region).isSingleton() || + if (!R.isSingleton() || (SmackOptions::BitPrecise && SmackOptions::NoByteAccessInference)) s << "[" << Naming::PTR_TYPE << "] "; - const Type *T = regions->get(F, region).getType(); + const Type *T = R.getType(); s << (T ? type(T) : intType(8)); return s.str(); } -std::string SmackRep::memPath(unsigned region) { return memReg(region); } +std::string SmackRep::memType(const Function *F, unsigned region) { + return memTypeOf(regions->get(F, region)); +} + +std::string SmackRep::memLocalReg(unsigned idx) { + return indexedName(Naming::MEMORY + ".L", {idx}); +} + +std::string SmackRep::memSharedReg(unsigned idx) { + return indexedName(Naming::MEMORY + ".S", {idx}); +} + +// Resolve a region index in the current function's numbering to the owner +// of its Boogie memory map: global-backed regions of ordinary functions +// resolve to the entry function's module-level map, and other +// cross-function memory resolves to a shared module-level map (first == +// nullptr, second indexing Regions::getShared). A nullptr first with +// currentFunction set means shared; callers must special-case a null +// currentFunction before resolving. +std::pair +SmackRep::resolveRegion(unsigned region) { + 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}; + } + return {currentFunction, region}; +} + +Region &SmackRep::region(unsigned r) { + if (!currentFunction) + return regions->get(currentFunction, r); + auto res = resolveRegion(r); + if (!res.first) + return regions->getShared(res.second); + return regions->get(res.first, res.second); +} + +std::string SmackRep::memType(unsigned region) { + return memTypeOf(this->region(region)); +} + +std::string SmackRep::memPath(unsigned region) { + if (!currentFunction) + return memReg(region); + auto res = resolveRegion(region); + if (!res.first) + return memSharedReg(res.second); // shared module-level map + if (res.first != currentFunction) + return memReg(res.second); // the entry function's module-level map + if (currentFunction->hasName() && + !SmackOptions::usesGlobalMemory(currentFunction->getName())) + return memLocalReg(region); // procedure-local shadow + return memReg(region); +} std::string SmackRep::memPath(const llvm::Value *v, const Function *F) { return memPath(regions->idx(v, F)); @@ -317,8 +376,7 @@ SmackRep::memoryMaps(const Function *F) { bool SmackRep::isExternal(const llvm::Value *v) { return v->getType()->isPointerTy() && - !regions->get(currentFunction, regions->idx(v, currentFunction)) - .isAllocated(); + !region(regions->idx(v, currentFunction)).isAllocated(); } const Stmt *SmackRep::alloca(llvm::AllocaInst &i) { @@ -340,7 +398,7 @@ const Stmt *SmackRep::memcpy(const llvm::MemCpyInst &mci) { unsigned r1 = regions->idx(mci.getRawDest(), currentFunction, length); unsigned r2 = regions->idx(mci.getRawSource(), currentFunction, length); - const Type *T = regions->get(currentFunction, r1).getType(); + const Type *T = region(r1).getType(); Decl *P = memcpyProc(T ? type(T) : intType(8), length); auxDecls[P->getName()] = P; @@ -349,10 +407,10 @@ const Stmt *SmackRep::memcpy(const llvm::MemCpyInst &mci) { return Stmt::call( P->getName(), - {Expr::id(memReg(r1)), Expr::id(memReg(r2)), expr(dst), expr(src), + {Expr::id(memPath(r1)), Expr::id(memPath(r2)), expr(dst), expr(src), integerToPointer(expr(len), len->getType()->getIntegerBitWidth()), Expr::lit(mci.isVolatile())}, - {memReg(r1)}); + {memPath(r1)}); } const Stmt *SmackRep::memset(const llvm::MemSetInst &msi) { @@ -364,7 +422,7 @@ const Stmt *SmackRep::memset(const llvm::MemSetInst &msi) { unsigned r = regions->idx(msi.getRawDest(), currentFunction, length); - const Type *T = regions->get(currentFunction, r).getType(); + const Type *T = region(r).getType(); Decl *P = memsetProc(T ? type(T) : intType(8), length); auxDecls[P->getName()] = P; @@ -373,10 +431,10 @@ const Stmt *SmackRep::memset(const llvm::MemSetInst &msi) { return Stmt::call( P->getName(), - {Expr::id(memReg(r)), expr(dst), expr(val), + {Expr::id(memPath(r)), expr(dst), expr(val), integerToPointer(expr(len), len->getType()->getIntegerBitWidth()), Expr::lit(msi.isVolatile())}, - {memReg(r)}); + {memPath(r)}); } const Stmt *SmackRep::valueAnnotation(const CallInst &CI) { @@ -403,7 +461,7 @@ const Stmt *SmackRep::valueAnnotation(const CallInst &CI) { const unsigned bits = this->getSize(T); const unsigned bytes = bits / 8; const unsigned R = regions->idx(GEP, currentFunction); - bool bytewise = regions->get(currentFunction, R).bytewiseAccess(); + bool bytewise = region(R).bytewiseAccess(); attrs.push_back(Attr::attr("name", {Expr::id(naming->get(*A))})); attrs.push_back(Attr::attr( "field", { @@ -459,7 +517,7 @@ const Stmt *SmackRep::valueAnnotation(const CallInst &CI) { const unsigned bytes = bits / 8; const unsigned length = count * bytes; const unsigned R = regions->idx(V, currentFunction, length); - bool bytewise = regions->get(currentFunction, R).bytewiseAccess(); + bool bytewise = region(R).bytewiseAccess(); args.push_back(expr(CI.getArgOperand(1))); attrs.push_back(Attr::attr("name", {Expr::id(naming->get(*A))})); attrs.push_back(Attr::attr( @@ -535,9 +593,9 @@ const Expr *SmackRep::load(const llvm::Value *P) { const PointerType *T = dyn_cast(P->getType()); assert(T && "Expected pointer type."); const unsigned R = regions->idx(P, currentFunction); - bool bytewise = regions->get(currentFunction, R).bytewiseAccess(); - bool singleton = regions->get(currentFunction, R).isSingleton(); - const Type *resultTy = regions->get(currentFunction, R).getType(); + bool bytewise = region(R).bytewiseAccess(); + bool singleton = region(R).isSingleton(); + const Type *resultTy = region(R).getType(); const Expr *M = Expr::id(memPath(R)); std::string N = Naming::LOAD + "." + @@ -562,9 +620,9 @@ const Stmt *SmackRep::store(const Value *P, const Expr *V) { const Stmt *SmackRep::store(unsigned R, const Type *T, const Expr *P, const Expr *V) { - bool bytewise = regions->get(currentFunction, R).bytewiseAccess(); - bool singleton = regions->get(currentFunction, R).isSingleton(); - const Type *resultTy = regions->get(currentFunction, R).getType(); + bool bytewise = region(R).bytewiseAccess(); + bool singleton = region(R).isSingleton(); + const Type *resultTy = region(R).getType(); std::string N = Naming::STORE + "." + (bytewise ? "bytes." @@ -1106,10 +1164,10 @@ ProcDecl *SmackRep::procedure(Function *F, CallBase *CI) { !F->isDeclaration() && !isContractExpr(F)) { auto &info = regions->getFunctionRegionInfo(F); for (unsigned r : info.inputRegions) - params.push_back({memReg(r) + ".in", memType(F, r)}); + params.push_back({memLocalReg(r) + ".in", memType(F, r)}); for (unsigned r : info.outputRegions) - rets.push_back({memReg(r) + ".out", memType(F, r)}); + rets.push_back({memLocalReg(r) + ".out", memType(F, r)}); } return static_cast( @@ -1413,9 +1471,8 @@ const Stmt *SmackRep::inverseFPCastAssume(const StoreInst *si) { assert(PT && "Expected pointer type."); const Type *T = PT->getElementType(); unsigned R = regions->idx(P, currentFunction); - if (!T->isFloatingPointTy() || - !regions->get(currentFunction, R).bytewiseAccess() || - regions->get(currentFunction, R).isSingleton()) { + if (!T->isFloatingPointTy() || !region(R).bytewiseAccess() || + region(R).isSingleton()) { return nullptr; } return inverseFPCastAssume( diff --git a/lib/smack/VectorOperations.cpp b/lib/smack/VectorOperations.cpp index 977c16acc..f5adf430f 100644 --- a/lib/smack/VectorOperations.cpp +++ b/lib/smack/VectorOperations.cpp @@ -288,10 +288,10 @@ FuncDecl *VectorOperations::load(const Value *V) { type(ET); auto R = rep->regions->idx(V, rep->currentFunction); - auto MT = rep->regions->get(rep->currentFunction, R).getType(); + auto MT = rep->region(R).getType(); MT || (MT = IntegerType::get(V->getContext(), 8)); auto FN = rep->opName(Naming::LOAD, {ET, MT}); - auto M = rep->memType(rep->currentFunction, R); + auto M = rep->memType(R); auto P = rep->type(PT); auto E = rep->type(ET); auto F = (MT == ET) ? Decl::function(FN, {{"M", M}, {"p", P}}, E, @@ -308,10 +308,10 @@ FuncDecl *VectorOperations::store(const Value *V) { type(ET); auto R = rep->regions->idx(V, rep->currentFunction); - auto MT = rep->regions->get(rep->currentFunction, R).getType(); + auto MT = rep->region(R).getType(); MT || (MT = IntegerType::get(V->getContext(), 8)); auto FN = rep->opName(Naming::STORE, {ET, MT}); - auto M = rep->memType(rep->currentFunction, R); + auto M = rep->memType(R); auto P = rep->type(PT); auto E = rep->type(ET); auto F = (MT == ET) ? Decl::function(FN, {{"M", M}, {"p", P}, {"v", E}}, M, From 404f5e1d04a343ff5f181283abaf60c563212077 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Wed, 8 Jul 2026 23:54:46 -0700 Subject: [PATCH 13/15] Keep threading for region classes with paired same-function regions The CI run caught test/c/data/two_arrays1.c timing out under the no-reuse and reuse memory models: the shared-memory union-find fused the two arrays through their common callee's formal parameter (array1 ~ formal ~ array2), collapsing memory that both the threading scheme and develop keep separate, and making the merged map 4x more expensive to reason about (192s vs 43s locally). A class now keeps the per-call-site threading when some function has exactly two distinct regions in it: that is deliberate program structure (two objects flowing through one callee), and merging loses real separation. Classes where a function has three or more regions are DSA-collapse artifacts (11-198 duplicated members on the ntdrivers benchmarks); threading those costs far more than the separation is worth, so they still bind to module-level maps. Regions bound by globals identity in Phase 3.6 keep their binding even inside threaded classes: sea-dsa propagates global symbols along call chains, so a bound callee implies a bound caller and the mix stays consistent. Measured: two_arrays1 40.7s (develop: 51.4s; unguarded merge: 192s); ntdrivers unchanged within noise (all 7: 192s vs develop 178s, same verdicts); all 2052 regression configurations pass. Co-Authored-By: Claude Fable 5 --- lib/smack/Regions.cpp | 215 +++++++++++++++++++++--------------------- 1 file changed, 108 insertions(+), 107 deletions(-) diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 96f566164..cdc909182 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -1125,119 +1125,120 @@ void Regions::unifySharedRegions(Module &M) { } // Union-find over (function, region index) pairs, linked by call-site - // mappings and global-memory mappings. Rebuilt from scratch whenever an - // entry-side merge shifts indices (mergeCalleeRegion repairs the - // mappings the union-find is derived from, so rebuilding is correct). - while (true) { - std::map, unsigned> ids; - std::vector parent; - auto id = [&](const Function *F, unsigned r) { - auto key = std::make_pair(F, r); - auto it = ids.find(key); - if (it != ids.end()) - return it->second; - unsigned n = parent.size(); - ids[key] = n; - parent.push_back(n); - return n; - }; - std::function find = [&](unsigned x) { - while (parent[x] != x) { - parent[x] = parent[parent[x]]; - x = parent[x]; - } - return x; - }; - auto unite = [&](unsigned a, unsigned b) { parent[find(a)] = find(b); }; - - for (auto &cs : callSiteMappings) { - auto *CB = const_cast(cs.first); - Function *callee = CB->getCalledFunction(); - if (!callee) - callee = dyn_cast( - CB->getCalledOperand()->stripPointerCastsAndAliases()); - if (!callee) - continue; - const Function *caller = CB->getParent()->getParent(); - for (auto &m : cs.second) - unite(id(callee, m.first), id(caller, m.second)); - } - if (entryF) - for (auto &gm : globalMemoryMappings) - for (auto &m : gm.second) - unite(id(gm.first, m.first), id(entryF, m.second)); - - // A class containing two entry regions means those regions alias - // through some call chain; merge them and rebuild. - bool merged = false; - if (entryF) { - std::map entryRep; - for (auto &kv : ids) { - if (kv.first.first != entryF) - continue; - unsigned root = find(kv.second); - auto it = entryRep.find(root); - if (it == entryRep.end()) - entryRep[root] = kv.first.second; - else if (it->second != kv.first.second) { - mergeCalleeRegion(entryF, it->second, kv.first.second); - merged = true; - break; - } - } + // mappings and global-memory mappings. + std::map, unsigned> ids; + std::vector parent; + auto id = [&](const Function *F, unsigned r) { + auto key = std::make_pair(F, r); + auto it = ids.find(key); + if (it != ids.end()) + return it->second; + unsigned n = parent.size(); + ids[key] = n; + parent.push_back(n); + return n; + }; + std::function find = [&](unsigned x) { + while (parent[x] != x) { + parent[x] = parent[parent[x]]; + x = parent[x]; } - if (merged) - continue; - - // Stable: bind every non-entry member of an entry class to the entry - // region, and give every entry-less multi-member class a fresh - // module-level shared map. - std::map classEntry; - if (entryF) - for (auto &kv : ids) - if (kv.first.first == entryF) - classEntry[find(kv.second)] = kv.first.second; + return x; + }; + auto unite = [&](unsigned a, unsigned b) { parent[find(a)] = find(b); }; - std::map classSize; + for (auto &cs : callSiteMappings) { + auto *CB = const_cast(cs.first); + Function *callee = CB->getCalledFunction(); + if (!callee) + callee = dyn_cast( + CB->getCalledOperand()->stripPointerCastsAndAliases()); + if (!callee) + continue; + const Function *caller = CB->getParent()->getParent(); + for (auto &m : cs.second) + unite(id(callee, m.first), id(caller, m.second)); + } + if (entryF) + for (auto &gm : globalMemoryMappings) + for (auto &m : gm.second) + unite(id(gm.first, m.first), id(entryF, m.second)); + + // A 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). Classes where some function has three or + // more regions are DSA-collapse artifacts spanning dozens of regions on + // the ntdrivers benchmarks; threading those costs far more than the + // separation is worth, so they still merge. + std::set classThreaded; + { + std::map, unsigned> mult; for (auto &kv : ids) - classSize[find(kv.second)]++; + 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); + } + for (auto &m : maxMult) + if (m.second == 2) + classThreaded.insert(m.first); + } - std::map classShared; - for (auto &kv : ids) { - const Function *F = kv.first.first; - unsigned r = kv.first.second; - if (F == entryF) - continue; - assert(r < funcRegionVecs[F].size() && + std::map classEntry; + if (entryF) + for (auto &kv : ids) + if (kv.first.first == entryF) + classEntry[find(kv.second)] = kv.first.second; + + std::map classSize; + for (auto &kv : ids) + classSize[find(kv.second)]++; + + std::map classShared; + for (auto &kv : ids) { + const Function *F = kv.first.first; + 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. + continue; + } + if (F == entryF) + 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; + assert(ce->second < funcRegionVecs[entryF].size() && "region indices must be repaired by remapAfterMerge"); - unsigned root = find(kv.second); - auto ce = classEntry.find(root); - if (ce != classEntry.end()) { - 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]); - // Referenced from other functions: must be a module-level map, - // not a local of the entry procedure. - funcRegionVecs[entryF][ce->second].markGlobalScope(); - continue; - } - if (classSize[root] < 2) - continue; // function-private: stays a procedure-local map - auto cs = classShared.find(root); - unsigned s; - if (cs == classShared.end()) { - s = sharedRegions.size(); - sharedRegions.push_back(funcRegionVecs[F][r]); - classShared[root] = s; - } else { - s = cs->second; - sharedRegions[s].mergeAttributes(funcRegionVecs[F][r]); - } - sharedRegionIndex[{F, r}] = s; + funcRegionVecs[entryF][ce->second].mergeAttributes(funcRegionVecs[F][r]); + // Referenced from other functions: must be a module-level map, + // not a local of the entry procedure. + funcRegionVecs[entryF][ce->second].markGlobalScope(); + continue; + } + if (classSize[root] < 2) + continue; // function-private: stays a procedure-local map + auto cs = classShared.find(root); + unsigned s; + if (cs == classShared.end()) { + s = sharedRegions.size(); + sharedRegions.push_back(funcRegionVecs[F][r]); + classShared[root] = s; + } else { + s = cs->second; + sharedRegions[s].mergeAttributes(funcRegionVecs[F][r]); } - break; + sharedRegionIndex[{F, r}] = s; } } From 76165f71158cc5045a669088f9281771d1aac972 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Fri, 10 Jul 2026 09:03:01 -0700 Subject: [PATCH 14/15] Preserve field-granular regions in the CS pipeline The context-sensitive pipeline produced *coarser* memory maps than the context-insensitive baseline (hid-waltop: 39 module maps vs develop's 214), defeating its own purpose and slowing verification up to 18x on LDV driver benchmarks. Phase-wise instrumentation located the losses: - Phase 1 pre-seeded formals, call arguments, globals, and pointer call returns with whole-pointee-extent regions; each such probe overlaps and absorbs every field region on its node (a whole-global probe run per function collapsed __SMACK_static_init's 737 field regions to ~40). These probes were a workaround for call-site mappings mutating region indices, which the bookkeeping-repair machinery has since made safe: regions are now created from actual accesses only, and memory reached through calls gets field-precise regions from the call-site mapping fixpoint. The link-following closure (whole-node regions) is removed for the same reason; pointer-return probes remain only for external functions. - The bottom-up pass of propagateRegionMerges merged caller regions on representative-node equality, folding disjoint fields. It is replaced by an overlap-only normalization sweep (same predicate idx() uses), run again after Phases 3.6-3.7 since merges can widen extents without re-checking neighbors. - __SMACK_static_init and __SMACK_init_func* bodies are emitted in the entry function's region context, but their region probes previously fell back to the underlying global, collapsing every field to its base. Their cells are now translated from their own DSA graph into the entry graph through a globals-seeded SimulationMapper, composing offsets with sea-dsa's cell semantics (collapsed nodes fold to zero, array nodes wrap modulo the node size); the same translation backs cross-function lookups in DSAWrapper. Globals no access covers are anchored in the entry vector so module maps keep at least per-global granularity. - Region::mergeAttributes absorbs only emission-relevant attributes (type, singleton, bytewise); absorbing the matching flags (incomplete/complicated/collapsed) armed spurious cross-node merges after normalization, and one such post-pass merge left an already-emitted map reference dangling. - isExternal no longer probes regions (a whole-pointee probe at translation time could merge field regions late); it asks the DSA node directly. computeGlobalMemoryMappings lookups are now non-mutating (findRegion). The threading guard for paired regions additionally requires a small class, since field-granular classes made the multiplicity test fire on large collapse artifacts. Measured (corral, wall seconds): develop before after module maps (dev) hid-waltop 43_1a 2.0 37.2 1.9 214 (214) two_arrays1 51.4 40.7 24.5 cdaudio_true 31.7 29.4 29.1 70 (52) parport_true 56.7 62.4 60.5 108 (102) floppy2_true 26.6 33.1 105.9 46 (38) with identical verdicts everywhere; all 2052 regression configurations pass. floppy2's residual comes from its per-function access patterns (memset/whole-struct operations), not the region pipeline, and is left as a follow-up. Co-Authored-By: Claude Fable 5 --- include/smack/DSAWrapper.h | 12 + include/smack/Regions.h | 24 ++ lib/smack/DSAWrapper.cpp | 50 +++- lib/smack/Regions.cpp | 398 ++++++++++++++++++----------- lib/smack/SmackModuleGenerator.cpp | 9 +- lib/smack/SmackRep.cpp | 2 +- 6 files changed, 331 insertions(+), 164 deletions(-) diff --git a/include/smack/DSAWrapper.h b/include/smack/DSAWrapper.h index 0b4f6eca6..9de9cd34b 100644 --- a/include/smack/DSAWrapper.h +++ b/include/smack/DSAWrapper.h @@ -7,12 +7,15 @@ #ifndef DSAWRAPPER_H #define DSAWRAPPER_H +#include +#include #include #include #include "seadsa/DsaAnalysis.hh" #include "seadsa/Global.hh" #include "seadsa/Graph.hh" +#include "seadsa/Mapper.hh" namespace smack { @@ -57,6 +60,15 @@ class DSAWrapper : public llvm::ModulePass { bool isTypeSafe(const llvm::Value *v, const llvm::Function &F); unsigned getNumGlobals(const seadsa::Node *n); + // 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); + // Per-function graph access for context-sensitive analysis. 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 c7478b275..05f9d1e4b 100644 --- a/include/smack/Regions.h +++ b/include/smack/Regions.h @@ -122,6 +122,20 @@ class Regions : public ModulePass, public InstVisitor { // The function currently being visited (set during visit phase). const llvm::Function *currentFunction = nullptr; + // First defined entry point; the region context for usesGlobalMemory + // functions (__SMACK_static_init, __SMACK_init_func*), whose bodies are + // emitted against the entry function's regions. + const llvm::Function *entryFunction = nullptr; + + // The vector that F's regions live in: usesGlobalMemory functions share + // the entry function's regions. + const llvm::Function *regionHome(const llvm::Function *F) const; + + // When set, values probed through idx() belong to this function and their + // cells are translated into the target function's graph through shared + // globals (offset-precise), instead of being looked up directly. + const llvm::Function *translationSource = nullptr; + // DSAWrapper pointer cached during runOnModule. DSAWrapper *DSA = nullptr; @@ -140,6 +154,8 @@ class Regions : public ModulePass, public InstVisitor { // 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, + unsigned length); void computeCallSiteMappings(llvm::Module &M); void computeOneCallSiteMapping(llvm::CallBase *CI, @@ -152,6 +168,9 @@ class Regions : public ModulePass, public InstVisitor { // merged-region aliases) after F's region `remove` was merged into `keep` // and erased from F's region vector. Requires keep < remove. void remapAfterMerge(const llvm::Function *F, unsigned keep, unsigned remove); + int findRegion(const llvm::Function *F, const seadsa::Node *node, + unsigned offset); + bool normalizeOverlaps(const llvm::Function *F); void computeGlobalMemoryMappings(llvm::Module &M); void unifySharedRegions(llvm::Module &M); void computeFunctionRegions(llvm::Module &M); @@ -169,6 +188,10 @@ class Regions : public ModulePass, public InstVisitor { unsigned idx(const llvm::Value *v, const llvm::Function *F, unsigned length); Region &get(const llvm::Function *F, unsigned R); + // Set while translating a usesGlobalMemory function's body against the + // entry function's regions (see translationSource). + void setTranslationSource(const llvm::Function *F) { translationSource = F; } + const FunctionRegionInfo & getFunctionRegionInfo(const llvm::Function *F) const; std::set getAccessedRegions(const llvm::Function *F) const; @@ -180,6 +203,7 @@ class Regions : public ModulePass, public InstVisitor { // reach the entry function's regions. Returns -1 if F's region r is not // backed by a shared map. int getSharedRegionIndex(const llvm::Function *F, unsigned r) const; + bool isAllocatedValue(const llvm::Value *v, const llvm::Function *F); unsigned numSharedRegions() const { return sharedRegions.size(); } Region &getShared(unsigned i) { return sharedRegions[i]; } diff --git a/lib/smack/DSAWrapper.cpp b/lib/smack/DSAWrapper.cpp index 53df5d188..68fdb2af3 100644 --- a/lib/smack/DSAWrapper.cpp +++ b/lib/smack/DSAWrapper.cpp @@ -190,9 +190,21 @@ unsigned DSAWrapper::getOffset(const Value *v, const Function &F) { auto &graph = SD->getGraph(F); if (graph.hasCell(*v)) return graph.getCell(*v).getOffset(); - // V might be from a different function (e.g., a GEP in __SMACK_static_init - // when we're resolving in the entry function's context). Strip to the - // underlying object (the global variable) and look that up instead. + // 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()) { + auto *n = c.getNode(); + unsigned long rawOff = (unsigned long)c.getOffset() + srcCell.getOffset(); + if (n->isOffsetCollapsed()) + return 0; + if (n->isArray() && n->size() > 0) + return (unsigned)(rawOff % n->size()); + return (unsigned)rawOff; + } + } const Value *base = getUnderlyingObject(v); if (base != v && graph.hasCell(*base)) return graph.getCell(*base).getOffset(); @@ -208,6 +220,26 @@ 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; +} + const seadsa::Node *DSAWrapper::getNode(const Value *v, const Function &F) { if (!SD->hasGraph(F)) return getNode(v); @@ -218,8 +250,16 @@ const seadsa::Node *DSAWrapper::getNode(const Value *v, const Function &F) { return node; } // V might be from a different function (e.g., a GEP in __SMACK_static_init - // when we're resolving in the entry function's context). Strip to the - // underlying object (the global variable) and look that up instead. + // when we're resolving in the entry function's context). Translate its + // cell from its own graph through the globals the two graphs share; this + // 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()) + 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(); diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index cdc909182..25f77637c 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -173,13 +173,15 @@ bool Region::merge(Region &R) { } void Region::mergeAttributes(const Region &R) { + // Absorb only the attributes that govern the emitted map (type, + // singleton, byte-level access). The matching flags (incomplete, + // complicated, collapsed) describe this region's own node and drive + // 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; allocated = allocated || R.allocated; bytewise = SmackOptions::BitPrecise && (bytewise || R.bytewise || collapse); - incomplete = incomplete || R.incomplete; - complicated = complicated || R.complicated; - collapsed = collapsed || R.collapsed; globalScope = globalScope || R.globalScope; type = (bytewise || collapse) ? NULL : type; } @@ -222,11 +224,44 @@ void Regions::getAnalysisUsage(llvm::AnalysisUsage &AU) const { AU.addRequired(); } +static void dumpPhase(const char *tag, + std::map> &vecs) { + if (!getenv("SMACK_DEBUG_PHASES")) + return; + unsigned total = 0, maxf = 0; + const Function *maxF = nullptr; + for (auto &kv : vecs) { + total += kv.second.size(); + if (kv.second.size() > maxf) { + maxf = kv.second.size(); + maxF = kv.first; + } + } + errs() << "PHASE " << tag << ": total=" << total << " max=" << maxf << " (" + << (maxF ? maxF->getName() : "?") << ")\n"; +} + +const Function *Regions::regionHome(const Function *F) const { + if (F && entryFunction && F != entryFunction && F->hasName() && + SmackOptions::usesGlobalMemory(F->getName()) && + !SmackOptions::isEntryPoint(F->getName())) + return entryFunction; + return F; +} + bool Regions::runOnModule(Module &M) { if (!SmackOptions::NoMemoryRegionSplitting) { Region::init(M, *this); DSA = &getAnalysis(); + for (auto &F : M) { + if (!F.isDeclaration() && F.hasName() && + SmackOptions::isEntryPoint(F.getName())) { + entryFunction = &F; + break; + } + } + // The unified memory model binds all shared memory to the first entry // point's region numbering; a second entry point would emit its own // numbering against those maps and silently verify the wrong program. @@ -246,99 +281,61 @@ bool Regions::runOnModule(Module &M) { // Each function gets its own region vector computed from its own CS graph. // Also visit formal params and call-site actual args so that call-site // mapping (Phase 3) doesn't create new regions or alter indices. + // Regions are created from actual accesses only: pre-seeding formals, + // call arguments, or globals with whole-pointee extents merges away the + // field-granular regions the accesses create (a whole-struct probe + // overlaps and absorbs every field region on the node). Regions for + // memory reached only through calls are created field-precisely by the + // call-site mapping fixpoint (Phase 3). for (auto &F : M) { if (F.isDeclaration()) continue; - // Visit formal pointer parameters. - for (auto &A : F.args()) - if (A.getType()->isPointerTy()) - idx(&A, &F); - // Visit all instructions. - currentFunction = &F; + // usesGlobalMemory functions (e.g., __SMACK_static_init) are emitted + // in the entry function's region context, so their accesses must + // create the entry function's regions; they are Boogie-level callees + // of the entry point with no LLVM call site to map them through. + const Function *H = regionHome(&F); + currentFunction = H; + translationSource = H == &F ? nullptr : &F; visit(const_cast(F)); + translationSource = nullptr; } currentFunction = nullptr; - // Visit actual pointer arguments at call sites (in the caller's context). - for (auto &F : M) { - if (F.isDeclaration()) - continue; - for (auto &BB : F) { - for (auto &I : BB) { - if (auto *CB = dyn_cast(&I)) { - for (unsigned i = 0; i < CB->arg_size(); i++) { - Value *arg = CB->getArgOperand(i); - if (arg->getType()->isPointerTy()) - idx(arg, &F); - } - } - } - } - } - // Visit globals in each function's context that accesses them. - for (auto &F : M) { - if (F.isDeclaration()) - continue; - if (!DSA->hasGraph(F)) - continue; - auto &graph = DSA->getGraph(F); + // Anchor globals that no access covered (e.g., extern or uninitialized + // state touched only through callees) in the entry function's vector, + // so that module-level maps keep at least per-global granularity. + // Globals already covered by finer regions (typically the per-field + // stores of __SMACK_static_init) are left untouched: a whole-global + // probe would merge those field regions away. + if (entryFunction && DSA->hasGraph(*entryFunction)) { + auto &entryGraph = DSA->getGraph(*entryFunction); for (auto &GV : M.globals()) { - if (GV.getType()->isPointerTy() && graph.hasCell(GV)) - idx(&GV, &F); - } - } - - // Create regions for all DSA nodes reachable through pointer links - // from existing regions. This ensures callers have regions for data - // accessible through pointer indirection (e.g., **arg), which their - // callees may access. Without this, call-site mappings would be - // incomplete and regions that should be distinct would be merged. - for (auto &F : M) { - if (F.isDeclaration() || !DSA->hasGraph(F)) - continue; - bool grew = true; - while (grew) { - grew = false; - auto ®ions = funcRegionVecs[&F]; - std::set existing; - for (auto &r : regions) - if (r.getRepresentative()) - existing.insert(r.getRepresentative()); - unsigned origSize = regions.size(); - // idx() below can cascade-merge and shrink the vector; re-check the - // live size so regions[i] never reads out of bounds. - for (unsigned i = 0; i < origSize && i < regions.size(); i++) { - auto *rep = regions[i].getRepresentative(); - if (!rep) - continue; - for (auto &link : rep->links()) { - auto *target = link.second->getNode(); - if (target && !existing.count(target)) { - existing.insert(target); - Region R(target, F.getContext()); - unsigned before = regions.size(); - idx(R, &F); - grew = grew || regions.size() > before; - } - } - } + if (!entryGraph.hasCell(GV)) + continue; + auto cell = entryGraph.getCell(GV); + if (findRegion(entryFunction, cell.getNode(), cell.getOffset()) < 0) + idx(&GV, entryFunction); } } + dumpPhase("1-visits", funcRegionVecs); // Phase 2: Compute per-function read/write sets (direct accesses). for (auto &F : M) { if (F.isDeclaration()) continue; - FunctionRegionInfo &info = funcRegions[&F]; + const Function *H = regionHome(&F); + translationSource = H == &F ? nullptr : &F; + FunctionRegionInfo &info = funcRegions[H]; for (inst_iterator I = inst_begin(&F), E = inst_end(&F); I != E; ++I) { if (auto *LI = dyn_cast(&*I)) { - info.readRegions.insert(idx(LI->getPointerOperand(), &F)); + info.readRegions.insert(idx(LI->getPointerOperand(), H)); } else if (auto *SI = dyn_cast(&*I)) { - info.modifiedRegions.insert(idx(SI->getPointerOperand(), &F)); + info.modifiedRegions.insert(idx(SI->getPointerOperand(), H)); } else if (auto *AI = dyn_cast(&*I)) { - unsigned r = idx(AI->getPointerOperand(), &F); + unsigned r = idx(AI->getPointerOperand(), H); info.readRegions.insert(r); info.modifiedRegions.insert(r); } else if (auto *AI = dyn_cast(&*I)) { - unsigned r = idx(AI->getPointerOperand(), &F); + unsigned r = idx(AI->getPointerOperand(), H); info.readRegions.insert(r); info.modifiedRegions.insert(r); } else if (auto *MSI = dyn_cast(&*I)) { @@ -347,18 +344,19 @@ bool Regions::runOnModule(Module &M) { length = CI->getZExtValue(); else length = std::numeric_limits::max(); - info.modifiedRegions.insert(idx(MSI->getDest(), &F, length)); + info.modifiedRegions.insert(idx(MSI->getDest(), H, length)); } else if (auto *MTI = dyn_cast(&*I)) { unsigned length; if (auto CI = dyn_cast(MTI->getLength())) length = CI->getZExtValue(); else length = std::numeric_limits::max(); - info.readRegions.insert(idx(MTI->getSource(), &F, length)); - info.modifiedRegions.insert(idx(MTI->getDest(), &F, length)); + info.readRegions.insert(idx(MTI->getSource(), H, length)); + info.modifiedRegions.insert(idx(MTI->getDest(), H, length)); } } } + translationSource = nullptr; // Phase 3: Compute call-site mappings (callee region -> caller region). // Iterate because link-following may create new regions in callers, @@ -382,6 +380,7 @@ bool Regions::runOnModule(Module &M) { << " passes; some memory-region mappings may be incomplete\n"; mappingsFinal = true; + dumpPhase("3-mappings", funcRegionVecs); // Phase 3.5: Propagate region merges top-down through the call graph. // When a caller collapses two callee regions (maps both to the same // caller region), the callee must merge them to preserve the invariant @@ -393,12 +392,14 @@ bool Regions::runOnModule(Module &M) { "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 // function's regions. These are emitted as module-level memory maps // (which Corral's variable-tracking abstraction can reason about // lazily) instead of being threaded through procedure signatures. 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 @@ -408,6 +409,14 @@ bool Regions::runOnModule(Module &M) { // Only function-private regions remain procedure-local. unifySharedRegions(M); + // Phase 3.8: Final normalization. Merges in Phases 3.5-3.7 can widen + // extents without re-checking overlap; every emitted reference must see + // the final region structure, so re-establish the no-overlap invariant + // before anything is generated. + for (auto &kv : funcRegionVecs) + normalizeOverlaps(kv.first); + + dumpPhase("3.7-unify", funcRegionVecs); // Phase 4: Transitive closure of region access sets. computeFunctionRegions(M); @@ -431,9 +440,54 @@ Region &Regions::get(const Function *F, unsigned R) { return funcRegionVecs[F][R]; } +// Probe V's region in F when V belongs to translationSource: resolve V's +// cell in its own function's graph and translate it into F's graph through +// their shared globals, preserving field offsets (a direct lookup would +// fall back to the underlying global and collapse every field to its base). +// Compose an offset onto a node following sea-dsa's cell semantics: +// offset-collapsed nodes fold every offset to zero, and array nodes wrap +// offsets modulo the node size (the array stride). Composing raw offsets +// across graphs without this scatters accesses past the node's extent. +static unsigned composeOffset(const seadsa::Node *n, unsigned long rawOff) { + if (!n || n->isOffsetCollapsed()) + return 0; + if (n->isArray() && n->size() > 0) + return (unsigned)(rawOff % n->size()); + return (unsigned)rawOff; +} + +int Regions::idxTranslated(const Value *V, const Function *F, unsigned length) { + if (!translationSource || translationSource == F || !DSA || + !DSA->hasGraph(*translationSource) || !DSA->hasGraph(*F)) + return -1; + auto &srcG = DSA->getGraph(*translationSource); + auto &dstG = DSA->getGraph(*F); + if (&srcG == &dstG || !srcG.hasCell(*V)) + return -1; + 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()); + return (int)idx(R, F); +} + unsigned Regions::idx(const Value *V, const Function *F) { SDEBUG(errs() << "[regions] for: " << *V << " in function: " << F->getName() << "\n"); + unsigned length = + DSA ? DSA->getPointedTypeSize(V) : std::numeric_limits::max(); + int t = idxTranslated(V, F, length); + if (t >= 0) + return (unsigned)t; Region R(V, F); return idx(R, F); } @@ -441,6 +495,9 @@ unsigned Regions::idx(const Value *V, const Function *F) { unsigned Regions::idx(const Value *V, const Function *F, unsigned length) { SDEBUG(errs() << "[regions] for: " << *V << " with length " << length << " in function: " << F->getName() << "\n"); + int t = idxTranslated(V, F, length); + if (t >= 0) + return (unsigned)t; Region R(V, F, length); return idx(R, F); } @@ -491,6 +548,11 @@ unsigned Regions::idx(Region &R, const Function *F) { if (r == regions.size()) { regions.emplace_back(R); structuralVersion++; + if (mappingsFinal && F == entryFunction && getenv("SMACK_DEBUG_LATE")) { + errs() << "LATE-ENTRY-CREATE idx " << r << " "; + R.print(errs()); + errs() << "\n"; + } } else { // In case R was merged with an existing region, we must now also merge @@ -506,6 +568,17 @@ unsigned Regions::idx(Region &R, const Function *F) { SDEBUG(regions[q].print(errs())); SDEBUG(errs() << "\n"); + if (mappingsFinal && F == entryFunction && getenv("SMACK_DEBUG_LATE")) { + errs() << "LATE-ENTRY-MERGE " << q << " into " << r << " probe "; + R.print(errs()); + errs() << " absorber "; + regions[r].print(errs()); + errs() << " victim "; + regions[q].print(errs()); + errs() << " src=" + << (translationSource ? translationSource->getName() : "-") + << "\n"; + } regions[r].merge(regions[q]); regions.erase(regions.begin() + q); remapAfterMerge(F, r, q); @@ -578,7 +651,11 @@ void Regions::visitCallBase(CallBase &I) { Function *F = I.getCalledFunction(); std::string name = F && F->hasName() ? F->getName().str() : ""; - if (I.getType()->isPointerTy() && name != "malloc") + // Only external functions need a region for their returned pointer: + // returns from defined functions are mapped field-precisely through the + // call-site mappings, and a whole-pointee probe here would merge away + // the field regions of whatever the callee returns. + if (F && F->isDeclaration() && I.getType()->isPointerTy() && name != "malloc") idx(&I, currentFunction); if (name.find("__SMACK_values") != std::string::npos) { @@ -984,69 +1061,58 @@ void Regions::propagateRegionMerges(Module &M) { } } - // Bottom-up pass: merge caller regions when the callee has collapsed - // them. Merging on representative-node equality alone loses field - // sensitivity (disjoint offset ranges on the same node are merged too), - // but it is what keeps per-function region counts bounded: the - // link-following closure creates whole-node regions, and without this - // consolidation the transitive access closure blows up region counts on - // large inputs. Field-granular threading needs a redesign of the - // closure/interface computation, not just a weaker merge condition. - for (auto it = sccs.rbegin(); it != sccs.rend(); ++it) { - auto &scc = *it; - bool changed = true; - while (changed) { - changed = false; - for (const Function *F : scc) { - if (!callGraph.count(F)) - continue; - bool merged = false; - for (auto &edge : callGraph[F]) { - CallBase *CB = edge.first; - if (!callSiteMappings.count(CB)) - continue; - if (!funcRegionVecs.count(F)) - continue; - - auto &mapping = callSiteMappings[CB]; - auto &callerRegions = funcRegionVecs[F]; - - // Build rep -> mapped caller region index. - std::map repToMappedCaller; - std::set mappedCallerIndices; - for (auto &m : mapping) { - mappedCallerIndices.insert(m.second); - if (m.second < callerRegions.size()) { - auto *rep = callerRegions[m.second].getRepresentative(); - if (rep) - repToMappedCaller[rep] = m.second; - } - } + // Normalization pass: merges above can widen a region's extent past + // its neighbors without re-checking for overlap, breaking the + // regions-never-alias invariant. Merge any pair that overlaps (by the + // same predicate idx() uses); unlike the earlier representative-node + // merging this is precision-preserving — disjoint field regions on the + // same node stay distinct. + for (auto &kv : funcRegionVecs) + if (normalizeOverlaps(kv.first)) + globalChanged = true; + } +} - // Find unmapped caller regions whose rep matches a mapped one. - for (unsigned i = 0; i < callerRegions.size() && !merged; i++) { - if (mappedCallerIndices.count(i)) - continue; - auto *rep = callerRegions[i].getRepresentative(); - if (rep && repToMappedCaller.count(rep)) { - unsigned keep = repToMappedCaller[rep]; - if (mergeCalleeRegion(F, keep, i)) { - changed = true; - merged = true; - } - } - } - if (merged) - break; // restart since indices shifted - } - if (changed) - break; +// Merge any overlapping region pairs of F (by the same predicate idx() +// uses) until none remain. Returns true if anything merged. +bool Regions::normalizeOverlaps(const Function *F) { + bool any = false; + bool changed = true; + while (changed) { + changed = false; + auto ®ions = funcRegionVecs[F]; + for (unsigned i = 0; i < regions.size() && !changed; i++) { + for (unsigned j = i + 1; j < regions.size(); j++) { + if (regions[i].overlaps(regions[j]) || + regions[j].overlaps(regions[i])) { + mergeCalleeRegion(F, i, j); + changed = true; + any = true; + break; } - if (changed) - globalChanged = true; } } } + return any; +} + +// Find the existing region of F containing (node, offset) without creating +// or merging anything. Returns -1 if no region covers it. +int Regions::findRegion(const Function *F, const seadsa::Node *node, + unsigned offset) { + if (!node) + return -1; + auto it = funcRegionVecs.find(F); + if (it == funcRegionVecs.end()) + return -1; + auto ®ions = it->second; + for (unsigned r = 0; r < regions.size(); r++) + if (regions[r].getRepresentative() == node && + !((unsigned long)regions[r].getOffset() + regions[r].getLength() <= + offset || + (unsigned long)offset + 1 <= regions[r].getOffset())) + return (int)r; + return -1; } void Regions::computeGlobalMemoryMappings(Module &M) { @@ -1083,19 +1149,26 @@ void Regions::computeGlobalMemoryMappings(Module &M) { 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. + // 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; - unsigned fR = idx(&GV, &F); - unsigned entryR = idx(&GV, entryF); - auto it = mapping.find(fR); + 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[fR] = entryR; + mapping[(unsigned)fR] = (unsigned)entryR; changed = true; - } else if (it->second != entryR) { - mergeCalleeRegion(entryF, it->second, entryR); + } else if (it->second != (unsigned)entryR) { + mergeCalleeRegion(entryF, it->second, (unsigned)entryR); changed = true; } } @@ -1164,18 +1237,21 @@ void Regions::unifySharedRegions(Module &M) { for (auto &m : gm.second) unite(id(gm.first, m.first), id(entryF, m.second)); - // A 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). Classes where some function has three or - // more regions are DSA-collapse artifacts spanning dozens of regions on - // the ntdrivers benchmarks; threading those costs far more than the - // separation is worth, so they still merge. + // 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. std::set classThreaded; { + std::map classSizePre; + for (auto &kv : ids) + classSizePre[find(kv.second)]++; std::map, unsigned> mult; for (auto &kv : ids) mult[{find(kv.second), kv.first.first}]++; @@ -1185,7 +1261,7 @@ void Regions::unifySharedRegions(Module &M) { cur = std::max(cur, m.second); } for (auto &m : maxMult) - if (m.second == 2) + if (m.second == 2 && classSizePre.at(m.first) <= 8) classThreaded.insert(m.first); } @@ -1361,6 +1437,16 @@ Regions::getGlobalMemoryMapping(const Function *F) const { return emptyMapping; } +// Whether v points at allocated (stack/heap) memory, without going through +// idx(): a region probe here would carry the whole pointee extent and merge +// away field-granular regions at translation time. +bool Regions::isAllocatedValue(const llvm::Value *v, const llvm::Function *F) { + if (!DSA) + return true; + auto *node = F ? DSA->getNode(v, *F) : DSA->getNode(v); + return !node || node->isHeap() || node->isAlloca(); +} + int Regions::getSharedRegionIndex(const Function *F, unsigned r) const { auto it = sharedRegionIndex.find({F, r}); if (it != sharedRegionIndex.end()) diff --git a/lib/smack/SmackModuleGenerator.cpp b/lib/smack/SmackModuleGenerator.cpp index a7bb7bc69..865d6b7c6 100644 --- a/lib/smack/SmackModuleGenerator.cpp +++ b/lib/smack/SmackModuleGenerator.cpp @@ -66,10 +66,15 @@ void SmackModuleGenerator::generateProgram(llvm::Module &M) { // match the global declarations (which use entry function's indices). if (rep.entryFunction && F.hasName() && SmackOptions::usesGlobalMemory(F.getName()) && - !SmackOptions::isEntryPoint(F.getName())) + !SmackOptions::isEntryPoint(F.getName())) { rep.currentFunction = rep.entryFunction; - else + // Region probes for this body's values must be translated from its + // own DSA graph into the entry function's graph (field-precise). + getAnalysis().setTranslationSource(&F); + } else { rep.currentFunction = &F; + getAnalysis().setTranslationSource(nullptr); + } SDEBUG(errs() << "Analyzing function: " << naming.get(F) << "\n"); diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 01519bddf..7828c35be 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -376,7 +376,7 @@ SmackRep::memoryMaps(const Function *F) { bool SmackRep::isExternal(const llvm::Value *v) { return v->getType()->isPointerTy() && - !region(regions->idx(v, currentFunction)).isAllocated(); + !regions->isAllocatedValue(v, currentFunction); } const Stmt *SmackRep::alloca(llvm::AllocaInst &i) { From 0d6524ac3d5ca8645564f8c8fdbce217a49b19dc Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Fri, 10 Jul 2026 09:21:50 -0700 Subject: [PATCH 15/15] Emit every memory map at module level MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit floppy2_true still ran 4x slower than develop after the granularity fixes, with an identical CEGAR trajectory (same rounds, same tracked variables, same inlinings) but 4x the per-VC solving time. The structural difference: fine-grained regions produce many single-member classes, which stayed procedure-local maps — and Corral's variable-tracking abstraction applies to global variables only. An untracked global map is havoced for free; a procedure-local map is fully precise in every inlined instance, unconditionally. Local maps are strictly worse than globals under Corral. All regions now get module-level maps: single-member classes and regions outside every mapping bind to shared maps, and the entry function's own regions are all module-level (this is develop's memory layout, at context-sensitive granularity). Procedure-local shadows remain only for the threaded classes, which need .in/.out copies. Boogie and Corral infer the modifies sets. Measured (corral, wall seconds): develop before after floppy2_true 26.6 105.9 39.9 parport_true 56.7 60.5 50.2 cdaudio_true 31.7 29.1 27.4 all 7 ntdrivers 178 ~250 176.5 hid-waltop 43_1a 2.0 1.9 1.8 two_arrays1 51.4 24.5 28.0 The 7-benchmark ntdrivers total now beats develop. All verdicts unchanged; all 2052 regression configurations pass. Co-Authored-By: Claude Fable 5 --- lib/smack/Regions.cpp | 40 ++++++++++++++++++++++++++++++++++++++-- 1 file changed, 38 insertions(+), 2 deletions(-) diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 25f77637c..15548b497 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -1275,6 +1275,7 @@ void Regions::unifySharedRegions(Module &M) { for (auto &kv : ids) classSize[find(kv.second)]++; + std::set> threadedPairs; std::map classShared; for (auto &kv : ids) { const Function *F = kv.first.first; @@ -1285,6 +1286,7 @@ void Regions::unifySharedRegions(Module &M) { // (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) @@ -1302,8 +1304,11 @@ void Regions::unifySharedRegions(Module &M) { funcRegionVecs[entryF][ce->second].markGlobalScope(); continue; } - if (classSize[root] < 2) - continue; // function-private: stays a procedure-local map + // 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 + // is fully precise in every inlined instance (measured 4x slower on + // floppy2). Boogie/Corral infer the modifies sets. auto cs = classShared.find(root); unsigned s; if (cs == classShared.end()) { @@ -1316,6 +1321,37 @@ 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. + for (auto &fr : funcRegions) { + const Function *F = fr.first; + if (F == entryF) + continue; + if (F->hasName() && SmackOptions::usesGlobalMemory(F->getName())) + continue; + for (unsigned r : getAccessedRegions(F)) { + if (r >= funcRegionVecs[F].size()) + continue; + if (threadedPairs.count({F, r}) || sharedRegionIndex.count({F, r})) + continue; + auto gm = globalMemoryMappings.find(F); + if (gm != globalMemoryMappings.end() && gm->second.count(r)) + 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) + for (auto &R : funcRegionVecs[entryF]) + R.markGlobalScope(); } void Regions::computeFunctionRegions(Module &M) {