This chapter describes how to create a checker — a type-checking compiler plugin that detects bugs or verifies their absence. After a programmer annotates a program, the checker verifies that the code is consistent with the annotations. If you only want to use a checker, you do not need to read this chapter. People who wish to edit the Checker Framework source code or make pull requests should read the Checker Framework Developer Manual.
Writing a simple checker is easy! For example, here is a complete, useful type-checker:
import java.lang.annotation.Documented;
import java.lang.annotation.Target;
import java.lang.annotation.ElementType;
import org.checkerframework.common.subtyping.qual.Unqualified;
import org.checkerframework.framework.qual.SubtypeOf;
@Documented
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(Unqualified.class)
public @interface Encrypted {}
This checker is so short because it builds on the Subtyping Checker (Chapter 30). See Section 30.2 for more details about this particular checker. When you wish to create a new checker, it is often easiest to begin by building it declaratively on top of the Subtyping Checker, and then return to this chapter when you need more expressiveness or power than the Subtyping Checker affords.
Three choices for creating your own checker are:
• Customize an existing checker. Checkers that are designed for extension include the Subtyping Checker (Chapter 30), the Accumulation Checker (Chapter 38), the Fake Enumeration Checker (Chapter 9), and the Units Checker (Chapter 20).
• Follow the instructions in this chapter to create a checker from scratch. This enables creation of checkers that are more powerful than customizing an existing checker.
• Copy and then modify a different existing checker — whether one distributed with the Checker Framework or a third-party one. A problem with this strategy is that you can get tangled up if you don’t fully understand the subtleties of the existing checker that you are modifying. Usually, it is easier to follow the instructions in this chapter. (If you are going to copy a checker despite the dangers, one good choice to copy and modify is the Regex Checker (Chapter 14). A bad choice is the Nullness Checker (Chapter 3), which is more sophisticated than anything you want to start out building.)
You do not need all of the details in this chapter, at least at first. In addition to reading this chapter of the manual, you may find it helpful to examine the implementations of the checkers that are distributed with the Checker Framework. The Javadoc documentation of the framework and the checkers is in the distribution and is also available online at https://checkerframework.org/api/.
If you write a new checker and wish to advertise it to the world, let us know so we can mention it in Chapter 31 or even include it in the Checker Framework distribution.
This table shows the relationship among tools that the Checker Framework builds on or that are built on the Checker Framework. You use the Checker Framework to build pluggable type systems, and the Annotation File Utilities to manipulate .java and .class files.
|
Subtyping Checker |
Nullness Checker |
Index Checker |
Tainting Checker |
… |
Your Checker |
||
|
Base Checker (enforces subtyping rules) |
Type inference |
Other tools |
|||||
|
Checker Framework (enables creation of pluggable type-checkers) |
( |
||||||
|
Java type annotations syntax and classfile format (no built-in semantics) |
|||||||
The Base Checker (more precisely, the BaseTypeChecker) enforces the standard subtyping rules. The Subtyping Checker is a simple use of the Base Checker that supports
providing type qualifiers on the command line. You usually want to build your checker on the Base Checker.
The Checker Framework provides abstract base classes (default implementations), and a specific checker overrides as little or as much of the default implementations as necessary. To simplify checker implementations, by default the Checker Framework automatically discovers the parts of a checker by looking for specific files. Thus, checker implementations follow a very formulaic structure. To illustrate, a checker for MyProp must be laid out as follows:
myPackage/ | qual/ type qualifiers | MyPropChecker.java interface to the compiler | MyPropVisitor.java [optional] type rules | MyPropAnnotatedTypeFactory.java [optional] type introduction and dataflow rules
MyPropChecker.java is occasionally optional, such as if you are building on the Subtyping Checker. If you want to create an artifact containing just the qualifiers (similar to the Checker Framework’s checker-qual artifact), you should put the qual/ directory in a separate
Maven module or Gradle subproject.
Sections 37.5–37.9 describe the individual components of a type system as written using the Checker Framework:
37.5 Type qualifiers and hierarchy. You define the annotations for the type system and the subtyping relationships among qualified types (for instance, @NonNull Object is a subtype of @Nullable
Object). This is also where you specify the default annotation that applies whenever the programmer wrote no annotation and no other defaulting rule applies.
37.6 Interface to the compiler. The compiler interface indicates which annotations are part of the type system, which command-line options and @SuppressWarnings annotations the checker
recognizes, etc.
37.7 Type rules. You specify the type system semantics (type rules), violation of which yields a type error. A type system has two types of rules.
• Subtyping rules related to the type hierarchy, such as that in every assignment, the type of the right-hand side is a subtype of the type of the left-hand side. Your checker automatically inherits these subtyping rules from the Base Checker (Chapter 30), so there is nothing for you to do.
• Additional rules that are specific to your particular checker. For example, in the Nullness type system, only references whose type is @NonNull may be dereferenced. You write these
additional rules yourself.
37.8 Type introduction rules. You specify the type of some expressions where the rules differ from the built-in framework rules.
37.9 Dataflow rules. These optional rules enhance flow-sensitive type qualifier inference (also sometimes called “local variable type inference”).
You can place your checker’s source files wherever you like. One choice is to write your checker in a fork of the Checker Framework repository https://github.com/typetools/checker-framework. Another choice is to write it in a stand-alone repository. Here is a template for a stand-alone repository: https://github.com/typetools/templatefora-checker; at that URL, click the “Use this template” button.
Once your custom checker is written, using it is very similar to using a built-in checker (Section 2.2): simply pass the fully-qualified name of your BaseTypeChecker subclass to the -processor command-line option:
javac -processor mypackage.MyPropChecker SourceFile.java
Note that your custom checker’s .class files must be on the same path (the classpath or processorpath) as the Checker Framework. Invoking a custom checker that builds on the Subtyping Checker is slightly different (Section 30.1).
To make your job easier, we recommend that you build your type-checker incrementally, testing at each phase rather than trying to build the whole thing at once.
Here is a good way to proceed.
1. Write the user manual. Do this before you start coding. The manual explains the type system, what it guarantees, how to use it, etc., from the point of view of a user. Writing the manual will help you flesh out your goals and the concepts, which are easier to
understand and change in text than in an implementation. Section 37.13 gives a suggested structure for the manual chapter, which will help you avoid omitting any parts. If your checker is in a clone of the
Checker Framework, don’t forget to add a LaTeX \include directive to manual.tex. Get feedback from
someone else at this point to ensure that your manual is comprehensible.
Once you have designed and documented the parts of your type system, you should “play computer”, manually type-checking some code according to the rules you defined. During manual checking, ask yourself what reasoning you applied, what information you needed, and whether your written-down rules were sufficient. It is more efficient to find problems now rather than after coding up your design.
2. Implement the type qualifiers and hierarchy (Section 37.5). Compile your changes.
Write simple test cases that consist of only assignments, to test your type hierarchy. For instance, if your type hierarchy consists of a supertype @UnknownSign and a subtype @NonNegative, then you could write a test case such as:
import org.checkerframework.checker.mycheckername.qual.UnknownSign;
import org.checkerframework.checker.mycheckername.qual.NonNegative;
class TestHierarchy {
void testHierarchy(@UnknownSign int us, @NonNegative int nn) {
@UnknownSign int a = us;
@UnknownSign int b = nn;
// :: error: [assignment]
@NonNegative int c = us; // expected error on this line
@NonNegative int d = nn;
}
}
If you are working in a clone of the Checker Framework, put the above test case in file checker/tests/mycheckername/TestHierarchy.java.
Type-check your test files using the Subtyping Checker (Chapter 30), using a command like
javacheck \ -processor org.checkerframework.common.subtyping.SubtypingChecker \ -Aquals=org.checkerframework.checker.mycheckername.qual.MyTopQual,org.checkerframework.checker.mycheckername.qual.MyBottomQual \ TestHierarchy.java
3. Write the checker class itself (Section 37.6).
Ensure that you can still type-check your test files and that the results are the same. You will not use the Subtyping Checker any more; you will call the checker directly, as in
javac -processor mypackage.MyChecker File1.java File2.java ...
If the default qualifier is not the top qualifier, you may see warning: (inconsistent.constructor.type). If the checker should never issue such an error (because a newly-constructed object can be correctly viewed as any type at all), then copy TaintingVisitor.java into your
checker, changing “Tainting”.
4. Create test infrastructure. If your checker source code is in a clone of the Checker Framework repository, integrate your checker with the Checker Framework’s Gradle targets for testing (Section 37.11). This will make it much more convenient to run tests, and to ensure that they are passing, as your work proceeds.
If there are errors in the “all-systems” tests, don’t worry about them until after you have annotated the JDK. However, specifying @RelevantJavaTypes (Section 37.5.5) may eliminate some of
those errors, especially if the default qualifier is not the top qualifier.
5. Annotate parts of the JDK, if relevant (Section 37.10). You will clone the Checker Framework JDK, naming it
jdk in a sibling directory of checker-framework (that is, they have the same parent). Most changes will consist of adding an import statement, plus uses of qualifiers, in Java files under src/java.base/share/classes/. Also follow the instructions in
section “Qualifier definitions” of file README.md.
Write test cases for a few of the annotated JDK methods to ensure that the annotations are being properly read by your checker.
If there are errors in the Checker Framework’s “all-systems” tests, you can suppress them if they are expected. See framework/tests/all-systems/README for more information.
6. Implement type rules, if any (Section 37.7). Some type systems need JDK annotations but don’t have any additional type rules.
Before implementing type rules (or any other code in your type-checker), read the Javadoc to familiarize yourself with the utility routines in the org.checkerframework.javacutil package, especially AnnotationBuilder, AnnotationUtils, ElementUtils, TreeUtils, TypeAnnotationUtils, and TypesUtils. You will learn how to access needed information and avoid reimplementing existing functionality.
Write simple test cases to test the type rules, and ensure that the type-checker behaves as expected on those test files. For example, if your type system forbids indexing an array by a possibly-negative value, then you would write a test case such as:
void testArrayIndexing(String[] myArray, @UnknownSign int us, @NonNegative int nn) {
myArray[us]; // expected error on this line
myArray[nn];
}
7. Implement type introduction rules, if any (Section 37.8). Some type systems need JDK annotations but don’t have any type introduction rules.
Test your type introduction rules. For example, if your type system sets the qualifier for manifest literal integers and for array lengths, you would write a test case like the following:
void testTypeIntroduction(String[] myArray) {
@NonNegative int nn1 = -1; // expected error on this line
@NonNegative int nn2 = 0;
@NonNegative int nn3 = 1;
@NonNegative int nn4 = myArray.length;
}
8. Optionally, implement dataflow refinement rules (Section 37.9). Dataflow refinement rules are only possible for a type system that supports a run-time test (Section 33.7.4).
Test them if you wrote any. For instance, if after an arithmetic comparison, your type system infers which expressions are now known to be non-negative, you could write a test case such as:
void testDataflow(@UnknownSign int us, @NonNegative int nn) {
@NonNegative int nn2;
nn2 = us; // expected error on this line
if (us > 0) {
nn2 = us;
}
if (us >= 0) {
nn2 = us;
}
if (0 < us) {
nn2 = us;
}
if (0 <= us) {
nn2 = us;
}
nn = us; // expected error on this line
}
A type system designer specifies the qualifiers in the type system (Section 37.5.1) and the type hierarchy that relates them. The type hierarchy — the subtyping relationships among the qualifiers — can be
defined either declaratively via meta-annotations (Section 37.5.2), or procedurally through subclassing QualifierHierarchy or TypeHierarchy (Section 37.5.3).
Type qualifiers are defined as Java annotations. In Java, an annotation is defined using the Java @interface keyword. Here is how to define a two-qualifier hierarchy:
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.framework.qual.DefaultQualifierInHierarchy;
import org.checkerframework.framework.qual.SubtypeOf;
/**
* The run-time value of the integer is unknown.
*
* @checker_framework.manual #nonnegative-checker Non-Negative Checker
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({})
@DefaultQualifierInHierarchy
public @interface UnknownSign {}
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.framework.qual.LiteralKind;
import org.checkerframework.framework.qual.SubtypeOf;
/**
* Indicates that the value is greater than or equal to zero.
*
* @checker_framework.manual #nonnegative-checker Non-Negative Checker
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({UnknownSign.class})
public @interface NonNegative {}
The @SubtypeOf meta-annotation indicates the parent in the type hierarchy.
The @Target meta-annotation indicates where the annotation may be written. All type qualifiers that users can write in source code should
have the value ElementType.TYPE_USE, and optionally the additional value ElementType.TYPE_PARAMETER, but no other ElementType values.
The qualifiers should be in a qual subpackage of the type-checker package — by default, the checker reflectively determines the qualifiers, and the only thing that matters for that is the package name. As mentioned in Section 37.2, the files for that qual package can be either in a subdirectory or in a separate Gradle module, depending on whether they should be distributable separately. The Checker Framework automatically treats
any annotation that is declared in the qual package as a type qualifier. (See Section 37.6.1 for more details.) For example, the Nullness Checker’s source file is located at
.../nullness/NullnessChecker.java. The @NonNull qualifier is defined in file .../nullness/qual/NonNull.java.
Your type system should include a top qualifier and a bottom qualifier (Section 37.5.7). The top qualifier is conventionally named CheckerNameUnknown. Most type systems
should also include a polymorphic qualifier @PolyMyTypeSystem (Section 37.5.2).
One of the annotations must be meta-annotated with @DefaultQualifierInHierarchy or @DefaultFor(TypeUseLocation.OTHERWISE). It is usually easiest to make the top type be the default; this may or may not be the correct default for the type system design.
Choose good names for the qualifiers, because users will write these in their source code. The Javadoc of every type qualifier should include a precise English description and an example use of the qualifier.
In source code, declaration annotations are written on their own line, and type qualifiers are written on the same line as the type they apply to. Section 40.6.10 explains how to configure tools to format type annotations properly.
Declaratively, the type system designer uses two meta-annotations (written on the declaration of qualifier annotations) to specify the qualifier hierarchy.
• @SubtypeOf denotes that a qualifier is a subtype of another qualifier or qualifiers, specified as an array of class literals. For example, for any type T, @NonNull T is a subtype of @Nullable
T:
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf( { Nullable.class } )
public @interface NonNull {}
@SubtypeOf accepts multiple annotation classes as an argument, permitting the type hierarchy to be an arbitrary DAG.
All type qualifiers, except for polymorphic qualifiers (see below and also Section 32.2), need to be properly annotated with SubtypeOf.
The top qualifier is annotated with @SubtypeOf( { } ). The top qualifier is the qualifier that is a supertype of all other qualifiers. For example, @Nullable is the top
qualifier of the Nullness type system, hence is defined as:
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf( {} )
public @interface Nullable {}
If the top qualifier of the hierarchy is the generic unqualified type (this is not recommended!), then its children will use @SubtypeOf(Unqualified.class), but no @SubtypeOf({}) annotation on the top qualifier Unqualified is necessary. For an example, see the
Encrypted type system of Section 30.2.
• @PolymorphicQualifier denotes that a qualifier is a polymorphic qualifier. For example:
import java.lang.annotation.ElementType;
import java.lang.annotation.Target;
import org.checkerframework.framework.qual.PolymorphicQualifier;
@PolymorphicQualifier(Nullable.class)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface PolyNull {}
A polymorphic qualifier must not have a @SubtypeOf meta-annotation nor be mentioned in any other @SubtypeOf meta-annotation.
For how to restrict instantiation, see Section 37.5.2. For a general description of polymorphic qualifiers, see Section 32.2.
The declarative and procedural mechanisms for specifying the hierarchy can be used together. If any of the annotations representing type qualifiers have elements, then the relationships between those qualifiers must be defined procedurally.
Sometimes, you wish to restrict how a polymorphic qualifier can be instantiated. An example is the Signedness Checker (Chapter 21). Its two main qualifiers are @Signed and @Unsigned, and the top qualifier
(which should be rarely used) is @UnknownSignedness.
As described so far, there is no way for a programmer to require that two method arguments have the same signedness type. Writing
void foo(@PolySigned Object a, @PolySigned Object b) { ... }
permits every invocation, because one of its instantiations is
void foo(@UnknownSignedness Object a, @UnknownSignedness Object b) { ... }
which is consistent with any two arguments, regardless of their signedness type.
It is possible to permit only method calls whose arguments have exactly the same type qualifier. This is enabled for an entire type system. To do so, create a subclass of DefaultQualifierPolymorphism, override its combine method, and make method createQualifierPolymorphism in the type factory return an instance of the new subclass. The Signedness Checker gives an example.
Changing the qualifier polymorphism allows a loophole: upcasts to top. For example, the type system permits a call like
Objects.equals((@UnknownSignedness) mySigned, (@UnknownSignedness) myUnsigned)
A type system can forbid upcasts to top (including in assignments, not just explicit casts) to close this loophole.
If you change the qualifier polymorphism, your type system may need class qualifier polymorphism (see Section 32.3). And, you may need to suppress false positive warnings within the body of methods whose
formal parameter types are annotated with the polymorphic qualifier (e.g., @PolySigned).
The declarative syntax suffices for most cases. More complex type hierarchies can be expressed by overriding, in your subclass of BaseAnnotatedTypeFactory, either
createQualifierHierarchy or createTypeHierarchy (typically only one of these needs to be overridden).
For more details, see the Javadoc of those methods and of the classes QualifierHierarchy and TypeHierarchy.
The QualifierHierarchy class represents the qualifier hierarchy (not the type hierarchy). A type-system designer may subclass QualifierHierarchy to express customized qualifier relationships (e.g., relationships based on annotation arguments).
The TypeHierarchy class represents the type hierarchy — that is, relationships between annotated types, rather than merely type qualifiers, e.g., @NonNull Date is a
subtype of @Nullable Date. The default TypeHierarchy uses QualifierHierarchy to determine all subtyping relationships. The default TypeHierarchy handles generic type arguments, array
components, type variables, and wildcards in a similar manner to the Java standard subtype relationship but taking qualifiers into consideration. Some type systems may need to override that behavior. For instance, the Java Language Specification specifies that two generic types are subtypes only if their type
arguments are identical: for example, List<Date> is not a subtype of List<Object>, or of any other generic List. (In the technical jargon, the generic arguments are “invariant” or “novariant”.)
A type system applies the default qualifier where the user has not written a qualifier (and no other default qualifier is applicable), as explained in Section 33.5.
The type system designer must specify the default annotation. The designer can specify the default annotation declaratively, using the @DefaultQualifierInHierarchy meta-annotation. Note that the default will apply to any source code that the checker reads, including stub libraries, but will not apply to compiled .class files that the checker reads.
Alternately, the type system designer may specify a default procedurally, by overriding the GenericAnnotatedTypeFactory.addCheckedCodeDefaults method. You may do this even if you have declaratively defined the qualifier hierarchy.
If the default qualifier in the type hierarchy requires a value, there are ways for the type system designer to specify a default value both declaratively and procedurally, as well. To do so declaratively, after the declaration of the element in the qualifier file, append the string default value,
where value is the value you want to be the default. For instance, int value() default 0; would make value default to zero. Alternatively, the procedural method described above can be used.
The default qualifier applies to most, but not all, unannotated types. Section 33.5.3 describes other defaulting rules that are automatically added to every checker. Also, Section 33.5 describes other meta-annotations used to specify default annotations.
Sometimes, a checker is only relevant to certain Java types. The @RelevantJavaTypes annotation on the checker class indicates that its qualifiers may only be written on those
types, their subtypes, and their supertypes.
As an example of relevant types, the Format String Checker is relevant only to CharSequence and its subtypes such as String. You cannot write @Format on a List or a Number. As another example, the Index Checker and the Signedness Checker are only relevant to integral numeric types. You cannot
write @Positive on a List or a float.
If a user writes an annotation on an irrelevant type, the Checker Framework issues an anno.on.irrelevant error.
Irrelevant types are ordinarily defaulted to the top annotation. A checker designer may change the default, and it may differ from type to type. For example, the Signedness Checker treats all types that are not numeric integral types as @Signed, but treats the char and Character types as @Unsigned.
If a type is relevant, so are all its supertypes including Object. This prevents qualifiers from being lost via an assignment to a supertype. For example, in this code:
@SomeAnn MyClass x = ...; Object y = x; MyClass z = (MyClass) y;
variables x and z have the same type qualifiers, without them being lost via the assignment to Object.
Every annotation should belong to only one type system. No annotation should be used by multiple type systems. This is true even of annotations that are internal to the type system and are not intended to be written by the programmer.
Suppose that you have two type systems that both use the same type qualifier @Bottom. In a client program, a use of type T may require type qualifier @Bottom for one type system but a different qualifier for the other type system. There is no annotation that a programmer
can write to make the program type-check under both type systems.
This also applies to type qualifiers that a programmer does not write, because the compiler outputs .class files that contain an explicit type qualifier on every type — a defaulted or inferred type qualifier if the programmer didn’t write a type qualifier explicitly.
When you define a type system, its qualifier hierarchy must be a lattice: every set of qualifiers has a unique least upper bound and a unique greatest lower bound. This implies that there must be a top qualifier that is a supertype of all other qualifiers, and there must be a bottom qualifier that is a subtype of all other
qualifiers. Furthermore, the top qualifier and bottom qualifier should be defined specifically for the type system. Don’t reuse an existing qualifier from the Checker Framework such as @Unqualified.
It is possible that a single type-checker checks multiple qualifier hierarchies. An example is the Nullness Checker, which has three separate qualifier hierarchies, one each for nullness, initialization, and map keys. In this case, each qualifier hierarchy would have its own top qualifier and its own bottom qualifier; they don’t all have to share a single top qualifier or a single bottom qualifier.
Bottom qualifier Your qualifier hierarchy must have a bottom qualifier — a qualifier that is a (direct or indirect) subtype of every other qualifier.
null has the bottom type. Because the only value with type Void is null, uses of the type Void are also bottom. (The only exception is if the type system has special treatment for null values, as the Nullness Checker does. In that case, add the
meta-annotation @QualifierForLiterals(LiteralKind.NULL) to the correct qualifier.) This legal code will not type-check unless null has the
bottom type:
<T> T f() {
return null;
}
Some type systems have a special bottom type that is used only for the null value, and for dead code and other erroneous situations. In this case, users should only write the bottom qualifier on explicit bounds. Also, the definition of the bottom qualifier should be meta-annotated with:
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, TypeUseLocation.EXPLICIT_UPPER_BOUND})
Furthermore, by convention the name of such a qualifier ends with “Bottom”.
It might seem that the hierarchy shown in Figure 3.5 lacks a bottom qualifier. The actual implementation does contain a bottom qualifier, @FBCBottom, that users rarely write.
Top qualifier Your qualifier hierarchy must have a single top qualifier — a qualifier that is a (direct or indirect) supertype of every other qualifier. There are many reasons this is essential. One reason is that the default type for local variables is the top qualifier, and there must be an unambiguous choice for the default type.
Sometimes, an annotation needs to refer to a Java expression. Section 33.8 gives examples of such annotations and also explains what Java expressions can and cannot be referred to.
This section explains how to implement a dependent type annotation.
A “dependent type annotation” must have one element, value, that is an array of strings. The Checker Framework verifies that the annotation’s arguments are valid expressions according to the rules of Section 33.8. If the expression is not valid, an error is issued and the string in the annotation is changed to indicate that the expression is not valid.
The Checker Framework standardizes the expression strings. For example, a field f can be referred to as either “f” or “this.f”. If the programmer writes “f”, the Checker Framework treats it as if the programmer had written “this.f”. An
advantage of this canonicalization is that comparisons, such as isSubtype, can be implemented as string comparisons.
The Checker Framework viewpoint-adapts type annotations on method, constructor, and field declarations at uses of those methods, constructors, and fields. For example, given the following class
class MyClass {
Object field = ...;
@Anno("this.field") Object field2 = ...;
}
and assuming the variable myClass is of type MyClass, then the type of myClass.field is viewpoint-adapted to @Anno("myClass.field").
To use this built-in functionality, add a @JavaExpression annotation to any annotation element that should be interpreted as a Java expression. The type of the element must be an
array of Strings. If your checker requires special handling of Java expressions, your checker implementation should override GenericAnnotatedTypeFactory.createDependentTypesHelper to return a subclass of DependentTypesHelper.
Given a specific expression in the program (of type Tree or Node), a checker may need to obtain its canonical string representation. This enables the checker to create a dependent type annotation that refers to it, or to compare to the string expression of an existing expression annotation. To obtain the string, first
create a JavaExpression object by calling fromTree(ExpressionTree) or fromNode(Node). Then, call toString() on the JavaExpression object.
Some pre- and post-condition annotations that have multiple elements (that is, annotations that take multiple arguments) should be repeatable, so that programmers can specify them more than once. An example is @EnsuresNonNullIf; it could not be defined with each of its elements being a list, as (for example) @KeyFor is.
Make an annotation A repeatable by defining a nested annotation (within A’s definition) named List, and writing @Repeatable(A.List.class) on A’s definition.
A checker’s entry point is a subclass of SourceChecker, and is usually a direct subclass of either BaseTypeChecker or AggregateChecker.
This entry point, which we call the checker class, serves two roles: an interface to the compiler and a factory for constructing type-system classes.
Because the Checker Framework provides reasonable defaults, oftentimes the checker class has no work to do. Here are the complete definitions of the checker classes for the Interning Checker and the Nullness Checker:
package my.package;
import org.checkerframework.common.basetype.BaseTypeChecker;
@SupportedLintOptions({"dotequals"})
public final class InterningChecker extends BaseTypeChecker {}
package my.package;
import org.checkerframework.common.basetype.BaseTypeChecker;
@SupportedLintOptions({"flow", "cast", "cast:redundant"})
public class NullnessChecker extends BaseTypeChecker {}
(The @SupportedLintOptions annotation is optional, and many checker classes do not have one.)
The checker class bridges between the Java compiler and the checker. It invokes the type-rule check visitor on every Java source file being compiled. The checker uses SourceChecker.reportError and SourceChecker.reportWarning to issue errors and warnings.
Also, the checker class follows the factory method pattern to construct the concrete classes (e.g., visitor, factory) and annotation hierarchy representation. It is a convention that, for a type system named Foo, the compiler interface (checker), the visitor, and the annotated type factory are named
FooChecker, FooVisitor, and FooAnnotatedTypeFactory. BaseTypeChecker uses the convention to reflectively construct the
components. Otherwise, the checker writer must specify the component classes for construction.
A checker can customize the default error messages through a Properties-loadable text file named messages.properties that appears
in the same directory as the checker class. The property file keys are the strings passed to reportError and reportWarning (like
"type.incompatible") and the values are the strings to be printed ("cannot assign ..."). The messages.properties file only needs to mention the new messages that the checker defines. It is also allowed to override messages defined in superclasses, but this is rarely
needed. Section 34.1.3 discusses best practices when using a message key in a @SuppressWarnings annotation.
A checker must indicate the annotations that it supports (that make up its type hierarchy).
By default, a checker supports all type annotations in a subdirectory named qual that is in the same directory as the checker (unless you are creating multiple distribution artifacts, one for your checker and one for its qualifiers). A type annotation is meta-annotated with either
@Target(ElementType.TYPE_USE) or @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}).
To indicate support for annotations that are located outside of the qual subdirectory, or annotations that have other ElementType values, checker writers can override the createSupportedTypeQualifiers method (see its Javadoc for details). It is required to define
createSupportedTypeQualifiers if you are mixing qualifiers from multiple directories (including when extending an existing checker that has its own qualifiers), and if you are using the Buck build tool, whose class loader cannot find the qualifier directory.
An aggregate checker (which extends AggregateChecker) does not need to specify its type qualifiers, but each of its component checkers should do so.
Sometimes, multiple checkers work together and should always be run together. There are two different ways to bundle multiple checkers together, by creating either an “aggregate checker” or a “compound checker”.
1. An aggregate checker runs multiple independent, unrelated checkers. There is no communication or cooperation among them.
The effect is the same as if a user passes multiple processors to the -processor command-line option, except the error messages are interleaved such that all errors about a line of code appear together.
For example, instead of a user having to run
javac -processor DistanceUnitChecker,VelocityUnitChecker,MassUnitChecker MyFile.java
the user can write
javac -processor MyUnitCheckers MyFile.java
if you define an aggregate checker class. Extend AggregateChecker and override the getSupportedCheckers method, like the following:
public class MyUnitCheckers extends AggregateChecker {
@Override
protected Collection<Class<? extends SourceChecker>> getSupportedCheckers() {
Collection<Class<? extends SourceChecker>> checkers = new ArrayList<>(3);
Collections.addAll(
checkers,
DistanceUnitChecker.class, VelocityUnitChecker.class, MassUnitChecker.class);
return checkers;
}
}
An example of an aggregate checker is I18nChecker (see Section 17.2), which consists of I18nSubchecker and LocalizableKeyChecker.
2. Use a compound checker to express dependencies among checkers. Suppose it only makes sense to run MyChecker if MyHelperChecker has already been run; that might be the case if MyHelperChecker computes some information that MyChecker needs to use.
Override MyChecker. to return a list of the checkers that MyChecker depends on.
Every one of them will be run before MyChecker is run. One of MyChecker’s subcheckers may itself be a compound checker, and multiple checkers may declare a dependence on the same subchecker. The Checker Framework will run each checker once, and in an order consistent with all the dependences.
getImmediateSubcheckerClasses
A checker obtains information from its subcheckers (those that ran before it) by querying their AnnotatedTypeFactory to determine the types of variables. Obtain the
AnnotatedTypeFactory by calling getTypeFactoryOfSubcheckerOrNull.
An example of a compound checker is SignednessChecker (see Chapter 21) for
which ValueChecker is a subchecker.
A checker can provide two kinds of command-line options: boolean flags and named string values (the standard annotation processor options).
To specify a simple boolean flag, add:
@SupportedLintOptions({"myflag"})
to your checker subclass. The value of the flag can be queried using
checker.getLintOption("myflag", false)
The second argument sets the default value that should be returned.
To pass a flag on the command line, call javac as follows:
javac -processor mypackage.MyChecker -Alint=myflag
For more complicated options, one can use the standard @SupportedOptions annotation on the checker, as in:
@SupportedOptions({"myoption"})
The value of the option can be queried using
checker.getOption("myoption")
To pass an option on the command line, call javac as follows:
javac -processor mypackage.MyChecker -Amyoption=p1,p2
The value is returned as a single string and you have to perform the required parsing of the option.
The default options passed to a custom checker may be customized by overriding the getOptions method in the custom checker class.
For example, to ignore the introduce.eliminate warnings raised by the Optional Checker (Chapter 5), override getOptions as follows:
@Override
public Map<String, String> getOptions() {
Map<String, String> options = new HashMap<>(super.getOptions());
options.put("suppressWarnings", "optional:introduce.eliminate");
return options;
}
in the OptionalChecker class.
A type system’s rules define which operations on values of a particular type are forbidden. These rules must be defined procedurally, not declaratively. Put them in a file MyCheckerVisitor.java that extends BaseTypeVisitor.
BaseTypeVisitor performs type-checking at each node of a source file’s AST. It uses the visitor design pattern to traverse Java syntax trees as provided by Oracle’s jdk.compiler API, and it issues an error or warning (by calling reportError or reportWarning) whenever the type system is
violated.
Most type-checkers override only a few methods in BaseTypeVisitor. A checker’s visitor overrides one method in the base visitor for each special rule in the type qualifier
system. The last line of the overridden version is “return super.visitTreeType(node, p);”. If the method didn’t raise any error, the superclass implementation can perform standard checks.
By default, BaseTypeVisitor performs subtyping checks that are similar to Java subtype rules, but taking the type qualifiers into account. BaseTypeVisitor issues these errors:
• invalid assignment (type.incompatible) for an assignment from an expression type to an incompatible type. The assignment may be a simple assignment, or pseudo-assignment like return expressions or argument passing in a method invocation
In particular, in every assignment and pseudo-assignment, the left-hand side of the assignment is a supertype of (or the same type as) the right-hand side. For example, this assignment is not permitted:
@Nullable Object myObject;
@NonNull Object myNonNullObject;
...
myNonNullObject = myObject; // invalid assignment
• invalid generic argument (type.argument) when a type is bound to an incompatible generic type variable
• invalid method invocation (method.invocation) when a method is invoked on an object whose type is incompatible with the method receiver type
• invalid overriding parameter type (override.param) when a parameter in a method declaration is incompatible with that parameter in the overridden method’s declaration
• invalid overriding return type (override.return) when the return type in a method declaration is incompatible with the return type in the overridden method’s declaration
• invalid overriding receiver type (override.receiver) when a receiver in a method declaration is incompatible with that receiver in the overridden method’s declaration
The Checker Framework needs to do its own traversal of the AST even though it operates as an ordinary annotation processor [Dar06]. Java provides a visitor for Java code that is intended to be used by annotation processors, but that visitor only visits the public elements of Java code, such as classes, fields, methods, and method arguments — it does not visit code bodies or various other locations. The Checker Framework hardly uses the built-in visitor — as soon as the built-in visitor starts to visit a class, then the Checker Framework’s visitor takes over and visits all of the class’s source code.
Because there is no standard API for the AST of Java code1, the Checker Framework uses the javac implementation. This is why the Checker Framework is not deeply integrated with Eclipse or IntelliJ IDEA, but runs as an external tool (see Section 39.8).
1 Actually, there is a standard API for Java ASTs — JSR 198 (Extension API for Integrated Development Environments) [Cro06]. If tools were to implement it (which would just require writing wrappers or adapters), then the Checker Framework and similar tools could be portable among different compilers and IDEs.
If a method’s contract is expressible in the type system’s annotation syntax, then you should write annotations, in a stub file or annotated JDK (Chapter 36).
If the contract is not expressible, you can create a declaration annotation, and your checker can treat methods with that annotation specially. An example is the @FormatMethod annotation; see Section 15.5.
A final alternative is to write a type-checking rule for method invocation, where your rule checks the (class and) name of the method being called and then treats the method in a special way.
The annotated type of expressions and types is defined via type introduction rules in the type factory. For most expressions and types, these rules are the same regardless of the type system. For example, the type of a method invocation expression is the return type of the invoked method, viewpoint-adapted for the call site. The framework implements these rules so that all type systems automatically use them. For other expressions, such as string literals, their (annotated) types depend on the type system, so the framework provides a way to specify what qualifiers should apply to these expressions.
Defaulting rules are type introduction rules for computing the annotated type for an unannotated type; these rules are explained in Section 37.5.4. The meta-annotation @QualifierForLiterals can be written on an annotation declaration to specify that the annotation should be applied to the type of literals listed in the meta-annotation.
If the meta-annotations are not sufficiently expressive, then you can write your own type introduction rules. There are three ways to do so. Each makes changes to an AnnotatedTypeMirror, which is the Checker Framework’s representation of an annotated type.
1. Define a subclass of TreeAnnotator, typically as a private inner class of your AnnotatedTypeFactory. There is a method of
TreeAnnotator for every AST node, and the visitor has access to both the tree (the AST node) and its type.
A TreeAnnotator is best suited to changing the type of an expression. Don’t try to use a TreeAnnotator to change the type of a variable or method declaration, because that change will not generally be seen at uses of the variable or method.
After defining your TreeAnnotator, override createTreeAnnotator (in your subclass of AnnotatedTypeFactory) to return a ListTreeAnnotator containing your new TreeAnnotator, as in:
@Override
protected TreeAnnotator createTreeAnnotator() {
return new ListTreeAnnotator(super.createTreeAnnotator(), new MyTreeAnnotator(this));
}
In code like the above, you might choose to put your TreeAnnotator first. Several tree annotators are run by default, and among them, PropagationTreeAnnotator adds annotations to AnnotatedTypeMirrors that do not have an annotation, but has no effect on those that
have an annotation.
2. Define a subclass of a TypeAnnotator, typically as a private inner class of your AnnotatedTypeFactory. There is a method of
TypeAnnotator for every kind of type, and the visitor has access to only the type (including base type and qualifiers). In your subclass of AnnotatedTypeFactory, override createTypeAnnotator to return a ListTypeAnnotator containing that annotator, as
in
@Override
protected TypeAnnotator createTypeAnnotator() {
return new ListTypeAnnotator(new MyTypeAnnotator(this), super.createTypeAnnotator());
}
(or put your TypeAnnotator last, depending on the behavior you want).
3. Create a subclass of AnnotatedTypeFactory and override two addComputedTypeAnnotations methods: addComputedTypeAnnotations(Tree,AnnotatedTypeMirror) (or addComputedTypeAnnotations(Tree,AnnotatedTypeMirror,boolean) if extending GenericAnnotatedTypeFactory) and addComputedTypeAnnotations(Element,AnnotatedTypeMirror). The methods can make arbitrary changes to the annotations on a type.
Recall that AnnotatedTypeFactory, when given a program expression, returns the expression’s type. This should include not only the qualifiers that the programmer explicitly wrote in the source code, but also default annotations and type refinement (see Section 33.4 for explanations of these concepts).
The approach of overriding addComputedTypeAnnotations is a last resort, if your logic cannot be implemented using a TreeAnnotator or a TypeAnnotator. The implementation of addComputedTypeAnnotations in
GenericAnnotatedTypeFactory calls the tree annotator and the type annotator (in that order), but by overriding the method you can cause your logic to be run even earlier or even later.
TreeAnnotators
A subclass of TreeAnnotator should not, in general, call getAnnotatedType() more than once. This is primarily a concern for visitBinary() and visitCompoundAssignment(). For example, the implementation of visitBinary() should
not start with
AnnotatedTypeMirror lExpr = getAnnotatedType(tree.getLeftOperand());
AnnotatedTypeMirror rExpr = getAnnotatedType(tree.getRightOperand());
The reason is that PropagationTreeAnnotator already does such recursion. If two TreeAnnotators do so, then expressions at the base of a large binary tree will be visited exponentially many times, leading to slowdowns or the appearance of an infinite loop.
One approach is to not call getAnnotatedType() in visitBinary(); this is what UpperBoundAnnotatedTypeFactory does.
Another approach is to disable PropagationTreeAnnotator, doing all work in a different TreeAnnotator. Create a subclass of PropagationTreeAnnotator whose visitBinary() method does no work, and use that subclass in place of
PropagationTreeAnnotator itself. This is what RegexAnnotatedTypeFactory and UnitsAnnotatedTypeFactory do.
By default, every checker performs flow-sensitive type refinement, as described in Section 33.7.
This section of the manual explains how to enhance the Checker Framework’s built-in type refinement. Most commonly, you will inform the Checker Framework about a run-time test that gives information about the type qualifiers in your type system. Section 33.7.4 gives examples of type systems with and without run-time tests.
The steps to customizing type refinement are:
1. §37.9.1 Determine which expressions will be refined.
2. §37.9.2 Create required class and configure its use.
4. §37.9.4 Implement the refinement.
The Regex Checker’s dataflow customization for the RegexUtil.asRegex run-time check is used as a running example.
If needed, you can find more details about the implementation of type refinement, and the control flow graph (CFG) data structure that it uses, in the Dataflow Manual.
A run-time check or run-time operation involves multiple expressions (arguments, results). Determine which expression the customization will refine. This is usually specific to the type system and run-time test. There is no code to write in this step; you are merely determining the design of your type refinement.
For the program operation op(a,b), you can refine the types in either or both of the following ways:
1. Change the result type of the entire expression op(a,b).
As an example (and as the running example of implementing a dataflow refinement), the RegexUtil.asRegex method is declared as:
@Regex(0) String asRegex(String s, int groups) { ... }
This annotation is sound and conservative: it says that an expression such as RegexUtil.asRegex(myString, myInt) has type @Regex(0) String. However, this annotation is imprecise. When the group argument is known at compile time, a better estimate can be given.
For example, RegexUtil.asRegex(myString, 2) has type @Regex(2) String.
2. Change the type of some other expression, such as a or b.
As an example, consider an equality test in the Nullness type system:
@Nullable String s;
if (s != null) {
...
} else {
...
}
The type of s != null is always boolean. However, in the true branch, the type of s can be refined to @NonNull String.
If you are refining the types of arguments or the result of a method call, then you may be able to implement your flow-sensitive refinement rules by just writing @EnsuresQualifier and/or @EnsuresQualifierIf annotations. When this is possible, it is the best approach.
Sections 37.9.2–37.9.4 explain how to create a transfer class when the @EnsuresQualifier and @EnsuresQualifierIf annotations are insufficient.
In the same directory as MyCheckerChecker.java, create a class named MyCheckerTransfer that extends CFTransfer.
Leave the class body empty for now, except for a constructor:
public MyCheckerTransfer(CFAnalysis analysis) {
super(analysis);
}
Your class will add functionality by overriding methods of CFTransfer, which performs the default Checker Framework type refinement.
As an example, the Regex Checker’s extended CFTransfer is RegexTransfer.
(If you disregard the instructions above and choose a different name or a different directory for your MyCheckerTransfer class, you will also need to override the createFlowTransferFunction method in your type factory to return a new instance of the class.)
(As a reminder, use of @EnsuresQualifier and @EnsuresQualifierIf may obviate the need for a transfer class.)
Decide what source code syntax is relevant to the run-time checks or run-time operations you are trying to support. The CFG (control flow graph) represents source code as Nodes. Some Nodes correspond to a node in the abstract syntax tree of the program being checked, while others are synthesized during CFG construction and have no corresponding AST node (see
Section 37.9.3).
In your extended CFTransfer, override the visitor method that handles the Nodes relevant to your run-time check or run-time operation. Leave the body of the overriding method empty for now.
For example, the Regex Checker refines the type based on a call to the RegexUtil.isRegex method. A method call is represented by a MethodInvocationNode. Therefore, RegexTransfer overrides the visitMethodInvocation method:
public TransferResult<CFValue, CFStore> visitMethodInvocation(
MethodInvocationNode n, TransferInput<CFValue, CFStore> in) { ... }
The Node subclasses can be found in the org.checkerframework.dataflow.cfg.node package. Some examples are EqualToNode, LeftShiftNode, and VariableDeclarationNode.
A Node is basically equivalent to a javac compiler Tree.
See Section 37.14 for more information about Trees. As an example, the statement String a = ""; is represented as this abstract syntax tree:
VariableTree:
name: "a"
type:
IdentifierTree
name: String
initializer:
LiteralTree
value: ""
Each visitor method in CFAbstractTransfer returns a TransferResult. A TransferResult represents the refined information that is known after an operation. It has two components: the result type for the Node being evaluated, and a map from expressions in scope to estimates of their types (a Store). Each of these components is relevant to one of the two cases in Section 37.9.1:
1.
Changing the TransferResult’s result type changes the type that is returned by the AnnotatedTypeFactory for the tree corresponding to the Node that was visited. (Remember that BaseTypeVisitor uses the AnnotatedTypeFactory to look up the type of a Tree, and then performs checks on types of one or more Trees.)
For example, when RegexTransfer evaluates a RegexUtil.asRegex invocation, it updates the TransferResult’s result type. This changes the type of the RegexUtil.asRegex invocation when its Tree is looked up by the AnnotatedTypeFactory. See below for details.
2. Updating the Store treats an expression as having a refined type for the remainder of the method or conditional block. For example, when the Nullness Checker’s dataflow evaluates
myvar != null, it updates the Store to specify that the variable myvar should be treated as having type @NonNull for the rest of the then branch.
Not all kinds of expressions can be refined; currently method return values, local variables, fields, and array values can be stored in the Store. Other kinds of expressions, like binary
expressions or casts, cannot be stored in the Store.
The rest of this section details implementing the visitor method RegexTransfer.visitMethodInvocation for the RegexUtil.asRegex run-time test. You can find other examples of visitor methods in LockTransfer and FormatterTransfer.
1. Determine if the visited Node is of interest
A visitor method is invoked for all instances of a given Node kind in the program. The visitor must inspect the Node to determine if it is an instance of the desired run-time test or operation. For example, visitMethodInvocation is called when dataflow processes any method invocation, but
the RegexTransfer should only refine the result of RegexUtil.asRegex invocations:
@Override
public TransferResult<CFValue, CFStore> visitMethodInvocation(...)
...
MethodAccessNode target = n.getTarget();
ExecutableElement method = target.getMethod();
Node receiver = target.getReceiver();
if (receiver instanceof ClassNameNode) {
String receiverName = ((ClassNameNode) receiver).getElement().toString();
// Is this a call to static method asRegex(s, groups) in a class named RegexUtil?
if (receiverName.equals("RegexUtil")
&& ElementUtils.matchesElement(method,
"asRegex", String.class, int.class)) {
...
2. Determine the refined type
Sometimes the refined type is dependent on the parts of the operation, such as arguments passed to it.
For example, the refined type of RegexUtil.asRegex is dependent on the integer argument to the method call. The RegexTransfer uses this argument to build the
resulting type @Regex(i), where i is the value of the integer argument. For simplicity the below code only uses the value of the integer argument if the argument was an integer literal. It could be extended to use the value of the argument if it was any compile-time
constant or was inferred at compile time by another analysis, such as the Constant Value Checker (Chapter 24).
AnnotationMirror regexAnnotation;
Node count = n.getArgument(1);
if (count instanceof IntegerLiteralNode) {
// argument is a literal integer
IntegerLiteralNode iln = (IntegerLiteralNode) count;
Integer groupCount = iln.getValue();
regexAnnotation = factory.createRegexAnnotation(groupCount);
} else {
// argument is not a literal integer; fall back to @Regex(), which is the same as @Regex(0)
regexAnnotation = AnnotationBuilder.fromClass(factory.getElementUtils(), Regex.class);
}
3. Return a TransferResult with the refined types
Recall that the type of an expression is refined by modifying the TransferResult returned by a visitor method. Since the RegexTransfer is updating the type of the run-time test itself, it will update the result type and not the Store.
A CFValue is created to hold the type inferred. CFValue is a
wrapper class for values being inferred by dataflow:
CFValue newResultValue = analysis.createSingleAnnotationValue(regexAnnotation,
result.getResultValue().getType().getUnderlyingType());
Then, RegexTransfer’s visitMethodInvocation creates and returns a TransferResult using newResultValue as the result type.
return new RegularTransferResult<>(newResultValue, result.getRegularStore());
As a result of this code, when the Regex Checker encounters a RegexUtil.asRegex method call, the checker will refine the return type of the method if it can determine the value of the integer parameter at compile time.
By default, the Checker Framework assumes that modifications to an object’s fields do not change its type qualifiers. This is true for all provenance-based type systems (see Section 33.7.4), for all
value-based type systems over immutable values, and for some other type systems. To indicate that side effects can change a value’s type qualifiers, write sideEffectsUnrefineAliases = true; in the type factory constructor, before the call to this.postInit();. Note
that this setting may lead to large numbers of false positive warnings. You can reduce the number of false positive warnings by writing more precise side effect annotations.
In the uncommon case that you wish to disable the Checker Framework’s built-in flow inference in your checker (this is different than choosing not to extend it as described in Section 37.9), put the following two
lines at the beginning of the constructor for your subtype of BaseAnnotatedTypeFactory:
// disable flow inference
super(checker, /*useFlow=*/ false);
You will need to supply annotations for relevant parts of the JDK; otherwise, your type-checker may produce spurious warnings for code that uses the JDK. You have two options:
• Write JDK annotations in a fork of https://github.com/typetools/jdk.
If your checker is written in a fork of https://github.com/typetools/jdk, then the checker and the JDK must use the same fork name (GitHub organization) and branch name; this is necessary so that the CI jobs use the right annotated JDK.
Clone the JDK and the Checker Framework in the same place; that is, your working copy of the JDK (a jdk directory) should be a sibling of your working copy of the Checker Framework (a checker-framework directory).
Here are some tips:
– Add an @AnnotatedFor annotation to each file you annotate.
– Whenever you add a file, fully annotate it, as described in Section 36.1.4.
– If you are only annotating fields and method signatures (but not ensuring that method bodies type-check), then you don’t need to suppress warnings, because the JDK is not type-checked.
– Double-check your work. If you forget to import an annotation, or you misspell it in the import statement or at some use, it will be silently ignored, which is frustrating.
• Write JDK annotations as stub files (partial Java source files).
Create a file jdk.astub in the checker’s main source directory. You can also create jdkN.astub files that contain methods or classes that only exist in certain JDK versions. The JDK stub files will be automatically used by the checker, unless the user supplies the
command-line option -Aignorejdkastub.
You can also supply .astub files in that directory for other libraries. You should list those other libraries in a @StubFiles annotation on the checker’s main class, so that they
will also be automatically used.
When a stub file should be used by multiple checkers (for example, if it contains purity annotations that are needed by multiple distinct checkers), the stub file should appear in directory checker/src/main/resources/. In the distribution, it will appear at the top level of the
checker.jar file. It will not be used automatically; a user must pass the -Astubs=checker.jar/stubfilename.astub command-line argument (see Section 2.2.1).
While creating a stub file, you may find the debugging options described in Section 36.5.7 useful.
The Checker Framework provides a convenient way to write tests for your checker. Each test case is a Java file, with inline indications of what errors and warnings (if any) a checker should emit. An example is
class MyNullnessTest {
void method() {
Object nullable = null;
// :: error: [dereference.of.nullable]
nullable.toString();
}
}
When the Nullness Checker is run on the above code, it should produce exactly one error, whose message key is dereference.of.nullable, on the line following the “// ::” comment.
The testing infrastructure is extensively documented in file checker-framework/checker/tests/README.md.
If your checker’s source code is within a fork of the Checker Framework repository, then you can copy the testing infrastructure used by some existing type system.
The Checker Framework provides debugging options that can be helpful when implementing a checker. These are provided via the standard javac “-A” switch, which is used to pass options to an annotation processor.
• -AprintAllQualifiers: print all type qualifiers, including qualifiers meta-annotated with @InvisibleQualifier, which are usually not shown.
• -AprintVerboseGenerics: print more information about type parameters and wildcards when they appear in warning messages. Supplying this also implies -AprintAllQualifiers.
• -Anomsgtext: use message keys (such as “type.invalid”) rather than full message text when reporting errors or warnings. This is used by the Checker Framework’s own tests, so they do not need to be changed if the English message is updated.
• -Aonelinemsg: print each error message on a single line, with logical lines separated by “/”. This is useful when using a tool that only shows the first line of the error.
• -AnoPrintErrorStack: don’t print a stack trace when an internal Checker Framework error occurs. Setting this option is rare. You should only do it if you have discovered a bug in a checker, you have already reported the bug, and you want to continue using the checker on a large codebase without
being inundated in stack traces.
• -AnoWarnMemoryConstraints: when memory constraints are impeding performance, issue a note rather than a warning. This prevents the message from being elevated to an error by -Werror.
• -AdumpOnErrors: output a stack trace when reporting errors or warnings.
• -AexceptionLineSeparator: control what line separator is used when printing exceptions. This is useful when tools, such as Maven, only display the first line of exception messages. For example, -AexceptionLineSeparator=" ".
• -Adetailedmsgtext: Output error/warning messages in a stylized format that is easy for tools to parse. This is useful for tools that run the Checker Framework and parse its output, such as IDE plugins. See the source code of SourceChecker.java for details about the format.
The javac-diagnostics-wrapper tool can transform javac’s textual output into other formats, such as JSON in LSP (Language Server Protocol) format.
• -Aignorejdkastub: ignore the jdk.astub and jdkN.astub files in the checker directory. Files passed through the -Astubs option are still processed. This is useful when experimenting with an alternative stub file.
• -ApermitMissingJdk: don’t issue an error if no annotated JDK can be found.
• -AparseAllJdk: parse all JDK files at startup rather than as needed.
• -AstubDebug: print debugging messages while processing stub files. Section 36.5.7 describes more diagnostic command-line arguments.
• -Afilenames: print the name of each file before type-checking it. This can be useful for determining that a long compilation job is making progress.
This option can also help to keep a CI job alive (for example, Travis CI terminates any job that does not produce output for 10 minutes). This does not work if you are using Maven, because Maven does not print the full output of the Java compiler (see https://github.com/codehaus-plexus/plexus-compiler/issues/149). (Also, maven-compiler-plugin is buggy: it sometimes doesn’t print any output if it cannot parse it.)
• -Ashowchecks: print debugging information for each pseudo-assignment check (commonAssignmentCheck) performed by BaseTypeVisitor; see
Section 37.7.
• -AshowWpiFailedInferences: print debugging information about failed inference steps during whole-program inference. Must be used with -Ainfer; see Section 35.2.
If the Checker Framework is in an infinite loop, you can use -Afilenames and -Ashowchecks (which is very verbose) to determine what source code triggers the infinite loop.
While the Checker Framework is in its infinite loop (no more progress is being made), get a traceback (stack trace) from each Java thread, using any of the following four techniques:
• From a different shell than the Checker Framework is running in (running just jcmd gives a list of process IDs):
– jstack pid
– jcmd pid Thread.print
– kill -QUIT pid
• From the same shell that the Checker Framework is running in:
– Press ctrl-\
• -AoutputArgsToFile: This saves to a file the final command-line parameters as passed to the compiler. The file can be used as a script to re-execute the same compilation command. (The script file must be marked as executable on Unix, or must have a .bat extension on Windows.)
Example usage: -AoutputArgsToFile=$HOME/scriptfile
The -AoutputArgsToFile command-line argument is processed by CheckerMain, not by the annotation processor. That means that it can be supplied only when you use the Checker Framework compiler (the “Checker Framework javac wrapper”), and it cannot be written in a file
containing command-line arguments passed to the compiler using the @argfile syntax.
To understand control flow in your program and the resulting type refinement, you can create a graphical representation of the CFG.
Typical use is:
javacheck -processor mypackage.MyProcessor -Aflowdotdir=. MyClass.java for dotfile in *.dot; do dot -Tpdf -o "$dotfile.pdf" "$dotfile"; done
or (for more verbose output)
javacheck -processor mypackage.MyProcessor \ -Acfgviz=org.checkerframework.dataflow.cfg.visualize.DOTCFGVisualizer,outdir=.,verbose \ MyClass.java for dotfile in *.dot; do dot -Tpdf -o "$dotfile.pdf" "$dotfile"; done
where the first command creates file MyClass.dot that represents the CFG, and the second command writes the CFG to a PDF file. The dot program is part of Graphviz.
In the output, conditional basic blocks are represented as octagons with two successors. Special basic blocks are represented as ovals (e.g., the entry and exit point of the method).
To create a CFG while running a type-checker, use the following command-line options.
(See above for typical usage.)
• -Aflowdotdir=somedir: Specify directory for .dot files visualizing the CFG. Shorthand for
-Acfgviz=org.checkerframework.dataflow.cfg.visualize.DOTCFGVisualizer,outdir=somedir. The directory must already exist.
• -Averbosecfg: Enable additional output in the CFG visualization. Equivalent to passing verbose to cfgviz, e.g., as in -Acfgviz=MyVisualizer,verbose.
• -Acfgviz=VizClassName[,opts,...]: Mechanism to visualize the control flow graph (CFG) of all the methods and code fragments analyzed by the dataflow analysis (Section 37.9). The graph also contains information about flow-sensitively refined types of various expressions at many program points.
The argument is a comma-separated sequence. The first element is the fully-qualified name of the org.checkerframework.dataflow.cfg.visualize.CFGVisualizer implementation that should be used. Currently, the possibilities are:
– org.checkerframework.dataflow.cfg.visualize.DOTCFGVisualizer
– org.checkerframework.dataflow.cfg.visualize.StringCFGVisualizer
The remaining keys or key-value pairs are passed to CFGVisualizer.init. Supported keys include
– verbose outputs the store after each basic block (in addition to before); shows transfer result values, unique IDs, and the processing order
– outdir directory into which to write files
– checkerName
You can also use CFGVisualizeLauncher to generate a DOT or String representation of the control flow graph of a given method in a given class. The CFG is
generated and output, but no dataflow analysis is performed.
java -cp $CHECKERFRAMEWORK/checker/dist/checker.jar \ org.checkerframework.dataflow.cfg.visualize.CFGVisualizeLauncher \ MyClass.java --class MyClass --method test --pdf
The above command will generate the corresponding .dot and .pdf files for the method test in the class MyClass in the project directory. To generate a string representation of the graph to standard output, remove --pdf but add
--string. For example:
java -cp $CHECKERFRAMEWORK/checker/dist/checker.jar \ org.checkerframework.dataflow.cfg.visualize.CFGVisualizeLauncher \ MyClass.java --class MyClass --method test --string
For more details about invoking CFGVisualizeLauncher, run it with no arguments.
• -AresourceStats: Whether to output resource statistics at JVM shutdown.
• -AatfDoNotCache: If provided, the Checker Framework will not cache results but will recompute them. This makes the Checker Framework run slower. If the Checker Framework behaves differently with and without this flag, then there is a bug in its caching code. Please report that bug.
• -AatfCacheSize: The size of the Checker Framework’s internal caches. Ignored if -AatfDoNotCache is provided. Most users have no need to set this.
The following example demonstrates how these options are used:
$ javac -processor org.checkerframework.checker.interning.InterningChecker \
docs/examples/InterningExampleWithWarnings.java -Ashowchecks -Anomsgtext -Afilenames
[InterningChecker] InterningExampleWithWarnings.java
success (line 18): STRING_LITERAL "foo"
actual: DECLARED @org.checkerframework.checker.interning.qual.Interned java.lang.String
expected: DECLARED @org.checkerframework.checker.interning.qual.Interned java.lang.String
success (line 19): NEW_CLASS new String("bar")
actual: DECLARED java.lang.String
expected: DECLARED java.lang.String
docs/examples/InterningExampleWithWarnings.java:21: (not.interned)
if (foo == bar) {
^
success (line 22): STRING_LITERAL "foo == bar"
actual: DECLARED @org.checkerframework.checker.interning.qual.Interned java.lang.String
expected: DECLARED java.lang.String
1 error
You can use any standard debugger to observe the execution of your checker.
You can also set up remote (or local) debugging using the following command as a template:
java -jar "$CHECKERFRAMEWORK/checker/dist/checker.jar" \
-J-Xdebug -J-Xrunjdwp:transport=dt_socket,server=y,suspend=y,address=5005 \
-processor org.checkerframework.checker.nullness.NullnessChecker \
src/sandbox/FileToCheck.java
This section describes how to write a chapter for this manual that describes a new type-checker. This is a prerequisite to having your type-checker distributed with the Checker Framework, which is the best way for users to find it and for it to be kept up to date with Checker Framework changes. Even if you do not want your checker distributed with the Checker Framework, these guidelines may help you write better documentation.
When writing a chapter about a new type-checker, see the existing chapters for inspiration. (But recognize that the existing chapters aren’t perfect: maybe they can be improved too.)
A chapter in the Checker Framework manual should generally have the following sections:
The text before the first section in the chapter should state the guarantee that the checker provides and why it is important. It should give an overview of the concepts. It should state how to run the checker.
This section includes descriptions of the annotations with links to the Javadoc. Separate type annotations from declaration annotations, and put any type annotations that a programmer may not write (they are only used internally by the implementation) last within each variety of annotation.
Draw a diagram of the type hierarchy. A textual description of the hierarchy is not sufficient; the diagram really helps readers to understand the system. The diagram will appear in directory docs/manual/figures/; see its README file for tips.
The Javadoc for the annotations deserves the same care as the manual chapter. Each annotation’s Javadoc comment should use the @checker_framework.manual Javadoc taglet to refer to the chapter that describes the checker, and the polymorphic qualifier’s Javadoc should also refer to the
qualifier-polymorphism section. For example, in PolyPresent.java:
* @checker_framework.manual #optional-checker Optional Checker * @checker_framework.manual #qualifier-polymorphism Qualifier polymorphism
This section gives more details about when an error is issued, with examples. This section may be omitted if the checker does not contain special type-checking rules — that is, if the checker only enforces the usual Java subtyping rules.
Code examples.
Sometimes you can omit some of the above sections. Sometimes there are additional sections, such as tips on suppressing warnings, comparisons to other tools, and run-time support.
You will create a new belly-rub-checker.tex file, then \input it at a logical place in manual.tex (not necessarily as the last checker-related chapter). Also add two references to the checker’s chapter: one at the beginning of Chapter 1, and identical text in the appropriate part of Section 33.7.4. Add the new file to docs/manual/Makefile. Keep the lists
in the same order as the manual chapters, to help us notice if anything is missing.
For a chapter or (sub)*section, use \sectionAndLabel{Section title}{section-label}. Section labels should start with the checker name (as in bellyrub-examples) and not with “sec:”. Figure labels should start with
“fig-checkername” and not with “fig:”. The \sectionAndLabel convention is required by the lwarp-postprocess script, which makes the HTML version of the manual use stable, label-based anchors in cross-references. Use \begin{figure} for all figures, including those whose content is a table, in order to have a single consistent numbering for all figures.
Don’t forget to write Javadoc for any annotations that the checker uses. That is part of the documentation and is the first thing that many users may see. The documentation for any annotation should include an example use of the annotation. Also ensure that the Javadoc links back to the manual, using the
@checker_framework.manual custom Javadoc tag.
Since this section of the manual was written, the useful “Hitchhiker’s Guide to javac” has become available at https://openjdk.org/groups/compiler/doc/hhgtjavac/index.html. See it first, and then refer to this section. (This section of the manual should be revised, or parts eliminated, in light of that document.)
A checker built using the Checker Framework makes use of a few interfaces from the underlying compiler (Oracle’s OpenJDK javac). This section describes those interfaces.
The compiler uses and exposes three hierarchies to model the Java source code and classfiles.
A TypeMirror represents a Java type.
There is a TypeMirror interface to represent each type kind, e.g., PrimitiveType for primitive types, ExecutableType for method types, and NullType for the type of the null literal.
TypeMirror does not represent annotated types though. A checker should use the Checker Framework types API, AnnotatedTypeMirror, instead.
AnnotatedTypeMirror parallels the TypeMirror API, but also presents the type annotations associated with the type.
The Checker Framework and the checkers use the types API extensively.
An Element represents a potentially-public declaration that can be accessed from elsewhere: classes,
interfaces, methods, constructors, and fields. Element represents elements found in both source code and bytecode.
There is an Element interface to represent each construct, e.g., TypeElement for classes/interfaces, ExecutableElement for methods/constructors, and VariableElement for local variables and method parameters.
If you need to operate on the declaration level, always use elements rather than trees (see below). This allows the code to work on both source and bytecode elements.
Example: retrieve declaration annotations, check variable modifiers (e.g., strictfp, synchronized)
A Tree represents a syntactic unit in the source code, such as a method declaration, statement, block,
for loop, etc. Trees only represent source code to be compiled (or found in -sourcepath); no tree is available for classes read from bytecode.
There is a Tree interface for each Java source structure, e.g., ClassTree for class declaration, MethodInvocationTree for a method invocation, and EnhancedForLoopTree for an enhanced for statement (also known as a foreach loop).
You should limit your use of trees. A checker uses Trees mainly to traverse the source code and retrieve the types/elements corresponding to them. Then, the checker performs any needed checks on the types/elements instead.
To obtain the position (line number and column number) of a Tree, use a com.sun.source.util.Trees instance to obtain a com.sun.source.util.SourcePositions via getSourcePositions(), then call getStartPosition(...) (or
getEndPosition(...)) on it. com.sun.source.tree.CompilationUnitTree has a LineMap that lets you convert positions to line numbers. Alternatively, you can cast the Tree to the javac-internal type com.sun.tools.javac.tree.JCTree
and call its pos() method, which returns a JCDiagnostic.DiagnosticPosition; doing so requires your code to be compiled and run with --add-exports jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED and --add-exports
jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED.
The three APIs use some common idioms and conventions; knowing them will help you to create your checker.
Type-checking: Do not use instanceof Subinterface to determine which kind of TypeMirror or Element an expression is, because some of the classes that implement the TypeMirror and Element subinterfaces implement
multiple subinterfaces. For example, type instanceof DeclaredType and type instanceof UnionType both return true if type is a com.sun.tools.javac.code.Type.UnionClassType object.
Instead, use the TypeMirror.getKind() or Element.getKind() method. For example, if type is a
com.sun.tools.javac.code.Type.UnionClassType object, then type.getKind() == TypeKind.DECLARED is false and type.getKind() == TypeKind.UNION is true.
For Trees, you can use either Tree.getKind() or instanceof.
Visitors and Scanners: The compiler and the Checker Framework use the visitor pattern extensively. For example, visitors are used to traverse the source tree (BaseTypeVisitor extends TreePathScanner) and for type checking (TreeAnnotator implements TreeVisitor).
Utility classes: Some useful methods appear in a utility class. The OpenJDK convention is that the utility class for a Foo hierarchy is Foos (e.g., Types, Elements, and Trees). The Checker Framework uses a common Utils suffix to distinguish the class names (e.g., TypesUtils, TreeUtils, ElementUtils), with one notable exception: AnnotatedTypes.
AnnotationMirror is an interface that is implemented both by javac and the Checker Framework. The documentation of AnnotationMirror says, “Annotations should be compared using the equals method. There is no guarantee that any particular annotation will always be represented by the same object.” The second sentence is true, but the first sentence is wrong. You should never compare
AnnotationMirrors using equals(), which (for some implementations) is reference equality. AnnotationUtils has various methods that should be used
instead. Also, AnnotationMirrorMap and AnnotationMirrorSet can be used.
The Checker Framework builds on the Annotation Processing API introduced in Java 6. A type-checking annotation processor is one that extends AbstractTypeProcessor; it
gets run on each class source file after the compiler confirms that the class is valid Java code.
The most important methods of AbstractTypeProcessor are typeProcess and getSupportedSourceVersion. The former method is where you
would insert any sort of method call to walk the AST, and the latter just returns a constant indicating the source version that is supported. Implementing these two methods should be enough for a basic plugin; see the Javadoc for the class for other methods that you may find useful later on.
The Checker Framework uses Oracle’s Tree API to access a program’s AST. The Tree API is specific to the Oracle OpenJDK, so the Checker Framework only works with the OpenJDK javac, not with Eclipse’s compiler ecj. This also limits the tightness of the integration of the Checker Framework into other IDEs such as IntelliJ IDEA. An implementation-neutral API would be preferable. In the future, the Checker Framework can be migrated to use the Java Model AST of JSR 198 (Extension API for Integrated Development Environments) [Cro06], which gives access to the source code of a method. But, at present no tools implement JSR 198. Also see Section 37.7.1.
The javac compiler interfaces can be daunting to a newcomer, and their documentation is a bit sparse. The Checker Framework aims to abstract a lot of these complexities. You do not have to understand the implementation of javac to build powerful and useful checkers. Beyond this document, other useful resources include the Java Infrastructure Developer’s guide at https://netbeans.apache.org/wiki/main/javahowto/Java_DevelopersGuide/ and the compiler mailing list archives at https://mail.openjdk.org/pipermail/compiler-dev/ (subscribe at https://mail.openjdk.org/mailman/listinfo/compiler-dev).
To integrate a new checker with the Checker Framework release, perform the following:
• Make sure check-compilermsgs and check-purity run without warnings or errors.