Add @NonNullIfReturn: parameter-level conditional postcondition for nullness

checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturn.java

@@ -0,0 +1,107 @@
+package org.checkerframework.checker.nullness.qual;
+
+import org.checkerframework.framework.qual.ParameterConditionalPostconditionAnnotation;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * A <b>parameter</b> contract: indicates that the annotated parameter is guaranteed to be non-null
+ * when the method returns the given boolean value.
+ *
+ * <p>This is the parameter-level analogue of {@link EnsuresNonNullIf}. It expresses the same
+ * conditional postcondition (this parameter is non-null if the method returns {@code value()}) but
+ * is written on the parameter instead of the method, so no expression string like {@code "#1"} is
+ * needed.
+ *
+ * <p><b>Example 1: Simple null check</b>
+ *
+ * <pre>{@code
+ * public static boolean isNonNull(
+ *     @NonNullIfReturn(true) @Nullable Object obj
+ * ) {
+ *   return obj != null;
+ * }
+ * }</pre>
+ *
+ * If {@code isNonNull(obj)} returns {@code true}, then {@code obj} is non-null after the call.
+ * Equivalent to the method-level contract {@code @EnsuresNonNullIf(expression="#1", result=true)}.
+ *
+ * <p><b>Example 2: equals(Object)</b>
+ *
+ * <pre>{@code
+ * @Override
+ * public boolean equals(
+ *     @NonNullIfReturn(true) @Nullable Object other
+ * ) {
+ *   ...
+ * }
+ * }</pre>
+ *
+ * If {@code equals(other)} returns {@code true}, then {@code other} was non-null.
+ *
+ * <p><b>Example 3: Negative return value</b>
+ *
+ * <pre>{@code
+ * public static boolean isNull(
+ *     @NonNullIfReturn(false) @Nullable Object obj
+ * ) {
+ *   return obj == null;
+ * }
+ * }</pre>
+ *
+ * If {@code isNull(obj)} returns {@code false}, then {@code obj} is non-null.
+ *
+ * <p><b>Example 4: Multiple parameters</b>
+ *
+ * <pre>{@code
+ * public static boolean bothNonNull(
+ *     @NonNullIfReturn(true) @Nullable Object a,
+ *     @NonNullIfReturn(true) @Nullable Object b
+ * ) {
+ *   return a != null && b != null;
+ * }
+ * }</pre>
+ *
+ * If the method returns {@code true}, then {@code a} is non-null and {@code b} is non-null. Each
+ * parameter's annotation contributes independently.
+ *
+ * <ul>
+ *   <li><b>Scope:</b> The annotation applies only to the parameter on which it is written. The
+ *       "expression" of the contract is implicitly that parameter (e.g. the first parameter is
+ *       {@code "#1"}).
+ *   <li><b>Meaning:</b> For a call {@code m(...)} that returns {@code v}, if {@code v} equals the
+ *       annotation's {@code value()}, then the Nullness Checker treats the corresponding argument
+ *       as {@link NonNull} at program points after the call (in the same way as for {@link
+ *       EnsuresNonNullIf} with {@code expression="#n"} and {@code result=value()}).
+ *   <li><b>One-way guarantee:</b> No converse implication is assumed. For example,
+ *       {@code @NonNullIfReturn(true)} does not imply that when the method returns {@code false},
+ *       the parameter is null.
+ *   <li><b>Target:</b> Only formal parameters. Putting this annotation on a method or field is a
+ *       misuse and may be rejected by the checker or ignored.
+ * </ul>
+ *
+ * @see EnsuresNonNullIf
+ * @see NonNull
+ * @see Nullable
+ * @see org.checkerframework.checker.nullness.NullnessChecker
+ * @checker_framework.manual #nullness-checker Nullness Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.PARAMETER})
+@ParameterConditionalPostconditionAnnotation(qualifier = NonNull.class)
+public @interface NonNullIfReturn {
+    /**
+     * The return value of the method under which the annotated parameter is guaranteed to be
+     * non-null.
+     *
+     * @return the return value under which the parameter is non-null (typically {@code true} for
+     *     methods like {@code equals} or {@code isNonNull}, or {@code false} for methods like
+     *     {@code isNull})
+     */
+    boolean value();
+}

checker-qual/src/main/java/org/checkerframework/framework/qual/ParameterConditionalPostconditionAnnotation.java

