diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturns.java b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturns.java new file mode 100644 index 000000000000..cd7cc03d355d --- /dev/null +++ b/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 parameter contract: expresses that the parameter is non-null when the method returns the + * given value. + * + *

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 + * 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(@NonNullIfReturns(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(@NonNullIfReturns(true) @Nullable Object other) {
+ *   return this == other;
+ * }
+ * }
+ * + *

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

{@code
+ * public static boolean isNull(@NonNullIfReturns(false) @Nullable Object obj) {
+ *   return obj == null;
+ * }
+ * }
+ * + * When {@code isNull(obj)} returns false, {@code obj} was non-null. + * + * + * + *

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(); +} 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 new file mode 100644 index 000000000000..170ab9eb6c08 --- /dev/null +++ b/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 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 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.NonNullIfReturns}: + * + * 


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

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 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/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, 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 b911609f025b..ddf3d3ad5f3f 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; @@ -12,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; @@ -25,6 +27,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,17 +39,32 @@ * @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. 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; /** The factory that this ContractsFromMethod is associated with. */ protected final GenericAnnotatedTypeFactory atypeFactory; + /** + * 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 = CollectionsPlume.createLruCache(CACHE_SIZE); + /** * Creates a ContractsFromMethod for the given factory. * @@ -107,10 +125,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 @@ -181,6 +202,60 @@ private Set getContractsOfKind( result.add(contract); } } + + // Gather conditional postconditions from parameter-level annotations + 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) { + 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 v = + AnnotationUtils.getElementValue( + metaAnnotation, "result", Boolean.class, true); + resultValue = v; + } + String expressionString = "#" + (i + 1); + T contract = + clazz.cast( + Contract.create( + kind, + expressionString, + enforcedQualifier, + paramAnnotation, + resultValue)); + result.add(contract); + } + } + } return result; }