Unexpected required.method.not.called when implementing a resources collection/map

[jacek-lewandowski]

So I was trying to implement a resources map to be used to such situations, I have this:

@InheritableMustCall({ "removeAll" })
public class ResourcesMap<K, V>
{
    private final Map<K, V> map;

    public ResourcesMap()
    {
        this.map = new HashMap<>();
    }

    public @MustCallAlias V get(K key)
    {
        return map.get(key);
    }

    public @Owning V remove(K key)
    {
        return map.remove(key);
    }

    @CreatesMustCallFor
    public @MustCallAlias V put(K key, @Owning V value)
    {
        return map.put(key, value);
    }

    public void forEach(Consumer<@MustCallAlias V> consumer)
    {
        map.values().forEach(consumer);
    }

    public <T> void removeAll(T initial, OwningBiFunction<T, V> consumer)
    {
        Iterator<V> iterator = map.values().iterator();
        T acc = initial;
        while (iterator.hasNext())
        {
            V value = iterator.next();
            try
            {
                iterator.remove();
            }
            finally
            {
                acc = consumer.apply(acc, value);
            }
        }
    }

    public <T> void removeAll(OwningConsumer<V> consumer)
    {
        Iterator<V> iterator = map.values().iterator();
        while (iterator.hasNext())
        {
            V value = iterator.next();
            try
            {
                iterator.remove();
            }
            finally
            {
                consumer.accept(value);
            }
        }
    }

    public interface OwningConsumer<V> extends Consumer<V>
    {
        @Override
        void accept(@Owning V v);
    }

    public interface OwningBiFunction<T, V> extends BiFunction<T, V, T>
    {
        @Override
        T apply(T t, @Owning V v);
    }
}

which is used in the following way:

        ResourcesMap<TableId, UncommittedTableData.FlushWriter> flushWriters = new ResourcesMap<>();
        try (CloseableIterator<PaxosKeyState> iterator = updateSupplier.flushIterator(paxos))
        {
            while (iterator.hasNext())
            {
                PaxosKeyState next = iterator.next();
                UncommittedTableData.FlushWriter writer = flushWriters.get(next.tableId);
                if (writer == null)
                {
                    writer = getOrCreateTableState(next.tableId).flushWriter();
                    flushWriters.put(next.tableId, writer);
                }
                writer.append(next);
            }

            flushWriters.removeAll(UncommittedTableData.FlushWriter::finish);
        }
        catch (IOException t)
        {
            flushWriters.removeAll((Throwable) t, (acc, flushWriter) -> flushWriter.abort((acc)));
            throw new IOException(t);
        }

where the FlushWriter is something like:

    @InheritableMustCall({ "finish", "abort" })
    public interface FlushWriter
    {
        void append(PaxosKeyState commitState) throws IOException;

        void finish();

        Throwable abort(Throwable accumulate);

        default void appendAll(Iterable<PaxosKeyState> states) throws IOException
        {
            for (PaxosKeyState state : states)
                append(state);
        }
    }

Now, when I try to check it, it complains with the following:

    [javac] /home/jlewandowski/dev/cassandra/c18190-ecj/src/java/org/apache/cassandra/service/paxos/uncommitted/PaxosUncommittedTracker.java:161: error: [builder:required.method.not.called] @MustCall methods removeAll, finish, abort may not have been invoked on flushWriters or any of its aliases.
    [javac]         ResourcesMap<TableId, UncommittedTableData.FlushWriter> flushWriters = new ResourcesMap<>();
    [javac]                                                                 ^
    [javac]   The type of object is: org.apache.cassandra.utils.ResourcesMap<org.apache.cassandra.schema.TableId,org.apache.cassandra.service.paxos.uncommitted.UncommittedTableData.FlushWriter>.
    [javac]   Reason for going out of scope: possible exceptional exit due to throw new IOException(t); with exception type java.io.IOException

I'm not sure what I'm doing wrong there?

[jacek-lewandowski]

@msridhar do you think it is possible to fix it for the upcoming release? Or maybe you can suggest some workaround? I'm sorry, I know that Apache Cassandra is a demanding project for this kind of tools but we believe your tool will help use significantly improve the code :)

[kelloggm]

Hi @jacek-lewandowski, I took a look at this example. I don't think it indicates a bug in the checker per se: rather, I think the issue here is that the error message was confusing. The confusing-ness of the error message was in turn caused by the use of @MustCallAlias annotations on things that aren't actually resource aliases: in particular, on the map's get and put methods.

