Merge branch 'release-2.7.1'

.github/workflows/smack-ci.yaml

@@ -23,6 +23,7 @@ jobs:
  "--exhaustive --folder=c/pthread_extras",
  "--exhaustive --folder=c/strings",
  "--exhaustive --folder=c/special",
+ "--exhaustive --folder=c/targeted-checks",
  "--exhaustive --folder=rust/array --languages=rust",
  "--exhaustive --folder=rust/basic --languages=rust",
  "--exhaustive --folder=rust/box --languages=rust",
@@ -32,6 +33,7 @@ jobs:
  "--exhaustive --folder=rust/panic --languages=rust",
  "--exhaustive --folder=rust/recursion --languages=rust",
  "--exhaustive --folder=rust/structures --languages=rust",
+ "--exhaustive --folder=rust/targeted-checks",
  "--exhaustive --folder=rust/vector --languages=rust",
  "--exhaustive --folder=rust/cargo/** --languages=cargo --threads=1",
  "--exhaustive --folder=llvm --languages=llvm-ir"

CMakeLists.txt

@@ -155,6 +155,15 @@ add_executable(llvm2bpl
  tools/llvm2bpl/llvm2bpl.cpp
 )
 
+add_library(externalizePass STATIC
+ tools/externalizer/ExternalizePass.h
+ tools/externalizer/ExternalizePass.cpp
+)
+
+add_executable(extern-statics
+ tools/externalizer/extern-statics.cpp
+)
+
 # We need to include Boost header files at least for macOS
 find_package(Boost 1.55)
 if(Boost_FOUND)
@@ -182,10 +191,18 @@ target_link_libraries(smackTranslator ${LLVM_LIBS} ${LLVM_SYSTEM_LIBS}
  ${LLVM_LDFLAGS})
 target_link_libraries(llvm2bpl smackTranslator utils SeaDsaAnalysis)
 
+target_link_libraries(externalizePass ${LLVM_LIBS} ${LLVM_SYSTEM_LIBS}
+ ${LLVM_LDFLAGS})
+target_link_libraries(extern-statics externalizePass)
+
 install(TARGETS llvm2bpl
  RUNTIME DESTINATION bin
 )
 
+install(TARGETS extern-statics
+ RUNTIME DESTINATION bin
+)
+
 install(FILES
  ${CMAKE_CURRENT_SOURCE_DIR}/bin/smack
  ${CMAKE_CURRENT_SOURCE_DIR}/bin/smack-doctor
@@ -200,6 +217,7 @@ install(DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/share/smack
  USE_SOURCE_PERMISSIONS
  FILES_MATCHING PATTERN "*.py" PATTERN "*.h" PATTERN "*.c" PATTERN "Makefile"
  PATTERN "*.rs" PATTERN "*.f90" PATTERN "*.di" PATTERN "*.toml"
+ PATTERN "*.cpp" PATTERN "cassert"
 )
 
 install(FILES

Doxyfile

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

README.md

@@ -39,10 +39,7 @@ See below for system requirements, installation, usage, and everything else.
 * As a last resort, send mail to 
  [Michael](mailto:[email protected]), [Zvonimir](mailto:[email protected]), or both.
 
-* To stay informed about updates, you can either watch SMACK's Github page,
- or you can join [SMACK's Google Group](http:https://groups.google.com/group/smack-dev)
- mailing list. Even without a Google account, you may join by sending mail to
- [[email protected]](mailto:[email protected]).
+* To stay informed about updates, you can watch SMACK's Github page.
 
 
 ### Acknowledgements

bin/build.sh

@@ -22,21 +22,22 @@
 ################################################################################
 
 # Set these flags to control various installation options
-INSTALL_DEPENDENCIES=1
-INSTALL_MONO=0 # Mono is needed only for lockpwn and symbooglix
-INSTALL_Z3=1
-INSTALL_CVC4=0
-INSTALL_YICES2=0
-INSTALL_BOOGIE=1
-INSTALL_CORRAL=1
-BUILD_SYMBOOGLIX=0
-BUILD_LOCKPWN=0
-BUILD_SMACK=1
-TEST_SMACK=1
-BUILD_LLVM=0 # LLVM is typically installed from packages (see below)
+INSTALL_DEPENDENCIES=${INSTALL_DEPENDENCIES:-1}
+INSTALL_MONO=${INSTALL_MONO:-0} # Mono is needed only for lockpwn and symbooglix
+INSTALL_Z3=${INSTALL_Z3:-1}
+INSTALL_CVC4=${INSTALL_CVC4:-0}
+INSTALL_YICES2=${INSTALL_YICES2:-0}
+INSTALL_BOOGIE=${INSTALL_BOOGIE:-1}
+INSTALL_CORRAL=${INSTALL_CORRAL:-1}
+BUILD_SYMBOOGLIX=${BUILD_SYMBOOGLIX:-0}
+BUILD_LOCKPWN=${BUILD_LOCKPWN:-0}
+BUILD_SMACK=${BUILD_SMACK:-1}
+TEST_SMACK=${TEST_SMACK:-1}
+INSTALL_LLVM=${INSTALL_LLVM:-1}
+BUILD_LLVM=${BUILD_LLVM:-0} # LLVM is typically installed from packages (see below)
 
 # Support for more programming languages
-INSTALL_OBJECTIVEC=0
+INSTALL_OBJECTIVEC=${INSTALL_OBJECTIVEC:-0}
 INSTALL_RUST=${INSTALL_RUST:-0}
 
 # Development dependencies
@@ -66,7 +67,7 @@ CONFIGURE_INSTALL_PREFIX=
 CMAKE_INSTALL_PREFIX=
 
 # Partial list of dependencies; the rest are added depending on the platform
-DEPENDENCIES="git cmake python3-yaml python3-psutil python3-toml unzip wget ninja-build apt-transport-https dotnet-sdk-3.1 libboost-all-dev"
+DEPENDENCIES="git cmake python3-yaml python3-psutil python3-toml unzip wget ninja-build apt-transport-https dotnet-sdk-5.0 libboost-all-dev"
 
 shopt -s extglob
 
@@ -190,23 +191,32 @@ puts "Detected distribution: $distro"
 case "$distro" in
 linux-opensuse*)
  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-debian-8.10.zip"
- DEPENDENCIES+=" llvm-clang llvm-devel gcc-c++ make"
+ if [ ${INSTALL_LLVM} -eq 1 ] ; then
+ DEPENDENCIES+=" llvm-clang llvm-devel"
+ fi
+ DEPENDENCIES+=" gcc-c++ make"
  DEPENDENCIES+=" ncurses-devel"
  ;;
 
 linux-@(ubuntu|neon)-16*)
  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-18.04.zip"
- DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
+ if [ ${INSTALL_LLVM} -eq 1 ] ; then
+ DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
+ fi
  ;;
 
 linux-@(ubuntu|neon)-18*)
  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-18.04.zip"
- DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
+ if [ ${INSTALL_LLVM} -eq 1 ] ; then
+ DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
+ fi
  ;;
 
 linux-@(ubuntu|neon)-20*)
  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-18.04.zip"
- DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
+ if [ ${INSTALL_LLVM} -eq 1 ] ; then
+ DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
+ fi
  ;;
 
 *)
@@ -224,7 +234,7 @@ do
  INSTALL_PREFIX="${2%/}"
  CONFIGURE_INSTALL_PREFIX="--prefix=$2"
  CMAKE_INSTALL_PREFIX="-DCMAKE_INSTALL_PREFIX=$2"
- echo export PATH=${INSTALL_PREFIX}/bin:$PATH >> ${SMACKENV}
+ echo export PATH=\"${INSTALL_PREFIX}/bin:\$PATH\" >> ${SMACKENV}
  shift
  shift
  ;;
@@ -268,8 +278,10 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] ; then
  fi
 
  # Adding LLVM repository
- ${WGET} -O - http:https://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
- sudo add-apt-repository "deb http:https://apt.llvm.org/${UBUNTU_CODENAME}/ llvm-toolchain-${UBUNTU_CODENAME}-${LLVM_SHORT_VERSION} main"
+ if [ ${INSTALL_LLVM} -eq 1 ] ; then
+ ${WGET} -O - http:https://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
+ sudo add-apt-repository "deb http:https://apt.llvm.org/${UBUNTU_CODENAME}/ llvm-toolchain-${UBUNTU_CODENAME}-${LLVM_SHORT_VERSION} main"
+ fi
 
  # Adding .NET repository
  ${WGET} -q https://packages.microsoft.com/config/ubuntu/${RELEASE_VERSION}/packages-microsoft-prod.deb -O packages-microsoft-prod.deb
@@ -375,14 +387,17 @@ fi
 if [ ${INSTALL_YICES2} -eq 1 ] ; then
  if [ ! -d "$YICES2_DIR" ] ; then
  puts "Installing Yices2"
- mkdir -p ${YICES2_DIR}
- ${WGET} https://yices.csl.sri.com/releases/${YICES2_VERSION}/yices-${YICES2_VERSION}-x86_64-pc-linux-gnu-static-gmp.tar.gz -O yices2-downloaded.tgz
- tar xf yices2-downloaded.tgz
- cd yices-${YICES2_VERSION}
- ./install-yices ${YICES2_DIR}
- cd ..
- rm -rf yices2-downloaded.tgz yices-${YICES2_VERSION}
+ sudo apt-get install -y gperf libgmp-dev
+ cd ${DEPS_DIR}
+ git clone -b Yices-${YICES2_VERSION} https://github.com/SRI-CSL/yices2 yices2-src
+ cd yices2-src
+ autoconf
+ ./configure --prefix=${YICES2_DIR}
+ make -j
+ make install
  ln -s ${YICES2_DIR}/bin/yices-smt2 ${YICES2_DIR}/bin/yices2
