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