Merge branch 'release-2.1.0'

.travis.yml

@@ -39,21 +39,21 @@ env:
 
 before_install:
   - sudo rm -rf /usr/local/clang-7.0.0
-  - sudo add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial-4.0 main"
+  - sudo add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial-5.0 main"
   - wget -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
   - sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF
   - sudo apt-get install -y apt-transport-https
   - echo "deb https://download.mono-project.com/repo/ubuntu stable-xenial main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
   - sudo apt-get update
 
 install:
-  - sudo apt-get install -y clang-4.0 clang-format-4.0 llvm-4.0-dev mono-complete ninja-build
-  - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-4.0 20
-  - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-4.0 20
-  - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-4.0 20
-  - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-4.0 20
-  - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-4.0 20
-  - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-4.0 20
+  - sudo apt-get install -y clang-5.0 clang-format-5.0 llvm-5.0-dev mono-complete ninja-build
+  - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-5.0 20
+  - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-5.0 20
+  - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-5.0 20
+  - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-5.0 20
+  - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-5.0 20
+  - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-5.0 20
   - sudo pip install pyyaml psutil
 
 script:

CMakeLists.txt

@@ -6,7 +6,7 @@ cmake_minimum_required(VERSION 2.8)
 project(smack)
 
 if (NOT WIN32 OR MSYS OR CYGWIN)
-  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-4.0 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
+  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-5.0 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
 
   if (LLVM_CONFIG_EXECUTABLE STREQUAL "LLVM_CONFIG_EXECUTABLE-NOTFOUND")
     message(FATAL_ERROR "llvm-config could not be found!")

Doxyfile

@@ -5,7 +5,7 @@
 #---------------------------------------------------------------------------
 DOXYFILE_ENCODING      = UTF-8
 PROJECT_NAME           = smack
-PROJECT_NUMBER         = 2.0.0
+PROJECT_NUMBER         = 2.1.0
 PROJECT_BRIEF          = "A bounded software verifier."
 PROJECT_LOGO           =
 OUTPUT_DIRECTORY       = docs

bin/versions

@@ -5,6 +5,6 @@ BOOGIE_COMMIT=5c829b6340
 CORRAL_COMMIT=c446f5e827
 SYMBOOGLIX_COMMIT=7210e5d09b
 LOCKPWN_COMMIT=73eddf97bd
-LLVM_SHORT_VERSION=4.0
-LLVM_FULL_VERSION=4.0.1
+LLVM_SHORT_VERSION=5.0
+LLVM_FULL_VERSION=5.0.2
 RUST_VERSION=2016-12-16

docs/installation.md

@@ -80,8 +80,8 @@ to Docker's official documentation.
 
 SMACK depends on the following projects:
 
-* [LLVM][] version [4.0.1][LLVM-4.0.1]
-* [Clang][] version [4.0.1][Clang-4.0.1]
+* [LLVM][] version [5.0.2][LLVM-5.0.2]
+* [Clang][] version [5.0.2][Clang-5.0.2]
 * [Python][] version 2.7 or greater
 * [Ninja][] version 1.5.1 or greater
 * [Mono][] version 5.0.0 or greater (except on Windows)
@@ -203,9 +203,9 @@ shell in the `test` directory by executing
 [CMake]: http://www.cmake.org
 [Python]: http://www.python.org
 [LLVM]: http://llvm.org
-[LLVM-4.0.1]: http://llvm.org/releases/download.html#4.0.1
+[LLVM-5.0.2]: http://llvm.org/releases/download.html#5.0.2
 [Clang]: http://clang.llvm.org
-[Clang-4.0.1]: http://llvm.org/releases/download.html#4.0.1
+[Clang-5.0.2]: http://llvm.org/releases/download.html#5.0.2
 [Boogie]: https://github.com/boogie-org/boogie
 [Corral]: https://github.com/boogie-org/corral
 [Z3]: https://github.com/Z3Prover/z3/

docs/running.md

@@ -107,7 +107,7 @@ SMACK should report no errors for this example.
 
 Under the hood, SMACK first compiles the example into an LLVM bitcode file using Clang:
 ```Shell
-clang -c -Wall -emit-llvm -O0 -g -I../../share/smack/include simple.c -o simple.bc
+clang -c -Wall -emit-llvm -O0 -g -Xclang -disable-O0-optnone -I../../share/smack/include simple.c -o simple.bc
 ```
 We use the `-g` flag to compile with debug information enabled, which the SMACK
 verifier leverages to generate more informative error traces. Then, the generated bitcode

