How NullAway Works

This page gives some further details on the inner workings of NullAway.

Type Inference

The most complex part of the NullAway implementation is its intra-procedural type inference, which infers nullability information for local variables and some types of expressions based on code within the same method. The inference can infer different types for locals / expressions at different program points, e.g.:

void foo(@Nullable Object x) {
  if (x != null) {
    // inference learns x is @NonNull here
    x.toString();
  }
  // x is still @Nullable here, hence error is reported
  x.hashCode();
}

The inference also learns nullability facts for more complex expressions, e.g.:

class ListNode { 
  int data; 
  @Nullable ListNode next; 
  @Nullable ListNode getNext() { return next; }
  
  void doStuff() {
    if (this.next != null && this.next.getNext() != null) {
       // NullAway infers this.next.getNext() to be @NonNull here
       this.next.getNext().toString();
    }
  }
}

Type inference is implemented as a dataflow analysis, leveraging the Checker Framework's dataflow library. An abstract state is a mapping from access paths to a corresponding nullability state. For further background on access paths see Section 5.2 of this document. NullAway allows for zero-argument method calls (like getters) to be included in access paths along with field names. NullAway also makes the simplifying (but unsound) assumption that callees perform no mutation, and hence does not invalidate nullability state for access paths across method calls.

The dataflow transfer functions are implemented here. For the most part, the transfer functions simply propagate information learned from assignments and null checks for any expression representable as an access path. Some care must be taken in constructing the initial store when analyzing the body of a lambda expression. Unlike normal methods, lambda parameters inherit the nullability of their corresponding functional interface methods, to eliminate verbosity, so some logic is required to "infer" the initial nullability of the lambda parameters.

For matching of containsKey() and get() calls for maps, NullAway additionally tracks the receiver and first argument to such calls as an access path. So, if there is a call ap1.get(ap2) underneath a conditional if (ap1.containsKey(ap2)), where ap1 and ap2 are representable access paths, NullAway treats the get() call as returning @NonNull.

Error Checking

Given the results of type inference, in some cases, error checking involves directly checking the conditions that would lead to each possible error message. The logic is in the main NullAway class. E.g., to check fields assignments, we ensure that if the field is @NonNull, the right-hand side expression of the assignment is not @Nullable. Checking of dereferences, parameter passing and returns, and method overriding is similarly straightforward.

Checking for proper initialization of @NonNull fields is more involved. Here, we must again leverage the results of dataflow analysis, to show that the relevant field is @NonNull at the exit node of the relevant constructor / initializer (i.e., it is initialized on all paths). Similarly, dataflow analysis is used to check for read-before-init errors, by inferring field nullability at the program point before the read. Our dataflow analysis has been designed such that we can analyze a method once (an expensive operation) and re-use the result for type inference and all initialization checking. NullAway also has targeted inter-procedural reasoning to allow, e.g., for field initialization in a private method that is always invoked from an initializer.

Some other special cases are worth mentioning. Java 8 lambdas are treated as overrides of the corresponding functional interface methods, so override checking proceeds similarly to that of normal methods, but with inherited nullability for unannotated parameters (as discussed in the above section on inference). Method references are also checked against the expected functional interface method, but careful handling of corner cases like unbound instance methods is required. Finally, unboxing of a null value leads to an NPE, so we introduce checks for nullability for various operations that cause unboxing.

Extensibility through Handlers

The main way to extend the behavior of NullAway beyond the core inference and checking described above, is to use a handler.

Through the NullAway codebase, there are multiple extension points, at which the core code calls specific methods of the Handler interface for all registered handler objects. To extend or override the default behavior for NullAway, it often suffices to scan that interface for the corresponding extension point method(s), then subclass BaseNoOpHandler overriding only said method(s), and finally add an instance of the new handler at the end of the list returned by Handlers.buildDefault().

For example, consider LibraryModelsHandler, which is used to provide models for unannotated third-party library methods. This handler first uses a service loader to find custom models for methods, in addition to those declared inside the DefaultLibraryModels class. It then registers itself as a handler overriding, among others, Handler.onDataflowVisitMethodInvocation. This particular extension hook allows it to change, on a callsite by callsite basis, the nullability assumption for the method's return value. By default, NullAway assumes unannotated methods return @NonNull. However, the LibraryModelsHandler changes that value for those methods for which an explicit library model exists which shows the return method to be @Nullable, and the NullAway core dataflow simply moves forward propagating that @Nullable value in those cases.

LibraryModelsHandler overrides similar extension points to mark the arguments to certain library methods as @NonNull and check for correct overriding of modeled library methods. Because of the handlers mechanism, the core NullAway classes don't need to know about the existence of library models at all, they only need the general hooks to override the default return nullability and argument nullability of unannotated methods. These same hooks can be used by other handlers that derive this information from sources other than explicit library models (e.g. ContractHandler below, or even our experimental bytecode analysis).

Some other NullAway extensions implemented as handlers include:

• RxNullabilityPropagator: This is a handler which propagates nullability information across call boundaries for select methods inside an Rx stream. For example, this allows handling the following code: observable.filter(o -> o != null).map(o -> o.toString()). This is an example of handlers being used to add limited forms of inter-procedural inference, which is prohibitively expensive in the general case.
• ContractHandler: Adds support for a subset of the specifications of the @Contract annotation (e.g. @Contract("!null -> !null") means that if the method's sole argument is @NonNull, then the dataflow analysis should also assume the return is @NonNull).
• ApacheThriftIsSetHandler: Correctly interprets isSetXXXX() calls inside code generated by the Apache Thrift library as checking the nullability of property XXXX.
• OptionalEmptinessHandler: Implements our support for preventing .get(...) calls on Optional values without checking that the Optional is non-empty, effectively extending NullAway to handle accesses to potentially empty optional values the same it way it handles dereference of @Nullable values, without any optional-specific changes to the core tool.

Note that handlers overriding the same extension method are chained together, and the order of the handler chain in Handlers.buildDefault() can matter in certain cases. Please refer to the documentation of the corresponding Handler interface method. In general, due to the performance focus of NullAway, handler chains should remain shallow for most extension methods, and handlers are expected to be as performant as core code. One important advantage of handlers, besides helping to keep the core code readable, is that they allow turning on and off specific non-core NullAway features by simply adding or removing the corresponding handler from Handlers.buildDefault().

JSpecify

Work is underway to implement support for the JSpecify specification of the semantics of Java nullability annotations. This work includes support for nullability annotations on generic type arguments. For now this support is mostly off by default, but can be enabled by passing the -XepOpt:NullAway:JSpecifyMode flag. An exception is support for the @NullMarked and @NullUnmarked annotations, which is on by default (except for module support, which is not yet implemented).

Relevant code for implementing JSpecify support sits in the com.uber.nullaway.generics package, mainly in the GenericsChecks class. Tests are in the com.uber.nullaway.jspecify package.