public class LowerBoundTransfer extends IndexAbstractTransfer
>, <, ≥, ≤, ==, and != nodes are represented as combinations of > and ≥ (e.g. == is ≥ in both directions in the then branch), and implement refinements based on these decompositions.
Refinement/transfer rules for conditionals:
There are two "primitives":
x > y, which implies things about x based on y's type:
y has type: implies x has type:
gte-1 nn
nn pos
pos pos
and x ≥ y:
y has type: implies x has type:
gte-1 gte-1
nn nn
pos pos
These two "building blocks" can be combined to make all
other conditional expressions:
EXPR THEN ELSE
x > y x > y y ≥ x
x ≥ y x ≥ y y > x
x < y y > x x ≥ y
x ≤ y y ≥ x x > y
Or, more formally:
EXPR THEN ELSE
x > y x_refined = GLB(x_orig, promote(y)) y_refined = GLB(y_orig, x)
x ≥ y x_refined = GLB(x_orig, y) y_refined = GLB(y_orig, promote(x))
x < y y_refined = GLB(y_orig, promote(x)) x_refined = GLB(x_orig, y)
x ≤ y y_refined = GLB(y_orig, x) x_refined = GLB(x_orig, promote(y))
where GLB is the greatest lower bound and promote is the increment
function on types (or, equivalently, the function specified by the "x
> y" information above).
There's also ==, which is a special case. Only the THEN
branch is refined:
EXPR THEN ELSE
x == y x ≥ y && y ≥ x nothing known
or, more formally:
EXPR THEN ELSE
x == y x_refined = GLB(x_orig, y_orig) nothing known
y_refined = GLB(x_orig, y_orig)
finally, not equal:
EXPR THEN ELSE
x != y nothing known x ≥ y && y ≥ x
more formally:
EXPR THEN ELSE
x != y nothing known x_refined = GLB(x_orig, y_orig)
y_refined = GLB(x_orig, y_orig)
| Modifier and Type | Field and Description |
|---|---|
AnnotationMirror |
GTEN1
The canonical
GTENegativeOne annotation. |
AnnotationMirror |
NN
The canonical
NonNegative annotation. |
AnnotationMirror |
POS
The canonical
Positive annotation. |
AnnotationMirror |
UNKNOWN
The canonical
LowerBoundUnknown annotation. |
analysissequentialSemantics| Constructor and Description |
|---|
LowerBoundTransfer(CFAnalysis analysis) |
| Modifier and Type | Method and Description |
|---|---|
protected void |
refineGT(Node left,
AnnotationMirror leftAnno,
Node right,
AnnotationMirror rightAnno,
CFStore store)
The implementation of the algorithm for refining a > test.
|
protected void |
refineGTE(Node left,
AnnotationMirror leftAnno,
Node right,
AnnotationMirror rightAnno,
CFStore store)
Refines left to exactly the level of right, since in the worst case they're equal.
|
protected TransferResult<CFValue,CFStore> |
strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> result,
Node firstNode,
Node secondNode,
CFValue firstValue,
CFValue secondValue,
boolean notEqualTo)
Implements the transfer rules for both equal nodes and not-equals nodes.
|
isArrayLengthFieldAccess, visitGreaterThan, visitGreaterThanOrEqual, visitLessThan, visitLessThanOrEqualaddInformationFromPreconditions, finishValue, finishValue, getTypeFactoryOfSubchecker, getValueFromFactory, getValueWithSameAnnotations, initialStore, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitArrayAccess, visitAssignment, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitFieldAccess, visitLocalVariable, visitMethodInvocation, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitReturn, visitStringConcatenateAssignment, visitStringConversion, visitTernaryExpression, visitThisLiteral, visitVariableDeclaration, visitWideningConversionvisitArrayCreation, 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, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, 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, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThisLiteral, visitInstanceOf, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitUnsignedRightShiftpublic final AnnotationMirror GTEN1
GTENegativeOne annotation.public final AnnotationMirror NN
NonNegative annotation.public final AnnotationMirror POS
Positive annotation.public final AnnotationMirror UNKNOWN
LowerBoundUnknown annotation.public LowerBoundTransfer(CFAnalysis analysis)
protected TransferResult<CFValue,CFStore> strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> result, Node firstNode, Node secondNode, CFValue firstValue, CFValue secondValue, boolean notEqualTo)
strengthenAnnotationOfEqualTo in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>result - the previous resultnotEqualTo - 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.null.protected void refineGT(Node left, AnnotationMirror leftAnno, Node right, AnnotationMirror rightAnno, CFStore store)
refineGT in class IndexAbstractTransferprotected void refineGTE(Node left, AnnotationMirror leftAnno, Node right, AnnotationMirror rightAnno, CFStore store)
refineGTE in class IndexAbstractTransfer