Package org.checkerframework.common.accumulation

Class AccumulationTransfer

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.accumulation.AccumulationTransfer

All Implemented Interfaces:

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

Direct Known Subclasses:

CalledMethodsTransfer, InitializedFieldsTransfer

public class AccumulationTransfer
extends CFTransfer

The default transfer function for an accumulation checker.

Subclasses should call the accumulate(Node, TransferResult, String...) accumulate} method to add a string to the estimate at a particular program point.

Field Summary

Fields

Modifier and Type	Field	Description
protected final AccumulationAnnotatedTypeFactory	atypeFactory	The type factory.

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

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor	Description
AccumulationTransfer(CFAnalysis analysis)	Build a new AccumulationTransfer for the given analysis.

Method Summary

Modifier and Type	Method	Description
void	accumulate(Node node, TransferResult<CFValue,CFStore> result, String... values)	Updates the estimate of how many things node has accumulated.

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, visitAssignment, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitFieldAccess, visitInstanceOf, visitLambdaResultExpression, visitLocalVariable, visitMethodInvocation, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitReturn, visitStringConcatenateAssignment, visitStringConversion, visitSwitchExpressionNode, visitTernaryExpression, 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

Field Details

atypeFactory

protected final AccumulationAnnotatedTypeFactory atypeFactory

The type factory.

Constructor Details

AccumulationTransfer

public AccumulationTransfer(CFAnalysis analysis)

Build a new AccumulationTransfer for the given analysis.

Parameters:

analysis - the analysis

Method Details

accumulate

public void accumulate(Node node,
 TransferResult<CFValue,CFStore> result,
 String... values)

Updates the estimate of how many things node has accumulated.

If the node is an invocation of a method that returns its receiver, then its receiver's type will also be updated. In a chain of method calls, this process will continue backward as long as each receiver is itself a receiver-returning method invocation.

For example, suppose node is the expression a.b().c(), the new value (added by the accumulation analysis because of the .c() call) is "foo", and b and c return their receiver. This method will directly update the estimate of a.b().c() to include "foo". In addition, the estimates for the expressions a.b() and a would have their estimates updated to include "foo", because c and b (respectively) return their receivers. Note that due to what kind of values can be held in the store, this information is lost outside the method chain. That is, the returns-receiver propagated information is lost outside the expression in which the returns-receiver method invocations are nested.

As a concrete example, consider the Called Methods accumulation checker: if build requires a, b, and c to be called, then foo.a().b().c().build(); will typecheck (they are in one fluent method chain), but foo.a().b().c(); foo.build(); will not -- the store does not keep the information that a, b, and c have been called outside the chain. foo's type will be CalledMethods("a"), because only a() was called directly on foo. For such code to typecheck, the Called Methods accumulation checker uses an additional rule: the return type of a receiver-returning method rr() is CalledMethods("rr"). This rule is implemented directly in the TreeAnnotator subclass defined in the Called Methods type factory.

Parameters:

node - the node whose estimate should be expanded

result - the transfer result containing the store to be modified

values - the new accumulation values