The Checker Framework Manual:
Custom pluggable types for Java

Chapter 33 Advanced type system features

This chapter describes features that are automatically supported by every checker written with the Checker Framework. You may wish to skim or skip this chapter on first reading. After you have used a checker for a little while and want to be able to express more sophisticated and useful types, or to understand more about how the Checker Framework works, you can return to it.

33.1 Invariant array types

Java’s type system is unsound with respect to arrays. That is, the Java type-checker approves code that is unsafe and will cause a run-time crash. Technically, the problem is that Java has “covariant array types”, such as treating String[] as a subtype of Object[]. Consider the following example: 

    String[] strings = new String[] {"hello"};
    Object[] objects = strings;
    objects[0] = new Object();
    String myString = strings[0];

The above code puts an Object in the array strings and thence in myString, even though myString = new Object() should be, and is, rejected by the Java type system. Java prevents corruption of the JVM by doing a costly run-time check at every array assignment; nonetheless, it is undesirable to learn about a type error only via a run-time crash rather than at compile time.

When you pass the -AinvariantArrays command-line option, the Checker Framework is stricter than Java, in the sense that it treats arrays invariantly rather than covariantly. This means that a type system built upon the Checker Framework is sound: you get a compile-time guarantee without the need for any run-time checks. But it also means that the Checker Framework rejects code that is similar to what Java unsoundly accepts. The guarantee and the compile-time checks are about your extended type system. The Checker Framework does not reject the example code above, which contains no type annotations.

Java’s covariant array typing is sound if the array is used in a read-only fashion: that is, if the array’s elements are accessed but the array is not modified. However, facts about read-only usage are not built into any of the type-checkers. Therefore, when using type systems along with -AinvariantArrays, you will need to suppress any warnings that are false positives because the array is treated in a read-only way.

33.2 Context-sensitive type inference for array constructors

When you write an expression, the Checker Framework gives it the most precise possible type, depending on the particular expression or value. For example, when using the Regex Checker (Chapter 14), the string "hello" is given type @Regex String because it is a legal regular expression (whether it is meant to be used as one or not) and the string "(foo" is given the type @PartialRegex String because it is not a legal regular expression.

Array constructors work differently. When you create an array with the array constructor syntax, such as the right-hand side of this assignment: 

String[] myStrings = {"hello"};

then the expression does not get the most precise possible type, because doing so could cause inconvenience. Rather, its type is determined by the context in which it is used: the left-hand side if it is in an assignment, the declared formal parameter type if it is in a method call, etc.

In particular, if the expression {"hello"} were given the type @Regex String[], then the assignment would be illegal! But the Checker Framework gives the type String[] based on the assignment context, so the code type-checks.

If you prefer a specific type for a constructed array, you can indicate that either in the context (change the declaration of myStrings) or in a new construct (change the expression to new @Regex String[] {"hello"}).

33.3 Upper bound of qualifiers on uses of a given type (annotations on a class declaration)

The examples in this section use the type qualifier hierarchy @A :> @B :> @C.

A qualifier on a use of a certain type must be a subtype or equal to the upper bound for that type. The upper bound of qualifiers used on a given type is specified by annotating the type declaration with some qualifier — that is, by writing an annotation on a class declaration. 

    @C class MyClass {}

This means that @B MyClass is an invalid type. (Annotations on class declarations may also specify default annotations for uses of the type; see Section 33.5.1.)

If it is not possible to annotate the class’s definition (e.g., for primitives and some library classes), the type-system designer can specify an upper bound by using the meta-annotation @UpperBoundFor.

If no annotation is present on a type declaration and if no @UpperBoundFor mentions the type, then the bound is top. This can be changed by overriding AnnotatedTypeFactory#getTypeDeclarationBounds.

There are two exceptions.

  • • An expression can have a supertype of the upper bound; that is, some expression could have type @B MyClass. This type is not written explicitly, but results from viewpoint adaptation.

  • • Using usual CLIMB-to-top rules (Section 33.5.3), local variables of type MyClass default to @A MyClass. It is legal for @A MyClass to be the type of a local variable. For consistency, users are allowed to write such a type on a local variable declaration.

Due to existing type rules, an expression of type @A MyClass can only be used in limited ways.

  • • Since every field, formal parameter, and return type of type MyClass (or lower) is annotated as @B (or lower), it cannot be assigned to a field, passed to a method, or returned from a method.

  • • It can be used in a context that requires @A Object (or whatever the least supertype is of MyClass for which the @A qualifier is permitted). Examples include being tested against null or (for most type systems) being passed to polymorphic routines such as System.out.println or System.identityHashCode.

These operations might refine its type. If a user wishes to annotate a method that does type refinement, its formal parameter must be of illegal type @A MyClass, which requires a warning suppression.

If the framework were to forbid expressions and local variables from having types inconsistent with the class annotation, then important APIs and common coding paradigms would no longer type-check.

Consider the annotation 

    @NonNull class Optional { ... }

