org.checkerframework.checker.index.upperbound

Class UpperBoundTransfer

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.index.IndexAbstractTransfer

org.checkerframework.checker.index.upperbound.UpperBoundTransfer

All Implemented Interfaces:

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

public class UpperBoundTransfer
extends IndexAbstractTransfer

Field Summary

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

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor and Description
UpperBoundTransfer(CFAnalysis analysis)

Method Summary

Modifier and Type	Method and Description
protected void	refineGT(Node larger, javax.lang.model.element.AnnotationMirror largerAnno, Node smaller, javax.lang.model.element.AnnotationMirror smallerAnno, CFStore store, TransferInput<CFValue,CFStore> in)
protected void	refineGTE(Node left, javax.lang.model.element.AnnotationMirror leftAnno, Node right, javax.lang.model.element.AnnotationMirror rightAnno, CFStore store, TransferInput<CFValue,CFStore> in) This method refines the type of the right expression to the glb the previous type of right and the type of left.
protected TransferResult<CFValue,CFStore>	strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> res, 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>	visitAssignment(AssignmentNode node, TransferInput<CFValue,CFStore> in)
TransferResult<CFValue,CFStore>	visitFieldAccess(FieldAccessNode n, TransferInput<CFValue,CFStore> in) If n is an array length field access, then the type of a.length is the glb of @LTEqLengthOf("a") and the value of a.length in the store.
TransferResult<CFValue,CFStore>	visitMethodInvocation(MethodInvocationNode n, TransferInput<CFValue,CFStore> in) If n is an String.length() method invocation, then the type of s.length() is the glb of @LTEqLengthOf("s") and the value of s.length() in the store.
TransferResult<CFValue,CFStore>	visitNumericalAddition(NumericalAdditionNode n, TransferInput<CFValue,CFStore> in) If some Node a is known to be less than the length of some array, x, then, the type of a + b, is @LTLengthOf(value="x", offset="-b").
TransferResult<CFValue,CFStore>	visitNumericalSubtraction(NumericalSubtractionNode n, TransferInput<CFValue,CFStore> in) If some Node a is known to be less than the length of some sequence x, then the type of a - b is @LTLengthOf(value="x", offset="b").

Methods inherited from class org.checkerframework.checker.index.IndexAbstractTransfer

visitGreaterThan, visitGreaterThanOrEqual, visitLessThan, visitLessThanOrEqual

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

addInformationFromPreconditions, finishValue, finishValue, getTypeFactoryOfSubchecker, getValueFromFactory, getValueWithSameAnnotations, initialStore, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitArrayAccess, visitCase, visitClassName, visitConditionalNot, visitEqualTo, 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, visitImplicitThisLiteral, visitInstanceOf, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, 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, visitImplicitThisLiteral, visitInstanceOf, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitUnsignedRightShift

Constructor Detail

UpperBoundTransfer

public UpperBoundTransfer(CFAnalysis analysis)

Method Detail

visitAssignment

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

Specified by:

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

Overrides:

visitAssignment in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

refineGT

protected void refineGT(Node larger,
                        javax.lang.model.element.AnnotationMirror largerAnno,
                        Node smaller,
                        javax.lang.model.element.AnnotationMirror smallerAnno,
                        CFStore store,
                        TransferInput<CFValue,CFStore> in)

Specified by:

refineGT in class IndexAbstractTransfer

refineGTE

protected void refineGTE(Node left,
                         javax.lang.model.element.AnnotationMirror leftAnno,
                         Node right,
                         javax.lang.model.element.AnnotationMirror rightAnno,
                         CFStore store,
                         TransferInput<CFValue,CFStore> in)

This method refines the type of the right expression to the glb the previous type of right and the type of left.

Also, if the left expression is an array access, then the types of sub expressions of the right are refined.

Specified by:

refineGTE in class IndexAbstractTransfer

strengthenAnnotationOfEqualTo

protected TransferResult<CFValue,CFStore> strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> res,
                                                                        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).

Note that when overriding this method, when a new type is inserted into the store, splitAssignments 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:

res - the previous result

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 null.

visitNumericalAddition

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

If some Node a is known to be less than the length of some array, x, then, the type of a + b, is @LTLengthOf(value="x", offset="-b"). If b is known to be less than the length of some other array, y, then the type of a + b is @LTLengthOf(value={"x", "y"}, offset={"-b", "-a"}).

Alternatively, if a is known to be less than the length of x when some offset, o, is added to a (the type of a is @LTLengthOf(value="x", offset="o")), then the type of a + b is @LTLengthOf(value="x",offset="o - b"). (Note, if "o - b" can be computed, then it is and the result is used in the annotation.)

In addition, If expression i has type @LTLengthOf(value = "f2", offset = "f1.length") int and expression j is less than or equal to the length of f1, then the type of i + j is .@LTLengthOf("f2").

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> in)

If some Node a is known to be less than the length of some sequence x, then the type of a - b is @LTLengthOf(value="x", offset="b"). If b is known to be less than the length of some other sequence, this doesn't add any information about the type of a - b. But, if b is non-negative or positive, then a - b should keep the types of a.

Specified by:

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

Overrides:

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

visitFieldAccess

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

If n is an array length field access, then the type of a.length is the glb of @LTEqLengthOf("a") and the value of a.length in the store.

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> in)

If n is an String.length() method invocation, then the type of s.length() is the glb of @LTEqLengthOf("s") and the value of s.length() in the store.

Specified by:

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

Overrides:

visitMethodInvocation in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>