The Checker Framework

One of the interesting tools I learned about [1] at JavaOne 2012 [2] is The Checker Framework [3]. One of the Checker Framework's web pages [4] states [5] that the Checker Framework "enhances Java’s type system to make it more powerful and useful," allowing software developers "to detect and prevent errors in their Java programs." One way to look at the Checker Framework is as an implementation of what JSR 305 [6] ("Annotations for Software Defect Detection") might have been had it not fallen into the Dormant [7] stage.

The intention of JSR 308 [8] ("Annotations on Java Types") is to "extend the Java annotation syntax to permit annotations on any occurrence of a type." Once JSR 308 is approved and becomes part of the Java programming language, annotations will be allowed in places they are not currently allowed. Although JSR 308 is still in Early Draft Review 2 [9] stage, Checker Framework allows a developer to include commented-out annotation code in places not currently allowed until made available by JSR 308. It is important to note here that JSR 308 only makes annotations more generally available (specifies more types of source code against which they can be applied) and does not specify any new annotations.

The Checker Framework requires Java SE 6 [10] or later. The Checker Framework can be downloaded as a single ZIP file at http://types.cs.washington.edu/checker-framework/current/checkers.zip [11]. The downloaded file can be unzipped to the directory checker-framework and then an environmental variable called CHECKERS can be set to point to that expanded directory's subdirectory "checkers." For example, if the checkers.zip is unzipped to C:\checker-framework, then the environmental variable CHECKERS should be set to C:\checker-framework\checkers.

One the Checker Framework checkers.zip has been downloaded, expanded, and pointed to by the CHECKERS environmental variable, it is time to try the Checker Framework out. The "long way" of running the Checker Framework is shown next and is used with the -version tag to verify that Checker Framework is applied:

Windows

java -Xbootclasspath/p:%CHECKERS%/binary/jsr308-all.jar -jar %CHECKERS%/binary/jsr308-all.jar -version

Linux

java -Xbootclasspath/p:$CHECKERS/binary/jsr308-all.jar -jar $CHECKERS/binary/jsr308-all.jar -version

The above should lead to output that looks something like that shown in the next screen snapshot.

[12]

The installed Checker Framework can now be applied to compiling code. The next code listing shows a simple class that specifies that a method argument should not be null via the checkers.nullness.quals.NonNull [13] (@NonNull [14]) annotation.

Example of Using Checker Framework's @NonNull

package dustin.examples;

import checkers.nullness.quals.NonNull;
import static java.lang.System.out;

public class CheckersDemo
{
public void printNonNullToString(@NonNull final Object object)
{
out.println(object.toString());
}

public static void main(final String[] arguments)
{
final CheckersDemo me = new CheckersDemo();
final String nullStr = null;
me.printNonNullToString(nullStr);
}
}

The above code listing shows a null being passed to a method with the argument annotated with @NonNull. NetBeans 7.3 flags this with the yellow squiggles and warning if hovered over. This is shown in the next screen snapshots.

[15]

[16]

Although NetBeans flags the null setting of a parameter marked with the @NonNull annotation, the compiler builds that code without complaint. This is where the Checker Framework comes in. Because it's a pain to type in the long command I showed previously, I either run the command shown above with a script or set up an alias as described in the Checker Framework Installation Instructions [17]. In this case, I'll use an alias like this:

Setting Windows Command Line Alias for Java Checker

doskey javachecker=java -Xbootclasspath/p:%CHECKERS%\binary\jsr308-all.jar -jar %CHECKERS%\binary\jsr308-all.jar $*

The setting of this alias and running it with the -version flag is demonstrated in the next screen snapshot.

[18]

It is far easier to apply this approach with the alias set. This can be used to compile the class in question as shown next (command using my 'javachecker' alias and image showing result).

javachecker -d classes src\dustin\examples\*.java

[19]

The above command demonstrates that I am able to use normal javac options such as -d to specify the destination directory for compiled .class files and pass along the Java source files to be compiled as normal. The example also demonstrates that without specifying the checker processor to run as part of the compilation, the @NotNull additional typing is not enforced during compilation.

Before showing how to specify a processor to force the @NonNull to be be enforced during compilation, I want to quickly demonstrate that this compilation approach will still report standard compiler errors. Just for this example, I have renamed the "nullStr" variable passed to the method of interest on line 17 to "nullStry" so that it is a compiler error. The next two screen snapshots show this change (and NetBeans's reported compilation error) and how the Checker Framework compilation approach also reports the javac error.

[20]

[21]

Having shown that this approach to compilation compiles compilable code normally, reports compiler errors normally, and shows version appropriately, it is time to apply it to stronger type enforcement. I fix the compiler error in my code by removing the extra "y" that I had added. Then, I need to pass -processor checkers.nullness.NullnessChecker as an additional flag and argument to the compilation process. Note that there are other processors besides NullnessChecker [14], but I am using NullnessChecker here to enforce the @NonNull at compile time.

The following shows the command along with the output window demonstrating that command in action. Note that the compilation process is not allowed to complete and an error based on violation of the @NonNull typing is reported.

javachecker -processor checkers.nullness.NullnessChecker -d classes src\dustin\examples\*.java

[22]

This blog post has introduced the Checker Framework and shown how to quickly apply it to stronger type enforcement in Java source code. I only focused on one type of stronger typing here, but the Checker Framework supplies other built-in type checks and supports the option of writing custom type enforcement checks.

Original posting available at http://marxsoftware.blogspot.com/ [23] (Inspired by Actual Events)