and the client code 

    Map<String, Optional> m;
    String key = ...;
    Optional value = m.get(key);
    if (value != null) {
      ...
    }

The type of m.get(key) is @Nullable Optional, which is an illegal type. However, this is a very common paradigm. Programmers should not need to rewrite the code to test m.containsKey(key) nor suppress a warning in this safe code.

33.4 The effective qualifier on a type (defaults and inference)

A checker sometimes treats a type as having a slightly different qualifier than what is written on the type — especially if the programmer wrote no qualifier at all. Most readers can skip this section on first reading, because you will probably find the system simply “does what you mean”, without forcing you to write too many qualifiers in your program. In particular, programmers rarely write qualifiers in method bodies (except on type arguments and array component types).

The following steps determine the effective qualifier on a type — the qualifier that the checkers treat as being present.

  • 1. If a type qualifier is present in the source code, that qualifier is used.

  • 2. If there is no explicit qualifier on a type, then a default qualifier is applied; see Section 33.5. Defaulted qualifiers are treated by checkers exactly as if the programmer had written them explicitly.

  • 3. The type system may refine a qualified type on a local variable — that is, treat it as a subtype of how it was declared or defaulted. This refinement is always sound and has the effect of eliminating false positive error messages. See Section 33.7.

33.5 Default qualifier for unannotated types

An unannotated Java type is treated as if it had a default annotation. Both the type system designer and an end-user programmer can control the defaulting. Defaulting never applies to uses of type variables, even if they do not have an explicit type annotation. Most of this section is about defaults for source code that is read by the compiler. When the compiler reads a .class file, different defaulting rules apply. See Section 33.5.6 for these rules.

There are several defaulting mechanisms, for convenience and flexibility. When determining the default qualifier for a use of an unannotated type, MyClass, the following rules are used in order, until one applies.

  • 1. The qualifier specified via @DefaultQualifierForUse on the declaration of MyClass. (Section 33.5.1)

  • 2. If no @NoDefaultQualifierForUse is written on the declaration of MyClass, the qualifier explicitly written on the declaration of MyClass. (Section 33.5.1)

  • 3. The qualifier with a meta-annotation @DefaultFor(types = MyClass.class). (Section 33.5.1)

  • 4. The qualifier with a meta-annotation @DefaultFor(typeKinds = KIND), where KIND is the TypeKind of MyClass. (Section 33.5.1)

  • 5. The qualifier with a meta-annotation @DefaultFor(names = REGEX), where REGEX matches the name of the variable being defined (if any). For return types, the name of the method is used. (Section 33.5.1)

  • 6. The qualifier in the innermost user-written @DefaultQualifier for the location of the use of MyClass. (Section 33.5.2)

  • 7. The qualifier in the meta-annotation @DefaultFor for the location of the use of MyClass. These are defaults specified by the type system designer (Section 37.5.4); this is usually CLIMB-to-top (Section 33.5.3).

  • 8. The qualifier with the meta-annotation @DefaultQualifierInHierarchy.

If the unannotated type is the type of a local variable, then the first 5 rules are skipped and only rules 6 and 7 apply. If rule 7 applies, it makes the type of local variables top so they can be refined.

33.5.1 Default for use of a type

The type declaration annotation @DefaultQualifierForUse indicates that the specified qualifier should be added to all unannotated uses of the type.

For example: 

@DefaultQualifierForUse(B.class)
class MyClass {}

This means any unannotated use of MyClass is treated as @B MyClass by the checker. (Except for locals, which can be refined.)

Similarly, the meta-annotation @DefaultFor can be used to specify defaults for uses of types, using the types element, or type kinds, using the typeKinds element.

Interaction between qualifier bounds and DefaultQualifierForUse:

  • • If a type declaration is annotated with a qualifier bound, but not a @DefaultQualifierForUse, then the qualifier bound is added to all unannotated uses of that type (except locals). For example, @C class MyClass {} is equivalent to 

    @DefaultQualifierForUse(C.class)
@C class MyClass {}

  • • If the qualifier bound should not be added to all unannotated uses, then @NoDefaultQualifierForUse should be written on the declaration: 

    @NoDefaultQualifierForUse
@C class MyClass {}

    This means that unannotated uses of MyClass are defaulted normally.

  • • If neither @DefaultQualifierForUse nor a qualifier bound is present on a type declaration, that is equivalent to writing @NoDefaultQualifierForUse.

33.5.2 Controlling defaults in source code

The end-user programmer specifies a default qualifier by writing the @DefaultQualifier(ClassName, [locations]) annotation on a package, class, method, or variable declaration. The argument to @DefaultQualifier is the Class name of an annotation. The optional second argument indicates where the default applies. If the second argument is omitted, the specified annotation is the default in all locations. See the Javadoc of DefaultQualifier for details.

For example, using the Nullness type system (Chapter 3): 

import org.checkerframework.framework.qual.DefaultQualifier;
import org.checkerframework.checker.nullness.qual.NonNull;