+ cd ${DEPS_DIR}
+ rm -rf yices2-src
  puts "Installed Yices2"
  else
  puts "Yices2 already installed"

bin/versions

@@ -1,8 +1,8 @@
 Z3_VERSION="4.8.10"
 CVC4_VERSION="1.8"
 YICES2_VERSION="2.6.2"
-BOOGIE_VERSION="2.8.26"
-CORRAL_VERSION="1.0.17"
+BOOGIE_VERSION="2.9.1"
+CORRAL_VERSION="1.1.8"
 SYMBOOGLIX_COMMIT="ccb2e7f2b3"
 LOCKPWN_COMMIT="12ba58f1ec"
 LLVM_SHORT_VERSION="11"

docs/installation.md

@@ -3,29 +3,12 @@
 
 In principle SMACK can be run on any platform on which [LLVM][] and [Boogie][]
 can run. In practice we have run SMACK on standard Ubuntu and openSUSE Linux
-distributions, OS X, and Windows via Cygwin. Below we outline system
+distributions, OS X, and Windows. Below we outline system
 requirements and installation instructions for typical system configurations.
 A quick way to get started without worrying about system requirements and
 installation, however, is to launch our reproducible and portable development
 environment using [Vagrant][]. An even quicker way to get started is to use
-our prepackaged Vagrant box.
-
-### Super-Quick Setup: Virtual Smack
-
-Just download [vsmack](bin/vsmack) and put it in your executable path, ensure
-[Vagrant][] and [VirtualBox][] are installed, and run `vsmack` directly on
-your source files. For example,
-````Shell
-# fetch vsmack and set executable permission
-wget -O ~/bin/vsmack https://raw.githubusercontent.com/smackers/smack/develop/bin/vsmack
-chmod u+x ~/bin/vsmack
-
-# fetch a source file
-wget https://raw.githubusercontent.com/smackers/smack/develop/test/basic/simple.c
-
-# run vsmack
-vsmack simple.c
-````
+our prepackaged Docker container.
 
 ### Quick Setup 1: Vagrant Development Environment
 
@@ -56,13 +39,13 @@ vagrant destroy
 ````
 
 ### Quick Setup 2: Docker
+
 SMACK can also be run in a [Docker][] container. We tested the Dockerfile on
 the following configurations:
 
 * Ubuntu 18.04, Docker version 19.03.6
 * Windows WSL Ubuntu 20.04, Docker Desktop with Docker engine version 20.10.2
 
-
 #### Docker Hub
 
 SMACK's Docker container images can be pulled from Docker Hub directly:
@@ -96,7 +79,6 @@ SMACK depends on the following projects:
 * [Boost][] version 1.55 or greater
 * [Python][] version 3.6.8 or greater
 * [Ninja][] version 1.5.1 or greater
-* [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
 * [sea-dsa][]
@@ -134,7 +116,7 @@ script. Alternatively, you can read how to accomplish this below.
 
 The general instructions for installation on OS X mainly follow those above for
 Linux, and are outlined in our automated [build.sh][] script in `bin/build.sh`.
-Note however that `bin/build.sh` does not run on OS X . it can only be used as
+Note however that `bin/build.sh` does not run on OS X . It can only be used as
 reference guidelines.
 
 In addition to the requirements above, installing SMACK and its dependencies
@@ -144,20 +126,6 @@ the [Homebrew][] package manager. [Mono][] can be installed from binaries
 either from the [Mono][] download page, or via [Homebrew Cask][].
 
 ### Installation on Windows
-#### Cygwin (Deprecated)
-
-The general instructions for installation on Windows using [Cygwin][] mainly
-follow those above for Linux, and are outlined in our automated [build.sh][]
-script in `bin/build.sh`. Note however that an actual [.NET][] Framework and
-SDK should be present in place of the [Mono][] emulator, and that prebuilt
-[Z3][], [Boogie][], and [Corral][] may be installed via their Windows
-installers rather than built from source.
-
-**NOTE** Although we have not pinpointed the problem exactly, building [LLVM][]
-and [Clang][] is problematic on some [Cygwin][] configurations. Please consult
-[LLVM][] documentation in case of any issues.
-
-#### Windows Subsystem for Linux (Recommended)
 
 SMACK can be installed on the Windows Subsystem for Linux (WSL) by following the
 same procedure as the Linux installation (i.e., via the build script [build.sh][]).