diff --git a/annotation-file-utilities/src/test/resources/annotations/tests/classfile/all-annotations.jaif b/annotation-file-utilities/src/test/resources/annotations/tests/classfile/all-annotations.jaif index b85e148acfd5..d06586d9d022 100644 --- a/annotation-file-utilities/src/test/resources/annotations/tests/classfile/all-annotations.jaif +++ b/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 - 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 cefeb158817d..0ba40ea1b0c2 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/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 methods = ElementFilter.methodsIn(annoType.getEnclosedElements()); // Mapping from argument simple name to its annotated type. Map 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 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)) { 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 6e404219653f..2b7d4d17f7fc 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/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. diff --git a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java b/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java index 16cb11061b7f..f4f169140497 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java +++ b/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java @@ -216,10 +216,11 @@ private Set 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 Set getContract( @Nullable AnnotationMirror argumentAnno, @Nullable Map 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); diff --git a/framework/tests/flow/ContractsOverridingSubtyping.java b/framework/tests/flow/ContractsOverridingSubtyping.java index ffa79d9b2755..0c32ee76b85c 100644 --- a/framework/tests/flow/ContractsOverridingSubtyping.java +++ b/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() { diff --git a/framework/tests/flow/Postcondition.java b/framework/tests/flow/Postcondition.java index 527652c3c276..cc3a9c3b534c 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 ***** */ + // :: 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; + } } diff --git a/framework/tests/flow/Precondition.java b/framework/tests/flow/Precondition.java index d3fc9a5de7cc..d789e885629e 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(); } + + // :: warning: [contracts.toptype] + @RequiresQualifier(expression = "f1", qualifier = Unqualified.class) + void noOpForTesting() {} }