Contents:
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'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.
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.
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.
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.
unzip javarifier.zip
export PATH=${PATH}:${HOME}/jsr308/javarifier/scripts/
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.
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.myClassTwoTo 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'`
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
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
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
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.
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.
equals()
and hashCode()
methods is inferred to be @Assignable
.
equals()
method, any field that
is not read in the equals()
method is inferred to be @Assignable
.
Iterator.next()
or Enumeration.nextElement()
is inferred to be @Assignable
.
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:
U: <Graph.createGraph.this: UNKNOWN Graph[] MUTABLE>
This constraint indicates that the receiver (this
) of method
Graph.createGraph
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).
An example of a constraint variable is:
<Graph.createGraph.this: UNKNOWN Graph[] MUTABLE>
It contains the following parts:
U: <<Hashtable: int hashMap(java.lang.Object)>.-1: UNKNOWN Hashtable[] ctx:m>
U: <Graph.createGraph.$e0: UNKNOWN Vertex[] ctx:r>
U: <HashEntry.setNext.this: UNKNOWN HashEntry[] ctx:m> U: <HashEntry.setNext.this: UNKNOWN HashEntry[] ctx:r>
To run the test suite, do any one of the following commands:
ant run-tests make -C tests cd tests; make
javarifier.HeuristicsVisitor
. [default false]javarifier.OpenWorld
. [default false]javarifier.OutputFormat
for a description of these formats. [default JAIF]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]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.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]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]-dumpConstraints
in the manual
for information. [default false]javarifier.ConstraintGenerator
. [default false]javarifier.BoundGuarder
. [default false]javarifier.ParameterConstraints
. [default false]javarifier.StubConstraints
. [default false]javarifier.SubtypeConstraints
. [default false]javarifier.OpenWorld
. [default false]soot.toolkits.scalar.LocalSplitter
. [default false]javarifier.TypeInitializer
. [default false]soot.SootResolver
. [default false]javarifier.TypeInferencer
. [default false]javarifier.BoundGuarder
. [default false]javarifier.ConstraintManager
. [default false]javarifier.ConstraintGenerator
, javarifier.ConstraintManager
. [default false]javarifier.ConstraintTracker#printCauses
. [default false]javarifier.JVMLSigParser
. [default false]javarifier.Incorporater
. [default false]javarifier.AnnotationScene
. [default false]javarifier.AnnotationStorer
. [default false]To build Javarifier from source, run the following commands:
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
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
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.
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.
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.
@RoMaybe
qualifier for parametric
polymorphism over mutability to @PolyRead
.
@PolyRead
. Matches
Inference of reference mutability, which appears in ECOOP '08.
--dumpConstraints
command-line option and the format of its output.
--printStubs
command-line option.
--applyHeuristics
.
checkers.quals
to
checkers.javari.quals
Last revised: August 31, 2010