Merge branch 'release-2.8.0' into main

.github/workflows/smack-ci.yaml

@@ -24,6 +24,7 @@ jobs:
             "--exhaustive --folder=c/strings",
             "--exhaustive --folder=c/special",
             "--exhaustive --folder=c/targeted-checks",
+            "--exhaustive --folder=c/unroll",
             "--exhaustive --folder=rust/array --languages=rust",
             "--exhaustive --folder=rust/basic --languages=rust",
             "--exhaustive --folder=rust/box --languages=rust",

CMakeLists.txt

@@ -120,6 +120,7 @@ add_library(smackTranslator STATIC
   include/smack/RewriteBitwiseOps.h
   include/smack/NormalizeLoops.h
   include/smack/RustFixes.h
+  include/smack/AnnotateLoopExits.h
   include/smack/SplitAggregateValue.h
   include/smack/Prelude.h
   include/smack/SmackWarnings.h
@@ -146,6 +147,7 @@ add_library(smackTranslator STATIC
   lib/smack/RewriteBitwiseOps.cpp
   lib/smack/NormalizeLoops.cpp
   lib/smack/RustFixes.cpp
+  lib/smack/AnnotateLoopExits.cpp
   lib/smack/SplitAggregateValue.cpp
   lib/smack/Prelude.cpp
   lib/smack/SmackWarnings.cpp

CONTRIBUTING.md

@@ -8,7 +8,7 @@ items before you start contributing:
   By participating, you are expected to honor this code.
 * We use this [git branching
   model](http://nvie.com/posts/a-successful-git-branching-model/). Please avoid
-  working directly on the `master` branch.
+  working directly on the `main` branch.
 * We follow guidelines for [good git commit
   practice](https://wiki.openstack.org/wiki/GitCommitMessages)
 * We follow the [LLVM Coding

Doxyfile

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

README.md

@@ -1,4 +1,4 @@
-[![master branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=master)](https://github.com/smackers/smack/actions)
+[![main branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=main)](https://github.com/smackers/smack/actions)
 [![develop branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=develop)](https://github.com/smackers/smack/actions)
 
 <img src="docs/smack-logo.png" width=400 alt="SMACK Logo" align="right">

bin/build.sh

@@ -60,6 +60,7 @@ source ${SMACK_DIR}/bin/versions
 
 SMACKENV=${ROOT_DIR}/smack.environment
 WGET="wget --no-verbose"
+Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-glibc-2.31.zip"
 
 # Install prefix -- system default is used if left unspecified
 INSTALL_PREFIX=
@@ -190,30 +191,14 @@ 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_VERSION}/z3-${Z3_VERSION}-x64-debian-8.10.zip"
   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"
-  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"
-  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"
+linux-@(ubuntu|neon)-@(16|18|20)*)
   if [ ${INSTALL_LLVM} -eq 1 ] ; then
     DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
   fi
@@ -489,7 +474,9 @@ if [ ${BUILD_SMACK} -eq 1 ] ; then
 
   mkdir -p ${SMACK_DIR}/build
   cd ${SMACK_DIR}/build
-  cmake ${CMAKE_INSTALL_PREFIX} -DCMAKE_BUILD_TYPE=Debug .. -G Ninja
+  cmake -DCMAKE_CXX_COMPILER=clang++-${LLVM_SHORT_VERSION} \
+        -DCMAKE_C_COMPILER=clang-${LLVM_SHORT_VERSION} ${CMAKE_INSTALL_PREFIX} \
+        -DCMAKE_BUILD_TYPE=Debug .. -G Ninja
   ninja
 
   if [ -n "${CMAKE_INSTALL_PREFIX}" ] ; then

bin/versions

@@ -1,10 +1,10 @@
-Z3_VERSION="4.8.10"
+Z3_VERSION="4.8.12"
 CVC4_VERSION="1.8"
 YICES2_VERSION="2.6.2"
-BOOGIE_VERSION="2.9.1"
+BOOGIE_VERSION="2.9.6"
 CORRAL_VERSION="1.1.8"
 SYMBOOGLIX_COMMIT="ccb2e7f2b3"
 LOCKPWN_COMMIT="12ba58f1ec"
-LLVM_SHORT_VERSION="11"
-LLVM_FULL_VERSION="11.1.0"
+LLVM_SHORT_VERSION="12"
+LLVM_FULL_VERSION="12.0.1"
 RUST_VERSION="nightly-2021-03-01"

docs/installation.md

@@ -51,7 +51,7 @@ the following configurations:
 SMACK's Docker container images can be pulled from Docker Hub directly:
 
 ```shell
-docker pull smackers/smack:stable # built from the master branch
+docker pull smackers/smack:stable # built from the main branch
 docker pull smackers/smack:latest # built from the develop branch
 ```
 
@@ -74,16 +74,16 @@ to Docker's official documentation.
 
 SMACK depends on the following projects:
 
-* [LLVM][] version [11.1.0][LLVM-11.1.0]
-* [Clang][] version [11.1.0][Clang-11.1.0]
+* [LLVM][] version [12.0.1][LLVM-12.0.1]
+* [Clang][] version [12.0.1][Clang-12.0.1]
 * [Boost][] version 1.55 or greater
 * [Python][] version 3.6.8 or greater
 * [Ninja][] version 1.5.1 or greater
 * [Z3][] or compatible SMT-format theorem prover
 * [Boogie][] or [Corral][] or compatible Boogie-format verifier
 * [sea-dsa][]
 
-See [here](https://github.com/smackers/smack/blob/master/bin/versions) for
+See [here](https://github.com/smackers/smack/blob/main/bin/versions) for
 compatible version numbers of [Boogie][] and [Corral][]. See the appropriate
 installation instructions below for installing these requirements.
 
@@ -189,16 +189,16 @@ shell in the `test` directory by executing
 [CMake]: http://www.cmake.org
 [Python]: http://www.python.org
 [LLVM]: http://llvm.org
-[LLVM-11.1.0]: http://llvm.org/releases/download.html#11.1.0
+[LLVM-12.0.1]: http://llvm.org/releases/download.html#12.0.1
 [Clang]: http://clang.llvm.org
-[Clang-11.1.0]: http://llvm.org/releases/download.html#11.1.0
+[Clang-12.0.1]: http://llvm.org/releases/download.html#12.0.1
 [Boogie]: https://github.com/boogie-org/boogie
 [Corral]: https://github.com/boogie-org/corral
 [Z3]: https://github.com/Z3Prover/z3/
 [Mono]: http://www.mono-project.com/
 [Cygwin]: https://www.cygwin.com
 [.NET]: https://msdn.microsoft.com/en-us/vstudio/aa496123.aspx
-[build.sh]: https://github.com/smackers/smack/blob/master/bin/build.sh
+[build.sh]: https://github.com/smackers/smack/blob/main/bin/build.sh
 [Xcode]: https://developer.apple.com/xcode/
 [Homebrew]: http://brew.sh/
 [Homebrew Cask]: https://formulae.brew.sh/cask/

include/smack/AnnotateLoopExits.h

@@ -0,0 +1,29 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+#ifndef ANNOTATELOOPEXITS_H
+#define ANNOTATELOOPEXITS_H
+
+#include "llvm/IR/Function.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/Module.h"
+#include "llvm/Pass.h"
+#include <map>
+
+namespace smack {
+
+class AnnotateLoopExits : public llvm::FunctionPass {
+private:
+  llvm::Function *LoopExitFunction;
+
+public:
+  static char ID; // Pass identification, replacement for typeid
+  AnnotateLoopExits() : llvm::FunctionPass(ID) {}
+  bool doInitialization(llvm::Module &M) override;
+  virtual llvm::StringRef getPassName() const override;
+  virtual bool runOnFunction(llvm::Function &F) override;
+  virtual void getAnalysisUsage(llvm::AnalysisUsage &) const override;
+};
+} // namespace smack
+
+#endif // ANNOTATELOOPEXITS_H