Add @NonNullIfReturn: parameter-level conditional postcondition for nullness

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

@@ -0,0 +1,82 @@
+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: expresses that the parameter is non-null when the method returns the
+ * given value.
+ *
+ * <p><b>Semantic meaning:</b> {@code @NonNullIfReturns(v)} means: <i>this parameter is non-null
+ * when the method returns v</i>. That is: {@code method returns value() ⇒ parameter != null}.
+ *
+ * <p>This annotation only makes sense on parameters whose root type is {@code @Nullable} or
+ * parametric. The checker refines the parameter's type to {@code @NonNull} in code paths where the
+ * method's return value is known (e.g., inside {@code if (method(arg))} or {@code if
+ * (!method(arg))} blocks).
+ *
+ * <p><b>Example 1: hasLength</b> — param is non-null when method returns true.
+ *
+ * <pre>{@code
+ * public static boolean hasLength(@NonNullIfReturns(true) @Nullable String str) {
+ *   return (str != null && !str.isEmpty());
+ * }
+ * }</pre>
+ *
+ * When {@code hasLength(s)} returns true, {@code s} was non-null.
+ *
+ * <p><b>Example 2: equals</b> — param is non-null when method returns true.
+ *
+ * <pre>{@code
+ * @Override
+ * public boolean equals(@NonNullIfReturns(true) @Nullable Object other) {
+ *   return this == other;
+ * }
+ * }</pre>
+ *
+ * <p><b>Example 3: isNull</b> — param is non-null when method returns false.
+ *
+ * <pre>{@code
+ * public static boolean isNull(@NonNullIfReturns(false) @Nullable Object obj) {
+ *   return obj == null;
+ * }
+ * }</pre>
+ *
+ * When {@code isNull(obj)} returns false, {@code obj} was non-null.
+ *
+ * <ul>
+ *   <li><b>Scope:</b> The annotation applies only to the parameter on which it is written.
+ *   <li><b>Meaning:</b> {@code @NonNullIfReturns(v)} means: param is non-null when method returns
+ *       v.
+ *   <li><b>Target:</b> Only formal parameters.
+ * </ul>
+ *
+ * <p>For a fixed return value, use {@link NonNullIfReturnsTrue} or {@link NonNullIfReturnsFalse}
+ * instead.
+ *
+ * @see NonNullIfReturnsTrue
+ * @see NonNullIfReturnsFalse
+ * @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 NonNullIfReturns {
+    /**
+     * The return value under which the parameter is non-null.
+     *
+     * @return the return value under which the parameter has the qualifier (e.g., {@code true} for
+     *     {@code hasLength}, {@code false} for {@code isNull})
+     */
+    boolean value();
+}

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

@@ -0,0 +1,24 @@
+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: the parameter is non-null when the method returns {@code false}.
+ *
+ * <p>Equivalent to {@code @NonNullIfReturns(false)} but with a fixed value for use when the return
+ * condition is always false (e.g. {@code isNull}).
+ *
+ * @see NonNullIfReturns
+ * @see NonNullIfReturnsTrue
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.PARAMETER})
+@ParameterConditionalPostconditionAnnotation(qualifier = NonNull.class, result = false)
+public @interface NonNullIfReturnsFalse {}

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

@@ -0,0 +1,24 @@
+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: the parameter is non-null when the method returns {@code true}.
+ *
+ * <p>Equivalent to {@code @NonNullIfReturns(true)} but with a fixed value for use when the return
+ * condition is always true (e.g. {@code hasLength}, {@code equals}).
+ *
+ * @see NonNullIfReturns
+ * @see NonNullIfReturnsFalse
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.PARAMETER})
+@ParameterConditionalPostconditionAnnotation(qualifier = NonNull.class, result = true)
+public @interface NonNullIfReturnsTrue {}

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

