From c2aafcbd3abf5f9e52d89c8848068f4b799ad4a3 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Sat, 3 Aug 2019 07:11:57 -0600 Subject: [PATCH 1/5] Updated LLVM to 8.0.1 --- .travis.yml | 16 ++++++++-------- CMakeLists.txt | 2 +- bin/versions | 4 ++-- docs/installation.md | 8 ++++---- lib/DSA/Basic.cpp | 1 - 5 files changed, 15 insertions(+), 16 deletions(-) diff --git a/.travis.yml b/.travis.yml index 44cdae9c9..70f6ce234 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 main" + - sudo add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial-8 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 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 apt-get install -y clang-8 clang-format-8 llvm-8-dev mono-complete ninja-build + - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-8 20 + - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-8 20 + - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-8 20 + - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-8 20 + - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-8 20 + - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-8 20 - sudo pip install pyyaml psutil script: diff --git a/CMakeLists.txt b/CMakeLists.txt index f416e8a51..40f5078cc 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-7.1 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config") + find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-8 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 29a48ffeb..d9e780e1d 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=7 -LLVM_FULL_VERSION=7.1.0 +LLVM_SHORT_VERSION=8 +LLVM_FULL_VERSION=8.0.1 RUST_VERSION=2016-12-16 diff --git a/docs/installation.md b/docs/installation.md index f4f3e3e67..e129dd08b 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 [7.1.0][LLVM-7.1.0] -* [Clang][] version [7.1.0][Clang-7.1.0] +* [LLVM][] version [8.0.1][LLVM-8.0.1] +* [Clang][] version [8.0.1][Clang-8.0.1] * [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-7.1.0]: http://llvm.org/releases/download.html#7.1.0 +[LLVM-8.0.1]: http://llvm.org/releases/download.html#8.0.1 [Clang]: http://clang.llvm.org -[Clang-7.1.0]: http://llvm.org/releases/download.html#7.1.0 +[Clang-8.0.1]: http://llvm.org/releases/download.html#8.0.1 [Boogie]: https://github.com/boogie-org/boogie [Corral]: https://github.com/boogie-org/corral [Z3]: https://github.com/Z3Prover/z3/ diff --git a/lib/DSA/Basic.cpp b/lib/DSA/Basic.cpp index 46b429626..0088aef40 100644 --- a/lib/DSA/Basic.cpp +++ b/lib/DSA/Basic.cpp @@ -21,7 +21,6 @@ #include "llvm/IR/Instructions.h" #include "llvm/IR/Intrinsics.h" #include "llvm/IR/Module.h" -#include "llvm/IR/TypeBuilder.h" #include "llvm/IR/InstIterator.h" #include "llvm/IR/GetElementPtrTypeIterator.h" From bb39de7c9c1bbfe128a11fb484062779cf394d98 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Sat, 3 Aug 2019 09:01:16 -0600 Subject: [PATCH 2/5] Removed references to TerminatorInst This class got removed in LLVM 8. --- include/smack/SmackInstGenerator.h | 2 +- lib/smack/NormalizeLoops.cpp | 4 ++-- lib/smack/SmackInstGenerator.cpp | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/include/smack/SmackInstGenerator.h b/include/smack/SmackInstGenerator.h index 18f897b7f..e65db1f5e 100644 --- a/include/smack/SmackInstGenerator.h +++ b/include/smack/SmackInstGenerator.h @@ -36,7 +36,7 @@ class SmackInstGenerator : public llvm::InstVisitor { Block *createBlock(); Block *getBlock(llvm::BasicBlock *bb); - void generatePhiAssigns(llvm::TerminatorInst &i); + void generatePhiAssigns(llvm::Instruction &i); void generateGotoStmts( llvm::Instruction &i, std::vector> target); diff --git a/lib/smack/NormalizeLoops.cpp b/lib/smack/NormalizeLoops.cpp index d21a5f1a5..457cad557 100644 --- a/lib/smack/NormalizeLoops.cpp +++ b/lib/smack/NormalizeLoops.cpp @@ -46,7 +46,7 @@ BasicBlock *makeForwardingBlock(BasicBlock *target) { * Returns a vector of each successor index in \param ti which equals \param * headerBlock. */ -std::vector getSuccessorIndices(TerminatorInst *ti, +std::vector getSuccessorIndices(Instruction *ti, BasicBlock *headerBlock) { std::vector result; unsigned numSuccs = ti->getNumSuccessors(); @@ -71,7 +71,7 @@ std::vector getSuccessorIndices(TerminatorInst *ti, */ void splitBlock(BasicBlock *BB, BasicBlock *headerBlock, std::map &blockMap) { - TerminatorInst *ti = BB->getTerminator(); + Instruction *ti = BB->getTerminator(); // Get a list of all successor indices which point to headerBlock. std::vector succIndices = getSuccessorIndices(ti, headerBlock); diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index 43aadd3f8..55fcd4807 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -177,7 +177,7 @@ void SmackInstGenerator::visitInstruction(llvm::Instruction &inst) { llvm_unreachable("Instruction not handled."); } -void SmackInstGenerator::generatePhiAssigns(llvm::TerminatorInst &ti) { +void SmackInstGenerator::generatePhiAssigns(llvm::Instruction &ti) { llvm::BasicBlock *block = ti.getParent(); std::list lhs; std::list rhs; From 976422fc4d7072198bcf476001ef9e30feeb3a25 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Tue, 6 Aug 2019 11:49:17 -0600 Subject: [PATCH 3/5] Updated vagrant VM to Ubuntu 18.04 bionic --- Vagrantfile | 2 +- bin/build.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Vagrantfile b/Vagrantfile index 22d9228ea..7f342ebd1 100644 --- a/Vagrantfile +++ b/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 = "bento/ubuntu-16.04" + ubuntu_config.vm.box = "bento/ubuntu-18.04" end # This provision, 'fix-no-tty', gets rid of an error during build diff --git a/bin/build.sh b/bin/build.sh index 1d905b443..c20615efd 100755 --- a/bin/build.sh +++ b/bin/build.sh @@ -279,8 +279,8 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then fi # Adding LLVM repository - sudo add-apt-repository "deb http://apt.llvm.org/${UBUNTU_CODENAME}/ llvm-toolchain-${UBUNTU_CODENAME}-${LLVM_SHORT_VERSION} main" ${WGET} -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add - + sudo add-apt-repository "deb http://apt.llvm.org/${UBUNTU_CODENAME}/ llvm-toolchain-${UBUNTU_CODENAME}-${LLVM_SHORT_VERSION} main" # Adding MONO repository sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF sudo apt-get install -y apt-transport-https From f828333366741e09a9084c2f6243c7d47bc182e2 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 6 Aug 2019 22:26:17 -0600 Subject: [PATCH 4/5] Updated Dockerfile to Ubuntu 18.04 bionic --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index a419042bb..fbb10f8bc 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,4 +1,4 @@ -FROM ubuntu:16.04 +FROM ubuntu:18.04 MAINTAINER Shaobo He ENV SMACKDIR /home/user/smack From 63bce15e72dfb3ebb5a5bbb2b749fbce2bda9087 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Wed, 7 Aug 2019 04:26:14 -0600 Subject: [PATCH 5/5] Bumped version number to 2.4.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 e8bdaf2d8..f77267f29 100644 --- a/Doxyfile +++ b/Doxyfile @@ -5,7 +5,7 @@ #--------------------------------------------------------------------------- DOXYFILE_ENCODING = UTF-8 PROJECT_NAME = smack -PROJECT_NUMBER = 2.3.0 +PROJECT_NUMBER = 2.4.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 e094b1a7b..1ff4f2723 100755 --- a/share/smack/reach.py +++ b/share/smack/reach.py @@ -11,7 +11,7 @@ from smackgen import * from smackverify import * -VERSION = '2.3.0' +VERSION = '2.4.0' def reachParser(): parser = argparse.ArgumentParser(add_help=False, parents=[verifyParser()]) diff --git a/share/smack/top.py b/share/smack/top.py index 04ebc5d9a..97cb68db2 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.3.0' +VERSION = '2.4.0' def results(args): """A dictionary of the result output messages."""