Record accessor Pure handling is incorrect

[neilccbrown]

There are a few bugs in the handling of record accessors and @Pure. They are technically separate bugs but they closely relate (and I have a pull request ready to address them all) so I'll put all three of them here:

Record accessors are not always treated as @Pure like they should be:

record Pair(@Nullable String first, @Nullable String second)
{
    public String example()
    {
        if (first() == null || second() == null)
            return "";
        else
            // This gives an error but should not because all methods involved are @Pure:
            return "" + first().length() + " " + second().length();
    }
}

Pull request #5205 partially addressed this but not in all cases in the flow/value handling. The example works if you only check+use first() or only second().

Record methods with the same name as an accessor are treated like an accessor but they should not be:

record Pair(@Nullable String first, @Nullable String second)
{
    // An unrelated non-pure method of same name:
    public @Nullable String first(List<String> ss)
    {
        return ss.isEmpty() ? null : ss.get(0);
    }

    public String checkPurityOfImpureMethod()
    {
        List<String> ss = List.of();
        if (first(ss) == null)
            return "";
        else
            // This should throw an exception but does not because first is assumed @Pure:
            return "" + "".length() + first(ss).length();
    }
}

Manually written accessors are always be treated as pure even if they are not marked as such:

record Wrapper(@Nullable List<String> items)
{
    // Not @Pure:
    public @Nullable List<String> items()
    {
        if (items != null) items.clear();
        return items;
    }

    public String example()
    {
        if (items() == null)
            return "";
        else
            // Should throw an exception but doesn't due to items() being considered @Pure
            return "" + items().size();
    }
}

(This last one is admittedly inadvisable as record accessors shouldn't have side effects. But it seems like the framework should support it if the user really wants to do it. Assuming they are @Pure seems like a bug rather than an intended feature.)

This all affects version 3.26.0.

[mernst]

Thanks for noticing these problems (and for the forthcoming fix!).

[neilccbrown]

Incidentally, I tried the obvious work-around for the first bug by introducing an explicit accessor with the @Pure annotation. If you do this on a generic type, like so, even without the annotation:

record Pair<A, B>(A first, B second)
{
    public A first() { return first; }
}

You get a javac compiler error:

error: invalid accessor method in record Pair
    public A first() { return first; }
         ^
  (return type of accessor method first() must match the type of record component first)
  where A is a type-variable:
    A extends Object declared in record Pair

I've now discovered that this is a compiler bug that only occurs when a processor is present. I found it quite confusing why the error came straight from javac but then I couldn't reproduce it outside of projects using the checker framework! Will be fixed in JDK 20 but it could bite checker framework users in the mean time.