Werner M. Dietl

Electrical and Computer Engineering, University of Waterloo

ABDCFE: A Beautifully Designed Checker Framework Experience

Or: A Better Documented Checker Framework Experience Werner Dietl, <wdietl@uwaterloo.ca>

Some thoughts, accumulating all our recent discussions on many topics: the meaning of annotations on a constructor, on type parameters, etc. I will present type rules as the set of constraints that have to hold — allowing us to discuss both static checking and type inference. I will also mix in runtime interpretations - assuming that for some type system we would want runtime type information.

The end result of this discussion should be a clearer understanding of what we want as the default behavior of the Checker Framework — embodied in the BaseTypeVisitor/InferenceTypeVisitor.

The discussion is still on the current annotation abstraction. However, we should keep going from annotations to qualifiers in the back of our minds.

Many of the issues were previously only discussed in person; let me know if any of this write-up is not how you interpreted things. Sorry for taking so long with this message - it kept growing in scope and at some point I even switched to LaTeX and later to AsciiDoc. Mike suggested sending the current status to continue the discussion. Also, the terminology is probably still inconsistent, depending on the day I got to work on the message.

Consider this a very rough draft/outline of what I eventually want.

1. Preliminaries

1.1. Notation

For two qualifiers q1 and q2, we write q1 <: q2 to create a subtype constraint between the qualifiers. In type checking mode, … In type inference mode, …

For two qualified types t1 and t2, we write t1 <: t2 to create a subtype constraint between the types, which is broken down according to Java rules: go to a common super class, invariant type arguments, etc.

Viewpoint adaptation: we already have methodFromUse, constructorFromUse, and typeVariablesFromUse functions. We should raise the abstraction for these and introduce a separate function for viewpoint adaptation adapt that takes two types (and also some enum or a tree???) and returns the adapted type. The standard implementation for the other functions then simply distribute viewpoint adaptation.

We currently have three different isValidUse functions (reference, primitive, arrays) that take the use-type and source Tree (and declaration type for references). Instead I propose having a single isValidUse function that takes the use-type, a new enum that characterizes the location, and a Tree (or should it be a TreePath) to the type use. The enum can then also be used in a meta-annotation (something like @ValidAt or @ValidFor) to declaratively define isValidUse. Constants would be NEW, PARAMETER, RETURN, etc.

The type validator calls isValidUse recursively on each component of a type, changing the enum and tree accordingly (maybe not the tree?) That is, each invocation only sees an erased type. Do we want to keep this behavior?

2. Open Issues

Logging framework
Do we want a "defaulting" mode, which applies the defaults from a type checker to the code, but does not perform type checks. Google thinks this would improve performance for their use cases.

3. Design Goals

Use interfaces and default implementations
Limit use of reflection
Do continue to use meta-annotations on type qualifiers
Do we want to keep the @TypeQualifer annotation? We currently don’t check its presence. We use checkers.quals.TypeQualifier. Should we use/alias http://jsr-305.googlecode.com/svn/trunk/javadoc/javax/annotation/meta/TypeQualifier.html? After renaming, this qualifier would be org.checkerframework.quals.TypeQualifier.
Plan for inference from the beginning
Limit use of javac compiler internals to a few utility classes. Using com.sun.source is necessary for AST access. Avoid anything below com.sun.tools.
Considerations for effect systems like purity?
Considerations for type-state systems like KeyFor?
Careful when comparing AnnotationMirrors.

4. Projects

The following is a list of the projects that are part of the Checker Framework.

External dependencies are to jsr308-langtools and junit.

The build of the annotated JDK also depends on annotation-tools. The source code however does not depend on annotation-tools.

4.1. `javacutil`

A library of useful functions building on OpenJDK’s javac.

The goal is that other projects should use javacutil instead of directly accessing javac implementation details.

A long-term goal could be to use something like this as an abstraction between our code and javac vs. Eclipse vs. other Java compilers.

Previously, this project was called javacutils.

4.1.1. Open issues

document naming conventions and ensure consistency (e.g. plural vs. singular)
ensure other projects use javacutil instead of directly accessing javac details.

4.1.2. Dependencies

This project does not depend on any other Checker Framework projects and provides basic utilities.

4.1.3. Package name

Current package name: javacutils

New package name: org.checkerframework.javacutil

