Checker Framework for pluggable type-checking

Contents:

• Introduction
• Writing specifications
  • Write specifications for the normal (non-exceptional) case
• Dealing with type-checker warnings
  • Suppressing warnings
  • Do not circumvent the type-checker
• Hints
  • Specifying checkRep
  • Is checkRep necessary?
• Who made the Checker Framework?

Introduction

It is better to detect a bug at compile time than at run time. This handout describes the Checker Framework, which creates a type system that is stronger than Java's built-in type system. This helps you to make your code more robust, by preventing even more errors at compile time.

Read chapters 1, 2, 3, and 4. of the Checker Framework Manual. You can skip the installation instructions, because Gradle will automatically download the Checker Framework for you. You may also find the FAQ and the Troubleshooting guide helpful if you have questions. The reading will save you time in the long run. Feel free to ask the staff questions if you don't find your question answered in the documentation.

To compile and test your code without running the Nullness Checker, use ./gradlew build -PnoChecker.

Writing specifications

You will write specifications about the nullness, initialization, and map key properties of your code. There are many other facts about your code that you will not attempt to express. You are only required to express side effect properties to the extent that they are necessary in order to prove facts about nullness, initialization, and map keys.

The Checker Framework does not read your English-language comments, such as "may be null". Instead, you need to add @Nullable to the type of the variable.

The Checker Framework does not know about CSE 331 specifications such as @spec.modifies. To specify that a method has no side effects, annotate it with @SideEffectFree.

Type annotations should be written immediately before a type. For example, do not write @Nullable private String getLabel() {...}. The Java compiler will let you put modifiers such as private in the middle of the type @Nullable String, but doing so is confusing and bad style. Note that method annotations, such as @RequiresNonNull, should be written before visibility modifiers such as private.

Don't forget to add import statements, such as

import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.qual.SideEffectFree;

Do not write extranous annotations. For example, do not write @NonNull in a place where @NonNull is the default. (You do need to write @NonNull on a type variable if you want to override the type argument the client provided, though.) You will be graded down for extraneous annotations.

Write type annotations primarily on method signatures (as specifications). You do not need to write them on local variables within method bodies, but you do need to write them on type argumennts, as in List<@KeyFor("mygraph")> String. Also, you do not need to write type annotations on your tests.

Within a method signature, to refer to a formal parameter, use # followed by the one-based parameter index. For example: #1, #3. Also see section Writing Java expressions in the Checker Framework manual.

Be sure to write a justification for anything you do that suppresses a warning, including @SuppressWarnings, @AssumeAssertion, castNonNull, etc. The justification should explain why the property is definitely true, even though the Nullness Checker cannot verify it.

Write specifications for the normal (non-exceptional) case

Write specifications for the normal (non-exceptional) behavior of your program. That is, write programs that prevent your program from crashing due to (mis)use of null. If your method accepts any argument, but it throws an exception if its argument is null, then the formal parameter should have @NonNull, not @NonNull, type. That way, the Nullness Checker will warn if a client supplies a value that would lead to a crash.

Dealing with type-checker warnings

If the type-checker issues a warning, here are some possible reasons why.

• Your code can throw a null pointer exception. Fix the bug.
• Your code is not consistent with its specification (the annotations). You might need to change the code or change the specification.
• Your code does not suffer a null pointer exception, but the annotations are not sufficient to prove that fact. You might need to add annotations, either at the location of the reported warnings or elsewhere.
• Your code is correct, but for a subtle reason that is beyond the ability of the type-checker to reason about. In this case, you need to either
  • change your code to use a simpler design with more obvious correctness properties, or
  • suppress the warning together with a comment that argues that your code is correct. (This should be rare with well-designed code!)
• Your code is correct, but there is a bug in the type-checker. This is unlikely, but possible. Maybe some library method is incorrectly annotated, or maybe the Nullness Checker has a different bug. In this case, first construct an argument that your code is correct and the type-checker is wrong. Then, send your report, along with a minimal test case, to the course staff. In the meanwhile, you can suppress the warning (with an appropriate comment) so that you can continue to do work.

If you think your code is correct, you should express an argument that the code is correct, and then translate that argument into annotations. This process is described in two sections of the Checker Framework manual: What to do if a checker issues a warning about your code and Unexpected type-checking results. Sometimes you will find that your argument was incomplete (it was missing a step, and therefore missing an annotation). Other times you will find that Nullness Checker annotations cannot express your argument: either because it cannot express a fact you depend upon, or because it cannot make a true inference. Don't jump to the conclusion that it is wrong, however, because you might be missing something.

If the Nullness Checker warns that a call to someMap.get(aKey) is nullable, then usually the reason is that before the call, the Nullness Checker could not establish that aKey is definitely a key in someMap. Figure out how to help the Nullness Checker conclude that fact.

Suppressing warnings

Your goal is to obtain a compile-time guarantee of correct use of null. Therefore, you are strongly discouraged from suppressing warnings.

