Confusing behavior with @CreatesMustCallFor

[jacek-lewandowski]

I have this class (relevant part):

@InheritableMustCall("disconnect")
public class JavaDriverClient
{
    private @Owning Cluster cluster;
    private @Owning Session session;

    @CreatesMustCallFor
    public void connect(ProtocolOptions.Compression compression) throws Exception
    {

        disconnect();
        cluster = clusterBuilder.build();
        session = cluster.connect();
    }

    @EnsuresCalledMethods(value = {"cluster", "session"}, methods = "close")
    public void disconnect()
    {
        session.close();
        session = null;
        cluster.close();
        cluster = null;
    }
}

and the checker fails with the following exception:

    [javac] /home/jlewandowski/dev/cassandra/c18239-static-analysis/tools/stress/src/org/apache/cassandra/stress/util/JavaDriverClient.java:203: error: [builder:required.method.not.called] @MustCall method close may not have been invoked on field session or any of its aliases.
    [javac]         session = cluster.connect();
    [javac]                 ^
    [javac]   The type of object is: com.datastax.driver.core.Session.
    [javac]   Reason for going out of scope:  Non-final owning field might be overwritten

It refers to the session = cluster.connect(); in connect method. It shouldn't because disconnect() was called before. However, it only allows to overwrite cluster after disconnect() and any additional owned resource cannot be overwritten.

[kelloggm]

@jacek-lewandowski Sorry I missed this issue when you initially filed it!

I think the issue here might be that the checker is implicitly assuming that clusterBuilder.build() may be able to assign session, so it is invalidating the information it gains from the @EnsuresCalledMethods annotation on disconnect(). Basically, the checker's information looks like this (checker information in [] between lines:

    public void connect(ProtocolOptions.Compression compression) throws Exception
    {
        disconnect();
// [ session -> @CalledMethods("close"), cluster -> @CalledMethods("close") ]
        cluster = clusterBuilder.build(); // what if build() can assign session, because of secret evil aliasing?
// [ session -> @CalledMethods({}), cluster -> @CalledMethods({}) ]
        session = cluster.connect(); // session cannot be assigned anymore, because it's no longer provable that it has been closed
    }

You can tell the checker that build() cannot assign session by writing an @Pure or @SideEffectFree annotation on it; unfortunately, these annotations are trusted rather than checker by default, so this is similar to suppressing a warning. Since they aren't checked, you should probably only do that if build() really does not have side-effects (and, if you write @Pure, is deterministic). If not, you'll have to suppress the warning (with a comment indicating why you believe that build() doesn't assign session and so the disconnect() call's information is still valid.

This sort of problem is a consequence of the checker's conservatism: in the absence of a specification that says otherwise, it assumes any call to another method invalidates any information it is holding about fields.

[kelloggm]

There is a longer explanation of this issue in the manual here: https://checkerframework.org/manual/#type-refinement-purity, if you'd like to read more.