@KeyFor refinement doesn't work for autoboxed types

[atomicknight]

Environment: Checker Framework 1.9.11, Oracle JDK 1.8.0_65, Windows 7/8.1

Example:

import java.util.Map;

public abstract class KeyForRefinement {
    public void working1(Object key) {
        Map<Object, Object> m = getObjectMap();
        if (!m.containsKey(key)) {
            m.put(key, new Object());
        }
        m.get(key).toString();
    }

    public void working2(Integer key) {
        Map<Integer, Object> m = getIntegerMap();
        if (!m.containsKey(key)) {
            m.put(key, new Object());
        }
        m.get(key).toString();
    }

    public void working3(Double key) {
        Map<Double, Object> m = getDoubleMap();
        if (!m.containsKey(key)) {
            m.put(key, new Object());
        }
        m.get(key).toString();
    }

    public void notWorking1(int key) {
        Map<Integer, Object> m = getIntegerMap();
        if (!m.containsKey(key)) {
            m.put(key, new Object());
        }
        m.get(key).toString();  // Should not generate error but does
    }

    public void notWorking2(double key) {
        Map<Double, Object> m = getDoubleMap();
        if (!m.containsKey(key)) {
            m.put(key, new Object());
        }
        m.get(key).toString();  // Should not generate error but does
    }

    public abstract Map<Object, Object> getObjectMap();
    public abstract Map<Integer, Object> getIntegerMap();
    public abstract Map<Double, Object> getDoubleMap();
}

When Map#get is invoked with an object argument, the key variable is correctly refined to be of the @KeyFor type. However, invoking the same method with a primitive type does not appear to perform the same refinement.

[mernst]

Thanks for the bug report.

I have added a test case as file checker-framework/checker/tests/nullness/KeyForAutoboxing.java.

Another test case (included in that file) is

public void notWorking5(double key, Map<Double, Object> m) {
  if (m.get(Double.valueOf(key)) != null) {
    m.get(Double.valueOf(key)).toString();  // Should not generate error but does
  }
}

My hypothesis is that the issue is that method Double.valueOf is not @Deterministic. Thus, even after Double.valueOf(key) is inserted into the map as a key, the expression Double.valueOf(key) is not considered to necessarily be a key in the map. This is the right behavior for non-@Deterministic methods.

Double.valueOf isn't @Deterministic in that it may return a different value each time it is called with the same argument. However, Double.valueOf is deterministic with respect to equals and hashCode, in the sense that for a given argument d, Double.valueOf(d) always returns values that are equals to one another and for which hashCode returns the same value.

I'm not sure exactly how to solve the problem. We could hard-code the KeyFor Checker to treat of autoboxing operators such as Double.valueOf as @Deterministic. Or, perhaps there are other solutions to the problem.

[bitterfox]

Hi all, I think this is not a false-positive. This is true-positive when we consider the return value of getDoubleMap() is IdentityHashMap. But I'm not sure that this behavior is intentioned to prevent an error of IdentityHashMap. (If a return type getDoubleMap is HashMap or something like that, this is completely a false-positive.)

Please consider following code:

    public abstract Map<Double, Object> getDoubleMap() { return new IdentityHashMap<>(); }

    public void m(double key) {
        Map<Double, Object> m = getDoubleMap();
        if (!m.containsKey(key)) {
            m.put(key, new Object());
        }
        m.get(key).toString(); // NPE occur at this point; So the compile-error is correct
    }

When we consider an instance of Map could be an IdentityHashMap, should compiler issue an error for m.get(key).toString()(where a type of m is Map or AbstractMap)? If so, when a type of m is not a supertype of IdentityHashMap, I meant when m is HashMap or something like that or is not Map or AbstractMap, shouldn't compiler emit an error?