org.checkerframework.common.aliasing

Class AliasingVisitor

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<AliasingAnnotatedTypeFactory>

org.checkerframework.common.aliasing.AliasingVisitor

All Implemented Interfaces:

com.sun.source.tree.TreeVisitor<java.lang.Void,java.lang.Void>

public class AliasingVisitor
extends BaseTypeVisitor<AliasingAnnotatedTypeFactory>

This visitor ensures that every constructor whose result is annotated as @Unique does not leak aliases.

TODO: Implement @NonLeaked and @LeakedToResult verifications:

@NonLeaked: When a method declaration has a parameter annotated as @NonLeaked, the method body must not leak a reference to that parameter.

@LeakedToResult: When a method declaration has a parameter annotated as @LeakedToResult, the method body must not leak a reference to that parameter, except at the method return statements.

Both of the checks above are similar to the @Unique check that is implemented in this visitor.

Nested Class Summary

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

BaseTypeVisitor.OverrideChecker

Field Summary

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

Constructor Summary

Constructors

Constructor and Description
AliasingVisitor(BaseTypeChecker checker)

Method Summary

Modifier and Type	Method and Description
protected void	commonAssignmentCheck(AnnotatedTypeMirror varType, AnnotatedTypeMirror valueType, com.sun.source.tree.Tree valueTree, @CompilerMessageKey java.lang.String errorKey) Checks the validity of an assignment (or pseudo-assignment) from a value to a variable and emits an error message (through the compiler's messaging interface) if it is not valid.
protected void	commonAssignmentCheck(com.sun.source.tree.Tree varTree, com.sun.source.tree.ExpressionTree valueExp, @CompilerMessageKey java.lang.String errorKey) Checks the validity of an assignment (or pseudo-assignment) from a value to a variable and emits an error message (through the compiler's messaging interface) if it is not valid.
java.lang.Void	visitMethodInvocation(com.sun.source.tree.MethodInvocationTree node, java.lang.Void p) Checks that if a method call is being invoked inside a constructor with result type @Unique, it must not leak the "this" reference.
java.lang.Void	visitNewArray(com.sun.source.tree.NewArrayTree node, java.lang.Void p)
java.lang.Void	visitThrow(com.sun.source.tree.ThrowTree node, java.lang.Void p) Checks the type of a thrown exception.
java.lang.Void	visitVariable(com.sun.source.tree.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, checkOverride, checkPostcondition, checkPreconditions, checkThrownExpression, checkTypeArguments, checkTypecastRedundancy, checkTypecastSafety, checkVarargs, commonAssignmentCheck, createOverrideChecker, createTypeFactory, createTypeValidator, enclosingMemberSelect, enclosingStatement, getExceptionParameterLowerBoundAnnotations, getThrowUpperBoundAnnotations, getTypeFactory, isAccessAllowed, isAssignable, isValidUse, isValidUse, isValidUse, isVectorCopyInto, processClassTree, reportPurityErrors, scan, setRoot, shouldSkipUses, skipReceiverSubtypeCheck, testTypevarContainment, typeCheckVectorCopyIntoArgument, validateType, validateTypeOf, visitAnnotation, visitArrayAccess, visitAssignment, visitCatch, visitClass, visitCompilationUnit, visitCompoundAssignment, visitConditionalExpression, visitEnhancedForLoop, visitIdentifier, visitInstanceOf, visitLambdaExpression, visitMemberReference, visitMethod, visitNewClass, visitParameterizedType, visitReturn, visitTry, 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, visitBinary, visitBlock, visitBreak, visitCase, visitContinue, visitDoWhileLoop, visitEmptyStatement, visitErroneous, visitExpressionStatement, visitForLoop, visitIf, visitImport, visitIntersectionType, visitLabeledStatement, visitLiteral, visitMemberSelect, visitModifiers, visitOther, visitParenthesized, visitPrimitiveType, visitSwitch, visitSynchronized, visitUnionType, visitWhileLoop, visitWildcard

Methods inherited from class java.lang.Object

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

Constructor Detail

AliasingVisitor

public AliasingVisitor(BaseTypeChecker checker)

Method Detail

visitMethodInvocation

public java.lang.Void visitMethodInvocation(com.sun.source.tree.MethodInvocationTree node,
                                            java.lang.Void p)

Checks that if a method call is being invoked inside a constructor with result type @Unique, it must not leak the "this" reference. There are 3 ways to make sure that this is not happening:

1. this is not an argument of the method call.
2. this is an argument of the method call, but the respective parameter is annotated as @NonLeaked.
3. this is an argument of the method call, but the respective parameter is annotated as @LeakedToResult AND the result of the method call is not being stored (the method call is a statement).

The private method isUniqueCheck handles cases 2 and 3.

Specified by:

visitMethodInvocation in interface com.sun.source.tree.TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitMethodInvocation in class BaseTypeVisitor<AliasingAnnotatedTypeFactory>

commonAssignmentCheck

protected void commonAssignmentCheck(com.sun.source.tree.Tree varTree,
                                     com.sun.source.tree.ExpressionTree valueExp,
                                     @CompilerMessageKey java.lang.String errorKey)

Description copied from class: BaseTypeVisitor

Checks the validity of an assignment (or pseudo-assignment) from a value to a variable and emits an error message (through the compiler's messaging interface) if it is not valid.

Overrides:

commonAssignmentCheck in class BaseTypeVisitor<AliasingAnnotatedTypeFactory>

Parameters:

varTree - the AST node for the lvalue (usually a variable)

valueExp - the AST node for the rvalue (the new value)

errorKey - the error message to use if the check fails (must be a compiler message key, see CompilerMessageKey)

commonAssignmentCheck

protected void commonAssignmentCheck(AnnotatedTypeMirror varType,
                                     AnnotatedTypeMirror valueType,
                                     com.sun.source.tree.Tree valueTree,
                                     @CompilerMessageKey java.lang.String errorKey)

Description copied from class: BaseTypeVisitor

Checks the validity of an assignment (or pseudo-assignment) from a value to a variable and emits an error message (through the compiler's messaging interface) if it is not valid.

Overrides:

commonAssignmentCheck in class BaseTypeVisitor<AliasingAnnotatedTypeFactory>

Parameters:

varType - the annotated type of the variable

valueType - the annotated type of the value

valueTree - the location to use when reporting the error message

errorKey - the error message to use if the check fails (must be a compiler message key, see CompilerMessageKey)

visitThrow

public java.lang.Void visitThrow(com.sun.source.tree.ThrowTree node,
                                 java.lang.Void p)

Description copied from class: BaseTypeVisitor

Checks the type of a thrown exception. Subclasses should override checkThrownExpression(ThrowTree node) rather than this method to change the behavior of this check.

Specified by:

visitThrow in interface com.sun.source.tree.TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitThrow in class BaseTypeVisitor<AliasingAnnotatedTypeFactory>

visitVariable

public java.lang.Void visitVariable(com.sun.source.tree.VariableTree node,
                                    java.lang.Void p)

Specified by:

visitVariable in interface com.sun.source.tree.TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitVariable in class BaseTypeVisitor<AliasingAnnotatedTypeFactory>

visitNewArray

public java.lang.Void visitNewArray(com.sun.source.tree.NewArrayTree node,
                                    java.lang.Void p)

Specified by:

visitNewArray in interface com.sun.source.tree.TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitNewArray in class BaseTypeVisitor<AliasingAnnotatedTypeFactory>