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
|
\htmlhr
\chapterAndLabel{Signedness Checker}{signedness-checker}
The Signedness Checker guarantees that signed and unsigned integral values are not mixed
together in a computation. In addition, it prohibits meaningless operations, such
as division on an unsigned value.
Recall that a computer represents a number as a sequence of bits.
Signedness indicates how to interpret the most significant bit. For
example, the bits \<10000010> ordinarily represent the value -126, but when
interpreted as unsigned, those bits represent the value 130. The bits
\<01111110> represent the value 126 in signed and in unsigned interpretation.
The range of signed byte values is -128 to 127. The range of unsigned byte
values is 0 to 255.
Signedness is only applicable to integral types: \<bype>, \<char>,
\<short>, \<int>, and \<long>. Floating-point types (\<float> and
\<double>) do not have operations that interpret the bits as unsigned.
Signedness is primarily about how the bits of the representation are
interpreted, not about the values that it can represent. An unsigned value
is always positive, but just because a variable's value is positive does
not mean that it should be marked as \<@Unsigned>. If variable $v$ will be
compared to a signed value, or used in arithmetic operations with a signed
value, then $v$ should have signed type.
To indicate the range of possible values for a variable, use the
\refqualclass{checker/index/qual}{NonNegative} annotation of the Index
Checker (see \chapterpageref{index-checker}) or the
\refqualclass{common/value/qual}{IntRange} annotation of the Constant Value
Checker (see \chapterpageref{constant-value-checker}).
\sectionAndLabel{Annotations}{signedness-checker-annotations}
The Signedness Checker uses type annotations to indicate the signedness that the programmer intends an expression to have.
\begin{figure}
\includeimage{signedness}{3.5cm}
\caption{The type qualifier hierarchy of the signedness annotations.
Qualifiers in gray are used internally by the type system but should never be written by a programmer.}
\label{fig-signedness-hierarchy}
\end{figure}
These are the qualifiers in the signedness type system:
\begin{description}
\item[\refqualclass{checker/signedness/qual}{Unsigned}]
indicates that the programmer intends the value to be
interpreted as unsigned.
That is, if the most significant bit in the bitwise representation is
set, then the bits should be interpreted as a large positive value.
\item[\refqualclass{checker/signedness/qual}{Signed}]
indicates that the programmer intends the value to be
interpreted as signed.
That is, if the most significant bit in the bitwise representation is
set, then the bits should be interpreted as a negative value.
This is the default annotation.
\item[\refqualclass{checker/signedness/qual}{SignedPositive}]
indicates that a value is known at compile time to be in the positive
signed range, so it has the same interpretation as signed or unsigned
and may be used with either interpretation. Programmers should usually
write \refqualclass{checker/signedness/qual}{Signed} or
\refqualclass{checker/signedness/qual}{Unsigned} instead.
\item[\refqualclass{checker/signedness/qual}{SignednessGlb}]
indicates that a value may be interpreted as unsigned or signed. It
covers the same cases as
\refqualclass{checker/signedness/qual}{SignedPositive}, plus manifest literals, to
prevent the programmer from having to annotate them all explicitly.
This annotation should almost never be written by the
programmer.
\item[\refqualclass{checker/signedness/qual}{PolySigned}]
indicates qualifier polymorphism.
For a description of qualifier polymorphism, see
Section~\ref{qualifier-polymorphism}.
\item[\refqualclass{checker/signedness/qual}{UnknownSignedness}]
indicates that a value's type is not relevant or known to this checker.
This annotation is used internally, and should not be
written by the programmer.
\item[\refqualclass{checker/signedness/qual}{SignednessBottom}]
indicates that the value is \<null>.
This annotation is used internally, and should not
be written by the programmer.
\end{description}
\subsectionAndLabel{Default qualifiers}{signedness-checker-annotations-default-qualifiers}
The only type qualifier that the programmer should need to write is
\refqualclass{checker/signedness/qual}{Unsigned}.
When a programmer leaves an expression unannotated, the
Signedness Checker treats it in one of the following ways:
\begin{itemize}
\item
All \code{byte}, \code{short}, \code{int}, and \code{long} literals default
to \refqualclass{checker/signedness/qual}{SignednessGlb}.
\item
All \code{byte}, \code{short}, \code{int}, and \code{long} variables default
to \refqualclass{checker/signedness/qual}{Signed}.
\item
All other expressions default to \refqualclass{checker/signedness/qual}{UnknownSignedness}.
\end{itemize}
\sectionAndLabel{Prohibited operations}{signedness-checker-prohibited-operations}
The Signedness Checker prohibits the following uses of operators:
\begin{itemize}
\item
Division (\code{/}) or modulus (\code{\%}) with an \code{@Unsigned}
operand.
\item
Signed right shift (\verb|>>|) with an \code{@Unsigned} left operand.
\item
Unsigned right shift (\verb|>>>|) with a \code{@Signed} left operand.
\item
Greater/less than (or equal) comparators
(\code{<}, \code{<=}, \code{>}, \code{>=}) with an \code{@Unsigned}
operand.
\item
Any other binary operator with one \code{@Unsigned} operand and one
\code{@Signed} operand, with the exception of left shift (\verb|<<|).
\end{itemize}
Like every type-checker built with the Checker Framework, the Signedness
Checker ensures that assignments and pseudo-assignments have consistent types.
For example, it is not permitted to assign a \code{@Signed} expression to an
\code{@Unsigned} variable or vice versa.
\sectionAndLabel{Rationale}{signedness-checker-rationale}
The Signedness Checker prevents misuse of unsigned values in Java code.
Most Java operations interpret operands as signed. If applied to unsigned
values, those operations would produce unexpected, incorrect results.
Consider the following Java code:
\begin{Verbatim}
public class SignednessManualExample {
int s1 = -2;
int s2 = -1;
@Unsigned int u1 = 2147483646; // unsigned: 2^32 - 2, signed: -2
@Unsigned int u2 = 2147483647; // unsigned: 2^32 - 1, signed: -1
void m() {
int w = s1 / s2; // OK: result is 2, which is correct for -2 / -1
int x = u1 / u2; // ERROR: result is 2, which is incorrect for (2^32 - 2) / (2^32 - 1)
}
int s3 = -1;
int s4 = 5;
@Unsigned int u3 = 2147483647; // unsigned: 2^32 - 1, signed: -1
@Unsigned int u4 = 5;
void m2() {
int y = s3 % s4; // OK: result is -1, which is correct for -1 % 5
int z = u3 % u4; // ERROR: result is -1, which is incorrect for (2^32 - 1) % 5 = 2
}
}
\end{Verbatim}
These examples illustrate why division and modulus with an unsigned operand
are illegal. Other uses of operators are prohibited for similar reasons.
\sectionAndLabel{Utility routines for manipulating unsigned values}{signedness-utilities}
Class \refclass{checker/signedness}{SignednessUtil} provides static
utility methods for working with unsigned values. Some of these
re-implement functionality in JDK 8, making it available in earlier
versions of Java. Others provide new functionality. All of them are
properly annotated with \refqualclass{checker/signedness/qual}{Unsigned}
where appropriate, so using them may reduce the number of annotations that
you need to write.
Class \refclass{checker/signedness}{SignednessUtilExtra} contains more utility
methods that reference packages not included in Android. This class is not
included in \code{checker-qual.jar}, so you may want to copy the methods to your code.
\sectionAndLabel{Local type refinement}{signedness-refinement}
Local type refinment/inference (Section~\ref{type-refinement}) may be
surprising for the Signedness type system. Ordinarily, an expression with
unsigned type may not participate in a division, as shown in
Sections~\ref{signedness-checker-prohibited-operations}
and~\ref{signedness-checker-rationale}. However, if a constant is assigned
to a variable that was declared with \<@Unsigned> type, then---just like
the constant---the variable may be treated as either signed or unsigned.
For example, it can participate in division. Since the result of the
division is signed, you cannot accidentally assign the division result to
an \<@Unsigned> variable.
\begin{Verbatim}
void useLocalVariables() {
int s1 = -2;
int s2 = -1;
@Unsigned int u1 = 2147483646; // unsigned: 2^32 - 2, signed: -2
@Unsigned int u2 = 2147483647; // unsigned: 2^32 - 1, signed: -1
int w = s1 / s2; // OK: result is 2, which is correct for -2 / -1
int x = u1 / u2; // OK; computation over constants, interpreted as signed; result is signed
}
\end{Verbatim}
|