@@ -0,0 +1,58 @@
+package org.checkerframework.framework.qual;
+
+import java.lang.annotation.Annotation;
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * A meta-annotation that indicates that an annotation E is a <b>parameter</b> conditional
+ * postcondition annotation: E is written on a formal parameter and expresses that the annotated
+ * parameter has a given qualifier when the method returns a given boolean value.
+ *
+ * <p>E must have a single element {@code value()} of type {@code boolean} with the same meaning as
+ * {@link EnsuresQualifierIf#result()}. The expression to which the qualifier applies is implicit:
+ * it is the annotated parameter (e.g. {@code "#1"} for the first parameter).
+ *
+ * <p>This is the parameter-level analogue of {@link ConditionalPostconditionAnnotation}. It allows
+ * expressing conditional postconditions on parameters without putting the contract on the method
+ * and without using expression strings like {@code "#1"}.
+ *
+ * <p>For example, the nullness checker defines:
+ *
+ * <pre><code>
+ * {@literal @}ParameterConditionalPostconditionAnnotation(qualifier = NonNull.class)
+ * {@literal @}Target(ElementType.PARAMETER)
+ * public {@literal @}interface NonNullIfReturn {
+ *   boolean value();
+ * }
+ * </code></pre>
+ *
+ * <p>Usage:
+ *
+ * <pre><code>
+ * public boolean equals(
+ *     {@literal @}NonNullIfReturn(true) {@literal @}Nullable Object other
+ * ) { ... }
+ * </code></pre>
+ *
+ * <p>This is equivalent to the method-level contract {@code @EnsuresNonNullIf(expression="#1",
+ * result=true)} on the method.
+ *
+ * @see ConditionalPostconditionAnnotation
+ * @see EnsuresQualifierIf
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.ANNOTATION_TYPE})
+public @interface ParameterConditionalPostconditionAnnotation {
+    /**
+     * The qualifier that is established on the annotated parameter when the method returns the
+     * value specified by the parameter annotation's {@code value()} element.
+     *
+     * @return the qualifier
+     */
+    Class<? extends Annotation> qualifier();
+}

checker/tests/nullness/NonNullIfReturnTest.java

@@ -0,0 +1,76 @@
+// Test that @NonNullIfReturn (parameter-level conditional postcondition) is respected by the
+// Nullness Checker. Same semantics as @EnsuresNonNullIf(expression="#1", result=true) on the
+// method, but written on the parameter.
+
+import org.checkerframework.checker.nullness.qual.NonNull;
+import org.checkerframework.checker.nullness.qual.NonNullIfReturn;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class NonNullIfReturnTest {
+
+    // Example 1: Simple null check (equivalent to @EnsuresNonNullIf(expression="#1", result=true))
+    public static boolean isNonNull(@NonNullIfReturn(true) @Nullable Object obj) {
+        return obj != null;
+    }
+
+    void useIsNonNull(@Nullable Object p) {
+        if (isNonNull(p)) {
+            @NonNull Object n = p; // OK: p is non-null when isNonNull returns true
+            n.hashCode(); // use n
+        } else {
+            // Contract does not apply: when isNonNull returns false, p may be null.
+            // :: error: (assignment.type.incompatible)
+            @NonNull Object n = p;
+        }
+    }
+
+    // Example 2: equals (parameter is non-null when return is true)
+    @Override
+    public boolean equals(@NonNullIfReturn(true) @Nullable Object other) {
+        return this == other;
+    }
+
+    void useEquals(NonNullIfReturnTest a, @Nullable Object b) {
+        if (a.equals(b)) {
+            @NonNull Object n = b; // OK: b is non-null when equals returns true
+            n.hashCode(); // use n
+        }
+    }
+
+    // Example 3: Negative return value (parameter is non-null when return is false)
+    public static boolean isNull(@NonNullIfReturn(false) @Nullable Object obj) {
+        return obj == null;
+    }
+
+    void useIsNull(@Nullable Object p) {
+        if (!isNull(p)) {
+            @NonNull Object n = p; // OK: p is non-null when isNull returns false
+            n.hashCode(); // use n
+        } else {
+            // Contract does not apply: when isNull returns true, p is null.
+            // :: error: (assignment.type.incompatible)
+            @NonNull Object n = p;
+        }
+    }
+
+    // Example 4: Multiple parameters
+    public static boolean bothNonNull(
+            @NonNullIfReturn(true) @Nullable Object a, @NonNullIfReturn(true) @Nullable Object b) {
+        return a != null && b != null;
+    }
+
+    void useBothNonNull(@Nullable Object x, @Nullable Object y) {
+        if (bothNonNull(x, y)) {
+            @NonNull Object nx = x; // OK
+            @NonNull Object ny = y; // OK
+            nx.hashCode();
+            ny.hashCode();
+        } else {
+            // Contract does not apply: when bothNonNull returns false, x or y may be null.
+            // :: error: (assignment.type.incompatible)
+            @NonNull Object nx = x;
+            // :: error: (assignment.type.incompatible)
+            @NonNull Object ny = y;
+        }
+    }
+}

