File: signature-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 (183 lines) | stat: -rw-r--r-- 9,436 bytes parent folder | download | duplicates (3)
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
\htmlhr
\chapterAndLabel{Signature String Checker for string representations of types}{signature-checker}

The Signature String Checker, or Signature Checker for short, verifies that
string representations of types and signatures are used correctly.

Java defines multiple different string representations for types (see
Section~\ref{signature-annotations}), and it is easy to
misuse them or to miss bugs during testing.  Using the wrong string format
leads to a run-time exception or an incorrect result.  This is a particular
problem for fully qualified and binary names, which are nearly the same ---
they differ only for nested classes and arrays.


\sectionAndLabel{Signature annotations}{signature-annotations}

Java defines six formats for the string representation of a type.
There is an annotation for each of these representations.
Figure~\ref{fig-signature-hierarchy} shows how they are related;
examples appear in a table below.

\begin{figure}
\includeimage{signature-types}{7cm}
\caption{Partial type hierarchy for the Signature type system, showing
  string representations of a Java type.
  The type qualifiers are applicable to \<CharSequence> and its subtypes.
  Programmers usually only need to write
  the boldfaced qualifiers; other qualifiers are
  included to improve the internal handling of String literals.}
\label{fig-signature-hierarchy}
\end{figure}

\begin{description}

\item[\refqualclass{checker/signature/qual}{FullyQualifiedName}]
  A \emph{fully qualified name} (\href{https://docs.oracle.com/javase/specs/jls/se11/html/jls-6.html#jls-6.7}{JLS \S
    6.7}), such as
  \<package.Outer.Inner>, is used in Java code and in messages to
  the user.

