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

[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.

[Vivek-kr22]

import java.util.PriorityQueue;

import org.checkerframework.checker.nullness.qual.NonNull;

public class MyClass { public static void main(String[] args) { PriorityQueue<@NonNull String> queue = new PriorityQueue<>(); queue.add("Item 1"); queue.add("Item 2");

    while (!queue.isEmpty()) {
        @NonNull String firstItem = queue.poll(); // Ensures non-null value
        System.out.println("Processing: " + firstItem);
    }
}

}

Key Changes: 1.Queue Declaration: Declared the PriorityQueue with @NonNull annotations to ensure all elements in the queue are non-null.

2.Loop Logic: Wrapped the poll() method inside a condition that ensures the queue is non-empty.

3.Annotations: Used @NonNull to explicitly indicate that poll() will not return null when the queue is not empty.

=>This should satisfy the conditional postcondition requirements of the NullnessChecker. Let me know if you’d like further assistance! @mernst @GoogleCodeExporter @jayvdb @jschaf @mgsloan