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.

1 files changed, 22 insertions, 60 deletions

diff --git a/.travis.yml b/.travis.yml
index 5a8a6e45..c8de1292 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,6 +1,8 @@
 sudo: required
 dist: trusty
 language: cpp
+services:
+    - docker
 compiler:
     # FIXME: For now, building with Clang is disabled because the STP built with
     # it hits an assertion failure during some tests. We should sort this out
@@ -32,25 +34,25 @@ env:
     #   COVERAGE: {0, 1}
     #   USE_TCMALLOC: {0, 1}
 
-    # COVERAGE when set indicates that coverage data should be uploaded to the service, only ONE job should have COVERAGE set
+    # COVERAGE when set indicates that coverage data should be uploaded to the service
 
     matrix:
 
     # TODO: Add Doxygen build
 
     # Check newer LLVMs
-    - LLVM_VERSION=3.7 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
-    - LLVM_VERSION=3.6 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
-    - LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
-
-    - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
-    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
+    - LLVM_VERSION=3.7 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
+    - LLVM_VERSION=3.6 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
+    - LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
+    - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
+    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 REQUIRES_RTTI=1
 
     # ASan build. Do unoptimized build otherwise the optimizer might remove problematic code
-    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_TCMALLOC=0 ASAN_BUILD=1
+    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_TCMALLOC=0 SANITIZER_BUILD=address
+    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_TCMALLOC=0 SANITIZER_BUILD=undefined
 
     # Test just using Z3
-    - LLVM_VERSION=3.4 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=3.4 SOLVERS=Z3 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
 
     # Test we can build against STP master
     - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
@@ -59,7 +61,7 @@ env:
     - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
 
     # Test metaSMT support
-    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=BTOR KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=BTOR KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 REQUIRES_RTTI=1
 
     # Check at least one build with Asserts disabled.
     - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0
@@ -71,78 +73,38 @@ env:
     - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
 
     # Coverage build
-    - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=1 USE_TCMALLOC=0
+    - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=1 USE_TCMALLOC=0
     global:
     - secure: EF/WAc4BdIRUchF3mjATN3/UwtGWtGaRgb5oIIJHjKhgZFdPsgWsXFgaOB0jaK2hfO/svj/LvlasuRIGxeePVjeaiX8ZlVpuHiX67vdYLY+0kCDRwkusRjm60/GbPU9O/Xjgb/d4aWAEkoq5OnsprVTEvU8iY2JHtAqgwR+wW9I=
     - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw=
     - secure: DQAEQWJblXvIztN/sgH63OtFncI+Qju6wRy1zIV/iLf5KbAmLs1h3itU7EsE/+3+LgV1MVQ5QNJDBUj17A6VHRKNaQ5qnIllTAcC3o0nPDohQkQoCgDG8HZ+M4wtVfr7q2K6byEPB2UbSH+mEjSMTihJufgBBVfKyyozAfYycjg=
+    - KLEE_TRAVIS_BUILD: 1
+    - REPOSITORY: klee
 
 matrix:
   include:
     - os: osx
       osx_image: xcode8.3
-      env: LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=0
-
-addons:
-  apt:
-    sources:
-    - sourceline: 'ppa:ubuntu-toolchain-r/test'
-    - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.4 main'
-      key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
-    - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.5 main'
-      key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
-    - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.6 main'
-      key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
-    - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.7 main'
-      key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
-    - sourceline: 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_14.04/ /'
-      key_url: 'http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_14.04/Release.key'
-    packages:
-    - gcc-4.8
-    - g++-4.8
-    - libboost-program-options-dev
-    - libcap-dev
-    - libedit-dev
-    - libselinux1-dev
-    - cmake
-    - lcov
+      env: LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=0
 
 cache:
   ccache: true
   apt: true
   directories:
     - $HOME/Library/Caches/Homebrew
+
 before_install:
     ###########################################################################
     # Set up the locations to get various packages from
     # We assume the Travis image uses Ubuntu 14.04 LTS
     ###########################################################################
     # Update package information
-    - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then sudo apt-get update; fi
-    - if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then brew update && brew tap klee/klee && brew install ccache && export PATH="/usr/local/opt/ccache/libexec:$PATH" ; fi
-    ###########################################################################
-    # Set up out of source build directory
-    ###########################################################################
     - export KLEE_SRC=`pwd`
+    - export KLEE_SRC_TRAVIS=`pwd`
     - cd ../
-    - mkdir build
-    - cd build/
-    - export BUILD_DIR=`pwd`
-    ###########################################################################
-    # Install stuff
-    ###########################################################################
-    # Install LLVM and the LLVM bitcode compiler we require to build KLEE
-    - ${KLEE_SRC}/.travis/install-llvm-and-runtime-compiler.sh
-    - ${KLEE_SRC}/.travis/install-tcmalloc.sh
-    # Install lit (llvm-lit is not available)
-    - sudo pip2 install lit
-    # Get SMT solvers
-    - ${KLEE_SRC}/.travis/solvers.sh
-    # Get needed utlities/libraries for testing KLEE
-    - mkdir test-utils/
-    - cd test-utils/
-    - ${KLEE_SRC}/.travis/testing-utils.sh
-    - cd ../
+    - export BASE=`pwd`
+    - ${KLEE_SRC_TRAVIS}/scripts/build/build-travis.sh
 script:
     # Build KLEE and run tests
-    - ${KLEE_SRC}/.travis/klee.sh
+    - if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then export PATH="/usr/local/opt/ccache/libexec:$PATH"; ${KLEE_SRC_TRAVIS}/scripts/build/klee.sh; fi
+    - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then ${KLEE_SRC_TRAVIS}/scripts/build/build-docker.sh; fi