add range calculation for euclidean modulo

Author: maul-esel

trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Boogie2ACSL.java

@@ -451,10 +451,7 @@ private BacktranslatedExpression translateBinaryExpression(
 					return lhs;
 				}
 			}
-			final var absRightRange = rightRange.abs();
-			final var maxRightMinusOne =
-					absRightRange.getMaxValue() == null ? null : absRightRange.getMaxValue().subtract(BigInteger.ONE);
-			range = new BigInterval(BigInteger.ZERO, maxRightMinusOne);
+			range = leftRange.euclideanModulo(rightRange);
 
 			// TODO: properly backtranslate from euclidean modulo (mod) to C remainder (%)
 			operator = Operator.ARITHMOD;

trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/BigInterval.java

@@ -41,6 +41,8 @@ public class BigInterval {
 	public BigInterval(final BigInteger minValue, final BigInteger maxValue) {
 		mMinValue = minValue;
 		mMaxValue = maxValue;
+		assert mMinValue == null || mMaxValue == null
+				|| maxValue.compareTo(minValue) >= 0 : "empty interval not supported";
 	}
 
 	public static BigInterval unbounded() {
@@ -99,6 +101,24 @@ public boolean contains(final BigInteger element) {
 		return minBoundOk && maxBoundOk;
 	}
 
+	public BigInterval join(final BigInterval other) {
+		final var minValue = mMinValue == null || other.mMinValue == null ? null : mMinValue.min(other.mMinValue);
+		final var maxValue = mMaxValue == null || other.mMaxValue == null ? null : mMaxValue.max(other.mMaxValue);
+		return new BigInterval(minValue, maxValue);
+	}
+
+	public BigInterval intersect(final BigInterval other) {
+		final var minValue = mMinValue == null ? other.mMinValue
+				: other.mMinValue == null ? mMinValue : mMinValue.max(other.mMinValue);
+		final var maxValue = mMaxValue == null ? other.mMaxValue
+				: other.mMaxValue == null ? mMaxValue : mMaxValue.min(other.mMaxValue);
+		if (maxValue.compareTo(mMinValue) < 0) {
+			// empty interval not supported
+			return null;
+		}
+		return new BigInterval(minValue, maxValue);
+	}
+
 	public BigInterval negate() {
 		final var minValue = mMaxValue == null ? null : mMaxValue.negate();
 		final var maxValue = mMinValue == null ? null : mMinValue.negate();
@@ -232,4 +252,47 @@ public BigInterval euclideanModulo(final BigInteger divisor) {
 		// k*divisor-1 (modulo will be divisor-1), so the smallest interval encompassing all values is the entire range.
 		return new BigInterval(BigInteger.ZERO, absDivisor.subtract(BigInteger.ONE));
 	}
+
+	// Code adapted from https://stackoverflow.com/a/56918042 (there shown for truncating remainder)
+	public BigInterval euclideanModulo(final BigInterval divisor) {
+		if (divisor.contains(BigInteger.ZERO)) {
+			// Modulo resp. division by zero is unspecified, so we assume it can yield any number.
+			return unbounded();
+		}
+
+		if (divisor.isSingleton()) {
+			return euclideanModulo(divisor.mMinValue);
+		}
+
+		// For euclidean modulo, divisors D and (- D) yield the same result. So we take the absolute value.
+		// (https://www.microsoft.com/en-us/research/publication/division-and-modulus-for-computer-scientists/)
+		final var absDivisor = divisor.abs();
+
+		final var length = length();
+		if (length != null && absDivisor.mMaxValue != null && length.compareTo(absDivisor.mMaxValue) >= 0) {
+			// If length is greater than the largest possible divisor, the interval contains all possible mod values.
+			return new BigInterval(BigInteger.ZERO, absDivisor.mMaxValue.subtract(BigInteger.ONE));
+		}
+		if (length != null && length.compareTo(absDivisor.mMinValue) >= 0) {
+			// If the length is somewhere inside the interval of possible divisors, we split into two cases:
+			// all divisors up to length, and all greater divisors.
+			// For divisors up to length, we know (as in the previous case) that we can get all possible mod values (for
+			// the new sub-interval of divisors); for divisors greater than length, we use a recursive call.
+			// (NOTE that the recursion depth should be limited to 2, as length is outside the new sub-interval.)
+			final var lowerHalf = new BigInterval(BigInteger.ZERO, length.subtract(BigInteger.ONE));
+			final var upperHalf = euclideanModulo(new BigInterval(length.add(BigInteger.ONE), absDivisor.mMaxValue));
+			return lowerHalf.join(upperHalf);
+		}
+		if (absDivisor.mMinValue.compareTo(mMaxValue) > 0) {
+			// trivial case: modulo is guaranteed to have no effect
+			return this;
+		}
+		if (absDivisor.mMaxValue != null && absDivisor.mMaxValue.compareTo(mMaxValue) > 0) {
+			return new BigInterval(BigInteger.ZERO, mMaxValue);
+		}
+
+		// fallback to imprecise approximation
+		return new BigInterval(BigInteger.ZERO,
+				absDivisor.mMaxValue == null ? null : absDivisor.mMaxValue.subtract(BigInteger.ONE));
+	}
 }