From c20f8ae7db61f1ee09c5a31b4624dd8745f28616 Mon Sep 17 00:00:00 2001 From: Henry Xi Date: Tue, 10 Feb 2026 13:28:07 -0500 Subject: [PATCH 1/6] Add @NonNullIfReturn parameter annotation for conditional nullness --- .../nullness/qual/NonNullIfReturn.java | 107 ++++++++++++++++++ ...terConditionalPostconditionAnnotation.java | 58 ++++++++++ .../tests/nullness/NonNullIfReturnTest.java | 76 +++++++++++++ .../util/DefaultContractsFromMethod.java | 47 ++++++++ 4 files changed, 288 insertions(+) create mode 100644 checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturn.java create mode 100644 checker-qual/src/main/java/org/checkerframework/framework/qual/ParameterConditionalPostconditionAnnotation.java create mode 100644 checker/tests/nullness/NonNullIfReturnTest.java diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturn.java b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturn.java new file mode 100644 index 000000000000..e7a2ff1681b4 --- /dev/null +++ b/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 parameter contract: indicates that the annotated parameter is guaranteed to be non-null + * when the method returns the given boolean value. + * + *

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. + * + *

Example 1: Simple null check + * + * 

{@code
+ * public static boolean isNonNull(
+ *     @NonNullIfReturn(true) @Nullable Object obj
+ * ) {
+ *   return obj != null;
+ * }
+ * }
+ * + * 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)}. + * + *

Example 2: equals(Object) + * + * 

{@code
+ * @Override
+ * public boolean equals(
+ *     @NonNullIfReturn(true) @Nullable Object other
+ * ) {
+ *   ...
+ * }
+ * }
+ * + * If {@code equals(other)} returns {@code true}, then {@code other} was non-null. + * + *

Example 3: Negative return value + * + * 

{@code
+ * public static boolean isNull(
+ *     @NonNullIfReturn(false) @Nullable Object obj
+ * ) {
+ *   return obj == null;
+ * }
+ * }
+ * + * If {@code isNull(obj)} returns {@code false}, then {@code obj} is non-null. + * + *

Example 4: Multiple parameters + * + * 

{@code
+ * public static boolean bothNonNull(
+ *     @NonNullIfReturn(true) @Nullable Object a,
+ *     @NonNullIfReturn(true) @Nullable Object b
+ * ) {
+ *   return a != null && b != null;
+ * }
+ * }
+ * + * If the method returns {@code true}, then {@code a} is non-null and {@code b} is non-null. Each + * parameter's annotation contributes independently. + * + * + * + * @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(); +} diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/ParameterConditionalPostconditionAnnotation.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/ParameterConditionalPostconditionAnnotation.java new file mode 100644 index 000000000000..bac37373bd48 --- /dev/null +++ b/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 parameter 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. + * + *

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). + * + *

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"}. + * + *

For example, the nullness checker defines: + * + * 


+ * {@literal @}ParameterConditionalPostconditionAnnotation(qualifier = NonNull.class)
+ * {@literal @}Target(ElementType.PARAMETER)
+ * public {@literal @}interface NonNullIfReturn {
+ *   boolean value();
+ * }
+ *
+ * + *

Usage: + * + * 


