Merge branch 'master' of https://github.com/Z3Prover/z3

.travis.yml

@@ -17,6 +17,15 @@ env:
 ###############################################################################
 # Ubuntu 16.04 LTS
 ###############################################################################
+    # 64-bit UBSan Debug build
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug UBSAN_BUILD=1 RUN_UNIT_TESTS=SKIP
+    # 64-bit ASan Debug build
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so
+    # Build for running unit tests under ASan/UBSan
+    # FIXME: We should really be doing a debug build but the unit tests run too
+    # slowly when we do that.
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo ASAN_BUILD=1 RUN_UNIT_TESTS=BUILD_AND_RUN ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so UBSAN_BUILD=1 RUN_API_EXAMPLES=0 RUN_SYSTEM_TESTS=0 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0
+
     # 64-bit GCC 5.4 RelWithDebInfo
     - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo
     # 64-bit Clang 3.9 RelWithDebInfo

README-CMake.md

@@ -270,6 +270,7 @@ The following useful options can be passed to CMake whilst configuring.
 * ``API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature.
 * ``WARNINGS_AS_ERRORS`` - STRING. If set to ``TRUE`` compiler warnings will be treated as errors. If set to ``False`` compiler warnings will not be treated as errors.
     If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors.
+* ``Z3_C_EXAMPLES_FORCE_CXX_LINKER`` - BOOL. If set to ``TRUE`` the C API examples will request that the C++ linker is used rather than the C linker.
 
 On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface.
 

contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile

@@ -30,6 +30,7 @@ RUN apt-get update && \
         libgomp1 \
         libomp5 \
         libomp-dev \
+        llvm-3.9 \
         make \
         mono-devel \
         ninja-build \
@@ -47,4 +48,4 @@ RUN useradd -m user && \
     echo 'user  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
 USER user
 WORKDIR /home/user
-
+ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer

contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile

@@ -16,6 +16,7 @@ RUN apt-get update && \
         libgmp-dev \
         libgomp1 \
         lib32gomp1 \
+        llvm-3.9 \
         make \
         mono-devel \
         ninja-build \
@@ -32,4 +33,4 @@ RUN useradd -m user && \
     echo 'user  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
 USER user
 WORKDIR /home/user
-
+ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer

contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile

@@ -18,6 +18,7 @@ RUN apt-get update && \
         libgomp1 \
         libomp5 \
         libomp-dev \
+        llvm-3.9 \
         make \
         mono-devel \
         ninja-build \
@@ -35,4 +36,4 @@ RUN useradd -m user && \
     echo 'user  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
 USER user
 WORKDIR /home/user
-
+ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer

contrib/ci/Dockerfiles/z3_build.Dockerfile

@@ -5,6 +5,7 @@ FROM ${DOCKER_IMAGE_BASE}
 # Build arguments. This can be changed when invoking
 # `docker build`.
 ARG ASAN_BUILD
+ARG ASAN_DSO
 ARG BUILD_DOCS
 ARG CC
 ARG CXX
@@ -13,8 +14,10 @@ ARG JAVA_BINDINGS
 ARG NO_SUPPRESS_OUTPUT
 ARG PYTHON_BINDINGS
 ARG PYTHON_EXECUTABLE=/usr/bin/python2.7
+ARG RUN_API_EXAMPLES
 ARG RUN_SYSTEM_TESTS
 ARG RUN_UNIT_TESTS
+ARG SANITIZER_PRINT_SUPPRESSIONS
 ARG TARGET_ARCH
 ARG TEST_INSTALL
 ARG UBSAN_BUILD
@@ -32,6 +35,7 @@ ARG Z3_VERBOSE_BUILD_OUTPUT
 
 ENV \
   ASAN_BUILD=${ASAN_BUILD} \
+  ASAN_DSO=${ASAN_DSO} \
   BUILD_DOCS=${BUILD_DOCS} \
   CC=${CC} \
   CXX=${CXX} \
@@ -40,6 +44,8 @@ ENV \
   NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT} \
   PYTHON_BINDINGS=${PYTHON_BINDINGS} \
   PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \
+  SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS} \
+  RUN_API_EXAMPLES=${RUN_API_EXAMPLES} \
   RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS} \
   RUN_UNIT_TESTS=${RUN_UNIT_TESTS} \
   TARGET_ARCH=${TARGET_ARCH} \
