diff --git a/.github/workflows/continuous-integration.yml b/.github/workflows/continuous-integration.yml index 9f1c6c1284..14a8478b18 100644 --- a/.github/workflows/continuous-integration.yml +++ b/.github/workflows/continuous-integration.yml @@ -25,13 +25,13 @@ jobs: epVersion: 2.31.0 - os: macos-latest java: 17 - epVersion: 2.32.0 + epVersion: 2.33.0 - os: windows-latest java: 17 - epVersion: 2.32.0 + epVersion: 2.33.0 - os: ubuntu-latest java: 17 - epVersion: 2.32.0 + epVersion: 2.33.0 fail-fast: false runs-on: ${{ matrix.os }} steps: @@ -60,7 +60,7 @@ jobs: ORG_GRADLE_PROJECT_epApiVersion: ${{ matrix.epVersion }} run: ./gradlew codeCoverageReport continue-on-error: true - if: runner.os == 'Linux' && matrix.java == '17' && matrix.epVersion == '2.32.0' && github.repository == 'uber/NullAway' + if: runner.os == 'Linux' && matrix.java == '17' && matrix.epVersion == '2.33.0' && github.repository == 'uber/NullAway' - name: Upload coverage reports to Codecov uses: codecov/codecov-action@v4 with: diff --git a/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java new file mode 100644 index 0000000000..b42842ddbe --- /dev/null +++ b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java @@ -0,0 +1,54 @@ +package com.uber.nullaway.annotations; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * An annotation describing a nullability post-condition for an instance method. Each parameter to + * the annotation should be a field of the enclosing class. The method must ensure that the method + * returns true in case the fields are non-null. The method can also return false in case the fields + * are non-null (inverse logic), and in such case, you must set {@code result} to false. NullAway + * verifies that the property holds. + * + *

Here is an example: + * + * 

