org.checkerframework.checker.lock

Class LockAnnotatedTypeFactory

java.lang.Object

org.checkerframework.framework.type.AnnotatedTypeFactory

org.checkerframework.framework.type.GenericAnnotatedTypeFactory<CFValue,LockStore,LockTransfer,LockAnalysis>

org.checkerframework.checker.lock.LockAnnotatedTypeFactory

All Implemented Interfaces:

AnnotationProvider

public class LockAnnotatedTypeFactory
extends GenericAnnotatedTypeFactory<CFValue,LockStore,LockTransfer,LockAnalysis>

LockAnnotatedTypeFactory builds types with @LockHeld and @LockPossiblyHeld annotations. LockHeld identifies that an object is being used as a lock and is being held when a given tree is executed. LockPossiblyHeld is the default type qualifier for this hierarchy and applies to all fields, local variables and parameters -- hence it does not convey any information other than that it is not LockHeld.

However, there are a number of other annotations used in conjunction with these annotations to enforce proper locking.

See the Checker Framework Manual:

Lock Checker

Nested Class Summary

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
protected AnnotationMirror	GUARDEDBY The @GuardedByBottom annotation.
protected AnnotationMirror	GUARDEDBYBOTTOM The @GuardedByBottom annotation.
protected AnnotationMirror	GUARDEDBYUNKNOWN The @GuardedByUnknown annotation.
protected AnnotationMirror	GUARDSATISFIED The @GuardSatisfied annotation.
protected Class<? extends Annotation>	javaxGuardedBy The javax.annotation.concurrent.GuardedBy annotation, or null if not on the classpath.
protected Class<? extends Annotation>	jcipGuardedBy The net.jcip.annotations.GuardedBy annotation, or null if not on the classpath.
protected AnnotationMirror	LOCKHELD The @LockHeld annotation.
protected AnnotationMirror	LOCKPOSSIBLYHELD The @LockPossiblyHeld annotation.
static String	NOT_EFFECTIVELY_FINAL dependent type annotation error message for when the expression is not effectively final.
protected AnnotationMirror	SIDEEFFECTFREE The @SideEffectFree annotation.

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

artificialTreeToEnclosingElementMap, 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

Constructor and Description
LockAnnotatedTypeFactory(BaseTypeChecker checker) Create a new LockAnnotatedTypeFactory.

Method Summary

Modifier and Type	Method and Description
void	addComputedTypeAnnotations(Element elt, AnnotatedTypeMirror type) To add annotations to the type of method or constructor parameters, add a TypeAnnotator using GenericAnnotatedTypeFactory.createTypeAnnotator() and see the comment in TypeAnnotator.visitExecutable(org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType, Void).
void	addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, boolean useFlow) Like GenericAnnotatedTypeFactory.addComputedTypeAnnotations(Tree, AnnotatedTypeMirror).
protected DependentTypesHelper	createDependentTypesHelper() Creates an DependentTypesHelper and returns it.
protected LockAnalysis	createFlowAnalysis(List<Pair<VariableElement,CFValue>> fieldValues) Returns the appropriate flow analysis class that is used for the org.checkerframework.dataflow analysis.
LockTransfer	createFlowTransferFunction(CFAbstractAnalysis<CFValue,LockStore,LockTransfer> analysis) Returns the appropriate transfer function that is used for the org.checkerframework.dataflow analysis.
protected QualifierHierarchy	createQualifierHierarchy() Returns the QualifierHierarchy to be used by this checker.
protected Set<Class<? extends Annotation>>	createSupportedTypeQualifiers() Returns a mutable set of annotation classes that are supported by a checker.
protected TreeAnnotator	createTreeAnnotator() Returns a TreeAnnotator that adds annotations to a type based on the contents of a tree.
AnnotatedTypeFactory.ParameterizedExecutableType	methodFromUse(ExpressionTree tree, ExecutableElement methodElt, AnnotatedTypeMirror receiverType) Determines the type of the invoked method based on the passed expression tree, executable element, and receiver type.

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

