org.checkerframework.common.accumulation

Class AccumulationAnnotatedTypeFactory

java.lang.Object

org.checkerframework.framework.type.AnnotatedTypeFactory

org.checkerframework.framework.type.GenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis>

org.checkerframework.common.basetype.BaseAnnotatedTypeFactory

org.checkerframework.common.accumulation.AccumulationAnnotatedTypeFactory

All Implemented Interfaces:

AnnotationProvider

public abstract class AccumulationAnnotatedTypeFactory
extends BaseAnnotatedTypeFactory

An annotated type factory for an accumulation checker.

New accumulation checkers should extend this class and implement a constructor, which should take a BaseTypeChecker and call both the constructor defined in this class and GenericAnnotatedTypeFactory.postInit().

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected class	AccumulationAnnotatedTypeFactory.AccumulationQualifierHierarchy All accumulation analyses share a similar type hierarchy.
protected class	AccumulationAnnotatedTypeFactory.AccumulationTreeAnnotator This tree annotator implements the following rule(s): RRA If a method returns its receiver, and the receiver has an accumulation type, then the default type of the method's return value is the type of the receiver.

Nested classes/interfaces inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory

GenericAnnotatedTypeFactory.ScanState

Nested classes/interfaces inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory

AnnotatedTypeFactory.ParameterizedExecutableType

Field Summary

Fields

Modifier and Type	Field and Description
AnnotationMirror	bottom The canonical bottom annotation for this accumulation checker.
AnnotationMirror	top The canonical top annotation for this accumulation checker: an instance of the accumulator annotation with no arguments.

Fields inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory

analysis, cfgVisualizer, defaults, dependentTypesHelper, emptyStore, exceptionalExitStores, flowByDefault, flowResult, flowResultAnalysisCaches, initializationStaticStore, initializationStore, methodInvocationStores, poly, regularExitStores, returnStatementStores, scannedClasses, transfer, treeAnnotator, typeAnnotator

Fields inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory

checker, elements, fromExpressionTreeCache, fromMemberTreeCache, fromTypeTreeCache, ignoreUninferredTypeArguments, loader, objectGetClass, processingEnv, qualHierarchy, qualifierUpperBounds, reflectionResolver, root, shouldCache, stubTypes, trees, typeArgumentInference, typeFormatter, typeHierarchy, types, typeVarSubstitutor, uid, visitorState

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	AccumulationAnnotatedTypeFactory(BaseTypeChecker checker, Class<? extends Annotation> accumulator, Class<? extends Annotation> bottom) Create an annotated type factory for an accumulation checker.
protected	AccumulationAnnotatedTypeFactory(BaseTypeChecker checker, Class<? extends Annotation> accumulator, Class<? extends Annotation> bottom, @Nullable Class<? extends Annotation> predicate) Create an annotated type factory for an accumulation checker.

Method Summary

Modifier and Type	Method and Description
protected String	convertToPredicate(AnnotationMirror anno) Converts the given annotation mirror to a predicate.
AnnotationMirror	createAccumulatorAnnotation(List<String> values) Creates a new instance of the accumulator annotation that contains the elements of values.
AnnotationMirror	createAccumulatorAnnotation(String value) Creates a new instance of the accumulator annotation that contains exactly one value.
protected AnnotationMirror	createPredicateAnnotation(String p) Creates a new predicate annotation from the given string.
QualifierHierarchy	createQualifierHierarchy(MultiGraphQualifierHierarchy.MultiGraphFactory factory) Factory method to easily change what QualifierHierarchy is created.
protected TreeAnnotator	createTreeAnnotator() Returns a TreeAnnotator that adds annotations to a type based on the contents of a tree.
protected boolean	evaluatePredicate(AnnotationMirror subAnno, String pred) Evaluates whether the accumulator annotation subAnno makes the predicate pred true.
protected boolean	evaluatePredicate(List<String> trueVariables, String pred) Evaluates whether treating the variables in trueVariables as true literals (and all other names as false literals) makes the predicate pred evaluate to true.
List<String>	getAccumulatedValues(AnnotationMirror anno) Returns all the values that anno has accumulated.
boolean	isAccumulatorAnnotation(AnnotationMirror anm) Is the given annotation an accumulator annotation? Returns false if the argument is bottom.
protected boolean	isPredicate(AnnotationMirror anno) Returns true if anno is a predicate annotation.
protected boolean	isPredicateSubtype(String p, String q) Extension point for subtyping behavior between predicates.
boolean	returnsThis(MethodInvocationTree tree) Returns true if the return type of the given method invocation tree has an @This annotation from the Returns Receiver Checker.

