Inference of Pluggable Type Systems

A general inference framework for context-sensitive pluggable type systems.

Extends the Checker Framework
Currently supports inference of Universe Types, Ownership Types, Reference Immutability and EnerJ.
Download: checker-inference.tar.gz (Apr 2, 2012)
NOTE: It uses a modified jsr308-langtools. The latest jsr308-langtools at http://types.cs.washington.edu/jsr308/ is not compatible with checker-inference

The following instructions assume either a Unix-like (e.g., Linux, Mac).

Download checker-inference.tar.gz. It contains a modified jsr308-langtools, extended Checker Framework and Annotation File Utilities.
Unpack the distribution tar file by running:
```
  tar xvfz checker-inference.tar.gz
```
There are three folders: annotation-tools, checker-framework and jsr308-langtools.
Add the checker-inference/checker-framework/checker/binary directory to your path.

Test Run: Type "javac-ri" in the command line. If you can see

  javac: no source files or class names
  Usage: javac <options> <source files>
  use -help for a list of possible options

Then the installation is successful.

Infer the immutable references for the Jolden/BH program in the benchmark folder.

          cd checker-inference/checker-framework/checker/
          ./binary/javac-ri benchmark/jolden/bh/*.java

The inference results are dumped to:

result.jaif: The result in JAIF format containing fields, parameters and return values, but no local variables.
ri-result.csv: The result for all variables
pure-methods.csv: The pure methods inferred by the tool.

Inferring Universe Types and Ownership Types is similar. Just change javac-ri to javac-ut or javac-ot.

To be done

A newer version is released. (Apr 2, 2012)
Our paper describing this framework has been accepted by ECOOP 2012. (Feb 29, 2012)