[TravisCI] Modify TravisCI/Docker build scripts to support doing ASan/UBSan builds

of KLEE.

Two configurations (one for each build system) have been added to
TravisCI to do an ASan build.

7 files changed, 78 insertions, 8 deletions

diff --git a/.travis.yml b/.travis.yml
index 435d5139..a0b5e7ae 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -38,7 +38,6 @@ env:
     #- 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
     #- 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 USE_CMAKE=1
 
-    # TODO: Add ASan build
     # TODO: Add coverage build
     # TODO: Add Doxygen build
 
@@ -47,6 +46,10 @@ env:
     - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1
     - LLVM_VERSION=2.9 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 USE_CMAKE=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_CMAKE=1 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_CMAKE=0 USE_TCMALLOC=0 ASAN_BUILD=1
+
     # TODO: Port all configurations below to CMake build system
 
     # Test we can still build with Z3 in the old build sytem
diff --git a/.travis/klee.sh b/.travis/klee.sh
index 8db724ac..61806df3 100755
--- a/.travis/klee.sh
+++ b/.travis/klee.sh
@@ -112,6 +112,11 @@ else
 fi
 
 ###############################################################################
+# Handle Sanitizer flags
+###############################################################################
+source ${KLEE_SRC}/.travis/sanitizer_flags.sh
+
+###############################################################################
 # KLEE
 ###############################################################################
 mkdir klee
@@ -131,7 +136,8 @@ if [ "X${USE_CMAKE}" == "X1" ]; then
     CMAKE_BUILD_TYPE="Debug"
   fi
   # Compute CMake build type
-  CXXFLAGS="${COVERAGE_FLAGS}" \
+  CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \
+  CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \
   cmake \
     -DLLVM_CONFIG_BINARY="/usr/lib/llvm-${LLVM_VERSION}/bin/llvm-config" \
     -DLLVMCC="${KLEE_CC}" \
@@ -163,11 +169,12 @@ else
               ${KLEE_METASMT_CONFIGURE_OPTION} \
               ${KLEE_UCLIBC_CONFIGURE_OPTION} \
               ${TCMALLOC_OPTION} \
-              CXXFLAGS="${COVERAGE_FLAGS}"
-  make \
-    DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
-    ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
-    ENABLE_SHARED=0
+              CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \
+              CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \
+              LDFLAGS="${SANITIZER_LD_FLAGS}"
+  make  DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
+        ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
+        ENABLE_SHARED=0
 fi
 
 ###############################################################################
diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh
index 7195ceb0..6376c4bc 100755
--- a/.travis/metaSMT.sh
+++ b/.travis/metaSMT.sh
@@ -8,6 +8,12 @@ git clone git://github.com/hoangmle/metaSMT.git
 cd metaSMT
 git clone git://github.com/agra-uni-bremen/dependencies.git
 
+source ${KLEE_SRC}/.travis/sanitizer_flags.sh
+if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then
+  echo "Error: Requested Sanitized build but sanitized build of metaSMT is not implemented"
+  exit 1
+fi
+
 # Bootstrap
 export BOOST_ROOT=/usr
 sudo cp dependencies/Z3-2.19/Z3Config.cmake /usr # this is a hack
diff --git a/.travis/sanitizer_flags.sh b/.travis/sanitizer_flags.sh
new file mode 100644
index 00000000..4d3dce2c
--- /dev/null
+++ b/.travis/sanitizer_flags.sh
@@ -0,0 +1,39 @@
+# 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
+
+# AddressSanitizer
+if [ "X${ASAN_BUILD}" == "X1" ]; then
+  echo "Using ASan"
+  ASAN_CXX_FLAGS="-fsanitize=address -fno-omit-frame-pointer"
+  ASAN_C_FLAGS="${ASAN_CXX_FLAGS}"
+  ASAN_LD_FLAGS="${ASAN_CXX_FLAGS}"
+  IS_SANITIZED_BUILD=1
+else
+  echo "Not using ASan"
+  ASAN_CXX_FLAGS=""
+  ASAN_C_FLAGS=""
+  ASAN_LD_FLAGS=""
+fi
+
+# Undefined Behaviour Sanitizer
+if [ "X${UBSAN_BUILD}" == "X1" ]; then
+  echo "Using UBSan"
+  UBSAN_CXX_FLAGS="-fsanitize=undefined"
+  UBSAN_C_FLAGS="${UBSAN_CXX_FLAGS}"
+  UBSAN_LD_FLAGS="${UBSAN_CXX_FLAGS}"
+  IS_SANITIZED_BUILD=1
+else
+  echo "Not using UBSan"
+  UBSAN_CXX_FLAGS=""
+  UBSAN_C_FLAGS=""
+  UBSAN_LD_FLAGS=""
+fi
+
+# Set variables to be used by clients.
+SANITIZER_CXX_FLAGS="${ASAN_CXX_FLAGS} ${UBSAN_CXX_FLAGS}"
+SANITIZER_C_FLAGS="${ASAN_C_FLAGS} ${UBSAN_C_FLAGS}"
+SANITIZER_LD_FLAGS="${ASAN_LD_FLAGS} ${UBSAN_LD_FLAGS}"
diff --git a/.travis/solvers.sh b/.travis/solvers.sh
index d64c1077..04f3276f 100755
--- a/.travis/solvers.sh
+++ b/.travis/solvers.sh
@@ -16,6 +16,12 @@ for solver in ${SOLVER_LIST}; do
     cd ../
     ;;
   Z3)
+    # FIXME: Move this into its own script
+    source ${KLEE_SRC}/.travis/sanitizer_flags.sh
+    if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then
+      echo "Error: Requested Sanitized build but Z3 being used is not sanitized"
+      exit 1
+    fi
     echo "Z3"
     # Should we install libz3-dbg too?
     sudo apt-get -y install libz3 libz3-dev
diff --git a/.travis/stp.sh b/.travis/stp.sh
index 53b7b6bc..4cc55c62 100755
--- a/.travis/stp.sh
+++ b/.travis/stp.sh
@@ -6,12 +6,17 @@ set -e
 STP_LOG="$(pwd)/stp-build.log"
 
 if [ "x${STP_VERSION}" != "x" ]; then
+    # Get Sanitizer flags
+    source ${KLEE_SRC}/.travis/sanitizer_flags.sh
+
     # Build minisat
     git clone https://github.com/stp/minisat
     cd minisat
     mkdir build
     cd build
     MINISAT_DIR=`pwd`
+    CFLAGS="${SANITIZER_C_FLAGS}" \
+    CXXFLAGS="${SANITIZER_CXX_FLAGS}" \
     cmake -DCMAKE_INSTALL_PREFIX=/usr ..
     make
     sudo make install
@@ -23,6 +28,8 @@ if [ "x${STP_VERSION}" != "x" ]; then
     cd build
     # 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}" \
     cmake -DBUILD_SHARED_LIBS:BOOL=OFF -DENABLE_PYTHON_INTERFACE:BOOL=OFF -DNO_BOOST:BOOL=ON ../src
 
     set +e # Do not exit if build fails because we need to display the log
diff --git a/Dockerfile b/Dockerfile
index 747cbef8..d42b09c8 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -14,7 +14,9 @@ ENV LLVM_VERSION=3.4 \
     KLEE_SRC=/home/klee/klee_src \
     COVERAGE=0 \
     BUILD_DIR=/home/klee/klee_build \
-    USE_CMAKE=1
+    USE_CMAKE=1 \
+    ASAN_BUILD=0 \
+    UBSAN_BUILD=0
 
 RUN apt-get update && \
     apt-get -y --no-install-recommends install \