From 9c579565d498c9f4a50ffb04affea4b46a372893 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 20 Nov 2012 22:37:42 -0800
Subject: [PATCH] Starting automatic generation of JNI bindings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
scripts/mk_project.py | 1 +
scripts/mk_util.py | 58 ++++++++++++++++++++++++++----------
scripts/update_api.py | 69 +++++++++++++++++++++++++++++++++++++++++++
3 files changed, 113 insertions(+), 15 deletions(-)
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 4ef6efd11..acf964589 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -71,6 +71,7 @@ def init_project_def():
static=build_static_lib(),
export_files=API_files)
add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
+ add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3j')
add_hlib('cpp', 'api/c++', includes2install=['z3++.h'])
set_z3py_dir('api/python')
# Examples
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index c91db090e..b1a12b733 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -59,6 +59,7 @@ Z3PY_SRC_DIR=None
VS_PROJ = False
TRACE = False
DOTNET_ENABLED=False
+JAVA_ENABLED=False
STATIC_LIB=False
VER_MAJOR=None
VER_MINOR=None
@@ -264,26 +265,29 @@ def display_help():
print " -v, --vsproj generate Visual Studio Project Files."
print " -t, --trace enable tracing in release mode."
print " -n, --nodotnet do not generate Microsoft.Z3.dll make rules."
+ print " -j, --java generate Java bindinds."
print " --staticlib build Z3 static library."
exit(0)
# 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, DOTNET_ENABLED, STATIC_LIB, PREFIX, GMP
- options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:dsxhmcvtnp:g', ['build=',
- 'debug',
- 'silent',
- 'x64',
- 'help',
- 'makefiles',
- 'showcpp',
- 'vsproj',
- 'trace',
- 'nodotnet',
- 'staticlib',
- 'prefix=',
- 'gmp'
- ])
+ global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE
+ global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP
+ options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:dsxhmcvtnp:gj', ['build=',
+ 'debug',
+ 'silent',
+ 'x64',
+ 'help',
+ 'makefiles',
+ 'showcpp',
+ 'vsproj',
+ 'trace',
+ 'nodotnet',
+ 'staticlib',
+ 'prefix=',
+ 'gmp',
+ 'java'
+ ])
for opt, arg in options:
if opt in ('-b', '--build'):
if arg == 'src':
@@ -315,6 +319,8 @@ def parse_options():
PREFIX = arg
elif opt in ('-g', '--gmp'):
GMP = True
+ elif opt in ('-j', '--java'):
+ JAVA_ENABLED = True
else:
raise MKException("Invalid command line option '%s'" % opt)
@@ -396,6 +402,9 @@ def get_z3py_dir():
def is_verbose():
return VERBOSE
+def is_java_enabled():
+ return JAVA_ENABLED
+
def get_cpp_files(path):
return filter(lambda f: f.endswith('.cpp'), os.listdir(path))
@@ -832,6 +841,21 @@ class DotNetDLLComponent(Component):
shutil.copy('%s/%s.dll' % (build_path, self.dll_name),
'%s/bin/%s.dll' % (dist_path, self.dll_name))
+
+class JavaDLLComponent(Component):
+ def __init__(self, name, dll_name, path, deps):
+ Component.__init__(self, name, path, deps)
+ if dll_name == None:
+ dll_name = name
+ self.dll_name = dll_name
+
+ def mk_makefile(self, out):
+ return
+
+ def main_component(self):
+ return JAVA_ENABLED
+
+
class ExampleComponent(Component):
def __init__(self, name, path):
Component.__init__(self, name, path, [])
@@ -965,6 +989,10 @@ def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=N
c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir)
reg_component(name, c)
+def add_java_dll(name, deps=[], path=None, dll_name=None):
+ c = JavaDLLComponent(name, dll_name, path, deps)
+ reg_component(name, c)
+
def add_cpp_example(name, path=None):
c = CppExampleComponent(name, path)
reg_component(name, c)
diff --git a/scripts/update_api.py b/scripts/update_api.py
index e7d3ddb19..89c7ab74d 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -132,6 +132,11 @@ Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint',
STRING : 'string', STRING_PTR : 'byte**', BOOL : 'int', SYMBOL : 'IntPtr',
PRINT_MODE : 'uint', ERROR_CODE : 'uint' }
+# Mapping to Java types
+Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double',
+ STRING : 'String', STRING_PTR : 'StringPtr',
+ BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int' }
+
next_type_id = FIRST_OBJ_ID
def def_Type(var, c_type, py_type):
@@ -165,6 +170,13 @@ def type2dotnet(ty):
global Type2Dotnet
return Type2Dotnet[ty]
+def type2java(ty):
+ global Type2Java
+ if (ty >= FIRST_OBJ_ID):
+ return 'long'
+ else:
+ return Type2Java[ty]
+
def _in(ty):
return (IN, ty);
@@ -224,6 +236,20 @@ def param2dotnet(p):
else:
return type2dotnet(param_type(p))
+def param2java(p):
+ k = param_kind(p)
+ if k == OUT:
+ if param_type(p) == INT or param_type(p) == UINT:
+ return "IntPtr"
+ elif param_type(p) == INT64 or param_type(p) == UINT64:
+ return "LongPtr"
+ else:
+ return "long" # ?
+ if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
+ return "%s[]" % type2java(param_type(p))
+ else:
+ return type2java(param_type(p))
+
def param2pystr(p):
if param_kind(p) == IN_ARRAY or param_kind(p) == OUT_ARRAY or param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT:
return "ctypes.POINTER(%s)" % type2pystr(param_type(p))
@@ -399,6 +425,48 @@ def mk_dotnet_wrappers():
dotnet.write(" }\n\n")
dotnet.write("}\n\n")
+def java_method_name(name):
+ result = ''
+ name = name[3:] # Remove Z3_
+ n = len(name)
+ i = 0
+ while i < n:
+ if name[i] == '_':
+ i = i + 1
+ if i < n:
+ result += name[i].upper()
+ else:
+ result += name[i]
+ i = i + 1
+ return result
+
+def mk_java():
+ if not is_java_enabled():
+ return
+ java_dir = get_component('java').src_dir
+ java_nativef = '%s/Z3Native.java' % java_dir
+ java_wrapperf = '%s/Z3Native.c' % java_dir
+ java_native = open(java_nativef, 'w')
+ java_native.write('public final class Z3Native {\n')
+ java_native.write('public static class IntPtr { public int value; }\n')
+ java_native.write('public static class LongPtr { public long value; }\n')
+ java_native.write('public static class StringPtr { public String value; }\n')
+ for name, result, params in _dotnet_decls:
+ java_native.write(' public static native %s %s(' % (type2java(result), java_method_name(name)))
+ first = True
+ i = 0;
+ for param in params:
+ if first:
+ first = False
+ else:
+ java_native.write(', ')
+ java_native.write('%s a%d' % (param2java(param), i))
+ i = i + 1
+ java_native.write(');\n')
+ java_native.write('}\n');
+ if is_verbose():
+ print "Generated '%s'" % java_nativef
+
def mk_log_header(file, name, params):
file.write("void log_%s(" % name)
i = 0
@@ -668,6 +736,7 @@ mk_bindings()
mk_py_wrappers()
mk_dotnet()
mk_dotnet_wrappers()
+mk_java()
log_h.close()
log_c.close()