Non-Empty Checker (#6679)

Co-authored-by: Michael Ernst <[email protected]>
Co-authored-by: Suzanne Millstein <[email protected]>

build.gradle

@@ -114,7 +114,7 @@ allprojects { currentProj ->
   //   * any new checkers have been added, or
   //   * backward-incompatible changes have been made to APIs or elsewhere.
   // To make a snapshot release: ./gradlew publish
-  version '3.44.1-SNAPSHOT'
+  version '3.44.2-SNAPSHOT'
 
   tasks.withType(JavaCompile).configureEach {
     options.fork = true

checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/EnsuresNonEmpty.java

@@ -0,0 +1,53 @@
+package org.checkerframework.checker.nonempty.qual;
+
+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.InheritedAnnotation;
+import org.checkerframework.framework.qual.PostconditionAnnotation;
+
+/**
+ * Indicates that a particular expression evaluates to a non-empty value, if the method terminates
+ * successfully.
+ *
+ * <p>This annotation applies to {@link java.util.Collection}, {@link java.util.Iterator}, {@link
+ * java.lang.Iterable}, and {@link java.util.Map}, but not {@link java.util.Optional}.
+ *
+ * <p>This postcondition annotation is useful for methods that make a value non-empty by side
+ * effect:
+ *
+ * <pre><code>
+ *   {@literal @}EnsuresNonEmpty("ids")
+ *   void addId(String id) {
+ *     ids.add(id);
+ *   }
+ * </code></pre>
+ *
+ * It can also be used for a method that fails if a given value is empty, indicating that the
+ * argument is non-empty if the method returns normally:
+ *
+ * <pre><code>
+ *   /** Throws an exception if the argument is empty. *&#47;
+ *   {@literal @}EnsuresNonEmpty("#1")
+ *   void useTheMap(Map&lt;T, U&gt; arg) { ... }
+ * </code></pre>
+ *
+ * @see NonEmpty
+ * @see org.checkerframework.checker.nonempty.NonEmptyChecker
+ * @checker_framework.manual #non-empty-checker Non-Empty Checker
+ */
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+@PostconditionAnnotation(qualifier = NonEmpty.class)
+@InheritedAnnotation
+public @interface EnsuresNonEmpty {
+  /**
+   * The expression (a collection, iterator, iterable, or map) that is non-empty, if the method
+   * returns normally.
+   *
+   * @return the expression (a collection, iterator, iterable, or map) that is non-empty, if the
+   *     method returns normally
+   */
+  String[] value();
+}

checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/EnsuresNonEmptyIf.java

@@ -0,0 +1,87 @@
+package org.checkerframework.checker.nonempty.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 specific expressions are non-empty, if the method returns the given result
+ * (either true or false).
+ *
+ * <p>Here are ways this conditional postcondition annotation can be used:
+ *
+ * <p><b>Method parameters:</b> Suppose that a method has a parameter that is a list, and returns
+ * true if the length of the list is non-zero. You could annotate the method as follows:
+ *
+ * <pre><code>&nbsp;@EnsuresNonEmptyIf(result = true, expression = "#1")
+ * &nbsp;public &lt;T&gt; boolean isLengthGreaterThanZero(List&lt;T&gt; items) { ... }</code>
+ * </pre>
+ *
+ * because, if {@code isLengthGreaterThanZero} returns true, then {@code items} was non-empty. Note
+ * that you can write more than one {@code @EnsuresNonEmptyIf} annotations on a single method.
+ *
+ * <p><b>Fields:</b> The value expression can refer to fields, even private ones. For example:
+ *
+ * <pre><code>&nbsp;@EnsuresNonEmptyIf(result = true, expression = "this.orders")
+ * &nbsp;public &lt;T&gt; boolean areOrdersActive() {
+ *    return this.orders != null &amp;&amp; this.orders.size() &gt; 0;
+ * }</code></pre>
+ *
+ * An {@code @EnsuresNonEmptyIf} annotation that refers to a private field is useful for verifying
+ * that a method establishes a property, even though client code cannot directly affect the field.
+ *
+ * <p><b>Method postconditions:</b> Suppose that if a method {@code areOrdersActive()} returns true,
+ * then {@code getOrders()} will return a non-empty Map. You can express this relationship as:
+ *
+ * <pre><code>&nbsp;@EnsuresNonEmptyIf(result = true, expression = "this.getOrders()")
+ * &nbsp;public &lt;T&gt; boolean areOrdersActive() {
+ *    return this.orders != null &amp;&amp; this.orders.size() &gt; 0;
+ * }</code></pre>
+ *
+ * @see NonEmpty
+ * @see EnsuresNonEmpty
+ * @checker_framework.manual #non-empty-checker Non-Empty Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+@ConditionalPostconditionAnnotation(qualifier = NonEmpty.class)
+@InheritedAnnotation
+public @interface EnsuresNonEmptyIf {
+
+  /**
+   * A return value of the method; when the method returns that value, the postcondition holds.
+   *
+   * @return the return value of the method for which the postcondition holds
+   */
+  boolean result();
+
+  /**
+   * Returns the Java expressions that are non-empty after the method returns the given result.
+   *
+   * @return the Java expressions that are non-empty after the method returns the given result
+   */
+  String[] expression();
+
+  /**
+   * A wrapper annotation that makes the {@link EnsuresNonEmptyIf} annotation repeatable.
+   *
+   * <p>Programmers generally do not need to write ths. It is created by Java when a programmer
+   * writes more than one {@link EnsuresNonEmptyIf} annotation at the same location.
+   */
+  @Retention(RetentionPolicy.RUNTIME)
+  @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+  @ConditionalPostconditionAnnotation(qualifier = NonEmpty.class)
+  @interface List {
+    /**
+     * Returns the repeatable annotations.
+     *
+     * @return the repeatable annotations
+     */
+    EnsuresNonEmptyIf[] value();
+  }
+}

checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/NonEmpty.java

@@ -0,0 +1,20 @@
+package org.checkerframework.checker.nonempty.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.SubtypeOf;
+
+/**
+ * The {@link java.util.Collection Collection}, {@link java.util.Iterator Iterator}, {@link
+ * java.lang.Iterable Iterable}, or {@link java.util.Map Map} is definitely non-empty.
+ *
+ * @checker_framework.manual #non-empty-checker Non-Empty Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
+@SubtypeOf(UnknownNonEmpty.class)
+public @interface NonEmpty {}

checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/PolyNonEmpty.java

@@ -0,0 +1,20 @@
+package org.checkerframework.checker.nonempty.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.PolymorphicQualifier;
+
+/**
+ * A polymorphic qualifier for the Non-Empty type system.
+ *
+ * @checker_framework.manual #non-empty-checker Non-Empty Checker
+ * @checker_framework.manual #qualifier-polymorphism Qualifier polymorphism
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@PolymorphicQualifier(UnknownNonEmpty.class)
+public @interface PolyNonEmpty {}

checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/RequiresNonEmpty.java

@@ -0,0 +1,96 @@
+package org.checkerframework.checker.nonempty.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.PreconditionAnnotation;
+
+/**
+ * Indicates a method precondition: the specified expressions that may be a {@link
+ * java.util.Collection collection}, {@link java.util.Iterator iterator}, {@link java.lang.Iterable
+ * iterable}, or {@link java.util.Map map} must be non-empty when the annotated method is invoked.
+ *
+ * <p>For example:
+ *
+ * <pre>
+ * import java.util.LinkedList;
+ * import java.util.List;
+ * import org.checkerframework.checker.nonempty.qual.NonEmpty;
+ * import org.checkerframework.checker.nonempty.qual.RequiresNonEmpty;
+ * import org.checkerframework.dataflow.qual.Pure;
+ *
+ * class MyClass {
+ *
+ *   List&lt;String&gt; list1 = new LinkedList&lt;&gt;();
+ *   List&lt;String&gt; list2;
+ *
+ * &nbsp; @RequiresNonEmpty("list1")
+ * &nbsp; @Pure
+ *   void m1() {}
+ *
+ * &nbsp; @RequiresNonEmpty({"list1", "list2"})
+ * &nbsp; @Pure
+ *   void m2() {}
+ *
+ * &nbsp; @RequiresNonEmpty({"list1", "list2"})
+ *   void m3() {}
+ *
+ *   void m4() {}
+ *
+ *   void test(@NonEmpty List&lt;String&gt; l1, @NonEmpty List&lt;String&gt; l2) {
+ *     MyClass testClass = new MyClass();
+ *
+ *     testClass.m1(); // Compile-time error: m1 requires that list1 is @NonEmpty.
+ *
+ *     testClass.list1 = l1;
+ *     testClass.m1(); // OK
+ *
+ *     testClass.m2(); // Compile-time error: m2 requires that list2 is @NonEmpty
+ *
+ *     testClass.list2 = l2;
+ *     testClass.m2(); // OK
+ *
+ *     testClass.m4();
+ *
+ *     testClass.m2(); // Compile-time error: m4 is not pure and might have assigned a field.
+ *   }
+ * }
+ * </pre>
+ *
+ * This annotation should not be used for formal parameters (instead, give them a {@code @NonEmpty}
+ * type). The {@code @RequiresNonEmpty} annotation is intended for non-parameter expressions, such
+ * as field accesses or method calls.
+ *
+ * @checker_framework.manual #non-empty-checker Non-Empty Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD, ElementType.PARAMETER})
+@PreconditionAnnotation(qualifier = NonEmpty.class)
+public @interface RequiresNonEmpty {
+
+  /**
+   * The Java {@link java.util.Collection collection}, {@link java.util.Iterator iterator}, {@link
+   * java.lang.Iterable iterable}, or {@link java.util.Map map} that must be non-empty.
+   *
+   * @return the Java expression that must be non-empty
+   */
+  String[] value();
+
+  /**
+   * A wrapper annotation that makes the {@link RequiresNonEmpty} annotation repeatable.
+   *
+   * <p>Programmers generally do not need to write this. It is created by Java when a programmer
+   * writes more than one {@link RequiresNonEmpty} annotation at the same location.
+   */
+  @interface List {
+    /**
+     * Returns the repeatable annotations.
+     *
+     * @return the repeatable annotations
+     */
+    RequiresNonEmpty[] value();
+  }
+}

checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/UnknownNonEmpty.java

@@ -0,0 +1,22 @@
+package org.checkerframework.checker.nonempty.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.DefaultQualifierInHierarchy;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * The {@link java.util.Collection Collection}, {@link java.util.Iterator Iterator}, {@link
+ * java.lang.Iterable Iterable}, or {@link java.util.Map Map} may or may not be empty.
+ *
+ * @checker_framework.manual #non-empty-checker Non-Empty Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
+@DefaultQualifierInHierarchy
+@SubtypeOf({})
+public @interface UnknownNonEmpty {}

checker/bin/wpi-many.sh

@@ -159,7 +159,7 @@ if [ "${has_java8}" = "no" ] && [ "${has_java11}" = "no" ] && [ "${has_java17}"
 fi
 
 if [ "${CHECKERFRAMEWORK}" = "" ]; then
-    echo "CHECKERFRAMEWORK is not set; it must be set to a locally-built Checker Framework. Please clone and build github.com/typetools/checker-framework"
+    echo "CHECKERFRAMEWORK is not set; it must be set to a locally-built Checker Framework. Please clone and build https://github.com/typetools/checker-framework"
     exit 2
 fi
 

checker/src/main/java/org/checkerframework/checker/interning/InterningAnnotatedTypeFactory.java

@@ -78,7 +78,7 @@ public class InterningAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
   final AnnotationMirrorSet INTERNED_SET = AnnotationMirrorSet.singleton(INTERNED);
 
   /**
-   * Creates a new {@link InterningAnnotatedTypeFactory} that operates on a particular AST.
+   * Creates a new {@link InterningAnnotatedTypeFactory}.
    *
    * @param checker the checker to use
    */

checker/src/main/java/org/checkerframework/checker/nonempty/NonEmptyAnnotatedTypeFactory.java

@@ -0,0 +1,61 @@
+package org.checkerframework.checker.nonempty;
+
+import com.sun.source.tree.ExpressionTree;
+import com.sun.source.tree.NewArrayTree;
+import java.util.List;
+import javax.lang.model.element.AnnotationMirror;
+import org.checkerframework.checker.nonempty.qual.NonEmpty;
+import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.framework.type.AnnotatedTypeFactory;
+import org.checkerframework.framework.type.AnnotatedTypeMirror;
+import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator;
+import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
+import org.checkerframework.javacutil.AnnotationBuilder;
+
+/** The type factory for the {@link NonEmptyChecker}. */
+public class NonEmptyAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
+
+  /** The @{@link NonEmpty} annotation. */
+  public final AnnotationMirror NON_EMPTY = AnnotationBuilder.fromClass(elements, NonEmpty.class);
+
+  /**
+   * Creates a new {@link NonEmptyAnnotatedTypeFactory} that operates on a particular AST.
+   *
+   * @param checker the checker to use
+   */
+  public NonEmptyAnnotatedTypeFactory(BaseTypeChecker checker) {
+    super(checker);
+    this.sideEffectsUnrefineAliases = true;
+    this.postInit();
+  }
+
+  @Override
+  protected TreeAnnotator createTreeAnnotator() {
+    return new ListTreeAnnotator(super.createTreeAnnotator(), new NonEmptyTreeAnnotator(this));
+  }
+
+  /** The tree annotator for the Non-Empty Checker. */
+  private class NonEmptyTreeAnnotator extends TreeAnnotator {
+
+    /**
+     * Creates a new {@link NonEmptyTreeAnnotator}.
+     *
+     * @param aTypeFactory the type factory for this tree annotator
+     */
+    public NonEmptyTreeAnnotator(AnnotatedTypeFactory aTypeFactory) {
+      super(aTypeFactory);
+    }
+
+    @Override
+    public Void visitNewArray(NewArrayTree tree, AnnotatedTypeMirror type) {
+      if (!type.hasEffectiveAnnotation(NON_EMPTY)) {
+        List<? extends ExpressionTree> initializers = tree.getInitializers();
+        if (initializers != null && !initializers.isEmpty()) {
+          type.replaceAnnotation(NON_EMPTY);
+        }
+      }
+      return super.visitNewArray(tree, type);
+    }
+  }
+}