From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 28 May 2014 03:35:40 +0000 (-0400)
Subject: Some fixes to GC order in Java.
X-Git-Tag: cvc5-1.0.0~6881
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b49d2e6938fbee46737bbd71419febca2ec318d;p=cvc5.git

Some fixes to GC order in Java.
---

diff --git a/src/expr/expr.i b/src/expr/expr.i
index 31788f06b..b50686f52 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -15,6 +15,50 @@
 %rename(apply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const;
 #endif /* SWIGPYTHON */
 
+#ifdef SWIGJAVA
+%typemap(javabody) CVC4::Expr %{
+  private long swigCPtr;
+  protected boolean swigCMemOwn;
+
+  protected $javaclassname(long cPtr, boolean cMemoryOwn) {
+    swigCMemOwn = cMemoryOwn;
+    swigCPtr = cPtr;
+    this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+%javamethodmodifiers CVC4::Expr::operator=(const Expr&) "protected";
+%typemap(javacode) CVC4::Expr %{
+  // a ref is kept here to keep Java GC from collecting the ExprManager
+  // before the Expr
+  private Object em;
+
+  public Expr assign(Expr e) {
+    Expr r = assignInternal(e);
+    this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+    return r;
+  }
+%}
+%typemap(javaconstruct) Expr {
+    this($imcall, true);
+    this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+  }
+%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::Expr {
+    SmtEngine.dlRef(em);
+    em = null;
+    if (swigCPtr != 0) {
+      if (swigCMemOwn) {
+        swigCMemOwn = false;
+        CVC4JNI.delete_Expr(swigCPtr);
+      }
+      swigCPtr = 0;
+    }
+  }
+#endif /* SWIGJAVA */
+
 %ignore CVC4::operator<<(std::ostream&, const Expr&);
 %ignore CVC4::operator<<(std::ostream&, const TypeCheckingException&);
 
@@ -23,7 +67,7 @@
 %ignore CVC4::expr::operator<<(std::ostream&, ExprDag);
 %ignore CVC4::expr::operator<<(std::ostream&, ExprSetLanguage);
 
-%rename(assign) CVC4::Expr::operator=(const Expr&);
+%rename(assignInternal) CVC4::Expr::operator=(const Expr&);
 %rename(equals) CVC4::Expr::operator==(const Expr&) const;
 %ignore CVC4::Expr::operator!=(const Expr&) const;
 %rename(less) CVC4::Expr::operator<(const Expr&) const;
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index b29f59621..fccadf43c 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -7,7 +7,7 @@
   // before the ExprManager
   private Object options;
 %}
-%typemap(javaconstruct) CVC4::ExprManager {
+%typemap(javaconstruct) ExprManager {
     this($imcall, true);
     this.options = SmtEngine.mkRef(options); // keep ref to options in SWIG proxy class
   }
diff --git a/src/expr/type.i b/src/expr/type.i
index 6394dda67..16d059eac 100644
--- a/src/expr/type.i
+++ b/src/expr/type.i
@@ -8,9 +8,52 @@
 %rename(apply) CVC4::TypeHashFunction::operator()(const CVC4::Type&) const;
 #endif /* SWIGPYTHON */
 
+#ifdef SWIGJAVA
+%typemap(javabody) CVC4::Type %{
+  private long swigCPtr;
+  protected boolean swigCMemOwn;
+
+  protected $javaclassname(long cPtr, boolean cMemoryOwn) {
+    swigCMemOwn = cMemoryOwn;
+    swigCPtr = cPtr;
+    this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+%javamethodmodifiers CVC4::Type::operator=(const Type&) "protected";
+%typemap(javacode) CVC4::Type %{
+  // a ref is kept here to keep Java GC from collecting the ExprManager
+  // before the Type
+  private Object em;
+
+  public Type assign(Type t) {
+    Type r = assignInternal(t);
+    this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+    return r;
+  }
+%}
+%typemap(javaconstruct) Type {
+    this($imcall, true);
+    this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+  }
+%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::Type {
+    SmtEngine.dlRef(em);
+    em = null;
+    if (swigCPtr != 0) {
+      if (swigCMemOwn) {
+        swigCMemOwn = false;
+        CVC4JNI.delete_Type(swigCPtr);
+      }
+      swigCPtr = 0;
+    }
+  }
+#endif /* SWIGJAVA */
 %ignore CVC4::operator<<(std::ostream&, const Type&);
 
-%rename(assign) CVC4::Type::operator=(const Type&);
+%rename(assignInternal) CVC4::Type::operator=(const Type&);
 %rename(equals) CVC4::Type::operator==(const Type&) const;
 %ignore CVC4::Type::operator!=(const Type&) const;
 %rename(less) CVC4::Type::operator<(const Type&) const;
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index 7bece21b3..9cf4467a8 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -27,7 +27,7 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jc
 }
 }
 %}
-%typemap(javaconstruct) CVC4::SmtEngine {
+%typemap(javaconstruct) SmtEngine {
     this($imcall, true);
     emRef = mkRef(em); // keep ref to expr manager in SWIG proxy class
   }