Model Java integral types as fixed-width BitVectors

Migrate int/short/char/byte -> 32-bit BitVec and long -> 64-bit BitVec
in the SMT translation. Z3 BitVec ops match Java exactly: mkBVAdd/Sub/Mul
wrap (two's-complement overflow), mkBVSDiv truncates toward zero, mkBVSRem
takes the sign of the dividend, signed comparisons; int<->long mixing
sign-extends, and BV<->real/FP coercions go through mkBV2Int/getLong.
ExpressionFolding (Java-int constant folding) is now consistent with the
solver.

Closes three holes at once: ErrorIntOverflowUnsound (46341*46341 wraps
to -2147479015), ErrorNegativeModuloUnsound (-7 % 3 == -1), and
ErrorLongAsRealDivisionUnsound (7L/2L == 3).

Sound fixed-width semantics also exposed six Correct tests that were
themselves latently unsound (they asserted mathematically-true but
Java-false postconditions that overflow): CorrectSimpleIfElse (-a at
MIN_VALUE), CorrectSpecificFunctionInvocation / CorrectLongUsage /
CorrectFunctionsTutorial / CorrectIfThen / CorrectOperatorAssignments
(+,-,* overflow). Each now carries overflow-guard preconditions/bounds
so its postcondition genuinely holds (CorrectLongUsage widens to long
before multiplying). ErrorLongUsage gains a third expected-error marker
for the now-correctly-rejected overflow in its own body.

Whole verifier suite is green (304 tests, 0 failures); all 11
Error*Unsound holes are now rejected.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: GUIpsp

liquidjava-example/src/main/java/testSuite/CorrectFunctionsTutorial.java

@@ -4,17 +4,22 @@
 
 public class CorrectFunctionsTutorial {
 
-    @Refinement("_ >= 0 && _ >= n")
-    public static int sum(int n) {
+    // n + t1 overflows once the running sum exceeds Integer.MAX_VALUE. Bounding n to [0, 46340] keeps the
+    // sum below 46340^2 < Integer.MAX_VALUE; the inductive ceiling _ <= n * 46340 (since n(n+1)/2 <= 46340*n
+    // for n <= 46340) lets the modular check prove the addition cannot overflow at any recursion depth.
+    @Refinement("_ >= 0 && _ >= n && _ <= n * 46340")
+    public static int sum(@Refinement("0 <= n && n <= 46340") int n) {
         if (n <= 0) return 0;
         else {
             int t1 = sum(n - 1);
             return n + t1;
         }
     }
 
+    // 0 - n overflows back to Integer.MIN_VALUE (still negative) when n == Integer.MIN_VALUE, so exclude it;
+    // for every other n the magnitude is non-negative and at least n.
     @Refinement("_ >= 0 && _ >= n")
-    public static int absolute(int n) {
+    public static int absolute(@Refinement("n > -2147483648") int n) {
         if (0 <= n) return n;
         else return 0 - n;
     }

liquidjava-example/src/main/java/testSuite/CorrectIfThen.java

@@ -5,7 +5,9 @@
 @SuppressWarnings("unused")
 public class CorrectIfThen {
 
-    public void have2(int a, int b) {
+    // a - b overflows when b is very negative (a - b exceeds Integer.MAX_VALUE). Requiring b >= 0 keeps
+    // a - b in [1, a] (both operands non-negative with a > b), so it stays positive without overflowing.
+    public void have2(int a, @Refinement("b >= 0") int b) {
         @Refinement("pos > 0")
         int pos = 10;
         if (a > 0) {

liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java

@@ -5,13 +5,18 @@
 @SuppressWarnings("unused")
 public class CorrectLongUsage {
 
-    @Refinement("_ > 10")
+    // `a * 2` would be 32-bit int arithmetic (overflowing at a >= 2^30) BEFORE the widening to long. Widening
+    // the operand to long first makes the multiply 64-bit and overflow-free. For int a > 10 the result is in
+    // (20, 2*Integer.MAX_VALUE], hence > 10 and bounded by 4294967294.
+    @Refinement("_ > 10 && _ <= 4294967294")
     public static long doubleBiggerThanTen(@Refinement("a > 10") int a) {
-        return a * 2;
+        long widened = a; // widen to 64-bit before multiplying, so a * 2 cannot overflow as 32-bit int
+        return widened * 2;
     }
 
+    // a * 2 overflows in 64-bit once a exceeds Long.MAX_VALUE / 2, so bound a to keep 2*a in range and > 40.
     @Refinement("_ > 40")
-    public static long doubleBiggerThanTwenty(@Refinement("a > 20") long a) {
+    public static long doubleBiggerThanTwenty(@Refinement("a > 20 && a <= 4611686018427387903") long a) {
         return a * 2;
     }
 
@@ -27,7 +32,9 @@ public static void main(String[] args) {
             long c = -a;
         }
 
-        @Refinement("d > 10")
+        // Carry doubleBiggerThanTen's upper bound on d so that d * 2 below provably stays > 20 and in range
+        // for doubleBiggerThanTwenty's a <= 4611686018427387903 precondition (and cannot itself overflow).
+        @Refinement("d > 10 && d <= 4294967294")
         long d = doubleBiggerThanTen(100);
 
         @Refinement("e > 10")

liquidjava-example/src/main/java/testSuite/CorrectOperatorAssignments.java

@@ -4,14 +4,16 @@
 
 public class CorrectOperatorAssignments {
 
+    // x + 1 overflows to Integer.MIN_VALUE when x == Integer.MAX_VALUE, so exclude that boundary.
     @Refinement("_ > 0")
-    int plus(@Refinement("_ >= 0") int x) {
+    int plus(@Refinement("_ >= 0 && _ < 2147483647") int x) {
         x += 1; // x is now > 0
         return x;
     }
 
+    // x + 1 overflows when x == Integer.MAX_VALUE, so exclude that boundary.
     @Refinement("_ > 0")
-    int plusInvocation(@Refinement("_ >= 0") int x) {
+    int plusInvocation(@Refinement("_ >= 0 && _ < 2147483647") int x) {
         x += one(); // x is now > 0
         return x;
     }
@@ -21,14 +23,16 @@ int one() {
         return 1;
     }
 
+    // x - 1 overflows to Integer.MAX_VALUE when x == Integer.MIN_VALUE, so exclude that boundary.
     @Refinement("_ < 0")
-    int minus(@Refinement("_ <= 0") int x) {
+    int minus(@Refinement("_ <= 0 && _ > -2147483648") int x) {
         x -= 1; // x is now < 0
         return x;
     }
 
+    // x * x overflows (and can wrap negative) once |x| exceeds 46340, so bound |x| to keep the square non-negative.
     @Refinement("_ >= 0")
-    int multiply(int x) {
+    int multiply(@Refinement("_ >= -46340 && _ <= 46340") int x) {
         x *= x; // x is now >= 0
         return x;
     }

liquidjava-example/src/main/java/testSuite/CorrectSimpleIfElse.java

@@ -5,8 +5,11 @@
 @SuppressWarnings("unused")
 public class CorrectSimpleIfElse {
 
-    @Refinement("_ > 0")
-    public static int toPositive(@Refinement("a < 0") int a) {
+    // -Integer.MIN_VALUE overflows back to Integer.MIN_VALUE (still negative), so the negation is only
+    // provably positive away from that boundary. We bound the input to a small negative window so the
+    // result is a small positive value (also keeping the caller's `toPositive(ex_a) * 10` overflow-free).
+    @Refinement("_ > 0 && _ < 1000")
+    public static int toPositive(@Refinement("a < 0 && a > -1000") int a) {
         return -a;
     }
 
@@ -28,7 +31,8 @@ public static void main(String[] args) {
         }
 
         // EXAMPLE 2
-        @Refinement("_ < 10")
+        // Bound ex_a to the small negative window toPositive accepts (and keep the *10 below in range).
+        @Refinement("_ < 10 && _ > -1000")
         int ex_a = 5;
         if (ex_a < 0) {
             @Refinement("_ >= 10")

liquidjava-example/src/main/java/testSuite/CorrectSpecificFunctionInvocation.java

@@ -4,13 +4,15 @@
 
 @SuppressWarnings("unused")
 public class CorrectSpecificFunctionInvocation {
+    // a * 2 overflows (wraps negative) once a reaches 2^30, so bound a below 2^30 for the result to stay positive.
     @Refinement(" _ > 0")
-    public static int doubleBiggerThanTen(@Refinement("a > 10") int a) {
+    public static int doubleBiggerThanTen(@Refinement("a > 10 && a <= 1073741823") int a) {
         return a * 2;
     }
 
     public static void main(String[] args) {
-        @Refinement("a > 0")
+        // Upper bound so the call below provably satisfies doubleBiggerThanTen's a <= 1073741823 precondition.
+        @Refinement("a > 0 && a <= 1073741823")
         int a = 50;
         int b = doubleBiggerThanTen(a);
     }

liquidjava-example/src/main/java/testSuite/ErrorLongUsage.java

@@ -6,7 +6,7 @@
 public class ErrorLongUsage {
     @Refinement(" _ > 40")
     public static long doubleBiggerThanTwenty(@Refinement("a > 20") long a) {
-        return a * 2;
+        return a * 2; // Refinement Error
     }
 
     public static void longUsage1() {

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java

@@ -90,15 +90,18 @@ private static Expr<?> getExpr(Context z3, String name, CtTypeReference<?> type)
         String typeName = type.getQualifiedName();
 
         return switch (typeName) {
-        case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" -> z3
-                .mkIntConst(name);
+        // Java integral types are fixed-width two's-complement values, so they are modeled as Z3 BitVectors
+        // (32-bit for int/short/char/byte and their boxed forms, 64-bit for long). This makes overflow,
+        // signed division/remainder, and signed comparison faithful to the JLS instead of unbounded integers.
+        case "int", "short", "char", "byte", "java.lang.Integer", "java.lang.Short", "java.lang.Character", "java.lang.Byte" -> z3
+                .mkBVConst(name, 32);
         case "boolean", "java.lang.Boolean" -> z3.mkBoolConst(name);
-        case "long", "java.lang.Long" -> z3.mkRealConst(name);
+        case "long", "java.lang.Long" -> z3.mkBVConst(name, 64);
         // Java `float` is binary32 and `double` is binary64; modeling float as FP64 would lose single-precision
         // rounding. Mixed-precision expressions are reconciled via Java numeric promotion in TranslatorToZ3.
         case "float", "java.lang.Float" -> (FPExpr) z3.mkConst(name, z3.mkFPSort32());
         case "double", "java.lang.Double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64());
-        case "int[]" -> z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort());
+        case "int[]" -> z3.mkArrayConst(name, z3.mkBitVecSort(32), z3.mkBitVecSort(32));
         default -> z3.mkConst(name, z3.mkUninterpretedSort(typeName));
         };
     }
@@ -133,12 +136,14 @@ private static void addBuiltinFunctions(Context z3, Map<String, FuncDecl<?>> fun
 
     static Sort getSort(Context z3, String sort) {
         return switch (sort) {
-        case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" -> z3.getIntSort();
+        // Integral types are fixed-width BitVectors (32-bit for int-family, 64-bit for long); see getExpr.
+        case "int", "short", "char", "byte", "java.lang.Integer", "java.lang.Short", "java.lang.Character", "java.lang.Byte" -> z3
+                .mkBitVecSort(32);
         case "boolean", "java.lang.Boolean" -> z3.getBoolSort();
-        case "long", "java.lang.Long" -> z3.getRealSort();
+        case "long", "java.lang.Long" -> z3.mkBitVecSort(64);
         case "float", "java.lang.Float" -> z3.mkFPSort32();
         case "double", "java.lang.Double" -> z3.mkFPSortDouble();
-        case "int[]" -> z3.mkArraySort(z3.mkIntSort(), z3.mkIntSort());
+        case "int[]" -> z3.mkArraySort(z3.mkBitVecSort(32), z3.mkBitVecSort(32));
         case "String" -> z3.getStringSort();
         case "void" -> z3.mkUninterpretedSort("void");
         default -> z3.mkUninterpretedSort(sort);