Prototype LLVM 15 support

.gitmodules

@@ -1,3 +1,3 @@
 [submodule "sea-dsa"]
   path = sea-dsa
-  url = https://github.com/seahorn/sea-dsa.git
+  url = https://github.com/shaobo-he/sea-dsa.git

bin/versions

@@ -5,6 +5,6 @@ BOOGIE_VERSION="2.15.7"
 CORRAL_VERSION="1.1.8"
 SYMBOOGLIX_COMMIT="ccb2e7f2b3"
 LOCKPWN_COMMIT="12ba58f1ec"
-LLVM_SHORT_VERSION="14"
-LLVM_FULL_VERSION="14.0.0"
+LLVM_SHORT_VERSION="15"
+LLVM_FULL_VERSION="15.0.6"
 RUST_VERSION="nightly-2022-08-12"

include/smack/BoogieAst.h

@@ -605,7 +605,7 @@ class ProcDecl : public Decl, public CodeContainer {
 
   ParameterList params;
   ParameterList rets;
-  SpecificationList requires;
+  SpecificationList requires_;
   SpecificationList ensures;
 
 public:
@@ -622,9 +622,9 @@ class ProcDecl : public Decl, public CodeContainer {
   ParameterList &getReturns() { return rets; }
 
   typedef SpecificationList::iterator spec_iterator;
-  spec_iterator requires_begin() { return requires.begin(); }
-  spec_iterator requires_end() { return requires.end(); }
-  SpecificationList &getRequires() { return requires; }
+  spec_iterator requires_begin() { return requires_.begin(); }
+  spec_iterator requires_end() { return requires_.end(); }
+  SpecificationList &getRequires() { return requires_; }
 
   spec_iterator ensures_begin() { return ensures.begin(); }
   spec_iterator ensures_end() { return ensures.end(); }

include/smack/SmackRep.h

@@ -172,8 +172,9 @@ class SmackRep {
   const Stmt *alloca(llvm::AllocaInst &i);
   const Stmt *memcpy(const llvm::MemCpyInst &msi);
   const Stmt *memset(const llvm::MemSetInst &msi);
-  const Expr *load(const llvm::Value *P);
+  const Expr *load(const llvm::Value *P, const llvm::Type *T);
   const Stmt *store(const llvm::Value *P, const llvm::Value *V);
+  const Stmt *store(const llvm::Value *P, const llvm::Type *T, const Expr *V);
   const Stmt *store(const llvm::Value *P, const Expr *V);
 
   const Stmt *valueAnnotation(const llvm::CallInst &CI);

include/smack/VectorOperations.h

@@ -38,8 +38,8 @@ class VectorOperations {
   FuncDecl *shuffle(Type *T, Type *U, std::vector<int> mask);
   FuncDecl *insert(Type *T, Type *IT);
   FuncDecl *extract(Type *T, Type *IT);
-  FuncDecl *load(const Value *V);
-  FuncDecl *store(const Value *V);
+  FuncDecl *load(const Value *V, Type *ET);
+  FuncDecl *store(const Value *V, Type *ET);
 };
 } // namespace smack
 

lib/smack/AddTiming.cpp

@@ -26,6 +26,7 @@
 #include "llvm/IR/Function.h"
 #include "llvm/IR/Instructions.h"
 #include "llvm/IR/IntrinsicInst.h"
+#include "llvm/IR/Operator.h"
 #include "llvm/IR/Value.h"
 #include "llvm/Pass.h"
 #include "llvm/Support/Alignment.h"
@@ -137,7 +138,7 @@ InstructionCost AddTiming::getInstructionCost(const Instruction *I) const {
 
   switch (I->getOpcode()) {
   case Instruction::GetElementPtr: {
-    Type *ValTy = I->getOperand(0)->getType()->getPointerElementType();
+    Type *ValTy = cast<GetElementPtrInst>(I)->getSourceElementType();
     return TTI->getAddressComputationCost(ValTy);
   }
 
@@ -189,16 +190,14 @@ InstructionCost AddTiming::getInstructionCost(const Instruction *I) const {
     Type *ValTy = SI->getValueOperand()->getType();
     assert(!ValTy->isStructTy() &&
            "Timing annotations do not currently work for struct sized stores");
-    return TTI->getMemoryOpCost(I->getOpcode(), ValTy,
-                                Align(SI->getAlignment()),
+    return TTI->getMemoryOpCost(I->getOpcode(), ValTy, SI->getAlign(),
                                 SI->getPointerAddressSpace());
   }
   case Instruction::Load: {
     const LoadInst *LI = cast<LoadInst>(I);
     assert(!I->getType()->isStructTy() &&
            "Timing annotations do not currently work for struct sized loads");
-    return TTI->getMemoryOpCost(I->getOpcode(), I->getType(),
-                                Align(LI->getAlignment()),
+    return TTI->getMemoryOpCost(I->getOpcode(), I->getType(), LI->getAlign(),
                                 LI->getPointerAddressSpace());
   }
   case Instruction::ZExt:

lib/smack/BoogieAst.cpp

@@ -644,9 +644,10 @@ void ProcDecl::print(std::ostream &os) const {
     os << "\n";
     print_seq<std::string>(os, mods, "  modifies ", ", ", ";");
   }
-  if (requires.size() > 0) {
+  if (requires_.size() > 0) {
     os << "\n";
-    print_seq<const Expr *>(os, requires, "  requires ", ";\n  requires ", ";");
+    print_seq<const Expr *>(os, requires_, "  requires ", ";\n  requires ",
+                            ";");
   }
   if (ensures.size() > 0) {
     os << "\n";

lib/smack/CodifyStaticInits.cpp

@@ -24,6 +24,30 @@ namespace smack {
 
 using namespace llvm;
 
+namespace {
+using StaticInitItem = std::tuple<Constant *, Constant *, std::vector<Value *>>;
+
+void enqueueGlobal(GlobalVariable *G, std::deque<StaticInitItem> &worklist,
+                   std::set<const GlobalVariable *> &seen) {
+  if (!G || !G->hasInitializer() || !seen.insert(G).second)
+    return;
+  worklist.push_back(
+      std::make_tuple(G->getInitializer(), G, std::vector<Value *>()));
+}
+
+void enqueueReferencedGlobals(Constant *C, std::deque<StaticInitItem> &worklist,
+                              std::set<const GlobalVariable *> &seen) {
+  if (auto *G = dyn_cast<GlobalVariable>(C->stripPointerCasts())) {
+    enqueueGlobal(G, worklist, seen);
+    return;
+  }
+
+  for (Use &O : C->operands())
+    if (auto *SubC = dyn_cast<Constant>(O.get()))
+      enqueueReferencedGlobals(SubC, worklist, seen);
+}
+} // namespace
+
 bool CodifyStaticInits::runOnModule(Module &M) {
   TD = &M.getDataLayout();
   LLVMContext &C = M.getContext();
@@ -36,26 +60,27 @@ bool CodifyStaticInits::runOnModule(Module &M) {
   BasicBlock *B = BasicBlock::Create(C, "entry", F);
   IRBuilder<> IRB(B);
 
-  std::deque<std::tuple<Constant *, Constant *, std::vector<Value *>>> worklist;
+  std::deque<StaticInitItem> worklist;
+  std::set<const GlobalVariable *> seen;
 
   for (auto &G : M.globals())
     if (G.hasInitializer() && DSA->isRead(&G))
-      worklist.push_back(
-          std::make_tuple(G.getInitializer(), &G, std::vector<Value *>()));
+      enqueueGlobal(&G, worklist, seen);
 
   while (worklist.size()) {
     Constant *V = std::get<0>(worklist.front());
     Constant *P = std::get<1>(worklist.front());
     std::vector<Value *> I = std::get<2>(worklist.front());
     worklist.pop_front();
+    enqueueReferencedGlobals(V, worklist, seen);
 
     if (V->getType()->isIntegerTy() || V->getType()->isPointerTy() ||
         V->getType()->isFloatingPointTy() || V->getType()->isVectorTy())
 
-      IRB.CreateStore(
-          V,
-          IRB.CreateGEP(P->getType()->getScalarType()->getPointerElementType(),
-                        P, ArrayRef<Value *>(I)));
+      IRB.CreateStore(V, IRB.CreateGEP(cast<GlobalVariable>(
+                                           P->stripPointerCastsAndAliases())
+                                           ->getValueType(),
+                                       P, ArrayRef<Value *>(I)));
 
     else if (ArrayType *AT = dyn_cast<ArrayType>(V->getType()))
       for (unsigned i = AT->getNumElements(); i-- > 0;) {

lib/smack/DSAWrapper.cpp

@@ -11,6 +11,7 @@
 #include "smack/SmackOptions.h"
 #include "llvm/IR/InstIterator.h"
 #include "llvm/IR/IntrinsicInst.h"
+#include "llvm/IR/Operator.h"
 #include "llvm/Support/FileSystem.h"
 
 #include <set>
@@ -22,6 +23,43 @@ namespace smack {
 
 using namespace llvm;
 
+namespace {
+Type *inferPointeeType(const Value *V) {
+  V = V->stripPointerCastsAndAliases();
+
+  if (const auto *AI = dyn_cast<AllocaInst>(V))
+    return AI->getAllocatedType();
+  if (const auto *GV = dyn_cast<GlobalVariable>(V))
+    return GV->getValueType();
+  if (const auto *GEP = dyn_cast<GEPOperator>(V))
+    return GEP->getResultElementType();
+
+  Type *Evidence = nullptr;
+  for (const User *U : V->users()) {
+    Type *Candidate = nullptr;
+    if (const auto *LI = dyn_cast<LoadInst>(U)) {
+      if (LI->getPointerOperand()->stripPointerCastsAndAliases() == V)
+        Candidate = LI->getType();
+    } else if (const auto *SI = dyn_cast<StoreInst>(U)) {
+      if (SI->getPointerOperand()->stripPointerCastsAndAliases() == V)
+        Candidate = SI->getValueOperand()->getType();
+    } else if (const auto *GEP = dyn_cast<GEPOperator>(U)) {
+      if (GEP->getPointerOperand()->stripPointerCastsAndAliases() == V)
+        Candidate = GEP->getSourceElementType();
+    }
+
+    if (!Candidate)
+      continue;
+    if (!Evidence)
+      Evidence = Candidate;
+    else if (Evidence != Candidate)
+      return nullptr;
+  }
+
+  return Evidence;
+}
+} // namespace
+
 void DSAWrapper::getAnalysisUsage(llvm::AnalysisUsage &AU) const {
   AU.setPreservesAll();
   AU.addRequiredTransitive<seadsa::DsaAnalysis>();
@@ -92,8 +130,10 @@ bool DSAWrapper::isRead(const Value *V) {
 }
 
 unsigned DSAWrapper::getPointedTypeSize(const Value *v) {
-  if (llvm::PointerType *t = llvm::dyn_cast<llvm::PointerType>(v->getType())) {
-    llvm::Type *pointedType = t->getElementType();
+  if (v->getType()->isPointerTy()) {
+    llvm::Type *pointedType = inferPointeeType(v);
+    if (!pointedType)
+      return UINT_MAX;
     if (pointedType->isSized())
       return dataLayout->getTypeStoreSize(pointedType);
     else

lib/smack/MemorySafetyChecker.cpp

@@ -80,21 +80,14 @@ Value *accessSizeAsPointer(Module &M, Type *T) {
       PointerType::getUnqual(Type::getInt8Ty(M.getContext())));
 }
 
-Value *accessSizeAsPointer(Module &M, Value *V) {
-  auto T = dyn_cast<PointerType>(V->getType());
-  assert(T && "expected pointer type");
-
-  return accessSizeAsPointer(M, T->getPointerElementType());
-}
-
 Value *accessSizeAsPointer(LoadInst &I) {
   auto &M = *I.getParent()->getParent()->getParent();
-  return accessSizeAsPointer(M, I.getPointerOperand());
+  return accessSizeAsPointer(M, I.getType());
 }
 
 Value *accessSizeAsPointer(StoreInst &I) {
   auto &M = *I.getParent()->getParent()->getParent();
-  return accessSizeAsPointer(M, I.getPointerOperand());
+  return accessSizeAsPointer(M, I.getValueOperand()->getType());
 }
 } // namespace
 
@@ -113,10 +106,14 @@ bool MemorySafetyChecker::visitSplitAggregateAccess(Value *addr,
     if (auto *GEP = dyn_cast<GEPOperator>(addr)) {
       base = GEP->getPointerOperand();
       T = GEP->getSourceElementType();
+    } else if (auto *LI = dyn_cast<LoadInst>(I)) {
+      T = LI->getType();
+    } else if (auto *SI = dyn_cast<StoreInst>(I)) {
+      T = SI->getValueOperand()->getType();
     } else {
       auto *PT = dyn_cast<PointerType>(addr->getType());
       assert(PT && "expected pointer type");
-      T = PT->getPointerElementType();
+      T = Type::getInt8Ty(M.getContext());
     }
 
     insertMemoryAccessCheck(base, accessSizeAsPointer(M, T), I);

lib/smack/Prelude.cpp

@@ -1187,7 +1187,7 @@ void PtrOpGen::generatePtrNumConvs(std::stringstream &s) const {
 
   // e.g., function {:inline} $p2i.ref.i8(p: ref) returns (i8) {
   // $trunc.i64.i8(p) }
-  for (unsigned i = 8; i <= 64; i <<= 1) {
+  for (auto i : IntOpGen::INTEGER_SIZES) {
     s << Decl::function(
              indexedName("$p2i", {Naming::PTR_TYPE, prelude.rep.intType(i)}),
              {{"p", Naming::PTR_TYPE}}, prelude.rep.intType(i),