Implement @EnsuresPresentIf postcondition annotation

Author: jyoo980

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}