Research Abstracts - 2007

Introduction

We propose an extension to Java's annotation system [Bra04a] that permits annotations to appear on any use of a type, not just on class/method/field/variable declarations, as is the case in Java SE 6. Such a generalization removes arbitrary limitations of Java's annotation system, and it enables new uses of annotations. We are also considering other extensions, such as permitting multiple instances of a given annotation at one location, and permitting annotations on statements. The proposal has two parts: changes to the Java language annotation syntax and to the class file format. These changes necessitate some modifications to tools in the JDK.

The annotation extensions are intended to be a standard part of Java SE 7 that will be supported by every Java compiler. JCP (Java Community Process) Executive Committee, which controls the Java language and toolset, has given preliminary approval, and within the JCP the proposal is known as JSR 308. Further votes are required in the Java Community Process before the Java 7 language is officially amended.

The proposal document specifies the syntax of extended Java annotations, but it makes no commitment as to their semantics. As with Java's existing annotations [Bra04a], the semantics is dependent on annotation processors (compiler plug-ins), and not every annotation is necessarily sensible in every location where it is syntactically permitted to appear. The proposal is compatible with existing annotations, such as those specified in JSR 250, “Common Annotations for the Java Platform” [Mor06], and JSR 305, “Annotations for Software Defect Detection” [Pug06].

The proposal does not change the compile-time, load-time, or run-time semantics of Java. It does not change the abilities of Java annotation processors [Dar06]. The proposal merely makes annotations more general — and thus more useful for their current purposes, and also usable for new purposes that are compatible with the original vision for annotations [Bra04a].

Type qualifiers

One example use of annotation on types is to create custom type qualifiers in the Java language. Type qualifiers are modifiers that provide extra information about a type or variable; they can be thought of as a form of subtyping. Type qualifiers can help prevent errors and make possible a variety of program analyses. Since they are user-defined, developers can create and use the type qualifiers that are most appropriate for their software. A designer can define new type qualifiers using Java annotations, and can provide compiler plug-ins to check their semantics (for instance, by issuing lint-like warnings during compilation). A programmer can then use these type qualifiers throughout a program to obtain additional guarantees at compile time about the program. A system for custom type qualifiers requires extensions to Java's annotation system, described in this document; the existing Java SE 6 annotations are inadequate. Similarly to type qualifiers, other pluggable type systems [Bra04b] and similar lint-like checkers also require these extensions to Java's annotation system.

As an example of how our system might be used, consider a @NonNull type qualifier that signifies that a variable should never be assigned null [Det96, Eva96, DLNS98, FL03, CMM05]. The code in figure 1 demonstrates @NonNull in a sample method. A programmer can annotate any use of a type with the @NonNull annotation. A compiler plug-ins would check that a @NonNull variable is never assigned a possibly-null value, thus enforcing the @NonNull type system.

---

 1  @NonNullDefault
 2  class DAG {
 3
 4      Set<Edge> edges;		
 5
 6      // ...
 7
 8      List<Vertex> getNeighbors(@Interned @Readonly Vertex v) @Readonly { 
 9          List<Vertex> neighbors = new LinkedList<Vertex>();
10          for (Edge e : edges)		
11              if (e.from() == v)                          
12                  neighbors.add(e.to());      
13          return neighbors;			
14      }
15  }

Figure 1: The DAG class, which represents a directed acyclic graph, illustrates how type qualifiers might be written by a programmer and checked by a type-checking plug-in in order to detect or prevent errors.
(1) The @NonNullDefault annotation indicates that no reference in the DAG class may be null (unless otherwise annotated). It is equivalent to writing line 4 as “@NonNull Set<@NonNull Edge> edges;”, for example. This guarantees that the uses of edges on line 10, and e on lines 11 and 12, cannot cause a null pointer exception. Similarly, the (implicit) @NonNull return type of getNeighbors() (line 8) enables its clients to depend on the fact that it will always return a List, even if v has no neighbors.
(2) The two @Readonly annotations on method getNeighbors (line 8) guarantee to clients that the method does not modify (respectively) its argument (a Vertex) or its receiver (a DAG). The lack of a @Readonly annotation on the return value indicates that clients are free to modify the returned List.
(3) The @Interned annotation on line 8 (along with an @Interned annotation on the return type in the declaration of Edge.from(), not shown) indicates that the use of object equality (==) on line 11 is a valid optimization. In the absence of such annotations, use of the equals method is preferred to ==.

---

Additional examples of useful type qualifiers abound. We mention just a few others. C uses the const, volatile, and restrict type qualifiers. Type qualifiers YY for two-digit year strings and YYYY for four-digit year strings helped to detect, then verify the absence of, Y2K errors [EFA99]. Type qualifiers can indicate data that originated from an untrustworthy source [PØ95, VS97]; examples for C include user vs. kernel indicating user-space and kernel-space pointers in order to prevent attacks on operating systems [JW04], and tainted for strings that originated in user input and that should not be used as a format string [STFW01]. A localizable qualifier can indicate where translation of user-visible messages should be performed; similarly, annotations can indicate other properties of its contents, such as the format or encoding of a string. An interned qualifier can indicate which objects have been converted to canonical form and thus may be compared via object equality. Type qualifiers such as unique and unaliased can express properties about pointers and aliases [Eva96, CMM05]; other qualifiers can detect and prevent deadlock in concurrent programs [FTA02, AFKT03]. Flow-sensitive type qualifiers [FTA02] can express typestate properties such as whether a file is in the open, read, write, readwrite, or closed state, and can guarantee that a file is opened for reading before it is read, etc. The Vault language's type guards and capability states are similar [DF01].

