JastAdd
This is our old website.
Broken links can occur.
A new website is under construction.

Non-null types for Java

Non-null types is a type-based approach to detect possible null pointer violations in code statically at compile time. Fädrich and Leino showed how an object-oriented language such as Java or C# could be extended with non-null types. We have extended a Java compiler, in a modular way, to include non-null types. This is an example of how a large JastAdd project can be extended in an easy and declarative way. We have also implemented an inference algorithm to retrofit legacy code to include non-null types.

We provide two tools to support development in Java with non-null types: a checker to detect possible null-pointer violations at compiler time, and an inferencer to automatically annotate legacy code with nullness annotations.

The latest distribution of the tools is available at http://builds.jastadd.org/NonNullTools/latest and older versions are available at http://builds.jastadd.org/NonNullTools 

Non-null checker

 The non-null checker relies on type annotations to detect possible null-pointer violations. Consider the code snippet below:

class C {
    void test() { }
    public static void main(String[] args) {
        @NonNull C c1 = new C(); // c1 can only hold non-null values
        C c2 = null; // c2 can hold possibly-null values
        c1.test(); // ok: c1 can not be null
        c2.test(); // error: c2 may be null and the invocation may 
                   //        throw a null pointer exception
        c1 = c2; // error: a non-null variable may not be assigned a 
                 //        possibly null value

        c2 = c1; // ok: a possibly-null variable may be assigned a 
                 //     non-null value
        if(c2 != null) {
            c1 = c2; // ok: an explicit comparison to null acts as a
                     //     safe cast as long as there are no possibly
                     //     null assignments in the block
        }
    }
}

If we run the above program through the non-null checker we get the following output:

> java -jar JavaNonNullChecker.jar C.java
Errors:
C.java:7:
  Semantic Error: qualifier c2 may be null
C.java:9:
  Semantic Error: can not assign c1 of type C- a value of type C

The same program can be compiled using an normal Java compiler, but then the possible null-pointer violations would not be detected.

Non-null inferencer

We also provide a non-null inferencer that 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 checker as described previously.

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 -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:
T. Ekman, G. Hedin:Pluggable checking and inferencing of non-null types for Java. Journal of Object Technology, Vol. 6, No. 9, pages 455-475. Special Issue: TOOLS EUROPE 2007, October 2007.

The work by Fädrich and Leino is available in:
Declaring and Checking Non-Null Types in an Object-Oriented Language, Manuel Fädrich and Rustan Leino, Proceedings of the 18th ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, Anaheim, CA, October 2003, Available in pdf

 

Source code

The non-null checker and inferencer are built as extensions to the JastAdd Extensible Java Compiler. The latest version of the tool suite can be downloaded from  http://builds.jastadd.org/NonNullTools/latest and older builds are available at http://builds.jastadd.org/NonNullTools. The projects rely on Apache ant for building and make sure that the ant heap size is at least 256M. This can be done by setting the environment variable ANT_OPTS="-Xmx256M" on the command line or adding it to ~/.ant/ant.conf
  • Download NonNullTypes-src.jar
  • The archive contains a folder named NonNullTypes which holds all the sources for the non-null checker, the non-null inferencer, and the JastAddJ compiler. Unpack the archive using jar:
jar xf NonNullTypes-src.jar
  • Build the checker by running ant in the NonNullChecker folder and the inferencer by running ant in the NonNullInference folder.
  • There are separate ant targets for building the tools, running tests, generating runnable jars, and source jars. E.g.:
> cd NonNullInference
> ant 
> ant test

> ant jars
> ant source

Tests

  • There is an ant target named test which executes a test suite for each tool
  • 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.