+ * public boolean equals(
+ *     {@literal @}NonNullIfReturn(true) {@literal @}Nullable Object other
+ * ) { ... }
+ *
+ * + *

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 qualifier(); +} diff --git a/checker/tests/nullness/NonNullIfReturnTest.java b/checker/tests/nullness/NonNullIfReturnTest.java new file mode 100644 index 000000000000..d5b0548fccc1 --- /dev/null +++ b/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; + } + } +} diff --git a/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java b/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java index b911609f025b..dc78066b1db0 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java +++ b/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; @@ -25,6 +26,7 @@ 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 +38,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. @@ -181,6 +184,50 @@ private Set getContractsOfKind( result.add(contract); } } + + // Gather conditional postconditions from parameter-level annotations (e.g. + // @NonNullIfReturn). + if (kind == Contract.Kind.CONDITIONALPOSTCONDITION) { + List params = executableElement.getParameters(); + for (int i = 0; i < params.size(); i++) { + VariableElement param = params.get(i); + List> paramAnnotations = + atypeFactory.getDeclAnnotationWithMetaAnnotation( + param, ParameterConditionalPostconditionAnnotation.class); + for (IPair 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); + System.err.println( + "[DefaultContractsFromMethod] -> contract (" + + atypeFactory.getClass().getSimpleName() + + "): expression=\"" + + expressionString + + "\", resultValue=" + + resultValue + + ", qualifier=" + + enforcedQualifier.getAnnotationType()); + T contract = + clazz.cast( + Contract.create( + kind, + expressionString, + enforcedQualifier, + paramAnnotation, + resultValue)); + result.add(contract); + } + } + } return result; } From 387df9109ef9fa824aea3d1fda826b51165833f3 Mon Sep 17 00:00:00 2001 From: Henry Xi Date: Fri, 20 Feb 2026 16:41:38 -0500 Subject: [PATCH 2/6] Update contributors.tex --- docs/manual/contributors.tex | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/manual/contributors.tex b/docs/manual/contributors.tex index ed211a6a48ae..83ccd0c903c1 100644 --- a/docs/manual/contributors.tex +++ b/docs/manual/contributors.tex @@ -51,6 +51,7 @@ Hamed Taghani, Hannes Greule, Heath Borders, +Henry Xi, Ivory Wang, Jakub Vr\'ana, James Yoo, From d09e695181eec12e903982a7548565177d074bff Mon Sep 17 00:00:00 2001 From: Henry Xi Date: Sun, 22 Feb 2026 14:49:36 -0500 Subject: [PATCH 3/6] Add caching to parameter level conditional postconditions --- .../util/DefaultContractsFromMethod.java | 27 ++++++++++--------- 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java b/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java index dc78066b1db0..d0ea48baa1a8 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java +++ b/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java @@ -21,6 +21,7 @@ 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; @@ -50,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> + conditionalPostconditionCache = new ConcurrentHashMap<>(); + /** * Creates a ContractsFromMethod for the given factory. * @@ -110,10 +119,13 @@ public Set getPostconditions(ExecutableElement executabl @Override public Set 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 @@ -207,15 +219,6 @@ private Set getContractsOfKind( AnnotationUtils.getElementValue( paramAnnotation, "value", Boolean.class, true); String expressionString = "#" + (i + 1); - System.err.println( - "[DefaultContractsFromMethod] -> contract (" - + atypeFactory.getClass().getSimpleName() - + "): expression=\"" - + expressionString - + "\", resultValue=" - + resultValue - + ", qualifier=" - + enforcedQualifier.getAnnotationType()); T contract = clazz.cast( Contract.create( From 25a379b3cd7adcc3f0c75a900af51408a18b7074 Mon Sep 17 00:00:00 2001 From: Henry Xi Date: Sun, 1 Mar 2026 15:19:33 -0500 Subject: [PATCH 4/6] Change parameter contract name to @NotNullIfReturns --- .../nullness/qual/NonNullIfReturn.java | 107 ------------------ .../nullness/qual/NotNullIfReturns.java | 77 +++++++++++++ ...terConditionalPostconditionAnnotation.java | 21 +--- .../tests/nullness/NonNullIfReturnTest.java | 76 ------------- .../tests/nullness/NotNullIfReturnsTest.java | 73 ++++++++++++ 5 files changed, 155 insertions(+), 199 deletions(-) delete mode 100644 checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturn.java create mode 100644 checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NotNullIfReturns.java delete mode 100644 checker/tests/nullness/NonNullIfReturnTest.java create mode 100644 checker/tests/nullness/NotNullIfReturnsTest.java diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturn.java b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturn.java deleted file mode 100644 index e7a2ff1681b4..000000000000 --- a/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturn.java +++ /dev/null @@ -1,107 +0,0 @@ -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 parameter contract: indicates that the annotated parameter is guaranteed to be non-null - * when the method returns the given boolean value. - * - *

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. - * - *

Example 1: Simple null check - * - * 

{@code
- * public static boolean isNonNull(
- *     @NonNullIfReturn(true) @Nullable Object obj
- * ) {
- *   return obj != null;
- * }
- * }
- * - * 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)}. - * - *

Example 2: equals(Object) - * - * 

{@code
- * @Override
- * public boolean equals(
- *     @NonNullIfReturn(true) @Nullable Object other
- * ) {
- *   ...
- * }
- * }
- * - * If {@code equals(other)} returns {@code true}, then {@code other} was non-null. - * - *

Example 3: Negative return value - * - * 

