Add method pre- and postcondition using @RequiresNonnull/@EnsuresNonn…

…ull (#423)

Co-authored-by: Manu Sridharan <[email protected]>

.gitignore

@@ -105,6 +105,3 @@ tmp/
 
 # TeXlipse plugin
 .texlipse
-
-# kotlin
-annotations/

nullaway/src/main/java/com/uber/nullaway/ErrorMessage.java

@@ -47,6 +47,10 @@ public enum MessageTypes {
     ANNOTATION_VALUE_INVALID,
     CAST_TO_NONNULL_ARG_NONNULL,
     GET_ON_EMPTY_OPTIONAL,
-    SWITCH_EXPRESSION_NULLABLE
+    SWITCH_EXPRESSION_NULLABLE,
+    POSTCONDITION_NOT_SATISFIED,
+    PRECONDITION_NOT_SATISFIED,
+    WRONG_OVERRIDE_POSTCONDITION,
+    WRONG_OVERRIDE_PRECONDITION,
   }
 }

nullaway/src/main/java/com/uber/nullaway/NullAway.java

@@ -84,7 +84,6 @@
 import com.sun.tools.javac.code.Symbol;
 import com.sun.tools.javac.code.Symbol.VarSymbol;
 import com.sun.tools.javac.code.Type;
-import com.sun.tools.javac.code.Types;
 import com.sun.tools.javac.processing.JavacProcessingEnvironment;
 import com.sun.tools.javac.tree.JCTree;
 import com.uber.nullaway.ErrorMessage.MessageTypes;
