From e79bd749576b58ea4ee7cf3b16d20bf04dab86f2 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Sun, 12 Jul 2026 21:00:19 -0700
Subject: [PATCH] Avoid allocations for unused globals

---
 include/smack/DSAWrapper.h                 |  1 +
 include/smack/SmackRep.h                   |  3 ++-
 lib/smack/DSAWrapper.cpp                   |  6 ++++++
 lib/smack/SmackModuleGenerator.cpp         |  7 ++++++-
 lib/smack/SmackRep.cpp                     |  5 +++--
 test/c/memory-safety/global_alloc_alias.c  |  8 ++++++++
 test/c/memory-safety/global_alloc_unused.c | 11 +++++++++++
 7 files changed, 37 insertions(+), 4 deletions(-)
 create mode 100644 test/c/memory-safety/global_alloc_alias.c
 create mode 100644 test/c/memory-safety/global_alloc_unused.c

diff --git a/include/smack/DSAWrapper.h b/include/smack/DSAWrapper.h
index fa3a392de..f879e2e53 100644
--- a/include/smack/DSAWrapper.h
+++ b/include/smack/DSAWrapper.h
@@ -43,6 +43,7 @@ class DSAWrapper : public llvm::ModulePass {
 
   bool isStaticInitd(const seadsa::Node *n);
   bool isMemOpd(const seadsa::Node *n);
+  bool isAccessed(const llvm::Value *V);
   bool isRead(const llvm::Value *V);
   bool isSingletonGlobal(const llvm::Value *V);
   unsigned getPointedTypeSize(const llvm::Value *v);
diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h
index 44dfe7fe5..99e0dd257 100644
--- a/include/smack/SmackRep.h
+++ b/include/smack/SmackRep.h
@@ -201,7 +201,8 @@ class SmackRep {
   const Stmt *inverseFPCastAssume(const llvm::StoreInst *si);
 
   // used in SmackModuleGenerator
-  std::list<Decl *> globalDecl(const llvm::GlobalValue *g);
+  std::list<Decl *> globalDecl(const llvm::GlobalValue *g,
+                               bool allocate = true);
   void addInitFunc(const llvm::Function *f);
   Decl *getInitFuncs();
   const Expr *declareIsExternal(const Expr *e);
diff --git a/lib/smack/DSAWrapper.cpp b/lib/smack/DSAWrapper.cpp
index 2968fc1e1..9f75c0067 100644
--- a/lib/smack/DSAWrapper.cpp
+++ b/lib/smack/DSAWrapper.cpp
@@ -85,6 +85,12 @@ bool DSAWrapper::isMemOpd(const seadsa::Node *n) {
   return memOpds.count(n) > 0;
 }
 
+bool DSAWrapper::isAccessed(const Value *V) {
+  auto node = getNode(V);
+  assert(node && "Global values should have nodes.");
+  return node->isRead() || node->isModified();
+}
+
 bool DSAWrapper::isRead(const Value *V) {
   auto node = getNode(V);
   assert(node && "Global values should have nodes.");
diff --git a/lib/smack/SmackModuleGenerator.cpp b/lib/smack/SmackModuleGenerator.cpp
index 2c70404f4..36ee3533b 100644
--- a/lib/smack/SmackModuleGenerator.cpp
+++ b/lib/smack/SmackModuleGenerator.cpp
@@ -4,6 +4,7 @@
 #define DEBUG_TYPE "smack-mod-gen"
 #include "smack/SmackModuleGenerator.h"
 #include "smack/BoogieAst.h"
+#include "smack/DSAWrapper.h"
 #include "smack/Debug.h"
 #include "smack/Naming.h"
 #include "smack/Prelude.h"
@@ -25,6 +26,8 @@ void SmackModuleGenerator::getAnalysisUsage(llvm::AnalysisUsage &AU) const {
   AU.setPreservesAll();
   AU.addRequired<llvm::LoopInfoWrapperPass>();
   AU.addRequired<Regions>();
+  if (SmackOptions::MemorySafety)
+    AU.addRequired<DSAWrapper>();
 }
 
 bool SmackModuleGenerator::runOnModule(llvm::Module &m) {
@@ -37,11 +40,13 @@ void SmackModuleGenerator::generateProgram(llvm::Module &M) {
   Naming naming;
   SmackRep rep(&M.getDataLayout(), &naming, program, &getAnalysis<Regions>());
   std::list<Decl *> &decls = program->getDeclarations();
+  DSAWrapper *DSA =
+      SmackOptions::MemorySafety ? &getAnalysis<DSAWrapper>() : nullptr;
 
   SDEBUG(errs() << "Analyzing globals...\n");
 
   for (auto &G : M.globals()) {
-    auto ds = rep.globalDecl(&G);
+    auto ds = rep.globalDecl(&G, !DSA || DSA->isAccessed(&G));
     decls.insert(decls.end(), ds.begin(), ds.end());
   }
 
diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp
index d9fe57086..9b16fb5ba 100644
--- a/lib/smack/SmackRep.cpp
+++ b/lib/smack/SmackRep.cpp
@@ -1261,7 +1261,8 @@ void SmackRep::addAllocSizeAttr(const llvm::GlobalVariable *G,
   }
 }
 
-std::list<Decl *> SmackRep::globalDecl(const llvm::GlobalValue *v) {
+std::list<Decl *> SmackRep::globalDecl(const llvm::GlobalValue *v,
+                                       bool allocate) {
   using namespace llvm;
   std::list<Decl *> decls;
   std::list<const Attr *> ax;
@@ -1322,7 +1323,7 @@ std::list<Decl *> SmackRep::globalDecl(const llvm::GlobalValue *v) {
         Expr::id(name), pointerLit(globalsOffset -= (size + globalsPadding)))));
   }
 
-  if (!llvm::isa<Function>(v))
+  if (!llvm::isa<Function>(v) && allocate)
     globalAllocations[v] = size;
 
   return decls;
diff --git a/test/c/memory-safety/global_alloc_alias.c b/test/c/memory-safety/global_alloc_alias.c
new file mode 100644
index 000000000..e74bd8c64
--- /dev/null
+++ b/test/c/memory-safety/global_alloc_alias.c
@@ -0,0 +1,8 @@
+#include "smack.h"
+
+// @expect verified
+
+int x;
+int *p = &x;
+
+int main(void) { return *p; }
diff --git a/test/c/memory-safety/global_alloc_unused.c b/test/c/memory-safety/global_alloc_unused.c
new file mode 100644
index 000000000..a87821f4a
--- /dev/null
+++ b/test/c/memory-safety/global_alloc_unused.c
@@ -0,0 +1,11 @@
+#include "smack.h"
+
+// @expect verified
+// @checkbpl awk '/call \$galloc/ { found=1 } END { exit found }'
+
+void loga(char *);
+
+int main(void) {
+  loga("aaa");
+  return 0;
+}