mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-10-09 12:45:47 +00:00
Code Activity
z3/cmake/z3_add_cxx_flag.cmake

29 lines
1.3 KiB
CMake
Raw Permalink Normal View History

Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
include(CheckCXXCompilerFlag)
include(CMakeParseArguments)
function(z3_add_cxx_flag flag)
[CMake] Change the `WARNINGS_AS_ERRORS` option from BOOL to STRING to allow a new mode `SERIOUS_ONLY`. Modes: `ON` - All warnings are treated as errors (same as before) `OFF` - Warnings are not treated as errors (same as before) `SERIOUS_ONLY` - A subset of "serious" warnings are treated as errors. Upgrade code is included to upgrade old CMake cache's to use the new type of `WARNINGS_AS_ERRORS`. We should remove it eventually. The user's previous setting is preserved when doing this. Very few warnings are treated as errors for now. Developers can add more later as they see fit.
2017-07-09 14:21:27 +01:00
CMAKE_PARSE_ARGUMENTS(z3_add_flag "REQUIRED;GLOBAL" "" "" ${ARGN})
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}")
string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
[CMake] Teach build system to pass `/fp:precise` to compiler when using MSVC. This is set by the old build system but we weren't setting it. This actually MSVC's default but in an effort to try to behave more like the old build system we will set it anyway.
2017-04-28 23:28:04 +01:00
string(REPLACE ":" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
[CMake] Fix missing sanitization in `z3_add_cxx_flag flag()` function which caused CMake 2.8.12 to hit an error when handling the `-std=c++11` flag.
2017-06-24 13:47:51 +01:00
string(REPLACE "+" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
unset(HAS_${SANITIZED_FLAG_NAME})
CHECK_CXX_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME})
if (z3_add_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME})
message(FATAL_ERROR "The flag \"${flag}\" is required but your C++ compiler doesn't support it")
endif()
if (HAS_${SANITIZED_FLAG_NAME})
message(STATUS "C++ compiler supports ${flag}")
[CMake] Change the `WARNINGS_AS_ERRORS` option from BOOL to STRING to allow a new mode `SERIOUS_ONLY`. Modes: `ON` - All warnings are treated as errors (same as before) `OFF` - Warnings are not treated as errors (same as before) `SERIOUS_ONLY` - A subset of "serious" warnings are treated as errors. Upgrade code is included to upgrade old CMake cache's to use the new type of `WARNINGS_AS_ERRORS`. We should remove it eventually. The user's previous setting is preserved when doing this. Very few warnings are treated as errors for now. Developers can add more later as they see fit.
2017-07-09 14:21:27 +01:00
if (z3_add_flag_GLOBAL)
[CMake] Rework the CMake component graph (#10741) TY This PR substantially modernizes Z3's CMake build, replacing a significant amount of hand-rolled dependency bookkeeping with CMake's native target-graph features. The main benefits are: * **Less custom build logic.** The existing component system in `cmake/z3_add_component.cmake` manually walks and records the component-dependency graph. This PR moves that information onto CMake targets themselves, eliminating much of the `Z3_COMPONENT_*` / `Z3_DEPENDENT_*` variable machinery. * **A more accurate target graph.** Component dependencies, generated registration headers, and static-component linking are now modeled directly in CMake rather than reconstructed separately. * **More natural source-tree organization.** `add_subdirectory()` calls no longer need to be kept in a global topological order or reach deeply into the source tree. Forward component dependencies are allowed, so each directory can add its own children in a natural, alphabetical order. * **Better dependency propagation.** External dependencies such as GMP, Threads, and `atomic` are available to the components that actually need them. In particular, non-system GMP installations now work correctly because component targets can see GMP's include path. * **Cleaner package consumption.** Build-only compiler/linker policy is separated from the dependencies exported to static-package consumers, and Z3 behaves more cleanly when included via `add_subdirectory()` or `FetchContent`. * **Less code with the same observable package behavior.** The PR changes 34 files with +566/-902 lines, for a net reduction of roughly 336 lines, while preserving the existing targets, public headers, install layout, and registration behavior. The main enabler is raising the minimum CMake version from 3.16 to **3.30**. CMake 3.30 introduced **custom transitive properties**, which let targets propagate the registered module headers, tactic headers, and memory headers needed for generated registration code. This replaces the custom graph-walking logic previously used to accumulate those headers. As a result, the three functions `z3_add_install_tactic_rule`, `z3_add_memory_initializer_rule`, and `z3_add_gparams_register_modules_rule` are replaced by a single, substantially simpler function, `z3_generate_registration`, which generates the required headers from properties propagated through the target graph. Newer CMake also lets us model chains of `OBJECT` libraries correctly. Historically, only `OBJECT` libraries named directly in `target_link_libraries()` contributed their object files to the final link, which made transitive static-component dependencies awkward to represent. Using `INTERFACE_LINK_LIBRARIES_DIRECT`, those chains can now be expressed directly in the target graph. Every Z3 component also links to a new `INTERFACE` target, `z3_common`. This target owns the external library dependencies that consumers of a component may need, including GMP, Threads, `atomic`, and similar dependencies. Previously, these dependencies were attached only to the final `libz3` target; among other things, that meant individual components could not see the include path for a non-system GMP installation. `z3_common` is exported for static-package consumers, but Z3's own build policy is not. Internal compiler and linker flags now live on a separate `z3_internal_options` target used throughout the build. A possible follow-up is to replace `z3_internal_options` with toolchain files and/or CMake presets, but that would be a more disruptive change and is intentionally left out of this PR. Once CMake itself has an accurate model of the component graph, several pieces of surrounding machinery become unnecessary. We no longer need a topologically sorted list of `add_subdirectory()` calls or the previous requirement that child components be declared before their dependents. Each directory now adds its own subdirectories, in alphabetical order. Public headers are likewise installed through CMake file sets instead of hand-written `install(FILES ...)` rules. The CMake version bump also enables a few smaller cleanups: * use `GENERATOR_IS_MULTI_CONFIG` instead of inferring that from whether `CMAKE_CONFIGURATION_TYPES` is defined; * use `PROJECT_IS_TOP_LEVEL` guards so Z3 behaves correctly when consumed as a subdirectory or through `FetchContent`; * use `block()` instead of manually saving and restoring state around the Python `find_package()` call. One unrelated fix is included alongside these changes: the .NET example now stages its `csproj` and `Program.cs` into the build tree with `add_custom_command()` rather than `configure_file(..., COPYONLY)`, so the `dotnet` build target correctly notices source changes. Overall, the PR moves responsibility for dependency propagation and graph structure out of Z3's custom CMake code and back into CMake itself. The result is a smaller build system with fewer ordering constraints and less duplicated state, while keeping the package's externally visible behavior unchanged.
2026-09-06 05:37:34 -04:00
target_compile_options(z3_internal_options INTERFACE "${flag}")
target_link_options(z3_internal_options INTERFACE "${flag}")
[CMake] Change the `WARNINGS_AS_ERRORS` option from BOOL to STRING to allow a new mode `SERIOUS_ONLY`. Modes: `ON` - All warnings are treated as errors (same as before) `OFF` - Warnings are not treated as errors (same as before) `SERIOUS_ONLY` - A subset of "serious" warnings are treated as errors. Upgrade code is included to upgrade old CMake cache's to use the new type of `WARNINGS_AS_ERRORS`. We should remove it eventually. The user's previous setting is preserved when doing this. Very few warnings are treated as errors for now. Developers can add more later as they see fit.
2017-07-09 14:21:27 +01:00
else()
[CMake] Rework the CMake component graph (#10741) TY This PR substantially modernizes Z3's CMake build, replacing a significant amount of hand-rolled dependency bookkeeping with CMake's native target-graph features. The main benefits are: * **Less custom build logic.** The existing component system in `cmake/z3_add_component.cmake` manually walks and records the component-dependency graph. This PR moves that information onto CMake targets themselves, eliminating much of the `Z3_COMPONENT_*` / `Z3_DEPENDENT_*` variable machinery. * **A more accurate target graph.** Component dependencies, generated registration headers, and static-component linking are now modeled directly in CMake rather than reconstructed separately. * **More natural source-tree organization.** `add_subdirectory()` calls no longer need to be kept in a global topological order or reach deeply into the source tree. Forward component dependencies are allowed, so each directory can add its own children in a natural, alphabetical order. * **Better dependency propagation.** External dependencies such as GMP, Threads, and `atomic` are available to the components that actually need them. In particular, non-system GMP installations now work correctly because component targets can see GMP's include path. * **Cleaner package consumption.** Build-only compiler/linker policy is separated from the dependencies exported to static-package consumers, and Z3 behaves more cleanly when included via `add_subdirectory()` or `FetchContent`. * **Less code with the same observable package behavior.** The PR changes 34 files with +566/-902 lines, for a net reduction of roughly 336 lines, while preserving the existing targets, public headers, install layout, and registration behavior. The main enabler is raising the minimum CMake version from 3.16 to **3.30**. CMake 3.30 introduced **custom transitive properties**, which let targets propagate the registered module headers, tactic headers, and memory headers needed for generated registration code. This replaces the custom graph-walking logic previously used to accumulate those headers. As a result, the three functions `z3_add_install_tactic_rule`, `z3_add_memory_initializer_rule`, and `z3_add_gparams_register_modules_rule` are replaced by a single, substantially simpler function, `z3_generate_registration`, which generates the required headers from properties propagated through the target graph. Newer CMake also lets us model chains of `OBJECT` libraries correctly. Historically, only `OBJECT` libraries named directly in `target_link_libraries()` contributed their object files to the final link, which made transitive static-component dependencies awkward to represent. Using `INTERFACE_LINK_LIBRARIES_DIRECT`, those chains can now be expressed directly in the target graph. Every Z3 component also links to a new `INTERFACE` target, `z3_common`. This target owns the external library dependencies that consumers of a component may need, including GMP, Threads, `atomic`, and similar dependencies. Previously, these dependencies were attached only to the final `libz3` target; among other things, that meant individual components could not see the include path for a non-system GMP installation. `z3_common` is exported for static-package consumers, but Z3's own build policy is not. Internal compiler and linker flags now live on a separate `z3_internal_options` target used throughout the build. A possible follow-up is to replace `z3_internal_options` with toolchain files and/or CMake presets, but that would be a more disruptive change and is intentionally left out of this PR. Once CMake itself has an accurate model of the component graph, several pieces of surrounding machinery become unnecessary. We no longer need a topologically sorted list of `add_subdirectory()` calls or the previous requirement that child components be declared before their dependents. Each directory now adds its own subdirectories, in alphabetical order. Public headers are likewise installed through CMake file sets instead of hand-written `install(FILES ...)` rules. The CMake version bump also enables a few smaller cleanups: * use `GENERATOR_IS_MULTI_CONFIG` instead of inferring that from whether `CMAKE_CONFIGURATION_TYPES` is defined; * use `PROJECT_IS_TOP_LEVEL` guards so Z3 behaves correctly when consumed as a subdirectory or through `FetchContent`; * use `block()` instead of manually saving and restoring state around the Python `find_package()` call. One unrelated fix is included alongside these changes: the .NET example now stages its `csproj` and `Program.cs` into the build tree with `add_custom_command()` rather than `configure_file(..., COPYONLY)`, so the `dotnet` build target correctly notices source changes. Overall, the PR moves responsibility for dependency propagation and graph structure out of Z3's custom CMake code and back into CMake itself. The result is a smaller build system with fewer ordering constraints and less duplicated state, while keeping the package's externally visible behavior unchanged.
2026-09-06 05:37:34 -04:00
target_compile_options(z3_internal_options INTERFACE "${flag}")
[CMake] Change the `WARNINGS_AS_ERRORS` option from BOOL to STRING to allow a new mode `SERIOUS_ONLY`. Modes: `ON` - All warnings are treated as errors (same as before) `OFF` - Warnings are not treated as errors (same as before) `SERIOUS_ONLY` - A subset of "serious" warnings are treated as errors. Upgrade code is included to upgrade old CMake cache's to use the new type of `WARNINGS_AS_ERRORS`. We should remove it eventually. The user's previous setting is preserved when doing this. Very few warnings are treated as errors for now. Developers can add more later as they see fit.
2017-07-09 14:21:27 +01:00
endif()
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
else()
message(STATUS "C++ compiler does not support ${flag}")
endif()
endfunction()
Copy permalink