Add Queue.isEmpty/poll refinement

Author: nhioe

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/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()
@@ -464,6 +481,34 @@ public TransferResult<NullnessNoInitValue, NullnessNoInitStore> visitMethodInvoc
             }
         }
 
+        // Handle Collection.isEmpty(), mark receiver as non-empty in the false branch
+        if (nullnessTypeFactory.isCollectionIsEmpty(n)) {
+            JavaExpression receiverExpr = JavaExpression.fromNode(receiver);
+            if (CFAbstractStore.canInsertJavaExpression(receiverExpr)) {
+                NullnessNoInitStore thenStore = result.getThenStore();
+                NullnessNoInitStore elseStore = result.getElseStore();
+                elseStore.insertValue(receiverExpr, NONNULL);
+                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 (nullnessTypeFactory.isQueuePoll(n)) {
+            NullnessNoInitStore store = result.getRegularStore();
+            JavaExpression receiverExpr = JavaExpression.fromNode(receiver);
+            NullnessNoInitValue receiverValue = store.getValue(receiverExpr);
+            if (receiverValue != null && receiverValue.getAnnotations().contains(NONNULL)) {
+                AnnotatedTypeMirror receiverType = nullnessTypeFactory.getReceiverType(n.getTree());
+                if (!isElementTypeNullable(receiverType)) {
+                    makeNonNull(result, n);
+                    refineToNonNull(result);
+                }
+            }
+        }
+
         return result;
     }
 
@@ -485,6 +530,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) {

checker/tests/nullness/IsEmptyPoll.java

@@ -1,8 +1,6 @@
 // Test case for Issue 399:
 // https://github.com/typetools/checker-framework/issues/399
 
-// @skip-test until the issue is fixed
-
 import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;