diff --git a/docs/cs-dsa-memory-plan.md b/docs/cs-dsa-memory-plan.md new file mode 100644 index 000000000..454a5d543 --- /dev/null +++ b/docs/cs-dsa-memory-plan.md @@ -0,0 +1,121 @@ +# Context-Sensitive DSA Memory Regions in SMACK + +## Overview + +SMACK uses **context-sensitive** sea-dsa analysis (`-sea-dsa=cs`) with **per-function memory regions**. Each function gets its own region vector computed from its CS graph, and memory maps are threaded through procedure signatures as parameters (reads) and returns (writes). + +```boogie +// Memory maps are local in/out parameters, not globals +procedure foo(x: ref, $M.0.in: [ref]i8) returns ($M.0.out: [ref]i8) +{ var $M.0: [ref]i8; + $M.0 := $M.0.in; + $M.0 := $store.i8($M.0, x, 42); + $M.0.out := $M.0; } + +procedure main() + modifies $M.0; +{ call $M.0 := foo(x, $M.0); } +``` + +Entry points (`main`) keep globals with `modifies` clauses. Non-entry procedures use local in/out parameters. + +--- + +## Architecture + +### Phase 1: Per-Function Region Construction + +**Files:** `Regions.cpp` (runOnModule) + +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`). + +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. + +### Phase 2: Read/Write Sets + +Direct memory accesses in each function are recorded: +- `LoadInst` -> readRegions +- `StoreInst` -> modifiedRegions +- `AtomicCmpXchgInst`, `AtomicRMWInst` -> both +- `MemSetInst` -> modifiedRegions +- `MemTransferInst` -> readRegions (source) + modifiedRegions (dest) + +### Phase 2.5: Global Memory Mappings + +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. + +### Phase 3: Call-Site Mappings + +**`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. + +**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. + +### Phase 3.5: Region Merge Propagation + +**`propagateRegionMerges(M)`** enforces the soundness invariant: **regions must not alias**. Uses SCCs for proper ordering. + +**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. + +**Bottom-up pass:** When a callee has collapsed regions that the caller keeps separate, the caller's regions are merged to match. + +**Key invariant in `mergeCalleeRegion`:** When shifting callee-side keys in call-site mappings, existing entries (typically from parameter mappings) take priority over entries from merged-away regions. This prevents global mapping collisions from overwriting call-site-specific parameter mappings. + +### Phase 4: Transitive Closure + +**`computeFunctionRegions(M)`** propagates callee region accesses to callers through call-site mappings until convergence. Only mapped regions are propagated. + +--- + +## 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. + +### 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. + +### Region Creation from DSA Nodes +The `Region(const seadsa::Node*, LLVMContext&)` constructor enables creating regions for DSA nodes that have no corresponding LLVM Value in the function. This is needed when: +- A caller passes a pointer and the callee accesses through multiple levels of indirection +- Phase 1 link-following discovers reachable nodes +- Phase 3 link-following creates regions during mapping computation + +### Return Value Mapping +Call-site mappings include the callee's 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. + +--- + +## Test Results + +**197 total tests, 195 passed, 0 failed, 2 unknown.** + +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. + +--- + +## File Summary + +| File | Change | +|------|--------| +| `DSAWrapper.h/cpp` | Function-aware `getNode`/`getOffset`/`isTypeSafe` with per-function graph lookup | +| `Regions.h/cpp` | Per-function region vectors, call-site mappings, link-following, merge propagation, `Region(Node*)` constructor | +| `SmackRep.h/cpp` | Memory map params/returns in procedure signatures, call-site mapping for threading | +| `SmackInstGenerator.cpp` | Prologue/epilogue for local memory shadows, entry block initialization | +| `SmackModuleGenerator.cpp` | Local var declarations for non-entry functions, global-scope region handling | +| `Prelude.cpp` | Per-function region types in prelude generation | +| `SmackOptions.h/cpp` | `usesGlobalMemory`, `isEntryPoint` helpers | +| `top.py` | Switch to `-sea-dsa=cs`, fix `VProperty.__members__` for `--check` flag | 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..2333c1136 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,55 @@ 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 +117,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..ff6549130 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,599 @@ 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));