Java: The Checker Framework
One of the interesting tools I learned about at JavaOne 2012 is The Checker Framework. One of the Checker Framework’s web pages states 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 (‘Annotations for Software Defect Detection’) might have been had it not fallen into the Dormant stage.
The intention of JSR 308 (‘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 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 or later. The Checker Framework can be downloaded as a single ZIP file at http://types.cs.washington.edu/checker-framework/current/checkers.zip. 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.
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 (@NonNull) 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.
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. 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.
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
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.
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, 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
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.
Reference: The Checker Framework from our JCG partner Dustin Marx at the Inspired by Actual Events blog.