| package org.checkerframework.checker.index.upperbound; |
| |
| import com.sun.source.tree.Tree; |
| import com.sun.source.util.TreePath; |
| import java.util.ArrayList; |
| import java.util.Collections; |
| import java.util.List; |
| import java.util.Set; |
| import javax.lang.model.element.AnnotationMirror; |
| import javax.lang.model.type.TypeKind; |
| import javax.lang.model.type.TypeMirror; |
| import org.checkerframework.checker.index.IndexAbstractTransfer; |
| import org.checkerframework.checker.index.IndexRefinementInfo; |
| import org.checkerframework.checker.index.Subsequence; |
| import org.checkerframework.checker.index.inequality.LessThanAnnotatedTypeFactory; |
| import org.checkerframework.checker.index.qual.LessThan; |
| import org.checkerframework.checker.index.qual.NonNegative; |
| import org.checkerframework.checker.index.qual.Positive; |
| import org.checkerframework.checker.index.qual.SubstringIndexFor; |
| import org.checkerframework.checker.index.upperbound.UBQualifier.LessThanLengthOf; |
| import org.checkerframework.checker.index.upperbound.UBQualifier.UpperBoundUnknownQualifier; |
| import org.checkerframework.common.value.ValueCheckerUtils; |
| import org.checkerframework.dataflow.analysis.RegularTransferResult; |
| import org.checkerframework.dataflow.analysis.TransferInput; |
| import org.checkerframework.dataflow.analysis.TransferResult; |
| import org.checkerframework.dataflow.cfg.node.ArrayCreationNode; |
| import org.checkerframework.dataflow.cfg.node.AssignmentNode; |
| import org.checkerframework.dataflow.cfg.node.CaseNode; |
| import org.checkerframework.dataflow.cfg.node.FieldAccessNode; |
| import org.checkerframework.dataflow.cfg.node.IntegerLiteralNode; |
| import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; |
| import org.checkerframework.dataflow.cfg.node.Node; |
| import org.checkerframework.dataflow.cfg.node.NumericalAdditionNode; |
| import org.checkerframework.dataflow.cfg.node.NumericalMultiplicationNode; |
| import org.checkerframework.dataflow.cfg.node.NumericalSubtractionNode; |
| import org.checkerframework.dataflow.cfg.node.TypeCastNode; |
| import org.checkerframework.dataflow.expression.FieldAccess; |
| import org.checkerframework.dataflow.expression.JavaExpression; |
| import org.checkerframework.dataflow.expression.MethodCall; |
| import org.checkerframework.dataflow.util.NodeUtils; |
| import org.checkerframework.framework.flow.CFAbstractStore; |
| import org.checkerframework.framework.flow.CFAnalysis; |
| import org.checkerframework.framework.flow.CFStore; |
| import org.checkerframework.framework.flow.CFValue; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror; |
| import org.checkerframework.framework.type.QualifierHierarchy; |
| import org.checkerframework.javacutil.AnnotationUtils; |
| |
| /** |
| * Contains the transfer functions for the upper bound type system, a part of the Index Checker. |
| * This class implements the following refinement rules: |
| * |
| * <ul> |
| * <li>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 {@code int[] array = new |
| * int[expr];}, the type of expr is {@code @LTEqLength("array")}. |
| * <li>2. If {@code other * node} has type {@code typeOfMultiplication}, then if {@code other} is |
| * positive, then {@code node} is {@code typeOfMultiplication}. |
| * <li>3. If {@code other * node} has type {@code typeOfMultiplication}, if {@code other} is |
| * greater than 1, then {@code node} is {@code typeOfMultiplication} plus 1. |
| * <li>4. Given a subtraction node, {@code node}, that is known to have type {@code |
| * 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). |
| * <li>5. In an addition expression, refine the two operands based on the type of the whole |
| * expression with appropriate offsets. |
| * <li>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. |
| * <li>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. |
| * <li>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. |
| * <li>9. if x ≤ y, and y has a type that is related to the length of an array, then x has the |
| * same type. |
| * <li>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. |
| * <li>11. if two variables are equal, they have the same type |
| * <li>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). |
| * <li>13. If some Node a is known to be less than the length of some array, x, then, the type of |
| * a + b, is {@code @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 {@code @LTLengthOf(value={"x", |
| * "y"}, offset={"-b", "-a"})}. |
| * <li>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 {@code @LTLengthOf(value="x", offset="o"))}, then the type of a + b is |
| * {@code @LTLengthOf(value="x",offset="o - b")}. (Note, if "o - b" can be computed, then it |
| * is and the result is used in the annotation.) |
| * <li>15. If expression i has type {@code @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 |
| * {@code @LTLengthOf("f2")}. |
| * <li>16. If some Node a is known to be less than the length of some sequence x, then the type of |
| * a - b is {@code @LTLengthOf(value="x", offset="b")}. |
| * <li>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. |
| * <li>18. The type of a sequence length access (i.e. array.length) is |
| * {@code @LTLength(value={"array"...}, offset="-1")} where "array"... is the set of all |
| * sequences that are the same length (via the SameLen checker) as "array" |
| * <li>19. If n is an array length field access, then the type of a.length is the glb of |
| * {@code @LTEqLengthOf("a")} and the value of a.length in the store. |
| * <li>20. If n is a String.length() method invocation, then the type of s.length() is the glb of |
| * {@code @LTEqLengthOf("s")} and the value of s.length() in the store. |
| * </ul> |
| */ |
| public class UpperBoundTransfer extends IndexAbstractTransfer { |
| |
| /** The type factory associated with this transfer function. */ |
| private UpperBoundAnnotatedTypeFactory atypeFactory; |
| |
| /** The int TypeMirror. */ |
| TypeMirror intTM; |
| |
| /** |
| * Creates a new UpperBoundTransfer. |
| * |
| * @param analysis the analysis for this transfer function |
| */ |
| public UpperBoundTransfer(CFAnalysis analysis) { |
| super(analysis); |
| atypeFactory = (UpperBoundAnnotatedTypeFactory) analysis.getTypeFactory(); |
| intTM = atypeFactory.types.getPrimitiveType(TypeKind.INT); |
| } |
| |
| /** |
| * Case 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"). |
| */ |
| @Override |
| public TransferResult<CFValue, CFStore> visitAssignment( |
| AssignmentNode node, TransferInput<CFValue, CFStore> in) { |
| TransferResult<CFValue, CFStore> result = super.visitAssignment(node, in); |
| |
| Node expNode = node.getExpression(); |
| |
| // strip off typecast if any |
| Node expNodeSansCast = |
| (expNode instanceof TypeCastNode) ? ((TypeCastNode) expNode).getOperand() : expNode; |
| // null if right-hand-side is not an array creation expression |
| ArrayCreationNode acNode = |
| (expNodeSansCast instanceof ArrayCreationNode) |
| ? acNode = (ArrayCreationNode) expNodeSansCast |
| : null; |
| |
| if (acNode != null) { |
| // Right-hand side of assignment is an array creation expression |
| List<Node> nodeList = acNode.getDimensions(); |
| if (nodeList.size() < 1) { |
| return result; |
| } |
| Node dim = acNode.getDimension(0); |
| |
| UBQualifier previousQualifier = getUBQualifier(dim, in); |
| JavaExpression arrayExpr = JavaExpression.fromNode(node.getTarget()); |
| String arrayString = arrayExpr.toString(); |
| LessThanLengthOf newInfo = |
| (LessThanLengthOf) UBQualifier.createUBQualifier(arrayString, "-1"); |
| UBQualifier combined = previousQualifier.glb(newInfo); |
| AnnotationMirror newAnno = atypeFactory.convertUBQualifierToAnnotation(combined); |
| |
| JavaExpression dimExpr = JavaExpression.fromNode(dim); |
| result.getRegularStore().insertValue(dimExpr, newAnno); |
| propagateToOperands(newInfo, dim, in, result.getRegularStore()); |
| } |
| return result; |
| } |
| |
| /** |
| * {@code node} is known to be {@code typeOfNode}. If the node is a plus or a minus then the types |
| * of the left and right operands can be refined to include offsets. If the node is a |
| * multiplication, its operands can also be refined. See {@link |
| * #propagateToAdditionOperand(LessThanLengthOf, Node, Node, TransferInput, CFStore)}, {@link |
| * #propagateToSubtractionOperands(LessThanLengthOf, NumericalSubtractionNode, TransferInput, |
| * CFStore)}, and {@link #propagateToMultiplicationOperand(LessThanLengthOf, Node, Node, |
| * TransferInput, CFStore)} for details. |
| */ |
| private void propagateToOperands( |
| LessThanLengthOf typeOfNode, Node node, TransferInput<CFValue, CFStore> in, CFStore store) { |
| if (node instanceof NumericalAdditionNode) { |
| Node right = ((NumericalAdditionNode) node).getRightOperand(); |
| Node left = ((NumericalAdditionNode) node).getLeftOperand(); |
| propagateToAdditionOperand(typeOfNode, left, right, in, store); |
| propagateToAdditionOperand(typeOfNode, right, left, in, store); |
| } else if (node instanceof NumericalSubtractionNode) { |
| propagateToSubtractionOperands(typeOfNode, (NumericalSubtractionNode) node, in, store); |
| } else if (node instanceof NumericalMultiplicationNode) { |
| if (atypeFactory.hasLowerBoundTypeByClass(node, Positive.class)) { |
| Node right = ((NumericalMultiplicationNode) node).getRightOperand(); |
| Node left = ((NumericalMultiplicationNode) node).getLeftOperand(); |
| propagateToMultiplicationOperand(typeOfNode, left, right, in, store); |
| propagateToMultiplicationOperand(typeOfNode, right, left, in, store); |
| } |
| } |
| } |
| |
| /** |
| * {@code other} times {@code node} is known to be {@code typeOfMultiplication}. |
| * |
| * <p>This implies that if {@code other} is positive, then {@code node} is {@code |
| * typeOfMultiplication}. If {@code other} is greater than 1, then {@code node} is {@code |
| * typeOfMultiplication} plus 1. These are cases 2 and 3, respectively. |
| */ |
| private void propagateToMultiplicationOperand( |
| LessThanLengthOf typeOfMultiplication, |
| Node node, |
| Node other, |
| TransferInput<CFValue, CFStore> in, |
| CFStore store) { |
| if (atypeFactory.hasLowerBoundTypeByClass(other, Positive.class)) { |
| Long minValue = |
| ValueCheckerUtils.getMinValue( |
| other.getTree(), atypeFactory.getValueAnnotatedTypeFactory()); |
| if (minValue != null && minValue > 1) { |
| typeOfMultiplication = (LessThanLengthOf) typeOfMultiplication.plusOffset(1); |
| } |
| UBQualifier qual = getUBQualifier(node, in); |
| UBQualifier newQual = qual.glb(typeOfMultiplication); |
| JavaExpression je = JavaExpression.fromNode(node); |
| store.insertValue(je, atypeFactory.convertUBQualifierToAnnotation(newQual)); |
| } |
| } |
| |
| /** |
| * The subtraction node, {@code node}, is known to be {@code typeOfSubtraction}. |
| * |
| * <p>This means that the left node is less than or equal to the length of the array when the |
| * right node is subtracted from the left node. Note that unlike {@link |
| * #propagateToAdditionOperand(LessThanLengthOf, Node, Node, TransferInput, CFStore)} and {@link |
| * #propagateToMultiplicationOperand(LessThanLengthOf, Node, Node, TransferInput, CFStore)}, this |
| * method takes the NumericalSubtractionNode instead of the two operand nodes. This implements |
| * case 4. |
| * |
| * @param typeOfSubtraction type of node |
| * @param node subtraction node that has typeOfSubtraction |
| * @param in a TransferInput |
| * @param store location to store the refined type |
| */ |
| private void propagateToSubtractionOperands( |
| LessThanLengthOf typeOfSubtraction, |
| NumericalSubtractionNode node, |
| TransferInput<CFValue, CFStore> in, |
| CFStore store) { |
| UBQualifier left = getUBQualifier(node.getLeftOperand(), in); |
| UBQualifier newInfo = typeOfSubtraction.minusOffset(node.getRightOperand(), atypeFactory); |
| |
| UBQualifier newLeft = left.glb(newInfo); |
| JavaExpression leftJe = JavaExpression.fromNode(node.getLeftOperand()); |
| store.insertValue(leftJe, atypeFactory.convertUBQualifierToAnnotation(newLeft)); |
| } |
| |
| /** |
| * Refines the type of {@code operand} to {@code typeOfAddition} plus {@code other}. If {@code |
| * other} is non-negative, then {@code operand} also less than the length of the arrays in {@code |
| * typeOfAddition}. If {@code other} is positive, then {@code operand} also less than the length |
| * of the arrays in {@code typeOfAddition} plus 1. These are cases 5, 6, and 7. |
| * |
| * @param typeOfAddition type of {@code operand + other} |
| * @param operand the Node to refine |
| * @param other the Node added to {@code operand} |
| * @param in a TransferInput |
| * @param store location to store the refined types |
| */ |
| private void propagateToAdditionOperand( |
| LessThanLengthOf typeOfAddition, |
| Node operand, |
| Node other, |
| TransferInput<CFValue, CFStore> in, |
| CFStore store) { |
| UBQualifier operandQual = getUBQualifier(operand, in); |
| UBQualifier newQual = operandQual.glb(typeOfAddition.plusOffset(other, atypeFactory)); |
| |
| // If the node is NonNegative, add an LTEL to the qual. If Positive, add an LTL. |
| if (atypeFactory.hasLowerBoundTypeByClass(other, Positive.class)) { |
| newQual = newQual.glb(typeOfAddition.plusOffset(1)); |
| } else if (atypeFactory.hasLowerBoundTypeByClass(other, NonNegative.class)) { |
| newQual = newQual.glb(typeOfAddition); |
| } |
| JavaExpression operandJe = JavaExpression.fromNode(operand); |
| store.insertValue(operandJe, atypeFactory.convertUBQualifierToAnnotation(newQual)); |
| } |
| |
| /** |
| * Case 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. |
| */ |
| @Override |
| protected void refineGT( |
| Node larger, |
| AnnotationMirror largerAnno, |
| Node smaller, |
| AnnotationMirror smallerAnno, |
| CFStore store, |
| TransferInput<CFValue, CFStore> in) { |
| // larger > smaller |
| UBQualifier largerQual = |
| UBQualifier.createUBQualifier(largerAnno, (UpperBoundChecker) atypeFactory.getChecker()); |
| // larger + 1 >= smaller |
| UBQualifier largerQualPlus1 = largerQual.plusOffset(1); |
| UBQualifier rightQualifier = |
| UBQualifier.createUBQualifier(smallerAnno, (UpperBoundChecker) atypeFactory.getChecker()); |
| UBQualifier refinedRight = rightQualifier.glb(largerQualPlus1); |
| |
| if (largerQualPlus1.isLessThanLengthQualifier()) { |
| propagateToOperands((LessThanLengthOf) largerQualPlus1, smaller, in, store); |
| } |
| |
| refineSubtrahendWithOffset(larger, smaller, true, in, store); |
| |
| JavaExpression rightJe = JavaExpression.fromNode(smaller); |
| store.insertValue(rightJe, atypeFactory.convertUBQualifierToAnnotation(refinedRight)); |
| } |
| |
| /** |
| * Case 9: if x ≤ y, and y has a type that is related to the length of an array, then x has the |
| * same type. |
| */ |
| @Override |
| protected void refineGTE( |
| Node left, |
| AnnotationMirror leftAnno, |
| Node right, |
| AnnotationMirror rightAnno, |
| CFStore store, |
| TransferInput<CFValue, CFStore> in) { |
| UBQualifier leftQualifier = |
| UBQualifier.createUBQualifier(leftAnno, (UpperBoundChecker) atypeFactory.getChecker()); |
| UBQualifier rightQualifier = |
| UBQualifier.createUBQualifier(rightAnno, (UpperBoundChecker) atypeFactory.getChecker()); |
| UBQualifier refinedRight = rightQualifier.glb(leftQualifier); |
| |
| if (leftQualifier.isLessThanLengthQualifier()) { |
| propagateToOperands((LessThanLengthOf) leftQualifier, right, in, store); |
| } |
| |
| refineSubtrahendWithOffset(left, right, false, in, store); |
| |
| JavaExpression rightJe = JavaExpression.fromNode(right); |
| store.insertValue(rightJe, atypeFactory.convertUBQualifierToAnnotation(refinedRight)); |
| } |
| |
| /** |
| * Refines 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. This is |
| * case 10. |
| * |
| * <p>This is based on the fact that if {@code (minuend - subtrahend) >= offset}, and {@code |
| * minuend + o < l}, then {@code subtrahend + o + offset < l}. |
| * |
| * <p>If {@code gtNode} is not a {@link NumericalSubtractionNode}, the method does nothing. |
| * |
| * @param gtNode the node that is greater or equal to the offset |
| * @param offsetNode a node part of the offset |
| * @param offsetAddOne whether to add one to the offset |
| * @param in input of the transfer function |
| * @param store location to store the refined types |
| */ |
| private void refineSubtrahendWithOffset( |
| Node gtNode, |
| Node offsetNode, |
| boolean offsetAddOne, |
| TransferInput<CFValue, CFStore> in, |
| CFStore store) { |
| if (gtNode instanceof NumericalSubtractionNode) { |
| NumericalSubtractionNode subtractionNode = (NumericalSubtractionNode) gtNode; |
| |
| Node minuend = subtractionNode.getLeftOperand(); |
| UBQualifier minuendQual = getUBQualifier(minuend, in); |
| Node subtrahend = subtractionNode.getRightOperand(); |
| UBQualifier subtrahendQual = getUBQualifier(subtrahend, in); |
| |
| UBQualifier newQual = |
| subtrahendQual.glb( |
| minuendQual.plusOffset(offsetNode, atypeFactory).plusOffset(offsetAddOne ? 1 : 0)); |
| JavaExpression subtrahendJe = JavaExpression.fromNode(subtrahend); |
| store.insertValue(subtrahendJe, atypeFactory.convertUBQualifierToAnnotation(newQual)); |
| } |
| } |
| |
| /** Implements case 11. */ |
| @Override |
| protected TransferResult<CFValue, CFStore> strengthenAnnotationOfEqualTo( |
| TransferResult<CFValue, CFStore> res, |
| Node firstNode, |
| Node secondNode, |
| CFValue firstValue, |
| CFValue secondValue, |
| boolean notEqualTo) { |
| TransferResult<CFValue, CFStore> result = |
| super.strengthenAnnotationOfEqualTo( |
| res, firstNode, secondNode, firstValue, secondValue, notEqualTo); |
| IndexRefinementInfo rfi = new IndexRefinementInfo(result, analysis, firstNode, secondNode); |
| if (rfi.leftAnno == null || rfi.rightAnno == null) { |
| return result; |
| } |
| |
| CFStore equalsStore = notEqualTo ? rfi.elseStore : rfi.thenStore; |
| CFStore notEqualStore = notEqualTo ? rfi.thenStore : rfi.elseStore; |
| |
| refineEq(rfi.left, rfi.leftAnno, rfi.right, rfi.rightAnno, equalsStore); |
| |
| refineNeqSequenceLength(rfi.left, rfi.right, rfi.rightAnno, notEqualStore); |
| refineNeqSequenceLength(rfi.right, rfi.left, rfi.leftAnno, notEqualStore); |
| return rfi.newResult; |
| } |
| |
| /** Refines the type of the left and right node to glb of the left and right annotation. */ |
| private void refineEq( |
| Node left, AnnotationMirror leftAnno, Node right, AnnotationMirror rightAnno, CFStore store) { |
| UBQualifier leftQualifier = |
| UBQualifier.createUBQualifier(leftAnno, (UpperBoundChecker) atypeFactory.getChecker()); |
| UBQualifier rightQualifier = |
| UBQualifier.createUBQualifier(rightAnno, (UpperBoundChecker) atypeFactory.getChecker()); |
| UBQualifier glb = rightQualifier.glb(leftQualifier); |
| AnnotationMirror glbAnno = atypeFactory.convertUBQualifierToAnnotation(glb); |
| |
| List<Node> internalsRight = splitAssignments(right); |
| for (Node internal : internalsRight) { |
| JavaExpression rightJe = JavaExpression.fromNode(internal); |
| store.insertValue(rightJe, glbAnno); |
| } |
| |
| List<Node> internalsLeft = splitAssignments(left); |
| for (Node internal : internalsLeft) { |
| JavaExpression leftJe = JavaExpression.fromNode(internal); |
| store.insertValue(leftJe, glbAnno); |
| } |
| } |
| |
| /** |
| * If lengthAccess node 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). |
| * This is case 12. |
| */ |
| private void refineNeqSequenceLength( |
| Node lengthAccess, Node otherNode, AnnotationMirror otherNodeAnno, CFStore store) { |
| |
| // If lengthAccess is "receiver.length - c" where c is an integer constant, |
| // then lengthOffset is "c". |
| int lengthOffset = 0; |
| if (lengthAccess instanceof NumericalSubtractionNode) { |
| NumericalSubtractionNode subtraction = (NumericalSubtractionNode) lengthAccess; |
| Node offsetNode = subtraction.getRightOperand(); |
| Long offsetValue = |
| ValueCheckerUtils.getExactValue( |
| offsetNode.getTree(), atypeFactory.getValueAnnotatedTypeFactory()); |
| if (offsetValue != null |
| && offsetValue > Integer.MIN_VALUE |
| && offsetValue <= Integer.MAX_VALUE) { |
| lengthOffset = offsetValue.intValue(); |
| lengthAccess = subtraction.getLeftOperand(); |
| } else { |
| // Subtraction of non-constant expressions is not supported |
| return; |
| } |
| } |
| |
| JavaExpression receiver = null; |
| if (NodeUtils.isArrayLengthFieldAccess(lengthAccess)) { |
| FieldAccess fa = |
| (FieldAccess) JavaExpression.fromNodeFieldAccess((FieldAccessNode) lengthAccess); |
| receiver = fa.getReceiver(); |
| |
| } else if (atypeFactory.getMethodIdentifier().isLengthOfMethodInvocation(lengthAccess)) { |
| JavaExpression ma = JavaExpression.fromNode(lengthAccess); |
| if (ma instanceof MethodCall) { |
| receiver = ((MethodCall) ma).getReceiver(); |
| } |
| } |
| |
| if (receiver != null && !receiver.containsUnknown()) { |
| UBQualifier otherQualifier = |
| UBQualifier.createUBQualifier( |
| otherNodeAnno, (UpperBoundChecker) atypeFactory.getChecker()); |
| String sequence = receiver.toString(); |
| // Check if otherNode + c - 1 < receiver.length |
| if (otherQualifier.hasSequenceWithOffset(sequence, lengthOffset - 1)) { |
| // Add otherNode + c < receiver.length |
| UBQualifier newQualifier = |
| UBQualifier.createUBQualifier(sequence, Integer.toString(lengthOffset)); |
| otherQualifier = otherQualifier.glb(newQualifier); |
| for (Node internal : splitAssignments(otherNode)) { |
| JavaExpression leftJe = JavaExpression.fromNode(internal); |
| store.insertValue(leftJe, atypeFactory.convertUBQualifierToAnnotation(otherQualifier)); |
| } |
| } |
| } |
| } |
| |
| /** |
| * 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"}). |
| * |
| * <p>Alternatively, 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.) |
| * |
| * <p>In addition, 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"). |
| * |
| * <p>These three cases correspond to cases 13-15. |
| */ |
| @Override |
| public TransferResult<CFValue, CFStore> visitNumericalAddition( |
| NumericalAdditionNode n, TransferInput<CFValue, CFStore> in) { |
| // type of leftNode + rightNode is glb(t, s) where |
| // t = minusOffset(type(leftNode), rightNode) and |
| // s = minusOffset(type(rightNode), leftNode) |
| |
| UBQualifier left = getUBQualifierForAddition(n.getLeftOperand(), in); |
| UBQualifier t = left.minusOffset(n.getRightOperand(), atypeFactory); |
| |
| UBQualifier right = getUBQualifierForAddition(n.getRightOperand(), in); |
| UBQualifier s = right.minusOffset(n.getLeftOperand(), atypeFactory); |
| |
| UBQualifier glb = t.glb(s); |
| if (left.isLessThanLengthQualifier() && right.isLessThanLengthQualifier()) { |
| // 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"). |
| UBQualifier r = removeSequenceLengths((LessThanLengthOf) left, (LessThanLengthOf) right); |
| glb = glb.glb(r); |
| UBQualifier l = removeSequenceLengths((LessThanLengthOf) right, (LessThanLengthOf) left); |
| glb = glb.glb(l); |
| } |
| |
| return createTransferResult(n, in, glb); |
| } |
| |
| /** |
| * Return the result of adding i to j. |
| * |
| * <p>When expression i has type {@code @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"). |
| * |
| * <p>When expression i has type {@code @LTLengthOf (value = "f2", offset = "f1.length - 1") int} |
| * and expression j is less than the length of f1, then the type of i + j is @LTLengthOf("f2"). |
| * |
| * @param i the type of the expression added to j |
| * @param j the type of the expression added to i |
| * @return the type of i + j |
| */ |
| private UBQualifier removeSequenceLengths(LessThanLengthOf i, LessThanLengthOf j) { |
| List<String> lessThan = new ArrayList<>(); |
| List<String> lessThanOrEqual = new ArrayList<>(); |
| for (String sequence : i.getSequences()) { |
| if (i.isLessThanLengthOf(sequence)) { |
| lessThan.add(sequence); |
| } else if (i.hasSequenceWithOffset(sequence, -1)) { |
| lessThanOrEqual.add(sequence); |
| } |
| } |
| // Creates a qualifier that is the same a j with the array.length offsets removed. If |
| // an offset doesn't have an array.length, then the offset/array pair is removed. If |
| // there are no such pairs, Unknown is returned. |
| UBQualifier lessThanEqQ = j.removeSequenceLengthAccess(lessThanOrEqual); |
| // Creates a qualifier that is the same a j with the array.length - 1 offsets removed. If |
| // an offset doesn't have an array.length, then the offset/array pair is removed. If |
| // there are no such pairs, Unknown is returned. |
| UBQualifier lessThanQ = j.removeSequenceLengthAccessAndNeg1(lessThan); |
| |
| return lessThanEqQ.glb(lessThanQ); |
| } |
| |
| /** |
| * 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"). If b is known to be less than the length of some other |
| * sequence, this doesn't add any information about the type of a - b. But, if b is non-negative |
| * or positive, then a - b should keep the types of a. This corresponds to cases 16 and 17. |
| */ |
| @Override |
| public TransferResult<CFValue, CFStore> visitNumericalSubtraction( |
| NumericalSubtractionNode n, TransferInput<CFValue, CFStore> in) { |
| UBQualifier left = getUBQualifier(n.getLeftOperand(), in); |
| UBQualifier leftWithOffset = left.plusOffset(n.getRightOperand(), atypeFactory); |
| if (atypeFactory.hasLowerBoundTypeByClass(n.getRightOperand(), NonNegative.class) |
| || atypeFactory.hasLowerBoundTypeByClass(n.getRightOperand(), Positive.class)) { |
| // If the right side of the expression is NN or POS, then all the left side's |
| // annotations should be kept. |
| if (left.isLessThanLengthQualifier()) { |
| leftWithOffset = left.glb(leftWithOffset); |
| } |
| } |
| |
| // If the result of a numerical subtraction would be LTEL(b) or LTL(b), and b is HSS(a, |
| // from, to), and the subtraction node itself is i - from where i is LTEL(b), then the |
| // result is LTEL(a). If i is LTL(b) instead, the result is LTL(a). |
| |
| if (leftWithOffset.isLessThanLengthQualifier()) { |
| |
| LessThanLengthOf subtractionResult = (LessThanLengthOf) leftWithOffset; |
| |
| for (String b : subtractionResult.getSequences()) { |
| if (subtractionResult.hasSequenceWithOffset(b, -1) |
| || subtractionResult.hasSequenceWithOffset(b, 0)) { |
| |
| TreePath currentPath = this.atypeFactory.getPath(n.getTree()); |
| JavaExpression je; |
| try { |
| je = UpperBoundVisitor.parseJavaExpressionString(b, atypeFactory, currentPath); |
| } catch (NullPointerException npe) { |
| // I have no idea why this seems to happen only on a few JDK classes. It appears to |
| // only happen during the preprocessing step - the NPE is thrown while trying to find |
| // the enclosing class of a class tree, which is null. I can't find a reproducible test |
| // case that's smaller than the size of DualPivotQuicksort. Since this refinement is |
| // optional, but useful elsewhere, catching this NPE here and returning is always safe. |
| return createTransferResult(n, in, leftWithOffset); |
| } |
| |
| Subsequence subsequence = Subsequence.getSubsequenceFromReceiver(je, atypeFactory); |
| |
| if (subsequence != null) { |
| String from = subsequence.from; |
| String to = subsequence.to; |
| String a = subsequence.array; |
| |
| JavaExpression leftOp = JavaExpression.fromNode(n.getLeftOperand()); |
| JavaExpression rightOp = JavaExpression.fromNode(n.getRightOperand()); |
| |
| if (rightOp.toString().equals(from)) { |
| LessThanAnnotatedTypeFactory lessThanAtypeFactory = |
| atypeFactory.getLessThanAnnotatedTypeFactory(); |
| AnnotationMirror lessThanType = |
| lessThanAtypeFactory |
| .getAnnotatedType(n.getLeftOperand().getTree()) |
| .getAnnotation(LessThan.class); |
| |
| if (lessThanType != null && lessThanAtypeFactory.isLessThan(lessThanType, to)) { |
| UBQualifier ltlA = UBQualifier.createUBQualifier(a, "0"); |
| leftWithOffset = leftWithOffset.glb(ltlA); |
| } else if (leftOp.toString().equals(to) |
| || (lessThanType != null |
| && lessThanAtypeFactory.isLessThanOrEqual(lessThanType, to))) { |
| // It's necessary to check if leftOp == to because LessThan doesn't |
| // infer that things are less than or equal to themselves. |
| UBQualifier ltelA = UBQualifier.createUBQualifier(a, "-1"); |
| leftWithOffset = leftWithOffset.glb(ltelA); |
| } |
| } |
| } |
| } |
| } |
| } |
| return createTransferResult(n, in, leftWithOffset); |
| } |
| |
| /** |
| * Computes a type of a sequence length access. This is case 18. |
| * |
| * @param n sequence length access node |
| */ |
| private TransferResult<CFValue, CFStore> visitLengthAccess( |
| Node n, TransferInput<CFValue, CFStore> in, JavaExpression sequenceJe, Tree sequenceTree) { |
| if (sequenceTree == null) { |
| return null; |
| } |
| // Look up the SameLen type of the sequence. |
| AnnotationMirror sameLenAnno = atypeFactory.sameLenAnnotationFromTree(sequenceTree); |
| List<String> sameLenSequences; |
| if (sameLenAnno == null) { |
| sameLenSequences = Collections.singletonList(sequenceJe.toString()); |
| } else { |
| sameLenSequences = |
| AnnotationUtils.getElementValueArray( |
| sameLenAnno, atypeFactory.sameLenValueElement, String.class); |
| String sequenceString = sequenceJe.toString(); |
| if (!sameLenSequences.contains(sequenceString)) { |
| sameLenSequences.add(sequenceString); |
| } |
| } |
| |
| List<String> offsets = Collections.nCopies(sameLenSequences.size(), "-1"); |
| |
| if (CFAbstractStore.canInsertJavaExpression(sequenceJe)) { |
| UBQualifier qualifier = UBQualifier.createUBQualifier(sameLenSequences, offsets); |
| UBQualifier previous = getUBQualifier(n, in); |
| return createTransferResult(n, in, qualifier.glb(previous)); |
| } |
| |
| return null; |
| } |
| |
| /** |
| * 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. This is case 19. |
| */ |
| @Override |
| public TransferResult<CFValue, CFStore> visitFieldAccess( |
| FieldAccessNode n, TransferInput<CFValue, CFStore> in) { |
| if (NodeUtils.isArrayLengthFieldAccess(n)) { |
| FieldAccess arrayLength = (FieldAccess) JavaExpression.fromNodeFieldAccess(n); |
| JavaExpression arrayJe = arrayLength.getReceiver(); |
| Tree arrayTree = n.getReceiver().getTree(); |
| TransferResult<CFValue, CFStore> result = visitLengthAccess(n, in, arrayJe, arrayTree); |
| if (result != null) { |
| return result; |
| } |
| } |
| return super.visitFieldAccess(n, in); |
| } |
| |
| /** |
| * 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. This is case 20. |
| */ |
| @Override |
| public TransferResult<CFValue, CFStore> visitMethodInvocation( |
| MethodInvocationNode n, TransferInput<CFValue, CFStore> in) { |
| |
| if (atypeFactory.getMethodIdentifier().isLengthOfMethodInvocation(n)) { |
| JavaExpression stringLength = JavaExpression.fromNode(n); |
| if (stringLength instanceof MethodCall) { |
| JavaExpression receiverJe = ((MethodCall) stringLength).getReceiver(); |
| Tree receiverTree = n.getTarget().getReceiver().getTree(); |
| // receiverTree is null when the receiver is implicit "this". |
| if (receiverTree != null) { |
| TransferResult<CFValue, CFStore> result = |
| visitLengthAccess(n, in, receiverJe, receiverTree); |
| if (result != null) { |
| return result; |
| } |
| } |
| } |
| } |
| return super.visitMethodInvocation(n, in); |
| } |
| |
| /** |
| * Returns the UBQualifier for a node, with additional refinement useful specifically for integer |
| * addition, based on the information from subcheckers of the Index Checker. |
| * |
| * @param n the node |
| * @param in dataflow analysis transfer input |
| * @return the UBQualifier for {@code node} |
| */ |
| private UBQualifier getUBQualifierForAddition(Node n, TransferInput<CFValue, CFStore> in) { |
| |
| // The method takes the greatest lower bound of the qualifier returned by |
| // getUBQualifier and a qualifier created from a SubstringIndexFor annotation, if such |
| // annotation is present and the index is known to be non-negative. |
| |
| UBQualifier ubQualifier = getUBQualifier(n, in); |
| Tree nodeTree = n.getTree(); |
| // Annotation from the Substring Index hierarchy |
| AnnotatedTypeMirror substringIndexType = |
| atypeFactory.getSubstringIndexAnnotatedTypeFactory().getAnnotatedType(nodeTree); |
| AnnotationMirror substringIndexAnno = substringIndexType.getAnnotation(SubstringIndexFor.class); |
| // Annotation from the Lower bound hierarchy |
| AnnotatedTypeMirror lowerBoundType = |
| atypeFactory.getLowerBoundAnnotatedTypeFactory().getAnnotatedType(nodeTree); |
| // If the index has an SubstringIndexFor annotation and at the same time is non-negative, |
| // convert the SubstringIndexFor annotation to a upper bound qualifier. |
| if (substringIndexAnno != null |
| && (lowerBoundType.hasAnnotation(NonNegative.class) |
| || lowerBoundType.hasAnnotation(Positive.class))) { |
| UBQualifier substringIndexQualifier = |
| UBQualifier.createUBQualifier( |
| substringIndexAnno, (UpperBoundChecker) atypeFactory.getChecker()); |
| ubQualifier = ubQualifier.glb(substringIndexQualifier); |
| } |
| return ubQualifier; |
| } |
| |
| /** |
| * Returns the UBQualifier for node. It does this by finding a {@link CFValue} for node. First it |
| * checks the store in the transfer input. If one isn't there, the analysis is checked. If the |
| * UNKNOWN qualifier is returned, then the AnnotatedTypeMirror from the type factory is used. |
| * |
| * @param n node |
| * @param in transfer input |
| * @return the UBQualifier for node |
| */ |
| private UBQualifier getUBQualifier(Node n, TransferInput<CFValue, CFStore> in) { |
| QualifierHierarchy hierarchy = analysis.getTypeFactory().getQualifierHierarchy(); |
| JavaExpression je = JavaExpression.fromNode(n); |
| CFValue value = null; |
| if (CFAbstractStore.canInsertJavaExpression(je)) { |
| value = in.getRegularStore().getValue(je); |
| } |
| if (value == null) { |
| value = analysis.getValue(n); |
| } |
| UBQualifier qualifier = getUBQualifier(hierarchy, value); |
| if (qualifier.isUnknown()) { |
| // The qualifier from the store or analysis might be UNKNOWN if there was some error. |
| // For example, |
| // @LTLength("a") int i = 4; // error |
| // The type of i in the store is @UpperBoundUnknown, but the type of i as computed by |
| // the type factory is @LTLength("a"), so use that type. |
| CFValue valueFromFactory = getValueFromFactory(n.getTree(), n); |
| return getUBQualifier(hierarchy, valueFromFactory); |
| } |
| return qualifier; |
| } |
| |
| private UBQualifier getUBQualifier(QualifierHierarchy hierarchy, CFValue value) { |
| if (value == null) { |
| return UpperBoundUnknownQualifier.UNKNOWN; |
| } |
| Set<AnnotationMirror> set = value.getAnnotations(); |
| AnnotationMirror anno = hierarchy.findAnnotationInHierarchy(set, atypeFactory.UNKNOWN); |
| if (anno == null) { |
| return UpperBoundUnknownQualifier.UNKNOWN; |
| } |
| return UBQualifier.createUBQualifier(anno, (UpperBoundChecker) atypeFactory.getChecker()); |
| } |
| |
| private TransferResult<CFValue, CFStore> createTransferResult( |
| Node n, TransferInput<CFValue, CFStore> in, UBQualifier qualifier) { |
| AnnotationMirror newAnno = atypeFactory.convertUBQualifierToAnnotation(qualifier); |
| CFValue value = analysis.createSingleAnnotationValue(newAnno, n.getType()); |
| return createTransferResult(value, in); |
| } |
| |
| @Override |
| public TransferResult<CFValue, CFStore> visitCase( |
| CaseNode n, TransferInput<CFValue, CFStore> in) { |
| TransferResult<CFValue, CFStore> result = super.visitCase(n, in); |
| // Refines subtrahend in the switch expression |
| // TODO: This cannot be done in strengthenAnnotationOfEqualTo, because that does not provide |
| // transfer input. |
| Node caseNode = n.getCaseOperand(); |
| AssignmentNode assign = (AssignmentNode) n.getSwitchOperand(); |
| Node switchNode = assign.getExpression(); |
| refineSubtrahendWithOffset(switchNode, caseNode, false, in, result.getThenStore()); |
| return result; |
| } |
| |
| @Override |
| public TransferResult<CFValue, CFStore> visitIntegerLiteral( |
| IntegerLiteralNode n, TransferInput<CFValue, CFStore> pi) { |
| TransferResult<CFValue, CFStore> result = super.visitIntegerLiteral(n, pi); |
| |
| int intValue = n.getValue(); |
| AnnotationMirror newAnno; |
| switch (intValue) { |
| case 0: |
| newAnno = atypeFactory.ZERO; |
| break; |
| case -1: |
| newAnno = atypeFactory.NEGATIVEONE; |
| break; |
| default: |
| return result; |
| } |
| CFValue c = new CFValue(analysis, Collections.singleton(newAnno), intTM); |
| return new RegularTransferResult<>(c, result.getRegularStore()); |
| } |
| } |
