diff --git a/CMakeLists.txt b/CMakeLists.txt index 97c8b1862..d33f352e1 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -335,6 +335,17 @@ 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. +set(Z3_GENERATED_FILE_EXTRA_DEPENDENCIES + "${CMAKE_SOURCE_DIR}/scripts/mk_genfile_common.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 2bf7442ab..00dd01627 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..8e796168f 100644 --- a/contrib/cmake/src/api/CMakeLists.txt +++ b/contrib/cmake/src/api/CMakeLists.txt @@ -24,8 +24,10 @@ 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} + # 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 2279be716..6e4096057 100644 --- a/contrib/cmake/src/api/python/CMakeLists.txt +++ b/contrib/cmake/src/api/python/CMakeLists.txt @@ -38,6 +38,8 @@ 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" + ${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} @@ -54,7 +56,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 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_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 new file mode 100644 index 000000000..790ce7205 --- /dev/null +++ b/scripts/mk_genfile_common.py @@ -0,0 +1,519 @@ +# 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 + +############################################################################### +# 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() + +############################################################################### +# 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 + +############################################################################### +# Functions/data structures for generating ``install_tactics.cpp`` +############################################################################### + +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. + """ + 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') + 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 '), exec_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 '), exec_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 + +############################################################################### +# 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 + +############################################################################### +# 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') + +############################################################################### +# 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_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_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_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_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 188dad7a4..1c7ee4ab5 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 @@ -2498,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": @@ -2606,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 @@ -2620,17 +2523,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(): @@ -2681,82 +2576,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: @@ -2767,67 +2594,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: @@ -2838,61 +2612,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: @@ -2912,28 +2639,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) @@ -3026,83 +2732,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 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:]))