Methods inherited from class org.checkerframework.common.basetype.BaseAnnotatedTypeFactory

createFlowAnalysis

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

addAnnotationsFromDefaultForType, addCheckedCodeDefaults, addCheckedStandardDefaults, addComputedTypeAnnotations, addComputedTypeAnnotations, addComputedTypeAnnotations, addDefaultAnnotations, addUncheckedStandardDefaults, analyze, applyInferredAnnotations, applyQualifierParameterDefaults, applyQualifierParameterDefaults, checkAndPerformFlowAnalysis, checkForDefaultQualifierInHierarchy, constructorFromUse, constructorFromUsePreSubstitution, createAndInitQualifierDefaults, createCFGVisualizer, createDefaultForTypeAnnotator, createDefaultForUseTypeAnnotator, createDependentTypesHelper, createFlowTransferFunction, createQualifierDefaults, createQualifierPolymorphism, createTypeAnnotator, fromNewClass, getAnnotatedTypeLhs, getAnnotatedTypeLhsNoTypeVarDefault, getAnnotatedTypeRhsUnaryAssign, getAnnotatedTypeVarargsArray, getAnnotationFromJavaExpressionString, getAnnotationFromReceiver, getAnnotationMirrorFromJavaExpressionString, getCFGVisualizer, getDependentTypesHelper, getEmptyStore, getExceptionalExitStore, getFinalLocalValues, getFirstNodeOfKindForTree, getInferredValueFor, getMethodReturnType, getMethodReturnType, getNodesForTree, getQualifierPolymorphism, getReceiverAndOffsetFromJavaExpressionString, getReceiverFromJavaExpressionString, getRegularExitStore, getResultingTypeOfConstructorMemberReference, getReturnStatementStores, getShouldDefaultTypeVarLocals, getSortedQualifierNames, getStoreAfter, getStoreAfter, getStoreAfter, getStoreBefore, getStoreBefore, getStoreBefore, getSupportedMonotonicTypeQualifiers, getTypeFactoryOfSubchecker, handleCFGViz, methodFromUse, methodFromUsePreSubstitution, performFlowAnalysis, postAnalyze, postAsMemberOf, postDirectSuperTypes, postInit, preProcessClassTree, setRoot, typeVariablesFromUse

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

