Expose @EnsuresNonNull and @RequiresNonNull in annotations package (#999

)

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:
+ *
+ * <pre>
+ * 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();
+ *     }
+ * }
+ * </pre>
+ */
+@Retention(RetentionPolicy.CLASS)
+@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+public @interface EnsuresNonNull {
+  String[] value();
+}

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:
+ *
+ * <pre>
+ * 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();
+ *     }
+ * }
+ * </pre>
+ */
+@Retention(RetentionPolicy.CLASS)
+@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+public @interface RequiresNonNull {
+  String[] value();
+}

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

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

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