From 64ee9f168df650537c6264c1c4e6c16dd315966d Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 12:26:35 +0100
Subject: [PATCH] [TravisCI] Add ASan/LSan/UBSan suppression files and use them
in CI.
---
contrib/ci/Dockerfiles/z3_build.Dockerfile | 9 ++++++++-
contrib/ci/scripts/sanitizer_env.sh | 19 +++++++++++++++++++
contrib/ci/scripts/test_z3_examples_cmake.sh | 3 +++
contrib/ci/scripts/test_z3_system_tests.sh | 3 +++
.../ci/scripts/test_z3_unit_tests_cmake.sh | 3 +++
contrib/suppressions/README.md | 7 +++++++
contrib/suppressions/maintainers.txt | 3 +++
contrib/suppressions/sanitizers/README.md | 4 ++++
contrib/suppressions/sanitizers/asan.txt | 1 +
contrib/suppressions/sanitizers/lsan.txt | 1 +
contrib/suppressions/sanitizers/ubsan.txt | 1 +
11 files changed, 53 insertions(+), 1 deletion(-)
create mode 100644 contrib/ci/scripts/sanitizer_env.sh
create mode 100644 contrib/suppressions/README.md
create mode 100644 contrib/suppressions/maintainers.txt
create mode 100644 contrib/suppressions/sanitizers/README.md
create mode 100644 contrib/suppressions/sanitizers/asan.txt
create mode 100644 contrib/suppressions/sanitizers/lsan.txt
create mode 100644 contrib/suppressions/sanitizers/ubsan.txt
diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile
index 07504e6b9..65cf08087 100644
--- a/contrib/ci/Dockerfiles/z3_build.Dockerfile
+++ b/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
diff --git a/contrib/ci/scripts/sanitizer_env.sh b/contrib/ci/scripts/sanitizer_env.sh
new file mode 100644
index 000000000..e9af255d3
--- /dev/null
+++ b/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
diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh
index 2eda3de7b..1b8f988a2 100755
--- a/contrib/ci/scripts/test_z3_examples_cmake.sh
+++ b/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
diff --git a/contrib/ci/scripts/test_z3_system_tests.sh b/contrib/ci/scripts/test_z3_system_tests.sh
index dfb1084a4..d61a0ef02 100755
--- a/contrib/ci/scripts/test_z3_system_tests.sh
+++ b/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}"
diff --git a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
index e1c927f58..60c29556b 100755
--- a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
+++ b/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() {
diff --git a/contrib/suppressions/README.md b/contrib/suppressions/README.md
new file mode 100644
index 000000000..90df39084
--- /dev/null
+++ b/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.
diff --git a/contrib/suppressions/maintainers.txt b/contrib/suppressions/maintainers.txt
new file mode 100644
index 000000000..caa6798c6
--- /dev/null
+++ b/contrib/suppressions/maintainers.txt
@@ -0,0 +1,3 @@
+# Maintainers
+
+- Dan Liew (@delcypher)
diff --git a/contrib/suppressions/sanitizers/README.md b/contrib/suppressions/sanitizers/README.md
new file mode 100644
index 000000000..f76f920b2
--- /dev/null
+++ b/contrib/suppressions/sanitizers/README.md
@@ -0,0 +1,4 @@
+# Sanitizer supression files
+
+This directory contains files used to suppress
+ASan/LSan/UBSan warnings/errors.
diff --git a/contrib/suppressions/sanitizers/asan.txt b/contrib/suppressions/sanitizers/asan.txt
new file mode 100644
index 000000000..f058adfe2
--- /dev/null
+++ b/contrib/suppressions/sanitizers/asan.txt
@@ -0,0 +1 @@
+# AddressSanitizer suppression file
diff --git a/contrib/suppressions/sanitizers/lsan.txt b/contrib/suppressions/sanitizers/lsan.txt
new file mode 100644
index 000000000..a4ce0881a
--- /dev/null
+++ b/contrib/suppressions/sanitizers/lsan.txt
@@ -0,0 +1 @@
+# LeakSanitizer suppression file
diff --git a/contrib/suppressions/sanitizers/ubsan.txt b/contrib/suppressions/sanitizers/ubsan.txt
new file mode 100644
index 000000000..8feef305f
--- /dev/null
+++ b/contrib/suppressions/sanitizers/ubsan.txt
@@ -0,0 +1 @@
+# UndefinedBehavior sanitizer suppression file