From 0e03fe9bf20859d4fc764e5e8ddc9c1bbec1ee4b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 21 Nov 2016 00:05:59 +0000 Subject: [PATCH 1/3] Fix inconsistent emission of OCaml enumeration files. The ordering of emitted enum values is not consistent between python 2 or 3. The root cause of the problem was a dictionary's keys being iterated over which has no defined order. This has been fixed by iterating over the dictionary's items and ordering by values. We could order by key rather than the values but seeing as these represent an enum, ordering by value makes more sense. --- scripts/mk_util.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 235453845..a5440946c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2986,21 +2986,22 @@ def mk_z3consts_ml(api_files): 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 decls.items(): + 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 decls.items(): + 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 decls.items(): + 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') @@ -3068,7 +3069,7 @@ def mk_z3consts_ml(api_files): # 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(): + # 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:]) From 76bbecf4fe3232bbc67e7d1d06a6f9cdf5a8dc85 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 21 Nov 2016 00:45:43 +0000 Subject: [PATCH 2/3] Refactor `mk_z3consts_ml()` code into `mk_z3consts_ml_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 | 174 +++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 168 ++------------------------------- 3 files changed, 190 insertions(+), 162 deletions(-) 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 a5440946c..d644b269c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2924,173 +2924,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: - 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() + 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 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)) + print ('Generated "%s"' % generated_file) def mk_gui_str(id): return '4D2F40D8-E5F9-473B-B548-%012d' % id From 2e74a2c54e5935cdd1c8678d3a0641e7132da023 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 21 Nov 2016 01:04:55 +0000 Subject: [PATCH 3/3] Refactor `update_api.mk_ml()` so that the source and output directories can be different. This feature will be needed by the CMake build system to build the OCaml bindings. --- scripts/mk_util.py | 3 ++- scripts/update_api.py | 32 ++++++++++++++++++++++---------- 2 files changed, 24 insertions(+), 11 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index d644b269c..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(): 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__':