Add TravisCI and Docker support for building KLEE with Z3 support

4 files changed, 83 insertions, 22 deletions

diff --git a/.travis.yml b/.travis.yml
index 07ef8a01..9a17f968 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -19,30 +19,35 @@ env:
 
     # Check the matrix of:
     #   LLVM  : {2.9, 3.4}
-    #   STP   : {2.1.0, master}
+    #   SOLVERS : {Z3, STP, STP:Z3}
+    #   STP_VERSION   : {2.1.0, master}
     #   UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled
     # with Asserts enabled.
 
     # COVERAGE set indicated that coverage data should be uplaoded to the server, only ONE job should have COVERAGE set
 
-    # FIXME: Enable when we want to test LLVM3.5
     matrix:
-    #- LLVM_VERSION=3.5 STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1
+    # Test experimental Z3 support
+    - 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=STP:Z3 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    # FIXME: Enable when we want to test LLVM3.5
+    #- LLVM_VERSION=3.5 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1
     #- LLVM_VERSION=3.5 STP_VERSION=master KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1
-    - LLVM_VERSION=3.4 STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=1
-    - LLVM_VERSION=3.4 STP_VERSION=master KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
-    - LLVM_VERSION=2.9 STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
-    - LLVM_VERSION=2.9 STP_VERSION=master KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
-    - LLVM_VERSION=3.4 STP_VERSION=2.1.0 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
-    - LLVM_VERSION=3.4 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
-    - LLVM_VERSION=2.9 STP_VERSION=2.1.0 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
-    - LLVM_VERSION=2.9 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=1
+    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+
 
     # Check at least one build with Asserts disabled.
-    - LLVM_VERSION=2.9 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0
 
     # Check at least one Debug+Asserts build
-    - LLVM_VERSION=3.4 STP_VERSION=master KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0
+    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0
     global:
     - secure: EF/WAc4BdIRUchF3mjATN3/UwtGWtGaRgb5oIIJHjKhgZFdPsgWsXFgaOB0jaK2hfO/svj/LvlasuRIGxeePVjeaiX8ZlVpuHiX67vdYLY+0kCDRwkusRjm60/GbPU9O/Xjgb/d4aWAEkoq5OnsprVTEvU8iY2JHtAqgwR+wW9I=
     - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw=
@@ -58,11 +63,13 @@ before_install:
     - sudo sh -c 'echo "deb-src http://llvm.org/apt/precise/ llvm-toolchain-precise-3.4 main" >> /etc/apt/sources.list.d/llvm.list'
     - sudo sh -c 'echo "deb http://llvm.org/apt/precise/ llvm-toolchain-precise-3.5 main" >> /etc/apt/sources.list.d/llvm.list'
     - sudo sh -c 'echo "deb-src http://llvm.org/apt/precise/ llvm-toolchain-precise-3.5 main" >> /etc/apt/sources.list.d/llvm.list'
+    - sudo sh -c "echo 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_12.04/ /' >> /etc/apt/sources.list.d/z3.list"
     # Needed for CMake
     - sudo add-apt-repository -y ppa:ubuntu-sdk-team/ppa
     # Needed for new libstdc++ and gcc4.8
     - sudo add-apt-repository --yes ppa:ubuntu-toolchain-r/test/
     - wget -O - http://llvm.org/apt/llvm-snapshot.gpg.key|sudo apt-key add -
+    - wget -O - http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_12.04/Release.key | sudo apt-key add -
     - sudo apt-get update
     ###########################################################################
     # Set up out of source build directory
@@ -87,11 +94,8 @@ before_install:
     - ${KLEE_SRC}/.travis/install-llvm-and-runtime-compiler.sh
     # Install lit (llvm-lit is not available)
     - sudo pip install lit
-    # Build STP
-    - mkdir stp
-    - cd stp
-    - ${KLEE_SRC}/.travis/stp.sh
-    - cd ../
+    # Get SMT solvers
+    - ${KLEE_SRC}/.travis/solvers.sh
 script:
     # Get needed utlities/libraries for testing KLEE
     - mkdir test-utils/
diff --git a/.travis/klee.sh b/.travis/klee.sh
index fbce61e7..0f855b46 100755
--- a/.travis/klee.sh
+++ b/.travis/klee.sh
@@ -1,6 +1,7 @@
 #!/bin/bash -x
 # Make sure we exit if there is a failure
 set -e
+: ${SOLVERS?"Solvers must be specified"}
 
 # Calculate LLVM branch name to retrieve missing files from
 SVN_BRANCH="release_$( echo ${LLVM_VERSION} | sed 's/\.//g')"