4.2. `dataflow`

A dataflow framework built on top of OpenJDK’s javac.

4.2.1. Dependencies

This project only depends on javac and javacutil.

4.2.2. Package name

Current package name: dataflow

New package names: org.checkerframework.dataflow

4.3. `stubparser`

A parser for stub files, which is Java with a few variations.

Previously, this project was called javaparser.

4.3.1. Open issues

Receiver syntax change
Java 8 features

4.3.2. Dependencies

This project does not depend on any other Checker Framework projects and provides basic utilities.

Needs javacc to regenerate.

4.3.3. Package name

Current package name: cfjapa with a single parser sub-package.

New package name: org.checkerframework.stubparser without sub-package parser

4.4. `framework`

The "framework" parts of the Checker Framework project.

At the moment, there is only a single checkers project that mixes both framework classes and example type systems. I suggest we create a new framework project only for the framework parts and a separate checkers project for the example type systems, explained below.

4.4.1. Open issues

There will be a developer manual here, which focuses on Checker Framework development and a "user manual" in the checkers project, which focuses on the example type systems.

4.4.2. Dependencies

This project depends on javacutil, dataflow, and stubparser.

4.4.3. Package name

Current package name: checkers, mixed with example type systems

Possible new package names:

org.checkerframework.core
org.checkerframework.framework (repeats the framework part and is long)

The following current packages comprise the "framework":

checkers.source (suggested new name org.checkerframework.core.source)
checkers.types (suggested new name org.checkerframework.core.type)
checkers.quals (suggested new name org.checkerframework.core.qual)
checkers.flow (suggested new name org.checkerframework.core.flow)
checkers.util (suggested new name org.checkerframework.core.util)

(The classes in these packages should be carefully examined and restructured. In particular, the transition to QualifiedType will cause improvements to the structure.)

Package names should be singular.

The following two type checkers are implementations of the "core" framework:

checkers.basetype (suggested new name org.checkerframework.common.basetype)
checkers.subtyping (suggested new name org.checkerframework.common.subtyping)

they provide advanced functionality and convenience like meta-annotations to declare defaulting and subtyping.

We want to enable reflection-awareness for most type systems, meaning the following should also be part of the framework:

checkers.value (suggested new name org.checkerframework.common.value)
checkers.reflection (suggested new name org.checkerframework.common.reflection)

To distinguish these four type checkers from the core features and from example type checkers, they are in the checkerframework project, but in a separate package, org.checkerframework.common. (common is a bland name; is standard better?)

4.5. `inference`

The main framework project will be written in a style suitable for both type checking and inference.

This project will provide specific implementations that are needed only for inference, e.g. generally usable solvers.

4.5.1. Open issues

4.5.2. Dependencies

This project builds on framework.

4.5.3. Package name

Current package name: checkers.inference

New package name:+org.checkerframework.inference+

4.6. `checker`

Example type checkers illustrating how to use the Checker Framework.

Previously, this project was called checkers.

4.6.1. Open issues

Type systems like the Nullness Checker are intended for production use. Others are simple examples, but not meant for actual use.
Add more tutorial type systems, very well documented type systems that explain all features, but might not have an actual use case.

4.6.2. Dependencies

This project depends on all other projects.

4.6.3. Package name

Current package name: checkers

New package name: org.checkerframework.checker

4.7. Transition

One big question is how we can most elegantly transition from the current setup, using AnnotatedTypeMirror, to a system using QualifiedType that build on top of AnnotatedTypeMirror, to a system that only uses QualifiedType.

What package names should we use for the different phases?

Should we use separate branches or separate repositories?

5. Architecture

TODO

6. What the bleep is viewpoint adaptation?

Viewpoint adaptation is the idea of interpreting a type relative to the current "context". If the context changes, e.g. because of a field access, the type needs to be adapted to account for the change of context.

As an example, take standard type polymorphism:

class MyList<T> { T f; }

MyList<String> mls = ...;
String s = mls.f;

The declared type of field f is T. However, the type needs to be adapted depending on the receiver of a field access, e.g. mls.f has type String.

I’ve used similar ideas for non-polymorphic settings, where only the type annotations of a type are adapted depending on the viewpoint.

Required reading: my thesis.

7. Use of type annotations

Viewpoint adaptation is everywhere

