Merge branch 'release-2.0.0'

.travis.yml

@@ -1,5 +1,5 @@
 language: generic
-dist: trusty
+dist: xenial
 sudo: required
 compiler: clang
 
@@ -38,21 +38,22 @@ env:
     - TRAVIS_ENV="--exhaustive --folder=strings"
 
 before_install:
-  - sudo rm -rf /usr/local/clang-3.5.0
-  - sudo add-apt-repository "deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.9 main"
+  - sudo rm -rf /usr/local/clang-7.0.0
+  - sudo add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial-4.0 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
-  - echo "deb https://download.mono-project.com/repo/ubuntu stable-trusty main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
+  - echo "deb https://download.mono-project.com/repo/ubuntu stable-xenial main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
   - sudo apt-get update
 
 install:
-  - sudo apt-get install -y clang-3.9 llvm-3.9 mono-complete
-  - 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 apt-get install -y clang-4.0 clang-format-4.0 llvm-4.0-dev mono-complete ninja-build
+  - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-4.0 20
+  - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-4.0 20
+  - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-4.0 20
+  - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-4.0 20
+  - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-4.0 20
+  - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-4.0 20
   - sudo pip install pyyaml psutil
 
 script:
@@ -61,4 +62,7 @@ script:
   - $CC --version
   - clang --version
   - clang++ --version
+  - llvm-link --version
+  - llvm-config --version
+  - ./format/run-clang-format.py -e test/basic/transform-out.c -r lib/smack include/smack share/smack/include share/smack/lib test examples
   - ./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-3.9 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