@@ -43,6 +44,30 @@ COVERAGE_FLAGS=""
 if [ ${COVERAGE} -eq 1 ]; then
     COVERAGE_FLAGS='-fprofile-arcs -ftest-coverage'
 fi
+
+
+###############################################################################
+# Handle setting up solver configure flags for KLEE
+###############################################################################
+KLEE_Z3_CONFIGURE_OPTION=""
+KLEE_STP_CONFIGURE_OPTION=""
+SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /')
+
+for solver in ${SOLVER_LIST}; do
+  echo "Setting configuration option for ${solver}"
+  case ${solver} in
+  STP)
+    KLEE_STP_CONFIGURE_OPTION="--with-stp=${BUILD_DIR}/stp/build"
+    ;;
+  Z3)
+    echo "Z3"
+    KLEE_Z3_CONFIGURE_OPTION="--with-z3=/usr"
+    ;;
+  *)
+    echo "Unknown solver ${solver}"
+    exit 1
+  esac
+done
 ###############################################################################
 # KLEE
 ###############################################################################
@@ -57,7 +82,8 @@ ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \
             --with-llvmobj=/usr/lib/llvm-${LLVM_VERSION}/build \
             --with-llvmcc=${KLEE_CC} \
             --with-llvmcxx=${KLEE_CXX} \
-            --with-stp="${BUILD_DIR}/stp/build" \
+            ${KLEE_STP_CONFIGURE_OPTION} \
+            ${KLEE_Z3_CONFIGURE_OPTION} \
             ${KLEE_UCLIBC_CONFIGURE_OPTION} \
             CXXFLAGS="${COVERAGE_FLAGS}" \
             && make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
diff --git a/.travis/solvers.sh b/.travis/solvers.sh
new file mode 100755
index 00000000..db717f2d
--- /dev/null
+++ b/.travis/solvers.sh
@@ -0,0 +1,27 @@
+#!/bin/bash -x
+# Make sure we exit if there is a failure
+set -e
+: ${SOLVERS?"Solvers must be specified"}
+
+SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /')
+
+for solver in ${SOLVER_LIST}; do
+  echo "Getting solver ${solver}"
+  case ${solver} in
+  STP)
+    echo "STP"
+    mkdir stp
+    cd stp
+    ${KLEE_SRC}/.travis/stp.sh
+    cd ../
+    ;;
+  Z3)
+    echo "Z3"
+    # Should we install libz3-dbg too?
+    sudo apt-get -y install libz3 libz3-dev
+    ;;
+  *)
+    echo "Unknown solver ${solver}"
+    exit 1
+  esac
+done
diff --git a/Dockerfile b/Dockerfile
index a61f8353..aa3ca6b6 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -6,6 +6,7 @@ MAINTAINER Dan Liew <daniel.liew@imperial.ac.uk>
 # the resulting image is unnecessarily large!
 
 ENV LLVM_VERSION=3.4 \
+    SOLVERS=STP:Z3 \
     STP_VERSION=master \
     DISABLE_ASSERTIONS=0 \
     ENABLE_OPTIMIZED=1 \
@@ -40,7 +41,10 @@ RUN apt-get update && \
         unzip \
         binutils && \
     pip3 install -U lit tabulate && \
-    update-alternatives --install /usr/bin/python python /usr/bin/python3 50
+    update-alternatives --install /usr/bin/python python /usr/bin/python3 50 && \
+    ( wget -O - http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_14.04/Release.key | apt-key add - ) && \
+    echo 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_14.04/ /' >> /etc/apt/sources.list.d/z3.list && \
+    apt-get update
 
 # Create ``klee`` user for container with password ``klee``.
 # and give it password-less sudo access (temporarily so we can use the TravisCI scripts)
@@ -79,8 +83,8 @@ RUN sudo chown --recursive klee: ${KLEE_SRC}
 # Create build directory
 RUN mkdir -p ${BUILD_DIR}
 
-# Build STP (use TravisCI script)
-RUN cd ${BUILD_DIR} && mkdir stp && cd stp && ${KLEE_SRC}/.travis/stp.sh
+# Build/Install SMT solvers (use TravisCI script)
+RUN cd ${BUILD_DIR} && ${KLEE_SRC}/.travis/solvers.sh
 
 # Install testing utils (use TravisCI script)
 RUN cd ${BUILD_DIR} && mkdir testing-utils && cd testing-utils && \