Nullness Checker Tutorial

Java 8

Java 8 has added several new features to Java. A feature that this document focuses on is the possibility to augment the static type system of Java with a set of type qualifiers. In Java, a type qualifier is an annotation (e.g., @NonNull and @Nullable) that can appear before the use of a type. As in previous versions of Java, programmers can also annotate declarations of classes, fields, methods, local variables, method parameters, etc. Java 8 permits declaration of custom type qualifiers. However, this document focuses on the annotations provided by the Nullness Checker.

Annotation Locations

Java 7 already permits annotations at declarations. The following code snippet from the BloomFilter class in the Guava library shows the use of three annotations at the declarations of a class, method, and method parameter.

@Beta
public final class BloomFilter<T> implements Predicate<T>, Serializable {
  //...
  @Override
  public boolean equals(@Nullable Object object) {
    //...
  }
}

Java 8 permits annotations anywhere that a type can appear including casts and array levels. Here are a few examples.

Casts

nnObject = (@NonNull Date) object; // cast

Arrays

Java 8 permits annotations at every level of an array. For example, the following declares the type of the messages array as a @NonNull array of @Nullable String values. That is, the array itself is @NonNull but its elements are @Nullable.

// arrays:  non-null array of possibly-null Strings
@Nullable String @NonNull [] messages;

Receiver Parameter

Java 8 makes it possible to annotate the implicit receiver parameter (this) of an instance method. The following example annotates the receiver parameter (this) of method setCategory as @UnderInitialization(Object.class):

class Node {
  // receiver ("this" parameter)
  void setCategory(@UnderInitialization(Object.class) Node this, Object category) {
    this.category = category;
  }
}

Generics

Java 8 permits annotations for both declaration and use of generic types. The checker framework comes with a version of the Java standard libraries with nullness annotation. The following shows the nullness annotations for the declaration of a generic type, namely, java.util.Collection.

public interface Collection<E extends @Nullable Object> extends Iterable<E> {
  //...
}

Nullness Checker

Goal

Given a Java program, the goal of the Nullness Checker is to statically ensure that the program won't throw a null pointer exception at run time.

Annotations

The Nullness Checker defines several annotations including type qualifiers. The most common annotations of the Nullness Checker are the type qualifiers @Nullable and @NonNull. The following are some of the common annotations that you may need.

@NonNull

@NonNull is a type annotation that indicates an expression is never null. For a field of a class, the @NonNull annotation indicates that this field is never null after the class has been fully initialized. For static fields, the @NonNull annotation indicates that this field is never null after the containing class is initialized. You rarely need to write the @NonNull annotation in source code, because it is often the default.

@Nullable

@Nullable is a type annotation that indicates the value is not known to be non-null. Only an expression of @Nullable type can be assigned null.

@UnderInitialization

This type qualifier indicates that the object is under initialization and has no alias with a different type exists. It is allowed to store partially initialized objects in fields of an @UnderInitialization object.

The @UnderInitialization annotation is commonly used for a helper method that is called by a constructor. For example:

class Node {
  Object data;
  Object category;

  public Node(Object data, Object category) {
    this.data = data;
    setCategory(category);
  }

  @EnsuresNonNull({"category"})
  void setCategory(@UnderInitialization(Object.class) Node this, Object category) {
    this.category = category;
  }
}

@Raw

@Raw is a slightly simpler variant of @UnderInitialization. @Raw and @UnderInitialization(Object.class) are interchangeable in the above code.

@EnsuresNonNull

All @NonNull fields must either have a default in the field declaration, or be assigned in the constructor or in a helper method that the constructor calls. If your code initializes some fields in a helper method, you will need to annotate the helper method with an annotation such as @EnsuresNonNull({"field1", "field2"}) for all the fields (in this case field1 and field2) that the helper method assigns. The example class Node presented for @UnderInitialization contains a use of @EnsuresNonNull.

@EnsuresNonNullIf

@EnsuresNonNullIf specifies a method postcondition. This method annotation specifies that some expressions are non-null, if the method returns true (or false depending on the arguments of the annotation).

Consider java.lang.Class. Method Class.getComponentType() may return null, but it is specified to return a non-null value if Class.isArray() is true. The annotated JDK that comes with the Nullness Checker declares this relationship as follows:

class Class {

  @EnsuresNonNullIf(expression="getComponentType()", result=true)
  public native boolean isArray();

  public native @Nullable Class<?> getComponentType();

}

A client that checks that a Class reference is indeed that of an array, can then dereference the result of Class.getComponentType safely without any nullness guards. For example:

if (clazz.isArray()) {
  // no possible null dereference on the following line
  TypeMirror componentType = typeFromClass(clazz.getComponentType());
  //...
}

