Restricted side effects: @SideEffectFreeExcept or @WritesFields

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.

Start by locating the existing side-effect annotations and the call-site state-flushing logic in the Checker Framework; the issue names no files or tests. Trace how current annotations are handled, then determine the annotation syntax, alias-aware flushing behavior, and regression coverage needed for the proposed receiver and field cases.