Introducing improved Optional Checker

checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/NonEmpty.java

@@ -8,8 +8,9 @@
 import org.checkerframework.framework.qual.SubtypeOf;
 
 /**
- * The {@link java.util.Collection Collection}, {@link java.util.Iterator Iterator}, {@link
- * java.lang.Iterable Iterable}, or {@link java.util.Map Map} is definitely non-empty.
+ * The {@link java.util.Collection Collection}, {@link java.util.Iterator Iterator}, {@link Iterable
+ * Iterable}, or {@link java.util.Map Map}, or {@link java.util.stream.Stream Stream} is definitely
+ * non-empty.
  *
  * @checker_framework.manual #non-empty-checker Non-Empty Checker
  */

checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/UnknownNonEmpty.java

@@ -10,7 +10,8 @@
 
 /**
  * The {@link java.util.Collection Collection}, {@link java.util.Iterator Iterator}, {@link
- * java.lang.Iterable Iterable}, or {@link java.util.Map Map} may or may not be empty.
+ * java.lang.Iterable Iterable}, {@link java.util.Map Map}, or {@link java.util.stream.Stream
+ * Stream} may or may not be empty.
  *
  * @checker_framework.manual #non-empty-checker Non-Empty Checker
  */

checker/src/main/java/org/checkerframework/checker/nonempty/NonEmptyChecker.java

@@ -1,17 +1,67 @@
 package org.checkerframework.checker.nonempty;
 
+import com.sun.source.tree.MethodTree;
+import java.util.Set;
+import org.checkerframework.checker.optional.OptionalChecker;
+import org.checkerframework.checker.optional.OptionalImplChecker;
+import org.checkerframework.checker.optional.OptionalImplVisitor;
 import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.framework.source.SourceChecker;
+import org.checkerframework.framework.source.SupportedOptions;
 
 /**
  * A type-checker that prevents {@link java.util.NoSuchElementException} in the use of container
  * classes.
  *
+ * <p>Runs the {@link org.checkerframework.checker.optional.OptionalImplChecker}(as a subchecker),
+ * using explicitly-written (i.e., programmer-written) annotations from the Non-Empty type system to
+ * refine the Optional analysis. This improves analysis of operations on containers (e.g., Streams,
+ * Collections) that result in values of type Optional.
+ *
  * @checker_framework.manual #non-empty-checker Non-Empty Checker
  */
+@SupportedOptions("checkAllDefs")
 public class NonEmptyChecker extends BaseTypeChecker {
 
   /** Creates a NonEmptyChecker. */
   public NonEmptyChecker() {
     super();
   }
+
+  @Override
+  protected Set<Class<? extends SourceChecker>> getImmediateSubcheckerClasses() {
+    Set<Class<? extends SourceChecker>> checkers = super.getImmediateSubcheckerClasses();
+    // Ideally, the OptionalImplChecker should only be added as a subchecker if this Non-Empty
+    // Checker is being run in aggregate with the top-level Optional Checker
+    // However, it appears that this information (via SourceChecker#getParentChecker()) is not
+    // available at the time when this method is called.
+    checkers.add(OptionalImplChecker.class);
+    return checkers;
+  }
+
+  @Override
+  public boolean shouldSkipDefs(MethodTree tree) {
+    if (!(this.getParentChecker() instanceof OptionalChecker)) {
+      // If the parent checker is null, or if it is NOT an instance of the top-level Optional
+      // Checker,
+      // this indicates that this Non-Empty Checker is being run independently. In this case, check
+      // all definitions, not just the ones related to the Optional Checker's guarantee.
+      return false;
+    }
+    return !getMethodsToVerify().contains(tree.getName().toString());
+  }
+
+  /**
+   * Obtains the methods to verify w.r.t. the Non-Empty type system from the Optional Checker.
+   *
+   * @return the set of names of the methods to be verified by the Non-Empty Checker
+   * @throws AssertionError if invoked when the {@link OptionalImplChecker} is not set as a
+   *     subchecker of this checker
+   */
+  private Set<String> getMethodsToVerify() {
+    OptionalImplChecker optionalCheckerImpl = getSubchecker(OptionalImplChecker.class);
+    assert optionalCheckerImpl != null;
+    OptionalImplVisitor optionalVisitor = (OptionalImplVisitor) optionalCheckerImpl.getVisitor();
+    return optionalVisitor.getNamesOfMethodsToVerifyWithNonEmptyChecker();
+  }
 }

checker/src/main/java/org/checkerframework/checker/nonempty/NonEmptyTransfer.java

@@ -188,8 +188,9 @@ private boolean isAccessOfNonEmptyCollection(
       TransferInput<CFValue, CFStore> in, MethodInvocationNode methodAccessNode) {
     Node receiver = methodAccessNode.getTarget().getReceiver();
 
-    return aTypeFactory.containsSameByClass(
-        in.getValueOfSubNode(receiver).getAnnotations(), NonEmpty.class);
+    CFValue receiverValue = in.getValueOfSubNode(receiver);
+    return receiverValue != null
+        && aTypeFactory.containsSameByClass(receiverValue.getAnnotations(), NonEmpty.class);
   }
 
   /**

checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.java

@@ -1,32 +1,26 @@
 package org.checkerframework.checker.optional;
 
-import java.util.Optional;
-import java.util.Set;
-import org.checkerframework.common.aliasing.AliasingChecker;
-import org.checkerframework.common.basetype.BaseTypeChecker;
-import org.checkerframework.framework.qual.RelevantJavaTypes;
-import org.checkerframework.framework.qual.StubFiles;
+import java.util.ArrayList;
+import java.util.Collection;
+import org.checkerframework.checker.nonempty.NonEmptyChecker;
+import org.checkerframework.framework.source.AggregateChecker;
 import org.checkerframework.framework.source.SourceChecker;
-import org.checkerframework.framework.source.SupportedOptions;
 
 /**
- * A type-checker that prevents misuse of the {@link java.util.Optional} class.
+ * A type-checker that prevents {@link java.util.NoSuchElementException} in the use of the {@link
+ * java.util.Optional} class.
  *
  * @checker_framework.manual #optional-checker Optional Checker
  */
