From a3d00ce35663ee707aa852acc0d1ac90e5938b9e Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Wed, 21 Feb 2024 17:39:58 +0100 Subject: [PATCH] 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 --- src/api/java/AST.java | 16 ++- src/api/java/ASTDecRefQueue.java | 31 ---- src/api/java/ASTMap.java | 16 ++- src/api/java/ASTVector.java | 34 +++-- src/api/java/ApplyResult.java | 16 ++- src/api/java/ApplyResultDecRefQueue.java | 31 ---- src/api/java/AstMapDecRefQueue.java | 30 ---- src/api/java/AstVectorDecRefQueue.java | 30 ---- src/api/java/CMakeLists.txt | 21 +-- src/api/java/Constructor.java | 16 ++- src/api/java/ConstructorDecRefQueue.java | 12 -- src/api/java/ConstructorList.java | 16 ++- src/api/java/ConstructorListDecRefQueue.java | 12 -- src/api/java/Context.java | 135 +---------------- src/api/java/Fixedpoint.java | 17 ++- src/api/java/FixedpointDecRefQueue.java | 31 ---- src/api/java/FuncInterp.java | 30 +++- src/api/java/FuncInterpDecRefQueue.java | 31 ---- src/api/java/FuncInterpEntryDecRefQueue.java | 30 ---- src/api/java/Goal.java | 16 ++- src/api/java/GoalDecRefQueue.java | 30 ---- src/api/java/IDecRefQueue.java | 83 ----------- src/api/java/Model.java | 16 ++- src/api/java/ModelDecRefQueue.java | 30 ---- src/api/java/Optimize.java | 16 ++- src/api/java/OptimizeDecRefQueue.java | 30 ---- src/api/java/ParamDescrs.java | 16 ++- src/api/java/ParamDescrsDecRefQueue.java | 31 ---- src/api/java/Params.java | 16 ++- src/api/java/ParamsDecRefQueue.java | 30 ---- src/api/java/Probe.java | 16 ++- src/api/java/ProbeDecRefQueue.java | 32 ----- src/api/java/Simplifier.java | 20 ++- src/api/java/SimplifierDecRefQueue.java | 31 ---- src/api/java/Solver.java | 16 ++- src/api/java/SolverDecRefQueue.java | 27 ---- src/api/java/Statistics.java | 20 ++- src/api/java/StatisticsDecRefQueue.java | 30 ---- src/api/java/Tactic.java | 17 ++- src/api/java/TacticDecRefQueue.java | 31 ---- src/api/java/Z3ReferenceQueue.java | 144 +++++++++++++++++++ 41 files changed, 448 insertions(+), 805 deletions(-) delete mode 100644 src/api/java/ASTDecRefQueue.java delete mode 100644 src/api/java/ApplyResultDecRefQueue.java delete mode 100644 src/api/java/AstMapDecRefQueue.java delete mode 100644 src/api/java/AstVectorDecRefQueue.java delete mode 100644 src/api/java/ConstructorDecRefQueue.java delete mode 100644 src/api/java/ConstructorListDecRefQueue.java delete mode 100644 src/api/java/FixedpointDecRefQueue.java delete mode 100644 src/api/java/FuncInterpDecRefQueue.java delete mode 100644 src/api/java/FuncInterpEntryDecRefQueue.java delete mode 100644 src/api/java/GoalDecRefQueue.java delete mode 100644 src/api/java/IDecRefQueue.java delete mode 100644 src/api/java/ModelDecRefQueue.java delete mode 100644 src/api/java/OptimizeDecRefQueue.java delete mode 100644 src/api/java/ParamDescrsDecRefQueue.java delete mode 100644 src/api/java/ParamsDecRefQueue.java delete mode 100644 src/api/java/ProbeDecRefQueue.java delete mode 100644 src/api/java/SimplifierDecRefQueue.java delete mode 100644 src/api/java/SolverDecRefQueue.java delete mode 100644 src/api/java/StatisticsDecRefQueue.java delete mode 100644 src/api/java/TacticDecRefQueue.java create mode 100644 src/api/java/Z3ReferenceQueue.java diff --git a/src/api/java/AST.java b/src/api/java/AST.java index c28c0cfcba7..99cdde948b1 100644 --- 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 { + + private ASTRef(AST referent, ReferenceQueue 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 deleted file mode 100644 index b0a6fa217e1..00000000000 --- a/src/api/java/ASTDecRefQueue.java +++ /dev/null @@ -1,31 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - ASTDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class ASTDecRefQueue extends IDecRefQueue -{ - public ASTDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) { - Native.decRef(ctx.nCtx(), obj); - } -}; diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java index 916811cec28..23a16a82881 100644 --- 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 { + + private ASTMapRef(ASTMap referent, ReferenceQueue 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 index a6b436a99f4..8a5603fcb08 100644 --- 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 { + + private ASTVectorRef(ASTVector referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.astVectorDecRef(ctx.nCtx(), z3Obj); + } + } } \ No newline at end of file diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java index 6cfedd40480..b0e035c4fc7 100644 --- 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 { + + private ApplyResultRef(ApplyResult referent, ReferenceQueue 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 deleted file mode 100644 index e1a6607818b..00000000000 --- a/src/api/java/ApplyResultDecRefQueue.java +++ /dev/null @@ -1,31 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - ApplyResultDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class ApplyResultDecRefQueue extends IDecRefQueue -{ - public ApplyResultDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) { - Native.applyResultDecRef(ctx.nCtx(), obj); - } -}; diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java deleted file mode 100644 index 6c96970b7e7..00000000000 --- a/src/api/java/AstMapDecRefQueue.java +++ /dev/null @@ -1,30 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - AstMapDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class ASTMapDecRefQueue extends IDecRefQueue { - public ASTMapDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) { - Native.astMapDecRef(ctx.nCtx(), obj); - } -} diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java deleted file mode 100644 index e7ce3e33e65..00000000000 --- a/src/api/java/AstVectorDecRefQueue.java +++ /dev/null @@ -1,30 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - AstVectorDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class ASTVectorDecRefQueue extends IDecRefQueue { - public ASTVectorDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) { - Native.astVectorDecRef(ctx.nCtx(), obj); - } -} diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 39ca1e76eb9..c5221014f28 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -91,17 +91,13 @@ 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 @@ -109,9 +105,7 @@ set(Z3_JAVA_JAR_SOURCE_FILES 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,13 +123,9 @@ 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 @@ -144,16 +133,11 @@ set(Z3_JAVA_JAR_SOURCE_FILES 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,16 +150,12 @@ 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 @@ -183,6 +163,7 @@ set(Z3_JAVA_JAR_SOURCE_FILES 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 index 59565f56509..8e1766cb02a 100644 --- 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 Constructor of(Context ctx, Symbol name, Symbol recognizer, @@ -114,4 +116,16 @@ static Constructor of(Context ctx, Symbol name, Symbol recognizer, return new Constructor<>(ctx, n, nativeObj); } + + private static class ConstructorRef extends Z3ReferenceQueue.Reference> { + + private ConstructorRef(Constructor referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.delConstructor(ctx.nCtx(), z3Obj); + } + } } diff --git a/src/api/java/ConstructorDecRefQueue.java b/src/api/java/ConstructorDecRefQueue.java deleted file mode 100644 index a76b26bb73c..00000000000 --- a/src/api/java/ConstructorDecRefQueue.java +++ /dev/null @@ -1,12 +0,0 @@ -package com.microsoft.z3; - -public class ConstructorDecRefQueue extends IDecRefQueue> { - public ConstructorDecRefQueue() { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) { - Native.delConstructor(ctx.nCtx(), obj); - } -} diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index d015c51c0ad..577c802f050 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -17,6 +17,8 @@ package com.microsoft.z3; +import java.lang.ref.ReferenceQueue; + /** * Lists of constructors **/ @@ -34,7 +36,7 @@ void incRef() { @Override void addToReferenceQueue() { - getContext().getConstructorListDRQ().storeReference(getContext(), this); + getContext().getReferenceQueue().storeReference(this, ConstructorListRef::new); } ConstructorList(Context ctx, Constructor[] constructors) @@ -43,4 +45,16 @@ void addToReferenceQueue() { constructors.length, Constructor.arrayToNative(constructors))); } + + private static class ConstructorListRef extends Z3ReferenceQueue.Reference> { + + private ConstructorListRef(ConstructorList referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.delConstructorList(ctx.nCtx(), z3Obj); + } + } } diff --git a/src/api/java/ConstructorListDecRefQueue.java b/src/api/java/ConstructorListDecRefQueue.java deleted file mode 100644 index 2f5dfcb3526..00000000000 --- a/src/api/java/ConstructorListDecRefQueue.java +++ /dev/null @@ -1,12 +0,0 @@ -package com.microsoft.z3; - -public class ConstructorListDecRefQueue extends IDecRefQueue> { - public ConstructorListDecRefQueue() { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) { - Native.delConstructorList(ctx.nCtx(), obj); - } -} diff --git a/src/api/java/Context.java b/src/api/java/Context.java index ad690b7e982..f3efa632a15 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -4319,119 +4319,9 @@ void checkContextMatch(Z3Object[] arr) checkContextMatch(a); } - private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue(); - private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue(); - private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue(); - private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue(); - private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue(); - private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue(); - private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue(); - private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue(); - private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue(); - private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue(); - private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue(); - private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue(); - private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(); - private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(); - private SimplifierDecRefQueue m_Simplifier_DRQ = new SimplifierDecRefQueue(); - private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(); - private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue(); - private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue(); - private ConstructorListDecRefQueue m_ConstructorList_DRQ = - new ConstructorListDecRefQueue(); + private Z3ReferenceQueue m_RefQueue = new Z3ReferenceQueue(this); - public IDecRefQueue> getConstructorDRQ() { - return m_Constructor_DRQ; - } - - public IDecRefQueue> getConstructorListDRQ() { - return m_ConstructorList_DRQ; - } - - public IDecRefQueue getASTDRQ() - { - return m_AST_DRQ; - } - - public IDecRefQueue getASTMapDRQ() - { - return m_ASTMap_DRQ; - } - - public IDecRefQueue getASTVectorDRQ() - { - return m_ASTVector_DRQ; - } - - public IDecRefQueue getApplyResultDRQ() - { - return m_ApplyResult_DRQ; - } - - public IDecRefQueue> getFuncEntryDRQ() - { - return m_FuncEntry_DRQ; - } - - public IDecRefQueue> getFuncInterpDRQ() - { - return m_FuncInterp_DRQ; - } - - public IDecRefQueue getGoalDRQ() - { - return m_Goal_DRQ; - } - - public IDecRefQueue getModelDRQ() - { - return m_Model_DRQ; - } - - public IDecRefQueue getParamsDRQ() - { - return m_Params_DRQ; - } - - public IDecRefQueue getParamDescrsDRQ() - { - return m_ParamDescrs_DRQ; - } - - public IDecRefQueue getProbeDRQ() - { - return m_Probe_DRQ; - } - - public IDecRefQueue getSolverDRQ() - { - return m_Solver_DRQ; - } - - public IDecRefQueue getStatisticsDRQ() - { - return m_Statistics_DRQ; - } - - public IDecRefQueue getTacticDRQ() - { - return m_Tactic_DRQ; - } - - public IDecRefQueue getSimplifierDRQ() - { - return m_Simplifier_DRQ; - } - - public IDecRefQueue getFixedpointDRQ() - { - return m_Fixedpoint_DRQ; - } - - public IDecRefQueue getOptimizeDRQ() - { - return m_Optimize_DRQ; - } + Z3ReferenceQueue getReferenceQueue() { return m_RefQueue; } /** * Disposes of the context. @@ -4439,27 +4329,16 @@ public IDecRefQueue getOptimizeDRQ() @Override public void close() { - m_AST_DRQ.forceClear(this); - m_ASTMap_DRQ.forceClear(this); - m_ASTVector_DRQ.forceClear(this); - m_ApplyResult_DRQ.forceClear(this); - m_FuncEntry_DRQ.forceClear(this); - m_FuncInterp_DRQ.forceClear(this); - m_Goal_DRQ.forceClear(this); - m_Model_DRQ.forceClear(this); - m_Params_DRQ.forceClear(this); - m_Probe_DRQ.forceClear(this); - m_Solver_DRQ.forceClear(this); - m_Optimize_DRQ.forceClear(this); - m_Statistics_DRQ.forceClear(this); - m_Tactic_DRQ.forceClear(this); - m_Simplifier_DRQ.forceClear(this); - m_Fixedpoint_DRQ.forceClear(this); + if (m_ctx == 0) + return; + + m_RefQueue.forceClear(); m_boolSort = null; m_intSort = null; m_realSort = null; m_stringSort = null; + m_RefQueue = null; synchronized (creation_lock) { Native.delContext(m_ctx); diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 96e1dd0cb21..c35f15e9667 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -19,6 +19,8 @@ import com.microsoft.z3.enumerations.Z3_lbool; +import java.lang.ref.ReferenceQueue; + /** * Object for managing fixedpoints **/ @@ -327,9 +329,18 @@ void incRef() { @Override void addToReferenceQueue() { - getContext().getFixedpointDRQ().storeReference(getContext(), this); + getContext().getReferenceQueue().storeReference(this, FixedpointRef::new); } - @Override - void checkNativeObject(long obj) { } + private static class FixedpointRef extends Z3ReferenceQueue.Reference { + + private FixedpointRef(Fixedpoint referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.fixedpointDecRef(ctx.nCtx(), z3Obj); + } + } } diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java deleted file mode 100644 index 69ed82092f5..00000000000 --- a/src/api/java/FixedpointDecRefQueue.java +++ /dev/null @@ -1,31 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - FixedpointDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class FixedpointDecRefQueue extends IDecRefQueue { - public FixedpointDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) - { - Native.fixedpointDecRef(ctx.nCtx(), obj); - } -}; diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java index 64f96534b05..3d2affc4a5e 100644 --- a/src/api/java/FuncInterp.java +++ b/src/api/java/FuncInterp.java @@ -17,6 +17,8 @@ package com.microsoft.z3; +import java.lang.ref.ReferenceQueue; + /** * A function interpretation is represented as a finite map and an 'else' value. * Each entry in the finite map represents the value of a function given a set @@ -93,7 +95,19 @@ void incRef() { @Override void addToReferenceQueue() { - getContext().getFuncEntryDRQ().storeReference(getContext(), this); + getContext().getReferenceQueue().storeReference(this, FuncEntryRef::new); + } + + private static class FuncEntryRef extends Z3ReferenceQueue.Reference> { + + private FuncEntryRef(Entry referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.funcEntryDecRef(ctx.nCtx(), z3Obj); + } } } @@ -186,6 +200,18 @@ void incRef() { @Override void addToReferenceQueue() { - getContext().getFuncInterpDRQ().storeReference(getContext(), this); + getContext().getReferenceQueue().storeReference(this, FuncInterpRef::new); + } + + private static class FuncInterpRef extends Z3ReferenceQueue.Reference> { + + private FuncInterpRef(FuncInterp referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.funcInterpDecRef(ctx.nCtx(), z3Obj); + } } } diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java deleted file mode 100644 index 06a6f2af851..00000000000 --- a/src/api/java/FuncInterpDecRefQueue.java +++ /dev/null @@ -1,31 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - FuncInterpDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class FuncInterpDecRefQueue extends IDecRefQueue> -{ - public FuncInterpDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) { - Native.funcInterpDecRef(ctx.nCtx(), obj); - } -}; diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java deleted file mode 100644 index 77bb78f5b6c..00000000000 --- a/src/api/java/FuncInterpEntryDecRefQueue.java +++ /dev/null @@ -1,30 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - FuncInterpEntryDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class FuncInterpEntryDecRefQueue extends IDecRefQueue> { - public FuncInterpEntryDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) { - Native.funcEntryDecRef(ctx.nCtx(), obj); - } -} diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index 3326f81fe02..e79ca7b7454 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -19,6 +19,8 @@ import com.microsoft.z3.enumerations.Z3_goal_prec; +import java.lang.ref.ReferenceQueue; + /** * A goal (aka problem). A goal is essentially a set of formulas, that can be * solved and/or transformed using tactics and solvers. @@ -262,6 +264,18 @@ void incRef() { @Override void addToReferenceQueue() { - getContext().getGoalDRQ().storeReference(getContext(), this); + getContext().getReferenceQueue().storeReference(this, GoalRef::new); + } + + private static class GoalRef extends Z3ReferenceQueue.Reference { + + private GoalRef(Goal referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.goalDecRef(ctx.nCtx(), z3Obj); + } } } diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java deleted file mode 100644 index 90bad1fb1c1..00000000000 --- a/src/api/java/GoalDecRefQueue.java +++ /dev/null @@ -1,30 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - GoalDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class GoalDecRefQueue extends IDecRefQueue { - public GoalDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) { - Native.goalDecRef(ctx.nCtx(), obj); - } -} diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java deleted file mode 100644 index b9ece31720a..00000000000 --- a/src/api/java/IDecRefQueue.java +++ /dev/null @@ -1,83 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - IDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -import java.lang.ref.PhantomReference; -import java.lang.ref.Reference; -import java.lang.ref.ReferenceQueue; -import java.util.IdentityHashMap; -import java.util.Map; - -/** - * A queue to handle management of native memory. - * - *

Mechanics: once an object is created, a metadata is stored for it in - * {@code referenceMap}, and a {@link PhantomReference} is created with a - * reference to {@code referenceQueue}. - * Once the object becomes strongly unreachable, the phantom reference gets - * added by JVM to the {@code referenceQueue}. - * After each object creation, we iterate through the available objects in - * {@code referenceQueue} and decrement references for them. - * - * @param Type of object stored in queue. - */ -public abstract class IDecRefQueue { - private final ReferenceQueue referenceQueue = new ReferenceQueue<>(); - private final Map, Long> referenceMap = - new IdentityHashMap<>(); - - protected IDecRefQueue() {} - - /** - * An implementation of this method should decrement the reference on a - * given native object. - * This function should always be called on the {@code ctx} thread. - * - * @param ctx Z3 context. - * @param obj Pointer to a Z3 object. - */ - protected abstract void decRef(Context ctx, long obj); - - public void storeReference(Context ctx, T obj) { - PhantomReference ref = new PhantomReference<>(obj, referenceQueue); - referenceMap.put(ref, obj.getNativeObject()); - clear(ctx); - } - - /** - * Clean all references currently in {@code referenceQueue}. - */ - protected void clear(Context ctx) - { - Reference ref; - while ((ref = referenceQueue.poll()) != null) { - long z3ast = referenceMap.remove(ref); - decRef(ctx, z3ast); - } - } - - /** - * Clean all references stored in {@code referenceMap}, - * regardless of whether they are in {@code referenceMap} or not. - */ - public void forceClear(Context ctx) { - for (long ref : referenceMap.values()) { - decRef(ctx, ref); - } - } -} diff --git a/src/api/java/Model.java b/src/api/java/Model.java index ffc4dd47f9d..cf9ab4b64e7 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -19,6 +19,8 @@ import com.microsoft.z3.enumerations.Z3_sort_kind; +import java.lang.ref.ReferenceQueue; + /** * A Model contains interpretations (assignments) of constants and functions. **/ @@ -296,6 +298,18 @@ void incRef() { @Override void addToReferenceQueue() { - getContext().getModelDRQ().storeReference(getContext(), this); + getContext().getReferenceQueue().storeReference(this, ModelRef::new); + } + + private static class ModelRef extends Z3ReferenceQueue.Reference { + + private ModelRef(Model referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.modelDecRef(ctx.nCtx(), z3Obj); + } } } diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java deleted file mode 100644 index f1b7c3fdd6e..00000000000 --- a/src/api/java/ModelDecRefQueue.java +++ /dev/null @@ -1,30 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - ModelDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class ModelDecRefQueue extends IDecRefQueue { - public ModelDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) { - Native.modelDecRef(ctx.nCtx(), obj); - } -} diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index 83833e36bf5..9679a96cd76 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -20,6 +20,8 @@ Nikolaj Bjorner (nbjorner) 2015-07-16 import com.microsoft.z3.enumerations.Z3_lbool; +import java.lang.ref.ReferenceQueue; + /** * Object for managing optimization context @@ -421,6 +423,18 @@ void incRef() { @Override void addToReferenceQueue() { - getContext().getOptimizeDRQ().storeReference(getContext(), this); + getContext().getReferenceQueue().storeReference(this, OptimizeRef::new); + } + + private static class OptimizeRef extends Z3ReferenceQueue.Reference { + + private OptimizeRef(Optimize referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.optimizeDecRef(ctx.nCtx(), z3Obj); + } } } diff --git a/src/api/java/OptimizeDecRefQueue.java b/src/api/java/OptimizeDecRefQueue.java deleted file mode 100644 index 0acf20068c6..00000000000 --- a/src/api/java/OptimizeDecRefQueue.java +++ /dev/null @@ -1,30 +0,0 @@ -/** -Copyright (c) 2012-2015 Microsoft Corporation - -Module Name: - - OptimizeDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class OptimizeDecRefQueue extends IDecRefQueue { - public OptimizeDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) { - Native.optimizeDecRef(ctx.nCtx(), obj); - } -}; diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java index fdaf29647a2..0695f8fe01e 100644 --- a/src/api/java/ParamDescrs.java +++ b/src/api/java/ParamDescrs.java @@ -19,6 +19,8 @@ import com.microsoft.z3.enumerations.Z3_param_kind; +import java.lang.ref.ReferenceQueue; + /** * A ParamDescrs describes a set of parameters. **/ @@ -97,6 +99,18 @@ void incRef() { @Override void addToReferenceQueue() { - getContext().getParamDescrsDRQ().storeReference(getContext(), this); + getContext().getReferenceQueue().storeReference(this, ParamDescrsRef::new); + } + + private static class ParamDescrsRef extends Z3ReferenceQueue.Reference { + + private ParamDescrsRef(ParamDescrs referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.paramDescrsDecRef(ctx.nCtx(), z3Obj); + } } } diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java deleted file mode 100644 index ee3257db968..00000000000 --- a/src/api/java/ParamDescrsDecRefQueue.java +++ /dev/null @@ -1,31 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - ParamDescrsDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class ParamDescrsDecRefQueue extends IDecRefQueue { - public ParamDescrsDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) - { - Native.paramDescrsDecRef(ctx.nCtx(), obj); - } -} diff --git a/src/api/java/Params.java b/src/api/java/Params.java index a76dd3cab3e..1edfa67ba1d 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -18,6 +18,8 @@ package com.microsoft.z3; +import java.lang.ref.ReferenceQueue; + /** * A ParameterSet represents a configuration in the form of Symbol/value pairs. **/ @@ -130,6 +132,18 @@ void incRef() { @Override void addToReferenceQueue() { - getContext().getParamsDRQ().storeReference(getContext(), this); + getContext().getReferenceQueue().storeReference(this, ParamsRef::new); + } + + private static class ParamsRef extends Z3ReferenceQueue.Reference { + + private ParamsRef(Params referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.paramsDecRef(ctx.nCtx(), z3Obj); + } } } diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java deleted file mode 100644 index 349713f67b0..00000000000 --- a/src/api/java/ParamsDecRefQueue.java +++ /dev/null @@ -1,30 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - ParamDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class ParamsDecRefQueue extends IDecRefQueue { - public ParamsDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) { - Native.paramsDecRef(ctx.nCtx(), obj); - } -} diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java index a36f3b64b02..cb4b134425a 100644 --- a/src/api/java/Probe.java +++ b/src/api/java/Probe.java @@ -17,6 +17,8 @@ package com.microsoft.z3; +import java.lang.ref.ReferenceQueue; + /** * Probes are used to inspect a goal (aka problem) and collect information that * may be used to decide which solver and/or preprocessing step will be used. @@ -56,6 +58,18 @@ void incRef() { @Override void addToReferenceQueue() { - getContext().getProbeDRQ().storeReference(getContext(), this); + getContext().getReferenceQueue().storeReference(this, ProbeRef::new); + } + + private static class ProbeRef extends Z3ReferenceQueue.Reference { + + private ProbeRef(Probe referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.probeDecRef(ctx.nCtx(), z3Obj); + } } } diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java deleted file mode 100644 index b25446c0cc4..00000000000 --- a/src/api/java/ProbeDecRefQueue.java +++ /dev/null @@ -1,32 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - ProbeDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class ProbeDecRefQueue extends IDecRefQueue -{ - public ProbeDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) - { - Native.probeDecRef(ctx.nCtx(), obj); - } -}; diff --git a/src/api/java/Simplifier.java b/src/api/java/Simplifier.java index b3fc89ccf11..c89241a7df3 100644 --- a/src/api/java/Simplifier.java +++ b/src/api/java/Simplifier.java @@ -18,6 +18,8 @@ Christoph Wintersteiger (cwinter) 2012-03-21 package com.microsoft.z3; +import java.lang.ref.ReferenceQueue; + public class Simplifier extends Z3Object { /* * A string containing a description of parameters accepted by the simplifier. @@ -32,7 +34,7 @@ public String getHelp() * Retrieves parameter descriptions for Simplifiers. */ public ParamDescrs getParameterDescriptions() { - return new ParamDescrs(getContext(), Native.simplifierGetParamDescrs(getContext().nCtx(), getNativeObject())); + return new ParamDescrs(getContext(), Native.simplifierGetParamDescrs(getContext().nCtx(), getNativeObject())); } Simplifier(Context ctx, long obj) @@ -53,6 +55,18 @@ void incRef() @Override void addToReferenceQueue() { - getContext().getSimplifierDRQ().storeReference(getContext(), this); + getContext().getReferenceQueue().storeReference(this, SimplifierRef::new); + } + + private static class SimplifierRef extends Z3ReferenceQueue.Reference { + + private SimplifierRef(Simplifier referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.simplifierDecRef(ctx.nCtx(), z3Obj); + } } -} \ No newline at end of file +} \ No newline at end of file diff --git a/src/api/java/SimplifierDecRefQueue.java b/src/api/java/SimplifierDecRefQueue.java deleted file mode 100644 index ba15dd5be38..00000000000 --- a/src/api/java/SimplifierDecRefQueue.java +++ /dev/null @@ -1,31 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - SimplifierDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class SimplifierDecRefQueue extends IDecRefQueue { - public SimplifierDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) - { - Native.simplifierDecRef(ctx.nCtx(), obj); - } -} diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index ce795d75833..b814a4db693 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -19,6 +19,8 @@ package com.microsoft.z3; import com.microsoft.z3.enumerations.Z3_lbool; + +import java.lang.ref.ReferenceQueue; import java.util.*; /** @@ -403,6 +405,18 @@ void incRef() { @Override void addToReferenceQueue() { - getContext().getSolverDRQ().storeReference(getContext(), this); + getContext().getReferenceQueue().storeReference(this, SolverRef::new); + } + + private static class SolverRef extends Z3ReferenceQueue.Reference { + + private SolverRef(Solver referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.solverDecRef(ctx.nCtx(), z3Obj); + } } } diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java deleted file mode 100644 index efa15d9398a..00000000000 --- a/src/api/java/SolverDecRefQueue.java +++ /dev/null @@ -1,27 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - SolverDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class SolverDecRefQueue extends IDecRefQueue { - public SolverDecRefQueue() { super(); } - - @Override - protected void decRef(Context ctx, long obj) { - Native.solverDecRef(ctx.nCtx(), obj); - } -} diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java index d509424ed99..6d42e1af0ab 100644 --- a/src/api/java/Statistics.java +++ b/src/api/java/Statistics.java @@ -17,6 +17,8 @@ package com.microsoft.z3; +import java.lang.ref.ReferenceQueue; + /** * Objects of this class track statistical information about solvers. **/ @@ -25,7 +27,7 @@ public class Statistics extends Z3Object { * Statistical data is organized into pairs of [Key, Entry], where every * Entry is either a {@code DoubleEntry} or a {@code UIntEntry} **/ - public class Entry + public static class Entry { /** * The key of the entry. @@ -191,11 +193,23 @@ public Entry get(String key) @Override void incRef() { - getContext().getStatisticsDRQ().storeReference(getContext(), this); + Native.statsIncRef(getContext().nCtx(), getNativeObject()); } @Override void addToReferenceQueue() { - Native.statsIncRef(getContext().nCtx(), getNativeObject()); + getContext().getReferenceQueue().storeReference(this, StatisticsRef::new); + } + + private static class StatisticsRef extends Z3ReferenceQueue.Reference { + + private StatisticsRef(Statistics referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.statsDecRef(ctx.nCtx(), z3Obj); + } } } diff --git a/src/api/java/StatisticsDecRefQueue.java b/src/api/java/StatisticsDecRefQueue.java deleted file mode 100644 index ed698e4cadf..00000000000 --- a/src/api/java/StatisticsDecRefQueue.java +++ /dev/null @@ -1,30 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - StatisticsDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class StatisticsDecRefQueue extends IDecRefQueue { - public StatisticsDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) { - Native.statsDecRef(ctx.nCtx(), obj); - } -} diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java index 11d02ca732f..d70d8a4096e 100644 --- a/src/api/java/Tactic.java +++ b/src/api/java/Tactic.java @@ -17,6 +17,8 @@ package com.microsoft.z3; +import java.lang.ref.ReferenceQueue; + /** * Tactics are the basic building block for creating custom solvers for specific * problem domains. The complete list of tactics may be obtained using @@ -98,6 +100,19 @@ void incRef() { @Override void addToReferenceQueue() { - getContext().getTacticDRQ().storeReference(getContext(), this); + //getContext().getTacticDRQ().storeReference(getContext(), this); + getContext().getReferenceQueue().storeReference(this, TacticRef::new); + } + + private static class TacticRef extends Z3ReferenceQueue.Reference { + + private TacticRef(Tactic referent, ReferenceQueue q) { + super(referent, q); + } + + @Override + void decRef(Context ctx, long z3Obj) { + Native.tacticDecRef(ctx.nCtx(), z3Obj); + } } } diff --git a/src/api/java/TacticDecRefQueue.java b/src/api/java/TacticDecRefQueue.java deleted file mode 100644 index 8f151f25ce6..00000000000 --- a/src/api/java/TacticDecRefQueue.java +++ /dev/null @@ -1,31 +0,0 @@ -/** -Copyright (c) 2012-2014 Microsoft Corporation - -Module Name: - - TacticDecRefQueue.java - -Abstract: - -Author: - - @author Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - -**/ - -package com.microsoft.z3; - -class TacticDecRefQueue extends IDecRefQueue { - public TacticDecRefQueue() - { - super(); - } - - @Override - protected void decRef(Context ctx, long obj) - { - Native.tacticDecRef(ctx.nCtx(), obj); - } -} diff --git a/src/api/java/Z3ReferenceQueue.java b/src/api/java/Z3ReferenceQueue.java new file mode 100644 index 00000000000..22435599fd9 --- /dev/null +++ b/src/api/java/Z3ReferenceQueue.java @@ -0,0 +1,144 @@ +/** +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + IDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ + +package com.microsoft.z3; + +import java.lang.ref.PhantomReference; +import java.lang.ref.ReferenceQueue; + +/** + * A queue to handle management of native memory. + * + *

Mechanics: When an object is created, a so-called {@link PhantomReference} + * is constructed that is associated with the created object and the reference queue {@code referenceQueue}. + * Once the object becomes strongly unreachable, the phantom reference gets + * added by JVM to the {@code referenceQueue}. + * After each object creation, we iterate through the available objects in + * {@code referenceQueue} and decrement references for them. + *

+ * In order for this to work, we need to (i) associate to each phantom reference the underlying + * native object (and its type) that it references and (ii) keep the phantom references themselves alive, so they are not + * garbage collected before the object they reference. + * We use a doubly-linked list of custom phantom references, subclasses of {@link Reference}, to achieve this. + * + */ +class Z3ReferenceQueue { + private final Context ctx; + private final ReferenceQueue referenceQueue = new ReferenceQueue<>(); + private final Reference referenceList = emptyList(); + + Z3ReferenceQueue(Context ctx) { + this.ctx = ctx; + } + + /** + * Create and store a new phantom reference. + */ + void storeReference(T z3Object, ReferenceConstructor refConstructor) { + referenceList.insert(refConstructor.construct(z3Object, referenceQueue)); + clear(); + } + + /** + * Clean all references currently in {@code referenceQueue}. + */ + private void clear() { + Reference ref; + while ((ref = (Reference)referenceQueue.poll()) != null) { + ref.cleanup(ctx); + } + } + + /** + * Clean all references stored in {@code referenceList}, + * regardless of whether they are in {@code referenceQueue} or not. + */ + @SuppressWarnings("StatementWithEmptyBody") + public void forceClear() { + // Decrement all reference counters + Reference cur = referenceList.next; + while (cur.next != null) { + cur.decRef(ctx, cur.nativePtr); + cur = cur.next; + } + + // Bulk-delete the reference list's entries + referenceList.next = cur; + cur.prev = referenceList; + + // Empty the reference queue so that there are no living phantom references anymore. + // This makes sure that all stored phantom references can be GC'd now. + while (referenceQueue.poll() != null) {} + } + + private static Reference emptyList() { + Reference head = new DummyReference(); + Reference tail = new DummyReference(); + head.next = tail; + tail.prev = head; + return head; + } + + // ================================================================================================================ + + @FunctionalInterface + interface ReferenceConstructor { + Reference construct(T reference, ReferenceQueue queue); + } + + abstract static class Reference extends PhantomReference { + + private Reference prev; + private Reference next; + private final long nativePtr; + + Reference(T referent, ReferenceQueue q) { + super(referent, q); + this.nativePtr = referent != null ? referent.getNativeObject() : 0; + } + + private void cleanup(Context ctx) { + decRef(ctx, nativePtr); + assert (prev != null && next != null); + prev.next = next; + next.prev = prev; + } + + private void insert(Reference ref) { + assert next != null; + ref.prev = this; + ref.next = this.next; + ref.next.prev = ref; + next = ref; + } + + abstract void decRef(Context ctx, long z3Obj); + } + + private static class DummyReference extends Reference { + + public DummyReference() { + super(null, null); + } + + @Override + void decRef(Context ctx, long z3Obj) { + // Should never be called. + assert false; + } + } +}