mirror of
https://github.com/Z3Prover/z3
synced 2025-04-26 18:45:33 +00:00
Starting automatic generation of JNI bindings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
e22805c139
commit
9c579565d4
3 changed files with 113 additions and 15 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue