working on JNI bindings

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

scripts/mk_project.py

@@ -71,7 +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_java_dll('java', 'api/java', dll_name='libz3j')
     add_hlib('cpp', 'api/c++', includes2install=['z3++.h'])
     set_z3py_dir('api/python')
     # Examples

scripts/mk_util.py

@@ -22,6 +22,7 @@ from fnmatch import fnmatch
 import distutils.sysconfig
 import compileall
 import subprocess
+import string
 
 def getenv(name, default):
     try:
@@ -36,7 +37,6 @@ CXXFLAGS=getenv("CXXFLAGS", "")
 LDFLAGS=getenv("LDFLAGS", "")
 JAVA=getenv("JAVA", "java")
 JAVAC=getenv("JAVAC", "javac")
-JAVAH=getenv("JAVAH", "javah")
 
 CXX_COMPILERS=['g++', 'clang++']
 C_COMPILERS=['gcc', 'clang']
@@ -71,6 +71,7 @@ VER_BUILD=None
 VER_REVISION=None
 PREFIX='/usr'
 GMP=False
+JAVA_HOME=None
 
 def which(program):
     import os
@@ -185,15 +186,34 @@ def check_java():
     r = exec_cmd([JAVAC, 'Z3Native.java'])
     if r != 0:
         raise MKException('Failed testing Java compiler (for source containing JNI bindings). Set environment variable JAVAC with the path to the Java compiler')
+    find_java_home()
+
+def find_java_home():
+    global JAVA_HOME
     if is_verbose():
-        print "Testing %s..." % JAVAH
+        print "Finding JAVA_HOME..."
-    r = exec_cmd([JAVAH, 'Z3Native'])
+    t = TempFile('output')
-    if not os.path.exists('Z3Native.h'):
+    null = open(os.devnull, 'wb')
-        r = 1
+    try: 
-    rmf('Z3Native.h')
+        subprocess.call([JAVA, '-verbose'], stdout=t.fname, stderr=null)
-    rmf('Z3Native.class')
+        t.commit()
-    if r != 0:
+    except:
-        raise MKException('Failed testing Java JNI Header file generator. Set environment variable JAVAH with the path to the Java JNI header file generator')
+        raise MKException('Failed to find JAVA_HOME')
+    open_pat     = re.compile("\[Opened (.*)\]")
+    t = open('output', 'r')
+    for line in t:
+        m = open_pat.match(line)
+        if m:
+            # Remove last 3 directives from m.group(1)
+            tmp  = m.group(1).split(os.sep)
+            path = string.join(tmp[:len(tmp) - 3], os.sep)
+            if is_verbose():
+                print "Checking jni.h..."
+            if not os.path.exists('%s/include/jni.h' % path):
+                raise MKException("Failed to detect jni.h at '%s/include'" % path)
+            JAVA_HOME = path
+            return
+    raise MKException('Failed to find JAVA_HOME')
 
 def is64():
     return sys.maxsize >= 2**32
@@ -315,13 +335,12 @@ def display_help(exit_code):
         print ""
         print "Some influential environment variables:"
         print "  CXX        C++ compiler"
-        print "  CC         C compiler (only used for compiling examples)"
+        print "  CC         C compiler"
         print "  LDFLAGS    Linker flags, e.g., -L<lib dir> if you have libraries in a non-standard directory"
         print "  CPPFLAGS   Preprocessor flags, e.g., -I<include dir> if you have header files in a non-standard directory"
         print "  CXXFLAGS   C++ compiler flags"
         print "  JAVA       Java virtual machine (only relevant if -j or --java option is provided)"
         print "  JAVAC      Java compiler (only relevant if -j or --java option is provided)"
-        print "  JAVAH      Java H file generator for JNI bindinds (only relevant if -j or --java option is provided)"
     exit(exit_code)
 
 # Parse configuration option for mk_make script
