Implement @EnsuresPresentIf postcondition annotation

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
+ *
+ * <p>Here are ways this conditional postcondition annotation can be used:
+ *
+ * <p><b>Method parameters:</b> Suppose that a method has two arguments of type Optional&lt;T&gt;
+ * and returns true if they are both equal <i>and</i> present. You could annotate the method as
+ * follows:
+ *
+ * <pre><code> &nbsp;@EnsuresPresentIf(expression="#1", result=true)
+ * &nbsp;@EnsuresPresentIf(expression="#2", result=true)
+ * &nbsp;public &lt;T&gt; boolean isPresentAndEqual(Optional&lt;T&gt; optA, Optional&lt;T&gt; optB) { ... }</code>
+ * </pre>
+ *
+ * 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.
+ *
+ * <p><b>Fields:</b> The value expressions can refer to fields, even private ones. For example:
+ *
+ * <pre><code> &nbsp;@EnsuresPresentIf(expression="this.optShape", result=true)
+ *  public boolean isShape() {
+ *    return (this.optShape != null &amp;&amp; this.optShape.isPresent());
+ * }</code></pre>
+ *
+ * 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.
+ *
+ * <p><b>Method postconditions:</b> Suppose that if a method {@code isRectangle()} returns true,
+ * then {@code getRectangle()} will return a present Optional. You an express this relationship as:
+ *
+ * <pre>{@code @EnsuresPresentIf(result=true, expression="getRectangle()")
+ * public @Pure isRectangle() { ... }}</pre>
+ *
+ * @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&lt;T&gt; that are present after the method
+   * returns the given result.
+   *
+   * @return the Java expressions of type Optional&lt;T&gt; 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.
+   *
+   * <p>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();
+  }
+}

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<String> optId = Optional.of("abc");
+
+  @Pure
+  public Optional<String> 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();
+  }
+}

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}