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):