diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2018-05-18 17:15:24 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-07-04 22:14:58 +0100 |
commit | eb75a38011726d4a045f3db3edbfef924f62c737 (patch) | |
tree | 52061a0fea581586bd8d6db90bbf70a024560d57 /.travis | |
parent | 6a8081d721a1fa6eba8e7efcbd1f3cf1ca4feb10 (diff) | |
download | klee-eb75a38011726d4a045f3db3edbfef924f62c737.tar.gz |
Extensive updates to the build script for dependencies and docker
Building/managing dependencies of KLEE are not easy. This script should change this. Features: * script install different versions in their specific directories This allows: - to have different versions in parallel installed: llvm, solvers - to have different optimization levels installed (Debug, no-debug, assertions, optimized) - to have different versions of instrumentation enabled (address, memory, leakage, undefined behavior) * the script is kept distribution agnostic: assuming basic packages are installed (a compiler), use `scripts/build/ubuntu-dependencies.sh` to install ubuntu specific ones * the script does not install any file into system directories (sudo is not required) files are only installed into a user specified BASE directory The same scripts are used for either local setup (`scripts/build/local_install.sh`) or create a docker image based of your current source folder (`scripts/build/build_docker.sh`) Change the defaults permanently by modifying (`scripts/build/common-defaults.sh`) or change them on the fly by providing them as environment variables on the command line. The same scripts are also used for TravisCI, so we test what we are using.
Diffstat (limited to '.travis')
-rwxr-xr-x | .travis/install-llvm-and-runtime-compiler.sh | 27 | ||||
-rwxr-xr-x | .travis/install-tcmalloc.sh | 22 | ||||
-rwxr-xr-x | .travis/klee.sh | 202 | ||||
-rwxr-xr-x | .travis/metaSMT.sh | 49 | ||||
-rw-r--r-- | .travis/sanitizer_flags.sh | 39 | ||||
-rwxr-xr-x | .travis/solvers.sh | 30 | ||||
-rwxr-xr-x | .travis/stp.sh | 72 | ||||
-rwxr-xr-x | .travis/testing-utils.sh | 9 | ||||
-rwxr-xr-x | .travis/z3.sh | 26 |
9 files changed, 0 insertions, 476 deletions
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/klee.sh b/.travis/klee.sh deleted file mode 100755 index 5c5a15b5..00000000 --- a/.travis/klee.sh +++ /dev/null @@ -1,202 +0,0 @@ -#!/bin/bash -x -# 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 -} - -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 -} - -############################################################################### -# Select the compiler to use to generate LLVM bitcode -############################################################################### -if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - KLEE_CC=/usr/bin/clang-${LLVM_VERSION} - KLEE_CXX=/usr/bin/clang++-${LLVM_VERSION} -elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then - 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 -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 ../ -else - KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE" -fi - -COVERAGE_FLAGS="" -if [ ${COVERAGE} -eq 1 ]; then - COVERAGE_FLAGS='-fprofile-arcs -ftest-coverage' -fi - - -############################################################################### -# Handle setting up solver configure flags for KLEE -############################################################################### -SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /') - -# 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" -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" - ;; - Z3) - echo "Z3" - KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=TRUE" - ;; - 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}" - ;; - *) - echo "Unknown solver ${solver}" - exit 1 - esac -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 -fi - -############################################################################### -# KLEE -############################################################################### -mkdir klee -cd klee - -GTEST_SRC_DIR="${BUILD_DIR}/test-utils/googletest-release-1.7.0/" -if [ "X${DISABLE_ASSERTIONS}" == "X1" ]; then - KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=FALSE" -else - KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=TRUE" -fi - -if [ "X${ENABLE_OPTIMIZED}" == "X1" ]; then - CMAKE_BUILD_TYPE="RelWithDebInfo" -else - CMAKE_BUILD_TYPE="Debug" -fi - -# TODO: We should support Ninja too -# Configure KLEE -CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \ -CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_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} \ - -DGTEST_SRC_DIR=${GTEST_SRC_DIR} \ - -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} \ - ${KLEE_ASSERTS_OPTION} \ - -DENABLE_UNIT_TESTS=TRUE \ - -DENABLE_SYSTEM_TESTS=TRUE \ - -DLIT_ARGS="-v" \ - ${KLEE_SRC} -make - -############################################################################### -# Unit tests -############################################################################### -# Prepare coverage information if COVERAGE is set -if [ ${COVERAGE} -eq 1 ]; then - coverage_setup -fi -make unittests - -# Generate and upload coverage if COVERAGE is set -if [ ${COVERAGE} -eq 1 ]; then - coverageup "unittests" -fi - -############################################################################### -# lit tests -############################################################################### -if [ ${COVERAGE} -eq 1 ]; then - coverage_setup -fi -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 - available_metasmt_backends="btor stp z3 yices2 cvc4" - for backend in $available_metasmt_backends; do - if [ "X${metasmt_default}" != "X$backend" ]; then - if [ "$backend" == "cvc4" ]; then - for num in {1..5}; do sleep 120; echo 'Keep Travis alive'; done & - fi - lit -v --param klee_opts=-metasmt-backend=$backend --param kleaver_opts=-metasmt-backend=$backend test/ - fi - done -fi - -# Generate and upload coverage if COVERAGE is set -if [ ${COVERAGE} -eq 1 ]; then - coverageup "systemtests" -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/solvers.sh b/.travis/solvers.sh deleted file mode 100755 index b419d679..00000000 --- a/.travis/solvers.sh +++ /dev/null @@ -1,30 +0,0 @@ -#!/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/:/ /') - -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 ../ - ;; - Z3) - echo "Z3" - ${KLEE_SRC}/.travis/z3.sh - ;; - metaSMT) - echo "metaSMT" - ${KLEE_SRC}/.travis/metaSMT.sh - ;; - *) - echo "Unknown solver ${solver}" - exit 1 - esac -done 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 |