Avoid unnecessary global allocations in memory-safety checks

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);

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);

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.");

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());
   }
 

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;

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; }

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;
+}