The Checker Framework Manual:
Custom pluggable types for Java

Chapter 6 Interning Checker

If the Interning Checker issues no errors for a given program, then all reference equality tests (i.e., all uses of “==”) are proper; that is, == is not misused where equals() should have been used instead.

Interning is a design pattern in which the same object is used whenever two different objects would be considered equal. Interning is also known as canonicalization or hash-consing, and it is related to the flyweight design pattern. Interning has two benefits: it can save memory, and it can speed up testing for equality by permitting use of ==.

The Interning Checker prevents two types of problems in your code. First, it prevents using == on non-interned values, which can result in subtle bugs. For example:

    Integer x = new Integer(22);
    Integer y = new Integer(22);
    System.out.println(x == y); // prints false!

Second, the Interning Checker helps to prevent performance problems that result from failure to use interning. (See Section 2.3 for caveats to the checker’s guarantees.)

Interning is such an important design pattern that Java builds it in for these types: String, Boolean, Byte, Character, Integer, and Short. Every string literal in the program is guaranteed to be interned (JLS §3.10.5), and the String.intern() method performs interning for strings that are computed at run time. The valueOf methods in wrapper classes always (Boolean, Byte) or sometimes (Character, Integer, Short) return an interned result (JLS §5.1.7). Users can also write their own interning methods for other types.

It is a proper optimization to use ==, rather than equals(), whenever the comparison is guaranteed to produce the same result — that is, whenever the comparison is never provided with two different objects for which equals() would return true. Here are three reasons that this property could hold:

• 1. Interning. A factory method ensures that, globally, no two different interned objects are equals() to one another. (For some classes, every instance is interned; however, in other cases it is possible for two objects of the class to be equals() to one another, even if one of them is interned.) Interned objects should always be immutable.

• 2. Global control flow. The program’s control flow is such that the constructor for class C is called a limited number of times, and with specific values that ensure the results are not equals() to one another. Objects of class C can always be compared with ==. Such objects may be mutable or immutable.

• 3. Local control flow. Even though not all objects of the given type may be compared with ==, the specific objects that can reach a given comparison may be.

  • • When searching for an element (say, in a collection), == may be appropriate.

  • • Some routines return either their argument, or a modified version of it. Your code might compare s == s.toLowerCase() to see whether a string contains any upper-case characters.

To eliminate Interning Checker errors, you will need to annotate the declarations of any expression used as an argument to ==. Thus, the Interning Checker could also have been called the Reference Equality Checker.

To run the Interning Checker, supply the -processor org.checkerframework.checker.interning.InterningChecker command-line option to javac. For examples, see Section 6.5.

6.1 Interning annotations

6.1.1 Interning qualifiers

These qualifiers are part of the Interning type system:

@Interned

indicates a type that includes only interned values (no non-interned values).

@InternedDistinct

indicates that the value is not equals() to any other Java value. This is a stronger (more restrictive) property than @Interned, but is a weaker property than writing @Interned on a class declaration. For details, see Section 6.3.3.

@UnknownInterned

indicates a type whose values might or might not be interned. It is used internally by the type system and is not written by programmers.

@PolyInterned

indicates qualifier polymorphism. For a description of qualifier polymorphism, see Section 32.2.

6.1.2 Interning method and class annotations

@UsesObjectEquals

is a class annotation (not a type annotation) that indicates that this class’s equals method is the same as that of Object. Since Object.equals uses reference equality, this means that for such a class, == and equals are equivalent, and so the Interning Checker does not issue errors or warnings for either one.

Two ways to satisfy this annotation are: (1) neither this class nor any of its superclasses overrides the equals method, or (2) this class defines equals with body return this == o;.

@InternMethod

is a method declaration annotation that indicates that this method returns an interned object and may be invoked on an uninterned object. See Section 6.3.1 for more details.

@EqualsMethod

is a method declaration annotation that indicates that this method has a specification like equals(). The Interning Checker permits use of this == arg within the body.

