From c247abfc65ac33fdf4ffc3b95dc62eac1cd19e4a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Aug 2018 22:13:25 -0700 Subject: [PATCH] prepare js output Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 1 + scripts/mk_util.py | 49 ++++++++++++++++++++++++++++++++-- scripts/update_api.py | 62 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 110 insertions(+), 2 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index dada93069..05ca765e9 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -89,6 +89,7 @@ def init_project_def(): set_z3py_dir('api/python') add_python(_libz3Component) add_python_install(_libz3Component) + add_js() # Examples add_cpp_example('cpp_example', 'c++') add_cpp_example('z3_tptp', 'tptp') diff --git a/scripts/mk_util.py b/scripts/mk_util.py index d51735255..770e118ee 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -82,6 +82,7 @@ VS_ARM = False LINUX_X64 = True ONLY_MAKEFILES = False Z3PY_SRC_DIR=None +Z3JS_SRC_DIR=None VS_PROJ = False TRACE = False PYTHON_ENABLED=False @@ -89,6 +90,7 @@ DOTNET_ENABLED=False DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None) JAVA_ENABLED=False ML_ENABLED=False +JS_ENABLED=False PYTHON_INSTALL_ENABLED=False STATIC_LIB=False STATIC_BIN=False @@ -654,6 +656,7 @@ def display_help(exit_code): print(" --dotnet-key= sign the .NET assembly using the private key in .") print(" --java generate Java bindings.") print(" --ml generate OCaml bindings.") + print(" --js generate JScript bindings.") print(" --python generate Python bindings.") print(" --staticlib build Z3 static library.") print(" --staticbin build a statically linked Z3 binary.") @@ -687,14 +690,14 @@ def display_help(exit_code): # Parse configuration option for mk_make script def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM - global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED + global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, JS_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED global LINUX_X64, SLOW_OPTIMIZE, USE_OMP, LOG_SYNC global GUARD_CF, ALWAYS_DYNAMIC_BASE try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf', - 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', + 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js', 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin', 'log-sync']) except: print("ERROR: Invalid command line option") @@ -755,6 +758,8 @@ def parse_options(): GIT_DESCRIBE = True elif opt in ('', '--ml'): ML_ENABLED = True + elif opt == "--js": + JS_ENABLED = True elif opt in ('', '--noomp'): USE_OMP = False elif opt in ('', '--log-sync'): @@ -817,6 +822,16 @@ def set_build_dir(d): BUILD_DIR = norm_path(d) REV_BUILD_DIR = reverse_path(d) +def set_z3js_dir(p): + global SRC_DIR, Z3JS_SRC_DIR + p = norm_path(p) + full = os.path.join(SRC_DIR, p) + if not os.path.exists(full): + raise MKException("Python bindings directory '%s' does not exist" % full) + Z3JS_SRC_DIR = full + if VERBOSE: + print("Js bindings directory was detected.") + def set_z3py_dir(p): global SRC_DIR, Z3PY_SRC_DIR p = norm_path(p) @@ -852,6 +867,10 @@ def get_components(): def get_z3py_dir(): return Z3PY_SRC_DIR +# Return directory where the js bindings are located +def get_z3js_dir(): + return Z3JS_SRC_DIR + # Return true if in verbose mode def is_verbose(): return VERBOSE @@ -862,6 +881,9 @@ def is_java_enabled(): def is_ml_enabled(): return ML_ENABLED +def is_js_enabled(): + return JS_ENABLED + def is_dotnet_enabled(): return DOTNET_ENABLED @@ -1411,6 +1433,22 @@ class DLLComponent(Component): shutil.copy('%s.a' % os.path.join(build_path, self.dll_name), '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) +class JsComponent(Component): + def __init__(self): + Component.__init__(self, "js", None, []) + + def main_component(self): + return False + + def mk_win_dist(self, build_path, dist_path): + return + + def mk_unix_dist(self, build_path, dist_path): + return + + def mk_makefile(self, out): + return + class PythonComponent(Component): def __init__(self, name, libz3Component): assert isinstance(libz3Component, DLLComponent) @@ -2320,6 +2358,9 @@ def add_python(libz3Component): name = 'python' reg_component(name, PythonComponent(name, libz3Component)) +def add_js(): + reg_component('js', JsComponent()) + def add_python_install(libz3Component): name = 'python_install' reg_component(name, PythonInstallComponent(name, libz3Component)) @@ -2949,6 +2990,9 @@ def mk_bindings(api_files): ml_output_dir = None if is_ml_enabled(): ml_output_dir = get_component('ml').src_dir + if is_js_enabled(): + set_z3js_dir("api/js") + js_output_dir = get_component('js').src_dir # Get the update_api module to do the work for us update_api.generate_files(api_files=new_api_files, api_output_dir=get_component('api').src_dir, @@ -2956,6 +3000,7 @@ def mk_bindings(api_files): dotnet_output_dir=dotnet_output_dir, java_output_dir=java_output_dir, java_package_name=java_package_name, + js_output_dir=get_z3js_dir(), ml_output_dir=ml_output_dir, ml_src_dir=ml_output_dir ) diff --git a/scripts/update_api.py b/scripts/update_api.py index 375a855de..917df94a2 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -741,6 +741,59 @@ def mk_java(java_dir, package_name): if mk_util.is_verbose(): print("Generated '%s'" % java_nativef) + +Type2Napi = { VOID : '', VOID_PTR : '', INT : 'number', UINT : 'number', INT64 : 'number', UINT64 : 'number', DOUBLE : 'number', + FLOAT : 'number', STRING : 'string', STRING_PTR : 'array', + BOOL : 'number', SYMBOL : 'external', PRINT_MODE : 'number', ERROR_CODE : 'number' } + +def type2napi(t): + try: + return Type2Napi[t] + except: + return "external" + +Type2NapiBuilder = { VOID : '', VOID_PTR : '', INT : 'int32', UINT : 'uint32', INT64 : 'int64', UINT64 : 'uint64', DOUBLE : 'double', + FLOAT : 'float', STRING : 'string', STRING_PTR : 'array', + BOOL : 'bool', SYMBOL : 'external', PRINT_MODE : 'int32', ERROR_CODE : 'int32' } + +def type2napibuilder(t): + try: + return Type2NapiBuilder[t] + except: + return "external" + + +def mk_js(js_output_dir): + with open(os.path.join(js_output_dir, "z3.json"), 'w') as ous: + ous.write("{\n") + ous.write(" \"api\": [\n") + for name, result, params in _dotnet_decls: + ous.write(" {\n") + ous.write(" \"name\": \"%s\",\n" % name) + ous.write(" \"c_type\": \"%s\",\n" % Type2Str[result]) + ous.write(" \"napi_type\": \"%s\",\n" % type2napi(result)) + ous.write(" \"arg_list\": [") + first = True + for p in params: + if first: + first = False + ous.write("\n {\n") + else: + ous.write(",\n {\n") + t = param_type(p) + k = t + ous.write(" \"name\": \"%s\",\n" % "") # TBD + ous.write(" \"c_type\": \"%s\",\n" % type2str(t)) + ous.write(" \"napi_type\": \"%s\",\n" % type2napi(t)) + ous.write(" \"napi_builder\": \"%s\"\n" % type2napibuilder(t)) + ous.write( " }") + ous.write("],\n") + ous.write(" \"napi_builder\": \"%s\"\n" % type2napibuilder(result)) + ous.write(" },\n") + ous.write(" ]\n") + ous.write("}\n") + + def mk_log_header(file, name, params): file.write("void log_%s(" % name) i = 0 @@ -1742,6 +1795,7 @@ def generate_files(api_files, dotnet_output_dir=None, java_output_dir=None, java_package_name=None, + js_output_dir=None, ml_output_dir=None, ml_src_dir=None): """ @@ -1822,6 +1876,9 @@ def generate_files(api_files, assert not ml_src_dir is None mk_ml(ml_src_dir, ml_output_dir) + if js_output_dir: + mk_js(js_output_dir) + def main(args): logging.basicConfig(level=logging.INFO) parser = argparse.ArgumentParser(description=__doc__) @@ -1855,6 +1912,10 @@ def main(args): dest="ml_output_dir", default=None, help="Directory to emit OCaml files. If not specified no files are emitted.") + parser.add_argument("--js_output_dir", + dest="js_output_dir", + default=None, + help="Directory to emit js bindings. If not specified no files are emitted.") pargs = parser.parse_args(args) if pargs.java_output_dir: @@ -1878,6 +1939,7 @@ def main(args): dotnet_output_dir=pargs.dotnet_output_dir, java_output_dir=pargs.java_output_dir, java_package_name=pargs.java_package_name, + js_output_dir=pargs.js_output_dir, ml_output_dir=pargs.ml_output_dir, ml_src_dir=pargs.ml_src_dir) return 0