Package org.checkerframework.checker.index.lowerbound

Class 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:
ForwardTransferFunction<CFValue,CFStore>, 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)
Dividing these rules up by cases, this class implements:
  • 1. The rule described above for >
  • 2. The rule described above for ≥
  • 3. The rule described above for <
  • 4. The rule described above for ≤
  • 5. The rule described above for ==
  • 6. The rule described above for !=
  • 7. A special refinement for != when the value being compared to is a compile-time constant with a value exactly equal to -1 or 0 (i.e. x != -1 and x is GTEN1 implies x is non-negative). Maybe two rules?
  • 8. When a compile-time constant -2 is added to a positive, the result is GTEN1
  • 9. When a compile-time constant 2 is added to a GTEN1, the result is positive
  • 10. When a positive is added to a positive, the result is positive
  • 11. When a non-negative is added to any other type, the result is that other type
  • 12. When a GTEN1 is added to a positive, the result is non-negative
  • 13. When the left side of a subtraction expression is > the right side according to the LessThanChecker, the result of the subtraction expression is positive
  • 14. When the left side of a subtraction expression is ≥ the right side according to the LessThanChecker, the result of the subtraction expression is non-negative
  • 15. special handling for when the left side is the length of an array or String that's stored as a field, and the right side is a compile time constant. Do we need this?
  • 16. Multiplying any value by a compile time constant of 1 preserves its type
  • 17. Multiplying two positives produces a positive
  • 18. Multiplying a positive and a non-negative produces a non-negative
  • 19. Multiplying two non-negatives produces a non-negative
  • 20. When the result of Math.random is multiplied by an array length, the result is NonNegative.
  • 21. literal 0 divided by anything is non-negative
  • 22. anything divided by literal zero is bottom
  • 23. literal 1 divided by a positive or non-negative is non-negative
  • 24. literal 1 divided by anything else is GTEN1
  • 25. anything divided by literal 1 is itself
  • 26. a positive or non-negative divided by a positive or non-negative is non-negative
  • 27. anything modded by literal 1 or -1 is non-negative
  • 28. a positive or non-negative modded by anything is non-negative
  • 29. a GTEN1 modded by anything is GTEN1
  • 30. anything right-shifted by a non-negative is non-negative
  • 31. anything bitwise-anded by a non-negative is non-negative
  • 32. If a and b are non-negative and a <= b and a != b, then b is pos.
  • 33. A char is always non-negative