addAnnotationsFromDefaultForType, addCheckedCodeDefaults, addCheckedStandardDefaults, addComputedTypeAnnotations, addDefaultAnnotations, addUncheckedStandardDefaults, analyze, applyInferredAnnotations, applyQualifierParameterDefaults, applyQualifierParameterDefaults, checkAndPerformFlowAnalysis, checkForDefaultQualifierInHierarchy, constructorFromUse, constructorFromUsePreSubstitution, createAndInitQualifierDefaults, createCFGVisualizer, createDefaultForTypeAnnotator, createDefaultForUseTypeAnnotator, 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, applyUnboxing, areSameByClass, binaryTreeArgTypes, canonicalAnnotation, checkInvalidOptionsInferSignatures, containsSameByClass, createAnnotatedTypeFormatter, createAnnotationClassLoader, createAnnotationFormatter, createQualifierHierarchyWithMultiGraphFactory, createQualifierUpperBounds, createTypeArgumentInference, createTypeHierarchy, createTypeVariableSubstitutor, declarationFromElement, fromElement, fromElement, fromElement, getAnnotatedNullType, getAnnotatedType, 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, getEnclosingClassOrMethod, 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, getWidenedAnnotations, getWidenedType, hasExplicitNoQualifierParameterInHierarchy, hasExplicitQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, initializeReflectionResolution, isFromByteCode, isFromStubFile, isSupportedQualifier, isSupportedQualifier, isSupportedQualifier, isWithinConstructor, mergeStubsIntoType, 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

NOT_EFFECTIVELY_FINAL

public static final String NOT_EFFECTIVELY_FINAL

dependent type annotation error message for when the expression is not effectively final.

See Also:

Constant Field Values

LOCKHELD

protected final AnnotationMirror LOCKHELD

The @LockHeld annotation.

LOCKPOSSIBLYHELD

protected final AnnotationMirror LOCKPOSSIBLYHELD

The @LockPossiblyHeld annotation.

SIDEEFFECTFREE

protected final AnnotationMirror SIDEEFFECTFREE

The @SideEffectFree annotation.

GUARDEDBYUNKNOWN

protected final AnnotationMirror GUARDEDBYUNKNOWN

The @GuardedByUnknown annotation.

GUARDEDBY

protected final AnnotationMirror GUARDEDBY

The @GuardedByBottom annotation.

GUARDEDBYBOTTOM

protected final AnnotationMirror GUARDEDBYBOTTOM

The @GuardedByBottom annotation.

GUARDSATISFIED

protected final AnnotationMirror GUARDSATISFIED

The @GuardSatisfied annotation.

jcipGuardedBy

protected final Class<? extends Annotation> jcipGuardedBy

The net.jcip.annotations.GuardedBy annotation, or null if not on the classpath.

javaxGuardedBy

protected final Class<? extends Annotation> javaxGuardedBy

The javax.annotation.concurrent.GuardedBy annotation, or null if not on the classpath.

Constructor Detail

LockAnnotatedTypeFactory

public LockAnnotatedTypeFactory(BaseTypeChecker checker)

Create a new LockAnnotatedTypeFactory.

Method Detail

createDependentTypesHelper

protected DependentTypesHelper createDependentTypesHelper()

Description copied from class: GenericAnnotatedTypeFactory

Creates an DependentTypesHelper and returns it.

Overrides:

createDependentTypesHelper in class GenericAnnotatedTypeFactory<CFValue,LockStore,LockTransfer,LockAnalysis>

Returns:

a new DependentTypesHelper

createSupportedTypeQualifiers

protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers()

Description copied from class: AnnotatedTypeFactory

Returns a mutable set of annotation classes that are supported by a checker.

Subclasses may override this method to return a mutable set of their supported type qualifiers through one of the 5 approaches shown below.

Subclasses should not call this method; they should call AnnotatedTypeFactory.getSupportedTypeQualifiers() instead.

By default, a checker supports all annotations located in a subdirectory called qual that's located in the same directory as the checker. Note that only annotations defined with the @Target({ElementType.TYPE_USE}) meta-annotation (and optionally with the additional value of ElementType.TYPE_PARAMETER, but no other ElementType values) are automatically considered as supported annotations.

To support a different set of annotations than those in the qual subdirectory, or that have other ElementType values, see examples below.

In total, there are 5 ways to indicate annotations that are supported by a checker:

1. Only support annotations located in a checker's qual directory:

   This is the default behavior. Simply place those annotations within the qual directory.

2. Support annotations located in a checker's qual directory and a list of other annotations:

   Place those annotations within the qual directory, and override AnnotatedTypeFactory.createSupportedTypeQualifiers() by calling AnnotatedTypeFactory.getBundledTypeQualifiers(Class...) with a varargs parameter list of the other annotations. Code example:

     @Override protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
         return getBundledTypeQualifiers(Regex.class, PartialRegex.class, RegexBottom.class, UnknownRegex.class);
     } 
    

