From 9f5d6ae75493a748d4603804288c5a6a4b56d797 Mon Sep 17 00:00:00 2001 From: Manu Sridharan Date: Wed, 2 Oct 2024 09:36:00 -0700 Subject: [PATCH] Revert "Support @EnsuresNonNullIf (#1044)" This reverts commit 8305c2ce8660eb51a00b6ac7e0b42f22eea98a1f. --- .../annotations/EnsuresNonNullIf.java | 54 -- .../com/uber/nullaway/NullabilityUtil.java | 36 +- .../dataflow/AccessPathNullnessAnalysis.java | 24 +- .../AccessPathNullnessPropagation.java | 3 +- .../uber/nullaway/dataflow/NullnessStore.java | 35 - .../nullaway/handlers/BaseNoOpHandler.java | 2 +- .../nullaway/handlers/CompositeHandler.java | 4 +- .../com/uber/nullaway/handlers/Handler.java | 4 +- .../com/uber/nullaway/handlers/Handlers.java | 2 - .../handlers/StreamNullabilityPropagator.java | 2 +- .../fieldcontract/EnsuresNonNullHandler.java | 43 +- .../EnsuresNonNullIfHandler.java | 323 ------- .../fieldcontract/FieldContractUtils.java | 95 -- .../uber/nullaway/EnsuresNonNullIfTests.java | 896 ------------------ 14 files changed, 76 insertions(+), 1447 deletions(-) delete mode 100644 annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java delete mode 100644 nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java delete mode 100644 nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/FieldContractUtils.java delete mode 100644 nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java diff --git a/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java deleted file mode 100644 index b42842ddbe..0000000000 --- a/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java +++ /dev/null @@ -1,54 +0,0 @@ -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/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java b/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java index 6e306851c5..6bae2114a0 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java +++ b/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java @@ -230,7 +230,14 @@ public static Stream getAllAnnotations(Symbol symbol */ public static @Nullable Set getAnnotationValueArray( Symbol.MethodSymbol methodSymbol, String annotName, boolean exactMatch) { - AnnotationMirror annot = findAnnotation(methodSymbol, annotName, 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; } @@ -248,33 +255,6 @@ 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/AccessPathNullnessAnalysis.java b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java index 6487e5d34a..8c2dae9151 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,7 +157,25 @@ public Set getNonnullFieldsOfReceiverAtExit(TreePath path, Context cont // be conservative and say nothing is initialized return Collections.emptySet(); } - return nullnessResult.getNonNullReceiverFields(); + 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; } /** @@ -172,7 +190,7 @@ public Set getNonnullFieldsOfReceiverBefore(TreePath path, Context cont if (store == null) { return Collections.emptySet(); } - return store.getNonNullReceiverFields(); + return getNonnullReceiverFields(store); } /** 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 88817b1a61..49dca06fac 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java @@ -852,8 +852,7 @@ public TransferResult visitSuper( @Override public TransferResult visitReturn( ReturnNode returnNode, TransferInput input) { - handler.onDataflowVisitReturn( - returnNode.getTree(), state, input.getThenStore(), input.getElseStore()); + handler.onDataflowVisitReturn(returnNode.getTree(), 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 43fd3d4714..8225d5c143 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java @@ -19,7 +19,6 @@ 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; @@ -31,7 +30,6 @@ 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; @@ -263,39 +261,6 @@ 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 d9f6ba13cf..3664529998 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, VisitorState state, NullnessStore thenStore, NullnessStore elseStore) { + ReturnTree tree, 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 f1a5997da2..df5293d690 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, VisitorState state, NullnessStore thenStore, NullnessStore elseStore) { + ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore) { for (Handler h : handlers) { - h.onDataflowVisitReturn(tree, state, thenStore, elseStore); + h.onDataflowVisitReturn(tree, 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 298d01d7db..f8a11afe85 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java @@ -269,14 +269,12 @@ 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, VisitorState state, NullnessStore thenStore, NullnessStore elseStore); + void onDataflowVisitReturn(ReturnTree tree, 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 8804f9149e..c8b81cbec0 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/Handlers.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/Handlers.java @@ -27,7 +27,6 @@ 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; @@ -70,7 +69,6 @@ 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 c411522da7..48e1ce6052 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, VisitorState state, NullnessStore thenStore, NullnessStore elseStore) { + ReturnTree tree, 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 ebce29f582..62cde6a7e1 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,6 +40,7 @@ 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; @@ -123,8 +124,46 @@ protected void validateOverridingRules( VisitorState state, MethodTree tree, Symbol.MethodSymbol overriddenMethod) { - FieldContractUtils.ensureStrictPostConditionInheritance( - annotName, overridingFieldNames, analysis, state, tree, 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)); } /** 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 deleted file mode 100644 index b4b116c545..0000000000 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java +++ /dev/null @@ -1,323 +0,0 @@ -/* - * 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 deleted file mode 100644 index ea25480aca..0000000000 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/FieldContractUtils.java +++ /dev/null @@ -1,95 +0,0 @@ -/* - * 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/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java deleted file mode 100644 index ea7655f720..0000000000 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java +++ /dev/null @@ -1,896 +0,0 @@ -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(); - } -}