mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

[CMake] Fix dependencies for generating install_tactic.cpp.

Browse source 
Previously CMake was not aware of which headers files the generation
of `install_tactic.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declared tactics/probes changed.
* New tactics/probes were added to new header files.

Now the `z3_add_component()` CMake function has been modifed to take an
optional `TACTIC_HEADERS` argument which allows the headers that declare
tactics/probes to be explicitly listed. The necessary component
declarations have been modified to declare their tactic/probe header
files.

With this information CMake will now regenerate `install_tactic.cpp`
correctly.

This required the `mk_install_tactic_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
This commit is contained in:
Dan Liew 2017-06-21 18:36:20 +01:00
parent a3ee785923
commit 229fd3dc3e
22 changed files with 171 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

41
cmake/z3_add_component.cmake
View file

@ -55,6 +55,7 @@ endfunction()
# SOURCES source1 [source2...]
# [COMPONENT_DEPENDENCIES component1 [component2...]]
# [PYG_FILES pygfile1 [pygfile2...]]
# [TACTIC_HEADERS header_file1 [header_file2...]]
# )
#
# Declares a Z3 component (as a CMake "object library") with target name
@ -81,8 +82,11 @@ endfunction()
# more ``<NAME>.pyg`` files that should used to be generate
# ``<NAME>_params.hpp`` header files used by the ``component_name``.
#
# The optional ``TACTIC_HEADERS`` keyword should be followed by a list of one or
# more header files that declare a tactic and/or a probe that is part of this
# component (see ``ADD_TACTIC()`` and ``ADD_PROBE()``).
macro(z3_add_component component_name)
CMAKE_PARSE_ARGUMENTS("Z3_MOD" "NOT_LIBZ3_COMPONENT" "" "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES" ${ARGN})
CMAKE_PARSE_ARGUMENTS("Z3_MOD" "NOT_LIBZ3_COMPONENT" "" "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES;TACTIC_HEADERS" ${ARGN})
message(STATUS "Adding component ${component_name}")
# Note: We don't check the sources exist here because
# they might be generated files that don't exist yet.
@ -117,6 +121,21 @@ macro(z3_add_component component_name)
unset(_full_output_file_path)
unset(_output_file)
# Add tactic/probe headers to global property
set_property(GLOBAL PROPERTY Z3_${component_name}_TACTIC_HEADERS "")
foreach (tactic_header ${Z3_MOD_TACTIC_HEADERS})
set(_full_tactic_header_file_path "${CMAKE_CURRENT_SOURCE_DIR}/${tactic_header}")
if (NOT (EXISTS "${_full_tactic_header_file_path}"))
message(FATAL_ERROR "\"${_full_tactic_header_file_path}\" does not exist")
endif()
set_property(GLOBAL
APPEND
PROPERTY Z3_${component_name}_TACTIC_HEADERS
"${_full_tactic_header_file_path}"
)
endforeach()
unset(_full_tactic_header_file_path)
# Using "object" libraries here means we have a convenient
# name to refer to a component in CMake but we don't actually
# create a static/library from them. This allows us to easily
@ -191,25 +210,33 @@ macro(z3_add_install_tactic_rule)
)
endif()
z3_expand_dependencies(_expanded_components ${ARGN})
# Get paths to search
set(_search_paths "")
# Get header files that declare tactics/probes
set(_tactic_header_files "")
foreach (dependency ${_expanded_components})
get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
list(APPEND _search_paths ${_dep_include_dirs})
get_property(_component_tactic_header_files
GLOBAL
PROPERTY Z3_${dependency}_TACTIC_HEADERS
)
list(APPEND _tactic_header_files ${_component_tactic_header_files})
endforeach()
unset(_component_tactic_header_files)
list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
add_custom_command(OUTPUT "install_tactic.cpp"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
"${CMAKE_CURRENT_BINARY_DIR}"
${_search_paths}
${_tactic_header_files}
DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
${_expanded_components}
${_tactic_header_files}
COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\""
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
VERBATIM
)
unset(_expanded_components)
unset(_tactic_header_files)
endmacro()
macro(z3_add_memory_initializer_rule)