Update ontology qualifier hierarchy

src/ontology/OntologyAnnotatedTypeFactory.java

@@ -1,24 +1,26 @@
 package ontology;
 
 import checkers.inference.BaseInferenceRealTypeFactory;
+import com.google.common.collect.ImmutableMap;
 import com.sun.source.tree.NewArrayTree;
 import com.sun.source.tree.NewClassTree;
-import java.util.Arrays;
 import java.util.EnumSet;
-import java.util.HashSet;
 import java.util.Map;
 import java.util.Set;
 import javax.lang.model.element.AnnotationMirror;
 import ontology.qual.OntologyValue;
 import ontology.util.OntologyUtils;
+import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.framework.qual.TypeUseLocation;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
+import org.checkerframework.framework.type.ElementQualifierHierarchy;
 import org.checkerframework.framework.type.QualifierHierarchy;
 import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
+import org.checkerframework.framework.util.QualifierKind;
 import org.checkerframework.framework.util.defaults.QualifierDefaults;
-import org.checkerframework.javacutil.AnnotationUtils;
+import org.checkerframework.javacutil.BugInCF;
 
 public class OntologyAnnotatedTypeFactory extends BaseInferenceRealTypeFactory {
 
@@ -28,19 +30,9 @@ public OntologyAnnotatedTypeFactory(BaseTypeChecker checker, boolean isInfer) {
         postInit();
     }
 
-    @SuppressWarnings("deprecation")
     @Override
     public QualifierHierarchy createQualifierHierarchy() {
-        return org.checkerframework.framework.util.MultiGraphQualifierHierarchy
-                .createMultiGraphQualifierHierarchy(this);
-    }
-
-    @SuppressWarnings("deprecation")
-    @Override
-    public QualifierHierarchy createQualifierHierarchyWithMultiGraphFactory(
-            org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory
-                    factory) {
-        return new OntologyQualifierHierarchy(factory, OntologyUtils.ONTOLOGY_BOTTOM);
+        return new OntologyQualifierHierarchy();
     }
 
     @Override
@@ -54,74 +46,109 @@ public TreeAnnotator createTreeAnnotator() {
         return new ListTreeAnnotator(super.createTreeAnnotator(), new OntologyTreeAnnotator());
     }
 
-    @SuppressWarnings("deprecation")
-    private static class OntologyQualifierHierarchy
-            extends org.checkerframework.framework.util.GraphQualifierHierarchy {
+    private final class OntologyQualifierHierarchy extends ElementQualifierHierarchy {
+
+        private final QualifierKind ONTOLOGY_KIND;
 
-        public OntologyQualifierHierarchy(
-                org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory
-                        f,
-                AnnotationMirror bottom) {
-            super(f, bottom);
+        public OntologyQualifierHierarchy() {
+            super(
+                    OntologyAnnotatedTypeFactory.this.getSupportedTypeQualifiers(),
+                    OntologyAnnotatedTypeFactory.this.elements);
+            this.ONTOLOGY_KIND = getQualifierKind(OntologyUtils.ONTOLOGY);
         }
 
         @Override
-        protected Set<AnnotationMirror> findBottoms(
-                Map<AnnotationMirror, Set<AnnotationMirror>> supertypes) {
-            Set<AnnotationMirror> newBottoms = super.findBottoms(supertypes);
-            newBottoms.remove(OntologyUtils.ONTOLOGY);
-            newBottoms.add(OntologyUtils.ONTOLOGY_BOTTOM);
-
-            // update supertypes
-            Set<AnnotationMirror> supertypesOfBtm = new HashSet<>();
-            supertypesOfBtm.add(OntologyUtils.ONTOLOGY_TOP);
-            supertypes.put(OntologyUtils.ONTOLOGY_BOTTOM, supertypesOfBtm);
-
-            return newBottoms;
+        public boolean isSubtype(AnnotationMirror subQualifier, AnnotationMirror superQualifier) {
+            if (getQualifierKind(subQualifier) != ONTOLOGY_KIND
+                    || getQualifierKind(superQualifier) != ONTOLOGY_KIND) {
+                throw new BugInCF(
+                        "unexpected annotation mirrors: %s, %s", subQualifier, superQualifier);
+            }
+
+            Set<OntologyValue> subValues = OntologyUtils.getOntologyValuesSet(subQualifier);
+            Set<OntologyValue> superValues = OntologyUtils.getOntologyValuesSet(superQualifier);
+
+            if (subValues.contains(OntologyValue.BOTTOM)
+                    || superValues.contains(OntologyValue.TOP)) {
+                return true;
+            } else if (subValues.contains(OntologyValue.POLY)
+                    && superValues.contains(OntologyValue.POLY)) {
+                return true;
+            } else if (subValues.contains(OntologyValue.POLY)
+                    || superValues.contains(OntologyValue.POLY)) {
+                return false;
+            } else {
+                return subValues.containsAll(superValues);
+            }
         }
 
         @Override
-        protected void finish(
-                QualifierHierarchy qualHierarchy,
-                Map<AnnotationMirror, Set<AnnotationMirror>> fullMap,
-                Map<AnnotationMirror, AnnotationMirror> polyQualifiers,
-                Set<AnnotationMirror> tops,
-                Set<AnnotationMirror> bottoms,
-                Object... args) {
-            super.finish(qualHierarchy, fullMap, polyQualifiers, tops, bottoms, args);
-
-            // substitue ONTOLOGY with ONTOLOGY_TOP in fullMap
-            assert fullMap.containsKey(OntologyUtils.ONTOLOGY);
-            Set<AnnotationMirror> ontologyTopSupers = fullMap.get(OntologyUtils.ONTOLOGY);
-            fullMap.remove(OntologyUtils.ONTOLOGY);
-            fullMap.put(OntologyUtils.ONTOLOGY_TOP, ontologyTopSupers);
-
-            // update tops
-            tops.remove(OntologyUtils.ONTOLOGY);
-            tops.add(OntologyUtils.ONTOLOGY_TOP);
+        public @Nullable AnnotationMirror leastUpperBound(
+                AnnotationMirror a1, AnnotationMirror a2) {
+            if (getQualifierKind(a1) != ONTOLOGY_KIND || getQualifierKind(a2) != ONTOLOGY_KIND) {
+                throw new BugInCF("unexpected annotation mirrors: %s, %s", a1, a2);
+            }
+
+            EnumSet<OntologyValue> a1Set = OntologyUtils.getOntologyValuesSet(a1);
+            EnumSet<OntologyValue> a2Set = OntologyUtils.getOntologyValuesSet(a2);
+
+            return OntologyUtils.createOntologyAnnotationByValues(
+                    processingEnv,
+                    OntologyUtils.lubOfOntologyValues(a1Set, a2Set)
+                            .toArray(new OntologyValue[] {}));
         }
 
         @Override
-        public boolean isSubtype(AnnotationMirror rhs, AnnotationMirror lhs) {
-            if (AnnotationUtils.areSameByName(rhs, OntologyUtils.ONTOLOGY)
-                    && AnnotationUtils.areSameByName(lhs, OntologyUtils.ONTOLOGY)) {
-                OntologyValue[] rhsValue = OntologyUtils.getOntologyValues(rhs);
-                OntologyValue[] lhsValue = OntologyUtils.getOntologyValues(lhs);
-                EnumSet<OntologyValue> rSet = EnumSet.noneOf(OntologyValue.class);
-                rSet.addAll(Arrays.asList(rhsValue));
-                EnumSet<OntologyValue> lSet = EnumSet.noneOf(OntologyValue.class);
-                lSet.addAll(Arrays.asList(lhsValue));
-
-                if (rSet.containsAll(lSet)
-                        || rSet.contains(OntologyValue.BOTTOM)
-                        || lSet.contains(OntologyValue.TOP)) {
-                    return true;
-                } else {
-                    return false;
-                }
-            } else {
-                return super.isSubtype(rhs, lhs);
+        public @Nullable AnnotationMirror greatestLowerBound(
+                AnnotationMirror a1, AnnotationMirror a2) {
+            if (getQualifierKind(a1) != ONTOLOGY_KIND || getQualifierKind(a2) != ONTOLOGY_KIND) {
+                throw new BugInCF("unexpected annotation mirrors: %s, %s", a1, a2);
             }
+
+            Set<OntologyValue> a1Set = OntologyUtils.getOntologyValuesSet(a1);
+            Set<OntologyValue> a2Set = OntologyUtils.getOntologyValuesSet(a2);
+
+            if (a1Set.contains(OntologyValue.POLY) && a2Set.contains(OntologyValue.POLY)) {
+                return OntologyUtils.POLY_ONTOLOGY;
+            } else if (a1Set.contains(OntologyValue.BOTTOM)
+                    || a2Set.contains(OntologyValue.BOTTOM)
+                    || a1Set.contains(OntologyValue.POLY)
+                    || a2Set.contains(OntologyValue.POLY)) {
+                return OntologyUtils.ONTOLOGY_BOTTOM;
+            }
+
+            a1Set.addAll(a2Set); // computes the union of the two sets
+            return OntologyUtils.createOntologyAnnotationByValues(
+                    processingEnv, a1Set.toArray(new OntologyValue[] {}));
+        }
+
+        @Override
+        protected Map<QualifierKind, AnnotationMirror> createTopsMap() {
+            return ImmutableMap.of(
+                    getQualifierKind(OntologyUtils.ONTOLOGY), OntologyUtils.ONTOLOGY_TOP);
+        }
+
+        @Override
+        protected Map<QualifierKind, AnnotationMirror> createBottomsMap() {
+            return ImmutableMap.of(
+                    getQualifierKind(OntologyUtils.ONTOLOGY), OntologyUtils.ONTOLOGY_BOTTOM);
+        }
+
+        @Override
+        public @Nullable AnnotationMirror getPolymorphicAnnotation(AnnotationMirror start) {
+            if (getQualifierKind(start) != ONTOLOGY_KIND) {
+                return null;
+            }
+            return OntologyUtils.POLY_ONTOLOGY;
+        }
+
+        @Override
+        public boolean isPolymorphicQualifier(AnnotationMirror qualifier) {
+            if (getQualifierKind(qualifier) != ONTOLOGY_KIND) {
+                throw new BugInCF("unexpected annotation mirror %s", qualifier);
+            }
+
+            return OntologyUtils.getOntologyValuesSet(qualifier).contains(OntologyValue.POLY);
         }
     }
 

src/ontology/qual/OntologyValue.java

@@ -14,6 +14,7 @@
 // the reason of this null pointer exception need to be investigated.
 public enum OntologyValue {
     TOP("TOP"),
+    POLY("poly"),
     SEQUENCE("sequence"),
     DICTIONARY("dictionary"),
     POSITION_3D("position_3d"),

src/ontology/solvers/backend/z3/OntologyZ3FormatTranslator.java

@@ -110,7 +110,7 @@ public BoolExpr serialize(PreferenceConstraint preferenceConstraint) {
 
     protected boolean isPolyOntology(Slot slot) {
         return slot instanceof ConstantSlot
-                && AnnotationUtils.areSameByName(
+                && AnnotationUtils.areSame(
                         ((ConstantSlot) slot).getValue(), OntologyUtils.POLY_ONTOLOGY);
     }
 }

src/ontology/util/OntologyUtils.java

@@ -11,7 +11,6 @@
 import javax.lang.model.util.Types;
 import ontology.qual.Ontology;
 import ontology.qual.OntologyValue;
-import ontology.qual.PolyOntology;
 import org.checkerframework.javacutil.AnnotationBuilder;
 import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.BugInCF;
@@ -59,7 +58,8 @@ private OntologyUtils(ProcessingEnvironment processingEnv) {
         ONTOLOGY_BOTTOM =
                 OntologyUtils.createOntologyAnnotationByValues(processingEnv, OntologyValue.BOTTOM);
         ONTOLOGY = AnnotationBuilder.fromClass(elements, Ontology.class);
-        POLY_ONTOLOGY = AnnotationBuilder.fromClass(elements, PolyOntology.class);
+        POLY_ONTOLOGY =
+                OntologyUtils.createOntologyAnnotationByValues(processingEnv, OntologyValue.POLY);
 
         ontologyValuesElement = TreeUtils.getMethod(Ontology.class, "values", processingEnv);
 
@@ -70,7 +70,10 @@ private OntologyUtils(ProcessingEnvironment processingEnv) {
     }
 
     public static void initOntologyUtils(ProcessingEnvironment processingEnv) {
-        if (singletonInstance == null) {
+        if (singletonInstance == null || processingEnv != singletonInstance.processingEnvironment) {
+            // Initialize the singleton instance if it's null or the processing env has changed.
+            // Note that the change of processing env can happen if we have both the initial
+            // type check and the final type check in a single execution.
             singletonInstance = new OntologyUtils(processingEnv);
         }
     }
@@ -136,22 +139,27 @@ public static OntologyValue[] getOntologyValues(AnnotationMirror type) {
                 new OntologyValue[] {OntologyValue.TOP});
     }
 
+    public static EnumSet<OntologyValue> getOntologyValuesSet(AnnotationMirror type) {
+        OntologyValue[] values = getOntologyValues(type);
+        EnumSet<OntologyValue> set = EnumSet.noneOf(OntologyValue.class);
+        set.addAll(Arrays.asList(values));
+        return set;
+    }
+
     public static EnumSet<OntologyValue> lubOfOntologyValues(
             EnumSet<OntologyValue> valueSet1, EnumSet<OntologyValue> valueSet2) {
         EnumSet<OntologyValue> lub = EnumSet.noneOf(OntologyValue.class);
 
-        for (OntologyValue value1 : valueSet1) {
-            if (value1 == OntologyValue.TOP) {
-                lub.clear();
-                break;
-            }
-            if (valueSet2.contains(value1)) {
-                lub.add(value1);
-            }
-        }
-
-        if (lub.isEmpty()) {
+        if (valueSet1.contains(OntologyValue.POLY) && valueSet2.contains(OntologyValue.POLY)) {
+            lub.add(OntologyValue.POLY);
+        } else if (valueSet1.contains(OntologyValue.TOP)
+                || valueSet2.contains(OntologyValue.TOP)
+                || valueSet1.contains(OntologyValue.POLY)
+                || valueSet2.contains(OntologyValue.POLY)) {
             lub.add(OntologyValue.TOP);
+        } else {
+            lub.addAll(valueSet1);
+            lub.retainAll(valueSet2);
         }
 
         return lub;

testing/PolyOntologyTest.java

@@ -1,6 +1,5 @@
 import ontology.qual.Ontology;
 import ontology.qual.OntologyValue;
-import ontology.qual.PolyOntology;
 
 public class PolyOntologyTest {
     @Ontology(values={OntologyValue.VELOCITY_3D}) Vector externalVelocity;
@@ -14,17 +13,34 @@ public void applyVelocity(Vector velocity) {
     public void applyForce(Vector force) {
         // :: fixable-error: (assignment.type.incompatible)
         @Ontology(values={OntologyValue.FORCE_3D}) Vector res = externalForce.add(force);
+        // :: fixable-error: (assignment.type.incompatible)
+        @Ontology(values={OntologyValue.FORCE_3D}) Vector max = Vector.max(externalForce, force);
     }
 }
 
 class Vector {
     int x;
     int y;
     int z;
-    public @PolyOntology Vector add( @PolyOntology Vector this, @PolyOntology Vector other) {
+    public @Ontology(values={OntologyValue.POLY}) Vector add( @Ontology(values={OntologyValue.POLY}) Vector this, @Ontology(values={OntologyValue.POLY}) Vector other) {
         this.x += other.x;
         this.y += other.y;
         this.z += other.z;
         return this;
     }
-}
+
+    public static @Ontology(values={OntologyValue.POLY}) Vector max(@Ontology(values={OntologyValue.POLY}) Vector a, @Ontology(values={OntologyValue.POLY}) Vector b) {
+        int aLength = a.length();
+        int bLength = b.length();
+
+        // test lub of polys
+        if (aLength > bLength) {
+            return a;
+        }
+        return b;
+    }
+
+    public int length() {
+        return x * x + y * y + z * z;
+    }
+}