RLC crashes when a class extends a MustCall Empty class

[Nausheen15]

@MustCall()
class NoMustCall {
}

@MustCall("close")
public class ExtendsMustCallEmpty extends NoMustCall {
    @Owning Socket socket;

    @EnsuresCalledMethods(value = "this.socket", methods = "close")
    void close() {
        try{
            socket.close();
        }
        catch (Exception e){
        
        }
    }
}

The Resource Leak Checker crashes on the above program. Here is the output.txt of the crash.
However, when I remove the MustCall() annotation from class NoMustCall, there is no crash or error. It does not even give the declaration.inconsistent.with.extends.clause error that is expected. Isn't that unsound?

[kelloggm]

The Resource Leak Checker crashes on the above program. Here is the output.txt of the crash.

Thanks for reporting this. Fixed by #6578.

However, when I remove the MustCall() annotation from class NoMustCall, there is no crash or error. It does not even give the declaration.inconsistent.with.extends.clause error that is expected. Isn't that unsound?

It's not unsound (and it's the intended design). Consider the fact that java.lang.Object is @MustCall({}), but all classes in Java (including e.g., java.net.Socket) extend it somehow.

The key idea for why this design is sound is that it's not possible to assign a concrete object of type ExtendsMustCallEmpty into a location whose type is NoMustCall unless you annotate the latter location: you will get an incompatible assignment error at whatever assignment/pseudo-assignment actually permits the subclass value to flow into the superclass-typed location. So, for example, this code is okay:

@MustCall("close") NoMustCall myObject = new ExtendsMustCallEmpty();

But this code is not:

NoMustCall myObject = new ExtendsMustCallEmpty();

[Nausheen15]

I see. That makes sense. Thanks for clarifying this and fixing the issue so quickly!

I tried to check the following code reading your comment but I did not get any incompatible assignment error. Is there something I am missing?

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

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

class NoMustCall {
    void close() {
    }
}

@MustCall("close")
public class ExtendsMustCallEmpty extends NoMustCall {
    @Owning Socket socket;

    ExtendsMustCallEmpty() {
        try{
            if(socket != null)
                socket.close();
            socket = new Socket("localhost", 8080);
        }
        catch (Exception e){
        
        }
    }

    @EnsuresCalledMethods(value = "this.socket", methods = "close")
    void close() {
        try{
            socket.close();
        }
        catch (Exception e){
        
        }
    }

}

class MainMethod {
    public static void main(String[] args) throws IOException {
        NoMustCall n = new ExtendsMustCallEmpty();
        n.close();
    }
}

[kelloggm]

@Nausheen15 I ran the checker on the following full test case, which is based on your example with minimum modifications that are necessary so that the Java compiler accepts it. The expected error on line 26 is issued.

// test for the crash in https://github.com/typetools/checker-framework/issues/6576

import java.net.Socket;
import org.checkerframework.checker.calledmethods.qual.*;
import org.checkerframework.checker.mustcall.qual.*;

@SuppressWarnings("all") // only check for crashes
public class Issue6576 {

  @MustCall() static class NoMustCall {}

  @MustCall("close") static class ExtendsMustCallEmpty extends NoMustCall {
    @Owning Socket socket;

    @EnsuresCalledMethods(value = "this.socket", methods = "close")
    void close() {
      try {
        socket.close();
      } catch (Exception e) {

      }
    }
  }

  public static void main(String[] args) {
    // error: assignment
    NoMustCall n = new ExtendsMustCallEmpty();
  }
}

[Nausheen15]

@kelloggm The error generated has the following error message @MustCall method close may not have been invoked on n or any of its aliases.. which seems to say that the problem is not with the assignment but in the missing close.

Here the super class also implements close and close is called on n. Though, there is no resource leak in this code (since the subclass close is the one actually called at runtime) I'd expect a type error at the assignment but this program doesn't give me any errors.

[kelloggm]

@Nausheen15 sorry, I definitely made a mistake when I wrote my previous comment - I left a warning suppression in place (on line 6) that was hiding the error that you're talking about. When I remove it, I see the same behavior.

which seems to say that the problem is not with the assignment but in the missing close.

That we see a required.method.not.called error and not an assignment error here is caused by the local variable defaulting rules: the @MustCall("close") annotation from the constructor is automatically added to the local variable declaration of n as a refinement, following the standard CLIMB-to-top defaulting rules. I should have realized that before, sorry.

To see an assignment error, we'd need to make n a non-CLIMB location, such as by making it a field.

#6576 (comment) the super class also implements close and close is called on n. Though, there is no resource leak in this code (since the subclass close is the one actually called at runtime) I'd expect a type error at the assignment but this program doesn't give me any errors.

I think there's more to the example that you're actually thinking of than is present in the code you've linked, because in the code you've linked the superclass does not implement close (it has an empty body), and so the whole piece of code isn't compilable.

[Nausheen15]

Oh I didn't know of the CLIMB-to-top rule. This was very helpful. Thanks!

Sorry, I forgot to add the required imports in my example perhaps that's why you couldn't compile it. I've edited my earlier comment to include them now. The updated code should be compilable.
The empty close was added so that I could call close on n and remove the missing mustcall error.

I also tried replacing the assignment statement with @Mustcall() NoMustCall = new ... and observed the expected incompatible assignment error. Thanks for helping me understand this once again!