Nullness Checker: support Q.isEmpty - Q.poll logic

[GoogleCodeExporter]

What steps will reproduce the problem?
1. Use the attached code.
2. javac -processor org.checkerframework.checker.nullness.NullnessChecker 
-proc:only XX.java

What is the expected output? What do you see instead?

Should accept the code - but instead gives this error (which is wrong).
XX.java:41: error: [contracts.conditional.postcondition.not.satisfied] the 
conditional postcondition about 'this.popCheapest()' at this return statement 
is not satisfied
        return _pq.isEmpty();
        ^
1 error


What version of the product are you using? On what operating system?
1.8.10 / OSX

Please provide any additional information below.

Original issue reported on code.google.com by [email protected] on 12 Feb 2015 at 12:20

Attachments:

• XX.java

[GoogleCodeExporter]

I don't see anything tying Queue#isEmpty or Queue#poll to the return value of 
popCheapest - this requires quite deep understanding of the code.

Original comment by [email protected] on 17 Mar 2015 at 5:10

• Changed state: Invalid

[GoogleCodeExporter]

Sounds like perhaps a problem with the PQ annotations then - because Q.isEmpty 
returns false is the Q still has an element, and thus Q.poll returns a non-null 
element.

Original comment by [email protected] on 17 Mar 2015 at 6:18

[GoogleCodeExporter]

Thanks for the comment, I see the point now.
I don't see this as a defect in @EnsuresNonNullIf, which does what it is 
supposed to. I changed the title accordingly.

I rather think we need additional logic to support the connection between 
Q.isEmpty and Q.poll, similarly to the connection between Map.get and 
Map.containsKey. None of the current pre/post-condition annotations is 
expressive enough to express such general logic. We will need something like

https://code.google.com/p/checker-framework/source/browse/checker/src/org/checke
rframework/checker/nullness/MapGetHeuristics.java

for Queues. (Note there is an updated version in our working repository right 
now.)

Original comment by [email protected] on 17 Mar 2015 at 3:19

• Changed title: Nullness Checker: support Q.isEmpty - Q.poll logic
• Changed state: Accepted
• Added labels: Type-Enhancement
• Removed labels: Type-Defect

[mernst]

Consider the following test case (which is committed to the repository):

import java.util.ArrayList;
import java.util.Queue;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

public final class IsEmptyPoll extends ArrayList<String> {

    void mNonNull(Queue<String> q) {
        while (!q.isEmpty()) {
            @NonNull String firstNode = q.poll();
        }
    }

    void mNullable(Queue<@Nullable String> q) {
        while (!q.isEmpty()) {
            // :: error: (assignment.type.incompatible)
            @NonNull String firstNode = q.poll();
        }
    }

    void mNoCheck(Queue<@Nullable String> q) {
        // :: error: (assignment.type.incompatible)
        @NonNull String firstNode = q.poll();
    }
}

The Nullness Checker considers all calls to poll() to return a possibly-null value, but the first one does not.

This cannot be handled via annotations in the JDK for two reasons.

1. Class LinkedList inherits isEmpty from AbstractCollection.
   That is, LinkedList.java does not contain a definition for isEmpty.

2. @EnsuresNonNullIf(result=false, "poll()") is an incorrect annation for isEmpty because actually the return type becomes E, which is not necessarily @NonNull.

Therefore, it must be handled by creating a new "non-empty" checker, which is analogous to the current Map Key Checker.

[mernst]

Here are some more implementation notes.

Precise handling of PriorityQueue.peek() and poll()

The Nullness Checker issues a false positive warning for this code:

import java.util.PriorityQueue;
import org.checkerframework.checker.nullness.qual.NonNull;

public class MyClass {
    public static void usePriorityQueue(PriorityQueue<@NonNull Object> active) {
        while (!(active.isEmpty())) {
            @NonNull Object queueMinPathNode = active.peek();
        }
    }
}

The Checker Framework does not determine that active.peek() returns a non-null value in this context.

The contract of peek() is that it returns a non-null value if the queue is not empty and the queue contains no null values.

To handle this code precisely, the Nullness Checker needs to know, for each queue, whether it is empty.
This is analogous to how the Nullness Checker tracks whether a particular value is a key in a map.

It should be handled the same way: by adding a new subchecker, called the Nonempty Checker to the Nullness Checker. Its types are:

• @UnknownNonEmpty -- the queue might or might not be empty
• @NonEmpty -- the queue is definitely non-empty

There is a start at this type-checker in branch nonempty-checker. It:

• defines the annotations
• creates the integration into the Nullness Checker

However, it is not done. (In fact, it doesn't even compile.) The NonEmpty Subchecker itself has not been written. This will be similar to, but simpler than, the Map Key Subchecker.

You will also need to annotate the JDK to indicate the behavior of library methods:

• Collection.add: annotate with @EnsuresNonEmpty
• Collection.isEmpty: annotate with @EnsuresNonEmptyIf
• Collection.contains: annotate with @EnsuresNonEmptyIf
• add other annotations as appropriate

Handling Colection.remove, removeAll, and clear is a bit unusual.
After calling these, the receiver must be @NonEmptyUnknown -- that is, "possibly empty").
That means that these methods must not be called on an expression of declared type @NonEmpty.
These methods can be called on an expression that has been refined to @NonEmpty; since these are side-effecting methods, the Checker Framework will undo any type refinement and the variable will have type @NonEmptyUnknown.)
It is unusual for legality of a method call to depend on the declared type, but this seems to work.

When you are done, the Nullness Checker should issue only the // :: diagnostics from checker/tests/nullness/IsEmptyPoll.java -- no more and no fewer.
You can test that by running the Nullness Checker on the file, and when you are done you should delete the // @skip-test line so that the file is run as part of the Checker Framework test suite.