@@ -50,6 +56,7 @@ ENV \
   USE_OPENMP=${USE_OPENMP} \
   Z3_SRC_DIR=${Z3_SRC_DIR} \
   Z3_BUILD_DIR=/home/user/z3_build \
+  Z3_BUILD_TYPE=${Z3_BUILD_TYPE} \
   Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR} \
   Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT} \
   Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \
@@ -62,7 +69,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/suppressions/sanitizers"
 # Deliberately leave out `contrib`
 ADD /cmake ${Z3_SRC_DIR}/cmake/
 ADD /doc ${Z3_SRC_DIR}/doc/
@@ -89,7 +97,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/README.md

@@ -30,8 +30,10 @@ the future.
 * `JAVA_BINDINGS` - Build and test Java API bindings (`0` or `1`)
 * `NO_SUPPRESS_OUTPUT` - Don't suppress output of some commands (`0` or `1`)
 * `PYTHON_BINDINGS` - Build and test Python API bindings (`0` or `1`)
+* `RUN_API_EXAMPLES` - Build and run API examples (`0` or `1`)
 * `RUN_SYSTEM_TESTS` - Run system tests (`0` or `1`)
 * `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`)
+* `SANITIZER_PRINT_SUPPRESSIONS` - Show ASan/UBSan suppressions (`0` or `1`)
 * `TARGET_ARCH` - Target architecture (`x86_64` or `i686`)
 * `TEST_INSTALL` - Test running `install` target (`0` or `1`)
 * `UBSAN_BUILD` - Do [UndefinedBehaviourSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) build (`0` or `1`)

contrib/ci/scripts/build_z3_cmake.sh

@@ -22,6 +22,7 @@ set -o pipefail
 : ${USE_LTO?"USE_LTO must be specified"}
 : ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX must be specified"}
 : ${Z3_WARNINGS_AS_ERRORS?"Z3_WARNINGS_AS_ERRORS must be specified"}
+: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
 
 ADDITIONAL_Z3_OPTS=()
 
@@ -105,6 +106,16 @@ fi
 # Set compiler flags
 source ${SCRIPT_DIR}/set_compiler_flags.sh
 
+if [ "X${UBSAN_BUILD}" = "X1" ]; then
+  # HACK: When building with UBSan the C++ linker
+  # must be used to avoid the following linker errors.
+  # undefined reference to `__ubsan_vptr_type_cache'
+  # undefined reference to `__ubsan_handle_dynamic_type_cache_miss'
+  ADDITIONAL_Z3_OPTS+=( \
+    '-DZ3_C_EXAMPLES_FORCE_CXX_LINKER=ON' \
+  )
+fi
+
 # Sanity check
 if [ ! -e "${Z3_SRC_DIR}/CMakeLists.txt" ]; then
   echo "Z3_SRC_DIR is invalid"

contrib/ci/scripts/ci_defaults.sh

@@ -9,8 +9,13 @@ export DOTNET_BINDINGS="${DOTNET_BINDINGS:-1}"
 export JAVA_BINDINGS="${JAVA_BINDINGS:-1}"
 export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}"
 export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}"
+export RUN_API_EXAMPLES="${RUN_API_EXAMPLES:-1}"
 export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
 export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}"
+# Don't print suppressions by default because that breaks the Z3
+# regression tests because they don't expect them to appear in Z3's
+# output.
+export SANITIZER_PRINT_SUPPRESSIONS="${SANITIZER_PRINT_SUPPRESSIONS:-0}"
 export TARGET_ARCH="${TARGET_ARCH:-x86_64}"
 export TEST_INSTALL="${TEST_INSTALL:-1}"
 export UBSAN_BUILD="${UBSAN_BUILD:-0}"
@@ -49,6 +54,7 @@ unset PLATFORM
 # NOTE: The following variables are not set here because
 # they are specific to the CI implementation
 # PYTHON_EXECUTABLE
+# ASAN_DSO
 # Z3_SRC_DIR
 # Z3_BUILD_DIR
 # Z3_SYSTEM_TEST_DIR

contrib/ci/scripts/run_quiet.sh

