The Checker Framework Manual:
Custom pluggable types for Java

Chapter 9 Fake Enum Checker for fake enumerations

The Fake Enum Checker, or Fenum Checker, enables you to define a type alias or typedef, in which two different sets of values have the same representation (the same Java type) but are not allowed to be used interchangeably. It is also possible to create a typedef using the Subtyping Checker (Chapter 30), and that approach is sometimes more appropriate.

One common use for the Fake Enum Checker is the fake enumeration pattern (Section 9.6). For example, consider this code adapted from Android’s IntDef documentation: 

@NavigationMode int NAVIGATION_MODE_STANDARD = 0;
@NavigationMode int NAVIGATION_MODE_LIST = 1;
@NavigationMode int NAVIGATION_MODE_TABS = 2;

@NavigationMode int getNavigationMode();

void setNavigationMode(@NavigationMode int mode);

The Fake Enum Checker can issue a compile-time warning if the programmer ever tries to call setNavigationMode with an int that is not a @NavigationMode int.

The Fake Enum Checker gives the same safety guarantees as a true enumeration type or typedef, but retains backward-compatibility with interfaces that use existing Java types. You can apply fenum annotations to any Java type, including all primitive types and also reference types. Thus, you could use it (for example) to represent floating-point values between 0 and 1, or Strings with some particular characteristic. (Note that the Fake Enum Checker does not let you create a shorter alias for a long type name, as a real typedef would if Java supported it.)

As explained in Section 9.1, you can either define your own fenum annotations, such as @NavigationMode above, or you can use the @Fenum type qualifier with a string argument. Figure 9.1 shows part of the type hierarchy for the Fenum type system.

(image)

Figure 9.1: Partial type hierarchy for the Fenum type system. There are two forms of fake enumeration annotations — above, illustrated by @Fenum("A") and @FenumC. See Section 9.1 for descriptions of how to introduce both types of fenums. The type qualifiers in gray (@FenumTop, @FenumUnqualified, and @FenumBottom) should never be written in source code; they are used internally by the type system. @FenumUnqualified is the default qualifier for unannotated types, except for upper bounds which default to @FenumTop.

9.1 Fake enum annotations

The Fake Enum Checker supports two ways to introduce a new fake enum (fenum):

  • 1. Introduce your own specialized fenum annotation with code like this in file MyFenum.java: 

    package myPackage.qual;

import   java.lang.annotation.Documented;
import   java.lang.annotation.ElementType;
import   java.lang.annotation.Retention;
import   java.lang.annotation.RetentionPolicy;
import   java.lang.annotation.Target;
import   org.checkerframework.checker.fenum.qual.FenumTop;
import   org.checkerframework.framework.qual.SubtypeOf;

@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(FenumTop.class)
public @interface MyFenum {}

    You only need to adapt the italicized package, annotation, and file names in the example.

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

  • 2. Use the provided @Fenum annotation, which takes a String argument to distinguish different fenums or type aliases. For example, @Fenum("A") and @Fenum("B") are two distinct type qualifiers.

The first approach allows you to define a short, meaningful name suitable for your project, whereas the second approach allows quick prototyping.

9.2 What the Fenum Checker checks

The Fenum Checker ensures that unrelated types are not mixed. All types with a particular fenum annotation, or @Fenum(...) with a particular String argument, are disjoint from all unannotated types and from all types with a different fenum annotation or String argument.

The checker ensures that only compatible fenum types are used in comparisons and arithmetic operations (if applicable to the annotated type).

It is the programmer’s responsibility to ensure that fields with a fenum type are properly initialized before use. Otherwise, one might observe a null reference or zero value in the field of a fenum type. (The Nullness Checker (Chapter 3) can prevent failure to initialize a reference variable.)

9.3 Running the Fenum Checker

The Fenum Checker can be invoked by running the following commands.

  • • If you define your own annotation(s), provide the name(s) of the annotation(s) 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.checker.fenum.FenumChecker \
        -Aquals=myPackage.qual.MyFenum MyFile.java ...

    The annotations listed in -Aquals must be accessible to the compiler during compilation. Before you run the Fenum 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.

    You can also provide the fully-qualified paths to a set of directories that contain the annotations 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.checker.fenum.FenumChecker \
        -AqualDirs=/full/path/to/myProject/bin:/full/path/to/myLibrary/bin MyFile.java ...

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

      .../myProject/bin/myPackage/qual/MyFenum.class

    The two options can be used at the same time to provide groups of annotations from directories, and individually named annotations.

  • • If your code uses the @Fenum annotation, you do not need the -Aquals or -AqualDirs option: 

        javac -processor org.checkerframework.checker.fenum.FenumChecker MyFile.java ...

For an example of running the Fake Enum Checker on Android code, see https://github.com/karlicoss/checker-fenum-android-demo.

9.4 Suppressing warnings

One example of when you need to suppress warnings is when you initialize the fenum constants to literal values. To remove this warning message, add a @SuppressWarnings annotation to either the field or class declaration, for example: 

@SuppressWarnings("fenum:assignment") // initialization of fake enums
class MyConsts {
  public static final @Fenum("A") int ACONST1 = 1;
  public static final @Fenum("A") int ACONST2 = 2;
}

9.5 Example

The following example introduces two fenums in class TestStatic and then performs a few typical operations. 

@SuppressWarnings("fenum:assignment")   // initialization of fake enums
public class TestStatic {
  public static final @Fenum("A") int ACONST1 = 1;
  public static final @Fenum("A") int ACONST2 = 2;

    public static final @Fenum("B") int BCONST1 = 4;
    public static final @Fenum("B") int BCONST2 = 5;
}

class FenumUser {
  @Fenum("A") int state1 = TestStatic.ACONST1;         // ok
  @Fenum("B") int state2 = TestStatic.ACONST1;         // Incompatible fenums forbidden!

    void fenumArg(@Fenum("A") int p) {}

    void fenumTest() {
      state1 = 4;                       // Direct use of value forbidden!
      state1 = TestStatic.BCONST1;      // Incompatible fenums forbidden!
      state1 = TestStatic.ACONST2;      // ok

        fenumArg(5);                    // Direct use of value forbidden!
        fenumArg(TestStatic.BCONST1);   // Incompatible fenums forbidden!
        fenumArg(TestStatic.ACONST1);   // ok
    }
}

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

The paper “Building and using pluggable type-checkers” [DDE+11] (ICSE 2011, https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-icse2011.pdf) describes case studies of the Fake Enum Checker.

9.6 The fake enumeration pattern

Java’s enum keyword lets you define an enumeration type: a finite set of distinct values that are related to one another but are disjoint from all other types, including other enumerations. Before enums were added to Java, there were two ways to encode an enumeration, both of which are error-prone:

the fake enum pattern

a set of int or String constants (as often found in older C code).

the typesafe enum pattern

a class with a private constructor.

Sometimes you need to use the fake enum pattern, rather than a real enum or the typesafe enum pattern. One reason is backward-compatibility. A public API that predates Java’s enum keyword may use int constants; it cannot be changed, because doing so would break existing clients. For example, Java’s JDK still uses int constants in the AWT and Swing frameworks, and Android also uses int constants rather than Java enums. Another reason is performance, especially in environments with limited resources. Use of an int instead of an object can reduce code size, memory requirements, and run time.

In cases when code has to use the fake enum pattern, the Fake Enum Checker, or Fenum Checker, gives the same safety guarantees as a true enumeration type. The developer can introduce new types that are distinct from all values of the base type and from all other fake enums. Fenums can be introduced for primitive types as well as for reference types.

9.7 References