@@ -461,7 +460,7 @@ public Description matchMethod(MethodTree tree, VisitorState state) {
     boolean exhaustiveOverride = config.exhaustiveOverride();
     if (isOverriding || !exhaustiveOverride) {
       Symbol.MethodSymbol closestOverriddenMethod =
-          getClosestOverriddenMethod(methodSymbol, state.getTypes());
+          NullabilityUtil.getClosestOverriddenMethod(methodSymbol, state.getTypes());
       if (closestOverriddenMethod != null) {
         return checkOverriding(closestOverriddenMethod, methodSymbol, null, state);
       }
@@ -1817,7 +1816,7 @@ private boolean isInitializerMethod(VisitorState state, Symbol.MethodSymbol symb
       }
     }
     Symbol.MethodSymbol closestOverriddenMethod =
-        getClosestOverriddenMethod(symbol, state.getTypes());
+        NullabilityUtil.getClosestOverriddenMethod(symbol, state.getTypes());
     if (closestOverriddenMethod == null) {
       return false;
     }
@@ -1965,7 +1964,7 @@ public boolean nullnessFromDataflow(VisitorState state, ExpressionTree expr) {
       // figure out if we care
       return false;
     }
-    return nullnessToBool(nullness);
+    return NullabilityUtil.nullnessToBool(nullness);
   }
 
   public AccessPathNullnessAnalysis getNullnessAnalysis(VisitorState state) {
@@ -2113,51 +2112,6 @@ private static ExpressionTree stripParensAndCasts(ExpressionTree expr) {
     return expr;
   }
 
-  private static boolean nullnessToBool(Nullness nullness) {
-    switch (nullness) {
-      case BOTTOM:
-      case NONNULL:
-        return false;
-      case NULL:
-      case NULLABLE:
-        return true;
-      default:
-        throw new AssertionError("Impossible: " + nullness);
-    }
-  }
-
-  /**
-   * find the closest ancestor method in a superclass or superinterface that method overrides
-   *
-   * @param method the subclass method
-   * @param types the types data structure from javac
-   * @return closest overridden ancestor method, or <code>null</code> if method does not override
-   *     anything
-   */
-  @Nullable
-  private Symbol.MethodSymbol getClosestOverriddenMethod(Symbol.MethodSymbol method, Types types) {
-    // taken from Error Prone MethodOverrides check
-    Symbol.ClassSymbol owner = method.enclClass();
-    for (Type s : types.closure(owner.type)) {
-      if (types.isSameType(s, owner.type)) {
-        continue;
-      }
-      for (Symbol m : s.tsym.members().getSymbolsByName(method.name)) {
-        if (!(m instanceof Symbol.MethodSymbol)) {
-          continue;
-        }
-        Symbol.MethodSymbol msym = (Symbol.MethodSymbol) m;
-        if (msym.isStatic()) {
-          continue;
-        }
-        if (method.overrides(msym, owner, types, /*checkReturn*/ false)) {
-          return msym;
-        }
-      }
-    }
-    return null;
-  }
-
   /**
    * Returns the computed nullness information from an expression. If none is available, it returns
    * Nullable.

nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java

@@ -41,6 +41,8 @@
 import com.sun.tools.javac.code.Types;
 import com.sun.tools.javac.tree.JCTree;
 import com.sun.tools.javac.util.JCDiagnostic;
+import java.util.HashSet;
+import java.util.Set;
 import java.util.stream.Stream;
 import javax.annotation.Nullable;
 import javax.lang.model.element.AnnotationMirror;
@@ -79,6 +81,38 @@ public static boolean lambdaParamIsImplicitlyTyped(VariableTree lambdaParameter)
     return diagnosticPosition.getStartPosition() == diagnosticPosition.getPreferredPosition();
   }
 
+  /**
+   * find the closest ancestor method in a superclass or superinterface that method overrides
+   *
+   * @param method the subclass method
+   * @param types the types data structure from javac
+   * @return closest overridden ancestor method, or <code>null</code> if method does not override
+   *     anything
+   */
+  @Nullable
+  public static Symbol.MethodSymbol getClosestOverriddenMethod(
+      Symbol.MethodSymbol method, Types types) {
+    // taken from Error Prone MethodOverrides check
+    Symbol.ClassSymbol owner = method.enclClass();
+    for (Type s : types.closure(owner.type)) {
+      if (types.isSameType(s, owner.type)) {
+        continue;
+      }
+      for (Symbol m : s.tsym.members().getSymbolsByName(method.name)) {
+        if (!(m instanceof Symbol.MethodSymbol)) {
+          continue;
+        }
+        Symbol.MethodSymbol msym = (Symbol.MethodSymbol) m;
+        if (msym.isStatic()) {
+          continue;
+        }
+        if (method.overrides(msym, owner, types, /*checkReturn*/ false)) {
+          return msym;
+        }
+      }
+    }
+    return null;
+  }
   /**
    * finds the symbol for the top-level class containing the given symbol
    *
@@ -179,6 +213,34 @@ public static Stream<? extends AnnotationMirror> getAllAnnotations(Symbol symbol
     return AnnotationUtils.getElementValue(annot, "value", String.class, true);
   }
 
+  /**
+   * Retrieve the {@code value} attribute of a method annotation of some type where the {@code
+   * value} is an array.
+   *
+   * @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 The {@code value} attribute of the annotation as a {@code Set}, or {@code null} if the
+   *     annotation is not present.
+   */
+  public static @Nullable Set<String> 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;
+      }
+    }
+    if (annot == null) {
+      return null;
+    }
+    return new HashSet<>(AnnotationUtils.getElementValueArray(annot, "value", String.class, true));
+  }
+
   /**
    * Works for method parameters defined either in source or in class files
    *
@@ -227,6 +289,27 @@ public static boolean mayBeNullFieldFromType(@Nullable Symbol symbol, Config con
         && Nullness.hasNullableAnnotation(symbol, config);
   }
 
+  /**
+   * Converts a {@link Nullness} to a {@code bool} value.
+   *
+   * @param nullness The nullness value.
+   * @return true if the nullness value represents a {@code Nullable} value. To be more specific, it
+   *     returns true if the nullness value is either {@link Nullness#NULL} or {@link
+   *     Nullness#NULLABLE}.
+   */
+  public static boolean nullnessToBool(Nullness nullness) {
+    switch (nullness) {
+      case BOTTOM:
+      case NONNULL:
+        return false;
+      case NULL:
+      case NULLABLE:
+        return true;
+      default:
+        throw new AssertionError("Impossible: " + nullness);
+    }
+  }
+
   /**
    * Check if a symbol comes from unannotated code.
    *

nullaway/src/main/java/com/uber/nullaway/annotations/EnsuresNonNull.java

@@ -0,0 +1,19 @@
+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();
+}

nullaway/src/main/java/com/uber/nullaway/annotations/RequiresNonNull.java

@@ -0,0 +1,19 @@
+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();
+}

nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPath.java

@@ -32,9 +32,11 @@
 import com.sun.tools.javac.code.Type;
 import com.sun.tools.javac.code.Types;
 import java.util.ArrayList;
+import java.util.Collections;
 import java.util.List;
 import javax.annotation.Nullable;
 import javax.lang.model.element.Element;
+import javax.lang.model.element.VariableElement;
 import org.checkerframework.dataflow.cfg.node.FieldAccessNode;
 import org.checkerframework.dataflow.cfg.node.IntegerLiteralNode;
 import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
@@ -43,6 +45,7 @@
 import org.checkerframework.dataflow.cfg.node.MethodInvocationNode;
 import org.checkerframework.dataflow.cfg.node.Node;
 import org.checkerframework.dataflow.cfg.node.StringLiteralNode;
+import org.checkerframework.dataflow.cfg.node.SuperNode;
 import org.checkerframework.dataflow.cfg.node.ThisLiteralNode;
 import org.checkerframework.dataflow.cfg.node.VariableDeclarationNode;
 import org.checkerframework.dataflow.cfg.node.WideningConversionNode;
@@ -255,6 +258,21 @@ public static AccessPath getAccessPathForNodeWithMapGet(Node node, @Nullable Typ
     }
   }
 
+  /**
+   * Constructs an access path ending with the class field element in the argument. The receiver is
+   * the method receiver itself.
+   *
+   * @param element the receiver element.
+   * @return access path representing the class field
+   */
+  public static AccessPath fromFieldElement(VariableElement element) {
+    Preconditions.checkArgument(
+        element.getKind().isField(),
+        "element must be of type: FIELD but received: " + element.getKind());
+    Root root = new Root();
+    return new AccessPath(root, Collections.singletonList(new AccessPathElement(element)));
+  }
+
   private static boolean isBoxingMethod(Symbol.MethodSymbol methodSymbol) {
     return methodSymbol.isStatic()
         && methodSymbol.getSimpleName().contentEquals("valueOf")
@@ -318,6 +336,8 @@ && isBoxingMethod(ASTHelpers.getSymbol(methodInvocationTree))) {
       result = new Root(((LocalVariableNode) node).getElement());
     } else if (node instanceof ThisLiteralNode) {
       result = new Root();
+    } else if (node instanceof SuperNode) {
+      result = new Root();
     } else {
       // don't handle any other cases
       result = null;

nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java

@@ -18,8 +18,10 @@
 
 package com.uber.nullaway.dataflow;
 
+import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
 import com.google.errorprone.VisitorState;
+import com.sun.source.tree.Tree;
 import com.sun.source.util.TreePath;
 import com.sun.tools.javac.util.Context;
 import com.uber.nullaway.Config;
@@ -34,6 +36,8 @@
 import javax.lang.model.element.Element;
 import javax.lang.model.element.ElementKind;
 import javax.lang.model.element.VariableElement;
+import org.checkerframework.dataflow.analysis.AnalysisResult;
+import org.checkerframework.dataflow.cfg.node.MethodAccessNode;
 import org.checkerframework.dataflow.cfg.node.MethodInvocationNode;
 import org.checkerframework.dataflow.cfg.node.Node;
 
@@ -220,6 +224,55 @@ public NullnessStore getNullnessInfoBeforeNewContext(
         });
   }
 
