Fix polymorphism check and introduce the concept of PolymorphicInstanceSlot

src/checkers/inference/DefaultSlotManager.java

@@ -369,8 +369,11 @@ public int getNumberOfSlots() {
         return nextId - 1;
     }
 
-    @Override
-    public SourceVariableSlot createSourceVariableSlot(AnnotationLocation location, TypeMirror type) {
+    private SourceVariableSlot createSourceVariableSlot(
+            AnnotationLocation location,
+            TypeMirror type,
+            boolean insertable
+    ) {
         AnnotationMirror defaultAnnotation = null;
         if (!InferenceOptions.makeDefaultsExplicit) {
             // retrieve the default annotation when needed
@@ -381,7 +384,7 @@ public SourceVariableSlot createSourceVariableSlot(AnnotationLocation location,
         if (location.getKind() == AnnotationLocation.Kind.MISSING) {
             if (InferenceMain.isHackMode()) {
                 //Don't cache slot for MISSING LOCATION. Just create a new one and return.
-                sourceVarSlot = new SourceVariableSlot(nextId(), location, type, defaultAnnotation, true);
+                sourceVarSlot = new SourceVariableSlot(nextId(), location, type, defaultAnnotation, insertable);
                 addToSlots(sourceVarSlot);
             } else {
                 throw new BugInCF("Creating SourceVariableSlot on MISSING_LOCATION!");
@@ -391,13 +394,25 @@ public SourceVariableSlot createSourceVariableSlot(AnnotationLocation location,
             int id = locationCache.get(location);
             sourceVarSlot = (SourceVariableSlot) getSlot(id);
         } else {
-            sourceVarSlot = new SourceVariableSlot(nextId(), location, type, defaultAnnotation, true);
+            sourceVarSlot = new SourceVariableSlot(nextId(), location, type, defaultAnnotation, insertable);
             addToSlots(sourceVarSlot);
             locationCache.put(location, sourceVarSlot.getId());
         }
         return sourceVarSlot;
     }
 
+    @Override
+    public SourceVariableSlot createSourceVariableSlot(AnnotationLocation location, TypeMirror type) {
+        return createSourceVariableSlot(location, type, true);
+    }
+
+    @Override
+    public VariableSlot createPolymorphicInstanceSlot(AnnotationLocation location, TypeMirror type) {
+        // TODO: For now, a polymorphic instance slot is just equivalent to a non-insertable
+        //  source variable slot. We may consider changing this implementation later.
+        return createSourceVariableSlot(location, type, false);
+    }
+
     /**
      * Find the default annotation for this location by checking the real type factory.
      * @param location location to create a new {@link SourceVariableSlot}

src/checkers/inference/InferenceAnnotatedTypeFactory.java

@@ -150,7 +150,12 @@ public InferenceAnnotatedTypeFactory(
         existentialInserter = new ExistentialVariableInserter(slotManager, constraintManager,
                                                               realTop, varAnnot, variableAnnotator);
 
-        inferencePoly = new InferenceQualifierPolymorphism(slotManager, variableAnnotator, this, varAnnot);
+        inferencePoly = new InferenceQualifierPolymorphism(
+                slotManager,
+                variableAnnotator,
+                this,
+                realTypeFactory,
+                varAnnot);
 
         constantToVariableAnnotator = new ConstantToVariableAnnotator(realTop, varAnnot);
         // Every subclass must call postInit!

src/checkers/inference/InferenceQualifierPolymorphism.java

@@ -1,5 +1,7 @@
 package checkers.inference;
 
+import checkers.inference.model.VariableSlot;
+import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType;
 import org.checkerframework.framework.type.visitor.AnnotatedTypeScanner;
@@ -26,14 +28,17 @@ public class InferenceQualifierPolymorphism {
     private final AnnotationMirror varAnnot;
     private final SlotManager slotManager;
     private final InferenceAnnotatedTypeFactory atypeFactory;
+    private final BaseAnnotatedTypeFactory realTypeFactory;
 
     public InferenceQualifierPolymorphism(final SlotManager slotManager,
                                           final VariableAnnotator variableAnnotator,
                                           final InferenceAnnotatedTypeFactory atypeFactory,
+                                          final BaseAnnotatedTypeFactory realTypeFactory,
                                           final AnnotationMirror varAnnot) {
         this.slotManager = slotManager;
         this.variableAnnotator = variableAnnotator;
         this.atypeFactory = atypeFactory;
+        this.realTypeFactory = realTypeFactory;
         this.varAnnot = varAnnot;
     }
 
@@ -57,13 +62,13 @@ private class PolyReplacer extends AnnotatedTypeScanner<Void, Void> {
         /**
          * The variable slot created for this method call
          */
-        private SourceVariableSlot polyVar = null;
+        private VariableSlot polyVar = null;
 
         private PolyReplacer(Tree methodCall) {
             this.methodCall = methodCall;
         }
 
-        private SourceVariableSlot getOrCreatePolyVar() {
+        private VariableSlot getOrCreatePolyVar() {
             if (polyVar == null) {
                 polyVar = variableAnnotator.getOrCreatePolyVar(methodCall);
             }
@@ -80,7 +85,7 @@ public Void scan(AnnotatedTypeMirror type, Void v) {
                     if (InferenceMain.isHackMode(slot == null)) {
                     } else if (slot instanceof ConstantSlot) {
                         AnnotationMirror constant = ((ConstantSlot) slot).getValue();
-                        if (atypeFactory.getQualifierHierarchy().isPolymorphicQualifier(constant)) {
+                        if (realTypeFactory.getQualifierHierarchy().isPolymorphicQualifier(constant)) {
                             type.replaceAnnotation(slotManager.getAnnotation(getOrCreatePolyVar()));
                         }
                     }

src/checkers/inference/SlotManager.java

@@ -46,6 +46,19 @@ public interface SlotManager {
      */
     SourceVariableSlot createSourceVariableSlot(AnnotationLocation location, TypeMirror type);
 
+    /**
+     * Create new VariableSlot and return the reference to it if no VariableSlot
+     * on this location exists. Otherwise return the reference to existing VariableSlot
+     * on this location. Each location uniquely identifies a polymorphic instance.
+     * For now, there's no dedicated slot for polymorphic instance, but we may add one
+     * in the future.
+     *
+     * @param location
+     *            used to locate this variable in code
+     * @return VariableSlot that corresponds to this location
+     */
+    VariableSlot createPolymorphicInstanceSlot(AnnotationLocation location, TypeMirror type);
+
     /**
      * Create new RefinementVariableSlot (as well as the refinement constraint if
      * possible) and return the reference to it if no RefinementVariableSlot on this

src/checkers/inference/VariableAnnotator.java

@@ -134,7 +134,7 @@ public class VariableAnnotator extends AnnotatedTypeScanner<Void,Tree> {
      * methodCall -> variable created to represent Poly qualifiers
      * See InferenceQualifierPolymorphism.
      */
-    private final Map<Tree, SourceVariableSlot> treeToPolyVar;
+    private final Map<Tree, VariableSlot> treeToPolyVar;
 
     // An instance of @VarAnnot
     private final AnnotationMirror varAnnot;
@@ -206,10 +206,10 @@ protected AnnotationLocation treeToLocation(Tree tree) {
      * one and return it, if we haven't created one for the given tree. see InferenceQualifierPolymorphism
      * @return The Variable representing PolymorphicQualifier for the given tree
      */
-    public SourceVariableSlot getOrCreatePolyVar(Tree tree) {
-        SourceVariableSlot polyVar = treeToPolyVar.get(tree);
+    public VariableSlot getOrCreatePolyVar(Tree tree) {
+        VariableSlot polyVar = treeToPolyVar.get(tree);
         if (polyVar == null) {
-            polyVar = slotManager.createSourceVariableSlot(treeToLocation(tree), TreeUtils.typeOf(tree));
+            polyVar = slotManager.createPolymorphicInstanceSlot(treeToLocation(tree), TreeUtils.typeOf(tree));
             treeToPolyVar.put(tree, polyVar);
         }