diff options
Diffstat (limited to '.travis')
| -rwxr-xr-x | .travis/klee.sh | 19 | ||||
| -rwxr-xr-x | .travis/metaSMT.sh | 6 | ||||
| -rw-r--r-- | .travis/sanitizer_flags.sh | 39 | ||||
| -rwxr-xr-x | .travis/solvers.sh | 6 | ||||
| -rwxr-xr-x | .travis/stp.sh | 7 |
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 |