@@ -892,17 +911,24 @@ class DotNetDLLComponent(Component):
 
 
 class JavaDLLComponent(Component):
-    def __init__(self, name, dll_name, path, deps):
+    def __init__(self, name, dll_name, path):
-        Component.__init__(self, name, path, deps)
+        Component.__init__(self, name, path, [])
         if dll_name == None:
             dll_name = name
         self.dll_name          = dll_name
 
     def mk_makefile(self, out):
-        return
+        if is_java_enabled():
+            dllfile = '%s$(SO_EXT)' % self.dll_name
+            out.write('%s: %s/Z3Native.java %s$(SO_EXT)\n' % (dllfile, self.to_src_dir, get_component('api_dll').dll_name))
+            out.write('\tcd %s; %s Z3Native.java\n' % (self.to_src_dir, JAVAC))
+            out.write('\tmv %s/*.class .\n' % self.to_src_dir)
+            out.write('\t$(CC) $(CXXFLAGS) $(CXX_OUT_FLAG)Z3Native$(OBJ_EXT) -I%s/include -I%s %s/Z3Native.c\n' % (JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir))
+            out.write('\t$(CC) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) -L. Z3Native$(OBJ_EXT) -lz3\n' % dllfile)
+            out.write('%s: %s\n\n' % (self.name, dllfile))
     
     def main_component(self):
-        return JAVA_ENABLED
+        return is_java_enabled()
 
 
 class ExampleComponent(Component):
@@ -1038,8 +1064,8 @@ 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):
+def add_java_dll(name, path=None, dll_name=None):
-    c = JavaDLLComponent(name, dll_name, path, deps)
+    c = JavaDLLComponent(name, dll_name, path)
     reg_component(name, c)
 
 def add_cpp_example(name, path=None):
@@ -1202,9 +1228,9 @@ def mk_config():
             print 'Prefix:         %s' % PREFIX
             print '64-bit:         %s' % is64()
             if is_java_enabled():
+                print 'Java Home:      %s' % JAVA_HOME
                 print 'Java Compiler:  %s' % JAVAC
                 print 'Java VM:        %s' % JAVA
-                print 'Java H gen.:    %s' % JAVAH
 
 def mk_install(out):
     out.write('install:\n')

scripts/update_api.py

@@ -137,6 +137,11 @@ Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64
               STRING : 'String', STRING_PTR : 'StringPtr', 
               BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int' }
 
+Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble',
+               STRING : 'jstring', STRING_PTR : 'jobject',
+               BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint' }
+
+
 next_type_id = FIRST_OBJ_ID
 
 def def_Type(var, c_type, py_type):
@@ -177,6 +182,13 @@ def type2java(ty):
     else:
         return Type2Java[ty]
 
+def type2javaw(ty):
+    global Type2JavaW
+    if (ty >= FIRST_OBJ_ID):
+        return 'jlong'
+    else:
+        return Type2JavaW[ty]
+
 def _in(ty):
     return (IN, ty);
 
@@ -241,15 +253,31 @@ def param2java(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:
+        elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID:
             return "LongPtr"
+        elif param_type(p) == STRING:
+            return "StringPtr"
         else:
-            return "long" # ? 
+            print "ERROR: unreachable code"
+            assert(False)
+            exit(1)
     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 param2javaw(p):
+    k = param_kind(p)
+    if k == OUT:
+        return "jobject"
+    if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
+        if param_type(p) == INT or param_type(p) == UINT:
+            return "jintArray"
+        else:
+            return "jlongArray"
+    else:
+        return type2javaw(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))
@@ -440,6 +468,30 @@ def java_method_name(name):
         i = i + 1
     return result
 
