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