The Checker Framework Manual:
Custom pluggable types for Java

Chapter 7 Called Methods Checker for the builder pattern and more

The Called Methods Checker tracks the names of methods that have definitely been called on an object. This checker is useful for checking any property of the form “call method A before method B”. For the purpose of this checker, a method has “definitely been called” if it is invoked: a method that might never return or that might throw an exception has definitely been called on every path after the call, including exceptional paths. The checker also assumes that the program is free of null-pointer dereferences. You can verify that all pointer dereferences are safe by running the Nullness Checker (Chapter 3).

The Called Methods Checker provides built-in support for one such property: that clients of the builder pattern for object construction always provide all required arguments before calling build(). The builder pattern is a flexible and readable way to construct objects, but it is error-prone. Failing to provide a required argument causes a run-time error that manifests during testing or in the field, instead of at compile time as for regular Java constructors. The Called Methods Checker verifies at compile time that your code correctly uses the builder pattern, never omitting a required argument. The Called Methods Checker has built-in support for Lombok (see the caveats about Lombok in Section 7.2) and AutoValue.

You can verify other builders, or verify other properties of the form “foo() must be called before bar()”, by writing method specifications. Section 7.5 describes another example related to a security property.

If the checker issues no warnings, then you have a guarantee that your code supplies all the required information to the builder. The checker might yield a false positive warning when your code is too tricky for it to verify. Please submit an issue if you discover this.

7.1 How to run the Called Methods Checker 

javac -processor calledmethods MyFile.java ...
javac -processor org.checkerframework.checker.calledmethods.CalledMethodsChecker MyFile.java ...

The Called Methods Checker supports the following optional command-line arguments:

  • • The -ACalledMethodsChecker_disableBuilderFrameworkSupports option disables automatic annotation inference for builder frameworks. Section 7.4 describes its syntax. Supply this if you are uninterested in errors in the use of builders, but are using the Called Methods Checker to detect errors in other types of code.

  • • The -ACalledMethodsChecker_disableReturnsReceiver option disables the Returns Receiver Checker (Chapter 25), which ordinarily runs as a subchecker of the Called Methods Checker. If the code being checked does not use fluent APIs, then you can supply this option and the Called Methods Checker will run much faster. This option is the default when the Called Methods Checker is run as part of the Resource Leak Checker (Chapter 8).

  • • The -ACalledMethodsChecker_useValueChecker option improves precision when analyzing code that uses the AWS SDK’s DescribeImageRequest API. See Section 7.5.

7.2 For Lombok users

The Called Methods Checker supports projects that use Lombok via the io.freefair.lombok Gradle plugin automatically. However, note that the checker’s error messages refer to Lombok’s output, which is a variant of your source code that appears in a delombok directory. To fix issues, you should edit your original source code, not the files in the checker’s error messages.

If you use Lombok with a build system other than Gradle, you must configure it to do two tasks. If either of these is not done, the checker will not issue any errors on Lombok code.

  • • set Lombok configuration option lombok.addLombokGeneratedAnnotation = true

  • • delombok the code before passing it to the checker

7.3 Specifying your code

The Called Methods Checker reads method specifications (contracts) that state what a method requires when it is called. It warns if method arguments do not satisfy the method’s specification.

If you use AutoValue or Lombok, most specifications are automatically inferred by the Called Methods Checker, from field annotations such as @Nullable and field types such as Optional. Section 7.4 gives defaulting rules for Lombok and AutoValue.

  

(image)

  

Figure 7.1: The type hierarchy for the Called Methods type system, for an object with two methods: a() and b(). Types displayed in gray should rarely be written by the programmer.

In some cases, you may need to specify your code. You do so by writing one of the following type annotations (Figure 7.1):

@CalledMethods(String[] methodNames)

The annotated type represents values on which all the given methods were definitely called. (Other methods might also have been called.) @CalledMethods(), with no arguments, is the default annotation.

Suppose that the method build is annotated as 

    class MyObjectBuilder {
      MyObject build(@CalledMethods({"setX", "setY"}) MyObjectBuilder this) { ... }
    }

Then the receiver for any call to build() must have had setX() and setY() called on it.

A typical case in which Lombok users must manually write this annotation is when performing extra builder input validation. Performing validation can be done through subclassing generated builders and overriding the generated build() method as follows. 

    class MyObjectSubBuilder extends MyObjectBuilder {
      @Override
      MyObject build(@CalledMethods({"setX", "setY"}) MyObjectSubBuilder this) {
        MyObject o = super.build();
        if ((o.getX() == null) != (o.getY() == null)) {
          throw new IllegalArgumentException("Nullness for x and y should be equal");
        }
        return o;
      }
    }
@CalledMethodsPredicate(String expression)

The boolean expression specifies the required method calls. The string is a boolean expression composed of method names, disjunction (||), conjunction (&&), not (!), and parentheses.

For example, the annotation @CalledMethodsPredicate("x && y || z") on a type represents objects such that either both the x() and y() methods have been called on the object, or the z() method has been called on the object.

A note on the not operator (!): the annotation @CalledMethodsPredicate("!m") means “it is not true that m was definitely called”; equivalently “there is some path on which m was not called”. The annotation @CalledMethodsPredicate("!m") does not mean “m was not called”.

The Called Methods Checker does not have a way of expressing that a method must never be called. You can do unsound bug-finding for such a property by using the ! operator. The Called Methods Checker will detect if the method was always called, but will silently approve the code if the method is called on some but not all paths.

@This

@This may only be written on a method return type, and means that the method returns its receiver. This is helpful when type-checking fluent APIs. This annotation is defined by the Returns Receiver Checker (Chapter 25), but is particularly useful for the Called Methods Checker because many builders are fluent APIs.

For Lombok users it is important to (manually) add @This to any custom method that calls any other generated builder method. For instance, in the following example, it is important to annotate setXMod42() with @This, since the added method calls setX() (which returns the current builder instance). 

        class MyObjectBuilder {

            @This
            MyObjectBuilder setXMod42(int x) {
              return setX(x % 42);
            }
        }
@CalledMethodsBottom

The bottom type for the Called Methods hierarchy. Conceptually, this annotation means that all possible methods have been called on the object. Programmers should rarely, if ever, need to write this annotation — write an appropriate @CalledMethods annotation instead. The type of null is @CalledMethodsBottom.

There are also method annotations:

@EnsuresCalledMethods

This declaration annotation specifies a post-condition on a method, indicating the methods it guarantees to be called. This annotation is repeatable, meaning that you can write multiple copies of it (with different arguments) on the same method, and the checker will check all of them.

For example, this specification: 

    @EnsuresCalledMethods(value = "#1", methods = {"x", "y"})
    void m(Param p) { ... }

guarantees that p.x() and p.y() will always be called before m returns. The body of m must satisfy that property, and clients of m can depend on the property.

Sometimes, you need to provide information to enable the Called Methods Checker to verify the property. Consider this example: 

    @EnsuresCalledMethods(value="#1", methods="close")
    public void closeSocket(Socket sock) throws IOException {
        sock.close();
        m();
    }

If m() might have side-effects (i.e., it is not annotated as @SideEffectFree, as @Pure), then the Called Methods Checker issues an error because it cannot make any assumptions about the call to m(), and therefore assumes the worst: that all information it knows about in-scope variables (including that close() was called on sock) is stale and must be discarded. Here are possible fixes:

  • • add a @SideEffectFree or @Pure annotation to m(), if m() is in fact side-effect free or pure.

  • • re-order the calls to sock.close() and m() so that the call to sock.close() appears last in closeSocket().

@EnsuresCalledMethodsIf

This declaration annotation specifies a post-condition on a method, indicating the methods it guarantees to be called if it returns a given result.

For example, this specification: 

    @EnsuresCalledMethodsIf(expression = "#1", methods = {"x", "y"}, result=true)
    boolean m(Param p) { ... }

guarantees that p.x() and p.y() will always be called if m returns true. The body of m must satisfy that property, and clients of m can depend on the property.

@EnsuresCalledMethodsVarargs

This version of @EnsuresCalledMethods always applies to the varargs parameter of the annotated method. It has only one argument, which is the list of methods that are guaranteed to be called on the varargs parameter’s elements before the method returns. This annotation currently cannot be verified, and an ensuresvarargs.unverified error is always issued when it is used. When annotating a method as @EnsuresCalledMethodsVarargs, you should verify that the named methods are actually called on every element of the varargs parameter via some other method (such as manual inspection) and then suppress the warning.

@EnsuresCalledMethodsOnException

This declaration annotation specifies a post-condition on a method, indicating the methods it guarantees to call when it throws an exception. Like most post-condition annotations, the other Called Methods post-condition annotations (@EnsuresCalledMethods, @EnsuresCalledMethodsIf, and @EnsuresCalledMethodsVarargs) only specify behavior for normal returns. The annotation @EnsuresCalledMethodsOnException allows you to write stronger specifications indicating that a method always calls the given methods: 

    @EnsuresCalledMethods(value = "#1", methods = {"close"})
    @EnsuresCalledMethodsOnException(value = "#1", methods = {"close"})
    void closeIfNonNull(Closeable p) {
      if (p != null) {
        p.close();
      }
    }

@EnsuresCalledMethodsOnException can also be used together with the Resource Leak Checker’s @Owning annotation. See Section 8.4.1.

@RequiresCalledMethods

This declaration annotation specifies a pre-condition on a method, indicating that the expressions in its value argument must have called-methods types that include all the methods named in its methods argument. If the expression is a parameter of the annotated method, you should use a @CalledMethods annotation on the parameter instead.

7.4 Default handling for Lombok and AutoValue

This section explains how the Called Methods Checker infers types for code that uses the Lombok and AutoValue frameworks. Most readers can skip these details.

You can disable support for builder frameworks by specifying them in a comma-separated lowercase list to the command-line flag disableBuilderFrameworkSupports. For example, to disable both Lombok and AutoValue support, use:
-ACalledMethodsChecker_disableBuilderFrameworkSupports=autovalue,lombok

The Called Methods Checker automatically assumes default annotations for code that uses builders generated by Lombok and AutoValue. There are three places where annotations are usually assumed:

  • • A @CalledMethods annotation is placed on the receiver of the build() method, indicating the setter methods that must be invoked on the builder before calling build(). For Lombok, this annotation’s argument is the set of @lombok.NonNull fields that do not have default values. For AutoValue, it is the set of fields that are not @Nullable, Optional, or a Guava Immutable Collection.

  • • The return type of a toBuilder() method (for example, if the toBuilder = true option is passed to Lombok’s @Builder annotation) is annotated with the same @CalledMethods annotation as the receiver of build(), using the same rules as above.

  • • A @This annotation is placed on the return type of each setter in the builder’s implementation.

If your program directly defines any of these methods (for example, by adding your own setters to a Lombok builder), you may need to write the annotations manually.

Minor notes/caveats on these rules:

  • • Lombok fields annotated with @Singular will be treated as defaulted (i.e., not required), because Lombok will set them to empty collections if the corresponding setter is not called.

  • • If you manually provide defaults to a Lombok builder (for example, by defining the builder yourself and assigning a default value to the builder’s field), the checker will treat that field as defaulted most of the time. In particular, it will not treat it as defaulted if it is defined in bytecode rather than in source code.

7.5 Using the Called Methods Checker for properties unrelated to builders

The Called Methods Checker can be used to verify any property of the form “always call A before B”, even if the property is unrelated to builders.

For example, consider the AWS EC2 describeImages API, which clients use during the process of initializing a new cloud instance. CVE-2018-15869 describes how an improperly-configured request to this API can make the requesting client vulnerable to a “machine-image sniping” attack that would allow a malicious third party to control the operating system image used to initialize the machine. To prevent this attack, clients must specify some trusted source for the image by calling the withOwners or withImageIds methods on the request prior to sending it to AWS. Using a stub file for the describeImages API (DescribeImages.astub), the Called Methods Checker can prove that a client is not vulnerable to such an attack.

To improve precision, you can specify the -ACalledMethodsChecker_useValueChecker command-line option, which instructs the checker to treat provably-safe calls to the withFilters method of a DescribeImagesRequest as equivalent to the withOwners or withImageIds methods.

7.6 More information

The paper “Verifying Object Construction” [KRS+20] (ICSE 2020, https://homes.cs.washington.edu/~mernst/pubs/object-construction-icse2020-abstract.html) gives more information about the Called Methods Checker, such as theoretical underpinnings and results of experiments. (The paper uses an earlier name, “Object Construction Checker”.)