+# Return the Java method name used to retrieve the elements of the given parameter
+def java_get_array_elements(p):
+    if param_type(p) == INT or param_type(p) == UINT:
+        return 'GetIntArrayElements'
+    else:
+        return 'GetLongArrayElements'
+# Return the Java method name used to release the elements of the given parameter
+def java_release_array_elements(p):
+    if param_type(p) == INT or param_type(p) == UINT:
+        return 'ReleaseIntArrayElements'
+    else:
+        return 'ReleaseLongArrayElements'
+# Return the type of the java array elements
+def java_array_element_type(p):
+    if param_type(p) == INT or param_type(p) == UINT:
+        return 'jint'
+    else:
+        return 'jlong'
+def java_set_array_region(p):
+    if param_type(p) == INT or param_type(p) == UINT:
+        return 'SetIntArrayRegion'
+    else:
+        return 'SetLongArrayRegion'
+
 def mk_java():
     if not is_java_enabled():
         return
@@ -447,12 +499,14 @@ def mk_java():
     java_nativef  = '%s/Z3Native.java' % java_dir
     java_wrapperf = '%s/Z3Native.c' % java_dir 
     java_native   = open(java_nativef, 'w')
+    java_native.write('// Automatically generated file\n')
     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 IntPtr { public int value; }\n')
