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,
TransferInput<CFValue,CFStore> in)
The implementation of the algorithm for refining a > test.
|
protected void |
refineGTE(Node left,
AnnotationMirror leftAnno,
Node right,
AnnotationMirror rightAnno,
CFStore store,
TransferInput<CFValue,CFStore> in)
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.
|
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, 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 IndexAbstractTransfer