Version of @Pure that persists through side effects

[metalhead8816]

Checker output and YourClassName.java reproduction case attached.

This is fairly common for use of nano protos where initialization might occur in between copying of data based on nullness of a field.

A workaround for now is to use a local variable before the initialization of mutableData and then assign after initialization based on the local variable.

nullness-issue-pure.zip

[wmdietl]

Thanks for the report!

At first I thought that making the constructor for MutableData @Pure would solve the issue.
However, the problem is something completely different: the field update between the check and the use of the pure method.

Take this example:

import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.qual.Pure;

class YourClassNameHere {
  int i;

  void foo(PureData pureData) {
    if (pureData.value() != null) {
      this.i = 4;

      @NonNull Object o = pureData.value();
    }
  }

  interface PureData {
      @Pure
      @Nullable Object value();
  }
}

This results in the same message:

YourClassNameHere.java:13: error: [assignment.type.incompatible] incompatible types in assignment.
      @NonNull Object o = pureData.value();
                                        ^
  found   : @Initialized @Nullable Object
  required: @UnknownInitialization @NonNull Object
1 error

A pure method is only guaranteed to return the same value if the heap didn't change.
The update to field i could influence the result of PureData.value(), for example, an implementation of that method could depend on the value of i to decide whether to return null or not.

By storing the result of pureData.value() in a local variable you ensure that the method is only invoked once and the result can't change.

Please let us know whether this explains the behavior.

[metalhead8816]

Hi Werner,
That definitely explains the behavior, although I would think this comes up quite a bit especially when combined with @autovalue (which my actual code hitting this is). Is there a different annotation to state that this value will not change if called multiple times since it is a simple getter?

[mernst]

Is there a different annotation to state that this value will not change if called multiple times since it is a simple getter?

Side effects can change the result of a getter, by changing the private variable that it returns. So you would need a much stronger requirement than "is a simple getter".

Are you looking for an annotation that is like @Pure, but indicates that the method returns the same value throughout the program and no side effect can affect its value?

[metalhead8816]

Yes, an annotation for denoting this method returns an immutable piece of data. AutoValue already has strong guarantees here, but if each of the value methods could be annotated with @immutable or something like that I think it could solve this.

[mernst]

@Immutable would not be the right annotation. (The fact that a routine returns an immutable datum is orthogonal to whether the routine returns the same value every time the routine is called.)

[metalhead8816]

OK, happy for a different annotation, but I hope my point has come across. Maybe if the class is considered an immutable POJO than each of its methods should be considered to never return different data based on any heap updates.

So maybe the annotations should be placed at the class level to signify this for each method. As you mentioned a method level annotation makes less sense unless it also signifies the underlying data backing the return value in the class isn't changing.

Some ideas for method annotations:
@novariation
@NoCalculation

Maybe if class is @pojo and @immutable this applies to all methods.

[mernst]

I agree this would be valuable. My main point is that we need to be careful about the semantics because it would be easy to propose an unsound rule, and about the naming so that programmers can understand it. Thanks for the suggestions!

[mernst]

As a summary, there is no bug. The Checker Framework is working as intended. However, there is a feature request to make the Checker Framework more expressive and issue fewer false positive warnings.

I see three ways we could deal with this problem:

• Users can put computations in a local variable. This workaround works fine, but it requires a change to some source code.

• Create an annotation to indicate that a particular method has the same value throughout the run, regardless of side effects. The method might have different effects on different runs. This could be a replacement for @Pure (such as @PureSideEffectImmune) or a user could write it along with @Pure, as in @Pure @SideEffectImmune. We need a good name for this. Some preliminary work was done at Waterloo on @SingleRunDeterministic, which may be the same concept.

• We can create a more general and expressive mechanism, which would handle this issue and also other cases that have come up. The Checker Framework would define annotations @ReadsFields and @WritesFields. If provided, each is an overapproximation to all possible fields that are read or written by the method. Currently, whenever a side effect happens, the dataflow framework conservatively discards facts from the dataflow store. With these annotations, if the side effect expression's @WritesFields annotation is disjoint from the @ReadsFields annotation of the expression for which a dataflow fact is known, then the dataflow fact is retained rather than discarded. This is what issue Restricted side effects: @SideEffectFreeExcept or @WritesFields #984 is getting at, though that issue doesn't give as many details as what I have provided here.

I'm leaving this issue open because we would like to solve it. Anyone who wants to can contribute a pull request that implements one of the possible fixes.
In the meanwhile, the existence of a workaround means this is not a blocking issue.