Update ontology qualifier hierarchy (#58)

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,101 @@ 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);
             }
+
+            EnumSet<OntologyValue> a1Set = OntologyUtils.getOntologyValuesSet(a1);
+            EnumSet<OntologyValue> a2Set = OntologyUtils.getOntologyValuesSet(a2);
+
+            return OntologyUtils.createOntologyAnnotationByValues(
+                    processingEnv,
+                    OntologyUtils.glbOfOntologyValues(a1Set, a2Set)
+                            .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/OntologyTypeValidator.java

@@ -0,0 +1,59 @@
+package ontology;
+
+import checkers.inference.InferenceValidator;
+import checkers.inference.InferenceVisitor;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Set;
+import javax.lang.model.element.AnnotationMirror;
+import javax.tools.Diagnostic;
+import ontology.qual.Ontology;
+import ontology.qual.OntologyValue;
+import ontology.util.OntologyUtils;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.framework.source.DiagMessage;
+import org.checkerframework.framework.type.AnnotatedTypeFactory;
+import org.checkerframework.framework.type.AnnotatedTypeMirror;
+import org.checkerframework.framework.type.QualifierHierarchy;
+
+/**
+ * This class checks the well-formedness of ontology values used inside an {@link Ontology}
+ * annotation. The current rules include: 1. If the type is TOP, BOTTOM, or POLY, the annotation
+ * shouldn't contain other values (e.g., @Ontology({POLY, FORCE_3D}) is invalid).
+ */
+public class OntologyTypeValidator extends InferenceValidator {
+    public OntologyTypeValidator(
+            BaseTypeChecker checker,
+            InferenceVisitor<?, ?> visitor,
+            AnnotatedTypeFactory atypeFactory) {
+        super(checker, visitor, atypeFactory);
+    }
+
+    @Override
+    protected List<DiagMessage> isTopLevelValidType(
+            QualifierHierarchy qualifierHierarchy, AnnotatedTypeMirror type) {
+        List<DiagMessage> errorMsgs =
+                new ArrayList<>(super.isTopLevelValidType(qualifierHierarchy, type));
+
+        AnnotationMirror am = type.getAnnotation(Ontology.class);
+        if (am != null) {
+            Set<OntologyValue> values = OntologyUtils.getOntologyValuesSet(am);
+            if (values.size() > 1) {
+                if (values.contains(OntologyValue.POLY)
+                        || values.contains(OntologyValue.TOP)
+                        || values.contains(OntologyValue.BOTTOM)) {
+                    // Should only have one ontology value when the type is one of {POLY, TOP,
+                    // BOTTOM}
+                    errorMsgs.add(
+                            new DiagMessage(
+                                    Diagnostic.Kind.ERROR,
+                                    "type.invalid.conflicting.elements",
+                                    am,
+                                    type));
+                }
+            }
+        }
+
+        return errorMsgs;
+    }
+}

src/ontology/OntologyVisitor.java

@@ -1,6 +1,7 @@
 package ontology;
 
 import checkers.inference.InferenceChecker;
+import checkers.inference.InferenceValidator;
 import checkers.inference.InferenceVisitor;
 import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
 
@@ -13,4 +14,9 @@ public OntologyVisitor(
             boolean infer) {
         super(checker, ichecker, factory, infer);
     }
+
+    @Override
+    protected InferenceValidator createTypeValidator() {
+        return new OntologyTypeValidator(checker, this, atypeFactory);
+    }
 }

src/ontology/messages.properties

@@ -0,0 +1 @@
+type.invalid.conflicting.elements=invalid type: conflicting elements in annotation %s of type "%s"

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);
     }
 }