The Checker Framework Manual:
Custom pluggable types for Java

Chapter 23 Purity Checker

A side-effect-free method is one that has no externally-visible side effects: it changes no object that exists when it is called, except in ways that no caller can observe, such as updating a private cache. A deterministic method returns the same value each time it is called on the same arguments; equality is with respect to ==, not .equals(). A pure method is both side-effect-free and deterministic. The Purity Checker can check and infer all three types of methods, and “purity” refers to all concepts.

All checkers utilize purity annotations to aid type refinement (Section 33.7). By default, purity annotations are trusted, not checked.

To check purity annotations, pass -AcheckPurityAnnotations to any checker. The Purity Checker is conservative, so you are likely to need to suppress some warnings. To run only the Purity Checker (this is uncommon), supply the following command-line option to javac: -processor org.checkerframework.framework.util.PurityChecker. That implies -AcheckPurityAnnotations, so you do not need to supply both options.

To infer purity annotations, supply the command-line option -AsuggestPureMethods. The Checker Framework will suggest methods that can be marked as @SideEffectFree, @Deterministic, or @Pure. In addition, such suggestions are output by -Ainfer and when using whole-program inference.

23.1 Purity annotations

@SideEffectFree

indicates that the method has no externally-visible side effects.

@Deterministic

indicates that if the method is called multiple times with identical arguments, then it returns the identical result according to == (not just according to equals()).

@Pure

indicates that the method is both @SideEffectFree and @Deterministic.

23.2 Lambdas, method references, and functional interfaces

Creating a lambda, or declaring a local or anonymous class, is not itself a side effect. A lambda expression evaluates to an object but does not run the code in the lambda’s body. A side-effect-free method may therefore create a lambda whose body has side effects:

    @SideEffectFree
    Runnable makeRunnable() {
      return () -> count++; // OK: creating the lambda has no side effect
    }

The effects of the body occur where the functional method is invoked, and each such invocation is checked on its own.

Likewise, evaluating a method reference does not run the referenced method. However, the qualifier expression of a method reference expr::m is evaluated where the method reference appears, so its effects are effects of the enclosing method:

    @SideEffectFree
    Supplier<String> makeSupplier() {
      return sideEffect()::toString; // error: sideEffect() is called here
    }

The body of a lambda is checked against the purity annotations on the functional interface method that the lambda implements, not against those on the method that creates the lambda. For example:

    @FunctionalInterface
    interface PureSupplier {
      @SideEffectFree String get();
    }

    PureSupplier s1 = () -> "hello";                      // OK
    PureSupplier s2 = () -> { count++; return ""; };      // error: the body has a side effect

Similarly, the method that a method reference refers to must be annotated at least as pure as the functional interface method:

    @SideEffectFree String name() { ... }
    String describe() { ... }

    PureSupplier s3 = this::name;       // OK
    PureSupplier s4 = this::describe;   // error: describe() is not @SideEffectFree

The functional interface method’s purity annotations include those that it inherits from methods that it overrides (Section 23.4). If the functional interface method has no purity annotation — for example, because it is declared in an unannotated library and no stub file annotates it — then neither a lambda’s body nor a method reference is checked against it.

The errors shown in this section are reported only when purity annotations are checked: by the Purity Checker, or by another checker when you pass -AcheckPurityAnnotations. With -Ainfer, the body of a lambda is not checked; instead, it is used to infer the purity of the functional interface method.

23.2.1 Functional-interface parameters of methods with purity annotations

A method annotated with a purity annotation may call the functional methods of its own functional-interface parameters. A functional-interface parameter is one whose type, or the interface that declares the type’s functional method, is annotated with @FunctionalInterface, as Function, Runnable, and the other interfaces in java.util.function are. A parameter of a type such as Iterable, AutoCloseable, or Comparable is not one, even though the type has a single abstract method. A call to the functional method of such a parameter is treated as having the purity that the method promises:

  • • In a @SideEffectFree method, the call is treated as side-effect-free.

  • • In a @Deterministic method, the call is treated as deterministic.

  • • In a @Pure method, the call is treated as pure.

    @SideEffectFree
    int m(Function<String, Integer> f, String s) {
      return f.apply(s); // permitted: apply is treated as side-effect-free
    }

The assumption applies only when the parameter is effectively final and the functional method is called directly on the parameter. It does not apply to a call through a local variable or field that aliases the parameter, nor to a method of the parameter’s type other than its functional method, such as Function.andThen:

    @SideEffectFree
    int m2(Function<String, Integer> f, String s) {
      Function<String, Integer> g = f;
      return g.apply(s); // error: g is not a parameter
    }

A call may reach the method through any method that it overrides, and such a call checks its arguments only against the overridden method’s promise. So the method may assume only the purity that it and every method it overrides promise for that parameter. An overridden method that makes no promise, or whose parameter at that position is not a functional interface (for example, its type is a type variable), guarantees nothing, and the assumption does not apply.

At each call to such a method, every argument passed to a functional-interface parameter must have the purity that the method promises (side-effect-free for a @SideEffectsOnly method). The requirement is the same for every functional-interface parameter, and it applies even if the method’s body never calls that parameter’s functional method. Only a parameter whose declared type is a functional interface is checked: the method may assume nothing about an argument to a parameter whose type is a type variable, nor about the elements of a varargs array. How the argument is checked depends on its form:

  • • A method reference is checked via the referenced method, which must have the required purity annotations.

  • • A lambda is checked via its body, which must have the required purity.

  • • Any other argument is checked via the functional method of the argument’s declared type, which must have the required purity annotations.

    m(String::length, "hi");    // OK: String.length() is side-effect-free
    m(s -> s.length(), "hi");   // OK: the lambda body is side-effect-free
    m(s -> count++, "hi");      // error: the lambda body has a side effect

    void caller(Function<String, Integer> g) {
      m(g, "hi");              // error: [purity.functional.argument] Function.apply is not @SideEffectFree
    }

If the functional method returns void, a @Pure method requires only that the argument be side-effect-free, because a side-effect-free call that returns no value is deterministic. Otherwise a @Pure method requires the argument to be deterministic too, even if the method calls it only on an error path. For example, Objects.requireNonNull(T, Supplier<String)> is @Pure, so the following is an error, because String.format is not deterministic:

    Objects.requireNonNull(x, () -> String.format("bad %s", y));         // error: [purity.call]

The assumption affects purity checking, and the dataflow analysis of a lambda in the method body, but not the dataflow analysis of the body itself. A direct call to a functional-interface parameter in the body still discards refinements of fields, as a call to any method that is not annotated as side-effect-free does:

    @SideEffectFree
    int m(Function<String, Integer> f, String s) {
      if (this.x != null) {
        f.apply(s);
        return this.x.hashCode(); // error: [dereference.of.nullable]
      }
      return 0;
    }

23.3 Purity annotations are trusted

By default, purity annotations are trusted by every checker built with the Checker Framework. Purity annotations on called methods affect type-checking of client code, so an incorrect purity annotation can make type-checking unsound. You can make a mistake by writing @SideEffectFree on the declaration of a method that is not side-effect-free, or by writing @Deterministic on the declaration of a method that is not deterministic.

Other than in the Purity Checker, checking of purity annotations (-AcheckPurityAnnotations) is not enabled by default because of a high false positive rate. In the future, after a new purity-checking analysis is implemented, the Checker Framework will default to checking purity annotations.

23.4 Overriding methods inherit specifications from overridden methods

A purity annotation is inherited: if a method in a superclass or superinterface has a purity annotation, then every overriding definition has that annotation too, even if the annotation is not written on the overriding definition. An overriding definition may strengthen the specification by writing a stronger annotation, but it cannot weaken it.

For example, the Object class is annotated as:

class Object {
  ...
  @Pure int hashCode() { ... }
}

(where @Pure means both @SideEffectFree and @Deterministic). Therefore, every definition of hashCode, including those in your program, is implicitly annotated as @Pure and its body is checked accordingly:

MyClass.java:1465: error: [purity.assign.field] field assignment not allowed in deterministic side-effect-free method
    this.hash = h;
        ^

You can fix the definition by making its body pure. Alternately, you can suppress the warning; see Chapter 34.

23.5 Suppressing warnings

The command-line options -AassumeSideEffectFree, -AassumeDeterministic, and -AassumePure make the Checker Framework unsoundly assume that every called method is side-effect-free, is deterministic, or is both, respectively.

The command-line option -AassumePureGetters makes the Checker Framework unsoundly assume that every getter method is side-effect-free and deterministic. For the purposes of -AassumePureGetters, a getter method is defined as an instance method with no formal parameters, whose name starts with “get”, “is”, “not”, or “has” followed by an uppercase letter.

These options can make flow-sensitive type refinement much more effective, since method calls will not cause the analysis to discard information that it has learned. However, these options can mask real errors. They are most appropriate when one of the following is true:

  • • You are starting out annotating a project.

  • • You are using the Checker Framework to find bugs but not to give a guarantee that no more errors exist of the given type.

  • • You are working with an unannotated library that makes the given assumptions, in which case (say) using -AassumePureGetters is easier than writing stub files for all the library’s getter methods.