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

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

@@ -59,6 +59,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;
@@ -101,6 +102,11 @@
 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.PostconditionAnnotation;
+import org.checkerframework.framework.qual.PreconditionAnnotation;
+import org.checkerframework.framework.qual.RequiresQualifier;
 import org.checkerframework.framework.qual.Unused;
 import org.checkerframework.framework.source.DiagMessage;
 import org.checkerframework.framework.source.SourceVisitor;
@@ -2260,6 +2266,23 @@ public Void visitAnnotation(AnnotationTree tree, Void p) {
       return null;
     }
 
+    if (isPreOrPostConditionAnnotation(annoName)) {
+      AnnotationMirror anno = TreeUtils.annotationFromAnnotationTree(tree);
+      System.out.printf("anno = %s for annoName = %s for tree = %s%n", anno, annoName, tree);
+      // TODO: `getQualifierEnforcedByContractAnnotation` does not work for @PreconditionAnnotation
+      // or @PostconditionAnnotation.  Should I extend the method to handle that, or should I put
+      // the logic here and avoid calling the method?
+      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);
+        }
+      }
+    }
+
     List<ExecutableElement> methods = ElementFilter.methodsIn(annoType.getEnclosedElements());
     // Mapping from argument simple name to its annotated type.
     Map<String, AnnotatedTypeMirror> annoTypes = ArrayMap.newArrayMapOrHashMap(methods.size());
@@ -2316,6 +2339,29 @@ 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<>(
+          // In Java 9+, use `List.of()`.
+          Arrays.asList(
+              PreconditionAnnotation.class.getName(),
+              PostconditionAnnotation.class.getName(),
+              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();
+    return preAndPostConditionAnnotations.contains(annoName);
+  }
+
   /**
    * If the computation of the type of the ConditionalExpressionTree in
    * org.checkerframework.framework.type.TypeFromTree.TypeFromExpression.visitConditionalExpression(ConditionalExpressionTree,

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

@@ -88,6 +88,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 qualifer %s in a contract annotation %s has no effect
 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

@@ -213,10 +213,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);
   }

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() {}
 }