org.checkerframework.checker.index.upperbound

Class UpperBoundAnnotatedTypeFactory.UpperBoundQualifierHierarchy

java.lang.Object

org.checkerframework.framework.type.QualifierHierarchy

org.checkerframework.framework.util.MultiGraphQualifierHierarchy

org.checkerframework.checker.index.upperbound.UpperBoundAnnotatedTypeFactory.UpperBoundQualifierHierarchy

Enclosing class:

UpperBoundAnnotatedTypeFactory

protected final class UpperBoundAnnotatedTypeFactory.UpperBoundQualifierHierarchy
extends MultiGraphQualifierHierarchy

The qualifier hierarchy for the upperbound type system. The qh is responsible for determining the relationships within the qualifiers - especially subtyping relations.

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, polymorphicQualifier, polyQualifiers, supertypesGraph, supertypesMap, tops

Constructor Summary

Constructors

Constructor and Description
UpperBoundQualifierHierarchy(MultiGraphQualifierHierarchy.MultiGraphFactory factory)

Method Summary

Modifier and Type	Method and Description
AnnotationMirror	greatestLowerBound(AnnotationMirror a1, AnnotationMirror a2) Returns the greatest lower bound for the qualifiers a1 and a2.
boolean	implementsWidening() Returns whether or not this hierarchy implements QualifierHierarchy.widenUpperBound(AnnotationMirror, AnnotationMirror)
boolean	isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) Computes subtyping as per the subtyping in the qualifier hierarchy structure unless both annotations are the same.
AnnotationMirror	leastUpperBound(AnnotationMirror a1, AnnotationMirror a2) Determines the least upper bound of a1 and a2.
AnnotationMirror	widenUpperBound(AnnotationMirror a, AnnotationMirror b) If the type hierarchy has an infinite ascending chain, then the dataflow analysis might never reach a fixed point.

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

addPolyRelations, buildFullMap, findBottoms, findLub, findTops, finish, getBottomAnnotation, getBottomAnnotations, getPolymorphicAnnotation, getTopAnnotation, getTopAnnotations, getTypeQualifiers, greatestLowerBoundTypeVariable, isSubtype, isSubtypeTypeVariable, isSubtypeTypeVariable, leastUpperBoundTypeVariable, toString

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

canHaveEmptyAnnotationSet, findAnnotationInHierarchy, findAnnotationInSameHierarchy, findCorrespondingAnnotation, getAnnotationInHierarchy, getWidth, greatestLowerBound, greatestLowerBounds, greatestLowerBounds, greatestLowerBoundsTypeVariable, isSubtype, isSubtype, isValid, leastUpperBound, leastUpperBounds, leastUpperBounds, leastUpperBoundsTypeVariable, replacePolyAll, updateMappingToMutableSet

Methods inherited from class java.lang.Object

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

Constructor Detail

UpperBoundQualifierHierarchy

public UpperBoundQualifierHierarchy(MultiGraphQualifierHierarchy.MultiGraphFactory factory)

Parameters:

factory - MultiGraphFactory to use to construct this

Method Detail

greatestLowerBound

public AnnotationMirror greatestLowerBound(AnnotationMirror a1,
                                           AnnotationMirror a2)

Description copied from class: QualifierHierarchy

Returns the greatest lower bound for the qualifiers a1 and a2.

The two qualifiers have to be from the same qualifier hierarchy. Otherwise, null will be returned.

Overrides:

greatestLowerBound in class MultiGraphQualifierHierarchy

Parameters:

a1 - first annotation

a2 - second annotation

Returns:

greatest lower bound of the two annotations

leastUpperBound

public AnnotationMirror leastUpperBound(AnnotationMirror a1,
                                        AnnotationMirror a2)

Determines the least upper bound of a1 and a2. If a1 and a2 are both the same type of Value annotation, then the LUB is the result of taking the intersection of values from both a1 and a2.

Overrides:

leastUpperBound in class MultiGraphQualifierHierarchy

Returns:

the least upper bound of a1 and a2

widenUpperBound

public AnnotationMirror widenUpperBound(AnnotationMirror a,
                                        AnnotationMirror b)

Description copied from class: QualifierHierarchy

If the type hierarchy has an infinite ascending chain, then the dataflow analysis might never reach a fixed point. To prevent this, implement this method such that it returns an upper bound for the two qualifiers that is wider than the least upper bound. If this method is implemented, also override QualifierHierarchy.implementsWidening() and return true.

Otherwise, returns the least upper bound of the two annotations.

Overrides:

widenUpperBound in class QualifierHierarchy

Parameters:

a - annotation

b - annotation

Returns:

an upper bound that is wider than the least upper bound of a1 and a2 (or the lub if the type hierarchy does not require this)

implementsWidening

public boolean implementsWidening()

Description copied from class: QualifierHierarchy

Returns whether or not this hierarchy implements QualifierHierarchy.widenUpperBound(AnnotationMirror, AnnotationMirror)

Overrides:

implementsWidening in class QualifierHierarchy

Returns:

whether or not this hierarchy implements QualifierHierarchy.widenUpperBound(AnnotationMirror, AnnotationMirror)

isSubtype

public boolean isSubtype(AnnotationMirror subAnno,
                         AnnotationMirror superAnno)

Computes subtyping as per the subtyping in the qualifier hierarchy structure unless both annotations are the same. In this case, rhs is a subtype of lhs iff rhs contains at least every element of lhs.

Overrides:

isSubtype in class MultiGraphQualifierHierarchy

Parameters:

subAnno - the sub qualifier

superAnno - the super qualifier

Returns:

true if rhs is a subtype of lhs, false otherwise