Add Queue.isEmpty/poll refinement

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java

@@ -113,6 +113,14 @@ public class NullnessNoInitAnnotatedTypeFactory
     private final ExecutableElement mapGet =
             TreeUtils.getMethod("java.util.Map", "get", 1, processingEnv);
 
+    /** The Collection.isEmpty method. */
+    private final ExecutableElement collectionIsEmpty =
+            TreeUtils.getMethod("java.util.Collection", "isEmpty", 0, processingEnv);
+
+    /** The Queue.poll method. */
+    private final ExecutableElement queuePoll =
+            TreeUtils.getMethod("java.util.Queue", "poll", 0, processingEnv);
+
     // List is in alphabetical order.  If you update it, also update
     // ../../../../../../../../docs/manual/nullness-checker.tex
     // and make a pull request for variables NONNULL_ANNOTATIONS and BASE_COPYABLE_ANNOTATIONS in
@@ -1072,4 +1080,24 @@ private AnnotationMirror ensuresNonNullAnno(String expression) {
     public boolean isMapGet(Node node) {
         return NodeUtils.isMethodInvocation(node, mapGet, getProcessingEnv());
     }
+
+    /**
+     * Returns true if {@code node} is an invocation of Collection.isEmpty.
+     *
+     * @param node a CFG node
+     * @return true if {@code node} is an invocation of Collection.isEmpty
+     */
+    public boolean isCollectionIsEmpty(Node node) {
+        return NodeUtils.isMethodInvocation(node, collectionIsEmpty, getProcessingEnv());
+    }
+
+    /**
+     * Returns true if {@code node} is an invocation of Queue.poll.
+     *
+     * @param node a CFG node
+     * @return true if {@code node} is an invocation of Queue.poll
+     */
+    public boolean isQueuePoll(Node node) {
+        return NodeUtils.isMethodInvocation(node, queuePoll, getProcessingEnv());
+    }
 }

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitStore.java

@@ -1,18 +1,29 @@
 package org.checkerframework.checker.nullness;
 
+import com.sun.source.tree.MethodInvocationTree;
+
 import org.checkerframework.checker.initialization.InitializationAnnotatedTypeFactory;
 import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.nullness.qual.PolyNull;
+import org.checkerframework.dataflow.cfg.node.MethodInvocationNode;
+import org.checkerframework.dataflow.cfg.node.Node;
 import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer;
 import org.checkerframework.dataflow.expression.FieldAccess;
+import org.checkerframework.dataflow.expression.JavaExpression;
+import org.checkerframework.dataflow.util.PurityUtils;
 import org.checkerframework.framework.flow.CFAbstractAnalysis;
 import org.checkerframework.framework.flow.CFAbstractStore;
 import org.checkerframework.framework.qual.MonotonicQualifier;
 import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
+import org.checkerframework.javacutil.TreeUtils;
 
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.Map;
+import java.util.Set;
+
+import javax.lang.model.element.ExecutableElement;
 
 /**
  * In addition to the base class behavior, tracks whether {@link PolyNull} is known to be {@link
@@ -40,6 +51,9 @@ public class NullnessNoInitStore extends CFAbstractStore<NullnessNoInitValue, Nu
      */
     protected Map<FieldAccess, NullnessNoInitValue> initializedFields;
 