{@code
- * public static boolean isNull(
- *     @NonNullIfReturn(false) @Nullable Object obj
- * ) {
- *   return obj == null;
- * }
- * }
- * - * If {@code isNull(obj)} returns {@code false}, then {@code obj} is non-null. - * - *

Example 4: Multiple parameters - * - * 

{@code
- * public static boolean bothNonNull(
- *     @NonNullIfReturn(true) @Nullable Object a,
- *     @NonNullIfReturn(true) @Nullable Object b
- * ) {
- *   return a != null && b != null;
- * }
- * }
- * - * If the method returns {@code true}, then {@code a} is non-null and {@code b} is non-null. Each - * parameter's annotation contributes independently. - * - * - * - * @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(); -} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NotNullIfReturns.java b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NotNullIfReturns.java new file mode 100644 index 000000000000..5a6211d404e1 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NotNullIfReturns.java @@ -0,0 +1,77 @@ +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 parameter contract: expresses that the parameter is non-null when the method returns the + * given value. + * + *

Semantic meaning: {@code @NotNullIfReturns(v)} means: this parameter is non-null + * when the method returns v. That is: {@code method returns value() ⇒ parameter != null}. + * + *

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). + * + *

Example 1: hasLength — param is non-null when method returns true. + * + * 

{@code
+ * public static boolean hasLength(@NotNullIfReturns(true) @Nullable String str) {
+ *   return (str != null && !str.isEmpty());
+ * }
+ * }
+ * + * When {@code hasLength(s)} returns true, {@code s} was non-null. + * + *

Example 2: equals — param is non-null when method returns true. + * + * 

{@code
+ * @Override
+ * public boolean equals(@NotNullIfReturns(true) @Nullable Object other) {
+ *   return this == other;
+ * }
+ * }
+ * + *

Example 3: isNull — param is non-null when method returns false. + * + * 