include/smack/BoogieAst.h

@@ -680,6 +680,6 @@ std::ostream &operator<<(std::ostream &os, const Expr *e);
 
 std::ostream &operator<<(std::ostream &os, Decl &e);
 std::ostream &operator<<(std::ostream &os, Decl *e);
-}
+} // namespace smack
 
 #endif // BOOGIEAST_H

include/smack/BplFilePrinter.h

@@ -23,6 +23,6 @@ class BplFilePrinter : public llvm::ModulePass {
 
   virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const;
 };
-}
+} // namespace smack
 
 #endif // BPLPRINTER_H

include/smack/BplPrinter.h

@@ -17,6 +17,6 @@ class BplPrinter : public llvm::ModulePass {
   virtual bool runOnModule(llvm::Module &m);
   virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const;
 };
-}
+} // namespace smack
 
 #endif // BPLPRINTER_H

include/smack/CodifyStaticInits.h

@@ -20,4 +20,4 @@ class CodifyStaticInits : public llvm::ModulePass {
   virtual bool runOnModule(llvm::Module &M);
   virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const;
 };
-}
+} // namespace smack

include/smack/Contracts.h

@@ -33,4 +33,4 @@ class ContractsExtractor : public InstVisitor<ContractsExtractor> {
     return ConstantInt::get(Type::getInt32Ty(ctx), slices.size());
   }
 };
-}
+} // namespace smack

include/smack/DSAWrapper.h

@@ -17,7 +17,7 @@ class DSGraph;
 class TDDataStructures;
 class BUDataStructures;
 class DSNodeEquivs;
-}
+} // namespace llvm
 
 namespace dsa {
 template <class dsa> struct TypeSafety;
@@ -74,6 +74,6 @@ class DSAWrapper : public llvm::ModulePass {
   const llvm::DSNode *getNode(const llvm::Value *v);
   void printDSAGraphs(const char *Filename);
 };
-}
+} // namespace smack
 
 #endif // DSAWRAPPER_H

include/smack/ExtractContracts.h

@@ -16,4 +16,4 @@ class ExtractContracts : public ModulePass {
   virtual bool runOnModule(Module &M);
   virtual void getAnalysisUsage(AnalysisUsage &AU) const;
 };
-}
+} // namespace smack

include/smack/IntegerOverflowChecker.h

@@ -32,6 +32,6 @@ class IntegerOverflowChecker : public llvm::ModulePass {
   void addBlockingAssume(llvm::Function *va, llvm::Value *flag,
                          llvm::Instruction *i);
 };
-}
+} // namespace smack
 
 #endif // INTEGEROVERFLOWCHECKER_H

include/smack/MemorySafetyChecker.h

@@ -35,6 +35,6 @@ class MemorySafetyChecker : public llvm::FunctionPass,
   void visitMemSetInst(llvm::MemSetInst &I);
   void visitMemTransferInst(llvm::MemTransferInst &I);
 };
-}
+} // namespace smack
 
 #endif // MEMORYSAFETYCHECKER_H

include/smack/Naming.h

@@ -116,6 +116,6 @@ class Naming {
   static bool isSmackGeneratedName(std::string s);
   static std::string escape(std::string s);
 };
-}
+} // namespace smack
 
 #endif

include/smack/NormalizeLoops.h

@@ -19,6 +19,6 @@ class NormalizeLoops : public llvm::ModulePass {
   virtual bool runOnModule(llvm::Module &m) override;
   virtual void getAnalysisUsage(llvm::AnalysisUsage &) const override;
 };
-}
+} // namespace smack
 
 #endif // NORMALIZELOOPS_H

include/smack/Prelude.h

@@ -215,6 +215,6 @@ class Prelude {
   FuncDecl *unsafeStore(Binding elemBinding, const Expr *body,
                         bool bytes = true);
 };
-}
+} // namespace smack
 
 #endif // PRELUDE_H

include/smack/Regions.h

@@ -92,6 +92,6 @@ class Regions : public ModulePass, public InstVisitor<Regions> {
   void visitMemIntrinsic(MemIntrinsic &);
   void visitCallInst(CallInst &);
 };
-}
+} // namespace smack
 
 #endif // REGIONS_H

include/smack/RemoveDeadDefs.h

@@ -18,4 +18,4 @@ class RemoveDeadDefs : public llvm::ModulePass {
   RemoveDeadDefs() : llvm::ModulePass(ID) {}
   virtual bool runOnModule(llvm::Module &M);
 };
