JSR 308 Checkers and Framework

Version 0.2.3 (30 Aug 2007)

Contents:

Introduction

This distribution contains

This document describes how to use the provided plug-ins. If you wish to write your own compiler plug-in, you should first read this document, and then read the document "How to write a JSR 308 checker plug-in".

Finding bugs with a compiler plug-in is a two-step process.

  1. A programmer writes annotations that specify additional information about Java types. (For instance, a @NonNull annotation may specify that a variable should never have a null value. A @Interned annotation may specify that a variable only holds interned values.)
  2. The programmer runs the compiler plug-in, which reports whether the program contains any code that is inconsistent with the annotations. (For instance, a null-checking plug-in might verify the absence of null pointer exceptions, or show where in the program they might occur. An interning-checking plug-in might verify the absence of equality test errors, or show where in the program they might occur.)

Installation

Follow these steps to install the checkers and the framework.

  1. Install the JSR 308 implementation, which extends the Java language to permit annotations to appear on types.
  2. Download the checkers and framework: jsr308-checkers.zip.
  3. Unzip the distribution zipfile, which creates a checkers directory. We recommend that you do this in the parent of the JSR 308 openjdk directory, so that the checkers and openjdk directories are siblings.
  4. Edit the checkers/build.properties file so that the “compiler.lib” property specifies the location of the JSR 308 javac.jar library. (If the checkers and openjdk directories are siblings, no edits are necessary.)
  5. Build the checkers.jar library by running ant in the checkers directory.
  6. Add the checkers.jar file, which is produced in the checkers directory by a successful build, to your classpath.
  7. Test that everything works:

The JSR 308 checkers framework is implemented for the OpenJDK javac compiler. Eclipse users can use the checkers framework it even now by using javac as their external builder. (A checkers implementation builds on top of standard mechanisms such as JSR 269 annotation processing, but also accesses the compiler's AST. In the long run, a checker built using the checkers framework should not be dependent on any compiler specifics.)

Using a checker

To run a checker (also known as a type-checking compiler plug-in, or an annotation processor), run the JSR 308 compiler javac as usual, but pass the -typeprocessor plug-in_class command-line option:

  javac -typeprocessor plug-in_class ...

A concrete example (using the NonNull checker) is:

  javac -typeprocessor checkers.nonnull.NonnullChecker MyFile.java

You can always compile the code without the -typeprocessor command-line option, but in that case no checking of the type annotations is performed.

When writing source code with annotations, typically you will add

import checkers.quals.*;

at the top of the source file, so that you can use annotations such as @NonNull instead of @checkers.quals.NonNull.

Checking against unannotated code

A checker plug-in reads annotations from the source code or .class files of classes that are used by the code being compiled and checked. If annotated code uses unannotated code (e.g., libraries or the JDK), then the checker may issue warnings. For example, the NonNull checker will warn whenever an unannotated library call result is used in a non-null context:

  @NonNull myvar = library_call();   // WARNING: library_call is not known to return a non-null value

There are three ways to avoid such warnings.

  1. Obtain a version of the library that is annotated, or a set of external annotations that describe the library. In the future, we intend to distribute such annotations for popular libraries, such as the JDK.
  2. Annotate the library with @NonNull, using one of these techniques:
  3. Suppress specific errors and warnings by use of the @SuppressWarnings("annotationname") annotation, for example @SuppressWarnings("interned"). Currently, this annotation is only recognized when placed on a method.
  4. Suppress errors and warnings pertaining to un-annotated (or other) classes, by setting the checkers.skipClasses Java property to a regular expression that matches classes for which warnings and errors should be suppressed. For example, if you use -Dcheckers.skipClasses=^java\. on the command line when invoking javac, then the checkers will suppress warnings relating to uses of classes in the java package.

What the checker guarantees

A checker can guarantee that a particular property holds throughout the code. For example, a non-null checker can guarantee that every expression whose type is a @NonNull type never evaluates to null. An interned checker can guarantee that every expression whose type is an @Interned type evaluates to an interned value. The checker makes its guarantee by examining every part of your program and verifying that no part of the program violates the guarantee.

There are some limitations to the guarantee.

How to report bugs

We welcome bug reports, suggestions, bug fixes, new features, new type-checking plug-ins, and other improvements.

If you have any problems (with the checkers framework or with any of the checkers that are included with it), please let us know. See the JSR 308 bug-reporting instructions for guidelines, and use the same email address (jsr308-bugs@lists.csail.mit.edu) for reporting bugs.

Credits and changelog

The JSR 308 checkers framework was implemented by Matthew M. Papi. The non-null plug-in was implemented by Matthew M. Papi. The Javari plug-in was implemented by Telmo Correa. The IGJ plug-in was implemented by Mahmood Ali. The interned plug-in was implemented by Matthew M. Papi.

Differences from previous versions of the checkers and framework can be found in the changelog.