Merge branch 'release-2.5.0'

smackers · Aug 14, 2020 · e41b229 · e41b229
2 parents 212bbdb + c77b8ff
commit e41b229
Show file tree

Hide file tree

Showing 261 changed files with 4,994 additions and 2,909 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -9,68 +9,70 @@ addons:
       - cmake
       - python3-yaml
       - python3-psutil
+      - python3-pip
       - unzip
-      - libz-dev
-      - libedit-dev
+      - ninja-build
       - libboost-all-dev
 
-cache:
-  directories:
-    - $HOME/build/smackers/boogie
-    - $HOME/build/smackers/corral
-    - $HOME/build/smackers/symbooglix
-    - $HOME/build/smackers/lockpwn
-
 env:
   global:
     - COMPILER_NAME=clang COMPILER=clang++ CXX=clang++ CC=clang
   jobs:
     - TRAVIS_ENV="--exhaustive --folder=c/basic"
     - TRAVIS_ENV="--exhaustive --folder=c/data"
     - TRAVIS_ENV="--exhaustive --folder=c/ntdrivers-simplified"
+    - TRAVIS_ENV="--exhaustive --folder=c/ntdrivers"
     - TRAVIS_ENV="--exhaustive --folder=c/bits"
     - TRAVIS_ENV="--exhaustive --folder=c/float"
     - TRAVIS_ENV="--exhaustive --folder=c/locks"
     - TRAVIS_ENV="--exhaustive --folder=c/contracts"
     - TRAVIS_ENV="--exhaustive --folder=c/simd"
     - TRAVIS_ENV="--exhaustive --folder=c/memory-safety"
     - TRAVIS_ENV="--exhaustive --folder=c/pthread"
+    - TRAVIS_ENV="--exhaustive --folder=c/pthread_extras"
     - TRAVIS_ENV="--exhaustive --folder=c/strings"
     - TRAVIS_ENV="--exhaustive --folder=c/special"
+    - TRAVIS_ENV="--exhaustive --folder=rust/array --languages=rust"
     - TRAVIS_ENV="--exhaustive --folder=rust/basic --languages=rust"
+    - TRAVIS_ENV="--exhaustive --folder=rust/box --languages=rust"
     - TRAVIS_ENV="--exhaustive --folder=rust/functions --languages=rust"
     - TRAVIS_ENV="--exhaustive --folder=rust/generics --languages=rust"
     - TRAVIS_ENV="--exhaustive --folder=rust/loops --languages=rust"
+    - TRAVIS_ENV="--exhaustive --folder=rust/panic --languages=rust"
     - TRAVIS_ENV="--exhaustive --folder=rust/recursion --languages=rust"
     - TRAVIS_ENV="--exhaustive --folder=rust/structures --languages=rust"
     - TRAVIS_ENV="--exhaustive --folder=rust/vector --languages=rust"
 
 before_install:
+  - sudo rm -rf /usr/local/clang-7.0.0
+
+install:
+  - source ./bin/versions
   - wget -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
-  - sudo add-apt-repository "deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-8 main"
-  - sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF
+  - sudo add-apt-repository "deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-${LLVM_SHORT_VERSION} main"
+  - wget -q https://packages.microsoft.com/config/ubuntu/18.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb
+  - sudo dpkg -i packages-microsoft-prod.deb
   - sudo apt-get install -y apt-transport-https
-  - echo "deb https://download.mono-project.com/repo/ubuntu stable-bionic main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
   - sudo apt-get update
+  - sudo apt-get install -y clang-${LLVM_SHORT_VERSION} clang-format-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev dotnet-sdk-3.1
+  - pip3 install -U flake8
+  - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_SHORT_VERSION} 20
+  - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-${LLVM_SHORT_VERSION} 20
+  - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-${LLVM_SHORT_VERSION} 20
+  - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-${LLVM_SHORT_VERSION} 20
+  - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-${LLVM_SHORT_VERSION} 20
+  - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-${LLVM_SHORT_VERSION} 20
 
-install:
-  - sudo apt-get install -y clang-8 clang-format-8 llvm-8-dev mono-complete ca-certificates-mono 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:
-  - python --version
+before_script:
   - python3 --version
   - $CXX --version
   - $CC --version
   - clang --version
   - clang++ --version
   - llvm-link --version
   - llvm-config --version
+
+script:
   - ./format/run-clang-format.py -e test/c/basic/transform-out.c -r lib/smack include/smack share/smack/include share/smack/lib test examples
+  - flake8 test/regtest.py share/smack/ --extend-exclude share/smack/svcomp/,share/smack/reach.py
   - INSTALL_RUST=1 ./bin/build.sh
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -6,7 +6,11 @@ cmake_minimum_required(VERSION 3.4.3)
 project(smack)
 
 if (NOT WIN32 OR MSYS OR CYGWIN)
