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