Javarifier - Reference Immutability Inference Tool for Javari

Developed by the Javari team (javari@csail.mit.edu).

Contents:

• Motivation: Inferring reference immutability in Java programs
• Javarifier
  • Inference using existing Javari classes and stubs
• Installation
• Using Javarifier
  • Specifying a classpath
  • Outputting to a file
  • Specifying JDK jarfiles
  • Using stub classes
  • Understanding and debugging Javarifier output
  • Running Javarifier test suite
• Feedback
  • Update Log

Motivation: Inferring reference immutability in Java programs

Javarifier infers the immutability (according to the definition of the Javari language) of every reference in a Java program. In other words, it converts Java programs and libraries to Javari. It annotates source or .class format with backward-compatible comments or attributes.

Annotating programs aids developers in reasoning about the code and modifying it without introducing subtle mutation errors. Annotating libraries is important because Javari programs use libraries without Javari annotations often do not typecheck. Manually determining the mutability for each (public) parameter and return type is tedious and error-prone. Javarifier automatically performs this analysis.

Javarifier

Javarifier reads a set of Java classes to analyze (in .class format) and infers the (im)mutability of every reference. It outputs the inferred mutabilities in an annotation file, a textual file format for describing annotations of Java programs; the input class files are not modified. These annotations can be used directly, or inserted into either the .class files or the corresponding .java files using the annotation file utilities. If Javari annotations are inserted into the source code, they can be checked by the Javari type checker.

In earlier versions of Javari, methods must be invariant in the mutability of their parameters and return types. The newer definition of Javari used by both Javarifier and the Javari type checker permits covariant subtyping on parameters and contra-variant subtyping on return types.

Inference using existing Javari classes and stubs

Javarifier respects all existing Javari annotations in the program classes it analyzes. If any type is already annotated as @ReadOnly, Javarifier uses this annotation to determine the mutability of other types and does not change the existing @ReadOnly annotation. This mechanism is how Javarifier infers annotations on a program that uses libraries that have already been annotated using stub classes (also known as skeleton classes).

Installation

The following instructions assume either a Linux or Windows command-line environment.

The current distribution is Javarifier version 0.1.3, released April 27, 2008.

1. Download javarifier.zip.
2. Unpack the distribution zipfile by running:

     unzip javarifier.zip

   This command creates a directory named javarifier containing:

   • These instructions (javarifier.html)
   • The actual tool, javarifier
   • A lib directory containing libraries used by Javarifier
   • A src directory containing the source code of Javarifier (please contact us if you are interested in building from source)
   • The annotated-jdk directory, containing various classes of the JDK that have their method signatures annotated with Javari annotations.
3. Add the javarifier directory to your path.
   • For Unix, add the directory to your PATH environment variable.
     • For sh/bash, add to ~/.bashrc or ~/.bash_profile:

       export PATH=${PATH}:/path/to/javarifier/

     • For csh/tcsh, add to ~/.tcshrc or ~/.cshrc or ~/.login:

       setenv PATH=${PATH}:/path/to/javarifier/

   • For Windows, add the directory to your PATH system variable by going to

      Control Panel -> System -> Advanced -> Environment Variables 

     From there, find the PATH variable under “System variables” and append to it the javarifier directory.

Using Javarifier

The following instructions are for running javarifier on a Linux machine. The instructions are the same for Windows, except the tool is javarifier.bat, and you must use the Windows path names instead of the Linux path names.

The javarifier tool takes as arguments any number of fully-qualified names of the classes to analyze. All of these classes must be in your $CLASSPATH, although this behavior can be overriden with the -programCPEntries option. Here are examples:

javarifier myPackage.myClassOne myPackage.myClassTwo
javarifier myPackage.myClassOne myPackage.myClassTwo
javarifier `find myPackage -type f -name '*.java' | perl -p -e 's/\.java//g; s/\//./g'`

The last command above, if run in the parent directory of the myPackage source code directory, analyzes all classes in the package.

(Just using the default $CLASSPATH may not work, because the JVM may also load classes from other locations, such as the boot class path. An example is the classes in jdk/jre/lib/jce.jar. Therefore, you may need to add such jar files to CLASSPATH, or explicitly mention them on the javarifier command line via the -world option.)

Specifying a classpath

To specify a classpath other than $CLASSPATH for Javarifier to use to lookup classes being analyzed, you can use the -programCPEntries argument and pass in a full classpath. The first two of the following examples are identical.

javarifier myPackage.myClassTwo
javarifier myPackage.myClassTwo -programCPEntries $CLASSPATH
javarifier myPackage.myClassTwo -programCPEntries /path/to/classes1:/path/to/classes2

Outputting to a file

By default, all output, including the results, is printed to standard out. To output the results to an annotation file, use the -output option, followed by the name of the output file. Note that Javarifier outputs the results for all classes into a single file. For example:

javarifier myPackage.myClassOne myPackage.myClassTwo -output myPackage.jaif

Specifying JDK jarfiles

By default, Javarifier assumes that the JDK classes required by the program classes on which you are running Javarifier are in your CLASSPATH. For example, it assumes rt.jar is in your CLASSPATH. If this is not the case, or if you wish to reference a different JDK, you may use the -world option, followed by the classpath of your JDK jarfiles. For example:

