Package 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	Description
protected final ExecutableElement	ensuresLockHeldIfExpressionElement	The EnsuresLockHeldIf.expression element/field.
protected final ExecutableElement	ensuresLockHeldValueElement	The EnsuresLockHeld.value element/field.
protected final AnnotationMirror	GUARDEDBY	The @GuardedBy annotation.
protected final AnnotationMirror	GUARDEDBYBOTTOM	The @GuardedByBottom annotation.
protected final AnnotationMirror	GUARDEDBYUNKNOWN	The @GuardedByUnknown annotation.
protected final ExecutableElement	guardedByValueElement	The value() element/field of a @GuardedBy annotation.
protected final AnnotationMirror	GUARDSATISFIED	The @GuardSatisfied annotation.
protected final ExecutableElement	guardSatisfiedValueElement	The value() element/field of a @GuardSatisfied annotation.
protected final @Nullable Class<? extends Annotation>	javaxGuardedBy	The javax.annotation.concurrent.GuardedBy annotation, or null if not on the classpath.
protected final @Nullable Class<? extends Annotation>	jcipGuardedBy	The net.jcip.annotations.GuardedBy annotation, or null if not on the classpath.
protected final AnnotationMirror	LOCKHELD	The @LockHeld annotation.
protected final AnnotationMirror	LOCKPOSSIBLYHELD	The @LockPossiblyHeld annotation.
protected final AnnotationMirror	NEWOBJECT	The @NewObject annotation.
static final String	NOT_EFFECTIVELY_FINAL	dependent type annotation error message for when the expression is not effectively final.
protected final AnnotationMirror	SIDEEFFECTFREE	The @SideEffectFree annotation.

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

analysis, arraysAreRelevant, cfgVisualizer, contractsUtils, defaults, dependentTypesHelper, emptyStore, exceptionalExitStores, flowByDefault, flowResult, flowResultAnalysisCaches, formalParameterPattern, hasOrIsSubchecker, initializationStaticStore, initializationStore, methodInvocationStores, poly, regularExitStores, relevantJavaTypes, returnStatementStores, scannedClasses, shouldClearSubcheckerSharedCFGs, sideEffectsUnrefineAliases, subcheckerSharedCFG, transfer, treeAnnotator, typeAnnotator

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

