JSR-308, checkers framework and static analysis on GeeCON

I’ll be speaking about the JSR-308 specification (annotations on java types), which will be part of Java 7, on the GeeCON conference, which will take place from the 13th till the 14th of May 2010 in Poznan, Poland.

Apart from an introduction to the new annotations, I will cover the checkers framework, and do a live demo of some of the bundled checkers (nullability, immutability), as well as of my typestate checker. I will also show how to implement a simple custom checker, using the framework.

If you’ll be there, be sure not to miss it. If you’ve not yet registered, visit http://2010.geecon.org :).

See you there,
Adam

Typestate checker – checking iterators

In the new 0.2.2 release of the typestate checker (an extension to the JSR308 checkers framework), you can now specify a state, to which an object transits, if a method returns true or false using the afterTrue and afterFalse elements in state annotations.

A good use-case and example is an Iterator. As you probably know, before calling next(), it’s good to check if an element is available using hasNext(). So we can distinguish two “states” of an iterator: CheckHasNext – which means that it is unknown if an element is available or not and ReadNext, in which it is safe to call next().

After calling hasNext(), the iterator should transit to the ReadNext state, but only if the method returns true. Also, after calling next(), the iterator should always transit to the CheckHasNext state. Using typestate annotations, we can write that specification on a stub of the Iterator interface:

public interface Iterator<E> {
  public abstract boolean hasNext()
    @CheckHasNext(afterTrue=ReadNext.class)
    @ReadNext;
  public abstract E next() @ReadNext(after=CheckHasNext.class);
  public abstract void remove();
}

Here I am using annotations on the receiver of the method, a new place where you can put annotations introduced with JSR308.

You can download the definitions of the stubs and the states in an easy-to-run example here. All you need to do is edit the example.sh file to specify the path to the JSR308 distribution, which you can download from its homepage. There are several example source code files which you can typestate-check. It is also quite easy to typestate check your own files – just change the SOURCES parameter of javac.

For example, this snippet of code checks without errors:

  Iterator iter = collection.iterator();
  while (iter.hasNext()) {
    iter.next();
  }

While this throws an error on line 5:

  Iterator iter = collection.iterator();
  while (iter.hasNext()) {
    iter.next();
  }
  iter.next(); // error: iter is in a wrong state

You can find the newest release available for download on the checker’s homepage, as well as in a maven2 repository. The source code is available on github.

Have fun!
Adam

Javarsovia, static analysis and annotations

If you’ll be in Warsaw this weekend, and if you speak polish, be sure not to miss Javarsovia, a one-day conference organized by the Warsaw JUG. I am giving a talk there about how you can use annotations together with static analysis to find bugs in your program early (first presentation in the 3rd track, 9:45, room 103B). Among other things, I’ll be demoing the static access detector and the typestate checker.

See you there!
Adam

New features in Typestate Checker

I’ve uploaded a new version (0.2) of the typestate checker (for an introduction, see this blog post), which contains bug fixes and much improved exception handling. The binaries, source code and installation instructions are on the web page; the source code is also on github, and the binaries in the maven repository. You can use the typestate checker with the jsr308-maven plugin.

A new state-annotation element: onException is supported, which specifies the state, to which an object transits, in case of an exception being thrown (from the place where the object is used: a method or constructor). For example, the specification of some of InputStreams methods could look like this:

class InputStream implements Closeable {
   int read() /*@Open(onException=InputStreamError.class)*/
    throws java.io.IOException;
   close() /*@Any(after=Closed.class)*/
}

This specification says that the read method can only be invoked when the object is in the “open” state, and in case of an error, the object transits to the “inputStreamError” state; that means that the read method cannot be invoked anymore. The close method transits the object from any state (so it can be invoked both when the stream is open, or in an error), to a closed state; again, read cannot be invoked anymore.

The annotations are in comments to make the code Java5-compatible; the checkers framework will recognize them.

Thanks to such specification, and the typestate checker, we can verify at compile-time that no read operations are invoked when the stream is closed. For example, the code below won’t compile (type-check), if compiled with the typestate checker, because of the invalid use of the last read method:

int test(@Open InputStream stream) throws IOException {
  int ret = 0;
  try {
    int input;
    while ((input = stream.read()) != -1) {
      ret += input;
    }
  } finally {
    stream.close();
  }

  // An error will be reported here; the stream is closed
  ret += stream.read();

  return ret;
}

More examples can be found in the examples directory of the source distribution (and ran with the example.sh script; on github: example 1, example 2)