+  /**
+   * Get the {@link Nullness} value of an access path ending in a field at some program point.
+   *
+   * @param path Tree path to the specific program point.
+   * @param context Javac context.
+   * @param baseExpr The base expression {@code expr} for the access path {@code expr . f}
+   * @param field The field {@code f} for the access path {@code expr . f}
+   * @param trimReceiver if {@code true}, {@code baseExpr} will be trimmed to extract only the
+   *     receiver if the node associated to {@code baseExpr} is of type {@link MethodAccessNode}.
+   *     (e.g. {@code t.f()} will be converted to {@code t})
+   * @return The {@link Nullness} value of the access path at the program point. If the baseExpr and
+   *     field cannot be represented as an {@link AccessPath}, or if the dataflow analysis has no
+   *     result for the program point before {@code path}, conservatively returns {@link
+   *     Nullness#NULLABLE}
+   */
+  public Nullness getNullnessOfFieldForReceiverTree(
+      TreePath path, Context context, Tree baseExpr, VariableElement field, boolean trimReceiver) {
+    Preconditions.checkArgument(field.getKind().equals(ElementKind.FIELD));
+    AnalysisResult<Nullness, NullnessStore> result =
+        dataFlow.resultForExpr(path, context, nullnessPropagation);
+    if (result == null) {
+      return Nullness.NULLABLE;
+    }
+    NullnessStore store = result.getStoreBefore(path.getLeaf());
+    // used set of nodes, a tree can have multiple nodes.
+    Set<Node> baseNodes = result.getNodesForTree(baseExpr);
+    if (store == null || baseNodes == null) {
+      return Nullness.NULLABLE;
+    }
+    // look for all possible access paths might exist in store.
+    for (Node baseNode : baseNodes) {
+      // it trims the baseExpr to process only the receiver. (e.g. a.f() is trimmed to a)
+      if (trimReceiver && baseNode instanceof MethodAccessNode) {
+        baseNode = ((MethodAccessNode) baseNode).getReceiver();
+      }
+      AccessPath accessPath = AccessPath.fromBaseAndElement(baseNode, field);
+      if (accessPath == null) {
+        continue;
+      }
+      Nullness nullness = store.getNullnessOfAccessPath(accessPath);
+      // field is non-null if at least one access path referring to it exists with non-null
+      // nullness.
+      if (!nullness.equals(Nullness.NULLABLE)) {
+        return nullness;
+      }
+    }
+    return Nullness.NULLABLE;
+  }
+
   /**
    * Get the static fields that are guaranteed to be nonnull after a method or initializer block.
    *

nullaway/src/main/java/com/uber/nullaway/dataflow/DataFlow.java

@@ -242,7 +242,7 @@ S resultBefore(TreePath exprPath, Context context, T transfer) {
   }
 
   @Nullable
-  private <A extends AbstractValue<A>, S extends Store<S>, T extends ForwardTransferFunction<A, S>>
+  <A extends AbstractValue<A>, S extends Store<S>, T extends ForwardTransferFunction<A, S>>
       AnalysisResult<A, S> resultForExpr(TreePath exprPath, Context context, T transfer) {
     final Tree leaf = exprPath.getLeaf();
     Preconditions.checkArgument(