[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.

5 files changed, 71 insertions, 6 deletions

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