Research Abstracts - 2006

Custom Type Qualifiers Through Improved Java Annotations

Matthew M. Papi & Michael D. Ernst

What

We are developing a system for creating custom type qualifiers in the Java language. Specifically, the system extends Java's annotation syntax and processing tools, and uses these improved annotations to provide user-defined type qualifiers. A developer can write these annotations throughout a program, and then create plug-ins to the Java compiler and virtual machine to enforce the semantics of the qualifiers at compile-time and load-time.

For example, consider a "non-null" type qualifier that signifies that a variable should never be assigned null. With our system, a developer could declare a @NonNull annotation and use it essentially anywhere in a program that types are used - unlike standard Java annotations, which are only allowed on method parameters and the declarations of classes, methods, and fields. The developer could then write plug-ins to explicitly check that @NonNull variables are never assigned null.

Why

User-defined type qualifiers for the Java language can be extremely useful. Type qualifiers themselves can help prevent errors and make possible a variety of program analyses. Rigorous use of @NonNull, for example, could altogether eliminate null-pointer exceptions from programs. Since they are user-defined, these benefits are enhanced: developers can create and use the type qualifiers that are most appropriate for their software.

Using annotations for custom type qualifiers has a number of benefits over other potential designs. First, Java already implements annotations, and Java 6 will feature a pluggable framework for compile-time annotation processing. This allows our system to build on the existing stable mechanisms and integrate with the Java toolchain. Second, there is no learning overhead aside from that of the annotations themselves, so type qualifiers written with our system should be easy to adopt and use. Finally, since annotations do not affect the run-time semantics of a program, applications written with custom type qualifiers are backward-compatible with the vanilla JDK.

How

In Java 5, annotations can be written on method parameters and the declarations of classes, methods, and fields. We are additionally allowing annotations on local variable declarations, typecasts, method receivers (i.e. this), and generic type arguments. These can be written using the following syntax:

• for local variable declarations:

  	@NonNull String s;
  

• for typecasts:

  	String s = (@NonNull String)o;
  

• for method receivers:

  	public String foo() @ReadOnly { ... }
  

• for generic type arguments:

  	List<@NonNull String> foo;
  

Each of the components of the improved annotations heavily reuses existing parts of the JDK. The new syntax, for instance, requires a few modifications to the parser and the compiler's syntax tree representation. The foundation for the compiler plug-in interface is provided by Java 6's annotation processing framework. Java 6 will also provide syntax tree abstractions, which plug-ins will use for performing analyses to enforce type qualifier semantics, and a compiler API for access to the compiler's error reporting framework. Finally, load-time verification is built on Java's premain mechanism, which permits byte-code instrumentation and analysis just before the virtual machine starts running a program. Modifications to the Java compiler's code-emitting components will store type-qualifying annotations in the class file in a backward-compatible manner so that load-time plug-ins can locate the annotations and their targets in the bytecode for a class.

Progress and Future Work

Having experimented with Java 6, we have already demonstrated the implementation feasibility of our system. Currently, we are working on modifying the Java compiler to accept annotations in our non-standard locations and to store information about these annotations in the class file. After the implementation is complete, we intend to demonstrate the system by developing some example type qualifiers.

Research Support

This research is supported in part by NSF grant CCR-0133580.