Issue warnings when top is passed as a pre/postcondition qualifier

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

@@ -101,6 +101,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;
@@ -2243,6 +2248,14 @@ public Void visitAnnotation(AnnotationTree tree, Void p) {
       return null;
     }
 
+    if (this.isPreOrPostConditionAnnotation(annoName) && methodTree != null) {
+      ExecutableElement methodElement = TreeUtils.elementFromDeclaration(methodTree);
+      Set<Contract> contracts = atypeFactory.getContractsFromMethod().getContracts(methodElement);
+      for (Contract contract : contracts) {
+        checkValidRefinementContract(contract, methodTree);
+      }
+    }
+
     List<ExecutableElement> methods = ElementFilter.methodsIn(anno.getEnclosedElements());
     // Mapping from argument simple name to its annotated type.
     Map<String, AnnotatedTypeMirror> annoTypes = ArrayMap.newArrayMapOrHashMap(methods.size());
@@ -2299,6 +2312,51 @@ public Void visitAnnotation(AnnotationTree tree, Void p) {
     return null;
   }
 
+  /**
+   * Checks whether a given annotation name matches that of a pre or postcondition annotation.
+   *
+   * @param annotationName the annotation name to check
+   * @return true iff the annotation name matches that of a pre or postcondition annotation
+   */
+  private boolean isPreOrPostConditionAnnotation(Name annotationName) {
+    return annotationName.contentEquals(PreconditionAnnotation.class.getName())
+        || annotationName.contentEquals(PostconditionAnnotation.class.getName())
+        || annotationName.contentEquals(RequiresQualifier.class.getName())
+        || annotationName.contentEquals(EnsuresQualifier.class.getName())
+        || annotationName.contentEquals(EnsuresQualifierIf.class.getName());
+  }
+
+  /**
+   * Check whether a qualifier passed to a pre or postcondition contract is the top type in a
+   * qualifier hierarchy.
+   *
+   * <p>Passing a top type to a pre or postcondition qualifier has no effect, as refinement only
+   * occurs when going from a more general type (i.e., higher up in the lattice) to a more specific
+   * type (lower in the lattice). Additionally, types lower in the lattice implicitly have the
+   * top-level type, via subtyping.
+   *
+   * <p>As such, a warning should be issued in a case where a pre/postcondition requires a value
+   * have a top-level type.
+   *
+   * @param contract the contract for which a check for a valid refinement is performed
+   * @param methodTree the method on which the contract is written
+   */
+  private void checkValidRefinementContract(Contract contract, MethodTree methodTree) {
+    AnnotationMirror contractQualifier = contract.annotation;
+    AnnotationMirror topInContractQualifier = qualHierarchy.getTopAnnotation(contractQualifier);
+    DeclaredType topDeclaredType = topInContractQualifier.getAnnotationType();
+    DeclaredType contractDeclaredType = contractQualifier.getAnnotationType();
+    String warningKey =
+        contract.kind == Contract.Kind.POSTCONDITION
+                || contract.kind == Contract.Kind.CONDITIONALPOSTCONDITION
+            ? "contracts.postcondition.refinement"
+            : "contracts.precondition.refinement";
+    if (types.isSameType(topDeclaredType, contractDeclaredType)) {
+      Name topTypeName = contractQualifier.getAnnotationType().asElement().getSimpleName();
+      checker.reportWarning(methodTree, warningKey, methodTree.getName(), topTypeName);
+    }
+  }
+
   /**
    * 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,8 @@ 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.precondition.refinement=precondition for %s is redundant: refinement to a top type %s has no effect
+contracts.postcondition.refinement=postcondition for %s is redundant: refinement to a top type %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/tests/flow/ContractsOverridingSubtyping.java

@@ -13,6 +13,7 @@ static class Base {
     void requiresOdd() {}
 
     @RequiresQualifier(expression = "f", qualifier = Unqualified.class)
+    // :: warning: (contracts.precondition.refinement)
     void requiresUnqual() {}
 
     @EnsuresQualifier(expression = "f", qualifier = Odd.class)
@@ -21,6 +22,7 @@ void ensuresOdd() {
     }
 
     @EnsuresQualifier(expression = "f", qualifier = Unqualified.class)
+    // :: warning: (contracts.postcondition.refinement)
     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.postcondition.refinement)
     boolean ensuresIfUnqual() {
       return true;
     }
@@ -39,6 +42,7 @@ static class Derived extends Base {
 
     @Override
     @RequiresQualifier(expression = "f", qualifier = Unqualified.class)
+    // :: warning: (contracts.precondition.refinement)
     void requiresOdd() {}
 
     @Override
@@ -48,6 +52,7 @@ void requiresUnqual() {}
 
     @Override
     @EnsuresQualifier(expression = "f", qualifier = Unqualified.class)
+    // :: warning: (contracts.postcondition.refinement)
     // :: 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.postcondition.refinement)
     // :: 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.postcondition.refinement)
+  void noOpForTesting() {}
+
+  @EnsuresQualifierIf(result = true, expression = "f1", qualifier = Unqualified.class)
+  // :: warning: (contracts.postcondition.refinement)
+  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.precondition.refinement)
+  void noOpForTesting() {}
 }