From 8bc7d319c7ec1e5e3421a791e9c985db7433bf26 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 2 Mar 2016 11:59:48 +0000 Subject: [PATCH] Refactor ``mk_z3consts_py()`` to that is usable externally via a new function ``mk_z3consts_py_internal()`` which called by a new ``mk_consts_files.py`` script. This will script will allow the const declarations for the different Z3 language bindings to be generated. Right now only support for python is implemented but more can be added in the future. --- scripts/mk_consts_files.py | 47 ++++++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 20 ++++++++++------ 2 files changed, 60 insertions(+), 7 deletions(-) create mode 100755 scripts/mk_consts_files.py diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py new file mode 100755 index 000000000..543c56e0e --- /dev/null +++ b/scripts/mk_consts_files.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python +""" +Reads a list of Z3 API header files and +generate the constant declarations need +by one or more Z3 language bindings +""" +import mk_util +import argparse +import logging +import os +import sys + +def check_dir(output_dir): + if not os.path.isdir(output_dir): + logging.error('"{}" is not an existing directory'.format(output_dir)) + return 1 + return 0 + +def main(args): + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("api_files", nargs="+") + parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None) + pargs = parser.parse_args(args) + + for api_file in pargs.api_files: + if not os.path.exists(api_file): + logging.error('"{}" does not exist'.format(api_file)) + return 1 + + count = 0 + + if pargs.z3py_output_dir: + if check_dir(pargs.z3py_output_dir) != 0: + return 1 + mk_util.mk_z3consts_py_internal(pargs.api_files, pargs.z3py_output_dir) + count += 1 + + if count == 0: + logging.info('No files generated. You need to specific an output directory' + ' for the relevant langauge bindings') + # TODO: Add support for other bindings + return 0 + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:])) + diff --git a/scripts/mk_util.py b/scripts/mk_util.py index f7a51b4da..56726b1cc 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2999,6 +2999,17 @@ def mk_bindings(api_files): def mk_z3consts_py(api_files): if Z3PY_SRC_DIR is None: raise MKException("You must invoke set_z3py_dir(path):") + full_path_api_files = [] + api_dll = get_component(Z3_DLL_COMPONENT) + for api_file in api_files: + api_file_c = api_dll.find_file(api_file, api_dll.name) + api_file = os.path.join(api_file_c.src_dir, api_file) + full_path_api_files.append(api_file) + mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR) + +def mk_z3consts_py_internal(api_files, output_dir): + assert os.path.isdir(output_dir) + assert isinstance(api_files, list) blank_pat = re.compile("^ *\r?$") comment_pat = re.compile("^ *//.*$") @@ -3007,14 +3018,9 @@ def mk_z3consts_py(api_files): openbrace_pat = re.compile("{ *") closebrace_pat = re.compile("}.*;") - z3consts = open(os.path.join(Z3PY_SRC_DIR, 'z3consts.py'), 'w') + z3consts = open(os.path.join(output_dir, 'z3consts.py'), 'w') z3consts.write('# Automatically generated file\n\n') - - api_dll = get_component(Z3_DLL_COMPONENT) - for api_file in api_files: - api_file_c = api_dll.find_file(api_file, api_dll.name) - api_file = os.path.join(api_file_c.src_dir, api_file) api = open(api_file, 'r') SEARCHING = 0 @@ -3075,7 +3081,7 @@ def mk_z3consts_py(api_files): api.close() z3consts.close() if VERBOSE: - print("Generated '%s'" % os.path.join(Z3PY_SRC_DIR, 'z3consts.py')) + print("Generated '%s'" % os.path.join(output_dir, 'z3consts.py')) # Extract enumeration types from z3_api.h, and add .Net definitions