diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py index e582d8468..d0502c19d 100755 --- a/scripts/mk_consts_files.py +++ b/scripts/mk_consts_files.py @@ -22,6 +22,7 @@ def main(args): dest="java_package_name", default=None, help="Name to give the Java package (e.g. ``com.microsoft.z3``).") + parser.add_argument("--ml-output-dir", dest="ml_output_dir", default=None) pargs = parser.parse_args(args) if not mk_genfile_common.check_files_exist(pargs.api_files): @@ -60,6 +61,15 @@ def main(args): logging.info('Generated "{}"'.format(generated_file)) count += 1 + if pargs.ml_output_dir: + if not mk_genfile_common.check_dir_exists(pargs.ml_output_dir): + return 1 + output = mk_genfile_common.mk_z3consts_ml_internal( + pargs.api_files, + pargs.ml_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 7e7cb5584..98346f99f 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -376,6 +376,180 @@ def mk_z3consts_java_internal(api_files, package_name, output_dir): api.close() return generated_enumeration_files +# Extract enumeration types from z3_api.h, and add ML definitions +def mk_z3consts_ml_internal(api_files, output_dir): + """ + Generate ``z3enums.ml`` 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("^ *$") + 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' ] + if not os.path.exists(output_dir): + os.mkdir(output_dir) + + efile = open('%s.ml' % os.path.join(output_dir, "z3enums"), 'w') + z3consts_output_path = efile.name + efile.write('(* Automatically generated file *)\n\n') + efile.write('(** The enumeration types of 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: + sorted_decls = sorted(decls.items(), key=lambda pair: pair[1]) + efile.write('(** %s *)\n' % name[3:]) + efile.write('type %s =\n' % name[3:]) # strip Z3_ + for k, i in sorted_decls: + efile.write(' | %s \n' % k[3:]) # strip Z3_ + efile.write('\n') + efile.write('(** Convert %s to int*)\n' % name[3:]) + efile.write('let int_of_%s x : int =\n' % (name[3:])) # strip Z3_ + efile.write(' match x with\n') + for k, i in sorted_decls: + efile.write(' | %s -> %d\n' % (k[3:], i)) + efile.write('\n') + efile.write('(** Convert int to %s*)\n' % name[3:]) + efile.write('let %s_of_int x : %s =\n' % (name[3:],name[3:])) # strip Z3_ + efile.write(' match x with\n') + for k, i in sorted_decls: + efile.write(' | %d -> %s\n' % (i, k[3:])) + # use Z3.Exception? + efile.write(' | _ -> raise (Failure "undefined enum value")\n\n') + 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() + efile.close() + return z3consts_output_path + # efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w') + # efile.write('(* Automatically generated file *)\n\n') + # efile.write('(** The enumeration types of Z3. *)\n\n') + # for api_file in api_files: + # api_file_c = ml.find_file(api_file, ml.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.write('(** %s *)\n' % name[3:]) + # efile.write('type %s =\n' % name[3:]) # strip Z3_ + # for k, i in sorted(decls.items(), key=lambda pair: pair[1]): + # efile.write(' | %s \n' % k[3:]) # strip Z3_ + # efile.write('\n') + # efile.write('(** Convert %s to int*)\n' % name[3:]) + # efile.write('val int_of_%s : %s -> int\n' % (name[3:], name[3:])) # strip Z3_ + # efile.write('(** Convert int to %s*)\n' % name[3:]) + # efile.write('val %s_of_int : int -> %s\n' % (name[3:],name[3:])) # strip Z3_ + # efile.write('\n') + # 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() + # efile.close() + # if VERBOSE: + # print ('Generated "%s/z3enums.mli"' % ('%s' % gendir)) + ############################################################################### # Functions for generating a "module definition file" for MSVC diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 235453845..fd8962bda 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2870,7 +2870,8 @@ def mk_bindings(api_files): dotnet_output_dir=dotnet_output_dir, java_output_dir=java_output_dir, java_package_name=java_package_name, - ml_output_dir=ml_output_dir + ml_output_dir=ml_output_dir, + ml_src_dir=ml_output_dir ) cp_z3py_to_build() if is_ml_enabled(): @@ -2924,172 +2925,17 @@ def mk_z3consts_java(api_files): # Extract enumeration types from z3_api.h, and add ML definitions def mk_z3consts_ml(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("}.*;") - ml = get_component(ML_COMPONENT) - - DeprecatedEnums = [ 'Z3_search_failure' ] - gendir = ml.src_dir - if not os.path.exists(gendir): - os.mkdir(gendir) - - efile = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w') - efile.write('(* Automatically generated file *)\n\n') - efile.write('(** The enumeration types of Z3. *)\n\n') + full_path_api_files = [] for api_file in api_files: api_file_c = ml.find_file(api_file, ml.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.write('(** %s *)\n' % name[3:]) - efile.write('type %s =\n' % name[3:]) # strip Z3_ - for k, i in decls.items(): - efile.write(' | %s \n' % k[3:]) # strip Z3_ - efile.write('\n') - efile.write('(** Convert %s to int*)\n' % name[3:]) - efile.write('let int_of_%s x : int =\n' % (name[3:])) # strip Z3_ - efile.write(' match x with\n') - for k, i in decls.items(): - efile.write(' | %s -> %d\n' % (k[3:], i)) - efile.write('\n') - efile.write('(** Convert int to %s*)\n' % name[3:]) - efile.write('let %s_of_int x : %s =\n' % (name[3:],name[3:])) # strip Z3_ - efile.write(' match x with\n') - for k, i in decls.items(): - efile.write(' | %d -> %s\n' % (i, k[3:])) - # use Z3.Exception? - efile.write(' | _ -> raise (Failure "undefined enum value")\n\n') - 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() - efile.close() + full_path_api_files.append(api_file) + generated_file = mk_genfile_common.mk_z3consts_ml_internal( + full_path_api_files, + ml.src_dir) if VERBOSE: - print ('Generated "%s/z3enums.ml"' % ('%s' % gendir)) - # efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w') - # efile.write('(* Automatically generated file *)\n\n') - # efile.write('(** The enumeration types of Z3. *)\n\n') - # for api_file in api_files: - # api_file_c = ml.find_file(api_file, ml.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.write('(** %s *)\n' % name[3:]) - # efile.write('type %s =\n' % name[3:]) # strip Z3_ - # for k, i in decls.items(): - # efile.write(' | %s \n' % k[3:]) # strip Z3_ - # efile.write('\n') - # efile.write('(** Convert %s to int*)\n' % name[3:]) - # efile.write('val int_of_%s : %s -> int\n' % (name[3:], name[3:])) # strip Z3_ - # efile.write('(** Convert int to %s*)\n' % name[3:]) - # efile.write('val %s_of_int : int -> %s\n' % (name[3:],name[3:])) # strip Z3_ - # efile.write('\n') - # 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() - # efile.close() - # if VERBOSE: - # print ('Generated "%s/z3enums.mli"' % ('%s' % gendir)) + print ('Generated "%s"' % generated_file) def mk_gui_str(id): return '4D2F40D8-E5F9-473B-B548-%012d' % id diff --git a/scripts/update_api.py b/scripts/update_api.py index 3a3b2c40a..e531a103c 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1195,13 +1195,13 @@ def ml_alloc_and_store(t, lhs, rhs): alloc_str = '%s = caml_alloc_custom(&%s, sizeof(%s), 0, 1); ' % (lhs, pops, pts) return alloc_str + ml_set_wrap(t, lhs, rhs) -def mk_ml(ml_dir): +def mk_ml(ml_src_dir, ml_output_dir): global Type2Str - ml_nativef = os.path.join(ml_dir, 'z3native.ml') + ml_nativef = os.path.join(ml_output_dir, 'z3native.ml') ml_native = open(ml_nativef, 'w') ml_native.write('(* Automatically generated file *)\n\n') - ml_pref = open(os.path.join(ml_dir, 'z3native.ml.pre'), 'r') + ml_pref = open(os.path.join(ml_src_dir, 'z3native.ml.pre'), 'r') for s in ml_pref: ml_native.write(s); ml_pref.close() @@ -1250,14 +1250,14 @@ def mk_ml(ml_dir): if mk_util.is_verbose(): print ('Generated "%s"' % ml_nativef) - mk_z3native_stubs_c(ml_dir) + mk_z3native_stubs_c(ml_src_dir, ml_output_dir) -def mk_z3native_stubs_c(ml_dir): # C interface - ml_wrapperf = os.path.join(ml_dir, 'z3native_stubs.c') +def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface + ml_wrapperf = os.path.join(ml_output_dir, 'z3native_stubs.c') ml_wrapper = open(ml_wrapperf, 'w') ml_wrapper.write('// Automatically generated file\n\n') - ml_pref = open(os.path.join(ml_dir, 'z3native_stubs.c.pre'), 'r') + ml_pref = open(os.path.join(ml_src_dir, 'z3native_stubs.c.pre'), 'r') for s in ml_pref: ml_wrapper.write(s); ml_pref.close() @@ -1666,7 +1666,8 @@ def generate_files(api_files, dotnet_output_dir=None, java_output_dir=None, java_package_name=None, - ml_output_dir=None): + ml_output_dir=None, + ml_src_dir=None): """ Scan the api files in ``api_files`` and emit the relevant API files into the output directories specified. If an output directory is set to ``None`` @@ -1741,7 +1742,8 @@ def generate_files(api_files, mk_java(java_output_dir, java_package_name) if ml_output_dir: - mk_ml(ml_output_dir) + assert not ml_src_dir is None + mk_ml(ml_src_dir, ml_output_dir) def main(args): logging.basicConfig(level=logging.INFO) @@ -1768,6 +1770,10 @@ def main(args): dest="java_package_name", default=None, help="Name to give the Java package (e.g. ``com.microsoft.z3``).") + parser.add_argument("--ml-src-dir", + dest="ml_src_dir", + default=None, + help="Directory containing OCaml source files. If not specified no files are emitted") parser.add_argument("--ml-output-dir", dest="ml_output_dir", default=None, @@ -1779,6 +1785,11 @@ def main(args): logging.error('--java-package-name must be specified') return 1 + if pargs.ml_output_dir: + if pargs.ml_src_dir is None: + logging.error('--ml-src-dir must be specified') + return 1 + for api_file in pargs.api_files: if not os.path.exists(api_file): logging.error('"{}" does not exist'.format(api_file)) @@ -1790,7 +1801,8 @@ def main(args): dotnet_output_dir=pargs.dotnet_output_dir, java_output_dir=pargs.java_output_dir, java_package_name=pargs.java_package_name, - ml_output_dir=pargs.ml_output_dir) + ml_output_dir=pargs.ml_output_dir, + ml_src_dir=pargs.ml_src_dir) return 0 if __name__ == '__main__':