mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Merge pull request #797 from delcypher/refactor_ocaml_generated_files

Browse source 
Refactor OCaml generated file generation in preparation for CMake support
This commit is contained in:
Christoph M. Wintersteiger 2017-01-05 12:39:06 +01:00 committed by GitHub
parent f443bfed87 2e74a2c54e
commit 447c97a783
4 changed files with 214 additions and 172 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
scripts/mk_consts_files.py
View file

@ -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')

174
scripts/mk_genfile_common.py
View file

@ -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

170
scripts/mk_util.py
View file

@ -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

32
scripts/update_api.py
View file

@ -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__':