diff options
33 files changed, 1229 insertions, 496 deletions
diff --git a/.dockerignore b/.dockerignore index 8feca832..11d13733 100644 --- a/.dockerignore +++ b/.dockerignore @@ -1,4 +1,4 @@ -.git +#.git - Don't delete git, we need that to generate the correct version number autom4te.cache **/.*.swp Dockerfile diff --git a/.travis.yml b/.travis.yml index 5a8a6e45..c8de1292 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,6 +1,8 @@ sudo: required dist: trusty language: cpp +services: + - docker compiler: # FIXME: For now, building with Clang is disabled because the STP built with # it hits an assertion failure during some tests. We should sort this out @@ -32,25 +34,25 @@ env: # COVERAGE: {0, 1} # USE_TCMALLOC: {0, 1} - # COVERAGE when set indicates that coverage data should be uploaded to the service, only ONE job should have COVERAGE set + # COVERAGE when set indicates that coverage data should be uploaded to the service matrix: # TODO: Add Doxygen build # Check newer LLVMs - - LLVM_VERSION=3.7 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 - - LLVM_VERSION=3.6 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 - - LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 - - - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 - - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 + - LLVM_VERSION=3.7 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 + - LLVM_VERSION=3.6 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 + - LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 + - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 + - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 REQUIRES_RTTI=1 # ASan build. Do unoptimized build otherwise the optimizer might remove problematic code - - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_TCMALLOC=0 ASAN_BUILD=1 + - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_TCMALLOC=0 SANITIZER_BUILD=address + - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_TCMALLOC=0 SANITIZER_BUILD=undefined # Test just using Z3 - - LLVM_VERSION=3.4 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 SOLVERS=Z3 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 # Test we can build against STP master - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 @@ -59,7 +61,7 @@ env: - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 # Test metaSMT support - - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=BTOR KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=BTOR KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 REQUIRES_RTTI=1 # Check at least one build with Asserts disabled. - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0 @@ -71,78 +73,38 @@ env: - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 # Coverage build - - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=1 USE_TCMALLOC=0 + - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=1 USE_TCMALLOC=0 global: - secure: EF/WAc4BdIRUchF3mjATN3/UwtGWtGaRgb5oIIJHjKhgZFdPsgWsXFgaOB0jaK2hfO/svj/LvlasuRIGxeePVjeaiX8ZlVpuHiX67vdYLY+0kCDRwkusRjm60/GbPU9O/Xjgb/d4aWAEkoq5OnsprVTEvU8iY2JHtAqgwR+wW9I= - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw= - secure: DQAEQWJblXvIztN/sgH63OtFncI+Qju6wRy1zIV/iLf5KbAmLs1h3itU7EsE/+3+LgV1MVQ5QNJDBUj17A6VHRKNaQ5qnIllTAcC3o0nPDohQkQoCgDG8HZ+M4wtVfr7q2K6byEPB2UbSH+mEjSMTihJufgBBVfKyyozAfYycjg= + - KLEE_TRAVIS_BUILD: 1 + - REPOSITORY: klee matrix: include: - os: osx osx_image: xcode8.3 - env: LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=0 - -addons: - apt: - sources: - - sourceline: 'ppa:ubuntu-toolchain-r/test' - - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.4 main' - key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key' - - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.5 main' - key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key' - - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.6 main' - key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key' - - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.7 main' - key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key' - - sourceline: 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_14.04/ /' - key_url: 'http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_14.04/Release.key' - packages: - - gcc-4.8 - - g++-4.8 - - libboost-program-options-dev - - libcap-dev - - libedit-dev - - libselinux1-dev - - cmake - - lcov + env: LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=0 cache: ccache: true apt: true directories: - $HOME/Library/Caches/Homebrew + before_install: ########################################################################### # Set up the locations to get various packages from # We assume the Travis image uses Ubuntu 14.04 LTS ########################################################################### # Update package information - - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then sudo apt-get update; fi - - if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then brew update && brew tap klee/klee && brew install ccache && export PATH="/usr/local/opt/ccache/libexec:$PATH" ; fi - ########################################################################### - # Set up out of source build directory - ########################################################################### - export KLEE_SRC=`pwd` + - export KLEE_SRC_TRAVIS=`pwd` - cd ../ - - mkdir build - - cd build/ - - export BUILD_DIR=`pwd` - ########################################################################### - # Install stuff - ########################################################################### - # Install LLVM and the LLVM bitcode compiler we require to build KLEE - - ${KLEE_SRC}/.travis/install-llvm-and-runtime-compiler.sh - - ${KLEE_SRC}/.travis/install-tcmalloc.sh - # Install lit (llvm-lit is not available) - - sudo pip2 install lit - # Get SMT solvers - - ${KLEE_SRC}/.travis/solvers.sh - # Get needed utlities/libraries for testing KLEE - - mkdir test-utils/ - - cd test-utils/ - - ${KLEE_SRC}/.travis/testing-utils.sh - - cd ../ + - export BASE=`pwd` + - ${KLEE_SRC_TRAVIS}/scripts/build/build-travis.sh script: # Build KLEE and run tests - - ${KLEE_SRC}/.travis/klee.sh + - if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then export PATH="/usr/local/opt/ccache/libexec:$PATH"; ${KLEE_SRC_TRAVIS}/scripts/build/klee.sh; fi + - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then ${KLEE_SRC_TRAVIS}/scripts/build/build-docker.sh; fi diff --git a/.travis/install-llvm-and-runtime-compiler.sh b/.travis/install-llvm-and-runtime-compiler.sh deleted file mode 100755 index bd34d843..00000000 --- a/.travis/install-llvm-and-runtime-compiler.sh +++ /dev/null @@ -1,27 +0,0 @@ -#!/bin/bash -x -set -ev - -if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - sudo apt-get install -y llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev - - sudo apt-get install -y llvm-${LLVM_VERSION}-tools clang-${LLVM_VERSION} - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_VERSION} 20 - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-${LLVM_VERSION} 20 -elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then - # We use our own local cache if possible - set +e - brew install $HOME/Library/Caches/Homebrew/llvm\@${LLVM_VERSION}*.bottle.tar.gz - RES=$? - set -ev - if [ ${RES} -ne 0 ]; then - # This might build the llvm package use a time out to avoid dumping log information - brew install -v --build-bottle "llvm@${LLVM_VERSION}" - # Now bottle the brew - brew bottle llvm\@${LLVM_VERSION} - # Not make sure it's cached - cp llvm\@${LLVM_VERSION}*.bottle.tar.gz $HOME/Library/Caches/Homebrew/ - fi -else - echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" - exit 1 -fi diff --git a/.travis/install-tcmalloc.sh b/.travis/install-tcmalloc.sh deleted file mode 100755 index 0bc26616..00000000 --- a/.travis/install-tcmalloc.sh +++ /dev/null @@ -1,22 +0,0 @@ -#!/bin/bash -x -set -ev - -if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then - # Get tcmalloc release - wget https://github.com/gperftools/gperftools/releases/download/gperftools-2.4/gperftools-2.4.tar.gz - tar xfz gperftools-2.4.tar.gz - cd gperftools-2.4 - ./configure --disable-dependency-tracking --disable-cpu-profiler --disable-heap-checker --disable-debugalloc --enable-minimal --prefix=/usr - make - sudo make install - fi -elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then - if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then - echo "Error: Requested to install TCMalloc on macOS, which is not supported" - exit 1 - fi -else - echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" - exit 1 -fi diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh deleted file mode 100755 index 5d5b669e..00000000 --- a/.travis/metaSMT.sh +++ /dev/null @@ -1,49 +0,0 @@ -#!/bin/bash -x - -set -e - -: ${METASMT_VERSION?"METASMT_VERSION not specified"} - -# Get Z3, libgmp, gperf (required by yices2) -sudo apt-get -y install libz3 libz3-dev libgmp-dev gperf - -# Get Boost -if [ "X${METASMT_BOOST_VERSION}" != "X" ]; then - # Taken from boost/hana/.travis.yml - BOOST_URL="http://sourceforge.net/projects/boost/files/boost/${METASMT_BOOST_VERSION}/boost_${METASMT_BOOST_VERSION//\./_}.tar.gz" - BOOST_DIR=`pwd`/boost-${METASMT_BOOST_VERSION} - mkdir -p ${BOOST_DIR} - wget --quiet -O - ${BOOST_URL} | tar --strip-components=1 -xz -C ${BOOST_DIR} - sudo ln -s ${BOOST_DIR}/boost /usr/include/boost -else - sudo apt-get -y install libboost1.55-dev -fi - -# Get CVC4 -wget http://www.informatik.uni-bremen.de/agra/systemc-verification/media/snapshots/cvc4-594301e.tar.gz -tar -xf cvc4-594301e.tar.gz -sudo mv cvc4 /usr - -# Clone -git clone -b ${METASMT_VERSION} --single-branch --depth 1 https://github.com/hoangmle/metaSMT.git -cd metaSMT -git submodule update --init - -source ${KLEE_SRC}/.travis/sanitizer_flags.sh -if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then - echo "Error: Requested Sanitized build but sanitized build of metaSMT is not implemented" - exit 1 -fi - -# Bootstrap -export BOOST_ROOT=/usr -sudo cp dependencies/Z3-2.19/Z3Config.cmake /usr # this is a hack -./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off --build stp-git-basic --build boolector-2.2.0 --build minisat-git --build lingeling-ayv-86bf266-140429 --build yices-2.5.1 -DZ3_DIR=/usr -DCVC4_DIR=/usr/cvc4 -sudo cp deps/boolector-2.2.0/lib/* /usr/lib/ # -sudo cp deps/lingeling-ayv-86bf266-140429/lib/* /usr/lib/ # -sudo cp deps/minisat-git/lib/* /usr/lib/ # hack -sudo cp -r deps/stp-git-basic/lib/lib* /usr/lib/ # -sudo cp deps/yices-2.5.1/lib/* /usr/lib/ # - -# Build -make -C build install diff --git a/.travis/sanitizer_flags.sh b/.travis/sanitizer_flags.sh deleted file mode 100644 index 4d3dce2c..00000000 --- a/.travis/sanitizer_flags.sh +++ /dev/null @@ -1,39 +0,0 @@ -# This file is meant to be included by shell scripts -# that need to do a sanitized build. - -# Users of this script can use this variable -# to detect if a Sanitized build was enabled. -IS_SANITIZED_BUILD=0 - -# AddressSanitizer -if [ "X${ASAN_BUILD}" == "X1" ]; then - echo "Using ASan" - ASAN_CXX_FLAGS="-fsanitize=address -fno-omit-frame-pointer" - ASAN_C_FLAGS="${ASAN_CXX_FLAGS}" - ASAN_LD_FLAGS="${ASAN_CXX_FLAGS}" - IS_SANITIZED_BUILD=1 -else - echo "Not using ASan" - ASAN_CXX_FLAGS="" - ASAN_C_FLAGS="" - ASAN_LD_FLAGS="" -fi - -# Undefined Behaviour Sanitizer -if [ "X${UBSAN_BUILD}" == "X1" ]; then - echo "Using UBSan" - UBSAN_CXX_FLAGS="-fsanitize=undefined" - UBSAN_C_FLAGS="${UBSAN_CXX_FLAGS}" - UBSAN_LD_FLAGS="${UBSAN_CXX_FLAGS}" - IS_SANITIZED_BUILD=1 -else - echo "Not using UBSan" - UBSAN_CXX_FLAGS="" - UBSAN_C_FLAGS="" - UBSAN_LD_FLAGS="" -fi - -# Set variables to be used by clients. -SANITIZER_CXX_FLAGS="${ASAN_CXX_FLAGS} ${UBSAN_CXX_FLAGS}" -SANITIZER_C_FLAGS="${ASAN_C_FLAGS} ${UBSAN_C_FLAGS}" -SANITIZER_LD_FLAGS="${ASAN_LD_FLAGS} ${UBSAN_LD_FLAGS}" diff --git a/.travis/stp.sh b/.travis/stp.sh deleted file mode 100755 index e8647839..00000000 --- a/.travis/stp.sh +++ /dev/null @@ -1,72 +0,0 @@ -#!/bin/bash -x - -# TODO: For OSX we can prepare bottled formulas for STP and minisat - -# Make sure we exit if there is a failure -set -e - -STP_LOG="$(pwd)/stp-build.log" - -if [ "x${STP_VERSION}" != "x" ]; then - # Get Sanitizer flags - source ${KLEE_SRC}/.travis/sanitizer_flags.sh - - # Build minisat - git clone https://github.com/stp/minisat - cd minisat - mkdir build - cd build - MINISAT_DIR=`pwd` - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - CFLAGS="${SANITIZER_C_FLAGS}" \ - CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ - cmake -DCMAKE_INSTALL_PREFIX=/usr .. - elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then - CFLAGS="${SANITIZER_C_FLAGS}" \ - CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ - cmake -DCMAKE_INSTALL_PREFIX=/usr/local .. - else - echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" - exit 1 - fi - make - sudo make install - cd ../../ - - # Determine STP build flags - if [ "X${STP_VERSION}" = "Xmaster" ]; then - # 5e9ca6339a2b3b000aa7a90c18601fdcf1212fe1 Silently BUILD_SHARED_LIBS removed. STATICCOMPILE does something similar - STP_CMAKE_FLAGS=( \ - "-DENABLE_PYTHON_INTERFACE:BOOL=OFF" \ - "-DSTATICCOMPILE:BOOL=ON" \ - ) - else - STP_CMAKE_FLAGS=( \ - "-DENABLE_PYTHON_INTERFACE:BOOL=OFF" \ - "-DBUILD_SHARED_LIBS:BOOL=OFF" \ - ) - fi - - # Build STP - git clone --depth 1 -b "${STP_VERSION}" git://github.com/stp/stp.git src - mkdir build - cd build - # Disabling building of shared libs is a workaround. - # Don't build against boost because that is broken when mixing packaged boost libraries and gcc 4.8 - CFLAGS="${SANITIZER_C_FLAGS}" \ - CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ - cmake "${STP_CMAKE_FLAGS[@]}" ../src - - set +e # Do not exit if build fails because we need to display the log - make >> "${STP_LOG}" 2>&1 -else - echo "No STP_VERSION given or empty" - exit 1 -fi - -# Only show build output if something went wrong to keep log output short -if [ $? -ne 0 ]; then - echo "Build error" - cat "${STP_LOG}" - exit 1 -fi diff --git a/.travis/testing-utils.sh b/.travis/testing-utils.sh deleted file mode 100755 index eefccdd2..00000000 --- a/.travis/testing-utils.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/bash -x -# Make sure we exit if there is a failure -set -e - -# The New CMake build system just needs the GTest sources regardless -# of LLVM version. -wget https://github.com/google/googletest/archive/release-1.7.0.zip -unzip release-1.7.0.zip -exit 0 diff --git a/.travis/z3.sh b/.travis/z3.sh deleted file mode 100755 index 315d028c..00000000 --- a/.travis/z3.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/bin/bash -x - -# Make sure we exit if there is a failure -set -e - -source ${KLEE_SRC}/.travis/sanitizer_flags.sh -if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then - echo "Error: Requested Sanitized build but Z3 being used is not sanitized" - exit 1 -fi - -if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - # Should we install libz3-dbg too? - sudo apt-get -y install libz3 libz3-dev -elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then - set +e - brew install python@2 - if [[ "X$?" != "X0" ]]; then - brew link --overwrite python@2 - fi - set -e - brew install z3 -else - echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" - exit 1 -fi diff --git a/Dockerfile b/Dockerfile deleted file mode 100644 index 7d23dc7f..00000000 --- a/Dockerfile +++ /dev/null @@ -1,101 +0,0 @@ -FROM ubuntu:14.04 -MAINTAINER Dan Liew <daniel.liew@imperial.ac.uk> - -# FIXME: Docker doesn't currently offer a way to -# squash the layers from within a Dockerfile so -# the resulting image is unnecessarily large! - -ENV LLVM_VERSION=3.4 \ - SOLVERS=STP:Z3 \ - STP_VERSION=2.1.2 \ - DISABLE_ASSERTIONS=0 \ - ENABLE_OPTIMIZED=1 \ - KLEE_UCLIBC=klee_uclibc_v1.0.0 \ - KLEE_SRC=/home/klee/klee_src \ - COVERAGE=0 \ - BUILD_DIR=/home/klee/klee_build \ - ASAN_BUILD=0 \ - UBSAN_BUILD=0 \ - TRAVIS_OS_NAME=linux - -RUN apt-get update && \ - apt-get -y --no-install-recommends install \ - clang-${LLVM_VERSION} \ - llvm-${LLVM_VERSION} \ - llvm-${LLVM_VERSION}-dev \ - llvm-${LLVM_VERSION}-runtime \ - llvm \ - libcap-dev \ - git \ - subversion \ - cmake \ - make \ - libboost-program-options-dev \ - python3 \ - python3-dev \ - python3-pip \ - perl \ - flex \ - bison \ - libncurses-dev \ - zlib1g-dev \ - patch \ - wget \ - unzip \ - binutils && \ - pip3 install -U lit tabulate wllvm && \ - update-alternatives --install /usr/bin/python python /usr/bin/python3 50 && \ - ( wget -O - http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_14.04/Release.key | apt-key add - ) && \ - echo 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_14.04/ /' >> /etc/apt/sources.list.d/z3.list && \ - apt-get update - -# Create ``klee`` user for container with password ``klee``. -# and give it password-less sudo access (temporarily so we can use the TravisCI scripts) -RUN useradd -m klee && \ - echo klee:klee | chpasswd && \ - cp /etc/sudoers /etc/sudoers.bak && \ - echo 'klee ALL=(root) NOPASSWD: ALL' >> /etc/sudoers -USER klee -WORKDIR /home/klee - -# Copy across source files needed for build -RUN mkdir ${KLEE_SRC} -ADD / ${KLEE_SRC} - -# Set klee user to be owner -RUN sudo chown --recursive klee: ${KLEE_SRC} - -# Create build directory -RUN mkdir -p ${BUILD_DIR} - -# Build/Install SMT solvers (use TravisCI script) -RUN cd ${BUILD_DIR} && ${KLEE_SRC}/.travis/solvers.sh - -# Install testing utils (use TravisCI script) -RUN cd ${BUILD_DIR} && mkdir test-utils && cd test-utils && \ - ${KLEE_SRC}/.travis/testing-utils.sh - -# FIXME: The current TravisCI script expects clang-${LLVM_VERSION} to exist -RUN sudo ln -s /usr/bin/clang /usr/bin/clang-${LLVM_VERSION} && \ - sudo ln -s /usr/bin/clang++ /usr/bin/clang++-${LLVM_VERSION} - -# Build KLEE (use TravisCI script) -RUN cd ${BUILD_DIR} && ${KLEE_SRC}/.travis/klee.sh - -# Revoke password-less sudo and Set up sudo access for the ``klee`` user so it -# requires a password -USER root -RUN mv /etc/sudoers.bak /etc/sudoers && \ - echo 'klee ALL=(root) ALL' >> /etc/sudoers -USER klee - -# FIXME: Shouldn't we just invoke the `install` target? This will -# duplicate some files but the Docker image is already pretty bloated -# so this probably doesn't matter. -# Add KLEE binary directory to PATH -RUN echo 'export PATH=$PATH:'${BUILD_DIR}'/klee/bin' >> /home/klee/.bashrc - -# Link klee to /usr/bin so that it can be used by docker run -USER root -RUN for executable in ${BUILD_DIR}/klee/bin/* ; do ln -s ${executable} /usr/bin/`basename ${executable}`; done -USER klee diff --git a/scripts/build/Dockerfile_base b/scripts/build/Dockerfile_base new file mode 100644 index 00000000..8daee330 --- /dev/null +++ b/scripts/build/Dockerfile_base @@ -0,0 +1,15 @@ +# Build dependencies for LLVM +FROM ubuntu:16.04 +LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>" + +ENV DOCKER_BUILD=1 + +# Define all variables that can be changed as argument to docker build +ARG BASE=/tmp + +# Copy across all source files +ADD /scripts/build/* scripts/build/ + +# Install packages +RUN scripts/build/dependencies-ubuntu.sh && rm -rf /var/lib/apt/lists/* +WORKDIR $BASE diff --git a/scripts/build/Dockerfile_klee b/scripts/build/Dockerfile_klee new file mode 100644 index 00000000..79ad3838 --- /dev/null +++ b/scripts/build/Dockerfile_klee @@ -0,0 +1,58 @@ +# Build the final KLEE layer +ARG REPOSITORY +ARG LLVM_VERSION_SHORT +ARG LLVM_SUFFIX +ARG SOLVER_SUFFIX +ARG DEPS_SUFFIX +FROM ${REPOSITORY}/klee_deps:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX} +LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>" + +# Define all variables that can be changed as argument to the docker build +ARG BASE=/tmp +ARG COVERAGE=0 +ARG DEPS_SUFFIX +ARG DISABLE_ASSERTIONS +ARG ENABLE_OPTIMIZED +ARG ENABLE_DEBUG +ARG KLEE_TRAVIS_BUILD +ARG KLEE_UCLIBC +ARG LLVM_VERSION +ARG LLVM_SUFFIX +ARG METASMT_BOOST_VERSION +ARG METASMT_DEFAULT +ARG METASMT_VERSION +ARG REQUIRES_RTTI +ARG SANITIZER_BUILD +ARG SANITIZER_SUFFIX +ARG SOLVER_SUFFIX +ARG SOLVERS +ARG STP_VERSION +ARG TRAVIS_OS_NAME +ARG USE_TCMALLOC +ARG Z3_VERSION + +ENV DOCKER_BUILD=1 + +# Copy across source files needed for build +ADD / ${BASE}/klee_src + +# TODO Remove when STP is fixed +RUN export LD_LIBRARY_PATH=${BASE}/metaSMT/deps/stp-git-basic/lib/ && export KLEE_SRC=${BASE}/klee_src && ${BASE}/klee_src/scripts/build/klee.sh && rm -rf ${BASE}/klee_src/.git + +# Create ``klee`` user for container with password ``klee``. +# and give it password-less sudo access (temporarily so we can use the TravisCI scripts) +RUN useradd -m klee && \ + echo klee:klee | chpasswd && \ + cp /etc/sudoers /etc/sudoers.bak && \ + echo 'klee ALL=(root) NOPASSWD: ALL' >> /etc/sudoers + +# Set klee user to be owner +RUN chown --recursive klee: ${BASE}/klee_src + +USER klee +WORKDIR /home/klee + +# Add KLEE binary directory to PATH +RUN /bin/bash -c 'DIR="${BASE}/klee_src/scripts/build" source ${BASE}/klee_src/scripts/build/common-defaults.sh && ln -s ${BASE}/klee_build* ${BASE}/klee_build && echo "export PATH=\"$PATH:${LLVM_BIN}:${BASE}/klee_build/bin\"" >> /home/klee/.bashrc' +# TODO Remove when STP is fixed +RUN /bin/bash -c 'echo "export LD_LIBRARY_PATH=${BASE}/metaSMT/deps/stp-git-basic/lib/" >> /home/klee/.bashrc' diff --git a/scripts/build/Dockerfile_klee_deps b/scripts/build/Dockerfile_klee_deps new file mode 100644 index 00000000..582d324f --- /dev/null +++ b/scripts/build/Dockerfile_klee_deps @@ -0,0 +1,33 @@ +# Build KLEE dependencies except LLVM and solvers +ARG REPOSITORY +ARG LLVM_VERSION_SHORT +ARG LLVM_SUFFIX +ARG SOLVER_SUFFIX +FROM ${REPOSITORY}/solver:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX} +LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>" + +# Define all variables that can be changed as argument to the docker build +ARG BASE=/tmp +ARG DISABLE_ASSERTIONS +ARG ENABLE_OPTIMIZED +ARG ENABLE_DEBUG +ARG KEEP_BUILD +ARG KEEP_SRC +ARG KLEE_TRAVIS_BUILD +ARG KLEE_UCLIBC +ARG LLVM_VERSION +ARG LLVM_SUFFIX +ARG REQUIRES_RTTI +ARG SANITIZER_BUILD +ARG TRAVIS_OS_NAME +ARG USE_TCMALLOC + +ENV DOCKER_BUILD=1 + +# Copy across source files needed for build +ADD /scripts/build/* scripts/build/ + +# Build KLEE (use TravisCI script) +RUN ${BASE}/scripts/build/testing-utils.sh +RUN ${BASE}/scripts/build/tcmalloc.sh +RUN ${BASE}/scripts/build/uclibc.sh diff --git a/scripts/build/Dockerfile_llvm_build b/scripts/build/Dockerfile_llvm_build new file mode 100644 index 00000000..548f0d8a --- /dev/null +++ b/scripts/build/Dockerfile_llvm_build @@ -0,0 +1,27 @@ +# Build LLVM +ARG LLVM_VERSION_SHORT +ARG REPOSITORY +FROM ${REPOSITORY}/base +LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>" + +ENV DOCKER_BUILD=1 + +# Define all variables that can be changed as argument to the docker build +ARG BASE=/tmp +ARG DISABLE_ASSERTIONS +ARG ENABLE_OPTIMIZED +ARG ENABLE_DEBUG +ARG KEEP_BUILD +ARG KEEP_SRC +ARG KLEE_TRAVIS_BUILD +ARG LLVM_VERSION +ARG PACKAGED +ARG REQUIRES_RTTI +ARG SANITIZER_BUILD +ARG TRAVIS_OS_NAME + +WORKDIR $BASE + +# Copy across source files needed for build +ADD /scripts/build/* scripts/build/ +RUN ./scripts/build/llvm.sh diff --git a/scripts/build/Dockerfile_solver_build b/scripts/build/Dockerfile_solver_build new file mode 100644 index 00000000..ba2af62a --- /dev/null +++ b/scripts/build/Dockerfile_solver_build @@ -0,0 +1,33 @@ +ARG REPOSITORY +ARG LLVM_SUFFIX +ARG LLVM_VERSION_SHORT +FROM ${REPOSITORY}/llvm_built:${LLVM_VERSION_SHORT}${LLVM_SUFFIX} +LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>" + +ENV DOCKER_BUILD=1 + +# Define all variables that can be changed as argument to docker build +ARG BASE=/tmp +ARG DISABLE_ASSERTIONS +ARG ENABLE_OPTIMIZED +ARG ENABLE_DEBUG +ARG KEEP_BUILD +ARG KEEP_SRC +ARG KLEE_TRAVIS_BUILD +ARG LLVM_VERSION +ARG METASMT_BOOST_VERSION +ARG METASMT_DEFAULT +ARG METASMT_VERSION +ARG REQUIRES_RTTI +ARG SOLVERS +ARG SANITIZER_BUILD +ARG STP_VERSION +ARG STORAGE_SPACE_OPTIMIZED=1 +ARG TRAVIS_OS_NAME +ARG Z3_VERSION + +WORKDIR $BASE + +# Copy across source files needed for build +ADD /scripts/build/* scripts/build/ +RUN scripts/build/solvers.sh diff --git a/scripts/build/build-docker.sh b/scripts/build/build-docker.sh new file mode 100755 index 00000000..a409fb0a --- /dev/null +++ b/scripts/build/build-docker.sh @@ -0,0 +1,100 @@ +#!/bin/bash +# Build a KLEE docker image. If needed, build all dependent layers as well. +set -e + +# We are going to build docker containers +export DOCKER_BUILD=1 + +# All scripts are located relative to this one +DIR="$(cd "$(dirname "$0")" && pwd)" +source "${DIR}/common-defaults.sh" +KLEEDIR="${DIR}/../.." + +############################################################################### +# Setup Docker variables needed to build layers layers +############################################################################### + +add_arg_variable() { + name=$1 + name_var=${!name} + if [[ (-z "$name_var") || ($name_var == "") ]] ; then + val="" + else + val="--build-arg ${name}=${name_var} " + fi + echo "$val" +} + +DOCKER_OPTS=() +for v in \ + LLVM_VERSION \ + LLVM_VERSION_SHORT \ + ENABLE_OPTIMIZED \ + DISABLE_ASSERTIONS \ + ENABLE_DEBUG \ + REQUIRES_RTTI \ + LLVM_SUFFIX \ + REPOSITORY \ + SANITIZER_BUILD \ + SANITIZER_SUFFIX \ + PACKAGED \ + KLEE_TRAVIS_BUILD \ + TRAVIS_OS_NAME \ + METASMT_VERSION \ + METASMT_DEFAULT \ + METASMT_BOOST_VERSION \ + SOLVER_SUFFIX \ + Z3_VERSION \ + STP_VERSION \ + KLEE_UCLIBC \ + DEPS_SUFFIX \ + USE_TCMALLOC \ + COVERAGE \ + KEEP_SRC \ + KEEP_BUILD \ + TCMALLOC_VERSION \ + GTEST_VERSION \ + SOLVERS \ + ; do + DOCKER_OPTS+=($(add_arg_variable $v)) +done + +echo "DOCKER_OPTS: ${DOCKER_OPTS[@]}" +docker_build_and_push() { + merge=$1 + image=$2 + script=$3 + set +e + # Get or build layer + echo "$image" + if ! docker pull $image ; then + set -e + # Update if needed + echo "BUILD IMAGE" + merge_arg="" + # if [[ "${merge}x" == "1x" ]]; then + # #merge_arg="--squash" + # fi + docker build ${merge_arg} -f "${DIR}/$script" ${@:4} -t "$image" "${KLEEDIR}" + set +e + docker push "$image" + fi + return 0 +} + +############################################################################### +# Build different layers +############################################################################### + +# Check if the build of dependencies only has been requested +if [[ -z ${DOCKER_BUILD_DEPS_ONLY} || "${DOCKER_BUILD_DEPS_ONLY}x" == "1x" ]]; then + echo "Build dependencies" + docker_build_and_push 1 ${REPOSITORY}/base Dockerfile_base "${DOCKER_OPTS[@]}" + docker_build_and_push 1 ${REPOSITORY}/llvm_built:${LLVM_VERSION_SHORT}${LLVM_SUFFIX} Dockerfile_llvm_build "${DOCKER_OPTS[@]}" + docker_build_and_push 1 ${REPOSITORY}/solver:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX} Dockerfile_solver_build "${DOCKER_OPTS[@]}" + docker_build_and_push 1 ${REPOSITORY}/klee_deps:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX} Dockerfile_klee_deps "${DOCKER_OPTS[@]}" +fi + +if [[ -z ${DOCKER_BUILD_DEPS_ONLY} || "${DOCKER_BUILD_DEPS_ONLY}x" != "1x" ]]; then + docker build -f "${DIR}/Dockerfile_klee" "${DOCKER_OPTS[@]}" --build-arg SOLVERS="$SOLVERS" -t ${REPOSITORY}/klee:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SANITIZER_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX} "${KLEEDIR}" +fi diff --git a/scripts/build/build-travis-containers.sh b/scripts/build/build-travis-containers.sh new file mode 100755 index 00000000..ad2ac73a --- /dev/null +++ b/scripts/build/build-travis-containers.sh @@ -0,0 +1,22 @@ +#!/bin/bash +# Build all the docker containers utilized, that would be +# also build by TravisCI. +# +# Every line starting with " - LLVM_VERSION=" is a single setup +set -e +DIR="$(cd "$(dirname "$0")" && pwd)" + +# Build dependencies only +export DOCKER_BUILD_DEPS_ONLY=1 +export KLEE_TRAVIS_BUILD="1" +export REPOSITORY="klee" +export TRAVIS_OS_NAME="linux" + +while read -r line +do + name=$(echo $line| grep "\- LLVM" | xargs -L 1 | cut -d "-" -f 2) + if [[ "x$name" == "x" ]]; then + continue + fi + /bin/bash -c "$name ./scripts/build/build-docker.sh" +done < "${DIR}/../../.travis.yml" diff --git a/scripts/build/build-travis.sh b/scripts/build/build-travis.sh new file mode 100755 index 00000000..47e3f088 --- /dev/null +++ b/scripts/build/build-travis.sh @@ -0,0 +1,23 @@ +#!/bin/bash +# Build/setup all Travis dependencies if needed +set -e +if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + export DOCKER_BUILD_DEPS_ONLY=1 + "${KLEE_SRC_TRAVIS}/scripts/build/build-docker.sh" +elif [[ "$TRAVIS_OS_NAME" == "osx" ]]; then + brew tap klee/klee + brew update + brew install ccache + set +e + brew install python@2 + if [[ "X$?" != "X0" ]]; then + brew link --overwrite python@2 + fi + set -e + pip install lit + export PATH="/usr/local/opt/ccache/libexec:$PATH" + "${KLEE_SRC_TRAVIS}/scripts/build/install-klee-deps.sh" +else + echo "UNKNOWN OS ${TRAVIS_OS_NAME}" + exit 1 +fi diff --git a/scripts/build/common-defaults.sh b/scripts/build/common-defaults.sh new file mode 100644 index 00000000..5cefef19 --- /dev/null +++ b/scripts/build/common-defaults.sh @@ -0,0 +1,53 @@ +# This file is meant to be included by shell scripts to provide common default +# values. +# It is used by: travis builds; docker builds and local builds +# Change defaults to setup different development environment +# Defines defaults used to build a default docker image outside of Travis +if [[ "${DOCKER_BUILD}x" == "1x" ]]; then + # Default for docker: Do not keep build and source files for small images + : "${KEEP_BUILD:=0}" + : "${KEEP_SRC:=0}" + echo "DOCKER_BUILD" +fi +if [[ "${KLEE_TRAVIS_BUILD}x" != "1x" ]]; then +: "${REPOSITORY:=klee}" +: "${LLVM_VERSION:=3.4}" +: "${DISABLE_ASSERTIONS:=0}" +: "${ENABLE_DEBUG:=1}" +: "${ENABLE_OPTIMIZED:=1}" +: "${SOLVERS:=STP}" +: "${STP_VERSION:=2.1.2}" +: "${Z3_VERSION:=4.4.1}" +: "${METASMT_VERSION:=v4.rc1}" +: "${METASMT_DEFAULT:=STP}" +: "${METASMT_BOOST_VERSION:=}" +: "${REQUIRES_RTTI:=0}" +: "${KLEE_UCLIBC:=klee_uclibc_v1.0.0}" +: "${USE_TCMALLOC:=1}" +: "${PACKAGED:=0}" +# undefined, address, memory +: "${SANITIZER_BUILD:=}" +# Defines if source and build artifacts should be preserved +: "${KEEP_BUILD:=1}" +: "${KEEP_SRC:=1}" +OS="$(uname)" +case $OS in + 'Linux') + TRAVIS_OS_NAME='linux' + ;; + 'Darwin') + TRAVIS_OS_NAME='osx' + ;; + *) ;; +esac +fi + +# General default values +: "${TCMALLOC_VERSION:=2.4}" +: "${GTEST_VERSION:=1.7.0}" + +if [[ "${DIR}x" == "x" ]]; then + echo "\${DIR} not set" + exit 1 +fi +source "${DIR}/common-functions" diff --git a/scripts/build/common-functions b/scripts/build/common-functions new file mode 100644 index 00000000..45c94fef --- /dev/null +++ b/scripts/build/common-functions @@ -0,0 +1,217 @@ +# Defines common function and variables used by the scripts + +function git_clone_or_update() { + local url="$1" + local destination="$2" + local branch="$3" + + if [[ ! -e "${destination}/.git" ]]; then + git clone $([ "${branch}x" != "x" ] && echo "--depth 1 -b ${branch}" || echo "") "$url" "$destination" + else + cd "$destination" + git pull + if [[ ! -z "$branch" ]]; then + git checkout "${branch}" + fi + fi +} + +function to_upper() { + echo "$1" | tr '[:lower:]' '[:upper:]' +} + +function to_lower() { + echo "$1" | tr '[:upper:]' '[:lower:]' +} + +# This file is meant to be included by shell scripts +# that need to do a sanitized build. + +# Users of this script can use this variable +# to detect if a Sanitized build was enabled. +IS_SANITIZED_BUILD=0 + +# Remove ":" separator +sanitizers=(${SANITIZER_BUILD//:/ }) +# Sort sanitizers +IFS=$'\n' sorted_sanitizers=($(sort <<<"${sanitizers[*]}")) +unset IFS + +# Set variables used by clients. +## Build variables +SANITIZER_CXX_FLAGS="" +SANITIZER_C_FLAGS="" +SANITIZER_LD_FLAGS="" +# Docker_suffix +SANITIZER_SUFFIX="" + +# +for sanitizer in ${sorted_sanitizers[@]}; do + # AddressSanitizer + if [ "X${sanitizer}" == "Xaddress" ]; then + echo "Using ASan" + flags=" -fsanitize=address -fno-omit-frame-pointer -g" + SANITIZER_CXX_FLAGS+=" ${flags}" + SANITIZER_C_FLAGS+=" ${flags}" + SANITIZER_LD_FLAGS+=" ${flags}" + SANITIZER_SUFFIX+="_asan" + IS_SANITIZED_BUILD=1 + continue + fi + + # Undefined Behaviour Sanitizer + if [ "X${sanitizer}" == "Xundefined" ]; then + echo "Using UBSan" + flags="-fsanitize=undefined -fno-omit-frame-pointer -g" + SANITIZER_CXX_FLAGS+=" ${flags}" + SANITIZER_C_FLAGS+=" ${flags}" + SANITIZER_LD_FLAGS+=" ${flags} -lubsan -fuse-ld=gold" + SANITIZER_SUFFIX+="_ubsan" + IS_SANITIZED_BUILD=1 + continue + fi + + # Undefined Behaviour Sanitizer + if [ "X${sanitizer}" == "Xmemory" ]; then + echo "Using Memory Sanitizer" + if [[ "X${PACKAGED}" == "X1" ]]; then + echo "simultanously memory sanitizer and packaged is not supported " + exit 1 + fi + + SANITIZER_SUFFIX+="_memsan" + SANITIZER_LLVM_UNINSTRUMENTED="${LLVM_BUILD}_uninstrumented" + SANITIZER_LLVM_LIBCXX="${LLVM_BUILD}_libcxx" + + SANITIZER_C_COMPILER="${SANITIZER_LLVM_UNINSTRUMENTED}/bin/clang" + SANITIZER_CXX_COMPILER="${SANITIZER_LLVM_UNINSTRUMENTED}/bin/clang++" + SANITIZER_CMAKE_C_COMPILER="-DCMAKE_C_COMPILER=${SANITIZER_C_COMPILER}" + SANITIZER_CMAKE_CXX_COMPILER="-DCMAKE_CXX_COMPILER=${SANITIZER_CXX_COMPILER}" + + MSAN_LINK_FLAGS="-lc++abi -Wl,--rpath=${SANITIZER_LLVM_LIBCXX}/lib -L${SANITIZER_LLVM_LIBCXX}/lib"; + MSAN_FLAGS="$MSAN_LINK_FLAGS -nostdinc++ \ + -isystem ${SANITIZER_LLVM_LIBCXX}/include \ + -isystem ${SANITIZER_LLVM_LIBCXX}/include/c++/v1 \ + -fsanitize=memory \ + -fsanitize-memory-track-origins \ + -w -fno-omit-frame-pointer -g"; + + SANITIZER_CXX_FLAGS+="${MSAN_FLAGS} -stdlib=libc++" + SANITIZER_C_FLAGS+="${MSAN_FLAGS}" + SANITIZER_LD_FLAGS+="${MSAN_LINK_FLAGS}" + + IS_SANITIZED_BUILD=1 + continue + fi + + echo "Unknown sanitizer: $sanitizer" + exit 1 +done + +# This file is meant to be included by shell scripts +# that need to retrieve llvm-specifi variables + +LLVM_VERSION_SHORT="${LLVM_VERSION/./}" +LLVM_SUFFIX="" + +BuildMode='' + +# Build from source +if [[ "${PACKAGED}x" == "1x" ]]; then + LLVM_SUFFIX+="_packaged" + set +e + llvm_config_path=$(which llvm-config-${LLVM_VERSION}) + if [[ -e "${llvm_config_path}" ]]; then + LLVM_BIN="$(llvm-config-${LLVM_VERSION} --bindir)" + fi + set -e +else + if [[ "${ENABLE_OPTIMIZED}" == "1" ]]; then + LLVM_SUFFIX+="_O" + BuildMode="Release" + else + LLVM_SUFFIX+="_NO" + fi + + if [[ ("${ENABLE_DEBUG}" == "1") || ("${ENABLE_OPTIMIZED}" != "1") ]]; then + LLVM_SUFFIX+="_D" + [ -z "$BuildMode" ] && BuildMode="Debug" || BuildMode="$BuildMode+Debug" + else + LLVM_SUFFIX+="_ND" + fi + + if [[ "${DISABLE_ASSERTIONS}" == "1" || -z "${DISABLE_ASSERTIONS}" ]]; then + LLVM_SUFFIX+="_NA" + else + LLVM_SUFFIX+="_A" + [ -z "$BuildMode" ] && BuildMode="Asserts" || BuildMode="$BuildMode+Asserts" + fi + + if [[ "${REQUIRES_RTTI}" == "1" ]]; then + LLVM_SUFFIX+="_RTTI" + fi + + if [[ "${SANITIZER_SUFFIX}x" != "x" ]]; then + LLVM_SUFFIX+="${SANITIZER_SUFFIX}" + fi + + LLVM_BASE="${BASE}/llvm-${LLVM_VERSION_SHORT}" + LLVM_BUILD="${LLVM_BASE}-build${LLVM_SUFFIX}" + LLVM_INSTALL="${LLVM_BASE}-install${LLVM_SUFFIX}" + LLVM_BIN="${LLVM_INSTALL}/bin" + if [[ ${LLVM_VERSION_SHORT} -le 37 ]]; then + LLVM_BUILDMODE="$BuildMode" + LLVM_BUILD_BIN="${LLVM_BUILD}/${LLVM_BUILDMODE}/bin" + else + LLVM_BUILD_BIN="${LLVM_BUILD}/bin" + fi +fi + +# Generate the suffix used for the solver combination +# Every solver needs to have a version explicitly specified +SOLVER_SUFFIX="" + +# Remove ":" separator +solvers=(${SOLVERS//:/ }) + +# Sort solvers +IFS=$'\n' sorted_solvers=($(sort <<<"${solvers[*]}")) +unset IFS + +for solver in ${sorted_solvers[@]}; do + # Make sure version a solver specific version variable is used + solver_var="$(to_upper "$solver")_VERSION" + SOLVER_VERSION="${!solver_var}" + if [[ -z "${SOLVER_VERSION}" ]] ; then + echo "Solver version for $solver not defined" + exit 1 + fi + # Add the solver to the suffix and lower case it + SOLVER_SUFFIX+="_$(to_lower "$solver")$(to_lower "$SOLVER_VERSION")" + echo $SOLVER_SUFFIX + if [[ "$(to_lower "$solver")" == "metasmt" ]]; then + if [[ "${REQUIRES_RTTI}x" != "1x" ]]; then + echo "METASMT requires an RTTI build" + exit 1 + fi + if [[ -z "${METASMT_DEFAULT}" ]]; then + echo "METASMT_DEFAULT not defined" + exit 1 + fi + if [[ -z "${METASMT_BOOST_VERSION}" ]] ; then + echo "METASMT_BOOST_VERSION not defined - use default" + SOLVER_SUFFIX+="_$(to_lower "$METASMT_DEFAULT")_boost-dev" + else + SOLVER_SUFFIX+="_$(to_lower "$METASMT_DEFAULT")_$(to_lower "$METASMT_BOOST_VERSION")" + fi + fi +done + +# This file is meant to be included by shell scripts that handle dependencies by +# KLEE beside LLVM and solvers +# +# Generate the suffix used for direct dependencies of KLEE like uclibc +DEPS_SUFFIX="" +if [[ "${KLEE_UCLIBC}" != "0" ]]; then + DEPS_SUFFIX+="_${KLEE_UCLIBC}" +fi diff --git a/scripts/build/dependencies-ubuntu.sh b/scripts/build/dependencies-ubuntu.sh new file mode 100755 index 00000000..065893cd --- /dev/null +++ b/scripts/build/dependencies-ubuntu.sh @@ -0,0 +1,42 @@ +#!/bin/bash +# Installs ubuntu dependencies +set -e + +# Update packages +apt update + +# Install essential build tools +apt -y --no-install-recommends install build-essential software-properties-common wget + +# Add repository for additional compilers +add-apt-repository ppa:ubuntu-toolchain-r/test -y +add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial main" +wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key| apt-key add - +apt update -y + +#Install essential dependencies +apt -y --no-install-recommends install \ + binutils \ + bison \ + cmake \ + flex \ + git \ + groff-base \ + libboost-program-options-dev \ + libncurses-dev \ + ninja-build \ + patch \ + perl \ + python \ + python3-dev \ + python3-pip \ + python3-setuptools \ + subversion \ + sudo \ + unzip \ + wget \ + zlib1g-dev +apt clean + +# Install lit for testing +pip3 install wheel && pip3 install lit diff --git a/scripts/build/install-klee-deps.sh b/scripts/build/install-klee-deps.sh new file mode 100755 index 00000000..622e621f --- /dev/null +++ b/scripts/build/install-klee-deps.sh @@ -0,0 +1,26 @@ +#!/bin/bash +set -e +########################################################################### +# Install KLEE dependencies +########################################################################### +DIR="$(cd "$(dirname "$0")" && pwd)" + +if [[ "${BASE}x" == "x" ]]; then + echo "\${BASE} not set" + exit 1 +fi + +# Install LLVM and the LLVM bitcode compiler we require to build KLEE +"${DIR}/llvm.sh" + +# Install allocators +"${DIR}/tcmalloc.sh" + +# Get SMT solvers +"${DIR}/solvers.sh" + +# Get needed utlities/libraries for testing KLEE +"${DIR}/testing-utils.sh" + +# Install uclibc +"${DIR}/uclibc.sh" diff --git a/scripts/build/install-local.sh b/scripts/build/install-local.sh new file mode 100755 index 00000000..50dfb612 --- /dev/null +++ b/scripts/build/install-local.sh @@ -0,0 +1,17 @@ +#!/bin/bash +# Install all dependencies to build KLEE in a directory ${BASE} +set -e +if [[ "${BASE}x" == "x" ]]; then + echo "\${BASE} not set" + exit 1 +fi + +# Create base directory if not exists +mkdir -p "${BASE}" +DIR=$(dirname "$(readlink -f "$0" || stat -f "$0")") + +# Install dependencies +"${DIR}/install-klee-deps.sh" + +# Build KLEE +"${DIR}/klee.sh" diff --git a/.travis/klee.sh b/scripts/build/klee.sh index 5c5a15b5..2b68dd7e 100755 --- a/.travis/klee.sh +++ b/scripts/build/klee.sh @@ -1,43 +1,35 @@ #!/bin/bash -x +# Compile KLEE # Make sure we exit if there is a failure set -e -: ${SOLVERS?"Solvers must be specified"} -coverage_setup() -{ - # Zero coverage for any file, e.g. previous tests - lcov --directory . --no-external --zerocounters - # Create a baseline by capturing any file used for compilation, no execution yet - lcov --rc lcov_branch_coverage=1 --directory . --base-directory=${KLEE_SRC} --no-external --capture --initial --output-file coverage_base.info - lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'test/*' --output-file coverage_base.info - lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'unittests/*' --output-file coverage_base.info -} +DIR="$(cd "$(dirname "$0")" && pwd)" +source "${DIR}/common-defaults.sh" -coverageup() -{ - # Create report - # (NOTE: "--rc lcov_branch_coverage=1" needs to be added in all calls, otherwise branch coverage gets dropped) - lcov --rc lcov_branch_coverage=1 --directory . --base-directory=${KLEE_SRC} --no-external --capture --output-file coverage.info - # Exclude uninteresting coverage goals (LLVM, googletest, and KLEE system and unit tests) - lcov --rc lcov_branch_coverage=1 --remove coverage.info 'test/*' --output-file coverage.info - lcov --rc lcov_branch_coverage=1 --remove coverage.info 'unittests/*' --output-file coverage.info - # Combine baseline and measured coverage - lcov --rc lcov_branch_coverage=1 -a coverage_base.info -a coverage.info -o coverage_all.info - # Debug info - lcov --rc lcov_branch_coverage=1 --list coverage_all.info - # Uploading report to CodeCov - bash <(curl -s https://codecov.io/bash) -R ${KLEE_SRC} -X gcov -y ${KLEE_SRC}/.codecov.yml -f coverage_all.info -F $1 -} +: ${SOLVERS?"Solvers must be specified"} +if [[ -z "${KLEE_UCLIBC}" ]]; then + echo "KLEE_UCLIBC must be specified: 0 or branch/tag" + exit 1 +fi +if [[ -z "${KLEE_SRC}" ]]; then + # Assumeption: this build script is part of the KLEE source tree + KLEE_SRC="${DIR}/../.." +fi +CMAKE_PREFIX_PATH="" ############################################################################### -# Select the compiler to use to generate LLVM bitcode +# Handling LLVM configuration ############################################################################### -if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - KLEE_CC=/usr/bin/clang-${LLVM_VERSION} - KLEE_CXX=/usr/bin/clang++-${LLVM_VERSION} +if [[ "$TRAVIS_OS_NAME" = "linux" ]] ; then + LLVM_CONFIG="${LLVM_BIN}/llvm-config" + LLVM_BUILD_DIR="/usr/lib/llvm-${LLVM_VERSION_SHORT}/build" + KLEE_CC="${LLVM_BIN}/clang" + KLEE_CXX="${LLVM_BIN}/clang++" elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then - KLEE_CC=/usr/local/bin/clang-${LLVM_VERSION} - KLEE_CXX=/usr/local/bin/clang++-${LLVM_VERSION} + LLVM_CONFIG="/usr/local/bin/llvm-config-${LLVM_VERSION}" + LLVM_BUILD_DIR="$(${LLVM_CONFIG} --src-root)" + KLEE_CC="/usr/local/bin/clang-${LLVM_VERSION}" + KLEE_CXX="/usr/local/bin/clang++-${LLVM_VERSION}" else echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" exit 1 @@ -47,14 +39,9 @@ fi # klee-uclibc ############################################################################### if [ "${KLEE_UCLIBC}" != "0" ]; then - git clone --depth 1 -b ${KLEE_UCLIBC} git://github.com/klee/klee-uclibc.git - cd klee-uclibc - ./configure --make-llvm-lib --with-cc "${KLEE_CC}" --with-llvm-config /usr/bin/llvm-config-${LLVM_VERSION} - make - KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=TRUE -DKLEE_UCLIBC_PATH=$(pwd) -DENABLE_POSIX_RUNTIME=TRUE" - cd ../ + KLEE_UCLIBC_CONFIGURE_OPTION=(-DENABLE_KLEE_UCLIBC=TRUE -DKLEE_UCLIBC_PATH="${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}" -DENABLE_POSIX_RUNTIME=TRUE) else - KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE" + KLEE_UCLIBC_CONFIGURE_OPTION=(-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE) fi COVERAGE_FLAGS="" @@ -66,28 +53,31 @@ fi ############################################################################### # Handle setting up solver configure flags for KLEE ############################################################################### -SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /') +SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /g') # Set CMake configure options -KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=OFF" -KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=OFF" -KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=OFF" +KLEE_Z3_CONFIGURE_OPTION=(-DENABLE_SOLVER_Z3=OFF) +KLEE_STP_CONFIGURE_OPTION=(-DENABLE_SOLVER_STP=OFF) +KLEE_METASMT_CONFIGURE_OPTION=(-DENABLE_SOLVER_METASMT=OFF) for solver in ${SOLVER_LIST}; do echo "Setting CMake configuration option for ${solver}" case ${solver} in STP) - KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=TRUE -DSTP_DIR=${BUILD_DIR}/stp/build" + KLEE_STP_CONFIGURE_OPTION=(-DENABLE_SOLVER_STP=TRUE -DSTP_DIR="${BASE}/stp-${STP_VERSION}-install") ;; Z3) echo "Z3" - KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=TRUE" + KLEE_Z3_CONFIGURE_OPTION=(-DENABLE_SOLVER_Z3=TRUE) + if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + KLEE_Z3_CONFIGURE_OPTION+=(-DZ3_INCLUDE_DIRS="${BASE}/z3-${Z3_VERSION}-install/include" -DZ3_LIBRARIES="${BASE}/z3-${Z3_VERSION}-install/lib/libz3.so") + fi ;; metaSMT) echo "metaSMT" if [ "X${METASMT_DEFAULT}" == "X" ]; then METASMT_DEFAULT=STP fi - KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=TRUE -DmetaSMT_DIR=${BUILD_DIR}/metaSMT/build -DMETASMT_DEFAULT_BACKEND=${METASMT_DEFAULT}" + KLEE_METASMT_CONFIGURE_OPTION=(-DENABLE_SOLVER_METASMT=TRUE -DmetaSMT_DIR="${BASE}/metaSMT/build" -DMETASMT_DEFAULT_BACKEND="${METASMT_DEFAULT}") ;; *) echo "Unknown solver ${solver}" @@ -98,34 +88,22 @@ done ############################################################################### # Handle additional configure flags ############################################################################### -TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE") -############################################################################### -# Handle Sanitizer flags -############################################################################### -source ${KLEE_SRC}/.travis/sanitizer_flags.sh - -############################################################################### -# Handling LLVM configuration -############################################################################### -if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - LLVM_CONFIG="/usr/lib/llvm-${LLVM_VERSION}/bin/llvm-config" - LLVM_BUILD_DIR="/usr/lib/llvm-${LLVM_VERSION}/build" -elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then - LLVM_CONFIG="/usr/local/bin/llvm-config-${LLVM_VERSION}" - LLVM_BUILD_DIR="$(${LLVM_CONFIG} --src-root)" -else - echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" - exit 1 +TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE") +if [[ "$TCMALLOC_OPTION" != "0" ]] ; then + if [[ ! -z "${CMAKE_PREFIX_PATH}" ]]; then + CMAKE_PREFIX_PATH+=":" + fi + CMAKE_PREFIX_PATH="${CMAKE_PREFIX_PATH}$BASE/tcmalloc-install" fi ############################################################################### # KLEE ############################################################################### -mkdir klee -cd klee - -GTEST_SRC_DIR="${BUILD_DIR}/test-utils/googletest-release-1.7.0/" +KLEE_BUILD="${BASE}/klee_build${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX}" +mkdir -p "${KLEE_BUILD}" +cd "${KLEE_BUILD}" +GTEST_SRC_DIR="${BASE}/googletest-release-${GTEST_VERSION}/" if [ "X${DISABLE_ASSERTIONS}" == "X1" ]; then KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=FALSE" else @@ -140,25 +118,63 @@ fi # TODO: We should support Ninja too # Configure KLEE -CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \ -CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \ +echo "CXXFLAGS=\"${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}\" \ +CFLAGS=\"${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}\" \ +LDFLAGS=\"${COVERAGE_LDFLAGS} ${SANITIZER_LD_FLAGS}\" \ cmake \ - -DLLVM_CONFIG_BINARY="${LLVM_CONFIG}" \ - -DLLVMCC="${KLEE_CC}" \ - -DLLVMCXX="${KLEE_CXX}" \ - ${KLEE_STP_CONFIGURE_OPTION} \ - ${KLEE_Z3_CONFIGURE_OPTION} \ - ${KLEE_METASMT_CONFIGURE_OPTION} \ - ${KLEE_UCLIBC_CONFIGURE_OPTION} \ - ${TCMALLOC_OPTION} \ + -DLLVM_CONFIG_BINARY=\"${LLVM_CONFIG}\" \ + -DLLVMCC=\"${KLEE_CC}\" \ + -DLLVMCXX=\"${KLEE_CXX}\" \ + ${KLEE_STP_CONFIGURE_OPTION[@]} \ + ${KLEE_Z3_CONFIGURE_OPTION[@]} \ + ${KLEE_METASMT_CONFIGURE_OPTION[@]} \ + ${KLEE_UCLIBC_CONFIGURE_OPTION[@]} \ + ${TCMALLOC_OPTION[@]} \ -DGTEST_SRC_DIR=${GTEST_SRC_DIR} \ -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} \ - ${KLEE_ASSERTS_OPTION} \ + ${KLEE_ASSERTS_OPTION[@]} \ -DENABLE_UNIT_TESTS=TRUE \ -DENABLE_SYSTEM_TESTS=TRUE \ - -DLIT_ARGS="-v" \ - ${KLEE_SRC} -make + -DLIT_ARGS=\"-v\" \ + ${SANITIZER_CMAKE_C_COMPILER[@]} \ + ${SANITIZER_CMAKE_CXX_COMPILER[@]} \ + -DCMAKE_PREFIX_PATH=${CMAKE_PREFIX_PATH} \ + ${KLEE_SRC}" > "${KLEE_BUILD}/.build_command" +source "${KLEE_BUILD}/.build_command" +make -j$(nproc) + +############################################################################### +# Prepare Coverage functionality +############################################################################### +coverage_setup() +{ + # TODO Remove it and put it to the proper package install section + apt update && apt -y --no-install-recommends install lcov + # Zero coverage for any file, e.g. previous tests + lcov --directory . --no-external --zerocounters + # Create a baseline by capturing any file used for compilation, no execution yet + lcov --rc lcov_branch_coverage=1 --directory . --base-directory="${KLEE_SRC}" --no-external --capture --initial --output-file coverage_base.info + lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'test/*' --output-file coverage_base.info + lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'unittests/*' --output-file coverage_base.info +} + +coverageup() +{ + # Create report + # (NOTE: "--rc lcov_branch_coverage=1" needs to be added in all calls, otherwise branch coverage gets dropped) + lcov --rc lcov_branch_coverage=1 --directory . --base-directory="${KLEE_SRC}" --no-external --capture --output-file coverage.info + # Exclude uninteresting coverage goals (LLVM, googletest, and KLEE system and unit tests) + lcov --rc lcov_branch_coverage=1 --remove coverage.info 'test/*' --output-file coverage.info + lcov --rc lcov_branch_coverage=1 --remove coverage.info 'unittests/*' --output-file coverage.info + # Combine baseline and measured coverage + lcov --rc lcov_branch_coverage=1 -a coverage_base.info -a coverage.info -o coverage_all.info + # Debug info + lcov --rc lcov_branch_coverage=1 --list coverage_all.info + # Uploading report to CodeCov + bash <(curl -s https://codecov.io/bash) -R "${KLEE_SRC}" -X gcov -y "${KLEE_SRC}/.codecov.yml" -f coverage_all.info -F $1 +} + +COVERAGE=${COVERAGE:=0} ############################################################################### # Unit tests @@ -184,7 +200,7 @@ make systemtests # If metaSMT is the only solver, then rerun lit tests with non-default metaSMT backends if [ "X${SOLVERS}" == "XmetaSMT" ]; then - metasmt_default=`echo "${METASMT_DEFAULT,,}"` # klee_opts and kleaver_opts use lowercase + metasmt_default=$(to_lower $METASMT_DEFAULT) # klee_opts and kleaver_opts use lowercase available_metasmt_backends="btor stp z3 yices2 cvc4" for backend in $available_metasmt_backends; do if [ "X${metasmt_default}" != "X$backend" ]; then diff --git a/scripts/build/llvm.sh b/scripts/build/llvm.sh new file mode 100755 index 00000000..459fdef9 --- /dev/null +++ b/scripts/build/llvm.sh @@ -0,0 +1,204 @@ +#!/bin/bash -x +set -ev +STAGE="$1" + +DIR="$(cd "$(dirname "$0")" && pwd)" +source "${DIR}/common-defaults.sh" + +if [[ "${LLVM_VERSION_SHORT}" == "" ]]; then + echo "LLVM_VERSION_SHORT not set" + exit 1 +fi + +if [[ "${BASE}" == "" ]]; then + echo "BASE not set" + exit 1 +fi + +# Install packages if possible +if [[ "${PACKAGED}x" == "1x" ]]; then + apt update + apt install -y llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev + apt install -y clang-${LLVM_VERSION} + exit 0 +fi + +if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + LLVM_BASE="${BASE}/llvm-${LLVM_VERSION_SHORT}" + # Checkout LLVM code + svn co http://llvm.org/svn/llvm-project/llvm/branches/release_${LLVM_VERSION_SHORT} "${LLVM_BASE}" + cd "${LLVM_BASE}/tools" + svn co http://llvm.org/svn/llvm-project/cfe/branches/release_${LLVM_VERSION_SHORT} clang + cd "${LLVM_BASE}/projects" + svn co http://llvm.org/svn/llvm-project/compiler-rt/branches/release_${LLVM_VERSION_SHORT} compiler-rt + + if [[ ${LLVM_VERSION_SHORT} -gt 37 ]]; then + cd "${LLVM_BASE}/projects" + svn co http://llvm.org/svn/llvm-project/libcxx/branches/release_${LLVM_VERSION_SHORT} libcxx + cd "${LLVM_BASE}/projects" + svn co http://llvm.org/svn/llvm-project/libcxxabi/branches/release_${LLVM_VERSION_SHORT} libcxxabi + fi + + # Apply existing patches if needed + if [ -f "${BASE}/scripts/build/llvm${LLVM_VERSION_SHORT}.patch" ]; then + cd "${LLVM_BASE}" + patch -p0 -i "${BASE}/scripts/build/llvm${LLVM_VERSION_SHORT}.patch" + fi +fi + + +# For memory sanitizer, we have a multi-stage build process +if [[ "${SANITIZER_BUILD}" == "memory" ]]; then + if [[ ${LLVM_VERSION_SHORT} -le 37 ]]; then + echo "Memory sanitizer builds for <= LLVM 3.7 are not supported" + exit 1 + fi + # Build uninstrumented compiler + mkdir "${SANITIZER_LLVM_UNINSTRUMENTED}" + cd "${SANITIZER_LLVM_UNINSTRUMENTED}" + cmake -GNinja -DCMAKE_BUILD_TYPE=Release "${LLVM_BASE}" + ninja + + # Build instrumented libc/libc++ + mkdir "${SANITIZER_LLVM_LIBCXX}" + cd "${SANITIZER_LLVM_LIBCXX}" + cmake -GNinja -DCMAKE_BUILD_TYPE=RelWithDebInfo \ + -DLLVM_USE_SANITIZER=MemoryWithOrigins \ + ${SANITIZER_CMAKE_C_COMPILER} \ + ${SANITIZER_CMAKE_CXX_COMPILER} \ + "${LLVM_BASE}" + ninja cxx cxxabi + + # Build instrumented clang + mkdir "${LLVM_BUILD}" + cd "${LLVM_BUILD}" + cmake -GNinja \ + ${SANITIZER_CMAKE_C_COMPILER} \ + ${SANITIZER_CMAKE_CXX_COMPILER} \ + -DCMAKE_C_FLAGS="$SANITIZER_C_FLAGS" \ + -DCMAKE_CXX_FLAGS="$SANITIZER_CXX_FLAGS" \ + -DCMAKE_BUILD_TYPE=Release \ + -DLLVM_USE_SANITIZER=MemoryWithOrigins \ + -DLLVM_ENABLE_LIBCXX=ON \ + -DCMAKE_EXE_LINKER_FLAGS="$SANITIZER_LD_FLAGS" \ + -DCMAKE_INSTALL_PREFIX="${LLVM_INSTALL}" \ + "${LLVM_BASE}" + # Build clang as a dependency and install all needed packages + ninja clang + ninja install-clang install-llvm-config install-llvm-objdump \ + install-llvm-link install-llvm-ar install-llvm-nm install-llvm-dis \ + install-clang-headers install-llvm-as installhdrs install-LLVMX86Disassembler \ + install-LLVMX86AsmParser install-LLVMX86CodeGen install-LLVMSelectionDAG \ + install-LLVMAsmPrinter install-LLVMX86Desc install-LLVMMCDisassembler \ + install-LLVMX86Info install-LLVMX86AsmPrinter install-LLVMX86Utils \ + install-LLVMMCJIT install-LLVMExecutionEngine install-LLVMRuntimeDyld \ + install-LLVMipo install-LLVMVectorize install-LLVMLinker install-LLVMIRReader \ + install-LLVMAsmParser install-LLVMCodeGen install-LLVMTarget install-LLVMScalarOpts \ + install-LLVMInstCombine install-LLVMInstrumentation install-LLVMProfileData \ + install-LLVMObject install-LLVMMCParser install-LLVMTransformUtils install-LLVMMC \ + install-LLVMAnalysis install-LLVMBitWriter install-LLVMBitReader install-LLVMCore \ + install-llvm-symbolizer install-LLVMSupport install-lli not FileCheck + cp "${LLVM_BUILD}/bin/FileCheck" "${LLVM_INSTALL}/bin/" + cp "${LLVM_BUILD}/bin/not" "${LLVM_INSTALL}/bin/" + exit 0 +fi + +if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + # Configure; build; and install + mkdir -p "${LLVM_BUILD}" + cd "${LLVM_BUILD}" + + # Skip building if already finished + if [[ -e "${LLVM_BUILD}/.build_finished" ]]; then + exit 0 + fi + + + # Configure LLVM + if [[ ${LLVM_VERSION_SHORT} -le 37 ]]; then + CONFIG=(--enable-jit --prefix="${LLVM_INSTALL}") + if [[ "${ENABLE_OPTIMIZED}" == "1" ]]; then + CONFIG+=(--enable-optimized) + else + CONFIG+=(--disable-optimized) + fi + + if [[ "${DISABLE_ASSERTIONS}" == "1" ]]; then + CONFIG+=(--disable-assertions) + else + CONFIG+=(--enable-assertions) + fi + + if [[ "${ENABLE_DEBUG}" == "1" ]]; then + CONFIG+=(--enable-debug-runtime --enable-debug-symbols) + else + CONFIG+=(--disable-debug-symbols) + fi + CC=${CC} CXX=${CXX} CFLAGS="${LLVM_CFLAGS}" CXXFLAGS="${LLVM_CXXFLAGS}" LDFLAGS="${LLVM_LDFLAGS}" "${LLVM_BASE}/configure" "${CONFIG[@]}" + else + CONFIG=(-DCMAKE_INSTALL_PREFIX="${LLVM_INSTALL}") + # cmake build + if [[ "${ENABLE_OPTIMIZED}" == "1" && "${ENABLE_DEBUG}" != "1" ]]; then + CONFIG+=(-DCMAKE_BUILD_TYPE=Release) + fi + if [[ "${ENABLE_OPTIMIZED}" == "1" && "${ENABLE_DEBUG}" == "1" ]]; then + CONFIG+=(-DCMAKE_BUILD_TYPE=RelWithDebInfo) + fi + if [[ "${ENABLE_OPTIMIZED}" != "1" && "${ENABLE_DEBUG}" == "1" ]]; then + CONFIG+=(-DCMAKE_BUILD_TYPE=Debug) + fi + + if [[ "${DISABLE_ASSERTIONS}" == "1" ]]; then + CONFIG+=(-DLLVM_ENABLE_ASSERTIONS=Off) + else + CONFIG+=(-DLLVM_ENABLE_ASSERTIONS=On) + fi + + if [[ ! -z "${LLVM_CFLAGS}" ]] ; then + CONFIG+=(-DCMAKE_C_FLAGS="$LLVM_CFLAGS") + fi + + if [[ ! -z "${LLVM_CXXFLAGS}" ]] ; then + CONFIG+=(-DCMAKE_CXX_FLAGS="$LLVM_CXXFLAGS") + fi + + if [[ ! -z "${LLVM_LDFLAGS}" ]]; then + LDFLAGS="${LLVM_LDFLAGS}" + fi + + cmake "${CONFIG[@]}" "${LLVM_BASE}" + fi + + make -j$(nproc) + make install + + touch "${LLVM_BUILD}/.build_finished" + + cp "${LLVM_BUILD_BIN}/FileCheck" "${LLVM_INSTALL}/bin/" + cp "${LLVM_BUILD_BIN}/not" "${LLVM_INSTALL}/bin/" + + if [[ "${KEEP_BUILD}x" != "1x" ]]; then + rm -rf "${LLVM_BUILD}" + fi + + if [[ "${KEEP_SRC}x" != "1x" ]]; then + rm -rf "${LLVM_BASE}" + fi +elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then + # We use our own local cache if possible + set +e + brew install "$HOME/Library/Caches/Homebrew/llvm\@${LLVM_VERSION}*.bottle.tar.gz" + RES=$? + set -ev + if [ ${RES} -ne 0 ]; then + # This might build the llvm package use a time out to avoid dumping log information + brew install -v --build-bottle "llvm@${LLVM_VERSION}" + # Now bottle the brew + brew bottle llvm\@${LLVM_VERSION} + # Not make sure it's cached + cp llvm\@${LLVM_VERSION}*.bottle.tar.gz $HOME/Library/Caches/Homebrew/ + fi +else + echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" + exit 1 +fi diff --git a/scripts/build/patches/llvm35.patch b/scripts/build/patches/llvm35.patch new file mode 100644 index 00000000..47744b91 --- /dev/null +++ b/scripts/build/patches/llvm35.patch @@ -0,0 +1,14 @@ +*** include/llvm/ADT/IntrusiveRefCntPtr.h 2014-07-06 00:20:59.000000000 +0200 +--- include/llvm/ADT/IntrusiveRefCntPtr_new.h 2016-06-21 10:04:15.610143165 +0200 +*************** +*** 154,159 **** +--- 154,162 ---- + } + + template <class X> ++ friend class IntrusiveRefCntPtr; ++ ++ template <class X> + IntrusiveRefCntPtr(IntrusiveRefCntPtr<X>&& S) : Obj(S.get()) { + S.Obj = 0; + } diff --git a/scripts/build/solver-metasmt.sh b/scripts/build/solver-metasmt.sh new file mode 100755 index 00000000..d8626149 --- /dev/null +++ b/scripts/build/solver-metasmt.sh @@ -0,0 +1,39 @@ +#!/bin/bash -x +set -e + +DIR="$(cd "$(dirname "$0")" && pwd)" +source "${DIR}/common-defaults.sh" + +: ${METASMT_VERSION?"METASMT_VERSION not specified"} + +# Get Z3, libgmp, gperf (required by yices2) +apt update +apt -y --no-install-recommends install gperf libgmp-dev +apt clean +rm -rf /var/lib/apt/lists/* + +# Clone +git clone --single-branch --depth 1 https://github.com/hoangmle/metaSMT.git "${BASE}/metaSMT" +cd "${BASE}/metaSMT" +git submodule update --init + +if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then + echo "Error: Requested Sanitized build but sanitized build of metaSMT is not implemented" + exit 1 +fi + +# Bootstrap +git clone https://github.com/agra-uni-bremen/dependencies.git +./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off \ + --build stp-git-basic --build boolector-2.2.0 --build minisat-git \ + --build lingeling-ayv-86bf266-140429 --build yices-2.5.1 --build Z3-4.4.1 \ + --build cvc4-1.5 + +# Build +make -C build install + +# Cleanup +if [[ "${STORAGE_SPACE_OPTIMIZED}x" == "1x" ]]; then + rm -rf deps/build + rm -rf deps/cache +fi diff --git a/scripts/build/solver-stp.sh b/scripts/build/solver-stp.sh new file mode 100755 index 00000000..2e65ca30 --- /dev/null +++ b/scripts/build/solver-stp.sh @@ -0,0 +1,57 @@ +#!/bin/bash -x + +# TODO: For OSX we can prepare bottled formulas for STP and minisat + +# Make sure we exit if there is a failure +set -e +DIR="$(cd "$(dirname "$0")" && pwd)" +source "${DIR}/common-defaults.sh" + +cd ${BASE} +if [ "x${STP_VERSION}" != "x" ]; then + # Build minisat + git_clone_or_update https://github.com/stp/minisat "${BASE}/minisat" + mkdir -p "${BASE}/minisat/build" + cd "${BASE}/minisat/build" + MINISAT_DIR="$(pwd)" + if [[ "$TRAVIS_OS_NAME" == "linux" || "$TRAVIS_OS_NAME" == "osx" ]]; then + CFLAGS="${SANITIZER_C_FLAGS}" \ + CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ + LDFLAGS="${SANITIZER_LD_FLAGS}" \ + cmake -DCMAKE_INSTALL_PREFIX="${BASE}/minisat-install" \ + ${SANITIZER_CMAKE_C_COMPILER} \ + ${SANITIZER_CMAKE_CXX_COMPILER} \ + "${BASE}/minisat" + else + echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" + exit 1 + fi + make + make install + + # Build STP + git_clone_or_update git://github.com/stp/stp.git "${BASE}/stp-${STP_VERSION}" ${STP_VERSION} + mkdir -p "${BASE}/stp-${STP_VERSION}-build" + cd "${BASE}/stp-${STP_VERSION}-build" + + STP_CMAKE_FLAGS=( \ + "-DENABLE_PYTHON_INTERFACE:BOOL=OFF" \ + -DNO_BOOST:BOOL=ON \ + -DENABLE_PYTHON_INTERFACE:BOOL=OFF \ + ${SANITIZER_CMAKE_C_COMPILER} \ + ${SANITIZER_CMAKE_CXX_COMPILER} \ + ) + # Disabling building of shared libs is a workaround. + # Don't build against boost because that is broken when mixing packaged boost libraries and gcc 4.8 + CFLAGS="${SANITIZER_C_FLAGS}" \ + CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ + LDFLAGS="${SANITIZER_LD_FLAGS}" \ + cmake ${STP_CMAKE_FLAGS} \ + -DCMAKE_PREFIX_PATH="${BASE}/minisat-install" "${BASE}/stp-${STP_VERSION}" \ + -DCMAKE_INSTALL_PREFIX="${BASE}/stp-${STP_VERSION}-install" + make + make install +else + echo "No STP_VERSION given or empty" + exit 1 +fi diff --git a/scripts/build/solver-z3.sh b/scripts/build/solver-z3.sh new file mode 100755 index 00000000..c6c3381d --- /dev/null +++ b/scripts/build/solver-z3.sh @@ -0,0 +1,34 @@ +#!/bin/bash -x + +# Make sure we exit if there is a failure +set -e +DIR="$(cd "$(dirname "$0")" && pwd)" +source "${DIR}/common-defaults.sh" + +if [[ -z "${Z3_VERSION}" ]] ; then + echo "Z3_VERSION is not defined" + exit 1 +fi + +if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + mkdir -p "${BASE}/z3-${Z3_VERSION}" + cd "${BASE}/z3-${Z3_VERSION}" + wget -qO- https://github.com/Z3Prover/z3/archive/z3-${Z3_VERSION}.tar.gz | tar xz --strip-components=1 + LDFLAGS="${SANITIZER_LD_FLAGS}" \ + CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ + python scripts/mk_make.py --prefix "${BASE}/z3-${Z3_VERSION}-install" + cd build + make -j$(nproc) + make install +elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then + set +e + brew install python@2 + if [[ "X$?" != "X0" ]]; then + brew link --overwrite python@2 + fi + set -e + brew install z3 +else + echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" + exit 1 +fi diff --git a/.travis/solvers.sh b/scripts/build/solvers.sh index b419d679..71ad0c2d 100755 --- a/.travis/solvers.sh +++ b/scripts/build/solvers.sh @@ -1,27 +1,27 @@ #!/bin/bash -x # Make sure we exit if there is a failure set -e -: ${SOLVERS?"Solvers must be specified"} -SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /') +DIR="$(cd "$(dirname "$0")" && pwd)" +source "${DIR}/common-defaults.sh" + +: ${SOLVERS?"Solvers must be specified"} +SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /g') for solver in ${SOLVER_LIST}; do echo "Getting solver ${solver}" case ${solver} in STP) echo "STP" - mkdir stp - cd stp - ${KLEE_SRC}/.travis/stp.sh - cd ../ + "${DIR}/solver-stp.sh" ;; Z3) echo "Z3" - ${KLEE_SRC}/.travis/z3.sh + "${DIR}/solver-z3.sh" ;; metaSMT) echo "metaSMT" - ${KLEE_SRC}/.travis/metaSMT.sh + "${DIR}/solver-metasmt.sh" ;; *) echo "Unknown solver ${solver}" diff --git a/scripts/build/tcmalloc.sh b/scripts/build/tcmalloc.sh new file mode 100755 index 00000000..ea5596d0 --- /dev/null +++ b/scripts/build/tcmalloc.sh @@ -0,0 +1,35 @@ +#!/bin/bash -x +set -ev + +DIR="$(cd "$(dirname "$0")" && pwd)" +source "${DIR}/common-defaults.sh" + +if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + # Get tcmalloc release + if [[ ! -e "${BASE}/gperftools-${TCMALLOC_VERSION}" ]]; then + cd "${BASE}" + wget "https://github.com/gperftools/gperftools/releases/download/gperftools-${TCMALLOC_VERSION}/gperftools-${TCMALLOC_VERSION}.tar.gz" + tar xfz "gperftools-${TCMALLOC_VERSION}.tar.gz" + fi + cd "${BASE}/gperftools-${TCMALLOC_VERSION}" + ./configure --disable-dependency-tracking --disable-cpu-profiler \ + --disable-heap-checker --disable-debugalloc --enable-minimal \ + --prefix="${BASE}/tcmalloc-install" + make + make install + if [[ "${KEEP_BUILD}x" != "1x" ]]; then + rm -rf "${BASE}/gperftools-${TCMALLOC_VERSION}" + fi + + if [[ "${KEEP_SRC}x" != "1x" ]]; then + rm -f "${BASE}/gperftools-${TCMALLOC_VERSION}.tar.gz" + fi +elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then + if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then + echo "Error: Requested to install TCMalloc on macOS, which is not supported" + exit 1 + fi +else + echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" + exit 1 +fi diff --git a/scripts/build/testing-utils.sh b/scripts/build/testing-utils.sh new file mode 100755 index 00000000..8a855291 --- /dev/null +++ b/scripts/build/testing-utils.sh @@ -0,0 +1,14 @@ +#!/bin/bash -x +# Make sure we exit if there is a failure +set -e + +DIR="$(cd "$(dirname "$0")" && pwd)" +source "${DIR}/common-defaults.sh" + +# The New CMake build system just needs the GTest sources regardless +# of LLVM version. +cd "${BASE}" + +wget https://github.com/google/googletest/archive/release-${GTEST_VERSION}.zip +unzip -o release-${GTEST_VERSION}.zip +rm release-${GTEST_VERSION}.zip diff --git a/scripts/build/uclibc.sh b/scripts/build/uclibc.sh new file mode 100755 index 00000000..3440bedb --- /dev/null +++ b/scripts/build/uclibc.sh @@ -0,0 +1,37 @@ +#!/bin/bash -x +# Build the uclibc library +# Make sure we exit if there is a failure +set -e +DIR="$(cd "$(dirname "$0")" && pwd)" +source "${DIR}/common-defaults.sh" + +if [[ -z "${KLEE_UCLIBC}" ]]; then + echo "KLEE_UCLIBC must be specified: 0 or branch/tag" + exit 1 +fi + +############################################################################### +# Handling LLVM configuration +############################################################################### +if [[ "$TRAVIS_OS_NAME" = "linux" || "$TRAVIS_OS_NAME" = "osx" ]] ; then + LLVM_CONFIG="${LLVM_BIN}/llvm-config" + KLEE_CC="${LLVM_BIN}/clang" + KLEE_CXX="${LLVM_BIN}/clang++" +else + echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" + exit 1 +fi + +############################################################################### +# klee-uclibc +############################################################################### +if [ "${KLEE_UCLIBC}" != "0" ]; then + if [[ "$TRAVIS_OS_NAME" = "osx" ]] ; then + echo "UCLibc is not supported Mac OSX" + exit 1 + fi + git_clone_or_update git://github.com/klee/klee-uclibc.git "${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}" "${KLEE_UCLIBC}" + cd "${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}" + ./configure --make-llvm-lib --with-cc ${KLEE_CC} --with-llvm-config ${LLVM_CONFIG} + make +fi |