Make worklist more efficient (#6625)

dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java

@@ -5,6 +5,7 @@
 import com.sun.source.tree.Tree;
 import java.util.Comparator;
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.IdentityHashMap;
 import java.util.Objects;
 import java.util.PriorityQueue;
@@ -486,7 +487,10 @@ protected static class Worklist {
      * Comparators to allow priority queue to order blocks by their depth-first order, using by
      * forward analysis.
      */
-    public class ForwardDFOComparator implements Comparator<Block> {
+    public class ForwardDfoComparator implements Comparator<Block> {
+      /** Creates a new ForwardDfoComparator. */
+      public ForwardDfoComparator() {}
+
       @SuppressWarnings("nullness:unboxing.of.nullable")
       @Override
       public int compare(Block b1, Block b2) {
@@ -498,7 +502,10 @@ public int compare(Block b1, Block b2) {
      * Comparators to allow priority queue to order blocks by their depth-first order, using by
      * backward analysis.
      */
-    public class BackwardDFOComparator implements Comparator<Block> {
+    public class BackwardDfoComparator implements Comparator<Block> {
+      /** Creates a new BackwardDfoComparator. */
+      public BackwardDfoComparator() {}
+
       @SuppressWarnings("nullness:unboxing.of.nullable")
       @Override
       public int compare(Block b1, Block b2) {
@@ -509,23 +516,31 @@ public int compare(Block b1, Block b2) {
     /** The backing priority queue. */
     protected final PriorityQueue<Block> queue;
 
+    /** Contains the same elements as {@link #queue}, for faster lookup. */
+    protected final Set<Block> queueSet;
+
     /**
      * Create a Worklist.
      *
      * @param direction the direction (forward or backward)
      */
     public Worklist(Direction direction) {
       if (direction == Direction.FORWARD) {
-        queue = new PriorityQueue<>(new ForwardDFOComparator());
+        queue = new PriorityQueue<>(new ForwardDfoComparator());
+        queueSet = new HashSet<>();
       } else if (direction == Direction.BACKWARD) {
-        queue = new PriorityQueue<>(new BackwardDFOComparator());
+        queue = new PriorityQueue<>(new BackwardDfoComparator());
+        queueSet = new HashSet<>();
       } else {
-        throw new BugInCF("Unexpected Direction meet: " + direction.name());
+        throw new BugInCF("Unexpected Direction: " + direction.name());
       }
     }
 
     /**
-     * Process the control flow graph, add the blocks to {@link #depthFirstOrder}.
+     * Process the control flow graph.
+     *
+     * <p>This implementation sets the depth-first order for each block, by adding the blocks to
+     * {@link #depthFirstOrder}.
      *
      * @param cfg the control flow graph to process
      */
@@ -537,6 +552,7 @@ public void process(ControlFlowGraph cfg) {
       }
 
       queue.clear();
+      queueSet.clear();
     }
 
     /**
@@ -549,6 +565,7 @@ public void process(ControlFlowGraph cfg) {
     @EnsuresNonNullIf(result = false, expression = "poll()")
     @SuppressWarnings("nullness:contracts.conditional.postcondition") // forwarded
     public boolean isEmpty() {
+      assert queue.isEmpty() == queueSet.isEmpty();
       return queue.isEmpty();
     }
 
@@ -559,7 +576,7 @@ public boolean isEmpty() {
      * @return true if {@link #queue} contains the given block
      */
     public boolean contains(Block block) {
-      return queue.contains(block);
+      return queueSet.contains(block);
     }
 
     /**
@@ -570,6 +587,7 @@ public boolean contains(Block block) {
      */
     public void add(Block block) {
       queue.add(block);
+      queueSet.add(block);
     }
 
     /**
@@ -580,7 +598,11 @@ public void add(Block block) {
      */
     @Pure
     public @Nullable Block poll() {
-      return queue.poll();
+      Block result = queue.poll();
+      if (result != null) {
+        queueSet.remove(result);
+      }
+      return result;
     }
 
     @Override