Merge branch 'release-1.9.0'

smackers · Sep 22, 2017 · 1458fa2 · 1458fa2
2 parents 5d79b66 + c151aed
commit 1458fa2
Show file tree

Hide file tree

Showing 129 changed files with 2,886 additions and 1,313 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -9,7 +9,6 @@ env:
   matrix:
     - TRAVIS_ENV="--exhaustive --folder=basic"
     - TRAVIS_ENV="--exhaustive --folder=ntdrivers-simplified"
-    - TRAVIS_ENV="--exhaustive --folder=pthread_extras"
     - TRAVIS_ENV="--exhaustive --folder=bits"
     - TRAVIS_ENV="--exhaustive --folder=float"
     - TRAVIS_ENV="--exhaustive --folder=locks"
@@ -19,19 +18,21 @@ env:
 
 before_install:
   - sudo rm -rf /usr/local/clang-3.5.0
-  - sudo add-apt-repository "deb http://llvm-apt.ecranbleu.org/apt/trusty/ llvm-toolchain-trusty-3.7 main"
-  - wget -O - http://llvm-apt.ecranbleu.org/apt/llvm-snapshot.gpg.key | sudo apt-key add -
+  - 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-get update
 
 install:
-  - sudo apt-get install -y clang-3.7 llvm-3.7
-  - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-3.7 20
-  - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.7 20
-  - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-3.7 20
-  - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-3.7 20
-  - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-3.7 20
+  - sudo apt-get install -y clang-3.9 llvm-3.9
+  - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-3.9 20
+  - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.9 20
+  - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-3.9 20
+  - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-3.9 20
+  - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-3.9 20
+  - sudo pip install pyyaml psutil
 
 script:
+  - python --version
   - $CXX --version
   - $CC --version
   - clang --version

diff --git 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-3.8 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
+  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-3.9 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!")
@@ -18,8 +18,13 @@ if (NOT WIN32 OR MSYS OR CYGWIN)
     OUTPUT_STRIP_TRAILING_WHITESPACE
   )
 
