Unsoundness in MustCallChecker (and RLC) for functional interfaces

[Calvin-L]

This example creates a Closeable functional interface and makes new instances of it in a few sneaky ways:

• normal inner class
• inline inner class
• anonymous class
• lambda expression
• method reference

// Test that the correct type is assigned to instantiations of functional
// interfaces.

import java.io.Closeable;
import org.checkerframework.checker.mustcall.qual.*;

public abstract class FunctionalInterfaces {

  @FunctionalInterface
  public interface Actor extends Closeable {
    void act();

    @Override
    default void close() {
    }
  }

  public static class ActorImpl implements Actor {
    @Override
    public void act() {
    }
  }

  public abstract void run(@MustCall({}) Actor a);

  public static void method() {
  }

  public void normalConstruction() {

    // :: error: (assignment)
    @MustCall({}) Actor a = new ActorImpl();

  }

  public void inlineClass() {

    class ActorImplInline implements Actor {
      @Override
      public void act() {
      }
    }

    // :: error: (assignment)
    @MustCall({}) Actor a = new ActorImplInline();

  }

  public void anonymousClass() {

    // :: error: (assignment)
    @MustCall({}) Actor a = new Actor() {
      public void act() {
      }
    };

  }

  public void lambda() {

    // :: error: (assignment)
    @MustCall({}) Actor a = () -> {
    };

  }

  public void methodRef() {

    // :: error: (assignment)
    @MustCall({}) Actor a = FunctionalInterfaces::method;

  }

}

I would expect all 5 cases would report an error, but only the first two do:

checker/tests/mustcall/FunctionalInterfaces.java:32: error: [assignment] incompatible types in assignment.
    @MustCall({}) Actor a = new ActorImpl();
                            ^
  found   : @MustCall("close") ActorImpl
  required: @MustCall Actor
checker/tests/mustcall/FunctionalInterfaces.java:45: error: [assignment] incompatible types in assignment.
    @MustCall({}) Actor a = new ActorImplInline();
                            ^
  found   : @MustCall FunctionalInterfaces.@MustCall("close") ActorImplInline
  required: @MustCall Actor
2 errors

I did my best to debug this one, but the problem actually seems to be in the "framework" part of the Checker Framework, and not in the Must Call Checker specifically---although I'm not quite knowledgeable enough to know for sure. It seems like new ClassName() is always assigned the correct type @MustCall({"close"}), but other ways of constructing an instance of the class do not get the right inherited annotations.

[msridhar]

I just looked into the anonymous class case for a bit. I think maybe the issue is in org.checkerframework.framework.type.AnnotatedTypeFactory#constructorFromUse(com.sun.source.tree.NewClassTree, boolean):

https://github.com/typetools/checker-framework/blob/e1dc97327eab2e704bbae3ff9aac5fc08a267a82/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java#L2759-L2759

For the NewClassTree I see a @MustCall("close") qualifier getting added by addComputedTypeAnnotations to type:

https://github.com/typetools/checker-framework/blob/e1dc97327eab2e704bbae3ff9aac5fc08a267a82/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java#L2783-L2783

But for the anonymous class case, this qualifier never gets properly added to the type of the con local. So, at the end of the method, I can still see that type has the @MustCall("close") qualifer but con does not.

@smillst does the above look like a problem to you?

[smillst]

Yes, I've got a fix: https://github.com/typetools/checker-framework/pull/6837.

[smillst]

Lambda and method reference cases are trickier. I'm still thinking about them.

[smillst]

I'm not convinced that the lambda and the method reference examples should issue warnings. Can you give an example where resource leak occurs using a lambda or method reference?

[Calvin-L]

It's a little contrived, but maybe something like this:

abstract class ResourceLambda {

    public void go(Path f) throws IOException {

        InputStream in = Files.newInputStream(f);
        runAndThen(in::close);

    }

    @FunctionalInterface
    @InheritableMustCall("close")
    public interface CloseProcedure {
        void close() throws IOException;
    }

    abstract void runAndThen(CloseProcedure closeProcedure);

}

The resource in will leak if the lambda's method is not called.

There is no way to annotate this code so that it passes, but it illustrates that a @FunctionalInterface might own some resource that needs closing.

Aside from resource leaks, I can imagine (subversive?) uses of the RLC to ensure that a program eventually calls certain methods---even if the reason for calling those methods is something other than "close file descriptors".

[Calvin-L]

Although, it might be best for the RLC to reject the lambda and methodRef cases entirely, on the grounds that they are probably not doing what the programmer intended. (Specifically, I am not sure the JVM guarantees to allocate a new object every time it evaluates a lambda expression. 🤔 )

[msridhar]

Aside from resource leaks, I can imagine (subversive?) uses of the RLC to ensure that a program eventually calls certain methods---even if the reason for calling those methods is something other than "close file descriptors".

I would not call this subversive. We always had an idea of others potentially using this checker for other "must-call" methods that do not necessarily relate to resource leaks. In fact, I worked with an undergrad to tinker around with using the RLC to check always-unlock-after-lock properties with Java ReentrantLocks. (It didn't seem to work out due to uses in fields that the RLC doesn't handle all that well, though we didn't push it too hard.)

Although, it might be best for the RLC to reject the lambda and methodRef cases entirely, on the grounds that they are probably not doing what the programmer intended. (Specifically, I am not sure the JVM guarantees to allocate a new object every time it evaluates a lambda expression. 🤔 )

I'm not sure about this either. It does seem to me that if we could fix the computed must-call types of lambdas and method refs that might be good in general, potentially for future type systems also.

[smillst]

It does seem to me that if we could fix the computed must-call types of lambdas and method refs that might be good in general, potentially for future type systems also.

The types are computed correctly, they just aren't checked. (Checking an assignment of a lambda or a method reference checks for congruence.) See
BaseTypeVisitor#commonAssignmentCheck(AnnotatedTypeMirror, ExpressionTree, String, Object...). You could override this to add back the usual common assignment check.