-// TODO: For a call to `@Optional#ofNullable`, if the argument has type
-// @NonNull, make the return type have type @Present.
-@RelevantJavaTypes(Optional.class)
-@StubFiles({"javaparser.astub"})
-@SupportedOptions("optionalMapAssumeNonNull")
-public class OptionalChecker extends BaseTypeChecker {
-  /** Create an OptionalChecker. */
+public class OptionalChecker extends AggregateChecker {
+
+  /** Creates a new {@link org.checkerframework.checker.optional.OptionalChecker} */
   public OptionalChecker() {}
 
   @Override
-  protected Set<Class<? extends SourceChecker>> getImmediateSubcheckerClasses() {
-    Set<Class<? extends SourceChecker>> subcheckers = super.getImmediateSubcheckerClasses();
-    subcheckers.add(AliasingChecker.class);
-    return subcheckers;
+  protected Collection<Class<? extends SourceChecker>> getSupportedCheckers() {
+    Collection<Class<? extends SourceChecker>> checkers = new ArrayList<>(2);
+    checkers.add(NonEmptyChecker.class);
+    return checkers;
   }
 }

checker/src/main/java/org/checkerframework/checker/optional/OptionalAnnotatedTypeFactory.java → checker/src/main/java/org/checkerframework/checker/optional/OptionalImplAnnotatedTypeFactory.java

@@ -21,8 +21,8 @@
 import org.checkerframework.javacutil.AnnotationBuilder;
 import org.checkerframework.javacutil.TreeUtils;
 
-/** OptionalAnnotatedTypeFactory for the Optional Checker. */
-public class OptionalAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
+/** OptionalImplAnnotatedTypeFactory for the OptionalImplChecker. */
+public class OptionalImplAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
 
   /** The element for java.util.Optional.map(). */
   private final ExecutableElement optionalMap;
@@ -31,11 +31,12 @@ public class OptionalAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
   protected final AnnotationMirror PRESENT = AnnotationBuilder.fromClass(elements, Present.class);
 
   /**
-   * Creates an OptionalAnnotatedTypeFactory.
+   * Creates an OptionalImplAnnotatedTypeFactory.
    *
-   * @param checker the Optional Checker associated with this type factory
+   * @param checker the {@link org.checkerframework.checker.optional.OptionalImplChecker} associated
+   *     with this type factory
    */
-  public OptionalAnnotatedTypeFactory(BaseTypeChecker checker) {
+  public OptionalImplAnnotatedTypeFactory(BaseTypeChecker checker) {
     super(checker);
     postInit();
     optionalMap = TreeUtils.getMethodOrNull("java.util.Optional", "map", 1, getProcessingEnv());
@@ -128,6 +129,6 @@ private boolean containsNullable(Collection<? extends AnnotationMirror> annos) {
   @Override
   public CFTransfer createFlowTransferFunction(
       CFAbstractAnalysis<CFValue, CFStore, CFTransfer> analysis) {
-    return new OptionalTransfer(analysis);
+    return new OptionalImplTransfer(analysis);
   }
 }

checker/src/main/java/org/checkerframework/checker/optional/OptionalImplChecker.java

@@ -0,0 +1,47 @@
+package org.checkerframework.checker.optional;
+
+import java.util.NavigableSet;
+import java.util.Optional;
+import java.util.Set;
+import org.checkerframework.common.aliasing.AliasingChecker;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.framework.qual.RelevantJavaTypes;
+import org.checkerframework.framework.qual.StubFiles;
+import org.checkerframework.framework.source.SourceChecker;
+import org.checkerframework.framework.source.SupportedOptions;
+
+/**
+ * The implementation of a type-checker that prevents misuse of the {@link java.util.Optional}
+ * class.
+ *
+ * @checker_framework.manual #optional-checker Optional Checker
+ */
+// TODO: For a call to `@Optional#ofNullable`, if the argument has type
+// @NonNull, make the return type have type @Present.
+@RelevantJavaTypes(Optional.class)
+@StubFiles({"javaparser.astub"})
+@SupportedOptions("optionalMapAssumeNonNull")
+public class OptionalImplChecker extends BaseTypeChecker {
+  /** Create an OptionalImplChecker. */
+  public OptionalImplChecker() {}
+
+  @Override
+  protected Set<Class<? extends SourceChecker>> getImmediateSubcheckerClasses() {
+    Set<Class<? extends SourceChecker>> subcheckers = super.getImmediateSubcheckerClasses();
+    subcheckers.add(AliasingChecker.class);
+    return subcheckers;
+  }
+
+  /**
+   * Use the "optional", rather than the "optionalimpl" prefix as the argument to a {@link
+   * SuppressWarnings} annotation,
+   *
+   * @return the set of suppress warnings prefixes that are respected by this checker
+   */
+  @Override
+  public NavigableSet<String> getSuppressWarningsPrefixes() {
+    NavigableSet<String> prefixes = super.getSuppressWarningsPrefixes();
+    prefixes.add("optional");
+    return prefixes;
+  }
+}