add subtype constraint in Inference type Hierarchy

Author: txiang61

src/checkers/inference/InferenceTypeHierarchy.java

@@ -7,11 +7,15 @@
 import org.checkerframework.framework.type.StructuralEqualityComparer;
 import org.checkerframework.framework.type.StructuralEqualityVisitHistory;
 import org.checkerframework.framework.type.SubtypeVisitHistory;
+import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.BugInCF;
 
 import javax.lang.model.element.AnnotationMirror;
 
+import checkers.inference.model.ConstantSlot;
+import checkers.inference.model.ConstraintManager;
 import checkers.inference.model.Slot;
+import checkers.inference.qual.VarAnnot;
 
 /**
  *  The InferenceTypeHierarchy along with the InferenceQualifierHierarchy is responsible for
@@ -27,6 +31,8 @@ public class InferenceTypeHierarchy extends DefaultTypeHierarchy {
     private final AnnotationMirror varAnnot;
     // TODO: Think this through, add any missing constraints
 
+    private final SlotManager slotMgr;
+    private final ConstraintManager constraintMgr;
 
     /**
      * Constructs an instance of {@code TypeHierarchy} for the type system
@@ -41,6 +47,9 @@ public InferenceTypeHierarchy(final BaseTypeChecker checker, final QualifierHier
               checker.getOption("ignoreRawTypeArguments", "true").equals("true"),
               checker.hasOption("invariantArrays"));
         this.varAnnot = varAnnot;
+
+        slotMgr = InferenceMain.getInstance().getSlotManager();
+        constraintMgr = InferenceMain.getInstance().getConstraintManager();
     }
 
     public boolean areEqual(AnnotatedTypeMirror type1, AnnotatedTypeMirror type2) {
@@ -52,6 +61,37 @@ public StructuralEqualityComparer createEqualityComparer() {
         return new InferenceEqualityComparer(this.typeargVisitHistory,
                 InferenceQualifierHierarchy.findVarAnnot(qualifierHierarchy.getTopAnnotations()));
     }
+
+    @Override
+    public boolean isSubtype(
+            final AnnotatedTypeMirror subtype, final AnnotatedTypeMirror supertype) {
+		AnnotationMirror subAnno = subtype.getAnnotationInHierarchy(varAnnot);
+        AnnotationMirror superAnno = supertype.getAnnotationInHierarchy(varAnnot);
+
+        if (!isVarAnnot(subAnno) || !isVarAnnot(superAnno)) {
+            return isSubtype(subtype, supertype, varAnnot);
+        }
+
+        final Slot subSlot   = slotMgr.getSlot(subAnno);
+        final Slot superSlot = slotMgr.getSlot(superAnno);
+
+        if (subSlot instanceof ConstantSlot || superSlot instanceof ConstantSlot) {
+            return isSubtype(subtype, supertype, varAnnot);
+        }
+
+        return constraintMgr.addSubtypeConstraintNoErrorMsg(subSlot, superSlot);
+    }
+
+    /**
+     * @return true if anno is an instance of @VarAnnot
+     */
+    public static boolean isVarAnnot(AnnotationMirror anno) {
+        if (InferenceMain.isHackMode(anno == null)) {
+            return false;
+        }
+
+        return AnnotationUtils.areSameByClass(anno, VarAnnot.class);
+    }
 }
 
 class InferenceEqualityComparer extends StructuralEqualityComparer {