From 87e99cd7342ec293f9ec1f39b57ebed817710232 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 9 Mar 2016 00:42:20 +0000 Subject: [PATCH] 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:]))