WPI: Unverifiable purity annotations are added to methods that are overridden by impure methods

[kelloggm]

Test case on this branch: kelloggm:purity-bad-override-wpi

WPI currently infers (and -AsuggestPureMethods suggests) purity annotations that are true of a particular implementation of a method, but not true of other methods in the same codebase that override that method. For example, consider the following pair of classes:

  class Foo {

    // This version is pure.
    String getA(int x) {
      return "A";
    }
  }

  class Bar extends Foo {

    String y;

    // This version is neither deterministic nor side-effect free.
    @java.lang.Override
    String getA(int x) {
      if (new Random().nextInt(5) > x) {
        return "B";
      } else {
        y = "C";
        return y;
      }
    }
  }

WPI currently infers @Pure for Foo#getA, which results in four spurious warnings in Bar#getA, because Bar#getA isn't pure.

(the warnings are the following:

      OverrideIncompatiblePurity.java:24: warning: (purity.not.deterministic.object.creation)
      OverrideIncompatiblePurity.java:24: warning: (purity.not.sideeffectfree.call)
      OverrideIncompatiblePurity.java:24: warning: (purity.not.deterministic.not.sideeffectfree.call)
      OverrideIncompatiblePurity.java:27: warning: (purity.not.deterministic.not.sideeffectfree.assign.field)

)

My expectation is that WPI will only infer verifiable purity annotations.

This problem is common in real projects, so I'd like to find a solution, even if it means WPI infers many fewer purity annotations. I attempted to implement a naive approach that uses a "lub" of the purity annotations on all overriding methods, but I could not find a way to implement that without doing major surgery (and it got very messy, very quickly, because "top" in a "hierarchy" of purity annotations is "no purity annotation", and it's not clear in the implementation when encountering a method with no annotation if that means "this method is impure" or "this method has not yet been analyzed in this WPI round").

One possible short term kludge would be to never infer purity annotations on non-final methods. Obviously, that's not ideal, but it would definitely avoid this problem.

A long term solution is to rework the purity checker as a typechecker with a proper type hierarchy, which would allow us to distinguish "impure" from "unqualified".

@mernst thoughts on how we should proceed here?

[kelloggm]

This problem also occurs for interfaces, which might present another challenge. Consider the following (which I've now checked into the same test case on the same branch):

  interface MyInterface {
    // WPI should definitely not infer @Pure for this unless all
    // implementations are pure.
    void method();
  }
  
  class MyImplementation implements MyInterface {

    int field;
    
    @java.lang.Override
    public void method() {
      // Side effect!
      field = 5;
    }
  }

This results in this warning:

      OverrideIncompatiblePurity.java:22: warning: (purity.not.sideeffectfree.assign.field)

The warning is caused by WPI inferring @SideEffectFree in the interface.