Here is a version of the program that compiles with no warnings on master (other than the new one that I've suppressed that was introduced in #5912, but there's nothing we can do about that one). I've stubbed out all of the classes that are used so that I could run the checker on this test on its own - hopefully they match the real ones closely enough.

I want to draw your attention to the most important change: I've replaced or removed all of the @MustCallAlias annotations. Most of them were replaced by @NotOwning annotations, since my understanding of this code is that calling removeAll on the map is the intended way to close out the resources.

// Test case for https://github.com/typetools/checker-framework/issues/6054

import java.io.*;
import java.util.*;
import java.util.function.*;
import org.checkerframework.checker.mustcall.qual.*;

@InheritableMustCall({"removeAll"})
public class ResourcesMap<K, V> {
  private final Map<K, V> map;

  public ResourcesMap() {
    this.map = new HashMap<>();
  }

  @NotOwning
  public V get(K key) {
    return map.get(key);
  }

  public @Owning V remove(K key) {
    return map.remove(key);
  }

  @CreatesMustCallFor
  @NotOwning
  public V put(K key, @Owning V value) {
    return map.put(key, value);
  }

  public void forEach(Consumer<V> consumer) {
    map.values().forEach(consumer);
  }

  public <T> void removeAll(T initial, OwningBiFunction<T, V> consumer) {
    Iterator<V> iterator = map.values().iterator();
    T acc = initial;
    while (iterator.hasNext()) {
      V value = iterator.next();
      try {
        iterator.remove();
      } finally {
        acc = consumer.apply(acc, value);
      }
    }
  }

  public <T> void removeAll(OwningConsumer<V> consumer) {
    Iterator<V> iterator = map.values().iterator();
    while (iterator.hasNext()) {
      V value = iterator.next();
      try {
        iterator.remove();
      } finally {
        consumer.accept(value);
      }
    }
  }

  public interface OwningConsumer<V> extends Consumer<V> {
    @Override
    void accept(@Owning V v);
  }

  public interface OwningBiFunction<T, V> extends BiFunction<T, V, T> {
    @Override
    T apply(T t, @Owning V v);
  }

  @InheritableMustCall({"finish", "abort"})
  public interface FlushWriter {
    void append(PaxosKeyState commitState) throws IOException;

    void finish();

    Throwable abort(Throwable accumulate);

    default void appendAll(Iterable<PaxosKeyState> states) throws IOException {
      for (PaxosKeyState state : states) append(state);
    }
  }

  public static void test(UpdateSupplier<PaxosKeyState> updateSupplier, PaxosKeyState paxos)
      throws IOException {
    // This warning suppression is necessary because of #5912's changes to defaulting.
    // Logically, what's happening here is that satisfying flushWriters' obligation
    // will satisfy the obligations of each of the FlushWriters it contains.
    @SuppressWarnings("mustcall:type.argument")
    ResourcesMap<TableId, FlushWriter> flushWriters = new ResourcesMap<>();
    try (CloseableIterator<PaxosKeyState> iterator = updateSupplier.flushIterator(paxos)) {
      while (iterator.hasNext()) {
        PaxosKeyState next = iterator.next();
        FlushWriter writer = flushWriters.get(next.tableId);
        if (writer == null) {
          writer = getOrCreateTableState(next.tableId).flushWriter();
          flushWriters.put(next.tableId, writer);
        }
        writer.append(next);
      }

      flushWriters.removeAll(FlushWriter::finish);
    } catch (IOException t) {
      flushWriters.removeAll((Throwable) t, (acc, flushWriter) -> flushWriter.abort((acc)));
      throw new IOException(t);
    }
  }

  static class TableState {
    FlushWriter flushWriter() {
      return null;
    }
  }

  static TableState getOrCreateTableState(TableId tableId) {
    return null;
  }

  static class PaxosKeyState {
    // stub added to permit compilation
    TableId tableId;
  }

  static class CloseableIterator<T> implements AutoCloseable {

    T next() {
      return null;
    }

    boolean hasNext() {
      return false;
    }

    public void close() throws IOException {
      // do nothing
    }
  }

  interface TableId {}

  interface UpdateSupplier<T> {
    CloseableIterator<T> flushIterator(T t);
  }
}

[msridhar]

I'm sorry, I know that Apache Cassandra is a demanding project for this kind of tools but we believe your tool will help use significantly improve the code :)

No need to apologize; we are really excited that the Resource Leak Checker could be useful for an important project like Cassandra! Please keep filing issues and letting us know pain points, and we will address them as soon as we can.

[msridhar]

@kelloggm

