diff --git a/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNull.java b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNull.java new file mode 100644 index 0000000000..f8a19e1eeb --- /dev/null +++ b/annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNull.java @@ -0,0 +1,34 @@ +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 whenever the + * method exits normally, the fields listed in the annotation are non-null. NullAway verifies that + * this property holds, and the property is used when checking call sites of the method. Here is an + * example: + * + *
+ * class Foo {
+ *     {@literal @}Nullable Object theField;
+ *     {@literal @}EnsuresNonNull("theField") // @EnsuresNonNull("this.theField") is also valid
+ *     void foo() {
+ *         theField = new Object();
+ *     }
+ *     void bar() {
+ *         foo();
+ *         // No error, NullAway knows theField is non-null after call to foo()
+ *         theField.toString();
+ *     }
+ * }
+ * 
+ */ +@Retention(RetentionPolicy.CLASS) +@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) +public @interface EnsuresNonNull { + String[] value(); +} diff --git a/annotations/src/main/java/com/uber/nullaway/annotations/RequiresNonNull.java b/annotations/src/main/java/com/uber/nullaway/annotations/RequiresNonNull.java new file mode 100644 index 0000000000..5398bcac59 --- /dev/null +++ b/annotations/src/main/java/com/uber/nullaway/annotations/RequiresNonNull.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 pre-condition for an instance method. Each parameter to + * the annotation should be a field of the enclosing class. Each call site of the method must ensure + * that the fields listed in the annotation are non-null before the call. NullAway verifies that + * this property holds, and uses the property when checking the body of the method. Here is an + * example: + * + *
+ * class Foo {
+ *     {@literal @}Nullable Object theField;
+ *     {@literal @}RequiresNonNull("theField") // @RequiresNonNull("this.theField") is also valid
+ *     void foo() {
+ *         // No error, NullAway knows theField is non-null after foo()
+ *         theField.toString();
+ *     }
+ *     void bar() {
+ *         // Error, theField may be null before the call to foo()
+ *         foo();
+ *         this.theField = new Object();
+ *         // No error
+ *         foo();
+ *     }
+ * }
+ * 
+ */ +@Retention(RetentionPolicy.CLASS) +@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) +public @interface RequiresNonNull { + String[] value(); +} diff --git a/nullaway/src/main/java/com/uber/nullaway/annotations/EnsuresNonNull.java b/nullaway/src/main/java/com/uber/nullaway/annotations/EnsuresNonNull.java deleted file mode 100644 index efb2ad79f5..0000000000 --- a/nullaway/src/main/java/com/uber/nullaway/annotations/EnsuresNonNull.java +++ /dev/null @@ -1,19 +0,0 @@ -package com.uber.nullaway.annotations; - -import java.lang.annotation.ElementType; -import java.lang.annotation.Retention; -import java.lang.annotation.RetentionPolicy; -import java.lang.annotation.Target; - -/** - * Can annotate a methods with @EnsuresNonnull(param) annotation where param is one of the classes - * fields. It indicates a post-condition for the method, that at every call site to this method, the - * class field in the argument is @Nonnull at exit point. If a method is annotated - * with @EnsuresNonnull(param), NullAway checks weather the @Nonnull assumption of the field at exit - * point is valid. - */ -@Retention(RetentionPolicy.CLASS) -@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) -public @interface EnsuresNonNull { - String[] value(); -} diff --git a/nullaway/src/main/java/com/uber/nullaway/annotations/RequiresNonNull.java b/nullaway/src/main/java/com/uber/nullaway/annotations/RequiresNonNull.java deleted file mode 100644 index f5f58e6090..0000000000 --- a/nullaway/src/main/java/com/uber/nullaway/annotations/RequiresNonNull.java +++ /dev/null @@ -1,19 +0,0 @@ -package com.uber.nullaway.annotations; - -import java.lang.annotation.ElementType; -import java.lang.annotation.Retention; -import java.lang.annotation.RetentionPolicy; -import java.lang.annotation.Target; - -/** - * Can annotate a methods with @RequiresNonnull(param) annotation where param is one of the classes - * fields. It indicates a pre-condition for the method, that at every call site to this method, the - * class field in the argument must be @Nonnull. If a method is annotated - * with @RequiresNonnull(param), NullAway dataflow analysis is going to assume that the filed with - * name param, is @Nonnull at the start point. - */ -@Retention(RetentionPolicy.CLASS) -@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) -public @interface RequiresNonNull { - String[] value(); -} 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 106abd949e..62cde6a7e1 100644 --- a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullHandler.java +++ b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullHandler.java @@ -95,12 +95,9 @@ protected boolean validateAnnotationSemantics( if (!isValidLocalPostCondition) { fieldNames.removeAll(nonnullFieldsOfReceiverAtExit); message = - "method: " - + methodSymbol - + " is annotated with @EnsuresNonNull annotation, it indicates that all fields in the annotation parameter" - + " must be guaranteed to be nonnull at exit point. However, the method's body fails to ensure this for the following fields: " - + fieldNames; - + String.format( + "Method is annotated with @EnsuresNonNull but fails to ensure the following fields are non-null at exit: %s", + fieldNames); state.reportMatch( analysis .getErrorBuilder() 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 113318ef3f..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 @@ -157,7 +157,10 @@ public void onMatchMethodInvocation( .getNullnessOfFieldForReceiverTree( state.getPath(), state.context, methodSelectTree, field, true); if (NullabilityUtil.nullnessToBool(nullness)) { - String message = "Expected field " + fieldName + " to be non-null at call site"; + String message = + "Expected field " + + fieldName + + " to be non-null at call site due to @RequiresNonNull annotation on invoked method"; state.reportMatch( analysis diff --git a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullTests.java b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullTests.java index dd94e36a5d..a61069446c 100644 --- a/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullTests.java +++ b/nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullTests.java @@ -149,7 +149,7 @@ public void ensuresNonNullInterpretation() { " nullItem = new Item();", " }", " @EnsuresNonNull(\"nullItem\")", - " // BUG: Diagnostic contains: test2() is annotated with @EnsuresNonNull annotation, it indicates that all fields in the annotation parameter must be guaranteed to be nonnull at exit point. However, the method's body fails to ensure this for the following fields: [nullItem]", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNull but fails to ensure the following fields are non-null at exit: [nullItem]", " public void test2() {", " }", " @EnsuresNonNull(\"this.nullItem\")", @@ -162,7 +162,7 @@ public void ensuresNonNullInterpretation() { " nullItem = new Item();", " }", " @EnsuresNonNull(\"nullItem\")", - " // BUG: Diagnostic contains: method: test5() is annotated with @EnsuresNonNull annotation, it indicates that all fields in the annotation parameter must be guaranteed to be nonnull at exit point. However, the method's body fails to ensure this for the following fields: [nullItem]", + " // BUG: Diagnostic contains: Method is annotated with @EnsuresNonNull but fails to ensure the following fields are non-null at exit: [nullItem]", " public void test5() {", " this.foo.test1();", " }",