I want to propose the following semantics for the standard checker, in particular for constructors and object creation. Let me call it the "viewpoint adaptation" interpretation. I will also argue why this interpretation is consistent with method invocations and field accesses.

Let’s take the following source code:

@OnClass
class MyClass extends @OnExt Super implements @OnImpl Intf {
  @OnField Data f;

  @OnConstructor
  MyClass(@OnCParam Data p) {
    this.f = p;
  }

  @OnConstructor2
  MyClass(@OnCParam2 int p) {
    this.f = new @OnNewData Data(p);
  }

  @OnRet Data foo(@OnReceiver MyClass this, @OnParam Object p) {
    return f;
  }
}

class SomeOtherClass {
  void annotated(@OnDataPar Data dp) {
    @OnLocal MyClass local = new @OnNew MyClass(dp);
    @OnDataLoc Data dl = local.foo(dp);
  }

  void empty(Data edp) {
    MyClass elocal = new MyClass(dp);
    Data edl = local.foo(dp);
  }
}

7.1. Constructors

Let’s start with the first constructor:

  @OnConstructor
  MyClass(@OnCParam Data p) {
    this.f = p;
  }

The type of "this" within the constructor for most type systems will be "@OnConstructor MyClass<T>". The type of the parameter p is relative to the current object "this".

How much adaptation of type of f do we need?

Of course, some type systems need different interpretations; e.g. the Initialization Checker changes the type of "this" within a constructor depending on what super-constructors have been called and what field set.

7.1.1. Things to check

isValid(@OnConstructor MyClass<T>, CONSTRUCTOR_RETURN)
isValid(@OnCParam Data, CONSTRUCTOR_PARAM)
typeof(p) <: adapt(@OnConstructor MyClass<T>, typeof(f)) TODO

7.2. Object creation

Let us now consider the invocation of that constructor:

  void annotated(@OnDataPar Data dp) {
    @OnLocal MyClass local = new @OnNew MyClass(dp);
  }

instantiation as viewpoint adaptation of declared constructor?

MyClass(@A Data p)
new @B MyClass(@C Data)
checks "@B MyClass" |> MyClass(@A Data p)

7.2.1. What qualifiers can occur in an instantiation?

We need to make a distinction between qualifiers that describe a property of a reference and qualifiers that describe a property of the referenced object. For some type systems these two sets are equal, but for others they are not.

For the Nullness Checker, objects are always @NonNull and there is no "null" object. Constructor invocation requires @NonNull. A reference however can be either @NonNull or @Nullable: the reference is either attached to a concrete object or not.

For IGJ/Javari an object is either @Mutable or @Immutable. A reference can additionally be @ReadOnly. It never makes sense to create a @ReadOnly object.

For ownership systems, an object is created with a concrete owner; references might abstract the owner. It never makes sense to create an object without an owner.

For the regex system, a concrete String either is not a regex, or has a specific matching group number. A reference gives an abstraction of this - giving a lower bound on the number of matching groups.

I agree that we could allow the respective superqualifier in an object creation and interpret it like assigning to a variable of that supertype. I have the following semantic issue with this interpretation: assume we have runtime type information. At object creation time we need to store the concrete type of the object in the heap. If we have only the supertype, we cannot decide what concrete type to use. If we allow "new @Readonly Object()" we don’t know what type to store in the new object.

I don’t see a reason to allow this, either. If an assignment to a supertype is required, standard subsumption will give us the desired type. Also, there is no overloading based on type qualifiers.

7.2.2. Things to check

7.3. Qualifiers on a class declaration

7.3.1. Things to check

7.4. Qualifiers on extends/implements

7.4.1. Things to check

8. Things to check for expressions

Only expressions that don’t contain type uses. Those are above.

8.1. Method invocations

8.1.1. Things to check

8.2. Casts

8.2.1. Discussion

The "casting" interpretation of object creation is: "new @Q Object()" is equal to "(@Q Object) new Object()". CF manual Section XXX.

The "overloading" interpretation of object creation is: "new @Q Object()" is a "template instantiation" of the constructor.

I don’t like either of these terms or interpretations.

To me an object creation has nothing in common with a cast. A cast checks the runtime type of an object against a given type. An object creation sets the runtime type of the object and performs some initialization. In the "casting" interpretation, how do we decide what the runtime type of an object should be and whether the cast is safe or not?