@CompareToMethod

is a method declaration annotation that indicates that this method has a specification like compareTo(). The Interning Checker permits use of if (arg1 == arg2) { return 0; } within the body.

@FindDistinct

is a formal parameter declaration annotation that indicates that this method uses == to perform comparisons against the annotated formal parameter. A common reason is that the method searches for the formal parameter in some data structure, using ==. Any value may be passed to the method.

6.2 Annotating your code with @Interned

In order to perform checking, you must annotate your code with the @Interned type annotation. A type annotated with @Interned contains the canonical representation of an object:

              String s1 = ...;   // type is (uninterned) "String"
    @Interned String s2 = ...;   // type is "@Interned String"

The Interning Checker ensures that only interned values can be assigned to s2.

6.3 Interned classes

An @Interned annotation on a class declaration indicates that all objects of that type are interned except for newly created objects. That means that all uses of such types are @Interned by default and the type @UnknownInterned MyClass is an invalid type.

An exception is constructor results. Constructor results and this within the body of the constructor are @UnknownInterned by default. Although @UnknownInterned InternedClass is not a legal type, no “type.invalid” error is issued at constructor declarations. Instead, an “interned.object.creation” error is issued at the invocation of the constructor. The user should inspect this location and suppress the warning if the newly created object is interned.

For example:

@Interned class InternedClass {
  @UnknownInterned InternedClass() {
    // error, "this" is @UnknownInterned.
    @Interned InternedClass that = this;
  }

    @SuppressWarnings("interning") // Only creation of an InternedClass object.
    static final InternedClass ONE = new InternedClass();
}

6.3.1 The intern() methods

Some interned classes use an intern() method to look up the interned version of the object. These methods must be annotated with the declaration annotation @InternMethod. This allows the checker to verify that a newly created object is immediately interned and therefore not issue an interned object creation error.

new InternedClass().intern() // no error

Because an intern method is expected to be called on uninterned objects, the type of this in intern is implicitly @UnknownInterned. This will cause an error if this is used someplace where an interned object is expected. Some of these warnings will be false positives that should be suppressed by the user.

@InternMethod
public InternedClass intern() {
  // Type of "this" inside an @InternMethod is @UnknownInterned
  @Interned InternedClass that = this; // error

    if (!pool.contains(this)) {
      @SuppressWarnings("interning:assignment")
      @Interned InternedClass internedThis = this;
      pool.add(internedThis);
    }
    return pool.get(this);
}

Some interned classes do not use an intern method to ensure that every object of that class is interned. For these classes, the user will have to manually inspect every constructor invocation and suppress the “interned.object.creation” error.

If the result of every invocation of a constructor is guaranteed to be interned, then the user should annotate the constructor result with @Interned and suppress a warning at the constructor.

@Interned class AnotherInternedClass {
  // manually verified that all constructor invocations are used such that all
  // new objects are interned
  @SuppressWarnings("super.invocation")
  @Interned AnotherInternedClass() {}
}

6.3.2 Default qualifiers and qualifiers for literals

The Interning Checker adds qualifiers to unannotated types, reducing the number of annotations that must appear in your code (see Section 33.4).

For a complete description of all defaulting rules for interning qualifiers, see the Javadoc for InterningAnnotatedTypeFactory.

6.3.3 InternedDistinct: values not equals() to any other value

The @InternedDistinct annotation represents values that are not equals() to any other value. Suppose expression e has type @InternedDistinct. Then e.equals(x) == (e == x). Therefore, it is legal to use == whenever at least one of the operands has type @InternedDistinct.

@InternedDistinct is stronger (more restrictive) than @Interned. For example, consider these variables:

@Interned String i = "22";
          String s = new Integer(22).toString();

The variable i is not @InternedDistinct because i.equals(s) is true.

@InternedDistinct is not as restrictive as stating that all objects of a given Java type are interned.

The @InternedDistinct annotation is rarely used, because it arises from coding paradigms that are tricky to reason about. One use is on static fields that hold canonical values of a type. Given this declaration:

