[CMake] Fix dependencies for generating mem_initializer.cpp.

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

* Existing headers that declare memory initializers/finalizers change.
* New headers are added that declare memory initializers/finalizer.

Now the `z3_add_component()` CMake function has been modifed so that
it now takes an optional `MEMORY_INIT_FINALIZER_HEADERS` argument
which allows the headers that declare memory initializers/finalizers
to be explicitly listed.

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

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

cmake/z3_add_component.cmake

@@ -57,6 +57,7 @@ endfunction()
 #   [PYG_FILES pygfile1 [pygfile2...]]
 #   [TACTIC_HEADERS header_file1 [header_file2...]]
 #   [EXTRA_REGISTER_MODULE_HEADERS header_file1 [header_file2...]]
+#   [MEMORY_INIT_FINALIZER_HEADERS header_file1 [header_file2...]]
 # )
 #
 # Declares a Z3 component (as a CMake "object library") with target name
@@ -93,11 +94,15 @@ endfunction()
 # 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.
+#
+# The optional ``MEMORY_INIT_FINALIZER_HEADERS`` keyword should be followed by a list
+# of one or more header files that contain memory initializer/finalizer declarations
+# (i.e. ``ADD_INITIALIZER()`` or ``ADD_FINALIZER()``).
 macro(z3_add_component component_name)
   CMAKE_PARSE_ARGUMENTS("Z3_MOD"
     "NOT_LIBZ3_COMPONENT"
     ""
-    "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES;TACTIC_HEADERS;EXTRA_REGISTER_MODULE_HEADERS" ${ARGN})
+    "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES;TACTIC_HEADERS;EXTRA_REGISTER_MODULE_HEADERS;MEMORY_INIT_FINALIZER_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.
@@ -176,6 +181,22 @@ macro(z3_add_component component_name)
   endforeach()
   unset(_full_extra_register_module_header)
 
+  # Add memory initializer/finalizer headers to global property
+  set_property(GLOBAL PROPERTY Z3_${component_name}_MEM_INIT_FINALIZER_HEADERS "")
+  foreach (memory_init_finalizer_header ${Z3_MOD_MEMORY_INIT_FINALIZER_HEADERS})
+    set(_full_memory_init_finalizer_header_path
+      "${CMAKE_CURRENT_SOURCE_DIR}/${memory_init_finalizer_header}")
+    if (NOT (EXISTS "${_full_memory_init_finalizer_header_path}"))
+      message(FATAL_ERROR "\"${_full_memory_init_finalizer_header_path}\" does not exist")
+    endif()
+    set_property(GLOBAL
+      APPEND
+      PROPERTY Z3_${component_name}_MEM_INIT_FINALIZER_HEADERS
+      "${_full_memory_init_finalizer_header_path}"
+    )
+  endforeach()
+  unset(_full_memory_init_finalizer_header_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
@@ -297,18 +318,31 @@ macro(z3_add_memory_initializer_rule)
     list(APPEND _search_paths ${_dep_include_dirs})
   endforeach()
   list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
+
+  # Get header files that declare initializers and finalizers
+  set(_mem_init_finalize_headers "")
+  foreach (dependency ${_expanded_components})
+    get_property(_dep_mem_init_finalize_headers
+      GLOBAL
+      PROPERTY Z3_${dependency}_MEM_INIT_FINALIZER_HEADERS
+    )
+    list(APPEND _mem_init_finalize_headers ${_dep_mem_init_finalize_headers})
+  endforeach()
+
   add_custom_command(OUTPUT "mem_initializer.cpp"
     COMMAND "${PYTHON_EXECUTABLE}"
     "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py"
     "${CMAKE_CURRENT_BINARY_DIR}"
-    ${_search_paths}
+    ${_mem_init_finalize_headers}
     DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py"
             ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
-            ${_expanded_components}
+            ${_mem_init_finalize_headers}
     COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp\""
     ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
     VERBATIM
   )
+  unset(_mem_init_finalize_headers)
+  unset(_expanded_components)
 endmacro()
 
 macro(z3_add_gparams_register_modules_rule)

scripts/mk_genfile_common.py

@@ -731,7 +731,7 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path):
 # Functions for generating ``mem_initializer.cpp``
 ###############################################################################
 
-def mk_mem_initializer_cpp_internal(component_src_dirs, path):
+def mk_mem_initializer_cpp_internal(h_files_full_path, path):
     """
         Generate a ``mem_initializer.cpp`` file in the directory ``path``.
         Returns the path to the generated file.
@@ -745,7 +745,7 @@ def mk_mem_initializer_cpp_internal(component_src_dirs, path):
 
        These procedures are invoked by the Z3 memory_manager
     """
-    assert isinstance(component_src_dirs, list)
+    assert isinstance(h_files_full_path, list)
     assert check_dir_exists(path)
     initializer_cmds = []
     finalizer_cmds   = []
@@ -756,11 +756,6 @@ def mk_mem_initializer_cpp_internal(component_src_dirs, path):
     # ADD_INITIALIZER with priority
     initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)')
     finalizer_pat        = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
-    h_files_full_path = []
-    for component_src_dir in sorted(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_mem_initializer_cpp.py

@@ -1,6 +1,6 @@
 #!/usr/bin/env python
 """
-Scans the source directories for
+Scans the listed header files for
 memory initializers and finalizers and
 emits and implementation of
 ``void mem_initialize()`` and
@@ -17,19 +17,19 @@ 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:
+    h_files_full_path = []
-        if not mk_genfile_common.check_dir_exists(source_dir):
+    for header_file in pargs.header_files:
-            return 1
+        h_files_full_path.append(os.path.abspath(header_file))
 
     output = mk_genfile_common.mk_mem_initializer_cpp_internal(
-        pargs.source_dirs,
+        h_files_full_path,
         pargs.destination_dir
     )
     logging.info('Generated "{}"'.format(output))

scripts/mk_util.py

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

src/util/CMakeLists.txt

@@ -61,4 +61,11 @@ z3_add_component(util
     z3_exception.cpp
   EXTRA_REGISTER_MODULE_HEADERS
     env_params.h
+  MEMORY_INIT_FINALIZER_HEADERS
+    debug.h
+    gparams.h
+    prime_generator.h
+    rational.h
+    symbol.h
+    trace.h
 )