-    java_native.write('public static class LongPtr { public long value; }\n')
+    java_native.write('  public static class LongPtr { public long value; }\n')
-    java_native.write('public static class StringPtr { public String value; }\n')
+    java_native.write('  public static class StringPtr { public String value; }\n')
+    java_native.write('  static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name
     for name, result, params in _dotnet_decls:
-        java_native.write('        public static native %s %s(' % (type2java(result), java_method_name(name)))
+        java_native.write('  public static native %s %s(' % (type2java(result), java_method_name(name)))
         first = True
         i = 0;
         for param in params:
@@ -463,7 +517,105 @@ def mk_java():
             java_native.write('%s a%d' % (param2java(param), i))
             i = i + 1
         java_native.write(');\n')
+    java_native.write('  public static void main(String[] args) {\n')
+    java_native.write('     IntPtr major = new IntPtr(), minor = new IntPtr(), build = new IntPtr(), revision = new IntPtr();\n')
+    java_native.write('     getVersion(major, minor, build, revision);\n')
+    java_native.write('     System.out.format("Z3 (for Java) %d.%d.%d%n", major.value, minor.value, build.value);\n')
+    java_native.write('  }\n')
     java_native.write('}\n');
+    java_wrapper = open(java_wrapperf, 'w')
+    java_wrapper.write('// Automatically generated file\n')
+    java_wrapper.write('#include<jni.h>\n')
+    java_wrapper.write('#include<stdlib.h>\n')
+    java_wrapper.write('#include"z3.h"\n')
+    for name, result, params in _dotnet_decls:
+        java_wrapper.write('JNIEXPORT %s JNICALL Java_Z3Native_%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), java_method_name(name)))
+        i = 0;
+        for param in params:
+            java_wrapper.write(', ')
+            java_wrapper.write('%s a%d' % (param2javaw(param), i))
+            i = i + 1
+        java_wrapper.write(') {\n')
+        # preprocess arrays, strings, in/out arguments
+        i = 0
+        for param in params:
+            k = param_kind(param)
+            if k == OUT or k == INOUT:
+                java_wrapper.write('  %s _a%s;\n' % (type2str(param_type(param)), i))
+            elif k == IN_ARRAY or k == INOUT_ARRAY:
+                java_wrapper.write('  %s * _a%s = (%s *) (*jenv)->%s(jenv, a%s, NULL);\n' % (type2str(param_type(param)),
+                                                                                             i,
+                                                                                             type2str(param_type(param)),
+                                                                                             java_get_array_elements(param),
+                                                                                             i))
+            elif k == OUT_ARRAY:
+                java_wrapper.write('  %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)), 
+                                                                                                     i, 
+                                                                                                     type2str(param_type(param)), 
+                                                                                                     param_array_capacity_pos(param), 
+                                                                                                     type2str(param_type(param))))
+            elif k == IN and param_type(param) == STRING:
+                java_wrapper.write('  Z3_string _a%s = (Z3_string) (*jenv)->GetStringUTFChars(jenv, a%s, NULL);\n' % (i, i))
+            i = i + 1
+        # invoke procedure
+        java_wrapper.write('  ')
+        if result != VOID:
+            java_wrapper.write('%s result = ' % type2str(result))
+        java_wrapper.write('%s(' % name)
+        i = 0
+        first = True
+        for param in params:
+            if first:
+                first = False
+            else:
+                java_wrapper.write(', ')
+            k = param_kind(param)
+            if k == OUT or k == INOUT:
+                java_wrapper.write('&_a%s' % i)
+            elif k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY:
+                java_wrapper.write('_a%s' % i)
+            elif k == IN and param_type(param) == STRING:
+                java_wrapper.write('_a%s' % i)
+            else:
+                java_wrapper.write('(%s)a%i' % (param2str(param), i))
+            i = i + 1
+        java_wrapper.write(');\n')
+        # cleanup 
+        i = 0
+        for param in params:
+            k = param_kind(param)
+            if k == OUT_ARRAY:
+                java_wrapper.write('  (*jenv)->%s(jenv, a%s, 0, (jsize)a%s, (%s *) _a%s);\n' % (java_set_array_region(param),
+                                                                                                i,
+                                                                                                param_array_capacity_pos(param),
+                                                                                                java_array_element_type(param),
+                                                                                                i))
+                java_wrapper.write('  free(_a%s);\n' % i)
+            elif k == IN_ARRAY or k == OUT_ARRAY:
+                java_wrapper.write('  (*jenv)->%s(jenv, a%s, (%s *) _a%s, JNI_ABORT);\n' % (java_release_array_elements(param), 
+                                                                                            i, 
+                                                                                            java_array_element_type(param),
+                                                                                            i))
+            elif k == OUT or k == INOUT:
+                if param_type(param) == INT or param_type(param) == UINT:
+                    java_wrapper.write('  {\n')
+                    java_wrapper.write('     jclass mc    = (*jenv)->GetObjectClass(jenv, a%s);\n' % i)
+                    java_wrapper.write('     jfieldID fid = (*jenv)->GetFieldID(jenv, mc, "value", "I");\n')
+                    java_wrapper.write('     (*jenv)->SetIntField(jenv, a%s, fid, (jint) _a%s);\n' % (i, i))
+                    java_wrapper.write('  }\n')
+                else:
+                    java_wrapper.write('  {\n')
+                    java_wrapper.write('     jclass mc    = (*jenv)->GetObjectClass(jenv, a%s);\n' % i)
+                    java_wrapper.write('     jfieldID fid = (*jenv)->GetFieldID(jenv, mc, "value", "J");\n')
+                    java_wrapper.write('     (*jenv)->SetLongField(jenv, a%s, fid, (jlong) _a%s);\n' % (i, i))
+                    java_wrapper.write('  }\n')
+            i = i + 1
+        # return
+        if result == STRING:
+            java_wrapper.write('  return (*jenv)->NewStringUTF(jenv, result);\n')
+        elif result != VOID:
+            java_wrapper.write('  return (%s) result;\n' % type2javaw(result))
+        java_wrapper.write('}\n')
     if is_verbose():
         print "Generated '%s'" % java_nativef
 

src/api/z3_api.h

@@ -1860,7 +1860,7 @@ BEGIN_MLAPI_EXCLUDE
        \param c logical context.
        \param num_sorts number of datatype sorts.
        \param sort_names names of datatype sorts.
-       \param sorts array of datattype sorts.
+       \param sorts array of datatype sorts.
        \param constructor_lists list of constructors, one list per sort.
 
        def_API('Z3_mk_datatypes', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, SYMBOL), _out_array(1, SORT), _inout_array(1, CONSTRUCTOR_LIST)))