org.checkerframework.checker.lock

Class LockVisitor

java.lang.Object

com.sun.source.util.TreeScanner<R,P>

com.sun.source.util.TreePathScanner<R,P>

org.checkerframework.framework.source.SourceVisitor<java.lang.Void,java.lang.Void>

org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

org.checkerframework.checker.lock.LockVisitor

All Implemented Interfaces:

TreeVisitor<java.lang.Void,java.lang.Void>

public class LockVisitor
extends org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

The LockVisitor enforces the special type-checking rules described in the Lock Checker manual chapter.

See the Checker Framework Manual:

Lock Checker

Nested Class Summary

Nested classes/interfaces inherited from class org.checkerframework.common.basetype.BaseTypeVisitor

org.checkerframework.common.basetype.BaseTypeVisitor.OverrideChecker

Field Summary

Fields

Modifier and Type	Field and Description
protected static java.util.regex.Pattern	selfReceiverPattern

Fields inherited from class org.checkerframework.common.basetype.BaseTypeVisitor

atypeFactory, checker, contractsUtils, positions, typeValidator, visitorState

Fields inherited from class org.checkerframework.framework.source.SourceVisitor

elements, root, trees, treesWithSuppressWarnings, types

Constructor Summary

Constructors

Constructor and Description
LockVisitor(org.checkerframework.common.basetype.BaseTypeChecker checker)

Method Summary

