0
# Signedness Checker Annotations
1

2
Signedness Checker annotations distinguish between signed and unsigned interpretations of integer types. While Java's integer types are inherently signed, this checker helps prevent errors when working with unsigned values (such as those from C libraries, byte arrays, or bitwise operations) by tracking the intended interpretation of numeric values.
3

4
## Capabilities
5

6
### Signed Integer Type
7

8
Indicates that the value should be interpreted as signed (default for most Java integer types).
9

10
```java { .api }
11
/**
12
 * The value is to be interpreted as signed. That is, if the most significant bit
13
 * in the bitwise representation is set, then the bits should be interpreted as a negative number.
14
 */
15
@Documented
16
@Retention(RetentionPolicy.RUNTIME)
17
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
18
@SubtypeOf({UnknownSignedness.class})
19
@DefaultQualifierInHierarchy
20
@DefaultFor(
21
    typeKinds = {
22
        TypeKind.BYTE, TypeKind.INT, TypeKind.LONG, TypeKind.SHORT,
23
        TypeKind.FLOAT, TypeKind.DOUBLE
24
    },
25
    types = {
26
        java.lang.Byte.class, java.lang.Integer.class, java.lang.Long.class,
27
        java.lang.Short.class, java.lang.Float.class, java.lang.Double.class
28
    },
29
    value = TypeUseLocation.EXCEPTION_PARAMETER)
30
public @interface Signed {}
31
```
32

33
**Usage Examples:**
34

35
```java
36
import org.checkerframework.checker.signedness.qual.Signed;
37

38
public class SignedExample {
39
    // Explicitly signed values (though this is the default)
40
    @Signed int temperature = -10; // Can be negative
41
    @Signed long accountBalance = -1000L; // Can represent debt
42
    
43
    // Method working with signed values
44
    public @Signed int calculateDifference(@Signed int a, @Signed int b) {
45
        return a - b; // Result can be negative
46
    }
47
    
48
    // Safe signed operations
49
    public void processSignedData(@Signed byte[] data) {
50
        for (@Signed byte b : data) {
51
            if (b < 0) {
52
                // Handle negative values appropriately
53
                System.out.println("Negative byte: " + b);
54
            }
55
        }
56
    }
57
}
58
```
59

60
### Unsigned Integer Type
61

62
Indicates that the value should be interpreted as unsigned (positive values with extended range).
63

64
```java { .api }
65
/**
66
 * The value is to be interpreted as unsigned. That is, if the most significant bit
67
 * in the bitwise representation is set, then the bits should be interpreted as a
68
 * large positive number rather than as a negative number.
69
 */
70
@Documented
71
@Retention(RetentionPolicy.RUNTIME)
72
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
73
@SubtypeOf({UnknownSignedness.class})
74
@DefaultFor(
75
    typeKinds = {TypeKind.CHAR},
76
    types = {java.lang.Character.class})
77
public @interface Unsigned {}
78
```
79

80
**Usage Examples:**
81

82
```java
83
import org.checkerframework.checker.signedness.qual.Unsigned;
84

85
public class UnsignedExample {
86
    // Unsigned values - always interpreted as positive
87
    @Unsigned int pixelColor = 0xFF0000FF; // RGBA color value
88
    @Unsigned byte[] hashBytes; // Hash values are unsigned
89
    
90
    // Method working with unsigned byte data
91
    public void processUnsignedBytes(@Unsigned byte[] data) {
92
        for (@Unsigned byte b : data) {
93
            // Interpret as 0-255, not -128 to 127
94
            int unsignedValue = Byte.toUnsignedInt(b);
95
            System.out.println("Unsigned value: " + unsignedValue);
96
        }
97
    }
98
    
99
    // Network protocol handling
100
    public @Unsigned int parseUnsignedInt(@Unsigned byte[] bytes) {
101
        // Build unsigned integer from byte array
102
        return ((bytes[0] & 0xFF) << 24) |
103
               ((bytes[1] & 0xFF) << 16) |
104
               ((bytes[2] & 0xFF) << 8) |
105
                (bytes[3] & 0xFF);
106
    }
107
    
108
    // File size handling
109
    public long getFileSize(@Unsigned int highBytes, @Unsigned int lowBytes) {
110
        return (((long) highBytes) << 32) | (lowBytes & 0xFFFFFFFFL);
111
    }
112
}
113
```
114

115
### Signed Positive Type
116

117
Indicates values that are positive in both signed and unsigned interpretations.
118

119
```java { .api }
120
/**
121
 * The expression's value is in the signed positive range; that is, its most significant bit is zero.
122
 * The value has the same interpretation as @Signed and @Unsigned — both interpretations are equivalent.
123
 * 
124
 * Programmers should rarely write @SignedPositive. Instead, write @Signed or @Unsigned 
125
 * to indicate the intended interpretation.
126
 */
127
@Documented
128
@Retention(RetentionPolicy.RUNTIME)
129
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
130
@SubtypeOf(SignednessGlb.class)
131
public @interface SignedPositive {}
132
```
133

134
**Usage Examples:**
135

136
```java
137
import org.checkerframework.checker.signedness.qual.SignedPositive;
138

139
public class SignedPositiveExample {
140
    // Values that are definitely positive (MSB = 0)
141
    @SignedPositive int count = 42; // Always positive
142
    @SignedPositive long timestamp = System.currentTimeMillis();
143
    
144
    // Method that ensures positive values
145
    public @SignedPositive int absoluteValue(@Signed int value) {
146
        return Math.abs(value); // Result is always positive
147
    }
148
    
149
    // Safe for both signed and unsigned operations
150
    public void processSafeValue(@SignedPositive int value) {
151
        // Safe to use in both contexts
152
        @Signed int signedView = value;     // OK - positive value
153
        @Unsigned int unsignedView = value; // OK - positive value
154
    }
155
}
156
```
157