\item[\refqualclass{checker/signature/qual}{ClassGetName}]
\begin{sloppypar}
  The type representation used by the
  \sunjavadoc{java.base/java/lang/Class.html\#getName()}{\code{Class.getName()}}, \<Class.forName(String)>,
  and \<Class.forName(String, boolean, ClassLoader)> methods.  This format
  is:  for any non-array type, the binary name; and for any array type, a
  format like the
  \href{https://docs.oracle.com/javase/specs/jvms/se11/html/jvms-4.html#jvms-4.3.2}{FieldDescriptor
    field descriptor}, but using
  ``\<.>''~where the field descriptor uses ``\</>''.  See examples below.
\end{sloppypar}

\item[\refqualclass{checker/signature/qual}{FieldDescriptor}]
  A \emph{field descriptor} (\href{https://docs.oracle.com/javase/specs/jvms/se11/html/jvms-4.html#jvms-4.3.2}{JVMS \S 4.3.2}), such as
  \<Lpackage/Outer\$Inner;>, is used in a \<.class> file's constant pool,
  for example to refer to other types.  It abbreviates primitive types and
  array types.  It uses internal form (binary names, but with \</> instead of
  \<.>; see
  \href{https://docs.oracle.com/javase/specs/jvms/se11/html/jvms-4.html#jvms-4.2.1}{JVMS
    \S 4.2}) for class names.  See examples below.

\item[\refqualclass{checker/signature/qual}{BinaryName}]
  A \emph{binary name} (\href{https://docs.oracle.com/javase/specs/jls/se11/html/jls-13.html#jls-13.1}{JLS \S 13.1}), such as
  \<package.Outer\$Inner>, is
  the conceptual name of a type in its own \<.class> file.

\item[\refqualclass{checker/signature/qual}{InternalForm}]
  The \emph{internal form}
  (\href{https://docs.oracle.com/javase/specs/jvms/se11/html/jvms-4.html#jvms-4.2}{JVMS
    \S 4.2}), such as \<package/Outer\$Inner>, is how a class name is
  actually represented in its own \<.class> file.  It is also known as the
  ``syntax of binary names that appear in class file structures''.  It is
  the same as the binary name, but with periods (\<.>) replaced by slashes
  (\</>).  Programmers more often use the binary name, leaving the internal
  form as a JVM implementation detail.

\item[\refqualclass{checker/signature/qual}{ClassGetSimpleName}]
  The type representation returned by the
  \sunjavadoc{java.base/java/lang/Class.html\#getSimpleName()}{\code{Class.getSimpleName()}}
  method.  This format is not required by any method in the JDK, so you
  will rarely write it in source code.  The string can be empty.  This
  is not the same as the ``simple name'' defined in
  (\href{https://docs.oracle.com/javase/specs/jls/se11/html/jls-6.html#jls-6.2}{JLS
    \S 6.2}), which is the same as
  \refqualclass{checker/signature/qual}{Identifier}.

\item[\refqualclass{checker/signature/qual}{FqBinaryName}]
  An extension of binary name format to represent primitives and arrays.
  It is like \refqualclass{checker/signature/qual}{FullyQualifiedName}, but using
  ``\<\$>'' instead of ``\<.>'' to separate nested classes from their
  containing classes.  For example, \<"pkg.Outer\$Inner"> or
  \<"pkg.Outer\$Inner[][]"> or \<"int[]">.

\end{description}

Other type qualifiers are the intersection of two or more qualifiers listed
above; for example, a
\refqualclass{checker/signature/qual}{BinaryNameInUnnamedPackage} is a string
that is a valid internal form \emph{and} a valid binary name.  A
programmer should never or rarely use these qualifiers, and you can ignore
them as implementation details of the Signature Checker, though you might
occasionally see them in an error message.  These qualifiers exist to give
literals sufficiently precise types that they can be used in any
appropriate context.

Java also defines other string formats for a type:  qualified names
(\href{https://docs.oracle.com/javase/specs/jls/se11/html/jls-6.html#jls-6.2}{JLS
  \S 6.2}) and canonical names
(\href{https://docs.oracle.com/javase/specs/jls/se11/html/jls-6.html#jls-6.7}{JLS
  \S 6.7}).  The Signature Checker does not include annotations for these.

Here are examples of the supported formats:
\label{signature-annotations-examples}


\newcommand{\naforanon}{\emph{n/a {\smaller for anonymous class}}}
\newcommand{\naforanonarray}{\emph{n/a {\smaller for array of anon.~class}}}
\newcommand{\naforprim}{\emph{n/a {\smaller for primitive type}}}
\newcommand{\naforarray}{\emph{n/a {\smaller for array type}}}
\newcommand{\emptystring}{\emph{\smaller (empty string)}}

\begin{small}
\begin{center}
\begin{tabular}{|l|l|l|l|l|l|}
\hline
\multicolumn{1}{|c|}{fully qualified name} & \multicolumn{1}{c|}{Class.getName} & \multicolumn{1}{c|}{field descriptor} & \multicolumn{1}{c|}{binary name} & \multicolumn{1}{c|}{internal form} & \multicolumn{1}{c|}{Class.getSimpleName} \\ \hline
int                 & int                  & I                    & \naforprim          & \naforprim          & int            \\
int[][]             & [[I                  & [[I                  & \naforarray         & \naforarray         & int[][]        \\
MyClass             & MyClass              & LMyClass;            & MyClass             & MyClass             & MyClass        \\
MyClass[]           & [LMyClass;           & [LMyClass;           & \naforarray         & \naforarray         & MyClass[]      \\
\naforanon          & MyClass\$22          & LMyClass\$22;        & MyClass\$22         & MyClass\$22         & \emptystring \\
\naforanonarray     & [LMyClass\$22;       & [LMyClass\$22;       & \naforarray         & \naforarray         & []             \\
java.lang.Integer   & java.lang.Integer    & Ljava/lang/Integer;  & java.lang.Integer   & java/lang/Integer   & Integer        \\
java.lang.Integer[] & [Ljava.lang.Integer; & [Ljava/lang/Integer; & \naforarray         & \naforarray         & Integer[]      \\
pkg.Outer.Inner     & pkg.Outer\$Inner     & Lpkg/Outer\$Inner;   & pkg.Outer\$Inner    & pkg/Outer\$Inner    & Inner          \\
pkg.Outer.Inner[]   & [Lpkg.Outer\$Inner;  & [Lpkg/Outer\$Inner;  & \naforarray         & \naforarray         & Inner[]        \\
\naforanon          & pkg.Outer\$22        & Lpkg/Outer\$22;      & pkg.Outer\$22       & pkg/Outer\$22       & \emptystring \\
\naforanonarray     & [Lpkg.Outer\$22;     & [Lpkg/Outer\$22;     & \naforarray         & \naforarray         & []             \\
\hline
\end{tabular}
\end{center}
\end{small}

Java defines one format for the string representation of a method signature:

\begin{description}

\item[\refqualclass{checker/signature/qual}{MethodDescriptor}]
  A \emph{method descriptor} (\href{https://docs.oracle.com/javase/specs/jvms/se11/html/jvms-4.html#jvms-4.3.3}{JVMS \S
    4.3.3}) identifies a method's signature (its parameter and return
  types), just as a field descriptor identifies a
  type.   The method descriptor for the method
\begin{Verbatim}
    Object mymethod(int i, double d, Thread t)
\end{Verbatim}
\noindent is
\begin{Verbatim}
    (IDLjava/lang/Thread;)Ljava/lang/Object;
\end{Verbatim}

\end{description}


\sectionAndLabel{What the Signature Checker checks}{signature-checks}

Certain methods in the JDK, such as \<Class.forName>, are annotated
indicating the type they require.  The Signature Checker ensures that
clients call them with the proper arguments.  The Signature Checker does
not reason about string operations such as concatenation, substring,
parsing, etc.

\begin{sloppypar}
To run the Signature Checker, supply the
\code{-processor org.checkerframework.checker.signature.SignatureChecker}
command-line option to javac.
\end{sloppypar}


% LocalWords:  Regex regex quals FullyQualifiedName BinaryName FieldDescriptor
% LocalWords:  Lpackage MyClass MethodDescriptor forName substring
%  LocalWords:  jls getName ClassGetName ClassLoader LMyClass Ljava
%  LocalWords:  DotSeparatedIdentifiers
%  LocalWords:  FieldDescriptorForPrimitiveOrArrayInUnnamedPackage