@@ -34,8 +34,8 @@ function run_quiet() {
     fi
     # Clean up
     rm "${STDOUT}" "${STDERR}"
-    [ $( echo "${OLD_SETTINGS}" | grep -c 'e') -ne 0 ] && set -e
-    [ $( echo "${OLD_SETTINGS}" | grep -c 'x') -ne 0 ] && set -x
+    [ "$( echo "${OLD_SETTINGS}" | grep -c 'e')" != "0" ] && set -e
+    [ "$( echo "${OLD_SETTINGS}" | grep -c 'x')" != "0" ] && set -x
     return ${EXIT_STATUS}
   fi
 }

contrib/ci/scripts/sanitizer_env.sh

@@ -0,0 +1,82 @@
+# 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="suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/lsan.txt"
+  # NOTE: If you get bad stacktraces try using `fast_unwind_on_malloc=0`
+  # NOTE: `malloc_context_size` controls size of recorded stacktrace for allocations.
+  #       If the reported stacktraces appear incomplete try increasing the value.
+  export ASAN_OPTIONS="malloc_context_size=100,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/asan.txt"
+
+  : ${SANITIZER_PRINT_SUPPRESSIONS?"SANITIZER_PRINT_SUPPRESSIONS must be specified"}
+  if [ "X${SANITIZER_PRINT_SUPPRESSIONS}" = "X1" ]; then
+    export LSAN_OPTIONS="${LSAN_OPTIONS},print_suppressions=1"
+    export ASAN_OPTIONS="${ASAN_OPTIONS},print_suppressions=1"
+  else
+    export LSAN_OPTIONS="${LSAN_OPTIONS},print_suppressions=0"
+    export ASAN_OPTIONS="${ASAN_OPTIONS},print_suppressions=0"
+  fi
+
+  : ${ASAN_SYMBOLIZER_PATH?"ASAN_SYMBOLIZER_PATH must be specified"}
+
+  # Run command without checking for leaks
+  function run_no_lsan() {
+    ASAN_OPTIONS="${ASAN_OPTIONS},detect_leaks=0" "${@}"
+  }
+
+  # Check path to ASan DSO
+  : ${ASAN_DSO?"ASAN_DSO must be specified"}
+  if [ ! -e "${ASAN_DSO}" ]; then
+    echo "ASAN_DSO (${ASAN_DSO}) does not exist"
+    exit 1
+  fi
+  # FIXME: We'll need to refactor this when we can do UBSan builds
+  # against a UBSan DSO.
+  function run_non_native_binding() {
+    # We need to preload the ASan DSO that libz3
+    # will have undefined references to.
+    # Don't run leak checking because we get lots reported leaks
+    # in the language runtime (e.g. python).
+    PLATFORM="$(uname -s)"
+    case "${PLATFORM}" in
+      Linux*)
+        LD_PRELOAD="${ASAN_DSO}" run_no_lsan "${@}"
+      ;;
+      Darwin*)
+        DYLD_INSERT_LIBRARIES="${ASAN_DSO}" run_no_lsan "${@}"
+      ;;
+      *)
+        echo "Unknown platform \"${PLATFORM}\""
+        exit 1
+      ;;
+    esac
+    unset PLATFORM
+  }
+else
+  # In non-ASan build just run directly
+  function run_no_lsan() {
+    "${@}"
+  }
+  function run_non_native_binding() {
+    "${@}"
+  }
+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,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/ubsan.txt"
+
+  : ${SANITIZER_PRINT_SUPPRESSIONS?"SANITIZER_PRINT_SUPPRESSIONS must be specified"}
+  if [ "X${SANITIZER_PRINT_SUPPRESSIONS}" = "X1" ]; then
+    export UBSAN_OPTIONS="${UBSAN_OPTIONS},print_suppressions=1"
+  else
+    export UBSAN_OPTIONS="${UBSAN_OPTIONS},print_suppressions=0"
+  fi
+fi

contrib/ci/scripts/test_z3_examples_cmake.sh

@@ -14,6 +14,13 @@ set -o pipefail
 : ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
 : ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"}
 : ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"}
+: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
+: ${RUN_API_EXAMPLES?"RUN_API_EXAMPLES must be specified"}
+
+if [ "X${RUN_API_EXAMPLES}" = "X0" ]; then
+  echo "Skipping run of API examples"
+  exit 0
+fi
 
 # Set compiler flags
 source ${SCRIPT_DIR}/set_compiler_flags.sh
