From b3713e7496eb3a32a7109a5f3b2007b190344644 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 6 Apr 2016 22:47:28 +0100 Subject: [PATCH] Refactor ``mk_z3consts_java()`` code into ``mk_z3consts_java_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 | 19 ++++++ scripts/mk_genfile_common.py | 110 +++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 106 +++------------------------------ 3 files changed, 137 insertions(+), 98 deletions(-) diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py index 482b13c94..e582d8468 100755 --- a/scripts/mk_consts_files.py +++ b/scripts/mk_consts_files.py @@ -17,6 +17,11 @@ def main(args): 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) + parser.add_argument("--java-output-dir", dest="java_output_dir", default=None) + parser.add_argument("--java-package-name", + dest="java_package_name", + default=None, + help="Name to give the Java package (e.g. ``com.microsoft.z3``).") pargs = parser.parse_args(args) if not mk_genfile_common.check_files_exist(pargs.api_files): @@ -41,6 +46,20 @@ def main(args): logging.info('Generated "{}"'.format(output)) count += 1 + if pargs.java_output_dir: + if pargs.java_package_name == None: + logging.error('Java package name must be specified') + return 1 + if not mk_genfile_common.check_dir_exists(pargs.java_output_dir): + return 1 + outputs = mk_genfile_common.mk_z3consts_java_internal( + pargs.api_files, + pargs.java_package_name, + pargs.java_output_dir) + for generated_file in outputs: + logging.info('Generated "{}"'.format(generated_file)) + 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 0734d52b0..d747baee8 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -255,6 +255,116 @@ def mk_z3consts_dotnet_internal(api_files, output_dir): z3consts.close() return z3consts_output_path + +def mk_z3consts_java_internal(api_files, package_name, output_dir): + """ + Generate "com.microsoft.z3.enumerations" package from the list of API + header files in ``api_files`` and write the package directory into + the ``output_dir`` directory + + Returns a list of the generated java source files. + """ + blank_pat = re.compile("^ *$") + 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' ] + gendir = os.path.join(output_dir, "enumerations") + if not os.path.exists(gendir): + os.mkdir(gendir) + + generated_enumeration_files = [] + 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: + efile = open('%s.java' % os.path.join(gendir, name), 'w') + generated_enumeration_files.append(efile.name) + efile.write('/**\n * Automatically generated file\n **/\n\n') + efile.write('package %s.enumerations;\n\n' % package_name) + + efile.write('/**\n') + efile.write(' * %s\n' % name) + efile.write(' **/\n') + efile.write('public enum %s {\n' % name) + efile.write + first = True + for k in decls: + i = decls[k] + if first: + first = False + else: + efile.write(',\n') + efile.write(' %s (%s)' % (k, i)) + efile.write(";\n") + efile.write('\n private final int intValue;\n\n') + efile.write(' %s(int v) {\n' % name) + efile.write(' this.intValue = v;\n') + efile.write(' }\n\n') + efile.write(' public static final %s fromInt(int v) {\n' % name) + efile.write(' for (%s k: values()) \n' % name) + efile.write(' if (k.intValue == v) return k;\n') + efile.write(' return values()[0];\n') + efile.write(' }\n\n') + efile.write(' public final int toInt() { return this.intValue; }\n') + # efile.write(';\n %s(int v) {}\n' % name) + efile.write('}\n\n') + efile.close() + mode = SEARCHING + 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() + return generated_enumeration_files + + ############################################################################### # Functions for generating a "module definition file" for MSVC ############################################################################### diff --git a/scripts/mk_util.py b/scripts/mk_util.py index be641ba35..38bf2a854 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2753,109 +2753,19 @@ def mk_z3consts_dotnet(api_files): # Extract enumeration types from z3_api.h, and add Java definitions def mk_z3consts_java(api_files): - blank_pat = re.compile("^ *$") - comment_pat = re.compile("^ *//.*$") - typedef_pat = re.compile("typedef enum *") - typedef2_pat = re.compile("typedef enum { *") - openbrace_pat = re.compile("{ *") - closebrace_pat = re.compile("}.*;") - java = get_component(JAVA_COMPONENT) - - DeprecatedEnums = [ 'Z3_search_failure' ] - gendir = os.path.join(java.src_dir, "enumerations") - if not os.path.exists(gendir): - os.mkdir(gendir) - + full_path_api_files = [] for api_file in api_files: api_file_c = java.find_file(api_file, java.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: - efile = open('%s.java' % os.path.join(gendir, name), 'w') - efile.write('/**\n * Automatically generated file\n **/\n\n') - efile.write('package %s.enumerations;\n\n' % java.package_name) - - efile.write('/**\n') - efile.write(' * %s\n' % name) - efile.write(' **/\n') - efile.write('public enum %s {\n' % name) - efile.write - first = True - for k in decls: - i = decls[k] - if first: - first = False - else: - efile.write(',\n') - efile.write(' %s (%s)' % (k, i)) - efile.write(";\n") - efile.write('\n private final int intValue;\n\n') - efile.write(' %s(int v) {\n' % name) - efile.write(' this.intValue = v;\n') - efile.write(' }\n\n') - efile.write(' public static final %s fromInt(int v) {\n' % name) - efile.write(' for (%s k: values()) \n' % name) - efile.write(' if (k.intValue == v) return k;\n') - efile.write(' return values()[0];\n') - efile.write(' }\n\n') - efile.write(' public final int toInt() { return this.intValue; }\n') - # efile.write(';\n %s(int v) {}\n' % name) - efile.write('}\n\n') - efile.close() - mode = SEARCHING - 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() + full_path_api_files.append(api_file) + generated_files = mk_genfile_common.mk_z3consts_java_internal( + full_path_api_files, + java.package_name, + java.src_dir) if VERBOSE: - print("Generated '%s'" % ('%s' % gendir)) + for generated_file in generated_files: + print("Generated '{}'".format(generated_file)) # Extract enumeration types from z3_api.h, and add ML definitions def mk_z3consts_ml(api_files):