From d3f87e44a2481ca3301d2317f4b177199f4ab7b7 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 26 Mar 2016 13:39:10 +0000 Subject: [PATCH] Refactor ``mk_z3consts_dotnet()`` code into ``mk_z3consts_dotnet_internal()`` and move that into ``mk_genfile_common.py``. Then adapt ``mk_util.py`` and ``mk_consts_files.py`` to call into the code at its new location. 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. --- scripts/mk_consts_files.py | 10 ++++ scripts/mk_genfile_common.py | 92 ++++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 87 ++-------------------------------- 3 files changed, 106 insertions(+), 83 deletions(-) diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py index 2c017bd2c..482b13c94 100755 --- a/scripts/mk_consts_files.py +++ b/scripts/mk_consts_files.py @@ -16,6 +16,7 @@ def main(args): parser = argparse.ArgumentParser(description=__doc__) parser.add_argument("api_files", nargs="+") parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None) + parser.add_argument("--dotnet-output-dir", dest="dotnet_output_dir", default=None) pargs = parser.parse_args(args) if not mk_genfile_common.check_files_exist(pargs.api_files): @@ -31,6 +32,15 @@ def main(args): logging.info('Generated "{}"'.format(output)) count += 1 + if pargs.dotnet_output_dir: + if not mk_genfile_common.check_dir_exists(pargs.dotnet_output_dir): + return 1 + output = mk_genfile_common.mk_z3consts_dotnet_internal( + pargs.api_files, + pargs.dotnet_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') diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 38d173108..9c6431248 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -163,6 +163,98 @@ def mk_z3consts_py_internal(api_files, output_dir): z3consts.close() return z3consts_output_path +def mk_z3consts_dotnet_internal(api_files, output_dir): + """ + Generate ``Enumerations.cs`` 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("}.*;") + + DeprecatedEnums = [ 'Z3_search_failure' ] + z3consts = open(os.path.join(output_dir, 'Enumerations.cs'), 'w') + z3consts_output_path = z3consts.name + z3consts.write('// Automatically generated file\n\n') + z3consts.write('using System;\n\n' + '#pragma warning disable 1591\n\n' + 'namespace Microsoft.Z3\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] + if name not in DeprecatedEnums: + z3consts.write(' /// %s\n' % name) + z3consts.write(' public enum %s {\n' % name) + z3consts.write + for k in decls: + i = decls[k] + z3consts.write(' %s = %s,\n' % (k, i)) + z3consts.write(' }\n\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.write('}\n'); + z3consts.close() + return z3consts_output_path + ############################################################################### # Functions for generating a "module definition file" for MSVC ############################################################################### diff --git a/scripts/mk_util.py b/scripts/mk_util.py index e6de3e8ea..dc85c2b76 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2738,96 +2738,17 @@ def mk_z3consts_py(api_files): if VERBOSE: print("Generated '{}".format(generated_file)) - # Extract enumeration types from z3_api.h, and add .Net definitions def mk_z3consts_dotnet(api_files): - 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("}.*;") - dotnet = get_component(DOTNET_COMPONENT) - - DeprecatedEnums = [ 'Z3_search_failure' ] - z3consts = open(os.path.join(dotnet.src_dir, 'Enumerations.cs'), 'w') - z3consts.write('// Automatically generated file\n\n') - z3consts.write('using System;\n\n' - '#pragma warning disable 1591\n\n' - 'namespace Microsoft.Z3\n' - '{\n') - + full_path_api_files = [] for api_file in api_files: api_file_c = dotnet.find_file(api_file, dotnet.name) api_file = os.path.join(api_file_c.src_dir, api_file) - - 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] - if name not in DeprecatedEnums: - z3consts.write(' /// %s\n' % name) - z3consts.write(' public enum %s {\n' % name) - z3consts.write - for k in decls: - i = decls[k] - z3consts.write(' %s = %s,\n' % (k, i)) - z3consts.write(' }\n\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.write('}\n'); - z3consts.close() + full_path_api_files.append(api_file) + generated_file = mk_genfile_common.mk_z3consts_dotnet_internal(full_path_api_files, dotnet.src_dir) if VERBOSE: - print("Generated '%s'" % os.path.join(dotnet.src_dir, 'Enumerations.cs')) - + print("Generated '{}".format(generated_file)) # Extract enumeration types from z3_api.h, and add Java definitions def mk_z3consts_java(api_files):