javarifier myPackage.myClassOne myPackage.myClassTwo -world /jdk1.7.0/jre/lib/rt.jar:/jdk1.7.0/jre/lib/resources.jar:/jdk1.7.0/jre/lib/all-other-jars.jar

Using stub classes

A stub class (or skeleton class) gives Javari types for an external library. Javarifier comes with annotated versions of part of the JDK, in directory annotated-jdk.

If no stub class is available for a particular class, then Javarifier assumes that every reference in that class has @Mutable type. The -printStubs flag causes Javarifier not to perform inference, but only to output a list of classes for which stubs are needed.

There are two ways to inform Javari of additional stub classes (or fully-annotated Javari classes).

• Place the corresponding class files in the annotated-jdk directory. For example, to have Javarifier treat packageA.packageB.classC as a stub class, put its class file at:

  annotated-jdk/packageA/packageB/classC.class

  The class file must contain the Javari annotations. This is automatic if you use the JSR 308 compiler to compile a Javari program, or you can use the annotation file utilities to insert the annotations in any Java .class file.
• Provide Javarifier with an additional classpath to look for stub classes using the -stubs argument, followed by a classpath to containing stub classes. All classes found in that classpath will be treated as stub classes. For example:

   javarifier myPackage.myClassOne myPackage.myClassTwo -stubs /path/to/stubs1:/path/to/stubs2

If you create stub versions of additional classes (whether in the JDK or other libraries), please contribute them back to the Javari project (email javari@csail.mit.edu) so that we can include them in future releases.

Understanding and debugging Javarifier output

Javarifier may infer some references to be @Mutable that you believe should be @ReadOnly (or vice versa). This usually indicates a problem with your code such as a bug, a missing @Assignable keyword, or simply that you have misunderstood what your code does. Sometimes, it can indicate a bug in Javarifier.

To understand why Javarifier inferred a particular type qualifier, you can examine the constraints generated by Javarifier during its inference process. Use the -dumpConstraints flag, as in:

javarifier myPackage.myClass -dumpConstraints

The Javarifier constraints are of three types:

• A line of the form "U: c1" indicates that type in c1 must be mutable.
• A line of the form "G: c1 -> c2" indicates that if the type in c1 is mutable, then the type in c2 must be mutable.
• A line of the form "GG: c1 => c2 -> c3" indicates that if the types in both c1 and c2 are mutable, then the type in c3 must be mutable.

An example of a constraint is

  U: <Graph.createGraph.this: UNKNOWN LGraph;[] MUTABLE>

• This constraint indicates that the receiver (this) of method Graph.createGraph must be mutable.
• The string "LGraph;" is the JVML format for the Graph class.
• The string "UNKNOWN LGraph;[]" indicates that the mutability of the Graph has not yet been determined. (Due to the unguarded constraint, it will be mutable in the end.)
• MUTABLE represents the romaybe-context that the constraint is referring to; this is used for inferring romaybe (see the paper cited below for details). Often the constraints are the same across contexts, so you might have the following two constraints:

    U: <HashEntry.setNext.this: UNKNOWN LHashEntry;[] MUTABLE>
    U: <HashEntry.setNext.this: UNKNOWN LHashEntry;[] READONLY>

• For method receivers, the index -1 is used to refer to the receiver, as in the following constraint:

    U: <<Hashtable: int hashMap(java.lang.Object)>.-1: UNKNOWN LHashtable;[] MUTABLE>

• Local variables are named if the classfile has the LocalVariableTypeTable attribute. Otherwise, they are named by their index (e.g., "e0"), as are temporary variables, as in:

    U: <Graph.createGraph.$e0: UNKNOWN LVertex;[] READONLY>

You may find it helpful to cross-reference between Javarifier constraints and the Java source code of the classes being analyzed (from the constraints were generated).

For more details about the constraints, see the paper "Inference of reference immutability". Contact us if you need more help understanding the constraints.

Running Javarifier test suite

A test suite is included with the release. To run the test suite, go into the tests/ directory and run make. The output will indicate whether the tests passed or failed.

Feedback

Please send questions, comments, bug reports and feature requests to javari@csail.mit.edu. When reporting bugs, please help us to resolve the issue quickly by including the complete output of Javarifier, and exact instructions of how to reproduce a bug (including all necessary input files).

Update Log

• Version 0.1: (Released November 2, 2007) First release.
• Version 0.1.1: (Released February 15, 2008) Several bug fixes and updated documentation.
• Version 0.1.2: (Released March 7, 2008) Several bug fixes. Javarifier now works on the Eclipse compiler, which is over 120,000 lines of Java code.
• Version 0.1.3: (Released April 27, 2008)
  • Changed the @RoMaybe qualifier for parametric polymorphism over mutability to @PolyRead.
  • Changed the type rule for inferring @PolyRead to match an updated version of Inference of reference mutability, to appear in ECOOP '08, which outlines the inference algorithm used by Javarifier.
  • Better documentation of the -dumpConstraints command-line option and the format of its output.
  • Documented the -printStubs command-line option.
  • Included a test suite for testing Javarifier installation.

Last revised: March 10, 2008