diff --git a/.travis.yml b/.travis.yml index 03e77990b..1892da779 100644 --- a/.travis.yml +++ b/.travis.yml @@ -15,53 +15,38 @@ env: # Configurations matrix: ############################################################################### -# Ubuntu 16.04 LTS +# Ubuntu 18.04 LTS ############################################################################### - # 64-bit UBSan Debug build - - 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 UBSAN_BUILD=1 RUN_UNIT_TESTS=SKIP - # 64-bit ASan Debug build - - 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 ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so - # Build for running unit tests under ASan/UBSan - # FIXME: We should really be doing a debug build but the unit tests run too - # slowly when we do that. - - 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 ASAN_BUILD=1 RUN_UNIT_TESTS=BUILD_AND_RUN ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so UBSAN_BUILD=1 RUN_API_EXAMPLES=0 RUN_SYSTEM_TESTS=0 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0 - - # 64-bit GCC 5.4 RelWithDebInfo - - 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 - # 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 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 RUN_UNIT_TESTS=BUILD_ONLY + # amount of time to execute compared to the optimized builds. - # 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 + # clang + - LINUX_BASE=ubuntu_18.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug UBSAN_BUILD=1 RUN_UNIT_TESTS=BUILD_ONLY + - LINUX_BASE=ubuntu_18.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=BUILD_ONLY + - LINUX_BASE=ubuntu_18.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo ASAN_BUILD=1 RUN_UNIT_TESTS=BUILD_AND_RUN UBSAN_BUILD=1 RUN_API_EXAMPLES=0 RUN_SYSTEM_TESTS=0 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0 + + # gcc + - LINUX_BASE=ubuntu_18.04 C_COMPILER=gcc CXX_COMPILER=g++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release RUN_UNIT_TESTS=BUILD_AND_RUN + - LINUX_BASE=ubuntu_18.04 C_COMPILER=gcc CXX_COMPILER=g++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug UBSAN_BUILD=1 RUN_UNIT_TESTS=BUILD_ONLY + - LINUX_BASE=ubuntu_18.04 C_COMPILER=gcc CXX_COMPILER=g++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=BUILD_ONLY # Both of the two configurations below build the docs because the current # implementation uses python as part of the building process. # TODO: Teach one of the configurations to upload built docs somewhere. # Test with Python 3 and API docs - - LINUX_BASE=ubuntu_16.04 PYTHON_EXECUTABLE=/usr/bin/python3 BUILD_DOCS=1 + - LINUX_BASE=ubuntu_18.04 PYTHON_EXECUTABLE=/usr/bin/python3 BUILD_DOCS=1 # Test with LibGMP and API docs - - LINUX_BASE=ubuntu_16.04 TARGET_ARCH=x86_64 USE_LIBGMP=1 BUILD_DOCS=1 PYTHON_EXECUTABLE=/usr/bin/python2.7 + - LINUX_BASE=ubuntu_18.04 TARGET_ARCH=x86_64 USE_LIBGMP=1 BUILD_DOCS=1 PYTHON_EXECUTABLE=/usr/bin/python2.7 # Unix Makefile generator build - - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_CMAKE_GENERATOR="Unix Makefiles" + - LINUX_BASE=ubuntu_18.04 TARGET_ARCH=x86_64 Z3_CMAKE_GENERATOR="Unix Makefiles" # LTO build - - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 USE_LTO=1 + - LINUX_BASE=ubuntu_18.04 TARGET_ARCH=x86_64 USE_LTO=1 # Static build. Note we have disable building the bindings because they won't work with a static libz3 - - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_STATIC_BUILD=1 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0 + - LINUX_BASE=ubuntu_18.04 TARGET_ARCH=x86_64 Z3_STATIC_BUILD=1 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0 script: diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile deleted file mode 100644 index 6012bb25f..000000000 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile +++ /dev/null @@ -1,52 +0,0 @@ -# This base image is not officially supported by Docker it -# is generated by running -# ``` -# ./update.sh xenial -# ``` -# from git@github.com:daald/docker-brew-ubuntu-core-32bit.git -# at commit 34ea593b40b423755b7d46b6c8c89fc8162ea74b -# -# We could actually store the image generated by this Dockerfile -# rather than just the bare image. However given we have a TravisCI -# cache I'm not sure if it faster to use the TravisCI cache or to -# download from DockerHub everytime. -FROM z3prover/ubuntu32:16.04 - -RUN apt-get update && \ - apt-get -y --no-install-recommends install \ - binutils \ - clang \ - clang-3.9 \ - cmake \ - doxygen \ - default-jdk \ - gcc \ - gcc-5 \ - git \ - graphviz \ - g++ \ - g++ \ - libgmp-dev \ - libgomp1 \ - libomp5 \ - libomp-dev \ - llvm-3.9 \ - make \ - ninja-build \ - python3 \ - python3-setuptools \ - python2.7 \ - python-setuptools \ - sudo - -# 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 -# TODO .NET core does not support Linux x86 yet, disable it for now. -# see: https://github.com/dotnet/coreclr/issues/9265 -ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer DOTNET_BINDINGS=0 diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile deleted file mode 100644 index 9c6bdc054..000000000 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile +++ /dev/null @@ -1,44 +0,0 @@ -FROM ubuntu:14.04 - -RUN apt-get update && \ - apt-get -y --no-install-recommends install \ - apt-transport-https \ - binutils \ - clang-3.9 \ - curl \ - doxygen \ - default-jdk \ - gcc-multilib \ - gcc-4.8-multilib \ - git \ - graphviz \ - g++-multilib \ - g++-4.8-multilib \ - libgmp-dev \ - libgomp1 \ - lib32gomp1 \ - llvm-3.9 \ - make \ - ninja-build \ - python3 \ - python3-setuptools \ - python2.7 \ - python-setuptools - -RUN curl -SL https://packages.microsoft.com/config/ubuntu/14.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 - -RUN curl -SL https://cmake.org/files/v3.12/cmake-3.12.0-Linux-x86_64.sh --output cmake-3.12.0-Linux-x86_64.sh && \ - sh cmake-3.12.0-Linux-x86_64.sh --prefix=/usr/local --exclude-subdir - -# 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-3.9/bin/llvm-symbolizer diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_18.04.Dockerfile similarity index 77% rename from contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile rename to contrib/ci/Dockerfiles/z3_base_ubuntu_18.04.Dockerfile index f4d9c873a..f13571ed1 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_18.04.Dockerfile @@ -1,28 +1,17 @@ -FROM ubuntu:16.04 +FROM ubuntu:18.04 RUN apt-get update && \ apt-get -y --no-install-recommends install \ - apt-transport-https \ - binutils \ - clang \ - clang-3.9 \ cmake \ + make \ + ninja-build \ + clang \ + g++ \ curl \ doxygen \ default-jdk \ - gcc-multilib \ - gcc-5-multilib \ git \ graphviz \ - g++-multilib \ - g++-5-multilib \ - libgmp-dev \ - libgomp1 \ - libomp5 \ - libomp-dev \ - llvm-3.9 \ - make \ - ninja-build \ python3 \ python3-setuptools \ python2.7 \ diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile index f9e5bfe38..6f8c236c5 100644 --- a/contrib/ci/Dockerfiles/z3_build.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile @@ -5,7 +5,6 @@ FROM ${DOCKER_IMAGE_BASE} # Build arguments. This can be changed when invoking # `docker build`. ARG ASAN_BUILD -ARG ASAN_DSO ARG BUILD_DOCS ARG CC ARG CXX @@ -34,7 +33,6 @@ ARG Z3_VERBOSE_BUILD_OUTPUT ENV \ ASAN_BUILD=${ASAN_BUILD} \ - ASAN_DSO=${ASAN_DSO} \ BUILD_DOCS=${BUILD_DOCS} \ CC=${CC} \ CXX=${CXX} \ diff --git a/contrib/ci/scripts/sanitizer_env.sh b/contrib/ci/scripts/sanitizer_env.sh index f1fa87442..f1efd03c8 100644 --- a/contrib/ci/scripts/sanitizer_env.sh +++ b/contrib/ci/scripts/sanitizer_env.sh @@ -29,33 +29,8 @@ if [ "X${ASAN_BUILD}" = "X1" ]; then ASAN_OPTIONS="${ASAN_OPTIONS},detect_leaks=0" "${@}" } - # Check path to ASan DSO - : ${ASAN_DSO?"ASAN_DSO must be specified"} - if [ ! -e "${ASAN_DSO}" ]; then - echo "ASAN_DSO (${ASAN_DSO}) does not exist" - exit 1 - fi - # FIXME: We'll need to refactor this when we can do UBSan builds - # against a UBSan DSO. function run_non_native_binding() { - # We need to preload the ASan DSO that libz3 - # will have undefined references to. - # Don't run leak checking because we get lots reported leaks - # in the language runtime (e.g. python). - PLATFORM="$(uname -s)" - case "${PLATFORM}" in - Linux*) - LD_PRELOAD="${ASAN_DSO}" run_no_lsan "${@}" - ;; - Darwin*) - DYLD_INSERT_LIBRARIES="${ASAN_DSO}" run_no_lsan "${@}" - ;; - *) - echo "Unknown platform \"${PLATFORM}\"" - exit 1 - ;; - esac - unset PLATFORM + "${@}" } else # In non-ASan build just run directly diff --git a/contrib/suppressions/sanitizers/lsan.txt b/contrib/suppressions/sanitizers/lsan.txt index 1480b7c09..a4ce0881a 100644 --- a/contrib/suppressions/sanitizers/lsan.txt +++ b/contrib/suppressions/sanitizers/lsan.txt @@ -1,5 +1 @@ # LeakSanitizer suppression file - -# Ignore Clang OpenMP leaks. -# See https://github.com/Z3Prover/z3/issues/1308 -leak:___kmp_allocate