+  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-4.0 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!")
@@ -179,6 +179,8 @@ add_library(smackTranslator STATIC
   include/smack/IntegerOverflowChecker.h
   include/smack/NormalizeLoops.h
   include/smack/SplitAggregateValue.h
+  include/smack/Prelude.h
+  include/smack/SmackWarnings.h
   lib/smack/AddTiming.cpp
   lib/smack/BoogieAst.cpp
   lib/smack/BplFilePrinter.cpp
@@ -201,6 +203,8 @@ add_library(smackTranslator STATIC
   lib/smack/IntegerOverflowChecker.cpp
   lib/smack/NormalizeLoops.cpp
   lib/smack/SplitAggregateValue.cpp
+  lib/smack/Prelude.cpp
+  lib/smack/SmackWarnings.cpp
 )
 
 add_executable(llvm2bpl

CONTRIBUTING.md

@@ -12,5 +12,7 @@ items before you start contributing:
 * We follow guidelines for [good git commit
   practice](https://wiki.openstack.org/wiki/GitCommitMessages)
 * We follow the [LLVM Coding
-  Standards](http://llvm.org/docs/CodingStandards.html)
+  Standards](http://llvm.org/docs/CodingStandards.html). We check the LLVM code
+  formatting rules during continuous integration using
+  [clang-format](https://clang.llvm.org/docs/ClangFormat.html).
 

Dockerfile

@@ -0,0 +1,32 @@
+FROM ubuntu:16.04
+MAINTAINER Shaobo He <[email protected]>
+
+ENV SMACKDIR /home/user/smack
+
+RUN apt-get update && \
+      apt-get -y install \
+      software-properties-common \
+      wget \
+      sudo
+
+# Borrowed from JFS
+# Create `user` user for container with password `user`.  and give it
+# password-less sudo access
+RUN useradd -m user && \
+    echo user:user | chpasswd && \
+    cp /etc/sudoers /etc/sudoers.bak && \
+    echo 'user  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
+
+USER user
+
+# Add the current directory to `/home/user/smack`
+ADD --chown=user . $SMACKDIR
+
+# Set the work directory
+WORKDIR $SMACKDIR
+
+# Build SMACK
+RUN sudo bin/build.sh
+
+# Add envinronment
+RUN echo "source /home/user/smack.environment" >> ~/.bashrc

Doxyfile

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

LICENSE

@@ -1,12 +1,15 @@
 The MIT License
 
-Copyright (c) 2008-2018 Zvonimir Rakamaric ([email protected]),
+Copyright (c) 2008-2019 Zvonimir Rakamaric ([email protected]),
                         Michael Emmi ([email protected])
-Modified work Copyright (c) 2013-2018 Montgomery Carter,
+Modified work Copyright (c) 2013-2019 Marek Baranowski,
+                                      Montgomery Carter,
                                       Pantazis Deligiannis,
+                                      Jack J. Garzella,
                                       Dietrich Geisler,
                                       Arvind Haran,
                                       Shaobo He,
+                                      Liam Machado,
                                       Jiten Thakkar,
                                       Jonathan Whitaker
 
@@ -32,25 +35,26 @@ THE SOFTWARE.
 Copyrights and Licenses for Third Party Software Distributed with SMACK:
 ==============================================================================
 SMACK contains code written by third parties.  Such software will have its own
-individual LICENSE.TXT file in the directory in which it appears.  This file
+individual LICENSE file in the directory in which it appears.  This file
 will describe the copyrights, license, and restrictions which apply to that
 code.
 
 The following pieces of software have additional or alternate copyrights,
 licenses, and/or restrictions:
 
-Program             Directories
--------             -----------
-poolalloc           include/assistDS
+Program             Directories           License
+-------             -----------           -------
+poolalloc           include/assistDS      lib/DSA/LICENSE
                     include/dsa
                     lib/AssistDS
                     lib/DSA
+run-clang-format    format                format/LICENSE
 
 In addition, a binary distribution of SMACK contains at least the following
 tools and packages, which come with their own licenses:
-- LLVM, clang, LLVM runtime (http://llvm.org/)
-- mono (http://www.mono-project.com/)
-- Boogie (https://github.com/boogie-org/boogie/)
-- Corral (https://github.com/boogie-org/corral/)
-- Z3 (https://github.com/Z3Prover/z3/)
+- LLVM, clang, LLVM runtime (http://llvm.org)
+- Boogie (https://github.com/boogie-org/boogie)
+- Corral (https://github.com/boogie-org/corral)
+- lockpwn (https://github.com/smackers/lockpwn)
+- Z3 (https://github.com/Z3Prover/z3)
 

bin/build.sh

@@ -58,7 +58,7 @@ CONFIGURE_INSTALL_PREFIX=
 CMAKE_INSTALL_PREFIX=
 
 # Partial list of dependencies; the rest are added depending on the platform
-DEPENDENCIES="git cmake python-yaml python-psutil unzip wget"
+DEPENDENCIES="git cmake python-yaml python-psutil unzip wget ninja-build"
 
 shopt -s extglob
 
@@ -181,23 +181,28 @@ puts "Detected distribution: $distro"
 # Set platform-dependent flags
 case "$distro" in
 linux-opensuse*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-debian-8.10.zip"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/Z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-debian-8.10.zip"
   DEPENDENCIES+=" llvm-clang llvm-devel gcc-c++ mono-complete make"
   DEPENDENCIES+=" ncurses-devel zlib-devel"
   ;;
 
 linux-@(ubuntu|neon)-14*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-14.04.zip"
-  DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION} mono-complete libz-dev libedit-dev"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/Z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-14.04.zip"
+  DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev mono-complete libz-dev libedit-dev"
   ;;
 
 linux-@(ubuntu|neon)-16*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-16.04.zip"
-  DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION} mono-complete libz-dev libedit-dev"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/Z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-16.04.zip"
+  DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev mono-complete libz-dev libedit-dev"
+  ;;
+
+linux-@(ubuntu|neon)-18*)
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/Z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-16.04.zip"
+  DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev mono-complete libz-dev libedit-dev"
   ;;
 
 linux-ubuntu-12*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-14.04.zip"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/Z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_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"
@@ -251,7 +256,7 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then
     sudo zypper --non-interactive install ${DEPENDENCIES}
     ;;
 
-  linux-@(ubuntu|neon)-1[46]*)
+  linux-@(ubuntu|neon)-1[468]*)
     RELEASE_VERSION=$(get-platform-trim "$(lsb_release -r)" | awk -F: '{print $2;}')
     case "$RELEASE_VERSION" in
     14*)
@@ -260,6 +265,9 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then
     16*)
       UBUNTU_CODENAME="xenial"
       ;;
+    18*)
+      UBUNTU_CODENAME="bionic"
+      ;;
     *)
       puts "Release ${RELEASE_VERSION} for ${distro} not supported. Dependencies must be installed manually."
       exit 1
@@ -478,9 +486,9 @@ if [ ${BUILD_SMACK} -eq 1 ] ; then
 
   mkdir -p ${SMACK_DIR}/build
   cd ${SMACK_DIR}/build
-  cmake ${CMAKE_INSTALL_PREFIX} -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_BUILD_TYPE=Debug ..
-  make
-  sudo make install
+  cmake ${CMAKE_INSTALL_PREFIX} -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_BUILD_TYPE=Debug .. -G Ninja
+  ninja
+  sudo ninja install
 
   puts "Configuring shell environment"
   echo export BOOGIE=\"mono ${BOOGIE_DIR}/Binaries/Boogie.exe\" >> ${SMACKENV}

bin/versions

@@ -1,10 +1,10 @@
 MONO_VERSION=5.0.0.100
-Z3_SHORT_VERSION=4.8.1
-Z3_FULL_VERSION=4.8.1.016872a5e0f6
-BOOGIE_COMMIT=cd0609f660
-CORRAL_COMMIT=d7d389f22d
+Z3_SHORT_VERSION=4.8.5
+Z3_FULL_VERSION=4.8.5
+BOOGIE_COMMIT=5c829b6340
+CORRAL_COMMIT=c446f5e827
 SYMBOOGLIX_COMMIT=7210e5d09b
 LOCKPWN_COMMIT=73eddf97bd
-LLVM_SHORT_VERSION=3.9
-LLVM_FULL_VERSION=3.9.1
+LLVM_SHORT_VERSION=4.0
+LLVM_FULL_VERSION=4.0.1
 RUST_VERSION=2016-12-16

docs/boogie-code.md

@@ -38,6 +38,33 @@ void assume(bool v) {
 }
 ````
 SMACK interprets the `@` symbol by inserting the value of the C variable `v`.
+Since the arguments of variadic functions may be promoted, SMACK allows users
+to append a format character to the `@` symbol as an indicator that the argument,
+rather than its promoted form, should be used in the format string. We allow the
+following format characters (inspired by Python and C) for the respective C types:
+`c` (`char`), `b` (`signed char`), `B` (`unsigned char`), `h` (`signed short`),
+`H` (`unsigned short`), `i` (`signed int`), `I` (`unsigned int`) and `f`
+(`float`).
+
+For example, without using such annotations, the definition of the `floorf`
+function is:
+```C
+float floorf(float x) {
+  double ret = __VERIFIER_nondet_double();
+  __SMACK_code("@ := ftd($rmode, $round.bvfloat(RTN, dtf($rmode, @)));", ret, x);
+   return ret;
+ }
+```
+where the `ftd` and `dtf` functions are conversions between `float` and `double`
+variables that are needed to deal with the promotion of the arguments.
+Whereas a better definition using these annotations is:
+```C
+float floorf(float x) {
+  float ret = __VERIFIER_nondet_float();
+  __SMACK_code("@f := $round.bvfloat(RTN, @f);", ret, x);
+   return ret;
+ }
+ ```
 
 One application of this functionality which has been valuable to the authors of
 SMACK is in encoding concurrency primitives into the generated Boogie code. The

docs/demos.md

@@ -2,5 +2,6 @@
 
 
 A narrated introduction and demonstration of SMACK can be seen at
-https://youtu.be/SPPSC1KdRzs
+https://youtu.be/SPPSC1KdRzs. Note that the demo is somewhat outdated; for
+example, Duality is no longer supported.