The Checker Framework Manual:
Custom pluggable types for Java

Chapter 4 Map Key Checker

The Map Key Checker tracks which values are keys for which maps. If variable v has type @KeyFor("m")..., then the value of v is a key in Map m. That is, the expression m.containsKey(v) evaluates to true.

Section 3.2.4 describes how @KeyFor annotations enable the Nullness Checker (Chapter 3) to treat calls to Map.get more precisely by refining its result to @NonNull in some cases.

4.1 Invoking the Map Key Checker

You will not typically run the Map Key Checker. It is automatically run by other checkers, in particular the Nullness Checker.

You can unsoundly suppress warnings related to map keys with @SuppressWarnings("keyfor"), or everywhere by using command-line option -AsuppressWarnings=keyfor; see Chapter 34.

The command-line argument -AassumeKeyFor makes the Map Key Checker unsoundly assume that the argument to Map.get is a key for the receiver map. This is like declaring the Map.get method as V get(Object key) rather than @Nullable V get(Object key). (Just changing the JDK declaration would not work, however, because the Map Key Checker has special-case logic for Map.get. This is different than suppressing warnings, because it changes a method’s return type. This is not the same as assuming that the return value is @NonNull, because the map’s value type might be @Nullable, as in Map<String, @Nullable Integer>.)

4.2 Map key annotations

These qualifiers are part of the Map Key type system:

@KeyFor(String[] maps)

indicates that the value assigned to the annotated variable is a key for at least the given maps.

@UnknownKeyFor

is used internally by the type system but should never be written by a programmer. It indicates that the value assigned to the annotated variable is not known to be a key for any map. It is the default type qualifier.

@KeyForBottom

is used internally by the type system but should never be written by a programmer. There are no values of this type (not even null).

The following method annotations can be used to establish a method postcondition that ensures that a certain expression is a key for a map:

@EnsuresKeyFor(String[] value, String[] map)

When the method with this annotation returns, the expression (or all the expressions) given in the value element is a key for the given maps. More precisely, the expression has the @KeyFor qualifier with the value arguments taken from the map element of this annotation.

@EnsuresKeyForIf(String[] expression, boolean result, String[] map)

If the method with this annotation returns the given boolean value, then the given expression (or all the given expressions) is a key for the given maps.

4.3 Default annotations

The qualifier for the type of the null literal is @UnknownKeyFor. If null were @KeyForBottom, that would mean that null is guaranteed to be a key for every map (which is not necessarily true).

4.3.1 Default for lower bounds

Lower bounds are defaulted to @UnknownKeyFor. However, in java.* packages, the default for lower bounds is @KeyForBottom.

It is challenging to choose a default for lower bounds of type variables and wildcards.

Here is a comparison of two choices for lower bounds:

If lower bounds are defaulted to @KeyForBottom (which is not currently the case), then whenever null is assigned to a variable whose type is a type variable, programmers must write an @UnknownKeyFor annotation on either the type variable declaration or the variable declarations, as shown in MyClass1 and MyClass2. A disadvantage of this default is that the Map Key Checker may issue warnings in code that has nothing to do with map keys, and in which no map key annotations are used.

If lower bounds are defaulted to @UnknownKeyFor (which is currently the case), then whenever a client might use a @KeyFor type argument, programmers must write a @KeyForBottom annotation on the type parameter, as in MySet2 (and Set).

4.3.2 Diagnosing the need for explicit @KeyFor on lower bounds

Under the current defaulting (lower bounds default to @UnknownKeyFor), suppose you write this code:

public class Graph<N> {
  Map<N, Integer> nodes = new HashMap<>();
}

class Client {
  @Nullable Graph<@KeyFor("g.nodes") String> g;
}

The Nullness Checker issues this error message:

Graph.java:14: error: [type.argument] incompatible types in type argument.
  @Nullable Graph<@KeyFor("g.nodes") String> g;
                  ^
  found   : @KeyFor("this.g.nodes") String
  required: [extends @UnknownKeyFor Object super @UnknownKeyFor null]

Note that the upper and lower bounds are both @UnknownKeyFor. You can make the code type-check by writing a lower bound, which is written before the type variable name (Section 32.1.2):

public class Graph<@KeyForBottom N> {
...

4.4 Examples

The Map Key Checker keeps track of which variables reference keys to which maps. A variable annotated with @KeyFor(mapSet) can only contain a value that is a key for all the maps in mapSet. For example:

Map<String,Date> m, n;
@KeyFor("m") String km;
@KeyFor("n") String kn;
@KeyFor({"m", "n"}) String kmn;
km = kmn;   // OK: a key for maps m and n is also a key for map m
km = kn;    // error: a key for map n is not necessarily a key for map m

As with any annotation, use of the @KeyFor annotation may force you to slightly refactor your code. For example, this would be illegal:

Map<String,Object> m;
Collection<@KeyFor("m") String> coll;
coll.add(x);   // error: element type is @KeyFor("m") String, but x does not have that type
m.put(x, ...);

The example type-checks if you reorder the two calls:

Map<String,Object> m;
Collection<@KeyFor("m") String> coll;
m.put(x, ...);    // after this statement, x has type @KeyFor("m") String
coll.add(x);      // OK

4.5 Local inference of @KeyFor annotations

Within a method body, you usually do not have to write @KeyFor explicitly (except sometimes on type arguments), because the checker infers it based on usage patterns. When the Map Key Checker encounters a run-time check for map keys, such as “if (m.containsKey(k)) ...”, then the Map Key Checker refines the type of k to @KeyFor("m") within the scope of the test (or until k is side-effected within that scope). The Map Key Checker also infers @KeyFor annotations based on iteration over a map’s key set or calls to put or containsKey. For more details about type refinement, see Section 33.7.

Suppose we have these declarations:

Map<String,Date> m = new HashMap<>();
String k = "key";
@KeyFor("m") String km;

Ordinarily, the following assignment does not type-check:

km = k;   // Error since k is not known to be a key for map m.

The following examples show cases where the Map Key Checker infers a @KeyFor annotation for variable k based on usage patterns, enabling the km = k assignment to type-check.

m.put(k, ...);
// At this point, the type of k is refined to @KeyFor("m") String.
km = k;   // OK



if (m.containsKey(k)) {
    // At this point, the type of k is refined to @KeyFor("m") String.
    km = k;   // OK
    ...
} else {
    km = k;   // Error since k is not known to be a key for map m.
    ...
}

The following example shows a case where the Map Key Checker resets its assumption about the type of a field used as a key because that field may have been side-effected.

class MyClass {
    private Map<String,Object> m;
    private String k;   // The type of k defaults to @UnknownKeyFor String
    private @KeyFor("m") String km;

    public void myMethod() {
        if (m.containsKey(k)) {
            km = k;   // OK: the type of k is refined to @KeyFor("m") String

             sideEffectFreeMethod();
             km = k;   // OK: the type of k is not affected by the method call
                       // and remains @KeyFor("m") String

             otherMethod();
             km = k;   // error: At this point, the type of k is once again
                       // @UnknownKeyFor String, because otherMethod might have
                       // side-effected k such that it is no longer a key for map m.
         }
    }

    @SideEffectFree
    private void sideEffectFreeMethod() { ... }

    private void otherMethod() { ... }
}