docs/manual/contributors.tex

@@ -51,6 +51,7 @@
 Hamed Taghani,
 Hannes Greule,
 Heath Borders,
+Henry Xi,
 Ivory Wang,
 Jakub Vr\'ana,
 James Yoo,

framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java

@@ -4,6 +4,7 @@
 import org.checkerframework.framework.qual.ConditionalPostconditionAnnotation;
 import org.checkerframework.framework.qual.EnsuresQualifier;
 import org.checkerframework.framework.qual.EnsuresQualifierIf;
+import org.checkerframework.framework.qual.ParameterConditionalPostconditionAnnotation;
 import org.checkerframework.framework.qual.PostconditionAnnotation;
 import org.checkerframework.framework.qual.PreconditionAnnotation;
 import org.checkerframework.framework.qual.QualifierArgument;
@@ -20,11 +21,13 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
+import java.util.concurrent.ConcurrentHashMap;
 
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.Element;
 import javax.lang.model.element.ExecutableElement;
 import javax.lang.model.element.Name;
+import javax.lang.model.element.VariableElement;
 import javax.lang.model.util.ElementFilter;
 
 /**
@@ -36,6 +39,7 @@
  * @see EnsuresQualifier
  * @see ConditionalPostconditionAnnotation
  * @see EnsuresQualifierIf
+ * @see ParameterConditionalPostconditionAnnotation
  */
 // TODO: This class assumes that most annotations have a field named "expression". If not, issue a
 // more helpful error message.
@@ -47,6 +51,14 @@ public class DefaultContractsFromMethod implements ContractsFromMethod {
     /** The factory that this ContractsFromMethod is associated with. */
     protected final GenericAnnotatedTypeFactory<?, ?, ?, ?> atypeFactory;
 
+    /**
+     * Cache for conditional postconditions. Methods like {@code equals} or {@code hasNext} may be
+     * invoked many times; caching avoids re-iterating parameters and re-scanning annotations on
+     * each invocation.
+     */
+    private final Map<ExecutableElement, Set<Contract.ConditionalPostcondition>>
+            conditionalPostconditionCache = new ConcurrentHashMap<>();
+
     /**
      * Creates a ContractsFromMethod for the given factory.
      *
@@ -107,10 +119,13 @@ public Set<Contract.Postcondition> getPostconditions(ExecutableElement executabl
     @Override
     public Set<Contract.ConditionalPostcondition> getConditionalPostconditions(
             ExecutableElement methodElement) {
-        return getContractsOfKind(
+        return conditionalPostconditionCache.computeIfAbsent(
                 methodElement,
-                Contract.Kind.CONDITIONALPOSTCONDITION,
-                Contract.ConditionalPostcondition.class);
+                elem ->
+                        getContractsOfKind(
+                                elem,
+                                Contract.Kind.CONDITIONALPOSTCONDITION,
+                                Contract.ConditionalPostcondition.class));
     }
 
     // Helper methods
@@ -181,6 +196,41 @@ private <T extends Contract> Set<T> getContractsOfKind(
                 result.add(contract);
             }
         }
+
+        // Gather conditional postconditions from parameter-level annotations (e.g.
+        // @NonNullIfReturn).
+        if (kind == Contract.Kind.CONDITIONALPOSTCONDITION) {
+            List<? extends VariableElement> params = executableElement.getParameters();
+            for (int i = 0; i < params.size(); i++) {
+                VariableElement param = params.get(i);
+                List<IPair<AnnotationMirror, AnnotationMirror>> paramAnnotations =
+                        atypeFactory.getDeclAnnotationWithMetaAnnotation(
+                                param, ParameterConditionalPostconditionAnnotation.class);
+                for (IPair<AnnotationMirror, AnnotationMirror> r : paramAnnotations) {
+                    AnnotationMirror paramAnnotation = r.first;
+                    AnnotationMirror metaAnnotation = r.second;
+                    AnnotationMirror enforcedQualifier =
+                            getQualifierEnforcedByContractAnnotation(metaAnnotation, null, null);
+                    if (enforcedQualifier == null) {
+                        continue;
+                    }
+                    @SuppressWarnings("deprecation") // permitted for use in the framework
+                    Boolean resultValue =
+                            AnnotationUtils.getElementValue(
+                                    paramAnnotation, "value", Boolean.class, true);
+                    String expressionString = "#" + (i + 1);
+                    T contract =
+                            clazz.cast(
+                                    Contract.create(
+                                            kind,
+                                            expressionString,
+                                            enforcedQualifier,
+                                            paramAnnotation,
+                                            resultValue));
+                    result.add(contract);
+                }
+            }
+        }
         return result;
     }