Type is not re-set to declared type following a side-effecting operation

[jyoo980]

Issue

I am currently developing a type system to reason about the non-emptiness of container types (e.g, List, Set etc). I have annotated parts of the typetools JDK with @mernst with qualifiers from our type system, e.g.,

// In List.java
...
@EnsuresNonEmpty("this")
boolean add(... List<E> this, E e)

boolean remove(... @NonEmpty List<E> this, ...)

The partially annotated JDK is available here.

With this change, I would expect the following code to fail type-checking:

import java.util.List;
import java.util.LinkedList;

import org.checkerframework.checker.nonempty.qual.UnknownNonEmpty;
import org.checkerframework.checker.nonempty.qual.NonEmpty;

class Issue6407 {
  void foo() {
    // items initially has the type @UnknownNonEmpty
    List<String> items = new LinkedList<>();
    items.add("hello");
    @NonEmpty List<String> bar = items; // OK
    items.remove("hello");
    @NonEmpty List<String> baz = items; // I expect an error here
  }
}

Specifically, I would expect the assignment to baz after the call to items.remove("hello") to fail, since List.remove is a side-effecting operation (i.e., not @Pure) and the type of the receiver is no longer guaranteed to be @NonEmpty.

However, this code type-checks cleanly.

Steps to Reproduce

Please follow the following sequence of shell commands

# Clone my fork of the Checker Framework
git clone git@github.com:jyoo980/checker-framework.git

# Clone my fork of the typetools JDK
git clone git@github.com:jyoo980/jdk.git

# Checkout the relevant branches
# Note, ensure that the `checker-framework` repo and the `jdk` repo are sibling directories
(cd checker-framework && git checkout --filter=blob:none yoo/nonempty-checker)
(cd jdk && git checkout --filter=blob:none yoo/nonempty-annos)

# Build the Checker Framework
cd checker-framework
./gradlew assemble

# Run the Non-Empty Checker on the test case from: https://gist.github.com/jyoo980/3bf7917ade06d644776af942d7312b34
checker/bin/javac -processor nonempty Issue6407.java

Expected output: the Non-Empty Checker should raise an assignment error at the last line
Actual output: the Non-Empty Checker type-checks Main.java cleanly

[msridhar]

@jyoo980 it may be helpful to create a repro case that does not involve the JDK. That would be easier to turn into a regression test, and also it would eliminate the possibility of this issue being specific to the JDK classes somehow.

[jyoo980]

@msridhar We're tracking this over in my fork: jyoo980#1. I'll re-open this if needed. It's not a bug, but we had to override a default setting for dataflow.