The flow algorithm was improved to properly handle various try-catch-finally combinations, inferring the states of the objects properly when the catches are “alive” or “dead” (if they return/throw an exception or not).

Any opinions, comments, suggestions are welcome! :)

Adam

Envers 1.2.0.GA in Maven repository; JSR308 typestate and maven plugin in GIT

The recently released Envers 1.2.0.GA finally made it to the JBoss Maven repository; you can find it here:
http://repository.jboss.org/maven2/org/jboss/envers/jboss-envers/1.2.0.GA-hibernate-3.3/

Also, following Bob’s example, I’ve put the JSR 308 typestate checker and Maven2 plugin on github:

• http://github.com/adamw/jsr308-typestate-checker/tree
• http://github.com/adamw/jsr308-maven2-plugin/tree

So everyone can now easily grab the source code and modify it.

Have fun!
Adam

JSR308 Checkers Maven2 plugin

I’ve written a prototype JSR308 Checkers Maven2 plugin. You can use the plugin to run any checker on the sources of your module(s).

The JSR308 compiler, and in effect also the checkers, are run in a separate, forked, JVM process. Additionally, this process only does the processing, without actual compilation. So all of your files will be compiled by the same javac as before. The plugin only runs the additional verification of the source code, and will not affect the produced bytecode. Java6 is required to run the forked JVM.

You can easily try using the standard checkers, for checking nullness, interning and mutability errors, as well as the typestate checker; I’ve uploaded the necessary jars to my repository, so to use any of them, you’ll need first to add repositories to your pom.xml:

<repositories>
    <repository>
        <id>mamut-releases</id>
        <url>http://repository.mamut.net.pl/content/repositories/releases</url>
        <releases>
            <enabled>true</enabled>
        </releases>
        <snapshots>
            <enabled>false</enabled>
        </snapshots>
    </repository>
</repositories>
<pluginRepositories>
    <pluginRepository>
        <id>mamut-releases</id>
        <url>http://repository.mamut.net.pl/content/repositories/releases</url>
        <releases>
            <enabled>true</enabled>
        </releases>
        <snapshots>
            <enabled>false</enabled>
        </snapshots>
    </pluginRepository>
</pluginRepositories>

Then, to use the annotations used by the standard checkers, you’ll have to declare a dependency:

<dependencies>
    <!-- annotations for the standard checkers: nullness, interning, mutability -->
    <dependency>
        <groupId>mamut.net.pl</groupId>
        <artifactId>checkers-quals</artifactId>
        <version>0.8.6</version>
    </dependency>
    <!-- and if you want to use the typestate checker: -->
    <dependency>
        <groupId>mamut.net.pl</groupId>
        <artifactId>typestate-checker</artifactId>
        <version>0.1</version>
    </dependency>
    <!-- other dependencies -->
</dependencies>

And finally, you need to attach the plugin to your build lifecycle:

<build>
    <plugins>
        <plugin>
            <groupId>mamut.net.pl</groupId>
            <artifactId>checkersplugin</artifactId>
            <version>0.1</version>
            <executions>
                <execution>
                    <!-- run the checkers after compilation; this can also be any later phase -->
                    <phase>process-classes</phase>
                    <goals>
                        <goal>check</goal>
                    </goals>
                </execution>
            </executions>
            <configuration>
                <!-- checkers you want to be run -->
                <processors>
                    <processor>checkers.nullness.NullnessChecker</processor>
                    <processor>checkers.interning.InterningChecker</processor>
                    <processor>checkers.typestate.TypestateChecker</processor>
                </processors>
                <!-- other configuration - see webpage for details -->
            </configuration>
        </plugin>
    </plugins>
</build>

And that’s it! After compiling, the specified checkers (annotations processors) will be run on your source code and report any errors found.

For more information and full configuration options description, see the web page: http://www.warski.org/checkersplugin.html

Waiting for feedback :)

Adam

Typestate checker – introduction

When dealing with mutable objects in Java, we quite often see that “states” of the class considered emerge. The (abstract) “state” depends of course on the content of the fields of the object. When methods are invoked, which mutate the fields, the state of the object may change. Also, it may be illegal to call some methods in one state, but legal in another.

So far, specifying the state space of an object, which methods can be called in which states, and how methods change the state, is done mainly in comments (javadocs). With the new possibilities brought by JSR 308 – type annotations, it’s now possible to do it in a much more structured way.

The basic idea is simple. Each state of our object is one annotation. We can define those annotations for example as inner classes. There are 2 immediate gains:

• we enumerate all the states of our object, so the state space is well defined;
• each state can be commented, so we have a very good place to describe when an object is in the given state and what does it mean.

