Package polyglot.ext.coffer

Coffer, an extension of Java that supports some of the resource management facilities of the Vault language.

See:
Description

Class Summary

ExtensionInfo	Extension information for coffer extension.
Topics	Extension information for coffer extension.
Version	Version information for coffer extension

Package polyglot.ext.coffer Description

Coffer, an extension of Java that supports some of the resource management facilities of the Vault language. See [1]. Coffer allows a linear capability, or key, to be associated with an object. Methods of the object may be invoked only when the key is held. A key is allocated when its object is created and deallocated by a free statement in a method of the object. The Coffer type system regulates allocation and freeing of keys to guarantee statically that keys are always deallocated. Coffer does not support such Vault features as key states and keyed variants.

Below is a small Coffer program declaring a FileReader class that guarantees the program cannot read from a closed reader.

1   tracked(F) class FileReader {
2       FileReader(File f) [] -> [F] throws IOException[] { ... }
3       int read() [F] -> [F] throws IOException[F] { ... }
4       void close() [F] -> [] { ... ; free this; }
5   }

The annotation tracked(F) on line 1 associates a key named F with instances of FileReader. Pre- and post-conditions on method and constructor signatures, written in brackets, specify how the set of held keys changes through an invocation. For example on line 2, the precondition [] indicates that no key need be held to invoke the constructor, and the postcondition [F] specifies that F is held when the constructor returns normally, and the declaration throws IOException[] ensures that F is not held if the constructor throws the exception. The close method (line 4) frees the key; no subsequent method that requires F can be invoked.

To implement Coffer, the Polyglot base compiler is extended in the following ways:

1. PPG is used to extend the parser to support the new syntax.
2. New AST nodes for free statements and keys are added.
3. The existing AST nodes for class, method, and constructor declarations are extended to support the additional type annotations.
4. New passes for computing held key sets at each program point and for checking those key sets are added.

[1] Robert DeLine and Manuel Fähndrich, "Enforcing high-level protocols in low-level software", PLDI '01, pp. 59-69.