I took a look at this example. I don't think it indicates a bug in the checker per se: rather, I think the issue here is that the error message was confusing. The confusing-ness of the error message was in turn caused by the use of @MustCallAlias annotations on things that aren't actually resource aliases: in particular, on the map's get and put methods.

Do the confusing error messages have the same root cause as #4947? It'd be great if we could somehow improve those.

[msridhar]

Also, while the checker may not report any warnings for @kelloggm's updated example, I'm not sure it is verifying the intended property. In particular:

1. We have @InheritableMustCall({"removeAll"}) on ResourcesMap, but that method is overloaded. I'm guessing our checker will verify that some removeAll() method is invoked; but we haven't really tested this, nor discussed what we want the annotation to mean in the presence of overloading. (We have related issue @CalledMethods doesn't distinguish between overloaded methods kelloggm/object-construction-checker#10 open from the original implementation of the Called Methods Checker; we should probably port it over to this repo.)
2. What is @InheritableMustCall({"finish", "abort"}) on FlushWriter intended to mean? I believe our intention was that both finish and abort should be called on any FlushWriter object. Reading the code, however, it looks like one or the other is invoked. So I'm not sure why the code passes the checker.

[kelloggm]

Do the confusing error messages have the same root cause as #4947?

Yes.

Reading the code, however, it looks like one or the other is invoked. So I'm not sure why the code passes the checker.

The warning about this is the one that I suppressed: the checker is not actually verifying anything about the FlushWriters here. All that's being verified in my version is that some removeAll method in ResourcesMap gets called.

[jacek-lewandowski]

Thanks for looking into that.

I must say I'm confused - the documentation says explicitly that it can be OR:

An expression of type @MustCall({"m1", "m2"}) may be obligated to call m1() and/or m2() before it is deallocated

We have a kind of a transaction-like object with different methods to commit or to discard. Therefore we expect either one or another method is called.

[jacek-lewandowski]

The trick with @NotOwning or upgrading to 3.36 works :)
I must admit I don't quite understand the difference between meaning of @NotOwning and @MustCallAlias

[kelloggm]

I must say I'm confused - the documentation says explicitly that it can be OR:

Sorry that this documentation is a bit confusing. Let me explain further (and if this is helpful in clarifying what @MustCall means, we can add it to the docs).

@MustCall({"a", "b"}) tells the checker that both a() and b() need to be called. However, a Must Call type is an overestimate of what might actually be required at run time---so a variable declared as @MustCall({"a", "b"}) is permitted at run time to evaluate to an expression that must call a(), must call b(), both, or neither---but not must call c() (or any other must call): that is, the set {a, b} is an upper bound on the possible must call obligations. The checker then enforces that all of the methods in the upper bound are called.

The checker doesn't currently have a way to express "this variable has a single must-call obligation, but that obligation can be satisfied by calling either a() or b()", which is subtly different (but corresponds to your actual use case, if I understand correctly). Probably the best workaround for this missing feature is to annotate the variable as @MustCall({"a"}) and then annotate b() as @EnsuresCalledMethods(expr="this", methods={"a"}) and suppress the ensuing warning (since presumably b doesn't actually call a). This would have the effect at the checker level of making any call to b() be treated as if it is also a call to a() and therefore fulfills the obligation.

I must admit I don't quite understand the difference between meaning of @NotOwning and @MustCallAlias

The key difference is that @NotOwning applies to a single variable/declaration: it says "there is no need to track this resource, since the annotated variable/declaration is just an alias that won't be used to fulfill the obligations". @MustCallAlias on the other hand is relative: a variable/declaration cannot be @MustCallAlias on its own, but must be @MustCallAlias'd with some other variable or declaration. It means "fulfilling the must-call obligations of one of the annotated elements is just as good as fulfilling the obligations of the other, so track them as if they were aliases." That's why it should always appear in pairs (such as on a parameter and a return type of a method, for example).

[jacek-lewandowski]

@MustCall({"a", "b"}) tells the checker that both a() and b() need to be called. However, a Must Call type is an overestimate of what might actually be required at run time---so a variable declared as @MustCall({"a", "b"}) is permitted at run time to evaluate to an expression that must call a(), must call b(), both, or neither---but not must call c() (or any other must call): that is, the set {a, b} is an upper bound on the possible must call obligations. The checker then enforces that all of the methods in the upper bound are called.

Let me say that my words:

@MustCall({"a", "b"})
class Test {
  void a();
  void b();
  void c();
}

@MustCall({"a"})      t = new Test(); // correct
@MustCall({"b"})      t = new Test(); // correct
@MustCall({"a", "b"}) t = new Test(); // correct
@MustCall({})         t = new Test(); // correct
@MustCall({"c"})      t = new Test(); // wrong

