HTTPS SSH

JastAddJ-NonNullInference

This module is an extension to the JastAdd extensible Java compiler (JastAddJ), implementing an inference algorithm for non-null types. The resulting tool, NonNullInferencer, automatically annotates legacy code with non-null annotations.

A companion module JastAddJ-NonNullChecker, detects possible null-pointer violations at compile time, according to the approach by Fähndrich and Leino.

  • Copyright (c) 2005-2014, JastAddJ-NonNullInference Committers

All rights reserved.

JastAddJ-NonNullInference is covered by the Modified BSD License. The full license text is distributed with this software. See the LICENSE file.

NonNullInference

The non-null inferencer takes a Java program without nullness annotations and infers some annotations. The annotated code can then be further annotated manually to improve the detection of possible null-pointer violations. The inferencer takes existing annotations into account, so it can be run on partially annotated code to automatically infer more annotations. Consider the following example:

$ cat C.java
class C {
  void v() { }
  public static void main(String[] args) {
    C c1 = new C();
    C c2 = null;
    c2 = c1;
    c1.v();
    c2.v();
    if(c2 != null) {
      c1 = c2;
    }
  }
}

$ java -jar JavaNonNullInferencer.jar -test C.java
class C {
  void v() { }
  public static void main(@NonNull String[] args) {
    @NonNull C c1 = new C();
    C c2 = null;
    c2 = c1;
    c1.v();
    c2.v();
    if(c2 != null) {
      c1 = c2;
    }
  }
}

The tool detects that the local variable c1 will never hold a null value and therefore annotates it with @nonnull. We think it is desirable to have as many variables non-null as possible and therefore annotates parameters as being non-null if there are no calls where they are possibly-null. That is the reason why the args parameter in main is annotated with @nonnull. There are still possible-null pointer violations in the program, e.g., the invocation of v() on c2. Such errors will be detected if we run the annotated source file through the non-null checker, described in the companion module.

The analysis is a whole program analysis so the tool should preferably process a complete project at a time rather than individual source files. The '-test' option instructs the tool to emit the annotated source code to standard output. Otherwise, the tool will generate annotated source files in a folder named 'inferred'. The name of the target folder can be changed using the option '-d'. Further details on command line options are available using the -help option.

Limitations

The inferencer does not infer non-nullness for array elements but only for the array itself. @nonnull String[] is thus a non-null reference to an array where the elements are possibly-null, and this is supported by the current tools. String[@nonnull] is a possibly-null reference to an array where each element is non-null which is not supported by the current tools.

The inferencer wants to infer as many non-null valued references as possible. If a method is not called it will therefore constrain the parameter types to be non-null. This is why we need to do a whole-program analysis when inferring annotations. If we process a project class by class most method arguments would be non-null which would cause a lot of errors when later checking another class that uses that class.

There may still be possible null-pointer violations in the automatically annotated code. Consider the following example. The analysis can not determine the value of b and the reference o must therefore be possibly null. There is thus no way of preventing the possible null-pointer dereference when calling toString() on o. If we run the checker on the annotated code we should thus get an error that we are trying to dereference a possibly null valued reference. Such errors can not completely be eliminated unless the analysis is exact, in which case we would not need anotations at all. The normal usage would be to manually guard such dereferences by an explicit null check before invoking the method.

String v(boolean b) {
 Object o = b ? new Object() : null;
 String s = o.toString(); // possible null-pointer dereference
 return s;
}

Further details

The following paper describes how JastAddJ is extended with NonNull type checking and inferencing:

  • Pluggable checking and inferencing of non-null types for Java
    Torbjörn Ekman, Görel Hedin
    Journal of Object Technology, Vol. 6, No. 9, pages 455-475.
    Special Issue: TOOLS EUROPE 2007, October 2007.
    Download paper here

The work by Fähndrich and Leino is available in:

  • Declaring and Checking Non-Null Types in an Object-Oriented Language
    Manuel Fähndrich, Rustan Leino
    Proceedings of the 18th ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA'03), Anaheim, CA, October 2003.
    Download paper here

Building

If you checked out this module as a Git repository with the --recursive option you should have the three submodules

If matching directories for these modules does not exist in the NonNullInference directory, but you are using Git, you should be able to run

$ git submodule init
$ git submodule update

in order to get the correct versions of the submodules. You could also checkout each repository to the correct revision manually. Example commands to get the right jastaddj version:

$ git clone https://bitbucket.org/jastadd/jastaddj.git
$ cd jastaddj
$ git checkout c572865

You only need to have javac and Apache Ant installed in order to build. All other tools used are available in JastAddJ.

Build targets:

$ ant         # Build the NonNullInferencer tool as java class files
$ ant jar     # Build the NonNullInferencer tool as a jar file
$ ant test    # Build the tool and run the test suite
$ ant clean   # Remove generated files

Running

To run the tool, do

$ java -jar JavaNonNullInferencer.jar -classpath=... -sourcepath=... java-files

This will place the annotated java-files in a directory inferred. For more options, do

$ java -jar JavaNonNullInferencer.jar -help

Tests

The main program RunTests.java is a test harness which collects and executes all test cases found in the test folder. Each test is simply a .java file and a corresponding .result file holding the expected result.

Variants

Note that if you check out older versions of the modules (2013 and previous), you need to rename the JastAddJ-JSR308 and the JastAddJ-NonNullChecker modules to JSR308 and NonNullChecker, respectively.