Warn when using the top type in a pre- or post-condition annotation

annotation-file-utilities/src/test/resources/annotations/tests/classfile/all-annotations.jaif

@@ -34,4 +34,3 @@ annotation @G: @Retention(RUNTIME)
 	boolean[] fieldC
 	int fieldD
 	int fieldE
-

framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java

@@ -61,6 +61,7 @@
 import java.util.Map;
 import java.util.Set;
 import java.util.StringJoiner;
+import java.util.TreeSet;
 import java.util.Vector;
 import javax.annotation.processing.ProcessingEnvironment;
 import javax.lang.model.element.AnnotationMirror;
@@ -104,7 +105,10 @@
 import org.checkerframework.framework.flow.CFAbstractStore;
 import org.checkerframework.framework.flow.CFAbstractValue;
 import org.checkerframework.framework.qual.DefaultQualifier;
+import org.checkerframework.framework.qual.EnsuresQualifier;
+import org.checkerframework.framework.qual.EnsuresQualifierIf;
 import org.checkerframework.framework.qual.HasQualifierParameter;
+import org.checkerframework.framework.qual.RequiresQualifier;
 import org.checkerframework.framework.qual.Unused;
 import org.checkerframework.framework.source.DiagMessage;
 import org.checkerframework.framework.source.SourceVisitor;
@@ -2387,6 +2391,21 @@ public Void visitAnnotation(AnnotationTree tree, Void p) {
       return null;
     }
 
+    // This logic is not in BaseTypeVisitor#checkContractsAtMethodDeclaration because that method
+    // apears to also check implicit annotations.
+    if (isPreOrPostConditionAnnotation(annoName)) {
+      AnnotationMirror anno = TreeUtils.annotationFromAnnotationTree(tree);
+      AnnotationMirror qualifier =
+          atypeFactory.getContractsFromMethod().getQualifierEnforcedByContractAnnotation(anno);
+      if (qualifier != null) {
+        AnnotationMirror topForQualifier = qualHierarchy.getTopAnnotation(qualifier);
+        if (AnnotationUtils.areSame(qualifier, topForQualifier)) {
+          Name contractQualName = qualifier.getAnnotationType().asElement().getSimpleName();
+          checker.reportWarning(tree, "contracts.toptype", contractQualName, tree);
+        }
+      }
+    }
+
     List<ExecutableElement> methods = ElementFilter.methodsIn(annoType.getEnclosedElements());
     // Mapping from argument simple name to its annotated type.
     Map<String, AnnotatedTypeMirror> annoTypes = ArrayMap.newArrayMapOrHashMap(methods.size());
@@ -2441,6 +2460,28 @@ public Void visitAnnotation(AnnotationTree tree, Void p) {
     return null;
   }
 
