From 3ab96281ebbd076f3916eee1b81a2b6f6245500e Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Aug 2022 22:49:47 +0700 Subject: [PATCH] Remove Travis CI configs. --- contrib/.travis.yml | 53 ----- .../z3_base_ubuntu_20.04.Dockerfile | 34 --- contrib/ci/Dockerfiles/z3_build.Dockerfile | 121 ---------- contrib/ci/README.md | 147 ------------ contrib/ci/maintainers.txt | 3 - contrib/ci/scripts/build_z3_cmake.sh | 133 ----------- contrib/ci/scripts/ci_defaults.sh | 59 ----- contrib/ci/scripts/install_deps_osx.sh | 47 ---- contrib/ci/scripts/run_quiet.sh | 41 ---- contrib/ci/scripts/sanitizer_env.sh | 58 ----- contrib/ci/scripts/set_compiler_flags.sh | 46 ---- contrib/ci/scripts/set_generator_args.sh | 20 -- contrib/ci/scripts/test_z3_docs.sh | 24 -- contrib/ci/scripts/test_z3_examples_cmake.sh | 125 ---------- contrib/ci/scripts/test_z3_install_cmake.sh | 24 -- contrib/ci/scripts/test_z3_system_tests.sh | 70 ------ .../ci/scripts/test_z3_unit_tests_cmake.sh | 47 ---- contrib/ci/scripts/travis_ci_entry_point.sh | 18 -- .../ci/scripts/travis_ci_linux_entry_point.sh | 220 ------------------ .../ci/scripts/travis_ci_osx_entry_point.sh | 51 ---- 20 files changed, 1341 deletions(-) delete mode 100644 contrib/.travis.yml delete mode 100644 contrib/ci/Dockerfiles/z3_base_ubuntu_20.04.Dockerfile delete mode 100644 contrib/ci/Dockerfiles/z3_build.Dockerfile delete mode 100644 contrib/ci/README.md delete mode 100644 contrib/ci/maintainers.txt delete mode 100755 contrib/ci/scripts/build_z3_cmake.sh delete mode 100644 contrib/ci/scripts/ci_defaults.sh delete mode 100755 contrib/ci/scripts/install_deps_osx.sh delete mode 100644 contrib/ci/scripts/run_quiet.sh delete mode 100644 contrib/ci/scripts/sanitizer_env.sh delete mode 100644 contrib/ci/scripts/set_compiler_flags.sh delete mode 100644 contrib/ci/scripts/set_generator_args.sh delete mode 100755 contrib/ci/scripts/test_z3_docs.sh delete mode 100755 contrib/ci/scripts/test_z3_examples_cmake.sh delete mode 100755 contrib/ci/scripts/test_z3_install_cmake.sh delete mode 100755 contrib/ci/scripts/test_z3_system_tests.sh delete mode 100755 contrib/ci/scripts/test_z3_unit_tests_cmake.sh delete mode 100755 contrib/ci/scripts/travis_ci_entry_point.sh delete mode 100755 contrib/ci/scripts/travis_ci_linux_entry_point.sh delete mode 100755 contrib/ci/scripts/travis_ci_osx_entry_point.sh diff --git a/contrib/.travis.yml b/contrib/.travis.yml deleted file mode 100644 index 230c690a6f6..00000000000 --- a/contrib/.travis.yml +++ /dev/null @@ -1,53 +0,0 @@ -cache: - # This persistent cache is used to cache the building of - # docker base images. - directories: - - $DOCKER_TRAVIS_CI_CACHE_DIR -sudo: required -language: cpp -services: - - docker -env: - global: - # This environment variable tells the `travis_ci_linux_entry_point.sh` - # script to look for a cached Docker image. - - DOCKER_TRAVIS_CI_CACHE_DIR=$HOME/.cache/docker - # Configurations - matrix: -############################################################################### -# Ubuntu 20.04 LTS -############################################################################### - # 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. - - # clang - - LINUX_BASE=ubuntu_20.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug - - LINUX_BASE=ubuntu_20.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release UBSAN_BUILD=1 - - LINUX_BASE=ubuntu_20.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release ASAN_BUILD=1 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0 - - # gcc - # ubsan/msan builds too slow - - LINUX_BASE=ubuntu_20.04 C_COMPILER=gcc CXX_COMPILER=g++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release BUILD_DOCS=1 - - LINUX_BASE=ubuntu_20.04 C_COMPILER=gcc CXX_COMPILER=g++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug - - # GMP library - - LINUX_BASE=ubuntu_20.04 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release USE_LIBGMP=1 - - LINUX_BASE=ubuntu_20.04 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug USE_LIBGMP=1 - - # Unix Makefile generator build - - LINUX_BASE=ubuntu_20.04 TARGET_ARCH=x86_64 Z3_CMAKE_GENERATOR="Unix Makefiles" - - # LTO build - # too slow - #- LINUX_BASE=ubuntu_20.04 C_COMPILER=gcc CXX_COMPILER=g++ TARGET_ARCH=x86_64 USE_LTO=1 RUN_UNIT_TESTS=BUILD_ONLY RUN_SYSTEM_TESTS=0 - #- LINUX_BASE=ubuntu_20.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 USE_LTO=1 RUN_UNIT_TESTS=BUILD_ONLY RUN_SYSTEM_TESTS=0 - - # Static build. Note we have disable building the bindings because they won't work with a static libz3 - - LINUX_BASE=ubuntu_20.04 TARGET_ARCH=x86_64 Z3_STATIC_BUILD=1 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0 - - -script: - # Use `travis_wait` when building because some configurations don't produce an - # output for a long time (linking & testing) - - travis_wait 55 contrib/ci/scripts/travis_ci_entry_point.sh || exit 1; diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_20.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_20.04.Dockerfile deleted file mode 100644 index 9ef85c67322..00000000000 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_20.04.Dockerfile +++ /dev/null @@ -1,34 +0,0 @@ -FROM ubuntu:20.04 - -ARG DEBIAN_FRONTEND=noninteractive -RUN apt-get update && \ - apt-get -y --no-install-recommends install \ - cmake \ - make \ - ninja-build \ - clang \ - g++ \ - curl \ - doxygen \ - default-jdk \ - git \ - graphviz \ - python3 \ - python3-setuptools \ - python-is-python3 \ - sudo - -RUN curl -SL https://packages.microsoft.com/config/ubuntu/20.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \ - dpkg -i packages-microsoft-prod.deb && \ - apt-get update && \ - apt-get -y --no-install-recommends install dotnet-sdk-2.1 - -# Create `user` user for container with password `user`. and give it -# password-less sudo access -RUN useradd -m user && \ - echo user:user | chpasswd && \ - cp /etc/sudoers /etc/sudoers.bak && \ - echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers -USER user -WORKDIR /home/user -#ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-7/bin/llvm-symbolizer diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile deleted file mode 100644 index f6e05fcb565..00000000000 --- a/contrib/ci/Dockerfiles/z3_build.Dockerfile +++ /dev/null @@ -1,121 +0,0 @@ -ARG DOCKER_IMAGE_BASE -FROM ${DOCKER_IMAGE_BASE} - - -# Build arguments. This can be changed when invoking -# `docker build`. -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/python -ARG RUN_API_EXAMPLES -ARG RUN_SYSTEM_TESTS -ARG RUN_UNIT_TESTS -ARG SANITIZER_PRINT_SUPPRESSIONS -ARG TARGET_ARCH -ARG TEST_INSTALL -ARG UBSAN_BUILD -ARG Z3_USE_LIBGMP -ARG USE_LTO -ARG Z3_SRC_DIR=/home/user/z3_src -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 -ARG Z3_VERBOSE_BUILD_OUTPUT - -ENV \ - ASAN_BUILD=${ASAN_BUILD} \ - BUILD_DOCS=${BUILD_DOCS} \ - CC=${CC} \ - CXX=${CXX} \ - DOTNET_BINDINGS=${DOTNET_BINDINGS} \ - JAVA_BINDINGS=${JAVA_BINDINGS} \ - NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT} \ - PYTHON_BINDINGS=${PYTHON_BINDINGS} \ - PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \ - SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS} \ - RUN_API_EXAMPLES=${RUN_API_EXAMPLES} \ - RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS} \ - RUN_UNIT_TESTS=${RUN_UNIT_TESTS} \ - TARGET_ARCH=${TARGET_ARCH} \ - TEST_INSTALL=${TEST_INSTALL} \ - UBSAN_BUILD=${UBSAN_BUILD} \ - Z3_USE_LIBGMP=${Z3_USE_LIBGMP} \ - USE_LTO=${USE_LTO} \ - Z3_SRC_DIR=${Z3_SRC_DIR} \ - Z3_BUILD_DIR=/home/user/z3_build \ - Z3_BUILD_TYPE=${Z3_BUILD_TYPE} \ - Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR} \ - Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT} \ - Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \ - Z3_SYSTEM_TEST_DIR=/home/user/z3_system_test \ - Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION} \ - Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \ - Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} - -# We add context across incrementally to maximal cache reuse - -# Build Z3 -RUN mkdir -p "${Z3_SRC_DIR}" && \ - mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts" && \ - mkdir -p "${Z3_SRC_DIR}/contrib/suppressions/sanitizers" -# Deliberately leave out `contrib` -ADD /cmake ${Z3_SRC_DIR}/cmake/ -ADD /doc ${Z3_SRC_DIR}/doc/ -ADD /examples ${Z3_SRC_DIR}/examples/ -ADD /scripts ${Z3_SRC_DIR}/scripts/ -ADD /src ${Z3_SRC_DIR}/src/ -ADD *.txt *.md *.cmake.in 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/ -RUN ${Z3_SRC_DIR}/contrib/ci/scripts/build_z3_cmake.sh - -# Test building docs -ADD \ - /contrib/ci/scripts/test_z3_docs.sh \ - /contrib/ci/scripts/run_quiet.sh \ - ${Z3_SRC_DIR}/contrib/ci/scripts/ -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 -ADD \ - /contrib/ci/scripts/test_z3_unit_tests_cmake.sh \ - ${Z3_SRC_DIR}/contrib/ci/scripts/ -RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_unit_tests_cmake.sh - -# Run system tests -ADD \ - /contrib/ci/scripts/test_z3_system_tests.sh \ - ${Z3_SRC_DIR}/contrib/ci/scripts/ -RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_system_tests.sh - -# Test install -ADD \ - /contrib/ci/scripts/test_z3_install_cmake.sh \ - ${Z3_SRC_DIR}/contrib/ci/scripts/ -RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_install_cmake.sh diff --git a/contrib/ci/README.md b/contrib/ci/README.md deleted file mode 100644 index 9a8262e3785..00000000000 --- a/contrib/ci/README.md +++ /dev/null @@ -1,147 +0,0 @@ -# Continuous integration scripts - -## TravisCI - -For testing on Linux and macOS we use [TravisCI](https://travis-ci.org/) - -TravisCI consumes the `.travis.yml` file in the root of the repository -to tell it how to build and test Z3. - -However the logic for building and test Z3 is kept out of this file -and instead in a set of scripts in `scripts/`. This avoids -coupling the build to TravisCI tightly so we can migrate to another -service if required in the future. - -The scripts rely on a set of environment variables to control the configuration -of the build. The `.travis.yml` declares a list of configuration with each -configuration setting different environment variables. - -Note that the build scripts currently only support Z3 built with CMake. Support -for building Z3 using the older Python/Makefile build system might be added in -the future. - -### Configuration variables - -* `ASAN_BUILD` - Do [AddressSanitizer](https://github.com/google/sanitizers/wiki/AddressSanitizer) build (`0` or `1`) -* `BUILD_DOCS` - Build API documentation (`0` or `1`) -* `C_COMPILER` - Path to C Compiler -* `CXX_COMPILER` - Path to C++ Compiler -* `DOTNET_BINDINGS` - Build and test .NET API bindings (`0` or `1`) -* `JAVA_BINDINGS` - Build and test Java API bindings (`0` or `1`) -* `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_API_EXAMPLES` - Build and run API examples (`0` or `1`) -* `RUN_SYSTEM_TESTS` - Run system tests (`0` or `1`) -* `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`) -* `SANITIZER_PRINT_SUPPRESSIONS` - Show ASan/UBSan suppressions (`0` or `1`) -* `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`) -* `Z3_USE_LIBGMP` - Use [GNU multiple precision library](https://gmplib.org/) (`0` or `1`) -* `USE_LTO` - Link binaries using link time optimization (`0` or `1`) -* `Z3_BUILD_TYPE` - CMake build type (`RelWithDebInfo`, `Release`, `Debug`, or `MinSizeRel`) -* `Z3_CMAKE_GENERATOR` - CMake generator (`Ninja` or `Unix Makefiles`) -* `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`) -* `Z3_BUILD_LIBZ3_SHARED` - Build Z3 binaries and libraries dynamically/statically (`0` or `1`) -* `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty latest revision will be used. -* `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option passed to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`) - -### Linux - -For Linux we use Docker to perform the build so that it easily reproducible -on a local machine and so that we can avoid depending on TravisCI's environment -and instead use a Linux distribution of our choice. - -The `scripts/travis_ci_linux_entry_point.sh` script - -1. Creates a base image containing all the dependencies needed to build and test Z3 -2. Builds and tests Z3 using the base image propagating configuration environment - variables (if set) into the build using the `--build-arg` argument of the `docker run` - command. - -The default values of the configuration environment variables -can be found in -[`scripts/ci_defaults.sh`](scripts/ci_defaults.sh). - -#### Linux specific configuration variables - -* `LINUX_BASE` - The base docker image identifier to use (`ubuntu_16.04`, `ubuntu32_16.04`, or `ubuntu_14.04`). - -#### 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. - -For example lets say we wanted to reproduce the build below. - -```yaml - - - 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 -``` - -This can be done by running the command - -```bash -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 scripts/travis_ci_linux_entry_point.sh -``` - -The `docker build` command which we use internally supports caching. What this -means in practice is that re-running the above command will re-use successfully -completed stages of the build provided they haven't changed. This requires that -the `Dockerfiles/z3_build.Dockerfile` is carefully crafted to avoid invalidating -the cache when unrelated files sent to the build context change. - -#### TravisCI docker image cache - -To improve build times the Z3 base docker images are cached using -[TravisCI's cache directory feature](https://docs.travis-ci.com/user/caching). -If the `DOCKER_TRAVIS_CI_CACHE_DIR` environment variable is set (see `.travis.yml`) -then the directory pointed to by the environment variable is used as a cache -for Docker images. - -The logic for this can be found in `scripts/travis_ci_linux_entry_point.sh`. -The build time improvements are rather modest (~ 2 minutes) and the cache is -rather large due to TravisCI giving each configuration its own cache. So this -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 every time. - -An [organization](https://hub.docker.com/u/z3prover/) has been created on -DockerHub for this. - -### macOS - -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 - env: Z3_BUILD_TYPE=RelWithDebInfo -``` - -Run the following: - -```bash -TRAVIS_BUILD_DIR=$(pwd) \ -Z3_BUILD_TYPE=RelWithDebInfo \ -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. diff --git a/contrib/ci/maintainers.txt b/contrib/ci/maintainers.txt deleted file mode 100644 index caa6798c66d..00000000000 --- a/contrib/ci/maintainers.txt +++ /dev/null @@ -1,3 +0,0 @@ -# Maintainers - -- Dan Liew (@delcypher) diff --git a/contrib/ci/scripts/build_z3_cmake.sh b/contrib/ci/scripts/build_z3_cmake.sh deleted file mode 100755 index 63b9410d8d0..00000000000 --- a/contrib/ci/scripts/build_z3_cmake.sh +++ /dev/null @@ -1,133 +0,0 @@ -#!/bin/bash -# This script builds Z3 - -SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" - -set -x -set -e -set -o pipefail - -: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"} -: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} -: ${Z3_BUILD_TYPE?"Z3_BUILD_TYPE must be specified"} -: ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"} -: ${Z3_STATIC_BUILD?"Z3_STATIC_BUILD must be specified"} -: ${Z3_USE_LIBGMP?"Z3_USE_LIBGMP must be specified"} -: ${BUILD_DOCS?"BUILD_DOCS must be specified"} -: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} -: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"} -: ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"} -: ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"} -: ${USE_LTO?"USE_LTO must be specified"} -: ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX must be specified"} -: ${Z3_WARNINGS_AS_ERRORS?"Z3_WARNINGS_AS_ERRORS must be specified"} -: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"} - -ADDITIONAL_Z3_OPTS=() - -# Static or dynamic libz3 -if [ "X${Z3_STATIC_BUILD}" = "X1" ]; then - ADDITIONAL_Z3_OPTS+=('-DZ3_BUILD_LIBZ3_SHARED=OFF') -else - ADDITIONAL_Z3_OPTS+=('-DZ3_BUILD_LIBZ3_SHARED=ON') -fi - -# Use LibGMP? -if [ "X${Z3_USE_LIBGMP}" = "X1" ]; then - ADDITIONAL_Z3_OPTS+=('-DZ3_USE_LIB_GMP=ON') -else - ADDITIONAL_Z3_OPTS+=('-DZ3_USE_LIB_GMP=OFF') -fi - -# Use link time optimziation? -if [ "X${USE_LTO}" = "X1" ]; then - ADDITIONAL_Z3_OPTS+=('-DZ3_LINK_TIME_OPTIMIZATION=ON') -else - ADDITIONAL_Z3_OPTS+=('-DZ3_LINK_TIME_OPTIMIZATION=OFF') -fi - -# Build API docs? -if [ "X${BUILD_DOCS}" = "X1" ]; then - ADDITIONAL_Z3_OPTS+=( \ - '-DZ3_BUILD_DOCUMENTATION=ON' \ - '-DZ3_ALWAYS_BUILD_DOCS=OFF' \ - ) -else - ADDITIONAL_Z3_OPTS+=('-DZ3_BUILD_DOCUMENTATION=OFF') -fi - -# Python bindings? -if [ "X${PYTHON_BINDINGS}" = "X1" ]; then - ADDITIONAL_Z3_OPTS+=( \ - '-DZ3_BUILD_PYTHON_BINDINGS=ON' \ - '-DZ3_INSTALL_PYTHON_BINDINGS=ON' \ - ) -else - ADDITIONAL_Z3_OPTS+=( \ - '-DZ3_BUILD_PYTHON_BINDINGS=OFF' \ - '-DZ3_INSTALL_PYTHON_BINDINGS=OFF' \ - ) -fi - -# .NET bindings? -if [ "X${DOTNET_BINDINGS}" = "X1" ]; then - ADDITIONAL_Z3_OPTS+=( \ - '-DZ3_BUILD_DOTNET_BINDINGS=ON' \ - '-DZ3_INSTALL_DOTNET_BINDINGS=ON' \ - ) -else - ADDITIONAL_Z3_OPTS+=( \ - '-DZ3_BUILD_DOTNET_BINDINGS=OFF' \ - '-DZ3_INSTALL_DOTNET_BINDINGS=OFF' \ - ) -fi - -# Java bindings? -if [ "X${JAVA_BINDINGS}" = "X1" ]; then - ADDITIONAL_Z3_OPTS+=( \ - '-DZ3_BUILD_JAVA_BINDINGS=ON' \ - '-DZ3_INSTALL_JAVA_BINDINGS=ON' \ - ) -else - ADDITIONAL_Z3_OPTS+=( \ - '-DZ3_BUILD_JAVA_BINDINGS=OFF' \ - '-DZ3_INSTALL_JAVA_BINDINGS=OFF' \ - ) -fi - -# Set compiler flags -source ${SCRIPT_DIR}/set_compiler_flags.sh - -if [ "X${UBSAN_BUILD}" = "X1" ]; then - # HACK: When building with UBSan the C++ linker - # must be used to avoid the following linker errors. - # undefined reference to `__ubsan_vptr_type_cache' - # undefined reference to `__ubsan_handle_dynamic_type_cache_miss' - ADDITIONAL_Z3_OPTS+=( \ - '-DZ3_C_EXAMPLES_FORCE_CXX_LINKER=ON' \ - ) -fi - -# Sanity check -if [ ! -e "${Z3_SRC_DIR}/CMakeLists.txt" ]; then - echo "Z3_SRC_DIR is invalid" - exit 1 -fi - -# Make build tree -mkdir -p "${Z3_BUILD_DIR}" -cd "${Z3_BUILD_DIR}" - -# Configure -cmake \ - -G "${Z3_CMAKE_GENERATOR}" \ - -DCMAKE_BUILD_TYPE=${Z3_BUILD_TYPE} \ - -DPYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \ - -DCMAKE_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} \ - -DWARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \ - "${ADDITIONAL_Z3_OPTS[@]}" \ - "${Z3_SRC_DIR}" - -# Build -source ${SCRIPT_DIR}/set_generator_args.sh -cmake --build $(pwd) "${GENERATOR_ARGS[@]}" diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh deleted file mode 100644 index d524503c7d1..00000000000 --- a/contrib/ci/scripts/ci_defaults.sh +++ /dev/null @@ -1,59 +0,0 @@ -# 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_API_EXAMPLES="${RUN_API_EXAMPLES:-1}" -export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}" -export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}" -# Don't print suppressions by default because that breaks the Z3 -# regression tests because they don't expect them to appear in Z3's -# output. -export SANITIZER_PRINT_SUPPRESSIONS="${SANITIZER_PRINT_SUPPRESSIONS:-0}" -export TARGET_ARCH="${TARGET_ARCH:-x86_64}" -export TEST_INSTALL="${TEST_INSTALL:-1}" -export UBSAN_BUILD="${UBSAN_BUILD:-0}" -export Z3_USE_LIBGMP="${Z3_USE_LIBGMP:-0}" -export USE_LTO="${USE_LTO:-0}" - -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 -# ASAN_DSO -# Z3_SRC_DIR -# Z3_BUILD_DIR -# Z3_SYSTEM_TEST_DIR diff --git a/contrib/ci/scripts/install_deps_osx.sh b/contrib/ci/scripts/install_deps_osx.sh deleted file mode 100755 index 64530e5f344..00000000000 --- a/contrib/ci/scripts/install_deps_osx.sh +++ /dev/null @@ -1,47 +0,0 @@ -#!/bin/bash - -SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" -. ${SCRIPT_DIR}/run_quiet.sh - -set -x -set -e -set -o pipefail - -run_quiet brew update -export HOMEBREW_NO_AUTO_UPDATE=1 - -function brew_install_or_upgrade() { - if brew ls --versions "$1" > /dev/null 2>&1 ; then - brew upgrade "$1" - else - brew install "$1" - fi -} - -# FIXME: We should fix the versions of dependencies used -# so that we have reproducible builds. - -# HACK: Just use CMake version in TravisCI for now -if [ "X${MACOS_UPDATE_CMAKE}" = "X1" ]; then - brew_install_or_upgrade cmake -fi - -if [ "X${Z3_CMAKE_GENERATOR}" = "XNinja" ]; then - brew_install_or_upgrade ninja -fi - -if [ "X${Z3_USE_LIBGMP}" = "X1" ]; then - brew_install_or_upgrade gmp -fi - -if [ "X${BUILD_DOCS}" = "X1" ]; then - brew_install_or_upgrade doxygen -fi - -if [ "X${DOTNET_BINDINGS}" = "X1" ]; then - brew_install_or_upgrade mono -fi - -if [ "X${JAVA_BINDINGS}" = "X1" ]; then - brew cask install java -fi diff --git a/contrib/ci/scripts/run_quiet.sh b/contrib/ci/scripts/run_quiet.sh deleted file mode 100644 index 0f49da3bedd..00000000000 --- a/contrib/ci/scripts/run_quiet.sh +++ /dev/null @@ -1,41 +0,0 @@ -# Simple wrapper function that runs a command suppressing -# it's output. However it's output will be shown in the -# case that `NO_SUPPRESS_OUTPUT` is set to `1` or the command -# fails. -# -# The use case for this trying to avoid large logs on TravisCI -function run_quiet() { - if [ "X${NO_SUPPRESS_OUTPUT}" = "X1" ]; then - "${@}" - else - OLD_SETTINGS="$-" - set +x - set +e - TMP_DIR="${TMP_DIR:-/tmp/}" - STDOUT="${TMP_DIR}/$$.stdout" - STDERR="${TMP_DIR}/$$.stderr" - "${@}" > "${STDOUT}" 2> "${STDERR}" - EXIT_STATUS="$?" - if [ "${EXIT_STATUS}" -ne 0 ]; then - echo "Command \"$@\" failed" - echo "EXIT CODE: ${EXIT_STATUS}" - echo "STDOUT" - echo "" - echo "\`\`\`" - cat ${STDOUT} - echo "\`\`\`" - echo "" - echo "STDERR" - echo "" - echo "\`\`\`" - cat ${STDERR} - echo "\`\`\`" - echo "" - fi - # Clean up - rm "${STDOUT}" "${STDERR}" - [ "$( echo "${OLD_SETTINGS}" | grep -c 'e')" != "0" ] && set -e - [ "$( echo "${OLD_SETTINGS}" | grep -c 'x')" != "0" ] && set -x - return ${EXIT_STATUS} - fi -} diff --git a/contrib/ci/scripts/sanitizer_env.sh b/contrib/ci/scripts/sanitizer_env.sh deleted file mode 100644 index 1a16b98a6f4..00000000000 --- a/contrib/ci/scripts/sanitizer_env.sh +++ /dev/null @@ -1,58 +0,0 @@ -# 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="suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/lsan.txt" - # NOTE: If you get bad stacktraces try using `fast_unwind_on_malloc=0` - # NOTE: `malloc_context_size` controls size of recorded stacktrace for allocations. - # If the reported stacktraces appear incomplete try increasing the value. - # leak checking disabled because it doesn't work on unpriviledged docker - export ASAN_OPTIONS="malloc_context_size=100,detect_leaks=0,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/asan.txt" - - : ${SANITIZER_PRINT_SUPPRESSIONS?"SANITIZER_PRINT_SUPPRESSIONS must be specified"} - if [ "X${SANITIZER_PRINT_SUPPRESSIONS}" = "X1" ]; then - export LSAN_OPTIONS="${LSAN_OPTIONS},print_suppressions=1" - export ASAN_OPTIONS="${ASAN_OPTIONS},print_suppressions=1" - else - export LSAN_OPTIONS="${LSAN_OPTIONS},print_suppressions=0" - export ASAN_OPTIONS="${ASAN_OPTIONS},print_suppressions=0" - fi - - #: ${ASAN_SYMBOLIZER_PATH?"ASAN_SYMBOLIZER_PATH must be specified"} - - # Run command without checking for leaks - function run_no_lsan() { - ASAN_OPTIONS="${ASAN_OPTIONS},detect_leaks=0" "${@}" - } - - function run_non_native_binding() { - "${@}" - } -else - # In non-ASan build just run directly - function run_no_lsan() { - "${@}" - } - function run_non_native_binding() { - "${@}" - } -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,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/ubsan.txt" - - : ${SANITIZER_PRINT_SUPPRESSIONS?"SANITIZER_PRINT_SUPPRESSIONS must be specified"} - if [ "X${SANITIZER_PRINT_SUPPRESSIONS}" = "X1" ]; then - export UBSAN_OPTIONS="${UBSAN_OPTIONS},print_suppressions=1" - else - export UBSAN_OPTIONS="${UBSAN_OPTIONS},print_suppressions=0" - fi -fi diff --git a/contrib/ci/scripts/set_compiler_flags.sh b/contrib/ci/scripts/set_compiler_flags.sh deleted file mode 100644 index 7efdecdac9d..00000000000 --- a/contrib/ci/scripts/set_compiler_flags.sh +++ /dev/null @@ -1,46 +0,0 @@ -# This script should is intended to be included by other -# scripts and should not be executed directly - -: ${TARGET_ARCH?"TARGET_ARCH must be specified"} -: ${ASAN_BUILD?"ASAN_BUILD must be specified"} -: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"} -: ${CC?"CC must be specified"} -: ${CXX?"CXX must be specified"} - -case ${TARGET_ARCH} in - x86_64) - CXXFLAGS="${CXXFLAGS} -m64" - CFLAGS="${CFLAGS} -m64" - ;; - i686) - CXXFLAGS="${CXXFLAGS} -m32" - CFLAGS="${CFLAGS} -m32" - ;; - *) - echo "Unknown arch \"${TARGET_ARCH}\"" - exit 1 -esac - -if [ "X${ASAN_BUILD}" = "X1" ]; then - CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer" - CFLAGS="${CFLAGS} -fsanitize=address -fno-omit-frame-pointer" -fi - -if [ "X${UBSAN_BUILD}" = "X1" ]; then - CXXFLAGS="${CXXFLAGS} -fsanitize=undefined" - CFLAGS="${CFLAGS} -fsanitize=undefined" -fi - -# Report flags -echo "CXXFLAGS: ${CXXFLAGS}" -echo "CFLAGS: ${CFLAGS}" - -# Report compiler -echo "CC: ${CC}" -${CC} --version -echo "CXX: ${CXX}" -${CXX} --version - -# Export the values -export CFLAGS -export CXXFLAGS diff --git a/contrib/ci/scripts/set_generator_args.sh b/contrib/ci/scripts/set_generator_args.sh deleted file mode 100644 index a704c518b13..00000000000 --- a/contrib/ci/scripts/set_generator_args.sh +++ /dev/null @@ -1,20 +0,0 @@ -# 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"} -: ${Z3_VERBOSE_BUILD_OUTPUT?"Z3_VERBOSE_BUILD_OUTPUT must be specified"} - -GENERATOR_ARGS=('--') -if [ "${Z3_CMAKE_GENERATOR}" = "Unix Makefiles" ]; then - GENERATOR_ARGS+=("-j$(nproc)") - if [ "X${Z3_VERBOSE_BUILD_OUTPUT}" = "X1" ]; then - GENERATOR_ARGS+=("VERBOSE=1") - fi -elif [ "${Z3_CMAKE_GENERATOR}" = "Ninja" ]; then - if [ "X${Z3_VERBOSE_BUILD_OUTPUT}" = "X1" ]; then - GENERATOR_ARGS+=("-v") - fi -else - echo "Unknown CMake generator \"${Z3_CMAKE_GENERATOR}\"" - exit 1 -fi diff --git a/contrib/ci/scripts/test_z3_docs.sh b/contrib/ci/scripts/test_z3_docs.sh deleted file mode 100755 index 6a65ffedd60..00000000000 --- a/contrib/ci/scripts/test_z3_docs.sh +++ /dev/null @@ -1,24 +0,0 @@ -#!/bin/bash - -SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" -. ${SCRIPT_DIR}/run_quiet.sh - -set -x -set -e -set -o pipefail - -: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} -: ${BUILD_DOCS?"BUILD_DOCS must be specified"} - -# Set CMake generator args -source ${SCRIPT_DIR}/set_generator_args.sh - -cd "${Z3_BUILD_DIR}" - -# Generate documentation -if [ "X${BUILD_DOCS}" = "X1" ]; then - # TODO: Make quiet once we've fixed the build - run_quiet cmake --build $(pwd) --target api_docs "${GENERATOR_ARGS[@]}" -fi - -# TODO: Test or perhaps deploy the built docs? diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh deleted file mode 100755 index a149a1d8363..00000000000 --- a/contrib/ci/scripts/test_z3_examples_cmake.sh +++ /dev/null @@ -1,125 +0,0 @@ -#!/bin/bash - -# This script tests Z3 - -SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" -. ${SCRIPT_DIR}/run_quiet.sh - -set -x -set -e -set -o pipefail -: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"} -: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} -: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"} -: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} -: ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"} -: ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"} -: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"} -: ${RUN_API_EXAMPLES?"RUN_API_EXAMPLES must be specified"} - -if [ "X${RUN_API_EXAMPLES}" = "X0" ]; then - echo "Skipping run of API examples" - exit 0 -fi - -# Set compiler flags -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 -cmake --build $(pwd) --target c_example "${GENERATOR_ARGS[@]}" -run_quiet examples/c_example_build_dir/c_example - -# Build and run C++ example -cmake --build $(pwd) --target cpp_example "${GENERATOR_ARGS[@]}" -run_quiet examples/cpp_example_build_dir/cpp_example - -# Build and run tptp5 example -cmake --build $(pwd) --target z3_tptp5 "${GENERATOR_ARGS[@]}" -# FIXME: Do something more useful with example -run_quiet examples/tptp_build_dir/z3_tptp5 -help - -# Build an run c_maxsat_example -cmake --build $(pwd) --target c_maxsat_example "${GENERATOR_ARGS[@]}" -# FIXME: It is known that the maxsat example leaks memory and the -# the Z3 developers have stated this is "wontfix". -# See https://github.com/Z3Prover/z3/issues/1299 -run_no_lsan \ - run_quiet \ - examples/c_maxsat_example_build_dir/c_maxsat_example \ - ${Z3_SRC_DIR}/examples/maxsat/ex.smt - -if [ "X${UBSAN_BUILD}" = "X1" ]; then - # FIXME: We really need libz3 to link against a shared UBSan runtime. - # Right now we link against the static runtime which breaks all the - # non-native language bindings. - echo "FIXME: Can't run other examples when building with UBSan" - exit 0 -fi - - -if [ "X${PYTHON_BINDINGS}" = "X1" ]; then - # Run python examples - # `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? - 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_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/all_interval_series.py - fi - run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/complex.py - run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/example.py - # FIXME: `hamiltonian.py` example is disabled because its too slow. - #${PYTHON_EXECUTABLE} python/hamiltonian.py - run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/marco.py - run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/mss.py - run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/socrates.py - run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/visitor.py - run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/z3test.py -fi - -if [ "X${DOTNET_BINDINGS}" = "X1" ]; then - # Run .NET example - if [ "X${ASAN_BUILD}" = "X1" ]; then - # The dotnet test get stuck on ASAN - # so don't run it for now. - echo "Skipping .NET example under ASan build" - else - run_quiet run_non_native_binding dotnet ${Z3_BUILD_DIR}/dotnet/netcoreapp2.0/dotnet.dll - fi -fi - -if [ "X${JAVA_BINDINGS}" = "X1" ]; then - # Build Java example - # FIXME: Move compilation step into CMake target - mkdir -p examples/java - cp ${Z3_SRC_DIR}/examples/java/JavaExample.java examples/java/ - javac examples/java/JavaExample.java -classpath com.microsoft.z3.jar - # Run Java example - if [ "$(uname)" = "Darwin" ]; then - # macOS - export DYLD_LIBRARY_PATH=$(pwd):${DYLD_LIBRARY_PATH} - else - # Assume Linux for now - export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH} - fi - 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_quiet \ - run_non_native_binding \ - java -cp .:examples/java:com.microsoft.z3.jar JavaExample - fi -fi - diff --git a/contrib/ci/scripts/test_z3_install_cmake.sh b/contrib/ci/scripts/test_z3_install_cmake.sh deleted file mode 100755 index 804158f6f9d..00000000000 --- a/contrib/ci/scripts/test_z3_install_cmake.sh +++ /dev/null @@ -1,24 +0,0 @@ -#!/bin/bash - -SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" - -set -x -set -e -set -o pipefail - -: ${TEST_INSTALL?"TEST_INSTALL must be specified"} -: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} - -if [ "X${TEST_INSTALL}" != "X1" ]; then - echo "Skipping install" - exit 0 -fi - -# Set CMake generator args -source ${SCRIPT_DIR}/set_generator_args.sh - -cd "${Z3_BUILD_DIR}" - -sudo cmake --build $(pwd) --target install "${GENERATOR_ARGS[@]}" - -# TODO: Test the installed version in some way diff --git a/contrib/ci/scripts/test_z3_system_tests.sh b/contrib/ci/scripts/test_z3_system_tests.sh deleted file mode 100755 index 19c17926872..00000000000 --- a/contrib/ci/scripts/test_z3_system_tests.sh +++ /dev/null @@ -1,70 +0,0 @@ -#!/bin/bash - -set -x -set -e -set -o pipefail - -: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} -: ${Z3_BUILD_TYPE?"Z3_BUILD_TYPE must be specified"} -: ${RUN_SYSTEM_TESTS?"RUN_SYSTEM_TESTS must be speicifed"} -: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"} -: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} -: ${Z3_SYSTEM_TEST_DIR?"Z3_SYSTEM_TEST_DIR must be specified"} -: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"} - -if [ "X${RUN_SYSTEM_TESTS}" != "X1" ]; then - echo "Skipping system tests" - exit 0 -fi - -# Sanitizer environment variables -SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" -source ${SCRIPT_DIR}/sanitizer_env.sh - -Z3_EXE="${Z3_BUILD_DIR}/z3" -Z3_LIB_DIR="${Z3_BUILD_DIR}" - -# Set value if not already defined externally -Z3_SYSTEM_TEST_GIT_URL="${Z3_GIT_URL:-https://github.com/Z3Prover/z3test.git}" - -# Clone repo to destination -mkdir -p "${Z3_SYSTEM_TEST_DIR}" -git clone "${Z3_SYSTEM_TEST_GIT_URL}" "${Z3_SYSTEM_TEST_DIR}" -cd "${Z3_SYSTEM_TEST_DIR}" - -if [ -n "${Z3_SYSTEM_TEST_GIT_REVISION}" ]; then - # If a particular revision is requested then check it out. - # This is useful for reproducible builds - git checkout "${Z3_SYSTEM_TEST_GIT_REVISION}" -fi - -############################################################################### -# Run system tests -############################################################################### - -# SMTLIBv2 tests -${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2 - -${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2-extra - -if [ "X${Z3_BUILD_TYPE}" = "XDebug" ]; then - ${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2-debug -fi - -if [ "X${PYTHON_BINDINGS}" = "X1" ]; then - # Run python binding tests - if [ "X${UBSAN_BUILD}" = "X1" ]; then - # FIXME: We need to build libz3 with a shared UBSan runtime for the bindings - # to work. - echo "FIXME: Skipping python binding tests when building with UBSan" - elif [ "X${ASAN_BUILD}" = "X1" ]; then - # FIXME: The `test_pyscripts.py` doesn't propagate LD_PRELOAD - # so under ASan the tests fail to run - # to work. - echo "FIXME: Skipping python binding tests when building with ASan" - else - run_non_native_binding ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/ - fi -fi - -# FIXME: Run `scripts/test_cs.py` once it has been modified to support mono diff --git a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh deleted file mode 100755 index 60c29556b6d..00000000000 --- a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh +++ /dev/null @@ -1,47 +0,0 @@ -#!/bin/bash - -SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" -. ${SCRIPT_DIR}/run_quiet.sh - -set -x -set -e -set -o pipefail - -: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} -: ${RUN_UNIT_TESTS?"RUN_UNIT_TESTS must be specified"} - -# 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() { - # 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 diff --git a/contrib/ci/scripts/travis_ci_entry_point.sh b/contrib/ci/scripts/travis_ci_entry_point.sh deleted file mode 100755 index 41bde72301f..00000000000 --- a/contrib/ci/scripts/travis_ci_entry_point.sh +++ /dev/null @@ -1,18 +0,0 @@ -#!/bin/bash - -SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" - -set -x -set -e -set -o pipefail - -: ${TRAVIS_OS_NAME?"TRAVIS_OS_NAME should be set"} - -if [ "${TRAVIS_OS_NAME}" = "osx" ]; then - ${SCRIPT_DIR}/travis_ci_osx_entry_point.sh -elif [ "${TRAVIS_OS_NAME}" = "linux" ]; then - ${SCRIPT_DIR}/travis_ci_linux_entry_point.sh -else - echo "Unsupported OS \"${TRAVIS_OS_NAME}\"" - exit 1 -fi diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh deleted file mode 100755 index 930fd9d20b9..00000000000 --- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh +++ /dev/null @@ -1,220 +0,0 @@ -#!/bin/bash - -SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" - -set -x -set -e -set -o pipefail - -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=() -# 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 - -if [ -n "${Z3_USE_LIBGMP}" ]; then - BUILD_OPTS+=("--build-arg" "Z3_USE_LIBGMP=${Z3_USE_LIBGMP}") -fi - -if [ -n "${BUILD_DOCS}" ]; then - BUILD_OPTS+=("--build-arg" "BUILD_DOCS=${BUILD_DOCS}") -fi - -if [ -n "${PYTHON_EXECUTABLE}" ]; then - BUILD_OPTS+=("--build-arg" "PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE}") -fi - -if [ -n "${PYTHON_BINDINGS}" ]; then - BUILD_OPTS+=("--build-arg" "PYTHON_BINDINGS=${PYTHON_BINDINGS}") -fi - -if [ -n "${DOTNET_BINDINGS}" ]; then - BUILD_OPTS+=("--build-arg" "DOTNET_BINDINGS=${DOTNET_BINDINGS}") -fi - -if [ -n "${JAVA_BINDINGS}" ]; then - BUILD_OPTS+=("--build-arg" "JAVA_BINDINGS=${JAVA_BINDINGS}") -fi - -if [ -n "${USE_LTO}" ]; then - BUILD_OPTS+=("--build-arg" "USE_LTO=${USE_LTO}") -fi - -if [ -n "${Z3_INSTALL_PREFIX}" ]; then - BUILD_OPTS+=("--build-arg" "Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX}") -fi - -# TravisCI reserves CC for itself so use a different name -if [ -n "${C_COMPILER}" ]; then - BUILD_OPTS+=("--build-arg" "CC=${C_COMPILER}") -fi - -# TravisCI reserves CXX for itself so use a different name -if [ -n "${CXX_COMPILER}" ]; then - BUILD_OPTS+=("--build-arg" "CXX=${CXX_COMPILER}") -fi - -if [ -n "${TARGET_ARCH}" ]; then - BUILD_OPTS+=("--build-arg" "TARGET_ARCH=${TARGET_ARCH}") -fi - -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 "${SANITIZER_PRINT_SUPPRESSIONS}" ]; then - BUILD_OPTS+=("--build-arg" "SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS}") -fi - -if [ -n "${UBSAN_BUILD}" ]; then - BUILD_OPTS+=("--build-arg" "UBSAN_BUILD=${UBSAN_BUILD}") -fi - -if [ -n "${TEST_INSTALL}" ]; then - BUILD_OPTS+=("--build-arg" "TEST_INSTALL=${TEST_INSTALL}") -fi - -if [ -n "${RUN_API_EXAMPLES}" ]; then - BUILD_OPTS+=("--build-arg" "RUN_API_EXAMPLES=${RUN_API_EXAMPLES}") -fi - -if [ -n "${RUN_SYSTEM_TESTS}" ]; then - BUILD_OPTS+=("--build-arg" "RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS}") -fi - -if [ -n "${Z3_SYSTEM_TEST_GIT_REVISION}" ]; then - BUILD_OPTS+=( \ - "--build-arg" \ - "Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION}" \ - ) -fi - -if [ -n "${RUN_UNIT_TESTS}" ]; then - BUILD_OPTS+=("--build-arg" "RUN_UNIT_TESTS=${RUN_UNIT_TESTS}") -fi - -if [ -n "${Z3_VERBOSE_BUILD_OUTPUT}" ]; then - BUILD_OPTS+=( \ - "--build-arg" \ - "Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT}" \ - ) -fi - -if [ -n "${Z3_STATIC_BUILD}" ]; then - BUILD_OPTS+=("--build-arg" "Z3_STATIC_BUILD=${Z3_STATIC_BUILD}") -fi - -if [ -n "${NO_SUPPRESS_OUTPUT}" ]; then - BUILD_OPTS+=( \ - "--build-arg" \ - "NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT}" \ - ) -fi - -if [ -n "${Z3_WARNINGS_AS_ERRORS}" ]; then - BUILD_OPTS+=( \ - "--build-arg" \ - "Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS}" \ - ) -fi - -case ${LINUX_BASE} in - ubuntu_20.04) - BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu_20.04.Dockerfile" - BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu:20.04" - ;; - *) - echo "Unknown Linux base ${LINUX_BASE}" - exit 1 - ;; -esac - -# Initially assume that we need to build the base Docker image -MUST_BUILD=1 - -# Travis CI persistent cache. -# -# This inspired by http://rundef.com/fast-travis-ci-docker-build . -# The idea is to cache the built image for subsequent builds to -# reduce build time. -if [ -n "${DOCKER_TRAVIS_CI_CACHE_DIR}" ]; then - CHECKSUM_FILE="${DOCKER_TRAVIS_CI_CACHE_DIR}/${BASE_DOCKER_IMAGE_NAME}.chksum" - CACHED_DOCKER_IMAGE="${DOCKER_TRAVIS_CI_CACHE_DIR}/${BASE_DOCKER_IMAGE_NAME}.gz" - if [ -f "${CACHED_DOCKER_IMAGE}" ]; then - # There's a cached image to use. Check the checksums of the Dockerfile - # match. If they don't that implies we need to build a fresh image. - if [ -f "${CHECKSUM_FILE}" ]; then - CURRENT_DOCKERFILE_CHECKSUM=$(sha256sum "${BASE_DOCKER_FILE}" | awk '{ print $1 }') - CACHED_DOCKERFILE_CHECKSUM=$(cat "${CHECKSUM_FILE}") - if [ "X${CURRENT_DOCKERFILE_CHECKSUM}" = "X${CACHED_DOCKERFILE_CHECKSUM}" ]; then - # Load the cached image - MUST_BUILD=0 - gunzip --stdout "${CACHED_DOCKER_IMAGE}" | docker load - fi - fi - fi -fi - -if [ "${MUST_BUILD}" -eq 1 ]; then - # The base image contains all the dependencies we want to build - # Z3. - docker build -t "${BASE_DOCKER_IMAGE_NAME}" - < "${BASE_DOCKER_FILE}" - - if [ -n "${DOCKER_TRAVIS_CI_CACHE_DIR}" ]; then - # Write image and checksum to cache - docker save "${BASE_DOCKER_IMAGE_NAME}" | \ - gzip > "${CACHED_DOCKER_IMAGE}" - sha256sum "${BASE_DOCKER_FILE}" | awk '{ print $1 }' > \ - "${CHECKSUM_FILE}" - fi -fi - - -DOCKER_MAJOR_VERSION=$(docker info --format '{{.ServerVersion}}' | sed 's/^\([0-9]\+\)\.\([0-9]\+\).*$/\1/') -DOCKER_MINOR_VERSION=$(docker info --format '{{.ServerVersion}}' | sed 's/^\([0-9]\+\)\.\([0-9]\+\).*$/\2/') -DOCKER_BUILD_FILE="${DOCKER_FILE_DIR}/z3_build.Dockerfile" - -if [ "${DOCKER_MAJOR_VERSION}${DOCKER_MINOR_VERSION}" -lt 1705 ]; then - # Workaround limitation in older Docker versions where the FROM - # command cannot be parameterized with an ARG. - sed \ - -e '/^ARG DOCKER_IMAGE_BASE/d' \ - -e 's/${DOCKER_IMAGE_BASE}/'"${BASE_DOCKER_IMAGE_NAME}/" \ - "${DOCKER_BUILD_FILE}" > "${DOCKER_BUILD_FILE}.patched" - DOCKER_BUILD_FILE="${DOCKER_BUILD_FILE}.patched" -else - # This feature landed in Docker 17.05 - # See https://github.com/moby/moby/pull/31352 - BUILD_OPTS+=( \ - "--build-arg" \ - "DOCKER_IMAGE_BASE=${BASE_DOCKER_IMAGE_NAME}" \ - ) -fi - -# Now build Z3 and test it using the created base image -docker build \ - -f "${DOCKER_BUILD_FILE}" \ - "${BUILD_OPTS[@]}" \ - . diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh deleted file mode 100755 index ad3b0c7ab0c..00000000000 --- a/contrib/ci/scripts/travis_ci_osx_entry_point.sh +++ /dev/null @@ -1,51 +0,0 @@ -#!/bin/bash - -SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" - -set -x -set -e -set -o pipefail - -# 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" - exit 1 -fi - -if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then - echo "TRAVIS_BUILD_DIR must be a directory" - 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_SYSTEM_TEST_DIR="${Z3_SRC_DIR}/z3_system_test" - -# Overwrite whatever what set in TravisCI -export CC="${C_COMPILER}" -export CXX="${CXX_COMPILER}" - -if [ "X${MACOS_SKIP_DEPS_UPDATE}" = "X1" ]; then - # This is just for local testing to avoid updating - echo "Skipping dependency update" -else - "${SCRIPT_DIR}/install_deps_osx.sh" -fi - -# Build Z3 -"${SCRIPT_DIR}/build_z3_cmake.sh" -# Test building docs -"${SCRIPT_DIR}/test_z3_docs.sh" -# Test examples -"${SCRIPT_DIR}/test_z3_examples_cmake.sh" -# Run unit tests -"${SCRIPT_DIR}/test_z3_unit_tests_cmake.sh" -# Run system tests -"${SCRIPT_DIR}/test_z3_system_tests.sh" -# Test install -"${SCRIPT_DIR}/test_z3_install_cmake.sh"