org.checkerframework.common.accumulation

Class AccumulationAnnotatedTypeFactory.AccumulationQualifierHierarchy

java.lang.Object

org.checkerframework.framework.util.MultiGraphQualifierHierarchy

org.checkerframework.common.accumulation.AccumulationAnnotatedTypeFactory.AccumulationQualifierHierarchy

All Implemented Interfaces:

QualifierHierarchy

Enclosing class:

AccumulationAnnotatedTypeFactory

protected class AccumulationAnnotatedTypeFactory.AccumulationQualifierHierarchy
extends MultiGraphQualifierHierarchy

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.)

Nested Class Summary

Nested classes/interfaces inherited from class org.checkerframework.framework.util.MultiGraphQualifierHierarchy

MultiGraphQualifierHierarchy.MultiGraphFactory

Field Summary

Fields inherited from class org.checkerframework.framework.util.MultiGraphQualifierHierarchy

bottoms, polyQualifiers, supertypesDirect, supertypesTransitive, tops

Constructor Summary

Constructors

Constructor and Description
AccumulationQualifierHierarchy(MultiGraphQualifierHierarchy.MultiGraphFactory factory) Create the qualifier hierarchy.

Method Summary

Modifier and Type	Method and Description
AnnotationMirror	getTopAnnotation(AnnotationMirror start) Return the top qualifier for the given qualifier, that is, the qualifier that is a supertype of qualifier but no further supertypes exist.
AnnotationMirror	greatestLowerBound(AnnotationMirror a1, 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.
boolean	isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) isSubtype in this type system is subset.
AnnotationMirror	leastUpperBound(AnnotationMirror a1, 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.

Methods inherited from class org.checkerframework.framework.util.MultiGraphQualifierHierarchy

addPolyRelations, findBottoms, findLub, findTops, finish, getBottomAnnotation, getBottomAnnotations, getPolymorphicAnnotation, getTopAnnotations, isPolymorphicQualifier, isSubtype, isValid, toString, transitiveClosure

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface org.checkerframework.framework.type.QualifierHierarchy

assertSameSize, assertSameSize, canHaveEmptyAnnotationSet, findAnnotationInHierarchy, findAnnotationInSameHierarchy, getWidth, greatestLowerBound, greatestLowerBounds, greatestLowerBounds, greatestLowerBoundsTypeVariable, greatestLowerBoundTypeVariable, isSubtype, isSubtype, isSubtypeTypeVariable, isSubtypeTypeVariable, leastUpperBound, leastUpperBounds, leastUpperBounds, leastUpperBoundsTypeVariable, leastUpperBoundTypeVariable, numberOfIterationsBeforeWidening, updateMappingToMutableSet, widenedUpperBound

Constructor Detail

AccumulationQualifierHierarchy

public AccumulationQualifierHierarchy(MultiGraphQualifierHierarchy.MultiGraphFactory factory)

Create the qualifier hierarchy.

Parameters:

factory - the factory

Method Detail

getTopAnnotation

public AnnotationMirror getTopAnnotation(AnnotationMirror start)

Description copied from interface: QualifierHierarchy

Return the top qualifier for the given qualifier, that is, the qualifier that is a supertype of qualifier but no further supertypes exist.

Specified by:

getTopAnnotation in interface QualifierHierarchy

Overrides:

getTopAnnotation in class MultiGraphQualifierHierarchy

Parameters:

start - any qualifier from one of the qualifier hierarchies represented by this

Returns:

the top qualifier of qualifier's hierarchy

greatestLowerBound

public AnnotationMirror greatestLowerBound(AnnotationMirror a1,
                                           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:

greatestLowerBound in interface QualifierHierarchy

Overrides:

greatestLowerBound in class MultiGraphQualifierHierarchy

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

leastUpperBound

public AnnotationMirror leastUpperBound(AnnotationMirror a1,
                                        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:

leastUpperBound in interface QualifierHierarchy

Overrides:

leastUpperBound in class MultiGraphQualifierHierarchy

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

isSubtype

public boolean isSubtype(AnnotationMirror subAnno,
                         AnnotationMirror superAnno)

isSubtype in this type system is subset.

Specified by:

isSubtype in interface QualifierHierarchy

Overrides:

isSubtype in class MultiGraphQualifierHierarchy

Parameters:

subAnno - the sub qualifier

superAnno - the super qualifier

Returns:

true iff subQualifier is a subqualifier of, or equal to, superQualifier