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