Fix Java destruction order issue; thanks to Zheng Manchun for reporting this bug.

2 files changed, 61 insertions, 0 deletions

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 8e601a396..6fb802497 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -2,6 +2,27 @@
 #include "expr/expr_manager.h"
 %}
 
+%typemap(javacode) CVC4::ExprManager %{
+  // a ref is kept here to keep Java GC from collecting the Options
+  // before the ExprManager
+  private Object options;
+%}
+%typemap(javaconstruct) ExprManager(Options options) {
+    this($imcall, true);
+    this.options = SmtEngine.mkRef(options); // keep ref to options in SWIG proxy class
+  }
+%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::ExprManager {
+    SmtEngine.dlRef(options);
+    options = null;
+    if (swigCPtr != 0) {
+      if (swigCMemOwn) {
+        swigCMemOwn = false;
+        CVC4JNI.delete_SmtEngine(swigCPtr);
+      }
+      swigCPtr = 0;
+    }
+  }
+
 #ifdef SWIGOCAML
   /* OCaml bindings cannot deal with this degree of overloading */
   %ignore CVC4::ExprManager::mkExpr(Kind, const std::vector<Expr>&);
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index c326d95d3..5d59cae61 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -2,6 +2,46 @@
 #include "smt/smt_engine.h"
 %}
 
+%typemap(javacode) CVC4::SmtEngine %{
+  // a ref is kept here to keep Java GC from collecting the EM
+  // before the SmtEngine
+  private Object emRef;
+  static final native Object mkRef(Object obj);
+  static final native void dlRef(Object obj);
+%}
+%native (mkRef) jobject SmtEngine::mkRef(jobject);
+%native (dlRef) void SmtEngine::dlRef(jobject);
+%{
+extern "C" {
+SWIGEXPORT jobject JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_mkRef(JNIEnv* jenv, jclass jcls, jobject o) {
+  if(o == NULL) {
+    return NULL;
+  }
+  return jenv->NewGlobalRef(o);
+}
+SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jclass jcls, jobject o) {
+  if(o != NULL) {
+    jenv->DeleteGlobalRef(o);
+  }
+}
+}
+%}
+%typemap(javaconstruct) SmtEngine(ExprManager em) {
+    this($imcall, true);
+    emRef = mkRef(em); // keep ref to expr manager in SWIG proxy class
+  }
+%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::SmtEngine {
+    dlRef(emRef);
+    emRef = null;
+    if (swigCPtr != 0) {
+      if (swigCMemOwn) {
+        swigCMemOwn = false;
+        CVC4JNI.delete_SmtEngine(swigCPtr);
+      }
+      swigCPtr = 0;
+    }
+  }
+
 %ignore CVC4::SmtEngine::setLogic(const char*);
 %ignore CVC4::SmtEngine::getProof;
 %ignore CVC4::stats::getStatisticsRegistry(SmtEngine*);