[java-dfa] Handling special cases for modular division

GitOrigin-RevId: 1acfd9722b1e171abd61181d35f856e3eba171eb

java/java-analysis-impl/src/com/intellij/codeInspection/dataFlow/value/DfaBinOpValue.java

@@ -167,6 +167,11 @@ public final class DfaBinOpValue extends DfaValue {
         return myFactory.getInt(0);
       }
       if (op == LongRangeBinOp.MOD) {
+        if (leftDfType instanceof DfIntegralType && rightDfType instanceof DfIntegralType) {
+          if (withinDivisorRange(state, left, right, ((DfIntegralType)leftDfType).getRange(), ((DfIntegralType)rightDfType).getRange())) {
+            return left;
+          }
+        }
         if (left instanceof DfaVariableValue && rightConst != null) {
           long divisor = rightConst.longValue();
           if (divisor > 1 && divisor <= Long.SIZE) {
@@ -222,6 +227,62 @@ public final class DfaBinOpValue extends DfaValue {
       return null;
     }
 
+    /**
+     * @param state memory state
+     * @param dividend dividend
+     * @param divisor divisor
+     * @param dividendRange
+     * @param divisorRange
+     * @return true if it's known that dividend is within divisor range
+     */
+    private static boolean withinDivisorRange(@NotNull DfaMemoryState state,
+                                              @NotNull DfaValue dividend,
+                                              @NotNull DfaValue divisor,
+                                              @NotNull LongRangeSet dividendRange,
+                                              @NotNull LongRangeSet divisorRange) {
+      if (divisorRange.min() > 0) {
+        // a % b where 0 <= a < b
+        if (dividendRange.min() > -divisorRange.max() && 
+            (dividendRange.max() < divisorRange.min() || state.getRelation(dividend, divisor) == RelationType.LT)) {
+          return true;
+        }
+        if (dividend instanceof DfaBinOpValue) {
+          LongRangeBinOp prevOp = ((DfaBinOpValue)dividend).getOperation();
+          if (prevOp == LongRangeBinOp.MINUS) {
+            boolean negative = dividendRange.max() <= 0;
+            boolean positive = dividendRange.min() >= 0;
+            if (positive || negative) {
+              DfaVariableValue left = ((DfaBinOpValue)dividend).getLeft();
+              DfaValue right = ((DfaBinOpValue)dividend).getRight();
+              DfIntegralType leftType = ObjectUtils.tryCast(state.getDfType(left), DfIntegralType.class);
+              DfIntegralType rightType = ObjectUtils.tryCast(state.getDfType(right), DfIntegralType.class);
+              if (leftType != null && rightType != null) {
+                LongRangeSet leftRange = leftType.getRange();
+                LongRangeSet rightRange = rightType.getRange();
+                if (leftRange.min() >= 0 && rightRange.min() >= 0) {
+                  // (a-b) % c where (a-b)<0 && a>=0 && b>=0 && b<c (or b==c && a>0)
+                  if (negative) {
+                    RelationType relation = state.getRelation(right, divisor);
+                    if (relation == RelationType.LT || relation == RelationType.EQ && leftRange.min() >= 1) {
+                      return true;
+                    }
+                  }
+                  // (a-b) % c where (a-b)>0 && a>=0 && b>=0 && a<c (or a==c && b>0)
+                  if (positive) {
+                    RelationType relation = state.getRelation(left, divisor);
+                    if (relation == RelationType.LT || relation == RelationType.EQ && rightRange.min() >= 1) {
+                      return true;
+                    }
+                  }
+                }
+              }
+            }
+          }
+        }
+      }
+      return false;
+    }
+
     @NotNull
     private DfaBinOpValue doCreate(DfaVariableValue left, DfaValue right, boolean isLong, LongRangeBinOp op) {
       long hash = ((isLong ? 1L : 0L) << 63) | ((long)left.getID() << 32) | right.getID();

java/java-analysis-impl/src/com/intellij/codeInspection/dataFlow/value/DfaCondition.java

@@ -98,6 +98,9 @@ public abstract class DfaCondition {
       }
       DfType leftType = dfaLeft.getDfType();
       DfType rightType = dfaRight.getDfType();
+      if (dfaLeft == dfaRight && dfaLeft instanceof DfaBinOpValue) {
+        return fromBoolean(relationType.isSubRelation(RelationType.EQ));
+      }
 
       if (relationType == RelationType.EQ || relationType == RelationType.NE) {
         if (leftType instanceof DfConstantType) {

java/java-tests/testData/inspection/dataFlow/fixture/ModSpecialCase.java

@@ -0,0 +1,40 @@
+import java.util.*;
+
+public class ModSpecialCase {
+  void test4(int a, int b, int c) {
+    if (a >= 0 && a < 1000) {
+      if (b >= 0 && b < 1000) {
+        if (a < c && a > b && <warning descr="Condition '(a - b) % c == a - b' is always 'true'">(a - b) % c == a - b</warning>) { }
+        if (a < c && a > b && <warning descr="Condition '(b - a) % c == b - a' is always 'true'">(b - a) % c == b - a</warning>) { }
+      }
+    }
+  }
+
+  void test3(int a, int b) {
+    if (a >= 0 && a < 1000) {
+      if (b >= 0 && b < 1000) {
+        if (<warning descr="Condition '(a - b) % 1000 != a - b' is always 'false'">(a - b) % 1000 != a - b</warning>) {}
+      }
+    }
+  }
+
+  void test2(String string, String s1, String s2) {
+    if (string.isEmpty() || s2.isEmpty()) return;
+    long sl = string.length();
+    long vc = s1.length();
+    long s2l = s2.length();
+    long st = vc + s2l;
+    if (sl < vc) {
+      if (<warning descr="Condition '(sl - vc) % st != 0' is always 'true'">(sl - vc) % st != 0</warning>) {
+
+      }
+    }
+  }
+
+  void test(String s1, String s2) {
+    if (s1.length() < s2.length()) {
+      int sz = s1.length() % s2.length();
+      if (<warning descr="Condition 'sz == s1.length()' is always 'true'">sz == s1.length()</warning>) {}
+    }
+  }
+}

java/java-tests/testSrc/com/intellij/java/codeInspection/DataFlowRangeAnalysisTest.java

@@ -79,4 +79,5 @@ public class DataFlowRangeAnalysisTest extends DataFlowInspectionTestCase {
   public void testDontWidenPlusInLoop() { doTest(); }
   public void testCollectionAddRemove() { doTest(); }
   public void testRelationsOnAddition() { doTest(); }
+  public void testModSpecialCase() { doTest(); }
 }