+  /** Pre- and post-condition annotations that take a qualifier as an argument. */
+  private TreeSet<String> preAndPostConditionAnnotations =
+      new TreeSet<>(
+          List.of(
+              RequiresQualifier.class.getName(),
+              EnsuresQualifier.class.getName(),
+              EnsuresQualifierIf.class.getName()));
+
+  /**
+   * Returns true if the given annotation name matches that of a pre- or post-condition annotation
+   * or meta-annotation that takes a qualifier as an argument.
+   *
+   * @param annotationName an annotation name
+   * @return true iff the annotation name matches that of a pre- or post-condition annotation
+   */
+  private boolean isPreOrPostConditionAnnotation(Name annotationName) {
+    String annoName = annotationName.toString();
+    // TODO: This method should also return true for any annotation that is meta-annotated with
+    // @PreconditionAnnotation or @PostconditionAnnotation.
+    return preAndPostConditionAnnotations.contains(annoName);
+  }
+
   @Override
   public Void visitConditionalExpression(ConditionalExpressionTree tree, Void p) {
     if (TreeUtils.isPolyExpression(tree)) {

framework/src/main/java/org/checkerframework/common/basetype/messages.properties

@@ -90,6 +90,7 @@ flowexpr.parse.context.not.determined=could not determine the context at '%s' wi
 flowexpr.parameter.not.final=parameter %s in '%s' is not effectively final (i.e., it gets re-assigned)
 contracts.precondition=precondition of %s is not satisfied.%nfound   : %s%nrequired: %s
 contracts.postcondition=postcondition of %s is not satisfied.%nfound   : %s%nrequired: %s
+contracts.toptype=the top qualifier %s has no effect in contract annotation %s
 contracts.conditional.postcondition=conditional postcondition is not satisfied when %s returns %s.%nfound   : %s%nrequired: %s
 contracts.conditional.postcondition.returntype=this annotation is only valid for methods with return type 'boolean'
 # Same text for "override" and "methodref", but different key.

framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java

@@ -216,10 +216,11 @@ private <T extends Contract> Set<T> getContract(
    * Returns the annotation mirror as specified by the {@code qualifier} element in {@code
    * contractAnno}. May return null.
    *
-   * @param contractAnno a pre- or post-condition annotation, such as {@code @RequiresQualifier}
+   * @param contractAnno a pre- or post-condition annotation, such as {@code @RequiresQualifier}.
+   *     Does not work for {@code PreconditionAnnotation} or {@code PostconditionAnnotation}.
    * @return the type annotation specified in {@code contractAnno.qualifier}
    */
-  private @Nullable AnnotationMirror getQualifierEnforcedByContractAnnotation(
+  public @Nullable AnnotationMirror getQualifierEnforcedByContractAnnotation(
       AnnotationMirror contractAnno) {
     return getQualifierEnforcedByContractAnnotation(contractAnno, null, null);
   }
@@ -262,12 +263,15 @@ private <T extends Contract> Set<T> getContract(
       @Nullable AnnotationMirror argumentAnno,
       @Nullable Map<String, String> argumentRenaming) {
 
+    // This method returns null for user-defined contract annotations defined with
+    // @PreconditionAnnotation or @PostconditionAnnotation.  TODO: extend the method to handle that.
+
     @SuppressWarnings("deprecation") // permitted for use in the framework
     Name c = AnnotationUtils.getElementValueClassName(contractAnno, "qualifier", false);
 
     AnnotationMirror anno;
     if (argumentAnno == null || argumentRenaming.isEmpty()) {
-      // If there are no arguments, use factory method that allows caching
+      // If there are no arguments, use factory method that allows caching.
       anno = AnnotationBuilder.fromName(factory.getElementUtils(), c);
     } else {
       AnnotationBuilder builder = new AnnotationBuilder(factory.getProcessingEnv(), c);

framework/tests/flow/ContractsOverridingSubtyping.java

@@ -12,6 +12,7 @@ static class Base {
     @RequiresQualifier(expression = "f", qualifier = Odd.class)
     void requiresOdd() {}
 
+    // :: warning: [contracts.toptype]
     @RequiresQualifier(expression = "f", qualifier = Unqualified.class)
     void requiresUnqual() {}
 
@@ -20,6 +21,7 @@ void ensuresOdd() {
       f = g;
     }
 
+    // :: warning: [contracts.toptype]
     @EnsuresQualifier(expression = "f", qualifier = Unqualified.class)
     void ensuresUnqual() {}
 
@@ -29,6 +31,7 @@ boolean ensuresIfOdd() {
       return true;
     }
 
+    // :: warning: [contracts.toptype]
     @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class)
     boolean ensuresIfUnqual() {
       return true;
@@ -38,6 +41,7 @@ boolean ensuresIfUnqual() {
   static class Derived extends Base {
 
     @Override
+    // :: warning: [contracts.toptype]
     @RequiresQualifier(expression = "f", qualifier = Unqualified.class)
     void requiresOdd() {}
 
@@ -47,6 +51,7 @@ void requiresOdd() {}
     void requiresUnqual() {}
 
     @Override
+    // :: warning: [contracts.toptype]
     @EnsuresQualifier(expression = "f", qualifier = Unqualified.class)
     // :: error: [contracts.postcondition.override]
     void ensuresOdd() {
@@ -60,6 +65,7 @@ void ensuresUnqual() {
     }
 
     @Override
+    // :: warning: [contracts.toptype]
     @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class)
     // :: error: [contracts.conditional.postcondition.true.override]
     boolean ensuresIfOdd() {

framework/tests/flow/Postcondition.java

@@ -1,3 +1,4 @@
+import org.checkerframework.common.subtyping.qual.Unqualified;
 import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.framework.qual.EnsuresQualifier;
 import org.checkerframework.framework.qual.EnsuresQualifierIf;
@@ -312,4 +313,15 @@ void t6(@Odd String p1, @ValueTypeAnno String p2) {
       @Odd String l6 = f1;
     }
   }
+
+  /** *** errors for invalid postconditions ***** */
+  // :: warning: [contracts.toptype]
+  @EnsuresQualifier(expression = "f1", qualifier = Unqualified.class)
+  void noOpForTesting() {}
+
+  // :: warning: [contracts.toptype]
+  @EnsuresQualifierIf(result = true, expression = "f1", qualifier = Unqualified.class)
+  boolean isF1NotSet() {
+    return f1 == null;
+  }
 }

framework/tests/flow/Precondition.java

@@ -1,3 +1,4 @@
+import org.checkerframework.common.subtyping.qual.Unqualified;
 import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.framework.qual.RequiresQualifier;
 import org.checkerframework.framework.test.*;
@@ -159,4 +160,8 @@ void t5(@Odd String p1, String p2, @ValueTypeAnno String p3) {
     // :: error: [flowexpr.parse.error]
     error2();
   }
+
+  // :: warning: [contracts.toptype]
+  @RequiresQualifier(expression = "f1", qualifier = Unqualified.class)
+  void noOpForTesting() {}
 }