+ * class Foo {
+ *     {@literal @}Nullable Object theField;
+ *
+ *     {@literal @}EnsuresNonNullIf("theField", result=true) // "this.theField" is also valid
+ *     boolean hasTheField() {
+ *         return theField != null;
+ *     }
+ *
+ *     void bar() {
+ *         if(!hasTheField()) {
+ *             return;
+ *         }
+ *
+ *         // No error, NullAway knows theField is non-null after call to hasTheField()
+ *         theField.toString();
+ *     }
+ * }
+ *
+ */ +@Retention(RetentionPolicy.CLASS) +@Target({ElementType.METHOD}) +public @interface EnsuresNonNullIf { + /** + * The list of fields that are non-null after the method returns the given result. + * + * @return The list of field names + */ + String[] value(); + + /** + * The return value of the method under which the postcondition holds. The default is set to true, + * which means the method should return true in case fields are non-null. + * + * @return true or false + */ + boolean result() default true; +} diff --git a/build.gradle b/build.gradle index 450c0f3dd2..812063c47a 100644 --- a/build.gradle +++ b/build.gradle @@ -112,7 +112,7 @@ subprojects { project -> project.apply plugin: "com.diffplug.spotless" spotless { java { - googleJavaFormat() + googleJavaFormat(deps.versions.googlejavaformat) } } } @@ -129,7 +129,7 @@ spotless { } } spotlessPredeclare { - java { googleJavaFormat('1.19.2') } + java { googleJavaFormat(deps.versions.googlejavaformat) } groovyGradle { greclipse() } diff --git a/gradle/dependencies.gradle b/gradle/dependencies.gradle index 9d2de3dea1..17b57a98bb 100755 --- a/gradle/dependencies.gradle +++ b/gradle/dependencies.gradle @@ -19,7 +19,7 @@ import org.gradle.util.VersionNumber // The oldest version of Error Prone that we support running on def oldestErrorProneVersion = "2.14.0" // Latest released Error Prone version that we've tested with -def latestErrorProneVersion = "2.32.0" +def latestErrorProneVersion = "2.33.0" // Default to using latest tested Error Prone version def defaultErrorProneVersion = latestErrorProneVersion def errorProneVersionToCompileAgainst = defaultErrorProneVersion @@ -40,7 +40,7 @@ if (project.hasProperty("epApiVersion")) { def versions = [ asm : "9.3", - checkerFramework : "3.43.0", + checkerFramework : "3.48.0", // for comparisons in other parts of the build errorProneLatest : latestErrorProneVersion, // The version of Error Prone used to check NullAway's code. @@ -53,6 +53,7 @@ def versions = [ autoValue : "1.10.2", autoService : "1.1.1", javaparser : "3.26.2", + googlejavaformat : "1.24.0", ] def apt = [ diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index 8e876e1c55..fb602ee2af 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,7 +1,7 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionSha256Sum=1541fa36599e12857140465f3c91a97409b4512501c26f9631fb113e392c5bd1 -distributionUrl=https\://services.gradle.org/distributions/gradle-8.10.1-bin.zip +distributionSha256Sum=31c55713e40233a8303827ceb42ca48a47267a0ad4bab9177123121e71524c26 +distributionUrl=https\://services.gradle.org/distributions/gradle-8.10.2-bin.zip networkTimeout=10000 validateDistributionUrl=true zipStoreBase=GRADLE_USER_HOME diff --git a/jmh/build.gradle b/jmh/build.gradle index 25e8a6ecb2..e1980c6155 100644 --- a/jmh/build.gradle +++ b/jmh/build.gradle @@ -104,8 +104,19 @@ def nullawayReleaseClasspath = configurations.nullawayReleaseDeps.filter({f -> ! def nullawayReleaseProcessorpath = configurations.nullawayReleaseProcessors.asPath -// Extra JVM arguments to expose relevant paths for compiling benchmarks def extraJVMArgs = [ + // needed exports for Error Prone to run + "--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED", + "--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED", + "--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED", + "--add-exports=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED", + "--add-exports=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED", + "--add-exports=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED", + "--add-exports=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED", + "--add-exports=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED", + "--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED", + "--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED", + // expose relevant paths for compiling benchmarks "-Dnullaway.caffeine.sources=${caffeineSourceDir.get()}", "-Dnullaway.caffeine.classpath=$caffeineClasspath", "-Dnullaway.autodispose.sources=${autodisposeSourceDir.get()}", diff --git a/nullaway/src/main/java/com/uber/nullaway/NullAway.java b/nullaway/src/main/java/com/uber/nullaway/NullAway.java index bc83d5a377..b6eb58651b 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullAway.java +++ b/nullaway/src/main/java/com/uber/nullaway/NullAway.java @@ -2453,10 +2453,11 @@ private boolean mayBeNullExpr(VisitorState state, ExpressionTree expr) { case NEW_CLASS: case NEW_ARRAY: case ARRAY_TYPE: + // Lambdas may return null, but the lambda literal itself should not be null case LAMBDA_EXPRESSION: - // Lambdas may return null, but the lambda literal itself should not be null + // These cannot be null; the compiler would catch it case MEMBER_REFERENCE: - // These cannot be null; the compiler would catch it + // result of compound assignment cannot be null case MULTIPLY_ASSIGNMENT: case DIVIDE_ASSIGNMENT: case REMAINDER_ASSIGNMENT: @@ -2468,9 +2469,8 @@ private boolean mayBeNullExpr(VisitorState state, ExpressionTree expr) { case AND_ASSIGNMENT: case XOR_ASSIGNMENT: case OR_ASSIGNMENT: - // result of compound assignment cannot be null + // rest are for auto-boxing case PLUS: - // rest are for auto-boxing case MINUS: case MULTIPLY: case DIVIDE: diff --git a/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java b/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java index 81e0d846bc..fb605a3254 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java +++ b/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java @@ -231,14 +231,7 @@ public static Stream getAllAnnotations(Symbol symbol */ public static @Nullable Set getAnnotationValueArray( Symbol.MethodSymbol methodSymbol, String annotName, boolean exactMatch) { - AnnotationMirror annot = null; - for (AnnotationMirror annotationMirror : methodSymbol.getAnnotationMirrors()) { - String name = AnnotationUtils.annotationName(annotationMirror); - if ((exactMatch && name.equals(annotName)) || (!exactMatch && name.endsWith(annotName))) { - annot = annotationMirror; - break; - } - } + AnnotationMirror annot = findAnnotation(methodSymbol, annotName, exactMatch); if (annot == null) { return null; } @@ -256,6 +249,33 @@ public static Stream getAllAnnotations(Symbol symbol return null; } + /** + * Retrieve the specific annotation of a method. + * + * @param methodSymbol A method to check for the annotation. + * @param annotName The qualified name or simple name of the annotation depending on the value of + * {@code exactMatch}. + * @param exactMatch If true, the annotation name must match the full qualified name given in + * {@code annotName}, otherwise, simple names will be checked. + * @return an {@code AnnotationMirror} representing that annotation, or null in case the + * annotation with a given name {@code annotName} doesn't exist in {@code methodSymbol}. + */ + public static @Nullable AnnotationMirror findAnnotation( + Symbol.MethodSymbol methodSymbol, String annotName, boolean exactMatch) { + AnnotationMirror annot = null; + for (AnnotationMirror annotationMirror : methodSymbol.getAnnotationMirrors()) { + String name = AnnotationUtils.annotationName(annotationMirror); + if ((exactMatch && name.equals(annotName)) || (!exactMatch && name.endsWith(annotName))) { + annot = annotationMirror; + break; + } + } + if (annot == null) { + return null; + } + return annot; + } + /** * Works for method parameters defined either in source or in class files * diff --git a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPath.java b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPath.java index 78fe3d8f61..a75fd858a9 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPath.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPath.java @@ -287,7 +287,7 @@ && castToNonNull(receiver.getTree()).getKind().equals(Tree.Kind.IDENTIFIER) && (receiver.toString().equals("Integer") || receiver.toString().equals("Long"))) { return argumentToMapKeySpecifier(arguments.get(0), state, apContext); } - // Fine to fallthrough: + // Fine to fallthrough: default: // Every other type of expression, including variables, field accesses, new A(...), etc. return getAccessPathForNode(argument, state, apContext); // Every AP is a MapKey too @@ -488,8 +488,8 @@ && isBoxingMethod(ASTHelpers.getSymbol(methodInvocationTree))) { break; } } - // Cascade to default, symbol is not a constant field - // fall through + // Cascade to default, symbol is not a constant field + // fall through default: return null; // Not an AP } diff --git a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java index 8c2dae9151..6487e5d34a 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java @@ -21,8 +21,8 @@ import static com.uber.nullaway.NullabilityUtil.castToNonNull; import com.google.common.base.Preconditions; -import com.google.common.collect.ImmutableList; import com.google.errorprone.VisitorState; +import com.google.errorprone.dataflow.nullnesspropagation.NullnessAnalysis; import com.sun.source.tree.Tree; import com.sun.source.util.TreePath; import com.sun.tools.javac.util.Context; @@ -157,25 +157,7 @@ public Set getNonnullFieldsOfReceiverAtExit(TreePath path, Context cont // be conservative and say nothing is initialized return Collections.emptySet(); } - return getNonnullReceiverFields(nullnessResult); - } - - private Set getNonnullReceiverFields(NullnessStore nullnessResult) { - Set nonnullAccessPaths = nullnessResult.getAccessPathsWithValue(Nullness.NONNULL); - Set result = new LinkedHashSet<>(); - for (AccessPath ap : nonnullAccessPaths) { - // A null root represents the receiver - if (ap.getRoot() == null) { - ImmutableList elements = ap.getElements(); - if (elements.size() == 1) { - Element elem = elements.get(0).getJavaElement(); - if (elem.getKind().equals(ElementKind.FIELD)) { - result.add(elem); - } - } - } - } - return result; + return nullnessResult.getNonNullReceiverFields(); } /** @@ -190,7 +172,7 @@ public Set getNonnullFieldsOfReceiverBefore(TreePath path, Context cont if (store == null) { return Collections.emptySet(); } - return getNonnullReceiverFields(store); + return store.getNonNullReceiverFields(); } /** diff --git a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java index 49dca06fac..88817b1a61 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java @@ -852,7 +852,8 @@ public TransferResult visitSuper( @Override public TransferResult visitReturn( ReturnNode returnNode, TransferInput input) { - handler.onDataflowVisitReturn(returnNode.getTree(), input.getThenStore(), input.getElseStore()); + handler.onDataflowVisitReturn( + returnNode.getTree(), state, input.getThenStore(), input.getElseStore()); return noStoreChanges(NULLABLE, input); } diff --git a/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java b/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java index 8225d5c143..43fd3d4714 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java @@ -19,6 +19,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.collect.Sets.intersection; +import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import com.google.errorprone.VisitorState; import com.uber.nullaway.Nullness; @@ -30,6 +31,7 @@ import java.util.function.Predicate; import java.util.stream.Collectors; import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; import org.checkerframework.nullaway.dataflow.analysis.Store; import org.checkerframework.nullaway.dataflow.cfg.node.FieldAccessNode; import org.checkerframework.nullaway.dataflow.cfg.node.LocalVariableNode; @@ -261,6 +263,39 @@ public NullnessStore filterAccessPaths(Predicate pred) { .collect(Collectors.toMap(Map.Entry::getKey, Map.Entry::getValue))); } + /** + * Return all the fields in the store that are Non-Null. + * + * @return Set of fields (represented as {@code Element}s) that are non-null + */ + public Set getNonNullReceiverFields() { + return getReceiverFields(Nullness.NONNULL); + } + + /** + * Return all the fields in the store that hold the {@code nullness} state. + * + * @param nullness The {@code Nullness} state + * @return Set of fields (represented as {@code Element}s) with the given {@code nullness}. + */ + public Set getReceiverFields(Nullness nullness) { + Set nonnullAccessPaths = this.getAccessPathsWithValue(nullness); + Set result = new LinkedHashSet<>(); + for (AccessPath ap : nonnullAccessPaths) { + // A null root represents the receiver + if (ap.getRoot() == null) { + ImmutableList elements = ap.getElements(); + if (elements.size() == 1) { + Element elem = elements.get(0).getJavaElement(); + if (elem.getKind().equals(ElementKind.FIELD)) { + result.add(elem); + } + } + } + } + return result; + } + /** class for building up instances of the store. */ public static final class Builder { private final Map contents; diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java index 3664529998..d9f6ba13cf 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java @@ -174,7 +174,7 @@ public NullnessHint onDataflowVisitFieldAccess( @Override public void onDataflowVisitReturn( - ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore) { + ReturnTree tree, VisitorState state, NullnessStore thenStore, NullnessStore elseStore) { // NoOp } diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java index df5293d690..f1a5997da2 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java @@ -220,9 +220,9 @@ public NullnessHint onDataflowVisitFieldAccess( @Override public void onDataflowVisitReturn( - ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore) { + ReturnTree tree, VisitorState state, NullnessStore thenStore, NullnessStore elseStore) { for (Handler h : handlers) { - h.onDataflowVisitReturn(tree, thenStore, elseStore); + h.onDataflowVisitReturn(tree, state, thenStore, elseStore); } } diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java index f8a11afe85..298d01d7db 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java @@ -269,12 +269,14 @@ NullnessHint onDataflowVisitFieldAccess( * Called when the Dataflow analysis visits a return statement. * * @param tree The AST node for the return statement being matched. + * @param state The current visitor state * @param thenStore The NullnessStore for the true case of the expression inside the return * statement. * @param elseStore The NullnessStore for the false case of the expression inside the return * statement. */ - void onDataflowVisitReturn(ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore); + void onDataflowVisitReturn( + ReturnTree tree, VisitorState state, NullnessStore thenStore, NullnessStore elseStore); /** * Called when the Dataflow analysis visits the result expression inside the body of lambda. diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/Handlers.java b/nullaway/src/main/java/com/uber/nullaway/handlers/Handlers.java index c8b81cbec0..8804f9149e 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/Handlers.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/Handlers.java @@ -27,6 +27,7 @@ import com.uber.nullaway.handlers.contract.ContractCheckHandler; import com.uber.nullaway.handlers.contract.ContractHandler; import com.uber.nullaway.handlers.contract.fieldcontract.EnsuresNonNullHandler; +import com.uber.nullaway.handlers.contract.fieldcontract.EnsuresNonNullIfHandler; import com.uber.nullaway.handlers.contract.fieldcontract.RequiresNonNullHandler; import com.uber.nullaway.handlers.temporary.FluentFutureHandler; @@ -69,6 +70,7 @@ public static Handler buildDefault(Config config) { handlerListBuilder.add(new GrpcHandler()); handlerListBuilder.add(new RequiresNonNullHandler()); handlerListBuilder.add(new EnsuresNonNullHandler()); + handlerListBuilder.add(new EnsuresNonNullIfHandler()); handlerListBuilder.add(new SynchronousCallbackHandler()); if (config.serializationIsActive() && config.getSerializationConfig().fieldInitInfoEnabled) { handlerListBuilder.add( diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java b/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java index 48e1ce6052..c411522da7 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java @@ -595,7 +595,7 @@ public NullnessStore.Builder onDataflowInitialStore( @Override public void onDataflowVisitReturn( - ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore) { + ReturnTree tree, VisitorState state, NullnessStore thenStore, NullnessStore elseStore) { Tree filterTree = returnToEnclosingMethodOrLambda.get(tree); if (filterTree != null) { assert (filterTree instanceof MethodTree || filterTree instanceof LambdaExpressionTree); diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullHandler.java index 62cde6a7e1..ebce29f582 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullHandler.java @@ -40,7 +40,6 @@ import com.uber.nullaway.handlers.MethodAnalysisContext; import com.uber.nullaway.handlers.contract.ContractUtils; import java.util.Collections; -import java.util.Iterator; import java.util.Set; import java.util.stream.Collectors; import javax.lang.model.element.VariableElement; @@ -124,46 +123,8 @@ protected void validateOverridingRules( VisitorState state, MethodTree tree, Symbol.MethodSymbol overriddenMethod) { - Set overriddenFieldNames = getAnnotationValueArray(overriddenMethod, annotName, false); - if (overriddenFieldNames == null) { - return; - } - if (overridingFieldNames == null) { - overridingFieldNames = Collections.emptySet(); - } - if (overridingFieldNames.containsAll(overriddenFieldNames)) { - return; - } - overriddenFieldNames.removeAll(overridingFieldNames); - - StringBuilder errorMessage = new StringBuilder(); - errorMessage - .append( - "postcondition inheritance is violated, this method must guarantee that all fields written in the @EnsuresNonNull annotation of overridden method ") - .append(castToNonNull(ASTHelpers.enclosingClass(overriddenMethod)).getSimpleName()) - .append(".") - .append(overriddenMethod.getSimpleName()) - .append(" are @NonNull at exit point as well. Fields ["); - Iterator iterator = overriddenFieldNames.iterator(); - while (iterator.hasNext()) { - errorMessage.append(iterator.next()); - if (iterator.hasNext()) { - errorMessage.append(", "); - } - } - errorMessage.append( - "] must explicitly appear as parameters at this method @EnsuresNonNull annotation"); - state.reportMatch( - analysis - .getErrorBuilder() - .createErrorDescription( - new ErrorMessage( - ErrorMessage.MessageTypes.WRONG_OVERRIDE_POSTCONDITION, - errorMessage.toString()), - tree, - analysis.buildDescription(tree), - state, - null)); + FieldContractUtils.ensureStrictPostConditionInheritance( + annotName, overridingFieldNames, analysis, state, tree, overriddenMethod); } /** diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java new file mode 100644 index 0000000000..b4b116c545 --- /dev/null +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java @@ -0,0 +1,323 @@ +/* + * Copyright (c) 2024 Uber Technologies, Inc. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in + * all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN + * THE SOFTWARE. + */ + +package com.uber.nullaway.handlers.contract.fieldcontract; + +import static com.uber.nullaway.NullabilityUtil.castToNonNull; +import static com.uber.nullaway.NullabilityUtil.getAnnotationValueArray; + +import com.google.errorprone.VisitorState; +import com.google.errorprone.util.ASTHelpers; +import com.sun.source.tree.LiteralTree; +import com.sun.source.tree.MethodTree; +import com.sun.source.tree.ReturnTree; +import com.sun.source.tree.Tree; +import com.sun.source.util.TreePath; +import com.sun.source.util.TreePathScanner; +import com.sun.tools.javac.code.Symbol; +import com.uber.nullaway.ErrorMessage; +import com.uber.nullaway.NullAway; +import com.uber.nullaway.NullabilityUtil; +import com.uber.nullaway.Nullness; +import com.uber.nullaway.dataflow.AccessPath; +import com.uber.nullaway.dataflow.AccessPathNullnessPropagation; +import com.uber.nullaway.dataflow.NullnessStore; +import com.uber.nullaway.handlers.AbstractFieldContractHandler; +import com.uber.nullaway.handlers.MethodAnalysisContext; +import com.uber.nullaway.handlers.contract.ContractUtils; +import java.util.HashSet; +import java.util.Map; +import java.util.Set; +import java.util.stream.Collectors; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.AnnotationValue; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.VariableElement; +import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode; +import org.jspecify.annotations.Nullable; + +/** + * This Handler parses {@code @EnsuresNonNullIf} annotation and when the annotated method is + * invoked, it marks the annotated fields as not-null in the following flows. + */ +public class EnsuresNonNullIfHandler extends AbstractFieldContractHandler { + + // List of return trees in the method under analysis + // This list is built in a way that return trees inside lambdas + // or anonymous classes aren't included. + private final Set returnTreesInMethodUnderAnalysis = new HashSet<>(); + + // The MethodTree and MethodAnalysisContext of the EnsureNonNullIf method + // under current semantic validation + // They are set to null when no methods are being validated. + private @Nullable MethodTree methodTreeUnderAnalysis; + private @Nullable MethodAnalysisContext methodAnalysisContextUnderAnalysis; + + public EnsuresNonNullIfHandler() { + super("EnsuresNonNullIf"); + } + + /** + * Validates whether all parameters mentioned in the @EnsuresNonNullIf annotation are guaranteed + * to be {@code @NonNull} at exit point of this method. + */ + @Override + protected boolean validateAnnotationSemantics( + MethodTree tree, MethodAnalysisContext methodAnalysisContext) { + if (tree.getBody() == null) { + return true; + } + + // clean up state variables, as we are visiting a new annotated method + methodTreeUnderAnalysis = tree; + methodAnalysisContextUnderAnalysis = methodAnalysisContext; + returnTreesInMethodUnderAnalysis.clear(); + + VisitorState state = methodAnalysisContext.state(); + NullAway analysis = methodAnalysisContext.analysis(); + + // we visit the tree of the method, just so we can build a map between + // return statements and their enclosing methods + buildUpReturnToEnclosingMethodMap(state); + + // if no returns, then, this method doesn't return boolean, and it's wrong + if (returnTreesInMethodUnderAnalysis.isEmpty()) { + raiseError( + tree, state, "Method is annotated with @EnsuresNonNullIf but does not return boolean"); + return false; + } + + // We force the nullness analysis of the method under validation + // The semantic validation will happen at each ReturnTree visit of the data-flow engine + analysis + .getNullnessAnalysis(state) + .forceRunOnMethod(new TreePath(state.getPath(), tree), state.context); + + // Clean up state + methodTreeUnderAnalysis = null; + methodAnalysisContextUnderAnalysis = null; + returnTreesInMethodUnderAnalysis.clear(); + + return true; + } + + private void buildUpReturnToEnclosingMethodMap(VisitorState methodState) { + returnTreesInMethodUnderAnalysis.clear(); + new TreePathScanner() { + @Override + public Void visitReturn(ReturnTree node, Void unused) { + TreePath enclosingMethod = + NullabilityUtil.findEnclosingMethodOrLambdaOrInitializer(getCurrentPath()); + if (enclosingMethod == null) { + throw new RuntimeException("no enclosing method, lambda or initializer!"); + } + + // We only add returns that are directly in the method under analysis + if (enclosingMethod.getLeaf().equals(methodTreeUnderAnalysis)) { + returnTreesInMethodUnderAnalysis.add(node); + } + return super.visitReturn(node, null); + } + }.scan(methodState.getPath(), null); + } + + /* + * Sub-classes can only strengthen the post-condition. + * We check if the list in the child classes is at least the same as in the parent class. + */ + @Override + protected void validateOverridingRules( + Set overridingFieldNames, + NullAway analysis, + VisitorState state, + MethodTree tree, + Symbol.MethodSymbol overriddenMethod) { + FieldContractUtils.ensureStrictPostConditionInheritance( + annotName, overridingFieldNames, analysis, state, tree, overriddenMethod); + } + + @Override + public void onDataflowVisitReturn( + ReturnTree returnTree, VisitorState state, NullnessStore thenStore, NullnessStore elseStore) { + // We only explore return statements that is inside + // the method under validation + if (!returnTreesInMethodUnderAnalysis.contains(returnTree)) { + return; + } + + // Get the declared configuration of the EnsureNonNullIf method under analysis + Symbol.MethodSymbol methodSymbolUnderAnalysis = + NullabilityUtil.castToNonNull(methodAnalysisContextUnderAnalysis).methodSymbol(); + + Set fieldNames = getAnnotationValueArray(methodSymbolUnderAnalysis, annotName, false); + if (fieldNames == null) { + throw new RuntimeException("List of field names shouldn't be null"); + } + + boolean trueIfNonNull = getResultValueFromAnnotation(methodSymbolUnderAnalysis); + + // We extract all the fields that are considered non-null by the data-flow engine + // We pick the "thenStore" case in case result is set to true + // or "elseStore" in case result is set to false + // and check whether the non-full fields match the ones in the annotation parameter + NullnessStore chosenStore = trueIfNonNull ? thenStore : elseStore; + Set nonNullFieldsInPath = + chosenStore.getNonNullReceiverFields().stream() + .map(e -> e.getSimpleName().toString()) + .collect(Collectors.toSet()); + boolean allFieldsAreNonNull = nonNullFieldsInPath.containsAll(fieldNames); + + // Whether the return true expression evaluates to a boolean literal or not. If null, then not + // a boolean literal. + Boolean expressionAsBoolean = null; + if (returnTree.getExpression() instanceof LiteralTree) { + LiteralTree expressionAsLiteral = (LiteralTree) returnTree.getExpression(); + if (expressionAsLiteral.getValue() instanceof Boolean) { + expressionAsBoolean = (Boolean) expressionAsLiteral.getValue(); + } + } + + /* + * Identify whether the expression is a boolean literal and whether + * it evaluates to the correct literal. + * - If result param in annotation is set to true, then expression should return true. + * - If result param in annotation is set to false, then expression should return false. + */ + boolean isBooleanLiteral = expressionAsBoolean != null; + boolean evaluatesToNonNullLiteral = + expressionAsBoolean != null && (trueIfNonNull == expressionAsBoolean); + + /* + * Decide whether the semantics of this ReturnTree are correct. + * The decision is as follows: + * + * If all fields in the path are verified: + * - Semantics are valid + * + * If fields in path aren't verified: + * - If the literal boolean is the opposite of the configured non-null boolean, semantics + * are then correct, as the method correctly returns in case the semantics don't hold. + * - Otherwise, semantics are wrong, as the method incorrectly returns. + * - If the expression isn't a literal boolean, then semantics are wrong, as we + * assume it is possible that the configured non-null boolean can be returned. + */ + if (!allFieldsAreNonNull) { + if (evaluatesToNonNullLiteral || !isBooleanLiteral) { + fieldNames.removeAll(nonNullFieldsInPath); + String message = + String.format( + "Method is annotated with @EnsuresNonNullIf but does not ensure fields %s", + fieldNames); + raiseError(returnTree, state, message); + } + } + } + + private void raiseError(Tree returnTree, VisitorState state, String message) { + NullAway analysis = + NullabilityUtil.castToNonNull(methodAnalysisContextUnderAnalysis).analysis(); + + state.reportMatch( + analysis + .getErrorBuilder() + .createErrorDescription( + new ErrorMessage(ErrorMessage.MessageTypes.POSTCONDITION_NOT_SATISFIED, message), + returnTree, + analysis.buildDescription(returnTree), + state, + null)); + } + + private boolean getResultValueFromAnnotation(Symbol.MethodSymbol methodSymbol) { + AnnotationMirror annot = NullabilityUtil.findAnnotation(methodSymbol, annotName, false); + if (annot == null) { + throw new RuntimeException("Annotation should not be null at this point"); + } + + Map elementValues = + annot.getElementValues(); + for (Map.Entry entry : + elementValues.entrySet()) { + ExecutableElement elem = entry.getKey(); + if (elem.getSimpleName().contentEquals("result")) { + return (boolean) entry.getValue().getValue(); + } + } + + // Default value of the 'result' field is true + return true; + } + + /** + * On every method annotated with {@link EnsuresNonNullIf}, this method injects the {@code + * Nonnull} value for the class fields given in the {@code @EnsuresNonNullIf} parameter to the + * dataflow analysis. + */ + @Override + public NullnessHint onDataflowVisitMethodInvocation( + MethodInvocationNode node, + Symbol.MethodSymbol methodSymbol, + VisitorState state, + AccessPath.AccessPathContext apContext, + AccessPathNullnessPropagation.SubNodeValues inputs, + AccessPathNullnessPropagation.Updates thenUpdates, + AccessPathNullnessPropagation.Updates elseUpdates, + AccessPathNullnessPropagation.Updates bothUpdates) { + if (node.getTree() == null) { + return super.onDataflowVisitMethodInvocation( + node, methodSymbol, state, apContext, inputs, thenUpdates, elseUpdates, bothUpdates); + } + + Set fieldNames = getAnnotationValueArray(methodSymbol, annotName, false); + if (fieldNames != null) { + fieldNames = ContractUtils.trimReceivers(fieldNames); + boolean trueIfNonNull = getResultValueFromAnnotation(methodSymbol); + // chosenUpdates is set to the thenUpdates or elseUpdates appropriately given the annotation's + // result value + AccessPathNullnessPropagation.Updates chosenUpdates = + trueIfNonNull ? thenUpdates : elseUpdates; + for (String fieldName : fieldNames) { + VariableElement field = + getInstanceFieldOfClass( + castToNonNull(ASTHelpers.enclosingClass(methodSymbol)), fieldName); + if (field == null) { + // Invalid annotation, will result in an error during validation. + continue; + } + AccessPath accessPath = + AccessPath.fromBaseAndElement(node.getTarget().getReceiver(), field, apContext); + if (accessPath == null) { + // Also likely to be an invalid annotation, will result in an error during validation. + continue; + } + + // The call to the EnsuresNonNullIf method ensures that the field is not null in the chosen + // updates. + // In here, we assume that the annotated method is already validated. + chosenUpdates.set(accessPath, Nullness.NONNULL); + } + } + + return super.onDataflowVisitMethodInvocation( + node, methodSymbol, state, apContext, inputs, thenUpdates, elseUpdates, bothUpdates); + } +} diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/FieldContractUtils.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/FieldContractUtils.java new file mode 100644 index 0000000000..ea25480aca --- /dev/null +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/FieldContractUtils.java @@ -0,0 +1,95 @@ +/* + * Copyright (c) 2024 Uber Technologies, Inc. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in + * all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN + * THE SOFTWARE. + */ +package com.uber.nullaway.handlers.contract.fieldcontract; + +import static com.uber.nullaway.NullabilityUtil.castToNonNull; +import static com.uber.nullaway.NullabilityUtil.getAnnotationValueArray; + +import com.google.errorprone.VisitorState; +import com.google.errorprone.util.ASTHelpers; +import com.sun.source.tree.MethodTree; +import com.sun.tools.javac.code.Symbol; +import com.uber.nullaway.ErrorMessage; +import com.uber.nullaway.NullAway; +import java.util.Collections; +import java.util.Set; + +public class FieldContractUtils { + + /** + * Checks that the fields mentioned in the annotation of the overridden method are also mentioned + * in the annotation of the overriding method. If not, reports an error. + * + * @param annotName name of the annotation + * @param overridingFieldNames set of fields mentioned in the overriding method's annotation + * @param analysis NullAway instance + * @param state the visitor state + * @param tree tree for the overriding method + * @param overriddenMethod the method that is being overridden + */ + public static void ensureStrictPostConditionInheritance( + String annotName, + Set overridingFieldNames, + NullAway analysis, + VisitorState state, + MethodTree tree, + Symbol.MethodSymbol overriddenMethod) { + Set overriddenFieldNames = getAnnotationValueArray(overriddenMethod, annotName, false); + if (overriddenFieldNames == null) { + return; + } + if (overridingFieldNames == null) { + overridingFieldNames = Collections.emptySet(); + } + if (overridingFieldNames.containsAll(overriddenFieldNames)) { + return; + } + overriddenFieldNames.removeAll(overridingFieldNames); + + StringBuilder errorMessage = new StringBuilder(); + errorMessage + .append( + "postcondition inheritance is violated, this method must guarantee that all fields written in the @") + .append(annotName) + .append(" annotation of overridden method ") + .append(castToNonNull(ASTHelpers.enclosingClass(overriddenMethod)).getSimpleName()) + .append(".") + .append(overriddenMethod.getSimpleName()) + .append(" are @NonNull at exit point as well. Fields [") + .append(String.join(", ", overriddenFieldNames)) + .append("] must explicitly appear as parameters at this method @") + .append(annotName) + .append(" annotation"); + + state.reportMatch( + analysis + .getErrorBuilder() + .createErrorDescription( + new ErrorMessage( + ErrorMessage.MessageTypes.WRONG_OVERRIDE_POSTCONDITION, + errorMessage.toString()), + tree, + analysis.buildDescription(tree), + state, + null)); + } +} diff --git a/nullaway/src/test/java/com/uber/nullaway/CoreTests.java b/nullaway/src/test/java/com/uber/nullaway/CoreTests.java index f3eb4d3711..a851d8efb2 100644 --- a/nullaway/src/test/java/com/uber/nullaway/CoreTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/CoreTests.java @@ -1053,4 +1053,20 @@ public void testStaticImportFromSubclass() { "}") .doTest(); } + + /** testing for no Checker Framework crash */ + @Test + public void ternaryBothCasesNull() { + defaultCompilationHelper + .addSourceLines( + "TestCase.java", + "package com.uber;", + "import org.jspecify.annotations.Nullable;", + "public class TestCase {", + " public static @Nullable String foo(String x) {", + " return x.isEmpty() ? null : null;", + " }", + "}") + .doTest(); + } } diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java new file mode 100644 index 0000000000..ea7655f720 --- /dev/null +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -0,0 +1,896 @@ +package com.uber.nullaway; + +import org.junit.Ignore; +import org.junit.Test; + +public class EnsuresNonNullIfTests extends NullAwayTestsBase { + + @Test + public void correctUse() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(\"nullableItem\")", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " public int runOk() {", + " if(!hasNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void correctUse_declarationReversed() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " public int runOk() {", + " if(!hasNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " return 0;", + " }", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void correctAndIncorrectUse() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " public int runOk() {", + " if(hasNullableItem()) {", + " nullableItem.call();", + " }", + " // BUG: Diagnostic contains: dereferenced expression nullableItem is @Nullable", + " nullableItem.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void correctUse_moreComplexFlow() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " if(nullableItem != null) {", + " return true;", + " } else {", + " return false;", + " }", + " }", + " public int runOk() {", + " if(!hasNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void multipleEnsuresNonNullIfMethods() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @Nullable Item nullableItem2;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " @EnsuresNonNullIf(value=\"nullableItem2\", result=true)", + " public boolean hasNullableItem2() {", + " return nullableItem2 != null;", + " }", + " public int runOk() {", + " if(!hasNullableItem() || !hasNullableItem2()) {", + " return 1;", + " }", + " nullableItem.call();", + " nullableItem2.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void multipleEnsuresNonNullIfMethods_2() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @Nullable Item nullableItem2;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " @EnsuresNonNullIf(value=\"nullableItem2\", result=true)", + " public boolean hasNullableItem2() {", + " return nullableItem2 != null;", + " }", + " public int runOk() {", + " if(hasNullableItem() && hasNullableItem2()) {", + " nullableItem.call();", + " nullableItem2.call();", + " return 1;", + " }", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void multipleEnsuresNonNullIfMethods_3() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @Nullable Item nullableItem2;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " @EnsuresNonNullIf(value=\"nullableItem2\", result=true)", + " public boolean hasNullableItem2() {", + " return nullableItem2 != null;", + " }", + " public int runOk() {", + " if(hasNullableItem() || hasNullableItem2()) {", + " // BUG: Diagnostic contains: dereferenced expression nullableItem is @Nullable", + " nullableItem.call();", + " // BUG: Diagnostic contains: dereferenced expression nullableItem2 is @Nullable", + " nullableItem2.call();", + " return 1;", + " }", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void multipleFieldsInSingleAnnotation() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @Nullable Item nullableItem2;", + " @EnsuresNonNullIf(value={\"nullableItem\", \"nullableItem2\"}, result=true)", + " public boolean hasNullableItems() {", + " return nullableItem != null && nullableItem2 != null;", + " }", + " public int runOk() {", + " if(!hasNullableItems()) {", + " return 1;", + " }", + " nullableItem.call();", + " nullableItem2.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void multipleFieldsInSingleAnnotation_oneNotValidated() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @Nullable Item nullableItem2;", + " @EnsuresNonNullIf(value={\"nullableItem\", \"nullableItem2\"}, result=true)", + " public boolean hasNullableItems() {", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem2]", + " return nullableItem != null;", + " }", + " public int runOk() {", + " if(!hasNullableItems()) {", + " return 1;", + " }", + " nullableItem.call();", + " nullableItem2.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void possibleDeferencedExpression() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @Nullable Item nullableItem2;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " @EnsuresNonNullIf(value=\"nullableItem2\", result=true)", + " public boolean hasNullableItem2() {", + " return nullableItem2 != null;", + " }", + " public int runOk() {", + " if(!hasNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " // BUG: Diagnostic contains: dereferenced expression nullableItem2 is @Nullable", + " nullableItem2.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void ensuresNonNullMethodUsingThis() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " return this.nullableItem != null;", + " }", + " public void runOk() {", + " if(!hasNullableItem()) {", + " return;", + " }", + " nullableItem.call();", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void postConditions_Inheritance() { + defaultCompilationHelper + .addSourceLines( + "SuperClass.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class SuperClass {", + " @Nullable Item a;", + " @Nullable Item b;", + " @EnsuresNonNullIf(value=\"a\", result=true)", + " public boolean hasA() {", + " return a != null;", + " }", + " @EnsuresNonNullIf(value=\"b\", result=true)", + " public boolean hasB() {", + " return b != null;", + " }", + " public void doSomething() {", + " if(hasA()) {", + " a.call();", + " }", + " }", + "}") + .addSourceLines( + "ChildLevelOne.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class ChildLevelOne extends SuperClass {", + " @Nullable Item c;", + " @EnsuresNonNullIf(value=\"c\", result=true)", + " // BUG: Diagnostic contains: postcondition inheritance is violated, this method must guarantee that all fields written in the @EnsuresNonNullIf annotation of overridden method SuperClass.hasA are @NonNull at exit point as well. Fields [a] must explicitly appear as parameters at this method @EnsuresNonNullIf annotation", + " public boolean hasA() {", + " return c != null;", + " }", + " @EnsuresNonNullIf(value={\"b\", \"c\"}, result=true)", + " public boolean hasB() {", + " return b != null && c != null;", + " }", + " public void doSomething() {", + " if(hasB()) {", + " b.call();", + " }", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + /** Tests related to setting return=false */ + @Test + public void setResultToFalse() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=false)", + " public boolean doesNotHaveNullableItem() {", + " return nullableItem == null;", + " }", + " public int runOk() {", + " if(doesNotHaveNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void setResultToFalse_multipleElements_wrongSemantics_1() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @Nullable Item nullableItem2;", + " @EnsuresNonNullIf(value={\"nullableItem\",\"nullableItem2\"}, result=false)", + " public boolean doesNotHaveNullableItem() {", + " // If nullableItem != null but nullableItem2 == null, then this function returns false. So returning false does not guarantee that both the fields are non-null.", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem, nullableItem2]", + " return nullableItem == null && nullableItem2 == null;", + " }", + " public int runOk() {", + " if(doesNotHaveNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " nullableItem2.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void setResultToFalse_multipleElements_correctSemantics() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @Nullable Item nullableItem2;", + " @EnsuresNonNullIf(value={\"nullableItem\",\"nullableItem2\"}, result=false)", + " public boolean nullableItemsAreNull() {", + " // If the function returns false, we know that neither of the fields can be null, i.e., both are non-null.", + " return nullableItem == null || nullableItem2 == null;", + " }", + " public int runOk() {", + " if(nullableItemsAreNull()) {", + " return 1;", + " }", + " nullableItem.call();", + " nullableItem2.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void setResultToFalse_multipleElements_correctSemantics_2() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @Nullable Item nullableItem2;", + " @EnsuresNonNullIf(value={\"nullableItem\",\"nullableItem2\"}, result=false)", + " public boolean nullableItemsAreNull() {", + " // If the function returns false, we know that neither of the fields can be null, i.e., both are non-null.", + " if(nullableItem == null || nullableItem2 == null) {", + " return true;", + " } else {", + " return false;", + " }", + " }", + " public int runOk() {", + " if(nullableItemsAreNull()) {", + " return 1;", + " }", + " nullableItem.call();", + " nullableItem2.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void setResultToFalse_multipleElements_correctSemantics_dereferenceFound() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @Nullable Item nullableItem2;", + " @EnsuresNonNullIf(value={\"nullableItem\",\"nullableItem2\"}, result=false)", + " public boolean nullableItemsAreNull() {", + " // If the function returns false, we know that neither of the fields can be null, i.e., both are non-null.", + " return nullableItem == null || nullableItem2 == null;", + " }", + " public int runOk() {", + " // BUG: Diagnostic contains: dereferenced expression nullableItem is @Nullable", + " nullableItem.call();", + " // BUG: Diagnostic contains: dereferenced expression nullableItem2 is @Nullable", + " nullableItem2.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + /******************************************************** + * Tests related to semantic issues + ******************************************************** + */ + @Test + public void semanticIssues_doesntEnsureNonNullabilityOfFields() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " if(nullableItem != null) {", + " return false;", + " } else {", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", + " return true;", + " }", + " }", + " public int runOk() {", + " if(!hasNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void noSemanticIssues_resultFalse() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=false)", + " public boolean doesNotHaveNullableItem() {", + " if(nullableItem != null) {", + " return false;", + " } else {", + " return true;", + " }", + " }", + " public int runOk() {", + " if(doesNotHaveNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void semanticIssue_combinationOfExpressionAndLiteralBoolean_2() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", + " return false || nullableItem != null;", + " }", + " public int runOk() {", + " if(!hasNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void semanticIssue_combinationOfExpressionAndLiteralBoolean() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", + " return true || nullableItem != null;", + " }", + " public int runOk() {", + " if(!hasNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void noSemanticIssue_combinationOfExpressionAndLiteralBoolean() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " return true && nullableItem != null;", + " }", + " public int runOk() {", + " if(!hasNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void semanticIssues_methodDeclarationReversed() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " public int runOk() {", + " if(!hasNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " return 0;", + " }", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " if(nullableItem != null) {", + " return false;", + " } else {", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", + " return true;", + " }", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void semanticIssues_ignoreLambdaReturns() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import java.util.function.BooleanSupplier;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " BooleanSupplier test = () -> {", + " return nullableItem == null;", + " };", + " return nullableItem != null;", + " }", + " public int runOk() {", + " if(!hasNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void semanticIssues_hardCodedReturnTrue() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", + " return true;", + " }", + " public void runOk() {", + " if(!hasNullableItem()) {", + " return;", + " }", + " nullableItem.call();", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void semanticIssues_warnsIfEnsuresNonNullDoesntReturnBoolean() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(value=\"nullableItem\", result=true)", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not return boolean", + " public void hasNullableItem() {", + " var x = nullableItem != null;", + " }", + " public void runOk() {", + " hasNullableItem();", + " // BUG: Diagnostic contains: dereferenced expression nullableItem is @Nullable", + " nullableItem.call();", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + // These tests are ignored because currently NullAway doesn't support data-flow of local variables + @Test + @Ignore // fails as both stores in the Return data flow mark the field as nullable + public void ensuresNonNullMethodWithMoreDataComplexFlow_2() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(\"nullableItem\", result=true)", + " public boolean hasNullableItem() {", + " var x = (nullableItem != null);", + " return x;", + " }", + " public int runOk() {", + " if(!hasNullableItem()) {", + " return 1;", + " }", + " nullableItem.call();", + " return 0;", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + @Ignore + public void ensuresNonNullMethodResultStoredInVariable() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(\"nullableItem\")", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " public void runOk() {", + " boolean check = hasNullableItem();", + " if(!check) {", + " return;", + " }", + " nullableItem.call();", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + @Ignore + public void ensuresNonNullMethodResultStoredInVariableInverse() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(\"nullableItem\")", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " public void runOk() {", + " boolean check = !hasNullableItem();", + " if(check) {", + " return;", + " }", + " nullableItem.call();", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } +}