[TravisCI] Try to run the Python and .NET examples under ASan.

.travis.yml

@@ -21,7 +21,7 @@ env:
     # 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
+    - 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
 
     # 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

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
@@ -32,6 +33,7 @@ ARG Z3_VERBOSE_BUILD_OUTPUT
 
 ENV \
   ASAN_BUILD=${ASAN_BUILD} \
+  ASAN_DSO=${ASAN_DSO} \
   BUILD_DOCS=${BUILD_DOCS} \
   CC=${CC} \
   CXX=${CXX} \

contrib/ci/scripts/ci_defaults.sh

@@ -49,6 +49,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/sanitizer_env.sh

@@ -18,11 +18,43 @@ if [ "X${ASAN_BUILD}" = "X1" ]; then
   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

contrib/ci/scripts/test_z3_examples_cmake.sh

@@ -64,16 +64,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_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/all_interval_series.py
+  fi
+  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/complex.py
+  run_non_native_binding run_quiet ${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_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/marco.py
+  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/mss.py
+  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/socrates.py
+  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/visitor.py
+  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/z3test.py
 fi
 
 if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
@@ -81,7 +86,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_non_native_binding run_quiet mono ./dotnet_test.exe
 fi
 
 if [ "X${JAVA_BINDINGS}" = "X1" ]; then
@@ -98,6 +103,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_non_native_binding \
+      run_quiet \
+        java -cp .:examples/java:com.microsoft.z3.jar JavaExample
+  fi
 fi
 

contrib/ci/scripts/travis_ci_linux_entry_point.sh

@@ -84,6 +84,10 @@ 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 "${UBSAN_BUILD}" ]; then
   BUILD_OPTS+=("--build-arg" "UBSAN_BUILD=${UBSAN_BUILD}")
 fi