The usual meaning of the term overloading is for a single method name to have multiple definitions - differentiated e.g. by the parameter number and types. The "overloading" interpretation mis-uses this term: there are no multiple definitions: a single constructor is invoked in different ways. Also note that the constructor can be overloaded in the standard sense: there can be multiple constructor definitions distinguished by parameter number and types.

8.3. Unary operations

8.4. Binary operations

8.5. Boxing and Unboxing

9. Things to check for type polymorphism

@OnClass
class MyClass<@OnTP T extends @OnUBound Data>
  extends @OnExt Super<@OnExtTArg String>
  implements @OnImpl Intf<@OnImplTArg Number>
{
  @OnField T f;

  @OnConstructor
  MyClass(@OnCParam T p) {
    this.f = p;
  }

  @OnConstructor2
  MyClass(@OnCParam2 int p) {
    this.f = new ... Data(p);
  }

  @OnRet T foo(@OnReceiver MyClass<@OnReceiverTA T> this,
                  @OnParam Object p) {
    return f;
  }
}

class SomeOtherClass {
  void annotated(@OnDataPar Data dp) {
    @OnLocal MyClass<@OnLocalTA Data> local =
      new @OnNew MyClass<@OnNewTA Data>(dp);
    @OnDataLoc Data dl = local.foo(dp);
  }

  void empty(Data edp) {
    MyClass<Data> elocal = new MyClass<Data>(dp);
    Data edl = local.foo(dp);
  }
}

9.1. Qualifiers on type parameter declarations

9.1.1. Things to check

9.2. Qualifiers on type variable uses

9.2.1. Things to check

9.3. Type polymorphic constructors and methods

9.3.1. Things to check

9.4. Type arguments in method/constructor invocations

9.4.1. Things to check

10. Implicits vs. defaults

11. Case study: SPARTA!

lower bounds

12. Case study: Inference and Verigames

13. Development notes

13.1. Required repositories

Create a new directory. NAME

Check out the required projects:

hg clone http://
hg clone http://

13.2. Eclipse

Create a new Eclipse workspace in directory NAME

eclipse -data NAME

Import all projects.

Make sure not to import the example projects.

See README file for Eclipse configs.

Werner M. Dietl

ABDCFE: A Beautifully Designed Checker Framework Experience

1. Preliminaries

1.1. Notation

2. Open Issues

3. Design Goals

4. Projects

4.1. javacutil

4.1.1. Open issues

4.1.2. Dependencies

4.1.3. Package name

4.2. dataflow

4.2.1. Dependencies

4.2.2. Package name

4.3. stubparser

4.3.1. Open issues

4.3.2. Dependencies

4.3.3. Package name

4.4. framework

4.4.1. Open issues

4.4.2. Dependencies

4.4.3. Package name

4.5. inference

4.5.1. Open issues

4.5.2. Dependencies

4.5.3. Package name

4.6. checker

4.6.1. Open issues

4.6.2. Dependencies

4.6.3. Package name

4.7. Transition

5. Architecture

6. What the bleep is viewpoint adaptation?

7. Use of type annotations

7.1. Constructors

7.1.1. Things to check

7.2. Object creation

7.2.1. What qualifiers can occur in an instantiation?

7.2.2. Things to check

7.3. Qualifiers on a class declaration

7.3.1. Things to check

7.4. Qualifiers on extends/implements

7.4.1. Things to check

8. Things to check for expressions

8.1. Method invocations

8.1.1. Things to check

8.2. Casts

8.2.1. Discussion

8.3. Unary operations

8.4. Binary operations

8.5. Boxing and Unboxing

9. Things to check for type polymorphism

9.1. Qualifiers on type parameter declarations

9.1.1. Things to check

9.2. Qualifiers on type variable uses

9.2.1. Things to check

9.3. Type polymorphic constructors and methods

9.3.1. Things to check

9.4. Type arguments in method/constructor invocations

9.4.1. Things to check

10. Implicits vs. defaults

11. Case study: SPARTA!

12. Case study: Inference and Verigames

13. Development notes

13.1. Required repositories

13.2. Eclipse

4.1. `javacutil`

4.2. `dataflow`

4.3. `stubparser`

4.4. `framework`

4.5. `inference`

4.6. `checker`