+    /** Receivers that are currently known to be non-empty queues. */
+    protected Set<JavaExpression> nonEmptyQueueReceivers;
+
     /**
      * Create a NullnessStore.
      *
@@ -53,6 +67,7 @@ public NullnessNoInitStore(
         super(analysis, sequentialSemantics);
         isPolyNullNonNull = false;
         isPolyNullNull = false;
+        nonEmptyQueueReceivers = new HashSet<>();
     }
 
     /**
@@ -67,6 +82,56 @@ public NullnessNoInitStore(NullnessNoInitStore s) {
         if (s.initializedFields != null) {
             initializedFields = s.initializedFields;
         }
+        nonEmptyQueueReceivers = new HashSet<>(s.nonEmptyQueueReceivers);
+    }
+
+    /**
+     * Marks the receiver as a queue known to be non-empty.
+     *
+     * @param receiver a queue receiver expression
+     */
+    public void markQueueAsNonEmpty(JavaExpression receiver) {
+        nonEmptyQueueReceivers.add(receiver);
+    }
+
+    /**
+     * Returns true if the receiver is known to be a non-empty queue.
+     *
+     * @param receiver a queue receiver expression
+     * @return true if the receiver is known to be a non-empty queue
+     */
+    public boolean isQueueNonEmpty(JavaExpression receiver) {
+        return nonEmptyQueueReceivers.contains(receiver);
+    }
+
+    @Override
+    public void updateForAssignment(Node n, @Nullable NullnessNoInitValue val) {
+        super.updateForAssignment(n, val);
+        JavaExpression expr = JavaExpression.fromNode(n);
+        if (expr != null) {
+            nonEmptyQueueReceivers.removeIf(
+                    receiver -> receiver.containsSyntacticEqualJavaExpression(expr));
+        }
+    }
+
+    @Override
+    public void updateForMethodCall(
+            MethodInvocationNode methodInvocationNode,
+            GenericAnnotatedTypeFactory<NullnessNoInitValue, NullnessNoInitStore, ?, ?>
+                    atypeFactory,
+            NullnessNoInitValue val) {
+        super.updateForMethodCall(methodInvocationNode, atypeFactory, val);
+
+        // Conservatively invalidate all non-empty queue information for side-effecting method
+        // calls.
+        MethodInvocationTree tree = methodInvocationNode.getTree();
+        ExecutableElement method = TreeUtils.elementFromUse(tree);
+        boolean hasSideEffect =
+                !(atypeFactory.isSideEffectFree(method)
+                        || PurityUtils.isSideEffectFree(atypeFactory, method));
+        if (hasSideEffect) {
+            nonEmptyQueueReceivers.clear();
+        }
     }
 
     @Override
@@ -118,6 +183,8 @@ public NullnessNoInitStore leastUpperBound(NullnessNoInitStore other) {
         NullnessNoInitStore lub = super.leastUpperBound(other);
         lub.isPolyNullNonNull = isPolyNullNonNull && other.isPolyNullNonNull;
         lub.isPolyNullNull = isPolyNullNull && other.isPolyNullNull;
+        lub.nonEmptyQueueReceivers = new HashSet<>(nonEmptyQueueReceivers);
+        lub.nonEmptyQueueReceivers.retainAll(other.nonEmptyQueueReceivers);
         return lub;
     }
 
@@ -131,7 +198,8 @@ protected boolean supersetOf(CFAbstractStore<NullnessNoInitValue, NullnessNoInit
                 || (other.isPolyNullNull != isPolyNullNull)) {
             return false;
         }
-        return super.supersetOf(other);
+        return super.supersetOf(other)
+                && nonEmptyQueueReceivers.containsAll(other.nonEmptyQueueReceivers);
     }
 
     @Override
@@ -141,7 +209,9 @@ protected String internalVisualize(
                 + viz.getSeparator()
                 + viz.visualizeStoreKeyVal("isPolyNullNonNull", isPolyNullNonNull)
                 + viz.getSeparator()
-                + viz.visualizeStoreKeyVal("isPolyNullNull", isPolyNullNull);
+                + viz.visualizeStoreKeyVal("isPolyNullNull", isPolyNullNull)
+                + viz.getSeparator()
+                + viz.visualizeStoreKeyVal("nonEmptyQueueReceivers", nonEmptyQueueReceivers);
     }
 
     /**

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitTransfer.java

@@ -39,6 +39,7 @@
 
 import java.util.List;
 import java.util.Map;
+import java.util.Queue;
 
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.ExecutableElement;
@@ -81,6 +82,14 @@ public class NullnessNoInitTransfer
      */
     protected final AnnotatedDeclaredType MAP_TYPE;
 
+    /**
+     * Java's Queue interface.
+     *
+     * <p>The qualifiers in this type don't matter -- it is not used as a fully-annotated
+     * AnnotatedDeclaredType, but just passed to asSuper().
+     */
+    protected final AnnotatedDeclaredType QUEUE_TYPE;
+
     /** The type factory for the nullness analysis that was passed to the constructor. */
     protected final NullnessNoInitAnnotatedTypeFactory nullnessTypeFactory;
 
@@ -130,6 +139,14 @@ public NullnessNoInitTransfer(NullnessNoInitAnalysis analysis) {
                                 nullnessTypeFactory,
                                 false);
 