@@ -21,6 +28,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
@@ -38,9 +48,21 @@ run_quiet examples/tptp_build_dir/z3_tptp5 -help
 
 # Build an run c_maxsat_example
 cmake --build $(pwd) --target c_maxsat_example "${GENERATOR_ARGS[@]}"
-run_quiet \
-  examples/c_maxsat_example_build_dir/c_maxsat_example \
-  ${Z3_SRC_DIR}/examples/maxsat/ex.smt
+# FIXME: It is known that the maxsat example leaks memory and the
+# the Z3 developers have stated this is "wontfix".
+# See https://github.com/Z3Prover/z3/issues/1299
+run_no_lsan \
+  run_quiet \
+    examples/c_maxsat_example_build_dir/c_maxsat_example \
+    ${Z3_SRC_DIR}/examples/maxsat/ex.smt
+
+if [ "X${UBSAN_BUILD}" = "X1" ]; then
+  # FIXME: We really need libz3 to link against a shared UBSan runtime.
+  # Right now we link against the static runtime which breaks all the
+  # non-native language bindings.
+  echo "FIXME: Can't run other examples when building with UBSan"
+  exit 0
+fi
 
 
 if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
@@ -48,16 +70,21 @@ if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
   # `all_interval_series.py` produces a lot of output so just throw
   # away output.
   # TODO: This example is slow should we remove it from testing?
-  run_quiet ${PYTHON_EXECUTABLE} python/all_interval_series.py
-  run_quiet ${PYTHON_EXECUTABLE} python/complex.py
-  run_quiet ${PYTHON_EXECUTABLE} python/example.py
+  if [ "X${ASAN_BUILD}" = "X1" -a "X${Z3_BUILD_TYPE}" = "XDebug" ]; then
+    # Too slow when doing ASan Debug build
+    echo "Skipping all_interval_series.py under ASan Debug build"
+  else
+    run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/all_interval_series.py
+  fi
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/complex.py
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/example.py
   # FIXME: `hamiltonian.py` example is disabled because its too slow.
   #${PYTHON_EXECUTABLE} python/hamiltonian.py
-  run_quiet ${PYTHON_EXECUTABLE} python/marco.py
-  run_quiet ${PYTHON_EXECUTABLE} python/mss.py
-  run_quiet ${PYTHON_EXECUTABLE} python/socrates.py
-  run_quiet ${PYTHON_EXECUTABLE} python/visitor.py
-  run_quiet ${PYTHON_EXECUTABLE} python/z3test.py
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/marco.py
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/mss.py
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/socrates.py
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/visitor.py
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/z3test.py
 fi
 
 if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
@@ -65,7 +92,7 @@ if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
   # FIXME: Move compliation step into CMake target
   mcs ${Z3_SRC_DIR}/examples/dotnet/Program.cs /target:exe /out:dotnet_test.exe /reference:Microsoft.Z3.dll /r:System.Numerics.dll
   # Run .NET example
-  run_quiet mono ./dotnet_test.exe
+  run_quiet run_non_native_binding mono ./dotnet_test.exe
 fi
 
 if [ "X${JAVA_BINDINGS}" = "X1" ]; then
@@ -82,6 +109,14 @@ if [ "X${JAVA_BINDINGS}" = "X1" ]; then
     # Assume Linux for now
     export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH}
   fi
-  run_quiet java -cp .:examples/java:com.microsoft.z3.jar JavaExample
+  if [ "X${ASAN_BUILD}" = "X1" ]; then
+    # The JVM seems to crash (SEGV) if we pre-load ASan
+    # so don't run it for now.
+    echo "Skipping JavaExample under ASan build"
+  else
+    run_quiet \
+      run_non_native_binding \
+        java -cp .:examples/java:com.microsoft.z3.jar JavaExample
+  fi
 fi
 

contrib/ci/scripts/test_z3_system_tests.sh

@@ -10,12 +10,17 @@ set -o pipefail
 : ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"}
 : ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
 : ${Z3_SYSTEM_TEST_DIR?"Z3_SYSTEM_TEST_DIR must be specified"}
+: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
 
 if [ "X${RUN_SYSTEM_TESTS}" != "X1" ]; then
   echo "Skipping system tests"
   exit 0
 fi
 
+# Sanitizer environment variables
+SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
+source ${SCRIPT_DIR}/sanitizer_env.sh
+
 Z3_EXE="${Z3_BUILD_DIR}/z3"
 Z3_LIB_DIR="${Z3_BUILD_DIR}"
 
