Merge branch 'release-2.6.3'

.github/workflows/smack-ci.yaml

@@ -0,0 +1,66 @@
+name: SMACK CI
+
+on: [push, pull_request]
+
+jobs:
+  check-regressions:
+    env:
+      COMPILER_NAME: clang
+      COMPILER: clang++
+      CXX: clang++
+      CC: clang
+    runs-on: ubuntu-20.04
+    strategy:
+      matrix:
+        travis_env:
+          [
+            "--exhaustive --folder=c/basic",
+            "--exhaustive --folder=c/data",
+            "--exhaustive --folder=c/ntdrivers-simplified",
+            "--exhaustive --folder=c/ntdrivers",
+            "--exhaustive --folder=c/bits",
+            "--exhaustive --folder=c/float",
+            "--exhaustive --folder=c/locks",
+            "--exhaustive --folder=c/contracts",
+            "--exhaustive --folder=c/simd",
+            "--exhaustive --folder=c/memory-safety",
+            "--exhaustive --folder=c/pthread",
+            "--exhaustive --folder=c/pthread_extras",
+            "--exhaustive --folder=c/strings",
+            "--exhaustive --folder=c/special",
+            "--exhaustive --folder=rust/array --languages=rust",
+            "--exhaustive --folder=rust/basic --languages=rust",
+            "--exhaustive --folder=rust/box --languages=rust",
+            "--exhaustive --folder=rust/functions --languages=rust",
+            "--exhaustive --folder=rust/generics --languages=rust",
+            "--exhaustive --folder=rust/loops --languages=rust",
+            "--exhaustive --folder=rust/panic --languages=rust",
+            "--exhaustive --folder=rust/recursion --languages=rust",
+            "--exhaustive --folder=rust/structures --languages=rust",
+            "--exhaustive --folder=rust/vector --languages=rust"
+          ]
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: install dependencies
+        env:
+          GITHUB_ACTIONS: true
+        run: INSTALL_DEV_DEPENDENCIES=1 INSTALL_RUST=1 ./bin/build.sh
+
+      - run: python3 --version
+      - run: $CXX --version
+      - run: $CC --version
+      - run: clang --version
+      - run: clang++ --version
+      - run: llvm-link --version
+      - run: llvm-config --version
+
+      - name: format checking
+        run: |
+          ./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
+      
+      - name: compile and test
+        env:
+          TRAVIS_ENV: ${{ matrix.travis_env }}
+        run: ./bin/build.sh

CMakeLists.txt

@@ -7,7 +7,7 @@ project(smack)
 
 if (NOT WIN32 OR MSYS OR CYGWIN)
 
-  file(STRINGS "bin/versions" LLVM_VERSION_STR REGEX "LLVM_SHORT_VERSION=[0-9]+")
+  file(STRINGS "bin/versions" LLVM_VERSION_STR REGEX "LLVM_SHORT_VERSION=\"[0-9]+\"")
   string(REGEX MATCH "[0-9]+" LLVM_SHORT_VERSION "${LLVM_VERSION_STR}")
 
   find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-${LLVM_SHORT_VERSION} llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")

Doxyfile

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

README.md

@@ -1,6 +1,5 @@
-
-[![Build Status](https://travis-ci.com/smackers/smack.svg?branch=master)](https://travis-ci.com/smackers/smack)
-[![Build Status](https://travis-ci.com/smackers/smack.svg?branch=develop)](https://travis-ci.com/smackers/smack)
+[![master branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=master)](https://github.com/smackers/smack/actions)
+[![develop branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=develop)](https://github.com/smackers/smack/actions)
 
 <img src="docs/smack-logo.png" width=400 alt="SMACK Logo" align="right">
 

bin/build.sh

@@ -39,6 +39,9 @@ BUILD_LLVM=0 # LLVM is typically installed from packages (see below)
 INSTALL_OBJECTIVEC=0
 INSTALL_RUST=${INSTALL_RUST:-0}
 
+# Development dependencies
+INSTALL_DEV_DEPENDENCIES=${INSTALL_DEV_DEPENDENCIES:-0}
+
 # PATHS
 SMACK_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && cd .. && pwd )"
 ROOT_DIR="$( cd "${SMACK_DIR}" && cd .. && pwd )"
@@ -459,6 +462,16 @@ if [ ${BUILD_LOCKPWN} -eq 1 ] ; then
 fi
 
 
+if [ ${INSTALL_DEV_DEPENDENCIES} -eq 1 ] ; then
+  sudo apt-get install -y python3-pip clang-format-${LLVM_SHORT_VERSION}
+  sudo pip3 install -U flake8
+  sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-${LLVM_SHORT_VERSION} 30
+  if [ "${GITHUB_ACTIONS}" = "true" ] ; then
+    exit 0
+  fi
+fi
+
+
 if [ ${BUILD_SMACK} -eq 1 ] ; then
   puts "Building SMACK"
 

docs/people.md

@@ -11,7 +11,7 @@
 
 * [Marek Baranowski](https://github.com/keram88) ([SOAR Lab](http://soarlab.org), University of Utah)
 * [Jack J. Garzella](https://www.linkedin.com/in/jack-j-garzella-7140a716) ([SOAR Lab](http://soarlab.org), University of Utah)
-* [Shaobo He](http://www.cs.utah.edu/~shaobo) ([SOAR Lab](http://soarlab.org), University of Utah)
+* [Shaobo He](http://www.cs.utah.edu/~shaobo) (Baidu USA)
 * [Liam Machado](https://github.com/liammachado) ([SOAR Lab](http://soarlab.org), University of Utah)
 
 ### Former Contributors

include/smack/MemorySafetyChecker.h

@@ -17,6 +17,7 @@ class MemorySafetyChecker : public llvm::FunctionPass,
   llvm::Function *getLeakCheckFunction(llvm::Module &M);
   llvm::Function *getSafetyCheckFunction(llvm::Module &M);
 
+  void copyDbgMetadata(llvm::Instruction *src, llvm::Instruction *dst);
   void insertMemoryLeakCheck(llvm::Instruction *I);
   void insertMemoryAccessCheck(llvm::Value *addr, llvm::Value *size,
                                llvm::Instruction *I);

include/smack/SmackInstGenerator.h

@@ -91,6 +91,7 @@ class SmackInstGenerator : public llvm::InstVisitor<SmackInstGenerator> {
   void visitPHINode(llvm::PHINode &i);
   void visitSelectInst(llvm::SelectInst &i);
   void visitCallInst(llvm::CallInst &i);
+  void visitCallBrInst(llvm::CallBrInst &i);
   void visitDbgValueInst(llvm::DbgValueInst &i);
   // TODO implement va_arg
   void visitLandingPadInst(llvm::LandingPadInst &i);

lib/smack/BoogieAst.cpp

@@ -555,7 +555,7 @@ void CallStmt::print(std::ostream &os) const {
   os << ";";
 }
 
-void Comment::print(std::ostream &os) const { os << "// " << str; }
+void Comment::print(std::ostream &os) const { os << "/* " << str << " */"; }
 
 void GotoStmt::print(std::ostream &os) const {
   os << "goto ";

lib/smack/CodifyStaticInits.cpp

@@ -39,18 +39,9 @@ bool CodifyStaticInits::runOnModule(Module &M) {
   std::deque<std::tuple<Constant *, Constant *, std::vector<Value *>>> worklist;
 
   for (auto &G : M.globals())
-    if (G.hasInitializer())
-
-      // HACK: Normally only isRead should be necessary here. However, there
-      // seems to be a bug in the DSA code which fails to mark some globals that
-      // are read as read. Currently this has only been observed with globals
-      // that have named addresses, e.g., excluding string constants. Thus the
-      // second predicate here is a messy hack that has little to do with the
-      // intended property of being read.
-      if (DSA->isRead(&G) || !G.hasGlobalUnnamedAddr())
-
-        worklist.push_back(
-            std::make_tuple(G.getInitializer(), &G, std::vector<Value *>()));
+    if (G.hasInitializer() && DSA->isRead(&G))
+      worklist.push_back(
+          std::make_tuple(G.getInitializer(), &G, std::vector<Value *>()));
 
   while (worklist.size()) {
     Constant *V = std::get<0>(worklist.front());

lib/smack/MemorySafetyChecker.cpp

@@ -30,20 +30,28 @@ Function *MemorySafetyChecker::getSafetyCheckFunction(Module &M) {
   return F;
 }
 
+void MemorySafetyChecker::copyDbgMetadata(Instruction *src, Instruction *dst) {
+  dst->setMetadata("dbg", src->getMetadata("dbg"));
+}
+
 void MemorySafetyChecker::insertMemoryLeakCheck(Instruction *I) {
   auto &M = *I->getParent()->getParent()->getParent();
-  CallInst::Create(getLeakCheckFunction(M), "", I);
+  auto ci = CallInst::Create(getLeakCheckFunction(M), "", I);
+  copyDbgMetadata(I, ci);
 }
 
 void MemorySafetyChecker::insertMemoryAccessCheck(Value *addr, Value *size,
                                                   Instruction *I) {
   auto &M = *I->getParent()->getParent()->getParent();
   auto &C = M.getContext();
   auto T = PointerType::getUnqual(Type::getInt8Ty(C));
-  CallInst::Create(getSafetyCheckFunction(M),
-                   {CastInst::Create(Instruction::BitCast, addr, T, "", I),
-                    CastInst::CreateBitOrPointerCast(size, T, "", I)},
-                   "", I);
+  auto ptrArg = CastInst::Create(Instruction::BitCast, addr, T, "", I);
+  auto sizeArg = CastInst::CreateBitOrPointerCast(size, T, "", I);
+  auto ci =
+      CallInst::Create(getSafetyCheckFunction(M), {ptrArg, sizeArg}, "", I);
+  copyDbgMetadata(I, ptrArg);
+  copyDbgMetadata(I, sizeArg);
+  copyDbgMetadata(I, ci);
 }
 
 bool MemorySafetyChecker::runOnFunction(Function &F) {

lib/smack/SmackInstGenerator.cpp

@@ -823,6 +823,13 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) {
   }
 }
 
+void SmackInstGenerator::visitCallBrInst(llvm::CallBrInst &cbi) {
+  processInstruction(cbi);
+  SmackWarnings::warnUnsound("callbr instruction " + i2s(cbi), currBlock, &cbi,
+                             cbi.getType()->isVoidTy());
+  emit(Stmt::skip());
+}
+
 bool isSourceLoc(const Stmt *stmt) {
   return (stmt->getKind() == Stmt::ASSUME &&
           (llvm::cast<const AssumeStmt>(stmt))->hasAttr("sourceloc")) ||

lib/smack/SmackRep.cpp

@@ -1305,7 +1305,9 @@ std::list<Decl *> SmackRep::globalDecl(const llvm::GlobalValue *v) {
     decls.push_back(Decl::axiom(Expr::eq(
         Expr::id(name), pointerLit(globalsOffset -= (size + globalsPadding)))));
   }
-  globalAllocations[v] = size;
+
+  if (!llvm::isa<Function>(v))
+    globalAllocations[v] = size;
 
   return decls;
 }

share/smack/lib/smack-rust.c

@@ -29,7 +29,7 @@
     return ret;                                                                \
   }
 
-#define mk_dummy_nondet_def(size)                                              \
+#define mk_dummy_int_nondet_def(size)                                          \
   mk_signed_type(size) __VERIFIER_nondet_i##size(void) {                       \
     return *((mk_signed_type(size) *)malloc(sizeof(mk_signed_type(size))));    \
   }                                                                            \
@@ -38,9 +38,14 @@
         (mk_unsigned_type(size) *)malloc(sizeof(mk_unsigned_type(size))));     \
   }
 
+#define mk_dummy_fp_nondet_def(ty)                                             \
+  ty __VERIFIER_nondet_##ty(void) { return *((ty *)malloc(sizeof(ty))); }
+
 #if CARGO_BUILD
-mk_dummy_nondet_def(8) mk_dummy_nondet_def(16) mk_dummy_nondet_def(32)
-    mk_dummy_nondet_def(64) void __VERIFIER_assert(int x) {}
+mk_dummy_int_nondet_def(8) mk_dummy_int_nondet_def(16)
+    mk_dummy_int_nondet_def(32) mk_dummy_int_nondet_def(64)
+        mk_dummy_fp_nondet_def(float)
+            mk_dummy_fp_nondet_def(double) void __VERIFIER_assert(int x) {}
 void __VERIFIER_assume(int x) {}
 #else
 mk_smack_nondet_decl(8) mk_smack_nondet_decl(16) mk_smack_nondet_decl(32)

share/smack/lib/smack.c

@@ -1742,14 +1742,15 @@ void __SMACK_decls(void) {
 
   D("procedure $free(p: ref);\n"
     "modifies $Alloc, $allocatedCounter;\n"
-    "requires $eq.ref.bool(p, $0.ref) || ($eq.ref.bool($base(p), p) && "
-    "$Alloc[p]);\n"
-    "requires $slt.ref.bool($0.ref, p);\n"
+    "requires $eq.ref.bool(p, $0.ref) || ($slt.ref.bool($0.ref, p) && "
+    "$eq.ref.bool($base(p), p) && $Alloc[p]);\n"
     "ensures $ne.ref.bool(p, $0.ref) ==> !$Alloc[p];\n"
     "ensures $ne.ref.bool(p, $0.ref) ==> (forall q: ref :: {$Alloc[q]} q != p "
     "==> $Alloc[q] == old($Alloc[q]));\n"
     "ensures $ne.ref.bool(p, $0.ref) ==> $allocatedCounter == "
-    "old($allocatedCounter) - 1;\n");
+    "old($allocatedCounter) - 1;\n"
+    "ensures $eq.ref.bool(p, $0.ref) ==> $allocatedCounter == "
+    "old($allocatedCounter);\n");
 
 #else // NO_REUSE does not reuse previously-allocated addresses
   D("var $Alloc: [ref] bool;");
@@ -1788,14 +1789,15 @@ void __SMACK_decls(void) {
 
   D("procedure $free(p: ref);\n"
     "modifies $Alloc, $allocatedCounter;\n"
-    "requires $eq.ref.bool(p, $0.ref) || ($eq.ref.bool($base(p), p) && "
-    "$Alloc[p]);\n"
-    "requires $slt.ref.bool($0.ref, p);\n"
+    "requires $eq.ref.bool(p, $0.ref) || ($slt.ref.bool($0.ref, p) && "
+    "$eq.ref.bool($base(p), p) && $Alloc[p]);\n"
     "ensures $ne.ref.bool(p, $0.ref) ==> !$Alloc[p];\n"
     "ensures $ne.ref.bool(p, $0.ref) ==> (forall q: ref :: {$Alloc[q]} q != p "
     "==> $Alloc[q] == old($Alloc[q]));\n"
     "ensures $ne.ref.bool(p, $0.ref) ==> $allocatedCounter == "
-    "old($allocatedCounter) - 1;\n");
+    "old($allocatedCounter) - 1;\n"
+    "ensures $eq.ref.bool(p, $0.ref) ==> $allocatedCounter == "
+    "old($allocatedCounter);\n");
 #endif
 
 #else

share/smack/lib/smack.rs

@@ -12,6 +12,8 @@ extern "C" {
     pub fn __VERIFIER_nondet_u32() -> u32;
     pub fn __VERIFIER_nondet_i64() -> i64;
     pub fn __VERIFIER_nondet_u64() -> u64;
+    pub fn __VERIFIER_nondet_float() -> f32;
+    pub fn __VERIFIER_nondet_double() -> f64;
     pub fn malloc(size: usize) -> *mut u8;
     pub fn __VERIFIER_memcpy(dest: *mut u8, src: *mut u8, count: usize) -> *mut u8;
     pub fn free(ptr: *mut u8);
@@ -139,6 +141,8 @@ make_verifier_nondet!(i64, __VERIFIER_nondet_i64);
 make_verifier_nondet!(u64, __VERIFIER_nondet_u64);
 make_verifier_nondet!(isize, __VERIFIER_nondet_i64);
 make_verifier_nondet!(usize, __VERIFIER_nondet_u64);
+make_verifier_nondet!(f32, __VERIFIER_nondet_float);
+make_verifier_nondet!(f64, __VERIFIER_nondet_double);
 
 #[cfg(not(verifier = "smack"))]
 #[cfg(feature = "std")]