Improved Java phantom references (#7131)

* Reworked phantom reference handling. - Replaced IDecRefQueue with a new Z3ReferenceQueue class - Z3ReferenceQueue manages custom subclasses of phantom references in a doubly-linked list - Replaced all subclasses of IDecRefQueue with subclasses of Z3ReferenceQueue.Reference. These custom reference classes are embedded in the class they reference count. - Context now owns a single Z3ReferenceQueue for all types of references. * Made Statistics.Entry a static subclass * Made Context.close idempotent (as recommended) * Update CMakeLists.txt for building the Java API. * Updated CMakeLists.txt again. * Use correct SuppressWarning annotation to silence the compiler * Formatting
Z3Prover · Feb 21, 2024 · a3d00ce · a3d00ce
1 parent f7691d3
commit a3d00ce
Show file tree

Hide file tree

Showing 41 changed files with 448 additions and 805 deletions.
diff --git a/src/api/java/AST.java b/src/api/java/AST.java
@@ -19,6 +19,8 @@
 
 import com.microsoft.z3.enumerations.Z3_ast_kind;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * The abstract syntax tree (AST) class.
  **/
@@ -196,7 +198,7 @@ void incRef() {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getASTDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, ASTRef::new);
     }
 
     static AST create(Context ctx, long obj)
@@ -217,4 +219,16 @@ static AST create(Context ctx, long obj)
             throw new Z3Exception("Unknown AST kind");
         }
     }
+
+    private static class ASTRef extends Z3ReferenceQueue.Reference<AST> {
+
+        private ASTRef(AST referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.decRef(ctx.nCtx(), z3Obj);
+        }
+    }
 }
diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java
diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java
@@ -17,6 +17,8 @@
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * Map from AST to AST
  **/
@@ -123,6 +125,18 @@ void incRef() {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getASTMapDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, ASTMapRef::new);
+    }
+
+    private static class ASTMapRef extends Z3ReferenceQueue.Reference<ASTMap> {
+
+        private ASTMapRef(ASTMap referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.astMapDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
@@ -17,6 +17,8 @@
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * Vectors of ASTs.
  **/
@@ -101,16 +103,6 @@ public ASTVector(Context ctx)
         super(ctx, Native.mkAstVector(ctx.nCtx()));
     }
 
-    @Override
-    void incRef() {
-        Native.astVectorIncRef(getContext().nCtx(), getNativeObject());
-    }
-
-    @Override
-    void addToReferenceQueue() {
-        getContext().getASTVectorDRQ().storeReference(getContext(), this);
-    }
-
     /**
      * Translates the AST vector into an AST[]
      * */
@@ -241,4 +233,26 @@ public RealExpr[] ToRealExprArray()
             res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }
+
+    @Override
+    void incRef() {
+        Native.astVectorIncRef(getContext().nCtx(), getNativeObject());
+    }
+
+    @Override
+    void addToReferenceQueue() {
+        getContext().getReferenceQueue().storeReference(this, ASTVectorRef::new);
+    }
+
+    private static class ASTVectorRef extends Z3ReferenceQueue.Reference<ASTVector> {
+
+        private ASTVectorRef(ASTVector referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.astVectorDecRef(ctx.nCtx(), z3Obj);
+        }
+    }
 }
diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java
@@ -17,6 +17,8 @@
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * ApplyResult objects represent the result of an application of a tactic to a
  * goal. It contains the subgoals that were produced.
@@ -66,6 +68,18 @@ void incRef() {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getApplyResultDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, ApplyResultRef::new);
+    }
+
+    private static class ApplyResultRef extends Z3ReferenceQueue.Reference<ApplyResult> {
+
+        private ApplyResultRef(ApplyResult referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.applyResultDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }
diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java
diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java
diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
@@ -91,27 +91,21 @@ add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
 
 set(Z3_JAVA_JAR_SOURCE_FILES
   AlgebraicNum.java
-  ApplyResultDecRefQueue.java
   ApplyResult.java
   ArithExpr.java
   ArithSort.java
   ArrayExpr.java
   ArraySort.java
-  ASTDecRefQueue.java
   AST.java
-  AstMapDecRefQueue.java
   ASTMap.java
-  AstVectorDecRefQueue.java
   ASTVector.java
   BitVecExpr.java
   BitVecNum.java
   BitVecSort.java
   BoolExpr.java
   BoolSort.java
   CharSort.java
-  ConstructorDecRefQueue.java
   Constructor.java
-  ConstructorListDecRefQueue.java
   ConstructorList.java
   Context.java
   DatatypeExpr.java
@@ -121,7 +115,6 @@ set(Z3_JAVA_JAR_SOURCE_FILES
   FiniteDomainExpr.java
   FiniteDomainNum.java
   FiniteDomainSort.java
-  FixedpointDecRefQueue.java
   Fixedpoint.java
   FPExpr.java
   FPNum.java
@@ -130,30 +123,21 @@ set(Z3_JAVA_JAR_SOURCE_FILES
   FPRMSort.java
   FPSort.java
   FuncDecl.java
-  FuncInterpDecRefQueue.java
-  FuncInterpEntryDecRefQueue.java
   FuncInterp.java
   Global.java
-  GoalDecRefQueue.java
   Goal.java
-  IDecRefQueue.java
   IntExpr.java
   IntNum.java
   IntSort.java
   IntSymbol.java
   Lambda.java
   ListSort.java
   Log.java
-  ModelDecRefQueue.java
   Model.java
-  OptimizeDecRefQueue.java
   Optimize.java
-  ParamDescrsDecRefQueue.java
   ParamDescrs.java
-  ParamsDecRefQueue.java
   Params.java
   Pattern.java
-  ProbeDecRefQueue.java
   Probe.java
   Quantifier.java
   RatNum.java
@@ -166,23 +150,20 @@ set(Z3_JAVA_JAR_SOURCE_FILES
   SeqSort.java
   SetSort.java
   Simplifier.java
-  SimplifierDecRefQueue.java
-  SolverDecRefQueue.java
   Solver.java
   Sort.java
-  StatisticsDecRefQueue.java
   Statistics.java
   Status.java
   StringSymbol.java
   Symbol.java
-  TacticDecRefQueue.java
   Tactic.java
   TupleSort.java
   UninterpretedSort.java
   UserPropagatorBase.java
   Version.java
   Z3Exception.java
   Z3Object.java
+  Z3ReferenceQueue.java
 )
 set(Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "")
 foreach (java_src_file ${Z3_JAVA_JAR_SOURCE_FILES})

diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java
@@ -17,6 +17,8 @@
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * Constructors are used for datatype sorts.
  **/
@@ -91,7 +93,7 @@ void incRef() {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getConstructorDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, ConstructorRef::new);
     }
 
     static <R> Constructor<R> of(Context ctx, Symbol name, Symbol recognizer,
@@ -114,4 +116,16 @@ static <R> Constructor<R> of(Context ctx, Symbol name, Symbol recognizer,
         return new Constructor<>(ctx, n, nativeObj);
 
     }
+
+    private static class ConstructorRef extends Z3ReferenceQueue.Reference<Constructor<?>> {
+
+        private ConstructorRef(Constructor<?> referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.delConstructor(ctx.nCtx(), z3Obj);
+        }
+    }
 }