@@ -23,7 +28,7 @@ Z3_LIB_DIR="${Z3_BUILD_DIR}"
 Z3_SYSTEM_TEST_GIT_URL="${Z3_GIT_URL:-https://github.com/Z3Prover/z3test.git}"
 
 # Clone repo to destination
-mkdir -p "${Z3_SYSTEM_TEST_GIT_URL}"
+mkdir -p "${Z3_SYSTEM_TEST_DIR}"
 git clone "${Z3_SYSTEM_TEST_GIT_URL}" "${Z3_SYSTEM_TEST_DIR}"
 cd "${Z3_SYSTEM_TEST_DIR}"
 
@@ -48,7 +53,18 @@ fi
 
 if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
   # Run python binding tests
-  ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/
+  if [ "X${UBSAN_BUILD}" = "X1" ]; then
+    # FIXME: We need to build libz3 with a shared UBSan runtime for the bindings
+    # to work.
+    echo "FIXME: Skipping python binding tests when building with UBSan"
+  elif [ "X${ASAN_BUILD}" = "X1" ]; then
+    # FIXME: The `test_pyscripts.py` doesn't propagate LD_PRELOAD
+    # so under ASan the tests fail to run
+    # to work.
+    echo "FIXME: Skipping python binding tests when building with ASan"
+  else
+    run_non_native_binding ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/
+  fi
 fi
 
 # FIXME: Run `scripts/test_cs.py` once it has been modified to support mono

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/ci/scripts/travis_ci_linux_entry_point.sh

@@ -84,6 +84,14 @@ if [ -n "${ASAN_BUILD}" ]; then
   BUILD_OPTS+=("--build-arg" "ASAN_BUILD=${ASAN_BUILD}")
 fi
 
+if [ -n "${ASAN_DSO}" ]; then
+  BUILD_OPTS+=("--build-arg" "ASAN_DSO=${ASAN_DSO}")
+fi
+
+if [ -n "${SANITIZER_PRINT_SUPPRESSIONS}" ]; then
+  BUILD_OPTS+=("--build-arg" "SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS}")
+fi
+
 if [ -n "${UBSAN_BUILD}" ]; then
   BUILD_OPTS+=("--build-arg" "UBSAN_BUILD=${UBSAN_BUILD}")
 fi
@@ -92,6 +100,10 @@ if [ -n "${TEST_INSTALL}" ]; then
   BUILD_OPTS+=("--build-arg" "TEST_INSTALL=${TEST_INSTALL}")
 fi
 
+if [ -n "${RUN_API_EXAMPLES}" ]; then
+  BUILD_OPTS+=("--build-arg" "RUN_API_EXAMPLES=${RUN_API_EXAMPLES}")
+fi
+
 if [ -n "${RUN_SYSTEM_TESTS}" ]; then
   BUILD_OPTS+=("--build-arg" "RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS}")
 fi

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,5 @@
+# LeakSanitizer suppression file
+
+# Ignore Clang OpenMP leaks.
+# See https://github.com/Z3Prover/z3/issues/1308
+leak:___kmp_allocate

contrib/suppressions/sanitizers/ubsan.txt

@@ -0,0 +1,7 @@
+# UndefinedBehavior sanitizer suppression file
+# FIXME: UBSan doesn't usually have false positives so we need to fix all of these!
+
+# Occurs when running tptp example
+# See https://github.com/Z3Prover/z3/issues/964
+null:rational.h
+null:mpq.h

examples/CMakeLists.txt

@@ -7,6 +7,30 @@ else()
   set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "")
 endif()
 
+option(Z3_C_EXAMPLES_FORCE_CXX_LINKER
+  "Force C++ linker when building C example projects" OFF)
+
+if (Z3_C_EXAMPLES_FORCE_CXX_LINKER)
+  # HACK: This is a workaround for UBSan.
+  message(STATUS "Forcing C++ linker to be used when building example C projects")
+  set(EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG
+    "-DFORCE_CXX_LINKER=ON"
+  )
+else()
+  set(EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG "")
+endif()
+
+if (DEFINED CMAKE_CONFIGURATION_TYPES)
+  message(WARNING
+    "Cannot set built type of external project when building with a "
+    "multi-configuration generator")
+  set(EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG "")
+else()
+  set(EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG
+    "-DCMAKE_BUILD_TYPE:STRING=${CMAKE_BUILD_TYPE}"
+  )
+endif()
+
 ################################################################################
 # Build example project using libz3's C API as an external project
 ################################################################################
