From d47aea398730634444bd31172fd2a04739a9efa7 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 11:23:44 +0100
Subject: [PATCH] [TravisCI] Workaround slow unit test execution for Debug
 builds.

Unit tests execute very slowly in Debug (i.e. unoptimized) builds.  This
causes TravisCI to terminate the job due to no console output being
seen.

To workaround this for the debug builds the tests are just compiled
but not executed. To implement this the `RUN_UNIT_TESTS` environment
variable now can take on the values `BUILD_ONLY`, `BUILD_AND_RUN`,
and `SKIP` rather than `0` or `1`.
---
 .travis.yml                                   | 11 ++++--
 contrib/ci/README.md                          |  2 +-
 contrib/ci/scripts/ci_defaults.sh             |  2 +-
 .../ci/scripts/test_z3_unit_tests_cmake.sh    | 36 ++++++++++++++-----
 4 files changed, 38 insertions(+), 13 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 50d63e593..ac00ef918 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -22,10 +22,17 @@ env:
     # 64-bit Clang 3.9 RelWithDebInfo
     - 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
 
+    # Debug builds
+    #
+    # Note the unit tests for the debug builds are compiled but **not**
+    # executed. This is because the debug build of unit tests takes a large
+    # amount of time to execute compared to the optimized builds. The hope is
+    # that just running the optimized unit tests is sufficient.
+    #
     # 64-bit GCC 5.4 Debug
-    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug RUN_UNIT_TESTS=BUILD_ONLY
     # 64-bit Clang Debug
-    - 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
+    - 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 RUN_UNIT_TESTS=BUILD_ONLY
 
     # 32-bit GCC 5.4 RelWithDebInfo
     - LINUX_BASE=ubuntu32_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=i686 Z3_BUILD_TYPE=RelWithDebInfo
diff --git a/contrib/ci/README.md b/contrib/ci/README.md
index 2e117c8b1..e4c9aecfd 100644
--- a/contrib/ci/README.md
+++ b/contrib/ci/README.md
@@ -31,7 +31,7 @@ the future.
 * `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_SYSTEM_TESTS` - Run system tests (`0` or `1`)
-* `RUN_UNIT_TESTS` - Run unit tests (`0` or `1`)
+* `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`)
 * `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`)
diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh
index 2fb3fa52a..d8e9376d8 100644
--- a/contrib/ci/scripts/ci_defaults.sh
+++ b/contrib/ci/scripts/ci_defaults.sh
@@ -10,7 +10,7 @@ export JAVA_BINDINGS="${JAVA_BINDINGS:-1}"
 export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}"
 export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}"
 export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
-export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}"
+export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}"
 export TARGET_ARCH="${TARGET_ARCH:-x86_64}"
 export TEST_INSTALL="${TEST_INSTALL:-1}"
 export UBSAN_BUILD="${UBSAN_BUILD:-0}"
diff --git a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
index 666673328..e1c927f58 100755
--- a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
+++ b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
@@ -10,17 +10,35 @@ set -o pipefail
 : ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
 : ${RUN_UNIT_TESTS?"RUN_UNIT_TESTS must be specified"}
 
-if [ "X${RUN_UNIT_TESTS}" != "X1" ]; then
-  echo "Skipping unit tests"
-  exit 0
-fi
-
 # Set CMake generator args
 source ${SCRIPT_DIR}/set_generator_args.sh
 
 cd "${Z3_BUILD_DIR}"
 
-# Build and run internal tests
-cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}"
-# Run all tests that don't require arguments
-run_quiet ./test-z3 /a
+function build_unit_tests() {
+  # Build internal tests
+  cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}"
+}
+
+function run_unit_tests() {
+  # Run all tests that don't require arguments
+  run_quiet ./test-z3 /a
+}
+
+case "${RUN_UNIT_TESTS}" in
+  BUILD_AND_RUN)
+    build_unit_tests
+    run_unit_tests
+  ;;
+  BUILD_ONLY)
+    build_unit_tests
+  ;;
+  SKIP)
+    echo "RUN_UNIT_TESTS set to \"${RUN_UNIT_TESTS}\" so skipping build and run"
+    exit 0
+  ;;
+  *)
+    echo "Error: RUN_UNIT_TESTS set to unhandled value \"${RUN_UNIT_TESTS}\""
+    exit 1
+  ;;
+esac