Merge ../checker-framework-branch-master into inference-phase-two

build.gradle

@@ -15,7 +15,7 @@ plugins {
   // Code formatting; defines targets "spotlessApply" and "spotlessCheck".
   // https://github.com/diffplug/spotless/tags ; see tags starting "gradle/"
   // Only works on JDK 11+ (even including the plugin crashes Gradle on JDK 8).
-  id 'com.diffplug.spotless' version '6.22.0'
+  id 'com.diffplug.spotless' version '6.23.3'
 }
 apply plugin: 'de.undercouch.download'
 
@@ -59,7 +59,7 @@ ext {
     hashmapUtil : '0.0.1',
     reflectionUtil : '1.1.0',
     plumeUtil : '1.8.1',
-    errorprone : '2.22.0',
+    errorprone : '2.23.0',
   ]
 }
 
@@ -114,7 +114,7 @@ allprojects {
   //   * 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.40.1-SNAPSHOT'
+  version '3.41.0'
 
   tasks.withType(JavaCompile).configureEach {
     options.fork = true

checker-qual/src/main/java/org/checkerframework/dataflow/qual/AssertMethod.java

@@ -0,0 +1,69 @@
+package org.checkerframework.dataflow.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;
+
+/**
+ * {@code AssertMethod} is a method annotation that indicates that a method throws an exception if
+ * the value of a boolean argument is false. This can be used to annotate methods such as JUnit's
+ * {@code Assertions.assertTrue(...)}.
+ *
+ * <p>The annotation enables flow-sensitive type refinement to be more precise. For example, if
+ * {@code Assertions.assertTrue} is annotated as follows:
+ *
+ * <pre><code>@AssertMethod(value = AssertionFailedError.class)
+ * public static void assertFalse(boolean condition);
+ * </code></pre>
+ *
+ * Then, in the code below, the Optional Checker can determine that {@code optional} has a value and
+ * the call to {@code Optional#get} will not throw an exception.
+ *
+ * <pre>
+ * Assertions.assertTrue(optional.isPresent());
+ * Object o = optional.get();
+ * </pre>
+ *
+ * <p>This annotation is a <em>trusted</em> annotation, meaning that the Checker Framework does not
+ * check whether the annotated method really does throw an exception depending on the boolean
+ * expression.
+ *
+ * @checker_framework.manual #type-refinement Automatic type refinement (flow-sensitive type
+ *     qualifier inference)
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target(ElementType.METHOD)
+public @interface AssertMethod {
+
+  /**
+   * The class of the exception thrown by this method. The default is {@link AssertionError}.
+   *
+   * @return class of the exception thrown by this method
+   */
+  Class<?> value() default AssertionError.class;
+
+  /**
+   * The one-based index of the boolean parameter that is tested.
+   *
+   * @return the one-based index of the boolean parameter that is tested
+   */
+  int parameter() default 1;
+
+  /**
+   * Returns whether this method asserts that the boolean expression is false.
+   *
+   * <p>For example, Junit's <a
+   * href="https://junit.org/junit5/docs/5.0.1/api/org/junit/jupiter/api/Assertions.html#assertFalse-boolean-">Assertions.assertFalse(...)</a>
+   * throws an exception if the first argument is false. So it is annotated as follows:
+   *
+   * <pre><code>@AssertMethod(value = AssertionFailedError.class, isAssertFalse = true)
+   * public static void assertFalse(boolean condition);
+   * </code></pre>
+   *
+   * @return the value for {@link #parameter} on which the method throws an exception
+   */
+  boolean isAssertFalse() default false;
+}

checker-util/src/main/java/org/checkerframework/checker/nullness/util/NullnessUtil.java

@@ -81,7 +81,8 @@ private NullnessUtil() {
    * @param message text to include if this method is misused
    * @return the argument, casted to have the type qualifier @NonNull
    */
-  public static @EnsuresNonNull("#1") <T extends @Nullable Object> @NonNull T castNonNull(
+  @EnsuresNonNull("#1")
+  public static <T extends @Nullable Object> @NonNull T castNonNull(
       @Nullable T ref, String message) {
     assert ref != null : "Misuse of castNonNull: called with a null argument: " + message;
     return (@NonNull T) ref;

checker/build.gradle

@@ -64,11 +64,11 @@ dependencies {
   testImplementation 'com.amazonaws:aws-java-sdk-ec2'
   testImplementation 'com.amazonaws:aws-java-sdk-kms'
   // The AWS SDK is used for testing the Called Methods Checker.
-  testImplementation platform('com.amazonaws:aws-java-sdk-bom:1.12.581')
+  testImplementation platform('com.amazonaws:aws-java-sdk-bom:1.12.603')
   // For the Resource Leak Checker's support for JavaEE.
   testImplementation 'javax.servlet:javax.servlet-api:4.0.1'
   // For the Resource Leak Checker's support for IOUtils.
-  testImplementation 'commons-io:commons-io:2.15.0'
+  testImplementation 'commons-io:commons-io:2.15.1'
 
   testImplementation group: 'junit', name: 'junit', version: '4.13.2'
   testImplementation project(':framework-test')

checker/src/main/java/org/checkerframework/checker/guieffect/Effect.java

@@ -108,6 +108,7 @@ public boolean equals(Effect e) {
   }
 
   @Override
+  @SuppressWarnings("SuperEqualsIsObjectEquals") // better style to use the equals() abstraction
   public boolean equals(@Nullable Object o) {
     if (o instanceof Effect) {
       return this.equals((Effect) o);

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java

@@ -515,9 +515,6 @@ public Void visitIdentifier(IdentifierTree tree, AnnotatedTypeMirror type) {
           type.replaceAnnotation(BOTTOM);
         }
       }
-      if (ElementUtils.isResourceVariable(elt)) {
-        type.replaceAnnotation(withoutClose(type.getPrimaryAnnotationInHierarchy(TOP)));
-      }
       return super.visitIdentifier(tree, type);
     }
   }

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java

@@ -12,13 +12,11 @@
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.Element;
 import javax.lang.model.type.TypeMirror;
-import org.checkerframework.checker.mustcall.qual.MustCall;
 import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.resourceleak.ResourceLeakChecker;
 import org.checkerframework.dataflow.analysis.TransferInput;
 import org.checkerframework.dataflow.analysis.TransferResult;
-import org.checkerframework.dataflow.cfg.node.AssignmentNode;
 import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
 import org.checkerframework.dataflow.cfg.node.MethodInvocationNode;
 import org.checkerframework.dataflow.cfg.node.Node;
@@ -31,7 +29,6 @@
 import org.checkerframework.framework.flow.CFStore;
 import org.checkerframework.framework.flow.CFTransfer;
 import org.checkerframework.framework.flow.CFValue;
-import org.checkerframework.javacutil.ElementUtils;
 import org.checkerframework.javacutil.TreePathUtil;
 import org.checkerframework.javacutil.TreeUtils;
 import org.checkerframework.javacutil.TypesUtils;
@@ -114,28 +111,6 @@ private AnnotationMirror getDefaultStringType(StringConversionNode n) {
     return this.defaultStringType;
   }
 
-  @Override
-  public TransferResult<CFValue, CFStore> visitAssignment(
-      AssignmentNode n, TransferInput<CFValue, CFStore> in) {
-    TransferResult<CFValue, CFStore> result = super.visitAssignment(n, in);
-    // Remove "close" from the type in the store for resource variables.
-    // The Resource Leak Checker relies on this code to avoid checking that
-    // resource variables are closed.
-    if (ElementUtils.isResourceVariable(TreeUtils.elementFromTree(n.getTarget().getTree()))) {
-      CFStore store = result.getRegularStore();
-      JavaExpression expr = JavaExpression.fromNode(n.getTarget());
-      CFValue value = store.getValue(expr);
-      AnnotationMirror withClose =
-          atypeFactory.getAnnotationByClass(value.getAnnotations(), MustCall.class);
-      if (withClose == null) {
-        return result;
-      }
-      AnnotationMirror withoutClose = atypeFactory.withoutClose(withClose);
-      insertIntoStores(result, expr, withoutClose);
-    }
-    return result;
-  }
-
   @Override
   public TransferResult<CFValue, CFStore> visitMethodInvocation(
       MethodInvocationNode n, TransferInput<CFValue, CFStore> in) {

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java

@@ -17,7 +17,6 @@
 import javax.lang.model.element.ExecutableElement;
 import javax.lang.model.element.TypeElement;
 import javax.lang.model.type.TypeMirror;
-import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey;
 import org.checkerframework.checker.mustcall.qual.InheritableMustCall;
 import org.checkerframework.checker.mustcall.qual.MustCall;
 import org.checkerframework.checker.mustcall.qual.MustCallAlias;
@@ -267,75 +266,6 @@ protected boolean skipReceiverSubtypeCheck(
     return true;
   }
 
-  /**
-   * This boolean is used to communicate between different levels of the common assignment check
-   * whether a given check is being carried out on a (pseudo-)assignment to a resource variable. In
-   * those cases, close doesn't need to be considered when doing the check, since close will always
-   * be called by Java.
-   *
-   * <p>The check for whether the LHS is a resource variable can only be carried out on the element,
-   * but the effect needs to happen at the stage where the type is available (i.e. close needs to be
-   * removed from the type). Thus, this variable is used to communicate that a resource variable was
-   * detected on the LHS.
-   */
-  private boolean commonAssignmentCheckOnResourceVariable = false;
-
-  /**
-   * {@inheritDoc}
-   *
-   * <p>Mark (using the {@code #commonAssignmentCheckOnResourceVariable} field of this class) any
-   * assignments where the LHS is a resource variable, so that close doesn't need to be considered.
-   * See {@link #commonAssignmentCheck(AnnotatedTypeMirror, AnnotatedTypeMirror, Tree, String,
-   * Object...)} for the code that uses and removes the mark.
-   */
-  @Override
-  protected boolean commonAssignmentCheck(
-      Tree varTree,
-      ExpressionTree valueExp,
-      @CompilerMessageKey String errorKey,
-      Object... extraArgs) {
-    Element elt = TreeUtils.elementFromTree(varTree);
-    if (elt != null && elt.getKind() == ElementKind.RESOURCE_VARIABLE) {
-      commonAssignmentCheckOnResourceVariable = true;
-    }
-    return super.commonAssignmentCheck(varTree, valueExp, errorKey, extraArgs);
-  }
-
-  /**
-   * {@inheritDoc}
-   *
-   * <p>Iff the LHS is a resource variable, then {@code #commonAssignmentCheckOnResourceVariable}
-   * will be true. This method guarantees that {@code #commonAssignmentCheckOnResourceVariable} will
-   * be false when it returns.
-   */
-  @Override
-  protected boolean commonAssignmentCheck(
-      AnnotatedTypeMirror varType,
-      AnnotatedTypeMirror valueType,
-      Tree valueTree,
-      @CompilerMessageKey String errorKey,
-      Object... extraArgs) {
-
-    if (commonAssignmentCheckOnResourceVariable) {
-      commonAssignmentCheckOnResourceVariable = false;
-      // The LHS has been marked as a resource variable.  Skip the standard common assignment
-      // check; instead do a check that does not include "close".
-      AnnotationMirror varAnno = varType.getPrimaryAnnotationInHierarchy(atypeFactory.TOP);
-      AnnotationMirror valueAnno = valueType.getPrimaryAnnotationInHierarchy(atypeFactory.TOP);
-      if (qualHierarchy.isSubtypeShallow(
-          atypeFactory.withoutClose(valueAnno),
-          valueType.getUnderlyingType(),
-          atypeFactory.withoutClose(varAnno),
-          varType.getUnderlyingType())) {
-        return true;
-      }
-      // Note that in this case, the rest of the common assignment check should fail (barring
-      // an exception).  Control falls through here to avoid duplicating error-issuing code.
-    }
-    // commonAssignmentCheckOnResourceVariable is already false, so no need to set it.
-    return super.commonAssignmentCheck(varType, valueType, valueTree, errorKey, extraArgs);
-  }
-
   /**
    * This method typically issues a warning if the result type of the constructor is not top,
    * because in top-default type systems that indicates a potential problem. The Must Call Checker

checker/src/main/java/org/checkerframework/checker/nullness/KeyForValue.java

@@ -84,19 +84,21 @@ public KeyForValue(
   }
 
   @Override
-  public KeyForValue leastUpperBound(@Nullable KeyForValue other) {
-    KeyForValue lub = super.leastUpperBound(other);
+  protected KeyForValue upperBound(
+      @Nullable KeyForValue other, TypeMirror upperBoundTypeMirror, boolean shouldWiden) {
+    KeyForValue upperBound = super.upperBound(other, upperBoundTypeMirror, shouldWiden);
+
     if (other == null || other.keyForMaps == null || this.keyForMaps == null) {
-      return lub;
+      return upperBound;
     }
     // Lub the keyForMaps by intersecting the sets.
-    lub.keyForMaps = new LinkedHashSet<>(this.keyForMaps.size());
-    lub.keyForMaps.addAll(this.keyForMaps);
-    lub.keyForMaps.retainAll(other.keyForMaps);
-    if (lub.keyForMaps.isEmpty()) {
-      lub.keyForMaps = null;
+    upperBound.keyForMaps = new LinkedHashSet<>(this.keyForMaps.size());
+    upperBound.keyForMaps.addAll(this.keyForMaps);
+    upperBound.keyForMaps.retainAll(other.keyForMaps);
+    if (upperBound.keyForMaps.isEmpty()) {
+      upperBound.keyForMaps = null;
     }
-    return lub;
+    return upperBound;
   }
 
   @Override

checker/src/main/java/org/checkerframework/checker/nullness/NullnessValue.java

@@ -41,8 +41,9 @@ public NullnessValue(
   }
 
   @Override
-  public NullnessValue leastUpperBound(@Nullable NullnessValue other) {
-    NullnessValue result = super.leastUpperBound(other);
+  protected NullnessValue upperBound(
+      @Nullable NullnessValue other, TypeMirror upperBoundTypeMirror, boolean shouldWiden) {
+    NullnessValue result = super.upperBound(other, upperBoundTypeMirror, shouldWiden);
 
     AnnotationMirror resultNullableAnno =
         analysis.getTypeFactory().getAnnotationByClass(result.annotations, Nullable.class);

checker/src/main/java/org/checkerframework/checker/nullness/junit-assertions.astub

@@ -53,10 +53,13 @@ public class Assertions {
 
 	public static void assertNull(@Nullable Object actual, Supplier<String> messageSupplier);
 
+	@EnsuresNonNull("#1")
 	public static void assertNotNull(Object actual);
 
+	@EnsuresNonNull("#1")
 	public static void assertNotNull(Object actual, String message);
 
+	@EnsuresNonNull("#1")
 	public static void assertNotNull(Object actual, Supplier<String> messageSupplier);
 
 	public static void assertEquals(short expected, short actual);

checker/src/main/java/org/checkerframework/checker/nullness/permit-nullness-assertion-exception.astub

@@ -17,24 +17,30 @@ public class Objects {
 }
 
 
-// No annotations for com.google.common.base.Preconditions or
+// No type annotations for com.google.common.base.Preconditions or
 // com.google.common.base.Verify are needed because they are annotated with
 // @CheckForNull and the Checker Framework treats @CheckForNull as @Nullable.
 
 
 package org.junit;
 
 public class Assertions {
+  @EnsuresNonNull("#1")
   public static void assertNotNull(@Nullable Object actual);
+  @EnsuresNonNull("#1")
   public static void assertNotNull(@Nullable Object actual, String message);
+  @EnsuresNonNull("#1")
   public static void assertNotNull(@Nullable Object actual, Supplier<String> messageSupplier);
 }
 
 
 package org.junit.jupiter.api;
 
 public class Assertions {
+  @EnsuresNonNull("#1")
   public static void assertNotNull(@Nullable Object actual);
+  @EnsuresNonNull("#1")
   public static void assertNotNull(@Nullable Object actual, String message);
+  @EnsuresNonNull("#1")
   public static void assertNotNull(@Nullable Object actual, Supplier<String> messageSupplier);
 }