It's fine to suppress a small number of warnings. You should generally try to use the annotations correctly as they save you a significant amount of time having to reason about your code. The point of the exercise of using the nullness checker is to get you reasoning about what facts are true about your program at sequential points in code, so it is theoretically within reason to suppress any warning so long as you are thorough in explaining why the code is safe even in spite of having to suppress an issue the nullness checker brought up.

For each suppressed warning, write a Java comment with a single sentence explaining why the @SuppressWarnings annotation or assert statement is correct. In other words, explain why adding the annotation/assertion is guaranteed to be correct and does not compromise the guarantee that your program never throws a NullPointerException. For example:

  @SuppressWarnings("nullness") // myArray is non-null up to index num_elts, and i<num_elts
  @NonNull Object o = myArray[i];

If your warning is not on a line with a variable declaration as in the example above, it may be necessary for you to shift where the warning occurs so that it does appear on a line with a variable declaration. You can usually do so by declaring new variables so that their type fixes the original warning but introduces a new one when you attempt to assign to that variable.

Rather than suppressing a warning, it is usually better to refactor your code so that the checker issues no warnings. That usually improves the design: if the correctness of your code is so obvious that it is apparent to the checker, then it will also be more apparent to other programmers!

The Checker Framework Manual states a number of ways to suppress warnings. You should only use the @SuppressWarnings annotation or the assert statement, preferring to use the @SuppressWarnings annotation when possible. Each such annotation should be on a single variable declaration (not on an entire method or class). For example:

// No @SuppressWarnings("nullness") annotation here on the class!
class MyClass {

  // No @SuppressWarnings("nullness") annotation here on the method!
  void myMethod() {
    ...
    // The expression is never null because ...
    @SuppressWarnings("nullness")
    @NonNull Object myVar = expression;
    ...
  }

  ...
}

If you have to suppress a warning, try to suppress it as early as possible, such as at an earlier line of a method rather than a later one, if you have a choice. Placing the suppression earlier generally leads to clearer code.

Sometimes, you may think a warning suppression is necessary even though it is not. If you feel that your implementation requires the use of @SuppressWarnings, we suggest that you discuss your code with the course staff.

Do not circumvent the type-checker

Do not circumvent the type-checker. One example would be replacing code such as

  x.method();

with

  if (x == null)
    throw new Error("x is null");
  x.method();

That replacement may quiet the compiler warnings, but it does does no good in terms of guaranteeing that your program does not crash. The original version crashes if x is null, and so does the modified version. The latter version is bad style and will be graded as such.

A reasonable rule of thumb is: don't add an if statement that cannot fail at run time, just to eliminate type-checker warnings. When a programmer sees a conditional, the programmer should assume that the test can evaluate to either true or false. Adding useless conditional statements degrades the readability of your code.

Hints

You don't have to write very many annotations! Because @NonNull is the default, you will probably never write it. Because of the type-checker's built-in dataflow analysis, you will rarely or never write annotations in method bodies — only on method signatures. One place you do need to write a @Nullable annotation is on the formal parameter in each equals(Object) method declaration, like so: public boolean equals(@Nullable Object) { ... }.

Specifying checkRep

class A {
  Object info;
  A() {
    info = new Object();
  }
}
class B extends A {
  Object moreInfo;
  B() {
    super();
    moreInfo = new Object();
  }
}

While executing the expression new B(), at the end of the A() constructor, the moreInfo field has not yet been initialized.

Here are three options for correcting your code so that the Checker Framework no longer issues a warning.

• Make your class final, so that the object is fully initialized at the end of its constructor. The downside of this is that you cannot extend the class.
• Don't call checkRep at the end of constructors. The downside of this is that you will not learn of defects (bugs) in the constructor.
• Don't let checkRep depend on fields added by subclasses, which requires that checkRep will never call any method that may be overridden. Write the specification this way:

  void checkRep(@UnknownInitialization(MyClass.class) MyClass this) { ... }

  which says that the receiver of checkRep is initialized as a MyClass but not as any subclass.

Is checkRep necessary?

If you are using the Nullness Checker to verify your code, assertions such as calls to the checkRep routine might seem redundant. If you have proved a fact, there is little point in testing it.

It is still a good idea to retain the assertions, however.

1. Your implementation may have representation invariants about properties beyond nullness, initialization, and map keys. Those parts of checkRep are not redundant.
2. checkRep can discover mistakes you made when suppressing a Nullness Checker warning — that is, you thought it was a false alarm, but it was actually a defect in your code.
3. If client code is not checked by the Nullness Checker, it might violate a method precondition or your representation invariant.

Just like it is prudent to use a seat belt even if your car is equipped with air bags, it is prudent to use both static and dynamic checking of your code.

Who made the Checker Framework?

One member of the Checker Framework team is Stephanie Dietzel, a former CSE 331 student. She used it in her assignments, joined the research team, performed case studies, improved a type system, and became a published author.

If you are a student who likes thinking about programs — and especially about programs that write programs, or programs that reason about programs — then you should also think about getting involved in undergraduate research. The Checker Framework is an exciting projects, and there are many other research projects in the Allen School. Once you have completed CSE 331, you will be ready to contribute!

Back to the CSE 331 handouts home page.