From 8313282cda10bbdc50d376b9ec59ae99652f9417 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sat, 2 Jul 2022 21:04:09 +0700 Subject: [PATCH 01/13] Use char version of find_last_of when possible. --- src/test/lp/lp.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index d7329309c..bc67ce1c6 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -1885,7 +1885,7 @@ void test_out_dir(std::string out_dir) { void find_dir_and_file_name(std::string a, std::string & dir, std::string& fn) { // todo: make it system independent - size_t last_slash_pos = a.find_last_of("/"); + size_t last_slash_pos = a.find_last_of('/'); if (last_slash_pos >= a.size()) { std::cout << "cannot find file name in " << a << std::endl; throw; From 42f50474631eb3cb1159a8df45a50aed276bba49 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sat, 2 Jul 2022 21:04:20 +0700 Subject: [PATCH 02/13] cmake: Cleanup remnants of workaround for USES_TERMINAL. In older versions, this was dependent upon the version of cmake, but when it was updated for newer cmake, these remnants were left. --- CMakeLists.txt | 9 +-------- cmake/z3_add_component.cmake | 8 ++++---- doc/CMakeLists.txt | 2 +- src/CMakeLists.txt | 2 +- src/api/CMakeLists.txt | 2 +- src/api/dotnet/CMakeLists.txt | 4 ++-- src/api/java/CMakeLists.txt | 4 ++-- src/api/python/CMakeLists.txt | 4 ++-- src/ast/pattern/CMakeLists.txt | 2 +- 9 files changed, 15 insertions(+), 22 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index e3fb1860b..2ca176568 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -10,13 +10,6 @@ project(Z3 VERSION 4.11.0.0 LANGUAGES CXX) set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified message(STATUS "Z3 version ${Z3_VERSION}") -################################################################################ -# Set various useful variables depending on CMake version -################################################################################ - -set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "USES_TERMINAL") -set(ADD_CUSTOM_TARGET_USES_TERMINAL_ARG "USES_TERMINAL") - ################################################################################ # Message for polluted source tree sanity checks ################################################################################ @@ -482,7 +475,7 @@ add_custom_target(uninstall COMMAND "${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake" COMMENT "Uninstalling..." - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL VERBATIM ) diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake index 47ecb04aa..aa5f8517f 100644 --- a/cmake/z3_add_component.cmake +++ b/cmake/z3_add_component.cmake @@ -122,7 +122,7 @@ macro(z3_add_component component_name) ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating \"${_full_output_file_path}\" from \"${pyg_file}\"" WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL VERBATIM ) list(APPEND _list_generated_headers "${_full_output_file_path}") @@ -283,7 +283,7 @@ macro(z3_add_install_tactic_rule) ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps" COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\"" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL VERBATIM ) unset(_expanded_components) @@ -321,7 +321,7 @@ macro(z3_add_memory_initializer_rule) ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${_mem_init_finalize_headers} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp\"" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL VERBATIM ) unset(_mem_init_finalize_headers) @@ -357,7 +357,7 @@ macro(z3_add_gparams_register_modules_rule) ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${_register_module_header_files} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp\"" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL VERBATIM ) unset(_expanded_components) diff --git a/doc/CMakeLists.txt b/doc/CMakeLists.txt index e37ca131f..54ba73fb0 100644 --- a/doc/CMakeLists.txt +++ b/doc/CMakeLists.txt @@ -69,7 +69,7 @@ add_custom_target(api_docs ${ALWAYS_BUILD_DOCS_ARG} DEPENDS ${DOC_EXTRA_DEPENDS} COMMENT "Generating documentation" - ${ADD_CUSTOM_TARGET_USES_TERMINAL_ARG} + USES_TERMINAL ) # Remove generated documentation when running `clean` target. diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 51fafb42f..5be29c950 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -204,7 +204,7 @@ if (MSVC) ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} COMMENT "Generating \"${dll_module_exports_file}\"" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL VERBATIM ) add_custom_target(libz3_extra_depends diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index 983180985..f00a2732b 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -29,7 +29,7 @@ add_custom_command(OUTPUT ${generated_files} # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency "${PROJECT_SOURCE_DIR}/scripts/mk_util.py" COMMENT "Generating ${generated_files}" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL VERBATIM ) diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 1e9f598e7..82abfbf09 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -19,7 +19,7 @@ add_custom_command(OUTPUT "${Z3_DOTNET_NATIVE_FILE}" "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating ${Z3_DOTNET_NATIVE_FILE}" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL ) # Generate Enumerations.cs @@ -35,7 +35,7 @@ add_custom_command(OUTPUT "${Z3_DOTNET_CONST_FILE}" "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating ${Z3_DOTNET_CONST_FILE}" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL ) set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 695c946a3..cb73702fe 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -32,7 +32,7 @@ add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}" # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency "${PROJECT_SOURCE_DIR}/scripts/mk_util.py" COMMENT "Generating \"${Z3_JAVA_NATIVE_JAVA}\" and \"${Z3_JAVA_NATIVE_CPP}\"" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL ) # Add rule to build native code that provides a bridge between @@ -88,7 +88,7 @@ add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH} "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating ${Z3_JAVA_PACKAGE_NAME}.enumerations package" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL ) set(Z3_JAVA_JAR_SOURCE_FILES diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 067a25e8c..f5e449ea8 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -43,7 +43,7 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3core.py" "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating z3core.py" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL ) list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3core.py") @@ -59,7 +59,7 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3consts.py" "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating z3consts.py" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL ) list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3consts.py") diff --git a/src/ast/pattern/CMakeLists.txt b/src/ast/pattern/CMakeLists.txt index 8d0cf0cb4..7393b7110 100644 --- a/src/ast/pattern/CMakeLists.txt +++ b/src/ast/pattern/CMakeLists.txt @@ -15,7 +15,7 @@ add_custom_command(OUTPUT "database.h" DEPENDS "${PROJECT_SOURCE_DIR}/scripts/mk_pat_db.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating \"database.h\"" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + USES_TERMINAL VERBATIM ) From 774ce3d7ab40ce3e77587882b3aa72db9d0e5d3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Aug 2022 07:36:39 +0300 Subject: [PATCH 03/13] create special case for osx arm shortcut when store/select are distinct Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 5 ++++- src/smt/theory_array.cpp | 4 ++-- src/smt/theory_array_base.cpp | 6 ++++++ 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 781961259..1fbff9cdb 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1830,8 +1830,11 @@ class JavaDLLComponent(Component): if IS_WINDOWS: # On Windows, CL creates a .lib file to link against. out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' % os.path.join('api', 'java', 'Native')) + elif IS_OSX and IS_ARCH_ARM64: + out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) -arch arm64 %s$(OBJ_EXT) libz3$(SO_EXT)\n' % + os.path.join('api', 'java', 'Native')) else: - out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) $(SLINK_EXTRA_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' % + out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' % os.path.join('api', 'java', 'Native')) out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name) deps = '' diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 9d3e93839..1f842c2ed 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -91,9 +91,9 @@ namespace smt { d->m_parent_selects.push_back(s); TRACE("array", tout << v << " " << mk_pp(s->get_expr(), m) << " " << mk_pp(get_enode(v)->get_expr(), m) << "\n";); m_trail_stack.push(push_back_trail(d->m_parent_selects)); - for (enode* n : d->m_stores) { + for (enode* n : d->m_stores) instantiate_axiom2a(s, n); - } + if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) { for (enode* store : d->m_parent_stores) { SASSERT(is_store(store)); diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 1be88a6de..8d545d3b4 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -179,6 +179,12 @@ namespace smt { conseq_expr = ctx.bool_var2expr(conseq.var()); } + if (m.are_distinct(idx1->get_expr(), idx2->get_expr())) { + ctx.mark_as_relevant(conseq); + assert_axiom(conseq); + continue; + } + literal ante = mk_eq(idx1->get_expr(), idx2->get_expr(), true); ctx.mark_as_relevant(ante); // ctx.force_phase(ante); From 3ab96281ebbd076f3916eee1b81a2b6f6245500e Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Aug 2022 22:49:47 +0700 Subject: [PATCH 04/13] 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 230c690a6..000000000 --- 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 9ef85c673..000000000 --- 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 f6e05fcb5..000000000 --- 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 9a8262e37..000000000 --- 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 caa6798c6..000000000 --- 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 63b9410d8..000000000 --- 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 d524503c7..000000000 --- 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 64530e5f3..000000000 --- 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 0f49da3be..000000000 --- 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 1a16b98a6..000000000 --- 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 7efdecdac..000000000 --- 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 a704c518b..000000000 --- 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 6a65ffedd..000000000 --- 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 a149a1d83..000000000 --- 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 804158f6f..000000000 --- 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 19c179268..000000000 --- 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 60c29556b..000000000 --- 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 41bde7230..000000000 --- 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 930fd9d20..000000000 --- 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 ad3b0c7ab..000000000 --- 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" From 112dba559fb0a9f23f69a66f45c87d3bd5d3b74b Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Aug 2022 23:34:48 +0700 Subject: [PATCH 05/13] Remove unused private member from smaller_pattern. --- src/ast/pattern/pattern_inference.cpp | 2 +- src/ast/pattern/pattern_inference.h | 5 +---- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index 09f583df4..d751a1388 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -106,7 +106,7 @@ pattern_inference_cfg::pattern_inference_cfg(ast_manager & m, pattern_inference_ m_params(params), m_bfid(m.get_basic_family_id()), m_afid(m.mk_family_id("arith")), - m_le(m), + m_le(), m_nested_arith_only(true), m_block_loop_patterns(params.m_pi_block_loop_patterns), m_candidates(m), diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h index 28218ee17..bb4cf4238 100644 --- a/src/ast/pattern/pattern_inference.h +++ b/src/ast/pattern/pattern_inference.h @@ -37,7 +37,6 @@ Revision History: every instance of f(g(X)) is also an instance of f(X). */ class smaller_pattern { - ast_manager & m; ptr_vector m_bindings; typedef std::pair expr_pair; @@ -50,9 +49,7 @@ class smaller_pattern { public: - smaller_pattern(ast_manager & m): - m(m) { - } + smaller_pattern() = default; smaller_pattern & operator=(smaller_pattern const &) = delete; From 55b70b4c7e39c2a39901dc1856bcaf00d3cd84b1 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 3 Aug 2022 00:29:22 +0700 Subject: [PATCH 06/13] Remove contrib/cmake. This mainly contained a bootstrap script that did nothing except say that it would be deleted soon. It has been 5 years, so it should be safe to go away now. --- contrib/cmake/bootstrap.py | 48 ------------------------ contrib/cmake/maintainers.txt | 3 -- contrib/cmake/src/test/lp/CMakeLists.txt | 6 --- 3 files changed, 57 deletions(-) delete mode 100755 contrib/cmake/bootstrap.py delete mode 100644 contrib/cmake/maintainers.txt delete mode 100644 contrib/cmake/src/test/lp/CMakeLists.txt diff --git a/contrib/cmake/bootstrap.py b/contrib/cmake/bootstrap.py deleted file mode 100755 index dac08b383..000000000 --- a/contrib/cmake/bootstrap.py +++ /dev/null @@ -1,48 +0,0 @@ -#!/usr/bin/env python -""" -This script is an artifact of compromise that was -made when the CMake build system was first introduced -(see #461). - -This script now does nothing. It remains only to not -break out-of-tree scripts that build Z3 using CMake. - -Eventually this script will be removed. -""" -import argparse -import logging -import os -import pprint -import shutil -import sys - -def main(args): - logging.basicConfig(level=logging.INFO) - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument('mode', - choices=['create', 'remove'], - help='The mode to use') - parser.add_argument("-l","--log-level", - type=str, - default="info", - dest="log_level", - choices=['debug','info','warning','error'] - ) - parser.add_argument("-H", "--hard-link", - action='store_true', - default=False, - dest='hard_link', - help='When using the create mode create hard links instead of copies' - ) - pargs = parser.parse_args(args) - - logLevel = getattr(logging, pargs.log_level.upper(),None) - logging.basicConfig(level=logLevel) - logging.warning('Use of this script is deprecated. The script will be removed in the future') - logging.warning('Action "{}" ignored'.format(pargs.mode)) - if pargs.hard_link: - logging.warning('Hard link option ignored') - return 0 - -if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) diff --git a/contrib/cmake/maintainers.txt b/contrib/cmake/maintainers.txt deleted file mode 100644 index caa6798c6..000000000 --- a/contrib/cmake/maintainers.txt +++ /dev/null @@ -1,3 +0,0 @@ -# Maintainers - -- Dan Liew (@delcypher) diff --git a/contrib/cmake/src/test/lp/CMakeLists.txt b/contrib/cmake/src/test/lp/CMakeLists.txt deleted file mode 100644 index 6683a1758..000000000 --- a/contrib/cmake/src/test/lp/CMakeLists.txt +++ /dev/null @@ -1,6 +0,0 @@ -add_executable(lp_tst lp_main.cpp lp.cpp $ $ $ $ ) -target_compile_definitions(lp_tst PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) -target_compile_options(lp_tst PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) -target_include_directories(lp_tst PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) -target_link_libraries(lp_tst PRIVATE ${Z3_DEPENDENT_LIBS}) -z3_append_linker_flag_list_to_target(lp_tst ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) From d8c99480c67efba789b39717ae04db07524b3bd4 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 3 Aug 2022 00:43:46 +0700 Subject: [PATCH 07/13] test/lp: Replace if linux with if not windows. This is stuff that works on posix, so we can flip the check. --- src/test/lp/lp.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index bc67ce1c6..04afd8f96 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -19,7 +19,7 @@ --*/ #include -#if _LINUX_ +#ifndef _WINDOWS #include #endif #include @@ -1735,7 +1735,7 @@ void random_test() { } } -#if _LINUX_ +#ifndef _WINDOWS void fill_file_names(vector &file_names, std::set & minimums) { char *home_dir = getenv("HOME"); if (home_dir == nullptr) { @@ -4072,7 +4072,7 @@ void test_lp_local(int argn, char**argv) { } if (args_parser.option_is_used("--solve_some_mps")) { -#if _LINUX_ +#ifndef _WINDOWS solve_some_mps(args_parser); #endif ret = 0; From d908ebec4ceb3e476da2d86017dfe51e443929ad Mon Sep 17 00:00:00 2001 From: Saloed Date: Wed, 3 Aug 2022 12:50:52 +0300 Subject: [PATCH 08/13] fix memory_high_watermark parameter according to documentation --- src/util/env_params.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/env_params.cpp b/src/util/env_params.cpp index 3ba6df735..db2c9a890 100644 --- a/src/util/env_params.cpp +++ b/src/util/env_params.cpp @@ -28,7 +28,7 @@ void env_params::updt_params() { enable_warning_messages(p.get_bool("warning", true)); memory::set_max_size(megabytes_to_bytes(p.get_uint("memory_max_size", 0))); memory::set_max_alloc_count(p.get_uint("memory_max_alloc_count", 0)); - memory::set_high_watermark(p.get_uint("memory_high_watermark", 0)); + memory::set_high_watermark(megabytes_to_bytes(p.get_uint("memory_high_watermark", 0))); } void env_params::collect_param_descrs(param_descrs & d) { From 85b96dc877521a62cc00e0c1ad3613f2194bebef Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 3 Aug 2022 15:24:23 +0700 Subject: [PATCH 09/13] cmake: Remove telling the Intel compiler to link OpenMP. This also removes a duplicated branch since the Intel compiler is already handled at the same time as GCC and Clang, so it doesn't need its own block as well. --- CMakeLists.txt | 8 -------- 1 file changed, 8 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 2ca176568..16ff2691d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -276,15 +276,7 @@ endif() # FIXME: Support ARM "-mfpu=vfp -mfloat-abi=hard" if ((TARGET_ARCHITECTURE STREQUAL "x86_64") OR (TARGET_ARCHITECTURE STREQUAL "i686")) if ((CMAKE_CXX_COMPILER_ID MATCHES "GNU") OR (CMAKE_CXX_COMPILER_ID MATCHES "Clang") OR (CMAKE_CXX_COMPILER_ID MATCHES "Intel")) - if (CMAKE_CXX_COMPILER_ID MATCHES "Intel") - # Intel's compiler requires linking with libiomp5 - list(APPEND Z3_DEPENDENT_LIBS "iomp5") - endif() set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2") - elseif (CMAKE_CXX_COMPILER_ID MATCHES "Intel") - set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2") - # Intel's compiler requires linking with libiomp5 - list(APPEND Z3_DEPENDENT_LIBS "iomp5") elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC") set(SSE_FLAGS "/arch:SSE2") else() From dc75031a369abc1ec36b8060aaf17d07d8d0e9ea Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 3 Aug 2022 15:21:23 +0700 Subject: [PATCH 10/13] Remove all per-OS defines apart from _WINDOWS. These are all unused and shouldn't be needed. Mostly we need something for differentiating between POSIX and non-POSIX (until we can reduce some of those differences as well). We shouldn't need to modify the build system to build on a new OS if it is basically a Unix and is supported by cmake. --- CMakeLists.txt | 26 +------------------------- scripts/mk_util.py | 16 ---------------- 2 files changed, 1 insertion(+), 41 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 16ff2691d..8c3d007f0 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -178,32 +178,10 @@ set(CMAKE_CXX_STANDARD_REQUIRED ON) ################################################################################ # Platform detection ################################################################################ -if (CMAKE_SYSTEM_NAME STREQUAL "Linux") - message(STATUS "Platform: Linux") - list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_LINUX_") -elseif (CMAKE_SYSTEM_NAME STREQUAL "Android") - message(STATUS "Platform: Android") - list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_ANDROID_") -elseif (CMAKE_SYSTEM_NAME MATCHES "GNU") - message(STATUS "Platform: GNU/Hurd") - list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_HURD_") -elseif (CMAKE_SYSTEM_NAME STREQUAL "Darwin") +if (CMAKE_SYSTEM_NAME STREQUAL "Darwin") if (TARGET_ARCHITECTURE STREQUAL "arm64") set(CMAKE_OSX_ARCHITECTURES "arm64") endif() - message(STATUS "Platform: Darwin") -elseif (CMAKE_SYSTEM_NAME MATCHES "FreeBSD") - message(STATUS "Platform: FreeBSD") - list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_") -elseif (CMAKE_SYSTEM_NAME MATCHES "NetBSD") - message(STATUS "Platform: NetBSD") - list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NetBSD_") -elseif (CMAKE_SYSTEM_NAME MATCHES "OpenBSD") - message(STATUS "Platform: OpenBSD") - list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_") -elseif (CYGWIN) - message(STATUS "Platform: Cygwin") - list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_CYGWIN") elseif (WIN32) message(STATUS "Platform: Windows") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS") @@ -216,8 +194,6 @@ elseif (EMSCRIPTEN) "-s DISABLE_EXCEPTION_CATCHING=0" "-s ERROR_ON_UNDEFINED_SYMBOLS=1" ) -else() - message(FATAL_ERROR "Platform \"${CMAKE_SYSTEM_NAME}\" not recognised") endif() list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 1fbff9cdb..83171ab66 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2594,46 +2594,30 @@ def mk_config(): SO_EXT = '.dylib' SLIBFLAGS = '-dynamiclib' elif sysname == 'Linux': - CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS - OS_DEFINES = '-D_LINUX_' SO_EXT = '.so' SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS elif sysname == 'GNU': - CXXFLAGS = '%s -D_HURD_' % CXXFLAGS - OS_DEFINES = '-D_HURD_' SO_EXT = '.so' SLIBFLAGS = '-shared' elif sysname == 'FreeBSD': - CXXFLAGS = '%s -D_FREEBSD_' % CXXFLAGS - OS_DEFINES = '-D_FREEBSD_' SO_EXT = '.so' SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS elif sysname == 'NetBSD': - CXXFLAGS = '%s -D_NETBSD_' % CXXFLAGS - OS_DEFINES = '-D_NETBSD_' SO_EXT = '.so' SLIBFLAGS = '-shared' elif sysname == 'OpenBSD': - CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS - OS_DEFINES = '-D_OPENBSD_' SO_EXT = '.so' SLIBFLAGS = '-shared' elif sysname == 'SunOS': - CXXFLAGS = '%s -D_SUNOS_' % CXXFLAGS - OS_DEFINES = '-D_SUNOS_' SO_EXT = '.so' SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -mimpure-text' % SLIBEXTRAFLAGS elif sysname.startswith('CYGWIN'): - CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS - OS_DEFINES = '-D_CYGWIN' SO_EXT = '.dll' SLIBFLAGS = '-shared' elif sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'): - CXXFLAGS = '%s -D_MINGW' % CXXFLAGS - OS_DEFINES = '-D_MINGW' SO_EXT = '.dll' SLIBFLAGS = '-shared' EXE_EXT = '.exe' From ad4c786ea4c3b75409d6ce63be50d9d5d6713e84 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Thu, 4 Aug 2022 09:31:14 +0700 Subject: [PATCH 11/13] mk_unix_dist.py: Fix --nopython Writing to the global PYTHON_ENABLED requires that it be flagged as a global. --- scripts/mk_unix_dist.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index d152b3625..3b1e71391 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -66,7 +66,7 @@ def display_help(): # Parse configuration option for mk_make script def parse_options(): - global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, OS_NAME + global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED, OS_NAME path = BUILD_DIR options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 'help', From 8a3556e5bad1be47d535712b51177b5a5cf78c12 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 3 Aug 2022 23:47:21 +0700 Subject: [PATCH 12/13] cmake: Remove dep on mk_util.py for update_api.py calls. update_api.py doesn't depend on mk_util.py any longer, so these dependencies can go away. --- src/api/CMakeLists.txt | 2 -- src/api/java/CMakeLists.txt | 2 -- 2 files changed, 4 deletions(-) diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index f00a2732b..08ea9ce29 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -26,8 +26,6 @@ add_custom_command(OUTPUT ${generated_files} DEPENDS "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} - # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency - "${PROJECT_SOURCE_DIR}/scripts/mk_util.py" COMMENT "Generating ${generated_files}" USES_TERMINAL VERBATIM diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index cb73702fe..e0d6bd0a0 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -29,8 +29,6 @@ add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} - # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency - "${PROJECT_SOURCE_DIR}/scripts/mk_util.py" COMMENT "Generating \"${Z3_JAVA_NATIVE_JAVA}\" and \"${Z3_JAVA_NATIVE_CPP}\"" USES_TERMINAL ) From a3161bdc155f66a619ae740887cb267e57dd0e97 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 3 Aug 2022 23:40:01 +0700 Subject: [PATCH 13/13] update_api.py: Remove usage of MKException. This wasn't working as it was being accessed from a function object rather than the module. Instead, let's just print the error and exit. --- scripts/update_api.py | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index a468a6885..37b8a31af 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -16,7 +16,6 @@ emit some of the files required for Z3's different language bindings. """ -import mk_exception import argparse import logging import re @@ -1700,8 +1699,8 @@ def def_APIs(api_files): m = pat2.match(line) if m: eval(line) - except Exception: - raise mk_exec_header.MKException("Failed to process API definition: %s" % line) + except Exception as e: + error('ERROR: While processing: %s: %s\n' % (e, line)) def write_log_h_preamble(log_h): log_h.write('// Automatically generated file\n')