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?
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, visitLessThanOrEqual
addInformationFromPreconditions, finishValue, finishValue, getTypeFactoryOfSubchecker, 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, visitWideningConversion
visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, 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, visitValueLiteral
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, 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
public 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 IndexAbstractTransfer
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 implements parts of cases 1, 2, 3, and 4 using the decomposition strategy described in this class's Javadoc.
refineGTE
in class IndexAbstractTransfer
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>>