Merge branch 'release-2.6.0'

zvonimir · zvonimir · commit c1ccb518fa9e · 2020-09-05T17:29:36.000-06:00
diff --git a/.gitmodules b/.gitmodules
@@ -1,4 +1,3 @@
 [submodule "sea-dsa"]
   path = sea-dsa
   url = https://github.com/seahorn/sea-dsa.git
-  branch = llvm-8.0
diff --git a/.travis.yml b/.travis.yml
@@ -73,6 +73,6 @@ before_script:
   - llvm-config --version
 
 script:
-  - ./format/run-clang-format.py -e test/c/basic/transform-out.c -r lib/smack include/smack share/smack/include share/smack/lib test examples
+  - ./format/run-clang-format.py -r lib/smack include/smack tools share/smack/include share/smack/lib test examples
   - flake8 test/regtest.py share/smack/ --extend-exclude share/smack/svcomp/,share/smack/reach.py
   - INSTALL_RUST=1 ./bin/build.sh
diff --git a/Doxyfile b/Doxyfile
@@ -5,7 +5,7 @@
 #---------------------------------------------------------------------------
 DOXYFILE_ENCODING      = UTF-8
 PROJECT_NAME           = smack
-PROJECT_NUMBER         = 2.5.0
+PROJECT_NUMBER         = 2.6.0
 PROJECT_BRIEF          = "A bounded software verifier."
 PROJECT_LOGO           =
 OUTPUT_DIRECTORY       = docs
diff --git a/bin/versions b/bin/versions
@@ -1,10 +1,10 @@
 Z3_VERSION=4.8.8
-CVC4_VERSION=1.7
+CVC4_VERSION=1.8
 YICES2_VERSION=2.6.2
-BOOGIE_VERSION=2.6.15
+BOOGIE_VERSION=2.7.15
 CORRAL_VERSION=1.0.12
 SYMBOOGLIX_COMMIT=ccb2e7f2b3
 LOCKPWN_COMMIT=12ba58f1ec
-LLVM_SHORT_VERSION=9
-LLVM_FULL_VERSION=9.0.1
-RUST_VERSION=2020-05-21
+LLVM_SHORT_VERSION=10
+LLVM_FULL_VERSION=10.0.1
+RUST_VERSION=2020-08-23
diff --git a/docs/installation.md b/docs/installation.md
@@ -80,8 +80,8 @@ to Docker's official documentation.
 
 SMACK depends on the following projects:
 
-* [LLVM][] version [9.0.1][LLVM-9.0.1]
-* [Clang][] version [9.0.1][Clang-9.0.1]
+* [LLVM][] version [10.0.1][LLVM-10.0.1]
+* [Clang][] version [10.0.1][Clang-10.0.1]
 * [Boost][] version 1.55 or greater
 * [Python][] version 3.6.8 or greater
 * [Ninja][] version 1.5.1 or greater
@@ -210,9 +210,9 @@ shell in the `test` directory by executing
 [CMake]: http://www.cmake.org
 [Python]: http://www.python.org
 [LLVM]: http://llvm.org
-[LLVM-9.0.1]: http://llvm.org/releases/download.html#9.0.1
+[LLVM-10.0.1]: http://llvm.org/releases/download.html#10.0.1
 [Clang]: http://clang.llvm.org
-[Clang-9.0.1]: http://llvm.org/releases/download.html#9.0.1
+[Clang-10.0.1]: http://llvm.org/releases/download.html#10.0.1
 [Boogie]: https://github.com/boogie-org/boogie
 [Corral]: https://github.com/boogie-org/corral
 [Z3]: https://github.com/Z3Prover/z3/
diff --git a/include/smack/Regions.h b/include/smack/Regions.h
@@ -6,6 +6,7 @@
 
 #include "seadsa/Graph.hh"
 #include "llvm/IR/InstVisitor.h"
+#include "llvm/Pass.h"
 
 using namespace llvm;
 
