Package org.checkerframework.common.value

Class ValueTransfer

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.value.ValueTransfer

All Implemented Interfaces:

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

public class ValueTransfer
extends CFTransfer

The transfer class for the Value Checker.

Field Summary

Fields

Modifier and Type	Field	Description
protected ValueAnnotatedTypeFactory	atypeFactory	The Value type factory.
protected QualifierHierarchy	qualHierarchy	The Value qualifier hierarchy.

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

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor	Description
ValueTransfer(CFAbstractAnalysis<CFValue,CFStore,CFTransfer> analysis)	Create a new ValueTransfer.

Method Summary

Modifier and Type	Method	Description
protected void	processConditionalPostconditions(MethodInvocationNode n, javax.lang.model.element.ExecutableElement methodElement, com.sun.source.tree.ExpressionTree tree, CFStore thenStore, CFStore elseStore)	Add information from the conditional postconditions of a method to the stores after an invocation.
protected TransferResult<CFValue,CFStore>	strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> transferResult, Node firstNode, Node secondNode, CFValue firstValue, CFValue secondValue, boolean notEqualTo)	Refine the annotation of secondNode if the annotation secondValue is less precise than firstValue.
TransferResult<CFValue,CFStore>	stringConcatenation(Node leftOperand, Node rightOperand, TransferInput<CFValue,CFStore> p, TransferResult<CFValue,CFStore> result)
TransferResult<CFValue,CFStore>	visitBitwiseAnd(BitwiseAndNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitBitwiseComplement(BitwiseComplementNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitBitwiseOr(BitwiseOrNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitBitwiseXor(BitwiseXorNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitConditionalAnd(ConditionalAndNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitConditionalNot(ConditionalNotNode n, TransferInput<CFValue,CFStore> p)	Reverse the role of the 'thenStore' and 'elseStore'.
TransferResult<CFValue,CFStore>	visitConditionalOr(ConditionalOrNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitEqualTo(EqualToNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitFieldAccess(FieldAccessNode node, TransferInput<CFValue,CFStore> in)
TransferResult<CFValue,CFStore>	visitFloatingDivision(FloatingDivisionNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitFloatingRemainder(FloatingRemainderNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitGreaterThan(GreaterThanNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitGreaterThanOrEqual(GreaterThanOrEqualNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitIntegerDivision(IntegerDivisionNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitIntegerRemainder(IntegerRemainderNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitLeftShift(LeftShiftNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitLessThan(LessThanNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitLessThanOrEqual(LessThanOrEqualNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitMethodInvocation(MethodInvocationNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitNotEqual(NotEqualNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitNumericalAddition(NumericalAdditionNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitNumericalMinus(NumericalMinusNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitNumericalMultiplication(NumericalMultiplicationNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitNumericalPlus(NumericalPlusNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitNumericalSubtraction(NumericalSubtractionNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitSignedRightShift(SignedRightShiftNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitStringConcatenate(StringConcatenateNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitUnsignedRightShift(UnsignedRightShiftNode n, TransferInput<CFValue,CFStore> p)

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

addInformationFromPreconditions, createTransferResult, finishValue, finishValue, getNarrowedValue, getValueFromFactory, getWidenedValue, initialStore, insertIntoStores, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processPostconditions, recreateTransferResult, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitArrayAccess, visitAssignment, visitCase, visitClassName, visitDeconstructorPattern, visitExpressionStatement, visitInstanceOf, visitLambdaResultExpression, visitLocalVariable, visitNarrowingConversion, visitNode, visitObjectCreation, visitReturn, visitStringConversion, visitSwitchExpressionNode, visitTernaryExpression, visitThis, visitVariableDeclaration, visitWideningConversion

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

visitArrayCreation, visitArrayType, visitAssertionError, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitDoubleLiteral, visitExplicitThis, visitFloatLiteral, visitImplicitThis, visitIntegerLiteral, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, 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, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitDoubleLiteral, visitExplicitThis, visitFloatLiteral, visitImplicitThis, visitIntegerLiteral, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast

Field Detail

atypeFactory

protected final ValueAnnotatedTypeFactory atypeFactory

The Value type factory.

qualHierarchy

protected final QualifierHierarchy qualHierarchy

The Value qualifier hierarchy.

Constructor Detail

ValueTransfer

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

Create a new ValueTransfer.

Parameters:

analysis - the corresponding analysis

Method Detail

visitFieldAccess

public TransferResult<CFValue,CFStore> visitFieldAccess(FieldAccessNode node,
                                                              TransferInput<CFValue,CFStore> in)

Specified by:

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

Overrides:

visitFieldAccess in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitMethodInvocation

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

Specified by:

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

Overrides:

visitMethodInvocation in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitStringConcatenate

public TransferResult<CFValue,CFStore> visitStringConcatenate(StringConcatenateNode n,
                                                                    TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitStringConcatenate in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

stringConcatenation

public TransferResult<CFValue,CFStore> stringConcatenation(Node leftOperand,
                                                                 Node rightOperand,
                                                                 TransferInput<CFValue,CFStore> p,
                                                                 TransferResult<CFValue,CFStore> result)

visitNumericalAddition

public TransferResult<CFValue,CFStore> visitNumericalAddition(NumericalAdditionNode n,
                                                                    TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitNumericalAddition in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitNumericalSubtraction

public TransferResult<CFValue,CFStore> visitNumericalSubtraction(NumericalSubtractionNode n,
                                                                       TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitNumericalSubtraction in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitNumericalMultiplication

public TransferResult<CFValue,CFStore> visitNumericalMultiplication(NumericalMultiplicationNode n,
                                                                          TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitNumericalMultiplication in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitIntegerDivision

public TransferResult<CFValue,CFStore> visitIntegerDivision(IntegerDivisionNode n,
                                                                  TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitIntegerDivision in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitFloatingDivision

public TransferResult<CFValue,CFStore> visitFloatingDivision(FloatingDivisionNode n,
                                                                   TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitFloatingDivision in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitIntegerRemainder

public TransferResult<CFValue,CFStore> visitIntegerRemainder(IntegerRemainderNode n,
                                                                   TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitIntegerRemainder in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitFloatingRemainder

public TransferResult<CFValue,CFStore> visitFloatingRemainder(FloatingRemainderNode n,
                                                                    TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitFloatingRemainder in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitLeftShift

public TransferResult<CFValue,CFStore> visitLeftShift(LeftShiftNode n,
                                                            TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitLeftShift in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitSignedRightShift

public TransferResult<CFValue,CFStore> visitSignedRightShift(SignedRightShiftNode n,
                                                                   TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitSignedRightShift in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitUnsignedRightShift

public TransferResult<CFValue,CFStore> visitUnsignedRightShift(UnsignedRightShiftNode n,
                                                                     TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitUnsignedRightShift in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitBitwiseAnd

public TransferResult<CFValue,CFStore> visitBitwiseAnd(BitwiseAndNode n,
                                                             TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitBitwiseAnd in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitBitwiseOr

public TransferResult<CFValue,CFStore> visitBitwiseOr(BitwiseOrNode n,
                                                            TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitBitwiseOr in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitBitwiseXor

public TransferResult<CFValue,CFStore> visitBitwiseXor(BitwiseXorNode n,
                                                             TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitBitwiseXor in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitNumericalMinus

public TransferResult<CFValue,CFStore> visitNumericalMinus(NumericalMinusNode n,
                                                                 TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitNumericalMinus in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitNumericalPlus

public TransferResult<CFValue,CFStore> visitNumericalPlus(NumericalPlusNode n,
                                                                TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitNumericalPlus in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitBitwiseComplement

public TransferResult<CFValue,CFStore> visitBitwiseComplement(BitwiseComplementNode n,
                                                                    TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitBitwiseComplement in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitLessThan

public TransferResult<CFValue,CFStore> visitLessThan(LessThanNode n,
                                                           TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitLessThan in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitLessThanOrEqual

public TransferResult<CFValue,CFStore> visitLessThanOrEqual(LessThanOrEqualNode n,
                                                                  TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitLessThanOrEqual in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitGreaterThan

public TransferResult<CFValue,CFStore> visitGreaterThan(GreaterThanNode n,
                                                              TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitGreaterThan in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitGreaterThanOrEqual

public TransferResult<CFValue,CFStore> visitGreaterThanOrEqual(GreaterThanOrEqualNode n,
                                                                     TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitGreaterThanOrEqual in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

strengthenAnnotationOfEqualTo

protected TransferResult<CFValue,CFStore> strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> transferResult,
                                                                              Node firstNode,
                                                                              Node secondNode,
                                                                              CFValue firstValue,
                                                                              CFValue secondValue,
                                                                              boolean notEqualTo)

Description copied from class: CFAbstractTransfer

Refine the annotation of secondNode if the annotation secondValue is less precise than firstValue. This is possible, if secondNode is an expression that is tracked by the store (e.g., a local variable or a field). Clients usually call this twice with firstNode and secondNode reversed, to refine each of them.

Note that when overriding this method, when a new type is inserted into the store, CFAbstractTransfer.splitAssignments(org.checkerframework.dataflow.cfg.node.Node) should be called, and the new type should be inserted into the store for each of the resulting nodes.

Overrides:

strengthenAnnotationOfEqualTo in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

Parameters:

transferResult - the previous result

firstNode - the node that might be more precise

secondNode - the node whose type to possibly refine

firstValue - the abstract value that might be more precise

secondValue - the abstract value that might be less precise

notEqualTo - if true, indicates that the logic is flipped (i.e., the information is added to the elseStore instead of the thenStore) for a not-equal comparison.

Returns:

the conditional transfer result (if information has been added), or res

processConditionalPostconditions

protected void processConditionalPostconditions(MethodInvocationNode n,
                                                javax.lang.model.element.ExecutableElement methodElement,
                                                com.sun.source.tree.ExpressionTree tree,
                                                CFStore thenStore,
                                                CFStore elseStore)

Description copied from class: CFAbstractTransfer

Add information from the conditional postconditions of a method to the stores after an invocation.

Overrides:

processConditionalPostconditions in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

Parameters:

n - a method call

methodElement - the method being called

tree - the tree for the method call

thenStore - the "then" store; is side-effected by this method

elseStore - the "else" store; is side-effected by this method

visitEqualTo

public TransferResult<CFValue,CFStore> visitEqualTo(EqualToNode n,
                                                          TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitEqualTo in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitNotEqual

public TransferResult<CFValue,CFStore> visitNotEqual(NotEqualNode n,
                                                           TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitNotEqual in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitConditionalNot

public TransferResult<CFValue,CFStore> visitConditionalNot(ConditionalNotNode n,
                                                                 TransferInput<CFValue,CFStore> p)

Description copied from class: CFAbstractTransfer

Reverse the role of the 'thenStore' and 'elseStore'.

Specified by:

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

Overrides:

visitConditionalNot in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitConditionalAnd

public TransferResult<CFValue,CFStore> visitConditionalAnd(ConditionalAndNode n,
                                                                 TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitConditionalAnd in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitConditionalOr

public TransferResult<CFValue,CFStore> visitConditionalOr(ConditionalOrNode n,
                                                                TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitConditionalOr in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>