Issue error if top is used in a contract 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
-

checker-qual/src/main/java/org/checkerframework/framework/qual/ConditionalPostconditionAnnotation.java

@@ -66,7 +66,10 @@
 @Target({ElementType.ANNOTATION_TYPE})
 public @interface ConditionalPostconditionAnnotation {
   /**
-   * The qualifier that will be established as a postcondition.
+   * The qualifier that will be established as a postcondition. There is no point using the top
+   * qualifier, which would have no effect because every expression has the top type (and possibly
+   * some more refined type). Establishing more refined types is the point of a pre- or
+   * post-condition annotation.
    *
    * <p>This element is analogous to {@link EnsuresQualifierIf#qualifier()}.
    */

checker-qual/src/main/java/org/checkerframework/framework/qual/PostconditionAnnotation.java

@@ -61,7 +61,10 @@
 @Target({ElementType.ANNOTATION_TYPE})
 public @interface PostconditionAnnotation {
   /**
-   * The qualifier that will be established as a postcondition.
+   * The qualifier that will be established as a postcondition. There is no point using the top
+   * qualifier, which would have no effect because every expression has the top type (and possibly
+   * some more refined type). Establishing more refined types is the point of a pre- or
+   * post-condition annotation.
    *
    * <p>This element is analogous to {@link EnsuresQualifier#qualifier()}.
    */

checker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.java

@@ -56,6 +56,15 @@
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.ANNOTATION_TYPE})
 public @interface PreconditionAnnotation {
-  /** The qualifier that must be established as a precondition. */
+  /**
+   * The qualifier that must be established as a precondition. There is no point using the top
+   * qualifier, which would have no effect because every expression has the top type (and possibly
+   * some more refined type). Establishing more refined types is the point of a pre- or
+   * post-condition annotation.
+   *
+   * <p>This element is analogous to {@link RequiresQualifier#qualifier()}.
+   *
+   * @return the qualifier that must be established as a precondition
+   */
   Class<? extends Annotation> qualifier();
 }

checker/tests/nullness/PreconditionFieldNotInStore.java

@@ -11,6 +11,7 @@ class PreconditionFieldNotInStore {
   @org.checkerframework.framework.qual.RequiresQualifier(
       expression = {"this.filename"},
       qualifier = org.checkerframework.checker.nullness.qual.Nullable.class)
+  // :: warning: [contracts.toptype]
   @org.checkerframework.checker.nullness.qual.NonNull String getIndentString() {
     return "indentString";
   }

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 qualifer %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

@@ -23,6 +23,7 @@
 import org.checkerframework.javacutil.AnnotationBuilder;
 import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.TreeUtils;
+import org.checkerframework.javacutil.TypeSystemError;
 import org.plumelib.util.IPair;
 
 /**
@@ -122,6 +123,7 @@ public Set<Contract.ConditionalPostcondition> getConditionalPostconditions(
   private <T extends Contract> Set<T> getContractsOfKind(
       ExecutableElement executableElement, Contract.Kind kind, Class<T> clazz) {
     Set<T> result = new LinkedHashSet<>();
+
     // Check for a single framework-defined contract annotation.
     // The result is RequiresQualifier, EnsuresQualifier, EnsuresQualifierIf, or null.
     AnnotationMirror frameworkContractAnno =
@@ -143,6 +145,27 @@ private <T extends Contract> Set<T> getContractsOfKind(
       }
     }
 
+    // At this point, `result` contains only framework-defined contract annotations.
+    Set<AnnotationMirror> tops = factory.getQualifierHierarchy().getTopAnnotations();
+    for (T contract : result) {
+      AnnotationMirror anno = contract.annotation;
+      if (AnnotationUtils.containsSame(tops, anno)) {
+        // TODO: issue a warning on the annotation itself rather than on the method declaration.
+        // This requires iterating over the annotation trees on the method declaration to determine
+        // which one led tho the given AnnotationMirror.
+        if (executableElement != null) {
+          String methodString = " on method " + executableElement.getSimpleName();
+          factory
+              .getChecker()
+              .reportWarning(
+                  executableElement,
+                  "contracts.toptype",
+                  anno,
+                  contract.contractAnnotation + methodString);
+        }
+      }
+    }
+
     // Check for type-system specific annotations.  These are the annotations that are
     // meta-annotated by `kind.metaAnnotation`, which is PreconditionAnnotation,
     // PostconditionAnnotation, or ConditionalPostconditionAnnotation.
@@ -158,6 +181,17 @@ private <T extends Contract> Set<T> getContractsOfKind(
       if (enforcedQualifier == null) {
         continue;
       }
+      if (AnnotationUtils.containsSame(tops, enforcedQualifier)) {
+        // TODO: Unfortunately, TypeSystemError does not permit giving a tree at which to issue the
+        // error.  Obtain the file and line number from the tree, and print them here.
+        // TODO: Issue a warning on the annotation itself rather than on the method declaration.
+        // This requires iterating over the annotation trees on the method declaration to determine
+        // which one led tho the given AnnotationMirror.
+        throw new TypeSystemError(
+            "Contract annotation %s on method %s uses the top qualifier %s, which has no effect.",
+            contractAnno, executableElement.getSimpleName(), enforcedQualifier);
+      }
+
       List<String> expressions = factory.getContractExpressions(kind, anno);
       Collections.sort(expressions);
       Boolean ensuresQualifierIfResult = factory.getEnsuresQualifierIfResult(kind, anno);

framework/tests/flow/ContractsOverridingSubtyping.java

@@ -13,6 +13,7 @@ static class Base {
     void requiresOdd() {}
 
     @RequiresQualifier(expression = "f", qualifier = Unqualified.class)
+    // :: warning: [contracts.toptype]
     void requiresUnqual() {}
 
     @EnsuresQualifier(expression = "f", qualifier = Odd.class)
@@ -21,6 +22,7 @@ void ensuresOdd() {
     }
 
     @EnsuresQualifier(expression = "f", qualifier = Unqualified.class)
+    // :: warning: [contracts.toptype]
     void ensuresUnqual() {}
 
     @EnsuresQualifierIf(expression = "f", result = true, qualifier = Odd.class)
@@ -30,6 +32,7 @@ boolean ensuresIfOdd() {
     }
 
     @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class)
+    // :: warning: [contracts.toptype]
     boolean ensuresIfUnqual() {
       return true;
     }
@@ -39,6 +42,7 @@ static class Derived extends Base {
 
     @Override
     @RequiresQualifier(expression = "f", qualifier = Unqualified.class)
+    // :: warning: [contracts.toptype]
     void requiresOdd() {}
 
     @Override
@@ -48,6 +52,7 @@ void requiresUnqual() {}
 
     @Override
     @EnsuresQualifier(expression = "f", qualifier = Unqualified.class)
+    // :: warning: [contracts.toptype]
     // :: error: [contracts.postcondition.override]
     void ensuresOdd() {
       f = g;
@@ -61,6 +66,7 @@ void ensuresUnqual() {
 
     @Override
     @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class)
+    // :: warning: [contracts.toptype]
     // :: error: [contracts.conditional.postcondition.true.override]
     boolean ensuresIfOdd() {
       f = g;

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 ***** */
+  @EnsuresQualifier(expression = "f1", qualifier = Unqualified.class)
+  // :: warning: [contracts.toptype]
+  void noOpForTesting() {}
+
+  @EnsuresQualifierIf(result = true, expression = "f1", qualifier = Unqualified.class)
+  // :: warning: [contracts.toptype]
+  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();
   }
+
+  @RequiresQualifier(expression = "f1", qualifier = Unqualified.class)
+  // :: warning: [contracts.toptype]
+  void noOpForTesting() {}
 }