diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/ConditionalPostconditionAnnotation.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/ConditionalPostconditionAnnotation.java index 9b7feb69237..4e28a675003 100644 --- a/checker-qual/src/main/java/org/checkerframework/framework/qual/ConditionalPostconditionAnnotation.java +++ b/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. * *

This element is analogous to {@link EnsuresQualifierIf#qualifier()}. */ diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/PostconditionAnnotation.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/PostconditionAnnotation.java index 67bb434e848..1deebf8c53f 100644 --- a/checker-qual/src/main/java/org/checkerframework/framework/qual/PostconditionAnnotation.java +++ b/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. * *

This element is analogous to {@link EnsuresQualifier#qualifier()}. */ diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.java index 95af23ec376..f1cdec923b4 100644 --- a/checker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.java +++ b/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. + * + *

This element is analogous to {@link RequiresQualifier#qualifier()}. + * + * @return the qualifier that must be established as a precondition + */ Class qualifier(); } diff --git a/checker/tests/nullness/PreconditionFieldNotInStore.java b/checker/tests/nullness/PreconditionFieldNotInStore.java index 4c1aa59fe4c..3447cd7eb5b 100644 --- a/checker/tests/nullness/PreconditionFieldNotInStore.java +++ b/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"; } 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..6aca35b12a6 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,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 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. 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 b22038222b5..1f0ac7a54e2 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java +++ b/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; /** @@ -121,6 +122,7 @@ public Set getConditionalPostconditions( private Set getContractsOfKind( ExecutableElement executableElement, Contract.Kind kind, Class clazz) { Set result = new LinkedHashSet<>(); + // Check for a single framework-defined contract annotation. // The result is RequiresQualifier, EnsuresQualifier, EnsuresQualifierIf, or null. AnnotationMirror frameworkContractAnno = @@ -140,6 +142,27 @@ private Set getContractsOfKind( } } + // At this point, `result` contains only framework-defined contract annotations. + Set 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. @@ -155,6 +178,17 @@ private Set 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 expressions = factory.getContractExpressions(kind, anno); Collections.sort(expressions); Boolean ensuresQualifierIfResult = factory.getEnsuresQualifierIfResult(kind, anno); diff --git a/framework/tests/flow/ContractsOverridingSubtyping.java b/framework/tests/flow/ContractsOverridingSubtyping.java index cf29e15c9c1..59105f867ee 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.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; diff --git a/framework/tests/flow/Postcondition.java b/framework/tests/flow/Postcondition.java index 5f8cbd303e7..26d4a5803ad 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.toptype) + void noOpForTesting() {} + + @EnsuresQualifierIf(result = true, expression = "f1", qualifier = Unqualified.class) + // :: warning: (contracts.toptype) + boolean isF1NotSet() { + return f1 == null; + } } diff --git a/framework/tests/flow/Precondition.java b/framework/tests/flow/Precondition.java index 367076e5d1f..754ae8a92e8 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.toptype) + void noOpForTesting() {} }