From c0b9db0050f22ce0955fdee7703f63f6d2c79433 Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Tue, 13 Nov 2018 16:40:53 -0800 Subject: [PATCH 1/8] Pass separate alignments to `CreateMemCpy` This reflects the changes made [here](https://reviews.llvm.org/rL322965). I'm not 100% sure that this is always correct, as I believe both alignments must be the same? --- lib/AssistDS/StructReturnToPointer.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/lib/AssistDS/StructReturnToPointer.cpp b/lib/AssistDS/StructReturnToPointer.cpp index 365aef0ef..17e1579ee 100644 --- a/lib/AssistDS/StructReturnToPointer.cpp +++ b/lib/AssistDS/StructReturnToPointer.cpp @@ -114,10 +114,12 @@ bool StructRet::runOnModule(Module& M) { continue; IRBuilder<> Builder(RI); if (auto LI = dyn_cast(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(RI->getReturnValue())) { StructType* ST = CS->getType(); // We could store the struct into the allocated space pointed by the first From d410a117264dfa515813a8af8272b746a6a40ad1 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Mon, 29 Jul 2019 08:59:08 -0600 Subject: [PATCH 2/8] Updated LLVM version to 7.1.0 --- .travis.yml | 16 ++++++++-------- CMakeLists.txt | 2 +- bin/versions | 4 ++-- docs/installation.md | 8 ++++---- 4 files changed, 15 insertions(+), 15 deletions(-) diff --git a/.travis.yml b/.travis.yml index 9f3ddbee0..f0f84add6 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,7 +39,7 @@ 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.1 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 @@ -47,13 +47,13 @@ before_install: - 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.1 clang-format-7.1 llvm-7.1-dev mono-complete ninja-build + - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-7.1 20 + - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-7.1 20 + - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-7.1 20 + - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-7.1 20 + - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-7.1 20 + - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-7.1 20 - sudo pip install pyyaml psutil script: diff --git a/CMakeLists.txt b/CMakeLists.txt index 348cf391d..f416e8a51 100644 --- a/CMakeLists.txt +++ b/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!") diff --git a/bin/versions b/bin/versions index 8b5536b48..29a48ffeb 100644 --- a/bin/versions +++ b/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 diff --git a/docs/installation.md b/docs/installation.md index 4c5c893d8..f4f3e3e67 100644 --- a/docs/installation.md +++ b/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/ From 4b3f7a2186b3561f57a75331f7fb05166fccf533 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Mon, 29 Jul 2019 09:04:40 -0600 Subject: [PATCH 3/8] Updated processing of memcpy and memset intrinsics LLVM 7 removes the alignment argument and hence our processing code had to be updated to account for this change. --- lib/smack/SmackInstGenerator.cpp | 2 -- lib/smack/SmackRep.cpp | 24 +++++++++--------------- 2 files changed, 9 insertions(+), 17 deletions(-) diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index 94d6e2eaa..43aadd3f8 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/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)); } diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index be0bdf4e7..0067f7c57 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -305,23 +305,21 @@ const Stmt *SmackRep::memcpy(const llvm::MemCpyInst &mci) { else length = std::numeric_limits::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::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 << ")"; From 8308149b5cf6c2770c760c5bc905c546cd79940a Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Mon, 29 Jul 2019 12:09:21 -0600 Subject: [PATCH 4/8] Fixed simd shuffle regression Mask was out of range. Also, a clang avx2 argument is needed to get it compiled in a VM. --- test/simd/shuffle.c | 3 ++- test/simd/shuffle_fail.c | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/test/simd/shuffle.c b/test/simd/shuffle.c index 71fa520b2..d93d45795 100644 --- a/test/simd/shuffle.c +++ b/test/simd/shuffle.c @@ -2,6 +2,7 @@ #include // @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; diff --git a/test/simd/shuffle_fail.c b/test/simd/shuffle_fail.c index c33c175f9..bbd5d4974 100644 --- a/test/simd/shuffle_fail.c +++ b/test/simd/shuffle_fail.c @@ -2,6 +2,7 @@ #include // @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; From acbe70f6ebb93e63fb346f350c968d3b04242ccf Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Mon, 29 Jul 2019 14:34:41 -0600 Subject: [PATCH 5/8] Fixed travis config file to use short LLVM version number 7 --- .travis.yml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/.travis.yml b/.travis.yml index f0f84add6..44cdae9c9 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,7 +39,7 @@ 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-7.1 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 @@ -47,13 +47,13 @@ before_install: - sudo apt-get update install: - - sudo apt-get install -y clang-7.1 clang-format-7.1 llvm-7.1-dev mono-complete ninja-build - - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-7.1 20 - - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-7.1 20 - - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-7.1 20 - - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-7.1 20 - - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-7.1 20 - - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-7.1 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: From c5f8613a70e1f1477b80bdc6576cbe2f03eafeba Mon Sep 17 00:00:00 2001 From: Michael Emmi Date: Tue, 30 Jul 2019 18:17:31 -0400 Subject: [PATCH 6/8] Added region-node types to debug output. --- lib/smack/Regions.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 5b746df56..9a0a53806 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -190,7 +190,9 @@ bool Region::overlaps(Region &R) { void Region::print(raw_ostream &O) { // TODO identify the representative - O << "[" << offset << "," << (offset + length) << "]{"; + O << "[" << offset << "," << (offset + length) << "]{"; if (isSingleton()) O << "S"; if (bytewise) From 99aa6fcbd534f3e854ed113763b312883f43c4f4 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Fri, 2 Aug 2019 01:50:32 -0600 Subject: [PATCH 7/8] Fixed formatting --- lib/smack/Regions.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 9a0a53806..c549d8bf5 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -191,7 +191,10 @@ bool Region::overlaps(Region &R) { void Region::print(raw_ostream &O) { // TODO identify the representative O << "[" << offset << "," << (offset + length) << "]{"; if (isSingleton()) O << "S"; From 327a32c91bd3ad5d75815be9733f728df00c7f1c Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Fri, 2 Aug 2019 11:22:05 -0600 Subject: [PATCH 8/8] Bumped version number to 2.3.0 --- Doxyfile | 2 +- share/smack/reach.py | 2 +- share/smack/top.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Doxyfile b/Doxyfile index 67c0f7512..e8bdaf2d8 100644 --- a/Doxyfile +++ b/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 diff --git a/share/smack/reach.py b/share/smack/reach.py index 7e491684d..e094b1a7b 100755 --- a/share/smack/reach.py +++ b/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()]) diff --git a/share/smack/top.py b/share/smack/top.py index a161d6a33..04ebc5d9a 100755 --- a/share/smack/top.py +++ b/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."""