The Checker Framework Manual:
Custom pluggable types for Java

Chapter 18 Signature String Checker for string representations of types

The Signature String Checker, or Signature Checker for short, verifies that string representations of types and signatures are used correctly.

Java defines multiple different string representations for types (see Section 18.1), and it is easy to misuse them or to miss bugs during testing. Using the wrong string format leads to a run-time exception or an incorrect result. This is a particular problem for fully qualified and binary names, which are nearly the same — they differ only for nested classes and arrays.

The paper “Building and using pluggable type-checkers” [DDE+11] (ICSE 2011, https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-icse2011.pdf) describes case studies of the Signature String Checker.

18.1 Signature annotations

Java defines six formats for the string representation of a type. There is an annotation for each of these representations. Figure 18.1 shows how they are related; examples appear in a table below.

(image)

Figure 18.1: Partial type hierarchy for the Signature type system, showing string representations of a Java type. The type qualifiers are applicable to CharSequence and its subtypes. Programmers usually only need to write the boldfaced qualifiers. The other qualifiers (and some not shown) are included to improve the internal handling of String literals.

@FullyQualifiedName

A fully qualified name (JLS §6.7), such as mypackage.Outer.Inner, is used in Java code and in messages to the user.

@ClassGetName

The type representation used by the Class.getName(), Class.forName(String), and Class.forName(String, boolean, ClassLoader) methods. This format is: for any non-array type, the binary name; and for any array type, a format like the FieldDescriptor field descriptor, but using “.” where the field descriptor uses “/”. See examples below.

@FieldDescriptor

A field descriptor (JVMS §4.3.2), such as Lmypackage/Outer$Inner;, is used in a .class file’s constant pool, for example to refer to other types. It abbreviates primitive types and array types. It uses internal form (binary names, but with / instead of .; see JVMS §4.2) for class names. See examples below.

@BinaryName

A binary name (JLS §13.1), such as mypackage.Outer$Inner, is the conceptual name of a type in its own .class file.

@InternalForm

The internal form (JVMS §4.2), such as mypackage/Outer$Inner, is how a class name is actually represented in its own .class file. It is also known as the “syntax of binary names that appear in class file structures”. It is the same as the binary name, but with periods (.) replaced by slashes (/). Programmers more often use the binary name, leaving the internal form as a JVM implementation detail.

@ClassGetSimpleName

The type representation returned by the Class.getSimpleName() method. This format is not required by any method in the JDK, so you will rarely write it in source code. The string can be empty. This is not the same as the “simple name” defined in (JLS §6.2), which is the same as @Identifier.

@FqBinaryName

An extension of binary name format to represent primitives and arrays. It is like @FullyQualifiedName, but using “$” instead of “.” to separate nested classes from their enclosing classes. For example, "pkg.Outer$Inner" or "pkg.Outer$Inner[][]" or "int[]".

@CanonicalName

Syntactically identical to @FullyQualifiedName, but some classes have multiple fully-qualified names, only one of which is canonical (see JLS §6.7).

Other type qualifiers are the intersection of two or more qualifiers listed above; for example, a @DotSeparatedIdentifiers is a string that is a valid fully-qualified name and a valid binary name. A programmer should rarely or never use these qualifiers, and you can ignore them as implementation details of the Signature Checker, though you might occasionally see them in an error message. These qualifiers exist to give literals sufficiently precise types that they can be used in any appropriate context.

Java also defines other string formats for a type, notably qualified names (JLS §6.2). The Signature Checker does not include annotations for these.

Here are examples of the supported formats:

fully qualified name Class.getName field descriptor binary name internal form Class.getSimpleName
int int I n/a for primitive type n/a for primitive type int
int[][] [[I [[I n/a for array type n/a for array type int[][]
MyClass MyClass LMyClass; MyClass MyClass MyClass
MyClass[] [LMyClass; [LMyClass; n/a for array type n/a for array type MyClass[]
n/a for anonymous class MyClass$22 LMyClass$22; MyClass$22 MyClass$22 (empty string)
n/a for array of anon. class [LMyClass$22; [LMyClass$22; n/a for array type n/a for array type []
java.lang.Integer java.lang.Integer Ljava/lang/Integer; java.lang.Integer java/lang/Integer Integer
java.lang.Integer[] [Ljava.lang.Integer; [Ljava/lang/Integer; n/a for array type n/a for array type Integer[]
pkg.Outer.Inner pkg.Outer$Inner Lpkg/Outer$Inner; pkg.Outer$Inner pkg/Outer$Inner Inner
pkg.Outer.Inner[] [Lpkg.Outer$Inner; [Lpkg/Outer$Inner; n/a for array type n/a for array type Inner[]
n/a for anonymous class pkg.Outer$22 Lpkg/Outer$22; pkg.Outer$22 pkg/Outer$22 (empty string)
n/a for array of anon. class [Lpkg.Outer$22; [Lpkg/Outer$22; n/a for array type n/a for array type []

Java defines one format for the string representation of a method signature:

@MethodDescriptor

A method descriptor (JVMS §4.3.3) identifies a method’s signature (its parameter and return types), just as a field descriptor identifies a type. The method descriptor for the method

    Object mymethod(int i, double d, Thread t)

is

    (IDLjava/lang/Thread;)Ljava/lang/Object;
18.1.1 How to choose which annotation to use

Sometimes, there are multiple valid annotations for a value. As an example, a non-primitive non-array type is represented identically by @BinaryName, @ClassGetName, and @FqBinaryName. Using the lowest type in the type hierarchy (in this case, @BinaryName) has two advantages. First, it acts as documentation that the value is never a primitive or array. Second, it permits the value to be used in any of the three contexts: as a @BinaryName, a @ClassGetName, or a @FqBinaryName.

Casting to @BinaryName from one of the other types adds clutter if it is not necessary. Suppose that a method returns a @ClassGetName and the value will only be used in contexts that require a @ClassGetName (say, it is passed to a method that requires an argument of that type). Then there is no point in casting to @BinaryName in between, even if you know the type being represented is not a primitive or an array.

18.2 What the Signature Checker checks

Certain methods in the JDK, such as Class.forName, are annotated indicating the type they require. The Signature Checker ensures that clients call them with the proper arguments. The Signature Checker does not reason about string operations such as concatenation, substring, parsing, etc.

To run the Signature Checker, supply the -processor org.checkerframework.checker.signature.SignatureChecker command-line option to javac.