Soundness holes: Tests and fixes

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/ErrorExceptionFlowUnsound.java

@@ -0,0 +1,23 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: exceptional control flow is not modeled. `1 / 0` throws at runtime, so the
+// assignment x = 1 after it never executes and x stays 0; but the verifier ignores the throw,
+// treats the try body as straight-line code, and ACCEPTS "_ == 1". Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorExceptionFlowUnsound {
+    public static void main(String[] args) {
+        int x = 0;
+        try {
+            int z = 1 / 0;
+            x = 1;
+        } catch (ArithmeticException ex) {
+            x = x;
+        }
+        @Refinement("_ == 1")
+        int y = x; // Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because y == 0
+        assert y == 1 : "y=" + y;
+    }
+}

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

@@ -0,0 +1,20 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: a field's refinement is assumed on read without proving it was ever
+// established. The field n defaults to 0, but the verifier trusts "@Refinement(_ > 0)" on the
+// field and ACCEPTS reading it into a "_ > 0" variable. At runtime n == 0. Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorFieldDefaultUnsound {
+    @Refinement("_ > 0")
+    int n;
+
+    public static void main(String[] args) {
+        ErrorFieldDefaultUnsound o = new ErrorFieldDefaultUnsound();
+        @Refinement("_ > 0")
+        int x = o.n; // Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because n defaults to 0
+        assert x > 0 : "x=" + x;
+    }
+}

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

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: `float` is modeled as 64-bit FP, not Java's 32-bit binary32. The float
+// literal 0.1f rounds to 0.100000001490116119... at runtime, which is not equal to 0.1, yet the
+// verifier ACCEPTS "_ == 0.1". Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorFloatPrecisionUnsound {
+    public static void main(String[] args) {
+        @Refinement("_ == 0.1")
+        float f = 0.1f; // Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because (float)0.1 != 0.1
+        assert f == 0.1 : "f=" + f;
+    }
+}

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

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: floating-point `%` is translated to the IEEE-754 remainder (mkFPRem),
+// but Java `%` is fmod (truncated remainder). 7.0 % 4.0 == 3.0 in Java; the IEEE remainder is
+// -1.0, so the verifier ACCEPTS "_ < 1.0". At runtime 3.0 < 1.0 is false. Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorFloatRemainderUnsound {
+    public static void main(String[] args) {
+        @Refinement("_ < 1.0")
+        double r = 7.0 % 4.0; // Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because r == 3.0
+        assert r < 1.0 : "r=" + r;
+    }
+}

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

@@ -0,0 +1,17 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: Java `int` is modeled as an unbounded Z3 integer, so 32-bit
+// two's-complement overflow is not modeled. 46341 * 46341 == 2147488281 mathematically,
+// but in Java `int` it wraps to -2147479015. The verifier currently ACCEPTS "_ > 0";
+// at runtime the value is negative, so the refinement is violated. Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorIntOverflowUnsound {
+    public static void main(String[] args) {
+        @Refinement("_ > 0")
+        int c = 46341 * 46341; // Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because c == -2147479015
+        assert c > 0 : "c=" + c;
+    }
+}

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

@@ -0,0 +1,20 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: Java `long` is modeled as a Z3 Real, so `/` becomes exact rational
+// division instead of truncating integer division. 7L / 2L == 3 in Java, but the verifier
+// models it as 3.5 and ACCEPTS "_ > 3". At runtime 3 > 3 is false. Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorLongAsRealDivisionUnsound {
+    public static void main(String[] args) {
+        @Refinement("c == 7")
+        long c = 7L;
+        @Refinement("d == 2")
+        long d = 2L;
+        @Refinement("_ > 3")
+        long e = c / d; // Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because e == 3
+        assert e > 3 : "e=" + e;
+    }
+}

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-example/src/main/java/testSuite/ErrorLoopSinglePassUnsound.java

@@ -0,0 +1,21 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: loop bodies are modeled as a single iteration (no loop invariant / no
+// havoc of mutated variables). The while loop runs until x == 2, so the real post-loop value is
+// 2, but the verifier models one pass and ACCEPTS "_ == 1". At runtime y == 1 is false.
+// Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorLoopSinglePassUnsound {
+    public static void main(String[] args) {
+        int x = 0;
+        while (x < 2) {
+            x = x + 1;
+        }
+        @Refinement("_ == 1")
+        int y = x; // Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because y == 2
+        assert y == 1 : "y=" + y;
+    }
+}

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

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: numeric narrowing casts are not modeled; the (int) cast of 1.9 is ignored
+// and the refinement is accepted vacuously. At runtime (int) 1.9 == 1, which does not satisfy
+// "_ == 1.9", yet the verifier currently ACCEPTS it. Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorNarrowingCastUnsound {
+    public static void main(String[] args) {
+        @Refinement("_ == 1.9")
+        int x = (int) 1.9; // Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because x == 1
+        assert x == 1.9 : "x=" + x;
+    }
+}

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

@@ -0,0 +1,18 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: integer `%` is translated to Z3's Euclidean modulo (result always >= 0),
+// but Java `%` takes the sign of the dividend. -7 % 3 == -1 in Java; the verifier models it as 2
+// and ACCEPTS "_ >= 0". At runtime -1 >= 0 is false. Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorNegativeModuloUnsound {
+    public static void main(String[] args) {
+        @Refinement("a == -7")
+        int a = -7;
+        @Refinement("_ >= 0")
+        int r = a % 3; // Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because r == -1
+        assert r >= 0 : "r=" + r;
+    }
+}

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

@@ -0,0 +1,18 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: assignments on a not-taken control-flow path are applied to the abstract
+// state. In `false && ((x = 1) == 1)` the right operand never executes (short-circuit), so x stays
+// 0 at runtime, but the verifier records x = 1 and ACCEPTS "_ == 1". Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorShortCircuitAssignUnsound {
+    public static void main(String[] args) {
+        int x = 0;
+        boolean b = false && ((x = 1) == 1);
+        @Refinement("_ == 1")
+        int y = x; // Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because y == 0
+        assert y == 1 : "y=" + y;
+    }
+}

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

@@ -0,0 +1,35 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// SOUNDNESS HOLE: typestate tracking is not robust to aliasing. `b = a` makes b and a the
+// same object; after a.close() the object is closed, but the state transition is recorded only on
+// variable a, so the verifier still believes b is open and ACCEPTS b.read(). Should be rejected.
+@StateSet({ "open", "closed" })
+public class ErrorTypestateAliasUnsound {
+    private boolean openFlag;
+
+    @StateRefinement(to = "open(this)")
+    public ErrorTypestateAliasUnsound() {
+        openFlag = true;
+    }
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {
+        openFlag = false;
+    }
+
+    @StateRefinement(from = "open(this)", to = "open(this)")
+    public void read() {
+        // the "open" precondition, checked at runtime: aborts under -ea when called on a closed object
+        assert openFlag : "read() called while closed";
+    }
+
+    public static void main(String[] args) {
+        ErrorTypestateAliasUnsound a = new ErrorTypestateAliasUnsound();
+        ErrorTypestateAliasUnsound b = a;
+        a.close();
+        b.read(); // State Refinement Error
+    }
+}