mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

prepare js output

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-08-03 22:13:25 -07:00
parent 51610842b9
commit c247abfc65
3 changed files with 110 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
scripts/mk_project.py
View file

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

49
scripts/mk_util.py
View file

@ -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=<file> sign the .NET assembly using the private key in <file>.")
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
)

62
scripts/update_api.py
View file

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