{@code
+ * public static boolean isNull(@NotNullIfReturns(false) @Nullable Object obj) {
+ *   return obj == null;
+ * }
+ * }
+ * + * When {@code isNull(obj)} returns false, {@code obj} was non-null. + * + * + * + * @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 NotNullIfReturns { + /** + * 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(); +} diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/ParameterConditionalPostconditionAnnotation.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/ParameterConditionalPostconditionAnnotation.java index bac37373bd48..33577b712f61 100644 --- a/checker-qual/src/main/java/org/checkerframework/framework/qual/ParameterConditionalPostconditionAnnotation.java +++ b/checker-qual/src/main/java/org/checkerframework/framework/qual/ParameterConditionalPostconditionAnnotation.java @@ -16,30 +16,19 @@ * {@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). * - *

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"}. - * - *

For example, the nullness checker defines: + *

For example, the nullness checker defines {@link + * org.checkerframework.checker.nullness.qual.NotNullIfReturns}: * * 


  * {@literal @}ParameterConditionalPostconditionAnnotation(qualifier = NonNull.class)
  * {@literal @}Target(ElementType.PARAMETER)
- * public {@literal @}interface NonNullIfReturn {
+ * public {@literal @}interface NotNullIfReturns {
  *   boolean value();
  * }
  *
* - *

Usage: - * - * 


- * public boolean equals(
- *     {@literal @}NonNullIfReturn(true) {@literal @}Nullable Object other
- * ) { ... }
- *
- * - *

This is equivalent to the method-level contract {@code @EnsuresNonNullIf(expression="#1", - * result=true)} on the method. + *

Usage: {@code @NotNullIfReturns(true)} means the parameter is non-null when the method returns + * true. * * @see ConditionalPostconditionAnnotation * @see EnsuresQualifierIf diff --git a/checker/tests/nullness/NonNullIfReturnTest.java b/checker/tests/nullness/NonNullIfReturnTest.java deleted file mode 100644 index d5b0548fccc1..000000000000 --- a/checker/tests/nullness/NonNullIfReturnTest.java +++ /dev/null @@ -1,76 +0,0 @@ -// 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; - } - } -} diff --git a/checker/tests/nullness/NotNullIfReturnsTest.java b/checker/tests/nullness/NotNullIfReturnsTest.java new file mode 100644 index 000000000000..a1af607bcd1e --- /dev/null +++ b/checker/tests/nullness/NotNullIfReturnsTest.java @@ -0,0 +1,73 @@ +// Test that @NotNullIfReturns (parameter-level conditional postcondition) is respected by the +// Nullness Checker. + +import org.checkerframework.checker.nullness.qual.NonNull; +import org.checkerframework.checker.nullness.qual.NotNullIfReturns; +import org.checkerframework.checker.nullness.qual.Nullable; + +public class NotNullIfReturnsTest { + + // Example 1: hasLength — param is non-null when method returns true + public static boolean hasLength(@NotNullIfReturns(true) @Nullable String str) { + return (str != null && !str.isEmpty()); + } + + void useHasLength(@Nullable String s) { + if (hasLength(s)) { + @NonNull String n = s; // OK: s is non-null when hasLength returns true + n.hashCode(); + } else { + // :: error: (assignment.type.incompatible) + @NonNull String n = s; + } + } + + // Example 2: equals — param is non-null when method returns true + @Override + public boolean equals(@NotNullIfReturns(true) @Nullable Object other) { + return this == other; + } + + void useEquals(NotNullIfReturnsTest a, @Nullable Object b) { + if (a.equals(b)) { + @NonNull Object n = b; // OK: b is non-null when equals returns true + n.hashCode(); + } + } + + // Example 3: isNull — param is non-null when method returns false + public static boolean isNull(@NotNullIfReturns(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(); + } else { + // :: error: (assignment.type.incompatible) + @NonNull Object n = p; + } + } + + // Example 4: Multiple parameters — both non-null when method returns true + public static boolean bothNonNull( + @NotNullIfReturns(true) @Nullable Object a, + @NotNullIfReturns(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 { + // :: error: (assignment.type.incompatible) + @NonNull Object nx = x; + // :: error: (assignment.type.incompatible) + @NonNull Object ny = y; + } + } +} From 781b000dd0bd652df7a3940747c9e74511ce961e Mon Sep 17 00:00:00 2001 From: Henry Xi Date: Sun, 1 Mar 2026 15:20:20 -0500 Subject: [PATCH 5/6] Add max size and LRU policy to caching --- .../util/DefaultContractsFromMethod.java | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java b/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java index d0ea48baa1a8..dbc1f4e3fe11 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java +++ b/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java @@ -13,6 +13,7 @@ import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.TreeUtils; +import org.plumelib.util.CollectionsPlume; import org.plumelib.util.IPair; import java.util.Collections; @@ -21,7 +22,6 @@ 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; @@ -45,6 +45,12 @@ // more helpful error message. public class DefaultContractsFromMethod implements ContractsFromMethod { + /** + * Maximum size for the conditional postcondition cache. Uses LRU eviction to avoid unbounded + * memory use. Concurrency is not a concern (single-threaded). + */ + private static final int CACHE_SIZE = 300; + /** The QualifierArgument.value field/element. */ protected final ExecutableElement qualifierArgumentValueElement; @@ -52,12 +58,12 @@ public class DefaultContractsFromMethod implements ContractsFromMethod { 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 + * LRU 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> - conditionalPostconditionCache = new ConcurrentHashMap<>(); + conditionalPostconditionCache = CollectionsPlume.createLruCache(CACHE_SIZE); /** * Creates a ContractsFromMethod for the given factory. @@ -198,7 +204,7 @@ private Set getContractsOfKind( } // Gather conditional postconditions from parameter-level annotations (e.g. - // @NonNullIfReturn). + // @NotNullIfReturns). if (kind == Contract.Kind.CONDITIONALPOSTCONDITION) { List params = executableElement.getParameters(); for (int i = 0; i < params.size(); i++) { @@ -218,6 +224,9 @@ private Set getContractsOfKind( Boolean resultValue = AnnotationUtils.getElementValue( paramAnnotation, "value", Boolean.class, true); + // value = return value under which param has the qualifier (e.g. + // @NotNullIfReturns(true) + // means param is non-null when method returns true). String expressionString = "#" + (i + 1); T contract = clazz.cast( From 1eecfca16db3fd2126b98e7e0e9353614a1f0bfe Mon Sep 17 00:00:00 2001 From: Henry Xi Date: Tue, 10 Mar 2026 16:35:18 -0400 Subject: [PATCH 6/6] Add support for NonNullIfReturnsTrue and NonNullIfReturnsFalse --- ...llIfReturns.java => NonNullIfReturns.java} | 17 +- .../nullness/qual/NonNullIfReturnsFalse.java | 24 +++ .../nullness/qual/NonNullIfReturnsTrue.java | 24 +++ ...terConditionalPostconditionAnnotation.java | 29 +++- .../tests/nullness/NonNullIfReturnsTest.java | 162 ++++++++++++++++++ .../tests/nullness/NotNullIfReturnsTest.java | 73 -------- .../common/basetype/messages.properties | 1 + .../util/DefaultContractsFromMethod.java | 30 +++- 8 files changed, 266 insertions(+), 94 deletions(-) rename checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/{NotNullIfReturns.java => NonNullIfReturns.java} (81%) create mode 100644 checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturnsFalse.java create mode 100644 checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturnsTrue.java create mode 100644 checker/tests/nullness/NonNullIfReturnsTest.java delete mode 100644 checker/tests/nullness/NotNullIfReturnsTest.java diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NotNullIfReturns.java b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturns.java similarity index 81% rename from checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NotNullIfReturns.java rename to checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturns.java index 5a6211d404e1..cd7cc03d355d 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NotNullIfReturns.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturns.java @@ -12,7 +12,7 @@ * A parameter contract: expresses that the parameter is non-null when the method returns the * given value. * - *

Semantic meaning: {@code @NotNullIfReturns(v)} means: this parameter is non-null + *

Semantic meaning: {@code @NonNullIfReturns(v)} means: this parameter is non-null * when the method returns v. That is: {@code method returns value() ⇒ parameter != null}. * *

This annotation only makes sense on parameters whose root type is {@code @Nullable} or @@ -23,7 +23,7 @@ *

Example 1: hasLength — param is non-null when method returns true. * * 

{@code
- * public static boolean hasLength(@NotNullIfReturns(true) @Nullable String str) {
+ * public static boolean hasLength(@NonNullIfReturns(true) @Nullable String str) {
  *   return (str != null && !str.isEmpty());
  * }
  * }
@@ -34,7 +34,7 @@ * * 
{@code
  * @Override
- * public boolean equals(@NotNullIfReturns(true) @Nullable Object other) {
+ * public boolean equals(@NonNullIfReturns(true) @Nullable Object other) {
  *   return this == other;
  * }
  * }
@@ -42,7 +42,7 @@ *

Example 3: isNull — param is non-null when method returns false. * * 

{@code
- * public static boolean isNull(@NotNullIfReturns(false) @Nullable Object obj) {
+ * public static boolean isNull(@NonNullIfReturns(false) @Nullable Object obj) {
  *   return obj == null;
  * }
  * }
@@ -51,11 +51,16 @@ * * * + *

For a fixed return value, use {@link NonNullIfReturnsTrue} or {@link NonNullIfReturnsFalse} + * instead. + * + * @see NonNullIfReturnsTrue + * @see NonNullIfReturnsFalse * @see EnsuresNonNullIf * @see NonNull * @see Nullable @@ -66,7 +71,7 @@ @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.PARAMETER}) @ParameterConditionalPostconditionAnnotation(qualifier = NonNull.class) -public @interface NotNullIfReturns { +public @interface NonNullIfReturns { /** * The return value under which the parameter is non-null. * diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturnsFalse.java b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturnsFalse.java new file mode 100644 index 000000000000..fe6d9420999e --- /dev/null +++ b/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 parameter contract: the parameter is non-null when the method returns {@code false}. + * + *

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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturnsTrue.java b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturnsTrue.java new file mode 100644 index 000000000000..33e685eabb16 --- /dev/null +++ b/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 parameter contract: the parameter is non-null when the method returns {@code true}. + * + *

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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/ParameterConditionalPostconditionAnnotation.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/ParameterConditionalPostconditionAnnotation.java index 33577b712f61..170ab9eb6c08 100644 --- a/checker-qual/src/main/java/org/checkerframework/framework/qual/ParameterConditionalPostconditionAnnotation.java +++ b/checker-qual/src/main/java/org/checkerframework/framework/qual/ParameterConditionalPostconditionAnnotation.java @@ -12,23 +12,26 @@ * 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. * - *

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). + *

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). * *

For example, the nullness checker defines {@link - * org.checkerframework.checker.nullness.qual.NotNullIfReturns}: + * org.checkerframework.checker.nullness.qual.NonNullIfReturns}: * * 


  * {@literal @}ParameterConditionalPostconditionAnnotation(qualifier = NonNull.class)
  * {@literal @}Target(ElementType.PARAMETER)
- * public {@literal @}interface NotNullIfReturns {
+ * public {@literal @}interface NonNullIfReturns {
  *   boolean value();
  * }
  *
* - *

Usage: {@code @NotNullIfReturns(true)} means the parameter is non-null when the method returns - * true. + *

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 @@ -39,9 +42,19 @@ 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. + * 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 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; } diff --git a/checker/tests/nullness/NonNullIfReturnsTest.java b/checker/tests/nullness/NonNullIfReturnsTest.java new file mode 100644 index 000000000000..c9215c381f12 --- /dev/null +++ b/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; + } + } +} diff --git a/checker/tests/nullness/NotNullIfReturnsTest.java b/checker/tests/nullness/NotNullIfReturnsTest.java deleted file mode 100644 index a1af607bcd1e..000000000000 --- a/checker/tests/nullness/NotNullIfReturnsTest.java +++ /dev/null @@ -1,73 +0,0 @@ -// Test that @NotNullIfReturns (parameter-level conditional postcondition) is respected by the -// Nullness Checker. - -import org.checkerframework.checker.nullness.qual.NonNull; -import org.checkerframework.checker.nullness.qual.NotNullIfReturns; -import org.checkerframework.checker.nullness.qual.Nullable; - -public class NotNullIfReturnsTest { - - // Example 1: hasLength — param is non-null when method returns true - public static boolean hasLength(@NotNullIfReturns(true) @Nullable String str) { - return (str != null && !str.isEmpty()); - } - - void useHasLength(@Nullable String s) { - if (hasLength(s)) { - @NonNull String n = s; // OK: s is non-null when hasLength returns true - n.hashCode(); - } else { - // :: error: (assignment.type.incompatible) - @NonNull String n = s; - } - } - - // Example 2: equals — param is non-null when method returns true - @Override - public boolean equals(@NotNullIfReturns(true) @Nullable Object other) { - return this == other; - } - - void useEquals(NotNullIfReturnsTest a, @Nullable Object b) { - if (a.equals(b)) { - @NonNull Object n = b; // OK: b is non-null when equals returns true - n.hashCode(); - } - } - - // Example 3: isNull — param is non-null when method returns false - public static boolean isNull(@NotNullIfReturns(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(); - } else { - // :: error: (assignment.type.incompatible) - @NonNull Object n = p; - } - } - - // Example 4: Multiple parameters — both non-null when method returns true - public static boolean bothNonNull( - @NotNullIfReturns(true) @Nullable Object a, - @NotNullIfReturns(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 { - // :: error: (assignment.type.incompatible) - @NonNull Object nx = x; - // :: error: (assignment.type.incompatible) - @NonNull Object ny = y; - } - } -} diff --git a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties index b7fcaf3d5c8a..c78a741af6a3 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/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 diff --git a/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java b/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java index dbc1f4e3fe11..ddf3d3ad5f3f 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java +++ b/framework/src/main/java/org/checkerframework/framework/util/DefaultContractsFromMethod.java @@ -203,8 +203,7 @@ private Set getContractsOfKind( } } - // Gather conditional postconditions from parameter-level annotations (e.g. - // @NotNullIfReturns). + // Gather conditional postconditions from parameter-level annotations if (kind == Contract.Kind.CONDITIONALPOSTCONDITION) { List params = executableElement.getParameters(); for (int i = 0; i < params.size(); i++) { @@ -218,15 +217,32 @@ private Set getContractsOfKind( AnnotationMirror enforcedQualifier = getQualifierEnforcedByContractAnnotation(metaAnnotation, null, null); if (enforcedQualifier == null) { + atypeFactory + .getChecker() + .reportError( + param, + "contracts.parameter.conditional.qualifier.not.supported", + paramAnnotation + .getAnnotationType() + .asElement() + .getSimpleName()); continue; } + // Result value: from param annotation's value() if present, else from + // meta-annotation's result() + Boolean resultValue; + Boolean fromParam = + AnnotationUtils.getElementValueOrNull( + paramAnnotation, "value", Boolean.class, false); + if (fromParam != null) { + resultValue = fromParam; + } else { @SuppressWarnings("deprecation") // permitted for use in the framework - Boolean resultValue = + Boolean v = AnnotationUtils.getElementValue( - paramAnnotation, "value", Boolean.class, true); - // value = return value under which param has the qualifier (e.g. - // @NotNullIfReturns(true) - // means param is non-null when method returns true). + metaAnnotation, "result", Boolean.class, true); + resultValue = v; + } String expressionString = "#" + (i + 1); T contract = clazz.cast(