Package org.checkerframework.checker.mustcall

Class MustCallTransfer

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.checker.mustcall.MustCallTransfer

All Implemented Interfaces:

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

public class MustCallTransfer
extends CFTransfer

Transfer function for the must-call type system. Its primary purposes are (1) to create temporary variables for expressions (which allow those expressions to have refined information in the store, which the consistency checker can use), and (2) to reset refined information when a method annotated with @CreatesMustCallFor is called.

Field Summary

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

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor	Description
MustCallTransfer(CFAnalysis analysis)	Create a MustCallTransfer.

Method Summary

Modifier and Type	Method	Description
protected @Nullable VariableTree	createTemporaryVar(Node node)	Creates a variable declaration for the given expression node, if possible.
protected boolean	isWpiEnabledForRLC()	Checks if WPI is enabled for the Resource Leak Checker inference.
protected boolean	shouldPerformWholeProgramInference(Tree tree)	See ResourceLeakChecker.ENABLE_WPI_FOR_RLC.
protected boolean	shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree)	See ResourceLeakChecker.ENABLE_WPI_FOR_RLC.
protected String	uniqueName(String prefix)	Creates a unique, arbitrary string that can be used as a name for a temporary variable, using the given prefix.
void	updateStoreWithTempVar(TransferResult<CFValue,CFStore> result, Node node)	This method either creates or looks up the temp var t for node, and then updates the store to give t the same type as node.
TransferResult<CFValue,CFStore>	visitAssignment(AssignmentNode n, TransferInput<CFValue,CFStore> in)
TransferResult<CFValue,CFStore>	visitMethodInvocation(MethodInvocationNode n, TransferInput<CFValue,CFStore> in)
TransferResult<CFValue,CFStore>	visitObjectCreation(ObjectCreationNode node, TransferInput<CFValue,CFStore> input)
TransferResult<CFValue,CFStore>	visitStringConversion(StringConversionNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitSwitchExpressionNode(SwitchExpressionNode node, TransferInput<CFValue,CFStore> input)
TransferResult<CFValue,CFStore>	visitTernaryExpression(TernaryExpressionNode node, TransferInput<CFValue,CFStore> input)

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

addInformationFromPreconditions, createTransferResult, finishValue, finishValue, getNarrowedValue, getValueFromFactory, getWidenedValue, initialStore, insertIntoStores, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, recreateTransferResult, setFixedInitialStore, splitAssignments, strengthenAnnotationOfEqualTo, usesSequentialSemantics, visitArrayAccess, visitCase, visitClassName, visitConditionalNot, visitDeconstructorPattern, visitEqualTo, visitExpressionStatement, visitFieldAccess, visitInstanceOf, visitLambdaResultExpression, visitLocalVariable, visitNarrowingConversion, visitNode, visitNotEqual, visitReturn, visitThis, visitVariableDeclaration, visitWideningConversion

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

visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThis, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThis, 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, visitClassDeclaration, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThis, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThis, 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 Details

MustCallTransfer

public MustCallTransfer(CFAnalysis analysis)

Create a MustCallTransfer.

Parameters:

analysis - the analysis

Method Details

visitStringConversion

public TransferResult<CFValue,CFStore> visitStringConversion(StringConversionNode n,
 TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitStringConversion in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitAssignment

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

Specified by:

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

Overrides:

visitAssignment in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitMethodInvocation

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

Specified by:

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

Overrides:

visitMethodInvocation in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

shouldPerformWholeProgramInference

protected boolean shouldPerformWholeProgramInference(Tree tree)

See ResourceLeakChecker.ENABLE_WPI_FOR_RLC.

Overrides:

shouldPerformWholeProgramInference in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

Parameters:

tree - a tree

Returns:

false if Resource Leak Checker is running as one of the upstream checkers and the -AenableWpiForRlc flag is not passed as a command line argument, otherwise returns the result of the super call

shouldPerformWholeProgramInference

protected boolean shouldPerformWholeProgramInference(Tree expressionTree,
 Tree lhsTree)

See ResourceLeakChecker.ENABLE_WPI_FOR_RLC.

Overrides:

shouldPerformWholeProgramInference in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

Parameters:

expressionTree - a tree

lhsTree - its element

Returns:

false if Resource Leak Checker is running as one of the upstream checkers and the -AenableWpiForRlc flag is not passed as a command line argument, otherwise returns the result of the super call

visitObjectCreation

public TransferResult<CFValue,CFStore> visitObjectCreation(ObjectCreationNode node,
 TransferInput<CFValue,CFStore> input)

Specified by:

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

Overrides:

visitObjectCreation in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitTernaryExpression

public TransferResult<CFValue,CFStore> visitTernaryExpression(TernaryExpressionNode node,
 TransferInput<CFValue,CFStore> input)

Specified by:

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

Overrides:

visitTernaryExpression in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitSwitchExpressionNode

public TransferResult<CFValue,CFStore> visitSwitchExpressionNode(SwitchExpressionNode node,
 TransferInput<CFValue,CFStore> input)

Specified by:

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

Overrides:

visitSwitchExpressionNode in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

updateStoreWithTempVar

public void updateStoreWithTempVar(TransferResult<CFValue,CFStore> result,
 Node node)

This method either creates or looks up the temp var t for node, and then updates the store to give t the same type as node.

Parameters:

node - the node to be assigned to a temporary variable

result - the transfer result containing the store to be modified

createTemporaryVar

protected @Nullable VariableTree createTemporaryVar(Node node)

Creates a variable declaration for the given expression node, if possible.

Note that error reporting code assumes that the names of temporary variables are not legal Java identifiers (see JLS 3.8). The temporary variable names generated here include an '-' character to make the names invalid.

Parameters:

node - an expression node

Returns:

a variable tree for the node, or null if an appropriate containing element cannot be located

uniqueName

protected String uniqueName(String prefix)

Creates a unique, arbitrary string that can be used as a name for a temporary variable, using the given prefix. Can be used up to Long.MAX_VALUE times.

Note that the correctness of the Resource Leak Checker depends on these names actually being unique, because LocalVariableNodes derived from them are used as keys in a map.

Parameters:

prefix - the prefix for the name

Returns:

a unique name that starts with the prefix

isWpiEnabledForRLC

protected boolean isWpiEnabledForRLC()

Checks if WPI is enabled for the Resource Leak Checker inference. See ResourceLeakChecker.ENABLE_WPI_FOR_RLC.

Returns:

returns true if WPI is enabled for the Resource Leak Checker