File: map-key-checker.tex

package info (click to toggle)
checker-framework-java 3.2.0%2Bds-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 23,104 kB
  • sloc: java: 145,916; xml: 839; sh: 518; makefile: 404; perl: 26
file content (302 lines) | stat: -rw-r--r-- 10,789 bytes parent folder | download | duplicates (2)
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