Closed Nausheen15 closed 1 month ago
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:
Socket
s 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.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!
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?
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.)
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?
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
Makes sense. I have no further questions. Thank you for your prompt response!
Closing this issue, since all questions have been answered.
The following code generates the below error with the resource leak checker.
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!