diff --git a/checker-qual/src/main/java/org/checkerframework/checker/optional/qual/EnsuresPresentIf.java b/checker-qual/src/main/java/org/checkerframework/checker/optional/qual/EnsuresPresentIf.java new file mode 100644 index 00000000000..f43d2974bb4 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/optional/qual/EnsuresPresentIf.java @@ -0,0 +1,91 @@ +package org.checkerframework.checker.optional.qual; + +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; +import org.checkerframework.framework.qual.ConditionalPostconditionAnnotation; +import org.checkerframework.framework.qual.InheritedAnnotation; + +/** + * Indicates that the given expressions of type Optional<T> are present, if the method returns + * the given result (either true or false).FOO + * + *

Here are ways this conditional postcondition annotation can be used: + * + *

Method parameters: Suppose that a method has two arguments of type Optional<T> + * and returns true if they are both equal and present. You could annotate the method as + * follows: + * + *

  @EnsuresPresentIf(expression="#1", result=true)
+ *  @EnsuresPresentIf(expression="#2", result=true)
+ *  public <T> boolean isPresentAndEqual(Optional<T> optA, Optional<T> optB) { ... }
+ * 
+ * + * because, if {@code isPresentAndEqual} returns true, then the first (#1) argument to {@code + * isPresentAndEqual} was present, and so was the second (#2) argument. Note that you can write two + * {@code @EnsurePresentIf} annotations on a single method. + * + *

Fields: The value expressions can refer to fields, even private ones. For example: + * + *

  @EnsuresPresentIf(expression="this.optShape", result=true)
+ *  public boolean isShape() {
+ *    return (this.optShape != null && this.optShape.isPresent());
+ * }
+ * + * An {@code @EnsuresPresentIf} annotation that refers to a private field is useful for verifying + * that client code performs needed checks in the right order, even if the client code cannot + * directly affect the field. + * + *

Method postconditions: Suppose that if a method {@code isRectangle()} returns true, + * then {@code getRectangle()} will return a present Optional. You an express this relationship as: + * + *

{@code @EnsuresPresentIf(result=true, expression="getRectangle()")
+ * public @Pure isRectangle() { ... }}
+ * + * @see Present + * @see EnsuresPresent + * @checker_framework.manual #optional-checker Optional Checker + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) +@ConditionalPostconditionAnnotation(qualifier = Present.class) +@InheritedAnnotation +public @interface EnsuresPresentIf { + /** + * Returns the Java expressions of type Optional<T> that are present after the method + * returns the given result. + * + * @return the Java expressions of type Optional<T> that are present after the method + * returns the given result. value {@link #result()} + * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions + */ + String[] expression(); + + /** + * Returns the return value of the method under which the postcondition holds. + * + * @return the return value of the method under which the postcondition holds. + */ + boolean result(); + + /** + * A wrapper annotation that makes the {@link EnsuresPresentIf} annotation repeatable. + * + *

Programmers generally do not need to write this. It is created by Java when a programmer + * writes more than one {@link EnsuresPresentIf} annotation at the same location. + */ + @Retention(RetentionPolicy.RUNTIME) + @Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) + @ConditionalPostconditionAnnotation(qualifier = Present.class) + public static @interface List { + /** + * Returns the repeatable annotations. + * + * @return the repeatable annotations. + */ + EnsuresPresentIf[] value(); + } +} diff --git a/checker/tests/optional/EnsuresPresentIfTest.java b/checker/tests/optional/EnsuresPresentIfTest.java new file mode 100644 index 00000000000..3212c2889a3 --- /dev/null +++ b/checker/tests/optional/EnsuresPresentIfTest.java @@ -0,0 +1,85 @@ +import java.util.Optional; +import org.checkerframework.checker.optional.qual.EnsuresPresentIf; +import org.checkerframework.checker.optional.qual.Present; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.framework.qual.EnsuresQualifierIf; + +public class EnsuresPresentIfTest { + + // :: warning: (optional.field) + private Optional optId = Optional.of("abc"); + + @Pure + public Optional getOptId() { + return Optional.of("abc"); + } + + @EnsuresPresentIf(result = true, expression = "getOptId()") + public boolean hasPresentId1() { + return getOptId().isPresent(); + } + + @EnsuresPresentIf(result = true, expression = "this.getOptId()") + public boolean hasPresentId2() { + return getOptId().isPresent(); + } + + @EnsuresQualifierIf(result = true, expression = "getOptId()", qualifier = Present.class) + public boolean hasPresentId3() { + return getOptId().isPresent(); + } + + @EnsuresQualifierIf(result = true, expression = "this.getOptId()", qualifier = Present.class) + public boolean hasPresentId4() { + return getOptId().isPresent(); + } + + @EnsuresPresentIf(result = true, expression = "optId") + public boolean hasPresentId5() { + return optId.isPresent(); + } + + @EnsuresPresentIf(result = true, expression = "this.optId") + public boolean hasPresentId6() { + return optId.isPresent(); + } + + @EnsuresQualifierIf(result = true, expression = "optId", qualifier = Present.class) + public boolean hasPresentId7() { + return optId.isPresent(); + } + + @EnsuresQualifierIf(result = true, expression = "this.optId", qualifier = Present.class) + public boolean hasPresentId8() { + return optId.isPresent(); + } + + void client() { + if (hasPresentId1()) { + getOptId().get(); + } + if (hasPresentId2()) { + getOptId().get(); + } + if (hasPresentId3()) { + getOptId().get(); + } + if (hasPresentId4()) { + getOptId().get(); + } + if (hasPresentId5()) { + optId.get(); + } + if (hasPresentId6()) { + optId.get(); + } + if (hasPresentId7()) { + optId.get(); + } + if (hasPresentId8()) { + optId.get(); + } + // :: error: (method.invocation) + optId.get(); + } +} diff --git a/docs/manual/advanced-features.tex b/docs/manual/advanced-features.tex index 591465bdbfb..39b3da64ad2 100644 --- a/docs/manual/advanced-features.tex +++ b/docs/manual/advanced-features.tex @@ -1233,6 +1233,8 @@ \item \refqualclass{checker/nullness/qual}{RequiresNonNull} \item \refqualclass{checker/nullness/qual}{EnsuresNonNull} \item \refqualclass{checker/nullness/qual}{EnsuresNonNullIf} +\item \refqualclass{checker/optional/qual}{EnsuresPresent} +\item \refqualclass{checker/optional/qual}{EnsuresPresentIf} % Not implemented: \refqualclass{checker/nullness/qual}{AssertNonNullIfNonNull} \item \refqualclass{checker/nullness/qual}{KeyFor} \item \refqualclass{checker/nullness/qual}{EnsuresKeyFor}