public class LowerBoundTransfer extends IndexAbstractTransfer
Also implements the logic for binary operations: +, -, *, /, and %.
>, <, ≥, ≤, ==, 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)
Dividing these rules up by cases, this class implements:
x != -1 and x is GTEN1 implies x is
non-negative). Maybe two rules?
a <= b and a != b, then b is pos.
| Modifier and Type | Field and Description |
|---|---|
javax.lang.model.element.AnnotationMirror |
GTEN1
The canonical
GTENegativeOne annotation. |
javax.lang.model.element.AnnotationMirror |
NN
The canonical
NonNegative annotation. |
javax.lang.model.element.AnnotationMirror |
POS
The canonical
Positive annotation. |
javax.lang.model.element.AnnotationMirror |
UNKNOWN
The canonical
LowerBoundUnknown annotation. |
analysis, sequentialSemantics| Constructor and Description |
|---|
LowerBoundTransfer(CFAnalysis analysis) |
visitGreaterThan, visitGreaterThanOrEqual, visitLessThan, visitLessThanOrEqualfinishValue, finishValue, getValueFromFactory, getValueWithSameAnnotations, initialStore, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitArrayAccess, visitAssignment, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitFieldAccess, visitLambdaResultExpression, visitLocalVariable, visitMethodInvocation, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitReturn, visitStringConcatenateAssignment, visitStringConversion, visitTernaryExpression, visitThisLiteral, visitVariableDeclaration, visitWideningConversionvisitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThisLiteral, visitInstanceOf, visitIntegerLiteral, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalMinus, visitNumericalPlus, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitValueLiteralclone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, waitvisitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThisLiteral, visitInstanceOf, visitIntegerLiteral, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalMinus, visitNumericalPlus, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCastpublic final javax.lang.model.element.AnnotationMirror GTEN1
GTENegativeOne annotation.public final javax.lang.model.element.AnnotationMirror NN
NonNegative annotation.public final javax.lang.model.element.AnnotationMirror POS
Positive annotation.public final javax.lang.model.element.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, javax.lang.model.element.AnnotationMirror leftAnno, Node right, javax.lang.model.element.AnnotationMirror rightAnno, CFStore store, TransferInput<CFValue,CFStore> in)
This implements parts of cases 1, 2, 3, and 4 using the decomposition strategy described in the Javadoc of this class.
refineGT in class IndexAbstractTransferprotected 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 implements parts of cases 1, 2, 3, and 4 using the decomposition strategy described in this class's Javadoc.
refineGTE in class IndexAbstractTransferprotected void addInformationFromPreconditions(CFStore info, AnnotatedTypeFactory factory, UnderlyingAST.CFGMethod method, com.sun.source.tree.MethodTree methodTree, javax.lang.model.element.ExecutableElement methodElement)
addInformationFromPreconditions in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>public javax.lang.model.element.AnnotationMirror getAnnotationForRemainder(IntegerRemainderNode node, TransferInput<CFValue,CFStore> p)
27. * % 1/-1 → nn
28. pos/nn % * → nn
29. gten1 % * → gten1
* % * → lbu
public TransferResult<CFValue,CFStore> visitNumericalAddition(NumericalAdditionNode n, TransferInput<CFValue,CFStore> p)
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> p)
visitNumericalSubtraction in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitNumericalSubtraction in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>public TransferResult<CFValue,CFStore> visitNumericalMultiplication(NumericalMultiplicationNode n, TransferInput<CFValue,CFStore> p)
visitNumericalMultiplication in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitNumericalMultiplication in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>public TransferResult<CFValue,CFStore> visitIntegerDivision(IntegerDivisionNode n, TransferInput<CFValue,CFStore> p)
visitIntegerDivision in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitIntegerDivision in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>public TransferResult<CFValue,CFStore> visitIntegerRemainder(IntegerRemainderNode n, TransferInput<CFValue,CFStore> p)
visitIntegerRemainder in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitIntegerRemainder in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>public TransferResult<CFValue,CFStore> visitSignedRightShift(SignedRightShiftNode n, TransferInput<CFValue,CFStore> p)
visitSignedRightShift in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitSignedRightShift in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>public TransferResult<CFValue,CFStore> visitUnsignedRightShift(UnsignedRightShiftNode n, TransferInput<CFValue,CFStore> p)
visitUnsignedRightShift in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitUnsignedRightShift in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>public TransferResult<CFValue,CFStore> visitBitwiseAnd(BitwiseAndNode n, TransferInput<CFValue,CFStore> p)
visitBitwiseAnd in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitBitwiseAnd in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>