@@ -14,7 +38,10 @@ ExternalProject_Add(c_example
   DEPENDS libz3
   # Configure step
   SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c"
-  CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+  CMAKE_ARGS
+    "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+    "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}"
+    "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
   # Build step
   ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
   BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir"
@@ -30,7 +57,10 @@ ExternalProject_Add(c_maxsat_example
   DEPENDS libz3
   # Configure step
   SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/maxsat"
-  CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+  CMAKE_ARGS
+    "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+    "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}"
+    "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
   # Build step
   ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
   BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_maxsat_example_build_dir"
@@ -47,7 +77,9 @@ ExternalProject_Add(cpp_example
   DEPENDS libz3
   # Configure step
   SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c++"
-  CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+  CMAKE_ARGS
+    "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+    "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
   # Build step
   ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
   BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/cpp_example_build_dir"
@@ -63,7 +95,9 @@ ExternalProject_Add(z3_tptp5
   DEPENDS libz3
   # Configure step
   SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/tptp"
-  CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+  CMAKE_ARGS
+    "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+    "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
   # Build step
   ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
   BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/tptp_build_dir"

examples/c/CMakeLists.txt

@@ -22,6 +22,17 @@ message(STATUS "Found Z3 ${Z3_VERSION_STRING}")
 message(STATUS "Z3_DIR: ${Z3_DIR}")
 
 add_executable(c_example test_capi.c)
+
+option(FORCE_CXX_LINKER "Force linker with C++ linker" OFF)
+if (FORCE_CXX_LINKER)
+  # This is a hack for avoiding UBSan linking errors
+  message(STATUS "Forcing use of C++ linker")
+  set_target_properties(c_example
+    PROPERTIES
+    LINKER_LANGUAGE CXX
+  )
+endif()
+
 target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS})
 target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES})
 

examples/maxsat/CMakeLists.txt

@@ -25,6 +25,16 @@ add_executable(c_maxsat_example maxsat.c)
 target_include_directories(c_maxsat_example PRIVATE ${Z3_C_INCLUDE_DIRS})
 target_link_libraries(c_maxsat_example PRIVATE ${Z3_LIBRARIES})
 
+option(FORCE_CXX_LINKER "Force linker with C++ linker" OFF)
+if (FORCE_CXX_LINKER)
+  # This is a hack for avoiding UBSan linking errors
+  message(STATUS "Forcing use of C++ linker")
+  set_target_properties(c_maxsat_example
+    PROPERTIES
+    LINKER_LANGUAGE CXX
+  )
+endif()
+
 if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows")
   # On Windows we need to copy the Z3 libraries
   # into the same directory as the executable

src/cmd_context/cmd_context.cpp

@@ -1608,7 +1608,9 @@ void cmd_context::validate_check_sat_result(lbool r) {
             throw cmd_exception("check annotation that says unsat");
 #else
             diagnostic_stream() << "BUG: incompleteness" << std::endl;
-            exit(ERR_INCOMPLETENESS);
+            // WORKAROUND: `exit()` causes LSan to be invoked and produce
+            // many false positives.
+            _Exit(ERR_INCOMPLETENESS);
 #endif
         }
         break;
@@ -1618,7 +1620,9 @@ void cmd_context::validate_check_sat_result(lbool r) {
             throw cmd_exception("check annotation that says sat");
 #else
             diagnostic_stream() << "BUG: unsoundness" << std::endl;
-            exit(ERR_UNSOUNDNESS);
+            // WORKAROUND: `exit()` causes LSan to be invoked and produce
+            // many false positives.
+            _Exit(ERR_UNSOUNDNESS);
 #endif
         }
         break;

src/parsers/smt2/smt2parser.cpp

@@ -444,7 +444,10 @@ namespace smt2 {
                 m_ctx.regular_stream()<< "line " << line << " column " << pos << ": " << escaped(msg, true) << "\")" << std::endl;
             }
             if (m_ctx.exit_on_error()) {
-                exit(1);
+                // WORKAROUND: ASan's LeakSanitizer reports many false positives when
+                // calling `exit()` so call `_Exit()` instead which avoids invoking leak
+                // checking.
+                _Exit(1);
             }
         }