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()