@@ -0,0 +1,60 @@
+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 either has a single element {@code value()} of type {@code boolean} with the same meaning as
+ * {@link EnsuresQualifierIf#result()}, or E has no such element and the result is fixed by this
+ * meta-annotation's {@link #result()} (for concrete annotations like
+ * {@code @NonNullIfReturnsTrue}). The expression to which the qualifier applies is implicit: it is
+ * the annotated parameter (e.g. {@code "#1"} for the first parameter).
+ *
+ * <p>For example, the nullness checker defines {@link
+ * org.checkerframework.checker.nullness.qual.NonNullIfReturns}:
+ *
+ * <pre><code>
+ * {@literal @}ParameterConditionalPostconditionAnnotation(qualifier = NonNull.class)
+ * {@literal @}Target(ElementType.PARAMETER)
+ * public {@literal @}interface NonNullIfReturns {
+ *   boolean value();
+ * }
+ * </code></pre>
+ *
+ * <p>Usage: {@code @NonNullIfReturns(true)} or {@code @NonNullIfReturnsTrue} means the parameter is
+ * non-null when the method returns true; {@code @NonNullIfReturns(false)} or
+ * {@code @NonNullIfReturnsFalse} when it returns false.
+ *
+ * @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, or by this {@link
+     * #result()} when the annotation has no {@code value()} (e.g. {@code @NonNullIfReturnsTrue}).
+     *
+     * @return the qualifier
+     */
+    Class<? extends Annotation> qualifier();
+
+    /**
+     * The return value under which the qualifier holds. Used when the concrete annotation has no
+     * {@code value()} element (e.g. {@code @NonNullIfReturnsTrue} /
+     * {@code @NonNullIfReturnsFalse}). Ignored when the concrete annotation has {@code value()}.
+     *
+     * @return true if the qualifier holds when the method returns true, false when it returns false
+     */
+    boolean result() default true;
+}

checker/tests/nullness/NonNullIfReturnsTest.java