-}
+} // namespace smack

include/smack/SimplifyLibCalls.h

@@ -25,4 +25,4 @@ class SimplifyLibCalls : public ModulePass,
   virtual bool runOnModule(Module &M);
   void visitCallInst(CallInst &);
 };
-}
+} // namespace smack

include/smack/Slicing.h

@@ -40,6 +40,6 @@ class Slice {
   const Decl *getBoogieDecl(Naming *naming, SmackRep *rep);
   const Expr *getBoogieExpression(Naming *naming, SmackRep *rep);
 };
-}
+} // namespace smack
 
 #endif

include/smack/SmackInstGenerator.h

@@ -98,6 +98,6 @@ class SmackInstGenerator : public llvm::InstVisitor<SmackInstGenerator> {
   void visitMemSetInst(llvm::MemSetInst &i);
   void visitIntrinsicInst(llvm::IntrinsicInst &i);
 };
-}
+} // namespace smack
 
 #endif // SMACKINSTVISITOR_H

include/smack/SmackModuleGenerator.h

@@ -23,6 +23,6 @@ class SmackModuleGenerator : public llvm::ModulePass {
   void generateProgram(llvm::Module &m);
   Program *getProgram() { return program; }
 };
-}
+} // namespace smack
 
 #endif // SMACKMODULEGENERATOR_H

include/smack/SmackOptions.h

@@ -32,6 +32,6 @@ class SmackOptions {
 
   static bool isEntryPoint(std::string);
 };
-}
+} // namespace smack
 
 #endif // SMACKREP_H

include/smack/SmackRep.h

@@ -197,6 +197,6 @@ class SmackRep {
   std::string opName(const std::string &operation,
                      std::list<const llvm::Type *> types);
 };
-}
+} // namespace smack
 
 #endif // SMACKREP_H

include/smack/SmackWarnings.h

@@ -50,6 +50,6 @@ class SmackWarnings {
   static bool isSufficientWarningLevel(WarningLevel level);
   static std::string getFlagStr(UnsetFlagsT flags);
 };
-}
+} // namespace smack
 
 #endif // SMACKWARNINGS_H

include/smack/SplitAggregateValue.h

@@ -36,4 +36,4 @@ class SplitAggregateValue : public llvm::BasicBlockPass {
                                    std::vector<InfoT> &info, llvm::Value *V);
   bool isConstantAggregate(llvm::Value *V);
 };
-}
+} // namespace smack

include/smack/VectorOperations.h

@@ -41,6 +41,6 @@ class VectorOperations {
   FuncDecl *load(const Value *V);
   FuncDecl *store(const Value *V);
 };
-}
+} // namespace smack
 
 #endif // VECTOROPERATIONS_H

include/smack/VerifierCodeMetadata.h

@@ -26,4 +26,4 @@ class VerifierCodeMetadata : public ModulePass,
   void visitInstruction(Instruction &);
   static bool isMarked(const Instruction &I);
 };
-}
+} // namespace smack

lib/AssistDS/ArgCast.cpp

@@ -153,8 +153,8 @@ bool ArgCast::runOnModule(Module& M) {
           } 
         } 
       } else {
-        SDEBUG(ArgType->dump());
-        SDEBUG(FormalType->dump());
+        SDEBUG(ArgType->print(smack::dbgs(), true));
+        SDEBUG(FormalType->print(smack::dbgs(), true));
         break;
       }
     }
