From 0df1a9c7404f4f18ce042427b3068cb060313b02 Mon Sep 17 00:00:00 2001
From: Aleksei Menshutin <a.menshutin@vkteam.ru>
Date: Fri, 16 Oct 2026 23:58:16 +0300
Subject: [PATCH] [JVM] Saturate FP casts at rounded integral upper bounds

---
 .../usvm/machine/operator/JcOperatorUtils.kt  |  4 +-
 .../FloatingPointIntegralBoundaries.java      | 27 +++++++++++
 .../FloatingPointIntegralBoundariesTest.kt    | 47 +++++++++++++++++++
 3 files changed, 77 insertions(+), 1 deletion(-)
 create mode 100644 usvm-jvm/src/samples/java/org/usvm/samples/primitives/FloatingPointIntegralBoundaries.java
 create mode 100644 usvm-jvm/src/test/kotlin/org/usvm/samples/primitives/FloatingPointIntegralBoundariesTest.kt

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/operator/JcOperatorUtils.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/operator/JcOperatorUtils.kt
index 18d480f65c..b3e7452aa9 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/operator/JcOperatorUtils.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/operator/JcOperatorUtils.kt
@@ -76,6 +76,8 @@ 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)
 
@@ -83,7 +85,7 @@ internal fun UExpr<UFpSort>.castToBv(sizeBits: Int): UExpr<UBvSort> =
             mkFpIsNaNExpr(this@castToBv),
             mkBv(0, sizeBits.toUInt()),
             mkIte(
-                mkFpLessExpr(fpBvMaxValue, this@castToBv),
+                mkFpLessOrEqualExpr(fpBvMaxValue, this@castToBv),
                 bvMaxValue,
                 mkIte(
                     mkFpLessExpr(this@castToBv, fpBvMinValue),
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/primitives/FloatingPointIntegralBoundaries.java b/usvm-jvm/src/samples/java/org/usvm/samples/primitives/FloatingPointIntegralBoundaries.java
new file mode 100644
index 0000000000..8fe751cf20
--- /dev/null
+++ b/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;
+    }
+}
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/primitives/FloatingPointIntegralBoundariesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/primitives/FloatingPointIntegralBoundariesTest.kt
new file mode 100644
index 0000000000..a60c519e77
--- /dev/null
+++ b/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 },
+        )
+    }
+}