Merge branch 'release-1.9.2'

.travis.yml

@@ -42,7 +42,8 @@ before_install:
   - sudo add-apt-repository "deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.9 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
-  - echo "deb http://download.mono-project.com/repo/ubuntu trusty main" | sudo tee /etc/apt/sources.list.d/mono-official.list
+  - sudo apt-get install -y apt-transport-https
+  - echo "deb https://download.mono-project.com/repo/ubuntu stable-trusty main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
   - sudo apt-get update
 
 install:

Doxyfile

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

Vagrantfile

@@ -10,7 +10,7 @@ Vagrant.configure(2) do |config|
   config.vm.synced_folder ".", "/home/vagrant/#{project_name}"
 
   config.vm.define :ubuntu do |ubuntu_config|
-    ubuntu_config.vm.box = "minimal/trusty64"
+    ubuntu_config.vm.box = "bento/ubuntu-16.04"
   end
 
   # This provision, 'fix-no-tty', gets rid of an error during build

bin/build.sh

@@ -181,18 +181,23 @@ puts "Detected distribution: $distro"
 # Set platform-dependent flags
 case "$distro" in
 linux-opensuse*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-debian-8.10.zip"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-debian-8.10.zip"
   DEPENDENCIES+=" llvm-clang llvm-devel gcc-c++ mono-complete make"
   DEPENDENCIES+=" ncurses-devel zlib-devel"
   ;;
 
-linux-@(ubuntu|neon)-1[46]*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-14.04.zip"
+linux-@(ubuntu|neon)-14*)
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-14.04.zip"
+  DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION} mono-complete libz-dev libedit-dev"
+  ;;
+
+linux-@(ubuntu|neon)-16*)
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-16.04.zip"
   DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION} mono-complete libz-dev libedit-dev"
   ;;
 
 linux-ubuntu-12*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-14.04.zip"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-14.04.zip"
   DEPENDENCIES+=" g++-4.8 autoconf automake bison flex libtool gettext gdb"
   DEPENDENCIES+=" libglib2.0-dev libfontconfig1-dev libfreetype6-dev libxrender-dev"
   DEPENDENCIES+=" libtiff-dev libjpeg-dev libgif-dev libpng-dev libcairo2-dev"
@@ -248,7 +253,6 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then
 
   linux-@(ubuntu|neon)-1[46]*)
     RELEASE_VERSION=$(get-platform-trim "$(lsb_release -r)" | awk -F: '{print $2;}')
-    UBUNTU_CODENAME="trusty"
     case "$RELEASE_VERSION" in
     14*)
       UBUNTU_CODENAME="trusty"
@@ -271,7 +275,8 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then
     ${WGET} -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
     # Adding MONO repository
     sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF
-    echo "deb http://download.mono-project.com/repo/ubuntu trusty main" | sudo tee /etc/apt/sources.list.d/mono-official.list
+    sudo apt-get install -y apt-transport-https
+    echo "deb https://download.mono-project.com/repo/ubuntu stable-${UBUNTU_CODENAME} main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
     sudo apt-get update
     sudo apt-get install -y ${DEPENDENCIES}
     sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_SHORT_VERSION} 30

bin/versions

@@ -1,7 +1,8 @@
 MONO_VERSION=5.0.0.100
-Z3_VERSION=4.6.0
-BOOGIE_COMMIT=c92bebd817
-CORRAL_COMMIT=179251cc9c
+Z3_SHORT_VERSION=4.8.1
+Z3_FULL_VERSION=4.8.1.016872a5e0f6
+BOOGIE_COMMIT=cd0609f660
+CORRAL_COMMIT=d7d389f22d
 SYMBOOGLIX_COMMIT=7210e5d09b
 LOCKPWN_COMMIT=73eddf97bd
 LLVM_SHORT_VERSION=3.9

include/smack/IntegerOverflowChecker.h

@@ -24,8 +24,8 @@ class IntegerOverflowChecker: public llvm::ModulePass {
   llvm::Value* extendBitWidth(llvm::Value* v, int bits, bool isSigned, llvm::Instruction* i);
   llvm::BinaryOperator* createFlag(llvm::Value* v, int bits, bool isSigned, llvm::Instruction* i);
   llvm::Value* createResult(llvm::Value* v, int bits, llvm::Instruction* i);
-  void addCheck(llvm::Function* co, llvm::BinaryOperator* flag, llvm::Instruction* i);
-  void addBlockingAssume(llvm::Function* va, llvm::BinaryOperator* flag, llvm::Instruction* i);
+  void addCheck(llvm::Function* co, llvm::Value* flag, llvm::Instruction* i);
+  void addBlockingAssume(llvm::Function* va, llvm::Value* flag, llvm::Instruction* i);
 };
 }
 

include/smack/Naming.h

