From 745f685a7a4d9c77ce884f8e1d51258a80328f27 Mon Sep 17 00:00:00 2001 From: zcai Date: Sun, 6 Feb 2022 01:52:49 -0500 Subject: [PATCH 1/7] update ontology qualifier hierarchy and add lub test for poly --- .../OntologyAnnotatedTypeFactory.java | 171 ++++++++++-------- src/ontology/qual/OntologyValue.java | 1 + src/ontology/qual/PolyOntology.java | 26 --- .../z3/OntologyZ3FormatTranslator.java | 2 +- src/ontology/util/OntologyUtils.java | 35 ++-- testing/PolyOntologyTest.java | 22 ++- 6 files changed, 138 insertions(+), 119 deletions(-) delete mode 100644 src/ontology/qual/PolyOntology.java diff --git a/src/ontology/OntologyAnnotatedTypeFactory.java b/src/ontology/OntologyAnnotatedTypeFactory.java index d4f9595..35a7961 100644 --- a/src/ontology/OntologyAnnotatedTypeFactory.java +++ b/src/ontology/OntologyAnnotatedTypeFactory.java @@ -1,24 +1,27 @@ 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; + +import javax.lang.model.element.AnnotationMirror; +import java.util.EnumSet; +import java.util.Map; +import java.util.Set; public class OntologyAnnotatedTypeFactory extends BaseInferenceRealTypeFactory { @@ -28,19 +31,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 +47,102 @@ 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 findBottoms( - Map> supertypes) { - Set newBottoms = super.findBottoms(supertypes); - newBottoms.remove(OntologyUtils.ONTOLOGY); - newBottoms.add(OntologyUtils.ONTOLOGY_BOTTOM); - - // update supertypes - Set 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 subValues = OntologyUtils.getOntologyValuesSet(subQualifier); + Set 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> fullMap, - Map polyQualifiers, - Set tops, - Set bottoms, - Object... args) { - super.finish(qualHierarchy, fullMap, polyQualifiers, tops, bottoms, args); - - // substitue ONTOLOGY with ONTOLOGY_TOP in fullMap - assert fullMap.containsKey(OntologyUtils.ONTOLOGY); - Set 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 a1Set = OntologyUtils.getOntologyValuesSet(a1); + EnumSet 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 rSet = EnumSet.noneOf(OntologyValue.class); - rSet.addAll(Arrays.asList(rhsValue)); - EnumSet 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 a1Set = OntologyUtils.getOntologyValuesSet(a1); + Set 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 createTopsMap() { + return ImmutableMap.of(getQualifierKind(OntologyUtils.ONTOLOGY), OntologyUtils.ONTOLOGY_TOP); + } + + @Override + protected Map 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); } } diff --git a/src/ontology/qual/OntologyValue.java b/src/ontology/qual/OntologyValue.java index 729d98b..9e63523 100644 --- a/src/ontology/qual/OntologyValue.java +++ b/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"), diff --git a/src/ontology/qual/PolyOntology.java b/src/ontology/qual/PolyOntology.java deleted file mode 100644 index 7597450..0000000 --- a/src/ontology/qual/PolyOntology.java +++ /dev/null @@ -1,26 +0,0 @@ -package ontology.qual; - -import java.lang.annotation.Documented; -import java.lang.annotation.ElementType; -import java.lang.annotation.Retention; -import java.lang.annotation.RetentionPolicy; -import java.lang.annotation.Target; -import org.checkerframework.framework.qual.PolymorphicQualifier; - -/** - * A Polymorphic qualifier for {@code Ontology}. - * - *

See the Checker - * Framework Manual for information on the semantics of polymorphic qualifiers in the checker - * framework. - * - *

- * - * @see Ontology - */ -@Documented -@PolymorphicQualifier(Ontology.class) -@Retention(RetentionPolicy.RUNTIME) -@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) -public @interface PolyOntology {} diff --git a/src/ontology/solvers/backend/z3/OntologyZ3FormatTranslator.java b/src/ontology/solvers/backend/z3/OntologyZ3FormatTranslator.java index 939d6e4..001fc28 100644 --- a/src/ontology/solvers/backend/z3/OntologyZ3FormatTranslator.java +++ b/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); } } diff --git a/src/ontology/util/OntologyUtils.java b/src/ontology/util/OntologyUtils.java index a9aac40..e72d24c 100644 --- a/src/ontology/util/OntologyUtils.java +++ b/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,7 @@ 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 +69,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 +138,27 @@ public static OntologyValue[] getOntologyValues(AnnotationMirror type) { new OntologyValue[] {OntologyValue.TOP}); } + public static EnumSet getOntologyValuesSet(AnnotationMirror type) { + OntologyValue[] values = getOntologyValues(type); + EnumSet set = EnumSet.noneOf(OntologyValue.class); + set.addAll(Arrays.asList(values)); + return set; + } + public static EnumSet lubOfOntologyValues( EnumSet valueSet1, EnumSet valueSet2) { EnumSet 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; diff --git a/testing/PolyOntologyTest.java b/testing/PolyOntologyTest.java index 9698990..36fe65a 100644 --- a/testing/PolyOntologyTest.java +++ b/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,6 +13,8 @@ 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); } } @@ -21,10 +22,25 @@ 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; } -} \ No newline at end of file + + 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; + } +} From 810febba280d1ca8b54bec543c9ba486e465c439 Mon Sep 17 00:00:00 2001 From: zcai Date: Mon, 7 Feb 2022 13:58:03 -0500 Subject: [PATCH 2/7] fix formatting --- .../OntologyAnnotatedTypeFactory.java | 44 +++++++++++-------- src/ontology/util/OntologyUtils.java | 3 +- 2 files changed, 27 insertions(+), 20 deletions(-) diff --git a/src/ontology/OntologyAnnotatedTypeFactory.java b/src/ontology/OntologyAnnotatedTypeFactory.java index 35a7961..6bd5d6d 100644 --- a/src/ontology/OntologyAnnotatedTypeFactory.java +++ b/src/ontology/OntologyAnnotatedTypeFactory.java @@ -4,6 +4,10 @@ import com.google.common.collect.ImmutableMap; import com.sun.source.tree.NewArrayTree; import com.sun.source.tree.NewClassTree; +import java.util.EnumSet; +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; @@ -18,11 +22,6 @@ import org.checkerframework.framework.util.defaults.QualifierDefaults; import org.checkerframework.javacutil.BugInCF; -import javax.lang.model.element.AnnotationMirror; -import java.util.EnumSet; -import java.util.Map; -import java.util.Set; - public class OntologyAnnotatedTypeFactory extends BaseInferenceRealTypeFactory { public OntologyAnnotatedTypeFactory(BaseTypeChecker checker, boolean isInfer) { @@ -60,18 +59,23 @@ public OntologyQualifierHierarchy() { @Override 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); + if (getQualifierKind(subQualifier) != ONTOLOGY_KIND + || getQualifierKind(superQualifier) != ONTOLOGY_KIND) { + throw new BugInCF( + "unexpected annotation mirrors: %s, %s", subQualifier, superQualifier); } Set subValues = OntologyUtils.getOntologyValuesSet(subQualifier); Set superValues = OntologyUtils.getOntologyValuesSet(superQualifier); - if (subValues.contains(OntologyValue.BOTTOM) || superValues.contains(OntologyValue.TOP)) { + if (subValues.contains(OntologyValue.BOTTOM) + || superValues.contains(OntologyValue.TOP)) { return true; - } else if (subValues.contains(OntologyValue.POLY) && superValues.contains(OntologyValue.POLY)) { + } else if (subValues.contains(OntologyValue.POLY) + && superValues.contains(OntologyValue.POLY)) { return true; - } else if (subValues.contains(OntologyValue.POLY) || superValues.contains(OntologyValue.POLY)) { + } else if (subValues.contains(OntologyValue.POLY) + || superValues.contains(OntologyValue.POLY)) { return false; } else { return subValues.containsAll(superValues); @@ -79,7 +83,8 @@ public boolean isSubtype(AnnotationMirror subQualifier, AnnotationMirror superQu } @Override - public @Nullable AnnotationMirror leastUpperBound(AnnotationMirror a1, AnnotationMirror a2) { + 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); } @@ -89,12 +94,13 @@ public boolean isSubtype(AnnotationMirror subQualifier, AnnotationMirror superQu return OntologyUtils.createOntologyAnnotationByValues( processingEnv, - OntologyUtils.lubOfOntologyValues(a1Set, a2Set).toArray(new OntologyValue[]{}) - ); + OntologyUtils.lubOfOntologyValues(a1Set, a2Set) + .toArray(new OntologyValue[] {})); } @Override - public @Nullable AnnotationMirror greatestLowerBound(AnnotationMirror a1, AnnotationMirror a2) { + 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); } @@ -113,19 +119,19 @@ public boolean isSubtype(AnnotationMirror subQualifier, AnnotationMirror superQu a1Set.addAll(a2Set); // computes the union of the two sets return OntologyUtils.createOntologyAnnotationByValues( - processingEnv, - a1Set.toArray(new OntologyValue[] {}) - ); + processingEnv, a1Set.toArray(new OntologyValue[] {})); } @Override protected Map createTopsMap() { - return ImmutableMap.of(getQualifierKind(OntologyUtils.ONTOLOGY), OntologyUtils.ONTOLOGY_TOP); + return ImmutableMap.of( + getQualifierKind(OntologyUtils.ONTOLOGY), OntologyUtils.ONTOLOGY_TOP); } @Override protected Map createBottomsMap() { - return ImmutableMap.of(getQualifierKind(OntologyUtils.ONTOLOGY), OntologyUtils.ONTOLOGY_BOTTOM); + return ImmutableMap.of( + getQualifierKind(OntologyUtils.ONTOLOGY), OntologyUtils.ONTOLOGY_BOTTOM); } @Override diff --git a/src/ontology/util/OntologyUtils.java b/src/ontology/util/OntologyUtils.java index e72d24c..be11a54 100644 --- a/src/ontology/util/OntologyUtils.java +++ b/src/ontology/util/OntologyUtils.java @@ -58,7 +58,8 @@ private OntologyUtils(ProcessingEnvironment processingEnv) { ONTOLOGY_BOTTOM = OntologyUtils.createOntologyAnnotationByValues(processingEnv, OntologyValue.BOTTOM); ONTOLOGY = AnnotationBuilder.fromClass(elements, Ontology.class); - POLY_ONTOLOGY = OntologyUtils.createOntologyAnnotationByValues(processingEnv, OntologyValue.POLY); + POLY_ONTOLOGY = + OntologyUtils.createOntologyAnnotationByValues(processingEnv, OntologyValue.POLY); ontologyValuesElement = TreeUtils.getMethod(Ontology.class, "values", processingEnv); From abbebe3835a0565916a005c4940379da4143b2ef Mon Sep 17 00:00:00 2001 From: zcai Date: Wed, 9 Feb 2022 01:20:33 -0500 Subject: [PATCH 3/7] add glbOfOntologyValues helper function --- .../OntologyAnnotatedTypeFactory.java | 18 +++++----------- src/ontology/util/OntologyUtils.java | 21 +++++++++++++++++++ 2 files changed, 26 insertions(+), 13 deletions(-) diff --git a/src/ontology/OntologyAnnotatedTypeFactory.java b/src/ontology/OntologyAnnotatedTypeFactory.java index 6bd5d6d..a6dd58c 100644 --- a/src/ontology/OntologyAnnotatedTypeFactory.java +++ b/src/ontology/OntologyAnnotatedTypeFactory.java @@ -105,21 +105,13 @@ public boolean isSubtype(AnnotationMirror subQualifier, AnnotationMirror superQu throw new BugInCF("unexpected annotation mirrors: %s, %s", a1, a2); } - Set a1Set = OntologyUtils.getOntologyValuesSet(a1); - Set 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; - } + EnumSet a1Set = OntologyUtils.getOntologyValuesSet(a1); + EnumSet a2Set = OntologyUtils.getOntologyValuesSet(a2); - a1Set.addAll(a2Set); // computes the union of the two sets return OntologyUtils.createOntologyAnnotationByValues( - processingEnv, a1Set.toArray(new OntologyValue[] {})); + processingEnv, + OntologyUtils.glbOfOntologyValues(a1Set, a2Set).toArray(new OntologyValue[]{}) + ); } @Override diff --git a/src/ontology/util/OntologyUtils.java b/src/ontology/util/OntologyUtils.java index be11a54..aafa913 100644 --- a/src/ontology/util/OntologyUtils.java +++ b/src/ontology/util/OntologyUtils.java @@ -158,6 +158,7 @@ public static EnumSet lubOfOntologyValues( || valueSet2.contains(OntologyValue.POLY)) { lub.add(OntologyValue.TOP); } else { + // computes the intersection of the two sets lub.addAll(valueSet1); lub.retainAll(valueSet2); } @@ -165,6 +166,26 @@ public static EnumSet lubOfOntologyValues( return lub; } + public static EnumSet glbOfOntologyValues( + EnumSet valueSet1, EnumSet valueSet2) { + EnumSet glb = EnumSet.noneOf(OntologyValue.class); + + if (valueSet1.contains(OntologyValue.POLY) && valueSet2.contains(OntologyValue.POLY)) { + glb.add(OntologyValue.POLY); + } else if (valueSet1.contains(OntologyValue.BOTTOM) + || valueSet2.contains(OntologyValue.BOTTOM) + || valueSet1.contains(OntologyValue.POLY) + || valueSet2.contains(OntologyValue.POLY)) { + glb.add(OntologyValue.BOTTOM); + } else { + // computes the union of the two sets + glb.addAll(valueSet1); + glb.addAll(valueSet2); + } + + return glb; + } + /** * check whether the passed values are validated as arguments of Ontology qualifier valid values * should not be null, and contains at least one ontology value, and doesn't cotains null From 27ae168327767b236a5b7f557fb75e6dc040e7c0 Mon Sep 17 00:00:00 2001 From: zcai Date: Wed, 9 Feb 2022 01:46:39 -0500 Subject: [PATCH 4/7] fix formatting --- src/ontology/OntologyAnnotatedTypeFactory.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ontology/OntologyAnnotatedTypeFactory.java b/src/ontology/OntologyAnnotatedTypeFactory.java index a6dd58c..a019810 100644 --- a/src/ontology/OntologyAnnotatedTypeFactory.java +++ b/src/ontology/OntologyAnnotatedTypeFactory.java @@ -110,8 +110,8 @@ public boolean isSubtype(AnnotationMirror subQualifier, AnnotationMirror superQu return OntologyUtils.createOntologyAnnotationByValues( processingEnv, - OntologyUtils.glbOfOntologyValues(a1Set, a2Set).toArray(new OntologyValue[]{}) - ); + OntologyUtils.glbOfOntologyValues(a1Set, a2Set) + .toArray(new OntologyValue[] {})); } @Override From f66452e0367cea5ae2a7dd16bdb89181999b32e7 Mon Sep 17 00:00:00 2001 From: zcai Date: Wed, 9 Feb 2022 14:41:25 -0500 Subject: [PATCH 5/7] add well-formedness check for ontology values --- src/ontology/OntologyTypeValidator.java | 57 +++++++++++++++++++++++++ src/ontology/OntologyVisitor.java | 14 ++++++ src/ontology/messages.properties | 1 + 3 files changed, 72 insertions(+) create mode 100644 src/ontology/OntologyTypeValidator.java create mode 100644 src/ontology/messages.properties diff --git a/src/ontology/OntologyTypeValidator.java b/src/ontology/OntologyTypeValidator.java new file mode 100644 index 0000000..7c7520f --- /dev/null +++ b/src/ontology/OntologyTypeValidator.java @@ -0,0 +1,57 @@ +package ontology; + +import checkers.inference.InferenceValidator; +import checkers.inference.InferenceVisitor; +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; + +import javax.lang.model.element.AnnotationMirror; +import javax.tools.Diagnostic; +import java.util.ArrayList; +import java.util.List; +import java.util.Set; + +/** + * 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 isTopLevelValidType( + QualifierHierarchy qualifierHierarchy, AnnotatedTypeMirror type + ) { + List errorMsgs = new ArrayList<>(super.isTopLevelValidType(qualifierHierarchy, type)); + + AnnotationMirror am = type.getAnnotation(Ontology.class); + if (am != null) { + Set 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; + } +} diff --git a/src/ontology/OntologyVisitor.java b/src/ontology/OntologyVisitor.java index beefdd3..8b34762 100644 --- a/src/ontology/OntologyVisitor.java +++ b/src/ontology/OntologyVisitor.java @@ -1,8 +1,17 @@ package ontology; import checkers.inference.InferenceChecker; +import checkers.inference.InferenceValidator; import checkers.inference.InferenceVisitor; +import com.sun.source.tree.Tree; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; +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; + +import java.util.List; public class OntologyVisitor extends InferenceVisitor { @@ -13,4 +22,9 @@ public OntologyVisitor( boolean infer) { super(checker, ichecker, factory, infer); } + + @Override + protected InferenceValidator createTypeValidator() { + return new OntologyTypeValidator(checker, this, atypeFactory); + } } diff --git a/src/ontology/messages.properties b/src/ontology/messages.properties new file mode 100644 index 0000000..229a2ad --- /dev/null +++ b/src/ontology/messages.properties @@ -0,0 +1 @@ +type.invalid.conflicting.elements=invalid type: conflicting elements in annotation %s of type "%s" From e1f6bc912bdef745c38121fe02ede322aaa2f43a Mon Sep 17 00:00:00 2001 From: zcai Date: Wed, 9 Feb 2022 15:23:59 -0500 Subject: [PATCH 6/7] add well-formedness test --- testing/WellFormednessTest.java | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 testing/WellFormednessTest.java diff --git a/testing/WellFormednessTest.java b/testing/WellFormednessTest.java new file mode 100644 index 0000000..5bacec7 --- /dev/null +++ b/testing/WellFormednessTest.java @@ -0,0 +1,11 @@ +import ontology.qual.Ontology; +import ontology.qual.OntologyValue; + +public class WellFormednessTest { + // :: error: (type.invalid.conflicting.elements) + @Ontology(values={OntologyValue.POLY, OntologyValue.FORCE_3D}) String invalidPoly; + // :: error: (type.invalid.conflicting.elements) + @Ontology(values={OntologyValue.TOP, OntologyValue.FORCE_3D}) String invalidTop; + // :: error: (type.invalid.conflicting.elements) + @Ontology(values={OntologyValue.BOTTOM, OntologyValue.FORCE_3D}) String invalidBottom; +} From 0d34a9cb8e749e32ceca356c822120d4df46f972 Mon Sep 17 00:00:00 2001 From: zcai Date: Wed, 9 Feb 2022 15:25:15 -0500 Subject: [PATCH 7/7] fix formatting --- src/ontology/OntologyTypeValidator.java | 38 +++++++++++++------------ src/ontology/OntologyVisitor.java | 8 ------ 2 files changed, 20 insertions(+), 26 deletions(-) diff --git a/src/ontology/OntologyTypeValidator.java b/src/ontology/OntologyTypeValidator.java index 7c7520f..2acde06 100644 --- a/src/ontology/OntologyTypeValidator.java +++ b/src/ontology/OntologyTypeValidator.java @@ -2,6 +2,11 @@ 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; @@ -11,32 +16,24 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.QualifierHierarchy; -import javax.lang.model.element.AnnotationMirror; -import javax.tools.Diagnostic; -import java.util.ArrayList; -import java.util.List; -import java.util.Set; - /** - * 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). + * 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 - ) { + AnnotatedTypeFactory atypeFactory) { super(checker, visitor, atypeFactory); } @Override protected List isTopLevelValidType( - QualifierHierarchy qualifierHierarchy, AnnotatedTypeMirror type - ) { - List errorMsgs = new ArrayList<>(super.isTopLevelValidType(qualifierHierarchy, type)); + QualifierHierarchy qualifierHierarchy, AnnotatedTypeMirror type) { + List errorMsgs = + new ArrayList<>(super.isTopLevelValidType(qualifierHierarchy, type)); AnnotationMirror am = type.getAnnotation(Ontology.class); if (am != null) { @@ -45,9 +42,14 @@ protected List isTopLevelValidType( 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)); + // 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)); } } } diff --git a/src/ontology/OntologyVisitor.java b/src/ontology/OntologyVisitor.java index 8b34762..31a507f 100644 --- a/src/ontology/OntologyVisitor.java +++ b/src/ontology/OntologyVisitor.java @@ -3,15 +3,7 @@ import checkers.inference.InferenceChecker; import checkers.inference.InferenceValidator; import checkers.inference.InferenceVisitor; -import com.sun.source.tree.Tree; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; -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; - -import java.util.List; public class OntologyVisitor extends InferenceVisitor {