Java API: added correct error handling.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

scripts/update_api.py

@@ -494,12 +494,12 @@ def mk_java():
     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')
-    java_native.write('  public static class errorHandler { public long ptr; }\n')
+    java_native.write('  public static native void setInternalErrorHandler(long ctx);\n\n')
     if IS_WINDOWS:
         java_native.write('  static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name)
     else:
         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
-    java_native.write('\n\n')
+    java_native.write('\n')
     for name, result, params in _dotnet_decls:
         java_native.write('  protected static native %s INTERNAL%s(' % (type2java(result), java_method_name(name)))
         first = True
@@ -553,6 +553,7 @@ def mk_java():
         java_native.write('  }\n\n')
     java_native.write('}\n')
     java_wrapper = open(java_wrapperf, 'w')
+    pkg_str = get_component('java').package_name.replace('.', '_')
     java_wrapper.write('// Automatically generated file\n')
     java_wrapper.write('#include<jni.h>\n')
     java_wrapper.write('#include<stdlib.h>\n')
@@ -578,7 +579,17 @@ def mk_java():
     java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW)                                 \\\n')
     java_wrapper.write('  delete [] NEW;                                                     \n\n')
     java_wrapper.write('#endif\n\n')
-    pkg_str = get_component('java').package_name.replace('.', '_')
+    java_wrapper.write('void Z3JavaErrorHandler(Z3_context c, Z3_error_code e)\n')
+    java_wrapper.write('{\n')
+    java_wrapper.write('  // Internal do-nothing error handler. This is required to avoid that Z3 calls exit()\n')
+    java_wrapper.write('  // upon errors, but the actual error handling is done by throwing exceptions in the\n')
+    java_wrapper.write('  // wrappers below.\n')
+    java_wrapper.write('}\n\n')
+    java_wrapper.write('JNIEXPORT void JNICALL Java_%s_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, long a0)\n' % pkg_str)
+    java_wrapper.write('{\n')
+    java_wrapper.write('  Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler);\n')
+    java_wrapper.write('}\n\n')
+    java_wrapper.write('')
     for name, result, params in _dotnet_decls:
         java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name)))
         i = 0;

src/api/java/Context.java

@@ -38,12 +38,11 @@ public class Context extends IDisposable
         InitContext();
     }
 
-    private Context(long ctx, long refCount, Native.errorHandler errh)
+    private Context(long ctx, long refCount)
     {
         super();
         this.m_ctx = ctx;
         this.m_refCount = refCount;
-        this.m_n_err_handler = errh;
     }
 
     /**
@@ -2908,21 +2907,6 @@ public class Context extends IDisposable
         Native.toggleWarningMessages((enabled) ? true : false);
     }
 
-    // /// <summary>
-    // /// A delegate which is executed when an error is raised.
-    // /// </summary>
-    // /// <remarks>
-    // /// Note that it is possible for memory leaks to occur if error handlers
-    // /// throw exceptions.
-    // /// </remarks>
-    // public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode,
-    // String errorString);
-
-    // /// <summary>
-    // /// The OnError event.
-    // /// </summary>
-    // public event ErrorHandler OnError = null;
-
     /**
      * Update a mutable configuration parameter. <remarks> The list of all
      * configuration parameters can be obtained using the Z3 executable:
@@ -2950,26 +2934,16 @@ public class Context extends IDisposable
     }
 
     long m_ctx = 0;
-    Native.errorHandler m_n_err_handler = null;
 
     long nCtx()
     {
         return m_ctx;
     }
 
-    // void NativeErrorHandler(long ctx, Z3_error_code errorCode)
-    // {
-    // // Do-nothing error handler. The wrappers in Z3.Native will throw
-    // exceptions upon errors.
-    // }
-
     void InitContext() throws Z3Exception
     {
         setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
-        // m_n_err_handler = new Native.errorHandler(NativeErrorHandler); //
+	Native.setInternalErrorHandler(nCtx());
-        // keep reference so it doesn't get collected.
-        // if (m_n_err_handler != null) Native.setErrorHandler(m_ctx,
-        // m_n_err_handler);
     }
 
     void CheckContextMatch(Z3Object other) throws Z3Exception
@@ -3087,7 +3061,6 @@ public class Context extends IDisposable
 
         if (m_refCount == 0)
         {
-            m_n_err_handler = null;
             try
             {
                 Native.delContext(m_ctx);
@@ -3099,7 +3072,7 @@ public class Context extends IDisposable
         } else
             /* re-queue the finalizer */
             /* BUG: DRQ's need to be taken over too! */
-            new Context(m_ctx, m_refCount, m_n_err_handler);
+            new Context(m_ctx, m_refCount);
     }
 
     /**