adaptGetClassReturnTypeToReceiver, addAliasedAnnotation, addAliasedAnnotation, addAliasedAnnotation, addAliasedAnnotation, addAliasedDeclAnnotation, addAnnotationFromFieldInvariant, addInheritedAnnotation, areSameByClass, canonicalAnnotation, checkInvalidOptionsInferSignatures, containsSameByClass, createAnnotatedTypeFormatter, createAnnotationClassLoader, createAnnotationFormatter, createQualifierHierarchy, createQualifierHierarchy, createQualifierHierarchyFactory, createQualifierUpperBounds, createSupportedTypeQualifiers, createTypeArgumentInference, createTypeHierarchy, createTypeVariableSubstitutor, declarationFromElement, fromElement, fromElement, fromElement, getAnnotatedNullType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedTypeFormatter, getAnnotatedTypeFromTypeTree, getAnnotationByClass, getAnnotationFormatter, getAnnotationMirror, getAnnotationWithMetaAnnotation, getBoxedType, getBundledTypeQualifiers, getCacheSize, getContext, getCurrentClassTree, getCurrentClassType, getCurrentMethodReceiver, getDeclAnnotation, getDeclAnnotationNoAliases, getDeclAnnotations, getDeclAnnotationWithMetaAnnotation, getDefaultTypeDeclarationBounds, getDummyAssignedTo, getElementUtils, getEnclosingElementForArtificialTree, getEnclosingType, getExpressionAndOffset, getFieldInvariantAnnotationTree, getFieldInvariantDeclarationAnnotations, getFieldInvariants, getFnInterfaceFromTree, getFunctionTypeFromTree, getFunctionTypeFromTree, getImplicitReceiverType, getNarrowedPrimitive, getPath, getProcessingEnv, getQualifierHierarchy, getQualifierParameterHierarchies, getQualifierParameterHierarchies, getQualifierUpperBounds, getReceiverType, getSelfType, getStringType, getSupportedTypeQualifierNames, getSupportedTypeQualifiers, getTreeUtils, getTypeArgumentInference, getTypeDeclarationBounds, getTypeHierarchy, getTypeOfExtendsImplements, getTypeVarSubstitutor, getUnboxedType, getUninferredWildcardType, getVisitorState, getWholeProgramInference, hasExplicitNoQualifierParameterInHierarchy, hasExplicitQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, initializeReflectionResolution, isAnyEnclosingThisDeref, isFromByteCode, isFromStubFile, isMostEnclosingThisDeref, isSupportedQualifier, isSupportedQualifier, isSupportedQualifier, isWithinConstructor, mergeStubsIntoType, methodFromUse, negateConstant, parseStubFiles, postProcessClassTree, postTypeVarSubstitution, setEnclosingElementForArtificialTree, shouldWarnIfStubRedundantWithBytecode, toAnnotatedType, toString, type, widenToUpperBound

Methods inherited from class java.lang.Object

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

Field Detail

top

public final AnnotationMirror top

The canonical top annotation for this accumulation checker: an instance of the accumulator annotation with no arguments.

bottom

public final AnnotationMirror bottom

The canonical bottom annotation for this accumulation checker.

Constructor Detail

AccumulationAnnotatedTypeFactory

protected AccumulationAnnotatedTypeFactory(BaseTypeChecker checker,
                                           Class<? extends Annotation> accumulator,
                                           Class<? extends Annotation> bottom,
                                           @Nullable Class<? extends Annotation> predicate)

Create an annotated type factory for an accumulation checker.

Parameters:

checker - the checker

accumulator - the accumulator type in the hierarchy. Must be an annotation with a single argument named "value" whose type is a String array.

bottom - the bottom type in the hierarchy, which must be a subtype of accumulator. The bottom type should be an annotation with no arguments.

predicate - the predicate annotation. Either null (if predicates are not supported), or an annotation with a single element named "value" whose type is a String.

AccumulationAnnotatedTypeFactory

protected AccumulationAnnotatedTypeFactory(BaseTypeChecker checker,
                                           Class<? extends Annotation> accumulator,
                                           Class<? extends Annotation> bottom)

Create an annotated type factory for an accumulation checker.

Parameters:

checker - the checker

accumulator - the accumulator type in the hierarchy. Must be an annotation with a single argument named "value" whose type is a String array.

bottom - the bottom type in the hierarchy, which must be a subtype of accumulator. The bottom type should be an annotation with no arguments.

Method Detail

createAccumulatorAnnotation

public AnnotationMirror createAccumulatorAnnotation(List<String> values)

Creates a new instance of the accumulator annotation that contains the elements of values.

Parameters:

values - the arguments to the annotation. The values can contain duplicates and can be in any order.

Returns:

an annotation mirror representing the accumulator annotation with values's arguments; this is top if values is empty

createAccumulatorAnnotation

public AnnotationMirror createAccumulatorAnnotation(String value)

