JSR 308 Checkers and Framework

Version 0.2.2 (16 Aug 2007)

Contents:

• Introduction
• Installation
• Using a checker
  • Checking against unannotated code
• What the checker guarantees
• How to report bugs
• Credits and changelog

Introduction

This distribution contains

• a set of 3 compiler plug-ins (also known as “annotation processors”) that find errors or verify their absence:
  1. for null pointer errors
  2. for mutability errors (incorrect side effects), based on the Javari type system.
  3. for mutability errors (incorrect side effects), based on the IGJ type system.
• a framework that facilitates the writing of such plug-ins.

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 by running the NonNull checker examples, and by running ant all-tests in the checkers directory.

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 that appear in 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.
   • If source code is available, you can annotate the source code and re-compile the library.
   • Use the skeleton class generation tool on a compiled library and annotate the fields and method signatures of the resulting skeleton classes. This approach is often suitable for quickly annotating portions of a library such as the JDK.
   • Whether or not source code is available, you can annotate the compiled .jar or .class files by using the annotation file utilities to express the annotations textually and then insert them in the compiled library classfiles.
3. 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.

• The checkers framework does not support reasoning about reflection. It is difficult for a tool to determine all possible effects of reflective calls, which may violate the property being checked.
• A compiler plug-in can check only those parts of your program that you run it on. If you compile some parts of your program without the -typeprocessor switch or with the checkers.skipClasses property (in other words, without running the checker), then there is no guarantee that the entire program satisfies the property being checked. An analogous situation is linking against an external library that was compiled without being checked by the compiler plug-in.
  Note that a checker can be useful in finding bugs even if it is unable to verify the correctness of an entire program.
• Specific checkers may have other limitations; see their documentation for details.

How to report bugs

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

We welcome bug reports and suggestions. 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.

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