Extensive updates to the build script for dependencies and docker

Building/managing dependencies of KLEE are not easy. This script should change
this.

Features:
* script install different versions in their specific directories
  This allows:
  - to have different versions in parallel installed: llvm, solvers
  - to have different optimization levels installed (Debug, no-debug,
    assertions, optimized)
  - to have different versions of instrumentation enabled (address, memory,
    leakage, undefined behavior)
* the script is kept distribution agnostic: assuming basic packages are
  installed (a compiler), use `scripts/build/ubuntu-dependencies.sh` to install
  ubuntu specific ones
* the script does not install any file into system directories (sudo is not
  required) files are only installed into a user specified BASE directory

The same scripts are used for either local setup (`scripts/build/local_install.sh`)
or create a docker image based of your current source folder (`scripts/build/build_docker.sh`)
Change the defaults permanently by modifying (`scripts/build/common-defaults.sh`)
or change them on the fly by providing them as environment variables on the
command line.

The same scripts are also used for TravisCI, so we test what we are using.

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