+        QUEUE_TYPE =
+                (AnnotatedDeclaredType)
+                        AnnotatedTypeMirror.createType(
+                                TypesUtils.typeFromClass(
+                                        Queue.class, analysis.getTypes(), elements),
+                                nullnessTypeFactory,
+                                false);
+
         nonNullAssumptionAfterInvocation =
                 !analysis.getTypeFactory()
                         .getChecker()
@@ -411,6 +428,15 @@ public TransferResult<NullnessNoInitValue, NullnessNoInitStore> visitThrow(
     @Override
     public TransferResult<NullnessNoInitValue, NullnessNoInitStore> visitMethodInvocation(
             MethodInvocationNode n, TransferInput<NullnessNoInitValue, NullnessNoInitStore> in) {
+        Node receiver = n.getTarget().getReceiver();
+        JavaExpression receiverExpr = JavaExpression.fromNode(receiver);
+        // Capture queue non-emptiness fact before superclass mutates the store when handling side
+        // effects.
+        boolean isNonEmptyQueuePoll =
+                nullnessTypeFactory.isQueuePoll(n)
+                        && receiverExpr != null
+                        && in.getRegularStore().isQueueNonEmpty(receiverExpr);
+
         TransferResult<NullnessNoInitValue, NullnessNoInitStore> result =
                 super.visitMethodInvocation(n, in);
 
@@ -420,7 +446,6 @@ public TransferResult<NullnessNoInitValue, NullnessNoInitStore> visitMethodInvoc
         boolean isMethodSideEffectFree =
                 nullnessTypeFactory.isSideEffectFree(method)
                         || PurityUtils.isSideEffectFree(nullnessTypeFactory, method);
-        Node receiver = n.getTarget().getReceiver();
         if (nonNullAssumptionAfterInvocation
                 || isMethodSideEffectFree
                 || !JavaExpression.fromNode(receiver).isAssignableByOtherCode()) {
@@ -464,6 +489,27 @@ public TransferResult<NullnessNoInitValue, NullnessNoInitStore> visitMethodInvoc
             }
         }
 
+        // Handle Collection.isEmpty(): mark receiver as non-empty in the false branch.
+        if (nullnessTypeFactory.isCollectionIsEmpty(n)) {
+            if (receiverExpr != null) {
+                NullnessNoInitStore thenStore = result.getThenStore();
+                NullnessNoInitStore elseStore = result.getElseStore();
+                elseStore.markQueueAsNonEmpty(receiverExpr);
+                return new ConditionalTransferResult<>(
+                        result.getResultValue(), thenStore, elseStore);
+            }
+        }
+
+        // Refine result to @NonNull if n is an invocation of Queue.poll(), the receiver is known to
+        // be non-empty, and Queue element type is @NonNull
+        if (isNonEmptyQueuePoll) {
+            AnnotatedTypeMirror receiverType = nullnessTypeFactory.getReceiverType(n.getTree());
+            if (!isElementTypeNullable(receiverType)) {
+                makeNonNull(result, n);
+                refineToNonNull(result);
+            }
+        }
+
         return result;
     }
 
@@ -485,6 +531,24 @@ private boolean isValueTypeNullable(AnnotatedTypeMirror mapOrSubtype) {
         return valueType.hasAnnotation(NULLABLE);
     }
 
+    /**
+     * Returns true if queueType's element type (the E type argument to Queue) is @Nullable.
+     *
+     * @param queueOrSubtype the Queue type, or a subtype
+     * @return true if queueType's element type is @Nullable
+     */
+    private boolean isElementTypeNullable(AnnotatedTypeMirror queueOrSubtype) {
+        AnnotatedDeclaredType queueType =
+                AnnotatedTypes.asSuper(nullnessTypeFactory, queueOrSubtype, QUEUE_TYPE);
+        int numTypeArguments = queueType.getTypeArguments().size();
+        if (numTypeArguments != 1) {
+            throw new TypeSystemError(
+                    "Wrong number %d of type arguments: %s", numTypeArguments, queueType);
+        }
+        AnnotatedTypeMirror elementType = queueType.getTypeArguments().get(0);
+        return elementType.hasAnnotation(NULLABLE);
+    }
+
     @Override
     public TransferResult<NullnessNoInitValue, NullnessNoInitStore> visitReturn(
             ReturnNode n, TransferInput<NullnessNoInitValue, NullnessNoInitStore> in) {