@@ -0,0 +1,162 @@
+// Tests @NonNullIfReturns, @NonNullIfReturnsTrue, and @NonNullIfReturnsFalse (parameter-level
+// conditional postconditions) for both correct refinement and expected errors.
+
+import org.checkerframework.checker.nullness.qual.NonNull;
+import org.checkerframework.checker.nullness.qual.NonNullIfReturns;
+import org.checkerframework.checker.nullness.qual.NonNullIfReturnsFalse;
+import org.checkerframework.checker.nullness.qual.NonNullIfReturnsTrue;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class NonNullIfReturnsTest {
+
+    // -----------------------------------------------------------------------
+    // @NonNullIfReturns(true) / (false)
+    // -----------------------------------------------------------------------
+
+    public static boolean hasLength(@NonNullIfReturns(true) @Nullable String str) {
+        return (str != null && !str.isEmpty());
+    }
+
+    void useHasLength(@Nullable String s) {
+        if (hasLength(s)) {
+            @NonNull String n = s;
+            n.hashCode();
+        } else {
+            // :: error: (assignment.type.incompatible)
+            @NonNull String n = s;
+        }
+    }
+
+    @Override
+    public boolean equals(@NonNullIfReturns(true) @Nullable Object other) {
+        return this == other;
+    }
+
+    void useEquals(NonNullIfReturnsTest a, @Nullable Object b) {
+        if (a.equals(b)) {
+            @NonNull Object n = b;
+            n.hashCode();
+        }
+    }
+
+    public static boolean isNull(@NonNullIfReturns(false) @Nullable Object obj) {
+        return obj == null;
+    }
+
+    void useIsNull(@Nullable Object p) {
+        if (!isNull(p)) {
+            @NonNull Object n = p;
+            n.hashCode();
+        } else {
+            // :: error: (assignment.type.incompatible)
+            @NonNull Object n = p;
+        }
+    }
+
+    public static boolean bothNonNull(
+            @NonNullIfReturns(true) @Nullable Object a,
+            @NonNullIfReturns(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;
+            @NonNull Object ny = y;
+            nx.hashCode();
+            ny.hashCode();
+        } else {
+            // :: error: (assignment.type.incompatible)
+            @NonNull Object nx = x;
+            // :: error: (assignment.type.incompatible)
+            @NonNull Object ny = y;
+        }
+    }
+
+    // Checker trusts the annotation; does not verify method body.
+    public boolean alwaysTrue(@NonNullIfReturns(true) @Nullable Object obj) {
+        return true;
+    }
+
+    void useAlwaysTrue(@Nullable Object p) {
+        if (alwaysTrue(p)) {
+            @NonNull Object n = p;
+            n.hashCode();
+        } else {
+            // :: error: (assignment.type.incompatible)
+            @NonNull Object n = p;
+        }
+    }
+
+    // -----------------------------------------------------------------------
+    // @NonNullIfReturnsTrue
+    // -----------------------------------------------------------------------
+
+    public static boolean hasLengthTrue(@NonNullIfReturnsTrue @Nullable String str) {
+        return (str != null && !str.isEmpty());
+    }
+
+    void useHasLengthTrue(@Nullable String s) {
+        if (hasLengthTrue(s)) {
+            @NonNull String n = s;
+            n.hashCode();
+        } else {
+            // :: error: (assignment.type.incompatible)
+            @NonNull String n = s;
+        }
+    }
+
+    public static boolean bothNonNullTrue(
+            @NonNullIfReturnsTrue @Nullable Object a, @NonNullIfReturnsTrue @Nullable Object b) {
+        return a != null && b != null;
+    }
+
+    void useBothNonNullTrue(@Nullable Object x, @Nullable Object y) {
+        if (bothNonNullTrue(x, y)) {
+            @NonNull Object nx = x;
+            @NonNull Object ny = y;
+            nx.hashCode();
+        } else {
+            // :: error: (assignment.type.incompatible)
+            @NonNull Object nx = x;
+            // :: error: (assignment.type.incompatible)
+            @NonNull Object ny = y;
+        }
+    }
+
+    // -----------------------------------------------------------------------
+    // @NonNullIfReturnsFalse
+    // -----------------------------------------------------------------------
+
+    public static boolean isNullFalse(@NonNullIfReturnsFalse @Nullable Object obj) {
+        return obj == null;
+    }
+
+    void useIsNullFalse(@Nullable Object p) {
+        if (!isNullFalse(p)) {
+            @NonNull Object n = p;
+            n.hashCode();
+        } else {
+            // :: error: (assignment.type.incompatible)
+            @NonNull Object n = p;
+        }
+    }
+
+    public static boolean neitherNull(
+            @NonNullIfReturnsFalse @Nullable Object a, @NonNullIfReturnsFalse @Nullable Object b) {
+        return a == null || b == null;
+    }
+
+    void useNeitherNull(@Nullable Object x, @Nullable Object y) {
+        if (!neitherNull(x, y)) {
+            @NonNull Object nx = x;
+            @NonNull Object ny = y;
+            nx.hashCode();
+        } else {
+            // :: 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/common/basetype/messages.properties

@@ -95,6 +95,7 @@ contracts.precondition.not.satisfied=precondition of %s is not satisfied.%nfound
 contracts.postcondition.not.satisfied=postcondition of %s is not satisfied.%nfound   : %s%nrequired: %s
 contracts.conditional.postcondition.not.satisfied=conditional postcondition is not satisfied when %s returns %s.%nfound   : %s%nrequired: %s
 contracts.conditional.postcondition.invalid.returntype=this annotation is only valid for methods with return type 'boolean'
+contracts.parameter.conditional.qualifier.not.supported=parameter conditional postcondition annotation %s uses a qualifier that is not supported by the current checker
 # Same text for "override" and "methodref", but different key.
 contracts.precondition.override.invalid=Subclass precondition is stronger for '%s' in %s.%n  In superclass %s: %s%n  In subclass %s: %s
 contracts.postcondition.override.invalid=Subclass postcondition is weaker for '%s' in %s.%n  In superclass %s: %s%n  In subclass %s: %s