158
### Polymorphic Signedness
159

160
Creates polymorphic relationships preserving signedness across method calls.
161

162
```java { .api }
163
/**
164
 * A polymorphic qualifier for signedness types.
165
 */
166
@Documented
167
@Retention(RetentionPolicy.RUNTIME)
168
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
169
@PolymorphicQualifier(UnknownSignedness.class)
170
public @interface PolySigned {}
171
```
172

173
**Usage Examples:**
174

175
```java
176
import org.checkerframework.checker.signedness.qual.PolySigned;
177

178
public class PolySignedExample {
179
    // Preserves signedness of input
180
    public @PolySigned int identity(@PolySigned int value) {
181
        return value; // Same signedness as input
182
    }
183
    
184
    // Bitwise operations preserving signedness
185
    public @PolySigned int bitwiseAnd(@PolySigned int a, @PolySigned int b) {
186
        return a & b; // Preserves signedness interpretation
187
    }
188
    
189
    // Array processing with preserved signedness
190
    public @PolySigned int[] processArray(@PolySigned int[] input) {
191
        @PolySigned int[] result = new @PolySigned int[input.length];
192
        for (int i = 0; i < input.length; i++) {
193
            result[i] = input[i] * 2; // Maintains signedness
194
        }
195
        return result;
196
    }
197
}
198
```
199

200
### Unknown Signedness
201

202
Indicates that the signedness is not known or not applicable.
203

204
```java { .api }
205
/**
206
 * The value's signedness is not known to the Signedness Checker.
207
 * This is also used for non-numeric values, which cannot have a signedness.
208
 */
209
@Documented
210
@Retention(RetentionPolicy.RUNTIME)
211
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
212
@SubtypeOf({})
213
public @interface UnknownSignedness {}
214
```
215

216
### Signedness Hierarchy Annotations
217

218
Additional annotations for the signedness type hierarchy.
219

220
```java { .api }
221
/**
222
 * The greatest lower bound (GLB) of @Signed and @Unsigned.
223
 * Represents values that could be interpreted as either signed or unsigned.
224
 */
225
@Documented
226
@Retention(RetentionPolicy.RUNTIME)
227
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
228
@SubtypeOf({Signed.class, Unsigned.class})
229
public @interface SignednessGlb {}
230

231
/**
232
 * The bottom type in the signedness hierarchy.
233
 */
234
@Documented
235
@Retention(RetentionPolicy.RUNTIME)
236
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
237
@SubtypeOf({SignedPositive.class})
238
@TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, TypeUseLocation.EXPLICIT_UPPER_BOUND})
239
public @interface SignednessBottom {}
240
```
241

242
## Common Usage Patterns
243

244
**File I/O and Network Operations:**
245

246
```java
247
import org.checkerframework.checker.signedness.qual.*;
248

249
public class IOExample {
250
    // Reading unsigned byte data
251
    public void readUnsignedBytes(InputStream is) throws IOException {
252
        @Unsigned byte[] buffer = new @Unsigned byte[1024];
253
        int bytesRead = is.read(buffer);
254
        
255
        for (int i = 0; i < bytesRead; i++) {
256
            @Unsigned byte b = buffer[i];
257
            int unsignedValue = Byte.toUnsignedInt(b); // 0-255 range
258
            processUnsignedByte(unsignedValue);
259
        }
260
    }
261
    
262
    // Network protocol with unsigned integers
263
    public @Unsigned int readUnsignedInt32(DataInputStream dis) throws IOException {
264
        return dis.readInt(); // Interpret as unsigned 32-bit value
265
    }
266
}
267
```
268

269
**Cryptographic Operations:**
270

271
```java
272
public class CryptoExample {
273
    // Hash values are always unsigned
274
    public @Unsigned byte[] computeHash(byte[] input) {
275
        MessageDigest md = MessageDigest.getInstance("SHA-256");
276
        return md.digest(input);
277
    }
278
    
279
    // Bitwise operations on unsigned data
280
    public @Unsigned int combineUnsignedBytes(@Unsigned byte[] bytes) {
281
        @Unsigned int result = 0;
282
        for (@Unsigned byte b : bytes) {
283
            result = (result << 8) | (b & 0xFF);
284
        }
285
        return result;
286
    }
287
}
288
```
289

290
## Type Definitions
291

292
```java { .api }
293
// Import statements for using signedness annotations
294
import org.checkerframework.checker.signedness.qual.Signed;
295
import org.checkerframework.checker.signedness.qual.Unsigned;
296
import org.checkerframework.checker.signedness.qual.SignedPositive;
297
import org.checkerframework.checker.signedness.qual.PolySigned;
298
import org.checkerframework.checker.signedness.qual.UnknownSignedness;
299
import org.checkerframework.checker.signedness.qual.SignednessGlb;
300
import org.checkerframework.checker.signedness.qual.SignednessBottom;
301

302
// Utility methods for safe signedness conversions
303
public class SignednessUtils {
304
    // Convert signed to unsigned interpretation
305
    public static @Unsigned int toUnsigned(@Signed int value) {
306
        return value; // Same bits, different interpretation
307
    }
308
    
309
    // Convert unsigned to signed interpretation  
310
    public static @Signed int toSigned(@Unsigned int value) {
311
        return value; // Same bits, different interpretation
312
    }
313
    
314
    // Safe unsigned comparison
315
    public static boolean unsignedLessThan(@Unsigned int a, @Unsigned int b) {
316
        return Integer.compareUnsigned(a, b) < 0;
317
    }
318
}
319
```