Class AccumulationAnnotatedTypeFactory.AccumulationQualifierHierarchy
- java.lang.Object
-
- org.checkerframework.framework.type.QualifierHierarchy
-
- org.checkerframework.framework.type.ElementQualifierHierarchy
-
- org.checkerframework.common.accumulation.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 ofAccPred("A || B")
, because when A is replaced withtrue
and B is replaced withfalse
, 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 overrideAccumulationAnnotatedTypeFactory.isPredicateSubtype(String, String)
if they require more precise subtyping; the check described here is overly conservative (and therefore sound), but not very precise.)
-
-
Field Summary
-
Fields inherited from class org.checkerframework.framework.type.ElementQualifierHierarchy
bottoms, bottomsMap, kindToElementlessQualifier, qualifierKindHierarchy, tops, topsMap
-
Fields inherited from class org.checkerframework.framework.type.QualifierHierarchy
atypeFactory
-
-
Constructor Summary
Constructors Modifier Constructor Description 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.
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description 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.boolean
isSubtypeQualifiers(javax.lang.model.element.AnnotationMirror subAnno, javax.lang.model.element.AnnotationMirror superAnno)
Tests whethersubQualifier
is equal to or a sub-qualifier ofsuperQualifier
, according to the type qualifier hierarchy, ignoring Java basetypes.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.-
Methods inherited from class org.checkerframework.framework.type.ElementQualifierHierarchy
createBottomsMap, createElementlessQualifierMap, createQualifierKindHierarchy, createTopsMap, findAnnotationInHierarchy, findAnnotationInSameHierarchy, getBottomAnnotation, getBottomAnnotations, getPolymorphicAnnotation, getQualifierKind, getQualifierKind, getTopAnnotation, getTopAnnotations, isPolymorphicQualifier, isValid
-
Methods inherited from class org.checkerframework.framework.type.QualifierHierarchy
assertSameSize, assertSameSize, canHaveEmptyAnnotationSet, getWidth, greatestLowerBoundQualifiersOnly, greatestLowerBoundShallow, greatestLowerBoundsShallow, isSubtypeQualifiersOnly, isSubtypeShallow, isSubtypeShallow, isSubtypeShallow, isSubtypeShallow, leastUpperBoundQualifiersOnly, leastUpperBoundShallow, leastUpperBoundsShallow, numberOfIterationsBeforeWidening, updateMappingToMutableSet, widenedUpperBound
-
-
-
-
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 hierarchyelements
- 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 classQualifierHierarchy
- Parameters:
a1
- first qualifiera2
- 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 classQualifierHierarchy
- Parameters:
a1
- the first qualifier; may not be in the same hierarchy asqualifier2
a2
- the second qualifier; may not be in the same hierarchy asqualifier1
- Returns:
- the least upper bound of the qualifiers, or
null
if the qualifiers are from different hierarchies
-
isSubtypeQualifiers
public boolean isSubtypeQualifiers(javax.lang.model.element.AnnotationMirror subAnno, javax.lang.model.element.AnnotationMirror superAnno)
Tests whethersubQualifier
is equal to or a sub-qualifier ofsuperQualifier
, according to the type qualifier hierarchy, ignoring Java basetypes.Clients should generally call
QualifierHierarchy.isSubtypeShallow(javax.lang.model.element.AnnotationMirror, javax.lang.model.type.TypeMirror, javax.lang.model.element.AnnotationMirror, javax.lang.model.type.TypeMirror)
. However, subtypes should generally override this method (if needed).This method behaves the same as
QualifierHierarchy.isSubtypeQualifiersOnly(AnnotationMirror, AnnotationMirror)
, which calls this method. This method is for clients inside the framework, and it hasprotected
access to prevent use by clients outside the framework. This makes it easy to find places where code outside the framework is ignoring Java basetypes -- at calls toQualifierHierarchy.isSubtypeQualifiersOnly(javax.lang.model.element.AnnotationMirror, javax.lang.model.element.AnnotationMirror)
.isSubtype in this type system is subset.
- Specified by:
isSubtypeQualifiers
in classQualifierHierarchy
- Parameters:
subAnno
- possible subqualifiersuperAnno
- possible superqualifier- Returns:
- true iff
subQualifier
is a subqualifier of, or equal to,superQualifier
-
-