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

.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
@@ -57,7 +64,7 @@ env:
     # 64-bit GCC 4.8 RelWithDebInfo
     - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo
     # 64-bit GCC 4.8 Debug
-    - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
+    - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug RUN_UNIT_TESTS=BUILD_ONLY
 
 # macOS (a.k.a OSX) support
 matrix:

contrib/ci/Dockerfiles/z3_build.Dockerfile

@@ -2,34 +2,33 @@ ARG DOCKER_IMAGE_BASE
 FROM ${DOCKER_IMAGE_BASE}
 
 
-# Specify defaults. This can be changed when invoking
+# Build arguments. This can be changed when invoking
 # `docker build`.
-ARG ASAN_BUILD=0
-ARG BUILD_DOCS=0
-ARG CC=gcc
-ARG CXX=g++
-ARG DOTNET_BINDINGS=1
-ARG JAVA_BINDINGS=1
-ARG NO_SUPPRESS_OUTPUT=0
-ARG PYTHON_BINDINGS=1
+ARG ASAN_BUILD
+ARG BUILD_DOCS
+ARG CC
+ARG CXX
+ARG DOTNET_BINDINGS
+ARG JAVA_BINDINGS
+ARG NO_SUPPRESS_OUTPUT
+ARG PYTHON_BINDINGS
 ARG PYTHON_EXECUTABLE=/usr/bin/python2.7
-ARG RUN_SYSTEM_TESTS=1
-ARG RUN_UNIT_TESTS=1
-ARG TARGET_ARCH=x86_64
-ARG TEST_INSTALL=1
-ARG UBSAN_BUILD=0
-ARG USE_LIBGMP=0
-ARG USE_LTO=0
-ARG USE_OPENMP=1
+ARG RUN_SYSTEM_TESTS
+ARG RUN_UNIT_TESTS
+ARG TARGET_ARCH
+ARG TEST_INSTALL
+ARG UBSAN_BUILD
+ARG USE_LIBGMP
+ARG USE_LTO
+ARG USE_OPENMP
 ARG Z3_SRC_DIR=/home/user/z3_src
-ARG Z3_BUILD_TYPE=RelWithDebInfo
-ARG Z3_CMAKE_GENERATOR=Ninja
-ARG Z3_INSTALL_PREFIX=/usr
-ARG Z3_STATIC_BUILD=0
-# Blank default indicates use latest.
+ARG Z3_BUILD_TYPE
+ARG Z3_CMAKE_GENERATOR
+ARG Z3_INSTALL_PREFIX
+ARG Z3_STATIC_BUILD
 ARG Z3_SYSTEM_TEST_GIT_REVISION
-ARG Z3_WARNINGS_AS_ERRORS=SERIOUS_ONLY
-ARG Z3_VERBOSE_BUILD_OUTPUT=0
+ARG Z3_WARNINGS_AS_ERRORS
+ARG Z3_VERBOSE_BUILD_OUTPUT
 
 ENV \
   ASAN_BUILD=${ASAN_BUILD} \
@@ -74,6 +73,7 @@ ADD *.txt *.md RELEASE_NOTES ${Z3_SRC_DIR}/
 
 ADD \
   /contrib/ci/scripts/build_z3_cmake.sh \
