public class UpperBoundTransfer extends IndexAbstractTransfer
int[] array = new
int[expr];, the type of expr is @LTEqLength("array").
other * node has type typeOfMultiplication, then if other is
positive, then node is typeOfMultiplication.
other * node has type typeOfMultiplication, if other is
greater than 1, then node is typeOfMultiplication plus 1.
node, that is known to have type typeOfSubtraction. An offset can be applied to the left node (i.e. the left node has the
same type, but with an offset based on the right node).
@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"}).
@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.)
@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").
@LTLengthOf(value="x", offset="b").
@LTLength(value={"array"...}, offset="-1") where "array"... is the set of all
sequences that are the same length (via the SameLen checker) as "array"
@LTEqLengthOf("a") and the value of a.length in the store.
@LTEqLengthOf("s") and the value of s.length() in the store.
analysis, sequentialSemantics| Constructor and Description |
|---|
UpperBoundTransfer(CFAnalysis analysis) |
| Modifier and Type | Method and Description |
|---|---|
protected void |
refineGT(Node larger,
AnnotationMirror largerAnno,
Node smaller,
AnnotationMirror smallerAnno,
CFStore store,
TransferInput<CFValue,CFStore> in)
Case 8: if x < y, and y has a type that is related to the length of an array, then x has
the same type, with an offset that is one less.
|
protected void |
refineGTE(Node left,
AnnotationMirror leftAnno,
Node right,
AnnotationMirror rightAnno,
CFStore store,
TransferInput<CFValue,CFStore> in)
Case 9: if x ≤ y, and y has a type that is related to the length of an array, then x has
the same type.
|
protected TransferResult<CFValue,CFStore> |
strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> res,
Node firstNode,
Node secondNode,
CFValue firstValue,
CFValue secondValue,
boolean notEqualTo)
Implements case 11.
|
TransferResult<CFValue,CFStore> |
visitAssignment(AssignmentNode node,
TransferInput<CFValue,CFStore> in)
Case 1: Refine the type of expressions used as an array dimension to be less than length of
the array to which the new array is assigned.
|
TransferResult<CFValue,CFStore> |
visitCase(CaseNode n,
TransferInput<CFValue,CFStore> in)
A case produces no value, but it may imply some facts about the argument to the switch
statement.
|
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 a 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").
|
visitGreaterThan, visitGreaterThanOrEqual, visitLessThan, visitLessThanOrEqualaddInformationFromPreconditions, createTransferResult, finishValue, finishValue, getNarrowedValue, getValueFromFactory, getValueWithSameAnnotations, getWidenedValue, initialStore, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, recreateTransferResult, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitArrayAccess, visitClassName, visitConditionalNot, visitEqualTo, visitInstanceOf, visitLambdaResultExpression, visitLocalVariable, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitReturn, visitStringConcatenateAssignment, visitStringConversion, visitTernaryExpression, visitThis, visitVariableDeclaration, visitWideningConversionvisitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThis, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThis, 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, visitValueLiteralclone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, waitvisitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThis, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThis, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitUnsignedRightShiftpublic UpperBoundTransfer(CFAnalysis analysis)
public TransferResult<CFValue,CFStore> visitAssignment(AssignmentNode node, TransferInput<CFValue,CFStore> in)
visitAssignment in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitAssignment in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>protected void refineGT(Node larger, AnnotationMirror largerAnno, Node smaller, AnnotationMirror smallerAnno, CFStore store, TransferInput<CFValue,CFStore> in)
refineGT in class IndexAbstractTransferprotected void refineGTE(Node left, AnnotationMirror leftAnno, Node right, AnnotationMirror rightAnno, CFStore store, TransferInput<CFValue,CFStore> in)
refineGTE in class IndexAbstractTransferprotected TransferResult<CFValue,CFStore> strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> res, Node firstNode, Node secondNode, CFValue firstValue, CFValue secondValue, boolean notEqualTo)
strengthenAnnotationOfEqualTo in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>res - the previous resultfirstNode - the node that might be more precisesecondNode - the node whose type to possibly refinefirstValue - the abstract value that might be more precisesecondValue - the abstract value that might be less precisenotEqualTo - 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.nullpublic TransferResult<CFValue,CFStore> visitNumericalAddition(NumericalAdditionNode n, TransferInput<CFValue,CFStore> in)
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").
These three cases correspond to cases 13-15.
visitNumericalAddition in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitNumericalAddition in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>public TransferResult<CFValue,CFStore> visitNumericalSubtraction(NumericalSubtractionNode n, TransferInput<CFValue,CFStore> in)
visitNumericalSubtraction in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitNumericalSubtraction in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>public TransferResult<CFValue,CFStore> visitFieldAccess(FieldAccessNode n, TransferInput<CFValue,CFStore> in)
visitFieldAccess in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitFieldAccess in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>public TransferResult<CFValue,CFStore> visitMethodInvocation(MethodInvocationNode n, TransferInput<CFValue,CFStore> in)
visitMethodInvocation in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitMethodInvocation in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>public TransferResult<CFValue,CFStore> visitCase(CaseNode n, TransferInput<CFValue,CFStore> in)
CFAbstractTransfervisitCase in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitCase in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>