[CMake] Fix dependencies for generating gparams_register_modules.cpp.

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

* Existing headers that declared module description/parameters change.
* New headers are added that declare module description/parameters.
* `.pyg` files that generate header files that declare module
  description/parameters change

Now the `z3_add_component()` CMake function has been modifed so that

* All header files that are generated from `.pyg` files are added as
dependencies and are scanned from module description/parameter
declarations. This implicit dependency of `gparams_register_modules.cpp`
depending on other generated header files seems unnecessary complex. We
should revisit this design decision once the Python/Makefile build
system is deprecated.

* The function now takes an optional `EXTRA_REGISTER_MODULE_HEADERS`
argument which allows the headers that declare module
description/paramters to be explicitly listed.

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

This required the `mk_gparams_register_modules_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.

cmake/z3_add_component.cmake

@@ -56,6 +56,7 @@ endfunction()
 #   [COMPONENT_DEPENDENCIES component1 [component2...]]
 #   [PYG_FILES pygfile1 [pygfile2...]]
 #   [TACTIC_HEADERS header_file1 [header_file2...]]
+#   [EXTRA_REGISTER_MODULE_HEADERS header_file1 [header_file2...]]
 # )
 #
 # Declares a Z3 component (as a CMake "object library") with target name
@@ -81,17 +82,28 @@ endfunction()
 # The optional ``PYG_FILES`` keyword should be followed by a list of one or
 # more ``<NAME>.pyg`` files that should used to be generate
 # ``<NAME>_params.hpp`` header files used by the ``component_name``.
+# This generated file will automatically be scanned for the register module
+# declarations (i.e. ``REG_PARAMS()``, ``REG_MODULE_PARAMS()``, and
+# ``REG_MODULE_DESCRIPTION()``).
 #
 # 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()``).
+#
+# The optional ``EXTRA_REGISTER_MODULE_HEADERS`` keyword should be followed by a list
+# of one or more header files that contain module registration declarations.
+# NOTE: The header files generated from ``.pyg`` files don't need to be included.
 macro(z3_add_component component_name)
-  CMAKE_PARSE_ARGUMENTS("Z3_MOD" "NOT_LIBZ3_COMPONENT" "" "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES;TACTIC_HEADERS" ${ARGN})
+  CMAKE_PARSE_ARGUMENTS("Z3_MOD"
+    "NOT_LIBZ3_COMPONENT"
+    ""
+    "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES;TACTIC_HEADERS;EXTRA_REGISTER_MODULE_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.
 
   set(_list_generated_headers "")
+  set_property(GLOBAL PROPERTY Z3_${component_name}_REGISTER_MODULE_HEADERS "")
   foreach (pyg_file ${Z3_MOD_PYG_FILES})
     set(_full_pyg_file_path "${CMAKE_CURRENT_SOURCE_DIR}/${pyg_file}")
     if (NOT (EXISTS "${_full_pyg_file_path}"))
@@ -116,6 +128,18 @@ macro(z3_add_component component_name)
       VERBATIM
     )
     list(APPEND _list_generated_headers "${_full_output_file_path}")
+
+    # FIXME: This implicit dependency of a generated file depending on
+    # generated files was inherited from the old build system.
+
+    # Typically generated headers contain `REG_PARAMS()`, `REG_MODULE_PARAMS()`
+    # and `REG_MODULE_DESCRIPTION()` declarations so add to the list of
+    # header files to scan.
+    set_property(GLOBAL
+      APPEND
+      PROPERTY Z3_${component_name}_REGISTER_MODULE_HEADERS
+      "${_full_output_file_path}"
+    )
   endforeach()
   unset(_full_include_dir_path)
   unset(_full_output_file_path)
@@ -136,6 +160,22 @@ macro(z3_add_component component_name)
   endforeach()
   unset(_full_tactic_header_file_path)
 
+  # Add additional register module headers
+  foreach (extra_register_module_header ${Z3_MOD_EXTRA_REGISTER_MODULE_HEADERS})
+    set(_full_extra_register_module_header_path
+      "${CMAKE_CURRENT_SOURCE_DIR}/${extra_register_module_header}"
+    )
+    if (NOT (EXISTS "${_full_extra_register_module_header_path}"))
+      message(FATAL_ERROR "\"${_full_extra_register_module_header_path}\" does not exist")
+    endif()
+    set_property(GLOBAL
+      APPEND
+      PROPERTY Z3_${component_name}_REGISTER_MODULE_HEADERS
+      "${_full_extra_register_module_header_path}"
+    )
+  endforeach()
+  unset(_full_extra_register_module_header)
+
   # 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
@@ -282,23 +322,27 @@ macro(z3_add_gparams_register_modules_rule)
     )
   endif()
   z3_expand_dependencies(_expanded_components ${ARGN})
-  # Get paths to search
+
-  set(_search_paths "")
+  # Get the list of header files to parse
+  set(_register_module_header_files "")
   foreach (dependency ${_expanded_components})
-    get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
+    get_property(_component_register_module_header_files GLOBAL PROPERTY Z3_${dependency}_REGISTER_MODULE_HEADERS)
-    list(APPEND _search_paths ${_dep_include_dirs})
+    list(APPEND _register_module_header_files ${_component_register_module_header_files})
   endforeach()
-  list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
+  unset(_component_register_module_header_files)
+
   add_custom_command(OUTPUT "gparams_register_modules.cpp"
     COMMAND "${PYTHON_EXECUTABLE}"
     "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py"
     "${CMAKE_CURRENT_BINARY_DIR}"
-    ${_search_paths}
+    ${_register_module_header_files}
     DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py"
             ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
-            ${_expanded_components}
+            ${_register_module_header_files}
     COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp\""
     ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
     VERBATIM
   )
+  unset(_expanded_components)
+  unset(_register_module_header_files)
 endmacro()

scripts/mk_genfile_common.py

@@ -587,7 +587,7 @@ def mk_def_file_internal(defname, dll_name, export_header_files):
 ###############################################################################
 # Functions for generating ``gparams_register_modules.cpp``
 ###############################################################################
-def mk_gparams_register_modules_internal(component_src_dirs, path):
+def mk_gparams_register_modules_internal(h_files_full_path, path):
     """
         Generate a ``gparams_register_modules.cpp`` file in the directory ``path``.
         Returns the path to the generated file.
@@ -600,7 +600,7 @@ def mk_gparams_register_modules_internal(component_src_dirs, path):
 
         This procedure is invoked by gparams::init()
     """
-    assert isinstance(component_src_dirs, list)
+    assert isinstance(h_files_full_path, list)
     assert check_dir_exists(path)
     cmds = []    
     mod_cmds = []
@@ -612,11 +612,6 @@ def mk_gparams_register_modules_internal(component_src_dirs, path):
     reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)')
     reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)')
     reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)')
-    h_files_full_path = []
-    for component_src_dir in component_src_dirs:
-        h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
-        h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files))
-        h_files_full_path.extend(h_files)
     for h_file in sorted_headers_by_component(h_files_full_path):
         added_include = False
         with open(h_file, 'r') as fin:

scripts/mk_gparams_register_modules_cpp.py

@@ -1,10 +1,8 @@
 #!/usr/bin/env python
 """
-Determines the available global parameters
+Determines the available global parameters from a list of header files and
-in header files in the list of source directions
+generates a ``gparams_register_modules.cpp`` file in the destination directory
-and generates a ``gparams_register_modules.cpp`` file in
+that defines a function ``void gparams_register_modules()``.
-the destination directory that defines a function
-``void gparams_register_modules()``.
 """
 import mk_genfile_common
 import argparse
@@ -16,19 +14,22 @@ def main(args):
     logging.basicConfig(level=logging.INFO)
     parser = argparse.ArgumentParser(description=__doc__)
     parser.add_argument("destination_dir", help="destination directory")
-    parser.add_argument("source_dirs", nargs="+",
+    parser.add_argument("header_files", nargs="+",
-                        help="One or more source directories to search")
+                        help="One or more header files to parse")
     pargs = parser.parse_args(args)
 
     if not mk_genfile_common.check_dir_exists(pargs.destination_dir):
         return 1
 
-    for source_dir in pargs.source_dirs:
+    if not mk_genfile_common.check_files_exist(pargs.header_files):
-        if not mk_genfile_common.check_dir_exists(source_dir):
+        return 1
-            return 1
+
+    h_files_full_path = []
+    for header_file in pargs.header_files:
+        h_files_full_path.append(os.path.abspath(header_file))
 
     output = mk_genfile_common.mk_gparams_register_modules_internal(
-        pargs.source_dirs,
+        h_files_full_path,
         pargs.destination_dir
     )
     logging.info('Generated "{}"'.format(output))

scripts/mk_util.py

@@ -2763,7 +2763,8 @@ def mk_gparams_register_modules(cnames, path):
     for cname in cnames:
         c = get_component(cname)
         component_src_dirs.append(c.src_dir)
-    generated_file = mk_genfile_common.mk_gparams_register_modules_internal(component_src_dirs, path)
+    h_files_full_path = get_header_files_for_components(component_src_dirs)
+    generated_file = mk_genfile_common.mk_gparams_register_modules_internal(h_files_full_path, path)
     if VERBOSE:
         print("Generated '{}'".format(generated_file))
 

src/ast/normal_forms/CMakeLists.txt

@@ -8,4 +8,6 @@ z3_add_component(normal_forms
     rewriter
   PYG_FILES
     nnf_params.pyg
+  EXTRA_REGISTER_MODULE_HEADERS
+    nnf.h
 )

src/cmd_context/CMakeLists.txt

@@ -18,4 +18,6 @@ z3_add_component(cmd_context
     interp
     rewriter
     solver
+  EXTRA_REGISTER_MODULE_HEADERS
+    context_params.h
 )

src/math/polynomial/CMakeLists.txt

@@ -11,5 +11,7 @@ z3_add_component(polynomial
     util
   PYG_FILES
     algebraic_params.pyg
+  EXTRA_REGISTER_MODULE_HEADERS
+    polynomial.h
 )
 

src/util/CMakeLists.txt

@@ -59,4 +59,6 @@ z3_add_component(util
     util.cpp
     warning.cpp
     z3_exception.cpp
+  EXTRA_REGISTER_MODULE_HEADERS
+    env_params.h
 )