RLC: Handling CreatesMustCall on NotOwning fields

[Nausheen15]

This program creates a MustCall on a NotOwning field and tries to satisfy it by calling n.nos.close(). I would expect this to have no errors but the checker's output is NotOwningCreatesMustCallFor.java:25: error: [reset.not.owning] Calling method bar resets the must-call obligations of the expression n.nos, which is non-owning. Either annotate its declaration with an @Owning annotation, extract it into a local variable, or write a corresponding @CreatesMustCallFor annotation on the method that encloses this statement. n.bar();
Is this a pattern the checker cannot handle or are NotOwning fields not supposed to have CreatesMustCallFor?

public class NotOwningCreatesMustCallFor {
    final Socket nos;

    public NotOwningCreatesMustCallFor(final Socket a) {
        nos = a;
    }

    @CreatesMustCallFor("this.nos")
    public void bar() throws IOException {
        nos.connect(null);
    }
}

class MainMethod {
    public static void main(String[] args) throws IOException {
        final Socket s = new Socket("localhost", 8080);
        NotOwningCreatesMustCallFor n = new NotOwningCreatesMustCallFor(s);
        
        try{
            n.bar();
        }
        catch (Exception e){
        }
        s.close();   
        n.nos.close();
    }
}

[kelloggm]

Is this a pattern the checker cannot handle or are NotOwning fields not supposed to have CreatesMustCallFor?

This is intentional: non-owning fields cannot be the target of a @CreatesMustCallFor annotation. The reason is that the checker doesn't enforce must-call obligations on non-owning fields, so while a must-call obligation for the field would be created by your code, the RLC wouldn't know to enforce that obligation.

The code example you provided looks similar to some "unconnected sockets" cases that we've seen before, and which partially motivated the creation of @CreatesMustCallFor. The way that I would annotate this code snippet is the following, which passes the checker:

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

import java.net.*;
import java.io.*;

public class NotOwningCreatesMustCallFor {
    // This socket is initially unconnected, but becomes owning
    // as soon as bar() is called.
    final @Owning @MustCall({}) Socket nos;

    public NotOwningCreatesMustCallFor(final @MustCall({}) Socket a) {
        nos = a;
    }

    @CreatesMustCallFor("this.nos")
    public void bar() throws IOException {
	// TODO: add details about what to connect to here
        nos.connect(null);
    }
}

class MainMethod {
    public static void main(String[] args) throws IOException {
	// Important: s here must actually not be connected to anything.
	// The RLC can't reason about the specific arguments to the socket
	// constructor, so conservatively we can only call the no-argument
	// constructor to create an unconnected socket.
        final Socket s = new Socket(); // = new Socket("localhost", 8080);
        NotOwningCreatesMustCallFor n = new NotOwningCreatesMustCallFor(s);
        
        try{
            n.bar();
        }
        catch (Exception e){
        }
        s.close();   
        n.nos.close();
    }
}

Note that I had to make a couple of changes to how the socket is initialized/connected - using a socket in this style requires us to defer providing the actual connection information until we call connect (or bind or a similar method).

[kelloggm]

One more thing I just realized: we can also make the parameter to the constructor @Owning and then remove the (duplicate) close call for s at the end.

[Nausheen15]

Thanks for clarifying this!