Replace Z3 phantom reference map by doubly-linked list.

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

@@ -24,11 +24,9 @@
 import com.microsoft.z3.enumerations.Z3_sort_kind;
 import com.microsoft.z3.enumerations.Z3_symbol_kind;
 import java.lang.ref.PhantomReference;
-import java.lang.ref.Reference;
 import java.lang.ref.ReferenceQueue;
 import java.math.BigInteger;
 import java.util.ArrayList;
-import java.util.IdentityHashMap;
 import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
@@ -126,8 +124,7 @@ class Z3FormulaCreator extends FormulaCreator<Long, Long, Long, Long> {
   /** Automatic clean-up of Z3 ASTs. */
   private final ReferenceQueue<Z3Formula> referenceQueue = new ReferenceQueue<>();
 
-  private final IdentityHashMap<PhantomReference<? extends Z3Formula>, Long> referenceMap =
-      new IdentityHashMap<>();
+  private final Z3AstReference referenceListHead;
 
   // todo: getters for statistic.
   private final Timer cleanupTimer = new Timer();
@@ -147,6 +144,17 @@ class Z3FormulaCreator extends FormulaCreator<Long, Long, Long, Long> {
     super(pEnv, pBoolType, pIntegerType, pRealType, pStringType, pRegexType);
     shutdownNotifier = pShutdownNotifier;
     config.inject(this);
+
+    if (usePhantomReferences) {
+      // Setup sentinel nodes for doubly-linked phantom reference list.
+      Z3AstReference head = new Z3AstReference();
+      Z3AstReference tail = new Z3AstReference();
+      head.next = tail;
+      tail.prev = head;
+      referenceListHead = head;
+    } else {
+      referenceListHead = null;
+    }
   }
 
   final Z3Exception handleZ3Exception(Z3Exception e) throws Z3Exception, InterruptedException {
@@ -265,14 +273,6 @@ protected <TD extends Formula, TR extends Formula> ArrayFormula<TD, TR> encapsul
         new Z3ArrayFormula<>(getEnv(), pTerm, pIndexType, pElementType), pTerm);
   }
 
-  private <T extends Z3Formula> T storePhantomReference(T out, Long pTerm) {
-    if (usePhantomReferences) {
-      PhantomReference<T> ref = new PhantomReference<>(out, referenceQueue);
-      referenceMap.put(ref, pTerm);
-    }
-    return out;
-  }
-
   @SuppressWarnings("unchecked")
   @Override
   public <T extends Formula> T encapsulate(FormulaType<T> pType, Long pTerm) {
@@ -392,16 +392,53 @@ public Long getFloatingPointType(FormulaType.FloatingPointType type) {
     return fpSort;
   }
 
+  private static final class Z3AstReference extends PhantomReference<Z3Formula> {
+    private final long z3Ast;
+    private @Nullable Z3AstReference prev;
+    private @Nullable Z3AstReference next;
+
+    // To generate dummy head and tail nodes
+    private Z3AstReference() {
+      this(null, null, 0);
+    }
+
+    private Z3AstReference(Z3Formula referent, ReferenceQueue<? super Z3Formula> q, long z3Ast) {
+      super(referent, q);
+      this.z3Ast = z3Ast;
+    }
+
+    private void insert(Z3AstReference ref) {
+      assert next != null;
+      ref.prev = this;
+      ref.next = this.next;
+      ref.next.prev = ref;
+      this.next = ref;
+    }
+
+    private void cleanup(long environment) {
+      Native.decRef(environment, z3Ast);
+      assert (prev != null && next != null);
+      prev.next = next;
+      next.prev = prev;
+    }
+  }
+
+  private <T extends Z3Formula> T storePhantomReference(T out, long pTerm) {
+    if (usePhantomReferences) {
+      referenceListHead.insert(new Z3AstReference(out, referenceQueue, pTerm));
+    }
+    return out;
+  }
+
   private void cleanupReferences() {
     if (!usePhantomReferences) {
       return;
     }
     cleanupTimer.start();
     try {
-      Reference<? extends Z3Formula> ref;
-      while ((ref = referenceQueue.poll()) != null) {
-        long z3ast = referenceMap.remove(ref);
-        Native.decRef(environment, z3ast);
+      Z3AstReference ref;
+      while ((ref = (Z3AstReference) referenceQueue.poll()) != null) {
+        ref.cleanup(environment);
       }
     } finally {
       cleanupTimer.stop();
@@ -979,13 +1016,27 @@ private long goalToAST(long z3context, long goal) {
   }
 
   /** Closing the context. */
+  @SuppressWarnings("empty-statement")
   public void forceClose() {
-    cleanupReferences();
-
     // Force clean all ASTs, even those which were not GC'd yet.
-    // Is a no-op if phantom reference handling is not enabled.
-    for (long ast : referenceMap.values()) {
-      Native.decRef(getEnv(), ast);
+    if (usePhantomReferences) {
+      Z3AstReference cur = referenceListHead.next;
+      assert cur != null;
+      while (cur.next != null) {
+        Native.decRef(environment, cur.z3Ast);
+        cur = cur.next;
+      }
+      Z3AstReference tail = cur;
+      // Bulk delete everything between head and tail
+      referenceListHead.next = tail;
+      tail.prev = referenceListHead;
+
+      // Remove already enqueued references.
+      while (referenceQueue.poll() != null) {
+        // NOTE: Together with the above list deletion, this empty loop will guarantee that no more
+        // ast references are reachable by the GC making them all eligible for garbage collection
+        // and preventing them from getting enqueued into the reference queue in the future.
+      }
     }
   }