@@ -91,6 +91,11 @@ class Naming {
   static const std::string MEMORY_SAFETY_FUNCTION;
   static const std::string MEMORY_LEAK_FUNCTION;
 
+  static const std::string RUST_ENTRY;
+  static const std::string RUST_PANIC1;
+  static const std::string RUST_PANIC2;
+  static const std::string RUST_PANIC_ANNOTATION;
+
   static const std::map<unsigned,std::string> INSTRUCTION_TABLE;
   static const std::map<unsigned,std::string> CMPINST_TABLE;
   static const std::map<unsigned,std::string> ATOMICRMWINST_TABLE;

lib/smack/IntegerOverflowChecker.cpp

@@ -7,6 +7,7 @@
 // operations, and optionally allows for the checking of overflow.
 //
 
+#define DEBUG_TYPE "smack-overflow"
 #include "smack/IntegerOverflowChecker.h"
 #include "smack/Naming.h"
 #include "llvm/IR/Module.h"
@@ -93,7 +94,7 @@ Value* IntegerOverflowChecker::createResult(Value* v, int bits, Instruction* i)
  * This adds a call instruction to __SMACK_check_overflow to determine if an
  * overflow occured as indicated by flag.
  */
-void IntegerOverflowChecker::addCheck(Function* co, BinaryOperator* flag, Instruction* i) {
+void IntegerOverflowChecker::addCheck(Function* co, Value* flag, Instruction* i) {
   ArrayRef<Value*> args(CastInst::CreateIntegerCast(flag, co->arg_begin()->getType(), false, "", i));
   CallInst::Create(co, args, "", i);
 }
@@ -102,7 +103,7 @@ void IntegerOverflowChecker::addCheck(Function* co, BinaryOperator* flag, Instru
  * This inserts a call to assume with flag negated to prevent the verifier
  * from exploring paths past a __SMACK_check_overflow
  */
-void IntegerOverflowChecker::addBlockingAssume(Function* va, BinaryOperator* flag, Instruction* i) {
+void IntegerOverflowChecker::addBlockingAssume(Function* va, Value* flag, Instruction* i) {
   ArrayRef<Value*> args(CastInst::CreateIntegerCast(BinaryOperator::CreateNot(flag, "", i),
         va->arg_begin()->getType(), false, "", i));
   CallInst::Create(va, args, "", i);
@@ -118,12 +119,28 @@ bool IntegerOverflowChecker::runOnModule(Module& m) {
     if (Naming::isSmackName(F.getName()))
       continue;
     for (inst_iterator I = inst_begin(F), E = inst_end(F); I != E; ++I) {
+      // Add check for UBSan left shift when needed
+      if (SmackOptions::IntegerOverflow) {
+        if (auto chkshft = dyn_cast<CallInst>(&*I)) {
+	  Function* chkfn = chkshft->getCalledFunction();
+          if (chkfn && chkfn->hasName() &&
+              chkfn->getName().find("__ubsan_handle_shift_out_of_bounds") != std::string::npos) {
+            // If the call to __ubsan_handle_shift_out_of_bounds is reachable,
+            // then an overflow is possible.
+            ConstantInt* flag = ConstantInt::getTrue(chkshft->getFunction()->getContext());
+            addCheck(co, flag, &*I);
+            addBlockingAssume(va, flag, &*I);
+            I->replaceAllUsesWith(flag);
+            instToRemove.push_back(&*I);
+          }
+        }
+      }
       if (auto ei = dyn_cast<ExtractValueInst>(&*I)) {
         if (auto ci = dyn_cast<CallInst>(ei->getAggregateOperand())) {
           Function* f = ci->getCalledFunction();
-          SmallVectorImpl<StringRef> *info = new SmallVector<StringRef, 3>;
-          if (f && f->hasName() && OVERFLOW_INTRINSICS.match(f->getName().str(), info)
-              && ei->getIndices()[0] == 1) {
+          SmallVector<StringRef, 4> info;
+          if (f && f->hasName() && OVERFLOW_INTRINSICS.match(f->getName(), &info) &&
+              ei->getIndices()[0] == 1) {
             /*
              * If ei is an ExtractValueInst whose value flows from an LLVM
              * checked value intrinsic f, then we do the following:
@@ -137,13 +154,16 @@ bool IntegerOverflowChecker::runOnModule(Module& m) {
              * - Finally, an assumption about the value of the flag is created
              *   to block erroneous checking of paths after the overflow check.
              */
+            DEBUG(errs() << "Processing intrinsic: " << f->getName().str() << "\n");
+            assert(info.size() == 4 && "Must capture three matched strings.");
+            bool isSigned = (info[1] == "s");
+            std::string op = info[2];
+            int bits = std::stoi(info[3]);
             Instruction* prev = &*std::prev(I);
-            bool isSigned = info->begin()[1].str() == "s";
-            std::string op = info->begin()[2].str();
-            std::string len = info->begin()[3].str();
-            int bits = std::stoi(len);
             Value* eo1 = extendBitWidth(ci->getArgOperand(0), bits, isSigned, &*I);
             Value* eo2 = extendBitWidth(ci->getArgOperand(1), bits, isSigned, &*I);
+            DEBUG(errs() << "Processing operator: " << op << "\n");
+            assert(INSTRUCTION_TABLE.count(op) != 0 && "Operator must be present in our instruction table.");
             BinaryOperator* ai = BinaryOperator::Create(INSTRUCTION_TABLE.at(op), eo1, eo2, "", &*I);
             if (auto pei = dyn_cast_or_null<ExtractValueInst>(prev)) {
               if (ci == dyn_cast<CallInst>(pei->getAggregateOperand())) {

lib/smack/Naming.cpp

@@ -61,6 +61,11 @@ const std::string Naming::MEM_OP = "$mop";
 const std::string Naming::REC_MEM_OP = "boogie_si_record_mop";
 const std::string Naming::MEM_OP_VAL = "$MOP";
 
+const std::string Naming::RUST_ENTRY = "_ZN3std2rt10lang_start";
+const std::string Naming::RUST_PANIC1 = "_ZN4core9panicking5panic";
+const std::string Naming::RUST_PANIC2 = "_ZN3std9panicking11begin_panic";
+const std::string Naming::RUST_PANIC_ANNOTATION = "rust_panic";
+
 const std::string Naming::BLOCK_LBL = "$bb";
 const std::string Naming::RET_VAR = "$r";
 const std::string Naming::EXN_VAR = "$exn";

lib/smack/SmackInstGenerator.cpp

@@ -477,8 +477,7 @@ void SmackInstGenerator::visitStoreInst(llvm::StoreInst& si) {
   if (SmackOptions::SourceLocSymbols) {
     if (const llvm::GlobalVariable* G = llvm::dyn_cast<const llvm::GlobalVariable>(P)) {
       if (const llvm::PointerType* t = llvm::dyn_cast<const llvm::PointerType>(G->getType())) {
-        if (!t->getElementType()->isPointerTy()) {
-          assert(G->hasName() && "Expected named global variable.");
+        if (!t->getElementType()->isPointerTy() && G->hasName()) {
           emit(recordProcedureCall(V, {Attr::attr("cexpr", G->getName().str())}));
         }
       }
@@ -600,7 +599,20 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) {
     // Semantically, this function simply returns the value v.
     Value* val = ci.getArgOperand(0);
     emit(Stmt::assign(rep->expr(&ci), rep->expr(val)));
-
+
+  } else if (name.find(Naming::RUST_ENTRY) != std::string::npos) {
+    // Set the entry point for Rust programs
+    auto castExpr = ci.getArgOperand(0);
+    if (auto CE = dyn_cast<const Constant>(castExpr)) {
+      auto mainFunc = CE->getOperand(0);
+      emit(Stmt::call(mainFunc->getName(), {},{}));
+    }
+
+  } else if (name.find(Naming::RUST_PANIC1) != std::string::npos
+             || name.find(Naming::RUST_PANIC2) != std::string::npos) {
+    // Convert Rust's panic functions into assertion violations
+    emit(Stmt::assert_(Expr::lit(false), {Attr::attr(Naming::RUST_PANIC_ANNOTATION)}));
+
   } else if (name.find(Naming::VALUE_PROC) != std::string::npos) {
     emit(rep->valueAnnotation(ci));
 

lib/smack/SmackRep.cpp

@@ -1080,7 +1080,7 @@ std::string SmackRep::getPrelude() {
     s << "// Global allocations" << "\n";
     std::list<const Stmt*> stmts;
     for (auto E : globalAllocations)
-      stmts.push_back(Stmt::call("$galloc", {expr(E.first), Expr::lit(E.second)}));
+      stmts.push_back(Stmt::call("$galloc", {expr(E.first), pointerLit(E.second)}));
     s << Decl::procedure("$global_allocations", {}, {}, {}, {Block::block("",stmts)}) << "\n";
     s << "\n";
   }

share/smack/frontend.py

@@ -61,10 +61,6 @@ def smack_header_path():
 def smack_headers(args):
   paths = []
   paths.append(smack_header_path())
-  if args.memory_safety or args.integer_overflow:
-    paths.append(os.path.join(smack_header_path(), 'string'))
-  if args.float:
-    paths.append(os.path.join(smack_header_path(), 'math'))
   return paths
 
 def smack_lib():
@@ -76,7 +72,7 @@ def default_clang_compile_command(args, lib = False):
   cmd += args.clang_options.split()
   cmd += ['-DMEMORY_MODEL_' + args.mem_mod.upper().replace('-','_')]
   if args.memory_safety: cmd += ['-DMEMORY_SAFETY']
-  if args.integer_overflow: cmd += (['-ftrapv'] if not lib else ['-DSIGNED_INTEGER_OVERFLOW_CHECK'])
+  if args.integer_overflow: cmd += (['-ftrapv', '-fsanitize=shift'] if not lib else ['-DSIGNED_INTEGER_OVERFLOW_CHECK'])
   if args.float: cmd += ['-DFLOAT_ENABLED']
   if sys.stdout.isatty(): cmd += ['-fcolor-diagnostics']
   return cmd
@@ -87,6 +83,12 @@ def compile_to_bc(input_file, compile_command, args):
   try_command(compile_command + ['-o', bc, input_file], console=True)
   return bc
 
+def d_compile_to_bc(input_file, compile_command, args):
+  """Compile a D source file to LLVM IR."""
+  bc = temporary_file(os.path.splitext(os.path.basename(input_file))[0], '.bc', args)
+  try_command(compile_command + ['-of=' + bc, input_file], console=True)
+  return bc
+
 def fortran_compile_to_bc(input_file, compile_command, args):
   """Compile a FORTRAN source file to LLVM IR."""
 
@@ -152,7 +154,7 @@ def d_frontend(input_file, args):
   compile_command = ['ldc2', '-output-ll']
   compile_command += map(lambda path: '-I=' + path, smack_headers(args))
   args.entry_points += ['_Dmain']
-  return compile_to_bc(input_file,compile_command,args)
+  return d_compile_to_bc(input_file,compile_command,args)
 
 def fortran_frontend(input_file, args):
   """Generate Boogie code from Fortran language source(s)."""
@@ -237,7 +239,7 @@ def rust_frontend(input_file, args):
 def default_build_libs(args):
   """Generate LLVM bitcodes for SMACK libraries."""
   bitcodes = []
-  libs = ['smack.c']
+  libs = ['smack.c', 'stdlib.c']
 
   if args.pthread:
     libs += ['pthread.c']

share/smack/include/smack.h

@@ -54,7 +54,6 @@ void __VERIFIER_assume(int);
 void __VERIFIER_assert(int);
 #endif
 void __VERIFIER_error(void);
-void exit(int);
 
 #ifndef AVOID_NAME_CONFLICTS
 #define assert(EX) __VERIFIER_assert(EX)

share/smack/lib/fenv.c

@@ -10,7 +10,7 @@ int fegetround(void) {
   const int CONST_FE_UPWARD = FE_UPWARD;
   const int CONST_FE_TOWARDZERO = FE_TOWARDZERO;
   int ret = __VERIFIER_nondet_int();
-  assume(ret < 0);
+  __VERIFIER_assume(ret < 0);
   __SMACK_code("if ($rmode == RNE) {@ := @;}", ret, CONST_FE_TONEAREST);
   __SMACK_code("if ($rmode == RTN) {@ := @;}", ret, CONST_FE_DOWNWARD);
   __SMACK_code("if ($rmode == RTP) {@ := @;}", ret, CONST_FE_UPWARD);

share/smack/lib/smack.c

@@ -46,6 +46,9 @@ void __VERIFIER_assert(int x) {
 void __VERIFIER_error(void) {
 #if !MEMORY_SAFETY && !SIGNED_INTEGER_OVERFLOW_CHECK
   __SMACK_code("assert false;");
+#elif MEMORY_SAFETY
+  __SMACK_code("assert {:valid_memtrack} $allocatedCounter == 0;");
+  __SMACK_code("assume false;");
 #else
   __SMACK_code("assume false;");
 #endif
@@ -55,14 +58,6 @@ void __SMACK_check_overflow(int flag) {
   __SMACK_dummy(flag); __SMACK_code("assert {:overflow} @ == $0;", flag);
 }
 
-void exit(int x) {
-#if MEMORY_SAFETY
-  __SMACK_code("assert $allocatedCounter == 0;");
-#endif
-  __SMACK_code("assume false;");
-  while(1);
-}
-
 char __VERIFIER_nondet_char(void) {
   char x = __SMACK_nondet_char();
   __VERIFIER_assume(x >= SCHAR_MIN && x <= SCHAR_MAX);
@@ -257,17 +252,6 @@ void* __VERIFIER_nondet_pointer(void) {
   return __VERIFIER_nondet();
 }
 
-void* calloc(size_t num, size_t size) {
-  void* ret;
-  if (__VERIFIER_nondet_int()) {
-    ret = 0;
-  } else {
-    ret = malloc(num * size);
-    memset(ret, 0, num * size);
-  }
-  return ret;
-}
-
 void __SMACK_dummy(int v) {
   __SMACK_code("assume true;");
 }