diff --git a/include/smack/SimplifyLibCalls.h b/include/smack/SimplifyLibCalls.h
@@ -12,17 +12,17 @@ namespace smack {
 
 using namespace llvm;
 
-class SimplifyLibCalls : public ModulePass,
+class SimplifyLibCalls : public FunctionPass,
                          public InstVisitor<SimplifyLibCalls> {
 private:
   bool modified;
   LibCallSimplifier *simplifier;
 
 public:
   static char ID;
-  SimplifyLibCalls() : ModulePass(ID) {}
+  SimplifyLibCalls() : FunctionPass(ID) {}
   virtual void getAnalysisUsage(AnalysisUsage &AU) const;
-  virtual bool runOnModule(Module &M);
+  virtual bool runOnFunction(Function &F);
   void visitCallInst(CallInst &);
 };
 } // namespace smack
diff --git a/include/smack/SmackInstGenerator.h b/include/smack/SmackInstGenerator.h
@@ -68,6 +68,7 @@ class SmackInstGenerator : public llvm::InstVisitor<SmackInstGenerator> {
   void visitUnreachableInst(llvm::UnreachableInst &i);
 
   void visitBinaryOperator(llvm::BinaryOperator &I);
+  void visitUnaryOperator(llvm::UnaryOperator &I);
 
   void visitExtractElementInst(llvm::ExtractElementInst &I);
   void visitInsertElementInst(llvm::InsertElementInst &I);
diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h
@@ -85,6 +85,7 @@ class SmackRep {
   bool isFpArithOp(unsigned opcode);
   const Expr *bop(unsigned opcode, const llvm::Value *lhs,
                   const llvm::Value *rhs, const llvm::Type *t);
+  const Expr *uop(const llvm::Value *op);
   const Expr *cmp(unsigned predicate, const llvm::Value *lhs,
                   const llvm::Value *rhs, bool isUnsigned);
   const Expr *select(const llvm::Value *condVal, const llvm::Value *trueVal,
@@ -147,6 +148,9 @@ class SmackRep {
   const Expr *bop(const llvm::BinaryOperator *BO);
   const Expr *bop(const llvm::ConstantExpr *CE);
 
+  const Expr *uop(const llvm::UnaryOperator *UO);
+  const Expr *uop(const llvm::ConstantExpr *CE);
+
   const Expr *cmp(const llvm::CmpInst *I);
   const Expr *cmp(const llvm::ConstantExpr *CE);
 
diff --git a/include/smack/SplitAggregateValue.h b/include/smack/SplitAggregateValue.h
@@ -14,13 +14,13 @@
 
 namespace smack {
 
-class SplitAggregateValue : public llvm::BasicBlockPass {
+class SplitAggregateValue : public llvm::FunctionPass {
 public:
   typedef std::vector<std::pair<llvm::Value *, unsigned>> IndexT;
   typedef std::pair<IndexT, llvm::Constant *> InfoT;
   static char ID;
-  SplitAggregateValue() : llvm::BasicBlockPass(ID) {}
-  virtual bool runOnBasicBlock(llvm::BasicBlock &BB);
+  SplitAggregateValue() : llvm::FunctionPass(ID) {}
+  virtual bool runOnFunction(llvm::Function &F);
 
 private:
   llvm::Value *splitAggregateLoad(llvm::LoadInst *li, std::vector<InfoT> &info,
diff --git a/include/utils/InitializePasses.h b/include/utils/InitializePasses.h
@@ -0,0 +1,13 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+#ifndef UTILS_INITIALIZEPASSES_H
+#define UTILS_INITIALIZEPASSES_H
+
+#include "llvm/InitializePasses.h"
+
+namespace llvm {
+void initializeDevirtualizePass(PassRegistry &Registry);
+} // end namespace llvm
+
+#endif // UTILS_INITIALIZEPASSES_H
diff --git a/lib/smack/AddTiming.cpp b/lib/smack/AddTiming.cpp
@@ -28,6 +28,7 @@
 #include "llvm/IR/IntrinsicInst.h"
 #include "llvm/IR/Value.h"
 #include "llvm/Pass.h"
+#include "llvm/Support/Alignment.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
 
@@ -186,15 +187,16 @@ unsigned 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, SI->getAlignment(),
+    return TTI->getMemoryOpCost(I->getOpcode(), ValTy,
+                                MaybeAlign(SI->getAlignment()),
                                 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(),
-                                LI->getAlignment(),
+                                MaybeAlign(LI->getAlignment()),
                                 LI->getPointerAddressSpace());
   }
   case Instruction::ZExt:
diff --git a/lib/smack/Debug.cpp b/lib/smack/Debug.cpp
@@ -42,15 +42,16 @@ void setCurrentDebugTypes(const char **Types, unsigned Count) {
 
 static ::llvm::cl::opt<bool, true> Debug("debug",
                                          cl::desc("Enable debug output"),
-                                         cl::Hidden, cl::location(DebugFlag));
+                                         cl::Hidden,
+                                         cl::location(smack::DebugFlag));
 
 namespace {
 
 struct DebugOnlyOpt {
   void operator=(const std::string &Val) const {
     if (Val.empty())
       return;
-    DebugFlag = true;
+    smack::DebugFlag = true;
     SmallVector<StringRef, 8> dbgTypes;
     StringRef(Val).split(dbgTypes, ',', -1, false);
     for (auto dbgType : dbgTypes)
diff --git a/lib/smack/ExtractContracts.cpp b/lib/smack/ExtractContracts.cpp
@@ -229,7 +229,8 @@ bool ExtractContracts::runOnModule(Module &M) {
     }
 
     if (!contractBlocks.empty()) {
-      auto *newF = CodeExtractor(contractBlocks).extractCodeRegion();
+      auto *newF = CodeExtractor(contractBlocks)
+                       .extractCodeRegion(CodeExtractorAnalysisCache(*F));
 
       std::vector<CallInst *> Is;
       for (auto V : newF->users())
@@ -258,7 +259,8 @@ bool ExtractContracts::runOnModule(Module &M) {
 
     for (auto const &entry : invariantBlocks) {
       auto BBs = entry.second;
-      auto *newF = CodeExtractor(BBs).extractCodeRegion();
+      auto *newF =
+          CodeExtractor(BBs).extractCodeRegion(CodeExtractorAnalysisCache(*F));
 
       std::vector<CallInst *> Is;
       for (auto V : newF->users())
diff --git a/lib/smack/Naming.cpp b/lib/smack/Naming.cpp
@@ -121,6 +121,7 @@ const std::map<unsigned, std::string> Naming::INSTRUCTION_TABLE{
     {Instruction::FMul, "$fmul"},
     {Instruction::FDiv, "$fdiv"},
     {Instruction::FRem, "$frem"},
+    {Instruction::FNeg, "$fneg"},
     {Instruction::ShuffleVector, "$shufflevector"},
     {Instruction::InsertElement, "$insertelement"},
     {Instruction::ExtractElement, "$extractelement"}};
diff --git a/lib/smack/Prelude.cpp b/lib/smack/Prelude.cpp
@@ -980,7 +980,7 @@ void IntOpGen::generateMemOps(std::stringstream &s) const {
       } else {
         auto loadBody = prelude.mapSelExpr(0);
         auto storeBody = prelude.mapUpdExpr(0, Expr::bvExtract(valExpr, 8, 0));
-        for (unsigned i = 1; i<size>> 3; ++i) {
+        for (unsigned i = 1; i < (size >> 3); ++i) {
           unsigned lowerIdx = i << 3;
           unsigned upperIdx = lowerIdx + 8;
           loadBody = Expr::bvConcat(prelude.mapSelExpr(i), loadBody);
@@ -1333,6 +1333,7 @@ const Attr *FpOp::fpAttrFunc(std::string opName) {
       {"fdiv", "fp.div"},
       {"frem", "fp.rem"},
       {"fma", "fp.fma"},
+      {"fneg", "fp.neg"},
       {"isnormal", "fp.isNormal"},
       {"issubnormal", "fp.isSubnormal"},
       {"iszero", "fp.isZero"},
@@ -1388,7 +1389,7 @@ void FpOpGen::generateArithOps(std::stringstream &s) const {
       {"abs", 1, false}, {"round", 1, true}, {"sqrt", 1, true},
       {"fadd", 2, true}, {"fsub", 2, true},  {"fmul", 2, true},
       {"fdiv", 2, true}, {"frem", 2, false}, {"min", 2, false},
-      {"max", 2, false}, {"fma", 3, true}};
+      {"max", 2, false}, {"fma", 3, true},   {"fneg", 1, false}};
 
   for (auto &f : fpArithOps) {
     if (SmackOptions::FloatEnabled)
diff --git a/lib/smack/SimplifyLibCalls.cpp b/lib/smack/SimplifyLibCalls.cpp
@@ -28,15 +28,16 @@ void SimplifyLibCalls::getAnalysisUsage(AnalysisUsage &AU) const {
   AU.addRequired<TargetLibraryInfoWrapperPass>();
 }
 
-bool SimplifyLibCalls::runOnModule(Module &M) {
+bool SimplifyLibCalls::runOnFunction(Function &F) {
   modified = false;
   simplifier = new LibCallSimplifier(
-      M.getDataLayout(), &getAnalysis<TargetLibraryInfoWrapperPass>().getTLI(),
+      F.getParent()->getDataLayout(),
+      &getAnalysis<TargetLibraryInfoWrapperPass>().getTLI(F),
       getAnalysis<OptimizationRemarkEmitterWrapperPass>().getORE(),
       &getAnalysis<BlockFrequencyInfoWrapperPass>().getBFI(),
       &getAnalysis<ProfileSummaryInfoWrapperPass>().getPSI());
   if (simplifier)
-    visit(M);
+    visit(F);
   return modified;
 }
 
diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp
@@ -200,7 +200,7 @@ void SmackInstGenerator::generatePhiAssigns(llvm::Instruction &ti) {
 
       llvm::PHINode *phi = llvm::cast<llvm::PHINode>(s);
       if (llvm::Value *v = phi->getIncomingValueForBlock(block)) {
-        v = v->stripPointerCasts();
+        v = v->stripPointerCastsAndAliases();
         lhs.push_back(rep->expr(phi));
         rhs.push_back(rep->expr(v));
       }
@@ -372,6 +372,20 @@ void SmackInstGenerator::visitBinaryOperator(llvm::BinaryOperator &I) {
   emit(Stmt::assign(rep->expr(&I), E));
 }
 
+/******************************************************************************/
+/*                   UNARY                    OPERATIONS                     */
+/******************************************************************************/
+
+void SmackInstGenerator::visitUnaryOperator(llvm::UnaryOperator &I) {
+  assert(I.getOpcode() == Instruction::FNeg && !isa<VectorType>(I.getType()) &&
+         "Unsupported unary operation!");
+  processInstruction(I);
+  SmackWarnings::warnIfUnsound(std::string("floating-point arithmetic ") +
+                                   I.getOpcodeName(),
+                               SmackOptions::FloatEnabled, currBlock, &I);
+  emit(Stmt::assign(rep->expr(&I), rep->uop(&I)));
+}
+
 /******************************************************************************/
 /*                   VECTOR                    OPERATIONS                     */
 /******************************************************************************/
@@ -505,7 +519,7 @@ void SmackInstGenerator::visitLoadInst(llvm::LoadInst &li) {
 void SmackInstGenerator::visitStoreInst(llvm::StoreInst &si) {
   processInstruction(si);
   const llvm::Value *P = si.getPointerOperand();
-  const llvm::Value *V = si.getValueOperand()->stripPointerCasts();
+  const llvm::Value *V = si.getValueOperand()->stripPointerCastsAndAliases();
   assert(!V->getType()->isAggregateType() && "Unexpected store value.");
 
   if (isa<VectorType>(V->getType())) {
@@ -635,7 +649,7 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) {
   Function *f = ci.getCalledFunction();
   if (!f) {
     assert(ci.getCalledValue() && "Called value is null");
-    f = cast<Function>(ci.getCalledValue()->stripPointerCasts());
+    f = cast<Function>(ci.getCalledValue()->stripPointerCastsAndAliases());
   }
 
   std::string name = f->hasName() ? f->getName() : "";
@@ -834,7 +848,7 @@ void SmackInstGenerator::visitDbgValueInst(llvm::DbgValueInst &dvi) {
       auto currInst = std::prev(nextInst);
       if (currInst != dvi.getParent()->begin()) {
         const Instruction &pi = *std::prev(currInst);
-        V = V->stripPointerCasts();
+        V = V->stripPointerCastsAndAliases();
         if (!llvm::isa<const PHINode>(&pi) &&
             V == llvm::dyn_cast<const Value>(&pi))
           emit(recordProcedureCall(
diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp
@@ -355,7 +355,7 @@ const Stmt *SmackRep::valueAnnotation(const CallInst &CI) {
 
   assert(CI.getNumArgOperands() > 0 && "Expected at least one argument.");
   assert(CI.getNumArgOperands() <= 2 && "Expected at most two arguments.");
-  const Value *V = CI.getArgOperand(0)->stripPointerCasts();
+  const Value *V = CI.getArgOperand(0)->stripPointerCastsAndAliases();
 
   if (CI.getNumArgOperands() == 1) {
     name = indexedName(Naming::VALUE_PROC, {type(V->getType())});
@@ -788,7 +788,7 @@ const Expr *SmackRep::expr(const llvm::Value *v, bool isConstIntUnsigned) {
   using namespace llvm;
 
   if (isa<const Constant>(v)) {
-    v = v->stripPointerCasts();
+    v = v->stripPointerCastsAndAliases();
   }
 
   if (isa<GlobalValue>(v)) {
@@ -924,6 +924,19 @@ const Expr *SmackRep::bop(unsigned opcode, const llvm::Value *lhs,
   return Expr::fn(opName(fn, {t}), expr(lhs), expr(rhs));
 }
 
+const Expr *SmackRep::uop(const llvm::ConstantExpr *CE) {
+  return uop(CE->getOperand(0));
+}
+
+const Expr *SmackRep::uop(const llvm::UnaryOperator *UO) {
+  return uop(UO->getOperand(0));
+}
+
+const Expr *SmackRep::uop(const llvm::Value *op) {
+  std::string fn = Naming::INSTRUCTION_TABLE.at(Instruction::FNeg);
+  return Expr::fn(opName(fn, {op->getType()}), expr(op));
+}
+
 const Expr *SmackRep::cmp(const llvm::CmpInst *I) {
   return cmp(I->getPredicate(), I->getOperand(0), I->getOperand(1),
              I->isUnsigned());
diff --git a/lib/smack/SmackWarnings.cpp b/lib/smack/SmackWarnings.cpp
@@ -38,8 +38,12 @@ SmackWarnings::getUnsetFlags(RequiredFlagsT requiredFlags) {
 
 std::string SmackWarnings::getFlagStr(UnsetFlagsT flags) {
   std::string ret = "";
-  for (auto f : flags)
-    ret += ("--" + f->ArgStr.str() + " ");
+  for (auto f : flags) {
+    if (f->ArgStr.str() == "bit-precise")
+      ret += ("--integer-encoding=bit-vector ");
+    else
+      ret += ("--" + f->ArgStr.str() + " ");
+  }
   return ret;
 }
 
diff --git a/lib/smack/SplitAggregateValue.cpp b/lib/smack/SplitAggregateValue.cpp
diff --git a/lib/utils/Devirt.cpp b/lib/utils/Devirt.cpp
diff --git a/sea-dsa b/sea-dsa
diff --git a/share/smack/reach.py b/share/smack/reach.py
diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
diff --git a/share/smack/top.py b/share/smack/top.py
diff --git a/test/c/basic/transform-out.c b/test/c/basic/transform-out.c
diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp
