From 11199c7acbd51eee103a5373895346cf97ce4d0b Mon Sep 17 00:00:00 2001 From: Tagir Valeev Date: Mon, 31 Dec 2018 15:51:32 +0700 Subject: [PATCH] DfaMemoryStateImpl#applySumRelations: fix bugs; apply relations for x-y <=> number --- .../dataFlow/DfaMemoryStateImpl.java | 86 +++++++++++-------- .../dataFlow/fixture/Algebraic.java | 39 ++++++++- 2 files changed, 90 insertions(+), 35 deletions(-) diff --git a/java/java-analysis-impl/src/com/intellij/codeInspection/dataFlow/DfaMemoryStateImpl.java b/java/java-analysis-impl/src/com/intellij/codeInspection/dataFlow/DfaMemoryStateImpl.java index 4505f857357a..a3c78a10219e 100644 --- a/java/java-analysis-impl/src/com/intellij/codeInspection/dataFlow/DfaMemoryStateImpl.java +++ b/java/java-analysis-impl/src/com/intellij/codeInspection/dataFlow/DfaMemoryStateImpl.java @@ -718,9 +718,6 @@ public class DfaMemoryStateImpl implements DfaMemoryState { } DfaVariableValue left = sum.getLeft(); DfaValue right = sum.getRight(); - if (appliedRange.equals(LongRangeSet.point(0)) && sum.isNegation()) { - return applyCondition(myFactory.createCondition(left, RelationType.EQ, right)); - } LongRangeSet leftRange = getValueFact(left, DfaFactType.RANGE); LongRangeSet rightRange = getValueFact(right, DfaFactType.RANGE); if (leftRange == null || rightRange == null) return true; @@ -886,7 +883,8 @@ public class DfaMemoryStateImpl implements DfaMemoryState { } private boolean applySumRelations(DfaValue left, RelationType type, DfaValue right) { - if (left instanceof DfaSumValue && right instanceof DfaVariableValue) { + if (type != RelationType.LT && type != RelationType.GT && type != RelationType.NE && type != RelationType.EQ) return true; + if (left instanceof DfaSumValue) { DfaSumValue sum = (DfaSumValue)left; LongRangeSet leftRange = getValueFact(sum.getLeft(), DfaFactType.RANGE); LongRangeSet rightRange = getValueFact(sum.getRight(), DfaFactType.RANGE); @@ -895,51 +893,71 @@ public class DfaMemoryStateImpl implements DfaMemoryState { LongRangeSet rightNegated = rightRange.negate(isLong); LongRangeSet rightCorrected = sum.isNegation() ? rightNegated : rightRange; - if (!sum.isNegation()) { - RelationType correctedType = type; - if (type == RelationType.LT || type == RelationType.GT) { - boolean overflowPossible = true; - if (!isLong) { - LongRangeSet other = getValueFact(right, DfaFactType.RANGE); - LongRangeSet overflowRange = getIntegerSumOverflowValues(leftRange, rightCorrected); - overflowPossible = other == null || other.intersects(overflowRange); + LongRangeSet resultRange = getValueFact(right, DfaFactType.RANGE); + RelationType correctedRelation = correctRelation(type, leftRange, rightCorrected, resultRange, isLong); + if (sum.isNegation()) { + if (resultRange != null) { + long min = resultRange.min(); + long max = resultRange.max(); + if (min == 0 && max == 0) { + // a-b (rel) 0 => a (rel) b + if (!applyCondition(myFactory.createCondition(sum.getLeft(), correctedRelation, sum.getRight()))) return false; } - if (overflowPossible) { - correctedType = RelationType.NE; + else if (min >= 0 && RelationType.GE.isSubRelation(type)) { + RelationType correctedGt = correctRelation(RelationType.GT, leftRange, rightCorrected, resultRange, isLong); + if (!applyCondition(myFactory.createCondition(sum.getLeft(), correctedGt, sum.getRight()))) return false; + } + else if (max <= 0 && RelationType.LE.isSubRelation(type)) { + RelationType correctedLt = correctRelation(RelationType.LT, leftRange, rightCorrected, resultRange, isLong); + if (!applyCondition(myFactory.createCondition(sum.getLeft(), correctedLt, sum.getRight()))) return false; + } + if (RelationType.EQ.equals(type) && !resultRange.contains(0)) { + // a-b == non-zero => a != b + if (!applyRelation(sum.getLeft(), sum.getRight(), true)) return false; } } + } + if (right instanceof DfaVariableValue) { // a+b (rel) c && a == c => b (rel) 0 if (areEqual(sum.getLeft(), right)) { - if (!applyCondition(myFactory.createCondition(sum.getRight(), correctedType, myFactory.getInt(0)))) { - return false; - } + RelationType finalRelation = sum.isNegation() ? correctedRelation.getFlipped() : correctedRelation; + if (!applyCondition(myFactory.createCondition(sum.getRight(), finalRelation, myFactory.getInt(0)))) return false; } // a+b (rel) c && b == c => a (rel) 0 - if (areEqual(sum.getRight(), right)) { - if (!applyCondition(myFactory.createCondition(sum.getLeft(), correctedType, myFactory.getInt(0)))) { - return false; + if (!sum.isNegation() && areEqual(sum.getRight(), right)) { + if (!applyCondition(myFactory.createCondition(sum.getLeft(), correctedRelation, myFactory.getInt(0)))) return false; + } + + if (!leftRange.subtractionMayOverflow(sum.isNegation() ? rightRange : rightNegated, isLong)) { + // a-positiveNumber >= b => a > b + if (rightCorrected.max() < 0 && RelationType.GE.isSubRelation(type)) { + if (!applyLessThanRelation(right, sum.getLeft())) return false; + } + // a+positiveNumber >= b => a > b + if (rightCorrected.min() > 0 && RelationType.LE.isSubRelation(type)) { + if (!applyLessThanRelation(sum.getLeft(), right)) return false; } } - } - - if (!leftRange.subtractionMayOverflow(sum.isNegation() ? rightRange : rightNegated, isLong)) { - // a-positiveNumber >= b => a > b - if (rightCorrected.max() < 0 && RelationType.GE.isSubRelation(type)) { - if (!applyLessThanRelation(right, sum.getLeft())) return false; + if (RelationType.EQ == type && !rightRange.contains(0)) { + // a+nonZero == b => a != b + if (!applyRelation(sum.getLeft(), right, true)) return false; } - // a+positiveNumber >= b => a > b - if (rightCorrected.min() > 0 && RelationType.LE.isSubRelation(type)) { - if (!applyLessThanRelation(sum.getLeft(), right)) return false; - } - } - if (RelationType.EQ == type && !rightRange.contains(0)) { - // a+nonZero == b => a != b - if (!applyRelation(sum.getLeft(), right, true)) return false; } } return true; } + private static RelationType correctRelation(RelationType relation, LongRangeSet summand1, LongRangeSet summand2, + LongRangeSet resultRange, boolean isLong) { + if (relation != RelationType.LT && relation != RelationType.GT) return relation; + boolean overflowPossible = true; + if (!isLong) { + LongRangeSet overflowRange = getIntegerSumOverflowValues(summand1, summand2); + overflowPossible = !overflowRange.isEmpty() && (resultRange == null || resultRange.fromRelation(relation).intersects(overflowRange)); + } + return overflowPossible ? RelationType.NE : relation; + } + @NotNull private static LongRangeSet getIntegerSumOverflowValues(LongRangeSet left, LongRangeSet right) { if (left.isEmpty() || right.isEmpty()) return LongRangeSet.empty(); diff --git a/java/java-tests/testData/inspection/dataFlow/fixture/Algebraic.java b/java/java-tests/testData/inspection/dataFlow/fixture/Algebraic.java index 9ad87d9b78bb..ad719c56cb64 100644 --- a/java/java-tests/testData/inspection/dataFlow/fixture/Algebraic.java +++ b/java/java-tests/testData/inspection/dataFlow/fixture/Algebraic.java @@ -1,6 +1,18 @@ import java.util.*; public class Algebraic { + void testOverflowDetection(int[] arr1, int[] arr2, int offset) { + int l1 = arr1.length; + int l2 = arr2.length; + if (l1 < l2 || offset < 0) return; + if (l1 - offset >= l2) { + if (l1 == l2 && offset == 0) {} + } + if (l1 - offset <= l2) { + if (l1 == l2 && offset == 0) {} + } + } + void test(int x, int y) { if (x + 1 > 0) { if (x == -2) { @@ -39,7 +51,10 @@ public class Algebraic { || startOffset + length < 0) { throw new IndexOutOfBoundsException(); } - if (startOffset == buffer.length && length > 0) { + // This is always false, but we cannot reliably detect this yet. If startOffset == buffer.length + // then startOffset + length <= buffer.length implies that length == 0 *or* startOffset + length overflows + // The latest case is ruled out by startOffset + length < 0, but our memory state is unable to track this. + if (startOffset == buffer.length && length > 0) { } } @@ -78,4 +93,26 @@ public class Algebraic { if (c < 1 || c > text.length() - 1) return; if (text.length() > c) {} } + + void testDiff(int x, int y) { + if (x - y > 0 && x == y) {} + if (y > 0 && x >= y) { + if (x - y < 0) {} + if (x - y > 0 && x == y) {} + } + if (x > 0 && y > 0) { + if (x - y > 1 && x <= y) {} + if (x - y > -1 && x <= y) {} + if (x - y < -1 && x <= y) {} + if (x - y == y && x == y) {} + if (x - y < y && (x == y || x < y)) {} + if (x - y > y && (x == y || x > y)) {} + } else { + if (x - y > 1 && x <= y) {} + if (x - y > -1 && x <= y) {} + if (x - y < -1 && x <= y) {} + if (x - y == y && x == y) {} + if (x - y < y && (x == y || x < y)) {} + } + } }