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

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?

Start with the test case on the kelloggm:purity-bad-override-wpi branch and reproduce the warnings for OverrideIncompatiblePurity.java using WPI and -AsuggestPureMethods. Read the WPI purity inference and purity checker behavior around overridden methods and unannotated methods. Done means inferred purity annotations are verifiable across overrides and the spurious warnings no longer occur.