From a2e3788a2095706e663312b418e3c3dad3e30c50 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 18:23:51 +0000 Subject: [PATCH 01/10] [CMake] Refactor the dependency on ``scripts/mk_util.py`` into a list ``Z3_GENERATED_FILE_EXTRA_DEPENDENCIES`` that is used by the ``add_custom_command()`` declarations. This will let us easily change the common dependencies for generating build files in the future. --- CMakeLists.txt | 12 ++++++++++++ contrib/cmake/cmake/z3_add_component.cmake | 9 +++++---- contrib/cmake/src/CMakeLists.txt | 2 +- contrib/cmake/src/api/CMakeLists.txt | 2 +- contrib/cmake/src/api/python/CMakeLists.txt | 4 ++-- contrib/cmake/src/ast/pattern/CMakeLists.txt | 2 +- 6 files changed, 22 insertions(+), 9 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 0e95cb65a..8ed9f5201 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -333,6 +333,18 @@ set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") +################################################################################ +# Extra dependencies for build rules that use the Python infrastructure to +# generate files used for Z3's build. Changes to these files will trigger +# a rebuild of all the generated files. +################################################################################ +# Note: ``update_api.py`` is deliberately not here because it not used +# to generate every generated file. The targets that need it list it explicitly. +# FIXME: We should drop the dependency on ``mk_util.py`` +set(Z3_GENERATED_FILE_EXTRA_DEPENDENCIES + "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" +) + ################################################################################ # Z3 components, library and executables ################################################################################ diff --git a/contrib/cmake/cmake/z3_add_component.cmake b/contrib/cmake/cmake/z3_add_component.cmake index eebc0c8d9..b90aa2fe7 100644 --- a/contrib/cmake/cmake/z3_add_component.cmake +++ b/contrib/cmake/cmake/z3_add_component.cmake @@ -104,7 +104,8 @@ macro(z3_add_component component_name) add_custom_command(OUTPUT "${_output_file}" COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/scripts/pyg2hpp.py" "${_full_pyg_file_path}" "${CMAKE_CURRENT_BINARY_DIR}" MAIN_DEPENDENCY "${_full_pyg_file_path}" - DEPENDS "${CMAKE_SOURCE_DIR}/scripts/pyg2hpp.py" "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + DEPENDS "${CMAKE_SOURCE_DIR}/scripts/pyg2hpp.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating \"${_full_output_file_path}\" from \"${pyg_file}\"" WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} @@ -203,7 +204,7 @@ macro(z3_add_install_tactic_rule) "${CMAKE_CURRENT_BINARY_DIR}" ${_search_paths} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${_expanded_components} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\"" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} @@ -235,7 +236,7 @@ macro(z3_add_memory_initializer_rule) "${CMAKE_CURRENT_BINARY_DIR}" ${_search_paths} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${_expanded_components} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp\"" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} @@ -267,7 +268,7 @@ macro(z3_add_gparams_register_modules_rule) "${CMAKE_CURRENT_BINARY_DIR}" ${_search_paths} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${_expanded_components} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp\"" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index 6708f505e..36b524f0a 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -186,7 +186,7 @@ if (MSVC) ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_def_file.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} COMMENT "Generating \"${dll_module_exports_file}\"" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} diff --git a/contrib/cmake/src/api/CMakeLists.txt b/contrib/cmake/src/api/CMakeLists.txt index 0fd012b87..78837c001 100644 --- a/contrib/cmake/src/api/CMakeLists.txt +++ b/contrib/cmake/src/api/CMakeLists.txt @@ -24,7 +24,7 @@ add_custom_command(OUTPUT ${generated_files} "--api_output_dir" "${CMAKE_CURRENT_BINARY_DIR}" DEPENDS "${CMAKE_SOURCE_DIR}/scripts/update_api.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} COMMENT "Generating ${generated_files}" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} diff --git a/contrib/cmake/src/api/python/CMakeLists.txt b/contrib/cmake/src/api/python/CMakeLists.txt index 2279be716..05d04e552 100644 --- a/contrib/cmake/src/api/python/CMakeLists.txt +++ b/contrib/cmake/src/api/python/CMakeLists.txt @@ -38,7 +38,7 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3core.py" DEPENDS ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "${CMAKE_SOURCE_DIR}/scripts/update_api.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating z3core.py" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} ) @@ -54,7 +54,7 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3consts.py" DEPENDS ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating z3consts.py" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} ) diff --git a/contrib/cmake/src/ast/pattern/CMakeLists.txt b/contrib/cmake/src/ast/pattern/CMakeLists.txt index 8cff3e739..59e0545a1 100644 --- a/contrib/cmake/src/ast/pattern/CMakeLists.txt +++ b/contrib/cmake/src/ast/pattern/CMakeLists.txt @@ -13,7 +13,7 @@ add_custom_command(OUTPUT "database.h" "${CMAKE_CURRENT_BINARY_DIR}/database.h" MAIN_DEPENDENCY "${CMAKE_CURRENT_SOURCE_DIR}/database.smt2" DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_pat_db.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating \"database.h\"" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM From 2b64729b2174bbae9d87d28a5e26afebafc6fce0 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 16:54:22 +0000 Subject: [PATCH 02/10] Move ``mk_z3consts_py_internal()`` out of ``mk_util.py`` into ``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_consts_files.py`` to use the code at its new location. The interface has been changed slightly so that ``mk_z3consts_py_internal()`` now returns the path to the generated file. The motivation behind this is so that clients of the function know the path to the generated file. Whilst I'm here also reindent ``mk_consts_files.py`` and move some of its code into ``mk_genfile_common.py`` so it can be shared. Also update Z3_GENERATED_FILE_EXTRA_DEPENDENCIES in the CMake build so it knows about ``mk_genfile_common.py``. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. --- CMakeLists.txt | 1 + scripts/mk_consts_files.py | 50 ++++++-------- scripts/mk_genfile_common.py | 126 +++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 79 +--------------------- 4 files changed, 152 insertions(+), 104 deletions(-) create mode 100644 scripts/mk_genfile_common.py diff --git a/CMakeLists.txt b/CMakeLists.txt index 8ed9f5201..5cdf06120 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -343,6 +343,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") # FIXME: We should drop the dependency on ``mk_util.py`` set(Z3_GENERATED_FILE_EXTRA_DEPENDENCIES "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + "${CMAKE_SOURCE_DIR}/scripts/mk_genfile_common.py" ) ################################################################################ diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py index 543c56e0e..2c017bd2c 100755 --- a/scripts/mk_consts_files.py +++ b/scripts/mk_consts_files.py @@ -4,44 +4,38 @@ Reads a list of Z3 API header files and generate the constant declarations need by one or more Z3 language bindings """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys -def check_dir(output_dir): - if not os.path.isdir(output_dir): - logging.error('"{}" is not an existing directory'.format(output_dir)) - return 1 - return 0 def main(args): - logging.basicConfig(level=logging.INFO) - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("api_files", nargs="+") - parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None) - pargs = parser.parse_args(args) + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("api_files", nargs="+") + parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None) + pargs = parser.parse_args(args) - for api_file in pargs.api_files: - if not os.path.exists(api_file): - logging.error('"{}" does not exist'.format(api_file)) - return 1 + if not mk_genfile_common.check_files_exist(pargs.api_files): + logging.error('One or more API files do not exist') + return 1 - count = 0 + count = 0 - if pargs.z3py_output_dir: - if check_dir(pargs.z3py_output_dir) != 0: - return 1 - mk_util.mk_z3consts_py_internal(pargs.api_files, pargs.z3py_output_dir) - count += 1 + if pargs.z3py_output_dir: + if not mk_genfile_common.check_dir_exists(pargs.z3py_output_dir): + return 1 + output = mk_genfile_common.mk_z3consts_py_internal(pargs.api_files, pargs.z3py_output_dir) + logging.info('Generated "{}"'.format(output)) + count += 1 - if count == 0: - logging.info('No files generated. You need to specific an output directory' - ' for the relevant langauge bindings') - # TODO: Add support for other bindings - return 0 + if count == 0: + logging.info('No files generated. You need to specific an output directory' + ' for the relevant langauge bindings') + # TODO: Add support for other bindings + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) - + sys.exit(main(sys.argv[1:])) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py new file mode 100644 index 000000000..abe10a0d1 --- /dev/null +++ b/scripts/mk_genfile_common.py @@ -0,0 +1,126 @@ +# This file contains code that is common to +# both the Python build system and the CMake +# build system. +# +# The code here generally is involved in +# generating files needed by Z3 at build time. +# +# You should **not** import ``mk_util`` here +# to avoid having this code depend on the +# of the Python build system. +import os +import logging +import re +import sys + +# Logger for this module +_logger = logging.getLogger(__name__) + + +############################################################################### +# Utility functions +############################################################################### +def check_dir_exists(output_dir): + """ + Returns ``True`` if ``output_dir`` exists, otherwise + returns ``False``. + """ + if not os.path.isdir(output_dir): + _logger.error('"{}" is not an existing directory'.format(output_dir)) + return False + return True + +def check_files_exist(files): + assert isinstance(files, list) + for f in files: + if not os.path.exists(f): + _logger.error('"{}" does not exist'.format(f)) + return False + return True + +############################################################################### +# Functions for generating constant declarations for language bindings +############################################################################### + +def mk_z3consts_py_internal(api_files, output_dir): + """ + Generate ``z3consts.py`` from the list of API header files + in ``api_files`` and write the output file into + the ``output_dir`` directory + + Returns the path to the generated file. + """ + assert os.path.isdir(output_dir) + assert isinstance(api_files, list) + + blank_pat = re.compile("^ *\r?$") + comment_pat = re.compile("^ *//.*$") + typedef_pat = re.compile("typedef enum *") + typedef2_pat = re.compile("typedef enum { *") + openbrace_pat = re.compile("{ *") + closebrace_pat = re.compile("}.*;") + + z3consts = open(os.path.join(output_dir, 'z3consts.py'), 'w') + z3consts_output_path = z3consts.name + z3consts.write('# Automatically generated file\n\n') + for api_file in api_files: + api = open(api_file, 'r') + + SEARCHING = 0 + FOUND_ENUM = 1 + IN_ENUM = 2 + + mode = SEARCHING + decls = {} + idx = 0 + + linenum = 1 + for line in api: + m1 = blank_pat.match(line) + m2 = comment_pat.match(line) + if m1 or m2: + # skip blank lines and comments + linenum = linenum + 1 + elif mode == SEARCHING: + m = typedef_pat.match(line) + if m: + mode = FOUND_ENUM + m = typedef2_pat.match(line) + if m: + mode = IN_ENUM + decls = {} + idx = 0 + elif mode == FOUND_ENUM: + m = openbrace_pat.match(line) + if m: + mode = IN_ENUM + decls = {} + idx = 0 + else: + assert False, "Invalid %s, line: %s" % (api_file, linenum) + else: + assert mode == IN_ENUM + words = re.split('[^\-a-zA-Z0-9_]+', line) + m = closebrace_pat.match(line) + if m: + name = words[1] + z3consts.write('# enum %s\n' % name) + for k in decls: + i = decls[k] + z3consts.write('%s = %s\n' % (k, i)) + z3consts.write('\n') + mode = SEARCHING + elif len(words) <= 2: + assert False, "Invalid %s, line: %s" % (api_file, linenum) + else: + if words[2] != '': + if len(words[2]) > 1 and words[2][1] == 'x': + idx = int(words[2], 16) + else: + idx = int(words[2]) + decls[words[1]] = idx + idx = idx + 1 + linenum = linenum + 1 + api.close() + z3consts.close() + return z3consts_output_path diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 188dad7a4..da3c6eef9 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -12,6 +12,7 @@ import re import getopt import shutil from mk_exception import * +import mk_genfile_common from fnmatch import fnmatch import distutils.sysconfig import compileall @@ -3026,83 +3027,9 @@ def mk_z3consts_py(api_files): api_file_c = api_dll.find_file(api_file, api_dll.name) api_file = os.path.join(api_file_c.src_dir, api_file) full_path_api_files.append(api_file) - mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR) - -def mk_z3consts_py_internal(api_files, output_dir): - assert os.path.isdir(output_dir) - assert isinstance(api_files, list) - - blank_pat = re.compile("^ *\r?$") - comment_pat = re.compile("^ *//.*$") - typedef_pat = re.compile("typedef enum *") - typedef2_pat = re.compile("typedef enum { *") - openbrace_pat = re.compile("{ *") - closebrace_pat = re.compile("}.*;") - - z3consts = open(os.path.join(output_dir, 'z3consts.py'), 'w') - z3consts.write('# Automatically generated file\n\n') - for api_file in api_files: - api = open(api_file, 'r') - - SEARCHING = 0 - FOUND_ENUM = 1 - IN_ENUM = 2 - - mode = SEARCHING - decls = {} - idx = 0 - - linenum = 1 - for line in api: - m1 = blank_pat.match(line) - m2 = comment_pat.match(line) - if m1 or m2: - # skip blank lines and comments - linenum = linenum + 1 - elif mode == SEARCHING: - m = typedef_pat.match(line) - if m: - mode = FOUND_ENUM - m = typedef2_pat.match(line) - if m: - mode = IN_ENUM - decls = {} - idx = 0 - elif mode == FOUND_ENUM: - m = openbrace_pat.match(line) - if m: - mode = IN_ENUM - decls = {} - idx = 0 - else: - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - assert mode == IN_ENUM - words = re.split('[^\-a-zA-Z0-9_]+', line) - m = closebrace_pat.match(line) - if m: - name = words[1] - z3consts.write('# enum %s\n' % name) - for k in decls: - i = decls[k] - z3consts.write('%s = %s\n' % (k, i)) - z3consts.write('\n') - mode = SEARCHING - elif len(words) <= 2: - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - if words[2] != '': - if len(words[2]) > 1 and words[2][1] == 'x': - idx = int(words[2], 16) - else: - idx = int(words[2]) - decls[words[1]] = idx - idx = idx + 1 - linenum = linenum + 1 - api.close() - z3consts.close() + generated_file = mk_genfile_common.mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR) if VERBOSE: - print("Generated '%s'" % os.path.join(output_dir, 'z3consts.py')) + print("Generated '{}".format(generated_file)) # Extract enumeration types from z3_api.h, and add .Net definitions From 8a35f744c7b285d5087107debc22e4274c8f39d8 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 19:08:47 +0000 Subject: [PATCH 03/10] Move ``mk_def_file_internal()`` out of ``mk_util.py`` into ``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_def_file.py`` to use the code at its new location. Whilst I'm here also reindent ``mk_def_file.py`` and make it use some of the code in ``mk_genfile_common.py`` to avoid code duplication. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. --- scripts/mk_def_file.py | 34 +++++++++++++++++----------------- scripts/mk_genfile_common.py | 33 +++++++++++++++++++++++++++++++++ scripts/mk_util.py | 23 +---------------------- 3 files changed, 51 insertions(+), 39 deletions(-) diff --git a/scripts/mk_def_file.py b/scripts/mk_def_file.py index 2b9b5a071..07418a975 100755 --- a/scripts/mk_def_file.py +++ b/scripts/mk_def_file.py @@ -6,31 +6,31 @@ exported symbols of a dll. This file can be passed to the ``/DEF`` to the linker used by MSVC. """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys def main(args): - logging.basicConfig(level=logging.INFO) - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("output_file", help="output def file path") - parser.add_argument("dllname", help="dllname to use in def file") - parser.add_argument("api_files", nargs="+") - pargs = parser.parse_args(args) + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("output_file", help="output def file path") + parser.add_argument("dllname", help="dllname to use in def file") + parser.add_argument("api_files", nargs="+") + pargs = parser.parse_args(args) - for api_file in pargs.api_files: - if not os.path.exists(api_file): - logging.error('"{}" does not exist'.format(api_file)) - return 1 + if not mk_genfile_common.check_files_exist(pargs.api_files): + logging.error('One or more api files do not exist') + return 1 - mk_util.mk_def_file_internal( - pargs.output_file, - pargs.dllname, - pargs.api_files) - return 0 + mk_genfile_common.mk_def_file_internal( + pargs.output_file, + pargs.dllname, + pargs.api_files) + logging.info('Generated "{}"'.format(pargs.output_file)) + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) + sys.exit(main(sys.argv[1:])) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index abe10a0d1..e0b9bce48 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -124,3 +124,36 @@ def mk_z3consts_py_internal(api_files, output_dir): api.close() z3consts.close() return z3consts_output_path + +############################################################################### +# Functions for generating a "module definition file" for MSVC +############################################################################### + +def mk_def_file_internal(defname, dll_name, export_header_files): + """ + Writes to a module definition file to a file named ``defname``. + + ``dll_name`` is the name of the dll (without the ``.dll`` suffix). + ``export_header_file`` is a list of header files to scan for symbols + to include in the module definition file. + """ + assert isinstance(export_header_files, list) + pat1 = re.compile(".*Z3_API.*") + fout = open(defname, 'w') + fout.write('LIBRARY "%s"\nEXPORTS\n' % dll_name) + num = 1 + for export_header_file in export_header_files: + api = open(export_header_file, 'r') + for line in api: + m = pat1.match(line) + if m: + words = re.split('\W+', line) + i = 0 + for w in words: + if w == 'Z3_API': + f = words[i+1] + fout.write('\t%s @%s\n' % (f, num)) + i = i + 1 + num = num + 1 + api.close() + fout.close() diff --git a/scripts/mk_util.py b/scripts/mk_util.py index da3c6eef9..f9d639daf 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2913,28 +2913,7 @@ def mk_def_file(c): dot_h_c = c.find_file(dot_h, c.name) api = os.path.join(dot_h_c.src_dir, dot_h) export_header_files.append(api) - mk_def_file_internal(defname, dll_name, export_header_files) - -def mk_def_file_internal(defname, dll_name, export_header_files): - pat1 = re.compile(".*Z3_API.*") - fout = open(defname, 'w') - fout.write('LIBRARY "%s"\nEXPORTS\n' % dll_name) - num = 1 - for export_header_file in export_header_files: - api = open(export_header_file, 'r') - for line in api: - m = pat1.match(line) - if m: - words = re.split('\W+', line) - i = 0 - for w in words: - if w == 'Z3_API': - f = words[i+1] - fout.write('\t%s @%s\n' % (f, num)) - i = i + 1 - num = num + 1 - api.close() - fout.close() + mk_genfile_common.mk_def_file_internal(defname, dll_name, export_header_files) if VERBOSE: print("Generated '%s'" % defname) From 404aa2a5a0355db1bbe546be138d3ea0477738cb Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 20:29:20 +0000 Subject: [PATCH 04/10] Move ``mk_gparams_register_modules_internal()`` from ``mk_util.py`` to ``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_gparams_register_modules_cpp.py`` to use the code at its new location. The interface has been changed slightly so that ``mk_gparams_register_modules_internal()`` now returns the path to the generated file. The motivation behind this so that clients of the function know the path to the generated file. Whilst I'm here reindent ``mk_gparams_register_modules_cpp.py`` and the relevant code in ``mk_util.py``. Also remove duplicated code that is now available in ``mk_genfile_common.py``. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. --- scripts/mk_genfile_common.py | 61 ++++++++++++++++++++++ scripts/mk_gparams_register_modules_cpp.py | 46 +++++++--------- scripts/mk_util.py | 59 +++------------------ 3 files changed, 86 insertions(+), 80 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index e0b9bce48..71db2518a 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -157,3 +157,64 @@ def mk_def_file_internal(defname, dll_name, export_header_files): num = num + 1 api.close() fout.close() + +############################################################################### +# Functions for generating ``gparams_register_modules.cpp`` +############################################################################### +def mk_gparams_register_modules_internal(component_src_dirs, path): + """ + Generate a ``gparams_register_modules.cpp`` file in the directory ``path``. + Returns the path to the generated file. + + This file implements the procedure + + ``` + void gparams_register_modules() + ``` + + This procedure is invoked by gparams::init() + """ + assert isinstance(component_src_dirs, list) + assert check_dir_exists(path) + cmds = [] + mod_cmds = [] + mod_descrs = [] + fullname = os.path.join(path, 'gparams_register_modules.cpp') + fout = open(fullname, 'w') + fout.write('// Automatically generated file.\n') + fout.write('#include"gparams.h"\n') + 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\(\'([^\']*)\', *\'([^\']*)\'\)') + 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)) + for h_file in h_files: + added_include = False + fin = open(os.path.join(component_src_dir, h_file), 'r') + for line in fin: + m = reg_pat.match(line) + if m: + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + cmds.append((m.group(1))) + m = reg_mod_pat.match(line) + if m: + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + mod_cmds.append((m.group(1), m.group(2))) + m = reg_mod_descr_pat.match(line) + if m: + mod_descrs.append((m.group(1), m.group(2))) + fin.close() + fout.write('void gparams_register_modules() {\n') + for code in cmds: + fout.write('{ param_descrs d; %s(d); gparams::register_global(d); }\n' % code) + for (mod, code) in mod_cmds: + fout.write('{ param_descrs * d = alloc(param_descrs); %s(*d); gparams::register_module("%s", d); }\n' % (code, mod)) + for (mod, descr) in mod_descrs: + fout.write('gparams::register_module_descr("%s", "%s");\n' % (mod, descr)) + fout.write('}\n') + fout.close() + return fullname diff --git a/scripts/mk_gparams_register_modules_cpp.py b/scripts/mk_gparams_register_modules_cpp.py index 1c7e221ba..cf6e8da96 100755 --- a/scripts/mk_gparams_register_modules_cpp.py +++ b/scripts/mk_gparams_register_modules_cpp.py @@ -6,42 +6,34 @@ and generates a ``gparams_register_modules.cpp`` file in the destination directory that defines a function ``void gparams_register_modules()``. """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys -def check_dir(path): - if not os.path.exists(path): - logging.error('"{}" does not exist'.format(path)) - return 1 - - if not os.path.isdir(path): - logging.error('"{}" is not a directory'.format(path)) - return 1 - - return 0 - - 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="+", - help="One or more source directories to search") - pargs = parser.parse_args(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="+", + help="One or more source directories to search") + pargs = parser.parse_args(args) - if check_dir(pargs.destination_dir) != 0: - return 1 + if not mk_genfile_common.check_dir_exists(pargs.destination_dir): + return 1 - for source_dir in pargs.source_dirs: - if check_dir(source_dir) != 0: - return 1 + for source_dir in pargs.source_dirs: + if not mk_genfile_common.check_dir_exists(source_dir): + return 1 - mk_util.mk_gparams_register_modules_internal(pargs.source_dirs, pargs.destination_dir) - return 0 + output = mk_genfile_common.mk_gparams_register_modules_internal( + pargs.source_dirs, + pargs.destination_dir + ) + logging.info('Generated "{}"'.format(output)) + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) + sys.exit(main(sys.argv[1:])) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index f9d639daf..260625ec4 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2839,61 +2839,14 @@ def mk_all_mem_initializer_cpps(): cnames.append(c.name) mk_mem_initializer_cpp(cnames, c.src_dir) -# Generate an ``gparams_register_modules.cpp`` at path. -# This file implements the procedure -# void gparams_register_modules() -# This procedure is invoked by gparams::init() def mk_gparams_register_modules(cnames, path): - component_src_dirs = [] - for cname in cnames: - c = get_component(cname) - component_src_dirs.append(c.src_dir) - mk_gparams_register_modules_internal(component_src_dirs, path) - -def mk_gparams_register_modules_internal(component_src_dirs, path): - cmds = [] - mod_cmds = [] - mod_descrs = [] - fullname = os.path.join(path, 'gparams_register_modules.cpp') - fout = open(fullname, 'w') - fout.write('// Automatically generated file.\n') - fout.write('#include"gparams.h"\n') - 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\(\'([^\']*)\', *\'([^\']*)\'\)') - 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)) - for h_file in h_files: - added_include = False - fin = open(os.path.join(component_src_dir, h_file), 'r') - for line in fin: - m = reg_pat.match(line) - if m: - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - cmds.append((m.group(1))) - m = reg_mod_pat.match(line) - if m: - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - mod_cmds.append((m.group(1), m.group(2))) - m = reg_mod_descr_pat.match(line) - if m: - mod_descrs.append((m.group(1), m.group(2))) - fin.close() - fout.write('void gparams_register_modules() {\n') - for code in cmds: - fout.write('{ param_descrs d; %s(d); gparams::register_global(d); }\n' % code) - for (mod, code) in mod_cmds: - fout.write('{ param_descrs * d = alloc(param_descrs); %s(*d); gparams::register_module("%s", d); }\n' % (code, mod)) - for (mod, descr) in mod_descrs: - fout.write('gparams::register_module_descr("%s", "%s");\n' % (mod, descr)) - fout.write('}\n') - fout.close() + component_src_dirs = [] + 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) if VERBOSE: - print("Generated '%s'" % fullname) + print("Generated '{}'".format(generated_file)) def mk_all_gparams_register_modules(): if not ONLY_MAKEFILES: From f4e98a4fe521e6b3fa4e5cf79fcf66fed859e4b8 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 21:56:42 +0000 Subject: [PATCH 05/10] Move ``mk_install_tactic_cpp_internal()`` from ``mk_util.py`` to ``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_install_tactic_cpp.py`` to use the code at its new location. The interface has been changed slightly so that ``mk_install_tactic_cpp_internal()`` now returns the path the generated file. The motivation behind this is so that clients of the function know the path of the generated file. Whilst I'm here reindent ``mk_install_tactic_cpp.py`` and the relevant code in ``mk_util.py``. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. --- scripts/mk_genfile_common.py | 90 ++++++++++++++++++++++++++++++++ scripts/mk_install_tactic_cpp.py | 47 +++++++---------- scripts/mk_util.py | 80 +++------------------------- 3 files changed, 115 insertions(+), 102 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 71db2518a..05bf21f36 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -218,3 +218,93 @@ def mk_gparams_register_modules_internal(component_src_dirs, path): fout.write('}\n') fout.close() return fullname + +############################################################################### +# Functions/data structures for generating ``install_tactics.cpp`` +############################################################################### + +# FIXME: Remove use of global data structures +ADD_TACTIC_DATA=[] +ADD_PROBE_DATA=[] + +def ADD_TACTIC(name, descr, cmd): + global ADD_TACTIC_DATA + ADD_TACTIC_DATA.append((name, descr, cmd)) + +def ADD_PROBE(name, descr, cmd): + global ADD_PROBE_DATA + ADD_PROBE_DATA.append((name, descr, cmd)) + + +def mk_install_tactic_cpp_internal(component_src_dirs, path): + """ + Generate a ``install_tactics.cpp`` file in the directory ``path``. + Returns the path the generated file. + + This file implements the procedure + + ``` + void install_tactics(tactic_manager & ctx) + ``` + + It installs all tactics found in the given component directories + ``component_src_dirs`` The procedure looks for ``ADD_TACTIC`` commands + in the ``.h`` and ``.hpp`` files of these components. + """ + global ADD_TACTIC_DATA, ADD_PROBE_DATA + ADD_TACTIC_DATA = [] + ADD_PROBE_DATA = [] + assert isinstance(component_src_dirs, list) + assert check_dir_exists(path) + fullname = os.path.join(path, 'install_tactic.cpp') + fout = open(fullname, 'w') + fout.write('// Automatically generated file.\n') + fout.write('#include"tactic.h"\n') + fout.write('#include"tactic_cmds.h"\n') + fout.write('#include"cmd_context.h"\n') + tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') + probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') + 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)) + for h_file in h_files: + added_include = False + fin = open(os.path.join(component_src_dir, h_file), 'r') + for line in fin: + if tactic_pat.match(line): + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + try: + exec(line.strip('\n '), globals()) + except Exception as e: + _logger.error("Failed processing ADD_TACTIC command at '{}'\n{}".format( + fullname, line)) + raise e + if probe_pat.match(line): + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + try: + exec(line.strip('\n '), globals()) + except Exception as e: + _logger.error("Failed processing ADD_PROBE command at '{}'\n{}".format( + fullname, line)) + raise e + fin.close() + # First pass will just generate the tactic factories + idx = 0 + for data in ADD_TACTIC_DATA: + fout.write('MK_SIMPLE_TACTIC_FACTORY(__Z3_local_factory_%s, %s);\n' % (idx, data[2])) + idx = idx + 1 + fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, FACTORY) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, alloc(FACTORY)))\n') + fout.write('#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE))\n') + fout.write('void install_tactics(tactic_manager & ctx) {\n') + idx = 0 + for data in ADD_TACTIC_DATA: + fout.write(' ADD_TACTIC_CMD("%s", "%s", __Z3_local_factory_%s);\n' % (data[0], data[1], idx)) + idx = idx + 1 + for data in ADD_PROBE_DATA: + fout.write(' ADD_PROBE("%s", "%s", %s);\n' % data) + fout.write('}\n') + fout.close() + return fullname diff --git a/scripts/mk_install_tactic_cpp.py b/scripts/mk_install_tactic_cpp.py index f8323d731..21e66b3ab 100755 --- a/scripts/mk_install_tactic_cpp.py +++ b/scripts/mk_install_tactic_cpp.py @@ -6,42 +6,33 @@ and generates a ``install_tactic.cpp`` file in the destination directory that defines a function ``void install_tactics(tactic_manager& ctx)``. """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys -def check_dir(path): - if not os.path.exists(path): - logging.error('"{}" does not exist'.format(path)) - return 1 - - if not os.path.isdir(path): - logging.error('"{}" is not a directory'.format(path)) - return 1 - - return 0 - - 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="+", - help="One or more source directories to search") - pargs = parser.parse_args(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="+", + help="One or more source directories to search") + pargs = parser.parse_args(args) - if check_dir(pargs.destination_dir) != 0: - return 1 + if not mk_genfile_common.check_dir_exists(pargs.destination_dir): + return 1 - for source_dir in pargs.source_dirs: - if check_dir(source_dir) != 0: - return 1 + for source_dir in pargs.source_dirs: + if not mk_genfile_common.check_dir_exists(source_dir): + return 1 - mk_util.mk_install_tactic_cpp_internal(pargs.source_dirs, pargs.destination_dir) - return 0 + output = mk_genfile_common.mk_install_tactic_cpp_internal( + pargs.source_dirs, + pargs.destination_dir + ) + logging.info('Generated "{}"'.format(output)) + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) - + sys.exit(main(sys.argv[1:])) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 260625ec4..b823ba327 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2682,82 +2682,14 @@ def mk_all_assembly_infos(major, minor, build, revision): else: raise MKException("Failed to find assembly template info file '%s'" % assembly_info_template) -ADD_TACTIC_DATA=[] -ADD_PROBE_DATA=[] - -def ADD_TACTIC(name, descr, cmd): - global ADD_TACTIC_DATA - ADD_TACTIC_DATA.append((name, descr, cmd)) - -def ADD_PROBE(name, descr, cmd): - global ADD_PROBE_DATA - ADD_PROBE_DATA.append((name, descr, cmd)) - -# Generate an install_tactics.cpp at path. -# This file implements the procedure -# void install_tactics(tactic_manager & ctx) -# It installs all tactics in the given component (name) list cnames -# The procedure looks for ADD_TACTIC commands in the .h files of these components. def mk_install_tactic_cpp(cnames, path): - component_src_dirs = [] - for cname in cnames: - c = get_component(cname) - component_src_dirs.append(c.src_dir) - mk_install_tactic_cpp_internal(component_src_dirs, path) - -def mk_install_tactic_cpp_internal(component_src_dirs, path): - global ADD_TACTIC_DATA, ADD_PROBE_DATA - ADD_TACTIC_DATA = [] - ADD_PROBE_DATA = [] - fullname = os.path.join(path, 'install_tactic.cpp') - fout = open(fullname, 'w') - fout.write('// Automatically generated file.\n') - fout.write('#include"tactic.h"\n') - fout.write('#include"tactic_cmds.h"\n') - fout.write('#include"cmd_context.h"\n') - tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') - probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') - 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)) - for h_file in h_files: - added_include = False - fin = open(os.path.join(component_src_dir, h_file), 'r') - for line in fin: - if tactic_pat.match(line): - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - try: - exec(line.strip('\n '), globals()) - except: - raise MKException("Failed processing ADD_TACTIC command at '%s'\n%s" % (fullname, line)) - if probe_pat.match(line): - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - try: - exec(line.strip('\n '), globals()) - except: - raise MKException("Failed processing ADD_PROBE command at '%s'\n%s" % (fullname, line)) - fin.close() - # First pass will just generate the tactic factories - idx = 0 - for data in ADD_TACTIC_DATA: - fout.write('MK_SIMPLE_TACTIC_FACTORY(__Z3_local_factory_%s, %s);\n' % (idx, data[2])) - idx = idx + 1 - fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, FACTORY) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, alloc(FACTORY)))\n') - fout.write('#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE))\n') - fout.write('void install_tactics(tactic_manager & ctx) {\n') - idx = 0 - for data in ADD_TACTIC_DATA: - fout.write(' ADD_TACTIC_CMD("%s", "%s", __Z3_local_factory_%s);\n' % (data[0], data[1], idx)) - idx = idx + 1 - for data in ADD_PROBE_DATA: - fout.write(' ADD_PROBE("%s", "%s", %s);\n' % data) - fout.write('}\n') - fout.close() + component_src_dirs = [] + for cname in cnames: + c = get_component(cname) + component_src_dirs.append(c.src_dir) + generated_file = mk_genfile_common.mk_install_tactic_cpp_internal(component_src_dirs, path) if VERBOSE: - print("Generated '%s'" % fullname) + print("Generated '{}'".format(generated_file)) def mk_all_install_tactic_cpps(): if not ONLY_MAKEFILES: From 114e165fadf2f8ae3ffd079dfeb98f3a1445c6cd Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 22:21:56 +0000 Subject: [PATCH 06/10] Move ``mk_mem_initializer_cpp_internal()`` from ``mk_util.py`` to ``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_mem_initializer_cpp.py`` to use the code at its new location. The interface has been changed slightly so that ``mk_mem_initializer_cpp_internal()`` now returns the path the generated file. The motivation behind this is so that clients of the function know the path of the generated file. Whilst I'm here reindent ``mk_mem_initializer_cpp.py`` and the relevant code in ``mk_util.py``. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. --- scripts/mk_genfile_common.py | 68 +++++++++++++++++++++++++++++++ scripts/mk_mem_initializer_cpp.py | 46 +++++++++------------ scripts/mk_util.py | 65 +++-------------------------- 3 files changed, 93 insertions(+), 86 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 05bf21f36..4c7565dac 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -308,3 +308,71 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): fout.write('}\n') fout.close() return fullname + +############################################################################### +# Functions for generating ``mem_initializer.cpp`` +############################################################################### + +def mk_mem_initializer_cpp_internal(component_src_dirs, path): + """ + Generate a ``mem_initializer.cpp`` file in the directory ``path``. + Returns the path to the generated file. + + This file implements the procedures + + ``` + void mem_initialize() + void mem_finalize() + ``` + + These procedures are invoked by the Z3 memory_manager + """ + assert isinstance(component_src_dirs, list) + assert check_dir_exists(path) + initializer_cmds = [] + finalizer_cmds = [] + fullname = os.path.join(path, 'mem_initializer.cpp') + fout = open(fullname, 'w') + fout.write('// Automatically generated file.\n') + initializer_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)') + # ADD_INITIALIZER with priority + initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') + finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') + 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)) + for h_file in h_files: + added_include = False + fin = open(os.path.join(component_src_dir, h_file), 'r') + for line in fin: + m = initializer_pat.match(line) + if m: + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + initializer_cmds.append((m.group(1), 0)) + m = initializer_prio_pat.match(line) + if m: + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + initializer_cmds.append((m.group(1), int(m.group(2)))) + m = finalizer_pat.match(line) + if m: + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + finalizer_cmds.append(m.group(1)) + fin.close() + initializer_cmds.sort(key=lambda tup: tup[1]) + fout.write('void mem_initialize() {\n') + for (cmd, prio) in initializer_cmds: + fout.write(cmd) + fout.write('\n') + fout.write('}\n') + fout.write('void mem_finalize() {\n') + for cmd in finalizer_cmds: + fout.write(cmd) + fout.write('\n') + fout.write('}\n') + fout.close() + return fullname diff --git a/scripts/mk_mem_initializer_cpp.py b/scripts/mk_mem_initializer_cpp.py index c8b68049f..b56fcbced 100755 --- a/scripts/mk_mem_initializer_cpp.py +++ b/scripts/mk_mem_initializer_cpp.py @@ -7,42 +7,34 @@ emits and implementation of ``void mem_finalize()`` into ``mem_initializer.cpp`` in the destination directory. """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys -def check_dir(path): - if not os.path.exists(path): - logging.error('"{}" does not exist'.format(path)) - return 1 - - if not os.path.isdir(path): - logging.error('"{}" is not a directory'.format(path)) - return 1 - - return 0 - - 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="+", - help="One or more source directories to search") - pargs = parser.parse_args(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="+", + help="One or more source directories to search") + pargs = parser.parse_args(args) - if check_dir(pargs.destination_dir) != 0: - return 1 + if not mk_genfile_common.check_dir_exists(pargs.destination_dir): + return 1 - for source_dir in pargs.source_dirs: - if check_dir(source_dir) != 0: - return 1 + for source_dir in pargs.source_dirs: + if not mk_genfile_common.check_dir_exists(source_dir): + return 1 - mk_util.mk_mem_initializer_cpp_internal(pargs.source_dirs, pargs.destination_dir) - return 0 + output = mk_genfile_common.mk_mem_initializer_cpp_internal( + pargs.source_dirs, + pargs.destination_dir + ) + logging.info('Generated "{}"'.format(output)) + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) + sys.exit(main(sys.argv[1:])) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index b823ba327..913914fef 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2700,67 +2700,14 @@ def mk_all_install_tactic_cpps(): cnames.append(c.name) mk_install_tactic_cpp(cnames, c.src_dir) -# Generate an mem_initializer.cpp at path. -# This file implements the procedures -# void mem_initialize() -# void mem_finalize() -# These procedures are invoked by the Z3 memory_manager def mk_mem_initializer_cpp(cnames, path): - component_src_dirs = [] - for cname in cnames: - c = get_component(cname) - component_src_dirs.append(c.src_dir) - mk_mem_initializer_cpp_internal(component_src_dirs, path) - -def mk_mem_initializer_cpp_internal(component_src_dirs, path): - initializer_cmds = [] - finalizer_cmds = [] - fullname = os.path.join(path, 'mem_initializer.cpp') - fout = open(fullname, 'w') - fout.write('// Automatically generated file.\n') - initializer_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)') - # ADD_INITIALIZER with priority - initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') - finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') - 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)) - for h_file in h_files: - added_include = False - fin = open(os.path.join(component_src_dir, h_file), 'r') - for line in fin: - m = initializer_pat.match(line) - if m: - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - initializer_cmds.append((m.group(1), 0)) - m = initializer_prio_pat.match(line) - if m: - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - initializer_cmds.append((m.group(1), int(m.group(2)))) - m = finalizer_pat.match(line) - if m: - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - finalizer_cmds.append(m.group(1)) - fin.close() - initializer_cmds.sort(key=lambda tup: tup[1]) - fout.write('void mem_initialize() {\n') - for (cmd, prio) in initializer_cmds: - fout.write(cmd) - fout.write('\n') - fout.write('}\n') - fout.write('void mem_finalize() {\n') - for cmd in finalizer_cmds: - fout.write(cmd) - fout.write('\n') - fout.write('}\n') - fout.close() + component_src_dirs = [] + 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) if VERBOSE: - print("Generated '%s'" % fullname) + print("Generated '{}'".format(generated_file)) def mk_all_mem_initializer_cpps(): if not ONLY_MAKEFILES: From 8840e5a00f52dd087fb1d3253efdfc927052991a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 23:21:09 +0000 Subject: [PATCH 07/10] Move ``mk_pat_db_internal()`` from ``mk_util.py`` to ``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_pat_db.py`` to use the code at its new location. Whilst I'm here reindent ``mk_mem_initializer_cpp.py``. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. --- scripts/mk_genfile_common.py | 15 +++++++++++++++ scripts/mk_pat_db.py | 31 +++++++++++++------------------ scripts/mk_util.py | 12 ++---------- 3 files changed, 30 insertions(+), 28 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 4c7565dac..943d4052a 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -376,3 +376,18 @@ def mk_mem_initializer_cpp_internal(component_src_dirs, path): fout.write('}\n') fout.close() return fullname + +############################################################################### +# Functions for generating ``database.h`` +############################################################################### + +def mk_pat_db_internal(inputFilePath, outputFilePath): + """ + Generate ``g_pattern_database[]`` declaration header file. + """ + with open(inputFilePath, 'r') as fin: + with open(outputFilePath, 'w') as fout: + fout.write('static char const g_pattern_database[] =\n') + for line in fin: + fout.write('"%s\\n"\n' % line.strip('\n')) + fout.write(';\n') diff --git a/scripts/mk_pat_db.py b/scripts/mk_pat_db.py index 3f2e7c507..76dc7ba48 100755 --- a/scripts/mk_pat_db.py +++ b/scripts/mk_pat_db.py @@ -3,32 +3,27 @@ Reads a pattern database and generates the corresponding header file. """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys def main(args): - logging.basicConfig(level=logging.INFO) - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("db_file", help="pattern database file") - parser.add_argument("output_file", help="output header file path") - pargs = parser.parse_args(args) + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("db_file", help="pattern database file") + parser.add_argument("output_file", help="output header file path") + pargs = parser.parse_args(args) - if not os.path.exists(pargs.db_file): - logging.error('"{}" does not exist'.format(pargs.db_file)) - return 1 + if not os.path.exists(pargs.db_file): + logging.error('"{}" does not exist'.format(pargs.db_file)) + return 1 - if (os.path.exists(pargs.output_file) and - not os.path.isfile(pargs.output_file)): - logging.error('Refusing to overwrite "{}"'.format( - pargs.output_file)) - return 1 - - mk_util.mk_pat_db_internal(pargs.db_file, pargs.output_file) - return 0 + mk_genfile_common.mk_pat_db_internal(pargs.db_file, pargs.output_file) + logging.info('Generated "{}"'.format(pargs.output_file)) + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) + sys.exit(main(sys.argv[1:])) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 913914fef..47afa2251 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2621,17 +2621,9 @@ def mk_pat_db(): c = get_component(PATTERN_COMPONENT) fin = os.path.join(c.src_dir, 'database.smt2') fout = os.path.join(c.src_dir, 'database.h') - mk_pat_db_internal(fin, fout) - -def mk_pat_db_internal(inputFilePath, outputFilePath): - with open(inputFilePath, 'r') as fin: - with open(outputFilePath, 'w') as fout: - fout.write('static char const g_pattern_database[] =\n') - for line in fin: - fout.write('"%s\\n"\n' % line.strip('\n')) - fout.write(';\n') + mk_genfile_common.mk_pat_db_internal(fin, fout) if VERBOSE: - print("Generated '%s'" % outputFilePath) + print("Generated '{}'".format(fout)) # Update version numbers def update_version(): From 87e99cd7342ec293f9ec1f39b57ebed817710232 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 9 Mar 2016 00:42:20 +0000 Subject: [PATCH 08/10] Move the code for generating ``*.hpp`` files from ``*.pyg`` from ``mk_util.py`` to ``mk_genfile_common.py``. A new function ``mk_hpp_from_pyg()`` has been added which provides a more sensible interface (hides the nasty ``exec()`` stuff) to create the ``*.hpp`` files from ``*.pyg`` files. Both ``mk_util.py`` and ``pyg2hpp.py`` have been modified to use the new interface. Whilst I'm here reindent ``pyg2hpp.py``. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. I've tested this change by making sure that the all the ``*.hpp`` files generated from ``*.pyg`` files match the files generated before this change. --- scripts/mk_genfile_common.py | 129 +++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 104 +--------------------------- scripts/pyg2hpp.py | 42 +++++------- 3 files changed, 150 insertions(+), 125 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 943d4052a..8b4b26313 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -391,3 +391,132 @@ def mk_pat_db_internal(inputFilePath, outputFilePath): for line in fin: fout.write('"%s\\n"\n' % line.strip('\n')) fout.write(';\n') + +############################################################################### +# Functions and data structures for generating ``*_params.hpp`` files from +# ``*.pyg`` files +############################################################################### + +UINT = 0 +BOOL = 1 +DOUBLE = 2 +STRING = 3 +SYMBOL = 4 +UINT_MAX = 4294967295 + +TYPE2CPK = { UINT : 'CPK_UINT', BOOL : 'CPK_BOOL', DOUBLE : 'CPK_DOUBLE', STRING : 'CPK_STRING', SYMBOL : 'CPK_SYMBOL' } +TYPE2CTYPE = { UINT : 'unsigned', BOOL : 'bool', DOUBLE : 'double', STRING : 'char const *', SYMBOL : 'symbol' } +TYPE2GETTER = { UINT : 'get_uint', BOOL : 'get_bool', DOUBLE : 'get_double', STRING : 'get_str', SYMBOL : 'get_sym' } + +def pyg_default(p): + if p[1] == BOOL: + if p[2]: + return "true" + else: + return "false" + return p[2] + +def pyg_default_as_c_literal(p): + if p[1] == BOOL: + if p[2]: + return "true" + else: + return "false" + elif p[1] == STRING: + return '"%s"' % p[2] + elif p[1] == SYMBOL: + return 'symbol("%s")' % p[2] + elif p[1] == UINT: + return '%su' % p[2] + else: + return p[2] + +def to_c_method(s): + return s.replace('.', '_') + + +def max_memory_param(): + return ('max_memory', UINT, UINT_MAX, 'maximum amount of memory in megabytes') + +def max_steps_param(): + return ('max_steps', UINT, UINT_MAX, 'maximum number of steps') + +def mk_hpp_from_pyg(pyg_file, output_dir): + """ + Generates the corresponding header file for the input pyg file + at the path ``pyg_file``. The file is emitted into the directory + ``output_dir``. + + Returns the path to the generated file + """ + CURRENT_PYG_HPP_DEST_DIR = output_dir + # Note OUTPUT_HPP_FILE cannot be a string as we need a mutable variable + # for the nested function to modify + OUTPUT_HPP_FILE = [ ] + # The function below has been nested so that it can use closure to capture + # the above variables that aren't global but instead local to this + # function. This avoids use of global state which makes this function safer. + def def_module_params(module_name, export, params, class_name=None, description=None): + dirname = CURRENT_PYG_HPP_DEST_DIR + assert(os.path.exists(dirname)) + if class_name is None: + class_name = '%s_params' % module_name + hpp = os.path.join(dirname, '%s.hpp' % class_name) + out = open(hpp, 'w') + out.write('// Automatically generated file\n') + out.write('#ifndef __%s_HPP_\n' % class_name.upper()) + out.write('#define __%s_HPP_\n' % class_name.upper()) + out.write('#include"params.h"\n') + if export: + out.write('#include"gparams.h"\n') + out.write('struct %s {\n' % class_name) + out.write(' params_ref const & p;\n') + if export: + out.write(' params_ref g;\n') + out.write(' %s(params_ref const & _p = params_ref::get_empty()):\n' % class_name) + out.write(' p(_p)') + if export: + out.write(', g(gparams::get_module("%s"))' % module_name) + out.write(' {}\n') + out.write(' static void collect_param_descrs(param_descrs & d) {\n') + for param in params: + out.write(' d.insert("%s", %s, "%s", "%s","%s");\n' % (param[0], TYPE2CPK[param[1]], param[3], pyg_default(param), module_name)) + out.write(' }\n') + if export: + out.write(' /*\n') + out.write(" REG_MODULE_PARAMS('%s', '%s::collect_param_descrs')\n" % (module_name, class_name)) + if description is not None: + out.write(" REG_MODULE_DESCRIPTION('%s', '%s')\n" % (module_name, description)) + out.write(' */\n') + # Generated accessors + for param in params: + if export: + out.write(' %s %s() const { return p.%s("%s", g, %s); }\n' % + (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) + else: + out.write(' %s %s() const { return p.%s("%s", %s); }\n' % + (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) + out.write('};\n') + out.write('#endif\n') + out.close() + OUTPUT_HPP_FILE.append(hpp) + + # Globals to use when executing the ``.pyg`` file. + pyg_globals = { + 'UINT' : UINT, + 'BOOL' : BOOL, + 'DOUBLE' : DOUBLE, + 'STRING' : STRING, + 'SYMBOL' : SYMBOL, + 'UINT_MAX' : UINT_MAX, + 'max_memory_param' : max_memory_param, + 'max_steps_param' : max_steps_param, + # Note that once this function is enterred that function + # executes with respect to the globals of this module and + # not the globals defined here + 'def_module_params' : def_module_params, + } + with open(pyg_file, 'r') as fh: + exec(fh.read() + "\n", pyg_globals, None) + assert len(OUTPUT_HPP_FILE) == 1 + return OUTPUT_HPP_FILE[0] diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 47afa2251..1c7ee4ab5 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2499,104 +2499,6 @@ def mk_auto_src(): mk_all_mem_initializer_cpps() mk_all_gparams_register_modules() -UINT = 0 -BOOL = 1 -DOUBLE = 2 -STRING = 3 -SYMBOL = 4 -UINT_MAX = 4294967295 -CURRENT_PYG_HPP_DEST_DIR = None - -def get_current_pyg_hpp_dest_dir(): - return CURRENT_PYG_HPP_DEST_DIR - -TYPE2CPK = { UINT : 'CPK_UINT', BOOL : 'CPK_BOOL', DOUBLE : 'CPK_DOUBLE', STRING : 'CPK_STRING', SYMBOL : 'CPK_SYMBOL' } -TYPE2CTYPE = { UINT : 'unsigned', BOOL : 'bool', DOUBLE : 'double', STRING : 'char const *', SYMBOL : 'symbol' } -TYPE2GETTER = { UINT : 'get_uint', BOOL : 'get_bool', DOUBLE : 'get_double', STRING : 'get_str', SYMBOL : 'get_sym' } - -def pyg_default(p): - if p[1] == BOOL: - if p[2]: - return "true" - else: - return "false" - return p[2] - -def pyg_default_as_c_literal(p): - if p[1] == BOOL: - if p[2]: - return "true" - else: - return "false" - elif p[1] == STRING: - return '"%s"' % p[2] - elif p[1] == SYMBOL: - return 'symbol("%s")' % p[2] - elif p[1] == UINT: - return '%su' % p[2] - else: - return p[2] - -def to_c_method(s): - return s.replace('.', '_') - -def def_module_params(module_name, export, params, class_name=None, description=None): - dirname = get_current_pyg_hpp_dest_dir() - assert(os.path.exists(dirname)) - if class_name is None: - class_name = '%s_params' % module_name - hpp = os.path.join(dirname, '%s.hpp' % class_name) - out = open(hpp, 'w') - out.write('// Automatically generated file\n') - out.write('#ifndef __%s_HPP_\n' % class_name.upper()) - out.write('#define __%s_HPP_\n' % class_name.upper()) - out.write('#include"params.h"\n') - if export: - out.write('#include"gparams.h"\n') - out.write('struct %s {\n' % class_name) - out.write(' params_ref const & p;\n') - if export: - out.write(' params_ref g;\n') - out.write(' %s(params_ref const & _p = params_ref::get_empty()):\n' % class_name) - out.write(' p(_p)') - if export: - out.write(', g(gparams::get_module("%s"))' % module_name) - out.write(' {}\n') - out.write(' static void collect_param_descrs(param_descrs & d) {\n') - for param in params: - out.write(' d.insert("%s", %s, "%s", "%s","%s");\n' % (param[0], TYPE2CPK[param[1]], param[3], pyg_default(param), module_name)) - out.write(' }\n') - if export: - out.write(' /*\n') - out.write(" REG_MODULE_PARAMS('%s', '%s::collect_param_descrs')\n" % (module_name, class_name)) - if description is not None: - out.write(" REG_MODULE_DESCRIPTION('%s', '%s')\n" % (module_name, description)) - out.write(' */\n') - # Generated accessors - for param in params: - if export: - out.write(' %s %s() const { return p.%s("%s", g, %s); }\n' % - (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) - else: - out.write(' %s %s() const { return p.%s("%s", %s); }\n' % - (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) - out.write('};\n') - out.write('#endif\n') - out.close() - if is_verbose(): - print("Generated '%s'" % hpp) - -def max_memory_param(): - return ('max_memory', UINT, UINT_MAX, 'maximum amount of memory in megabytes') - -def max_steps_param(): - return ('max_steps', UINT, UINT_MAX, 'maximum number of steps') - -PYG_GLOBALS = { 'UINT' : UINT, 'BOOL' : BOOL, 'DOUBLE' : DOUBLE, 'STRING' : STRING, 'SYMBOL' : SYMBOL, - 'UINT_MAX' : UINT_MAX, - 'max_memory_param' : max_memory_param, - 'max_steps_param' : max_steps_param, - 'def_module_params' : def_module_params } def _execfile(file, globals=globals(), locals=locals()): if sys.version < "2.7": @@ -2607,13 +2509,13 @@ def _execfile(file, globals=globals(), locals=locals()): # Execute python auxiliary scripts that generate extra code for Z3. def exec_pyg_scripts(): - global CURRENT_PYG_HPP_DEST_DIR for root, dirs, files in os.walk('src'): for f in files: if f.endswith('.pyg'): script = os.path.join(root, f) - CURRENT_PYG_HPP_DEST_DIR = root - _execfile(script, PYG_GLOBALS) + generated_file = mk_genfile_common.mk_hpp_from_pyg(script, root) + if is_verbose(): + print("Generated '{}'".format(generated_file)) # TODO: delete after src/ast/pattern/expr_pattern_match # database.smt ==> database.h diff --git a/scripts/pyg2hpp.py b/scripts/pyg2hpp.py index f1ada2b84..b1af3edc9 100755 --- a/scripts/pyg2hpp.py +++ b/scripts/pyg2hpp.py @@ -4,39 +4,33 @@ Reads a pyg file and emits the corresponding C++ header file into the specified destination directory. """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys def main(args): - logging.basicConfig(level=logging.INFO) - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("pyg_file", help="pyg file") - parser.add_argument("destination_dir", help="destination directory") - pargs = parser.parse_args(args) + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("pyg_file", help="pyg file") + parser.add_argument("destination_dir", help="destination directory") + pargs = parser.parse_args(args) - if not os.path.exists(pargs.pyg_file): - logging.error('"{}" does not exist'.format(pargs.pyg_file)) - return 1 + if not os.path.exists(pargs.pyg_file): + logging.error('"{}" does not exist'.format(pargs.pyg_file)) + return 1 - if not os.path.exists(pargs.destination_dir): - logging.error('"{}" does not exist'.format(pargs.destination_dir)) - return 1 + if not mk_genfile_common.check_dir_exists(pargs.destination_dir): + return 1 - if not os.path.isdir(pargs.destination_dir): - logging.error('"{}" is not a directory'.format(pargs.destination_dir)) - return 1 - - pyg_full_path = os.path.abspath(pargs.pyg_file) - destination_dir_full_path = os.path.abspath(pargs.destination_dir) - logging.info('Using {}'.format(pyg_full_path)) - # Use the existing infrastructure to do this - mk_util.CURRENT_PYG_HPP_DEST_DIR = destination_dir_full_path - mk_util._execfile(pyg_full_path, mk_util.PYG_GLOBALS) - return 0 + pyg_full_path = os.path.abspath(pargs.pyg_file) + destination_dir_full_path = os.path.abspath(pargs.destination_dir) + logging.info('Using {}'.format(pyg_full_path)) + output = mk_genfile_common.mk_hpp_from_pyg(pyg_full_path, destination_dir_full_path) + logging.info('Generated "{}"'.format(output)) + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) + sys.exit(main(sys.argv[1:])) From b3f6a3c4af0d157140a1a537927b9c086bef9b22 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 9 Mar 2016 01:20:08 +0000 Subject: [PATCH 09/10] Remove use of global data structures in ``mk_install_tactic_cpp_internal()`` --- scripts/mk_genfile_common.py | 29 +++++++++++++---------------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 8b4b26313..790ce7205 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -223,19 +223,6 @@ def mk_gparams_register_modules_internal(component_src_dirs, path): # Functions/data structures for generating ``install_tactics.cpp`` ############################################################################### -# FIXME: Remove use of global data structures -ADD_TACTIC_DATA=[] -ADD_PROBE_DATA=[] - -def ADD_TACTIC(name, descr, cmd): - global ADD_TACTIC_DATA - ADD_TACTIC_DATA.append((name, descr, cmd)) - -def ADD_PROBE(name, descr, cmd): - global ADD_PROBE_DATA - ADD_PROBE_DATA.append((name, descr, cmd)) - - def mk_install_tactic_cpp_internal(component_src_dirs, path): """ Generate a ``install_tactics.cpp`` file in the directory ``path``. @@ -251,9 +238,19 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): ``component_src_dirs`` The procedure looks for ``ADD_TACTIC`` commands in the ``.h`` and ``.hpp`` files of these components. """ - global ADD_TACTIC_DATA, ADD_PROBE_DATA ADD_TACTIC_DATA = [] ADD_PROBE_DATA = [] + def ADD_TACTIC(name, descr, cmd): + ADD_TACTIC_DATA.append((name, descr, cmd)) + + def ADD_PROBE(name, descr, cmd): + ADD_PROBE_DATA.append((name, descr, cmd)) + + exec_globals = { + 'ADD_TACTIC': ADD_TACTIC, + 'ADD_PROBE': ADD_PROBE, + } + assert isinstance(component_src_dirs, list) assert check_dir_exists(path) fullname = os.path.join(path, 'install_tactic.cpp') @@ -275,7 +272,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): added_include = True fout.write('#include"%s"\n' % h_file) try: - exec(line.strip('\n '), globals()) + exec(line.strip('\n '), exec_globals) except Exception as e: _logger.error("Failed processing ADD_TACTIC command at '{}'\n{}".format( fullname, line)) @@ -285,7 +282,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): added_include = True fout.write('#include"%s"\n' % h_file) try: - exec(line.strip('\n '), globals()) + exec(line.strip('\n '), exec_globals) except Exception as e: _logger.error("Failed processing ADD_PROBE command at '{}'\n{}".format( fullname, line)) From 98244ac9a97c4f5e641024657d0a4cd82e0ff9ab Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 9 Mar 2016 01:26:06 +0000 Subject: [PATCH 10/10] [CMake] Remove global "generated file" dependency on ``mk_util.py``. Most file generation scripts don't depend on it anymore. The exceptions are uses of ``update_api.py``. An explicit dependency has been added here and a ``FIXME`` has been left to indicate that this should be removed once ``update_api.py`` is completly independent of ``mk_util.py``. --- CMakeLists.txt | 2 -- contrib/cmake/src/api/CMakeLists.txt | 2 ++ contrib/cmake/src/api/python/CMakeLists.txt | 2 ++ 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 5cdf06120..0204a8a44 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -340,9 +340,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") ################################################################################ # Note: ``update_api.py`` is deliberately not here because it not used # to generate every generated file. The targets that need it list it explicitly. -# FIXME: We should drop the dependency on ``mk_util.py`` set(Z3_GENERATED_FILE_EXTRA_DEPENDENCIES - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" "${CMAKE_SOURCE_DIR}/scripts/mk_genfile_common.py" ) diff --git a/contrib/cmake/src/api/CMakeLists.txt b/contrib/cmake/src/api/CMakeLists.txt index 78837c001..8e796168f 100644 --- a/contrib/cmake/src/api/CMakeLists.txt +++ b/contrib/cmake/src/api/CMakeLists.txt @@ -26,6 +26,8 @@ add_custom_command(OUTPUT ${generated_files} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/update_api.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency + "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" COMMENT "Generating ${generated_files}" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM diff --git a/contrib/cmake/src/api/python/CMakeLists.txt b/contrib/cmake/src/api/python/CMakeLists.txt index 05d04e552..6e4096057 100644 --- a/contrib/cmake/src/api/python/CMakeLists.txt +++ b/contrib/cmake/src/api/python/CMakeLists.txt @@ -39,6 +39,8 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3core.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "${CMAKE_SOURCE_DIR}/scripts/update_api.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} + # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency + "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" COMMENT "Generating z3core.py" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} )