From 60c09cd4fbb3b9ebd377b707e87ab401e3a92628 Mon Sep 17 00:00:00 2001 From: mauricio Date: Tue, 24 Sep 2024 22:38:03 +0200 Subject: [PATCH 01/52] First draft of @EnsuresNonNullIf --- .../annotations/EnsuresNonNullIf.java | 37 +++ .../com/uber/nullaway/handlers/Handlers.java | 2 + .../EnsuresNonNullIfHandler.java | 243 ++++++++++++++++++ .../uber/nullaway/EnsuresNonNullIfTests.java | 153 +++++++++++ 4 files changed, 435 insertions(+) create mode 100644 annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java create mode 100644 nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java create 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 new file mode 100644 index 0000000000..4c8b3ee68f --- /dev/null +++ b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java @@ -0,0 +1,37 @@ +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. NullAway verifies that this property holds, + * however, in a straightforward way. The method must have the "return field != null" construct. + * + *

Here is an example: + * + * 

+ * class Foo {
+ *     {@literal @}Nullable Object theField;
+ *     {@literal @}EnsuresNonNullIf("theField") // @EnsuresNonNullIf("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 { + String[] value(); +} diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/Handlers.java b/nullaway/src/main/java/com/uber/nullaway/handlers/Handlers.java index c8b81cbec0..8804f9149e 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/Handlers.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/Handlers.java @@ -27,6 +27,7 @@ import com.uber.nullaway.handlers.contract.ContractCheckHandler; import com.uber.nullaway.handlers.contract.ContractHandler; import com.uber.nullaway.handlers.contract.fieldcontract.EnsuresNonNullHandler; +import com.uber.nullaway.handlers.contract.fieldcontract.EnsuresNonNullIfHandler; import com.uber.nullaway.handlers.contract.fieldcontract.RequiresNonNullHandler; import com.uber.nullaway.handlers.temporary.FluentFutureHandler; @@ -69,6 +70,7 @@ public static Handler buildDefault(Config config) { handlerListBuilder.add(new GrpcHandler()); handlerListBuilder.add(new RequiresNonNullHandler()); handlerListBuilder.add(new EnsuresNonNullHandler()); + handlerListBuilder.add(new EnsuresNonNullIfHandler()); handlerListBuilder.add(new SynchronousCallbackHandler()); if (config.serializationIsActive() && config.getSerializationConfig().fieldInitInfoEnabled) { handlerListBuilder.add( diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java new file mode 100644 index 0000000000..c4b91be95a --- /dev/null +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java @@ -0,0 +1,243 @@ +/* + * Copyright (c) 2017-2020 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.BinaryTree; +import com.sun.source.tree.BlockTree; +import com.sun.source.tree.IdentifierTree; +import com.sun.source.tree.LiteralTree; +import com.sun.source.tree.MemberSelectTree; +import com.sun.source.tree.MethodTree; +import com.sun.source.tree.PrimitiveTypeTree; +import com.sun.source.tree.ReturnTree; +import com.sun.source.tree.Tree; +import com.sun.source.util.TreeScanner; +import com.sun.tools.javac.code.Symbol; +import com.uber.nullaway.ErrorMessage; +import com.uber.nullaway.NullAway; +import com.uber.nullaway.Nullness; +import com.uber.nullaway.dataflow.AccessPath; +import com.uber.nullaway.dataflow.AccessPathNullnessPropagation; +import com.uber.nullaway.handlers.AbstractFieldContractHandler; +import com.uber.nullaway.handlers.MethodAnalysisContext; +import com.uber.nullaway.handlers.contract.ContractUtils; +import java.util.Set; +import javax.lang.model.element.VariableElement; +import javax.lang.model.type.TypeKind; +import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode; + +/** + * This Handler parses {@code @EnsuresNonNullIf} annotation and when the annotated method is + * invoked, it annotates the fields as not null. The following tasks are performed when the + * {@code @EnsuresNonNullIf} annotation is observed: + * + * + */ +public class EnsuresNonNullIfHandler extends AbstractFieldContractHandler { + + 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) { + Symbol.MethodSymbol methodSymbol = methodAnalysisContext.methodSymbol(); + VisitorState state = methodAnalysisContext.state(); + NullAway analysis = methodAnalysisContext.analysis(); + + Set fieldNames = getAnnotationValueArray(methodSymbol, annotName, false); + if (fieldNames == null) { + return false; + } + + // Validate that the method returns boolean + if (validateBooleanReturnType(tree, state, analysis)) { + return false; + } + // TODO: check if the fields actually exist + + // Check whether the method follows the expected pattern + BlockTree body = tree.getBody(); + boolean result = body != null && body.accept(new ReturnExpressionVisitor(), fieldNames); + + if (!result) { + String message = + String.format( + "Method is annotated with @EnsuresNonNullIf but does not implement 'return %s != null'", + fieldNames); + state.reportMatch( + analysis + .getErrorBuilder() + .createErrorDescription( + new ErrorMessage(ErrorMessage.MessageTypes.POSTCONDITION_NOT_SATISFIED, message), + tree, + analysis.buildDescription(tree), + state, + null)); + } + + return true; + } + + private static boolean validateBooleanReturnType( + MethodTree tree, VisitorState state, NullAway analysis) { + Tree returnType = tree.getReturnType(); + if (!(returnType instanceof PrimitiveTypeTree) + || ((PrimitiveTypeTree) returnType).getPrimitiveTypeKind() != TypeKind.BOOLEAN) { + state.reportMatch( + analysis + .getErrorBuilder() + .createErrorDescription( + new ErrorMessage( + ErrorMessage.MessageTypes.PRECONDITION_NOT_SATISFIED, + "@EnsuresNonNullIf methods should return true"), + tree, + analysis.buildDescription(tree), + state, + null)); + return true; + } + return false; + } + + // TODO: support multiple fields instead of just one + private static final class ReturnExpressionVisitor extends TreeScanner> { + + @Override + public Boolean visitReturn(ReturnTree node, Set fieldNames) { + var expression = node.getExpression(); + + // Has to be a binary expression, e.g., a != b; + if (!(expression instanceof BinaryTree)) { + return false; + } + + var binaryTree = (BinaryTree) expression; + + // Left op could be an identifier (e.g., "fieldName") or a field access (this.fieldName) + // The identifier has to be on the list of fields + boolean isAnIdentifier = binaryTree.getLeftOperand() instanceof IdentifierTree; + boolean isAFieldAccess = binaryTree.getLeftOperand() instanceof MemberSelectTree; + if (isAnIdentifier) { + var leftOp = (IdentifierTree) binaryTree.getLeftOperand(); + String identifier = leftOp.getName().toString(); + if (!fieldNames.contains(identifier)) { + return false; + } + } else if (isAFieldAccess) { + var leftOp = (MemberSelectTree) binaryTree.getLeftOperand(); + String identifier = leftOp.getIdentifier().toString(); + if (!fieldNames.contains(identifier)) { + return false; + } + } else { + // If not any, then, it's incorrect! + return false; + } + + // right op has to be "null"! + var rightOp = (LiteralTree) binaryTree.getRightOperand(); + if (!rightOp.toString().equals("null")) { + return false; + } + + // comparison has to be != + if (binaryTree.getKind() != Tree.Kind.NOT_EQUAL_TO) { + return false; + } + + return true; + } + } + + /** TODO */ + @Override + protected void validateOverridingRules( + Set overridingFieldNames, + NullAway analysis, + VisitorState state, + MethodTree tree, + Symbol.MethodSymbol overriddenMethod) {} + + /** + * 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); + 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 then not null at this + // point + bothUpdates.set(accessPath, Nullness.NONNULL); + } + } + + return super.onDataflowVisitMethodInvocation( + node, methodSymbol, state, apContext, inputs, thenUpdates, elseUpdates, bothUpdates); + } +} diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java new file mode 100644 index 0000000000..81c90cd198 --- /dev/null +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -0,0 +1,153 @@ +package com.uber.nullaway; + +import org.junit.Test; + +public class EnsuresNonNullIfTests extends NullAwayTestsBase { + + @Test + public void ensuresNonNullMethodCalled() { + 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() {", + " if(!hasNullableItem()) {" + " return;" + " }", + " nullableItem.call();", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void ensuresNonNullMethodCalledUsingThis() { + 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 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 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 + 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(); + } + + @Test + public void ensuresNonNullMethodNotCalled() { + 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 runNOk() {", + " // BUG: Diagnostic contains: dereferenced expression nullableItem", + " nullableItem.call();", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } + + @Test + public void warnsIfEnsuresNonNullIfIsWrong() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(\"nullableItem\")", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not implement", + " public boolean hasNullableItem() {" + + " return true;" + + " }" + + " public void runOk() {", + " if(!hasNullableItem()) {" + " return;" + " }", + " nullableItem.call();", + " }", + "}") + .addSourceLines( + "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") + .doTest(); + } +} From c674bf9e50cf8d6520dc39fa00df301630dee607 Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 11:44:23 +0200 Subject: [PATCH 02/52] Improve validation of the semantics of the EnsuresNonNullIfHandler --- .../AbstractFieldContractHandler.java | 8 +- .../EnsuresNonNullIfHandler.java | 189 ++++++-------- .../uber/nullaway/EnsuresNonNullIfTests.java | 234 ++++++++++++++++-- 3 files changed, 301 insertions(+), 130 deletions(-) diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/AbstractFieldContractHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/AbstractFieldContractHandler.java index 3d590f7c61..40b93f6d7f 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/AbstractFieldContractHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/AbstractFieldContractHandler.java @@ -53,6 +53,11 @@ public abstract class AbstractFieldContractHandler extends BaseNoOpHandler { /** Simple name of the annotation in {@code String} */ protected final String annotName; + // Set to true in case we are visiting a method with the annotation under analysis + protected boolean visitingAnnotatedMethod; + // Points to the method symbol that's currently being visited + protected Symbol.MethodSymbol visitingMethodSymbol; + protected AbstractFieldContractHandler(String annotName) { this.annotName = annotName; } @@ -65,12 +70,13 @@ protected AbstractFieldContractHandler(String annotName) { */ @Override public void onMatchMethod(MethodTree tree, MethodAnalysisContext methodAnalysisContext) { - Symbol.MethodSymbol methodSymbol = methodAnalysisContext.methodSymbol(); VisitorState state = methodAnalysisContext.state(); Set annotationContent = NullabilityUtil.getAnnotationValueArray(methodSymbol, annotName, false); boolean isAnnotated = annotationContent != null; + this.visitingAnnotatedMethod = isAnnotated; + this.visitingMethodSymbol = methodSymbol; boolean isValid = isAnnotated && validateAnnotationSyntax( 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 index c4b91be95a..f0f658258a 100644 --- 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 @@ -27,43 +27,39 @@ import com.google.errorprone.VisitorState; import com.google.errorprone.util.ASTHelpers; -import com.sun.source.tree.BinaryTree; -import com.sun.source.tree.BlockTree; -import com.sun.source.tree.IdentifierTree; import com.sun.source.tree.LiteralTree; -import com.sun.source.tree.MemberSelectTree; import com.sun.source.tree.MethodTree; -import com.sun.source.tree.PrimitiveTypeTree; import com.sun.source.tree.ReturnTree; -import com.sun.source.tree.Tree; -import com.sun.source.util.TreeScanner; +import com.sun.source.util.TreePath; import com.sun.tools.javac.code.Symbol; import com.uber.nullaway.ErrorMessage; import com.uber.nullaway.NullAway; 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.Set; +import java.util.stream.Collectors; import javax.lang.model.element.VariableElement; -import javax.lang.model.type.TypeKind; import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode; /** * This Handler parses {@code @EnsuresNonNullIf} annotation and when the annotated method is - * invoked, it annotates the fields as not null. The following tasks are performed when the - * {@code @EnsuresNonNullIf} annotation is observed: - * - *
    - *
  • It validates the syntax of the annotation. - *
  • It validates whether all fields specified in the annotation are part in a return expression - * comparing its value to null - *
+ * invoked, it marks the annotated fields as not-null in the following flows. */ public class EnsuresNonNullIfHandler extends AbstractFieldContractHandler { + // Field is set to true when the EnsuresNonNullIf method ensures that all listed fields are + // checked for non-nullness + private boolean currentEnsuresNonNullIfMethodChecksNullnessOfAllFields; + // List of fields missing in the current EnsuresNonNullIf method so we can build proper error + // message + private Set missingFieldNames; + public EnsuresNonNullIfHandler() { super("EnsuresNonNullIf"); } @@ -75,30 +71,34 @@ public EnsuresNonNullIfHandler() { @Override protected boolean validateAnnotationSemantics( MethodTree tree, MethodAnalysisContext methodAnalysisContext) { - Symbol.MethodSymbol methodSymbol = methodAnalysisContext.methodSymbol(); - VisitorState state = methodAnalysisContext.state(); - NullAway analysis = methodAnalysisContext.analysis(); - - Set fieldNames = getAnnotationValueArray(methodSymbol, annotName, false); - if (fieldNames == null) { + // If no body in the method, return false right away + // TODO: Do we need proper error message here? + if (tree.getBody() == null) { return false; } - // Validate that the method returns boolean - if (validateBooleanReturnType(tree, state, analysis)) { - return false; - } - // TODO: check if the fields actually exist - - // Check whether the method follows the expected pattern - BlockTree body = tree.getBody(); - boolean result = body != null && body.accept(new ReturnExpressionVisitor(), fieldNames); + // clean up state variables, as we are visiting a new annotated method + currentEnsuresNonNullIfMethodChecksNullnessOfAllFields = false; + missingFieldNames = null; - if (!result) { - String message = - String.format( - "Method is annotated with @EnsuresNonNullIf but does not implement 'return %s != null'", - fieldNames); + // We force the nullness analysis of the method + NullAway analysis = methodAnalysisContext.analysis(); + VisitorState state = methodAnalysisContext.state(); + analysis + .getNullnessAnalysis(state) + .forceRunOnMethod(new TreePath(state.getPath(), tree), state.context); + + // If listed fields aren't checked for their nullness, return error + if (!currentEnsuresNonNullIfMethodChecksNullnessOfAllFields) { + String message; + if (missingFieldNames == null) { + message = "Method is annotated with @EnsuresNonNullIf but does not return boolean"; + } else { + message = + String.format( + "Method is annotated with @EnsuresNonNullIf but does not ensure fields %s", + missingFieldNames); + } state.reportMatch( analysis .getErrorBuilder() @@ -113,77 +113,6 @@ protected boolean validateAnnotationSemantics( return true; } - private static boolean validateBooleanReturnType( - MethodTree tree, VisitorState state, NullAway analysis) { - Tree returnType = tree.getReturnType(); - if (!(returnType instanceof PrimitiveTypeTree) - || ((PrimitiveTypeTree) returnType).getPrimitiveTypeKind() != TypeKind.BOOLEAN) { - state.reportMatch( - analysis - .getErrorBuilder() - .createErrorDescription( - new ErrorMessage( - ErrorMessage.MessageTypes.PRECONDITION_NOT_SATISFIED, - "@EnsuresNonNullIf methods should return true"), - tree, - analysis.buildDescription(tree), - state, - null)); - return true; - } - return false; - } - - // TODO: support multiple fields instead of just one - private static final class ReturnExpressionVisitor extends TreeScanner> { - - @Override - public Boolean visitReturn(ReturnTree node, Set fieldNames) { - var expression = node.getExpression(); - - // Has to be a binary expression, e.g., a != b; - if (!(expression instanceof BinaryTree)) { - return false; - } - - var binaryTree = (BinaryTree) expression; - - // Left op could be an identifier (e.g., "fieldName") or a field access (this.fieldName) - // The identifier has to be on the list of fields - boolean isAnIdentifier = binaryTree.getLeftOperand() instanceof IdentifierTree; - boolean isAFieldAccess = binaryTree.getLeftOperand() instanceof MemberSelectTree; - if (isAnIdentifier) { - var leftOp = (IdentifierTree) binaryTree.getLeftOperand(); - String identifier = leftOp.getName().toString(); - if (!fieldNames.contains(identifier)) { - return false; - } - } else if (isAFieldAccess) { - var leftOp = (MemberSelectTree) binaryTree.getLeftOperand(); - String identifier = leftOp.getIdentifier().toString(); - if (!fieldNames.contains(identifier)) { - return false; - } - } else { - // If not any, then, it's incorrect! - return false; - } - - // right op has to be "null"! - var rightOp = (LiteralTree) binaryTree.getRightOperand(); - if (!rightOp.toString().equals("null")) { - return false; - } - - // comparison has to be != - if (binaryTree.getKind() != Tree.Kind.NOT_EQUAL_TO) { - return false; - } - - return true; - } - } - /** TODO */ @Override protected void validateOverridingRules( @@ -193,6 +122,49 @@ protected void validateOverridingRules( MethodTree tree, Symbol.MethodSymbol overriddenMethod) {} + @Override + public void onDataflowVisitReturn( + ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore) { + if (visitingAnnotatedMethod) { + // We might have already found a flow that ensures the non-nullness, so we don't keep going + // deep. + if (currentEnsuresNonNullIfMethodChecksNullnessOfAllFields) { + return; + } + + Set fieldNames = getAnnotationValueArray(visitingMethodSymbol, annotName, false); + + // We extract all the data-flow of the fields found by the engine in the "then" case (i.e., + // true case) + // and check whether all fields in the annotation parameter are non-null + Set nonNullFieldsInPath = + thenStore.getAccessPathsWithValue(Nullness.NONNULL).stream() + .flatMap(ap -> ap.getElements().stream()) + .map(e -> e.getJavaElement().getSimpleName().toString()) + .collect(Collectors.toSet()); + boolean allFieldsInPathAreVerified = nonNullFieldsInPath.containsAll(fieldNames); + + if (allFieldsInPathAreVerified) { + // If it's a literal, then, it needs to return true + if (tree.getExpression() instanceof LiteralTree) { + LiteralTree expressionAsLiteral = (LiteralTree) tree.getExpression(); + if (expressionAsLiteral.getValue() instanceof Boolean) { + boolean literalValueOfExpression = (boolean) expressionAsLiteral.getValue(); + this.currentEnsuresNonNullIfMethodChecksNullnessOfAllFields = literalValueOfExpression; + } + } else { + // We then trust on the analysis of the engine that, at this point, the field is checked + // for null + this.currentEnsuresNonNullIfMethodChecksNullnessOfAllFields = true; + } + } else { + // Build list of missing fields for the elegant validation error message + fieldNames.removeAll(nonNullFieldsInPath); + this.missingFieldNames = new HashSet<>(fieldNames); + } + } + } + /** * 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 @@ -232,7 +204,8 @@ public NullnessHint onDataflowVisitMethodInvocation( } // The call to the EnsuresNonNullIf method ensures that the field is then not null at this - // point + // point. In here, we assume that the annotated method is already validated, and therefore, + // does ensure the non-null. bothUpdates.set(accessPath, Nullness.NONNULL); } } diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java index 81c90cd198..34ee9b29d5 100644 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -1,5 +1,6 @@ package com.uber.nullaway; +import org.junit.Ignore; import org.junit.Test; public class EnsuresNonNullIfTests extends NullAwayTestsBase { @@ -15,12 +16,174 @@ public void ensuresNonNullMethodCalled() { "class Foo {", " @Nullable Item nullableItem;", " @EnsuresNonNullIf(\"nullableItem\")", - " public boolean hasNullableItem() {" - + " return nullableItem != null;" - + " }" - + " public void runOk() {", - " if(!hasNullableItem()) {" + " return;" + " }", + " 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 ensuresNonNullMethodWithMoreDataComplexFlow() { + 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() {", + " 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 + @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\")", + " 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 + public void understandsBasicReturnFlowsInEnsuresNonNullMethods() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(\"nullableItem\")", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", + " public boolean hasNullableItem() {", + " if(nullableItem != null) {", + " return false;", + " } else {", + " 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 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(\"nullableItem\")", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " @EnsuresNonNullIf(\"nullableItem2\")", + " 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 missingSomeChecks() { + 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(\"nullableItem\")", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " @EnsuresNonNullIf(\"nullableItem2\")", + " 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( @@ -39,11 +202,12 @@ public void ensuresNonNullMethodCalledUsingThis() { "class Foo {", " @Nullable Item nullableItem;", " @EnsuresNonNullIf(\"nullableItem\")", - " public boolean hasNullableItem() {" - + " return this.nullableItem != null;" - + " }" - + " public void runOk() {", - " if(!hasNullableItem()) {" + " return;" + " }", + " public boolean hasNullableItem() {", + " return this.nullableItem != null;", + " }", + " public void runOk() {", + " if(!hasNullableItem()) {", + " return;" + " }", " nullableItem.call();", " }", "}") @@ -63,12 +227,14 @@ public void ensuresNonNullMethodResultStoredInVariable() { "class Foo {", " @Nullable Item nullableItem;", " @EnsuresNonNullIf(\"nullableItem\")", - " public boolean hasNullableItem() {" - + " return nullableItem != null;" - + " }" - + " public void runOk() {", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " public void runOk() {", " boolean check = hasNullableItem();", - " if(!check) {" + " return;" + " }", + " if(!check) {", + " return;", + " }", " nullableItem.call();", " }", "}") @@ -137,12 +303,38 @@ public void warnsIfEnsuresNonNullIfIsWrong() { "class Foo {", " @Nullable Item nullableItem;", " @EnsuresNonNullIf(\"nullableItem\")", - " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not implement", - " public boolean hasNullableItem() {" - + " return true;" - + " }" - + " public void runOk() {", - " if(!hasNullableItem()) {" + " return;" + " }", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", + " public boolean hasNullableItem() {", + " 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 warnsIfEnsuresNonNullDoesntReturnBoolean() { + defaultCompilationHelper + .addSourceLines( + "Foo.java", + "package com.uber;", + "import javax.annotation.Nullable;", + "import com.uber.nullaway.annotations.EnsuresNonNullIf;", + "class Foo {", + " @Nullable Item nullableItem;", + " @EnsuresNonNullIf(\"nullableItem\")", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not return boolean", + " public void hasNullableItem() {", + " var x = nullableItem != null;", + " }", + " public void runOk() {", + " hasNullableItem();", " nullableItem.call();", " }", "}") From c511a79d3d47391c82db8f43eb6bf9f91dcf2136 Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 12:57:37 +0200 Subject: [PATCH 03/52] More tests --- .../uber/nullaway/EnsuresNonNullIfTests.java | 31 ++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java index 34ee9b29d5..cefa856549 100644 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -93,7 +93,7 @@ public void ensuresNonNullMethodWithMoreDataComplexFlow_2() { } @Test - public void understandsBasicReturnFlowsInEnsuresNonNullMethods() { + public void understandsWrongReturnFlowsInEnsuresNonNullMethods() { defaultCompilationHelper .addSourceLines( "Foo.java", @@ -157,6 +157,35 @@ public void multipleEnsuresNonNullIfMethods() { .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({\"nullableItem\", \"nullableItem2\"})", + " 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 missingSomeChecks() { defaultCompilationHelper From 9eac416d98c93b69a44416d7c4125e16a0f0c373 Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 12:57:57 +0200 Subject: [PATCH 04/52] Improve docs --- .../java/com/uber/nullaway/annotations/EnsuresNonNullIf.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java index 4c8b3ee68f..1891a5b38a 100644 --- a/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java +++ b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java @@ -8,8 +8,7 @@ /** * 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. NullAway verifies that this property holds, - * however, in a straightforward way. The method must have the "return field != null" construct. + * returns true in case the fields are non-null. NullAway verifies that this property holds. * *

Here is an example: * From 38d6d886db1dec307e62f2b62851f8ef5d320a9e Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 13:46:30 +0200 Subject: [PATCH 05/52] Validate post-conditions in child classes --- .../fieldcontract/EnsuresNonNullHandler.java | 43 +----------- .../EnsuresNonNullIfHandler.java | 10 ++- .../fieldcontract/FieldContractUtils.java | 68 +++++++++++++++++++ .../uber/nullaway/EnsuresNonNullIfTests.java | 52 ++++++++++++++ 4 files changed, 130 insertions(+), 43 deletions(-) create mode 100644 nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/FieldContractUtils.java diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullHandler.java index 62cde6a7e1..b68c09c29c 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullHandler.java @@ -40,7 +40,6 @@ import com.uber.nullaway.handlers.MethodAnalysisContext; import com.uber.nullaway.handlers.contract.ContractUtils; import java.util.Collections; -import java.util.Iterator; import java.util.Set; import java.util.stream.Collectors; import javax.lang.model.element.VariableElement; @@ -124,46 +123,8 @@ protected void validateOverridingRules( VisitorState state, MethodTree tree, Symbol.MethodSymbol overriddenMethod) { - Set overriddenFieldNames = getAnnotationValueArray(overriddenMethod, annotName, false); - if (overriddenFieldNames == null) { - return; - } - if (overridingFieldNames == null) { - overridingFieldNames = Collections.emptySet(); - } - if (overridingFieldNames.containsAll(overriddenFieldNames)) { - return; - } - overriddenFieldNames.removeAll(overridingFieldNames); - - StringBuilder errorMessage = new StringBuilder(); - errorMessage - .append( - "postcondition inheritance is violated, this method must guarantee that all fields written in the @EnsuresNonNull annotation of overridden method ") - .append(castToNonNull(ASTHelpers.enclosingClass(overriddenMethod)).getSimpleName()) - .append(".") - .append(overriddenMethod.getSimpleName()) - .append(" are @NonNull at exit point as well. Fields ["); - Iterator iterator = overriddenFieldNames.iterator(); - while (iterator.hasNext()) { - errorMessage.append(iterator.next()); - if (iterator.hasNext()) { - errorMessage.append(", "); - } - } - errorMessage.append( - "] must explicitly appear as parameters at this method @EnsuresNonNull annotation"); - state.reportMatch( - analysis - .getErrorBuilder() - .createErrorDescription( - new ErrorMessage( - ErrorMessage.MessageTypes.WRONG_OVERRIDE_POSTCONDITION, - errorMessage.toString()), - tree, - analysis.buildDescription(tree), - state, - null)); + FieldContractUtils.validateOverridingRules( + annotName, overridingFieldNames, analysis, state, tree, overriddenMethod); } /** diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java index f0f658258a..a59078ac61 100644 --- 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 @@ -113,14 +113,20 @@ protected boolean validateAnnotationSemantics( return true; } - /** TODO */ + /* + * 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) {} + Symbol.MethodSymbol overriddenMethod) { + FieldContractUtils.validateOverridingRules( + annotName, overridingFieldNames, analysis, state, tree, overriddenMethod); + } @Override public void onDataflowVisitReturn( diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/FieldContractUtils.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/FieldContractUtils.java new file mode 100644 index 0000000000..d5244151aa --- /dev/null +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/FieldContractUtils.java @@ -0,0 +1,68 @@ +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.Iterator; +import java.util.Set; + +public class FieldContractUtils { + + public static void validateOverridingRules( + 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 ["); + 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/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java index cefa856549..687c45c057 100644 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -371,4 +371,56 @@ public void warnsIfEnsuresNonNullDoesntReturnBoolean() { "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") .doTest(); } + + @Test + public void supportEnsuresNonNullOverridingTest() { + 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(\"a\")", + " public boolean hasA() {", + " return a != null;", + " }", + " @EnsuresNonNullIf(\"b\")", + " 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(\"c\")", + " // 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 @EnsuresNonNull annotation", + " public boolean hasA() {", + " return c != null;", + " }", + " @EnsuresNonNullIf({\"b\", \"c\"})", + " 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(); + } } From c2a5dc2a53d85d471e0ac0407fea2d7f1fe4665f Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 13:48:21 +0200 Subject: [PATCH 06/52] A few more tests --- .../uber/nullaway/EnsuresNonNullIfTests.java | 67 +++++++++++++++++++ 1 file changed, 67 insertions(+) diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java index 687c45c057..85ee3c6e9d 100644 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -157,6 +157,73 @@ public void multipleEnsuresNonNullIfMethods() { .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(\"nullableItem\")", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " @EnsuresNonNullIf(\"nullableItem2\")", + " 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(\"nullableItem\")", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " @EnsuresNonNullIf(\"nullableItem2\")", + " public boolean hasNullableItem2() {", + " return nullableItem2 != null;", + " }", + " public int runOk() {", + " if(hasNullableItem() || hasNullableItem2()) {", + " 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 From 17b9173fffcb0ab620242ad55cb4e8754f956c50 Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 13:51:14 +0200 Subject: [PATCH 07/52] Tests cleanup --- .../uber/nullaway/EnsuresNonNullIfTests.java | 32 ++++++++++--------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java index 85ee3c6e9d..a15ce3ea9f 100644 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -6,7 +6,7 @@ public class EnsuresNonNullIfTests extends NullAwayTestsBase { @Test - public void ensuresNonNullMethodCalled() { + public void ensuresNonNullMethod() { defaultCompilationHelper .addSourceLines( "Foo.java", @@ -93,7 +93,7 @@ public void ensuresNonNullMethodWithMoreDataComplexFlow_2() { } @Test - public void understandsWrongReturnFlowsInEnsuresNonNullMethods() { + public void catchesWrongReturnFlows() { defaultCompilationHelper .addSourceLines( "Foo.java", @@ -254,7 +254,7 @@ public void multipleFieldsInSingleAnnotation() { } @Test - public void missingSomeChecks() { + public void missingChecksAreDetected() { defaultCompilationHelper .addSourceLines( "Foo.java", @@ -288,7 +288,7 @@ public void missingSomeChecks() { } @Test - public void ensuresNonNullMethodCalledUsingThis() { + public void ensuresNonNullMethodUsingThis() { defaultCompilationHelper .addSourceLines( "Foo.java", @@ -350,12 +350,14 @@ public void ensuresNonNullMethodResultStoredInVariableInverse() { "class Foo {", " @Nullable Item nullableItem;", " @EnsuresNonNullIf(\"nullableItem\")", - " public boolean hasNullableItem() {" - + " return nullableItem != null;" - + " }" - + " public void runOk() {", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " public void runOk() {", " boolean check = !hasNullableItem();", - " if(check) {" + " return;" + " }", + " if(check) {", + " return;", + " }", " nullableItem.call();", " }", "}") @@ -375,10 +377,10 @@ public void ensuresNonNullMethodNotCalled() { "class Foo {", " @Nullable Item nullableItem;", " @EnsuresNonNullIf(\"nullableItem\")", - " public boolean hasNullableItem() {" - + " return nullableItem != null;" - + " }" - + " public void runNOk() {", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", + " public void runNOk() {", " // BUG: Diagnostic contains: dereferenced expression nullableItem", " nullableItem.call();", " }", @@ -389,7 +391,7 @@ public void ensuresNonNullMethodNotCalled() { } @Test - public void warnsIfEnsuresNonNullIfIsWrong() { + public void warnsIfEnsuresNonNullCheckIfIsWronglyImplemented() { defaultCompilationHelper .addSourceLines( "Foo.java", @@ -440,7 +442,7 @@ public void warnsIfEnsuresNonNullDoesntReturnBoolean() { } @Test - public void supportEnsuresNonNullOverridingTest() { + public void checksForPostconditionsInInheritance() { defaultCompilationHelper .addSourceLines( "SuperClass.java", From e4ab9ba1e4e686070a42e50e5a3a18e615fdca52 Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 13:56:19 +0200 Subject: [PATCH 08/52] Fix error message in FieldContractUtils --- .../handlers/contract/fieldcontract/FieldContractUtils.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 index d5244151aa..021fe96c19 100644 --- 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 @@ -51,8 +51,10 @@ public static void validateOverridingRules( errorMessage.append(", "); } } - errorMessage.append( - "] must explicitly appear as parameters at this method @EnsuresNonNull annotation"); + errorMessage + .append("] must explicitly appear as parameters at this method @") + .append(annotName) + .append("annotation"); state.reportMatch( analysis .getErrorBuilder() From 9cbcf4e838446ca5d7f2c5a82ffcac26e66783be Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 13:57:00 +0200 Subject: [PATCH 09/52] Fix error message in FieldContractUtils again --- .../handlers/contract/fieldcontract/FieldContractUtils.java | 2 +- .../src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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 index 021fe96c19..f11162e335 100644 --- 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 @@ -54,7 +54,7 @@ public static void validateOverridingRules( errorMessage .append("] must explicitly appear as parameters at this method @") .append(annotName) - .append("annotation"); + .append(" annotation"); state.reportMatch( analysis .getErrorBuilder() diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java index a15ce3ea9f..6c46ac0192 100644 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -474,7 +474,7 @@ public void checksForPostconditionsInInheritance() { "class ChildLevelOne extends SuperClass {", " @Nullable Item c;", " @EnsuresNonNullIf(\"c\")", - " // 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 @EnsuresNonNull annotation", + " // 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;", " }", From d044fae804029ee5b3f399d10bfd659adcf4bdaa Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 16:53:59 +0200 Subject: [PATCH 10/52] Add trueIfNonNull to invert the result of the EnsuresNonNullIf method --- .../annotations/EnsuresNonNullIf.java | 6 +- .../com/uber/nullaway/NullabilityUtil.java | 25 ++++-- .../EnsuresNonNullIfHandler.java | 43 +++++++-- .../uber/nullaway/EnsuresNonNullIfTests.java | 90 +++++++++++++++++++ 4 files changed, 149 insertions(+), 15 deletions(-) diff --git a/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java index 1891a5b38a..9a3946665a 100644 --- a/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java +++ b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java @@ -8,7 +8,9 @@ /** * 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. NullAway verifies that this property holds. + * returns true in case the fields are non-null. The method can also return true in case the fields + * are null (inverse logic), and in such case, you must set trueIfNonNull to false. NullAway + * verifies that the property holds. * *

Here is an example: * @@ -33,4 +35,6 @@ @Target({ElementType.METHOD}) public @interface EnsuresNonNullIf { String[] value(); + + boolean trueIfNonNull() 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 6bae2114a0..8467c91a07 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java +++ b/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java @@ -230,14 +230,7 @@ public static Stream getAllAnnotations(Symbol symbol */ public static @Nullable Set getAnnotationValueArray( Symbol.MethodSymbol methodSymbol, String annotName, boolean exactMatch) { - AnnotationMirror annot = null; - for (AnnotationMirror annotationMirror : methodSymbol.getAnnotationMirrors()) { - String name = AnnotationUtils.annotationName(annotationMirror); - if ((exactMatch && name.equals(annotName)) || (!exactMatch && name.endsWith(annotName))) { - annot = annotationMirror; - break; - } - } + AnnotationMirror annot = findAnnotation(methodSymbol, annotName, exactMatch); if (annot == null) { return null; } @@ -255,6 +248,22 @@ public static Stream getAllAnnotations(Symbol symbol return null; } + 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/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java index a59078ac61..3cf989587b 100644 --- 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 @@ -34,6 +34,7 @@ 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; @@ -42,8 +43,12 @@ 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; @@ -139,19 +144,23 @@ public void onDataflowVisitReturn( } Set fieldNames = getAnnotationValueArray(visitingMethodSymbol, annotName, false); + boolean trueIfNonNull = getTrueIfNonNullValue(visitingMethodSymbol); // We extract all the data-flow of the fields found by the engine in the "then" case (i.e., // true case) // and check whether all fields in the annotation parameter are non-null Set nonNullFieldsInPath = - thenStore.getAccessPathsWithValue(Nullness.NONNULL).stream() + thenStore + .getAccessPathsWithValue(trueIfNonNull ? Nullness.NONNULL : Nullness.NULL) + .stream() .flatMap(ap -> ap.getElements().stream()) .map(e -> e.getJavaElement().getSimpleName().toString()) .collect(Collectors.toSet()); boolean allFieldsInPathAreVerified = nonNullFieldsInPath.containsAll(fieldNames); if (allFieldsInPathAreVerified) { - // If it's a literal, then, it needs to return true + // If it's a literal, then, it needs to return true/false, depending on the trueIfNonNull + // flag if (tree.getExpression() instanceof LiteralTree) { LiteralTree expressionAsLiteral = (LiteralTree) tree.getExpression(); if (expressionAsLiteral.getValue() instanceof Boolean) { @@ -171,6 +180,26 @@ public void onDataflowVisitReturn( } } + private boolean getTrueIfNonNullValue(Symbol.MethodSymbol methodSymbol) { + AnnotationMirror annot = NullabilityUtil.findAnnotation(methodSymbol, annotName, false); + if (annot == null) { + return true; + } + + Map elementValues = + annot.getElementValues(); + for (Map.Entry entry : + elementValues.entrySet()) { + ExecutableElement elem = entry.getKey(); + if (elem.getSimpleName().contentEquals("trueIfNonNull")) { + return (boolean) entry.getValue().getValue(); + } + } + + // Not explicitly declared in the annotation, so we default to 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 @@ -193,6 +222,7 @@ public NullnessHint onDataflowVisitMethodInvocation( Set fieldNames = getAnnotationValueArray(methodSymbol, annotName, false); if (fieldNames != null) { + boolean trueIfNonNull = getTrueIfNonNullValue(methodSymbol); fieldNames = ContractUtils.trimReceivers(fieldNames); for (String fieldName : fieldNames) { VariableElement field = @@ -209,10 +239,11 @@ public NullnessHint onDataflowVisitMethodInvocation( continue; } - // The call to the EnsuresNonNullIf method ensures that the field is then not null at this - // point. In here, we assume that the annotated method is already validated, and therefore, - // does ensure the non-null. - bothUpdates.set(accessPath, Nullness.NONNULL); + // The call to the EnsuresNonNullIf method ensures that the field is then not null + // (or null, depending on the trueIfNotNUll flag) at this point. + // In here, we assume that the annotated method is already validated. + thenUpdates.set(accessPath, trueIfNonNull ? Nullness.NONNULL : Nullness.NULL); + elseUpdates.set(accessPath, trueIfNonNull ? Nullness.NULL : Nullness.NONNULL); } } diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java index 6c46ac0192..5077e486c8 100644 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -211,6 +211,7 @@ public void multipleEnsuresNonNullIfMethods_3() { " }", " 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();", @@ -313,6 +314,7 @@ public void ensuresNonNullMethodUsingThis() { } @Test + @Ignore public void ensuresNonNullMethodResultStoredInVariable() { defaultCompilationHelper .addSourceLines( @@ -340,6 +342,7 @@ public void ensuresNonNullMethodResultStoredInVariable() { } @Test + @Ignore public void ensuresNonNullMethodResultStoredInVariableInverse() { defaultCompilationHelper .addSourceLines( @@ -433,6 +436,7 @@ public void warnsIfEnsuresNonNullDoesntReturnBoolean() { " }", " public void runOk() {", " hasNullableItem();", + " // BUG: Diagnostic contains: dereferenced expression nullableItem is @Nullable", " nullableItem.call();", " }", "}") @@ -492,4 +496,90 @@ public void checksForPostconditionsInInheritance() { "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") .doTest(); } + + @Test + public void setTrueIfNonNullToFalse() { + 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\", trueIfNonNull=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 setTrueIfNonNullToFalseMultipleElements() { + 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\"}, trueIfNonNull=false)", + " public boolean doesNotHaveNullableItem() {", + " 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 setTrueIfNonNullToFalseMultipleElements_deferenceFound() { + 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\"}, trueIfNonNull=false)", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem, nullableItem2]", + " public boolean doesNotHaveNullableItem() {", + " 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(); + } } From d700ee38603598c894fab00d8b3d4f7eb9df8130 Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 16:56:50 +0200 Subject: [PATCH 11/52] Throw exception instead of returning default value in exceptional case --- .../contract/fieldcontract/EnsuresNonNullIfHandler.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 index 3cf989587b..52ef489bbc 100644 --- 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 @@ -183,7 +183,7 @@ public void onDataflowVisitReturn( private boolean getTrueIfNonNullValue(Symbol.MethodSymbol methodSymbol) { AnnotationMirror annot = NullabilityUtil.findAnnotation(methodSymbol, annotName, false); if (annot == null) { - return true; + throw new RuntimeException("Annotation should not be null at this point"); } Map elementValues = From 6842120e31e2ede519a26b13167800f244d05ff0 Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 16:58:47 +0200 Subject: [PATCH 12/52] Rename variable --- .../fieldcontract/EnsuresNonNullIfHandler.java | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) 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 index 52ef489bbc..35f5350dc1 100644 --- 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 @@ -58,9 +58,8 @@ */ public class EnsuresNonNullIfHandler extends AbstractFieldContractHandler { - // Field is set to true when the EnsuresNonNullIf method ensures that all listed fields are - // checked for non-nullness - private boolean currentEnsuresNonNullIfMethodChecksNullnessOfAllFields; + // Set to true when the current visited EnsuresNonNullIf method has correct semantics + private boolean semanticsHold; // List of fields missing in the current EnsuresNonNullIf method so we can build proper error // message private Set missingFieldNames; @@ -83,7 +82,7 @@ protected boolean validateAnnotationSemantics( } // clean up state variables, as we are visiting a new annotated method - currentEnsuresNonNullIfMethodChecksNullnessOfAllFields = false; + semanticsHold = false; missingFieldNames = null; // We force the nullness analysis of the method @@ -94,7 +93,7 @@ protected boolean validateAnnotationSemantics( .forceRunOnMethod(new TreePath(state.getPath(), tree), state.context); // If listed fields aren't checked for their nullness, return error - if (!currentEnsuresNonNullIfMethodChecksNullnessOfAllFields) { + if (!semanticsHold) { String message; if (missingFieldNames == null) { message = "Method is annotated with @EnsuresNonNullIf but does not return boolean"; @@ -139,7 +138,7 @@ public void onDataflowVisitReturn( if (visitingAnnotatedMethod) { // We might have already found a flow that ensures the non-nullness, so we don't keep going // deep. - if (currentEnsuresNonNullIfMethodChecksNullnessOfAllFields) { + if (semanticsHold) { return; } @@ -165,12 +164,12 @@ public void onDataflowVisitReturn( LiteralTree expressionAsLiteral = (LiteralTree) tree.getExpression(); if (expressionAsLiteral.getValue() instanceof Boolean) { boolean literalValueOfExpression = (boolean) expressionAsLiteral.getValue(); - this.currentEnsuresNonNullIfMethodChecksNullnessOfAllFields = literalValueOfExpression; + this.semanticsHold = literalValueOfExpression; } } else { // We then trust on the analysis of the engine that, at this point, the field is checked // for null - this.currentEnsuresNonNullIfMethodChecksNullnessOfAllFields = true; + this.semanticsHold = true; } } else { // Build list of missing fields for the elegant validation error message From df1293fbedb84af107b2ff112a96fb5e79fc10bf Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 17:10:14 +0200 Subject: [PATCH 13/52] Fix nullability issues in my code --- .../fieldcontract/EnsuresNonNullIfHandler.java | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) 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 index 35f5350dc1..bcb40838f0 100644 --- 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 @@ -46,6 +46,7 @@ import java.util.Map; import java.util.Set; import java.util.stream.Collectors; +import javax.annotation.Nullable; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.AnnotationValue; import javax.lang.model.element.ExecutableElement; @@ -62,7 +63,7 @@ public class EnsuresNonNullIfHandler extends AbstractFieldContractHandler { private boolean semanticsHold; // List of fields missing in the current EnsuresNonNullIf method so we can build proper error // message - private Set missingFieldNames; + @Nullable private Set missingFieldNames; public EnsuresNonNullIfHandler() { super("EnsuresNonNullIf"); @@ -136,13 +137,17 @@ protected void validateOverridingRules( public void onDataflowVisitReturn( ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore) { if (visitingAnnotatedMethod) { - // We might have already found a flow that ensures the non-nullness, so we don't keep going - // deep. + // We might have already found another return tree that results in what we need, + // so we don't keep going deep. if (semanticsHold) { return; } Set fieldNames = getAnnotationValueArray(visitingMethodSymbol, annotName, false); + if (fieldNames == null) { + throw new RuntimeException("List of field names shouldn't be null"); + } + boolean trueIfNonNull = getTrueIfNonNullValue(visitingMethodSymbol); // We extract all the data-flow of the fields found by the engine in the "then" case (i.e., From 1bf794c3c9840dcf5fe14b2a406ac10b27b40a19 Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 20:25:28 +0200 Subject: [PATCH 14/52] One more test --- .../uber/nullaway/EnsuresNonNullIfTests.java | 28 +++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java index 5077e486c8..c9246b238d 100644 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -32,6 +32,34 @@ public void ensuresNonNullMethod() { .doTest(); } + @Test + public void ensuresNonNullMethod_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\")", + " 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 ensuresNonNullMethodWithMoreDataComplexFlow() { defaultCompilationHelper From c4710828be2be4f365f0304802f795e7d7e0c267 Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Wed, 25 Sep 2024 20:26:29 +0200 Subject: [PATCH 15/52] Move ignored tests to the bottom --- .../uber/nullaway/EnsuresNonNullIfTests.java | 172 +++++++++--------- 1 file changed, 87 insertions(+), 85 deletions(-) diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java index c9246b238d..79219039cc 100644 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -91,35 +91,6 @@ public void ensuresNonNullMethodWithMoreDataComplexFlow() { .doTest(); } - @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\")", - " 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 public void catchesWrongReturnFlows() { defaultCompilationHelper @@ -341,62 +312,6 @@ public void ensuresNonNullMethodUsingThis() { .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(); - } - @Test public void ensuresNonNullMethodNotCalled() { defaultCompilationHelper @@ -610,4 +525,91 @@ public void setTrueIfNonNullToFalseMultipleElements_deferenceFound() { "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\")", + " 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(); + } } From 6ebac1126242a2799999bfae86e37192838a649b Mon Sep 17 00:00:00 2001 From: Manu Sridharan Date: Thu, 26 Sep 2024 14:34:23 -0700 Subject: [PATCH 16/52] add TODO --- .../com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java | 1 + 1 file changed, 1 insertion(+) diff --git a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java index 8c2dae9151..f15a5cdf86 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java @@ -160,6 +160,7 @@ public Set getNonnullFieldsOfReceiverAtExit(TreePath path, Context cont return getNonnullReceiverFields(nullnessResult); } + // TODO re-use this code private Set getNonnullReceiverFields(NullnessStore nullnessResult) { Set nonnullAccessPaths = nullnessResult.getAccessPathsWithValue(Nullness.NONNULL); Set result = new LinkedHashSet<>(); From 3b27daeddf86da03babfc5597e0fb6e85bdb39d2 Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Fri, 27 Sep 2024 13:55:45 +0200 Subject: [PATCH 17/52] Make use of internal state to get the enclosing method of a return tree --- .../main/java/com/uber/nullaway/NullAway.java | 3 +- .../AbstractFieldContractHandler.java | 7 - .../nullaway/handlers/BaseNoOpHandler.java | 4 +- .../nullaway/handlers/CompositeHandler.java | 6 +- .../com/uber/nullaway/handlers/Handler.java | 5 +- .../handlers/StreamNullabilityPropagator.java | 5 +- .../EnsuresNonNullIfHandler.java | 302 +++++++++++++----- .../fieldcontract/RequiresNonNullHandler.java | 7 +- 8 files changed, 236 insertions(+), 103 deletions(-) diff --git a/nullaway/src/main/java/com/uber/nullaway/NullAway.java b/nullaway/src/main/java/com/uber/nullaway/NullAway.java index 546dae75c2..4d2ea03e5a 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullAway.java +++ b/nullaway/src/main/java/com/uber/nullaway/NullAway.java @@ -384,7 +384,8 @@ public Description matchMethodInvocation(MethodInvocationTree tree, VisitorState return Description.NO_MATCH; } Symbol.MethodSymbol methodSymbol = getSymbolForMethodInvocation(tree); - handler.onMatchMethodInvocation(tree, new MethodAnalysisContext(this, state, methodSymbol)); + handler.onMatchMethodInvocation( + tree, methodSymbol, new MethodAnalysisContext(this, state, methodSymbol)); // assuming this list does not include the receiver List actualParams = tree.getArguments(); return handleInvocation(tree, state, methodSymbol, actualParams); diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/AbstractFieldContractHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/AbstractFieldContractHandler.java index 40b93f6d7f..fe571c5319 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/AbstractFieldContractHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/AbstractFieldContractHandler.java @@ -53,11 +53,6 @@ public abstract class AbstractFieldContractHandler extends BaseNoOpHandler { /** Simple name of the annotation in {@code String} */ protected final String annotName; - // Set to true in case we are visiting a method with the annotation under analysis - protected boolean visitingAnnotatedMethod; - // Points to the method symbol that's currently being visited - protected Symbol.MethodSymbol visitingMethodSymbol; - protected AbstractFieldContractHandler(String annotName) { this.annotName = annotName; } @@ -75,8 +70,6 @@ public void onMatchMethod(MethodTree tree, MethodAnalysisContext methodAnalysisC Set annotationContent = NullabilityUtil.getAnnotationValueArray(methodSymbol, annotName, false); boolean isAnnotated = annotationContent != null; - this.visitingAnnotatedMethod = isAnnotated; - this.visitingMethodSymbol = methodSymbol; boolean isValid = isAnnotated && validateAnnotationSyntax( diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java index 3664529998..e6a59beaae 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java @@ -79,7 +79,9 @@ public void onMatchMethod(MethodTree tree, MethodAnalysisContext methodAnalysisC @Override public void onMatchMethodInvocation( - MethodInvocationTree tree, MethodAnalysisContext methodAnalysisContext) { + MethodInvocationTree tree, + Symbol.MethodSymbol methodSymbol, + MethodAnalysisContext methodAnalysisContext) { // NoOp } diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java index df5293d690..6df118bcc7 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java @@ -104,9 +104,11 @@ public void onMatchMethodReference( @Override public void onMatchMethodInvocation( - MethodInvocationTree tree, MethodAnalysisContext methodAnalysisContext) { + MethodInvocationTree tree, + Symbol.MethodSymbol methodSymbol, + MethodAnalysisContext methodAnalysisContext) { for (Handler h : handlers) { - h.onMatchMethodInvocation(tree, methodAnalysisContext); + h.onMatchMethodInvocation(tree, methodSymbol, methodAnalysisContext); } } diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java index f8a11afe85..735b4e1b08 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java @@ -87,10 +87,13 @@ void onMatchTopLevelClass( * Called when NullAway first matches a particular method call-site. * * @param tree The AST node for the method invocation (call-site) being matched. + * @param methodSymbol The method symbol of the enclosing method * @param methodAnalysisContext The MethodAnalysisContext object */ void onMatchMethodInvocation( - MethodInvocationTree tree, MethodAnalysisContext methodAnalysisContext); + MethodInvocationTree tree, + Symbol.MethodSymbol methodSymbol, + MethodAnalysisContext methodAnalysisContext); /** * Called when NullAway first matches a particular lambda expression. diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java b/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java index 48e1ce6052..aff44c3a60 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java @@ -208,9 +208,10 @@ public void onMatchTopLevelClass( @Override public void onMatchMethodInvocation( - MethodInvocationTree tree, MethodAnalysisContext methodAnalysisContext) { + MethodInvocationTree tree, + Symbol.MethodSymbol methodSymbol, + MethodAnalysisContext methodAnalysisContext) { - Symbol.MethodSymbol methodSymbol = methodAnalysisContext.methodSymbol(); VisitorState state = methodAnalysisContext.state(); Type receiverType = ASTHelpers.getReceiverType(tree); for (StreamTypeRecord streamType : models) { 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 index bcb40838f0..9606702546 100644 --- 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 @@ -27,7 +27,9 @@ import com.google.errorprone.VisitorState; import com.google.errorprone.util.ASTHelpers; +import com.sun.source.tree.ClassTree; import com.sun.source.tree.LiteralTree; +import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.MethodTree; import com.sun.source.tree.ReturnTree; import com.sun.source.util.TreePath; @@ -37,21 +39,23 @@ import com.uber.nullaway.NullabilityUtil; import com.uber.nullaway.Nullness; import com.uber.nullaway.dataflow.AccessPath; +import com.uber.nullaway.dataflow.AccessPathNullnessAnalysis; 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.Collections; +import java.util.HashMap; import java.util.Map; import java.util.Set; import java.util.stream.Collectors; -import javax.annotation.Nullable; 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.jetbrains.annotations.NotNull; /** * This Handler parses {@code @EnsuresNonNullIf} annotation and when the annotated method is @@ -59,16 +63,27 @@ */ public class EnsuresNonNullIfHandler extends AbstractFieldContractHandler { - // Set to true when the current visited EnsuresNonNullIf method has correct semantics - private boolean semanticsHold; - // List of fields missing in the current EnsuresNonNullIf method so we can build proper error - // message - @Nullable private Set missingFieldNames; + private final Map returnToEnclosingMethodMap = new HashMap<>(); + private final Map methodToMethodSymbol = new HashMap<>(); + private final Map methodSymbolToMethod = new HashMap<>(); + private final Map> semantics = new HashMap<>(); public EnsuresNonNullIfHandler() { super("EnsuresNonNullIf"); } + /* + * Clean all the maps whenever a new top-level class is declared + */ + @Override + public void onMatchTopLevelClass( + NullAway analysis, ClassTree tree, VisitorState state, Symbol.ClassSymbol classSymbol) { + returnToEnclosingMethodMap.clear(); + methodToMethodSymbol.clear(); + methodSymbolToMethod.clear(); + semantics.clear(); + } + /** * Validates whether all parameters mentioned in the @EnsuresNonNullIf annotation are guaranteed * to be {@code @NonNull} at exit point of this method. @@ -76,45 +91,6 @@ public EnsuresNonNullIfHandler() { @Override protected boolean validateAnnotationSemantics( MethodTree tree, MethodAnalysisContext methodAnalysisContext) { - // If no body in the method, return false right away - // TODO: Do we need proper error message here? - if (tree.getBody() == null) { - return false; - } - - // clean up state variables, as we are visiting a new annotated method - semanticsHold = false; - missingFieldNames = null; - - // We force the nullness analysis of the method - NullAway analysis = methodAnalysisContext.analysis(); - VisitorState state = methodAnalysisContext.state(); - analysis - .getNullnessAnalysis(state) - .forceRunOnMethod(new TreePath(state.getPath(), tree), state.context); - - // If listed fields aren't checked for their nullness, return error - if (!semanticsHold) { - String message; - if (missingFieldNames == null) { - message = "Method is annotated with @EnsuresNonNullIf but does not return boolean"; - } else { - message = - String.format( - "Method is annotated with @EnsuresNonNullIf but does not ensure fields %s", - missingFieldNames); - } - state.reportMatch( - analysis - .getErrorBuilder() - .createErrorDescription( - new ErrorMessage(ErrorMessage.MessageTypes.POSTCONDITION_NOT_SATISFIED, message), - tree, - analysis.buildDescription(tree), - state, - null)); - } - return true; } @@ -133,54 +109,126 @@ protected void validateOverridingRules( annotName, overridingFieldNames, analysis, state, tree, overriddenMethod); } + /* + * Creates a map between the MethodTree and its related MethodSymbol + */ + @Override + public void onMatchMethod(MethodTree tree, MethodAnalysisContext methodAnalysisContext) { + Symbol.MethodSymbol methodSymbol = methodAnalysisContext.methodSymbol(); + + Set annotationContent = + NullabilityUtil.getAnnotationValueArray(methodSymbol, annotName, false); + boolean isAnnotated = annotationContent != null; + + if (isAnnotated) { + methodToMethodSymbol.put(tree, methodSymbol); + methodSymbolToMethod.put(methodSymbol, tree); + } + + super.onMatchMethod(tree, methodAnalysisContext); + } + + /* + * We create a map between the return tree and its enclosing method, so we can + * later identify whether the return statement belongs to the EnsuresNonNullIf annotated method. + */ + @Override + public void onMatchReturn(NullAway analysis, ReturnTree tree, VisitorState state) { + TreePath enclosingMethod = + NullabilityUtil.findEnclosingMethodOrLambdaOrInitializer(state.getPath()); + if (enclosingMethod == null) { + throw new RuntimeException("no enclosing method, lambda or initializer!"); + } + + // If it's not an annotated method, we don't care about analyzing it + if (!methodToMethodSymbol.containsKey(enclosingMethod.getLeaf())) { + return; + } + + // For now, we only support returns within methods directly, no lambdas. + if (!(enclosingMethod.getLeaf() instanceof MethodTree)) { + throw new RuntimeException( + "return statement outside of a method! (e.g. in a lambda or in an initializer block)"); + } + + // We match the return tree with its enclosing method + returnToEnclosingMethodMap.put(tree, (MethodTree) enclosingMethod.getLeaf()); + + // We now force the data-flow engine to run for the entire method, + // which will allow us to analyze all of its return statements via the dataFlowReturn callback + // We will call the data-flow engine for the same method multiple times, one of each return + // statement, but the caching theoretically kicks in. + MethodTree methodTree = (MethodTree) enclosingMethod.getLeaf(); + AccessPathNullnessAnalysis nullnessAnalysis = analysis.getNullnessAnalysis(state); + nullnessAnalysis.forceRunOnMethod(new TreePath(state.getPath(), methodTree), state.context); + } + @Override public void onDataflowVisitReturn( ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore) { - if (visitingAnnotatedMethod) { - // We might have already found another return tree that results in what we need, - // so we don't keep going deep. - if (semanticsHold) { - return; - } + MethodTree enclosingMethod = returnToEnclosingMethodMap.get(tree); - Set fieldNames = getAnnotationValueArray(visitingMethodSymbol, annotName, false); - if (fieldNames == null) { - throw new RuntimeException("List of field names shouldn't be null"); - } + // We might not have seen this return tree yet, so we stop + // This will be called again later, once we call the engine for it + if (enclosingMethod == null) { + return; + } + + // If it's not an EnsuresNonNullIf annotated method, we don't need to continue + boolean visitingAnnotatedMethod = methodToMethodSymbol.containsKey(enclosingMethod); + if (!visitingAnnotatedMethod) { + return; + } - boolean trueIfNonNull = getTrueIfNonNullValue(visitingMethodSymbol); - - // We extract all the data-flow of the fields found by the engine in the "then" case (i.e., - // true case) - // and check whether all fields in the annotation parameter are non-null - Set nonNullFieldsInPath = - thenStore - .getAccessPathsWithValue(trueIfNonNull ? Nullness.NONNULL : Nullness.NULL) - .stream() - .flatMap(ap -> ap.getElements().stream()) - .map(e -> e.getJavaElement().getSimpleName().toString()) - .collect(Collectors.toSet()); - boolean allFieldsInPathAreVerified = nonNullFieldsInPath.containsAll(fieldNames); - - if (allFieldsInPathAreVerified) { - // If it's a literal, then, it needs to return true/false, depending on the trueIfNonNull - // flag - if (tree.getExpression() instanceof LiteralTree) { - LiteralTree expressionAsLiteral = (LiteralTree) tree.getExpression(); - if (expressionAsLiteral.getValue() instanceof Boolean) { - boolean literalValueOfExpression = (boolean) expressionAsLiteral.getValue(); - this.semanticsHold = literalValueOfExpression; + // If we already found a path that keeps the correct semantics of the method, + // we don't need to keep searching for it + boolean hasCorrectSemantics = isHasCorrectSemantics(enclosingMethod); + if (hasCorrectSemantics) { + return; + } + + Symbol.MethodSymbol visitingMethodSymbol = methodToMethodSymbol.get(enclosingMethod); + Set fieldNames = getAnnotationValueArray(visitingMethodSymbol, annotName, false); + if (fieldNames == null) { + throw new RuntimeException("List of field names shouldn't be null"); + } + + boolean trueIfNonNull = getTrueIfNonNullValue(visitingMethodSymbol); + + // We extract all the data-flow of the fields found by the engine in the "then" case + // (i.e., true case) and check whether all fields in the annotation parameter are non-null + Set nonNullFieldsInPath = + thenStore.getAccessPathsWithValue(trueIfNonNull ? Nullness.NONNULL : Nullness.NULL).stream() + .flatMap(ap -> ap.getElements().stream()) + .map(e -> e.getJavaElement().getSimpleName().toString()) + .collect(Collectors.toSet()); + boolean allFieldsInPathAreVerified = nonNullFieldsInPath.containsAll(fieldNames); + + if (allFieldsInPathAreVerified) { + // If it's a literal, then, it needs to return true/false, + // depending on the trueIfNonNull flag + if (tree.getExpression() instanceof LiteralTree) { + LiteralTree expressionAsLiteral = (LiteralTree) tree.getExpression(); + if (expressionAsLiteral.getValue() instanceof Boolean) { + boolean literalValueOfExpression = (boolean) expressionAsLiteral.getValue(); + + // If the method returns true, it means the method + // ensures the proposed semantics + if (literalValueOfExpression) { + markCorrectSemantics(enclosingMethod); + } else { + markIncorrectSemantics(enclosingMethod, fieldNames); } - } else { - // We then trust on the analysis of the engine that, at this point, the field is checked - // for null - this.semanticsHold = true; } } else { - // Build list of missing fields for the elegant validation error message - fieldNames.removeAll(nonNullFieldsInPath); - this.missingFieldNames = new HashSet<>(fieldNames); + // We then trust on the analysis of the engine that, at this point, + // the field is checked for null + markCorrectSemantics(enclosingMethod); } + } else { + // Build list of missing fields for the elegant validation error message + fieldNames.removeAll(nonNullFieldsInPath); + markIncorrectSemantics(enclosingMethod, fieldNames); } } @@ -204,6 +252,45 @@ private boolean getTrueIfNonNullValue(Symbol.MethodSymbol methodSymbol) { return true; } + @Override + public void onMatchMethodInvocation( + MethodInvocationTree tree, + Symbol.MethodSymbol methodSymbol, + MethodAnalysisContext methodAnalysisContext) { + Set fieldNames = getAnnotationValueArray(methodSymbol, annotName, false); + boolean callToAnEnsureNonNullIfMethod = fieldNames != null; + + if (!callToAnEnsureNonNullIfMethod) { + return; + } + + if (!semanticsHold(methodSymbol)) { + VisitorState state = methodAnalysisContext.state(); + NullAway analysis = methodAnalysisContext.analysis(); + + Set missingFields = getMissingFields(methodSymbol); + + String message; + if (missingFields.isEmpty()) { + message = "Method is annotated with @EnsuresNonNullIf but does not return boolean"; + } else { + message = + String.format( + "Method is annotated with @EnsuresNonNullIf but does not ensure fields %s", + missingFields); + } + state.reportMatch( + analysis + .getErrorBuilder() + .createErrorDescription( + new ErrorMessage(ErrorMessage.MessageTypes.POSTCONDITION_NOT_SATISFIED, message), + getMethodTree(methodSymbol), + analysis.buildDescription(getMethodTree(methodSymbol)), + state, + null)); + } + } + /** * 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 @@ -225,7 +312,9 @@ public NullnessHint onDataflowVisitMethodInvocation( } Set fieldNames = getAnnotationValueArray(methodSymbol, annotName, false); - if (fieldNames != null) { + boolean callToAnEnsureNonNullIfMethod = fieldNames != null; + + if (callToAnEnsureNonNullIfMethod) { boolean trueIfNonNull = getTrueIfNonNullValue(methodSymbol); fieldNames = ContractUtils.trimReceivers(fieldNames); for (String fieldName : fieldNames) { @@ -254,4 +343,45 @@ public NullnessHint onDataflowVisitMethodInvocation( return super.onDataflowVisitMethodInvocation( node, methodSymbol, state, apContext, inputs, thenUpdates, elseUpdates, bothUpdates); } + + private void markIncorrectSemantics(MethodTree enclosingMethod, Set missingFields) { + semantics.put(enclosingMethod, missingFields); + } + + private void markCorrectSemantics(MethodTree enclosingMethod) { + semantics.put(enclosingMethod, Collections.emptySet()); + } + + private boolean isHasCorrectSemantics(MethodTree enclosingMethod) { + return semantics.containsKey(enclosingMethod) && semantics.get(enclosingMethod).isEmpty(); + } + + private boolean semanticsHold(Symbol.MethodSymbol methodSymbol) { + MethodTree methodTree = getMethodTree(methodSymbol); + + Set missingFields = semantics.get(methodTree); + if (missingFields == null) { + return false; + } + + return missingFields.isEmpty(); + } + + private @NotNull MethodTree getMethodTree(Symbol.MethodSymbol methodSymbol) { + MethodTree methodTree = methodSymbolToMethod.get(methodSymbol); + if (methodTree == null) { + throw new RuntimeException("Method tree not found!"); + } + return methodTree; + } + + private Set getMissingFields(Symbol.MethodSymbol methodSymbol) { + MethodTree methodTree = getMethodTree(methodSymbol); + Set missingFields = semantics.get(methodTree); + if (missingFields == null) { + return Collections.emptySet(); + } + + return missingFields; + } } diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/RequiresNonNullHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/RequiresNonNullHandler.java index 44a6e71782..b6981cc2db 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/RequiresNonNullHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/RequiresNonNullHandler.java @@ -130,14 +130,15 @@ protected void validateOverridingRules( */ @Override public void onMatchMethodInvocation( - MethodInvocationTree tree, MethodAnalysisContext methodAnalysisContext) { + MethodInvocationTree tree, + Symbol.MethodSymbol methodSymbol, + MethodAnalysisContext methodAnalysisContext) { VisitorState state = methodAnalysisContext.state(); - Symbol.MethodSymbol methodSymbol = methodAnalysisContext.methodSymbol(); NullAway analysis = methodAnalysisContext.analysis(); Set fieldNames = getAnnotationValueArray(methodSymbol, annotName, false); if (fieldNames == null) { - super.onMatchMethodInvocation(tree, methodAnalysisContext); + super.onMatchMethodInvocation(tree, methodSymbol, methodAnalysisContext); return; } fieldNames = ContractUtils.trimReceivers(fieldNames); From 4aa9ed0035aed83ee25a95cf893117bd5452458d Mon Sep 17 00:00:00 2001 From: mauricioaniche Date: Fri, 27 Sep 2024 14:32:47 +0200 Subject: [PATCH 18/52] Improvements here and there --- .../EnsuresNonNullIfHandler.java | 154 +++++++++++------- .../uber/nullaway/EnsuresNonNullIfTests.java | 3 +- 2 files changed, 95 insertions(+), 62 deletions(-) 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 index 9606702546..f7e6800430 100644 --- 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 @@ -55,7 +55,6 @@ import javax.lang.model.element.ExecutableElement; import javax.lang.model.element.VariableElement; import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode; -import org.jetbrains.annotations.NotNull; /** * This Handler parses {@code @EnsuresNonNullIf} annotation and when the annotated method is @@ -63,10 +62,16 @@ */ public class EnsuresNonNullIfHandler extends AbstractFieldContractHandler { + // Fast-access data structure to retrieve the enclosing MethodTree of a given ReturnTree private final Map returnToEnclosingMethodMap = new HashMap<>(); + + // Fast-access data structure to retrieve the method symbol of a method, and vice-versa private final Map methodToMethodSymbol = new HashMap<>(); private final Map methodSymbolToMethod = new HashMap<>(); - private final Map> semantics = new HashMap<>(); + + // Contains a map of all EnsuresNonNullIf methods and their list of semantic issues. + // An empty list means that the method has no semantic issues + private final Map> semanticValidationMap = new HashMap<>(); public EnsuresNonNullIfHandler() { super("EnsuresNonNullIf"); @@ -81,12 +86,13 @@ public void onMatchTopLevelClass( returnToEnclosingMethodMap.clear(); methodToMethodSymbol.clear(); methodSymbolToMethod.clear(); - semantics.clear(); + semanticValidationMap.clear(); } /** - * Validates whether all parameters mentioned in the @EnsuresNonNullIf annotation are guaranteed - * to be {@code @NonNull} at exit point of this method. + * The validateAnnotationSemantics() doesn't work for this case, as we need to visit all the + * ReturnTree objects before deciding whether or not the semantics match. Validation errors are + * reported the first time the EnsureNonNullIf method is called. */ @Override protected boolean validateAnnotationSemantics( @@ -140,7 +146,7 @@ public void onMatchReturn(NullAway analysis, ReturnTree tree, VisitorState state throw new RuntimeException("no enclosing method, lambda or initializer!"); } - // If it's not an annotated method, we don't care about analyzing it + // If it's not an annotated method, we don't care about analyzing this ReturnTree if (!methodToMethodSymbol.containsKey(enclosingMethod.getLeaf())) { return; } @@ -182,8 +188,7 @@ public void onDataflowVisitReturn( // If we already found a path that keeps the correct semantics of the method, // we don't need to keep searching for it - boolean hasCorrectSemantics = isHasCorrectSemantics(enclosingMethod); - if (hasCorrectSemantics) { + if (semanticsHold(enclosingMethod)) { return; } @@ -212,8 +217,8 @@ public void onDataflowVisitReturn( if (expressionAsLiteral.getValue() instanceof Boolean) { boolean literalValueOfExpression = (boolean) expressionAsLiteral.getValue(); - // If the method returns true, it means the method - // ensures the proposed semantics + // If the method returns literal 'true', + // it means the proposed semantics are ensured if (literalValueOfExpression) { markCorrectSemantics(enclosingMethod); } else { @@ -221,7 +226,8 @@ public void onDataflowVisitReturn( } } } else { - // We then trust on the analysis of the engine that, at this point, + // No literal boolean return that we can easily parse, + // so we then trust on the analysis of the engine that, at this point, // the field is checked for null markCorrectSemantics(enclosingMethod); } @@ -232,26 +238,10 @@ public void onDataflowVisitReturn( } } - private boolean getTrueIfNonNullValue(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("trueIfNonNull")) { - return (boolean) entry.getValue().getValue(); - } - } - - // Not explicitly declared in the annotation, so we default to true - return true; - } - + /* + * We use this matcher to double check if the semantic of the + * EnsureNonNullIf method is correct. + */ @Override public void onMatchMethodInvocation( MethodInvocationTree tree, @@ -265,29 +255,7 @@ public void onMatchMethodInvocation( } if (!semanticsHold(methodSymbol)) { - VisitorState state = methodAnalysisContext.state(); - NullAway analysis = methodAnalysisContext.analysis(); - - Set missingFields = getMissingFields(methodSymbol); - - String message; - if (missingFields.isEmpty()) { - message = "Method is annotated with @EnsuresNonNullIf but does not return boolean"; - } else { - message = - String.format( - "Method is annotated with @EnsuresNonNullIf but does not ensure fields %s", - missingFields); - } - state.reportMatch( - analysis - .getErrorBuilder() - .createErrorDescription( - new ErrorMessage(ErrorMessage.MessageTypes.POSTCONDITION_NOT_SATISFIED, message), - getMethodTree(methodSymbol), - analysis.buildDescription(getMethodTree(methodSymbol)), - state, - null)); + notifySemanticError(methodSymbol, methodAnalysisContext); } } @@ -344,22 +312,34 @@ public NullnessHint onDataflowVisitMethodInvocation( node, methodSymbol, state, apContext, inputs, thenUpdates, elseUpdates, bothUpdates); } + // Add the list of missing fields to a given method, + // indicating that this method doesn't hold the required semantics private void markIncorrectSemantics(MethodTree enclosingMethod, Set missingFields) { - semantics.put(enclosingMethod, missingFields); + semanticValidationMap.put(enclosingMethod, missingFields); } + // Add a method to the list of semantic validations, without any issues private void markCorrectSemantics(MethodTree enclosingMethod) { - semantics.put(enclosingMethod, Collections.emptySet()); + semanticValidationMap.put(enclosingMethod, Collections.emptySet()); } - private boolean isHasCorrectSemantics(MethodTree enclosingMethod) { - return semantics.containsKey(enclosingMethod) && semantics.get(enclosingMethod).isEmpty(); + // Returns whether the given method has valid semantic + // Returns false if the method doesn't have the right semantic, or is not on the map at all + private boolean semanticsHold(MethodTree enclosingMethod) { + Symbol.MethodSymbol methodSymbol = methodToMethodSymbol.get(enclosingMethod); + if (methodSymbol == null) { + return false; + } + return semanticsHold(methodSymbol); } + // Returns whether the given MethodSymbol has valid semantic + // Returns false if the method doesn't have the right semantic, or is not on the map at all private boolean semanticsHold(Symbol.MethodSymbol methodSymbol) { MethodTree methodTree = getMethodTree(methodSymbol); - Set missingFields = semantics.get(methodTree); + Set missingFields = semanticValidationMap.get(methodTree); + // It might be null in case the EnsuresNonNullIf method is completely wrong if (missingFields == null) { return false; } @@ -367,7 +347,8 @@ private boolean semanticsHold(Symbol.MethodSymbol methodSymbol) { return missingFields.isEmpty(); } - private @NotNull MethodTree getMethodTree(Symbol.MethodSymbol methodSymbol) { + // Gets the method tree of a given MethodSymbol + private MethodTree getMethodTree(Symbol.MethodSymbol methodSymbol) { MethodTree methodTree = methodSymbolToMethod.get(methodSymbol); if (methodTree == null) { throw new RuntimeException("Method tree not found!"); @@ -375,13 +356,64 @@ private boolean semanticsHold(Symbol.MethodSymbol methodSymbol) { return methodTree; } + // Gets the list of missing fields of a given method private Set getMissingFields(Symbol.MethodSymbol methodSymbol) { MethodTree methodTree = getMethodTree(methodSymbol); - Set missingFields = semantics.get(methodTree); + Set missingFields = semanticValidationMap.get(methodTree); if (missingFields == null) { return Collections.emptySet(); } return missingFields; } + + private boolean getTrueIfNonNullValue(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("trueIfNonNull")) { + return (boolean) entry.getValue().getValue(); + } + } + + // Not explicitly declared in the annotation, so we default to true + return true; + } + + // Notify about a semantic error in the given EnsuresNonNullIf method + private void notifySemanticError( + Symbol.MethodSymbol methodSymbol, MethodAnalysisContext methodAnalysisContext) { + VisitorState state = methodAnalysisContext.state(); + NullAway analysis = methodAnalysisContext.analysis(); + + MethodTree ensureNonNullIfMethod = getMethodTree(methodSymbol); + Set missingFields = getMissingFields(methodSymbol); + + String message; + if (missingFields.isEmpty()) { + message = "Method is annotated with @EnsuresNonNullIf but does not return boolean"; + } else { + message = + String.format( + "Method is annotated with @EnsuresNonNullIf but does not ensure fields %s", + missingFields); + } + + state.reportMatch( + analysis + .getErrorBuilder() + .createErrorDescription( + new ErrorMessage(ErrorMessage.MessageTypes.POSTCONDITION_NOT_SATISFIED, message), + ensureNonNullIfMethod, + analysis.buildDescription(ensureNonNullIfMethod), + state, + null)); + } } diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java index 79219039cc..d7faef990e 100644 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -353,7 +353,8 @@ public void warnsIfEnsuresNonNullCheckIfIsWronglyImplemented() { " }", " public void runOk() {", " if(!hasNullableItem()) {", - " return;" + " }", + " return;", + " }", " nullableItem.call();", " }", "}") From c0a70acca8de01865b14725fe203a57dbf3a238e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= Date: Sat, 28 Sep 2024 16:53:02 +0200 Subject: [PATCH 19/52] New approach --- .../main/java/com/uber/nullaway/NullAway.java | 3 +- .../nullaway/handlers/BaseNoOpHandler.java | 4 +- .../nullaway/handlers/CompositeHandler.java | 6 +- .../com/uber/nullaway/handlers/Handler.java | 5 +- .../handlers/StreamNullabilityPropagator.java | 5 +- .../EnsuresNonNullIfHandler.java | 372 ++++++------------ .../fieldcontract/RequiresNonNullHandler.java | 7 +- .../uber/nullaway/EnsuresNonNullIfTests.java | 249 ++++++++---- 8 files changed, 309 insertions(+), 342 deletions(-) diff --git a/nullaway/src/main/java/com/uber/nullaway/NullAway.java b/nullaway/src/main/java/com/uber/nullaway/NullAway.java index 4d2ea03e5a..546dae75c2 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullAway.java +++ b/nullaway/src/main/java/com/uber/nullaway/NullAway.java @@ -384,8 +384,7 @@ public Description matchMethodInvocation(MethodInvocationTree tree, VisitorState return Description.NO_MATCH; } Symbol.MethodSymbol methodSymbol = getSymbolForMethodInvocation(tree); - handler.onMatchMethodInvocation( - tree, methodSymbol, new MethodAnalysisContext(this, state, methodSymbol)); + handler.onMatchMethodInvocation(tree, new MethodAnalysisContext(this, state, methodSymbol)); // assuming this list does not include the receiver List actualParams = tree.getArguments(); return handleInvocation(tree, state, methodSymbol, actualParams); 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 e6a59beaae..3664529998 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java @@ -79,9 +79,7 @@ public void onMatchMethod(MethodTree tree, MethodAnalysisContext methodAnalysisC @Override public void onMatchMethodInvocation( - MethodInvocationTree tree, - Symbol.MethodSymbol methodSymbol, - MethodAnalysisContext methodAnalysisContext) { + MethodInvocationTree tree, MethodAnalysisContext methodAnalysisContext) { // 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 6df118bcc7..df5293d690 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java @@ -104,11 +104,9 @@ public void onMatchMethodReference( @Override public void onMatchMethodInvocation( - MethodInvocationTree tree, - Symbol.MethodSymbol methodSymbol, - MethodAnalysisContext methodAnalysisContext) { + MethodInvocationTree tree, MethodAnalysisContext methodAnalysisContext) { for (Handler h : handlers) { - h.onMatchMethodInvocation(tree, methodSymbol, methodAnalysisContext); + h.onMatchMethodInvocation(tree, methodAnalysisContext); } } 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 735b4e1b08..f8a11afe85 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java @@ -87,13 +87,10 @@ void onMatchTopLevelClass( * Called when NullAway first matches a particular method call-site. * * @param tree The AST node for the method invocation (call-site) being matched. - * @param methodSymbol The method symbol of the enclosing method * @param methodAnalysisContext The MethodAnalysisContext object */ void onMatchMethodInvocation( - MethodInvocationTree tree, - Symbol.MethodSymbol methodSymbol, - MethodAnalysisContext methodAnalysisContext); + MethodInvocationTree tree, MethodAnalysisContext methodAnalysisContext); /** * Called when NullAway first matches a particular lambda expression. 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 aff44c3a60..48e1ce6052 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java @@ -208,10 +208,9 @@ public void onMatchTopLevelClass( @Override public void onMatchMethodInvocation( - MethodInvocationTree tree, - Symbol.MethodSymbol methodSymbol, - MethodAnalysisContext methodAnalysisContext) { + MethodInvocationTree tree, MethodAnalysisContext methodAnalysisContext) { + Symbol.MethodSymbol methodSymbol = methodAnalysisContext.methodSymbol(); VisitorState state = methodAnalysisContext.state(); Type receiverType = ASTHelpers.getReceiverType(tree); for (StreamTypeRecord streamType : models) { 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 index f7e6800430..1fcf8e3288 100644 --- 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 @@ -27,29 +27,27 @@ import com.google.errorprone.VisitorState; import com.google.errorprone.util.ASTHelpers; -import com.sun.source.tree.ClassTree; import com.sun.source.tree.LiteralTree; -import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.MethodTree; import com.sun.source.tree.ReturnTree; 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.AccessPathNullnessAnalysis; 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.Collections; -import java.util.HashMap; +import java.util.HashSet; import java.util.Map; import java.util.Set; import java.util.stream.Collectors; +import javax.annotation.Nullable; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.AnnotationValue; import javax.lang.model.element.ExecutableElement; @@ -62,44 +60,109 @@ */ public class EnsuresNonNullIfHandler extends AbstractFieldContractHandler { - // Fast-access data structure to retrieve the enclosing MethodTree of a given ReturnTree - private final Map returnToEnclosingMethodMap = new HashMap<>(); + // Set to true when the current visited EnsuresNonNullIf method has correct semantics + private boolean semanticsHold; - // Fast-access data structure to retrieve the method symbol of a method, and vice-versa - private final Map methodToMethodSymbol = new HashMap<>(); - private final Map methodSymbolToMethod = new HashMap<>(); + private final Set returnTreesInMethodUnderAnalysis = new HashSet<>(); - // Contains a map of all EnsuresNonNullIf methods and their list of semantic issues. - // An empty list means that the method has no semantic issues - private final Map> semanticValidationMap = new HashMap<>(); + // List of fields missing in the current EnsuresNonNullIf method + // so we can build proper error message + @Nullable private Set missingFieldNames; + // The MethodTree and Symbol of the EnsureNonNullIf method under semantic validation + @Nullable private MethodTree methodTreeUnderAnalysis; + @Nullable private Symbol.MethodSymbol methodSymbolUnderAnalysis; public EnsuresNonNullIfHandler() { super("EnsuresNonNullIf"); } - /* - * Clean all the maps whenever a new top-level class is declared - */ - @Override - public void onMatchTopLevelClass( - NullAway analysis, ClassTree tree, VisitorState state, Symbol.ClassSymbol classSymbol) { - returnToEnclosingMethodMap.clear(); - methodToMethodSymbol.clear(); - methodSymbolToMethod.clear(); - semanticValidationMap.clear(); - } - /** - * The validateAnnotationSemantics() doesn't work for this case, as we need to visit all the - * ReturnTree objects before deciding whether or not the semantics match. Validation errors are - * reported the first time the EnsureNonNullIf method is called. + * 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 false; + } + + // clean up state variables, as we are visiting a new annotated method + semanticsHold = false; + missingFieldNames = null; + methodTreeUnderAnalysis = tree; + methodSymbolUnderAnalysis = methodAnalysisContext.methodSymbol(); + 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); + + // We force the nullness analysis of the method under validation + analysis + .getNullnessAnalysis(state) + .forceRunOnMethod(new TreePath(state.getPath(), tree), state.context); + + // If listed fields aren't checked for their nullness, return error + if (!semanticsHold) { + String message; + if (missingFieldNames == null) { + message = "Method is annotated with @EnsuresNonNullIf but does not return boolean"; + } else { + message = + String.format( + "Method is annotated with @EnsuresNonNullIf but does not ensure fields %s", + missingFieldNames); + } + state.reportMatch( + analysis + .getErrorBuilder() + .createErrorDescription( + new ErrorMessage(ErrorMessage.MessageTypes.POSTCONDITION_NOT_SATISFIED, message), + tree, + analysis.buildDescription(tree), + state, + null)); + } + + // Clean up state + semanticsHold = false; + missingFieldNames = null; + methodTreeUnderAnalysis = null; + methodSymbolUnderAnalysis = null; + returnTreesInMethodUnderAnalysis.clear(); + return true; } + private void buildUpReturnToEnclosingMethodMap(VisitorState methodState) { + returnTreesInMethodUnderAnalysis.clear(); + new TreePathScanner() { + @Override + public Void visitReturn(ReturnTree node, Void unused) { + VisitorState returnState = methodState.withPath(getCurrentPath()); + + TreePath enclosingMethod = + NullabilityUtil.findEnclosingMethodOrLambdaOrInitializer(returnState.getPath()); + 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)) { + return super.visitReturn(node, null); + } + + // We add the current return tree to the set as it's in the method + 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. @@ -115,93 +178,31 @@ protected void validateOverridingRules( annotName, overridingFieldNames, analysis, state, tree, overriddenMethod); } - /* - * Creates a map between the MethodTree and its related MethodSymbol - */ - @Override - public void onMatchMethod(MethodTree tree, MethodAnalysisContext methodAnalysisContext) { - Symbol.MethodSymbol methodSymbol = methodAnalysisContext.methodSymbol(); - - Set annotationContent = - NullabilityUtil.getAnnotationValueArray(methodSymbol, annotName, false); - boolean isAnnotated = annotationContent != null; - - if (isAnnotated) { - methodToMethodSymbol.put(tree, methodSymbol); - methodSymbolToMethod.put(methodSymbol, tree); - } - - super.onMatchMethod(tree, methodAnalysisContext); - } - - /* - * We create a map between the return tree and its enclosing method, so we can - * later identify whether the return statement belongs to the EnsuresNonNullIf annotated method. - */ - @Override - public void onMatchReturn(NullAway analysis, ReturnTree tree, VisitorState state) { - TreePath enclosingMethod = - NullabilityUtil.findEnclosingMethodOrLambdaOrInitializer(state.getPath()); - if (enclosingMethod == null) { - throw new RuntimeException("no enclosing method, lambda or initializer!"); - } - - // If it's not an annotated method, we don't care about analyzing this ReturnTree - if (!methodToMethodSymbol.containsKey(enclosingMethod.getLeaf())) { - return; - } - - // For now, we only support returns within methods directly, no lambdas. - if (!(enclosingMethod.getLeaf() instanceof MethodTree)) { - throw new RuntimeException( - "return statement outside of a method! (e.g. in a lambda or in an initializer block)"); - } - - // We match the return tree with its enclosing method - returnToEnclosingMethodMap.put(tree, (MethodTree) enclosingMethod.getLeaf()); - - // We now force the data-flow engine to run for the entire method, - // which will allow us to analyze all of its return statements via the dataFlowReturn callback - // We will call the data-flow engine for the same method multiple times, one of each return - // statement, but the caching theoretically kicks in. - MethodTree methodTree = (MethodTree) enclosingMethod.getLeaf(); - AccessPathNullnessAnalysis nullnessAnalysis = analysis.getNullnessAnalysis(state); - nullnessAnalysis.forceRunOnMethod(new TreePath(state.getPath(), methodTree), state.context); - } - @Override public void onDataflowVisitReturn( - ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore) { - MethodTree enclosingMethod = returnToEnclosingMethodMap.get(tree); - - // We might not have seen this return tree yet, so we stop - // This will be called again later, once we call the engine for it - if (enclosingMethod == null) { - return; - } - - // If it's not an EnsuresNonNullIf annotated method, we don't need to continue - boolean visitingAnnotatedMethod = methodToMethodSymbol.containsKey(enclosingMethod); - if (!visitingAnnotatedMethod) { + ReturnTree returnTree, NullnessStore thenStore, NullnessStore elseStore) { + // We only explore return statements that is inside + // the method under validation + if (!returnTreesInMethodUnderAnalysis.contains(returnTree)) { return; } - // If we already found a path that keeps the correct semantics of the method, - // we don't need to keep searching for it - if (semanticsHold(enclosingMethod)) { + // We might have already found another return tree that results in what we need, + // so we don't keep going deep. + if (semanticsHold) { return; } - Symbol.MethodSymbol visitingMethodSymbol = methodToMethodSymbol.get(enclosingMethod); - Set fieldNames = getAnnotationValueArray(visitingMethodSymbol, annotName, false); + Set fieldNames = getAnnotationValueArray(methodSymbolUnderAnalysis, annotName, false); if (fieldNames == null) { throw new RuntimeException("List of field names shouldn't be null"); } - boolean trueIfNonNull = getTrueIfNonNullValue(visitingMethodSymbol); + boolean trueIfNonNull = getTrueIfNonNullValue(methodSymbolUnderAnalysis); - // We extract all the data-flow of the fields found by the engine in the "then" case - // (i.e., true case) and check whether all fields in the annotation parameter are non-null + // We extract all the data-flow of the fields found by the engine in the "then" case (i.e., + // true case) + // and check whether all fields in the annotation parameter are non-null Set nonNullFieldsInPath = thenStore.getAccessPathsWithValue(trueIfNonNull ? Nullness.NONNULL : Nullness.NULL).stream() .flatMap(ap -> ap.getElements().stream()) @@ -210,53 +211,43 @@ public void onDataflowVisitReturn( boolean allFieldsInPathAreVerified = nonNullFieldsInPath.containsAll(fieldNames); if (allFieldsInPathAreVerified) { - // If it's a literal, then, it needs to return true/false, - // depending on the trueIfNonNull flag - if (tree.getExpression() instanceof LiteralTree) { - LiteralTree expressionAsLiteral = (LiteralTree) tree.getExpression(); + // If it's a literal, then, it needs to return true/false, depending on the trueIfNonNull + // flag + if (returnTree.getExpression() instanceof LiteralTree) { + LiteralTree expressionAsLiteral = (LiteralTree) returnTree.getExpression(); if (expressionAsLiteral.getValue() instanceof Boolean) { - boolean literalValueOfExpression = (boolean) expressionAsLiteral.getValue(); - - // If the method returns literal 'true', - // it means the proposed semantics are ensured - if (literalValueOfExpression) { - markCorrectSemantics(enclosingMethod); - } else { - markIncorrectSemantics(enclosingMethod, fieldNames); - } + this.semanticsHold = (boolean) expressionAsLiteral.getValue(); } } else { - // No literal boolean return that we can easily parse, - // so we then trust on the analysis of the engine that, at this point, - // the field is checked for null - markCorrectSemantics(enclosingMethod); + // We then trust on the analysis of the engine that, at this point, the field is checked + // for null + this.semanticsHold = true; } } else { // Build list of missing fields for the elegant validation error message fieldNames.removeAll(nonNullFieldsInPath); - markIncorrectSemantics(enclosingMethod, fieldNames); + this.missingFieldNames = new HashSet<>(fieldNames); } } - /* - * We use this matcher to double check if the semantic of the - * EnsureNonNullIf method is correct. - */ - @Override - public void onMatchMethodInvocation( - MethodInvocationTree tree, - Symbol.MethodSymbol methodSymbol, - MethodAnalysisContext methodAnalysisContext) { - Set fieldNames = getAnnotationValueArray(methodSymbol, annotName, false); - boolean callToAnEnsureNonNullIfMethod = fieldNames != null; - - if (!callToAnEnsureNonNullIfMethod) { - return; + private boolean getTrueIfNonNullValue(Symbol.MethodSymbol methodSymbol) { + AnnotationMirror annot = NullabilityUtil.findAnnotation(methodSymbol, annotName, false); + if (annot == null) { + throw new RuntimeException("Annotation should not be null at this point"); } - if (!semanticsHold(methodSymbol)) { - notifySemanticError(methodSymbol, methodAnalysisContext); + Map elementValues = + annot.getElementValues(); + for (Map.Entry entry : + elementValues.entrySet()) { + ExecutableElement elem = entry.getKey(); + if (elem.getSimpleName().contentEquals("trueIfNonNull")) { + return (boolean) entry.getValue().getValue(); + } } + + // Not explicitly declared in the annotation, so we default to true + return true; } /** @@ -280,9 +271,7 @@ public NullnessHint onDataflowVisitMethodInvocation( } Set fieldNames = getAnnotationValueArray(methodSymbol, annotName, false); - boolean callToAnEnsureNonNullIfMethod = fieldNames != null; - - if (callToAnEnsureNonNullIfMethod) { + if (fieldNames != null) { boolean trueIfNonNull = getTrueIfNonNullValue(methodSymbol); fieldNames = ContractUtils.trimReceivers(fieldNames); for (String fieldName : fieldNames) { @@ -311,109 +300,4 @@ public NullnessHint onDataflowVisitMethodInvocation( return super.onDataflowVisitMethodInvocation( node, methodSymbol, state, apContext, inputs, thenUpdates, elseUpdates, bothUpdates); } - - // Add the list of missing fields to a given method, - // indicating that this method doesn't hold the required semantics - private void markIncorrectSemantics(MethodTree enclosingMethod, Set missingFields) { - semanticValidationMap.put(enclosingMethod, missingFields); - } - - // Add a method to the list of semantic validations, without any issues - private void markCorrectSemantics(MethodTree enclosingMethod) { - semanticValidationMap.put(enclosingMethod, Collections.emptySet()); - } - - // Returns whether the given method has valid semantic - // Returns false if the method doesn't have the right semantic, or is not on the map at all - private boolean semanticsHold(MethodTree enclosingMethod) { - Symbol.MethodSymbol methodSymbol = methodToMethodSymbol.get(enclosingMethod); - if (methodSymbol == null) { - return false; - } - return semanticsHold(methodSymbol); - } - - // Returns whether the given MethodSymbol has valid semantic - // Returns false if the method doesn't have the right semantic, or is not on the map at all - private boolean semanticsHold(Symbol.MethodSymbol methodSymbol) { - MethodTree methodTree = getMethodTree(methodSymbol); - - Set missingFields = semanticValidationMap.get(methodTree); - // It might be null in case the EnsuresNonNullIf method is completely wrong - if (missingFields == null) { - return false; - } - - return missingFields.isEmpty(); - } - - // Gets the method tree of a given MethodSymbol - private MethodTree getMethodTree(Symbol.MethodSymbol methodSymbol) { - MethodTree methodTree = methodSymbolToMethod.get(methodSymbol); - if (methodTree == null) { - throw new RuntimeException("Method tree not found!"); - } - return methodTree; - } - - // Gets the list of missing fields of a given method - private Set getMissingFields(Symbol.MethodSymbol methodSymbol) { - MethodTree methodTree = getMethodTree(methodSymbol); - Set missingFields = semanticValidationMap.get(methodTree); - if (missingFields == null) { - return Collections.emptySet(); - } - - return missingFields; - } - - private boolean getTrueIfNonNullValue(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("trueIfNonNull")) { - return (boolean) entry.getValue().getValue(); - } - } - - // Not explicitly declared in the annotation, so we default to true - return true; - } - - // Notify about a semantic error in the given EnsuresNonNullIf method - private void notifySemanticError( - Symbol.MethodSymbol methodSymbol, MethodAnalysisContext methodAnalysisContext) { - VisitorState state = methodAnalysisContext.state(); - NullAway analysis = methodAnalysisContext.analysis(); - - MethodTree ensureNonNullIfMethod = getMethodTree(methodSymbol); - Set missingFields = getMissingFields(methodSymbol); - - String message; - if (missingFields.isEmpty()) { - message = "Method is annotated with @EnsuresNonNullIf but does not return boolean"; - } else { - message = - String.format( - "Method is annotated with @EnsuresNonNullIf but does not ensure fields %s", - missingFields); - } - - state.reportMatch( - analysis - .getErrorBuilder() - .createErrorDescription( - new ErrorMessage(ErrorMessage.MessageTypes.POSTCONDITION_NOT_SATISFIED, message), - ensureNonNullIfMethod, - analysis.buildDescription(ensureNonNullIfMethod), - state, - null)); - } } diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/RequiresNonNullHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/RequiresNonNullHandler.java index b6981cc2db..44a6e71782 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/RequiresNonNullHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/RequiresNonNullHandler.java @@ -130,15 +130,14 @@ protected void validateOverridingRules( */ @Override public void onMatchMethodInvocation( - MethodInvocationTree tree, - Symbol.MethodSymbol methodSymbol, - MethodAnalysisContext methodAnalysisContext) { + MethodInvocationTree tree, MethodAnalysisContext methodAnalysisContext) { VisitorState state = methodAnalysisContext.state(); + Symbol.MethodSymbol methodSymbol = methodAnalysisContext.methodSymbol(); NullAway analysis = methodAnalysisContext.analysis(); Set fieldNames = getAnnotationValueArray(methodSymbol, annotName, false); if (fieldNames == null) { - super.onMatchMethodInvocation(tree, methodSymbol, methodAnalysisContext); + super.onMatchMethodInvocation(tree, methodAnalysisContext); return; } fieldNames = ContractUtils.trimReceivers(fieldNames); diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java index d7faef990e..da19e1625e 100644 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -6,7 +6,7 @@ public class EnsuresNonNullIfTests extends NullAwayTestsBase { @Test - public void ensuresNonNullMethod() { + public void correctUse() { defaultCompilationHelper .addSourceLines( "Foo.java", @@ -33,7 +33,7 @@ public void ensuresNonNullMethod() { } @Test - public void ensuresNonNullMethod_2() { + public void correctUse_declarationReversed() { defaultCompilationHelper .addSourceLines( "Foo.java", @@ -42,18 +42,17 @@ public void ensuresNonNullMethod_2() { "import com.uber.nullaway.annotations.EnsuresNonNullIf;", "class Foo {", " @Nullable Item nullableItem;", - " @EnsuresNonNullIf(\"nullableItem\")", - " public boolean hasNullableItem() {", - " return nullableItem != null;", - " }", " public int runOk() {", - " if(hasNullableItem()) {", - " nullableItem.call();", + " if(!hasNullableItem()) {", + " return 1;", " }", - " // BUG: Diagnostic contains: dereferenced expression nullableItem is @Nullable", " nullableItem.call();", " return 0;", " }", + " @EnsuresNonNullIf(\"nullableItem\")", + " public boolean hasNullableItem() {", + " return nullableItem != null;", + " }", "}") .addSourceLines( "Item.java", "package com.uber;", "class Item {", " public void call() { }", "}") @@ -61,7 +60,7 @@ public void ensuresNonNullMethod_2() { } @Test - public void ensuresNonNullMethodWithMoreDataComplexFlow() { + public void correctUse_2() { defaultCompilationHelper .addSourceLines( "Foo.java", @@ -72,16 +71,13 @@ public void ensuresNonNullMethodWithMoreDataComplexFlow() { " @Nullable Item nullableItem;", " @EnsuresNonNullIf(\"nullableItem\")", " public boolean hasNullableItem() {", - " if(nullableItem != null) {", - " return true;", - " } else {", - " return false;", - " }", + " return nullableItem != null;", " }", " public int runOk() {", - " if(!hasNullableItem()) {", - " return 1;", + " if(hasNullableItem()) {", + " nullableItem.call();", " }", + " // BUG: Diagnostic contains: dereferenced expression nullableItem is @Nullable", " nullableItem.call();", " return 0;", " }", @@ -92,7 +88,7 @@ public void ensuresNonNullMethodWithMoreDataComplexFlow() { } @Test - public void catchesWrongReturnFlows() { + public void correctUse_moreComplexFlow() { defaultCompilationHelper .addSourceLines( "Foo.java", @@ -102,12 +98,11 @@ public void catchesWrongReturnFlows() { "class Foo {", " @Nullable Item nullableItem;", " @EnsuresNonNullIf(\"nullableItem\")", - " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", " public boolean hasNullableItem() {", " if(nullableItem != null) {", - " return false;", - " } else {", " return true;", + " } else {", + " return false;", " }", " }", " public int runOk() {", @@ -254,7 +249,7 @@ public void multipleFieldsInSingleAnnotation() { } @Test - public void missingChecksAreDetected() { + public void possibleDeferencedExpression() { defaultCompilationHelper .addSourceLines( "Foo.java", @@ -313,7 +308,7 @@ public void ensuresNonNullMethodUsingThis() { } @Test - public void ensuresNonNullMethodNotCalled() { + public void possibleDeferencedExpression_nonNullMethodNotCalled() { defaultCompilationHelper .addSourceLines( "Foo.java", @@ -337,60 +332,7 @@ public void ensuresNonNullMethodNotCalled() { } @Test - public void warnsIfEnsuresNonNullCheckIfIsWronglyImplemented() { - defaultCompilationHelper - .addSourceLines( - "Foo.java", - "package com.uber;", - "import javax.annotation.Nullable;", - "import com.uber.nullaway.annotations.EnsuresNonNullIf;", - "class Foo {", - " @Nullable Item nullableItem;", - " @EnsuresNonNullIf(\"nullableItem\")", - " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", - " public boolean hasNullableItem() {", - " 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 warnsIfEnsuresNonNullDoesntReturnBoolean() { - defaultCompilationHelper - .addSourceLines( - "Foo.java", - "package com.uber;", - "import javax.annotation.Nullable;", - "import com.uber.nullaway.annotations.EnsuresNonNullIf;", - "class Foo {", - " @Nullable Item nullableItem;", - " @EnsuresNonNullIf(\"nullableItem\")", - " // 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(); - } - - @Test - public void checksForPostconditionsInInheritance() { + public void postConditions_Inheritance() { defaultCompilationHelper .addSourceLines( "SuperClass.java", @@ -527,8 +469,159 @@ public void setTrueIfNonNullToFalseMultipleElements_deferenceFound() { .doTest(); } - // These tests are ignored because currently NullAway doesn't support data-flow of local variables + /******************************************************** + * 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(\"nullableItem\")", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", + " public boolean hasNullableItem() {", + " if(nullableItem != null) {", + " return false;", + " } else {", + " 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 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(\"nullableItem\")", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", + " public boolean hasNullableItem() {", + " if(nullableItem != null) {", + " return false;", + " } else {", + " 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(\"nullableItem\")", + " 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_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\")", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", + " public boolean hasNullableItem() {", + " 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(\"nullableItem\")", + " // 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() { From 5f2ad31e6c3f782e0fac40ad9a2a3b42ce700d18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= Date: Sat, 28 Sep 2024 17:37:44 +0200 Subject: [PATCH 20/52] Code review feedback --- .../com/uber/nullaway/NullabilityUtil.java | 11 ++++++ .../dataflow/AccessPathNullnessAnalysis.java | 25 ++----------- .../uber/nullaway/dataflow/NullnessStore.java | 35 +++++++++++++++++++ .../EnsuresNonNullIfHandler.java | 5 ++- .../fieldcontract/FieldContractUtils.java | 13 ++----- 5 files changed, 54 insertions(+), 35 deletions(-) diff --git a/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java b/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java index 8467c91a07..6e306851c5 100644 --- a/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java +++ b/nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java @@ -248,6 +248,17 @@ 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; 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 f15a5cdf86..6487e5d34a 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java @@ -21,8 +21,8 @@ import static com.uber.nullaway.NullabilityUtil.castToNonNull; import com.google.common.base.Preconditions; -import com.google.common.collect.ImmutableList; import com.google.errorprone.VisitorState; +import com.google.errorprone.dataflow.nullnesspropagation.NullnessAnalysis; import com.sun.source.tree.Tree; import com.sun.source.util.TreePath; import com.sun.tools.javac.util.Context; @@ -157,26 +157,7 @@ public Set getNonnullFieldsOfReceiverAtExit(TreePath path, Context cont // be conservative and say nothing is initialized return Collections.emptySet(); } - return getNonnullReceiverFields(nullnessResult); - } - - // TODO re-use this code - private Set getNonnullReceiverFields(NullnessStore nullnessResult) { - Set nonnullAccessPaths = nullnessResult.getAccessPathsWithValue(Nullness.NONNULL); - Set result = new LinkedHashSet<>(); - for (AccessPath ap : nonnullAccessPaths) { - // A null root represents the receiver - if (ap.getRoot() == null) { - ImmutableList elements = ap.getElements(); - if (elements.size() == 1) { - Element elem = elements.get(0).getJavaElement(); - if (elem.getKind().equals(ElementKind.FIELD)) { - result.add(elem); - } - } - } - } - return result; + return nullnessResult.getNonNullReceiverFields(); } /** @@ -191,7 +172,7 @@ public Set getNonnullFieldsOfReceiverBefore(TreePath path, Context cont if (store == null) { return Collections.emptySet(); } - return getNonnullReceiverFields(store); + return store.getNonNullReceiverFields(); } /** diff --git a/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java b/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java index 8225d5c143..d95986dd70 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java @@ -19,6 +19,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.collect.Sets.intersection; +import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import com.google.errorprone.VisitorState; import com.uber.nullaway.Nullness; @@ -30,6 +31,7 @@ import java.util.function.Predicate; import java.util.stream.Collectors; import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; import org.checkerframework.nullaway.dataflow.analysis.Store; import org.checkerframework.nullaway.dataflow.cfg.node.FieldAccessNode; import org.checkerframework.nullaway.dataflow.cfg.node.LocalVariableNode; @@ -261,6 +263,39 @@ public NullnessStore filterAccessPaths(Predicate pred) { .collect(Collectors.toMap(Map.Entry::getKey, Map.Entry::getValue))); } + /** + * Return all the fields in the store that are Non-Null. + * + * @return Set of fields (represented as @{code Element}s) that are non-null + */ + public Set getNonNullReceiverFields() { + return getReceiverFields(Nullness.NONNULL); + } + + /** + * Return all the fields in the store that hold the {@code nullness} state. + * + * @param nullness The {@code Nullness} state + * @return Set of fields (represented as @{code Element}s) with the given {@code nullness}. + */ + public Set getReceiverFields(Nullness nullness) { + Set nonnullAccessPaths = this.getAccessPathsWithValue(nullness); + Set result = new LinkedHashSet<>(); + for (AccessPath ap : nonnullAccessPaths) { + // A null root represents the receiver + if (ap.getRoot() == null) { + ImmutableList elements = ap.getElements(); + if (elements.size() == 1) { + Element elem = elements.get(0).getJavaElement(); + if (elem.getKind().equals(ElementKind.FIELD)) { + result.add(elem); + } + } + } + } + return result; + } + /** class for building up instances of the store. */ public static final class Builder { private final Map contents; diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java index 1fcf8e3288..2c9da03133 100644 --- 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 @@ -204,9 +204,8 @@ public void onDataflowVisitReturn( // true case) // and check whether all fields in the annotation parameter are non-null Set nonNullFieldsInPath = - thenStore.getAccessPathsWithValue(trueIfNonNull ? Nullness.NONNULL : Nullness.NULL).stream() - .flatMap(ap -> ap.getElements().stream()) - .map(e -> e.getJavaElement().getSimpleName().toString()) + thenStore.getReceiverFields(trueIfNonNull ? Nullness.NONNULL : Nullness.NULL).stream() + .map(e -> e.getSimpleName().toString()) .collect(Collectors.toSet()); boolean allFieldsInPathAreVerified = nonNullFieldsInPath.containsAll(fieldNames); 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 index f11162e335..a879653557 100644 --- 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 @@ -10,7 +10,6 @@ import com.uber.nullaway.ErrorMessage; import com.uber.nullaway.NullAway; import java.util.Collections; -import java.util.Iterator; import java.util.Set; public class FieldContractUtils { @@ -43,18 +42,12 @@ public static void validateOverridingRules( .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(" 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() From 3ad394476fbdde0979a406ef4d4120d695b66103 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= Date: Sat, 28 Sep 2024 17:38:45 +0200 Subject: [PATCH 21/52] Nit on javadoc --- .../contract/fieldcontract/EnsuresNonNullIfHandler.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 index 2c9da03133..1953f4e7f7 100644 --- 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 @@ -1,5 +1,5 @@ /* - * Copyright (c) 2017-2020 Uber Technologies, Inc. + * 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 From 3afb83663c1314719a3e70a70ff9c57858e47e5b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= Date: Sat, 28 Sep 2024 17:42:43 +0200 Subject: [PATCH 22/52] Nit in comments --- .../EnsuresNonNullIfHandler.java | 23 ++++++++++--------- 1 file changed, 12 insertions(+), 11 deletions(-) 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 index 1953f4e7f7..14cfec441e 100644 --- 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 @@ -68,6 +68,7 @@ public class EnsuresNonNullIfHandler extends AbstractFieldContractHandler { // List of fields missing in the current EnsuresNonNullIf method // so we can build proper error message @Nullable private Set missingFieldNames; + // The MethodTree and Symbol of the EnsureNonNullIf method under semantic validation @Nullable private MethodTree methodTreeUnderAnalysis; @Nullable private Symbol.MethodSymbol methodSymbolUnderAnalysis; @@ -128,7 +129,7 @@ protected boolean validateAnnotationSemantics( null)); } - // Clean up state + // Clean up state again semanticsHold = false; missingFieldNames = null; methodTreeUnderAnalysis = null; @@ -164,8 +165,8 @@ public Void visitReturn(ReturnTree node, Void unused) { } /* - * 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. + * 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( @@ -187,8 +188,8 @@ public void onDataflowVisitReturn( return; } - // We might have already found another return tree that results in what we need, - // so we don't keep going deep. + // We might have already found another return tree that results in + // what we need, so we don't keep going deep. if (semanticsHold) { return; } @@ -200,8 +201,8 @@ public void onDataflowVisitReturn( boolean trueIfNonNull = getTrueIfNonNullValue(methodSymbolUnderAnalysis); - // We extract all the data-flow of the fields found by the engine in the "then" case (i.e., - // true case) + // We extract all the data-flow of the fields found by the + // engine in the "then" case (i.e., true case) // and check whether all fields in the annotation parameter are non-null Set nonNullFieldsInPath = thenStore.getReceiverFields(trueIfNonNull ? Nullness.NONNULL : Nullness.NULL).stream() @@ -210,16 +211,16 @@ public void onDataflowVisitReturn( boolean allFieldsInPathAreVerified = nonNullFieldsInPath.containsAll(fieldNames); if (allFieldsInPathAreVerified) { - // If it's a literal, then, it needs to return true/false, depending on the trueIfNonNull - // flag + // If it's a literal, then, it needs to return true/false, + // depending on the trueIfNonNull flag if (returnTree.getExpression() instanceof LiteralTree) { LiteralTree expressionAsLiteral = (LiteralTree) returnTree.getExpression(); if (expressionAsLiteral.getValue() instanceof Boolean) { this.semanticsHold = (boolean) expressionAsLiteral.getValue(); } } else { - // We then trust on the analysis of the engine that, at this point, the field is checked - // for null + // We then trust on the analysis of the engine that, at this point, + // the field is checked for null this.semanticsHold = true; } } else { From de81671f7d65e36ac838b7c59e376278f7593e56 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= Date: Sat, 28 Sep 2024 17:46:13 +0200 Subject: [PATCH 23/52] Put class back to original state to reduce changes in PR --- .../com/uber/nullaway/handlers/AbstractFieldContractHandler.java | 1 + 1 file changed, 1 insertion(+) diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/AbstractFieldContractHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/AbstractFieldContractHandler.java index fe571c5319..3d590f7c61 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/AbstractFieldContractHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/AbstractFieldContractHandler.java @@ -65,6 +65,7 @@ protected AbstractFieldContractHandler(String annotName) { */ @Override public void onMatchMethod(MethodTree tree, MethodAnalysisContext methodAnalysisContext) { + Symbol.MethodSymbol methodSymbol = methodAnalysisContext.methodSymbol(); VisitorState state = methodAnalysisContext.state(); Set annotationContent = From 92b3a770500f950ef0eb3ff239e1684fcf3e3651 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= Date: Sun, 29 Sep 2024 09:51:40 +0200 Subject: [PATCH 24/52] Got it working --- .../AccessPathNullnessPropagation.java | 3 +- .../uber/nullaway/dataflow/NullnessStore.java | 4 +- .../nullaway/handlers/BaseNoOpHandler.java | 2 +- .../nullaway/handlers/CompositeHandler.java | 4 +- .../com/uber/nullaway/handlers/Handler.java | 4 +- .../handlers/StreamNullabilityPropagator.java | 2 +- .../EnsuresNonNullIfHandler.java | 125 +++++++++--------- .../uber/nullaway/EnsuresNonNullIfTests.java | 10 +- 8 files changed, 83 insertions(+), 71 deletions(-) diff --git a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java index 49dca06fac..88817b1a61 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java @@ -852,7 +852,8 @@ public TransferResult visitSuper( @Override public TransferResult visitReturn( ReturnNode returnNode, TransferInput input) { - handler.onDataflowVisitReturn(returnNode.getTree(), input.getThenStore(), input.getElseStore()); + handler.onDataflowVisitReturn( + returnNode.getTree(), state, input.getThenStore(), input.getElseStore()); return noStoreChanges(NULLABLE, input); } diff --git a/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java b/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java index d95986dd70..43fd3d4714 100644 --- a/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java +++ b/nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java @@ -266,7 +266,7 @@ public NullnessStore filterAccessPaths(Predicate pred) { /** * Return all the fields in the store that are Non-Null. * - * @return Set of fields (represented as @{code Element}s) that are non-null + * @return Set of fields (represented as {@code Element}s) that are non-null */ public Set getNonNullReceiverFields() { return getReceiverFields(Nullness.NONNULL); @@ -276,7 +276,7 @@ public Set getNonNullReceiverFields() { * 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}. + * @return Set of fields (represented as {@code Element}s) with the given {@code nullness}. */ public Set getReceiverFields(Nullness nullness) { Set nonnullAccessPaths = this.getAccessPathsWithValue(nullness); diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java index 3664529998..d9f6ba13cf 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java @@ -174,7 +174,7 @@ public NullnessHint onDataflowVisitFieldAccess( @Override public void onDataflowVisitReturn( - ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore) { + ReturnTree tree, VisitorState state, NullnessStore thenStore, NullnessStore elseStore) { // NoOp } diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java index df5293d690..f1a5997da2 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java @@ -220,9 +220,9 @@ public NullnessHint onDataflowVisitFieldAccess( @Override public void onDataflowVisitReturn( - ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore) { + ReturnTree tree, VisitorState state, NullnessStore thenStore, NullnessStore elseStore) { for (Handler h : handlers) { - h.onDataflowVisitReturn(tree, thenStore, elseStore); + h.onDataflowVisitReturn(tree, state, thenStore, elseStore); } } diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java index f8a11afe85..298d01d7db 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java @@ -269,12 +269,14 @@ NullnessHint onDataflowVisitFieldAccess( * Called when the Dataflow analysis visits a return statement. * * @param tree The AST node for the return statement being matched. + * @param state The current visitor state * @param thenStore The NullnessStore for the true case of the expression inside the return * statement. * @param elseStore The NullnessStore for the false case of the expression inside the return * statement. */ - void onDataflowVisitReturn(ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore); + void onDataflowVisitReturn( + ReturnTree tree, VisitorState state, NullnessStore thenStore, NullnessStore elseStore); /** * Called when the Dataflow analysis visits the result expression inside the body of lambda. diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java b/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java index 48e1ce6052..c411522da7 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/StreamNullabilityPropagator.java @@ -595,7 +595,7 @@ public NullnessStore.Builder onDataflowInitialStore( @Override public void onDataflowVisitReturn( - ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore) { + ReturnTree tree, VisitorState state, NullnessStore thenStore, NullnessStore elseStore) { Tree filterTree = returnToEnclosingMethodOrLambda.get(tree); if (filterTree != null) { assert (filterTree instanceof MethodTree || filterTree instanceof LambdaExpressionTree); diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java index 14cfec441e..a17c5d0121 100644 --- 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 @@ -30,6 +30,7 @@ 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; @@ -60,18 +61,11 @@ */ public class EnsuresNonNullIfHandler extends AbstractFieldContractHandler { - // Set to true when the current visited EnsuresNonNullIf method has correct semantics - private boolean semanticsHold; - private final Set returnTreesInMethodUnderAnalysis = new HashSet<>(); - // List of fields missing in the current EnsuresNonNullIf method - // so we can build proper error message - @Nullable private Set missingFieldNames; - // The MethodTree and Symbol of the EnsureNonNullIf method under semantic validation @Nullable private MethodTree methodTreeUnderAnalysis; - @Nullable private Symbol.MethodSymbol methodSymbolUnderAnalysis; + @Nullable private MethodAnalysisContext methodAnalysisContextUnderAnalysis; public EnsuresNonNullIfHandler() { super("EnsuresNonNullIf"); @@ -89,10 +83,8 @@ protected boolean validateAnnotationSemantics( } // clean up state variables, as we are visiting a new annotated method - semanticsHold = false; - missingFieldNames = null; methodTreeUnderAnalysis = tree; - methodSymbolUnderAnalysis = methodAnalysisContext.methodSymbol(); + methodAnalysisContextUnderAnalysis = methodAnalysisContext; returnTreesInMethodUnderAnalysis.clear(); VisitorState state = methodAnalysisContext.state(); @@ -102,38 +94,19 @@ protected boolean validateAnnotationSemantics( // 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"); + } + // We force the nullness analysis of the method under validation analysis .getNullnessAnalysis(state) .forceRunOnMethod(new TreePath(state.getPath(), tree), state.context); - // If listed fields aren't checked for their nullness, return error - if (!semanticsHold) { - String message; - if (missingFieldNames == null) { - message = "Method is annotated with @EnsuresNonNullIf but does not return boolean"; - } else { - message = - String.format( - "Method is annotated with @EnsuresNonNullIf but does not ensure fields %s", - missingFieldNames); - } - state.reportMatch( - analysis - .getErrorBuilder() - .createErrorDescription( - new ErrorMessage(ErrorMessage.MessageTypes.POSTCONDITION_NOT_SATISFIED, message), - tree, - analysis.buildDescription(tree), - state, - null)); - } - - // Clean up state again - semanticsHold = false; - missingFieldNames = null; - methodTreeUnderAnalysis = null; - methodSymbolUnderAnalysis = null; + // Clean up state + methodAnalysisContextUnderAnalysis = null; returnTreesInMethodUnderAnalysis.clear(); return true; @@ -181,19 +154,15 @@ protected void validateOverridingRules( @Override public void onDataflowVisitReturn( - ReturnTree returnTree, NullnessStore thenStore, NullnessStore elseStore) { + 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; } - // We might have already found another return tree that results in - // what we need, so we don't keep going deep. - if (semanticsHold) { - return; - } - + Symbol.MethodSymbol methodSymbolUnderAnalysis = + methodAnalysisContextUnderAnalysis.methodSymbol(); Set fieldNames = getAnnotationValueArray(methodSymbolUnderAnalysis, annotName, false); if (fieldNames == null) { throw new RuntimeException("List of field names shouldn't be null"); @@ -210,26 +179,64 @@ public void onDataflowVisitReturn( .collect(Collectors.toSet()); boolean allFieldsInPathAreVerified = nonNullFieldsInPath.containsAll(fieldNames); - if (allFieldsInPathAreVerified) { - // If it's a literal, then, it needs to return true/false, - // depending on the trueIfNonNull flag - if (returnTree.getExpression() instanceof LiteralTree) { - LiteralTree expressionAsLiteral = (LiteralTree) returnTree.getExpression(); - if (expressionAsLiteral.getValue() instanceof Boolean) { - this.semanticsHold = (boolean) expressionAsLiteral.getValue(); + if (returnTree.getExpression() instanceof LiteralTree) { + LiteralTree expressionAsLiteral = (LiteralTree) returnTree.getExpression(); + if (expressionAsLiteral.getValue() instanceof Boolean) { + boolean expressionAsBoolean = (boolean) expressionAsLiteral.getValue(); + + if (allFieldsInPathAreVerified && expressionAsBoolean) { + // correct semantic + // fields are verified and expression returns true + } else if (!allFieldsInPathAreVerified && !expressionAsBoolean) { + // correct semantic + // fields aren't all verified and expression return false + } else if (allFieldsInPathAreVerified && !expressionAsBoolean) { + // wrong semantic + // fields are verified but method is returning false, raise warn + String message = + String.format( + "The method ensures the %s of the fields, but doesn't return true", + (trueIfNonNull ? "non-nullability" : "nullability")); + raiseError(returnTree, state, message); + } else if (!allFieldsInPathAreVerified && expressionAsBoolean) { + // wrong semantic + // fields are not verified, but method returns true + fieldNames.removeAll(nonNullFieldsInPath); + String message = + String.format( + "Method is annotated with @EnsuresNonNullIf but does not ensure fields %s", + fieldNames); + raiseError(returnTree, state, message); } - } else { - // We then trust on the analysis of the engine that, at this point, - // the field is checked for null - this.semanticsHold = true; } } else { - // Build list of missing fields for the elegant validation error message - fieldNames.removeAll(nonNullFieldsInPath); - this.missingFieldNames = new HashSet<>(fieldNames); + if (allFieldsInPathAreVerified) { + // we trust on the engine here, as we can't evaluate the concrete boolean + // return of the return expression + } else { + 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 = methodAnalysisContextUnderAnalysis.analysis(); + state.reportMatch( + analysis + .getErrorBuilder() + .createErrorDescription( + new ErrorMessage(ErrorMessage.MessageTypes.POSTCONDITION_NOT_SATISFIED, message), + returnTree, + analysis.buildDescription(returnTree), + state, + null)); + } + private boolean getTrueIfNonNullValue(Symbol.MethodSymbol methodSymbol) { AnnotationMirror annot = NullabilityUtil.findAnnotation(methodSymbol, annotName, false); if (annot == null) { diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java index da19e1625e..d935ee5995 100644 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java @@ -451,8 +451,8 @@ public void setTrueIfNonNullToFalseMultipleElements_deferenceFound() { " @Nullable Item nullableItem;", " @Nullable Item nullableItem2;", " @EnsuresNonNullIf(value={\"nullableItem\",\"nullableItem2\"}, trueIfNonNull=false)", - " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem, nullableItem2]", " public boolean doesNotHaveNullableItem() {", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem, nullableItem2]", " return nullableItem == null || nullableItem2 == null;", " }", " public int runOk() {", @@ -484,11 +484,12 @@ public void semanticIssues_doesntEnsureNonNullabilityOfFields() { "class Foo {", " @Nullable Item nullableItem;", " @EnsuresNonNullIf(\"nullableItem\")", - " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", " public boolean hasNullableItem() {", " if(nullableItem != null) {", + " // BUG: Diagnostic contains: The method ensures the non-nullability of the fields, but doesn't return true", " return false;", " } else {", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", " return true;", " }", " }", @@ -523,11 +524,12 @@ public void semanticIssues_methodDeclarationReversed() { " return 0;", " }", " @EnsuresNonNullIf(\"nullableItem\")", - " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", " public boolean hasNullableItem() {", " if(nullableItem != null) {", + " // BUG: Diagnostic contains: The method ensures the non-nullability of the fields, but doesn't return true", " return false;", " } else {", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", " return true;", " }", " }", @@ -579,8 +581,8 @@ public void semanticIssues_2() { "class Foo {", " @Nullable Item nullableItem;", " @EnsuresNonNullIf(\"nullableItem\")", - " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", " public boolean hasNullableItem() {", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]", " return true;", " }", " public void runOk() {", From 04a7d42ae61c0b0eda91c2a3c1c6b8809de2c35d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= Date: Sun, 29 Sep 2024 10:12:44 +0200 Subject: [PATCH 25/52] Cleaning up the doc and more docs --- .../EnsuresNonNullIfHandler.java | 77 ++++++++++++------- 1 file changed, 49 insertions(+), 28 deletions(-) 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 index a17c5d0121..96593d58ee 100644 --- 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 @@ -46,6 +46,7 @@ import com.uber.nullaway.handlers.contract.ContractUtils; import java.util.HashSet; import java.util.Map; +import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; import javax.annotation.Nullable; @@ -179,41 +180,61 @@ public void onDataflowVisitReturn( .collect(Collectors.toSet()); boolean allFieldsInPathAreVerified = nonNullFieldsInPath.containsAll(fieldNames); + // We store whether the return true expression evaluates to a boolean literal or not. + Optional expressionAsBoolean = Optional.empty(); if (returnTree.getExpression() instanceof LiteralTree) { LiteralTree expressionAsLiteral = (LiteralTree) returnTree.getExpression(); if (expressionAsLiteral.getValue() instanceof Boolean) { - boolean expressionAsBoolean = (boolean) expressionAsLiteral.getValue(); - - if (allFieldsInPathAreVerified && expressionAsBoolean) { - // correct semantic - // fields are verified and expression returns true - } else if (!allFieldsInPathAreVerified && !expressionAsBoolean) { - // correct semantic - // fields aren't all verified and expression return false - } else if (allFieldsInPathAreVerified && !expressionAsBoolean) { - // wrong semantic - // fields are verified but method is returning false, raise warn - String message = - String.format( - "The method ensures the %s of the fields, but doesn't return true", - (trueIfNonNull ? "non-nullability" : "nullability")); - raiseError(returnTree, state, message); - } else if (!allFieldsInPathAreVerified && expressionAsBoolean) { - // wrong semantic - // fields are not verified, but method returns true - fieldNames.removeAll(nonNullFieldsInPath); - String message = - String.format( - "Method is annotated with @EnsuresNonNullIf but does not ensure fields %s", - fieldNames); - raiseError(returnTree, state, message); - } + expressionAsBoolean = Optional.of((boolean) expressionAsLiteral.getValue()); } - } else { - if (allFieldsInPathAreVerified) { + } + + boolean evaluatesToLiteral = expressionAsBoolean.isPresent(); + boolean evaluatesToTrue = evaluatesToLiteral && expressionAsBoolean.get(); + boolean evaluatesToFalse = evaluatesToLiteral && !expressionAsBoolean.get(); + + /* + * Decide whether the semantics of this ReturnTree are correct. + * The decision is as follows: + * + * If all fields in the path are verified: + * - If the literal boolean evaluates to true, it's correct, as the method + * does return true in case the semantics hold. + * - If the literal boolean evaluates to false, it's wrong, as the method + * incorrect return false when it should have returned true. + * - If the expression isn't a literal boolean, but something more complex, + * we assume it's correct as we trust the data-flow engine. + * + * If fields in path aren't verified: + * - If the literal boolean evaluates to false, it's correct, as the method + * correctly returns false in case the semantics don't hold. + * - If the literal boolean evaluates to true, it's wrong, as the method + * incorrectly returns true when it should have returned false. + */ + if (allFieldsInPathAreVerified) { + if (!evaluatesToLiteral) { + // correct semantic // we trust on the engine here, as we can't evaluate the concrete boolean // return of the return expression + } else if (evaluatesToTrue) { + // correct semantic + // fields are verified and expression returns true + } else { + // wrong semantic + // fields are verified but method is returning false, raise warn + String message = + String.format( + "The method ensures the %s of the fields, but doesn't return true", + (trueIfNonNull ? "non-nullability" : "nullability")); + raiseError(returnTree, state, message); + } + } else { + if (evaluatesToFalse) { + // correct semantic + // fields aren't all verified and expression return false } else { + // wrong semantic + // fields are not verified, but method returns true fieldNames.removeAll(nonNullFieldsInPath); String message = String.format( From ee32c4886d78c25c9413c67b2ce5eab87776d04e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= Date: Sun, 29 Sep 2024 10:13:19 +0200 Subject: [PATCH 26/52] Fix clean up --- .../handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java | 1 + 1 file changed, 1 insertion(+) 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 index 96593d58ee..06386cea3e 100644 --- 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 @@ -107,6 +107,7 @@ protected boolean validateAnnotationSemantics( .forceRunOnMethod(new TreePath(state.getPath(), tree), state.context); // Clean up state + methodTreeUnderAnalysis = null; methodAnalysisContextUnderAnalysis = null; returnTreesInMethodUnderAnalysis.clear(); From 81b1edc7e25ebfce4e1505cf2197e8008dcdb573 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= Date: Sun, 29 Sep 2024 10:13:34 +0200 Subject: [PATCH 27/52] More fixes --- .../handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java | 1 + 1 file changed, 1 insertion(+) 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 index 06386cea3e..4a5e247368 100644 --- 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 @@ -99,6 +99,7 @@ protected boolean validateAnnotationSemantics( 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 From fbd05a7001bd4a05e361624fe78f1be69235064b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= Date: Sun, 29 Sep 2024 10:56:43 +0200 Subject: [PATCH 28/52] Rename trueIfNonNull to result and make it compulsory, to match CheckerFramework --- .../annotations/EnsuresNonNullIf.java | 19 ++++++- .../EnsuresNonNullIfHandler.java | 13 +++-- .../uber/nullaway/EnsuresNonNullIfTests.java | 56 +++++++++---------- 3 files changed, 51 insertions(+), 37 deletions(-) diff --git a/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java index 9a3946665a..53086523fe 100644 --- a/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java +++ b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java @@ -9,7 +9,7 @@ * 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 true in case the fields - * are null (inverse logic), and in such case, you must set trueIfNonNull to false. NullAway + * are null (inverse logic), and in such case, you must set {@code result} to false. NullAway * verifies that the property holds. * *

Here is an example: @@ -17,14 +17,17 @@ * 

  * class Foo {
  *     {@literal @}Nullable Object theField;
- *     {@literal @}EnsuresNonNullIf("theField") // @EnsuresNonNullIf("this.theField") is also valid
+ *
+ *     {@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();
  *     }
@@ -34,7 +37,17 @@
 @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();
 
-  boolean trueIfNonNull() default true;
+  /**
+   * The return value of the method under which the postcondition holds.
+   *
+   * @return true or false
+   */
+  boolean result();
 }
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
index 4a5e247368..8ed12f73fc 100644
--- 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
@@ -171,7 +171,7 @@ public void onDataflowVisitReturn(
       throw new RuntimeException("List of field names shouldn't be null");
     }
 
-    boolean trueIfNonNull = getTrueIfNonNullValue(methodSymbolUnderAnalysis);
+    boolean trueIfNonNull = getResultValueFromAnnotation(methodSymbolUnderAnalysis);
 
     // We extract all the data-flow of the fields found by the
     // engine in the "then" case (i.e., true case)
@@ -260,7 +260,7 @@ private void raiseError(Tree returnTree, VisitorState state, String message) {
                 null));
   }
 
-  private boolean getTrueIfNonNullValue(Symbol.MethodSymbol methodSymbol) {
+  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");
@@ -271,13 +271,14 @@ private boolean getTrueIfNonNullValue(Symbol.MethodSymbol methodSymbol) {
     for (Map.Entry entry :
         elementValues.entrySet()) {
       ExecutableElement elem = entry.getKey();
-      if (elem.getSimpleName().contentEquals("trueIfNonNull")) {
+      if (elem.getSimpleName().contentEquals("result")) {
         return (boolean) entry.getValue().getValue();
       }
     }
 
     // Not explicitly declared in the annotation, so we default to true
-    return true;
+    throw new RuntimeException(
+        "EnsureNonNullIf requires explicit 'return' value of the method under which the postcondition holds.");
   }
 
   /**
@@ -302,7 +303,7 @@ public NullnessHint onDataflowVisitMethodInvocation(
 
     Set fieldNames = getAnnotationValueArray(methodSymbol, annotName, false);
     if (fieldNames != null) {
-      boolean trueIfNonNull = getTrueIfNonNullValue(methodSymbol);
+      boolean trueIfNonNull = getResultValueFromAnnotation(methodSymbol);
       fieldNames = ContractUtils.trimReceivers(fieldNames);
       for (String fieldName : fieldNames) {
         VariableElement field =
@@ -320,7 +321,7 @@ public NullnessHint onDataflowVisitMethodInvocation(
         }
 
         // The call to the EnsuresNonNullIf method ensures that the field is then not null
-        // (or null, depending on the trueIfNotNUll flag) at this point.
+        // (or null, depending on the result flag) at this point.
         // In here, we assume that the annotated method is already validated.
         thenUpdates.set(accessPath, trueIfNonNull ? Nullness.NONNULL : Nullness.NULL);
         elseUpdates.set(accessPath, trueIfNonNull ? Nullness.NULL : Nullness.NONNULL);
diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index d935ee5995..51366595c2 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -15,7 +15,7 @@ public void correctUse() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class Foo {",
             "  @Nullable Item nullableItem;",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    return nullableItem != null;",
             "  }",
@@ -49,7 +49,7 @@ public void correctUse_declarationReversed() {
             "    nullableItem.call();",
             "    return 0;",
             "  }",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    return nullableItem != null;",
             "  }",
@@ -69,7 +69,7 @@ public void correctUse_2() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class Foo {",
             "  @Nullable Item nullableItem;",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    return nullableItem != null;",
             "  }",
@@ -97,7 +97,7 @@ public void correctUse_moreComplexFlow() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class Foo {",
             "  @Nullable Item nullableItem;",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    if(nullableItem != null) {",
             "      return true;",
@@ -129,11 +129,11 @@ public void multipleEnsuresNonNullIfMethods() {
             "class Foo {",
             "  @Nullable Item nullableItem;",
             "  @Nullable Item nullableItem2;",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    return nullableItem != null;",
             "  }",
-            "  @EnsuresNonNullIf(\"nullableItem2\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem2\", result=true)",
             "  public boolean hasNullableItem2() {",
             "    return nullableItem2 != null;",
             "  }",
@@ -162,11 +162,11 @@ public void multipleEnsuresNonNullIfMethods_2() {
             "class Foo {",
             "  @Nullable Item nullableItem;",
             "  @Nullable Item nullableItem2;",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    return nullableItem != null;",
             "  }",
-            "  @EnsuresNonNullIf(\"nullableItem2\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem2\", result=true)",
             "  public boolean hasNullableItem2() {",
             "    return nullableItem2 != null;",
             "  }",
@@ -195,11 +195,11 @@ public void multipleEnsuresNonNullIfMethods_3() {
             "class Foo {",
             "  @Nullable Item nullableItem;",
             "  @Nullable Item nullableItem2;",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    return nullableItem != null;",
             "  }",
-            "  @EnsuresNonNullIf(\"nullableItem2\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem2\", result=true)",
             "  public boolean hasNullableItem2() {",
             "    return nullableItem2 != null;",
             "  }",
@@ -230,7 +230,7 @@ public void multipleFieldsInSingleAnnotation() {
             "class Foo {",
             "  @Nullable Item nullableItem;",
             "  @Nullable Item nullableItem2;",
-            "  @EnsuresNonNullIf({\"nullableItem\", \"nullableItem2\"})",
+            "  @EnsuresNonNullIf(value={\"nullableItem\", \"nullableItem2\"}, result=true)",
             "  public boolean hasNullableItems() {",
             "    return nullableItem != null && nullableItem2 != null;",
             "  }",
@@ -259,11 +259,11 @@ public void possibleDeferencedExpression() {
             "class Foo {",
             "  @Nullable Item nullableItem;",
             "  @Nullable Item nullableItem2;",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    return nullableItem != null;",
             "  }",
-            "  @EnsuresNonNullIf(\"nullableItem2\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem2\", result=true)",
             "  public boolean hasNullableItem2() {",
             "    return nullableItem2 != null;",
             "  }",
@@ -292,7 +292,7 @@ public void ensuresNonNullMethodUsingThis() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class Foo {",
             "  @Nullable Item nullableItem;",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    return this.nullableItem != null;",
             "  }",
@@ -317,7 +317,7 @@ public void possibleDeferencedExpression_nonNullMethodNotCalled() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class Foo {",
             "  @Nullable Item nullableItem;",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    return nullableItem != null;",
             "  }",
@@ -342,11 +342,11 @@ public void postConditions_Inheritance() {
             "class SuperClass {",
             "  @Nullable Item a;",
             "  @Nullable Item b;",
-            "  @EnsuresNonNullIf(\"a\")",
+            "  @EnsuresNonNullIf(value=\"a\", result=true)",
             "  public boolean hasA() {",
             "    return a != null;",
             "  }",
-            "  @EnsuresNonNullIf(\"b\")",
+            "  @EnsuresNonNullIf(value=\"b\", result=true)",
             "  public boolean hasB() {",
             "    return b != null;",
             "  }",
@@ -363,12 +363,12 @@ public void postConditions_Inheritance() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class ChildLevelOne extends SuperClass {",
             "  @Nullable Item c;",
-            "  @EnsuresNonNullIf(\"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({\"b\", \"c\"})",
+            "  @EnsuresNonNullIf(value={\"b\", \"c\"}, result=true)",
             "  public boolean hasB() {",
             "    return b != null && c != null;",
             "  }",
@@ -393,7 +393,7 @@ public void setTrueIfNonNullToFalse() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class Foo {",
             "  @Nullable Item nullableItem;",
-            "  @EnsuresNonNullIf(value=\"nullableItem\", trueIfNonNull=false)",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=false)",
             "  public boolean doesNotHaveNullableItem() {",
             "    return nullableItem == null;",
             "  }",
@@ -421,7 +421,7 @@ public void setTrueIfNonNullToFalseMultipleElements() {
             "class Foo {",
             "  @Nullable Item nullableItem;",
             "  @Nullable Item nullableItem2;",
-            "  @EnsuresNonNullIf(value={\"nullableItem\",\"nullableItem2\"}, trueIfNonNull=false)",
+            "  @EnsuresNonNullIf(value={\"nullableItem\",\"nullableItem2\"}, result=false)",
             "  public boolean doesNotHaveNullableItem() {",
             "    return nullableItem == null && nullableItem2 == null;",
             "  }",
@@ -450,7 +450,7 @@ public void setTrueIfNonNullToFalseMultipleElements_deferenceFound() {
             "class Foo {",
             "  @Nullable Item nullableItem;",
             "  @Nullable Item nullableItem2;",
-            "  @EnsuresNonNullIf(value={\"nullableItem\",\"nullableItem2\"}, trueIfNonNull=false)",
+            "  @EnsuresNonNullIf(value={\"nullableItem\",\"nullableItem2\"}, result=false)",
             "  public boolean doesNotHaveNullableItem() {",
             "    // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem, nullableItem2]",
             "    return nullableItem == null || nullableItem2 == null;",
@@ -483,7 +483,7 @@ public void semanticIssues_doesntEnsureNonNullabilityOfFields() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class Foo {",
             "  @Nullable Item nullableItem;",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    if(nullableItem != null) {",
             "      // BUG: Diagnostic contains: The method ensures the non-nullability of the fields, but doesn't return true",
@@ -523,7 +523,7 @@ public void semanticIssues_methodDeclarationReversed() {
             "    nullableItem.call();",
             "    return 0;",
             "  }",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    if(nullableItem != null) {",
             "      // BUG: Diagnostic contains: The method ensures the non-nullability of the fields, but doesn't return true",
@@ -550,7 +550,7 @@ public void semanticIssues_ignoreLambdaReturns() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class Foo {",
             "  @Nullable Item nullableItem;",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    BooleanSupplier test = () -> {",
             "      return nullableItem == null;",
@@ -580,7 +580,7 @@ public void semanticIssues_2() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class Foo {",
             "  @Nullable Item nullableItem;",
-            "  @EnsuresNonNullIf(\"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;",
@@ -607,7 +607,7 @@ public void semanticIssues_warnsIfEnsuresNonNullDoesntReturnBoolean() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class Foo {",
             "  @Nullable Item nullableItem;",
-            "  @EnsuresNonNullIf(\"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;",
@@ -635,7 +635,7 @@ public void ensuresNonNullMethodWithMoreDataComplexFlow_2() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class Foo {",
             "  @Nullable Item nullableItem;",
-            "  @EnsuresNonNullIf(\"nullableItem\")",
+            "  @EnsuresNonNullIf(\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    var x = (nullableItem != null);",
             "    return x;",

From b1faf00ac2f297287d4b2e65658a040aa1203609 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Sun, 29 Sep 2024 11:06:13 +0200
Subject: [PATCH 29/52] More cleanups

---
 .../fieldcontract/EnsuresNonNullHandler.java  |  2 +-
 .../EnsuresNonNullIfHandler.java              | 40 ++++++++-----------
 .../fieldcontract/FieldContractUtils.java     |  2 +-
 3 files changed, 19 insertions(+), 25 deletions(-)

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 b68c09c29c..ebce29f582 100644
--- a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullHandler.java
+++ b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullHandler.java
@@ -123,7 +123,7 @@ protected void validateOverridingRules(
       VisitorState state,
       MethodTree tree,
       Symbol.MethodSymbol overriddenMethod) {
-    FieldContractUtils.validateOverridingRules(
+    FieldContractUtils.ensureStrictPostConditionInheritance(
         annotName, overridingFieldNames, analysis, state, tree, overriddenMethod);
   }
 
diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java
index 8ed12f73fc..b632b3b899 100644
--- 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
@@ -62,9 +62,14 @@
  */
 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 Symbol of the EnsureNonNullIf method under semantic validation
+  // The MethodTree and MethodAnalysisContext of the EnsureNonNullIf method
+  // under current semantic validation
+  // They are set to null when no methods are being validated.
   @Nullable private MethodTree methodTreeUnderAnalysis;
   @Nullable private MethodAnalysisContext methodAnalysisContextUnderAnalysis;
 
@@ -103,6 +108,7 @@ protected boolean validateAnnotationSemantics(
     }
 
     // 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);
@@ -120,10 +126,8 @@ private void buildUpReturnToEnclosingMethodMap(VisitorState methodState) {
     new TreePathScanner() {
       @Override
       public Void visitReturn(ReturnTree node, Void unused) {
-        VisitorState returnState = methodState.withPath(getCurrentPath());
-
         TreePath enclosingMethod =
-            NullabilityUtil.findEnclosingMethodOrLambdaOrInitializer(returnState.getPath());
+            NullabilityUtil.findEnclosingMethodOrLambdaOrInitializer(getCurrentPath());
         if (enclosingMethod == null) {
           throw new RuntimeException("no enclosing method, lambda or initializer!");
         }
@@ -151,7 +155,7 @@ protected void validateOverridingRules(
       VisitorState state,
       MethodTree tree,
       Symbol.MethodSymbol overriddenMethod) {
-    FieldContractUtils.validateOverridingRules(
+    FieldContractUtils.ensureStrictPostConditionInheritance(
         annotName, overridingFieldNames, analysis, state, tree, overriddenMethod);
   }
 
@@ -164,6 +168,7 @@ public void onDataflowVisitReturn(
       return;
     }
 
+    // Get the declared configuration of the EnsureNonNullIf method under analysis
     Symbol.MethodSymbol methodSymbolUnderAnalysis =
         methodAnalysisContextUnderAnalysis.methodSymbol();
     Set fieldNames = getAnnotationValueArray(methodSymbolUnderAnalysis, annotName, false);
@@ -182,7 +187,7 @@ public void onDataflowVisitReturn(
             .collect(Collectors.toSet());
     boolean allFieldsInPathAreVerified = nonNullFieldsInPath.containsAll(fieldNames);
 
-    // We store whether the return true expression evaluates to a boolean literal or not.
+    // Whether the return true expression evaluates to a boolean literal or not.
     Optional expressionAsBoolean = Optional.empty();
     if (returnTree.getExpression() instanceof LiteralTree) {
       LiteralTree expressionAsLiteral = (LiteralTree) returnTree.getExpression();
@@ -192,8 +197,8 @@ public void onDataflowVisitReturn(
     }
 
     boolean evaluatesToLiteral = expressionAsBoolean.isPresent();
-    boolean evaluatesToTrue = evaluatesToLiteral && expressionAsBoolean.get();
     boolean evaluatesToFalse = evaluatesToLiteral && !expressionAsBoolean.get();
+    boolean evaluatesToTrue = evaluatesToLiteral && expressionAsBoolean.get();
 
     /*
      * Decide whether the semantics of this ReturnTree are correct.
@@ -212,18 +217,11 @@ public void onDataflowVisitReturn(
      * correctly returns false in case the semantics don't hold.
      * - If the literal boolean evaluates to true, it's wrong, as the method
      * incorrectly returns true when it should have returned false.
+     *
+     * The implementation below doesn't need to go through all the combinations.
      */
     if (allFieldsInPathAreVerified) {
-      if (!evaluatesToLiteral) {
-        // correct semantic
-        // we trust on the engine here, as we can't evaluate the concrete boolean
-        // return of the return expression
-      } else if (evaluatesToTrue) {
-        // correct semantic
-        // fields are verified and expression returns true
-      } else {
-        // wrong semantic
-        // fields are verified but method is returning false, raise warn
+      if (evaluatesToLiteral && evaluatesToFalse) {
         String message =
             String.format(
                 "The method ensures the %s of the fields, but doesn't return true",
@@ -231,12 +229,7 @@ public void onDataflowVisitReturn(
         raiseError(returnTree, state, message);
       }
     } else {
-      if (evaluatesToFalse) {
-        // correct semantic
-        // fields aren't all verified and expression return false
-      } else {
-        // wrong semantic
-        // fields are not verified, but method returns true
+      if (evaluatesToTrue) {
         fieldNames.removeAll(nonNullFieldsInPath);
         String message =
             String.format(
@@ -277,6 +270,7 @@ private boolean getResultValueFromAnnotation(Symbol.MethodSymbol methodSymbol) {
     }
 
     // Not explicitly declared in the annotation, so we default to true
+    // (This should never happen as the compiler would have caught it before)
     throw new RuntimeException(
         "EnsureNonNullIf requires explicit 'return' value of the method under which the postcondition holds.");
   }
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
index a879653557..85fe0b042c 100644
--- 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
@@ -14,7 +14,7 @@
 
 public class FieldContractUtils {
 
-  public static void validateOverridingRules(
+  public static void ensureStrictPostConditionInheritance(
       String annotName,
       Set overridingFieldNames,
       NullAway analysis,

From 0f71fde279d59c237705f392ece96e2ab601ce00 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Sun, 29 Sep 2024 11:16:15 +0200
Subject: [PATCH 30/52] Handle missing case where allFieldsInPathAreVerified is
 false and evaluatesToLiteral

---
 .../EnsuresNonNullIfHandler.java              | 14 +++---
 .../uber/nullaway/EnsuresNonNullIfTests.java  | 43 +++++++++++--------
 2 files changed, 33 insertions(+), 24 deletions(-)

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
index b632b3b899..52bdfcbd52 100644
--- 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
@@ -205,18 +205,20 @@ public void onDataflowVisitReturn(
      * The decision is as follows:
      *
      * If all fields in the path are verified:
-     * - If the literal boolean evaluates to true, it's correct, as the method
+     * - If the literal boolean evaluates to true, semantics are correct, as the method
      * does return true in case the semantics hold.
-     * - If the literal boolean evaluates to false, it's wrong, as the method
+     * - If the literal boolean evaluates to false, semantics are wrong, as the method
      * incorrect return false when it should have returned true.
      * - If the expression isn't a literal boolean, but something more complex,
-     * we assume it's correct as we trust the data-flow engine.
+     * we assume semantics are correct as we trust the data-flow engine.
      *
      * If fields in path aren't verified:
-     * - If the literal boolean evaluates to false, it's correct, as the method
+     * - If the literal boolean evaluates to false, semantics are correct, as the method
      * correctly returns false in case the semantics don't hold.
-     * - If the literal boolean evaluates to true, it's wrong, as the method
+     * - If the literal boolean evaluates to true, semantics are wrong, as the method
      * incorrectly returns true when it should have returned false.
+     * - If the expression isn't a literal boolean, then semantics are wrong, as we
+     * assume the data-flow engine is correct.
      *
      * The implementation below doesn't need to go through all the combinations.
      */
@@ -229,7 +231,7 @@ public void onDataflowVisitReturn(
         raiseError(returnTree, state, message);
       }
     } else {
-      if (evaluatesToTrue) {
+      if (evaluatesToTrue || !evaluatesToLiteral) {
         fieldNames.removeAll(nonNullFieldsInPath);
         String message =
             String.format(
diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index 51366595c2..4280b099fc 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -60,7 +60,7 @@ public void correctUse_declarationReversed() {
   }
 
   @Test
-  public void correctUse_2() {
+  public void correctAndIncorrectUse() {
     defaultCompilationHelper
         .addSourceLines(
             "Foo.java",
@@ -249,7 +249,7 @@ public void multipleFieldsInSingleAnnotation() {
   }
 
   @Test
-  public void possibleDeferencedExpression() {
+  public void multipleFieldsInSingleAnnotation_oneNotValidated() {
     defaultCompilationHelper
         .addSourceLines(
             "Foo.java",
@@ -259,20 +259,16 @@ public void possibleDeferencedExpression() {
             "class Foo {",
             "  @Nullable Item nullableItem;",
             "  @Nullable Item nullableItem2;",
-            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
-            "  public boolean hasNullableItem() {",
+            "  @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;",
             "  }",
-            "  @EnsuresNonNullIf(value=\"nullableItem2\", result=true)",
-            "  public boolean hasNullableItem2() {",
-            "    return nullableItem2 != null;",
-            "  }",
             "  public int runOk() {",
-            "    if(!hasNullableItem()) {",
+            "    if(!hasNullableItems()) {",
             "      return 1;",
             "    }",
             "    nullableItem.call();",
-            "    // BUG: Diagnostic contains: dereferenced expression nullableItem2 is @Nullable",
             "    nullableItem2.call();",
             "    return 0;",
             "  }",
@@ -283,7 +279,7 @@ public void possibleDeferencedExpression() {
   }
 
   @Test
-  public void ensuresNonNullMethodUsingThis() {
+  public void possibleDeferencedExpression() {
     defaultCompilationHelper
         .addSourceLines(
             "Foo.java",
@@ -292,14 +288,23 @@ public void ensuresNonNullMethodUsingThis() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class Foo {",
             "  @Nullable Item nullableItem;",
+            "  @Nullable Item nullableItem2;",
             "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
-            "    return this.nullableItem != null;",
+            "    return nullableItem != null;",
             "  }",
-            "  public void runOk() {",
+            "  @EnsuresNonNullIf(value=\"nullableItem2\", result=true)",
+            "  public boolean hasNullableItem2() {",
+            "    return nullableItem2 != null;",
+            "  }",
+            "  public int runOk() {",
             "    if(!hasNullableItem()) {",
-            "      return;" + "    }",
+            "      return 1;",
+            "    }",
             "    nullableItem.call();",
+            "    // BUG: Diagnostic contains: dereferenced expression nullableItem2 is @Nullable",
+            "    nullableItem2.call();",
+            "    return 0;",
             "  }",
             "}")
         .addSourceLines(
@@ -308,7 +313,7 @@ public void ensuresNonNullMethodUsingThis() {
   }
 
   @Test
-  public void possibleDeferencedExpression_nonNullMethodNotCalled() {
+  public void ensuresNonNullMethodUsingThis() {
     defaultCompilationHelper
         .addSourceLines(
             "Foo.java",
@@ -319,10 +324,12 @@ public void possibleDeferencedExpression_nonNullMethodNotCalled() {
             "  @Nullable Item nullableItem;",
             "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
-            "    return nullableItem != null;",
+            "    return this.nullableItem != null;",
             "  }",
-            "  public void runNOk() {",
-            "    // BUG: Diagnostic contains: dereferenced expression nullableItem",
+            "  public void runOk() {",
+            "    if(!hasNullableItem()) {",
+            "      return;",
+            "    }",
             "    nullableItem.call();",
             "  }",
             "}")

From 880ae4272040e7ab3fa8689b26d9a7b427d95da0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Sun, 29 Sep 2024 11:16:54 +0200
Subject: [PATCH 31/52] nit comment

---
 .../contract/fieldcontract/EnsuresNonNullIfHandler.java         | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
index 52bdfcbd52..ad41f67eef 100644
--- 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
@@ -220,7 +220,7 @@ public void onDataflowVisitReturn(
      * - If the expression isn't a literal boolean, then semantics are wrong, as we
      * assume the data-flow engine is correct.
      *
-     * The implementation below doesn't need to go through all the combinations.
+     * The implementation below is an optimized version of the decision table above.
      */
     if (allFieldsInPathAreVerified) {
       if (evaluatesToLiteral && evaluatesToFalse) {

From f478ac42289844b8fa5d0e2d9506fd5ab346e6d0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Sun, 29 Sep 2024 12:04:31 +0200
Subject: [PATCH 32/52] one more test

---
 .../uber/nullaway/EnsuresNonNullIfTests.java  | 28 +++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index 4280b099fc..c345125386 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -513,6 +513,34 @@ public void semanticIssues_doesntEnsureNonNullabilityOfFields() {
         .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 semanticIssues_methodDeclarationReversed() {
     defaultCompilationHelper

From d53958b261430875f3a04b816d693869d6efd3b0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Sun, 29 Sep 2024 12:06:17 +0200
Subject: [PATCH 33/52] one more test

---
 .../uber/nullaway/EnsuresNonNullIfTests.java  | 28 +++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index c345125386..7de6166e19 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -513,6 +513,34 @@ public void semanticIssues_doesntEnsureNonNullabilityOfFields() {
         .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() {",
+            "    // 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

From 13b0cca5477b1feb5a9d5b94e95a1aa6e74ace45 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Sun, 29 Sep 2024 12:26:56 +0200
Subject: [PATCH 34/52] FIX typo name of the test

---
 .../src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index 7de6166e19..b70a491154 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -514,7 +514,7 @@ public void semanticIssues_doesntEnsureNonNullabilityOfFields() {
   }
 
   @Test
-  public void noSemanticIssue_combinationOfExpressionAndLiteralBoolean() {
+  public void semanticIssue_combinationOfExpressionAndLiteralBoolean() {
     defaultCompilationHelper
         .addSourceLines(
             "Foo.java",

From 5d8157d8ad2019744eafb38ef7d5a018d1322bdd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Sun, 29 Sep 2024 12:27:09 +0200
Subject: [PATCH 35/52] FIX typo name of the test

---
 .../src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index b70a491154..b56d6c4fa8 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -514,7 +514,7 @@ public void semanticIssues_doesntEnsureNonNullabilityOfFields() {
   }
 
   @Test
-  public void semanticIssue_combinationOfExpressionAndLiteralBoolean() {
+  public void semanticIssue_combinationOfExpressionAndLiteralBoolean_2() {
     defaultCompilationHelper
         .addSourceLines(
             "Foo.java",

From 2623bfa438e891b0ab3a7c65b351c19843286b42 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Sun, 29 Sep 2024 12:28:16 +0200
Subject: [PATCH 36/52] one more test

---
 .../uber/nullaway/EnsuresNonNullIfTests.java  | 27 +++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index b56d6c4fa8..efc81f5feb 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -569,6 +569,33 @@ public void semanticIssue_combinationOfExpressionAndLiteralBoolean() {
         .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

From 1b1967c089d99fd41e7b0893233265c871599fb0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Sun, 29 Sep 2024 18:11:08 +0200
Subject: [PATCH 37/52] Fix nullaway issues in nullaway

---
 .../fieldcontract/EnsuresNonNullIfHandler.java        | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

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
index ad41f67eef..d26fee8e90 100644
--- 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
@@ -170,7 +170,8 @@ public void onDataflowVisitReturn(
 
     // Get the declared configuration of the EnsureNonNullIf method under analysis
     Symbol.MethodSymbol methodSymbolUnderAnalysis =
-        methodAnalysisContextUnderAnalysis.methodSymbol();
+        NullabilityUtil.castToNonNull(methodAnalysisContextUnderAnalysis).methodSymbol();
+
     Set fieldNames = getAnnotationValueArray(methodSymbolUnderAnalysis, annotName, false);
     if (fieldNames == null) {
       throw new RuntimeException("List of field names shouldn't be null");
@@ -197,8 +198,8 @@ public void onDataflowVisitReturn(
     }
 
     boolean evaluatesToLiteral = expressionAsBoolean.isPresent();
-    boolean evaluatesToFalse = evaluatesToLiteral && !expressionAsBoolean.get();
-    boolean evaluatesToTrue = evaluatesToLiteral && expressionAsBoolean.get();
+    boolean evaluatesToFalse = expressionAsBoolean.isPresent() && !expressionAsBoolean.get();
+    boolean evaluatesToTrue = expressionAsBoolean.isPresent() && expressionAsBoolean.get();
 
     /*
      * Decide whether the semantics of this ReturnTree are correct.
@@ -243,7 +244,9 @@ public void onDataflowVisitReturn(
   }
 
   private void raiseError(Tree returnTree, VisitorState state, String message) {
-    NullAway analysis = methodAnalysisContextUnderAnalysis.analysis();
+    NullAway analysis =
+        NullabilityUtil.castToNonNull(methodAnalysisContextUnderAnalysis).analysis();
+
     state.reportMatch(
         analysis
             .getErrorBuilder()

From 80ef2ca79c234858b4d7a8a35c878bb7b157b807 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Mon, 30 Sep 2024 07:00:52 +0200
Subject: [PATCH 38/52] JSpecify annotation

---
 .../contract/fieldcontract/EnsuresNonNullIfHandler.java         | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
index d26fee8e90..38e715f13b 100644
--- 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
@@ -49,12 +49,12 @@
 import java.util.Optional;
 import java.util.Set;
 import java.util.stream.Collectors;
-import javax.annotation.Nullable;
 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

From 54286028fa0720fae51d1e4a4e20ee1c4d0be0d5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Mon, 30 Sep 2024 07:02:41 +0200
Subject: [PATCH 39/52] small refactoring; fix compilation

---
 .../fieldcontract/EnsuresNonNullIfHandler.java        | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

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
index 38e715f13b..62262a1bd6 100644
--- 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
@@ -70,8 +70,8 @@ public class EnsuresNonNullIfHandler extends AbstractFieldContractHandler {
   // The MethodTree and MethodAnalysisContext of the EnsureNonNullIf method
   // under current semantic validation
   // They are set to null when no methods are being validated.
-  @Nullable private MethodTree methodTreeUnderAnalysis;
-  @Nullable private MethodAnalysisContext methodAnalysisContextUnderAnalysis;
+  private @Nullable MethodTree methodTreeUnderAnalysis;
+  private @Nullable MethodAnalysisContext methodAnalysisContextUnderAnalysis;
 
   public EnsuresNonNullIfHandler() {
     super("EnsuresNonNullIf");
@@ -133,12 +133,9 @@ public Void visitReturn(ReturnTree node, Void unused) {
         }
 
         // We only add returns that are directly in the method under analysis
-        if (!enclosingMethod.getLeaf().equals(methodTreeUnderAnalysis)) {
-          return super.visitReturn(node, null);
+        if (enclosingMethod.getLeaf().equals(methodTreeUnderAnalysis)) {
+          returnTreesInMethodUnderAnalysis.add(node);
         }
-
-        // We add the current return tree to the set as it's in the method
-        returnTreesInMethodUnderAnalysis.add(node);
         return super.visitReturn(node, null);
       }
     }.scan(methodState.getPath(), null);

From ca7a54a05dde4be1314d30ca086ee88be9bab090 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Mon, 30 Sep 2024 08:26:47 +0200
Subject: [PATCH 40/52] Use elseStore when result is set to false

---
 .../fieldcontract/EnsuresNonNullIfHandler.java    | 14 ++++++++------
 .../com/uber/nullaway/EnsuresNonNullIfTests.java  | 15 +++++++++------
 2 files changed, 17 insertions(+), 12 deletions(-)

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
index 62262a1bd6..5b2273cffc 100644
--- 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
@@ -176,14 +176,16 @@ public void onDataflowVisitReturn(
 
     boolean trueIfNonNull = getResultValueFromAnnotation(methodSymbolUnderAnalysis);
 
-    // We extract all the data-flow of the fields found by the
-    // engine in the "then" case (i.e., true case)
-    // and check whether all fields in the annotation parameter are non-null
+    // 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 =
-        thenStore.getReceiverFields(trueIfNonNull ? Nullness.NONNULL : Nullness.NULL).stream()
+        chosenStore.getNonNullReceiverFields().stream()
             .map(e -> e.getSimpleName().toString())
             .collect(Collectors.toSet());
-    boolean allFieldsInPathAreVerified = nonNullFieldsInPath.containsAll(fieldNames);
+    boolean allFieldsAreNonNull = nonNullFieldsInPath.containsAll(fieldNames);
 
     // Whether the return true expression evaluates to a boolean literal or not.
     Optional expressionAsBoolean = Optional.empty();
@@ -220,7 +222,7 @@ public void onDataflowVisitReturn(
      *
      * The implementation below is an optimized version of the decision table above.
      */
-    if (allFieldsInPathAreVerified) {
+    if (allFieldsAreNonNull) {
       if (evaluatesToLiteral && evaluatesToFalse) {
         String message =
             String.format(
diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index efc81f5feb..2c305cbd69 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -390,8 +390,9 @@ public void postConditions_Inheritance() {
         .doTest();
   }
 
+  /** Tests related to setting return=false */
   @Test
-  public void setTrueIfNonNullToFalse() {
+  public void setResultToFalse() {
     defaultCompilationHelper
         .addSourceLines(
             "Foo.java",
@@ -418,7 +419,7 @@ public void setTrueIfNonNullToFalse() {
   }
 
   @Test
-  public void setTrueIfNonNullToFalseMultipleElements() {
+  public void setResultToFalse_MultipleElements_wrongSemantics_1() {
     defaultCompilationHelper
         .addSourceLines(
             "Foo.java",
@@ -430,6 +431,8 @@ public void setTrueIfNonNullToFalseMultipleElements() {
             "  @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() {",
@@ -447,7 +450,7 @@ public void setTrueIfNonNullToFalseMultipleElements() {
   }
 
   @Test
-  public void setTrueIfNonNullToFalseMultipleElements_deferenceFound() {
+  public void setTrueIfNonNullToFalseMultipleElements_correctSemantics_deferenceFound() {
     defaultCompilationHelper
         .addSourceLines(
             "Foo.java",
@@ -458,12 +461,12 @@ public void setTrueIfNonNullToFalseMultipleElements_deferenceFound() {
             "  @Nullable Item nullableItem;",
             "  @Nullable Item nullableItem2;",
             "  @EnsuresNonNullIf(value={\"nullableItem\",\"nullableItem2\"}, result=false)",
-            "  public boolean doesNotHaveNullableItem() {",
-            "    // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem, nullableItem2]",
+            "  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(doesNotHaveNullableItem()) {",
+            "    if(nullableItemsAreNull()) {",
             "      return 1;",
             "    }",
             "    nullableItem.call();",

From bb139dfa525daf9bdd070aea4cdc9f7589339583 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Mon, 30 Sep 2024 08:28:59 +0200
Subject: [PATCH 41/52] Set return default value to true again

---
 .../com/uber/nullaway/annotations/EnsuresNonNullIf.java  | 9 +++++----
 .../contract/fieldcontract/EnsuresNonNullIfHandler.java  | 6 ++----
 .../java/com/uber/nullaway/EnsuresNonNullIfTests.java    | 2 +-
 3 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java
index 53086523fe..b42842ddbe 100644
--- a/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java
+++ b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java
@@ -8,8 +8,8 @@
 /**
  * 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 true in case the fields
- * are null (inverse logic), and in such case, you must set {@code result} to false. NullAway
+ * 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:
@@ -45,9 +45,10 @@
   String[] value();
 
   /**
-   * The return value of the method under which the postcondition holds.
+   * 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();
+  boolean result() default true;
 }
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
index 5b2273cffc..da1690cf6b 100644
--- 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
@@ -273,10 +273,8 @@ private boolean getResultValueFromAnnotation(Symbol.MethodSymbol methodSymbol) {
       }
     }
 
-    // Not explicitly declared in the annotation, so we default to true
-    // (This should never happen as the compiler would have caught it before)
-    throw new RuntimeException(
-        "EnsureNonNullIf requires explicit 'return' value of the method under which the postcondition holds.");
+    // Default value of the 'result' field is true
+    return true;
   }
 
   /**
diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index 2c305cbd69..1211ae93eb 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -15,7 +15,7 @@ public void correctUse() {
             "import com.uber.nullaway.annotations.EnsuresNonNullIf;",
             "class Foo {",
             "  @Nullable Item nullableItem;",
-            "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
+            "  @EnsuresNonNullIf(\"nullableItem\")",
             "  public boolean hasNullableItem() {",
             "    return nullableItem != null;",
             "  }",

From f23a8d427a5824526fa3ecbfdf318cc68ec3dd80 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Mon, 30 Sep 2024 08:34:06 +0200
Subject: [PATCH 42/52] Improve tests

---
 .../uber/nullaway/EnsuresNonNullIfTests.java  | 35 +++++++++++++++++--
 1 file changed, 32 insertions(+), 3 deletions(-)

diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index 1211ae93eb..0a319b123b 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -419,7 +419,7 @@ public void setResultToFalse() {
   }
 
   @Test
-  public void setResultToFalse_MultipleElements_wrongSemantics_1() {
+  public void setResultToFalse_multipleElements_wrongSemantics_1() {
     defaultCompilationHelper
         .addSourceLines(
             "Foo.java",
@@ -450,7 +450,7 @@ public void setResultToFalse_MultipleElements_wrongSemantics_1() {
   }
 
   @Test
-  public void setTrueIfNonNullToFalseMultipleElements_correctSemantics_deferenceFound() {
+  public void setResultToFalse_multipleElements_correctSemantics() {
     defaultCompilationHelper
         .addSourceLines(
             "Foo.java",
@@ -479,6 +479,35 @@ public void setTrueIfNonNullToFalseMultipleElements_correctSemantics_deferenceFo
         .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
    ********************************************************
@@ -664,7 +693,7 @@ public void semanticIssues_ignoreLambdaReturns() {
   }
 
   @Test
-  public void semanticIssues_2() {
+  public void semanticIssues_hardCodedReturnTrue() {
     defaultCompilationHelper
         .addSourceLines(
             "Foo.java",

From 45907e1040b72a62736ff3433c99713bf37a7d53 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Mon, 30 Sep 2024 08:38:18 +0200
Subject: [PATCH 43/52] test for error message when result=false

---
 .../uber/nullaway/EnsuresNonNullIfTests.java  | 33 +++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index 0a319b123b..24bb3b8cfa 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -545,6 +545,39 @@ public void semanticIssues_doesntEnsureNonNullabilityOfFields() {
         .doTest();
   }
 
+  @Test
+  public void semanticIssues_doesntEnsureNonNullabilityOfFields_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) {",
+            "      // BUG: Diagnostic contains: The method ensures the nullability of the fields, but doesn't return true",
+            "      return false;",
+            "    } else {",
+            "      // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]",
+            "      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

From 7a3d075ac8a8d3121e56b3906e2abbfc6f3a9312 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Mon, 30 Sep 2024 08:51:48 +0200
Subject: [PATCH 44/52] Return true in case body is null just like existing
 EnsureNonNull handler

---
 .../contract/fieldcontract/EnsuresNonNullIfHandler.java         | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
index da1690cf6b..117326ebde 100644
--- 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
@@ -85,7 +85,7 @@ public EnsuresNonNullIfHandler() {
   protected boolean validateAnnotationSemantics(
       MethodTree tree, MethodAnalysisContext methodAnalysisContext) {
     if (tree.getBody() == null) {
-      return false;
+      return true;
     }
 
     // clean up state variables, as we are visiting a new annotated method

From 3c7295e65bc5d234d1f8cacf3447b03299a9d1f6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Mon, 30 Sep 2024 09:49:25 +0200
Subject: [PATCH 45/52] simplify error message

---
 .../contract/fieldcontract/EnsuresNonNullIfHandler.java  | 9 ++++-----
 .../java/com/uber/nullaway/EnsuresNonNullIfTests.java    | 6 +++---
 2 files changed, 7 insertions(+), 8 deletions(-)

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
index 117326ebde..e7c2427980 100644
--- 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
@@ -224,11 +224,10 @@ public void onDataflowVisitReturn(
      */
     if (allFieldsAreNonNull) {
       if (evaluatesToLiteral && evaluatesToFalse) {
-        String message =
-            String.format(
-                "The method ensures the %s of the fields, but doesn't return true",
-                (trueIfNonNull ? "non-nullability" : "nullability"));
-        raiseError(returnTree, state, message);
+        raiseError(
+            returnTree,
+            state,
+            "The method ensures the non-nullability of the fields, but returns incorrectly");
       }
     } else {
       if (evaluatesToTrue || !evaluatesToLiteral) {
diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index 24bb3b8cfa..9936b363a1 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -525,7 +525,7 @@ public void semanticIssues_doesntEnsureNonNullabilityOfFields() {
             "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    if(nullableItem != null) {",
-            "      // BUG: Diagnostic contains: The method ensures the non-nullability of the fields, but doesn't return true",
+            "      // BUG: Diagnostic contains: The method ensures the non-nullability of the fields, but returns incorrectly",
             "      return false;",
             "    } else {",
             "      // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]",
@@ -558,7 +558,7 @@ public void semanticIssues_doesntEnsureNonNullabilityOfFields_resultFalse() {
             "  @EnsuresNonNullIf(value=\"nullableItem\", result=false)",
             "  public boolean doesNotHaveNullableItem() {",
             "    if(nullableItem != null) {",
-            "      // BUG: Diagnostic contains: The method ensures the nullability of the fields, but doesn't return true",
+            "      // BUG: Diagnostic contains: The method ensures the non-nullability of the fields, but returns incorrectly",
             "      return false;",
             "    } else {",
             "      // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]",
@@ -681,7 +681,7 @@ public void semanticIssues_methodDeclarationReversed() {
             "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    if(nullableItem != null) {",
-            "      // BUG: Diagnostic contains: The method ensures the non-nullability of the fields, but doesn't return true",
+            "      // BUG: Diagnostic contains: The method ensures the non-nullability of the fields, but returns incorrectly",
             "      return false;",
             "    } else {",
             "      // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]",

From 2bbbac267987a21cfc9208817c5bee18a9753408 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Mon, 30 Sep 2024 17:00:29 +0200
Subject: [PATCH 46/52] Broken test

---
 .../uber/nullaway/EnsuresNonNullIfTests.java  | 34 +++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index 9936b363a1..51a524e0be 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -479,6 +479,40 @@ public void setResultToFalse_multipleElements_correctSemantics() {
         .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

From ea10969dee15839866950c2e4e6d880b79491c86 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Mon, 30 Sep 2024 17:48:31 +0200
Subject: [PATCH 47/52] Fix issue when return=false and method returns boolean

---
 .../EnsuresNonNullIfHandler.java              | 31 +++++++++++--------
 .../uber/nullaway/EnsuresNonNullIfTests.java  |  4 +--
 2 files changed, 19 insertions(+), 16 deletions(-)

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
index e7c2427980..fc2e7ad4ee 100644
--- 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
@@ -196,41 +196,46 @@ public void onDataflowVisitReturn(
       }
     }
 
-    boolean evaluatesToLiteral = expressionAsBoolean.isPresent();
-    boolean evaluatesToFalse = expressionAsBoolean.isPresent() && !expressionAsBoolean.get();
-    boolean evaluatesToTrue = expressionAsBoolean.isPresent() && expressionAsBoolean.get();
+    /*
+     * 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.isPresent();
+    boolean evaluatesToNonNullLiteral =
+        expressionAsBoolean.isPresent() && (trueIfNonNull == expressionAsBoolean.get());
 
     /*
      * Decide whether the semantics of this ReturnTree are correct.
      * The decision is as follows:
      *
      * If all fields in the path are verified:
-     * - If the literal boolean evaluates to true, semantics are correct, as the method
-     * does return true in case the semantics hold.
-     * - If the literal boolean evaluates to false, semantics are wrong, as the method
-     * incorrect return false when it should have returned true.
+     * - If the literal boolean is equals to the configured non-null boolean, semantics are correct,
+     * as the method does return correctly in case the semantics hold.
+     * - If the literal boolean isn't equals to the configured non-null boolean, semantics are wrong,
+     * as the method incorrectly returns when it should have returned true.
      * - If the expression isn't a literal boolean, but something more complex,
      * we assume semantics are correct as we trust the data-flow engine.
      *
      * If fields in path aren't verified:
-     * - If the literal boolean evaluates to false, semantics are correct, as the method
-     * correctly returns false in case the semantics don't hold.
-     * - If the literal boolean evaluates to true, semantics are wrong, as the method
-     * incorrectly returns true when it should have returned false.
+     * - 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 the data-flow engine is correct.
      *
      * The implementation below is an optimized version of the decision table above.
      */
     if (allFieldsAreNonNull) {
-      if (evaluatesToLiteral && evaluatesToFalse) {
+      if (isBooleanLiteral && !evaluatesToNonNullLiteral) {
         raiseError(
             returnTree,
             state,
             "The method ensures the non-nullability of the fields, but returns incorrectly");
       }
     } else {
-      if (evaluatesToTrue || !evaluatesToLiteral) {
+      if (evaluatesToNonNullLiteral || !isBooleanLiteral) {
         fieldNames.removeAll(nonNullFieldsInPath);
         String message =
             String.format(
diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index 51a524e0be..562b1742e9 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -580,7 +580,7 @@ public void semanticIssues_doesntEnsureNonNullabilityOfFields() {
   }
 
   @Test
-  public void semanticIssues_doesntEnsureNonNullabilityOfFields_resultFalse() {
+  public void noSemanticIssues_resultFalse() {
     defaultCompilationHelper
         .addSourceLines(
             "Foo.java",
@@ -592,10 +592,8 @@ public void semanticIssues_doesntEnsureNonNullabilityOfFields_resultFalse() {
             "  @EnsuresNonNullIf(value=\"nullableItem\", result=false)",
             "  public boolean doesNotHaveNullableItem() {",
             "    if(nullableItem != null) {",
-            "      // BUG: Diagnostic contains: The method ensures the non-nullability of the fields, but returns incorrectly",
             "      return false;",
             "    } else {",
-            "      // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]",
             "      return true;",
             "    }",
             "  }",

From 3cb7d51c1d42555d3b3e409c7ce60cd8141aee23 Mon Sep 17 00:00:00 2001
From: Manu Sridharan 
Date: Mon, 30 Sep 2024 10:19:56 -0700
Subject: [PATCH 48/52] Let's not use an Optional here.  Since we check the
 code with NullAway, using null should be fine

---
 .../fieldcontract/EnsuresNonNullIfHandler.java       | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

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
index fc2e7ad4ee..e1e6aa7506 100644
--- 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
@@ -46,7 +46,6 @@
 import com.uber.nullaway.handlers.contract.ContractUtils;
 import java.util.HashSet;
 import java.util.Map;
-import java.util.Optional;
 import java.util.Set;
 import java.util.stream.Collectors;
 import javax.lang.model.element.AnnotationMirror;
@@ -187,12 +186,13 @@ public void onDataflowVisitReturn(
             .collect(Collectors.toSet());
     boolean allFieldsAreNonNull = nonNullFieldsInPath.containsAll(fieldNames);
 
-    // Whether the return true expression evaluates to a boolean literal or not.
-    Optional expressionAsBoolean = Optional.empty();
+    // 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 = Optional.of((boolean) expressionAsLiteral.getValue());
+        expressionAsBoolean = (Boolean) expressionAsLiteral.getValue();
       }
     }
 
@@ -202,9 +202,9 @@ public void onDataflowVisitReturn(
      * - 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.isPresent();
+    boolean isBooleanLiteral = expressionAsBoolean != null;
     boolean evaluatesToNonNullLiteral =
-        expressionAsBoolean.isPresent() && (trueIfNonNull == expressionAsBoolean.get());
+        expressionAsBoolean != null && (trueIfNonNull == expressionAsBoolean);
 
     /*
      * Decide whether the semantics of this ReturnTree are correct.

From 56a0984a935cc89a0dd7819590afe6c7f4bd481e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maur=C3=ADcio=20Aniche?= 
Date: Mon, 30 Sep 2024 19:57:25 +0200
Subject: [PATCH 49/52] No need to report when all paths are verified but
 return is wrong

---
 .../fieldcontract/EnsuresNonNullIfHandler.java | 18 ++----------------
 .../uber/nullaway/EnsuresNonNullIfTests.java   |  2 --
 2 files changed, 2 insertions(+), 18 deletions(-)

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
index e1e6aa7506..aad81b9aa0 100644
--- 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
@@ -211,12 +211,7 @@ public void onDataflowVisitReturn(
      * The decision is as follows:
      *
      * If all fields in the path are verified:
-     * - If the literal boolean is equals to the configured non-null boolean, semantics are correct,
-     * as the method does return correctly in case the semantics hold.
-     * - If the literal boolean isn't equals to the configured non-null boolean, semantics are wrong,
-     * as the method incorrectly returns when it should have returned true.
-     * - If the expression isn't a literal boolean, but something more complex,
-     * we assume semantics are correct as we trust the data-flow engine.
+     * - Semantics are valid
      *
      * If fields in path aren't verified:
      * - If the literal boolean is the opposite of the configured non-null boolean, semantics
@@ -224,17 +219,8 @@ public void onDataflowVisitReturn(
      * - Otherwise, semantics are wrong, as the method incorrectly returns.
      * - If the expression isn't a literal boolean, then semantics are wrong, as we
      * assume the data-flow engine is correct.
-     *
-     * The implementation below is an optimized version of the decision table above.
      */
-    if (allFieldsAreNonNull) {
-      if (isBooleanLiteral && !evaluatesToNonNullLiteral) {
-        raiseError(
-            returnTree,
-            state,
-            "The method ensures the non-nullability of the fields, but returns incorrectly");
-      }
-    } else {
+    if (!allFieldsAreNonNull) {
       if (evaluatesToNonNullLiteral || !isBooleanLiteral) {
         fieldNames.removeAll(nonNullFieldsInPath);
         String message =
diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
index 562b1742e9..ea7655f720 100644
--- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
+++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java
@@ -559,7 +559,6 @@ public void semanticIssues_doesntEnsureNonNullabilityOfFields() {
             "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    if(nullableItem != null) {",
-            "      // BUG: Diagnostic contains: The method ensures the non-nullability of the fields, but returns incorrectly",
             "      return false;",
             "    } else {",
             "      // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]",
@@ -713,7 +712,6 @@ public void semanticIssues_methodDeclarationReversed() {
             "  @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
             "  public boolean hasNullableItem() {",
             "    if(nullableItem != null) {",
-            "      // BUG: Diagnostic contains: The method ensures the non-nullability of the fields, but returns incorrectly",
             "      return false;",
             "    } else {",
             "      // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNullIf but does not ensure fields [nullableItem]",

From f98fb3caa183ea78d19e39643f20758c2aebdab4 Mon Sep 17 00:00:00 2001
From: Manu Sridharan 
Date: Mon, 30 Sep 2024 15:16:41 -0700
Subject: [PATCH 50/52] minor comment tweak

---
 .../contract/fieldcontract/EnsuresNonNullIfHandler.java         | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
index aad81b9aa0..9a4421631c 100644
--- 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
@@ -218,7 +218,7 @@ public void onDataflowVisitReturn(
      * 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 the data-flow engine is correct.
+     * assume it is possible that the configured non-null boolean can be returned.
      */
     if (!allFieldsAreNonNull) {
       if (evaluatesToNonNullLiteral || !isBooleanLiteral) {

From fa7728e140e0557b327cd86961be7f3a8d9ae37f Mon Sep 17 00:00:00 2001
From: Manu Sridharan 
Date: Mon, 30 Sep 2024 15:23:29 -0700
Subject: [PATCH 51/52] simplify dataflow update logic

---
 .../fieldcontract/EnsuresNonNullIfHandler.java      | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

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
index 9a4421631c..b4b116c545 100644
--- 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
@@ -289,8 +289,12 @@ public NullnessHint onDataflowVisitMethodInvocation(
 
     Set fieldNames = getAnnotationValueArray(methodSymbol, annotName, false);
     if (fieldNames != null) {
-      boolean trueIfNonNull = getResultValueFromAnnotation(methodSymbol);
       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(
@@ -306,11 +310,10 @@ public NullnessHint onDataflowVisitMethodInvocation(
           continue;
         }
 
-        // The call to the EnsuresNonNullIf method ensures that the field is then not null
-        // (or null, depending on the result flag) at this point.
+        // 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.
-        thenUpdates.set(accessPath, trueIfNonNull ? Nullness.NONNULL : Nullness.NULL);
-        elseUpdates.set(accessPath, trueIfNonNull ? Nullness.NULL : Nullness.NONNULL);
+        chosenUpdates.set(accessPath, Nullness.NONNULL);
       }
     }
 

From 1c5610cbdb6188420c5f06673624179b02e8c5d8 Mon Sep 17 00:00:00 2001
From: Manu Sridharan 
Date: Mon, 30 Sep 2024 15:27:54 -0700
Subject: [PATCH 52/52] comments

---
 .../fieldcontract/FieldContractUtils.java     | 32 +++++++++++++++++++
 1 file changed, 32 insertions(+)

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
index 85fe0b042c..ea25480aca 100644
--- 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
@@ -1,3 +1,24 @@
+/*
+ * 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;
@@ -14,6 +35,17 @@
 
 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,