mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-09-16 01:24:24 +00:00
Code Activity
z3/cmake/compiler_warnings.cmake
Alex Reinking c2c198d553
[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 02:37:34 -07:00

180 lines
6.7 KiB
CMake
Raw Permalink Blame History

################################################################################
# Compiler warning flags
################################################################################
# These are passed to relevant compiler provided they are supported
set(GCC_AND_CLANG_WARNINGS
"-Wall"
)
set(GCC_ONLY_WARNINGS "")
# Disable C++98 compatibility warnings to prevent excessive warning output
# when building with clang-cl or when -Weverything is enabled.
# These warnings are not useful for Z3 since it requires C++20.
#
# The "-Wno-zero-length-array" is for cases where Z3 is fetched by a CMake build
# to serve as a component in another system. Z3 has many classes whose last member
# is a zero-length array of some type T, indicating a variable-length array of T.
# If the including system compiles with "-Wzero-length-array", there will be
# many warnings. Overriding this prevents such warnings in the Z3 portion of the
# build of the including system.
set(CLANG_ONLY_WARNINGS
"-Wno-c++98-compat"
"-Wno-c++98-compat-pedantic"
"-Wno-zero-length-array"
"-Wc99-extensions"
"-Wsuggest-override"
"-Winconsistent-missing-override"
"-Wno-missing-field-initializers"
"-Wcast-qual"
"-Wimplicit-fallthrough"
"-Wextra-semi"
"-Wignored-qualifiers"
"-Wnoctad-maybe-unsupported"
"-Wdeprecated-copy-with-user-provided-copy"
"-Wgnu-anonymous-struct"
"-Wcovered-switch-default"
)
set(MSVC_WARNINGS "/W3")
################################################################################
# Serious warnings
################################################################################
# This declares the flags that are passed to the compiler when
# `WARNINGS_AS_ERRORS` is set to `SERIOUS_ONLY`. Only flags that are supported
# by the compiler are used.
#
# In effect this a "whitelist" approach where we explicitly tell the compiler
# which warnings we want to be treated as errors. The alternative would be a
# "blacklist" approach where we ask the compiler to treat all warnings are
# treated as errors but then we explicitly list which warnings which should be
# allowed.
#
# The "whitelist" approach seems simpiler because we can incrementally add
# warnings we "think are serious".
# TODO: Add more warnings that are considered serious enough that we should
# treat them as errors.
set(GCC_AND_CLANG_WARNINGS_AS_ERRORS
# https://clang.llvm.org/docs/DiagnosticsReference.html#wodr
"-Werror=odr"
# https://clang.llvm.org/docs/DiagnosticsReference.html#wreturn-type
"-Werror=return-type"
)
set(GCC_WARNINGS_AS_ERRORS
""
)
set(CLANG_WARNINGS_AS_ERRORS
# https://clang.llvm.org/docs/DiagnosticsReference.html#wdelete-non-virtual-dtor
"-Werror=delete-non-virtual-dtor"
# https://clang.llvm.org/docs/DiagnosticsReference.html#woverloaded-virtual
"-Werror=overloaded-virtual"
# warn the user if a class with virtual functions has a
# non-virtual destructor. This helps catch hard to
# track down memory errors
"-Werror=non-virtual-dtor"
# warn if a null dereference is detected
"-Werror=null-dereference"
# warn for potential performance problem casts
# "-Werror=cast-align"
# warn if float is implicit promoted to double
# "-Werror=double-promotion"
"-Werror=no-unreachable-code-return"
# warn the user if a variable declaration shadows one from a parent context
# "-Werror=shadow"
# warn for c-style casts
# "-Werror=old-style-cast"
# warn on sign conversions
# "-Werror=sign-conversion"
# warn on type conversions that may lose data
# "-Werror=conversion"
# warn on anything being unused
# "-Werror=unused"
)
################################################################################
# Test warning/error flags
################################################################################
set(WARNING_FLAGS_TO_CHECK "")
set(WARNING_AS_ERROR_FLAGS_TO_CHECK "")
if (CMAKE_CXX_COMPILER_ID MATCHES "GNU")
list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS})
list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS})
list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS})
list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_WARNINGS_AS_ERRORS})
elseif (CMAKE_CXX_COMPILER_ID MATCHES "Clang")
list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS})
list(APPEND WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS})
list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS})
list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${CLANG_WARNINGS_AS_ERRORS})
elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS})
else()
message(AUTHOR_WARNING "Unknown compiler")
endif()
# Loop through flags and use the ones which the compiler supports
foreach (flag ${WARNING_FLAGS_TO_CHECK})
z3_add_cxx_flag("${flag}")
endforeach()
# TODO: Remove this eventually.
# Detect legacy `WARNINGS_AS_ERRORS` boolean option and covert to new
# to new option type.
get_property(
WARNINGS_AS_ERRORS_CACHE_VAR_TYPE
CACHE
WARNINGS_AS_ERRORS
PROPERTY
TYPE
)
if (WARNINGS_AS_ERRORS_CACHE_VAR_TYPE STREQUAL "BOOL")
message(WARNING "Detected legacy WARNINGS_AS_ERRORS option. Upgrading")
set(WARNINGS_AS_ERRORS_DEFAULT "${WARNINGS_AS_ERRORS}")
# Delete old entry
unset(WARNINGS_AS_ERRORS CACHE)
else()
set(WARNINGS_AS_ERRORS_DEFAULT "SERIOUS_ONLY")
endif()
set(WARNINGS_AS_ERRORS
${WARNINGS_AS_ERRORS_DEFAULT}
CACHE STRING
"Treat warnings as errors. ON, OFF, or SERIOUS_ONLY"
)
# Set GUI options
set_property(
CACHE
WARNINGS_AS_ERRORS
PROPERTY STRINGS
"ON;OFF;SERIOUS_ONLY"
)
if (WARNINGS_AS_ERRORS STREQUAL "ON")
message(STATUS "Treating compiler warnings as errors")
if ((CMAKE_CXX_COMPILER_ID MATCHES "Clang") OR (CMAKE_CXX_COMPILER_ID MATCHES "GNU"))
target_compile_options(z3_internal_options INTERFACE "-Werror")
elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
target_compile_options(z3_internal_options INTERFACE "/WX")
else()
message(AUTHOR_WARNING "Unknown compiler")
endif()
elseif (WARNINGS_AS_ERRORS STREQUAL "SERIOUS_ONLY")
message(STATUS "Treating only serious compiler warnings as errors")
# Loop through the flags
foreach (flag ${WARNING_AS_ERROR_FLAGS_TO_CHECK})
# Add globally because some flags need to be passed at link time.
z3_add_cxx_flag("${flag}" GLOBAL)
endforeach()
elseif (WARNINGS_AS_ERRORS STREQUAL "OFF")
message(STATUS "Not treating compiler warnings as errors")
if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
# Warnings as errors is off by default for MSVC so setting this
# is not necessary but this duplicates the behaviour of the old
# build system.
target_compile_options(z3_internal_options INTERFACE "/WX-")
endif()
else()
message(FATAL_ERROR
"WARNINGS_AS_ERRORS set to unsupported value \"${WARNINGS_AS_ERRORS}\""
)
endif()
View git blame Copy permalink