Checker Framework Tutorial

This section of the tutorial is only for those who are interested in writing their own type-checkers. Please feel free to skip this section.

Although the Checker Framework ships with several checkers, it is often useful to write a custom checker. Perhaps there are other runtime exceptions you wish to prevent or maybe other properties of data that should always hold. In both these cases and others, you you might wish to write your own type checker. This section of the tutorial is for those who are interested in writing their own type-checkers. If you do not wish to write a new type-checker, feel free to skip this section.

Consider a hypothetical Encrypted type qualifier, which denotes that the representation of an object (such as a String, CharSequence, or byte[]) is encrypted. This project has three source files: Encrypted.java and PossibleUnencrypted.java , the type annotation definitions, and EncryptedDemo.java , the example program that use the Encrypted checker.

1. Write the type annotation definitions

For this example, the annotation definitions have already been written, Encrypted.java and PossibleUnencrypted.java. Please see the manual for further explanation of this file.

This code needs to be compiled with the Checker Framework compiler.

$ javacheck myqual/Encrypted.java
$ javacheck myqual/PossibleUnencrypted.java
                

The resulting .class files should either be on your classpath, or on the processor path (set via the -processorpath command-line option to javac).

2. Run the Encryption Checker

The @Encrypted annotations have already been written in EncryptionDemo.java. Types without annotations are defaulted to @PossibleUnencrypted. Invoke the compiler with the Subtyping Checker, specifying the @Encrypted and @PossibleUnencrypted annotations using the -Aquals option. You should add the Encrypted and PossibleUnencrypted classfiles to the processor classpath:

javacheck  -processor org.checkerframework.common.subtyping.SubtypingChecker -Aquals=myqual.Encrypted,myqual.PossibleUnencrypted encrypted/EncryptionDemo.java
encrypted/EncryptionDemo.java:21: error: [assignment.type.incompatible] incompatible types in assignment.
        /*@Encrypted*/ int encryptInt = (character + OFFSET) % Character.MAX_VALUE ;
                                                             ^
  found   : @PossibleUnencrypted int
  required: @Encrypted int
encrypted/EncryptionDemo.java:32: error: [argument.type.incompatible] incompatible types in argument.
        sendOverInternet(password);
                         ^
  found   : @PossibleUnencrypted String
  required: @Encrypted String
2 errors
                

3. Suppress the First Error

The first error needs to be suppressed, because the string on the left is considered "encrypted" in this encryption scheme. All @SuppressWarnings should have a comment explaining why suppressing the warning is the correct action. See the correction below.

// The SuppressWarnings is necessary because, the type system is not capable of
// validating that the return value is encrypted. -SOM 01/25/2013
@SuppressWarnings("encrypted")
private /*@Encrypted*/ char encryptCharacter(char character) {
                

4. Run the Encryption Checker

You should just see the following error.

encrypted/EncryptionDemo.java:34: error: [argument.type.incompatible] incompatible types in argument.
        sendOverInternet(password);
                         ^
  found   : @PossibleUnencrypted String
  required: @Encrypted String
1 error
                

This is a real error, because the programmer is trying to send a password over the internet without encrypting it first.

5. Correct the Second Error

The password should be encrypted before it is sent over the internet. The correction is below.

void sendPassword() {
   String password = getUserPassword();
   sendOverInternet(encrypt(password));
}