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: