Restricted side effects: @SideEffectFreeExcept or @WritesFields

[mernst]

Currently, side effect annotations are all-or-nothing. The Checker Framework does not have a way to indicate that some routine's side effects are limited.

Here is an idea for making the CF's side effect annotations somewhat more expressive, without devolving into an arbitrarily complex specification language. In particular, this enhancement would make it possible to specify that System.out.println side-effects only its receiver, and to specify that a setter only affects one particular field. Currently, anytime that those methods are called, the CF conservatively assumes that any side effect could occur, and all flow-sensitively refined information is lost.

A new method annotation, @SideEffectFreeExcept({expr1, expr2}), specifies that the method has no side effects, except for side effects to the given Java expressions. For example,

  class PrintStream {
    @SideEffectFreeExcept("this")
    public PrintStream printf(String format, Object... args)
  }

indicates that printf side-effects only its receiver formal parameter, but none of its other formal parameters and no global variables.

At a call to an annotated method, only the given expressions, or anything they might alias, need to be flushed from the abstract state. (The CF soundly, but conservatively, tracks potential aliasing.) At a call to an unannotated method, all of the abstract state (except for local variables) must be flushed. This will allow flow-sensitive type refinement to be more precise.

For now, the annotation will be trusted rather than checked. This is similar to other side-effect annotations. In the future, it could be checked by an ownership type system or some other mechanism.

[mernst]

A better name would be @WritesFields; the argument would be a superset of all the fields that could be written (directly or indirectly) on any execution of the method.