Home

Gradual Ownership Types are a framework to annotate programs with ownership types in a lightweight way, allowing only partial information about object owners to preserve the Owners-as-Dominators property for the object graph of a program. The front-end compiler is implemented for Java 1.4 via JastAdd as an extension of JastAddJ: The JastAdd Extensible Java Compiler.

The formal description of the framework is available in the paper "Gradual Ownership Types" presented at ESOP 2012 or in the accompanying technical report.

The compiler performs type-checking on the provided source files and generates translated source files with inserted dynamic checks if the key -gen is provided.

Download

The front-end compiler for Java 1.4 with Gradual Ownership Types is available for use, experiments and extension.

Build

All tools needed (jastadd2, jflex, beaver, etc.) are included into the archive with sources. You only need to have javac and Apache Ant installed in order to build. The ant script build.xml is located in the root folder of the archive. Inspect the README file for more information about the project structure.

To build the jar file with the compiler, run

ant rebuild.all

To run compiler tests:

ant run.tests

To create an executable jar file:

ant jar

To zip sources:

zip.sources

Run

How to run the OwnershipChecker (with a built executable jar):

java -jar OwnershipChecker.jar java-source-files

See what options are available, e.g., for optional generation of sources with dynamic checks inserted:

java -jar OwnershipChecker.jar

Example

class E /*<P>*/ {
  // the owner of myD is NOT specified
  D myD = new D /*<P>*/();
}

class D /*<owner>*/ {
  // the owner of e is specified
  E /*<owner>*/ e;
  
  void use(D /*<owner>*/ arg) { 
    System.out.println(arg.toString()); 
  }
  
  void exploit(E /*<owner>*/ arg) { this.e = arg; }

  void test() {
    final E e = new E /*<this>*/();
    // exact owner of d is unknown
    final D d = e.myD;
    // safe argument passing
    // owners of the receiver and the argument are equal
    d.use(d);
    // non-safe argument passing
    // dynamic type cast will be inserted
    d.exploit(e); 
  }
}

License

The sources are released under CRAPL license.

If you have questions or concerns about the CRAPL, or you need more information about this license, please contact Prof. Matthew Might.