Add Queue.isEmpty/poll refinement

[nhioe]

Fixes false positives in Queue.poll() by refining return type based on isEmpty checks.

Checker should know that the polled element is @NonNull if:

• isEmpty returns false
• The Queue element type is @NonNull

Existing test case in isEmptyPoll.java:

// should no longer raise any errors
  void mNonNull(Queue<String> q) {
      while (!q.isEmpty()) {
          @NonNull String firstNode = q.poll();
      }
  }

[wmdietl]

This looks great!
Please also add a note to the changelog.

[wmdietl]

Would it make sense to add a second statement in the loop body: firstNode = q.poll()? The second call should fail, right?

Maybe in a separate test, have while(...) { q.clear(); firstNode = q.poll(); } or something like that, to test other side-effecting methods. I'm a bit afraid that setting the receiver to NONNULL will not be cleared out by such an operation.

[nhioe]

Thank you for catching these. You're right, currently the implementation only accommodates the simplest path and will fail on those test cases, as NONNULL will persist across mutations.

I plan to clear the NONNULL on known side-effecting methods that may invalidate our guarantee (clear, remove, poll, etc). However, I imagine this could get complicated with arbitrary methods (e.g. some foo is called that mutates the queue)?

Is it reasonable to make the fix for known side-effecting methods and document this limitation?

[wmdietl]

I think we should look for a solution that works with the existing handling of side-effects.
As extra test, please add something with two separate queues, to ensure that while (!q1.isEmpty()) { q2.clear(); firstNode = q1.poll(); } also works correctly.

[wmdietl]

Suggested change

	// Handle Collection.isEmpty(), mark receiver as non-empty in the false branch
	// Handle Collection.isEmpty(): mark receiver as non-empty in the false branch.

The sentence read a bit odd. Documentation comments should still end with a period.

You need to explain somewhere how you mark the receiver as non-empty. The body adds NONNULL, which seems a bit odd - the receiver for any method invocation should already be non-null. So how is this conveying any information you can test for below?

[nhioe]

Semantically, marking it NONNULL doesn't map perfectly to collection state, but it acts as a signal to poll() about what we learned from isEmpty, so we can refine the return type. Is a custom annotation for non-empty worth exploring?

[wmdietl]

Could you add something about poll() to the Store? Check the conditions here and set the return type of poll() to non-null here? Hopefully such a fact would automatically removed on side effects.

[wmdietl]

Suggested change

	// be non-empty
	// and Queue element type is @NonNull
	// be non-empty, and the Queue element type is @NonNull.

I like the Oxford comma.

[wmdietl]

Thanks! I just looked at the expanded test and they look great! One comment about aliasing that you should think about and possibly fix. I'll look at the code soon.

[wmdietl]

You do not know whether q1 == q2 holds or not. So to be conservative, we need to drop the refinement.
This is related to the missing warning in test aliasClearBeforePoll.

[nhioe]

I see. I assume I'll need to conservatively drop all queue non-empty refinements queue-related refinements in the store whenever a side-effecting method is called.