Package org.checkerframework.checker.index.lowerbound

Class 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