mirror of
https://github.com/Z3Prover/z3
synced 2025-04-14 12:58:44 +00:00
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.
This commit is contained in:
Dan Liew
parent
404aa2a5a0
commit
f4e98a4fe5
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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:]))
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
Loading…
Reference in a new issue