Improving Code Quality With Checker Framework

It would've been nice if the intern hadn't messed with the transaction timeout by setting just a few seconds, instead of minutes, right? And that time when you let dirty parameters values compromise your data, remember? We are about to meet a new ally to avoid these situations!

The Checker Framework

Developed at the University of Washington’s School of Computer Science and Engineering, the Checker Framework proves to be a great addendum to improve overall code quality. It offers various compiler checkers that enforces rules and verification at compile time, warning and pointing each broken requirement found, all through a set of simple annotations and little configuration effort.

Compile time, enforcing rules, compile checking…it seems more complicated that it really is! Let’s grab a simple example, analyze each step and understand how it works.

Grab the code for the following examples here. By compiling/packaging you must expect a build failure due to some checker processor.

public class HelloChecker {

    @Nullable private String name;
    @MonotonicNonNull private String surname;

    public void hello() {
        final String fullName = name + ", " + surname;
        System.out.println(String.format("Name: %s", fullName));
    }

}

Check these two annotations (from package org.checkerframework.checker.nullness.qual) we saw at HelloChecker class:

•  @Nullable - Indicates that the property may be assigned null;

•  @MonotonicNonNull- This type may be null, but as soon as it assume a value, it must never becomes null again.

We compile the class and everything is fine as expected. It is important to note that our requirements expected that only the surname, when filled by user, must not be null again as per the  @MonotonicNonNull documentation:

Indicates a reference that may be null, but if it ever becomes non-null, then it never becomes null again. This is appropriate for lazily-initialized fields, among other uses. When the variable is read, its type is treated as   @Nullable, but when the variable is assigned, its type is treated as   @NonNull.

Let’s suppose that both name and surname are mandatory. Just annotate with a  @NonNull, or leave it with no annotations at all. That is it,  @NonNull is the default behaviour, and during compile time you will be warned about all errors found:

[ERROR] COMPILATION ERROR : 
[INFO] -------------------------------------------------------------
[ERROR] /home/diogo/checker-fw-example/src/main/java/net/diogosilverio/checker/HelloChecker.java:[6,8] [initialization.fields.uninitialized] the constructor does not initialize fields: name, surname
[INFO] 1 error
[INFO] -------------------------------------------------------------
[INFO] ------------------------------------------------------------------------
[INFO] BUILD FAILURE
[INFO] ------------------------------------------------------------------------
[INFO] Total time: 3.778 s
[INFO] Finished at: 2018-02-15T21:25:56-02:00
[INFO] Final Memory: 19M/209M
[INFO] ------------------------------------------------------------------------
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-compiler-plugin:3.7.0:compile (default-compile) on project checker-session: Compilation failure
[ERROR] /home/diogo/checker-fw-example/src/main/java/net/diogosilverio/checker/HelloChecker.java:[6,8] [initialization.fields.uninitialized] the constructor does not initialize fields: name, surname

The resulting failure is a non-initialized fields error, pointing to both fields. You can solve this problem with just a simple initialization:

public class HelloChecker {

    private String name;
    private String surname = "Doe";

    public HelloChecker(){
        this.name = "Jane";
    }
// Ommited code
}

Compile again to see everything working successfully. We will check all the necessary configuration soon! Next, let's see a little bit more about verifications provided by the framework.

Flavors

As mentioned before, there are lots of checkers covering many possible problems. Below there is a non-exhaustive list of some checkers provided:

• Nullness - Possible null pointer exceptions are detected;

• Map Key - Infers the correctness of keys;

• Tainting - Trustiness of values coming from beyond the application control;

• Regex - Prevents syntactic errors; and

• Units - Ensure operations between correct units of measure.

The manual provides a full list of checkers. I suggest you take a look and try all those interesting to your use cases.

Trying Some Flavors

Ok, it’s time to get your hands dirty and find out how it could be useful for our daily tasks!

You may pick your favorite IDE. I am using IDEA Ultimate 2018.1, Java 8 and Maven 3.5.2 for the following drills.

Dependencies

We will need three main dependencies for our examples, all using the current (2.5.0) version of the framework:

• Checker Framework;

• Checker Qualifiers;

• Checker Annotated JDK 8.

Make sure your pom.xml contains all of them:

<project xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
         xmlns="http://maven.apache.org/POM/4.0.0"
         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<!-- Ommited details -->
   <properties>
      <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
      <maven.compiler.source>1.8</maven.compiler.source>
      <maven.compiler.target>1.8</maven.compiler.target>
      <checker.version>2.5.0</checker.version>
   </properties>
   <dependencies>
      <dependency>
         <groupId>org.checkerframework</groupId>
         <artifactId>checker</artifactId>
         <version>${checker.version}</version>
      </dependency>
      <dependency>
         <groupId>org.checkerframework</groupId>
         <artifactId>jdk8</artifactId>
         <version>${checker.version}</version>
      </dependency>
      <dependency>
         <groupId>org.checkerframework</groupId>
         <artifactId>checker-qual</artifactId>
         <version>${checker.version}</version>
      </dependency>
   </dependencies>
</project>

We need a few more configurations to be set before starting coding. Create a property referring to the Checker annotated JDK 8 and the current framework version(at the writing of this article):

<properties>
  <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
  <maven.compiler.source>1.8</maven.compiler.source>
  <maven.compiler.target>1.8</maven.compiler.target>
  <checker.version>2.5.0</checker.version>
  <annotatedJdk>${org.checkerframework:jdk8:jar}</annotatedJdk> <!-- This one -->
</properties>

Then set the maven compiler plugin to do the hard work. We will provide all processors needed for the examples:

<build>
  <plugins>
    <plugin>
      <artifactId>maven-compiler-plugin</artifactId>
      <version>3.7.0</version>
      <configuration>
        <annotationProcessors>
          <annotationProcessor>org.checkerframework.checker.nullness.NullnessChecker</annotationProcessor>
          <annotationProcessor>org.checkerframework.checker.tainting.TaintingChecker</annotationProcessor>
          <annotationProcessor>org.checkerframework.checker.units.UnitsChecker</annotationProcessor>
        </annotationProcessors>
        <compilerArgs>
          <arg>-Xbootclasspath/p:${annotatedJdk}</arg>
        </compilerArgs>
      </configuration>
    </plugin>
  </plugins>
</build>

We just prepared the compiler to use three checkers:

• Nullness;

• Tainting;

• Units.

By simply listing those processors, we just enabled them to look for issues regarding our project’s code base.

Do not be limited to those three examples. I’ve picked them to illustrate a few common situations we may find in a daily basis.

Nullness Checker

The Nullness checker documentation is pretty straightforward: If no issues are warned, your program will never throw a Null Pointer exception.

Are you skeptical about this? Let’s try a small example and see how simple and accurate this processor is.

Here we have two different Maps, one for carrying good parameters and the other for possible null values according to the application needs:

public class NullChecker {

    private Map<Long, Parameter> successMap;
    private Map<Long, @Nullable Parameter> errorMap;
  // Ommited code
}

Since the Nullness checker is enabled, let’s grant that both maps are initialized:

public class NullChecker {

    private Map<Long, Parameter> successMap;
    private Map<Long, @Nullable Parameter> errorMap;

    public NullChecker() {
        this.successMap = new HashMap<>();
        this.errorMap = new HashMap<>();
    }
  // ...
}

Inside method start, we delegate the rules to some other method that may return a null value.

According to the processed result, we pick the correct map:

    public void start(final Parameter param) {

        Parameter processedParameter = processParameter(param);

        if (processedParameter != null) {
            System.out.println("Parameter is good");
            this.successMap.put(System.currentTimeMillis(), processedParameter);
        } else {
            this.errorMap.put(System.currentTimeMillis(), processedParameter);
            throw new IllegalArgumentException("Bad parameter!");
        }
    }

    private @Nullable Parameter processParameter(Parameter parameter) {
        Boolean condition = Boolean.FALSE;
        // Business rules & etc

        if (condition) {
            return new Parameter();
        }

        return null;
    }

The code above compiles fine. But what if we hadn’t declared errorMap as having a possible Nullable value? What if the method processParameter hadn’t told everyone explicitly that a possible null result might be returned?

Don’t take this checker for granted due to its simplicity. As soon as it is enabled, it will probably highlight a good number of cases you just passed by without noticing them.

Play along with those annotations and maps to find out how to fit these validations for new and local variables!

Tainting Checker

The second checker we will try is the Tainting checker. It helps us to ensure that we are handling validated values from arbitrary sources properly. The framework documentation advises us to determinate our boundaries by annotating unsafe sources and our sensitive methods.

There are two main annotations that help us do this job:

•  @Tainted - Everything annotated as Tainted is considered potentially unsafe and will not cross any Untainted boundary. This is the default for this checker;

•  @Untainted - Includes only trusted values.

To help illustrate the usage, the code below assumes the User will provide somehow a  @Tainted data Object to be sent somewhere by the application.

public void processData(@Tainted Object data){
this.sendUntrustedData(data);

final Object trustedData = this.sanitizeData(data);
this.sendTrustedData(trustedData);
}

We created two methods to test our Untainted boundary:

•  sendUntrustedData - Does not define an Untainted boundary;

•  sendTrustedData - Defines an Untainted boundary.

private void sendTrustedData(@Untainted Object data){
System.out.println("Sending trusted data: " + data.toString());
}

private void sendUntrustedData(Object data) {
System.out.println("Sending possible untrusted data: " + data.toString());
}

After defining both methods, we need a way to sanitize our data according to our boundary, so we may send our data safely:

@Untainted
@SuppressWarnings("tainting")
private Object sanitizeData(Object data) {
  // Data cleansing logic
  if(data != null){
  return data;
  }

  throw new IllegalArgumentException("Invalid data sent");
}

It is expected that you, as the developer, know how to delimit the untainted area and clean/provide a safe version of the user’s input. You must define the return as an @Untainted  result, suppressing tainting warnings.

Compiling the code will lead to a successful build. Mess a little with this code removing sanitized object or setting an  @Untainted boundary within the unsafe method and see what happens!

Don’t worry about forgetting to annotate your tainted objects. By default, the framework will consider every non sanitized object tainted while it tries to break through the untainted boundary.

Units Checker

Are you constantly mixing  timeToLive with other variables and messing around? Here we put our hand at the Units Checker. It allows us to qualify variables within a series of units, defined by kinds or SI units (and also polymorphic).

By Units kind we may qualify in a more generic way, such as @Time, @Length and @Temperature among other. The International System Units gives us a more detailed set of qualifiers. For  @Time, we may derive  @s, @min and  @h, for seconds, minutes and hours, respectively.

Let's try the following: We will define a few variables — timeToLive, extraTime, and maxSize, and evaluate when they are allowed to interact (or not).

Defining variables is our first step:

@Time
private Long timeToLive = 5000L * UnitsTools.s;

@Time
private Long extraTime = 1500L * UnitsTools.s;

@Length
private Long maxSize = 204800L * UnitsTools.m;

Ok. We defined all variables needed and qualified our values with the help of UnitTools class. Compiling our class will not raise any problems.

The happy path is adding some extraTime to our timeToLive variable:

@Time
public Long extraTTL(){
return timeToLive + extraTime;
}

So far, so good! Two @Time variables prior defined are always good. But what if we needed some arbitrary local value? Just sum any value with the UnitsTools help, right?

@Time
public Long extraInlineTTLDoesNotWork(){
return timeToLive + (1000L * UnitsTools.s);
}

Not good! We must define a local variable, prior to our operation, then return the new TTL:

@Time
public Long extraLocalTTL(){
  @Time Long extraTimeLocal = 1000L * UnitsTools.s;
  return timeToLive + extraTimeLocal;
}

Compile and see it work properly.

And what about the @Length one? Is it possible to sum maxSize with timeToLive ? Well, yes, it is:

public Long works(){
return timeToLive + maxSize;
}

The plugin will not complain about this operation. Instead, just annotate the method with your exp0ected output qualifier to allow the correct validation:

@Length
public Long doesNotWork(){
return maxSize + extraTime;
}

The code above will raise an incompatible type, as expected. 

Wrapping Up

The documentation is full of examples and in-depth explanation. I deeply recommend you to read those checkers that matter most to you, experimenting and applying to your project according to your needs.

The Checker Framework is a nice tool for our utility belt, but keep in mind that it is just a tool. It provides lots of checkers, for the most different needs, but as a developer we must keep focused on writing good and clean code from the beginning, reassessing the quality of the work done whenever is possible.