ajavaTypes, annotatedForValueElement, artificialTreeToEnclosingElementMap, checker, currentFileAjavaTypes, elements, ensuresQualifierExpressionElement, ensuresQualifierIfExpressionElement, ensuresQualifierIfListTM, ensuresQualifierIfListValueElement, ensuresQualifierIfResultElement, ensuresQualifierIfTM, ensuresQualifierListTM, ensuresQualifierListValueElement, ensuresQualifierTM, fieldInvariantFieldElement, fieldInvariantQualifierElement, fromExpressionTreeCache, fromMemberTreeCache, fromTypeTreeCache, hasQualifierParameterValueElement, ignoreUninferredTypeArguments, loader, methodValClassNameElement, methodValMethodNameElement, methodValParamsElement, noQualifierParameterValueElement, objectGetClass, processingEnv, qualHierarchy, qualifierUpperBounds, reflectionResolver, requiresQualifierExpressionElement, requiresQualifierListTM, requiresQualifierListValueElement, requiresQualifierTM, root, shouldCache, stubTypes, trees, typeArgumentInference, typeFormatter, typeHierarchy, types, typeVarSubstitutor, uid, wpiOutputFormat

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method	Description
void	addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, boolean useFlow)	Like GenericAnnotatedTypeFactory.addComputedTypeAnnotations(Tree, AnnotatedTypeMirror).
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).
protected DependentTypesHelper	createDependentTypesHelper()	Creates a DependentTypesHelper and returns it.
protected LockAnalysis	createFlowAnalysis()	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 given 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.
boolean	isSideEffectFree(ExecutableElement method)	Returns true if the given method is side-effect-free according to this AnnotationProvider — that is, if a call to the given method does not undo flow-sensitive type refinement.
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, addComputedTypeAnnotationsForWarnRedundant, addDefaultAnnotations, addSharedCFGForTree, addUncheckedStandardDefaults, analyze, annotationsForIrrelevantJavaType, applyInferredAnnotations, applyQualifierParameterDefaults, applyQualifierParameterDefaults, checkAndPerformFlowAnalysis, checkForDefaultQualifierInHierarchy, constructorFromUse, constructorFromUsePreSubstitution, createAndInitQualifierDefaults, createCFGVisualizer, createContractsFromMethod, createDefaultForTypeAnnotator, createDefaultForUseTypeAnnotator, createQualifierDefaults, createQualifierPolymorphism, createRequiresOrEnsuresQualifier, createTypeAnnotator, getAnnotatedTypeLhs, getAnnotatedTypeLhsNoTypeVarDefault, getAnnotatedTypeRhsUnaryAssign, getAnnotatedTypeVarargsArray, getAnnotationFromJavaExpression, getAnnotationFromJavaExpressionString, getAnnotationMirrorFromJavaExpressionString, getAnnotationsFromJavaExpression, getCFGVisualizer, getContractAnnotations, getContractAnnotations, getContractExpressions, getContractsFromMethod, getDefaultAnnotations, getDefaultAnnotationsForWarnRedundant, getDefaultForTypeAnnotator, getDefaultValueAnnotatedType, getDependentTypesHelper, getEmptyStore, getEnsuresQualifierIfResult, getExceptionalExitStore, getExplicitNewClassAnnos, getExplicitNewClassClassTypeArgs, getExpressionAndOffsetFromJavaExpressionString, getFinalLocalValues, getFirstNodeOfKindForTree, getInferredValueFor, getMethodReturnType, getNodesForTree, getPostconditionAnnotations, getPostconditionAnnotations, getPostconditionAnnotations, getPreconditionAnnotations, getPreconditionAnnotations, getPreconditionAnnotations, getPreOrPostconditionAnnotations, getQualifierPolymorphism, getRegularExitStore, getResultingTypeOfConstructorMemberReference, getReturnStatementStores, getSharedCFGForTree, getShouldDefaultTypeVarLocals, getSortedQualifierNames, getStoreAfter, getStoreAfter, getStoreAfter, getStoreBefore, getStoreBefore, getStoreBefore, getSupportedMonotonicTypeQualifiers, getTypeFactoryOfSubchecker, getTypeFactoryOfSubcheckerOrNull, handleCFGViz, irrelevantExtraMessage, isIgnoredExceptionType, isRelevant, isRelevant, isRelevantImpl, isUnreachable, methodFromUse, methodFromUsePreSubstitution, parseJavaExpressionString, performFlowAnalysis, postAnalyze, postAsMemberOf, postDirectSuperTypes, postInit, preProcessClassTree, setRoot, typeVariablesFromUse

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

adaptGetClassReturnTypeToReceiver, addAliasedDeclAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAnnotationFromFieldInvariant, addInheritedAnnotation, applyCaptureConversion, applyCaptureConversion, applyUnboxing, areSameByClass, binaryTreeArgTypes, binaryTreeArgTypes, canonicalAnnotation, checkInvalidOptionsInferSignatures, compoundAssignmentTreeArgTypes, containsSameByClass, containsUninferredTypeArguments, createAnnotatedTypeFormatter, createAnnotationClassLoader, createAnnotationFormatter, createQualifierUpperBounds, createTypeArgumentInference, createTypeHierarchy, createTypeVariableSubstitutor, declarationFromElement, doesAnnotatedForApplyToThisChecker, fromElement, fromElement, fromElement, fromNewClass, getAnnotatedNullType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedTypeFormatter, getAnnotatedTypeFromTypeTree, getAnnotationByClass, getAnnotationFormatter, getAnnotationMirror, getAnnotationWithMetaAnnotation, getBoxedType, getBundledTypeQualifiers, getCacheSize, getChecker, getCheckerNames, getContractExpressions, getContractListValues, getCurrentClassTree, getCurrentMethodReceiver, getDeclAnnotation, getDeclAnnotationNoAliases, getDeclAnnotations, getDeclAnnotationWithMetaAnnotation, getDefaultTypeDeclarationBounds, getDummyAssignedTo, getElementUtils, getEnclosingClassOrMethod, getEnclosingElementForArtificialTree, getEnclosingSubType, getEnclosingType, getEnumConstructorQualifiers, getExpressionAndOffset, getFieldInvariantAnnotationTree, getFieldInvariantDeclarationAnnotations, getFieldInvariants, getFnInterfaceFromTree, getFunctionTypeFromTree, getFunctionTypeFromTree, getImplicitReceiverType, getIterableElementType, getIterableElementType, getMethodReturnType, getNarrowedAnnotations, getNarrowedPrimitive, getPath, getProcessingEnv, getQualifierHierarchy, getQualifierParameterHierarchies, getQualifierParameterHierarchies, getQualifierUpperBounds, getReceiverType, getSelfType, getStringType, getSupportedTypeQualifierNames, getSupportedTypeQualifiers, getTreeUtils, getTypeArgumentInference, getTypeDeclarationBounds, getTypeHierarchy, getTypeOfExtendsImplements, getTypeVarSubstitutor, getUnboxedType, getUninferredWildcardType, getVisitorTreePath, getWholeProgramInference, getWidenedAnnotations, getWidenedType, getWidenedType, hasExplicitNoQualifierParameterInHierarchy, hasExplicitQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, initializeReflectionResolution, isDeterministic, isFromByteCode, isFromStubFile, isImmutable, isSupportedQualifier, isSupportedQualifier, isSupportedQualifier, isWithinConstructor, logGat, makeConditionConsistentWithOtherMethod, mergeAnnotationFileAnnosIntoType, negateConstant, order, parseAnnotationFiles, postProcessClassTree, replaceAnnotations, replaceAnnotations, setEnclosingElementForArtificialTree, setVisitorTreePath, shouldWarnIfStubRedundantWithBytecode, toAnnotatedType, toString, type, wpiAdjustForUpdateField, wpiAdjustForUpdateNonField, wpiPrepareMethodForWriting, wpiPrepareMethodForWriting, wpiShouldInferTypesForReceivers