Modifier and Type	Method and Description
protected boolean	checkOverride(MethodTree overriderTree, org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType enclosingType, org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType overridden, org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType overriddenType) Ensures that subclass methods are annotated with a stronger or equally strong side effect annotation than the parent class method.
protected void	commonAssignmentCheck(org.checkerframework.framework.type.AnnotatedTypeMirror varType, org.checkerframework.framework.type.AnnotatedTypeMirror valueType, Tree valueTree, @CompilerMessageKey java.lang.String errorKey)
LockAnnotatedTypeFactory	createTypeFactory()
protected java.util.Set<? extends javax.lang.model.element.AnnotationMirror>	getExceptionParameterLowerBoundAnnotations()
boolean	isValidUse(org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType declarationType, org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType useType, Tree tree) Skips the call to super and returns true.
void	processClassTree(ClassTree node) Disallows annotations from the @GuardedBy hierarchy on class declarations (other than @GuardedBy({}).
protected boolean	skipReceiverSubtypeCheck(MethodInvocationTree methodInvocationTree, org.checkerframework.framework.type.AnnotatedTypeMirror methodDefinitionReceiver, org.checkerframework.framework.type.AnnotatedTypeMirror methodCallReceiver) When visiting a method call, if the receiver formal parameter has type @GuardSatisfied and the receiver actual parameter has type @GuardedBy(...), this method verifies that the guard is satisfied, and it returns true, indicating that the receiver subtype check should be skipped.
java.lang.Void	visitAnnotation(AnnotationTree tree, java.lang.Void p)
java.lang.Void	visitArrayAccess(ArrayAccessTree tree, java.lang.Void p)
java.lang.Void	visitBinary(BinaryTree binaryTree, java.lang.Void p)
java.lang.Void	visitCompoundAssignment(CompoundAssignmentTree node, java.lang.Void p)
java.lang.Void	visitIdentifier(IdentifierTree tree, java.lang.Void p)
java.lang.Void	visitMemberSelect(MemberSelectTree tree, java.lang.Void p)
java.lang.Void	visitMethod(MethodTree node, java.lang.Void p) Issues an error if a method (explicitly or implicitly) annotated with @MayReleaseLocks has a formal parameter or receiver (explicitly or implicitly) annotated with @GuardSatisfied.
java.lang.Void	visitMethodInvocation(MethodInvocationTree node, java.lang.Void p) When visiting a method invocation, issue an error if the side effect annotation on the called method causes the side effect guarantee of the enclosing method to be violated.
java.lang.Void	visitSynchronized(SynchronizedTree node, java.lang.Void p) When visiting a synchronized block, issue an error if the expression has a type that implements the java.util.concurrent.locks.Lock interface.
java.lang.Void	visitVariable(VariableTree node, java.lang.Void p)

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

checkAccess, checkArguments, checkArrayInitialization, checkAssignability, checkConditionalPostcondition, checkConstructorInvocation, checkContract, checkDefaultConstructor, checkExceptionParameter, checkFieldInvariantDeclarations, checkForAnnotatedJdk, checkMethodInvocability, checkMethodReferenceAsOverride, checkOverride, checkPostcondition, checkPreconditions, checkThrownExpression, checkTypeArguments, checkTypecastRedundancy, checkTypecastSafety, checkVarargs, commonAssignmentCheck, commonAssignmentCheck, createOverrideChecker, createTypeValidator, enclosingMemberSelect, enclosingStatement, getThrowUpperBoundAnnotations, getTypeFactory, isAccessAllowed, isAssignable, isValidUse, isValidUse, isVectorCopyInto, reportPurityErrors, scan, setRoot, shouldSkipUses, testTypevarContainment, typeCheckVectorCopyIntoArgument, validateType, validateTypeOf, visitAssignment, visitCatch, visitClass, visitCompilationUnit, visitConditionalExpression, visitEnhancedForLoop, visitInstanceOf, visitLambdaExpression, visitMemberReference, visitNewArray, visitNewClass, visitParameterizedType, visitReturn, visitThrow, visitTypeCast, visitTypeParameter, visitUnary

Methods inherited from class org.checkerframework.framework.source.SourceVisitor

visit

Methods inherited from class com.sun.source.util.TreePathScanner

getCurrentPath, scan

Methods inherited from class com.sun.source.util.TreeScanner

reduce, scan, visitAnnotatedType, visitArrayType, visitAssert, visitBlock, visitBreak, visitCase, visitContinue, visitDoWhileLoop, visitEmptyStatement, visitErroneous, visitExpressionStatement, visitForLoop, visitIf, visitImport, visitIntersectionType, visitLabeledStatement, visitLiteral, visitModifiers, visitOther, visitParenthesized, visitPrimitiveType, visitSwitch, visitTry, visitUnionType, visitWhileLoop, visitWildcard

Methods inherited from class java.lang.Object

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

Field Detail

selfReceiverPattern

protected static final java.util.regex.Pattern selfReceiverPattern

Constructor Detail

LockVisitor

public LockVisitor(org.checkerframework.common.basetype.BaseTypeChecker checker)

Method Detail

visitVariable

public java.lang.Void visitVariable(VariableTree node,
                                    java.lang.Void p)

Specified by:

visitVariable in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitVariable in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

createTypeFactory

public LockAnnotatedTypeFactory createTypeFactory()

Overrides:

createTypeFactory in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

visitMethod

public java.lang.Void visitMethod(MethodTree node,
                                  java.lang.Void p)

Issues an error if a method (explicitly or implicitly) annotated with @MayReleaseLocks has a formal parameter or receiver (explicitly or implicitly) annotated with @GuardSatisfied. Also issues an error if a synchronized method has a @LockingFree, @SideEffectFree or @Pure annotation.

Specified by:

visitMethod in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitMethod in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

Parameters:

node - the MethodTree of the method definition to visit

skipReceiverSubtypeCheck

protected boolean skipReceiverSubtypeCheck(MethodInvocationTree methodInvocationTree,
                                           org.checkerframework.framework.type.AnnotatedTypeMirror methodDefinitionReceiver,
                                           org.checkerframework.framework.type.AnnotatedTypeMirror methodCallReceiver)

When visiting a method call, if the receiver formal parameter has type @GuardSatisfied and the receiver actual parameter has type @GuardedBy(...), this method verifies that the guard is satisfied, and it returns true, indicating that the receiver subtype check should be skipped. If the receiver actual parameter has type @GuardSatisfied, this method simply returns true without performing any other actions. The method returns false otherwise.

Overrides:

skipReceiverSubtypeCheck in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

Parameters:

methodInvocationTree - the MethodInvocationTree of the method being called

methodDefinitionReceiver - the ATM of the formal receiver parameter of the method being called

methodCallReceiver - the ATM of the receiver argument of the method call

Returns:

whether the caller can skip the receiver subtype check

getExceptionParameterLowerBoundAnnotations

protected java.util.Set<? extends javax.lang.model.element.AnnotationMirror> getExceptionParameterLowerBoundAnnotations()

Overrides:

getExceptionParameterLowerBoundAnnotations in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

commonAssignmentCheck

protected void commonAssignmentCheck(org.checkerframework.framework.type.AnnotatedTypeMirror varType,
                                     org.checkerframework.framework.type.AnnotatedTypeMirror valueType,
                                     Tree valueTree,
                                     @CompilerMessageKey java.lang.String errorKey)

Overrides:

commonAssignmentCheck in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

visitMemberSelect

public java.lang.Void visitMemberSelect(MemberSelectTree tree,
                                        java.lang.Void p)

Specified by:

visitMemberSelect in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitMemberSelect in class TreeScanner<java.lang.Void,java.lang.Void>

checkOverride

protected boolean checkOverride(MethodTree overriderTree,
                                org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType enclosingType,
                                org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType overridden,
                                org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType overriddenType)

Ensures that subclass methods are annotated with a stronger or equally strong side effect annotation than the parent class method.

Overrides:

checkOverride in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

visitArrayAccess

public java.lang.Void visitArrayAccess(ArrayAccessTree tree,
                                       java.lang.Void p)

Specified by:

visitArrayAccess in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitArrayAccess in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

isValidUse

public boolean isValidUse(org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType declarationType,
                          org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType useType,
                          Tree tree)

Skips the call to super and returns true.

GuardedBy({}) is the default type on class declarations, which is a subtype of the top annotation @GuardedByUnknown. However, it is valid to declare an instance of a class with any annotation from the @GuardedBy hierarchy. Hence, this method returns true for annotations in the @GuardedBy hierarchy.

Also returns true for annotations in the @LockPossiblyHeld hierarchy since the default for that hierarchy is the top type and annotations from that hierarchy cannot be explicitly written in code.

Overrides:

isValidUse in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

visitMethodInvocation

public java.lang.Void visitMethodInvocation(MethodInvocationTree node,
                                            java.lang.Void p)

When visiting a method invocation, issue an error if the side effect annotation on the called method causes the side effect guarantee of the enclosing method to be violated. For example, a method annotated with @ReleasesNoLocks may not call a method annotated with @MayReleaseLocks. Also check that matching @GuardSatisfied(index) on a method's formal receiver/parameters matches those in corresponding locations on the method call site.

Specified by:

visitMethodInvocation in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitMethodInvocation in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

Parameters:

node - the MethodInvocationTree of the method call being visited

visitSynchronized

public java.lang.Void visitSynchronized(SynchronizedTree node,
                                        java.lang.Void p)

When visiting a synchronized block, issue an error if the expression has a type that implements the java.util.concurrent.locks.Lock interface. This prevents explicit locks from being accidentally used as built-in (monitor) locks. This is important because the Lock Checker does not have a mechanism to separately keep track of the explicit lock and the monitor lock of an expression that implements the Lock interface (i.e. there is a @LockHeld annotation used in dataflow, but there are not distinct @MonitorLockHeld and @ExplicitLockHeld annotations). It is assumed that both kinds of locks will never be held for any expression that implements Lock.

Additionally, a synchronized block may not be present in a method that has a @LockingFree guarantee or stronger. An error is issued in this case.

Specified by:

visitSynchronized in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitSynchronized in class TreeScanner<java.lang.Void,java.lang.Void>

Parameters:

node - the SynchronizedTree for the synchronized block being visited

visitAnnotation

public java.lang.Void visitAnnotation(AnnotationTree tree,
                                      java.lang.Void p)

Specified by:

visitAnnotation in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitAnnotation in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

visitIdentifier

public java.lang.Void visitIdentifier(IdentifierTree tree,
                                      java.lang.Void p)

Specified by:

visitIdentifier in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitIdentifier in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

processClassTree

public void processClassTree(ClassTree node)

Disallows annotations from the @GuardedBy hierarchy on class declarations (other than @GuardedBy({}).

Overrides:

processClassTree in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>

visitBinary

public java.lang.Void visitBinary(BinaryTree binaryTree,
                                  java.lang.Void p)

Specified by:

visitBinary in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitBinary in class TreeScanner<java.lang.Void,java.lang.Void>

visitCompoundAssignment

public java.lang.Void visitCompoundAssignment(CompoundAssignmentTree node,
                                              java.lang.Void p)

Specified by:

visitCompoundAssignment in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitCompoundAssignment in class org.checkerframework.common.basetype.BaseTypeVisitor<LockAnnotatedTypeFactory>