class MyType {
  final static @InternedDistinct MyType SPECIAL = new MyType(...);
  ...
}

it would be legal to write myValue == MyType.SPECIAL rather than myValue.equals(MyType.SPECIAL).

The @InternedDistinct annotation is trusted (not verified), because it would be too complex to analyze the equals() method to ensure that no other value is equals() to an @InternedDistinct value. You will need to manually verify that it is only written in locations where its contract is satisfied. For example, here is one set of guidelines that you could check manually:

• • The constructor is private.

• • The factory method (whose return type is annotated with @InternedDistinct) returns the canonical version for certain values.

• • The class is final, so that subclasses cannot violate these properties.

The result of a constructor call (that is, new MyClass(...)) is not necessarily @InternedDistinct because the equals() method of MyClass might return true for two distinct objects.

6.4 What the Interning Checker checks

Objects of an @Interned type may be safely compared using the “==” operator.

The checker issues an error in two cases:

• 1. When a reference (in)equality operator (“==” or “!=”) has an operand of non-@Interned type. As a special case, the operation is permitted if either operand is of @InternedDistinct type.

• 2. When a non-@Interned type is used where an @Interned type is expected.

This example shows both sorts of problems:

                      Date date;
            @Interned Date idate;
    @InternedDistinct Date ddate;
    ...
    if (date == idate) ... // error: reference equality test is unsafe
    idate = date;           // error: idate's referent might no longer be interned
    ddate = idate;          // error: idate's referent might be equals() to some other value

The Interning Checker’s warnings look like

MyFile.java:716: error: [interning:not.interned] attempting to use a non-@Interned comparison operand
        if (date == idate)
            ^

To resolve a not.interned error, you should change the argument that is passed to ==, or use .equals() instead of ==, or suppress the warning.

The checker also issues a warning when .equals is used where == could be safely used. You can disable this behavior via the javac -Alint=-dotequals command-line option.

For a complete description of all checks performed by the checker, see the Javadoc for InterningVisitor.

To restrict which types the checker should type-check, pass a canonical name (fully-qualified name) using the -Acheckclass option. For example, to find only the interning errors related to uses of String, you can pass -Acheckclass=java.lang.String. The Interning Checker always checks all subclasses and superclasses of the given class.

6.4.1 Imprecision (false positive warnings) of the Interning Checker

The Interning Checker conservatively assumes that the Character, Integer, and Short valueOf methods return a non-interned value. In fact, these methods sometimes return an interned value and sometimes a non-interned value, depending on the run-time argument (JLS §5.1.7). If you know that the run-time argument to valueOf implies that the result is interned, then you will need to suppress an error. (The Interning Checker should make use of the Value Checker to estimate the upper and lower bounds on char, int, and short values so that it can more precisely determine whether the result of a given valueOf call is interned.)

6.5 Examples

To try the Interning Checker on a source file that uses the @Interned qualifier, use the following command:

    javac -processor org.checkerframework.checker.interning.InterningChecker docs/examples/InterningExample.java

Compilation will complete without errors or warnings.

To see the checker warn about incorrect usage of annotations, use the following command:

    javac -processor org.checkerframework.checker.interning.InterningChecker docs/examples/InterningExampleWithWarnings.java

The compiler will issue an error regarding violation of the semantics of @Interned.

The Daikon invariant detector (https://plse.cs.washington.edu/daikon/) is also annotated with @Interned. From directory java/, run make check-interning.

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 in which the Interning Checker found previously-unknown errors in real software.

6.6 Other interning annotations

The Checker Framework’s interning annotations are similar to annotations used elsewhere.

If your code is already annotated with a different interning annotation, the Checker Framework can type-check your code. It treats annotations from other tools as if you had written the corresponding annotation from the Interning Checker, as described in Figure 6.2. If the other annotation is a declaration annotation, it may be moved; see Section 40.6.10.