Skip to content

Commit

Permalink
Merge branch 'release-2.7.1'
Browse files Browse the repository at this point in the history
  • Loading branch information
zvonimir committed Sep 8, 2021
2 parents 6504b33 + 820acd9 commit 466dabf
Show file tree
Hide file tree
Showing 563 changed files with 1,336 additions and 367 deletions.
2 changes: 2 additions & 0 deletions .github/workflows/smack-ci.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand All @@ -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"
Expand Down
18 changes: 18 additions & 0 deletions CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Doxyfile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
5 changes: 1 addition & 4 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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://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
Expand Down
71 changes: 43 additions & 28 deletions bin/build.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
;;

*)
Expand All @@ -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
;;
Expand Down Expand Up @@ -268,8 +278,10 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] ; then
fi

# Adding LLVM repository
${WGET} -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
sudo add-apt-repository "deb http://apt.llvm.org/${UBUNTU_CODENAME}/ llvm-toolchain-${UBUNTU_CODENAME}-${LLVM_SHORT_VERSION} main"
if [ ${INSTALL_LLVM} -eq 1 ] ; then
${WGET} -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
sudo add-apt-repository "deb http://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
Expand Down Expand Up @@ -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"
Expand Down
4 changes: 2 additions & 2 deletions bin/versions
Original file line number Diff line number Diff line change
@@ -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"
Expand Down
90 changes: 0 additions & 90 deletions bin/vsmack

This file was deleted.

40 changes: 4 additions & 36 deletions docs/installation.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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][]
Expand Down Expand Up @@ -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
Expand All @@ -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][]).
Expand Down
Loading

0 comments on commit 466dabf

Please sign in to comment.