As an example, let’s assume that we have a class for reading a remote resource, for example RemoteResourceReader. Objects of this class can be in one of the three states:

• configuration – connection to the resource is being configured
• open – connection to the resource is open, data can be read
• closed – the connection is closed, data cannot be read

The inital state is configuration, in which we set the connection properties, like the URL, username, password, etc. Then, we can change the state to open, read some data, and close the connection, changing the state to closed. After that, we may re-open the connection to read more data, etc.

So how would the source of our class look like? First, we define the states:

public class RemoteResourceReader {
/** Connection to the resource is being configured */
public static @interface Configuration { }
/** Connection to the resource is open, data can be read */
public static @interface Open { }
/** Connection to the resource is closed, data cannot be read */
public static @interface Closed { }

(...)
}

Now, we have to specify what is the initial state and how methods change the state. Thanks to JSR 308, that is easy. Type annotations extend the number of places, where annotations are allowed; you may place them on any type. See its web page for more information.

One of the new places, where annotations are allowed, is the “method receiver”. This lets you specify meta-data (annotations) that apply to the object, on which the method is called. For example, we want to specify that the read method can be invoked on an object only when it is in the open state; similarly, the setURL method can be invoked only when the object is in the configuration state. Using JSR308, we can write it like this:

(...)
public String read() @Open { ... }
public void setURL(String newURL) @Configuration { ... }
(...)

However, to keep the code compatible with Java 5/6, we may place the annotations in comments. They will still be recognized by the JSR308 checker framework (why this is important – read on :) ).

Finally, what about state changes? Here, we also use the method receiver annotations. We may add an element to our state annotations, which will specify the state of the object after the method invocation. For example:

(...)
public void open() @Configuration(after=Open.class)
@Closed(after=Open.class) { ... }
public void close() @Open(after=Closed.class) { ... }
(...)

We have specified that:

• we can invoke the open method, if the object was in the configuration or closed states. After invoking this method, the object will be in the open state
• we can invoke the close method, only if the object was in the open state. After invoking this method, the object will be in the closed state

What are the benefits of using state annotations so far? Improved documentation: users immediately see in what states objects of the class can be, when it is legal to call a method and how the states change. However, there is more: you can check if your objects are in the correct state by using the typestate checker!

The typestate checker is built on top of the checkers framework, which out-of-the box provides other very useful checkers, for nullness and immutability. Be sure to try them out :).

To use the typestate checker, go here for downloads and installation instructions. The only additional requirement is that you must annotate your state annotations with @State. The checker will verify, using flow analysis, if you invoke methods on objects in the correct state, pass parameters in the correct state etc. This version of the checker should be treated more like a proof-of-concept, than as a final version. It is in a very early development stage, so your comments and experiences are very welcome! :)

To complete the RemoteResourceReader example, here is a full version of the class, ready to be used with the typestate checker:

public class RemoteResourceReader {
/** Connection to the resource is being configured */
@State public static @interface Configuration {
Class<?> after default Object.class }
/** Connection to the resource is open, data can be read */
@State public static @interface Open {
Class<?> after default Object.class }
/** Connection to the resource is closed, data cannot be read */
@State public static @interface Closed {
Class<?> after default Object.class }

// Initial state of the object - specified in the
// constructor's receiver annotation
public RemoteResourceReader() /*@Configuration*/ { ... }

public void setURL(String newURL) /*@Configuration*/ { ... }

public void open() /*@Configuration(after=Open.class)*/
/*@Closed(after=Open.class)*/ { ... }

public String read() /*@Open*/ { ... }

public void close() /*@Open(after=Closed.class)*/ { ... }
}

Finally, here is some example code which demonstrates what errors are caught by the typestate checker:

void readMore(@Open RemoteResourceReader rrr) { ... }

void test() {
// initially in the 'configuration' state
RemoteResourceReader rrr = new RemoteResourceReader();

// ok: correct state
rrr.setUrl("http://something");

// error: not in the 'open' state
rrr.close();

// changing state from 'configuration' to 'open'
rrr.open();

// ok
String read = rrr.read();

// error: not in the 'configuration' state
rrr.setUrl("http://different");

// ok: parameter in the 'open' state
readMore(rrr);

// ok
rrr.close();

// error: parameter not in the correct state
readMore(rrr);
}

If you’d like to make experiments with the typestate checker on your own, go ahead and download it. The setup is really easy. And remember, that your feedback is very valuable and important!

I’d like to thank Michael Ernst and the rest of the JSR308 team for helping me with some questions that I had during development. The specification and framework is really good and worth taking a look at :)

Adam