MDS/openide
1
0
Fork 0
mirror of https://gitflic.ru/project/openide/openide.git synced 2026-09-27 10:03:11 +07:00
Code Issues Packages Projects Releases Wiki Activity

DfaMemoryStateImpl#applySumRelations: fix bugs; apply relations for x-y <=> number

Browse Source
This commit is contained in:
Tagir Valeev
2018-12-31 15:54:17 +07:00
parent dcefdc9a86
commit 11199c7acb
2 changed files with 90 additions and 35 deletions
Download Patch File Download Diff File Expand all files Collapse all files
java/java-analysis-impl/src/com/intellij/codeInspection/dataFlow/DfaMemoryStateImpl.java
+52 -34
View File
@@ -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();
java/java-tests/testData/inspection/dataFlow/fixture/Algebraic.java
+38 -1
View File
@@ -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 && <warning descr="Condition 'offset == 0' is always 'true' when reached">offset == 0</warning>) {}
}
if (l1 - offset <= l2) {
if (l1 == l2 && offset == 0) {}
}
}
void test(int x, int y) {
if (x + 1 > 0) {
if (<warning descr="Condition 'x == -2' is always 'false'">x == -2</warning>) {
@@ -39,7 +51,10 @@ public class Algebraic {
|| startOffset + length < 0) {
throw new IndexOutOfBoundsException();
}
if (<warning descr="Condition 'startOffset == buffer.length && length > 0' is always 'false'">startOffset == buffer.length && <warning descr="Condition 'length > 0' is always 'false' when reached">length > 0</warning></warning>) {
// 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 (<warning descr="Condition 'text.length() > c' is always 'true'">text.length() > c</warning>) {}
}
void testDiff(int x, int y) {
if (<warning descr="Condition 'x - y > 0 && x == y' is always 'false'">x - y > 0 && <warning descr="Condition 'x == y' is always 'false' when reached">x == y</warning></warning>) {}
if (y > 0 && x >= y) {
if (<warning descr="Condition 'x - y < 0' is always 'false'">x - y < 0</warning>) {}
if (<warning descr="Condition 'x - y > 0 && x == y' is always 'false'">x - y > 0 && <warning descr="Condition 'x == y' is always 'false' when reached">x == y</warning></warning>) {}
}
if (x > 0 && y > 0) {
if (<warning descr="Condition 'x - y > 1 && x <= y' is always 'false'">x - y > 1 && <warning descr="Condition 'x <= y' is always 'false' when reached">x <= y</warning></warning>) {}
if (x - y > -1 && x <= y) {}
if (x - y < -1 && <warning descr="Condition 'x <= y' is always 'true' when reached">x <= y</warning>) {}
if (<warning descr="Condition 'x - y == y && x == y' is always 'false'">x - y == y && <warning descr="Condition 'x == y' is always 'false' when reached">x == y</warning></warning>) {}
if (x - y < y && (x == y || x < y)) {}
if (x - y > y && (<warning descr="Condition 'x == y || x > y' is always 'true' when reached"><warning descr="Condition 'x == y' is always 'false' when reached">x == y</warning> || <warning descr="Condition 'x > y' is always 'true' when reached">x > y</warning></warning>)) {}
} 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)) {}
}
}
}