The Checker Framework Manual:
Custom pluggable types for Java

Chapter 21 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 the integral types byte, short, int, and long and their boxed variants Byte, Short, Integer, and Long. char and Character are always unsigned. Floating-point types float, double, Float, and Double are always signed.

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 non-negative, but just because a variable’s value is non-negative 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 @NonNegative annotation of the Index Checker (see Chapter 11) or the @IntRange annotation of the Constant Value Checker (see Chapter 24).

The Signedness Checker trusts a @NonNegative or @Positive annotation on a byte, short, int, or long expression. To verify these annotations, also run the Index Checker. A char is always non-negative, so these annotations do not affect a char expression; a char expression has type @SignedPositive only when range analysis determines that its value is between 0 and 127.

Additional details appear in the paper “Preventing signedness errors in numerical computations in Java” [Mac16] (FSE 2016).

To run the Signedness Checker, run javac with -processor org.checkerframework.checker.signedness.SignednessChecker.

21.1 Annotations

The Signedness Checker uses type annotations to indicate the signedness that the programmer intends an expression to have.

These are the qualifiers in the signedness type system:

@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.

@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.

@SignedPositive

indicates that a value is known at compile time to be in the non-negative signed range, so it has the same interpretation as signed or unsigned and may be used with either interpretation. (Equivalently, the most significant bit is guaranteed to be 0.) Programmers should usually write @Signed or @Unsigned instead.

@SignednessGlb

indicates that a value may be interpreted as unsigned or signed. It covers the same cases as @SignedPositive, plus manifest literals, to prevent the programmer from having to annotate them all explicitly. Programmers should rarely write this annotation, except on fields whose value is a negative manifest literal.

@PolySigned

indicates qualifier polymorphism. When two formal parameter types are annotated with @PolySigned, the two arguments at a call site must have the same signedness type annotation. (This differs from the standard rule for polymorphic qualifiers.) For a description of qualifier polymorphism, see Section 32.2.

@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.

@SignednessBottom

indicates that the value is null. This annotation is used internally, and should not be written by the programmer.

21.1.1 Default qualifiers

The only type qualifier that the programmer should need to write is @Unsigned. When a programmer leaves an expression unannotated, the Signedness Checker treats it in one of the following ways:

• • All byte, short, int, and long literals default to @SignednessGlb.

• • All char and Character expressions are @Unsigned; this cannot be changed.

• • All char and Character variables are @Unsigned; this cannot be changed.

• • All other expressions default to @Signed.

21.2 Prohibited operations

The Signedness Checker prohibits the following uses of operators:

• • Division (/) or modulus (%) with an @Unsigned operand.

• • Signed right shift (>>) with an @Unsigned left operand.

• • Unsigned right shift (>>>) with a @Signed left operand.

• • Greater/less than (or equal) comparators (<, <=, >, >=) with an @Unsigned operand.

• • Any other binary operator with one @Unsigned operand and one @Signed operand, with the exception of left shift (<<).

There are some special cases where these operations are permitted; see Section 21.2.2.

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 @Signed expression to an @Unsigned variable or vice versa.

21.2.1 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:

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
    }
}

These examples illustrate why division and modulus with an unsigned operand are illegal. Other uses of operators are prohibited for similar reasons.

21.2.2 Permitted shifts

As exceptions to the rules given above, the Signedness Checker permits certain right shifts that are immediately followed by a cast or masking operation.

For example, right shift by 8 then mask by 0xFF evaluates to the same value whether the argument is interpreted as signed or unsigned. Thus, the Signedness Checker permits both ((myInt >> 8) & 0xFF) and ((myInt >>> 8) & 0xFF), regardless of the qualifier on the type of myInt.

Likewise, right shift by 8 then cast to byte evaluates to the same value whether the argument is interpreted as signed or unsigned, so the Signedness Checker permits both (byte) (myInt >> 8) and (byte) (myInt >>> 8), regardless of the type of myInt.

21.3 Utility routines for manipulating unsigned values

Class SignednessUtil provides static utility methods for working with unsigned values. They are properly annotated with @Unsigned where appropriate, so using them may reduce the number of annotations that you need to write. To use the SignednessUtil class, the checker-util.jar file must be on the classpath at run time.

Class SignednessUtilExtra contains more utility methods that reference packages not included in Android. This class is not included in checker-util.jar, so you may want to copy the methods to your code.

21.4 Local type refinement

Local type refinement/inference (Section 33.7) may be surprising for the Signedness type system. Ordinarily, an expression with unsigned type may not participate in a division, as shown in Sections 21.2 and 21.2.1. 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, due to local type refinement (Section 33.7). For example, it can participate in division.

    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
    }

To prevent local type refinement, use a cast:

         @Unsigned int u1 = (@Unsigned int) 2147483646;

Note that type-checking produces a different result for int x = u1 / u2; here than in the similar example in Section 21.2.1. In Section 21.2.1, the method is reading fields, and all it knows is the declared type of the field. In Section 21.4, the method is reading a local variable, and dataflow (that is, flow-sensitive type refinement) refines the types of local variables.

21.5 Instantiating polymorphism

When calling a method with formal parameters annotated as @PolySigned, all arguments for @PolySigned formal parameters must have comparable types. (One way to do this is for all types to be the same.) This is different than the usual rules for polymorphic qualifiers. If you violate this rule, then the Signedness Checker’s error messages can be obscure, because they are about @SignednessBottom. You can fix the signedness error messages by casting the arguments.

21.6 Other signedness annotations

The Checker Framework’s signedness annotations are similar to annotations used elsewhere.

If your code is already annotated with a different annotation, the Checker Framework can type-check your code. It treats annotations from other tools as if you had written the corresponding annotation from the Signedness Checker, as described in Figure 21.2.