Methods inherited from class java.lang.Object

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

Field Details

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 @GuardedBy annotation.

NEWOBJECT

protected final AnnotationMirror NEWOBJECT

The @NewObject annotation.

GUARDEDBYBOTTOM

protected final AnnotationMirror GUARDEDBYBOTTOM

The @GuardedByBottom annotation.

GUARDSATISFIED

protected final AnnotationMirror GUARDSATISFIED

The @GuardSatisfied annotation.

guardedByValueElement

protected final ExecutableElement guardedByValueElement

The value() element/field of a @GuardedBy annotation.

guardSatisfiedValueElement

protected final ExecutableElement guardSatisfiedValueElement

The value() element/field of a @GuardSatisfied annotation.

ensuresLockHeldValueElement

protected final ExecutableElement ensuresLockHeldValueElement

The EnsuresLockHeld.value element/field.

ensuresLockHeldIfExpressionElement

protected final ExecutableElement ensuresLockHeldIfExpressionElement

The EnsuresLockHeldIf.expression element/field.

jcipGuardedBy

protected final @Nullable Class<? extends Annotation> jcipGuardedBy

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

javaxGuardedBy

protected final @Nullable Class<? extends Annotation> javaxGuardedBy

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

Constructor Details

LockAnnotatedTypeFactory

public LockAnnotatedTypeFactory(BaseTypeChecker checker)

Create a new LockAnnotatedTypeFactory.

Method Details

createDependentTypesHelper

protected DependentTypesHelper createDependentTypesHelper()

Description copied from class: GenericAnnotatedTypeFactory

Creates a DependentTypesHelper and returns it. Use GenericAnnotatedTypeFactory.getDependentTypesHelper() to access the value.

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

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>

Returns:

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

createFlowTransferFunction

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

Description copied from class: GenericAnnotatedTypeFactory

Returns the appropriate transfer function that is used for the given 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>

Parameters:

analysis - a dataflow analysis

Returns:

a new transfer function

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

isSideEffectFree

public boolean isSideEffectFree(ExecutableElement method)

Description copied from interface: AnnotationProvider

Returns true if the given method is side-effect-free according to this AnnotationProvider — that is, if a call to the given method does not undo flow-sensitive type refinement.

Note that this method takes account of this AnnotationProvider's semantics, whereas org.checkerframework.dataflow.util.PurityUtils#isSideEffectFree does not.

Specified by:

isSideEffectFree in interface AnnotationProvider

Overrides:

isSideEffectFree in class AnnotatedTypeFactory

Parameters:

method - a method

Returns:

true if a call to the method does not undo flow-sensitive type refinement