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: