diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 519b1a944b1..b717b76f6e7 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/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 contracts = atypeFactory.getContractsFromMethod().getContracts(methodElement); + for (Contract contract : contracts) { + checkValidRefinementContract(contract, methodTree); + } + } + List methods = ElementFilter.methodsIn(anno.getEnclosedElements()); // Mapping from argument simple name to its annotated type. Map 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. + * + *

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. + * + *

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, diff --git a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties index effc8dbfe12..0ab24b4956e 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/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. diff --git a/framework/tests/flow/ContractsOverridingSubtyping.java b/framework/tests/flow/ContractsOverridingSubtyping.java index cf29e15c9c1..6602a5d035e 100644 --- a/framework/tests/flow/ContractsOverridingSubtyping.java +++ b/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; diff --git a/framework/tests/flow/Postcondition.java b/framework/tests/flow/Postcondition.java index 5f8cbd303e7..0752c7eb5f8 100644 --- a/framework/tests/flow/Postcondition.java +++ b/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; + } } diff --git a/framework/tests/flow/Precondition.java b/framework/tests/flow/Precondition.java index 367076e5d1f..e5117002c66 100644 --- a/framework/tests/flow/Precondition.java +++ b/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() {} }