3. Supporting only annotations that are explicitly listed: Override AnnotatedTypeFactory.createSupportedTypeQualifiers() and return a mutable set of the supported annotations. Code example:

     @Override protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
         return new HashSet<Class<? extends Annotation>>(
                 Arrays.asList(A.class, B.class));
     } 
    

   The set of qualifiers returned by AnnotatedTypeFactory.createSupportedTypeQualifiers() must be a fresh, mutable set. The methods AnnotatedTypeFactory.getBundledTypeQualifiers(Class...) must return a fresh, mutable set

Overrides:

createSupportedTypeQualifiers in class AnnotatedTypeFactory

Returns:

the type qualifiers supported this processor, or an empty set if none

createQualifierHierarchy

protected QualifierHierarchy createQualifierHierarchy()

Description copied from class: AnnotatedTypeFactory

Returns the QualifierHierarchy to be used by this checker.

The implementation builds the type qualifier hierarchy for the AnnotatedTypeFactory.getSupportedTypeQualifiers() using the meta-annotations found in them. The current implementation returns an instance of NoElementQualifierHierarchy.

Subclasses must override this method if their qualifiers have elements; the method must return an implementation of QualifierHierarchy, such as ElementQualifierHierarchy.

Overrides:

createQualifierHierarchy in class AnnotatedTypeFactory

Returns:

a QualifierHierarchy for this type system

createFlowAnalysis

protected LockAnalysis createFlowAnalysis(List<Pair<VariableElement,CFValue>> fieldValues)

Description copied from class: GenericAnnotatedTypeFactory

Returns the appropriate flow analysis class that is used for the org.checkerframework.dataflow analysis.

This implementation uses the checker naming convention to create the appropriate analysis. If no transfer function is found, it returns an instance of CFAnalysis.

Subclasses have to override this method to create the appropriate analysis if they do not follow the checker naming convention.

Overrides:

createFlowAnalysis in class GenericAnnotatedTypeFactory<CFValue,LockStore,LockTransfer,LockAnalysis>

createFlowTransferFunction

public LockTransfer createFlowTransferFunction(CFAbstractAnalysis<CFValue,LockStore,LockTransfer> analysis)

Description copied from class: GenericAnnotatedTypeFactory

Returns the appropriate transfer function that is used for the org.checkerframework.dataflow analysis.

This implementation uses the checker naming convention to create the appropriate transfer function. If no transfer function is found, it returns an instance of CFTransfer.

Subclasses have to override this method to create the appropriate transfer function if they do not follow the checker naming convention.

Overrides:

createFlowTransferFunction in class GenericAnnotatedTypeFactory<CFValue,LockStore,LockTransfer,LockAnalysis>

methodFromUse

public AnnotatedTypeFactory.ParameterizedExecutableType methodFromUse(ExpressionTree tree,
                                                                      ExecutableElement methodElt,
                                                                      AnnotatedTypeMirror receiverType)

Description copied from class: AnnotatedTypeFactory

Determines the type of the invoked method based on the passed expression tree, executable element, and receiver type.

Overrides:

methodFromUse in class AnnotatedTypeFactory

Parameters:

tree - either a MethodInvocationTree or a MemberReferenceTree

methodElt - the element of the referenced method

receiverType - the type of the receiver

Returns:

the method type being invoked with tree and the (inferred) type arguments

See Also:

AnnotatedTypeFactory.methodFromUse(MethodInvocationTree)

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,LockStore,LockTransfer,LockAnalysis>

Returns:

a tree annotator

addComputedTypeAnnotations

public void addComputedTypeAnnotations(Element elt,
                                       AnnotatedTypeMirror type)

Description copied from class: GenericAnnotatedTypeFactory

To add annotations to the type of method or constructor parameters, add a TypeAnnotator using GenericAnnotatedTypeFactory.createTypeAnnotator() and see the comment in TypeAnnotator.visitExecutable(org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType, Void).

Overrides:

addComputedTypeAnnotations in class GenericAnnotatedTypeFactory<CFValue,LockStore,LockTransfer,LockAnalysis>

Parameters:

elt - an element

type - the type obtained from elt

addComputedTypeAnnotations

public void addComputedTypeAnnotations(Tree tree,
                                       AnnotatedTypeMirror type,
                                       boolean useFlow)

Description copied from class: GenericAnnotatedTypeFactory

Like GenericAnnotatedTypeFactory.addComputedTypeAnnotations(Tree, AnnotatedTypeMirror). Overriding implementations typically simply pass the boolean to calls to super.

Overrides:

addComputedTypeAnnotations in class GenericAnnotatedTypeFactory<CFValue,LockStore,LockTransfer,LockAnalysis>

Parameters:

tree - an AST node

type - the type obtained from tree

useFlow - whether to use information from dataflow analysis