boolean (@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() >= 0 && (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; }