Further details

The full extensions to the Java language syntax and to the class file format can be found at the JSR 308 webpage, http://pag.csail.mit.edu/jsr308/.

References

[AFKT03]

Alex Aiken, Jeffrey S. Foster, John Kodumal, and Tachio Terauchi. Checking and inferring local non-aliasing. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pages 129–140, San Diego, CA, USA, June 9–11, 2003.

[BE04]

Adrian Birka and Michael D. Ernst. A practical type system and language for reference immutability. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2004), pages 35–49, Vancouver, BC, Canada, October 26–28, 2004.

[Bra04a]

Gilad Bracha. JSR 175: A metadata facility for the Java programming language. http://jcp.org/en/jsr/detail?id=175, September 30, 2004.

[Bra04b]

Gilad Bracha. Pluggable type systems. In OOPSLA Workshop on Revival of Dynamic Languages, Vancouver, BC, Canada, October 2004.

[CMM05]

Brian Chin, Shane Markstrum, and Todd Millstein. Semantic type qualifiers. In Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, pages 85–95, Chicago, IL, USA, June 13–15, 2005.

[Dar06]

Joe Darcy. JSR 269: Pluggable annotation processing API. http://jcp.org/en/jsr/detail?id=269, May 17, 2006. Public review version.

[Det96]

David L. Detlefs. An overview of the Extended Static Checking system. In Proceedings of the First Workshop on Formal Methods in Software Practice, pages 1–9, January 1996.

[DF01]

Robert DeLine and Manuel Fähndrich. Enforcing high-level protocols in low-level software. In Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, pages 59–69, Snowbird, UT, USA, June 20–22, 2001.

[DLNS98]

David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. SRC Research Report 159, Compaq Systems Research Center, December 18, 1998.

[EFA99]

Martin Elsman, Jeffrey S. Foster, and Alexander Aiken. Carillon — A System to Find Y2K Problems in C Programs, July 30, 1999.

[Eva96]

David Evans. Static detection of dynamic memory errors. In Proceedings of the SIGPLAN '96 Conference on Programming Language Design and Implementation, pages 44–53, Philadelphia, PA, USA, May 21–24, 1996.

[FL03]

Manuel Fähndrich and K. Rustan M. Leino. Declaring and checking non-null types in an object-oriented language. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2003), pages 302–312, Anaheim, CA, USA, November 6–8, 2003.

[FTA02]

Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Flow-sensitive type qualifiers. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, pages 1–12, Berlin, Germany, June 17–19, 2002.

[GF05]

David Greenfieldboyce and Jeffrey S. Foster. Type qualifiers for Java. http://www.cs.umd.edu/Grad/scholarlypapers/papers/greenfiledboyce.pdf, August 8, 2005.

[JW04]

Rob Johnson and David Wagner. Finding user/kernel pointer bugs with type inference. In 13th USENIX Security Symposium, pages 119–134, San Diego, CA, USA, August 11–13, 2004.

[KT01]

Günter Kniesel and Dirk Theisen. JAC — access right based encapsulation for Java. Software: Practice and Experience, 31(6):555–576, 2001.

[Mor06]

Rajiv Mordani. JSR 250: Common annotations for the Java platform. http://jcp.org/en/jsr/detail?id=250, May 11, 2006.

[PBKM00]

Sara Porat, Marina Biberstein, Larry Koved, and Bilba Mendelson. Automatic detection of immutable fields in Java. In CASCON, Mississauga, Ontario, Canada, November 13–16, 2000.

[PØ95]

Jens Palsberg and Peter Ørbæk. Trust in the λ-calculus. In SAS95, pages 314–329, Glasgow, UK, September 25–27, 1995.

[Pug06]

William Pugh. JSR 305: Annotations for software defect detection. http://jcp.org/en/jsr/detail?id=305, August 29, 2006. JSR Review Ballot version.

[STFW01]

Umesh Shankar, Kunal Talwar, Jeffrey S. Foster, and David Wagner. Detecting format string vulnerabilities with type qualifiers. In 10th USENIX Security Symposium, Washington, DC, USA, August 15–17, 2001.

[SW01]

Mats Skoglund and Tobias Wrigstad. A mode system for read-only references in Java. In 3rd Workshop on Formal Techniques for Java Programs, Budapest, Hungary, June 18, 2001. Revised.

[TE05]

Matthew S. Tschantz and Michael D. Ernst. Javari: Adding reference immutability to Java. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2005), pages 211–230, San Diego, CA, USA, October 18–20, 2005.

[VS97]

Dennis M. Volpano and Geoffrey Smith. A type-based approach to program security. In TAPSOFT '97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, pages 607–621, Lille, France, April 14–18, 1997.