Signedness Checker Annotations

/**
 * The value is 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 number.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({UnknownSignedness.class})
@DefaultQualifierInHierarchy
@DefaultFor(
    typeKinds = {
        TypeKind.BYTE, TypeKind.INT, TypeKind.LONG, TypeKind.SHORT,
        TypeKind.FLOAT, TypeKind.DOUBLE
    },
    types = {
        java.lang.Byte.class, java.lang.Integer.class, java.lang.Long.class,
        java.lang.Short.class, java.lang.Float.class, java.lang.Double.class
    },
    value = TypeUseLocation.EXCEPTION_PARAMETER)
public @interface Signed {}

import org.checkerframework.checker.signedness.qual.Signed;

public class SignedExample {
    // Explicitly signed values (though this is the default)
    @Signed int temperature = -10; // Can be negative
    @Signed long accountBalance = -1000L; // Can represent debt
    
    // Method working with signed values
    public @Signed int calculateDifference(@Signed int a, @Signed int b) {
        return a - b; // Result can be negative
    }
    
    // Safe signed operations
    public void processSignedData(@Signed byte[] data) {
        for (@Signed byte b : data) {
            if (b < 0) {
                // Handle negative values appropriately
                System.out.println("Negative byte: " + b);
            }
        }
    }
}

/**
 * The value is 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 number rather than as a negative number.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({UnknownSignedness.class})
@DefaultFor(
    typeKinds = {TypeKind.CHAR},
    types = {java.lang.Character.class})
public @interface Unsigned {}

import org.checkerframework.checker.signedness.qual.Unsigned;

public class UnsignedExample {
    // Unsigned values - always interpreted as positive
    @Unsigned int pixelColor = 0xFF0000FF; // RGBA color value
    @Unsigned byte[] hashBytes; // Hash values are unsigned
    
    // Method working with unsigned byte data
    public void processUnsignedBytes(@Unsigned byte[] data) {
        for (@Unsigned byte b : data) {
            // Interpret as 0-255, not -128 to 127
            int unsignedValue = Byte.toUnsignedInt(b);
            System.out.println("Unsigned value: " + unsignedValue);
        }
    }
    
    // Network protocol handling
    public @Unsigned int parseUnsignedInt(@Unsigned byte[] bytes) {
        // Build unsigned integer from byte array
        return ((bytes[0] & 0xFF) << 24) |
               ((bytes[1] & 0xFF) << 16) |
               ((bytes[2] & 0xFF) << 8) |
                (bytes[3] & 0xFF);
    }
    
    // File size handling
    public long getFileSize(@Unsigned int highBytes, @Unsigned int lowBytes) {
        return (((long) highBytes) << 32) | (lowBytes & 0xFFFFFFFFL);
    }
}

/**
 * The expression's value is in the signed positive range; that is, its most significant bit is zero.
 * The value has the same interpretation as @Signed and @Unsigned — both interpretations are equivalent.
 * 
 * Programmers should rarely write @SignedPositive. Instead, write @Signed or @Unsigned 
 * to indicate the intended interpretation.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(SignednessGlb.class)
public @interface SignedPositive {}

import org.checkerframework.checker.signedness.qual.SignedPositive;

public class SignedPositiveExample {
    // Values that are definitely positive (MSB = 0)
    @SignedPositive int count = 42; // Always positive
    @SignedPositive long timestamp = System.currentTimeMillis();
    
    // Method that ensures positive values
    public @SignedPositive int absoluteValue(@Signed int value) {
        return Math.abs(value); // Result is always positive
    }
    
    // Safe for both signed and unsigned operations
    public void processSafeValue(@SignedPositive int value) {
        // Safe to use in both contexts
        @Signed int signedView = value;     // OK - positive value
        @Unsigned int unsignedView = value; // OK - positive value
    }
}

/**
 * A polymorphic qualifier for signedness types.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@PolymorphicQualifier(UnknownSignedness.class)
public @interface PolySigned {}

import org.checkerframework.checker.signedness.qual.PolySigned;

public class PolySignedExample {
    // Preserves signedness of input
    public @PolySigned int identity(@PolySigned int value) {
        return value; // Same signedness as input
    }
    
    // Bitwise operations preserving signedness
    public @PolySigned int bitwiseAnd(@PolySigned int a, @PolySigned int b) {
        return a & b; // Preserves signedness interpretation
    }
    
    // Array processing with preserved signedness
    public @PolySigned int[] processArray(@PolySigned int[] input) {
        @PolySigned int[] result = new @PolySigned int[input.length];
        for (int i = 0; i < input.length; i++) {
            result[i] = input[i] * 2; // Maintains signedness
        }
        return result;
    }
}

/**
 * The value's signedness is not known to the Signedness Checker.
 * This is also used for non-numeric values, which cannot have a signedness.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({})
public @interface UnknownSignedness {}

/**
 * The greatest lower bound (GLB) of @Signed and @Unsigned.
 * Represents values that could be interpreted as either signed or unsigned.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({Signed.class, Unsigned.class})
public @interface SignednessGlb {}

/**
 * The bottom type in the signedness hierarchy.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({SignedPositive.class})
@TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, TypeUseLocation.EXPLICIT_UPPER_BOUND})
public @interface SignednessBottom {}

import org.checkerframework.checker.signedness.qual.*;

public class IOExample {
    // Reading unsigned byte data
    public void readUnsignedBytes(InputStream is) throws IOException {
        @Unsigned byte[] buffer = new @Unsigned byte[1024];
        int bytesRead = is.read(buffer);
        
        for (int i = 0; i < bytesRead; i++) {
            @Unsigned byte b = buffer[i];
            int unsignedValue = Byte.toUnsignedInt(b); // 0-255 range
            processUnsignedByte(unsignedValue);
        }
    }
    
    // Network protocol with unsigned integers
    public @Unsigned int readUnsignedInt32(DataInputStream dis) throws IOException {
        return dis.readInt(); // Interpret as unsigned 32-bit value
    }
}

public class CryptoExample {
    // Hash values are always unsigned
    public @Unsigned byte[] computeHash(byte[] input) {
        MessageDigest md = MessageDigest.getInstance("SHA-256");
        return md.digest(input);
    }
    
    // Bitwise operations on unsigned data
    public @Unsigned int combineUnsignedBytes(@Unsigned byte[] bytes) {
        @Unsigned int result = 0;
        for (@Unsigned byte b : bytes) {
            result = (result << 8) | (b & 0xFF);
        }
        return result;
    }
}

// Import statements for using signedness annotations
import org.checkerframework.checker.signedness.qual.Signed;
import org.checkerframework.checker.signedness.qual.Unsigned;
import org.checkerframework.checker.signedness.qual.SignedPositive;
import org.checkerframework.checker.signedness.qual.PolySigned;
import org.checkerframework.checker.signedness.qual.UnknownSignedness;
import org.checkerframework.checker.signedness.qual.SignednessGlb;
import org.checkerframework.checker.signedness.qual.SignednessBottom;

// Utility methods for safe signedness conversions
public class SignednessUtils {
    // Convert signed to unsigned interpretation
    public static @Unsigned int toUnsigned(@Signed int value) {
        return value; // Same bits, different interpretation
    }
    
    // Convert unsigned to signed interpretation  
    public static @Signed int toSigned(@Unsigned int value) {
        return value; // Same bits, different interpretation
    }
    
    // Safe unsigned comparison
    public static boolean unsignedLessThan(@Unsigned int a, @Unsigned int b) {
        return Integer.compareUnsigned(a, b) < 0;
    }
}