+  /contrib/ci/scripts/ci_defaults.sh \
   /contrib/ci/scripts/set_compiler_flags.sh \
   /contrib/ci/scripts/set_generator_args.sh \
   ${Z3_SRC_DIR}/contrib/ci/scripts/

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`)
@@ -58,8 +58,9 @@ The `scripts/travis_ci_linux_entry_point.sh` script
    variables (if set) into the build using the `--build-arg` argument of the `docker run`
    command.
 
-If an environemnt variable is not set a defaults value is used which can be
-found in `Dockerfiles/z3_build.Dockerfile`.
+The default values of the configuration environment variables
+can be found in
+[`scripts/ci_defaults.sh`](scripts/ci_defaults.sh).
 
 #### Linux specific configuration variables
 
@@ -67,8 +68,9 @@ found in `Dockerfiles/z3_build.Dockerfile`.
 
 #### Reproducing a build locally
 
-A build can be reproduced locally by using the `scripts/travis_ci_linux_entry_point.sh`
-script and setting the appropriate environment variable.
+A build can be reproduced locally by using the
+`scripts/travis_ci_linux_entry_point.sh` script and setting the appropriate
+environment variable.
 
 For example lets say we wanted to reproduce the build below.
 
@@ -104,11 +106,43 @@ feature might be removed in the future.
 
 It may be better to just build the base image once (outside of TravisCI), upload
 it to [DockerHub](https://hub.docker.com/) and have the build pull down the pre-built
-image everytime.
+image every time.
 
 An [organization](https://hub.docker.com/u/z3prover/) has been created on
 DockerHub for this.
 
 ### macOS
 
-Not yet implemented.
+For macOS we execute directly on TravisCI's macOS environment.  The entry point
+for the TravisCI builds is the
+[`scripts/travis_ci_osx_entry_point.sh`](scripts/travis_ci_osx_entry_point.sh)
+scripts.
+
+#### macOS specific configuration variables
+
+* `MACOS_SKIP_DEPS_UPDATE` - If set to `1` installing the necessary build dependencies
+  is skipped. This is useful for local testing if the dependencies are already installed.
+* `MACOS_UPDATE_CMAKE` - If set to `1` the installed version of CMake will be upgraded.
+
+#### Reproducing a build locally
+
+To reproduce a build (e.g. like the one shown below)
+
+```yaml
+- os: osx
+  osx_image: xcode8.3
+  # Note: Apple Clang does not support OpenMP
+  env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0
+```
+
+Run the following:
+
+```bash
+TRAVIS_BUILD_DIR=$(pwd) \
+Z3_BUILD_TYPE=RelWithDebInfo \
+USE_OPEN_MP=0 \
+contrib/ci/scripts/travis_ci_osx_entry_point.sh
+```
+
+Note this assumes that the current working directory is the root of the Z3
+git repository.

contrib/ci/scripts/ci_defaults.sh

@@ -0,0 +1,54 @@
+# This file should be sourced by other scripts
+# and not executed directly
+
+# Set CI build defaults
+
+export ASAN_BUILD="${ASAN_BUILD:-0}"
+export BUILD_DOCS="${BUILD_DOCS:-0}"
+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_SYSTEM_TESTS="${RUN_SYSTEM_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}"
+export USE_LIBGMP="${USE_LIBGMP:-0}"
+export USE_LTO="${USE_LTO:-0}"
+export USE_OPENMP="${USE_OPENMP:-1}"
+
+export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}"
+export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}"
+export Z3_STATIC_BUILD="${Z3_STATIC_BUILD:-0}"
+# Default is blank which means get latest revision
+export Z3_SYSTEM_TEST_GIT_REVISION="${Z3_SYSTEM_TEST_GIT_REVISION:-}"
+export Z3_WARNINGS_AS_ERRORS="${Z3_WARNINGS_AS_ERRORS:-SERIOUS_ONLY}"
+export Z3_VERBOSE_BUILD_OUTPUT="${Z3_VERBOSE_BUILD_OUTPUT:-0}"
+
+# Platform specific defaults
+PLATFORM="$(uname -s)"
+case "${PLATFORM}" in
+  Linux*)
+    export C_COMPILER="${C_COMPILER:-gcc}"
+    export CXX_COMPILER="${CXX_COMPILER:-g++}"
+    export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr}"
+  ;;
+  Darwin*)
+    export C_COMPILER="${C_COMPILER:-clang}"
+    export CXX_COMPILER="${CXX_COMPILER:-clang++}"
+    export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr/local}"
+  ;;
+  *)
+    echo "Unknown platform \"${PLATFORM}\""
+    exit 1
+  ;;
+esac
+unset PLATFORM
+
+# NOTE: The following variables are not set here because
+# they are specific to the CI implementation
+# PYTHON_EXECUTABLE
+# Z3_SRC_DIR
+# Z3_BUILD_DIR
+# Z3_SYSTEM_TEST_DIR

contrib/ci/scripts/set_generator_args.sh

@@ -1,4 +1,4 @@
-# This script should is intended to be included by other
+# This script is intended to be included by other
 # scripts and should not be executed directly
 
 : ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"}

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

contrib/ci/scripts/travis_ci_linux_entry_point.sh

@@ -11,16 +11,21 @@ DOCKER_FILE_DIR="$(cd ${SCRIPT_DIR}/../Dockerfiles; echo $PWD)"
 : ${LINUX_BASE?"LINUX_BASE must be specified"}
 
 
-
 # Sanity check. Current working directory should be repo root
 if [ ! -f "./README.md" ]; then
   echo "Current working directory should be repo root"
   exit 1
 fi
 
+# Get defaults
+source "${SCRIPT_DIR}/ci_defaults.sh"
+
 BUILD_OPTS=()
-# Override options if they have been provided.
-# Otherwise the defaults in the Docker file will be used
+# Pass Docker build arguments
+if [ -n "${Z3_BUILD_TYPE}" ]; then
+  BUILD_OPTS+=("--build-arg" "Z3_BUILD_TYPE=${Z3_BUILD_TYPE}")
+fi
+
 if [ -n "${Z3_CMAKE_GENERATOR}" ]; then
   BUILD_OPTS+=("--build-arg" "Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR}")
 fi

contrib/ci/scripts/travis_ci_osx_entry_point.sh

@@ -6,26 +6,8 @@ set -x
 set -e
 set -o pipefail
 
-# Set defaults
-# FIXME: Refactor this so we don't need to stay in sync with
-# `z3_build.Dockerfile`.
-export ASAN_BUILD="${ASAN_BUILD:-0}"
-export BUILD_DOCS="${BUILD_DOCS:-0}"
-export C_COMPILER="${C_COMPILER:-clang}"
-export CXX_COMPILER="${CXX_COMPILER:-clang++}"
-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 PYTHON_EXECUTABLE="$(which python)"
-export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
-export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}"
-export TARGET_ARCH="${TARGET_ARCH:-x86_64}"
-export TEST_INSTALL="${TEST_INSTALL:-1}"
-export UBSAN_BUILD="${UBSAN_BUILD:-0}"
-export USE_LIBGMP="${USE_LIBGMP:-0}"
-export USE_LTO="${USE_LTO:-0}"
-export USE_OPENMP="${USE_OPENMP:-1}"
+# Get defaults
+source "${SCRIPT_DIR}/ci_defaults.sh"
 
 if [ -z "${TRAVIS_BUILD_DIR}" ]; then
   echo "TRAVIS_BUILD_DIR must be set to root of Z3 repository"
@@ -37,15 +19,12 @@ if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then
   exit 1
 fi
 
+# These variables are specific to the macOS TravisCI
+# implementation and are not set in `ci_defaults.sh`.
+export PYTHON_EXECUTABLE="${PYTHON_EXECUTABLE:-$(which python)}"
 export Z3_SRC_DIR="${TRAVIS_BUILD_DIR}"
 export Z3_BUILD_DIR="${Z3_SRC_DIR}/build"
-export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}"
-export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}"
-export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr/local}"
-export Z3_STATIC_BUILD="${Z3_STATIC_BUILD:-0}"
 export Z3_SYSTEM_TEST_DIR="${Z3_SRC_DIR}/z3_system_test"
-export Z3_WARNINGS_AS_ERRORS="${Z3_WARNINGS_AS_ERRORS:-SERIOUS_ONLY}"
-export Z3_VERBOSE_BUILD_OUTPUT="${Z3_VERBOSE_BUILD_OUTPUT:-0}"
 
 # Overwrite whatever what set in TravisCI
 export CC="${C_COMPILER}"