Javarifier: Inference of reference immutability for Javari

Contents:

• Motivation: Inferring reference immutability in Java programs
• Javarifier
  • Inference using existing Javari classes and stubs
  • Differences from previous versions of Javari
• Installation
• Using Javarifier
  • Specifying a classpath
  • Outputting to a file
  • Specifying library jarfiles
  • Using stub classes
  • Applying heuristics to exclude fields from the abstract state
  • Understanding and debugging Javarifier output
    • Printing the cause tree
    • Printing constraints
    • Printing a constraint variable
  • Running the Javarifier test suite
  • Command-line options
• Building from source
  • Compiling with Eclipse
• Feedback
  • Release notes

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.

0. 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.
1. Download javarifier.zip.
2. Unpack the distribution zipfile, as a sibling of the Checker Framework (for example, in ~/jsr308/javarifier/) by running:

     unzip javarifier.zip

3. Add the javarifier/scripts directory to your path.
   • For Unix, add the directory to your PATH environment variable. If you use the sh or bash shell, add to ~/.bashrc or ~/.bash_profile:

     export PATH=${PATH}:${HOME}/jsr308/javarifier/scripts/

   • 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 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

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. (One reason this can happen is that you are using JDK 7. You may need to add, to the Checker Framework's annotated JDK, stubs for classes that are new in JDK 7.)

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.

• A field that is only written to in the constructor or in the equals() and hashCode() methods is inferred to be @Assignable.
• If a class implements the equals() method, any field that is not read in the equals() method is inferred to be @Assignable.
• A field that is written to in a method that overrides either Iterator.next() or Enumeration.nextElement() is inferred to be @Assignable.

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.

Printing the cause tree

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:

• Constraint variable (not a program variable!) of a variable that is not readonly. (TODO: check that.) See below for an explanation of its formatting.
• Source code information: location and pseudocode.
  • The location takes one of three forms:
    • “ClassName:LineNumber:”, if debug information (-g compiler flag) is available
    • “ClassName:: methodName”, if debug information is not available
    • empty, if Javarifier has no source information for the constraint (such as if the constraint came from a stub file, or subtyping constraints in overriding relationships)
  • The pseudocode represents an assignment of the form "$e1 = $e2;", "name.field = $e2", "name[...] = $e3", etc., where $en indicates a variable introduced by Javarifier.
• An explanation. This is sometimes the constraint that Javarifier generates from the source code construct, and other times is an English description. A common explanation to appear at the end of a cause chain is "Stub", which indicates that the variable is known via a stub declaration.

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

Printing constraints

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:

• A line of the form "U: c1" indicates that the type in c1 must be mutable. See below for an explanation of constraint variable formatting. An example of a constraint is

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

  This constraint indicates that the receiver (this) of method Graph.createGraph 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.

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

Printing a constraint variable

An example of a constraint variable is:

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

It contains the following parts:

• The variable name from tho source code.
  • 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 Hashtable[] ctx:m>

  • 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 Vertex[] ctx:r>

• The type, including mutability. In this case, the string "UNKNOWN Graph[]" indicates that the mutability of the Graph has not yet been determined. (Due to the unguarded constraint, it will be mutable in the end.)
• ctx:m represents the romaybe-context that the constraint is referring to; this is used for inferring romaybe (see the paper "Inference of reference immutability" for details). Often the constraints are the same across contexts, so you might have the following two constraints:

    U: <HashEntry.setNext.this: UNKNOWN HashEntry[] ctx:m>
    U: <HashEntry.setNext.this: UNKNOWN HashEntry[] ctx:r>
  

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

• General Options
  • -h -help --help=boolean. Print the short usage message. This does not include verbosity or debugging options. [default false]
  • -H --allHelp=boolean. Print the extended usage message. This includes verbosity and debugging options but not internal options. [default false]
  • -v -version --version=boolean. Print the current Javarifier version. [default false]
• Execution Options
  • -Q --reallyQuiet=boolean. Be quiet, do not print much information. [default false]
  • --applyHeuristics=boolean. Use heuristics to set fields that should be excluded from the abstract state of the object to be assignable. See: javarifier.HeuristicsVisitor. [default false]
  • --openWorld=boolean. Forces all public method return types to have mutable (or polyread) types and all public fields to have this-mutable types. See: javarifier.OpenWorld. [default false]
• Input Options
  • --programCPEntries=string. Specify a colon-delimited classpath other than $CLASSPATH for Javarifier to use to look up classes being analyzed.
  • --stubs --stubCPEntries=string. Specify a colon-delimited classpath to look for stub classes. All classes found in this path will be treated as stub classes.
  • --world --worldCPEntries=string. By default, Javarifier assumes that the JDK classes required by the program classes on which you are running Javarifier are in your $CLASSPATH. If this is not the case, or if you wish to reference a different JDK, you may use this followed by the colon-delimited classpath of your JDK jarfiles.
  • --useWorldAsStubs=boolean. If false (the default), then missing stubs cause Javarifier to halt. If true, then Javarifier uses world classes as stubs, after both the default stub entries and the stub entries. [default false]
  • --extraAnnotationInputFile=filename. If specified, annotations will be loaded from this annotation file as well as the class files for all classes in the Soot scene.
• Output Options
  • --output --outputFile=filename. By default, all output, including the results, is printed to standard out. Use this option to output the results to an annotation file. Note that Javarifier outputs the results for all classes into a single file.
  • --outputFormat=format. Specify the output annotation format. See javarifier.OutputFormat for a description of these formats. [default JAIF]
  • --outputFilterLocals=boolean. Tells ScenePrinter to omit a bunch of uninteresting local variables from the output. These are generally the ones that cannot be annotated in source code, so this option is good for comparing Javarifier results with manual annotations. [default false]
  • --outputLimitKind=construct. Tells ScenePrinter to output "omitted" instead of the type for elements not of the given construct. The construct can be "field", "local", "parameter", "receiver", or "return". Useful to study the types assigned to elements of each kind separately.
  • --outputSortMembers=boolean. Tells ScenePrinter to output fields and methods sorted by name instead of by order of appearance in the class file. If several methods have the same name, they are outputted in the order they appear in the class file. [default false]
  • --outputMainClassFirst=boolean. Tells ScenePrinter to output all the classes mentioned on the command line (in the order of first mention on the command line) before all the other classes. [default false]
  • --skipEmpty=boolean. The skipEmpty flag indicates that annotations should not be outputted for empty code. That is, there should be no annotations for interfaces and abstract methods. [default false]
  • --includeImmutableClasses=boolean. The includeImmutableClasses flag indicates that @ReadOnly annotations should be output even for references that are of some type that is known to be @Unmodifiable, such as java.lang.String. [default false]
• Utility Options (no inference)
  • --justPassThrough=boolean. Do not perform inference. Just read annotations (treating even program classes as fully annotated), expand defaults and @Unmodifiable, and write the results back out. Use this mode to convert manual annotations to a form in which they can be compared to Javarifier annotations. [default false]
  • --printStubs=boolean. Do not perform inference. Just output a list of classes for which stubs are needed to perform inference. In the future, an option such as --missingStubs may be added, which only outputs a list of stubs that are needed but missing. [default false]
• Verbosity Options
  • --dumpCauses=boolean. Enumerates the causes for each type qualifier Javarifier infers. For each annotation this outputs the shortest-length inference chain. See the manual section on "Printing the cause tree". [default false]
  • --dumpConstraints=boolean. Dump the raw constraints generated by Javarifier during its inference process. See the section on -dumpConstraints in the manual for information. [default false]
  • --dumpResults=boolean. Dump results. [default false]
  • --dumpGeneratorConstraints=boolean. Dump generator constraints. See: javarifier.ConstraintGenerator. [default false]
  • --dumpBoundGuards=boolean. Dump bound guards. See: javarifier.BoundGuarder. [default false]
  • --dumpParamCons=boolean. Dump parameter constraints. See: javarifier.ParameterConstraints. [default false]
  • --dumpStubCons=boolean. Dump stub constraints. See: javarifier.StubConstraints. [default false]
  • --dumpSubtypeCons=boolean. Dump subtype constraints. See: javarifier.SubtypeConstraints. [default false]
  • --dumpOpenWorldCons=boolean. Dump open world constraints. See: javarifier.OpenWorld. [default false]
• Debugging Options
  • --debugLocalSplitting=boolean. Debug local splitting. See: soot.toolkits.scalar.LocalSplitter. [default false]
  • --debugStubs=boolean. Debug stubs. [default false]
  • --debugResolver=boolean. Debug signature resolver. See: javarifier.TypeInitializer. [default false]
  • --debugResolve=boolean. Debug Soot resolver. See: soot.SootResolver. [default false]
  • --debugTypeInference=boolean. Debug type inference. See: javarifier.TypeInferencer. [default false]
  • --debugBoundGuarder=boolean. Debug bound guarder. See: javarifier.BoundGuarder. [default false]
  • --debugSubtyping=boolean. Debug subtyping. See: javarifier.ConstraintManager. [default false]
  • --debugConstraintGeneration=boolean. Debug constraint generation. See: javarifier.ConstraintGenerator, javarifier.ConstraintManager. [default false]
  • --debugConstraints=boolean. Debug constraints. See: javarifier.ConstraintTracker#printCauses. [default false]
  • --debugSigParser=boolean. Debug signature parser. See: javarifier.JVMLSigParser. [default false]
  • --debugConstraintIncorporating=boolean. Debug constraint incorporating. See: javarifier.Incorporater. [default false]
  • --debugAnnotationLoading=boolean. Debug annotation loading. See: javarifier.AnnotationScene. [default false]
  • --debugAnnotationStoring=boolean. Debug annotation storing. See: javarifier.AnnotationStorer. [default false]
• Internal Options
  • --defaultStubCPEntries=string. Set the default classpath for stub classes.
  • --defaultWorldCPEntries=string. Set the default classpath for JDK jarfiles.

Building from source

To build Javarifier from source, run the following commands:

1. Set environment variables. Add the following to your ~/.bashrc or equivalent. Set the JAVA_HOME environment variable to the location of your JDK 7 installation (not the JRE installation). Then log out and log back in:

   export JAVA_HOME=/path/to/your/jdk
   export JSR308=$HOME/jsr308
   export PATH=$JSR308/jsr308-langtools/dist/bin:${PATH}
   export CLASSPATH=${CLASSPATH}:$JAVA_HOME/lib/tools.jar:$JSR308/checker-framework/checkers/binary/checkers.jar

2. Obtain the source code.

   mkdir -p $JSR308
   cd $JSR308
   hg clone https://code.google.com/p/jsr308-langtools/ jsr308-langtools
   git clone https://github.com/typetools/annotation-tools.git annotation-tools
   git clone https://github.com/typetools/checker-framework.git checker-framework
   git clone https://github.com/typetools/javarifier.git 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

• 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. Matches Inference of reference mutability, which appears in ECOOP '08.
  • 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.
• Version 0.1.4: (Released September 18, 2010)
  • Implemented and documented the heuristics for excluding fields from the abstract state of an object. See --applyHeuristics.
  • Refactored the package containing all the Javari annotations from checkers.quals to checkers.javari.quals
  • Command-line options now start with a double-dash prefix instead of a single-dash prefix. Run javarifier -h for a list, or javarifier -H for a full list.
  • Improved diagnostic output (see --dumpCauses). Removed some unnecessary and uninformative messages from output.
  • The Javarifier release no longer includes a copy of the annotated JDK. A Javarifier user should get the annotated JDK by installing the Checker Framework.
  • Account for updates to scene library and Type Annotations specification.
  • Add Eclipse .project and .classpath files.
  • Many bug fixes to code, build files, and tests.
  `
  • Uses plume-lib (plume.jar added to lib/).

Last revised: August 31, 2010