about summary refs log tree commit diff homepage
path: root/scripts/build
diff options
context:
space:
mode:
Diffstat (limited to 'scripts/build')
-rw-r--r--scripts/build/Dockerfile_base15
-rw-r--r--scripts/build/Dockerfile_klee58
-rw-r--r--scripts/build/Dockerfile_klee_deps33
-rw-r--r--scripts/build/Dockerfile_llvm_build27
-rw-r--r--scripts/build/Dockerfile_solver_build33
-rwxr-xr-xscripts/build/build-docker.sh100
-rwxr-xr-xscripts/build/build-travis-containers.sh22
-rwxr-xr-xscripts/build/build-travis.sh23
-rw-r--r--scripts/build/common-defaults.sh53
-rw-r--r--scripts/build/common-functions217
-rwxr-xr-xscripts/build/dependencies-ubuntu.sh42
-rwxr-xr-xscripts/build/install-klee-deps.sh26
-rwxr-xr-xscripts/build/install-local.sh17
-rwxr-xr-xscripts/build/klee.sh218
-rwxr-xr-xscripts/build/llvm.sh204
-rw-r--r--scripts/build/patches/llvm35.patch14
-rwxr-xr-xscripts/build/solver-metasmt.sh39
-rwxr-xr-xscripts/build/solver-stp.sh57
-rwxr-xr-xscripts/build/solver-z3.sh34
-rwxr-xr-xscripts/build/solvers.sh30
-rwxr-xr-xscripts/build/tcmalloc.sh35
-rwxr-xr-xscripts/build/testing-utils.sh14
-rwxr-xr-xscripts/build/uclibc.sh37
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