LowerBoundTransfer

java.lang.Object
- org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<TransferResult<V,S>,TransferInput<V,S>>
- - org.checkerframework.framework.flow.CFAbstractTransfer<CFValue,CFStore,CFTransfer>
  - - org.checkerframework.framework.flow.CFTransfer
    - - org.checkerframework.checker.index.IndexAbstractTransfer
      - org.checkerframework.checker.index.lowerbound.LowerBoundTransfer

All Implemented Interfaces:: TransferFunction<CFValue,CFStore>, NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

public class LowerBoundTransfer
extends IndexAbstractTransfer

Implements dataflow refinement rules based on tests: <, >, ==, and their derivatives.

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)

Field Summary

Fields
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.

Fields inherited from class org.checkerframework.framework.flow.CFAbstractTransfer
analysis, sequentialSemantics

Constructor Summary

Constructors
Constructor and Description

LowerBoundTransfer(CFAnalysis analysis)

Constructors
Constructor and Description
`LowerBoundTransfer(CFAnalysis analysis)`

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`AnnotationMirror`	`getAnnotationForRemainder(IntegerRemainderNode node, TransferInput<CFValue,CFStore> p)` getAnnotationForRemainder handles these cases: * % 1/-1 → nn pos/nn % * → nn gten1 % * → gten1 * % * → lbu
`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.
`TransferResult<CFValue,CFStore>`	`visitBitwiseAnd(BitwiseAndNode n, TransferInput<CFValue,CFStore> p)`
`TransferResult<CFValue,CFStore>`	`visitIntegerDivision(IntegerDivisionNode n, TransferInput<CFValue,CFStore> p)`
`TransferResult<CFValue,CFStore>`	`visitIntegerRemainder(IntegerRemainderNode n, TransferInput<CFValue,CFStore> p)`
`TransferResult<CFValue,CFStore>`	`visitNumericalAddition(NumericalAdditionNode n, TransferInput<CFValue,CFStore> p)`
`TransferResult<CFValue,CFStore>`	`visitNumericalMultiplication(NumericalMultiplicationNode n, TransferInput<CFValue,CFStore> p)`
`TransferResult<CFValue,CFStore>`	`visitNumericalSubtraction(NumericalSubtractionNode n, TransferInput<CFValue,CFStore> p)`
`TransferResult<CFValue,CFStore>`	`visitSignedRightShift(SignedRightShiftNode n, TransferInput<CFValue,CFStore> p)`
`TransferResult<CFValue,CFStore>`	`visitUnsignedRightShift(UnsignedRightShiftNode n, TransferInput<CFValue,CFStore> p)`

Methods inherited from class org.checkerframework.checker.index.IndexAbstractTransfer
visitGreaterThan, visitGreaterThanOrEqual, visitLessThan, visitLessThanOrEqual

Methods inherited from class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor
visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThisLiteral, visitInstanceOf, visitIntegerLiteral, visitLambdaResultExpression, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalMinus, visitNumericalPlus, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitValueLiteral

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail
- GTEN1
```
public final AnnotationMirror GTEN1
```
  The canonical GTENegativeOne annotation.
- NN
```
public final AnnotationMirror NN
```
  The canonical NonNegative annotation.
- POS
```
public final AnnotationMirror POS
```
  The canonical Positive annotation.
- UNKNOWN
```
public final AnnotationMirror UNKNOWN
```
  The canonical LowerBoundUnknown annotation.

Constructor Detail

LowerBoundTransfer

public LowerBoundTransfer(CFAnalysis analysis)

Method Detail

strengthenAnnotationOfEqualTo

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.

Overrides:: strengthenAnnotationOfEqualTo in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>
Parameters:: result - the previous result; notEqualTo - 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.
Returns:: the conditional transfer result (if information has been added), or null.

refineGT

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. Changes the type of left (the greater one) to one closer to bottom than the type of right. Can't call the promote function from the ATF directly because a new expression isn't introduced here - the modifications have to be made to an existing one.

Specified by:: refineGT in class IndexAbstractTransfer

refineGTE

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. Modifies an existing type in the store, but has to be careful not to overwrite a more precise existing type.

Specified by:: refineGTE in class IndexAbstractTransfer

getAnnotationForRemainder

public AnnotationMirror getAnnotationForRemainder(IntegerRemainderNode node,
                                                  TransferInput<CFValue,CFStore> p)

getAnnotationForRemainder handles these cases: * % 1/-1 → nn pos/nn % * → nn gten1 % * → gten1 * % * → lbu