Class AccumulationAnnotatedTypeFactory.AccumulationQualifierHierarchy

  • Enclosing class:
    AccumulationAnnotatedTypeFactory

    protected class AccumulationAnnotatedTypeFactory.AccumulationQualifierHierarchy
    extends ElementQualifierHierarchy
    All accumulation analyses share a similar type hierarchy. This class implements the subtyping, LUB, and GLB for that hierarchy. The lattice looks like:
           acc()
          /   \
     acc(x)   acc(y) ...
          \   /
         acc(x,y) ...
            |
          bottom
     
    Predicate subtyping is defined as follows:
    • An accumulator is a subtype of a predicate if substitution from the accumulator to the predicate makes the predicate true. For example, Acc(A) is a subtype of AccPred("A || B"), because when A is replaced with true and B is replaced with false, the resulting boolean formula evaluates to true.
    • A predicate P is a subtype of an accumulator iff after converting the accumulator into a predicate representing the conjunction of its elements, P is a subtype of that predicate according to the rule for subtyping between two predicates defined below.
    • A predicate P is a subtype of another predicate Q iff P and Q are equal. An extension point (AccumulationAnnotatedTypeFactory.isPredicateSubtype(String, String)) is provided to allow more complex subtyping behavior between predicates. (The "correct" subtyping rule is that P is a subtype of Q iff P implies Q. That rule would require an SMT solver in the general case, which is undesirable because it would require an external dependency. A user can override AccumulationAnnotatedTypeFactory.isPredicateSubtype(String, String) if they require more precise subtyping; the check described here is overly conservative (and therefore sound), but not very precise.)
    • Constructor Detail

      • AccumulationQualifierHierarchy

        protected AccumulationQualifierHierarchy​(java.util.Collection<java.lang.Class<? extends java.lang.annotation.Annotation>> qualifierClasses,
                                                 javax.lang.model.util.Elements elements)
        Creates a ElementQualifierHierarchy from the given classes.
        Parameters:
        qualifierClasses - classes of annotations that are the qualifiers for this hierarchy
        elements - element utils
    • Method Detail

      • greatestLowerBoundQualifiers

        public javax.lang.model.element.AnnotationMirror greatestLowerBoundQualifiers​(javax.lang.model.element.AnnotationMirror a1,
                                                                                      javax.lang.model.element.AnnotationMirror a2)
        GLB in this type system is set union of the arguments of the two annotations, unless one of them is bottom, in which case the result is also bottom.
        Specified by:
        greatestLowerBoundQualifiers in class QualifierHierarchy
        Parameters:
        a1 - first qualifier
        a2 - second qualifier
        Returns:
        greatest lower bound of the two annotations, or null if the two annotations are not from the same hierarchy
      • leastUpperBoundQualifiers

        public javax.lang.model.element.AnnotationMirror leastUpperBoundQualifiers​(javax.lang.model.element.AnnotationMirror a1,
                                                                                   javax.lang.model.element.AnnotationMirror a2)
        LUB in this type system is set intersection of the arguments of the two annotations, unless one of them is bottom, in which case the result is the other annotation.
        Specified by:
        leastUpperBoundQualifiers in class QualifierHierarchy
        Parameters:
        a1 - the first qualifier; may not be in the same hierarchy as qualifier2
        a2 - the second qualifier; may not be in the same hierarchy as qualifier1
        Returns:
        the least upper bound of the qualifiers, or null if the qualifiers are from different hierarchies