1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302
|
\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.
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}.
\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.type.incompatible] 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
|