Merge branch 'release-1.8.0'

.travis.yml

@@ -0,0 +1,40 @@
+language: generic
+dist: trusty
+sudo: required
+compiler: clang
+
+env:
+  global:
+    - COMPILER_NAME=clang COMPILER=clang++ CXX=clang++ CC=clang
+  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"
+    - TRAVIS_ENV="--exhaustive --folder=contracts"
+    - TRAVIS_ENV="--exhaustive --folder=memory-safety"
+    - TRAVIS_ENV="--exhaustive --folder=pthread"
+
+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 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
+
+script:
+  - $CXX --version
+  - $CC --version
+  - clang --version
+  - clang++ --version
+  - ./bin/build.sh
+

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 PATHS ${LLVM_CONFIG} DOC "llvm-config")
+  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-3.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!")
@@ -18,7 +18,10 @@ if (NOT WIN32 OR MSYS OR CYGWIN)
     OUTPUT_STRIP_TRAILING_WHITESPACE
   )
 
-  set(LLVM_CXXFLAGS "${LLVM_CXXFLAGS} -fno-exceptions -fno-rtti")
+  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_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0")
+  set(CMAKE_C_FLAGS_DEBUG "${CMAKE_C_FLAGS_DEBUG} -O0")
 
   execute_process(
     COMMAND ${LLVM_CONFIG_EXECUTABLE} --libs
@@ -52,7 +55,12 @@ else()
     message(FATAL_ERROR "Invalid LLVM build directory: ${LLVM_BUILD}")
   endif()
 
-  set(LLVM_CXXFLAGS "\"/I${LLVM_SRC}/include\" \"/I${LLVM_BUILD}/include\" -D_SCL_SECURE_NO_WARNINGS -wd4146 -wd4244 -wd4355 -wd4482 -wd4800")
+  ## TODO how to enable debug mode on Windows?
+  # set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0")
+  # set(CMAKE_C_FLAGS_DEBUG "${CMAKE_C_FLAGS_DEBUG} -O0")
+
+  set(CMAKE_CXX_FLAGS "\"/I${LLVM_SRC}/include\" \"/I${LLVM_BUILD}/include\" -D_SCL_SECURE_NO_WARNINGS -wd4146 -wd4244 -wd4355 -wd4482 -wd4800")
+
   set(LLVM_LDFLAGS "")
   set(LLVM_LIBS "${LLVM_LIBDIR}/LLVMTransformUtils.lib" "${LLVM_LIBDIR}/LLVMipa.lib" "${LLVM_LIBDIR}/LLVMAnalysis.lib" "${LLVM_LIBDIR}/LLVMTarget.lib" "${LLVM_LIBDIR}/LLVMMC.lib" "${LLVM_LIBDIR}/LLVMObject.lib" "${LLVM_LIBDIR}/LLVMBitReader.lib" "${LLVM_LIBDIR}/LLVMCore.lib" "${LLVM_LIBDIR}/LLVMSupport.lib")
 
@@ -146,7 +154,7 @@ add_library(smackTranslator STATIC
   include/smack/BoogieAst.h
   include/smack/BplFilePrinter.h
   include/smack/BplPrinter.h
-  include/smack/DSAAliasAnalysis.h
+  include/smack/DSAWrapper.h
   include/smack/Naming.h
   include/smack/Regions.h
   include/smack/SmackInstGenerator.h
@@ -157,13 +165,12 @@ add_library(smackTranslator STATIC
   include/smack/ExtractContracts.h
   include/smack/SimplifyLibCalls.h
   include/smack/SmackRep.h
-  include/smack/SmackRepFlatMem.h
   include/smack/MemorySafetyChecker.h
   include/smack/SignedIntegerOverflowChecker.h
   lib/smack/BoogieAst.cpp
   lib/smack/BplFilePrinter.cpp
   lib/smack/BplPrinter.cpp
-  lib/smack/DSAAliasAnalysis.cpp
+  lib/smack/DSAWrapper.cpp
   lib/smack/Naming.cpp
   lib/smack/Regions.cpp
   lib/smack/SmackInstGenerator.cpp
@@ -174,7 +181,6 @@ add_library(smackTranslator STATIC
   lib/smack/ExtractContracts.cpp
   lib/smack/SimplifyLibCalls.cpp
   lib/smack/SmackRep.cpp
-  lib/smack/SmackRepFlatMem.cpp
   lib/smack/MemorySafetyChecker.cpp
   lib/smack/SignedIntegerOverflowChecker.cpp
 )
@@ -183,9 +189,6 @@ add_executable(llvm2bpl
   tools/llvm2bpl/llvm2bpl.cpp
 )
 
-set_target_properties(llvm2bpl smackTranslator assistDS dsa
-    PROPERTIES COMPILE_FLAGS "${LLVM_CXXFLAGS}")
-
 target_link_libraries(smackTranslator ${LLVM_LIBS} ${LLVM_SYSTEM_LIBS} ${LLVM_LDFLAGS})
 target_link_libraries(llvm2bpl smackTranslator assistDS dsa)
 

Doxyfile

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

README.md

@@ -1,4 +1,5 @@
-[![Build Status](http://kornat.cs.utah.edu:8080/job/smack/badge/icon)](http://kornat.cs.utah.edu:8080/job/smack/)
+| **master** | [![Build Status](https://travis-ci.org/smackers/smack.svg?branch=master)](https://travis-ci.org/smackers/smack) | **develop** | [![Build Status](https://travis-ci.org/smackers/smack.svg?branch=develop)](https://travis-ci.org/smackers/smack) |
+| --- | --- | --- | --- |
 
 <img src="docs/smack-logo.png" width=400 alt="SMACK Logo" align="right">
 

bin/build.sh

@@ -43,7 +43,7 @@ LLVM_DIR="${ROOT}/llvm"
 source ${SMACK_DIR}/bin/versions
 
 SMACKENV=${ROOT}/smack.environment
-WGET="wget --no-verbose --method=GET"
+WGET="wget --no-verbose"
 
 # Install prefix -- system default is used if left unspecified
 INSTALL_PREFIX=
@@ -160,9 +160,9 @@ linux-opensuse*)
   DEPENDENCIES+=" ncurses-devel zlib-devel"
   ;;
 
-linux-ubuntu-14*)
+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.7 llvm-3.7 mono-complete libz-dev libedit-dev"
+  DEPENDENCIES+=" clang-3.8 llvm-3.8 mono-complete libz-dev libedit-dev"
   ;;
 
 linux-ubuntu-12*)
@@ -221,21 +221,21 @@ then
     sudo zypper --non-interactive install ${DEPENDENCIES}
     ;;
 
-  linux-ubuntu-14*)
+  linux-ubuntu-1[46]*)
     # Adding LLVM repository
-    sudo add-apt-repository "deb http://llvm-apt.ecranbleu.org/apt/trusty/ llvm-toolchain-trusty-3.7 main"
+    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 -
     # 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.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 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
     ;;
 
   linux-ubuntu-12*)
@@ -299,16 +299,16 @@ then
   mkdir -p ${LLVM_DIR}/src/{tools/clang,projects/compiler-rt}
   mkdir -p ${LLVM_DIR}/build
 
-  ${WGET} http://llvm.org/releases/3.7.1/llvm-3.7.1.src.tar.xz
-  ${WGET} http://llvm.org/releases/3.7.1/cfe-3.7.1.src.tar.xz
-  ${WGET} http://llvm.org/releases/3.7.1/compiler-rt-3.7.1.src.tar.xz
+  ${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
 
-  tar -C ${LLVM_DIR}/src -xvf llvm-3.7.1.src.tar.xz --strip 1
-  tar -C ${LLVM_DIR}/src/tools/clang -xvf cfe-3.7.1.src.tar.xz --strip 1
-  tar -C ${LLVM_DIR}/src/projects/compiler-rt -xvf compiler-rt-3.7.1.src.tar.xz --strip 1
+  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
 
   cd ${LLVM_DIR}/build/
-  cmake ${CMAKE_INSTALL_PREFIX} -DCMAKE_BUILD_TYPE=Release ../src
+  cmake -G "Unix Makefiles" ${CMAKE_INSTALL_PREFIX} -DCMAKE_BUILD_TYPE=Release ../src
   make
   sudo make install
 
@@ -340,7 +340,7 @@ then
   ${WGET} https://nuget.org/nuget.exe
   mono ./nuget.exe restore Boogie.sln
   rm -rf /tmp/nuget/
-  xbuild Boogie.sln /p:Configuration=Release
+  msbuild Boogie.sln /p:Configuration=Release
   ln -s ${Z3_DIR}/bin/z3 ${BOOGIE_DIR}/Binaries/z3.exe
 
   puts "Built Boogie"
@@ -356,7 +356,7 @@ then
   git reset --hard ${CORRAL_COMMIT}
   git submodule init
   git submodule update
-  xbuild cba.sln /p:Configuration=Release
+  msbuild cba.sln /p:Configuration=Release
   ln -s ${Z3_DIR}/bin/z3 ${CORRAL_DIR}/bin/Release/z3.exe
 
   puts "Built Corral"
@@ -370,7 +370,7 @@ then
   git clone https://github.com/smackers/lockpwn.git
   cd ${LOCKPWN_DIR}
   git reset --hard ${LOCKPWN_COMMIT}
-  xbuild lockpwn.sln /p:Configuration=Release
+  msbuild lockpwn.sln /p:Configuration=Release
   ln -s ${Z3_DIR}/bin/z3 ${LOCKPWN_DIR}/Binaries/z3.exe
 
   puts "Built lockpwn"
@@ -403,7 +403,7 @@ then
   puts "Running SMACK regression tests"
 
   cd ${SMACK_DIR}/test
-  ./regtest.py
+  ./regtest.py ${TRAVIS_ENV}
   res=$?
 
   puts "Regression tests complete"

bin/package-smack.sh

@@ -6,7 +6,7 @@
 # Note: this script requires CDE to be downloaded from
 # http://www.pgbovine.net/cde.html
 
-VERSION=1.7.2
+VERSION=1.8.0
 PACKAGE=smack-$VERSION-64
 
 # Create folder to export

bin/versions

@@ -1,4 +1,4 @@
-MONO_VERSION=3.8.0
+MONO_VERSION=5.0.0.100
 BOOGIE_COMMIT=4e4c3a5252
 CORRAL_COMMIT=874a078e39
 LOCKPWN_COMMIT=a4d802a1cb

docs/installation.md

@@ -59,10 +59,10 @@ vagrant destroy
 
 SMACK depends on the following projects:
 
-* [LLVM][] version [3.7.1][LLVM-3.7.1]
-* [Clang][] version [3.7.1][Clang-3.7.1]
+* [LLVM][] version [3.8.1][LLVM-3.8.1]
+* [Clang][] version [3.8.1][Clang-3.8.1]
 * [Python][] version 2.7 or greater
-* [Mono][] version 3.8.0 or greater (except on Windows)
+* [Mono][] version 5.0.0 or greater (except on Windows)
 * [Z3][] or compatible SMT-format theorem prover
 * [Boogie][] or [Corral][] or compatible Boogie-format verifier
 
@@ -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.7.1]: http://llvm.org/releases/download.html#3.7.1
+[LLVM-3.8.1]: http://llvm.org/releases/download.html#3.8.1
 [Clang]: http://clang.llvm.org
-[Clang-3.7.1]: http://llvm.org/releases/download.html#3.7.1
+[Clang-3.8.1]: http://llvm.org/releases/download.html#3.8.1
 [Boogie]: https://github.com/boogie-org/boogie
 [Corral]: https://corral.codeplex.com/
 [Z3]: https://github.com/Z3Prover/z3/

include/smack/CodifyStaticInits.h

@@ -6,7 +6,6 @@
 #include "llvm/IR/Instructions.h"
 #include "llvm/IR/Module.h"
 #include "llvm/Pass.h"
-#include "smack/DSAAliasAnalysis.h"
 
 namespace smack {
 

include/smack/DSAAliasAnalysis.h → include/smack/DSAWrapper.h

@@ -1,19 +1,11 @@
-//===- DataStructureAA.cpp - Data Structure Based Alias Analysis ----------===//
 //
 //                     The LLVM Compiler Infrastructure
 //
 // This file was developed by the LLVM research group and is distributed under
-// the University of Illinois Open Source License. See LICENSE.TXT for details.
+// the University of Illinois Open Source License. See LICENSE for details.
 //
-//===----------------------------------------------------------------------===//
-//
-// This pass uses the top-down data structure graphs to implement a simple
-// context sensitive alias analysis.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef LLVM_ANALYSIS_DATA_STRUCTURE_AA_H
-#define LLVM_ANALYSIS_DATA_STRUCTURE_AA_H
+#ifndef DSAWRAPPER_H
+#define DSAWRAPPER_H
 
 #include "assistDS/DSNodeEquivs.h"
 #include "dsa/DataStructure.h"
@@ -61,7 +53,7 @@ class MemcpyCollector : public llvm::InstVisitor<MemcpyCollector> {
   }
 };
 
-class DSAAliasAnalysis : public llvm::ModulePass, public llvm::AliasAnalysis {
+class DSAWrapper : public llvm::ModulePass {
 private:
   llvm::Module *module;
   llvm::TDDataStructures *TD;
@@ -73,14 +65,16 @@ class DSAAliasAnalysis : public llvm::ModulePass, public llvm::AliasAnalysis {
   std::unordered_set<const llvm::DSNode*> intConversions;
   const DataLayout* dataLayout;
 
+  std::vector<const llvm::DSNode*> collectMemcpys(llvm::Module &M, MemcpyCollector* mcc);
+  std::vector<const llvm::DSNode*> collectStaticInits(llvm::Module &M);
+  llvm::DSGraph *getGraphForValue(const llvm::Value *V);
+  unsigned getOffset(const MemoryLocation* l);
+
 public:
   static char ID;
-  DSAAliasAnalysis() : ModulePass(ID) {}
-
-  void printDSAGraphs(const char* Filename);
+  DSAWrapper() : ModulePass(ID) {}
 
   virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const {
-    llvm::AliasAnalysis::getAnalysisUsage(AU);
     AU.setPreservesAll();
     AU.addRequiredTransitive<llvm::BUDataStructures>();
     AU.addRequiredTransitive<llvm::TDDataStructures>();
@@ -90,7 +84,6 @@ class DSAAliasAnalysis : public llvm::ModulePass, public llvm::AliasAnalysis {
 
   virtual bool runOnModule(llvm::Module &M) {
     dataLayout = &M.getDataLayout();
-    InitializeAliasAnalysis(this, dataLayout);
     TD = &getAnalysis<llvm::TDDataStructures>();
     BU = &getAnalysis<llvm::BUDataStructures>();
     nodeEqs = &getAnalysis<llvm::DSNodeEquivs>();
@@ -101,29 +94,19 @@ class DSAAliasAnalysis : public llvm::ModulePass, public llvm::AliasAnalysis {
     return false;
   }
 
-  const llvm::DSNode *getNode(const llvm::Value* v);
-  bool isAlloced(const llvm::Value* v);
-  bool isExternal(const llvm::Value* v);
-  bool isSingletonGlobal(const llvm::Value *V);
+  bool isMemcpyd(const llvm::DSNode* n);
+  bool isStaticInitd(const llvm::DSNode* n);
   bool isFieldDisjoint(const llvm::Value* V, const llvm::Function* F);
   bool isFieldDisjoint(const GlobalValue* V, unsigned offset);
   bool isRead(const llvm::Value* V);
-  bool isMemcpyd(const llvm::DSNode* n);
-  bool isStaticInitd(const llvm::DSNode* n);
+  bool isAlloced(const llvm::Value* v);
+  bool isExternal(const llvm::Value* v);
+  bool isSingletonGlobal(const llvm::Value *V);
   unsigned getPointedTypeSize(const Value* v);
   unsigned getOffset(const Value* v);
-
-  virtual AliasResult alias(const MemoryLocation &LocA, const MemoryLocation &LocB);
-
-private:
-  bool isComplicatedNode(const llvm::DSNode* n);
-  std::vector<const llvm::DSNode*> collectMemcpys(llvm::Module &M, MemcpyCollector* mcc);
-  std::vector<const llvm::DSNode*> collectStaticInits(llvm::Module &M);
-  llvm::DSGraph *getGraphForValue(const llvm::Value *V);
-  bool equivNodes(const llvm::DSNode* n1, const llvm::DSNode* n2);
-  unsigned getOffset(const MemoryLocation* l);
-  bool disjoint(const MemoryLocation* l1, const MemoryLocation* l2);
+  const llvm::DSNode *getNode(const llvm::Value* v);
+  void printDSAGraphs(const char* Filename);
 };
 }
 
-#endif
+#endif // DSAWRAPPER_H