The Checker Framework Manual:
Custom pluggable types for Java

Chapter 30 Subtyping Checker

The Subtyping Checker enforces only subtyping rules. It operates over annotations specified by a user on the command line. Thus, users can create a simple type-checker without writing any code beyond definitions of the type qualifier annotations.

The Subtyping Checker can accommodate all of the type system enhancements that can be declaratively specified (see Chapter 37). This includes type introduction rules via the @QualifierForLiterals meta-annotation, and other features such as type refinement (Section 33.7) and qualifier polymorphism (Section 32.2).

The Subtyping Checker is also useful to type system designers who wish to experiment with a checker before writing code; the Subtyping Checker demonstrates the functionality that a checker inherits from the Checker Framework.

If you need typestate analysis, then you can extend a typestate checker. For more details (including a definition of “typestate”), see Section 31.30. See Section 40.7.1 for a simpler alternative.

For type systems that require special checks (e.g., warning about dereferences of possibly-null values), you will need to write code and extend the framework as discussed in Chapter 37.

30.1 Using the Subtyping Checker

The Subtyping Checker is used in the same way as other checkers (using the -processor org.checkerframework.common.subtyping.SubtypingChecker option; see Chapter 2), except that it requires an additional annotation processor argument via the standard “-A” switch. You must provide one or both of the two following command-line arguments:

• • Provide the fully-qualified class name(s) of the annotation(s) in the custom type system through the -Aquals option, using a comma-no-space-separated notation:

    javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \
          -processor org.checkerframework.common.subtyping.SubtypingChecker \
          -Aquals=myPackage.qual.MyQual,myPackage.qual.OtherQual MyFile.java ...
  

• • Provide the fully-qualified paths to a set of directories that contain the annotations in the custom type system through the -AqualDirs option, using a colon-no-space-separated notation. For example, if the Checker Framework is on the classpath rather than the processorpath:

    javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \
          -processor org.checkerframework.common.subtyping.SubtypingChecker \
          -AqualDirs=/full/path/to/myProject/bin:/full/path/to/myLibrary/bin MyFile.java
  

If the Checker Framework is on the processorpath, place the annotations on the processorpath instead of on the classpath.

30.1.1 Compiling your qualifiers and your project

The annotations listed in -Aquals or -AqualDirs must be accessible to the compiler during compilation. Before you run the Subtyping Checker with javac, they must be compiled and on the same path (the classpath or processorpath) as the Checker Framework. It is not sufficient to supply their source files on the command line.

30.1.2 Suppressing warnings from the Subtyping Checker

When suppressing a warning issued by the Subtyping Checker, as the “checker name” you may use the unqualified, uncapitalized name of any of the annotations passed to -Aquals. (See Section 34.1.1 for details about the @SuppressWarnings syntax.) As a matter of style, you should choose one of the annotations as the “checker name” part of the @SuppressWarnings string and use it consistently; this avoids confusion and makes it easier to search for uses.

30.2 Subtyping Checker example

Consider a hypothetical Encrypted type qualifier, which denotes that the representation of an object (such as a String, CharSequence, or byte[]) is encrypted. To use the Subtyping Checker for the Encrypted type system, follow these steps.

(This example also appears in the Checker Framework Tutorial, in more detail.)

• 1. Define two annotations for the Encrypted and PossiblyUnencrypted qualifiers:

  package myPackage.qual;
  
  import   org.checkerframework.framework.qual.DefaultFor;
  import   org.checkerframework.framework.qual.SubtypeOf;
  import   org.checkerframework.framework.qual.TypeUseLocation;
  import   java.lang.annotation.ElementType;
  import   java.lang.annotation.Target;
  
  /**
   * Denotes that the representation of an object is encrypted.
   */
  @SubtypeOf(PossiblyUnencrypted.class)
  @DefaultFor({TypeUseLocation.LOWER_BOUND})
  @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
  public @interface Encrypted {}
  

   

  package myPackage.qual;
  
  import   org.checkerframework.framework.qual.DefaultQualifierInHierarchy;
  import   org.checkerframework.framework.qual.SubtypeOf;
  import   java.lang.annotation.ElementType;
  import   java.lang.annotation.Target;
  
  /**
   * Denotes that the representation of an object might not be encrypted.
   */
  @DefaultQualifierInHierarchy
  @SubtypeOf({})
  @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
  public @interface PossiblyUnencrypted {}
  

  Note that all custom annotations must have the @Target(ElementType.TYPE_USE) meta-annotation. See Section 37.5.1.

  Don’t forget to compile these classes:

  $ javac myPackage/qual/Encrypted.java myPackage/qual/PossiblyUnencrypted.java
  

  The resulting .class files should be on the same path (the classpath or processor path) as the Checker Framework.

• 2. Write @Encrypted annotations in your program (say, in file YourProgram.java):

  import myPackage.qual.Encrypted;
  
  ...
  
  public @Encrypted String encrypt(String text) {
      // ...
  }
  
  // Only send encrypted data!
  public void sendOverInternet(@Encrypted String msg) {
      // ...
  }
  
  void sendText() {
      // ...
      @Encrypted String ciphertext = encrypt(plaintext);
      sendOverInternet(ciphertext);
      // ...
  }
  
  void sendPassword() {
      String password = getUserPassword();
      sendOverInternet(password);
  }
  

  You may also need to add @SuppressWarnings annotations to the encrypt and decrypt methods. Analyzing them is beyond the capability of any realistic type system.

