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();
- }
-}