Merge branch 'release-2.3.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-6.0 main"
+  - sudo add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial-7 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-6.0 clang-format-6.0 llvm-6.0-dev mono-complete ninja-build
-  - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-6.0 20
-  - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-6.0 20
-  - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-6.0 20
-  - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-6.0 20
-  - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-6.0 20
-  - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-6.0 20
+  - sudo apt-get install -y clang-7 clang-format-7 llvm-7-dev mono-complete ninja-build
+  - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-7 20
+  - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-7 20
+  - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-7 20
+  - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-7 20
+  - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-7 20
+  - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-7 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-6.0 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
+  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-7.1 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.2.0
+PROJECT_NUMBER         = 2.3.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=6.0
-LLVM_FULL_VERSION=6.0.1
+LLVM_SHORT_VERSION=7
+LLVM_FULL_VERSION=7.1.0
 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 [6.0.1][LLVM-6.0.1]
-* [Clang][] version [6.0.1][Clang-6.0.1]
+* [LLVM][] version [7.1.0][LLVM-7.1.0]
+* [Clang][] version [7.1.0][Clang-7.1.0]
 * [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-6.0.1]: http://llvm.org/releases/download.html#6.0.1
+[LLVM-7.1.0]: http://llvm.org/releases/download.html#7.1.0
 [Clang]: http://clang.llvm.org
-[Clang-6.0.1]: http://llvm.org/releases/download.html#6.0.1
+[Clang-7.1.0]: http://llvm.org/releases/download.html#7.1.0
 [Boogie]: https://github.com/boogie-org/boogie
 [Corral]: https://github.com/boogie-org/corral
 [Z3]: https://github.com/Z3Prover/z3/

lib/AssistDS/StructReturnToPointer.cpp

@@ -114,10 +114,12 @@ bool StructRet::runOnModule(Module& M) {
           continue;
         IRBuilder<> Builder(RI);
         if (auto LI = dyn_cast<LoadInst>(RI->getOperand(0))) {
-          Builder.CreateMemCpy(fargs.at(0),
+          Builder.CreateMemCpy(
+              fargs.at(0),
+              targetData.getPrefTypeAlignment(fargs.at(0)->getType()),
               LI->getPointerOperand(),
-              targetData.getTypeStoreSize(LI->getType()),
-              targetData.getPrefTypeAlignment(LI->getType()));
+              targetData.getPrefTypeAlignment(LI->getType()),
+              targetData.getTypeStoreSize(LI->getType()));
         } else if (auto CS = dyn_cast<ConstantStruct>(RI->getReturnValue())) {
           StructType* ST = CS->getType();
           // We could store the struct into the allocated space pointed by the first

lib/smack/Regions.cpp

@@ -190,7 +190,12 @@ bool Region::overlaps(Region &R) {
 
 void Region::print(raw_ostream &O) {
   // TODO identify the representative
-  O << "<Node>[" << offset << "," << (offset + length) << "]{";
+  O << "<Node:";
+  if (type)
+    O << *type;
+  else
+    O << "*";
+  O << ">[" << offset << "," << (offset + length) << "]{";
   if (isSingleton())
     O << "S";
   if (bytewise)

lib/smack/SmackInstGenerator.cpp

@@ -868,13 +868,11 @@ void SmackInstGenerator::visitLandingPadInst(llvm::LandingPadInst &lpi) {
 
 void SmackInstGenerator::visitMemCpyInst(llvm::MemCpyInst &mci) {
   processInstruction(mci);
-  assert(mci.getNumOperands() == 6);
   emit(rep->memcpy(mci));
 }
 
 void SmackInstGenerator::visitMemSetInst(llvm::MemSetInst &msi) {
   processInstruction(msi);
-  assert(msi.getNumOperands() == 6);
   emit(rep->memset(msi));
 }
 

lib/smack/SmackRep.cpp

@@ -305,23 +305,21 @@ const Stmt *SmackRep::memcpy(const llvm::MemCpyInst &mci) {
   else
     length = std::numeric_limits<unsigned>::max();
 
-  unsigned r1 = regions->idx(mci.getOperand(0), length);
-  unsigned r2 = regions->idx(mci.getOperand(1), length);
+  unsigned r1 = regions->idx(mci.getRawDest(), length);
+  unsigned r2 = regions->idx(mci.getRawSource(), length);
 
   const Type *T = regions->get(r1).getType();
   Decl *P = memcpyProc(T ? type(T) : intType(8), length);
   auxDecls[P->getName()] = P;
 
-  const Value *dst = mci.getArgOperand(0), *src = mci.getArgOperand(1),
-              *len = mci.getArgOperand(2), *aln = mci.getArgOperand(3),
-              *vol = mci.getArgOperand(4);
+  const Value *dst = mci.getRawDest(), *src = mci.getRawSource(),
+              *len = mci.getLength();
 
   return Stmt::call(
       P->getName(),
       {Expr::id(memReg(r1)), Expr::id(memReg(r2)), expr(dst), expr(src),
        integerToPointer(expr(len), len->getType()->getIntegerBitWidth()),
-       integerToPointer(expr(aln), aln->getType()->getIntegerBitWidth()),
-       Expr::eq(expr(vol), integerLit(1ULL, 1))},
+       Expr::lit(mci.isVolatile())},
       {memReg(r1)});
 }
 
@@ -332,22 +330,20 @@ const Stmt *SmackRep::memset(const llvm::MemSetInst &msi) {
   else
     length = std::numeric_limits<unsigned>::max();
 
-  unsigned r = regions->idx(msi.getOperand(0), length);
+  unsigned r = regions->idx(msi.getRawDest(), length);
 
   const Type *T = regions->get(r).getType();
   Decl *P = memsetProc(T ? type(T) : intType(8), length);
   auxDecls[P->getName()] = P;
 
-  const Value *dst = msi.getArgOperand(0), *val = msi.getArgOperand(1),
-              *len = msi.getArgOperand(2), *aln = msi.getArgOperand(3),
-              *vol = msi.getArgOperand(4);
+  const Value *dst = msi.getRawDest(), *val = msi.getValue(),
+              *len = msi.getLength();
 
   return Stmt::call(
       P->getName(),
       {Expr::id(memReg(r)), expr(dst), expr(val),
        integerToPointer(expr(len), len->getType()->getIntegerBitWidth()),
-       integerToPointer(expr(aln), aln->getType()->getIntegerBitWidth()),
-       Expr::eq(expr(vol), integerLit(1ULL, 1))},
+       Expr::lit(msi.isVolatile())},
       {memReg(r)});
 }
 
@@ -1276,7 +1272,6 @@ Decl *SmackRep::memcpyProc(std::string type, unsigned length) {
     << "dst: ref, "
     << "src: ref, "
     << "len: ref, "
-    << "align: ref, "
     << "isvolatile: bool"
     << ") returns ("
     << "M.ret: [ref] " << type << ")";
@@ -1351,7 +1346,6 @@ Decl *SmackRep::memsetProc(std::string type, unsigned length) {
     << "dst: ref, "
     << "val: " << intType(8) << ", "
     << "len: ref, "
-    << "align: ref, "
     << "isvolatile: bool"
     << ") returns ("
     << "M.ret: [ref] " << type << ")";

share/smack/reach.py

@@ -11,7 +11,7 @@
 from smackgen import *
 from smackverify import *
 
-VERSION = '2.2.0'
+VERSION = '2.3.0'
 
 def reachParser():
     parser = argparse.ArgumentParser(add_help=False, parents=[verifyParser()])

share/smack/top.py

@@ -15,7 +15,7 @@
 from replay import replay_error_trace
 from frontend import link_bc_files, frontends, languages, extra_libs 
 
-VERSION = '2.2.0'
+VERSION = '2.3.0'
 
 def results(args):
   """A dictionary of the result output messages."""

test/simd/shuffle.c

@@ -2,6 +2,7 @@
 #include <smack.h>
 
 // @expect verified
+// @flag --clang-options=-mavx2
 
 int main() {
   __m128i A = _mm_set_epi32(13, 12, 11, 10);
@@ -10,7 +11,7 @@ int main() {
   A = _mm_shuffle_epi32(A, 2 * 1 + 3 * 4 + 2 * 16 + 3 * 64);
   B = _mm_shuffle_epi32(B, 2 * 1 + 3 * 4 + 2 * 16 + 3 * 64);
 
-  __m128i C = _mm_blend_epi32(A, B, 0xf0);
+  __m128i C = _mm_blend_epi32(A, B, 0xf);
 
   assert(_mm_extract_epi32(C, 0) != 0);
   return 0;

test/simd/shuffle_fail.c

@@ -2,6 +2,7 @@
 #include <smack.h>
 
 // @expect error
+// @flag --clang-options=-mavx2
 
 int main() {
   __m128i A = _mm_set_epi32(13, 12, 11, 10);
@@ -10,7 +11,7 @@ int main() {
   A = _mm_shuffle_epi32(A, 2 * 1 + 3 * 4 + 2 * 16 + 3 * 64);
   B = _mm_shuffle_epi32(B, 2 * 1 + 3 * 4 + 2 * 16 + 3 * 64);
 
-  __m128i C = _mm_blend_epi32(A, B, 0xf0);
+  __m128i C = _mm_blend_epi32(A, B, 0xf);
 
   assert(_mm_extract_epi32(C, 0) == 0);
   return 0;