[TravisCI] Add ASan/LSan/UBSan suppression files and use them in

CI.

contrib/ci/Dockerfiles/z3_build.Dockerfile

@@ -62,7 +62,8 @@ ENV \
 
 # Build Z3
 RUN mkdir -p "${Z3_SRC_DIR}" && \
-  mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts"
+  mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts" && \
+  mkdir -p "${Z3_SRC_DIR}/contrib/ci/suppressions/sanitizers"
 # Deliberately leave out `contrib`
 ADD /cmake ${Z3_SRC_DIR}/cmake/
 ADD /doc ${Z3_SRC_DIR}/doc/
@@ -89,7 +90,13 @@ RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_docs.sh
 # Test examples
 ADD \
   /contrib/ci/scripts/test_z3_examples_cmake.sh \
+  /contrib/ci/scripts/sanitizer_env.sh \
   ${Z3_SRC_DIR}/contrib/ci/scripts/
+ADD \
+  /contrib/suppressions/sanitizers/asan.txt \
+  /contrib/suppressions/sanitizers/lsan.txt \
+  /contrib/suppressions/sanitizers/ubsan.txt \
+  ${Z3_SRC_DIR}/contrib/suppressions/sanitizers/
 RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_examples_cmake.sh
 
 # Run unit tests

contrib/ci/scripts/sanitizer_env.sh

@@ -0,0 +1,19 @@
+# This script is intended to be included by other
+# scripts and should not be executed directly
+
+: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"}
+: ${ASAN_BUILD?"ASAN_BUILD must be specified"}
+: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
+
+if [ "X${ASAN_BUILD}" = "X1" ]; then
+  # Use suppression files
+  export LSAN_OPTIONS="print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/lsan.txt"
+  export ASAN_OPTIONS="print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/asan.txt"
+fi
+
+if [ "X${UBSAN_BUILD}" = "X1" ]; then
+  # `halt_on_error=1,abort_on_error=1` means that on the first UBSan error
+  # the program will terminate by calling `abort(). Without this UBSan will
+  # allow execution to continue. We also use a suppression file.
+  export UBSAN_OPTIONS="halt_on_error=1,abort_on_error=1,print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/ubsan.txt"
+fi

contrib/ci/scripts/test_z3_examples_cmake.sh

@@ -21,6 +21,9 @@ source ${SCRIPT_DIR}/set_compiler_flags.sh
 # Set CMake generator args
 source ${SCRIPT_DIR}/set_generator_args.sh
 
+# Sanitizer environment variables
+source ${SCRIPT_DIR}/sanitizer_env.sh
+
 cd "${Z3_BUILD_DIR}"
 
 # Build and run C example

contrib/ci/scripts/test_z3_system_tests.sh

@@ -16,6 +16,9 @@ if [ "X${RUN_SYSTEM_TESTS}" != "X1" ]; then
   exit 0
 fi
 
+# Sanitizer environment variables
+source ${SCRIPT_DIR}/sanitizer_env.sh
+
 Z3_EXE="${Z3_BUILD_DIR}/z3"
 Z3_LIB_DIR="${Z3_BUILD_DIR}"
 

contrib/ci/scripts/test_z3_unit_tests_cmake.sh

@@ -13,6 +13,9 @@ set -o pipefail
 # Set CMake generator args
 source ${SCRIPT_DIR}/set_generator_args.sh
 
+# Sanitizer environment variables
+source ${SCRIPT_DIR}/sanitizer_env.sh
+
 cd "${Z3_BUILD_DIR}"
 
 function build_unit_tests() {

contrib/suppressions/README.md

@@ -0,0 +1,7 @@
+# Suppression files
+
+This directory contains suppression files used by various
+program analysis tools.
+
+Suppression files tell a program analysis tool to suppress
+various warnings/errors.

contrib/suppressions/maintainers.txt

@@ -0,0 +1,3 @@
+# Maintainers
+
+- Dan Liew (@delcypher)

contrib/suppressions/sanitizers/README.md

@@ -0,0 +1,4 @@
+# Sanitizer supression files
+
+This directory contains files used to suppress
+ASan/LSan/UBSan warnings/errors.

contrib/suppressions/sanitizers/asan.txt

@@ -0,0 +1 @@
+# AddressSanitizer suppression file

contrib/suppressions/sanitizers/lsan.txt

@@ -0,0 +1 @@
+# LeakSanitizer suppression file

contrib/suppressions/sanitizers/ubsan.txt

@@ -0,0 +1 @@
+# UndefinedBehavior sanitizer suppression file