Creates a new instance of the accumulator annotation that contains exactly one value.

Parameters:

value - the argument to the annotation

Returns:

an annotation mirror representing the accumulator annotation with value as its argument

returnsThis

public boolean returnsThis(MethodInvocationTree tree)

Returns true if the return type of the given method invocation tree has an @This annotation from the Returns Receiver Checker.

Parameters:

tree - a method invocation tree

Returns:

true if the method being invoked returns its receiver

isAccumulatorAnnotation

public boolean isAccumulatorAnnotation(AnnotationMirror anm)

Is the given annotation an accumulator annotation? Returns false if the argument is bottom.

Parameters:

anm - an annotation mirror

Returns:

true if the annotation mirror is an instance of this factory's accumulator annotation

createTreeAnnotator

protected TreeAnnotator createTreeAnnotator()

Description copied from class: GenericAnnotatedTypeFactory

Returns a TreeAnnotator that adds annotations to a type based on the contents of a tree.

The default tree annotator is a ListTreeAnnotator of the following:

1. PropagationTreeAnnotator: Propagates annotations from subtrees
2. LiteralTreeAnnotator: Adds annotations based on QualifierForLiterals meta-annotations
3. DependentTypesTreeAnnotator: Adapts dependent annotations based on context

Subclasses may override this method to specify additional tree annotators, for example:

 new ListTreeAnnotator(super.createTreeAnnotator(), new KeyLookupTreeAnnotator(this));
 

Overrides:

createTreeAnnotator in class GenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis>

Returns:

a tree annotator

createQualifierHierarchy

public QualifierHierarchy createQualifierHierarchy(MultiGraphQualifierHierarchy.MultiGraphFactory factory)

Description copied from class: AnnotatedTypeFactory

Factory method to easily change what QualifierHierarchy is created. Needs to be public only because the GraphFactory must be able to call this method. No external use of this method is necessary.

Overrides:

createQualifierHierarchy in class AnnotatedTypeFactory

getAccumulatedValues

public List<String> getAccumulatedValues(AnnotationMirror anno)

Returns all the values that anno has accumulated.

Parameters:

anno - an accumulator annotation; must not be bottom

Returns:

the list of values the annotation has accumulated; it is a new list, so it is safe for clients to side-effect

isPredicateSubtype

protected boolean isPredicateSubtype(String p,
                                     String q)

Extension point for subtyping behavior between predicates. This implementation conservatively returns true only if the predicates are equal, or if the prospective supertype (q) is equivalent to top (that is, the empty string).

Parameters:

p - a predicate

q - another predicate

Returns:

true if p is a subtype of q

evaluatePredicate

protected boolean evaluatePredicate(AnnotationMirror subAnno,
                                    String pred)

Evaluates whether the accumulator annotation subAnno makes the predicate pred true.

Parameters:

subAnno - an accumulator annotation

pred - a predicate

Returns:

whether the accumulator annotation satisfies the predicate

evaluatePredicate

protected boolean evaluatePredicate(List<String> trueVariables,
                                    String pred)

Evaluates whether treating the variables in trueVariables as true literals (and all other names as false literals) makes the predicate pred evaluate to true.

Parameters:

trueVariables - a list of names that should be replaced with true

pred - a predicate

Returns:

whether the true variables satisfy the predicate

createPredicateAnnotation

protected AnnotationMirror createPredicateAnnotation(String p)

Creates a new predicate annotation from the given string.

Parameters:

p - a valid predicate

Returns:

an annotation representing that predicate

convertToPredicate

protected String convertToPredicate(AnnotationMirror anno)

Converts the given annotation mirror to a predicate.

Parameters:

anno - an annotation

Returns:

the predicate, as a String, that is equivalent to that annotation. May return the empty string.

isPredicate

protected boolean isPredicate(AnnotationMirror anno)

Returns true if anno is a predicate annotation.

Parameters:

anno - an annotation

Returns:

true if anno is a predicate annotation