Unable to verify EnsuresCalledMethods

[Nausheen15]

The following code generates the below error with the resource leak checker.

import java.io.IOException;
import java.net.Socket;

import org.checkerframework.checker.calledmethods.qual.*;
import org.checkerframework.checker.mustcall.qual.*;

public class UnifiedSocket extends Socket {
    private @Owning Socket socket1;
    private @Owning Socket socket2;

    @Override
    @EnsuresCalledMethods(value="this.socket1", methods="close")
    @EnsuresCalledMethods(value="this.socket2", methods="close")
    public synchronized void close() throws IOException {
        try{
            if (socket1 != null) {
                socket1.close();
            }
        }
        finally {
            if (socket2 != null) {
                socket2.close();
            }
        }
    }
}

UnifiedSocket.java:14: error: [contracts.postcondition] postcondition of close is not satisfied.
    public synchronized void close() throws IOException {
                             ^
  found   : no information about this.socket1
  required: this.socket1 is @CalledMethods("close")

Why does the checker complain of no information about this.socket1, though it is closed? What is the right way to close the two sockets such that the checker can verify both the annotations?

I am using version 3.43.0 of the checker framework. Also, I would appreciate it if someone could point me to the library annotations for the Socket class. Thanks!

[kelloggm]

Why does the checker complain of no information about this.socket1, though it is closed?

I think it's complaining because socket2.close() might have arbitrary side-effects, and so the checker removes information about non-final fields from the local store (that is, it loses the fact that socket1.close() was called earlier in the method).

What is the right way to close the two sockets such that the checker can verify both the annotations?

Here are some test files from the RLC's test suite that should be useful for you to see what the checker can and cannot verify:

• this test seems to be the closest to what you're trying to do. The big difference there is that the Sockets are final; the requirements for closing non-final fields are stronger, due to the possible presence of side-effects. Here is an unsafe version of the same code.
• Here is a version where the destructors are separate (i.e., each socket has its own close method). This might or might not be useful to you.
• this example is probably closest to what you're trying to do. It has extensive comments explaining why it can't be verified.

Also, I would appreciate it if someone could point me to the library annotations for the Socket class

Here are the standard @MustCall annotations used by the RLC. These are kept separate from the main JDK because they're unsound if the RLC isn't going to run with obligation creation support. The rest of the annotations are in the annotated JDK.

Hope this helps, and happy to answer any other questions!

[Nausheen15]

Thanks for the detailed reply.
I was wondering if a method call does assign something to socket1, then wouldn't it be annotated with CreatesMustCallFor(socket1) ? I would expect the fact that socket2.close() will not have such an annotation should be enough to retain that socket1.close() was indeed called earlier. Could you explain why this could be unsound?

[kelloggm]

I was wondering if a method call does assign something to socket1, then wouldn't it be annotated with CreatesMustCallFor(socket1) ? I would expect the fact that socket2.close() will not have such an annotation should be enough to retain that socket1.close() was indeed called earlier. Could you explain why this could be unsound?

The checker might be overly conservative here; I haven't thought in detail about whether the absence of an @CreatesMustCallFor annotation could be treated as evidence that no side-effects to resource-carrying variables are performed. (The behavior of clearing the stores when a side-effectful method is called is inherited from the framework, not specific to the RLC, and we haven't looked into whether there is a justification for changing it.)

[Nausheen15]

I see, thanks for clarifying. I have a slightly unrelated question about the library annotations for the Socket class.

I see an @EnsuresCalledMethodsIf(expression="this", result=true, methods={"close"}) annotation on the isClosed method. I suppose that this will help verifying a client that closes a socket only when it isn't already closed. However, the manual defines it as an annotation added when close() is actually called in the annotated method's body which isn't the case for isClosed. Could you please explain why you chose to annotate it this way?

[kelloggm]

However, the manual defines it as an annotation added when close() is actually called in the annotated method's body which isn't the case for isClosed

That's a fair point. However, because isClosed will only return true on which close() was called at some point in the past, the technical meaning of @CalledMethods is preserved. Maybe the manual should be clarified to allow this case, because this is often something we want to do when writing specifications for libraries. You're right that the checker wouldn't be able to verify this annotation if we'd written it on a custom class with the same API as Socket.

Could you please explain why you chose to annotate it this way?

The reason is exactly the one that you gave - that is:

this will help verifying a client that closes a socket only when it isn't already closed

[Nausheen15]

Makes sense. I have no further questions. Thank you for your prompt response!

[jyoo980]

Closing this issue, since all questions have been answered.