boolean (DfaValue left, RelationType type, DfaValue right) { if (type != RelationType.LT && type != RelationType.GT && type != RelationType.NE && type != RelationType.EQ) return true; if (!(left instanceof DfaBinOpValue binOp)) { if (right instanceof DfaBinOpValue) { return applyBinOpRelations(right, type.getFlipped(), left); } return true; } LongRangeBinOp op = binOp.getOperation(); if (op != LongRangeBinOp.PLUS && op != LongRangeBinOp.MINUS) return true; DfaVariableValue leftLeft = binOp.getLeft(); DfaValue leftRight = binOp.getRight(); LongRangeSet leftRange = extractRange(getDfType(leftLeft)); LongRangeSet rightRange = extractRange(getDfType(leftRight)); LongRangeType lrType = binOp.getDfType().getLongRangeType(); LongRangeSet rightNegated = rightRange.negate(lrType); LongRangeSet rightCorrected = op == LongRangeBinOp.MINUS ? rightNegated : rightRange; LongRangeSet resultRange = extractRange(getDfType(right)); RelationType correctedRelation = correctRelation(type, leftRange, rightCorrected, resultRange, lrType); if (op == LongRangeBinOp.MINUS) { long min = resultRange.min(); long max = resultRange.max(); if (min == 0 && max == 0) { // a-b (rel) 0 => a (rel) b if (!applyCondition(leftLeft.cond(correctedRelation, leftRight))) return false; } else if (min == 0 && type == RelationType.GT || min >= 1 && RelationType.GE.isSubRelation(type)) { RelationType correctedGt = correctRelation(RelationType.GT, leftRange, rightCorrected, resultRange, lrType); if (!applyCondition(leftLeft.cond(correctedGt, leftRight))) return false; } else if (max == 0 && type == RelationType.LT || max <= -1 && RelationType.LE.isSubRelation(type)) { RelationType correctedLt = correctRelation(RelationType.LT, leftRange, rightCorrected, resultRange, lrType); if (!applyCondition(leftLeft.cond(correctedLt, leftRight))) return false; } if (RelationType.EQ.equals(type) && !resultRange.contains(0)) { // a-b == non-zero => a != b if (!applyRelation(leftLeft, leftRight, true)) return false; } } if (op == LongRangeBinOp.PLUS && RelationType.EQ == type && !resultRange.intersects(lrType.fullRange().mul(LongRangeSet.point(2), lrType))) { // a+b == odd => a != b if (!applyRelation(leftLeft, leftRight, true)) return false; } if (right instanceof DfaVariableValue) { // a+b (rel) c && a == c => b (rel) 0 if (areEqual(leftLeft, right)) { RelationType finalRelation = op == LongRangeBinOp.MINUS ? Objects.requireNonNull(correctedRelation.getFlipped()) : correctedRelation; if (!applyCondition(leftRight.cond(finalRelation, binOp.getDfType().meetRange(LongRangeSet.point(0))))) return false; } // a+b (rel) c && b == c => a (rel) 0 if (op == LongRangeBinOp.PLUS && areEqual(leftRight, right)) { if (!applyCondition(leftLeft.cond(correctedRelation, binOp.getDfType().meetRange(LongRangeSet.point(0))))) return false; } if (!applyRelationOnAddition(type, leftLeft, leftRange, rightCorrected, right, lrType)) return false; if (op == LongRangeBinOp.PLUS && leftRight instanceof DfaVariableValue) { if (!applyRelationOnAddition(type, (DfaVariableValue)leftRight, rightRange, leftRange, right, lrType)) return false; } } return true; }