-  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-8 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
+
+  file(STRINGS "bin/versions" LLVM_VERSION_STR REGEX "LLVM_SHORT_VERSION=[0-9]+")
+  string(REGEX MATCH "[0-9]+" LLVM_SHORT_VERSION "${LLVM_VERSION_STR}")
+
+  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-${LLVM_SHORT_VERSION} 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!")
@@ -112,6 +116,7 @@ add_library(smackTranslator STATIC
   include/smack/BplFilePrinter.h
   include/smack/BplPrinter.h
   include/smack/DSAWrapper.h
+  include/smack/InitializePasses.h
   include/smack/Naming.h
   include/smack/Regions.h
   include/smack/SmackInstGenerator.h
@@ -167,7 +172,7 @@ if (Boost_FOUND)
 endif ()
 # We have to import LLVM's cmake definitions to build sea-dsa
 # Borrowed from sea-dsa's CMakeLists.txt
-find_package (LLVM 8.0.1 EXACT CONFIG)
+find_package (LLVM ${LLVM_SHORT_VERSION} CONFIG)
 list(APPEND CMAKE_MODULE_PATH "${LLVM_CMAKE_DIR}")
 include(AddLLVM)
 include(HandleLLVMOptions)
@@ -176,7 +181,7 @@ include(HandleLLVMOptions)
 # The following solution is from: https://stackoverflow.com/questions/30985215/passing-variables-down-to-subdirectory-only
 set(SMACK_BUILD_TYPE "${CMAKE_BUILD_TYPE}")
 set(CMAKE_BUILD_TYPE "Release")
-add_subdirectory(sea-dsa/src)
+add_subdirectory(sea-dsa/lib/seadsa)
 set(CMAKE_BUILD_TYPE ${SMACK_BUILD_TYPE})
 
 target_link_libraries(smackTranslator ${LLVM_LIBS} ${LLVM_SYSTEM_LIBS} ${LLVM_LDFLAGS})

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

diff --git a/LICENSE b/LICENSE
@@ -1,8 +1,8 @@
 The MIT License
 
-Copyright (c) 2008-2019 Zvonimir Rakamaric ([email protected]),
+Copyright (c) 2008-2020 Zvonimir Rakamaric ([email protected]),
                         Michael Emmi ([email protected])
-Modified work Copyright (c) 2013-2019 Marek Baranowski,
+Modified work Copyright (c) 2013-2020 Marek Baranowski,
                                       Montgomery Carter,
                                       Pantazis Deligiannis,
                                       Jack J. Garzella,
@@ -44,10 +44,7 @@ licenses, and/or restrictions:
 
 Program             Directories           License
 -------             -----------           -------
-poolalloc           include/assistDS      lib/DSA/LICENSE
-                    include/dsa
-                    lib/AssistDS
-                    lib/DSA
+sea-dsa             sea-dsa               sea-dsa/license.txt
 run-clang-format    format                format/LICENSE
 
 In addition, a binary distribution of SMACK contains at least the following

diff --git a/README.md b/README.md
@@ -1,5 +1,6 @@
-| **master** | [![Build Status](https://travis-ci.com/smackers/smack.svg?branch=master)](https://travis-ci.com/smackers/smack) | **develop** | [![Build Status](https://travis-ci.com/smackers/smack.svg?branch=develop)](https://travis-ci.com/smackers/smack) |
-| --- | --- | --- | --- |
+
+[![Build Status](https://travis-ci.com/smackers/smack.svg?branch=master)](https://travis-ci.com/smackers/smack)
+[![Build Status](https://travis-ci.com/smackers/smack.svg?branch=develop)](https://travis-ci.com/smackers/smack)
 
 <img src="docs/smack-logo.png" width=400 alt="SMACK Logo" align="right">
 
@@ -47,10 +48,10 @@ See below for system requirements, installation, usage, and everything else.
 
 ### Acknowledgements
 
-SMACK project is partially supported by NSF award CCF 1346756 and Microsoft
-Research SEIF award. We also rely on University of Utah's
-[Emulab](http://www.emulab.net/) infrastructure for extensive benchmarking of
-SMACK.
+SMACK project has been partially supported by funding from the National Science
+Foundation, VMware, and Microsoft Research. We also rely on University of
+Utah's [Emulab](http://www.emulab.net/) infrastructure for extensive
+benchmarking of SMACK.
 
 
 ### Table of Contents

diff --git a/Vagrantfile b/Vagrantfile
@@ -25,7 +25,7 @@ Vagrant.configure(2) do |config|
   #   opensuse_config.vm.box = "chef/opensuse-13.1"
   # end
 
-  config.vm.provision "shell", binary: true, inline: <<-SHELL
+  config.vm.provision "shell", binary: true, privileged: false, inline: <<-SHELL
     apt-get update
     apt-get install -y software-properties-common
     cd /home/vagrant