Package org.checkerframework.checker.index.upperbound

Class UpperBoundTransfer

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.upperbound.UpperBoundTransfer
All Implemented Interfaces:
ForwardTransferFunction<CFValue,CFStore>, TransferFunction<CFValue,CFStore>, NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>
public class UpperBoundTransfer extends IndexAbstractTransfer
Contains the transfer functions for the upper bound type system, a part of the Index Checker. This class implements the following refinement rules:
  • 1. Refine the type of expressions used as an array dimension to be less than length of the array to which the new array is assigned. For example, in int[] array = new int[expr];, the type of expr is @LTEqLength("array").
  • 2. If other * node has type typeOfMultiplication, then if other is positive, then node is typeOfMultiplication.
  • 3. If other * node has type typeOfMultiplication, if other is greater than 1, then node is typeOfMultiplication plus 1.
  • 4. Given a subtraction node, node, that is known to have type typeOfSubtraction. An offset can be applied to the left node (i.e. the left node has the same type, but with an offset based on the right node).
  • 5. In an addition expression, refine the two operands based on the type of the whole expression with appropriate offsets.
  • 6. If an addition expression has a type that is less than length of an array, and one of the operands is non-negative, then the other is less than or equal to the length of the array.
  • 7. If an addition expression has a type that is less than length of an array, and one of the operands is positive, then the other is also less than the length of the array.
  • 8. if x < y, and y has a type that is related to the length of an array, then x has the same type, with an offset that is one less.
  • 9. if x ≤ y, and y has a type that is related to the length of an array, then x has the same type.
  • 10. refine the subtrahend in a subtraction which is greater than or equal to a certain offset. The type of the subtrahend is refined to the type of the minuend with the offset added.
  • 11. if two variables are equal, they have the same type
  • 12. If one node in a != expression is an sequence length field or method access (optionally with a constant offset subtracted) and the other node is less than or equal to that sequence length (minus the offset), then refine the other node's type to less than the sequence length (minus the offset).
  • 13. If some Node a is known to be less than the length of some array, x, then, the type of a + b, is @LTLengthOf(value="x", offset="-b"). If b is known to be less than the length of some other array, y, then the type of a + b is @LTLengthOf(value={"x", "y"}, offset={"-b", "-a"}).
  • 14. If a is known to be less than the length of x when some offset, o, is added to a (the type of a is @LTLengthOf(value="x", offset="o")), then the type of a + b is @LTLengthOf(value="x",offset="o - b"). (Note, if "o - b" can be computed, then it is and the result is used in the annotation.)
  • 15. If expression i has type @LTLengthOf(value = "f2", offset = "f1.length") int and expression j is less than or equal to the length of f1, then the type of i + j is @LTLengthOf("f2").
  • 16. If some Node a is known to be less than the length of some sequence x, then the type of a - b is @LTLengthOf(value="x", offset="b").
  • 17. If some Node a is known to be less than the length of some sequence x, and if b is non-negative or positive, then a - b should keep the types of a.
  • 18. The type of a sequence length access (i.e. array.length) is @LTLength(value={"array"...}, offset="-1") where "array"... is the set of all sequences that are the same length (via the SameLen checker) as "array"
  • 19. If n is an array length field access, then the type of a.length is the glb of @LTEqLengthOf("a") and the value of a.length in the store.
  • 20. If n is a String.length() method invocation, then the type of s.length() is the glb of @LTEqLengthOf("s") and the value of s.length() in the store.