From 2b64729b2174bbae9d87d28a5e26afebafc6fce0 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 16:54:22 +0000 Subject: [PATCH] Move ``mk_z3consts_py_internal()`` out of ``mk_util.py`` into ``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_consts_files.py`` to use the code at its new location. The interface has been changed slightly so that ``mk_z3consts_py_internal()`` now returns the path to the generated file. The motivation behind this is so that clients of the function know the path to the generated file. Whilst I'm here also reindent ``mk_consts_files.py`` and move some of its code into ``mk_genfile_common.py`` so it can be shared. Also update Z3_GENERATED_FILE_EXTRA_DEPENDENCIES in the CMake build so it knows about ``mk_genfile_common.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. --- CMakeLists.txt | 1 + scripts/mk_consts_files.py | 50 ++++++-------- scripts/mk_genfile_common.py | 126 +++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 79 +--------------------- 4 files changed, 152 insertions(+), 104 deletions(-) create mode 100644 scripts/mk_genfile_common.py diff --git a/CMakeLists.txt b/CMakeLists.txt index 8ed9f5201..5cdf06120 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -343,6 +343,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") # FIXME: We should drop the dependency on ``mk_util.py`` set(Z3_GENERATED_FILE_EXTRA_DEPENDENCIES "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + "${CMAKE_SOURCE_DIR}/scripts/mk_genfile_common.py" ) ################################################################################ diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py index 543c56e0e..2c017bd2c 100755 --- a/scripts/mk_consts_files.py +++ b/scripts/mk_consts_files.py @@ -4,44 +4,38 @@ Reads a list of Z3 API header files and generate the constant declarations need by one or more Z3 language bindings """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys -def check_dir(output_dir): - if not os.path.isdir(output_dir): - logging.error('"{}" is not an existing directory'.format(output_dir)) - return 1 - return 0 def main(args): - logging.basicConfig(level=logging.INFO) - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("api_files", nargs="+") - parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None) - pargs = parser.parse_args(args) + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("api_files", nargs="+") + parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None) + pargs = parser.parse_args(args) - for api_file in pargs.api_files: - if not os.path.exists(api_file): - logging.error('"{}" does not exist'.format(api_file)) - return 1 + if not mk_genfile_common.check_files_exist(pargs.api_files): + logging.error('One or more API files do not exist') + return 1 - count = 0 + count = 0 - if pargs.z3py_output_dir: - if check_dir(pargs.z3py_output_dir) != 0: - return 1 - mk_util.mk_z3consts_py_internal(pargs.api_files, pargs.z3py_output_dir) - count += 1 + if pargs.z3py_output_dir: + if not mk_genfile_common.check_dir_exists(pargs.z3py_output_dir): + return 1 + output = mk_genfile_common.mk_z3consts_py_internal(pargs.api_files, pargs.z3py_output_dir) + logging.info('Generated "{}"'.format(output)) + count += 1 - if count == 0: - logging.info('No files generated. You need to specific an output directory' - ' for the relevant langauge bindings') - # TODO: Add support for other bindings - return 0 + if count == 0: + logging.info('No files generated. You need to specific an output directory' + ' for the relevant langauge bindings') + # TODO: Add support for other bindings + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) - + sys.exit(main(sys.argv[1:])) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py new file mode 100644 index 000000000..abe10a0d1 --- /dev/null +++ b/scripts/mk_genfile_common.py @@ -0,0 +1,126 @@ +# This file contains code that is common to +# both the Python build system and the CMake +# build system. +# +# The code here generally is involved in +# generating files needed by Z3 at build time. +# +# You should **not** import ``mk_util`` here +# to avoid having this code depend on the +# of the Python build system. +import os +import logging +import re +import sys + +# Logger for this module +_logger = logging.getLogger(__name__) + + +############################################################################### +# Utility functions +############################################################################### +def check_dir_exists(output_dir): + """ + Returns ``True`` if ``output_dir`` exists, otherwise + returns ``False``. + """ + if not os.path.isdir(output_dir): + _logger.error('"{}" is not an existing directory'.format(output_dir)) + return False + return True + +def check_files_exist(files): + assert isinstance(files, list) + for f in files: + if not os.path.exists(f): + _logger.error('"{}" does not exist'.format(f)) + return False + return True + +############################################################################### +# Functions for generating constant declarations for language bindings +############################################################################### + +def mk_z3consts_py_internal(api_files, output_dir): + """ + Generate ``z3consts.py`` from the list of API header files + in ``api_files`` and write the output file into + the ``output_dir`` directory + + Returns the path to the generated file. + """ + assert os.path.isdir(output_dir) + assert isinstance(api_files, list) + + blank_pat = re.compile("^ *\r?$") + comment_pat = re.compile("^ *//.*$") + typedef_pat = re.compile("typedef enum *") + typedef2_pat = re.compile("typedef enum { *") + openbrace_pat = re.compile("{ *") + closebrace_pat = re.compile("}.*;") + + z3consts = open(os.path.join(output_dir, 'z3consts.py'), 'w') + z3consts_output_path = z3consts.name + z3consts.write('# Automatically generated file\n\n') + for api_file in api_files: + api = open(api_file, 'r') + + SEARCHING = 0 + FOUND_ENUM = 1 + IN_ENUM = 2 + + mode = SEARCHING + decls = {} + idx = 0 + + linenum = 1 + for line in api: + m1 = blank_pat.match(line) + m2 = comment_pat.match(line) + if m1 or m2: + # skip blank lines and comments + linenum = linenum + 1 + elif mode == SEARCHING: + m = typedef_pat.match(line) + if m: + mode = FOUND_ENUM + m = typedef2_pat.match(line) + if m: + mode = IN_ENUM + decls = {} + idx = 0 + elif mode == FOUND_ENUM: + m = openbrace_pat.match(line) + if m: + mode = IN_ENUM + decls = {} + idx = 0 + else: + assert False, "Invalid %s, line: %s" % (api_file, linenum) + else: + assert mode == IN_ENUM + words = re.split('[^\-a-zA-Z0-9_]+', line) + m = closebrace_pat.match(line) + if m: + name = words[1] + z3consts.write('# enum %s\n' % name) + for k in decls: + i = decls[k] + z3consts.write('%s = %s\n' % (k, i)) + z3consts.write('\n') + mode = SEARCHING + elif len(words) <= 2: + assert False, "Invalid %s, line: %s" % (api_file, linenum) + else: + if words[2] != '': + if len(words[2]) > 1 and words[2][1] == 'x': + idx = int(words[2], 16) + else: + idx = int(words[2]) + decls[words[1]] = idx + idx = idx + 1 + linenum = linenum + 1 + api.close() + z3consts.close() + return z3consts_output_path diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 188dad7a4..da3c6eef9 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -12,6 +12,7 @@ import re import getopt import shutil from mk_exception import * +import mk_genfile_common from fnmatch import fnmatch import distutils.sysconfig import compileall @@ -3026,83 +3027,9 @@ def mk_z3consts_py(api_files): api_file_c = api_dll.find_file(api_file, api_dll.name) api_file = os.path.join(api_file_c.src_dir, api_file) full_path_api_files.append(api_file) - mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR) - -def mk_z3consts_py_internal(api_files, output_dir): - assert os.path.isdir(output_dir) - assert isinstance(api_files, list) - - blank_pat = re.compile("^ *\r?$") - comment_pat = re.compile("^ *//.*$") - typedef_pat = re.compile("typedef enum *") - typedef2_pat = re.compile("typedef enum { *") - openbrace_pat = re.compile("{ *") - closebrace_pat = re.compile("}.*;") - - z3consts = open(os.path.join(output_dir, 'z3consts.py'), 'w') - z3consts.write('# Automatically generated file\n\n') - for api_file in api_files: - api = open(api_file, 'r') - - SEARCHING = 0 - FOUND_ENUM = 1 - IN_ENUM = 2 - - mode = SEARCHING - decls = {} - idx = 0 - - linenum = 1 - for line in api: - m1 = blank_pat.match(line) - m2 = comment_pat.match(line) - if m1 or m2: - # skip blank lines and comments - linenum = linenum + 1 - elif mode == SEARCHING: - m = typedef_pat.match(line) - if m: - mode = FOUND_ENUM - m = typedef2_pat.match(line) - if m: - mode = IN_ENUM - decls = {} - idx = 0 - elif mode == FOUND_ENUM: - m = openbrace_pat.match(line) - if m: - mode = IN_ENUM - decls = {} - idx = 0 - else: - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - assert mode == IN_ENUM - words = re.split('[^\-a-zA-Z0-9_]+', line) - m = closebrace_pat.match(line) - if m: - name = words[1] - z3consts.write('# enum %s\n' % name) - for k in decls: - i = decls[k] - z3consts.write('%s = %s\n' % (k, i)) - z3consts.write('\n') - mode = SEARCHING - elif len(words) <= 2: - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - if words[2] != '': - if len(words[2]) > 1 and words[2][1] == 'x': - idx = int(words[2], 16) - else: - idx = int(words[2]) - decls[words[1]] = idx - idx = idx + 1 - linenum = linenum + 1 - api.close() - z3consts.close() + generated_file = mk_genfile_common.mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR) if VERBOSE: - print("Generated '%s'" % os.path.join(output_dir, 'z3consts.py')) + print("Generated '{}".format(generated_file)) # Extract enumeration types from z3_api.h, and add .Net definitions