[JVM] Saturate FP casts at rounded integral upper bounds

usvm-jvm/src/main/kotlin/org/usvm/machine/operator/JcOperatorUtils.kt

@@ -76,14 +76,16 @@ internal fun UExpr<UFpSort>.castToBv(sizeBits: Int): UExpr<UBvSort> =
     with(ctx) {
         val bvMaxValue = bvMaxValueSigned<KBvSort>(sizeBits.toUInt())
         val bvMinValue = bvMinValueSigned<KBvSort>(sizeBits.toUInt())
+        // A signed maximum may round up to the first out-of-range integer (for example, double 2^63).
+        // Clamp equality as well, before SMT fp.to_sbv becomes underspecified.
         val fpBvMaxValue = mkBvToFpExpr(sort, fpRoundingModeSortDefaultValue(), bvMaxValue, signed = true)
         val fpBvMinValue = mkBvToFpExpr(sort, fpRoundingModeSortDefaultValue(), bvMinValue, signed = true)
 
         mkIte(
             mkFpIsNaNExpr(this@castToBv),
             mkBv(0, sizeBits.toUInt()),
             mkIte(
-                mkFpLessExpr(fpBvMaxValue, this@castToBv),
+                mkFpLessOrEqualExpr(fpBvMaxValue, this@castToBv),
                 bvMaxValue,
                 mkIte(
                     mkFpLessExpr(this@castToBv, fpBvMinValue),

usvm-jvm/src/samples/java/org/usvm/samples/primitives/FloatingPointIntegralBoundaries.java

@@ -0,0 +1,27 @@
+package org.usvm.samples.primitives;
+
+public class FloatingPointIntegralBoundaries {
+    public static boolean doubleAtLongUpperBoundary(double value) {
+        if (value != 0x1.0p63) {
+            return false;
+        }
+
+        return (long) value == Long.MAX_VALUE;
+    }
+
+    public static boolean floatAtIntUpperBoundary(float value) {
+        if (value != 0x1.0p31f) {
+            return false;
+        }
+
+        return (int) value == Integer.MAX_VALUE;
+    }
+
+    public static boolean floatAtLongUpperBoundary(float value) {
+        if (value != 0x1.0p63f) {
+            return false;
+        }
+
+        return (long) value == Long.MAX_VALUE;
+    }
+}

usvm-jvm/src/test/kotlin/org/usvm/samples/primitives/FloatingPointIntegralBoundariesTest.kt

@@ -0,0 +1,47 @@
+package org.usvm.samples.primitives
+
+import org.junit.jupiter.api.Test
+import org.usvm.samples.JavaMethodTestRunner
+import org.usvm.test.util.checkers.eq
+
+class FloatingPointIntegralBoundariesTest : JavaMethodTestRunner() {
+    init {
+        options = options.copy(throwExceptionOnStepFailure = true)
+    }
+
+    @Test
+    fun `double at two to the power 63 saturates to long max`() {
+        val boundary = Math.scalb(1.0, 63)
+
+        checkDiscoveredProperties(
+            FloatingPointIntegralBoundaries::doubleAtLongUpperBoundary,
+            eq(count = 2),
+            { value, result -> value == boundary && result == true },
+            { value, result -> value != boundary && result == false },
+        )
+    }
+
+    @Test
+    fun `float at two to the power 31 saturates to int max`() {
+        val boundary = Math.scalb(1.0f, 31)
+
+        checkDiscoveredProperties(
+            FloatingPointIntegralBoundaries::floatAtIntUpperBoundary,
+            eq(count = 2),
+            { value, result -> value == boundary && result == true },
+            { value, result -> value != boundary && result == false },
+        )
+    }
+
+    @Test
+    fun `float at two to the power 63 saturates to long max`() {
+        val boundary = Math.scalb(1.0f, 63)
+
+        checkDiscoveredProperties(
+            FloatingPointIntegralBoundaries::floatAtLongUpperBoundary,
+            eq(count = 2),
+            { value, result -> value == boundary && result == true },
+            { value, result -> value != boundary && result == false },
+        )
+    }
+}