@RequiresNonNull

@RequiresNonNull specifies a method precondition: The annotated method expects the specified variables (typically field references) to be non-null when the method is invoked. For example:

@Nullable Object field1;
@Nullable Object field2;

@RequiresNonNull("field1")
void method1() {
  field1.toString(); // OK, field1 is known to be non-null
  field2.toString(); // error, might throw NullPointerException
}

@SuppressWarnings

You can suppress specific errors and warnings of the Nullness Checker by using @SuppressWarnings("nullness"). The following shows a justified use of @SuppressWarnings("nullness").

// might return null
@Nullable Object getObject(...) { ... }
void myMethod() {
  // The programmer knows that this particular call never returns null,
  // perhaps based on the arguments or the state of other objects.
  @SuppressWarnings("nullness")
  @NonNull Object o2 = getObject(...);
}

assert and @AssumeAssertion

Occasionally, it is inconvenient or verbose to use the @SuppressWarnings annotation. For example, Java permits annotations such as @SuppressWarnings to appear on declarations but not statements. In such cases, you may be able to suppress the warning using an assert statement of a special form. If the string @AssumeAssertion(nullness) appears in the assert message, then the Nullness Checker treats the assertion as suppressing a warning and assumes that the assertion always succeeds. For example, the checker assumes that no null pointer exception can occur in code such as

assert x != null : "@AssumeAssertion(nullness)";
... x.f ...

Default Annotations

Unannotated references are treated as if they had a default annotation. For the Nullness Checker, the default annotation of all types (including fields and method parameters) is @NonNull, except that @Nullable is used for casts, local variables, instanceof, and implicit bounds of generic types.

Nullness Checks

The checker issues a warning in the following cases:

When the code dereferences an expression whose type is not @NonNull.
When the code flows the null value into an expression of @NonNull type. As a special case, the checker warns whenever a field of @NonNull type is not initialized in a constructor.

This example illustrates the programming errors that the checker detects:

// might be null
@Nullable Object obj;

// never null
@NonNull Object nnobj;
...
// checker warning: dereference might cause null pointer exception
obj.toString()

// checker warning: nnobj may become null
nnobj = obj;

// checker warning: redundant test Parameter passing and return values are
// checked analogously to assignments.
if (nnobj == null)

Arrays

The components of a newly created object of reference type are all null. Only after initialization can the array actually be considered to contain non-null components. Therefore, the following is not allowed:

@NonNull Object [] oa = new @NonNull Object[10]; // error

Instead, one creates a nullable or lazy-nonnull array, initializes each component, and then assigns the result to a non-null array:

@Nullable Object [] temp = new Object[10];
for (int i = 0; i < temp.length; ++i) {
  temp[i] = new Object();
}
@SuppressWarnings("nullness")
@NonNull Object [] oa = temp;

Note that the checker is currently not powerful enough to ensure that each array component was initialized. Therefore, the last assignment needs to be trusted: that is, a programmer must verify that it is safe, then write a @SuppressWarnings annotation.

Subtyping

An annotation indicates a contract that a client can depend upon. A subclass is not permitted to weaken the contract; for example, if a method accepts null as an argument, then every overriding definition must also accept null. A subclass is permitted to strengthen the contract though; for example, if a method does not accept null as an argument, then an overriding definition is permitted to accept null. Similarly, if a method guarantees that it returns a non-null value, then every overriding definition must also guarantee that it returns a non-null value.

The Nullness Checker assumes that method java.lang.Object.equals is annotated like the following:

boolean equals(@Nullable Object a1)

Because method java.lang.Object.equals declares its argument as @Nullable, every method that overrides java.lang.Object.equals must declare its argument as @Nullable.

Similarly, the Nullness Checker assumes that method java.lang.Object.clone is annotated like the following:

Object clone() throws CloneNotSupportedException;

Because method java.lang.Object.clone declares its return type as @NonNull, every method that overrides java.lang.Object.clone must declare its return type as @NonNull.

Local Type Qualifier Inference

The Nullness Checker infers type qualifiers for most local variables. This feature reduces the number of annotations that you have to write.

As an example, suppose you write

@Nullable String myVar;
//...
myVar = "hello";
myVar.hashCode();

Although the Nullness Checker issues a warning whenever a method such as hashCode() is called on a possibly-null value, the Nullness Checker need not issue a warning in this case. After the assignment, the Nullness Checker treats myVar as having type @NonNull String, which is a subtype of its declared type.

Here is another example:

@Nullable String myVar;
//...
if (myVar != null) {
  myVar.hashCode();
}

Once again, the Nullness Checker need not issue a warning. Even though myVar is declared as @Nullable String, the type of myVar is @NonNull String within the body of the if test.

