diff --git a/checker/src/main/java/org/checkerframework/checker/optional/OptionalAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/optional/OptionalAnnotatedTypeFactory.java
new file mode 100644
index 00000000000..8abd6f4e5b6
--- /dev/null
+++ b/checker/src/main/java/org/checkerframework/checker/optional/OptionalAnnotatedTypeFactory.java
@@ -0,0 +1,133 @@
+package org.checkerframework.checker.optional;
+
+import com.sun.source.tree.ExpressionTree;
+import com.sun.source.tree.MemberReferenceTree;
+import com.sun.source.tree.MethodInvocationTree;
+import com.sun.source.tree.Tree;
+import com.sun.source.tree.Tree.Kind;
+import java.util.Collection;
+import java.util.function.Function;
+import javax.lang.model.element.AnnotationMirror;
+import javax.lang.model.element.ElementKind;
+import javax.lang.model.element.ExecutableElement;
+import org.checkerframework.checker.optional.qual.Present;
+import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.framework.flow.CFAbstractAnalysis;
+import org.checkerframework.framework.flow.CFStore;
+import org.checkerframework.framework.flow.CFTransfer;
+import org.checkerframework.framework.flow.CFValue;
+import org.checkerframework.framework.type.AnnotatedTypeMirror;
+import org.checkerframework.javacutil.AnnotationBuilder;
+import org.checkerframework.javacutil.TreeUtils;
+
+/** OptionalAnnotatedTypeFactory for the Optional Checker. */
+public class OptionalAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
+
+ /** The element for java.util.Optional.map(). */
+ private final ExecutableElement optionalMap;
+
+ /** The @{@link Present} annotation. */
+ protected final AnnotationMirror PRESENT = AnnotationBuilder.fromClass(elements, Present.class);
+
+ /**
+ * Creates an OptionalAnnotatedTypeFactory.
+ *
+ * @param checker the Optional Checker associated with this type factory
+ */
+ public OptionalAnnotatedTypeFactory(BaseTypeChecker checker) {
+ super(checker);
+ postInit();
+ optionalMap = TreeUtils.getMethodOrNull("java.util.Optional", "map", 1, getProcessingEnv());
+ }
+
+ @Override
+ public AnnotatedTypeMirror getAnnotatedType(Tree tree) {
+ AnnotatedTypeMirror result = super.getAnnotatedType(tree);
+ optionalMapNonNull(tree, result);
+ return result;
+ }
+
+ /**
+ * If {@code tree} is a call to {@link java.util.Optional#map(Function)} whose argument is a
+ * method reference, then this method adds {@code @Present} to {@code type} if the following is
+ * true:
+ *
+ *
+ * - The type of the receiver to {@link java.util.Optional#map(Function)} is {@code @Present},
+ * and
+ *
- {@link #returnHasNullable(MemberReferenceTree)} returns false.
+ *
+ *
+ * @param tree a tree
+ * @param type the type of the tree, which may be side-effected by this method
+ */
+ private void optionalMapNonNull(Tree tree, AnnotatedTypeMirror type) {
+ if (!TreeUtils.isMethodInvocation(tree, optionalMap, processingEnv)) {
+ return;
+ }
+ MethodInvocationTree mapTree = (MethodInvocationTree) tree;
+ ExpressionTree argTree = mapTree.getArguments().get(0);
+ if (argTree.getKind() == Kind.MEMBER_REFERENCE) {
+ MemberReferenceTree memberReferenceTree = (MemberReferenceTree) argTree;
+ AnnotatedTypeMirror optType = getReceiverType(mapTree);
+ if (optType == null || !optType.hasEffectiveAnnotation(Present.class)) {
+ return;
+ }
+ if (!returnHasNullable(memberReferenceTree)) {
+ // The method still could have a @PolyNull on the return and might return null.
+ // If @PolyNull is the primary annotation on the parameter and not on any type arguments or
+ // array elements, then it is still safe to mark the optional type as present.
+ // TODO: Add the check for poly null on arguments.
+ type.replaceAnnotation(PRESENT);
+ }
+ }
+ }
+
+ /**
+ * Returns true if the return type of the function type of {@code memberReferenceTree} is
+ * annotated with {@code @Nullable}.
+ *
+ * @param memberReferenceTree a member reference
+ * @return true if the return type of the function type of {@code memberReferenceTree} is
+ * annotated with {@code @Nullable}
+ */
+ private boolean returnHasNullable(MemberReferenceTree memberReferenceTree) {
+ if (TreeUtils.MemberReferenceKind.getMemberReferenceKind(memberReferenceTree)
+ .isConstructorReference()) {
+ return false;
+ }
+ ExecutableElement memberReferenceFuncType = TreeUtils.elementFromUse(memberReferenceTree);
+ if (memberReferenceFuncType.getEnclosingElement().getKind() == ElementKind.ANNOTATION_TYPE) {
+ // Annotation element accessor are always non-null;
+ return false;
+ }
+
+ if (!checker.hasOption("optionalMapAssumeNonNull")) {
+ return true;
+ }
+ return containsNullable(memberReferenceFuncType.getAnnotationMirrors())
+ || containsNullable(memberReferenceFuncType.getReturnType().getAnnotationMirrors());
+ }
+
+ /**
+ * Returns true if {@code annos} contains a nullable annotation.
+ *
+ * @param annos a collection of annotations
+ * @return true if {@code annos} contains a nullable annotation
+ */
+ private boolean containsNullable(Collection extends AnnotationMirror> annos) {
+ for (AnnotationMirror anno : annos) {
+ if (anno.getAnnotationType().asElement().getSimpleName().contentEquals("Nullable")) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ @Override
+ public CFTransfer createFlowTransferFunction(
+ CFAbstractAnalysis analysis) {
+ return new OptionalTransfer(analysis);
+ }
+}
diff --git a/checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.java b/checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.java
index 2cf7131ee9d..1c6db443bef 100644
--- a/checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.java
+++ b/checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.java
@@ -4,6 +4,7 @@
import org.checkerframework.common.basetype.BaseTypeChecker;
import org.checkerframework.framework.qual.RelevantJavaTypes;
import org.checkerframework.framework.qual.StubFiles;
+import org.checkerframework.framework.source.SupportedOptions;
/**
* A type-checker that prevents misuse of the {@link java.util.Optional} class.
@@ -14,6 +15,7 @@
// @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 OptionalChecker() {}
diff --git a/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java b/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java
index 4f3f6ca6860..badf2484cdf 100644
--- a/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java
+++ b/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java
@@ -18,9 +18,10 @@
import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGLambda;
import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
import org.checkerframework.dataflow.expression.JavaExpression;
-import org.checkerframework.framework.flow.CFAnalysis;
+import org.checkerframework.framework.flow.CFAbstractAnalysis;
import org.checkerframework.framework.flow.CFStore;
import org.checkerframework.framework.flow.CFTransfer;
+import org.checkerframework.framework.flow.CFValue;
import org.checkerframework.framework.type.AnnotatedTypeFactory;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.TreeUtils;
@@ -45,7 +46,7 @@ public class OptionalTransfer extends CFTransfer {
*
* @param analysis the Optional Checker instance
*/
- public OptionalTransfer(CFAnalysis analysis) {
+ public OptionalTransfer(CFAbstractAnalysis analysis) {
super(analysis);
atypeFactory = analysis.getTypeFactory();
Elements elements = atypeFactory.getElementUtils();
diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/OptionalTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/OptionalTest.java
index 6f96b48e0c7..ee2087f2303 100644
--- a/checker/src/test/java/org/checkerframework/checker/test/junit/OptionalTest.java
+++ b/checker/src/test/java/org/checkerframework/checker/test/junit/OptionalTest.java
@@ -14,7 +14,11 @@ public class OptionalTest extends CheckerFrameworkPerDirectoryTest {
* @param testFiles the files containing test code, which will be type-checked
*/
public OptionalTest(List testFiles) {
- super(testFiles, org.checkerframework.checker.optional.OptionalChecker.class, "optional");
+ super(
+ testFiles,
+ org.checkerframework.checker.optional.OptionalChecker.class,
+ "optional",
+ "-AoptionalMapAssumeNonNull");
}
@Parameters
diff --git a/checker/tests/optional/MapNoNewNull.java b/checker/tests/optional/MapNoNewNull.java
new file mode 100644
index 00000000000..f9148ee235b
--- /dev/null
+++ b/checker/tests/optional/MapNoNewNull.java
@@ -0,0 +1,16 @@
+import java.math.BigInteger;
+import java.util.Optional;
+
+class MapNoNewNull {
+
+ @SuppressWarnings("optional.parameter")
+ void m(Optional digitsAnnotation) {
+ if (digitsAnnotation.isPresent()) {
+ BigInteger maxValue = digitsAnnotation.map(Digits::integer).map(BigInteger::valueOf).get();
+ }
+ }
+}
+
+@interface Digits {
+ public int integer();
+}
diff --git a/checker/tests/optional/OptionalMapMethodReference.java b/checker/tests/optional/OptionalMapMethodReference.java
new file mode 100644
index 00000000000..85642d9e9c9
--- /dev/null
+++ b/checker/tests/optional/OptionalMapMethodReference.java
@@ -0,0 +1,34 @@
+import java.util.Optional;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.nullness.qual.PolyNull;
+import org.checkerframework.checker.optional.qual.Present;
+
+public class OptionalMapMethodReference {
+ Optional getString() {
+ return Optional.of("");
+ }
+
+ @Present Optional method() {
+ Optional o = getString();
+ @Present Optional oInt;
+ if (o.isPresent()) {
+ // :: error: (assignment)
+ oInt = o.map(this::convertNull);
+ oInt = o.map(this::convertPoly);
+ return o.map(this::convert);
+ }
+ return Optional.of(0);
+ }
+
+ @Nullable Integer convertNull(String s) {
+ return null;
+ }
+
+ @PolyNull Integer convertPoly(@PolyNull String s) {
+ return null;
+ }
+
+ Integer convert(String s) {
+ return 0;
+ }
+}
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java
index 2258e288dc5..e9d575476ae 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java
@@ -1931,6 +1931,15 @@ public boolean isUnbound() {
return unbound;
}
+ /**
+ * Returns whether this kind is a constructor reference.
+ *
+ * @return whether this kind is a constructor reference
+ */
+ public boolean isConstructorReference() {
+ return mode == ReferenceMode.NEW;
+ }
+
/**
* Returns the kind of member reference {@code tree} is.
*