• 3. Invoke the compiler with the Subtyping Checker, specifying the @Encrypted annotation using the -Aquals option. You should add the Encrypted classfile to the processor classpath:

    javac -processorpath myqualpath -processor org.checkerframework.common.subtyping.SubtypingChecker \
          -Aquals=myPackage.qual.Encrypted,myPackage.qual.PossiblyUnencrypted YourProgram.java
  
  YourProgram.java:42: incompatible types.
  found   : @myPackage.qual.PossiblyUnencrypted java.lang.String
  required: @myPackage.qual.Encrypted java.lang.String
      sendOverInternet(password);
                       ^
  

• 4. You can also provide the fully-qualified paths to a set of directories that contain the qualifiers using the -AqualDirs option, and add the directories to the boot classpath, for example:

    javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \
          -processor org.checkerframework.common.subtyping.SubtypingChecker \
          -AqualDirs=/full/path/to/myProject/bin:/full/path/to/myLibrary/bin YourProgram.java
  

  Note that in these two examples, the compiled class file of the myPackage.qual.Encrypted and myPackage.qual.PossiblyUnencrypted annotations must exist in either the myProject/bin directory or the myLibrary/bin directory. The following placement of the class files will work with the above commands:

    .../myProject/bin/myPackage/qual/Encrypted.class
    .../myProject/bin/myPackage/qual/PossiblyUnencrypted.class
  

Also, see the example project in the docs/examples/subtyping-extension directory.

30.3 Type aliases and typedefs

A type alias or typedef is a type that shares the same representation as another type but is conceptually distinct from it. For example, some strings in your program may be street addresses; others may be passwords; and so on. You wish to indicate, for each string, which one it is, and to avoid mixing up the different types of strings. Likewise, you could distinguish integers that are offsets from those that are absolute values.

Creating a new type makes your code easier to understand by conveying the intended use of each variable. It also prevents errors that come from using the wrong type or from mixing incompatible types in an operation.

If you want to create a type alias or typedef, you have multiple options: a regular Java subtype, the Units Checker (Chapter 20), the Fake Enum Checker (Chapter 9), or the Subtyping Checker.

A Java subtype is easy to create and does not require a tool such as the Checker Framework; for instance, you would declare class Address extends String. There are a number of limitations to this “pseudo-typedef”, however [Goe06]. Primitive types and final types (including String) cannot be extended. Equality and identity tests can return incorrect results when a wrapper object is used. Existing return types in code would need to be changed, which is easy with an annotation but disruptive when changing the Java type. Therefore, it is best to avoid the pseudo-typedef antipattern.

The Units Checker (Chapter 20) is useful for the particular case of units of measurement, such as kilometers versus miles.

The Fake Enum Checker (Chapter 9) builds in a set of assumptions. If those fit your use case, then it’s easiest to use the Fake Enum Checker (though you can achieve the same effect using the Subtyping Checker). The Fake Enum Checker forbids mixing of fenums of different types, or fenums and unannotated types. For instance, binary operations other than string concatenations are forbidden, such as NORTH+1, NORTH+MONDAY, and NORTH==MONDAY. However, NORTH+SOUTH is permitted.

By default, the Subtyping Checker does not forbid any operations.

If you choose to use the Subtyping Checker, then you have an additional design choice to make about the type system. In the general case, your type system will look something like Figure 30.1.

References whose type is @MyType are known to store only values from your new type. There is no such guarantee for @MyTypeUnknown and @NotMyType, but those types mean different things. An expression of type @NotMyType is guaranteed never to evaluate to a value of your new type. An expression of type @MyTypeUnknown may evaluate to any value — including values of your new type and values not of your new type. (@MyTypeBottom is the type of null and is also used for dead code and erroneous situations; it can be ignored for this discussion.)

A key choice for the type system designer is which type is the default. That is, if a programmer does not write @MyType on a given type use, should that type use be interpreted as @MyTypeUnknown or as @NotMyType?

• • If unannotated types are interpreted as @NotMyType, then the type system enforces very strong separation between your new type and all other types. Values of your type will never mix with values of other types. If you don’t see @MyType written explicitly on a type, you will know that it does not contain values of your type.

• • If unannotated types are interpreted as @MyTypeUnknown, then a generic, unannotated type may contain a value of your new type. In this case, @NotMyType does not need to exist, and @MyTypeBottom may or may not exist in your type system.

A downside of the stronger guarantee that comes from using @NotMyType as the default is the need to write additional annotations. For example, if @NotMyType is the default, this code does not type-check:

void method(Object o) { ... }
<U> void use(List<U> list) {
  method(list.get(0));
}

Because (implicit) upper bounds are interpreted as the top type (see Section 32.1.2), this is interpreted as

void method(@NotMyType Object o) { ... }
<U extends @MyTypeUnknown Object> void use(List<U> list) {
  // type error: list.get(0) has type @MyTypeUnknown, method expects @NotMyType
  method(list.get(0));
}

To make the code type-check, it is necessary to write an explicit annotation, either to restrict use’s argument or to expand method’s parameter type.