Exercises

Exercise 1

If you run the Nullness Checker on the following piece of code, which part of the code will cause an error message and why?

public class TreeNode {
  int value = 0;
  @Nullable TreeNode left = null;
  @Nullable TreeNode right = null;
  //...
  int addTree() {
    int total = value;
    total += left.addTree();
    total += right.addTree();
    return total;
  }
}

Exercise 2

If you run the Nullness Checker on the following piece of code, the checker will report the warnings shown below the code. What annotations will you add to resolve the warnings?

class TreeNode {
  Object data;
  TreeNode left;
  TreeNode right;

  public TreeNode(Object data, TreeNode l, TreeNode r) {
    this.data = data;
    setChildren(l, r);
  }

  void setChildren(TreeNode l, TreeNode r) {
    left = l;
    right = r;
  }
}

TreeNode.java: warning: [initialization.fields.uninitialized] the constructor does not initialize fields: left, right
  public TreeNode(Object data, TreeNode l, TreeNode r) {
         ^
TreeNode.java: warning: [method.invocation.invalid] call to setChildren(TreeNode,TreeNode) not allowed on the given receiver.
    setChildren(l, r);
               ^
  found   : @UnderInitialization(java.lang.Object.class) @NonNull TreeNode
  required: @Initialized @NonNull TreeNode
2 warnings

Exercise 3

If you run the Nullness Checker on the following piece of code, the checker will report the warning shown below the code. What annotations will you add to resolve the warnings? Do you think that it's justified to suppress this warning? How would you suppress this warning?

public class TreeNode {
  int value = 0;
  @Nullable TreeNode left = null;
  @Nullable TreeNode right = null;

  static @Nullable TreeNode createTree(int levels) {
    if (levels == 0) {
      return null;
    } else {
      TreeNode n = new TreeNode();
      n.left = createTree(levels - 1);
      n.right = createTree(levels - 1);
      return n;
    }
  }

  void printTree() {
    System.out.println(value);
    if (left != null) left.printTree();
    if (right != null) right.printTree();
  }
  
  static void printTwoLeveledTree() {
    TreeNode twoLeveledTree = createTree(2);
    twoLeveledTree.printTree();
  }
}

warning: [dereference.of.nullable] dereference of possibly-null reference twoLeveledTree
return twoLeveledTree.printTree();
       ^

Exercise 4

If you run the Nullness Checker on the following piece of code, the checker will report the warning shown below the code. Why does the checker report the warning? How would you resolve this warning?

public class TreeNode {
  Object[] children;

  public TreeNode(int size) {
    children = new Object[size];
    for (int i = 0; i < size; ++i) {
      children[i] = new Object();
    }
  }
}

TreeNode.java: warning: [assignment.type.incompatible] incompatible types in assignment.
      children = new Object[size];
                 ^
  found   : @Nullable Object @NonNull []
  required: @NonNull Object @NonNull []

Exercise 5

If you run the Nullness Checker on the following piece of code, the checker will report the warnings shown below the code. Why does the checker report the warnings? How would you resolve these warnings?

interface Function {
  String apply(@Nullable String input);
}

class Trimmer implements Function {
  @Override
  public @Nullable String apply(String input) {
    return input.trim();
  }
}

Override.java: warning: [override.return.invalid] @Initialized @Nullable String apply(@Initialized @NonNull Trimmer this, @Initialized @NonNull String p0) in Trimmer cannot override @Initialized @NonNull String apply(@Initialized @NonNull Function this, @Initialized @Nullable String p0) in Function; attempting to use an incompatible return type
  public @Nullable String apply(String input) {
                   ^
  found   : @Initialized @Nullable String
  required: @Initialized @NonNull String
Override.java: warning: [override.param.invalid] @Initialized @Nullable String apply(@Initialized @NonNull Trimmer this, @Initialized @NonNull String p0) in Trimmer cannot override @Initialized @NonNull String apply(@Initialized @NonNull Function this, @Initialized @Nullable String p0) in Function; attempting to use an incompatible parameter type
  public @Nullable String apply(String input) {
                                       ^
  found   : @Initialized @NonNull String
  required: @Initialized @Nullable String
2 warnings

References

The Checker Framework Manual v1.8.0.

Nullness Checker Tutorial

Java 8

Annotation Locations

Casts

Arrays

Receiver Parameter

Generics

Nullness Checker

Goal

Annotations

assert and @AssumeAssertion

Default Annotations

Nullness Checks

Arrays

Subtyping

Local Type Qualifier Inference

Exercises

Exercise 1

Exercise 2

Exercise 3

Exercise 4

Exercise 5

References

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Clone this wiki locally