org.checkerframework.common.aliasing

Class AliasingTransfer

java.lang.Object

org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<TransferResult<V,S>,TransferInput<V,S>>

org.checkerframework.framework.flow.CFAbstractTransfer<CFValue,CFStore,CFTransfer>

org.checkerframework.framework.flow.CFTransfer

org.checkerframework.common.aliasing.AliasingTransfer

All Implemented Interfaces:

TransferFunction<CFValue,CFStore>, NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

public class AliasingTransfer
extends CFTransfer

Type refinement is treated in the usual way, except that at (pseudo-)assignments the RHS may lose its type refinement, before the LHS is type-refined.

The RHS always loses its type refinement (it is widened to @MaybeAliased, and its declared type must have been @MaybeAliased) except in the following cases:

1. The RHS is a fresh expression.
2. The LHS is a @NonLeaked formal parameter and the RHS is an argument in a method call or constructor invocation.
3. The LHS is a @LeakedToResult formal parameter, the RHS is an argument in a method call or constructor invocation, and the method's return value is discarded.

Field Summary

Fields inherited from class org.checkerframework.framework.flow.CFAbstractTransfer

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor and Description
AliasingTransfer(CFAbstractAnalysis<CFValue,CFStore,CFTransfer> analysis)

Method Summary

Modifier and Type	Method and Description
protected void	processPostconditions(MethodInvocationNode n, CFStore store, javax.lang.model.element.ExecutableElement methodElement, com.sun.source.tree.Tree tree) Handling pseudo-assignments.
TransferResult<CFValue,CFStore>	visitAssignment(AssignmentNode n, TransferInput<CFValue,CFStore> in) Case 1: For every assignment, the LHS is refined if the RHS has type @Unique and is a method invocation or a new class instance.
TransferResult<CFValue,CFStore>	visitMethodInvocation(MethodInvocationNode n, TransferInput<CFValue,CFStore> in) Case 3: Given a method invocation expression, if the parent of the expression is not a statement, check if there are any arguments of the method call annotated as @LeakedToResult and remove it from the store, since it might be leaked.

Methods inherited from class org.checkerframework.framework.flow.CFAbstractTransfer

addInformationFromPreconditions, finishValue, finishValue, getTypeFactoryOfSubchecker, getValueFromFactory, getValueWithSameAnnotations, initialStore, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, setFixedInitialStore, splitAssignments, strengthenAnnotationOfEqualTo, usesSequentialSemantics, visitArrayAccess, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitFieldAccess, visitLocalVariable, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitReturn, visitStringConcatenateAssignment, visitStringConversion, visitTernaryExpression, visitThisLiteral, visitVariableDeclaration, visitWideningConversion

Methods inherited from class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor

visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThisLiteral, visitInstanceOf, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLessThan, visitLessThanOrEqual, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitUnsignedRightShift, visitValueLiteral

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.checkerframework.dataflow.cfg.node.NodeVisitor

visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThisLiteral, visitInstanceOf, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLessThan, visitLessThanOrEqual, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitUnsignedRightShift

Constructor Detail

AliasingTransfer

public AliasingTransfer(CFAbstractAnalysis<CFValue,CFStore,CFTransfer> analysis)

Method Detail

visitAssignment

public TransferResult<CFValue,CFStore> visitAssignment(AssignmentNode n,
                                                       TransferInput<CFValue,CFStore> in)

Case 1: For every assignment, the LHS is refined if the RHS has type @Unique and is a method invocation or a new class instance.

Specified by:

visitAssignment in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

Overrides:

visitAssignment in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

processPostconditions

protected void processPostconditions(MethodInvocationNode n,
                                     CFStore store,
                                     javax.lang.model.element.ExecutableElement methodElement,
                                     com.sun.source.tree.Tree tree)

Handling pseudo-assignments. Called by CFAbstractTransfer.visitMethodInvocation().

Case 2: Given a method call, traverses all formal parameters of the method declaration, and if it doesn't have the @NonLeaked or @LeakedToResult annotations, we remove the node of the respective argument in the method call from the store. If parameter has @LeakedToResult, visitMethodInvocation() handles it.

Overrides:

processPostconditions in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitMethodInvocation

public TransferResult<CFValue,CFStore> visitMethodInvocation(MethodInvocationNode n,
                                                             TransferInput<CFValue,CFStore> in)

Case 3: Given a method invocation expression, if the parent of the expression is not a statement, check if there are any arguments of the method call annotated as @LeakedToResult and remove it from the store, since it might be leaked.

Specified by:

visitMethodInvocation in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

Overrides:

visitMethodInvocation in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>