docs/manual/map-key-checker.tex

\htmlhr
\chapterAndLabel{Map Key Checker}{map-key-checker}

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

Section~\ref{map-key-qualifiers} describes how \code{@KeyFor} annotations
enable the
Nullness Checker (\chapterpageref{nullness-checker}) to treat calls to
\sunjavadoc{java.base/java/util/Map.html\#get(java.lang.Object)}{\code{Map.get}}
more precisely by refining its result to \<@NonNull> in some cases.


\sectionAndLabel{Invoking the Map Key Checker}{map-key-invoking}

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 \chapterpageref{suppressing-warnings}.

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 \code{Map<String, @Nullable Integer>}.


\sectionAndLabel{Map key annotations}{map-key-annotations}

These qualifiers are part of the Map Key type system:

\begin{description}

\item[\refqualclasswithparams{checker/nullness/qual}{KeyFor}{String[] maps}]
  indicates that the value assigned to the annotated variable is a key for at
  least the given maps.

\item[\refqualclass{checker/nullness/qual}{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.

\item[\refqualclass{checker/nullness/qual}{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>).

\end{description}

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

\begin{description}
\item[\refqualclasswithparams{checker/nullness/qual}{EnsuresKeyFor}{String[] value, String[] map}]
  When the method with this annotation returns, the expression (or all the
  expressions) given in the \code{value} element is a key for the given
  maps. More precisely, the expression has the \code{@KeyFor} qualifier
  with the \code{value} arguments taken from the \code{targetValue} element
  of this annotation.
\item[\refqualclasswithparams{checker/nullness/qual}{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.
\end{description}

\begin{figure}
\includeimage{map-key-keyfor}{5cm}
\caption{The subtyping relationship of the Map Key Checker's qualifiers.
\<@KeyFor(A)> is a supertype of \<@KeyFor(B)> if and only if \<A> is a subset of
\<B>.  Qualifiers in gray are used internally by the type system but should
never be written by a programmer.}
\label{fig-map-key-keyfor-hierarchy}
\end{figure}

\sectionAndLabel{Default annotations}{map-key-defaults}

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

\subsectionAndLabel{Default for lower bounds}{map-key-defaults-lowerbound}

Lower bounds are defaulted to \code{@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:

%BEGIN LATEX
\medskip
%END LATEX

\noindent
\begin{tabular}{ll}
\<@KeyForBottom> default                   & \<@UnknownKeyFor> default (current choice) \\
\hline
\code{class MyClass1<@UnknownKeyFor T> \{}  & \code{class MyClass1<T> \{} \\
\code{~~T var = null; // OK}               & \code{~~T var = null; // OK} \\
\hline
\code{class MyClass2<T> \{}   & \\
\code{~~@UnknownKeyFor T var = null; // OK} & \\
\hline
\code{class MyClass3<T> \{}    &  \\
\code{~~T var = null; // ERROR}             &  \\
\hline
& \code{class MySet1<T> implements Set<T> \{ \}} \\
& \code{MySet1<@KeyFor("m") String> s1; // ERROR} \\
\hline
\code{class Set<E> \{ \}} &
                \code{class Set<@KeyForBottom E> \{ \}} \\
\code{class MySet2<T> implements Set<T> \{ \}} &
                \code{class MySet2<@KeyForBottom T> implements Set<T> \{ \}} \\
\code{MySet2<@KeyFor("m") String> s2; // OK}
%HEVEA~~~
 &
                \code{MySet2<@KeyFor("m") String> s2; // OK} \\

% List<@KeyFor("m")> // ERROR unless List's type argument has lower bound of @KeyForBottom.
\end{tabular}

%BEGIN LATEX
\medskip
%END LATEX


If lower bounds are defaulted to \code{@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 on 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 \code{@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>).


\subsectionAndLabel{Diagnosing the need for explicit @KeyFor on lower bounds}{map-key-lowerbound-explicit}

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

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

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

\noindent
The Nullness Checker issues this error message:

\begin{Verbatim}
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]
\end{Verbatim}

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~\ref{generics-instantiation}):

\begin{Verbatim}
public class Graph<@KeyForBottom N> {
...
\end{Verbatim}


\sectionAndLabel{Examples}{map-key-examples}

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

\begin{verbatim}
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
\end{verbatim}


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

\begin{verbatim}
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, ...);
\end{verbatim}

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

\begin{verbatim}
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
\end{verbatim}



\sectionAndLabel{Inference of @KeyFor annotations}{map-key-annotations-inference}

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
\sunjavadoc{java.base/java/util/Map.html\#keySet()}{\textrm{key set}} or calls to
\sunjavadoc{java.base/java/util/Map.html\#put(K,V)}{put}
or
\sunjavadoc{java.base/java/util/Map.html\#containsKey(java.lang.Object)}{containsKey}.
For more details about type refinement, see Section~\ref{type-refinement}.

Suppose we have these declarations:

\begin{verbatim}
Map<String,Date> m = new Map<>();
String k = "key";
@KeyFor("m") String km;
\end{verbatim}

Ordinarily, the following assignment does not type-check:

\begin{verbatim}
km = k;   // Error since k is not known to be a key for map m.
\end{verbatim}

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.


\begin{verbatim}
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.
    ...
}
\end{verbatim}


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.

\begin{verbatim}
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() { ... }
}
\end{verbatim}


%% LocalWords:  KeyFor containsKey java keyfor UnknownKeyFor KeyForBottom
%% LocalWords:  mapSet keySet km threeLetterWordSubset JT MyClass1 MySet1
%% LocalWords:  MyClass2 MyClass3 s1 MySet2 s2 EnsuresKeyFor targetValue
%% LocalWords:  EnsuresKeyForIf boolean lowerbound AsuppressWarnings
%% LocalWords:  AassumeKeyFor