Z3ReferenceQueue.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import java.lang.ref.PhantomReference;
import java.lang.ref.ReferenceQueue;
 
class Z3ReferenceQueue {
    private final Context ctx;
    private final ReferenceQueue<Z3Object> referenceQueue = new ReferenceQueue<>();
    private final Reference<?> referenceList = emptyList();
 
    Z3ReferenceQueue(Context ctx) {
        this.ctx = ctx;
    }
 
    <T extends Z3Object> void storeReference(T z3Object, ReferenceConstructor<T> refConstructor) {
        referenceList.insert(refConstructor.construct(z3Object, referenceQueue));
        clear();
    }
 
    private void clear() {
        Reference<?> ref;
        while ((ref = (Reference<?>)referenceQueue.poll()) != null) {
            ref.cleanup(ctx);
        }
    }
 
    @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<T extends Z3Object> {
        Reference<T> construct(T reference, ReferenceQueue<Z3Object> queue);
    }
 
    abstract static class Reference<T extends Z3Object> extends PhantomReference<T> {
 
        private Reference<?> prev;
        private Reference<?> next;
        private final long nativePtr;
 
        Reference(T referent, ReferenceQueue<Z3Object> 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<Z3Object> {
 
        public DummyReference() {
            super(null, null);
        }
 
        @Override
        void decRef(Context ctx, long z3Obj) {
            // Should never be called.
            assert false;
        }
    }
}