@@ -199,10 +199,10 @@ bool ArgCast::runOnModule(Module& M) {
     // Debug printing
     SDEBUG(errs() << "ARGCAST:");
     SDEBUG(errs() << "ERASE:");
-    SDEBUG(CI->dump());
+    SDEBUG(CI->print(smack::dbgs(), true));
     SDEBUG(errs() << "ARGCAST:");
     SDEBUG(errs() << "ADDED:");
-    SDEBUG(CINew->dump());
+    SDEBUG(CINew->print(smack::dbgs(), true));
 
     CI->eraseFromParent();
     numChanged++;

lib/AssistDS/DSNodeEquivs.cpp

@@ -116,7 +116,7 @@ FunctionList DSNodeEquivs::getCallees(CallSite &CS) {
   SDEBUG(
   if (Callees.empty()) {
     errs() << "Failed to get callees for callsite:\n";
-    CS.getInstruction()->dump();
+    CS.getInstruction()->print(smack::dbgs(), true);
   });
 
   return Callees;

lib/AssistDS/Devirt.cpp

@@ -237,7 +237,7 @@ Devirtualize::buildBounce (CallSite CS, std::vector<const Function*>& Targets) {
   // Set the names of the arguments.
   //
   F->arg_begin()->setName("funcPtr");
-  for (auto A = ++F->arg_begin(), E = F->arg_end(); A != E; ++A)
+  for (auto A = std::next(F->arg_begin()), E = F->arg_end(); A != E; ++A)
     A->setName("arg");
 
   //
@@ -263,7 +263,7 @@ Devirtualize::buildBounce (CallSite CS, std::vector<const Function*>& Targets) {
     std::vector<Value*> Args;
     Function::arg_iterator P, PE;
     FunctionType::param_iterator T, TE;
-    for (P = ++F->arg_begin(), PE = F->arg_end(),
+    for (P = std::next(F->arg_begin()), PE = F->arg_end(),
          T = FT->param_begin(), TE = FT->param_end();
          P != PE && T != TE; ++P, ++T)
       Args.push_back(castTo(&*P, *T, "", BL));

lib/AssistDS/DynCount.cpp

@@ -128,7 +128,7 @@ Dyncount::runOnModule (Module & M) {
     : M.getFunction ("MAIN__");
 
   BasicBlock & BB = MainFunc->getEntryBlock();
-  Constant * Setup = M.getOrInsertFunction ("DYN_COUNT_setup", Type::getVoidTy(M.getContext()), Total->getType(), Safe->getType(), NULL);
+  Constant * Setup = M.getOrInsertFunction ("DYN_COUNT_setup", Type::getVoidTy(M.getContext()), Total->getType(), Safe->getType());
   std::vector<Value *> args;
   args.push_back (Total);
   args.push_back (Safe);

lib/AssistDS/GEPExprArgs.cpp

@@ -118,7 +118,8 @@ bool GEPExprArgs::runOnModule(Module& M) {
           for (auto II = F->arg_begin(); NI != NewF->arg_end(); ++II, ++NI) {
             ValueMap[&*II] = &*NI;
             NI->setName(II->getName());
-            NI->addAttr(F->getAttributes().getParamAttributes(II->getArgNo() + 1));
+            auto ArgAttrs = AttrBuilder(F->getAttributes().getParamAttributes(II->getArgNo() + 1));
+            NI->addAttrs(ArgAttrs);
           }
           NewF->setAttributes(NewF->getAttributes().addAttributes(
               F->getContext(), 0, F->getAttributes().getRetAttributes()));
@@ -152,29 +153,21 @@ bool GEPExprArgs::runOnModule(Module& M) {
               fargs.at(j)->replaceAllUsesWith(GEP_new);
           }
 
-          // TODO: Should we use attrbuilder?
-          AttributeSet NewCallPAL=AttributeSet();
-
           // Get the initial attributes of the call
-          AttributeSet CallPAL = CI->getAttributes();
+          AttributeList CallPAL = CI->getAttributes();
           AttributeSet RAttrs = CallPAL.getRetAttributes();
           AttributeSet FnAttrs = CallPAL.getFnAttributes();
-          if (!RAttrs.isEmpty())
-            NewCallPAL=NewCallPAL.addAttributes(F->getContext(),0,RAttrs);
 
           SmallVector<Value*, 8> Args;
+          SmallVector<AttributeSet, 8> ArgAttrs;
           Args.push_back(GEP->getPointerOperand());
+          ArgAttrs.push_back(AttributeSet());
           for(unsigned j =1;j<CI->getNumOperands();j++) {
             Args.push_back(CI->getOperand(j));
-            // position in the AttributesBuilder
-            AttributeSet Attrs = CallPAL.getParamAttributes(j);
-            if (!Attrs.isEmpty())
-              NewCallPAL=NewCallPAL.addAttributes(F->getContext(),Args.size(),Attrs);
+            ArgAttrs.push_back(CallPAL.getParamAttributes(j));
           }
-          // Create the new attributes vec.
-          if (!FnAttrs.isEmpty())
-            NewCallPAL=NewCallPAL.addAttributes(F->getContext(),~0, FnAttrs);
 
+          auto NewCallPAL = AttributeList::get(F->getContext(), FnAttrs, RAttrs, ArgAttrs);
           CallInst *CallI = CallInst::Create(NewF,Args,"", CI);
           CallI->setCallingConv(CI->getCallingConv());
           CallI->setAttributes(NewCallPAL);