From 3367031aa0f9e3aecf39b2485379bdc5c17e3939 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Fri, 19 Jan 2024 13:25:51 -0800 Subject: [PATCH 1/3] Issue warnings when top is passed as a pre/postcondition qualifier --- .../common/basetype/BaseTypeVisitor.java | 34 +++++++++++++++++++ .../common/basetype/messages.properties | 2 ++ 2 files changed, 36 insertions(+) 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..57e9c3c704d 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -1280,6 +1280,8 @@ private void checkContractsAtMethodDeclaration( contract.viewpointAdaptDependentTypeAnnotation( atypeFactory, stringToJavaExpr, methodTree); + checkValidRefinementContract(annotation, contract.kind, methodTree); + JavaExpression exprJe; try { exprJe = StringToJavaExpression.atMethodBody(expressionString, methodTree, checker); @@ -1340,6 +1342,38 @@ private void checkContractsAtMethodDeclaration( } } + /** + * Check whether a qualifier passed to a pre or postcondition 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 contractQualifier the type passed to the qualifier parameter of a contract + * @param contractKind the type of the contract (either a pre or postcondition) + * @param methodTree the method on which the contract is written + */ + private void checkValidRefinementContract( + AnnotationMirror contractQualifier, Contract.Kind contractKind, MethodTree methodTree) { + AnnotationMirror topInContractQualifier = qualHierarchy.getTopAnnotation(contractQualifier); + DeclaredType topDeclaredType = topInContractQualifier.getAnnotationType(); + DeclaredType contractDeclaredType = contractQualifier.getAnnotationType(); + String warningKey = + contractKind == Contract.Kind.POSTCONDITION + || contractKind == 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); + } + } + /** * Scans a {@link JavaExpression} and adds all the parameters in the {@code JavaExpression} to the * passed set. 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. From 578e3d5560c1b06c3e873f19c33ee3ac9d51d5f9 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Sat, 20 Jan 2024 14:11:49 -0800 Subject: [PATCH 2/3] Check contracts in `BaseTypeVisitor.visitAnnotation` --- .../common/basetype/BaseTypeVisitor.java | 90 ++++++++++++------- .../flow/ContractsOverridingSubtyping.java | 4 + 2 files changed, 60 insertions(+), 34 deletions(-) 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 57e9c3c704d..f4aa22d57e2 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,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.PostconditionAnnotation; +import org.checkerframework.framework.qual.PreconditionAnnotation; import org.checkerframework.framework.qual.Unused; import org.checkerframework.framework.source.DiagMessage; import org.checkerframework.framework.source.SourceVisitor; @@ -1280,8 +1284,6 @@ private void checkContractsAtMethodDeclaration( contract.viewpointAdaptDependentTypeAnnotation( atypeFactory, stringToJavaExpr, methodTree); - checkValidRefinementContract(annotation, contract.kind, methodTree); - JavaExpression exprJe; try { exprJe = StringToJavaExpression.atMethodBody(expressionString, methodTree, checker); @@ -1342,38 +1344,6 @@ private void checkContractsAtMethodDeclaration( } } - /** - * Check whether a qualifier passed to a pre or postcondition 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 contractQualifier the type passed to the qualifier parameter of a contract - * @param contractKind the type of the contract (either a pre or postcondition) - * @param methodTree the method on which the contract is written - */ - private void checkValidRefinementContract( - AnnotationMirror contractQualifier, Contract.Kind contractKind, MethodTree methodTree) { - AnnotationMirror topInContractQualifier = qualHierarchy.getTopAnnotation(contractQualifier); - DeclaredType topDeclaredType = topInContractQualifier.getAnnotationType(); - DeclaredType contractDeclaredType = contractQualifier.getAnnotationType(); - String warningKey = - contractKind == Contract.Kind.POSTCONDITION - || contractKind == 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); - } - } - /** * Scans a {@link JavaExpression} and adds all the parameters in the {@code JavaExpression} to the * passed set. @@ -2277,6 +2247,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()); @@ -2333,6 +2311,50 @@ 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(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/tests/flow/ContractsOverridingSubtyping.java b/framework/tests/flow/ContractsOverridingSubtyping.java index cf29e15c9c1..e8323eed72c 100644 --- a/framework/tests/flow/ContractsOverridingSubtyping.java +++ b/framework/tests/flow/ContractsOverridingSubtyping.java @@ -21,6 +21,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 +31,7 @@ boolean ensuresIfOdd() { } @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class) + // :: warning: (contracts.postcondition.refinement) boolean ensuresIfUnqual() { return true; } @@ -48,6 +50,7 @@ void requiresUnqual() {} @Override @EnsuresQualifier(expression = "f", qualifier = Unqualified.class) + // :: warning: (contracts.postcondition.refinement) // :: error: (contracts.postcondition.override) void ensuresOdd() { f = g; @@ -61,6 +64,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; From 583bc2b21db1f65c5e1b633398354e7d75b1ef99 Mon Sep 17 00:00:00 2001 From: James Yoo Date: Sat, 20 Jan 2024 15:37:13 -0800 Subject: [PATCH 3/3] Add tests --- .../common/basetype/BaseTypeVisitor.java | 2 ++ .../tests/flow/ContractsOverridingSubtyping.java | 2 ++ framework/tests/flow/Postcondition.java | 12 ++++++++++++ framework/tests/flow/Precondition.java | 5 +++++ 4 files changed, 21 insertions(+) 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 f4aa22d57e2..b717b76f6e7 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -105,6 +105,7 @@ 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; @@ -2320,6 +2321,7 @@ public Void visitAnnotation(AnnotationTree tree, Void p) { 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()); } diff --git a/framework/tests/flow/ContractsOverridingSubtyping.java b/framework/tests/flow/ContractsOverridingSubtyping.java index e8323eed72c..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) @@ -41,6 +42,7 @@ static class Derived extends Base { @Override @RequiresQualifier(expression = "f", qualifier = Unqualified.class) + // :: warning: (contracts.precondition.refinement) void requiresOdd() {} @Override 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() {} }