Merge branch 'release-1.7.1'

Author: zvonimir

CMakeLists.txt

@@ -159,6 +159,7 @@ add_library(smackTranslator STATIC
   include/smack/SmackRep.h
   include/smack/SmackRepFlatMem.h
   include/smack/MemorySafetyChecker.h
+  include/smack/SignedIntegerOverflowChecker.h
   lib/smack/BoogieAst.cpp
   lib/smack/BplFilePrinter.cpp
   lib/smack/BplPrinter.cpp
@@ -175,6 +176,7 @@ add_library(smackTranslator STATIC
   lib/smack/SmackRep.cpp
   lib/smack/SmackRepFlatMem.cpp
   lib/smack/MemorySafetyChecker.cpp
+  lib/smack/SignedIntegerOverflowChecker.cpp
 )
 
 add_executable(llvm2bpl

Doxyfile

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

bin/build.sh

@@ -24,7 +24,7 @@ INSTALL_DEPENDENCIES=1
 BUILD_Z3=1
 BUILD_BOOGIE=1
 BUILD_CORRAL=1
-BUILD_LOCKPWN=0
+BUILD_LOCKPWN=1
 BUILD_SMACK=1
 TEST_SMACK=1
 BUILD_LLVM=0 # LLVM is typically installed from packages (see below)
@@ -369,6 +369,7 @@ then
   cd ${ROOT}
   git clone https://github.com/smackers/lockpwn.git
   cd ${LOCKPWN_DIR}
+  git reset --hard ${LOCKPWN_COMMIT}
   xbuild lockpwn.sln /p:Configuration=Release
   ln -s ${Z3_DIR}/bin/z3 ${LOCKPWN_DIR}/Binaries/z3.exe
 

bin/package-smack.sh

@@ -6,7 +6,7 @@
 # Note: this script requires CDE to be downloaded from
 # http://www.pgbovine.net/cde.html
 
-VERSION=1.7.0
+VERSION=1.7.1
 PACKAGE=smack-$VERSION-64
 
 # Create folder to export

bin/smack-svcomp-wrapper.sh

@@ -4,16 +4,20 @@
 
 ROOT="$( cd "$(dirname "$(readlink -f "${0}")")" && pwd )"
 SMACK_BIN="${ROOT}/smack/bin"
+BOOGIE_BIN="${ROOT}/boogie"
 CORRAL_BIN="${ROOT}/corral"
 LOCKPWN_BIN="${ROOT}/lockpwn"
 LLVM_BIN="${ROOT}/llvm/bin"
+LLVM_LIB="${ROOT}/llvm/lib"
 
-# Setting mono heap size to 9GB
-export MONO_GC_PARAMS=max-heap-size=9g
+# Setting mono heap size to 13GB
+export MONO_GC_PARAMS=max-heap-size=13g
 
 export PATH=${LLVM_BIN}:$SMACK_BIN:$PATH
+export BOOGIE="mono ${BOOGIE_BIN}/Boogie.exe"
 export CORRAL="mono ${CORRAL_BIN}/corral.exe"
 export LOCKPWN="mono ${LOCKPWN_BIN}/lockpwn.exe"
+export LD_LIBRARY_PATH=${LLVM_LIB}:$LD_LIBRARY_PATH
 
 smack -x=svcomp --verifier=svcomp -q $@
 

bin/versions

@@ -1,3 +1,4 @@
 MONO_VERSION=3.8.0
 BOOGIE_COMMIT=4e4c3a5252
 CORRAL_COMMIT=874a078e39
+LOCKPWN_COMMIT=a4d802a1cb

include/smack/BoogieAst.h

@@ -194,6 +194,7 @@ class Attr {
 public:
   Attr(std::string n, std::initializer_list<const Expr*> vs) : name(n), vals(vs) {}
   void print(std::ostream& os) const;
+  std::string getName() const { return name; }
 
   static const Attr* attr(std::string s);
   static const Attr* attr(std::string s, std::string v);
@@ -268,6 +269,13 @@ class AssumeStmt : public Stmt {
   void add(const Attr* a) {
     attrs.push_back(a);
   }
+  bool hasAttr(std::string name) const {
+    for (auto a = attrs.begin(); a != attrs.end(); ++a) {
+      if ((*a)->getName() == name)
+        return true;
+    }
+    return false;
+  }
   void print(std::ostream& os) const;
   static bool classof(const Stmt* S) { return S->getKind() == ASSUME; }
 };

include/smack/SignedIntegerOverflowChecker.h

@@ -0,0 +1,27 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+#ifndef SIGNEDINTEGEROVERFLOWCHECKER_H
+#define SIGNEDINTEGEROVERFLOWCHECKER_H
+
+#include "llvm/Pass.h"
+#include "llvm/IR/Module.h"
+#include <map>
+
+namespace smack {
+  
+class SignedIntegerOverflowChecker: public llvm::ModulePass {
+public:
+  static char ID; // Pass identification, replacement for typeid
+  SignedIntegerOverflowChecker() : llvm::ModulePass(ID) {}
+  virtual bool runOnModule(llvm::Module& m);
+private:
+  static std::map<std::string, llvm::Instruction::BinaryOps> INSTRUCTION_TABLE;
+  static std::map<int, std::string> INT_MAX_TABLE;
+  static std::map<int, std::string> INT_MIN_TABLE;
+  void replaceValue(llvm::Value* ee, llvm::Value* er);
+};
+
+}
+
+#endif //SIGNEDINTEGEROVERFLOWCHECKER_H

include/smack/SmackInstGenerator.h

@@ -23,6 +23,7 @@ class SmackInstGenerator : public llvm::InstVisitor<SmackInstGenerator> {
   Naming& naming;
 
   Block* currBlock;
+  llvm::BasicBlock::const_iterator nextInst;
   std::map<const llvm::BasicBlock*, Block*> blockMap;
   std::map<const llvm::Value*, std::string> sourceNames;
 

include/smack/SmackRep.h

@@ -68,7 +68,7 @@ class SmackRep {
 
   const Expr* cast(unsigned opcode, const llvm::Value* v, const llvm::Type* t);
   const Expr* bop(unsigned opcode, const llvm::Value* lhs, const llvm::Value* rhs, const llvm::Type* t);
-  const Expr* cmp(unsigned predicate, const llvm::Value* lhs, const llvm::Value* rhs);
+  const Expr* cmp(unsigned predicate, const llvm::Value* lhs, const llvm::Value* rhs, bool isUnsigned);
 
   std::string procName(const llvm::User& U);
   std::string procName(llvm::Function* F, const llvm::User& U);
@@ -99,14 +99,14 @@ class SmackRep {
   std::string type(const llvm::Type* t);
   std::string type(const llvm::Value* v);
 
-  const Expr* lit(const llvm::Value* v);
+  const Expr* lit(const llvm::Value* v, bool isUnsigned=false);
   const Expr* lit(const llvm::Value* v, unsigned flag);
 
   const Expr* ptrArith(const llvm::GetElementPtrInst* I);
   const Expr* ptrArith(const llvm::ConstantExpr* CE);
   const Expr* ptrArith(const llvm::Value* p, std::vector< std::pair<llvm::Value*,llvm::Type*> > args);
 
-  const Expr* expr(const llvm::Value* v);
+  const Expr* expr(const llvm::Value* v, bool isConstIntUnsigned=false);
 
   const Expr* cast(const llvm::Instruction* I);
   const Expr* cast(const llvm::ConstantExpr* CE);