And the same pattern applies to subclasses. Do I understand that correctly?

The checker doesn't currently have a way to express "this variable has a single must-call obligation, but that obligation can be satisfied by calling either a() or b()", which is subtly different (but corresponds to your actual use case, if I understand correctly). Probably the best workaround for this missing feature is to annotate the variable as @MustCall({"a"}) and then annotate b() as @EnsuresCalledMethods(expr="this", methods={"a"}) and suppress the ensuing warning (since presumably b doesn't actually call a). This would have the effect at the checker level of making any call to b() be treated as if it is also a call to a() and therefore fulfills the obligation.

Yes, our use case is that we expect either one or another method is called. I have some idea you may consider - instead of pointing to the exact method name that must be called, let the user point to the user-defined or some predefined annotation - that is, must-call obligation would refer to any method annotated with that annotation. In our case it could look like this:

@MustCall({CloseMethod.class})
class Transaction {
  @CloseMethod
  void commit();

  @CloseMethod
  void abort();
}

Also, that approach would make project refactorings safer as the CheckerFramework would not need to base on quoted method names. WDYT?

The key difference is that @NotOwning applies to a single variable/declaration: it says "there is no need to track this resource, since the annotated variable/declaration is just an alias that won't be used to fulfill the obligations". @MustCallAlias on the other hand is relative: a variable/declaration cannot be @MustCallAlias on its own, but must be @MustCallAlias'd with some other variable or declaration. It means "fulfilling the must-call obligations of one of the annotated elements is just as good as fulfilling the obligations of the other, so track them as if they were aliases." That's why it should always appear in pairs (such as on a parameter and a return type of a method, for example).

Got it, thanks for explanation!

Sorry that this documentation is a bit confusing. Let me explain further (and if this is helpful in clarifying what @MustCall means, we can add it to the docs).

All those explanation are very useful to me, I fully support adding those notes to the docs :)

[msridhar]

Hi @jacek-lewandowski,

Let me say that my words:

@MustCall({"a", "b"})
class Test {
  void a();
  void b();
  void c();
}

@MustCall({"a"})      t = new Test(); // correct
@MustCall({"b"})      t = new Test(); // correct
@MustCall({"a", "b"}) t = new Test(); // correct
@MustCall({})         t = new Test(); // correct
@MustCall({"c"})      t = new Test(); // wrong

And the same pattern applies to subclasses. Do I understand that correctly?

I think this is reversed. You can see a figure depicting @MustCall subtyping here:

https://checkerframework.org/manual/#must-call-annotations

Basically, if A is a superset of B, then you can assign a value of type @MustCall(B) into a variable of type @MustCall(A). So with your same Test class, I think the answers are:

@MustCall({"a"})      t = new Test(); // wrong
@MustCall({"b"})      t = new Test(); // wrong
@MustCall({"a", "b"}) t = new Test(); // correct
@MustCall({})         t = new Test(); // wrong
@MustCall({"c"})      t = new Test(); // wrong
@MustCall({"a,b,c"})      t = new Test(); // correct

Yes, our use case is that we expect either one or another method is called. I have some idea you may consider - instead of pointing to the exact method name that must be called, let the user point to the user-defined or some predefined annotation - that is, must-call obligation would refer to any method annotated with that annotation. In our case it could look like this:

@MustCall({CloseMethod.class})
class Transaction {
  @CloseMethod
  void commit();

  @CloseMethod
  void abort();
}

Also, that approach would make project refactorings safer as the CheckerFramework would not need to base on quoted method names. WDYT?

I really like this idea! It's useful for a couple of reasons. First, it gives a possible workaround for the issue we currently have with method overloading (if there was a case where only one of the overloads serves as the @MustCall method). And yes, this makes the annotation less "stringly-typed" so the code is more robust to rename refactorings. Strictly speaking, supporting discovery of must-call methods via annotations and supporting calling any one of a set of must-call methods are two different things. For the latter, we may want to add a new class-level annotation like @MustCallAny, with the current @MustCall annotation meaning @MustCallAll.

Sorry that this documentation is a bit confusing. Let me explain further (and if this is helpful in clarifying what @MustCall means, we can add it to the docs).

All those explanation are very useful to me, I fully support adding those notes to the docs :)

Sure, we will work on this! FYI, a couple of us are fairly busy with other obligations through the month of July; we should have more cycles in early August to work on triaging and fixing all these issues. We are very grateful for all the reports.