These are some common questions about the Checker Framework and about pluggable type-checking in general. Feel free to suggest improvements to the answers, or other questions to include here.
Contents:
40.1: Motivation for pluggable type-checking
40.1.1: I don’t make type errors, so would pluggable type-checking help me?
40.1.2: Should I use pluggable types (type qualifiers), or should I use Java subtypes?
40.2: Getting started
40.2.1: How do I get started annotating an existing program?
40.2.2: Which checker should I start with?
40.2.3: How can I join the checker-framework-dev mailing list?
40.3: Usability of pluggable type-checking
40.3.1: Are type annotations easy to read and write?
40.3.2: Will my code become cluttered with type annotations?
40.3.3: Will using the Checker Framework slow down my program? Will it slow down the compiler?
40.3.4: How do I shorten the command line when invoking a checker?
40.3.5: Method pre-condition contracts, including formal parameter annotations, make no sense for public methods
40.4: How to handle warnings and errors
40.4.1: What should I do if a checker issues a warning about my code?
40.4.2: Why does a checker issue a warning even though the code checks a property?
40.4.3: What does a certain Checker Framework warning message mean?
40.4.4: What do square brackets mean in a Checker Framework warning message?
40.4.5: Can a pluggable type-checker guarantee that my code is correct?
40.4.6: What guarantee does the Checker Framework give for concurrent code?
40.4.7: How do I make compilation succeed even if a checker issues errors?
40.4.8: Why does the checker always say there are 100 errors or warnings?
40.4.9: Why does the Checker Framework report an error regarding a type I have not written in my program?
40.4.10: Why does the Checker Framework accept code on one line but reject it on the next?
40.4.11: How can I do run-time monitoring of properties that were not statically checked?
40.5: False positive warnings
40.5.1: What is a “false positive” warning?
40.5.2: How can I improve the Checker Framework to eliminate a false positive warning?
40.5.3: Why doesn’t the Checker Framework infer types for fields and method return types?
40.5.4: Why are some operations legal in constructors but not in methods?
40.5.5: Why doesn’t the Checker Framework track relationships between variables?
40.5.6: Why isn’t the Checker Framework path-sensitive?
40.6: Syntax of type annotations
40.6.1: What is a “receiver”?
40.6.2: What is the meaning of an annotation after a type, such as @NonNull Object @Nullable?
40.6.3: What is the meaning of array annotations such as @NonNull Object @Nullable []?
40.6.4: What is the meaning of varargs annotations such as @English String @NonEmpty ...?
40.6.5: What is the meaning of a type qualifier at a class declaration?
40.6.6: How are type qualifiers written on upper and lower bounds?
40.6.7: Why shouldn’t a qualifier apply to both types and declarations?
40.6.8: How do I annotate a fully-qualified type name?
40.6.9: What is the difference between type annotations and declaration annotations?
40.6.10: How should type annotations be formatted in source code? Where should I write type annotations?
40.6.11: How does the Checker Framework handle obsolete declaration annotations?
40.6.12: How do I convert from other tools’ declaration annotations to type annotations?
40.7: Semantics of type annotations
40.7.1: How can I handle typestate, or phases of my program with different data properties?
40.7.2: Why are explicit and implicit bounds defaulted differently?
40.7.3: How should I annotate code that uses generics?
40.7.4: Why are type annotations declared with @Retention(RetentionPolicy.RUNTIME)?
40.8: Creating a new checker
40.8.1: How do I create a new checker?
40.8.2: What properties can and cannot be handled by type-checking?
40.8.3: Why is there no declarative syntax for writing type rules?
40.9: Tool questions
40.9.1: How does pluggable type-checking work?
40.9.2: What classpath is needed to use an annotated library?
40.9.3: Why do .class files contain more annotations than the source code?
40.9.4: Is there a type-checker for managing checked and unchecked exceptions?
40.9.5: The Checker Framework runs too slowly
40.9.6: What does the Checker Framework version number mean?
40.10: Relationship to other tools
40.10.1: Why not just use a bug detector (like SpotBugs or Error Prone)?
40.10.2: How does the Checker Framework compare with Eclipse’s null analysis?
40.10.3: How does the Checker Framework compare with NullAway?
40.10.4: How does the Checker Framework compare with JSpecify?
40.10.5: How does the Checker Framework compare with the EISOP Checker Framework?
40.10.6: How does the Checker Framework compare with the JDK’s Optional type?
40.10.7: How does pluggable type-checking compare with JML?
40.10.8: Is the Checker Framework an official part of Java?
40.10.9: What is the relationship between the Checker Framework and JSR 305?
40.10.10: What is the relationship between the Checker Framework and JSR 308?
Occasionally, a developer claims to make no errors that type-checking could catch, or that any such errors are unimportant because they have low impact and are easy to fix. When I investigate the claim, I invariably find that the developer is mistaken.
Very frequently, the developer has underestimated what type-checking can discover. Not every type error leads to an exception being thrown; and even if an exception is thrown, it may not seem related to classical types. Remember that a type system can discover null pointer dereferences, incorrect side effects, security errors such as information leakage or SQL injection, partially-initialized data, wrong units of measurement, and many other errors. Every programmer makes errors sometimes and works with other people who do. Even where type-checking does not discover a problem directly, it can indicate code with bad smells, thus revealing problems, improving documentation, and making future maintenance easier.
There are other ways to discover errors, including extensive testing and debugging. You should continue to use these. But type-checking is a good complement to these. Type-checking is more effective for some problems, and less effective for other problems. It can reduce (but not eliminate) the time and effort that you spend on other approaches. There are many important errors that type-checking and other automated approaches cannot find; pluggable type-checking gives you more time to focus on those.
In brief, use subtypes when you can, and use type qualifiers when you cannot use subtypes.
For some programming tasks, you can use either a Java subtype (interfaces or subclasses) or a type qualifier. As an example, suppose that your code currently uses String to represent an address. You could use Java subclasses by creating a new Address class and refactor your code to use
it, or you could use type qualifiers by creating an @Address annotation and applying it to some uses of String in your code. As another example, suppose that your code currently uses MyClass in two different ways that should not interact with one another. You could use
Java subclasses by changing MyClass into an interface or abstract class, defining two subclasses, and ensuring that neither subclass ever refers to the other subclass nor to the parent class.
If Java subclasses solve your problem, then that is probably better. We do not encourage you to use type qualifiers as a poor substitute for classes. An advantage of using classes is that the Java type-checker runs every time you compile your code; by contrast, it is possible to forget to run the pluggable type-checker. However, sometimes type qualifiers are a better choice; here are some reasons:
Using a new class may make your code incompatible with existing libraries or clients. You may need to write a conversion at every call to and return from a library call; these conversions add clutter, reduce performance, and (by creating new objects) break object equality properties. Brian Goetz also notes some problems in an article on the pseudo-typedef antipattern [Goe06].
It is possible to add annotations to code you do not maintain or cannot change; for example, you can write library annotations (see Chapter 36).
A Java object has just one class at run time. If you care about multiple correctness properties, then using the Java type system requires a combinatorial number of classes (all possible combinations). By contrast, arbitrary type qualifiers can be used at the same time.
A code change may introduce bugs, whereas adding annotations does not change the run-time behavior.
Type annotations can be applied to primitives and to final classes such as String, which cannot be subclassed.
Type qualifiers permit you to remove operations, with a compile-time guarantee. More generally, type qualifiers permit creating a new supertype, not just a subtype, of an existing Java type.
The Checker Framework is able to verify the correctness of code that the Java type-checker would reject. Here are a few examples.
• It uses a dataflow analysis to determine a more precise type for variables after conditional tests or assignments.
• It treats certain Java constructs more precisely, such as reflection (see Chapter 26).
• It includes special-case logic for type-checking specific methods, such as the Nullness Checker’s treatment of Map.get.
You can add type annotations to just part of your code, and suppress warnings at entry points to the annotated portion. By contrast, using a new Java type requires using it everywhere or writing conversion routines at every entry point.
Type qualifiers have no run-time representation. Therefore, there is no space overhead for separate classes or for wrapper classes for primitives. There is no run-time overhead due to extra dereferences or dynamic dispatch for methods that could otherwise be statically dispatched.
The programmer does not have to convert primitive types to wrappers, which would make the code both uglier and slower. Thanks to defaults and type refinement (Section 33.5), you may be able to write and think in terms of the original Java type, rather than having to explicitly write one of the subtypes in all locations.
See Section 2.4.2.
You should start with a property that matters to you. Think about what aspects of your code cause the most errors, or cost the most time during maintenance, or are most often incorrectly documented. Focusing on what you care about will give you the best benefits.
When you first start out with the Checker Framework, it’s usually best to get experience with an existing type-checker before you write your own new checker.
Many users are tempted to start with the Nullness Checker (see Chapter 3), since null pointer errors are common and familiar. The Nullness Checker works very well, but be warned of three facts that make the absence of null pointer exceptions challenging to verify.
1. Dereferences happen throughout your codebase, so there are a lot of potential problems. By contrast, fewer lines of code are related to locking, regular expressions, etc., so those properties are easier to check.
2. Programmers use null for many different purposes. More seriously, programmers write run-time tests against null, and those are difficult for any static analysis to capture.
3. The Nullness Checker interacts with initialization and map keys.
If null pointer exceptions are most important to you, then by all means use the Nullness Checker. But if you just want to try some type-checker, there are others that are easier to use.
We do not recommend indiscriminately running all the checkers on your code. The reason is that each one has a cost — not just at compile time, but also in terms of code clutter and human time to maintain the annotations. If the property is important to you, is difficult for people to reason about, or has caused problems in the past, then you should run that checker. For other properties, the benefits may not repay the effort. You will be the best judge of this for your own code, of course.
Some of the third-party checkers (see Chapter 31) have known bugs that limit their usability. (Report the ones that affect you, so the developers will prioritize fixing them.)
The checker-framework-dev@googlegroups.com mailing list is for Checker Framework developers. Anyone is welcome to join checker-framework-dev, after they
have had several pull requests accepted.
Anyone is welcome to send mail to the checker-framework-dev@googlegroups.com mailing list — for implementation details it is generally a better place for discussions than the general checker-framework-discuss@googlegroups.com mailing list.
Anyone is welcome to join checker-framework-discuss@googlegroups.com and send mail to it. This list is for user-focused discussions. It is not for submitting bug reports,
which should use the issue tracker (Section 41.2).
The papers “Practical pluggable types for Java” [PAC+08] and “Building and using pluggable type-checkers” [DDE+11] discuss case studies in which programmers found type annotations to be natural to read and write. The code continued to feel like Java, and the type-checking errors were easy to comprehend and often led to real bugs.
You don’t have to take our word for it, though. You can try the Checker Framework for yourself.
The difficulty of adding and verifying annotations depends on your program. If your program is well-designed and -documented, then skimming the existing documentation and writing type annotations is extremely easy. Otherwise, you may find yourself spending a lot of time trying to understand, reverse-engineer, or fix bugs in your program, and then just a moment writing a type annotation that describes what you discovered. This process inevitably improves your code. You must decide whether it is a good use of your time. For code that is not causing trouble now and is unlikely to do so in the future (the code is bug-free, and you do not anticipate changing it or using it in new contexts), then the effort of writing type annotations for it may not be justified.
In summary: annotations do not clutter code; they are used much less frequently than generic types, which Java programmers find acceptable; and they reduce the overall volume of documentation that a codebase needs.
As with any language feature, it is possible to write ugly code that over-uses annotations. However, in normal use, very few annotations need to be written. Figure 1 of the paper “Practical pluggable types for Java” [PAC+08] reports data for over 350,000 lines of type-annotated code:
• 1 annotation per 62 lines for nullness annotations (@NonNull, @Nullable, etc.)
• 1 annotation per 1736 lines for interning annotations (@Interned)
These numbers are for annotating existing code. New code that is written with the type annotation system in mind is cleaner and more correct, so it requires even fewer annotations.
Each annotation that a programmer writes replaces a sentence or phrase of English descriptive text that would otherwise have been written in the Javadoc. So, use of annotations actually reduces the overall size of the documentation, at the same time as making it machine-processable and less ambiguous.
Using the Checker Framework has no impact on the execution of your program: the javac compiler emits identical bytecodes whether or not the Checker Framework is used, so there is no run-time effect. Because there is no run-time representation of type qualifiers, there is no way to use reflection to query the qualifier on a given object, though you can use reflection to examine a class/method/field declaration.
Using the Checker Framework does increase compilation time. It can increase the compilation time by 2–10 times — or more, if you run many pluggable type-checkers at once. For workarounds, see Section 40.9.5.
The compile options to javac can be long to type; for example, javac -processor org.checkerframework.checker.nullness.NullnessChecker .... You can use shorthand for built-in checkers, such as javac -processor nullness ... (see Section 2.2.4), or you can use auto-discovery to eliminate the need for the -processor command-line option (see Section 2.2.3).
Some people go further and say that pre-condition contracts make no sense for any method. This objection is sometimes stated as, “A method parameter should never be annotated as @NonNull. A client could pass any value at all, so the method implementation cannot depend on the value being
non-null. Furthermore, if a client passes an illegal value, it is the method’s responsibility to immediately tell the client about the illegal value.”
Here is an example that invalidates this general argument. Consider a binary search routine. Its specification requires that clients pass in a sorted array.
/** Return index of the search key, if it is contained in the sorted array a; otherwise ... */
int binarySearch(Object @Sorted [] a, Object key)
The binarySearch routine is fast — it runs in O(log n) time where n is the length of the array. If the routine had to validate that its input array is sorted, then it would run in O(n) time, negating all benefit of binary search. In other words, binarySearch should not validate its
input!
The nature of a contract is that if the caller violates its responsibilities by passing bad values, then the callee is absolved of its responsibilities. It is polite for the callee to try to provide a useful diagnostic to the misbehaving caller (for example, by raising a particular exception quickly), but it is not required. In such a situation, the callee has the flexibility to do anything that is convenient.
In some cases, a routine has a complete specification: the contract permits the caller to pass any value, and the callee is required to throw particular exceptions for particular inputs. This approach is common for public methods, but it is not required and is not always the right thing. As explained in Section 2.4.3, even when a method has a complete specification, the annotations should indicate normal behavior: behavior that will avoid exceptions.
For a discussion of this issue, see Section 2.4.5.
Suppose a checker issues a warning about a line of code. One way to eliminate a warning is to perform a run-time test (Section 33.7.4), such as adding if (x != null) before a
dereference of x to avoid a warning about a potential null pointer dereference. However, sometimes the checker issues a warning even though the code contains a run-time test. Two common reasons are non-determinism in the expression being tested and side effects to the expression after the run-time
test. For details and examples, see Section 33.7.5.
Read the error message first; sometimes that is enough to clarify it.
Search through this manual for the text of the warning message or for words that appear in it.
If nothing else explains it, then open an issue (Section 41.2). Be sure to say what you think it means or what specific part does not make sense to you, and what you have already done to try to understand it.
In a message like this:
found : ? extends T extends @UnknownKeyFor Object
required: [extends @UnknownKeyFor Object super @UnknownKeyFor null]
the square brackets enclose the upper and lower bounds that the type parameter needs to be within.
Each checker looks for certain errors. You can use multiple checkers to detect more errors in your code, but you will never have a guarantee that your code is completely bug-free.
If the type-checker issues no warning, then you have a guarantee that your code is free of some particular error. There are some limitations to the guarantee.
Most importantly, if you run a pluggable checker on only part of a program, then you only get a guarantee that those parts of the program are error-free. For example, if your code uses a library that has not been type-checked, then the library might be incorrect, or your code might misuse the library. As another example, suppose you have type-checked a framework that clients are intended to extend. You should recommend that clients run the pluggable checker. There is no way to force users to do so, so you may want to retain dynamic checks or use other mechanisms to detect errors.
Section 2.3 states other limitations to a checker’s guarantee, such as regarding concurrency. Java’s type system is also unsound in certain situations, such as for arrays and casts (however, the Checker Framework is sound for arrays and casts). Java uses dynamic checks in some places where it is unsound, so that errors are thrown at run time. The pluggable type-checkers do not currently have built-in dynamic checkers to check for the places they are unsound. Writing dynamic checkers would be an interesting and valuable project.
Other types of dynamism in a Java application do not jeopardize the guarantee, because the type-checker is conservative. For example, at a method call, dynamic dispatch chooses some implementation of the method, but it is impossible to know at compile time which one it will be. The type-checker gives a guarantee no matter what implementation of the method is invoked.
Even if a pluggable checker cannot give an ironclad guarantee of correctness, it is still useful. It can find errors, exclude certain types of possible problems (e.g., restricting the possible class of problems), improve documentation, and increase confidence in your software.
The Lock Checker (see Chapter 10) offers a way to detect and prevent certain concurrency errors.
By default, the Checker Framework assumes that the code that it is checking is sequential: that is, there are no concurrent accesses from another thread. This means that the Checker Framework is unsound for concurrent code, in the sense that it may fail to issue a warning about errors that occur only when the code is running in a concurrent setting. For example, the Nullness Checker issues no warning for this code:
if (myobject.myfield != null) {
myobject.myfield.toString();
}
This code is safe when run on its own. However, in the presence of multithreading, the call to toString may fail because another thread may set myobject.myfield to null after the nullness check in the if condition, but before the if body is
executed.
If you supply the -AconcurrentSemantics command-line option, then the Checker Framework assumes that any field can be changed at any time. This limits the amount of type refinement (Section 33.7) that the Checker Framework can do.
Section 2.2 describes the -Awarns command-line option that turns checker errors into warnings, so type-checking errors will not cause javac to exit with a failure status.
By default, javac only reports the first 100 errors or warnings. Furthermore, once javac encounters an error, it doesn’t try compiling any more files (but does complete compilation of all the ones that it has started so far).
To see more than 100 errors or warnings, use the javac options -Xmaxerrs and -Xmaxwarns. To convert Checker Framework errors into warnings so that javac will process all your source files, use the option -Awarns. See Section 2.2 for more details.
Sometimes, a Checker Framework warning message will mention a type you have not written in your program. This is typically because a default has been applied where you did not write a type; see Section 33.5. In other cases, this is because type refinement has given an expression a more specific type than you wrote or than was defaulted; see Section 33.7. Note that an invocation of an impure method may cause the loss of all information that was determined via type refinement; see Section 33.7.5.
Sometimes, the Checker Framework permits code on one line, but rejects the same code a few lines later:
if (myField != null) {
myField.hashCode(); // no warning
someMethod();
myField.hashCode(); // warning about potential NullPointerException
}
The reason is explained in the section on type refinement (Section 33.7), which also tells how to specify the side effects of someMethod (Section 33.7.5).
Some properties are not checked statically (see Chapter 34 for reasons that code might not be statically checked). In such cases, it would be desirable to check the property dynamically, at run time. Currently, the Checker Framework has no support for adding code to perform run-time checking.
Adding such support would be an interesting and valuable project. An example would be an option that causes the Checker Framework to automatically insert a run-time check anywhere that static checking is suppressed. If you are able to add run-time verification functionality, we would gladly welcome it as a contribution to the Checker Framework.
Some checkers have library methods that you can explicitly insert in your source code. Examples include the Nullness Checker’s NullnessUtil.castNonNull method (see Section 3.4.1) and the Regex Checker’s RegexUtil class (see Section 14.2.4). But, it would be better to have more general support that does not require the user to explicitly insert method calls.
A “false positive” is when the tool reports a potential problem, but the code is actually correct and will never violate the given property at run time.
The Checker Framework aims to be sound; that is, if the Checker Framework does not report any possible errors, then your code is correct.
Every sound tool suffers false positive errors. Wherever the Checker Framework issues an error, you can think of it as saying, “I can’t prove this code is safe”, but the code might be safe for some complex, tricky reason that is beyond the capabilities of its analysis.
If you are sure that the warning is a false positive, you have several options. Perhaps you just need to write annotations, especially on method signatures but perhaps within method bodies as well. Sometimes you can rewrite the code in a clearer way that the Checker Framework can verify, and that might be easier for people to understand, too. If these don’t work, then you can suppress the warning (Section 2.4.5). You also might want to report the false positive in the Checker Framework issue tracker (Section 41.2), if it appears in real-world, well-written code. Finally, you could improve the Checker Framework to make it more precise, so that it does not suffer that false positive (see Section 40.5.2).
As noted in Section 40.5.1, every sound analysis tool suffers false positives.
For any given false positive warning, it is theoretically possible to improve the Checker Framework to eliminate it. (But, it’s theoretically impossible to eliminate all false positives. That is, there will always exist some programs that don’t go wrong at run time but for which the Checker Framework issues a warning.)
Some improvements affect the implementation of the type system; they do not add any new types. Such an improvement is invisible to users, except that the users suffer fewer false positive warnings. This type of improvement to the type checker’s implementation is often worthwhile.
Other improvements change the type system or add a new type system. Defining new types is a powerful way to improve precision, but it is costly too. A simpler type system is easier for users to understand, less likely to contain bugs, and more efficient.
By design, each type system in the Checker Framework has limited expressiveness. Our goal is to implement enough functionality to handle common, well-written real-world code, not to cover every possible situation.
When reporting bugs, please focus on realistic scenarios. We are sure that you can make up artificial code that stymies the type-checker! Those bugs are not a good use of your time to report, nor of the maintainers’ time to evaluate and fix. When reporting a bug, it’s very helpful to minimize it to give a tiny example that is easy to evaluate and fix, but please also indicate how it arises in real-world, well-written code.
Consider the following code. A programmer can tell that all three invocations of format are safe — they never suffer an IllegalFormatException exception at run time:
class MyClass {
final String field = "%d";
String method() {
return "%d";
}
void m() {
String local = "%d";
String.format(local, 5); // Format String Checker verifies the call is safe
String.format(field, 5); // Format String Checker warns the call might not be safe
String.format(method(), 5); // Format String Checker warns the call might not be safe
}
}
However, the Format String Checker can only verify the first call. It issues a false positive warning about the second and third calls.
The Checker Framework can verify all three calls, with no false positive warnings, if you annotate the type of field and the return type of method as @Format(INT).
By default, the Checker Framework infers types for local variables (Section 33.7), but not for fields and method return types. (The Checker Framework includes a whole-program type inference tool that infers field and method return types; see Section 35.2.) There are several reasons for this design choice.
The designer of an API makes certain promises to clients; these are codified in the API’s specification or contract. The implementation might return a more specific type today, but the designer does not want clients to depend on that. For example, a string might happen to be a regular expression because it contains no characters with special meaning in regexes, but that is not guaranteed to always be true. It’s better for the programmer to explicitly write the intended specification.
To infer types for a non-final method, it is necessary to examine every overriding implementation, so that the method’s return type annotation is compatible with all values that are returned by any overriding implementation. In general, examining all implementations is impossible, because clients may override the method. When possible, it is inconvenient to provide all that source code, and it would slow down the type-checker.
A related issue is that determining which values can be returned by a method m requires analyzing m’s body, which requires analyzing all the methods called by m, and so forth. This quickly devolves to analyzing the whole program. Determining all possible values assigned to a field is equally hard.
Type-checking is modular — it works on one procedure at a time, examining that procedure and the specifications (not implementations) of methods that it calls. Therefore, type-checking is fast and can work on partial programs. The Checker Framework performs modular type-checking, not a whole-program analysis.
When the compiler is called on class Client and class Library, the programmer has no control over which class is analyzed first. When the first class is compiled, it has access only to the signature of the other class. Therefore, a programmer would see inconsistent results depending on
whether Client was compiled first and had access only to the declared types of Library, or the Library was compiled first and the compiler refined the types of its methods and fields before Client looked them up.
The .class files produced with or without pluggable type-checking should specify the same types for all public fields and methods. If pluggable type-checking changed those types, then users would be confused. Depending on how a library was compiled, pluggable type-checking of a client program
would give different results.
Java permits you to initialize an instance field either in the constructor or in a field initializer. The Checker Framework behaves as if the field initializer assignments are performed at the beginning of the constructor (after superclass construction), because that is how Java executes the program.
Here is an example:
class MyClass1 {
@Nullable Object field;
MyClass1() {
field = new Object();
field.toString(); // no possible NullPointerException
}
}
class MyClass2 {
@Nullable Object field = new Object(); // Same initialization as for MyClass1
MyClass2() {
field.toString(); // no possible NullPointerException
}
}
class MyClass3 {
@Nullable Object field;
void myMethod() {
field.toString(); // Nullness Checker warns: possible NullPointerException
}
}
For consistency, the Checker Framework treats the MyClass1 and MyClass2 constructors the same.
The Checker Framework estimates the possible run-time value of each variable, as expressed in a type system. In general, the Checker Framework does not estimate relationships between two variables, except for specific relationships listed in Section 33.8.
For example, the Checker Framework does not track which variables are equal to one another. The Nullness Checker issues a warning, “dereference of possibly-null reference y”, for expression y.toString():
void nullnessExample1(@Nullable Object x) {
Object y = x;
if (x != null) {
System.out.println(y.toString());
}
}
Code that checks one variable and then uses a different variable is confusing and is often considered poor style.
The Nullness Checker is able to verify the correctness of a small variant of the program, thanks to type refinement (Section 33.7):
void nullnessExample2(@Nullable Object x) {
if (x != null) {
Object y = x;
System.out.println(y.toString());
}
}
The difference is that in the first example, nothing was known about x at the time y was set to it, and so the Nullness Checker recorded no facts about y. In the second example, the Nullness Checker knew that x was non-null when y was assigned
to it.
In the future, the Checker Framework could be enriched by tracking which variables are equal to one another, a technique called “copy propagation”.
This would handle the above examples, but wouldn’t handle other examples. For example, the following code is safe:
void requiresPositive(@Positive int arg) {}
void intExample1(int x) {
int y = x*x;
if (x > 0) {
requiresPositive(y);
}
}
void intExample2(int x) {
int y = x*x;
if (y > 0) {
requiresPositive(x);
}
}
However, the Index Checker (Chapter 11), which defines the @Positive type qualifier, issues warnings saying that it cannot prove that the arguments are @Positive.
A slight variant of intExample1 can be verified:
void intExample1a(int x) {
if (x > 0) {
int y = x*x;
requiresPositive(y);
}
}
No variant of intExample2 can be verified. It is not worthwhile to make the Checker Framework more complex and slow by tracking rich properties such as arbitrary arithmetic.
As another example of a false positive warning due to arbitrary arithmetic properties, consider the following code:
void falsePositive2(int arg) {
Object o;
if (arg * arg >= arg) { // always true!
o = new Object();
}
o.toString(); // Nullness Checker issues a false positive warning
}
The Checker Framework is not path-sensitive. That is, it maintains one estimate for each variable, and it assumes at every branch (such as if statement) that every choice could be taken.
In the following code, there are two if statements.
void falsePositive1(boolean b) {
Object o;
if (b) {
o = new Object();
}
if (b) {
o.toString(); // Nullness Checker issues a false positive warning
}
}
In general, if code has two if statements in succession, then there are 4 possible paths through the code: [true, true], [true, false], [false, true], and [false, false]. However, for this code only two of those paths are feasible: namely, [true, true] and [false, false].
The Checker Framework is not path-sensitive, so it issues a warning.
The lack of path-sensitivity can be viewed as a special case of the fact that the Checker Framework maintains a single estimate for each variable value, rather than tracking relationships between multiple variables (Section 40.5.5).
Making the Checker Framework path-sensitive would make it more powerful, but also much more complex and much slower. We have not yet found this necessary.
There is also a separate FAQ for the type annotations syntax (https://checkerframework.org/jsr308/jsr308-faq.html).
The receiver of a method is the this formal parameter, sometimes also called the “current object”. Within the method declaration, this is used to refer to the receiver formal parameter. At a method call, the receiver actual argument is written before a period and the method
name.
The method compareTo takes two formal parameters. At a call site like x.compareTo(y), the two arguments are x and y. It is desirable to be able to annotate the types of both of the formal parameters, and doing so is supported by both Java’s type
annotations syntax and by the Checker Framework.
A type annotation on the receiver is treated exactly like a type annotation on any other formal parameter. At each call site, the type of the argument must be consistent with (a subtype of or equal to) the declaration of the corresponding formal parameter. If not, the type-checker issues a warning.
Here is an example. Suppose that @A Object is a supertype of @B Object in the following declaration:
class MyClass {
void requiresA(@A MyClass this) { ... }
void requiresB(@B MyClass this) { ... }
}
Then the behavior of four different invocations is as follows:
@A MyClass myA = ...;
@B MyClass myB = ...;
myA.requiresA() // OK
myA.requiresB() // compile-time error
myB.requiresA() // OK
myB.requiresB() // OK
The invocation myA.requiresB() does not type-check because the actual argument’s type is not a subtype of the formal parameter’s type.
A top-level constructor does not have a receiver. An inner class constructor does have a receiver, whose type is the same as the containing outer class. The receiver is distinct from the object being constructed. In a method of a top-level class, the receiver is named this. In a constructor of an inner class,
the receiver is named Outer.this and the result is named this.
A method in an anonymous class has a receiver, but it is not possible to write the receiver in the formal parameter list because there is no name for the type of this.
@NonNull Object @Nullable?
In a type such as @NonNull Object @Nullable [], it may appear that the @Nullable annotation is written after the type Object. In fact, @Nullable modifies []. See the next FAQ, about array annotations (Section 40.6.3).
@NonNull Object @Nullable []?
You should parse this as: (@NonNull Object) (@Nullable []). Each annotation precedes the component of the type that it qualifies.
Thus, @NonNull Object @Nullable [] is a possibly-null array of non-null objects. Note that the first token in the type, “@NonNull”, applies to the element type Object, not to the array type as a whole. The annotation @Nullable applies to the array
([]).
Similarly, @Nullable Object @NonNull [] is a non-null array of possibly-null objects.
Some older tools have inconsistent semantics for annotations on array and varargs elements. Their semantics is unfortunate and confusing; developers should convert their code to use type annotations instead. Section 40.6.10 explains how the Checker Framework handles declaration annotations in the meantime.
@English String @NonEmpty ...?
Varargs annotations are treated similarly to array annotations. (A way to remember this is that when you write a varargs formal parameter such as void method(String... x) , the Java compiler generates a method that takes an array of strings; whenever your source
code calls the method with multiple arguments, the Java compiler packages them up into an array before calling the method.)
{}
Either of these annotations
void method(String @NonEmpty [] x) {}
void method(String @NonEmpty ... x) {}
applies to the array: the method takes a non-empty array of strings, or the varargs list must not be empty.
Either of these annotations
void method(@English String [] x) {}
void method(@English String ... x) {}
applies to the element type. The annotation documents that the method takes an array of English strings.
See Section 33.3.
See Section 32.1.2.
It is bad style for an annotation to apply to both types and declarations. In other words, every annotation should have a @Target meta-annotation, and the @Target meta-annotation should list either only declaration locations or only type annotations. (It’s OK for an annotation to target
both ElementType.TYPE_PARAMETER and ElementType.TYPE_USE, but no other declaration location along with ElementType.TYPE_USE.)
Sometimes, it may seem tempting for an annotation to apply to both type uses and (say) method declarations. Here is a hypothetical example:
“Each
Widgettype may have a@Versionannotation. I wish to prove that versions of widgets don’t get assigned to incompatible variables, and that older code does not call newer code (to avoid problems when backporting).A
@Versionannotation could be written like so:@Version("2.0") Widget createWidget(String value) { ... }
@Version("2.0")on the method could mean that thecreateWidgetmethod only appears in the 2.0 version.@Version("2.0")on the return type could mean that the returnedWidgetshould only be used by code that uses the 2.0 API ofWidget. It should be possible to specify these independently, such as a 2.0 method that returns a value that allows the 1.0 API method invocations.”
Both of these are type properties and should be specified with type annotations. No method annotation is necessary or desirable. The best way to require that the receiver has a certain property is to use a type annotation on the receiver of the method. (Slightly more formally, the property being checked is compatibility between the annotation on the type of the formal parameter receiver and the annotation on the type of the actual receiver.) If you do not know what “receiver” means, see Section 40.6.1.
Another example of a type-and-declaration annotation that represents poor design is JCIP’s @GuardedBy annotation [GPB+06]. As discussed in Section 10.6.1, it means two different things when
applied to a field or a method. To reduce confusion and increase expressiveness, the Lock Checker (see Chapter 10) uses the @Holding annotation for one of these meanings, rather than overloading @GuardedBy with
two distinct meanings.
A final example is @Nullable and @NonNull annotations that are intended to work both with modern tools that process type annotations and with old tools that were written before Java had type annotations. Such type-and-declaration annotations were a temporary measure, intended to be
used until the tool supported Java 8 (which was released in March 2014), and should not be necessary any longer.
If you write a fully-qualified type name in your program, then the Java language requires you to write a type annotation on the simple name part, such as
entity.hibernate. @Nullable User x;
If you try to write the type annotation before the entire fully-qualified name, such as
@Nullable entity.hibernate.User x; // illegal Java syntax
then you will get an error like one of the following:
error: scoping construct for static nested type cannot be annotated error: scoping construct cannot be annotated with type-use annotation
Java has two distinct varieties of annotation: type annotations and declaration annotations.
A type annotation can be written on any use of a type. It conceptually creates a new, more specific type. That is, it describes what values the type represents.
As an example, the int type contains these values: ..., -2, -1, 0, 1, 2, ...
The @Positive int type contains these values: 1, 2, ...
Therefore, @Positive int is a subtype of int.
A declaration annotation can be written on any declaration (a class, method, or variable). It describes the thing being declared, but does not describe run-time values. Here are examples of declaration annotations:
@Deprecated // programmers should not use this class
class MyClass { ... }
@Override // this method overrides a method in a supertype
void myMethod() { ... }
@SuppressWarnings(...) // compiler should not warn about the initialization expression
int myField = INITIALIZATION-EXPRESSION;
Here are examples that use both a declaration annotation and a type annotation:
@Override
@Regex String getPattern() { ... }
@GuardedBy("myLock")
@NonNull String myField;
Note that the type annotation describes the value, and the declaration annotation says something about the method or use of the field.
As a matter of style, declaration annotations are written on their own line, and type annotations are written directly before the type, on the same line.
The Java Language Specification, section 9.7.4 says: “It is customary, though not required, to write declaration annotations before all other modifiers, and type annotations immediately before the type to which they apply.”
A type annotation should be written immediately before the type it qualifies, on the same line. There should not be any modifiers (such as public) between them. This emphasizes that the type qualifier plus the Java base type is a logical unit, which aids people reading the code.
// Wrong formatting
@Positive
public int numItems;
// Correct formatting
public @Positive int numItems;
// Wrong formatting
@Nullable
public Object getThing() {
...
}
// Correct formatting
public @Nullable Object getThing() {
...
}
By contrast, declaration annotations are conventionally written on their own line.
// Wrong formatting
@Deprecated URL toURL() {
...
}
// Correct formatting
@Deprecated
URL toURL() {
...
}
The preferred order of modifiers is
1. declaration annotations
2. keyword modifiers such as public and strictfp
3. type annotations
4. type
Here is an example of a declaration annotation and a type annotation on a class declaration:
@Deprecated
public @Interned class Level {
...
}
The popular google-java-format tool formats type annotations incorrectly, with type annotations on their own line instead of on the same line as the type they modify. (Actually, you can see from method JavaInputAstVisitor.typeAnnotations() that it handles two of the many
type annotations — @Nullable and @NonNull — correctly, but all other type annotations incorrectly! This would be fixed by merging pull request #802.) Until this bug in
google-java-format is fixed, you have these options:
• Run google-java-format via Spotless and use the formatAnnotations
step to correct the formatting of type annotations.
• Run google-java-format via run-google-java-format.
If you define a new type qualifier — for example, because you are using the Subtyping Checker (Chapter 30) or Fake Enum Checker (Chapter 9), or because you have created a new checker (Chapter 37) — then the above tools will format your new type qualifiers incorrectly, like declaration annotations. Here is how to fix the formatting.
• For Spotless, change your configuration to indicate the new type qualifiers. If you use the Spotless plugin for
Gradle, edit your build.gradle file to change formatAnnotations() to (for example) formatAnnotations().addTypeAnnotation("Growable").addTypeAnnotation("Modifiable")....
• For run-google-java-format, make a pull request to change variable type_annotations in file fixup-google-java-format.py.
When a declaration annotation is an alias for a type annotation, the Checker Framework may move the annotation before replacing it by the canonical version. (If the declaration annotation is in an org.checkerframework package, it is not moved.)
For example,
import android.support.annotation.NonNull;
...
@NonNull Object [] returnsArray();
is treated as if the programmer had written
import org.checkerframework.checker.nullness.qual.NonNull;
...
Object @NonNull [] returnsArray();
because Android’s @NonNull annotation is a declaration annotation, which is understood to apply to the top-level return type of the annotated method.
When possible, you should use type annotations rather than declaration annotations, and write them in the correct location (Section 40.6.10).
Users who are using old Java 5–7 declaration annotations (for instance, from the FindBugs tool, which has not been maintained since 2015, and from its successor SpotBugs, which has not yet adopted type annotations, even though type annotations were added to Java in 2014) can use annotations in package
org.checkerframework.checker.nullness.compatqual to avoid name conflicts. These are available in package checker-compat-qual on Maven Central. Once
users are ready to upgrade to Java 8+ type annotations, those compatibility annotations are no longer necessary.
In order to convert from another tool’s declaration annotations to the Checker Framework’s type annotations, you need to change imports, rename annotations, move annotations written on arrays (see Section 40.6.11), and move annotations to simple type names.
For example, if a user writes
import android.support.annotation.Nullable;
...
@Nullable
public Map.Entry<Object, Object> intersects() { ... }
and then changes the import to org.checkerframework.checker.nullness.qual.Nullable, the code will not compile. (See Section 41.1.3 for more details.) The
user needs to also move the @Nullable annotation to a location where Java permits type annotations:
import org.checkerframework.checker.nullness.qual.Nullable;
...
public Map.@Nullable Entry<Object, Object> intersects() { ... }
Sometimes, your program works in phases that have different behavior. For example, you might have a field that starts out null and becomes non-null at some point during execution, such as after a method is called. You can express this property as follows:
1. Annotate the field type as @MonotonicNonNull.
2. Annotate the method that sets the field as @EnsuresNonNull("myFieldName"). (If method m1 calls
method m2, which actually sets the field, then you would probably write this annotation on both m1 and m2.)
3. Annotate any method that depends on the field being non-null as @RequiresNonNull("myFieldName"). The
type-checker will verify that such a method is only called when the field isn’t null — that is, the method is only called after the setting method.
You can also use a typestate checker (see Section 31.30), but typestate checkers have not been as extensively tested.
The following two bits of code have the same semantics under Java, but are treated differently by the Checker Framework’s CLIMB-to-top defaulting rules (Section 33.5.3):
class MyClass<T> { ... }
class MyClass<T extends Object> { ... }
The difference is the annotation on the upper bound of the type argument T. They are treated in the following way.
class MyClass<T> == class MyClass<T extends @TOPTYPEANNO Object> class MyClass<T extends Object> == class MyClass<T extends @DEFAULTANNO Object>
@TOPTYPEANNO is the top annotation in the type qualifier hierarchy. For example, for the nullness type system, the top type annotation is @Nullable, as shown in Figure 3.1.
@DEFAULTANNO is the default annotation for the type system. For example, for the nullness type system, the default type annotation is @NonNull.
In some type systems, the top qualifier and the default are the same. For such type systems, the two code snippets shown above are treated the same. An example is the regular expression type system; see Figure 14.1.
The CLIMB-to-top rule reduces the code edits required to annotate an existing program, and it treats types written in the program consistently.
When a user writes no upper bound, as in class C<T> , then Java permits the class to be instantiated with any type parameter. The Checker Framework behaves exactly the same, no matter what the default is for a particular type system — and no matter
whether the user has changed the default locally.
{ ... }
When a user writes an upper bound, as in class C<T extends OtherClass> , then the Checker Framework treats this occurrence of { ... }OtherClass exactly like any other occurrence, and applies the usual defaulting rules. Use of
Object is treated consistently with all other types in this location and all other occurrences of Object in the program.
Here are some style guidelines:
• Omit the extends clause when possible. To indicate no constraints on type qualifiers, write class MyClass<T> rather than class MyClass<T extends @TOPTYPEANNO Object>.
• When you write an Object upper bound, give an explicit type annotation. That is, write class C<T extends @DEFAULTANNO Object> even though it is equivalent to writing { ... }class C<T extends Object> .
{ ...
}
If you write just extends Object, then someone who is reading the code might think that it is irrelevant (which it is in plain Java). Also, some IDEs will suggest removing it.
Suppose unannotated code contains a declaration of a type parameter <T>. How should you annotate that declaration?
This is really a question about Java’s generic types, so if you understand Java generics, this question is moot. However, Java generics can be hard to understand, so here is a brief explanation of some concrete annotations, using nullness annotations for concreteness.
<T>
Any type argument may be supplied for T.
It is equivalent to <T extends @Nullable Object>, because @Nullable Object is the top type in the type hierarchy.
<T extends @Nullable Object>
Any type argument may be supplied for T.
It is equivalent to <T>, as noted above.
<T extends Object>
T can be instantiated by any type whose qualifier is @NonNull.
The default annotation is @NonNull, and annotation defaults apply to type uses such as Object but not to type variables such as T. Therefore, <T extends Object> is equivalent to <T extends @NonNull Object>. It permits any type
argument that is a subtype of @NonNull Object, which is any type argument whose qualifier is @NonNull, since @NonNull is the bottom type qualifier in the type qualifier hierarchy.
<T extends @NonNull Object>
T can be instantiated by any type whose qualifier is @NonNull.
It is equivalent to <T extends Object>, as noted above.
<@Nullable T>
T can be instantiated by any type whose qualifier is @Nullable.
The annotation @Nullable before T applies to T’s implicit lower bound. There is no explicit upper bound (that is, no extends), so the upper bound is the top type, @Nullable Object, just as for <T>, which was discussed above.
Therefore, <@Nullable T> is the same as <T super @Nullable void extends @Nullable Object>, except that the latter is not legal Java.
<T super @Nullable String>
T can be instantiated by any supertype of @Nullable String, which is any supertype of String (Object, Serializable, CharSequence, etc.) so long as its type qualifier is @Nullable.
<T super @NonNull String>
T can be instantiated by any supertype of @NonNull String. Since @NonNull is the bottom type qualifier, the instantiating type can have any type qualifier.
For more details about how the Checker Framework supports generics and polymorphism, see Chapter 32.
@Retention(RetentionPolicy.RUNTIME)?
Annotations such as @NonNull are declared with @Retention(RetentionPolicy.RUNTIME)assert statement), type-check dynamically-loaded code, check casts and instanceof operations, resolve reflection more precisely, or other tasks that we have not yet thought of. Not many such tools exist today, but the annotation designers wanted to
accommodate them in the future.
RUNTIME retention has negligible costs (no run-time dependency, minimal increase in heap size). To avoid these costs, a project can use the checker-qual-android dependency; as explained in Section 39.1, it is identical to checker-qual, except that in checker-qual-android annotations have CLASS retention.
For the purpose of static checking at compile time, CLASS retention is sufficient. Note that SOURCE retention would not be sufficient, because of separate compilation: when type-checking a class, the compiler needs
to read the annotations on libraries that it uses, and separately-compiled libraries are available to the compiler only as class files.
In addition to using the checkers that are distributed with the Checker Framework, you can write your own checker to check specific properties that you care about. Thus, you can find and prevent the bugs that are most important to you.
Chapter 37 gives complete details regarding how to write a checker. It also suggests places to look for more help, such as the Checker Framework API documentation (Javadoc) and the source code of the distributed checkers.
To whet your interest and demonstrate how easy it is to get started, here is an example of a complete, useful type-checker.
@SubtypeOf(Unqualified.class)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface Encrypted {}
Section 30.2 explains this checker and tells you how to run it.
In theory, any property about a program can be expressed and checked within a type system. In practice, types are a good choice for some properties and a bad choice for others.
A type expresses the set of possible values for an expression. Therefore, types are a good choice for any property that is about variable values or provenance.
Types are a poor choice for expressing properties about timing, such as that action B will happen within 10 milliseconds of action A. Types are not good for verifying the results of calculations; for example, they could ensure that code always calls an encrypt routine in the appropriate places, but not
that the encrypt routine is correctly implemented. Types are not a good solution for preventing infinite loops, except perhaps in special cases.
A type system implementer can declaratively specify the type qualifier hierarchy (Section 37.5.2) and the type introduction rules (Section 37.8). However, the Checker Framework uses a procedural syntax for specifying type-checking rules (Section 37.7). A declarative syntax might be more concise, more readable, and more verifiable than a procedural syntax.
We have not found the procedural syntax to be the most important impediment to writing a checker.
Previous attempts to devise a declarative syntax for realistic type systems have failed; see a technical paper [PAC+08] for a discussion. When an adequate syntax exists, then the Checker Framework can be extended to support it.
The Checker Framework enables you to define a new type system. It finds errors, or guarantees their absence, by performing type-checking that is similar to that already performed by the Java compiler.
Type-checking examines each statement of your program in turn, one at a time.
• Expressions are processed bottom-up. Given types for each sub-expression, the type-checker determines whether the types are legal for the expression’s operator and determines the type of the expression.
• An assignment is legal if the type of the right-hand side is a subtype of the declared type of the left-hand side.
• At a method call, the arguments are legal if they can be assigned to the formal parameters (this is called a “pseudo-assignment” and it follows the normal rules for assignment). The type of the method call is the declared type of the return type, where the method is declared. If the method declaration is not annotated, then a default annotation is used.
• Suppose that method Sub.m overrides method Super.m. The return type of Sub.m must be equal to or a subtype of the return type of Super.m (this is called “covariance”). The type of formal parameter i of Sub.m must be equal to or a
supertype of the type of formal parameter i in Super.m (this is called “contravariance”).
Suppose that you distribute a library, which contains Checker Framework annotations such as @Nullable. This enables clients of the library to use the Checker Framework to type-check their programs. To do so, they must have the Checker Framework annotations on their classpath, for instance by
using the Checker Framework Compiler.
Clients who do not wish to perform pluggable type-checking do not need to have the Checker Framework annotations (checker-qual.jar) in their classpath, either when compiling or running their programs.
The JVM does not issue a link error if an annotation is not found when a class is loaded. (By contrast, the JVM does issue a link error if a superclass, or a parameter/return/field type, is not found.) Likewise, there is no problem compiling against a library even if the library’s annotations are not on the classpath. These are properties of Java, and are not specific to the Checker Framework’s annotations.
.class files contain more annotations than the source code?
A .class file contains an annotation on every type, as computed by defaulting rules; see Section 33.4.
When an overridden method has a side effect annotation, the overriding method must have one too. However, if the side effect annotation is declared with the @InheritedAnnotation meta-annotation, the Checker Framework automatically adds the missing annotation. This is the case for most side effect annotations — these annotations are propagated from annotated libraries, such as the JDK, to your code.
It is possible to annotate exception types, and any type-checker built on the Checker Framework enforces that type annotations are consistent between throw statements and catch clauses that might catch them.
The Java compiler already enforces that all checked exceptions are caught or are declared to be passed through, so you would use annotations to express other properties about exceptions.
Checked exceptions are an example of a “type and effect” system, which is like a type system but also accounts for actions/behaviors such as side effects. The GUI Effect Checker (Chapter 19) is a type-and-effect system that is distributed with the Checker Framework.
Using a pluggable type-checker increases compile times by a factor of 2–10. Slow compilation speed is probably the worst thing about the Checker Framework.
To improve performance:
• Ensure that the Checker Framework has enough memory. The Checker Framework uses more memory than javac does, and Java’s default heap limit is so small that the Checker Framework might spend most of its time in garbage collection. (If this is the case, the Checker Framework will issue a
warning “Garbage collection consumed over 25% of CPU during the past minute.”) To permit the Checker Framework to use up to 4 GB of memory, pass an argument like -Xmx4g or set an environment variable like export _JAVA_OPTIONS=-Xmx4g. Also consider upgrading to a more
recent release of Java, because older versions of Java have worse memory management.
• Set your build system to perform incremental compilation. When compiling just a few source files (the size of a typical edit or commit), you won’t notice the slowdown even if the Checker Framework is very slow. If you compile all files in a large project, you will definitely notice a slowdown. You should structure your build system to make compiling all files rare, by declaring dependencies and using caching. (Note: Maven lacks dependency-driven build and caching. If your project uses Maven, consider switching to a more capable build system such as Gradle.)
• Write generic type arguments. Often, generic type inference is the slowest part of type-checking. You can significantly speed up type-checking by explicitly writing a few generic type arguments. To determine where to write them, temporarily set -AslowTypecheckingSeconds to a small value, such
as 1. Write type arguments where slow.typechecking warnings are issued.
If the Checker Framework is still too slow for you to run on every compilation, you can run it periodically, such as in a Git commit hook or in continuous integration.
The Checker Framework team does not currently have the resources to fix performance problems, but we welcome community contributions.
Here are some reasons that the Checker Framework is slow.
• It has to do all the same work as the compiler does, such as resolving overloading and overriding, inferring generics, and type-checking.
• Its analysis is general; it interprets user-defined type systems whereas javac hard-codes one type system and integrates it with other processing.
• Its analysis is much richer. javac can take certain shortcuts that are not correct for all possible type systems.
• It builds a control flow graph and performs a fixpoint analysis on it, which javac does not do.
• It manipulates multiple representations of data, including javac’s internal representation, source code, control flow graph, and its own internal representation. These transformations and lookups take time.
• It switches between dataflow analysis and type analysis, and this sometimes causes it to redo work.
• When running a compound or aggregate checker, it computes the control flow graph multiple times, and it makes multiple passes over the program rather than just one.
As explained in Section 1.3, a change in the middle number of the Checker Framework version string indicates a possible incompatibility.
Another policy is “semantic versioning” as defined at https://semver.org/. This version number policy, unfortunately, does not define key terms, such as “backwards compatible bug fixes”. It includes an escape hatch, “Semantic Versioning is all about conveying meaning by how the version number changes.” It has not been updated in over a decade (since January 2013), has only ever been updated once (from 1.0.0 to 2.0.0), and has about 100 open issues. It is a proposal, not a standard or an official definition. Projects that claim to follow it often do so loosely.
If the Checker Framework strictly used semver.org’s definition, every release would be a new major version, and the current version string would be past version 200.0.0. Always incrementing the major version number would not convey meaning to its users — for example, it would not indicate major new functionality or important behavior differences.
A pluggable type-checker is a verification tool that prevents or detects all errors of a given variety. If it issues no warnings, your code has no errors of a given variety (for details about the guarantee, see Section 2.3).
An alternate approach is to use a bug detector such as Error Prone, FindBugs [HP04, HSP05], SpotBugs, Jlint [Art01], PMD [Cop05], or the tools built into Eclipse (see Section 40.10.2) and IntelliJ. The NullAway and Eradicate tools are more like sound type-checking than bug detection, but all of those tools accept unsoundness — that is, false negatives or missed warnings — in exchange for analysis speed.
A pluggable type-checker or verifier differs from a bug detector in several ways:
• A type-checker reports all errors in your code. If a type-checker reports no warnings, then you have a guarantee (a proof) of correctness (Section 40.4.5).
A bug detector aims to find some of the most obvious errors. Even if a bug detector reports no warnings, there may still be errors in your code.
• A type-checker requires you to annotate your code with type qualifiers, or to run an inference tool that does so for you. That is, it requires you to write a specification, then it verifies that your code meets its specification.
Some bug detectors do not require annotations. This means that it may be easier to get started running a bug detector. The tool makes guesses about the intended behavior of your code, leading to false alarms or missed alarms.
• A verification tool may issue more warnings for a programmer to investigate. Some bug detectors internally generate many warnings, then use heuristics to discard some of them. The cost is missed alarms, when the tool’s heuristics classified the warnings as likely false positives and discarded them.
• A type-checker uses a more sophisticated and precise analysis. For example, it can take advantage of method annotations and annotations on generic type parameters, such as List<@NonNull String>. An example specific to the Nullness Checker (Chapter 3): no other tool correctly handles map keys or initialization.
A bug detector does a more lightweight analysis. This means that a bug detector usually runs faster, giving feedback to the programmer more rapidly and avoiding slowdowns. Its analysis is often narrow, avoiding properties that are tricky to reason about or that might lead to false alarms. The cost is missed alarms, when analysis is too weak to find the errors.
• Neither type-checking nor bug detection subsumes the other. A type-checker finds problems that a bug detector cannot. A bug detector finds problems that a type-checker does not: there is no need for the type-checker to address style rules, when a bug detector is adequate.
If your code is important to you, it is advantageous to run both types of tools.
For a case study that compared the nullness analysis of FindBugs (equivalent to SpotBugs), Jlint, PMD, and the Checker Framework, see section 6 of the paper “Practical pluggable types for Java” [PAC+08]. The case study was on a well-tested program in daily use. The Checker Framework tool found 8 nullness errors (that is, null pointer dereferences). None of the other tools found any errors. A follow-up 10 years later found that Eclipse’s nullness analysis found 0 of the errors, and IntelliJ’s nullness analyses found 3 of the errors that the Nullness Checker found.
The JSR 308 [Ern08b] documentation also contains a discussion of related work.
Eclipse comes with a null analysis that can detect potential null pointer errors in your code. Eclipse’s built-in analysis differs from the Checker Framework in several respects.
The Checker Framework’s Nullness Checker (see Chapter 3) is more precise: it does a deeper semantic analysis, so it issues fewer false positives than Eclipse. Eclipse’s nullness analysis is missing many features that the Checker Framework supports, such as handling of map keys, partially-initialized objects, method pre- and post-conditions, polymorphism, and a powerful dataflow analysis. These are essential for practical verification of real-world code with good precision. Furthermore, Eclipse by default ignores unannotated code (even unannotated parameters within a method that contains other annotations). As a result, Eclipse is more useful for bug-finding than for verification, and that is what the Eclipse documentation recommends.
Eclipse assumes by default that all code is multi-threaded, which cripples its local type inference. (This default can be turned off, however.) The Checker Framework allows the user to specify whether code will be run concurrently or not via the -AconcurrentSemantics command-line option (see
Section 40.4.6).
The Checker Framework builds on javac, so it is easier to run in integration scripts or in environments where not all developers have installed Eclipse.
Eclipse handles only nullness properties and is not extensible, whereas the Checker Framework comes with over 20 type-checkers (for a list, see Chapter 1) and is extensible to more properties.
There are also some benefits to Eclipse’s null analysis. It is faster than the Checker Framework, in part because it is less featureful. It is built into Eclipse, so you do not have to add it to your build scripts. Its IDE integration is tighter and slicker.
In a case study, the Nullness Checker found 9 errors in a program, and Eclipse’s analysis found 0.
NullAway is a lightweight, unsound type-checker whose aim is similar to that of the Nullness Checker (Chapter 3). For both tools, the user writes nullness annotations, and then the tool checks them.
NullAway is faster than the Nullness Checker and requires fewer annotations.
NullAway is unsound: even if NullAway issues no warnings, your code might crash with a null pointer exception. Two differences are that NullAway makes unchecked assumptions about getter methods, and that NullAway assumes all objects are always fully initialized. NullAway forces all generic arguments to be non-null, which is not an unsoundness but is less flexible than the Nullness Checker.
JSpecify defines the two annotations @NonNull and @Nullable. This is one more possibility in addition to the other definitions of those annotations listed in Section 3.7. JSpecify is not an official
standard.
You can use the JSpecify annotations or the Checker Framework ones, whichever you prefer. All nullness checkers we know of (e.g., Eclipse, EISOP, IntelliJ, NullAway, the Nullness Checker, SpotBugs) recognize the JSpecify and Nullness Checker versions of those two type annotations, so there is no tooling reason to prefer one over the other. JSpecify has only nullness annotations, and none for the dozens of other type-checkers that the Checker Framework supports.
The JSpecify specification language is weaker than what the Nullness Checker supports. For example, JSpecify lacks a polymorphic qualifier such as @PolyNull, and it lacks
method specifications (Section 3.2.2). It lacks annotations for initialization (Section 3.8), but you could consider that a benefit,
if you always suppress all initialization warnings, opting for convenience and simplicity over sound checking. Even if your code does not use all the specification power of the Nullness Checker, you will benefit from expressive specifications on libraries that your code uses.
If you want precise, sound type-checking, you will need to use some Nullness Checker annotations. You can mix two sets of annotations (those of JSpecify and of the Nullness Checker), or you can use just those of the Nullness Checker. Both approaches work.
JSpecify contains a notion of “unspecified nullness”. It is typically used for warning suppression in unannotated code, but doing so has two problems. First, it makes your specification tool-dependent, because a JSpecify-compliant tool may have any behavior (including issuing warnings or not issuing
warnings) for code that uses “unspecified nullness” or uses a library that uses “unspecified nullness”. Second, it mixes notions of nullness specification and warning suppression, which are separate concepts. The Checker Framework has well-defined behavior for all specifications, and it has rich facilities for warning
suppression (Chapter 34). For example, the -AskipUses command-line option (Section 34.4) suppresses warnings relating to
uses of unannotated libraries.
The Checker Framework does not need JSpecify’s @NullMarked, which makes a checker treat unannotated references as @NonNull. The Nullness Checker by default treats unannotated references as @NonNull. The Checker Framework does not need JSpecify’s
@NullUnmarked, which sets the default to “unspecified nullness”. The Nullness Checker supports explicit warning suppressions instead.
The EISOP Checker Framework (also called the EISOP Framework) is a fork of the Checker Framework. The main difference is that the EISOP Nullness Checker supports one interpretation of the full JSpecify “standard” (see Section 40.10.4), whereas the Checker Framework’s Nullness Checker only supports the non-ambiguous parts of JSpecify.
The EISOP Checker Framework is an “unfriendly fork” in that it incorporates improvements from the Checker Framework, but its developers do not contribute back to the Checker Framework: they only incorporate their improvements and bug fixes in their own version. The EISOP Checker Framework has introduced some bugs that do not exist in the Checker Framework, and it has fixed some bugs that exist in the Checker Framework, so neither one is strictly more correct than the other. If you use the EISOP Checker Framework, please encourage its developers to be good open-source citizens and contribute back to the Checker Framework. We wish the EISOP project well, because any project that gets more people to verify their code (by writing nullness specifications and running a checker) is a net positive for the programming community.
Optional type?
JDK 8 introduced the OptionalOptional correctly.
Section 3.7.3 explains the relationship between nullness and Optional and the benefits of each.
JML, the Java Modeling Language [LBR06], is a language for writing formal specifications.
JML aims to be more expressive than pluggable type-checking. A programmer can write a JML specification that describes arbitrary facts about program behavior. Then, the programmer can use formal reasoning or a theorem-proving tool to verify that the code meets the specification. Run-time checking is also possible. By contrast, pluggable type-checking can express a more limited set of properties about your program. Pluggable type-checking annotations are more concise and easier to understand.
JML is not as practical as pluggable type-checking. The JML toolset is less mature. For instance, if your code uses generics or other features of Java 5, then you cannot use JML. However, JML has a run-time checker, which the Checker Framework currently lacks.
The Checker Framework is not an official part of Java. The Checker Framework relies on type annotations, which became part of Java with Java 8 (released in March 2014). For more about type annotations, see the Type Annotations (JSR 308) FAQ.
JSR 305 aimed to define official Java names for some annotations, such as @NonNull and @Nullable. However, it did not aim to precisely define the semantics of those annotations nor to provide a reference implementation of an annotation processor that validated their use; as a result,
JSR 305 was of limited utility as a specification. JSR 305 has been abandoned; there has been no activity by its expert group since 2009.
By contrast, the Checker Framework precisely defines the meaning of a set of annotations and provides powerful type-checkers that validate them. However, the Checker Framework is not an official part of the Java language; it chooses one set of names, but another tool might choose other names.
In the future, the Java Community Process might revitalize JSR 305 or create a replacement JSR to standardize the names and meanings of specific annotations, after there is more experience with their use in practice.
The Checker Framework defines annotations @NonNull and @Nullable that are compatible with annotations defined by JSR 305, SpotBugs, IntelliJ, and other tools; see Section 3.7.
JSR 308, also known as the Type Annotations specification, dictates the syntax of type annotations in Java SE 8: how they are expressed in the Java language.
JSR 308 does not define any type annotations such as @NonNull, and it does not specify the semantics of any annotations. Those tasks are left to third-party tools. The Checker Framework is one such tool.