+  string(REPLACE "-DNDEBUG" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
+  string(REPLACE "-Wno-maybe-uninitialized" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
+  string(REPLACE "-fuse-ld=gold" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
+  string(REPLACE "-Wl," "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
+  string(REPLACE "-gsplit-dwarf" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
   string(REGEX REPLACE "-O[0-9]" "" CMAKE_CXX_FLAGS "${LLVM_CXXFLAGS}")
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fno-exceptions -fno-rtti")
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fno-exceptions -fno-rtti -Wno-undefined-var-template")
   set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0")
   set(CMAKE_C_FLAGS_DEBUG "${CMAKE_C_FLAGS_DEBUG} -O0")
 
@@ -151,6 +156,7 @@ add_library(dsa STATIC
 )
 
 add_library(smackTranslator STATIC
+  include/smack/AddTiming.h
   include/smack/BoogieAst.h
   include/smack/BplFilePrinter.h
   include/smack/BplPrinter.h
@@ -163,13 +169,17 @@ add_library(smackTranslator STATIC
   include/smack/CodifyStaticInits.h
   include/smack/RemoveDeadDefs.h
   include/smack/ExtractContracts.h
+  include/smack/VerifierCodeMetadata.h
   include/smack/SimplifyLibCalls.h
   include/smack/SmackRep.h
   include/smack/MemorySafetyChecker.h
   include/smack/SignedIntegerOverflowChecker.h
+  include/smack/SplitAggregateLoadStore.h
+  lib/smack/AddTiming.cpp
   lib/smack/BoogieAst.cpp
   lib/smack/BplFilePrinter.cpp
   lib/smack/BplPrinter.cpp
+  lib/smack/Debug.cpp
   lib/smack/DSAWrapper.cpp
   lib/smack/Naming.cpp
   lib/smack/Regions.cpp
@@ -179,10 +189,12 @@ add_library(smackTranslator STATIC
   lib/smack/CodifyStaticInits.cpp
   lib/smack/RemoveDeadDefs.cpp
   lib/smack/ExtractContracts.cpp
+  lib/smack/VerifierCodeMetadata.cpp
   lib/smack/SimplifyLibCalls.cpp
   lib/smack/SmackRep.cpp
   lib/smack/MemorySafetyChecker.cpp
   lib/smack/SignedIntegerOverflowChecker.cpp
+  lib/smack/SplitAggregateLoadStore.cpp
 )
 
 add_executable(llvm2bpl

diff --git a/Doxyfile b/Doxyfile
@@ -5,7 +5,7 @@
 #---------------------------------------------------------------------------
 DOXYFILE_ENCODING      = UTF-8
 PROJECT_NAME           = smack
-PROJECT_NUMBER         = 1.8.1
+PROJECT_NUMBER         = 1.9.0
 PROJECT_BRIEF          = "A bounded software verifier."
 PROJECT_LOGO           =
 OUTPUT_DIRECTORY       = docs

diff --git a/bin/build.sh b/bin/build.sh
@@ -53,6 +53,8 @@ CMAKE_INSTALL_PREFIX=
 # Partial list of dependnecies; the rest are added depending on the platform
 DEPENDENCIES="git cmake python-yaml python-psutil unzip wget"
 
+shopt -s extglob
+
 ################################################################################
 #
 # A FEW HELPER FUNCTIONS
@@ -155,18 +157,18 @@ puts "Detected distribution: $distro"
 # Set platform-dependent flags
 case "$distro" in
 linux-opensuse*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/z3-4.4.1-x64-debian-8.2.zip"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-debian-8.2.zip"
   DEPENDENCIES+=" llvm-clang llvm-devel gcc-c++ mono-complete make"
   DEPENDENCIES+=" ncurses-devel zlib-devel"
   ;;
 
-linux-ubuntu-1[46]*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/z3-4.4.1-x64-ubuntu-14.04.zip"
-  DEPENDENCIES+=" clang-3.8 llvm-3.8 mono-complete libz-dev libedit-dev"
+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"
+  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-4.4.1/z3-4.4.1-x64-ubuntu-14.04.zip"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_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"
@@ -221,21 +223,36 @@ then
     sudo zypper --non-interactive install ${DEPENDENCIES}
     ;;
 
-  linux-ubuntu-1[46]*)
+  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"
+      ;;
+    16*)
+      UBUNTU_CODENAME="xenial"
+      ;;
+    *)
+      puts "Release ${RELEASE_VERSION} for ${distro} not supported. Dependencies must be installed manually."
+      exit 1
+      ;;
+    esac
+
     # Adding LLVM repository
-    sudo add-apt-repository "deb http://llvm-apt.ecranbleu.org/apt/trusty/ llvm-toolchain-trusty-3.8 main"
-    ${WGET} -O - http://llvm-apt.ecranbleu.org/apt/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"
+    ${WGET} -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
     # Adding MONO repository
     sudo add-apt-repository "deb http://download.mono-project.com/repo/debian wheezy main"
     sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF
 #    echo "deb http://download.mono-project.com/repo/debian wheezy main" | sudo tee /etc/apt/sources.list.d/mono-xamarin.list
     sudo apt-get update
     sudo apt-get install -y ${DEPENDENCIES}
-    sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-3.8 20
-    sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.8 20
-    sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-3.8 20
-    sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-3.8 20
-    sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-3.8 20
+    sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_SHORT_VERSION} 30
+    sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-${LLVM_SHORT_VERSION} 30
+    sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-${LLVM_SHORT_VERSION} 30
+    sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-${LLVM_SHORT_VERSION} 30
+    sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-${LLVM_SHORT_VERSION} 30
     ;;
 
   linux-ubuntu-12*)
@@ -299,13 +316,13 @@ then
   mkdir -p ${LLVM_DIR}/src/{tools/clang,projects/compiler-rt}
   mkdir -p ${LLVM_DIR}/build
 
-  ${WGET} http://llvm.org/releases/3.8.1/llvm-3.8.1.src.tar.xz
-  ${WGET} http://llvm.org/releases/3.8.1/cfe-3.8.1.src.tar.xz
-  ${WGET} http://llvm.org/releases/3.8.1/compiler-rt-3.8.1.src.tar.xz
+  ${WGET} http://llvm.org/releases/${LLVM_FULL_VERSION}/llvm-${LLVM_FULL_VERSION}.src.tar.xz
+  ${WGET} http://llvm.org/releases/${LLVM_FULL_VERSION}/cfe-${LLVM_FULL_VERSION}.src.tar.xz
+  ${WGET} http://llvm.org/releases/${LLVM_FULL_VERSION}/compiler-rt-${LLVM_FULL_VERSION}.src.tar.xz
 
-  tar -C ${LLVM_DIR}/src -xvf llvm-3.8.1.src.tar.xz --strip 1
-  tar -C ${LLVM_DIR}/src/tools/clang -xvf cfe-3.8.1.src.tar.xz --strip 1
-  tar -C ${LLVM_DIR}/src/projects/compiler-rt -xvf compiler-rt-3.8.1.src.tar.xz --strip 1
+  tar -C ${LLVM_DIR}/src -xvf llvm-${LLVM_FULL_VERSION}.src.tar.xz --strip 1
+  tar -C ${LLVM_DIR}/src/tools/clang -xvf cfe-${LLVM_FULL_VERSION}.src.tar.xz --strip 1
+  tar -C ${LLVM_DIR}/src/projects/compiler-rt -xvf compiler-rt-${LLVM_FULL_VERSION}.src.tar.xz --strip 1
 
   cd ${LLVM_DIR}/build/
   cmake -G "Unix Makefiles" ${CMAKE_INSTALL_PREFIX} -DCMAKE_BUILD_TYPE=Release ../src
@@ -322,7 +339,7 @@ then
 
   ${WGET} ${Z3_DOWNLOAD_LINK} -O z3-downloaded.zip
   unzip -o z3-downloaded.zip -d z3-extracted
-  mv z3-extracted/z3-* ${Z3_DIR}
+  mv -f --backup=numbered z3-extracted/z3-* ${Z3_DIR}
   rm -rf z3-downloaded.zip z3-extracted
 
   puts "Installed Z3"
@@ -333,15 +350,17 @@ if [ ${BUILD_BOOGIE} -eq 1 ]
 then
   puts "Building Boogie"
 
-  git clone https://github.com/boogie-org/boogie.git ${BOOGIE_DIR}
+  if [ ! -d "$BOOGIE_DIR" ] ; then
+    git clone https://github.com/boogie-org/boogie.git ${BOOGIE_DIR}
+  fi
   cd ${BOOGIE_DIR}
   git reset --hard ${BOOGIE_COMMIT}
   cd ${BOOGIE_DIR}/Source
-  ${WGET} https://nuget.org/nuget.exe
+  ${WGET} https://dist.nuget.org/win-x86-commandline/latest/nuget.exe
   mono ./nuget.exe restore Boogie.sln
   rm -rf /tmp/nuget/
   msbuild Boogie.sln /p:Configuration=Release
-  ln -s ${Z3_DIR}/bin/z3 ${BOOGIE_DIR}/Binaries/z3.exe
+  ln -sf ${Z3_DIR}/bin/z3 ${BOOGIE_DIR}/Binaries/z3.exe
 
   puts "Built Boogie"
 fi
@@ -351,13 +370,15 @@ if [ ${BUILD_CORRAL} -eq 1 ]
 then
   puts "Building Corral"
 
-  git clone https://github.com/boogie-org/corral.git ${CORRAL_DIR}
+  if [ ! -d "$CORRAL_DIR" ] ; then
+    git clone https://github.com/boogie-org/corral.git ${CORRAL_DIR}
+  fi
   cd ${CORRAL_DIR}
   git reset --hard ${CORRAL_COMMIT}
   git submodule init
   git submodule update
   msbuild cba.sln /p:Configuration=Release
-  ln -s ${Z3_DIR}/bin/z3 ${CORRAL_DIR}/bin/Release/z3.exe
+  ln -sf ${Z3_DIR}/bin/z3 ${CORRAL_DIR}/bin/Release/z3.exe
 
   puts "Built Corral"
 fi
@@ -367,11 +388,13 @@ then
   puts "Building lockpwn"
 
   cd ${ROOT}
-  git clone https://github.com/smackers/lockpwn.git
+  if [ ! -d "$LOCKPWN_DIR" ] ; then
+    git clone https://github.com/smackers/lockpwn.git
+  fi
   cd ${LOCKPWN_DIR}
   git reset --hard ${LOCKPWN_COMMIT}
   msbuild lockpwn.sln /p:Configuration=Release
-  ln -s ${Z3_DIR}/bin/z3 ${LOCKPWN_DIR}/Binaries/z3.exe
+  ln -sf ${Z3_DIR}/bin/z3 ${LOCKPWN_DIR}/Binaries/z3.exe
 
   puts "Built lockpwn"
 fi

diff --git a/bin/package-smack.sh b/bin/package-smack.sh
diff --git a/bin/versions b/bin/versions
@@ -1,4 +1,7 @@
 MONO_VERSION=5.0.0.100
-BOOGIE_COMMIT=4e4c3a5252
-CORRAL_COMMIT=6f6926e3bb
+Z3_VERSION=4.5.0
+BOOGIE_COMMIT=c609ee2864
+CORRAL_COMMIT=b2738b4839
 LOCKPWN_COMMIT=a4d802a1cb
+LLVM_SHORT_VERSION=3.9
+LLVM_FULL_VERSION=3.9.1
diff --git a/docs/installation.md b/docs/installation.md
@@ -59,8 +59,8 @@ vagrant destroy
 
 SMACK depends on the following projects:
 
-* [LLVM][] version [3.8.1][LLVM-3.8.1]
-* [Clang][] version [3.8.1][Clang-3.8.1]
+* [LLVM][] version [3.9.1][LLVM-3.9.1]
+* [Clang][] version [3.9.1][Clang-3.9.1]
 * [Python][] version 2.7 or greater
 * [Mono][] version 5.0.0 or greater (except on Windows)
 * [Z3][] or compatible SMT-format theorem prover
@@ -168,9 +168,9 @@ shell in the `test` directory by executing
 [CMake]: http://www.cmake.org
 [Python]: http://www.python.org
 [LLVM]: http://llvm.org
-[LLVM-3.8.1]: http://llvm.org/releases/download.html#3.8.1
+[LLVM-3.9.1]: http://llvm.org/releases/download.html#3.9.1
 [Clang]: http://clang.llvm.org
-[Clang-3.8.1]: http://llvm.org/releases/download.html#3.8.1
+[Clang-3.9.1]: http://llvm.org/releases/download.html#3.9.1
 [Boogie]: https://github.com/boogie-org/boogie
 [Corral]: https://corral.codeplex.com/
 [Z3]: https://github.com/Z3Prover/z3/

diff --git a/docs/publications.md b/docs/publications.md
@@ -14,6 +14,11 @@ Zvonimir Rakamaric, Michael Emmi,
 This is an incomplete list of publications that use, leverage, or extend SMACK.
 If you have a publication for this list, please email [Zvonimir](mailto:[email protected]).
 
+1. [Refining Interprocedural Change-Impact Analysis using Equivalence Relations](https://www.microsoft.com/en-us/research/publication/refining-interprocedural-change-impact-analysis-using-equivalence-relations),
+Alex Gyori, Shuvendu Lahiri, Nimrod Partush,
+26th ACM SIGSOFT International Symposium on Software Testing and Analysis
+(ISSTA 2017)
+
 1. [Verifying Constant-Time Implementations](https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/almeida),
 Jose Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, Michael Emmi,
 25th USENIX Security Symposium

diff --git a/include/assistDS/DataStructureCallGraph.h b/include/assistDS/DataStructureCallGraph.h
@@ -20,7 +20,6 @@
 
 #include "llvm/IR/Module.h"
 #include "llvm/Analysis/CallGraph.h"
-#include "llvm/Support/Debug.h"
 #include "llvm/Support/raw_ostream.h"
 
 namespace llvm {

diff --git a/include/dsa/DSGraphTraits.h b/include/dsa/DSGraphTraits.h
@@ -97,27 +97,6 @@ template <> struct GraphTraits<const DSNode*> {
   static ChildIteratorType child_end(NodeType *N) { return N->end(); }
 };
 
-static       DSNode &dereference (      DSNode *N) { return *N; }
-
-template <> struct GraphTraits<DSGraph*> {
-  typedef DSNode NodeType;
-  typedef DSNode::iterator ChildIteratorType;
-
-  typedef std::pointer_to_unary_function<DSNode *, DSNode&> DerefFun;
-
-  // nodes_iterator/begin/end - Allow iteration over all nodes in the graph
-  typedef mapped_iterator<DSGraph::node_iterator, DerefFun> nodes_iterator;
-  static nodes_iterator nodes_begin(DSGraph *G) {
-    return map_iterator(G->node_begin(), DerefFun(dereference));
-  }
-  static nodes_iterator nodes_end(DSGraph *G) {
-    return map_iterator(G->node_end(), DerefFun(dereference));
-  }
-
-  static ChildIteratorType child_begin(NodeType *N) { return N->begin(); }
-  static ChildIteratorType child_end(NodeType *N) { return N->end(); }
-};
-
 template <> struct GraphTraits<const DSGraph*> {
   typedef const DSNode NodeType;
   typedef DSNode::const_iterator ChildIteratorType;