@DefaultQualifier(NonNull.class)
class MyClass {

    public boolean compile(File myFile)   { // myFile has type "@NonNull File"
      if (!myFile.exists())          //   no warning: myFile is non-null
        ...
      @Nullable File srcPath = ...; //    must annotate to specify "@Nullable File"
      if (srcPath.exists())          //   warning: srcPath might be null
        ...
    }

    @DefaultQualifier(Tainted.class)
    public boolean isJavaFile(File myFile) {   // myFile has type "@Tainted File"
      ...
    }
}

You may write multiple @DefaultQualifier annotations at a single location.

If @DefaultQualifier[s] is placed on a package (via the package-info.java file), then it applies to the given package and all subpackages.

33.5.3 Defaulting rules and CLIMB-to-top

Each type system defines a default qualifier (see Section 37.5.4). For example, the default qualifier for the Nullness Checker is @NonNull. When a user writes an unqualified type such as Date, the Nullness Checker interprets it as @NonNull Date.

The type system applies that default qualifier to most but not all type uses. In particular, unless otherwise stated, every type system uses the CLIMB-to-top rule. This rule states that the top qualifier in the hierarchy is the default for the CLIMB locations: Casts, Locals, and (some) Implicit Bounds. For example, when the user writes an unqualified type such as Date in such a location, the Nullness Checker interprets it as @Nullable Date (because @Nullable is the top qualifier in the hierarchy, see Figure 3.1). (Casts are treated a bit specially; see below.)

The CLIMB-to-top rule is used only for unannotated source code that is being processed by a checker. For unannotated libraries (code read by the compiler in .class or .jar form), see Section 33.5.6.

The rest of this section explains the rationale and implementation of CLIMB-to-top.

Here is the rationale for CLIMB-to-top:

  • • Local variables are defaulted to top because type refinement (Section 33.7) is applied to local variables. If a local variable starts as the top type, then the Checker Framework refines it to the best (most specific) possible type based on assignments to it. As a result, a programmer rarely writes an explicit annotation on any of those locations.

    Variables defaulted to top include local variables, resource variables in the try-with-resources construct, variables in for statements, and catch arguments (known as exception parameters in the Java Language Specification).

    Exception parameters default to the top type because they might catch an exception thrown anywhere in the program.

    An alternate design for exception parameters would be to default exception parameters to some other type T (instead of the top type); then the Checker Framework would need to issue a warning at every throw statement whose argument might not be a subtype of T. A checker can implement this alternate design by overriding a few methods. The alternative is not appropriate for all type systems. The alternative is unsound for deep type systems because the JDK’s annotations are trusted rather than checked. A deep type system is one where the type of a field can determine the type of its containing instance, such as tainting. Example: a user passes a secret regex to the JDK, and the JDK throws a format exception that includes the regex. This could be caught by a catch clause in the program whose exception parameter is not annotated as secret. As another example, the user passes a secret integer and the JDK throws an ArithmeticException that reveals the value.

  • • Cast types are defaulted to the same type as their argument expression. This has the same effect as if they were given the top type and then flow-sensitively refined to the type of their argument. However, note that programmer-written type qualifiers are not refined, so writing the top annotation is not the same as writing no annotation.

  • • Implicit upper bounds are defaulted to top to allow them to be instantiated in any way.

    Suppose a user declares a class as class C<T> { ... }. The Checker Framework assumes that the user intended to allow any instantiation of the class. The Checker Framework interprets the declaration as class C<T extends @Nullable Object> { ... } rather than as class C<T extends @NonNull Object> { ... }. The latter would forbid instantiations such as C<@Nullable String>, or would require rewriting of code. On the other hand, if a user writes an explicit bound such as class C<T extends D> { ... }, then the user intends some restriction on instantiation and can write a qualifier on the upper bound as desired.

    This rule means that the upper bound of class C<T> is defaulted differently than the upper bound of class C<T extends Object>. This is a bit unfortunate, but it is the least bad option. The more confusing alternative would be for “Object” to be defaulted differently in class C<T extends Object> and in an instantiation C<Object>, and for the upper bounds to be defaulted differently in class C<T extends Object> and class C<T extends Date>.

  • • Implicit lower bounds are defaulted to the bottom type, again to allow maximal instantiation. Note that Java does not allow a programmer to express both the upper and lower bounds of a type, but the Checker Framework allows the programmer to specify either or both; see Section 32.1.2.

A @DefaultQualifier that specifies a CLIMB-to-top location takes precedence over the CLIMB-to-top rule.

Here is how the Nullness Checker overrides part of the CLIMB-to-top rule: 

@DefaultQualifierInHierarchy
@DefaultFor({ TypeUseLocation.EXCEPTION_PARAMETER })
public @interface NonNull {}

public @interface Nullable {}

As mentioned above, exception parameters are always non-null, so @DefaultFor({ TypeUseLocation.EXCEPTION_PARAMETER }) on @NonNull overrides the CLIMB-to-top rule.

33.5.4 Inherited defaults

When overriding a method, programmers must fully specify types in the overriding method, which duplicates information on the overridden method. By contrast, declaration annotations that are meta-annotated with @InheritedAnnotation are inherited by overriding methods.

An example for type annotations is that when defining an equals() method, programmers must write the type annotation @Nullable: 

    public boolean equals(@Nullable Object obj) {
        ...
    }

An alternate design would be for every annotation on a superclass member to be automatically inherited by subclasses that override it.

The alternate design would reduce annotation effort.

However, the alternate design would reduce program comprehensibility. Currently, a user can determine the annotation on a parameter or return value by looking at a single file. If annotations could be inherited from supertypes, then a user would have to examine all supertypes, and do computations over them, to understand the meaning of an unannotated type in a given file. For declaration annotations, no computation is necessary; that is why they may be inherited. Computation is necessary for type annotations because different annotations might be inherited from a supertype and an interface, or from two interfaces. For return types, the inherited type should be the least upper bound of all annotations on overridden implementations in supertypes. For method parameters, the inherited type should be the greatest lower bound of all annotations on overridden implementations in supertypes. In each case, the Checker Framework would need to issue an error if no such annotations existed.

Because a program is read more often than it is edited/annotated, the Checker Framework does not currently support the alternate design. In the future, this feature may be added.

33.5.5 Inherited wildcard annotations

If a wildcard is unbounded and has no annotation (e.g., List<?>), the annotations on the wildcard’s bounds are copied from the type parameter to which the wildcard is an argument.

For example, the two wildcards in the declarations below are equivalent. 

class MyList<@Nullable T extends @Nullable Object> {}

MyList<?> listOfNullables;
MyList<@Nullable ? extends @Nullable Object> listOfNullables;

The Checker Framework copies these annotations because wildcards must be within the bounds of their corresponding type parameter. By contrast, if the bounds of a wildcard were defaulted differently from the bounds of its corresponding type parameter, then there would be many false positive type.argument warnings.

Here is another example of two equivalent wildcard declarations: 

class MyList<@Regex(5) T extends @Regex(1) Object> {}

MyList<?> listOfRegexes;
MyList<@Regex(5) ? extends @Regex(1) Object> listOfRegexes;

Note that this copying of annotations for a wildcard’s bounds applies only to unbounded wildcards. The two wildcards in the following example are equivalent. 

class MyList<@NonNull T extends @Nullable Object> {}

MyList<? extends Object> listOfNonNulls;
MyList<@NonNull ? extends @NonNull Object> listOfNonNulls2;

Note that the upper bound of the wildcard ? extends Object is defaulted to @NonNull using the CLIMB-to-top rule (see Section 33.5.3). Also note that the MyList class declaration could have been more succinctly written as: class MyList<T extends @Nullable Object> where the lower bound is implicitly the bottom annotation: @NonNull.

33.5.6 Default qualifiers for .class files (library defaults)

The defaulting rules presented so far apply to source code that is read by the compiler. When the compiler reads a .class file, different defaulting rules apply. The rules are the same regardless of whether the .class file is from your own codebase or from a library, including the JDK.

If the .class file was compiled using the checker (that is, if the checker was run during the compiler execution that created the .class file), then there is no need for defaults: the .class file has an explicit qualifier at each type use. (Furthermore, unless warnings were suppressed, those qualifiers are guaranteed to be correct.)

The rest of this section discusses the situation when the .class file was not compiled using the checker (that is, the checker was not run during the compiler execution that created the .class file). The .class file contains only the type qualifiers that the programmer wrote explicitly — possibly none. (Furthermore, there is no guarantee that these qualifiers are correct, since they have not been checked.) Each checker decides what qualifier to use where the programmer did not write an annotation.

  • • With -AuseConservativeDefaultsForUncheckedCode=-bytecode: (This is also the behavior if -AuseConservativeDefaultsForUncheckedCode is not supplied or is supplied without “bytecode” in its argument.)

    The source code defaulting rules are used.

    For example, an unannotated method 

        String concatenate(String p1, String p2)

    in a classfile would be interpreted as 

        @Default String concatenate(@Default String p1, @Default String p2)

    for an appropriate value of @Default. (The default might be different for return types and parameter types, depending on how the checker is written.)

    These defaulting rules are unsafe: the default might be different than what the library author intended, so the Checker Framework may not warn about some misuses of the library. (This includes both misuse by passing in a bad value and misuse by using a returned value incorrectly.) However, this unsafe default can be useful because it permits you to focus on errors within the codebase before you have annotated the libraries it uses.

  • • With -AuseConservativeDefaultsForUncheckedCode=bytecode:

    • – For method parameters and lower bounds, use the bottom qualifier (see Section 37.5.7).

    • – For method return values, fields, and upper bounds, use the top qualifier (see Section 37.5.7).

    For example, an unannotated method 

        String concatenate(String p1, String p2)

    in a classfile would be interpreted as 

        @MyTopQualifier String concatenate(@MyBottomQualifier String p1, @MyBottomQualifier String p2)

    where @MyTopQualifier is the top qualifier in the hierarchy and @MyBottomQualifier is the bottom qualifier in the hierarchy.

    These choices are conservative. They are likely to cause many false-positive type-checking errors, which will help you to know which library methods need annotations. You can then write those library annotations (see Chapter 36) or alternately suppress the warnings (see Chapter 34).

    There is one case in which these choices are not conservative. Fields default to the top qualifier, so any assignment into a field is permitted. If an unannotated library has a mutable public field (which would be poor code style), the Checker Framework won’t warn about incorrect assignments to the field.

33.6 Annotations on constructors

33.6.1 Annotations on constructor declarations

An annotation on the “return type” of a constructor declaration indicates what the constructor creates. For example, 

@B class MyClass {
  @C MyClass() {}
}

means that invoking that constructor creates a @C MyClass.

The Checker Framework cannot verify that the constructor really creates such an object, because the Checker Framework does not know the type-system-specific semantics of the @C annotation. Therefore, if the constructor result type is different than the top annotation in the hierarchy, the Checker Framework will issue a warning. The programmer should check the annotation manually, then suppress the warning.

Defaults

If a constructor declaration is unannotated, it defaults to the same type as that of its enclosing class (rather than the default qualifier in the hierarchy). For example, the Tainting Checker (Chapter 12) has @Tainted as its default qualifier. Consider the following class: 

    @Untainted class MyClass {
      MyClass() {}
    }

The constructor declaration is equivalent to @Untainted MyClass() {}.

The Checker Framework produces the same error messages for explicitly-written and defaulted annotations.

33.6.2 Annotations on constructor invocations

The type of a method call expression x.myMethod(y, z) is determined by the return type of the declaration of myMethod. There is no way to write an annotation on the call to change its type. However, it is possible to write a cast: (@Anno SomeType) x.myMethod(y, z). The Checker Framework will issue a warning that it cannot verify that the downcast is correct. The programmer should manually determine that the annotation is correct and then suppress the warning.

A constructor invocation new MyClass() is also a call, so its semantics are similar. The type of the expression is determined by the annotation on the result type of the constructor declaration. It is possible to write a cast (@Anno MyClass) new MyClass(). The syntax new @Anno MyClass() is shorthand for the cast. For either syntax, the Checker Framework will issue a warning that it cannot verify that the cast is correct. The programmer may suppress the warning if the code is correct.

33.7 Type refinement (flow-sensitive type qualifier inference)

A checker can sometimes deduce that an expression’s type is more specific than — that is, a subtype of — its declared or defaulted type (Section 33.5). This is called “flow-sensitive type refinement” or “local type inference”.

Due to local type refinement, a programmer typically does not write any qualifiers on local variables within a method body (except on type arguments and array component types). However, the programmer must write type annotations for method signatures (arguments and return values) and fields, unless the default annotations are correct. Local type refinement does not change the source code to insert the inferred annotations on local variables.

33.7.1 Type refinement examples

Here is an example for the Nullness Checker (Chapter 3). myVar is declared as @Nullable String, but it is treated as @NonNull String within the body of the if test. 

    @Nullable String myVar;
    ...                   //   myVar has type @Nullable String here.
    myVar.hashCode();     //   warning: possible dereference of null.
    ...
    if (myVar != null) {
      ...                 //   myVar has type @NonNull String here.
      myVar.hashCode();   //   no warning.
    }

Here is another example. Note that the same expression may yield a warning or not depending on its context (that is, depending on the current type refinement). 

    @Nullable String myVar;
    ...                   // myVar has type @Nullable String
    myVar = "hello";
    ...                   // myVar has type @NonNull String
    myVar.hashCode();     // no warning
    ...
    myVar = myMap.get(someKey);
    ...                   // myVar has type @Nullable String
    myVar.hashCode();     // warning: possible dereference of null

Type refinement applies to every checker, including new checkers that you write. Here is an example for the Regex Checker (Chapter 14): 

    void m2(String s) {
      s = RegexUtil.asRegex(s, 2);    // asRegex throws an exception if its argument is not
                                      // a regex with the given number of capturing groups
        ...   // s now has type "@Regex(2) String"
    }
33.7.2 Type refinement behavior

The checker treats a variable or expression as a subtype of its declared type:

  • • starting at the time that it is assigned a value, a method establishes a postcondition (e.g., as expressed by @EnsuresNonNull or @EnsuresQualifierIf), or a run-time check is performed (e.g., via an assertion or if statement).

  • • until its value might change (e.g., via an assignment, or because a method call might have a side effect).

The checker never treats a variable as a supertype of its declared type. For example, an expression with declared type @NonNull is never treated as possibly-null, and such an assignment is always illegal.

The functionality has a variety of names: type refinement, flow-sensitive type qualifier inference, local type inference, and sometimes just “flow”.

33.7.3 Which types are refined

You generally do not need to annotate the top-level type of a local variable. You do need to annotate its type arguments or array element types. (Type refinement does not change them, because doing so would not produce a subtype, as explained in Section 32.1.6 and Section 33.1.) Type refinement works within a method, so you still need to annotate method signatures (parameter and return type) and field types.

If you find examples where you think a value should be inferred to have (or not have) a given annotation, but the checker does not do so, please submit a bug report (see Section 41.2) that includes a small piece of Java code that reproduces the problem.

Fields and type refinement

Type refinement infers the type of fields in some restricted cases:

  • • A final initialized field: Type inference is performed for final fields that are initialized to a compile-time constant at the declaration site; so the type of protocol is @NonNull String in the following declaration: 

          public final String protocol = "https";

    Such an inferred type may leak to the public interface of the class. If you wish to override such behavior, you can explicitly insert the desired annotation, e.g., 

          public final @Nullable String protocol = "https";

  • • Within method bodies: Type inference is performed for fields in the context of method bodies, like local variables or any other expression. Consider the following example, where updatedAt is a nullable field: 

    class DBObject {
  @Nullable Date updatedAt;

    void m() {
      // updatedAt is @Nullable, so warning about .getTime()
      ... updatedAt.getTime() ... // warning about possible NullPointerException

        if (updatedAt == null) {
          updatedAt = new Date();
        }

        // updatedAt is now @NonNull, so .getTime() call is OK
        ... updatedAt.getTime() ...
    }
}

    A method call may invalidate inferences about field types; see Section 33.7.5.

33.7.4 Run-time tests and type refinement

Some type systems support a run-time test that the Checker Framework can use to refine types within the scope of a conditional such as if, after an assert statement, etc.

Whether a type system supports such a run-time test depends on whether the type system is computing properties of data itself, or properties of provenance (the source of the data). An example of a property about data is whether a string is a regular expression. An example of a property about provenance is units of measure: there is no way to look at the representation of a number and determine whether it is intended to represent kilometers or miles.

Type systems that support a run-time test are:

Type systems that do not currently support a run-time test, but could do so with some additional implementation work, are:

Type systems that cannot support a run-time test are:

33.7.5 Side effects, determinism, purity, and type refinement

Calling a method typically causes the checker to discard its knowledge of the refined type, because the method might assign a field. The @SideEffectFree annotation indicates that the method has no side effects, so calling it does not invalidate any dataflow facts.

Calling a method twice might have different results, so facts known about one call cannot be relied upon at another call. The @Deterministic annotation indicates that the method returns the same result every time it is called on the same arguments.

@Pure means both @SideEffectFree and @Deterministic. The @TerminatesExecution annotation indicates that a given method never returns. This can enable type refinement to be more precise.

Chapter 23 gives more information about these annotations. This section explains how to use them to improve type refinement.

Side effects

Consider the following declarations and uses: 

    @Nullable Object myField;

    int computeValue() { ... }

    void m() {
      ...
      if (myField != null) {
                          // The type of myField is now "@NonNull Object".
        int result = computeValue();
                          // The type of myField is now "@Nullable Object",
                          // because computeValue might have set myField to null.
        myField.toString(); // Warning: possible null pointer exception.
      }
    }

There are three ways to express that computeValue does not set myField to null, and thus to prevent the Nullness Checker from issuing a warning about the call myField.toString().

  • 1. If computeValue has no side effects, declare the method as @SideEffectFree: 

        @SideEffectFree
    int computeValue() { ... }

    The Nullness Checker issues no warnings, because it can reason that the second occurrence of myField has the same (non-null) value as the one in the test.

  • 2. If no method resets myField to null after it has been initialized to a non-null value (even if a method has some other side effect), declare the field as @MonotonicNonNull: 

        @MonotonicNonNull Object myField;

  • 3. If computeValue sets myField to a non-null value (or maintains it as a non-null value), declare the method as @EnsuresNonNull: 

        @EnsuresNonNull("myField")
    int computeValue() { ... }

    If computeValue maintains myField as a non-null value, even if it might have other side effects and even if other methods might set myField to null, declare it as 

        @RequiresNonNull("myField")
    @EnsuresNonNull("myField")
    int computeValue() { ... }

There are two other ways to suppress the warning:

  • • Put the expression in a local variable before the invocation. A method call never affects the value of a local variable.

  • • If the warning is about a formal parameter (including the receiver) to a method foo(), then instead of declaring foo() as @SideEffectFree, you can supply the -AinvocationPreservesArgumentNullness command-line argument; see Section 3.1.1.

Deterministic methods

Consider the following declaration and uses: 

    @Nullable Object getField(Object arg) { ... }

    void m() {
      ...
      if (x.getField(y) != null) {
        x.getField(y).toString(); // warning: possible null pointer exception
      }
    }

The Nullness Checker issues a warning regarding the toString() call, because its receiver x.getField(y) might be null, according to the @Nullable return type in the declaration of getField. The Nullness Checker cannot assume that getField returns non-null on the second call, just based on the fact that it returned non-null on the first call.

To indicate that a method returns the same value each time it is called on the same arguments, use the @Deterministic annotation. Actually, it is necessary to use @Pure, which means both @Deterministic and @SideEffectFree, because otherwise the first call might change a value that the method depends on.

If you change the declaration of getField to 

    @Pure
    @Nullable Object getField(Object arg) { ... }

then the Nullness Checker issues no warnings. Because getField is @SideEffectFree, the values of x and y are the same at both invocations. Because getField is @Deterministic, the two invocations of x.getField(y) have the same value. Therefore, x.getField(y) is non-null within the then branch of the if statement.

33.7.6 Assertions

If your code contains an assert statement, then your code could behave in two different ways at run time, depending on whether assertions are enabled or disabled via the -ea, -enableassertions, -da, or -disableassertions command-line options to java.

By default, the Checker Framework outputs warnings about any error that could happen at run time, whether assertions are enabled or disabled.

If you supply the -AassumeAssertionsAreEnabled command-line option, then the Checker Framework assumes assertions (that is, Java assert statements) are enabled, as if Java is run with the -ea or -enableassertions command-line argument. If you supply the -AassumeAssertionsAreDisabled command-line option, then the Checker Framework assumes assertions are disabled, as if Java is run with the -da or -disableassertions command-line argument. You may not supply both command-line options. It is uncommon to supply either one.

These command-line arguments have no effect on processing of assert statements whose message contains the text @AssumeAssertion; see Section 34.2.

33.7.7 The var keyword

The initial type of a variable declared with var is exactly the type of the initializer expression at the declaration. 

    var list1 = new ArrayList<@Tainted String>(); // type of list1 is ArrayList<@Tainted String>
    var list2 = new ArrayList<@Untainted String>(); // type of list2 is ArrayList<@Untainted String>

Flow-sensitive type refinement applies to these variables as usual. The base type qualifier may change at a later program point due to a subsequent assignment, but the qualifiers on type parameters and array contents remain exactly the same. 

    var list1 = new ArrayList<@Tainted String>(); // type of list1 is ArrayList<@Tainted String>
    var list2 = new ArrayList<@Untainted String>(); // type of list2 is ArrayList<@Untainted String>
    var list3 = list1; // type of list3 is ArrayList<@Tainted String>
    list2 = list1; // assignment error

33.8 Writing Java expressions as annotation arguments

Sometimes, it is necessary to write a Java expression as the argument to an annotation. The annotations that take a Java expression as an argument include:

The set of permitted expressions is a subset of all Java expressions, with a few extensions. The extensions are formal parameters like “#1” and (for some type systems) “<self>”.

  • • this, the receiver object. You can write this to annotate any variable or declaration where you could write this in code. Notably, it cannot be used in annotations on declarations of static fields or static methods. For a field, this is the field’s receiver (sometimes called its container). For a local variable, it is the method’s receiver.

  • • super, the receiver object as seen from the superclass. This can be used to refer to fields shadowed in the subclass (although shadowing fields is discouraged in Java).

  • • <self>, the value of the annotated reference (non-primitive) variable. Currently only defined for the @GuardedBy type system. For example, @GuardedBy("<self>") Object o indicates that the value referenced by o is guarded by the intrinsic (monitor) lock of the value referenced by o.

  • • a formal parameter, e.g., #2. It is represented as # followed by the one-based parameter index. For example: #1, #3. It is not permitted to write #0 to refer to the receiver object; use “this” instead.

    The formal parameter syntax #1 is less natural in source code than writing the formal parameter name. This syntax is necessary for separate compilation, because no formal parameter name information is available in a .class file. Suppose an annotated method m has already been compiled into a .class file, perhaps by a compilation that did not use the Checker Framework. When a client of m is later compiled, it cannot interpret a formal parameter name, but it can interpret a number.

    Within a method body, you may use the formal parameter name. The formal parameter name never works within a method signature or for a contract (pre- or post-condition) annotation; in those locations, an identifier is interpreted as a field name (not a formal parameter).

  • • a local variable, e.g., myLocalVar. The variable must be in scope; for example, a method annotation on method m cannot mention a local variable that is declared inside m.

  • • a static variable, e.g., System.out. Write the class name and the variable.

  • • a field of any expression. For example: next, this.next, #1.next. You may optionally omit a leading “this.”, just as in Java. Thus, this.next and next are equivalent.

  • • an array access. For example: this.myArray[i], vals[#1].

  • • an array creation. For example: new int[10], new String[] {"a", "b"}.

  • • literals: string, integer, char, long, float, double, null, class literals.

  • • a method invocation on any expression. This even works for overloaded methods and methods with type parameters. For example: m1(x, y.z, #2), a.m2("hello").

    Currently, the Checker Framework cannot prove all contracts about method calls, so you may need to suppress some warnings.

    One unusual feature of the Checker Framework’s Java expressions is that a method call is allowed to have side effects. Other tools forbid methods with side effects (and doing so is necessary if a specification is going to be checked at run time via assertions). The Checker Framework enables you to state more facts. For example, consider the annotation on java.io.BufferedReader.ready(): 

        @EnsuresNonNullIf(expression="readLine()", result=true)
    @Pure public boolean ready() throws IOException { ... }

    This states that if readLine() is called immediately after ready() returns true, then readLine() returns a non-null value.

  • • a binary expression, e.g., x + y or #1 - 1. These are used by the Index Checker, for example.

  • • a class name expression within another expression, e.g., “String” in String.class or “pkg.MyClass” in pkg.MyClass.staticField. The class name must be fully-qualified unless it can be referenced by its simple name without an import statement at the location where the annotation appears. For example, an annotation in class C can use the simple name of a class in java.lang or in the same package as C.

33.8.1 Limitations

If you mention a class in a Java expression, then that class must be available to the compiler. For example, if you write @EnsuresNonNull("package1.package2.MyClass.myField.myOtherField"), then you should pass MyClass.java to the compiler. Otherwise, the compiler does not know which components of the dotted name are packages, classes, and field names. In that case, you might get confusing error messages such as “Invalid ’package1.package2’ because could not find class package1 in package package2”.

It is not possible to write a quantification over all array components (e.g., to express that all array elements are non-null). There is no such Java expression, but it would be useful when writing specifications.

33.9 Field invariants

Sometimes a field declared in a superclass has a more precise type in a subclass. To express this fact, write @FieldInvariant on the subclass. It specifies the field’s type in the class on which this annotation is written. The field must be declared in a superclass and must be final.

For example, 

class Person {
  final @Nullable String nickname;
  public Person(@Nullable String nickname) {
    this.nickname = nickname;
  }
}

// A rapper always has a nickname.
@FieldInvariant(qualifier = NonNull.class, field = "nickname")
class Rapper extends Person {
  public Rapper(String nickname) {
    super(nickname);
  }
  void method() {
    ... nickname.length() ...   // legal, nickname is non-null in this class.
  }
}

A field invariant annotation can refer to more than one field. For example, @FieldInvariant(qualifier = NonNull.class, field = {"fieldA", "fieldB"}) means that fieldA and fieldB are both non-null in the class upon which the annotation is written. A field invariant annotation can also apply different qualifiers to different fields. For example, @FieldInvariant(qualifier = {NonNull.class, Untainted.class}, field = {"fieldA", "fieldB"}) means that fieldA is non-null and fieldB is untainted.

This annotation is inherited: if a superclass is annotated with @FieldInvariant, its subclasses have the same annotation. If a subclass has its own @FieldInvariant, then it must include the fields in the superclass annotation, and those fields’ annotations must be subtypes of (or equal to) the annotations for those fields in the superclass @FieldInvariant.

Currently, the @FieldInvariant annotation is trusted rather than checked. In other words, the @FieldInvariant annotation introduces a loophole in the type system, which requires verification by other means such as manual examination.

33.10 Unused fields

In an inheritance hierarchy, subclasses often introduce new methods and fields. For example, a Marsupial (and its subclasses such as Kangaroo) might have a field pouchSize indicating the size of the animal’s pouch. The field does not exist in superclasses such as Mammal and Animal, so Java issues a compile-time error if a program tries to access myMammal.pouchSize.

If you cannot use subtypes in your program, you can enforce similar requirements using type qualifiers. For fields, use the @Unused annotation (Section 33.10.1), which enforces that a field or method may only be accessed from a receiver expression with a given annotation (or one of its subtypes). For methods, annotate the receiver parameter this; then a method call type-checks only if the actual receiver is of the specified type.

Also see the discussion of typestate checkers in Section 31.30.

33.10.1 @Unused annotation

A Java subtype can have more fields than its supertype. For example: 

class   Animal {}
class   Mammal extends Animal { ... }
class   Marsupial extends Mammal {
  int   pouchSize; // pouch capacity, in cubic centimeters
  ...
}

You can simulate the same effect for type qualifiers: the @Unused annotation on a field declares that the field may not be accessed via a receiver of the given qualified type (or any supertype). For example: 

class Animal {
  @Unused(when=Mammal.class)
  int pouchSize; // pouch capacity, in cubic centimeters
  ...
}
@interface Mammal {}
@interface Marsupial {}

@Marsupial Animal joey = ...;
... joey.pouchSize ...     // OK
@Mammal Animal mae = ...;
... mae.pouchSize ...     // compile-time error

The above class declaration is like writing 

class @Mammal-Animal { ... }
class @Marsupial-Animal {
  int pouchSize; // pouch capacity, in cubic centimeters
  ...
}