diff options
Diffstat (limited to 'scripts')
-rw-r--r-- | scripts/build/Dockerfile_base | 15 | ||||
-rw-r--r-- | scripts/build/Dockerfile_klee | 58 | ||||
-rw-r--r-- | scripts/build/Dockerfile_klee_deps | 33 | ||||
-rw-r--r-- | scripts/build/Dockerfile_llvm_build | 27 | ||||
-rw-r--r-- | scripts/build/Dockerfile_solver_build | 33 | ||||
-rwxr-xr-x | scripts/build/build-docker.sh | 100 | ||||
-rwxr-xr-x | scripts/build/build-travis-containers.sh | 22 | ||||
-rwxr-xr-x | scripts/build/build-travis.sh | 23 | ||||
-rw-r--r-- | scripts/build/common-defaults.sh | 53 | ||||
-rw-r--r-- | scripts/build/common-functions | 217 | ||||
-rwxr-xr-x | scripts/build/dependencies-ubuntu.sh | 42 | ||||
-rwxr-xr-x | scripts/build/install-klee-deps.sh | 26 | ||||
-rwxr-xr-x | scripts/build/install-local.sh | 17 | ||||
-rwxr-xr-x | scripts/build/klee.sh | 218 | ||||
-rwxr-xr-x | scripts/build/llvm.sh | 204 | ||||
-rw-r--r-- | scripts/build/patches/llvm35.patch | 14 | ||||
-rwxr-xr-x | scripts/build/solver-metasmt.sh | 39 | ||||
-rwxr-xr-x | scripts/build/solver-stp.sh | 57 | ||||
-rwxr-xr-x | scripts/build/solver-z3.sh | 34 | ||||
-rwxr-xr-x | scripts/build/solvers.sh | 30 | ||||
-rwxr-xr-x | scripts/build/tcmalloc.sh | 35 | ||||
-rwxr-xr-x | scripts/build/testing-utils.sh | 14 | ||||
-rwxr-xr-x | scripts/build/uclibc.sh | 37 |
23 files changed, 1348 insertions, 0 deletions
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/scripts/build/klee.sh b/scripts/build/klee.sh new file mode 100755 index 00000000..2b68dd7e --- /dev/null +++ b/scripts/build/klee.sh @@ -0,0 +1,218 @@ +#!/bin/bash -x +# Compile KLEE +# Make sure we exit if there is a failure +set -e + +DIR="$(cd "$(dirname "$0")" && pwd)" +source "${DIR}/common-defaults.sh" + +: ${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="" +############################################################################### +# Handling LLVM configuration +############################################################################### +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 + 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 +fi + +############################################################################### +# klee-uclibc +############################################################################### +if [ "${KLEE_UCLIBC}" != "0" ]; then + 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) +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/:/ /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) +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="${BASE}/stp-${STP_VERSION}-install") + ;; + Z3) + echo "Z3" + 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="${BASE}/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") +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 +############################################################################### +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 + 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 +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[@]} \ + -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\" \ + ${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 +############################################################################### +# 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=$(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 + 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/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/scripts/build/solvers.sh b/scripts/build/solvers.sh new file mode 100755 index 00000000..71ad0c2d --- /dev/null +++ b/scripts/build/solvers.sh @@ -0,0 +1,30 @@ +#!/bin/bash -x +# Make sure we exit if there is a failure +set -e + +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" + "${DIR}/solver-stp.sh" + ;; + Z3) + echo "Z3" + "${DIR}/solver-z3.sh" + ;; + metaSMT) + echo "metaSMT" + "${DIR}/solver-metasmt.sh" + ;; + *) + echo "Unknown solver ${solver}" + exit 1 + esac +done 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 |