Javarifier: Inference of reference immutability for Javari

Contents:

Motivation: Inferring reference immutability in Java programs

Javarifier divides the variables in a program into two groups: the variables the program mutates, and the variables that are never mutated. In other words, Javarifier infers the immutability of every reference in a Java program. Javarifier uses Javari's definition of immutability. Thus, Javarifier converts Java programs and libraries to Javari.

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 can produce a textual output file, or can annotate .java files with backward-compatible comments, or can annotate .class files with backward-compatible attributes. The algorithm for inferring Javari reference immutability is explained in the paper "Inference of reference immutability", which appeared at ECOOP 2008.

Javarifier

Javarifier's input is Java .class files. Javarifier's output is an annotation file, a textual file format for describing annotations of Java programs; the input class files are not modified. The annotation file can be used by a tool such as the annotation file utilities, which inserts the annotations into either the .class files or the corresponding .java files. If Javari annotations are inserted into the source code, they can be checked by the Javari type checker.

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.

Differences from previous versions of Javari

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.

Installation

The current distribution is Javarifier version 0.1.4, released September 18, 2010.

The following instructions assume either a Unix-like (e.g., Linux, Mac) or Windows command-line environment.

  1. Install the Checker Framework and the Annotation File Utilities, in sibling directories; for example, ~/jsr308/checker-framework/ and ~/jsr308/annotation-tools/.
    Neither is strictly necessary to run Javarifier, but you almost certainly want both of them. Javarifier uses the Checker Framework's annotated JDK, when available. You will use the Annotation File Utilities to insert Javarifier's output into .java or .class files, and the Checker Framework to type-check the Javari annotations in .java files.
  2. Download javarifier.zip.
  3. Unpack the distribution zipfile, as a sibling of the Checker Framework (for example, in ~/jsr308/javarifier/) by running:
      unzip javarifier.zip
  4. Add the javarifier/scripts directory to your path.

Using Javarifier

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

The javarifier tool takes as arguments any number of fully-qualified names of the classes to analyze. For example:

javarifier myPackage.myClassOne myPackage.myClassTwo
To analyze all classes in a package myPackage, run the following in its parent directory:
javarifier `find myPackage -type f -name '*.java' | perl -p -e 's/\.java//g; s/\//./g'`

Specifying a classpath

All of the classes being analyzed must be on the path specified by the --programCPEntries option, which defaults to $CLASSPATH.

If you get an error "couldn't find class: ... (is your soot-class-path set properly?)", then the problem may be that you did not set --programCPEntries.

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

These two examples are identical:

javarifier myPackage.myClassTwo
javarifier myPackage.myClassTwo --programCPEntries $CLASSPATH

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 library jarfiles

The program on which you are running Javarifier may depend on the JDK and other libraries. By default, Javarifier assumes that those libraries are on 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 gives Javari types for an external library. The Checker Framework comes with annotated versions of part of the JDK, which Javarifier uses by default.

To inform Javari of additional stub classes (or fully-annotated Javari classes), use 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/stubs/dir:/path/to/stubs.jar

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.

If you get the error "Missing stub for class ...", then your stub library is missing the given class, or you have not specified the stub library location properly.

If you create stub versions of additional classes (whether in the JDK or other libraries), or if you improve existing libraries by adding annotations to them, please email them to javarifier-dev@googlegroups.com so that we can include them in future releases.

Applying heuristics to exclude fields from the abstract state

Javarifier implements several heuristics for inferring which fields should be excluded from the abstract state of an object. These heuristics may infer the @Assignable and @Mutable field annotations, and these annotations may affect the end results of Javarifier. To apply these heuristics, use the --applyHeuristics flag, as follows:

javarifier myPackage.myClass --applyHeuristics

These heuristics only apply to private, non-static, non-final fields. The following is a list of all heuristics currently implemented.

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.

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

To understand why Javarifier inferred a particular type qualifier, you can enumerate the causes for each qualifier. Use the --dumpCauses flag, as in:

javarifier myPackage.myClass --dumpCauses

For each annotation, this outputs the shortest-length inference tree. Each node of the tree is a cause, which explains why a particular variable is not readonly. That cause may refer to other variables, and the rest of the tree explains why those variables are not readonly. The tree is at most binary — each node has 0, 1, or 2 children. Most nodes have 1 child, making most of the tree a chain.

A cause consists of three pieces of information, each printed on its own line:

When the explanation mentions one other variable (e.g., when the constraint leading to mutability of a is "b → a"), the cause for the other variable is printed directly below, at the same indentation level. When the explanation mentions two other variables (e.g., when the constraint leading to mutability of a is "c → b → a"), the cause for the first variable is printed indented, after the word "GUARD", and the cause for the second variable is printed directly below, without any extra indentation.

Here is an abstract example of the output:

<Var1>
  ClassName:53: Stmt1 
  Var1 <: Var2 
<Var2>
  ClassName:: MemberName Stmt2 
  Why Var3 and Var4 implies Var2
GUARD:
  <Var3>
    ClassName:: MemberName Stmt3
    Why Var3 is directly apparent
<Var4>
  ClassName:: MemberName
  Stub

If the cause tree is not sufficient to understand the output, then you can also examine the raw 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:

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).

An example of a constraint variable is:

  <Graph.createGraph.this: UNKNOWN Graph[] MUTABLE>

It contains the following parts:

Running the Javarifier test suite

To run the test suite, do any one of the following commands:

  ant run-tests
  make -C tests
  cd tests; make

Command-line options

Building from source

To build Javarifier from source, run the following commands:

  1. Set environment variables. Add the following to your ~/.bashrc or equivalent, then log out and log back in:
    export JSR308=$HOME/jsr308
    export PATH=$JSR308/jsr308-langtools/dist/bin:${PATH}
    export CLASSPATH=${CLASSPATH}:...JAVA_HOME.../lib/tools.jar:$JSR308/checker-framework/checkers/checkers.jar
  2. Obtain the source code.
    mkdir -p $JSR308
    cd $JSR308
    hg clone https://jsr308-langtools.googlecode.com/hg/ jsr308-langtools
    hg clone https://checker-framework.googlecode.com/hg/ checker-framework
    hg clone https://annotation-tools.googlecode.com/hg annotation-tools
    hg clone https://javarifier.googlecode.com/hg/ javarifier
  3. Build everything. If any of the builds fails, consult that project's documentation.
    cd $JSR308/jsr308-langtools/make \
    && ant clean build-javac build-javap \
    && cd $JSR308/checker-framework/checkers \
    && ant dist all-tests \
    && cd $JSR308/annotation-tools \
    && ant \
    && cd $JSR308/javarifier \
    && ant jarfile

Later, to update all your sources and rebuild them, you can run:

cd $JSR308/jsr308-langtools
hg pull -u
cd $JSR308/checker-framework
hg pull -u
cd $JSR308/annotation-tools
hg pull -u
cd $JSR308/javarifier
hg pull -u

and re-run the "Build everything" command immediately above.

Some additional notes appear in the README file.

Compiling with Eclipse

The structure of the src/ and bin/ directories is such that Eclipse can understand the Javarifier as a project, overwrites class files in the same bin/ directory the build.xml script uses, and the build.xml file does not conflict with the .classpath and .project files that Eclipse uses. Therefore, you can safely use Eclipse for working on the Javarifier, but before committing code changes you should make sure that the code compiles using the build script.

Feedback

If you encounter a problem in Javarifier, please submit a bug report via its issue tracker. 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).

Other questions, comments, and feature requests can be sent to javarifier-dev@googlegroups.com.

Release notes


Last revised: August 31, 2010