diff --git a/liquidjava-example/src/main/java/testSuite/CorrectFunctionsTutorial.java b/liquidjava-example/src/main/java/testSuite/CorrectFunctionsTutorial.java index 7afab4331..0cf38d10c 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectFunctionsTutorial.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectFunctionsTutorial.java @@ -4,8 +4,11 @@ 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); @@ -13,8 +16,10 @@ public static int sum(int n) { } } + // 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; } diff --git a/liquidjava-example/src/main/java/testSuite/CorrectIfThen.java b/liquidjava-example/src/main/java/testSuite/CorrectIfThen.java index 9e5ed0446..64232faa5 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectIfThen.java +++ b/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) { diff --git a/liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java b/liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java index b8ceddb74..0d56217a3 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java +++ b/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") diff --git a/liquidjava-example/src/main/java/testSuite/CorrectOperatorAssignments.java b/liquidjava-example/src/main/java/testSuite/CorrectOperatorAssignments.java index 6cd580aaa..24cee7eec 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectOperatorAssignments.java +++ b/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; } diff --git a/liquidjava-example/src/main/java/testSuite/CorrectSimpleIfElse.java b/liquidjava-example/src/main/java/testSuite/CorrectSimpleIfElse.java index cc93f1dfb..d6907785e 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectSimpleIfElse.java +++ b/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") diff --git a/liquidjava-example/src/main/java/testSuite/CorrectSpecificFunctionInvocation.java b/liquidjava-example/src/main/java/testSuite/CorrectSpecificFunctionInvocation.java index 0bfdb2919..15194431a 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectSpecificFunctionInvocation.java +++ b/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); } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExceptionFlowUnsound.java b/liquidjava-example/src/main/java/testSuite/ErrorExceptionFlowUnsound.java new file mode 100644 index 000000000..353605320 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFieldDefaultUnsound.java b/liquidjava-example/src/main/java/testSuite/ErrorFieldDefaultUnsound.java new file mode 100644 index 000000000..c0c404e33 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFloatPrecisionUnsound.java b/liquidjava-example/src/main/java/testSuite/ErrorFloatPrecisionUnsound.java new file mode 100644 index 000000000..f3c6433ee --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFloatRemainderUnsound.java b/liquidjava-example/src/main/java/testSuite/ErrorFloatRemainderUnsound.java new file mode 100644 index 000000000..ead599643 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIntOverflowUnsound.java b/liquidjava-example/src/main/java/testSuite/ErrorIntOverflowUnsound.java new file mode 100644 index 000000000..39d3ac959 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongAsRealDivisionUnsound.java b/liquidjava-example/src/main/java/testSuite/ErrorLongAsRealDivisionUnsound.java new file mode 100644 index 000000000..5d9a3c8f9 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage.java index 524a9a02a..9b97b321e 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage.java +++ b/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() { diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopSinglePassUnsound.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopSinglePassUnsound.java new file mode 100644 index 000000000..fb6915d41 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNarrowingCastUnsound.java b/liquidjava-example/src/main/java/testSuite/ErrorNarrowingCastUnsound.java new file mode 100644 index 000000000..2fc6365c6 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNegativeModuloUnsound.java b/liquidjava-example/src/main/java/testSuite/ErrorNegativeModuloUnsound.java new file mode 100644 index 000000000..84576314c --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorShortCircuitAssignUnsound.java b/liquidjava-example/src/main/java/testSuite/ErrorShortCircuitAssignUnsound.java new file mode 100644 index 000000000..ce74a9a68 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTypestateAliasUnsound.java b/liquidjava-example/src/main/java/testSuite/ErrorTypestateAliasUnsound.java new file mode 100644 index 000000000..aa0c9879d --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index 864d65924..b68c60477 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -15,6 +15,11 @@ public class Context { private Map> classStates; private List aliases; + // Typestate aliasing: tracks, per local variable name, the set of other variable names that may + // currently refer to the same (stateful) object because of a reference-copy assignment (`b = a`). + // Used so a state transition through one reference can invalidate the tracked state of the others. + private Map> objectAliases; + private int counter; private static Context instance; @@ -26,6 +31,7 @@ private Context() { ctxGlobalVars = new ArrayList<>(); aliases = new ArrayList<>(); + objectAliases = new HashMap<>(); ghosts = new ArrayList<>(); classStates = new HashMap<>(); counter = 0; @@ -47,6 +53,7 @@ public void reinitializeAllContext() { reinitializeContext(); ctxFunctions = new ArrayList<>(); aliases = new ArrayList<>(); + objectAliases = new HashMap<>(); ghosts = new ArrayList<>(); classStates = new HashMap<>(); counter = 0; @@ -363,6 +370,68 @@ public List getAliases() { return aliases; } + // ---------------------- Typestate object aliasing ---------------------- + + /** + * Records that {@code target} now refers to the same object as {@code source} (a reference-copy assignment + * {@code target = source}). The relation is symmetric and transitive: {@code target} joins {@code source}'s alias + * group, so every member of that group becomes a mutual alias of {@code target}. Any previous aliasing of + * {@code target} is dropped first, because the assignment makes {@code target} point at {@code source}'s object + * instead of whatever it referred to before. + * + * @param target + * the variable being assigned to + * @param source + * the variable whose object {@code target} now also refers to + */ + public void recordObjectAlias(String target, String source) { + if (target == null || source == null || target.equals(source)) + return; + clearObjectAliases(target); + Set group = new HashSet<>(); + group.add(source); + group.addAll(objectAliases.getOrDefault(source, Collections.emptySet())); + group.add(target); + // Everyone in the group (including target) shares the full group as their alias set. + for (String member : group) { + Set others = new HashSet<>(group); + others.remove(member); + objectAliases.put(member, others); + } + } + + /** + * Returns the set of other variable names that may currently refer to the same object as {@code name}. Never + * {@code null}. + */ + public Set getObjectAliases(String name) { + return objectAliases.getOrDefault(name, Collections.emptySet()); + } + + /** + * Removes {@code name} from its alias group entirely (and from every other member's view of it). Called when + * {@code name} stops being a trustworthy alias of its old object: it is reassigned to a fresh value, or its tracked + * state is invalidated (havoc). + * + * @param name + * the variable to detach from any alias group + */ + public void clearObjectAliases(String name) { + if (name == null) + return; + Set group = objectAliases.remove(name); + if (group == null) + return; + for (String member : group) { + Set others = objectAliases.get(member); + if (others != null) { + others.remove(name); + if (others.isEmpty()) + objectAliases.remove(member); + } + } + } + @Override public String toString() { StringBuilder sb = new StringBuilder(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 33b5198c8..1e633156c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -13,29 +13,39 @@ import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler; import liquidjava.rj_language.BuiltinFunctionPredicate; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Enum; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.GroupExpression; import liquidjava.utils.StaticConstants; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; +import liquidjava.utils.constants.Ops; import liquidjava.utils.constants.Types; import org.apache.commons.lang3.NotImplementedException; +import spoon.reflect.code.BinaryOperatorKind; import spoon.reflect.code.CtArrayRead; import spoon.reflect.code.CtArrayWrite; import spoon.reflect.code.CtAssignment; import spoon.reflect.code.CtBinaryOperator; import spoon.reflect.code.CtBlock; import spoon.reflect.code.CtBreak; +import spoon.reflect.code.CtCatch; import spoon.reflect.code.CtConditional; import spoon.reflect.code.CtContinue; import spoon.reflect.code.CtConstructorCall; +import spoon.reflect.code.CtDo; import spoon.reflect.code.CtExpression; import spoon.reflect.code.CtFieldRead; import spoon.reflect.code.CtFieldWrite; +import spoon.reflect.code.CtFor; +import spoon.reflect.code.CtForEach; import spoon.reflect.code.CtIf; import spoon.reflect.code.CtInvocation; import spoon.reflect.code.CtLiteral; import spoon.reflect.code.CtLocalVariable; +import spoon.reflect.code.CtLoop; import spoon.reflect.code.CtNewArray; import spoon.reflect.code.CtNewClass; import spoon.reflect.code.CtOperatorAssignment; @@ -43,14 +53,18 @@ import spoon.reflect.code.CtStatement; import spoon.reflect.code.CtThisAccess; import spoon.reflect.code.CtThrow; +import spoon.reflect.code.CtTry; import spoon.reflect.code.CtUnaryOperator; import spoon.reflect.code.CtVariableAccess; import spoon.reflect.code.CtVariableRead; +import spoon.reflect.code.CtVariableWrite; +import spoon.reflect.code.CtWhile; import spoon.reflect.declaration.*; import spoon.reflect.factory.Factory; import spoon.reflect.reference.CtFieldReference; import spoon.reflect.reference.CtTypeReference; import spoon.reflect.reference.CtVariableReference; +import spoon.reflect.visitor.filter.TypeFilter; import spoon.support.reflect.code.CtVariableWriteImpl; public class RefinementTypeChecker extends TypeChecker { @@ -147,9 +161,11 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) { if (refinementFound == null) { refinementFound = new Predicate(); } + refinementFound = applyNarrowingCast(e, refinementFound); context.addVarToContext(varName, localVariable.getType(), new Predicate(), e); checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, localVariable); AuxStateHandler.addStateRefinements(this, varName, e); + trackReferenceAliasing(varName, localVariable.getType(), e); } } @@ -211,6 +227,7 @@ private void visitAssignment(CtAssignment assignment) thr CtVariable varDecl = (CtVariable) var.getDeclaration(); String name = var.getSimpleName(); checkAssignment(name, varDecl.getType(), ex, assignment.getAssignment(), assignment, varDecl); + trackReferenceAliasing(name, varDecl.getType(), assignment.getAssignment()); } else if (ex instanceof CtFieldWrite fw) { CtFieldReference cr = fw.getVariable(); @@ -283,8 +300,20 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { } else if (context.hasVariable(String.format(Formats.THIS, fieldName))) { String thisName = String.format(Formats.THIS, fieldName); - fieldRead.putMetadata(Keys.REFINEMENT, - Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName))); + Predicate defaultValue = unestablishedExternalFieldDefault(fieldRead); + if (defaultValue != null) { + // SOUNDNESS: reading some other object's field (target is not `this`) only carries the field's + // declared refinement if that refinement was actually established. A field with no initializer + // holds its Java default value (0 / 0.0 / false) right after construction, which need not satisfy + // the declared refinement. Model the read as that default value instead of trusting the + // refinement, so e.g. `@Refinement("_ > 0") int x = o.n;` is correctly rejected when `n` has no + // initializer. Reads through `this` keep the in-class field invariant (handled below), and fields + // with an initializer keep their established refinement. + fieldRead.putMetadata(Keys.REFINEMENT, defaultValue); + } else { + fieldRead.putMetadata(Keys.REFINEMENT, + Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName))); + } } else if (fieldRead.getVariable().getSimpleName().equals("length")) { String targetName = fieldRead.getTarget().toString(); @@ -317,6 +346,58 @@ private boolean tryStaticFinalConstantRefinement(CtFieldRead fieldRead) { return true; } + /** + * When a refined instance field is read off another object (the read target is not {@code this}) and the field has + * no initializer establishing its refinement, the field still holds its Java default value right after + * construction. Returns {@code #wild == } for such reads (so the declared refinement is NOT + * assumed), or {@code null} when the current {@code this#field} behavior should be kept: reads through {@code this} + * (in-class invariant), fields that have an initializer, or types without a representable primitive default. + */ + private Predicate unestablishedExternalFieldDefault(CtFieldRead fieldRead) { + // Reads through `this` (implicit or explicit) keep the in-class field invariant. + if (fieldRead.getTarget() == null || fieldRead.getTarget() instanceof CtThisAccess) + return null; + + CtField field = fieldRead.getVariable().getDeclaration(); + // Without a resolvable declaration we cannot tell whether the field is established; stay conservative and + // keep the existing behavior rather than risk rejecting an established field. + if (field == null) + return null; + // A field with an initializer (or a non-null constant value) establishes its refinement; trust it. + if (field.getDefaultExpression() != null) + return null; + + String type = fieldRead.getType() != null ? fieldRead.getType().getSimpleName() : null; + Predicate defaultLiteral = defaultLiteralForType(type); + // Only primitives have a refinement-checkable default literal; for everything else (e.g. references that + // default to null), keep the existing behavior to avoid spurious errors. + if (defaultLiteral == null) + return null; + return Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), defaultLiteral); + } + + /** The Java default value, as a literal {@link Predicate}, for a primitive type name, or {@code null} otherwise. */ + private static Predicate defaultLiteralForType(String type) { + if (type == null) + return null; + switch (type) { + case Types.INT: + case Types.SHORT: + case Types.LONG: + return Predicate.createLit("0", type); + case Types.CHAR: + // The char default is ''; model it via its numeric code point 0. + return Predicate.createLit("0", Types.INT); + case Types.FLOAT: + case Types.DOUBLE: + return Predicate.createLit("0.0", type); + case Types.BOOLEAN: + return Predicate.createLit("false", Types.BOOLEAN); + default: + return null; + } + } + @Override public void visitCtVariableRead(CtVariableRead variableRead) { super.visitCtVariableRead(variableRead); @@ -335,6 +416,156 @@ public void visitCtVariableRead(CtVariableRead variableRead) { public void visitCtBinaryOperator(CtBinaryOperator operator) { super.visitCtBinaryOperator(operator); otc.getBinaryOpRefinements(operator); + forgetShortCircuitedAssignments(operator); + } + + /** + * The right operand of {@code &&}/{@code ||} runs only conditionally (it is short-circuited when the left operand + * is already {@code false} resp. {@code true}). Spoon visits children before this method, so any assignment in that + * operand (e.g. {@code false && ((x = 1) == 1)}) has already committed its value to the context as if it always + * executed. That is unsound: at runtime the assignment may never happen, so the post-operator value of every + * variable written there is uncertain. Havoc those variables (give them a fresh, unconstrained instance) so the + * verifier can no longer assume the assigned value survives the operator. + * + *

+ * This is conservative: when the left operand is statically true (resp. false) the right operand does execute, yet + * we still forget the value. Forgetting only ever weakens what is known, so it cannot accept an unsound program; it + * costs precision only for the rare idiom of relying on a value assigned inside a short-circuited operand. + */ + private void forgetShortCircuitedAssignments(CtBinaryOperator operator) { + BinaryOperatorKind kind = operator.getKind(); + if (kind != BinaryOperatorKind.AND && kind != BinaryOperatorKind.OR) + return; + + havocVariablesWrittenIn(operator.getRightHandOperand()); + } + + /** + * Havocs (see {@link #havocVariable}) every local or field variable that appears as a write target anywhere inside + * {@code scope}. {@link CtVariableWrite} covers plain assignments ({@code x = ...}), compound assignments + * ({@code x += ...}) and the operand of pre/post increment/decrement ({@code x++}, {@code --x}), and its subtype + * {@link CtFieldWrite} covers field writes. + */ + private void havocVariablesWrittenIn(CtElement scope) { + if (scope == null) + return; + for (CtVariableWrite write : scope.getElements(new TypeFilter<>(CtVariableWrite.class))) { + CtVariableReference ref = write.getVariable(); + if (ref == null) + continue; + String name = (write instanceof CtFieldWrite) ? String.format(Formats.THIS, ref.getSimpleName()) + : ref.getSimpleName(); + havocVariable(name, write); + } + } + + /** + * Drops everything currently known about {@code name} by installing a fresh, unconstrained instance as its latest + * value. Subsequent reads resolve to this instance and therefore carry no refinement. + */ + private void havocVariable(String name, CtElement element) { + havocVariableState(name, element); + } + + /** + * Maintains the typestate alias registry across a reference assignment {@code target = rhs}. + * + *

+ * When {@code rhs} is a bare read of another local variable (a reference-copy such as {@code X b = a;}), {@code b} + * and {@code a} thereafter refer to the same object, so they are recorded as aliases. A later state transition + * through either one then invalidates the other (see {@link #havocObjectAliasesOf}). For any other right-hand side + * (a {@code new}, a method call, a field read, a literal, ...) {@code target} refers to a fresh or independent + * value, so it is detached from any alias group it was previously in. + * + *

+ * Primitive-typed targets are ignored: primitives cannot be stateful objects, so they can never participate in a + * typestate transition. This keeps the registry to the only case that matters (object references) and leaves + * single-reference usage completely unaffected. + */ + private void trackReferenceAliasing(String target, CtTypeReference targetType, CtExpression rhs) { + if (target == null || targetType == null || targetType.isPrimitive()) { + return; + } + // A bare local-variable read on the RHS (not a field read, which is a sibling type in Spoon) is the + // reference-copy that creates aliasing. + if (rhs instanceof CtVariableRead read && !(rhs instanceof CtFieldRead)) { + CtVariableReference srcRef = read.getVariable(); + String source = (srcRef != null) ? srcRef.getSimpleName() : null; + RefinedVariable srcVar = (source != null) ? context.getVariableByName(source) : null; + if (srcVar instanceof Variable) { + context.recordObjectAlias(target, source); + return; + } + } + // Reassignment to a fresh/independent object: target no longer aliases its old object. + context.clearObjectAliases(target); + } + + // ############################### Loops ########################################## + + /* + * Loop bodies are visited a single time by the underlying CtScanner, which models exactly one iteration and then + * commits the body's assignments as if that were the loop's post-state. That is unsound: a variable mutated in the + * loop keeps a value computed for one pass, but at runtime the loop may iterate zero or many times, so its + * post-loop value is unknown. After visiting each loop we therefore havoc (give a fresh, unconstrained instance to) + * every variable written in the body and in the for-update, so nothing assumed about its in-loop value survives the + * loop. Forgetting only weakens what is known, so it can never accept an unsound program; it costs precision only + * for code that relies on a specific value established by the loop. visitCt*Loop still calls super first so that + * any refinement/typestate error inside the body is still reported, exactly as before. + */ + + @Override + public void visitCtWhile(CtWhile whileLoop) { + super.visitCtWhile(whileLoop); + havocLoopVariables(whileLoop); + } + + @Override + public void visitCtDo(CtDo doLoop) { + super.visitCtDo(doLoop); + havocLoopVariables(doLoop); + } + + @Override + public void visitCtFor(CtFor forLoop) { + super.visitCtFor(forLoop); + havocLoopVariables(forLoop); + havocVariablesWrittenIn(forLoop.getExpression()); + for (CtStatement update : forLoop.getForUpdate()) + havocVariablesWrittenIn(update); + } + + @Override + public void visitCtForEach(CtForEach foreach) { + super.visitCtForEach(foreach); + havocLoopVariables(foreach); + } + + private void havocLoopVariables(CtLoop loop) { + havocVariablesWrittenIn(loop.getBody()); + } + + // ############################### Try/Catch ###################################### + + /* + * A try body is visited as straight-line code, so the underlying CtScanner commits every assignment in it as if the + * body ran to completion. That is unsound: an exception can interrupt the try at any point, so a statement after a + * throwing one may never execute and a variable assigned there may not hold that value once control leaves the try. + * The same holds inside each catch block, whose statements run only on the (uncertain) exceptional path. After + * visiting the try (so any refinement/typestate error inside the body or handlers is still reported, exactly as + * before), we therefore havoc (give a fresh, unconstrained instance to) every variable written in the try body and + * in each catch block, so nothing assumed about an in-try/in-catch value survives the statement. Forgetting only + * weakens what is known, so it can never accept an unsound program; it costs precision only for code that relies on + * a value established inside the try/catch. (A finally block always runs to completion, so its definite assignments + * could remain trusted; we keep the minimal sound option and do not special-case it.) + */ + + @Override + public void visitCtTry(CtTry tryBlock) { + super.visitCtTry(tryBlock); + havocVariablesWrittenIn(tryBlock.getBody()); + for (CtCatch catchBlock : tryBlock.getCatchers()) + havocVariablesWrittenIn(catchBlock.getBody()); } @Override @@ -538,7 +769,7 @@ private Predicate getAssignmentRefinement(String name, CtExpression assignmen if (parentElem instanceof CtOperatorAssignment operatorAssignment) { return otc.getOperatorAssignmentRefinement(name, operatorAssignment); } - return getRefinement(assignment); + return applyNarrowingCast(assignment, getRefinement(assignment)); } private Predicate getExpressionRefinements(CtExpression element) throws LJError { @@ -597,4 +828,61 @@ private void getPutVariableMetadata(CtElement elem, String name) { } elem.putMetadata(Keys.REFINEMENT, cref); } + + // ############################### Numeric Casts ########################################## + + /** + * Models a Java floating-point-to-integral narrowing cast on the value of {@code ex} (e.g. {@code (int) 1.9}, which + * is {@code 1} at runtime), so the refinement describes the truncated value rather than the original floating one. + * + *

+ * SOUNDNESS: without this, the cast is dropped and the value keeps its wide floating form, so a refinement like + * {@code _ == 1.9} on {@code (int) 1.9} is accepted even though the runtime value is {@code 1}. We rewrite the + * value-defining refinement {@code _ == E} into {@code _ == trunc(E)}, where {@code trunc} truncates toward zero + * (JLS §5.1.3). Only floating-to-integral casts change the value here, so casts that leave the value unchanged (an + * {@code int}-to-{@code int} cast such as {@code (int) one()}, or a widening cast such as {@code (float) 5L}) are + * left untouched and stay precise. + */ + private Predicate applyNarrowingCast(CtExpression ex, Predicate refinement) { + if (ex == null || refinement == null || !isFloatingToIntegralCast(ex)) + return refinement; + Optional value = wildcardEqualityValue(refinement); + if (value.isEmpty()) + return refinement; + Predicate truncated = Predicate.createInvocation(Keys.TRUNCATE, new Predicate(value.get())); + return Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), truncated); + } + + /** + * True when the outermost type cast on {@code ex} narrows a floating-point value to an integral one. The casts are + * ordered outermost-first by Spoon, and {@code ex.getType()} is the type of the operand before any cast is applied. + */ + private boolean isFloatingToIntegralCast(CtExpression ex) { + List> casts = ex.getTypeCasts(); + if (casts == null || casts.isEmpty()) + return false; + CtTypeReference operandType = ex.getType(); + return operandType != null && isFloatingType(operandType.getSimpleName()) + && isIntegralType(casts.get(0).getSimpleName()); + } + + private static boolean isFloatingType(String type) { + return Types.FLOAT.equals(type) || Types.DOUBLE.equals(type); + } + + private static boolean isIntegralType(String type) { + return Types.INT.equals(type) || Types.LONG.equals(type) || Types.SHORT.equals(type) || Types.CHAR.equals(type) + || "byte".equals(type); + } + + /** If {@code refinement} has the value-defining shape {@code _ == E} (possibly grouped), returns {@code E}. */ + private static Optional wildcardEqualityValue(Predicate refinement) { + Expression e = refinement.getExpression(); + while (e instanceof GroupExpression ge) + e = ge.getExpression(); + if (e instanceof BinaryExpression be && Ops.EQ.equals(be.getOperator()) + && Keys.WILDCARD.equals(be.getFirstOperand().toString())) + return Optional.of(be.getSecondOperand()); + return Optional.empty(); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 4935b4579..3ff9b4142 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -14,6 +14,7 @@ import liquidjava.processor.context.GhostFunction; import liquidjava.processor.context.GhostState; import liquidjava.processor.context.RefinedVariable; +import liquidjava.processor.context.Variable; import liquidjava.processor.facade.AliasDTO; import liquidjava.processor.facade.GhostDTO; import liquidjava.rj_language.Predicate; @@ -375,6 +376,46 @@ public void checkSMT(Predicate expectedType, CtElement element, String customMes element.putMetadata(Keys.REFINEMENT, expectedType); } + /** + * Drops everything currently known about {@code name} by installing a fresh, unconstrained instance as its latest + * value, and detaches it from any typestate alias group. Subsequent reads resolve to this instance and therefore + * carry no refinement, so no stale state (typestate or otherwise) can be assumed about it. + * + * @param name + * the variable to havoc + * @param element + * the program element to attribute the fresh instance to + */ + public void havocVariableState(String name, CtElement element) { + RefinedVariable rv = context.getVariableByName(name); + if (!(rv instanceof Variable)) + return; + String freshName = String.format(Formats.INSTANCE, name, context.getCounter()); + context.addInstanceToContext(freshName, rv.getType(), new Predicate(), element); + context.addRefinementInstanceToVariable(name, freshName); + context.addRefinementToVariableInContext(name, rv.getType(), new Predicate(), element); + context.clearObjectAliases(name); + } + + /** + * Invalidates (havocs) the tracked state of every variable that may alias {@code name}, leaving {@code name} itself + * untouched. Used after a typestate transition through {@code name}: any other reference to the same object would + * otherwise keep its now-stale state. Conservative and sound — havoc only ever weakens what is known. + * + * @param name + * the variable through which a state transition just occurred + * @param element + * the program element to attribute the fresh instances to + */ + public void havocObjectAliasesOf(String name, CtElement element) { + if (name == null) + return; + // Snapshot first: havocVariableState mutates the alias registry as it detaches each variable. + for (String alias : new java.util.ArrayList<>(context.getObjectAliases(name))) { + havocVariableState(alias, element); + } + } + public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo) throws LJError { vcChecker.processSubtyping(prevState, expectedState, context.getGhostStates(), target, factory); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index c4da97d87..dd6058a6d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -505,6 +505,9 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List new LiteralBoolean(value); case Types.INT, Types.SHORT -> new LiteralInt(value); case Types.LONG -> new LiteralLong(value); - case Types.DOUBLE, Types.FLOAT -> new LiteralReal(value); + case Types.DOUBLE -> new LiteralReal(value); + case Types.FLOAT -> new LiteralReal(value, true); case Types.CHAR -> new LiteralChar(value); default -> throw new IllegalArgumentException("Unsupported literal type: " + type); }; diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java index b21f1cf27..5711667f7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java @@ -8,13 +8,29 @@ public class LiteralReal extends Expression { private final double value; + /** + * True when this literal originates from a Java {@code float} (binary32) rather than a {@code double} (binary64). + * The stored {@link #value} keeps the full double for display/folding; the SMT translator rounds it to single + * precision so single-precision rounding is not silently lost. + */ + private final boolean isFloat; public LiteralReal(double v) { + this(v, false); + } + + public LiteralReal(double v, boolean isFloat) { value = v; + this.isFloat = isFloat; } public LiteralReal(String v) { + this(v, false); + } + + public LiteralReal(String v, boolean isFloat) { value = Double.parseDouble(v); + this.isFloat = isFloat; } @Override @@ -30,6 +46,10 @@ public double getValue() { return value; } + public boolean isFloat() { + return isFloat; + } + @Override public void getVariableNames(List toAdd) { // end leaf @@ -42,7 +62,7 @@ public void getStateInvocations(List toAdd, List all) { @Override public Expression clone() { - return new LiteralReal(value); + return new LiteralReal(value, isFloat); } @Override @@ -55,6 +75,7 @@ public int hashCode() { final int prime = 31; int result = 1; result = prime * result + Double.hashCode(value); + result = prime * result + Boolean.hashCode(isFloat); return result; } @@ -67,6 +88,6 @@ public boolean equals(Object obj) { if (getClass() != obj.getClass()) return false; LiteralReal other = (LiteralReal) obj; - return Double.doubleToLongBits(value) == Double.doubleToLongBits(other.value); + return Double.doubleToLongBits(value) == Double.doubleToLongBits(other.value) && isFloat == other.isFloat; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java index 464cd9898..78fb99684 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -105,6 +105,8 @@ public Expr visitLiteralChar(LiteralChar lit) { @Override public Expr visitLiteralReal(LiteralReal lit) { + if (lit.isFloat()) + return ctx.makeFloatLiteral((float) lit.getValue()); return ctx.makeDoubleLiteral(lit.getValue()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index 235cb170e..0719ad479 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -90,12 +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 "float", "double", "java.lang.Float", "java.lang.Double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64()); - case "int[]" -> z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort()); + 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.mkBitVecSort(32), z3.mkBitVecSort(32)); default -> z3.mkConst(name, z3.mkUninterpretedSort(typeName)); }; } @@ -130,12 +136,14 @@ private static void addBuiltinFunctions(Context z3, Map> 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); diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index cf568927a..6a4bf5835 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -2,10 +2,14 @@ import com.microsoft.z3.ArithExpr; import com.microsoft.z3.ArrayExpr; +import com.microsoft.z3.BitVecExpr; +import com.microsoft.z3.BitVecNum; +import com.microsoft.z3.BitVecSort; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.EnumSort; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; +import com.microsoft.z3.FPSort; import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntExpr; import com.microsoft.z3.IntNum; @@ -100,17 +104,28 @@ public Counterexample getCounterexample(Model model) { // #####################Literals and Variables##################### public Expr makeIntegerLiteral(int value) { - return z3.mkInt(value); + // Java int/short/char/byte literals are 32-bit two's-complement values. + return z3.mkBV(value, 32); } public Expr makeLongLiteral(long value) { - return z3.mkReal(value); + // Java long literals are 64-bit two's-complement values. + return z3.mkBV(value, 64); } public Expr makeDoubleLiteral(double value) { return z3.mkFP(value, z3.mkFPSort64()); } + /** + * Java {@code float} literals are single-precision (binary32). The caller has already rounded the value to a + * {@code float}, so emitting it into an {@link com.microsoft.z3.Context#mkFPSort32() FPSort32} constant preserves + * the single-precision rounding that a binary64 model would silently lose. + */ + public Expr makeFloatLiteral(float value) { + return z3.mkFP(value, z3.mkFPSort32()); + } + public Expr makeString(String s) { return z3.mkString(s); } @@ -164,6 +179,8 @@ public Expr makeFunctionInvocation(String name, Expr[] params) throws LJEr return makeStore(params); if (name.equals("getFromIndex")) return makeSelect(params); + if (name.equals(Keys.TRUNCATE)) + return makeTruncateToZero(params[0]); FuncDecl fd = funcTranslation.get(name); if (fd == null) fd = resolveFunctionDecl(name, params); @@ -233,17 +250,31 @@ private Expr makeStore(Expr[] params) { // #####################Boolean Operations##################### public Expr makeEquals(Expr e1, Expr e2) { - if (e1 instanceof FPExpr || e2 instanceof FPExpr) - return z3.mkFPEq(toFP(e1), toFP(e2)); + if (e1 instanceof FPExpr || e2 instanceof FPExpr) { + FPSort s = commonFPSort(e1, e2); + return z3.mkFPEq(toFP(e1, s), toFP(e2, s)); + } + if (bothBitVec(e1, e2)) { + BitVecExpr[] u = unifyBV(e1, e2); + return z3.mkEq(u[0], u[1]); + } if (e1 instanceof RealExpr || e2 instanceof RealExpr) return z3.mkEq(toReal(e1), toReal(e2)); + // Booleans, enums, strings, and ill-typed comparisons (e.g. a boolean against an integral literal) fall + // here; mkEq surfaces a proper sort-mismatch error rather than silently coercing. return z3.mkEq(e1, e2); } @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeLt(Expr e1, Expr e2) { - if (e1 instanceof FPExpr || e2 instanceof FPExpr) - return z3.mkFPLt(toFP(e1), toFP(e2)); + if (e1 instanceof FPExpr || e2 instanceof FPExpr) { + FPSort s = commonFPSort(e1, e2); + return z3.mkFPLt(toFP(e1, s), toFP(e2, s)); + } + if (bothBitVec(e1, e2)) { + BitVecExpr[] u = unifyBV(e1, e2); + return z3.mkBVSLT(u[0], u[1]); + } if (e1 instanceof RealExpr || e2 instanceof RealExpr) return z3.mkLt(toReal(e1), toReal(e2)); return z3.mkLt((ArithExpr) e1, (ArithExpr) e2); @@ -251,8 +282,14 @@ public Expr makeLt(Expr e1, Expr e2) { @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeLtEq(Expr e1, Expr e2) { - if (e1 instanceof FPExpr || e2 instanceof FPExpr) - return z3.mkFPLEq(toFP(e1), toFP(e2)); + if (e1 instanceof FPExpr || e2 instanceof FPExpr) { + FPSort s = commonFPSort(e1, e2); + return z3.mkFPLEq(toFP(e1, s), toFP(e2, s)); + } + if (bothBitVec(e1, e2)) { + BitVecExpr[] u = unifyBV(e1, e2); + return z3.mkBVSLE(u[0], u[1]); + } if (e1 instanceof RealExpr || e2 instanceof RealExpr) return z3.mkLe(toReal(e1), toReal(e2)); return z3.mkLe((ArithExpr) e1, (ArithExpr) e2); @@ -260,8 +297,14 @@ public Expr makeLtEq(Expr e1, Expr e2) { @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeGt(Expr e1, Expr e2) { - if (e1 instanceof FPExpr || e2 instanceof FPExpr) - return z3.mkFPGt(toFP(e1), toFP(e2)); + if (e1 instanceof FPExpr || e2 instanceof FPExpr) { + FPSort s = commonFPSort(e1, e2); + return z3.mkFPGt(toFP(e1, s), toFP(e2, s)); + } + if (bothBitVec(e1, e2)) { + BitVecExpr[] u = unifyBV(e1, e2); + return z3.mkBVSGT(u[0], u[1]); + } if (e1 instanceof RealExpr || e2 instanceof RealExpr) return z3.mkGt(toReal(e1), toReal(e2)); return z3.mkGt((ArithExpr) e1, (ArithExpr) e2); @@ -269,8 +312,14 @@ public Expr makeGt(Expr e1, Expr e2) { @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeGtEq(Expr e1, Expr e2) { - if (e1 instanceof FPExpr || e2 instanceof FPExpr) - return z3.mkFPGEq(toFP(e1), toFP(e2)); + if (e1 instanceof FPExpr || e2 instanceof FPExpr) { + FPSort s = commonFPSort(e1, e2); + return z3.mkFPGEq(toFP(e1, s), toFP(e2, s)); + } + if (bothBitVec(e1, e2)) { + BitVecExpr[] u = unifyBV(e1, e2); + return z3.mkBVSGE(u[0], u[1]); + } if (e1 instanceof RealExpr || e2 instanceof RealExpr) return z3.mkGe(toReal(e1), toReal(e2)); return z3.mkGe((ArithExpr) e1, (ArithExpr) e2); @@ -301,14 +350,23 @@ public Expr makeOr(Expr eval, Expr eval2) { public Expr makeMinus(Expr eval) { if (eval instanceof FPExpr) return z3.mkFPNeg((FPExpr) eval); + if (eval instanceof BitVecExpr bv) + // Two's-complement negation: wraps like Java unary minus (e.g. -Integer.MIN_VALUE == Integer.MIN_VALUE). + return z3.mkBVNeg(bv); return z3.mkUnaryMinus((ArithExpr) eval); } // #####################Arithmetic Operations##################### @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeAdd(Expr eval, Expr eval2) { - if (eval instanceof FPExpr || eval2 instanceof FPExpr) - return z3.mkFPAdd(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2)); + if (eval instanceof FPExpr || eval2 instanceof FPExpr) { + FPSort s = commonFPSort(eval, eval2); + return z3.mkFPAdd(z3.mkFPRoundNearestTiesToEven(), toFP(eval, s), toFP(eval2, s)); + } + if (bothBitVec(eval, eval2)) { + BitVecExpr[] u = unifyBV(eval, eval2); + return z3.mkBVAdd(u[0], u[1]); // wraps on overflow, exactly like Java + + } if (eval instanceof RealExpr || eval2 instanceof RealExpr) return z3.mkAdd(toReal(eval), toReal(eval2)); return z3.mkAdd((ArithExpr) eval, (ArithExpr) eval2); @@ -316,8 +374,14 @@ public Expr makeAdd(Expr eval, Expr eval2) { @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeSub(Expr eval, Expr eval2) { - if (eval instanceof FPExpr || eval2 instanceof FPExpr) - return z3.mkFPSub(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2)); + if (eval instanceof FPExpr || eval2 instanceof FPExpr) { + FPSort s = commonFPSort(eval, eval2); + return z3.mkFPSub(z3.mkFPRoundNearestTiesToEven(), toFP(eval, s), toFP(eval2, s)); + } + if (bothBitVec(eval, eval2)) { + BitVecExpr[] u = unifyBV(eval, eval2); + return z3.mkBVSub(u[0], u[1]); // wraps on overflow, exactly like Java - + } if (eval instanceof RealExpr || eval2 instanceof RealExpr) return z3.mkSub(toReal(eval), toReal(eval2)); return z3.mkSub((ArithExpr) eval, (ArithExpr) eval2); @@ -325,8 +389,14 @@ public Expr makeSub(Expr eval, Expr eval2) { @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeMul(Expr eval, Expr eval2) { - if (eval instanceof FPExpr || eval2 instanceof FPExpr) - return z3.mkFPMul(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2)); + if (eval instanceof FPExpr || eval2 instanceof FPExpr) { + FPSort s = commonFPSort(eval, eval2); + return z3.mkFPMul(z3.mkFPRoundNearestTiesToEven(), toFP(eval, s), toFP(eval2, s)); + } + if (bothBitVec(eval, eval2)) { + BitVecExpr[] u = unifyBV(eval, eval2); + return z3.mkBVMul(u[0], u[1]); // low-order bits wrap, exactly like Java * + } if (eval instanceof RealExpr || eval2 instanceof RealExpr) return z3.mkMul(toReal(eval), toReal(eval2)); return z3.mkMul((ArithExpr) eval, (ArithExpr) eval2); @@ -334,16 +404,36 @@ public Expr makeMul(Expr eval, Expr eval2) { @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeDiv(Expr eval, Expr eval2) { - if (eval instanceof FPExpr || eval2 instanceof FPExpr) - return z3.mkFPDiv(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2)); + if (eval instanceof FPExpr || eval2 instanceof FPExpr) { + FPSort s = commonFPSort(eval, eval2); + return z3.mkFPDiv(z3.mkFPRoundNearestTiesToEven(), toFP(eval, s), toFP(eval2, s)); + } + if (bothBitVec(eval, eval2)) { + BitVecExpr[] u = unifyBV(eval, eval2); + return z3.mkBVSDiv(u[0], u[1]); // signed division truncates toward zero, like Java / + } if (eval instanceof RealExpr || eval2 instanceof RealExpr) return z3.mkDiv(toReal(eval), toReal(eval2)); return z3.mkDiv((ArithExpr) eval, (ArithExpr) eval2); } public Expr makeMod(Expr eval, Expr eval2) { - if (eval instanceof FPExpr || eval2 instanceof FPExpr) - return z3.mkFPRem(toFP(eval), toFP(eval2)); + if (eval instanceof FPExpr || eval2 instanceof FPExpr) { + // Java `%` on floating point is fmod (truncated remainder, sign of dividend), NOT the + // IEEE-754 remainder (mkFPRem, which rounds the quotient to nearest). Encode fmod as + // r = a - b * trunc(a / b), where trunc rounds the quotient toward zero. + FPSort s = commonFPSort(eval, eval2); + FPExpr a = toFP(eval, s); + FPExpr b = toFP(eval2, s); + FPExpr q = z3.mkFPRoundToIntegral(z3.mkFPRoundTowardZero(), z3.mkFPDiv(z3.mkFPRoundTowardZero(), a, b)); + return z3.mkFPSub(z3.mkFPRoundNearestTiesToEven(), a, z3.mkFPMul(z3.mkFPRoundNearestTiesToEven(), b, q)); + } + if (bothBitVec(eval, eval2)) { + BitVecExpr[] u = unifyBV(eval, eval2); + // Java `%` takes the sign of the dividend; mkBVSRem is the signed remainder (sign of dividend), + // unlike mkBVSMod (sign of divisor) or Z3's Euclidean mkMod (always non-negative). + return z3.mkBVSRem(u[0], u[1]); + } if (eval instanceof RealExpr || eval2 instanceof RealExpr) return z3.mkMod(toInt(eval), toInt(eval2)); return z3.mkMod((IntExpr) eval, (IntExpr) eval2); @@ -354,6 +444,8 @@ private RealExpr toReal(Expr e) { return (RealExpr) e; if (e instanceof IntExpr) return z3.mkInt2Real((IntExpr) e); + if (e instanceof BitVecExpr bv) + return z3.mkInt2Real(z3.mkBV2Int(bv, true)); // signed BV -> int -> real throw new NotImplementedException(); } @@ -362,20 +454,141 @@ private IntExpr toInt(Expr e) { return (IntExpr) e; if (e instanceof RealExpr) return z3.mkReal2Int((RealExpr) e); + if (e instanceof BitVecExpr bv) + return z3.mkBV2Int(bv, true); // interpret the BitVector as a signed integer + throw new NotImplementedException(); + } + + /** + * Width in bits of a BitVector expression's sort. + */ + private int bvWidth(BitVecExpr e) { + return ((BitVecSort) e.getSort()).getSize(); + } + + /** + * Coerces a BitVector to {@code width} bits, mirroring Java integral conversions: widening sign-extends (Java + * widens {@code int} to {@code long} preserving sign, JLS §5.1.2) and narrowing keeps the low-order bits + * ({@code mkExtract} = Java narrowing primitive conversion, JLS §5.1.3). Same width is returned unchanged. + */ + private BitVecExpr toBV(BitVecExpr e, int width) { + int w = bvWidth(e); + if (w == width) + return e; + if (w < width) + return z3.mkSignExt(width - w, e); + return z3.mkExtract(width - 1, 0, e); + } + + /** + * Brings two operands to a common BitVector width before a binary operation, mirroring Java binary numeric + * promotion (JLS §5.6.2): if either operand is a {@code long} (64-bit) both become 64-bit, otherwise both stay + * 32-bit. A non-BitVector operand (e.g. an {@code IntExpr} literal that surfaced from a constant fold) is first + * converted to a BitVector. At least one operand is a {@link BitVecExpr} when this is called. + */ + private BitVecExpr[] unifyBV(Expr e1, Expr e2) { + BitVecExpr b1 = asBV(e1); + BitVecExpr b2 = asBV(e2); + int width = Math.max(bvWidth(b1), bvWidth(b2)); + return new BitVecExpr[] { toBV(b1, width), toBV(b2, width) }; + } + + /** + * Interprets {@code e} as a BitVector. BitVectors are returned as-is; an integer (which can appear if a fold + * produced a plain {@link IntExpr}) is reduced into a 32-bit BitVector via {@code mkInt2BV}. + */ + private BitVecExpr asBV(Expr e) { + if (e instanceof BitVecExpr bv) + return bv; + if (e instanceof IntExpr ie) + return z3.mkInt2BV(32, ie); + throw new NotImplementedException("Cannot interpret " + e.getSort() + " as a BitVector"); + } + + /** + * True when both operands can take the BitVector arithmetic/comparison path: at least one is a {@link BitVecExpr} + * (an actual integral value) and neither is a non-integral sort. A non-integral operand (boolean, enum, string, + * uninterpreted) makes this false so the caller falls through to the generic path, where Z3 raises a proper + * sort-mismatch error instead of this method silently coercing an ill-typed comparison. + */ + private boolean bothBitVec(Expr e1, Expr e2) { + return (e1 instanceof BitVecExpr || e2 instanceof BitVecExpr) && isBVCompatible(e1) && isBVCompatible(e2); + } + + private boolean isBVCompatible(Expr e) { + return e instanceof BitVecExpr || e instanceof IntExpr; + } + + /** + * Models a Java floating-point-to-integral narrowing cast, e.g. {@code (int) d}: the operand is rounded toward zero + * to a whole number (JLS §5.1.3 truncation). Returns an {@link IntExpr} so the cast result compares as an integer. + * + *

+ * For a floating-point operand the value is first rounded toward zero to an integral FP, converted to a real, then + * to an int (the real is whole, so {@code mkReal2Int}'s floor is exact). A real operand is truncated toward zero by + * flooring its magnitude and restoring the sign (plain {@code mkReal2Int} would floor toward negative infinity, + * which is wrong for negatives). An integer (already-integral BitVector) operand is returned unchanged. The result + * is a 32-bit BitVector so it compares directly against the integral cast target. + */ + @SuppressWarnings({ "unchecked", "rawtypes" }) + private Expr makeTruncateToZero(Expr e) { + if (e instanceof BitVecExpr bv) + return toBV(bv, 32); + if (e instanceof FPExpr fp) { + FPExpr integral = z3.mkFPRoundToIntegral(z3.mkFPRoundTowardZero(), fp); + return z3.mkInt2BV(32, z3.mkReal2Int(z3.mkFPToReal(integral))); + } + if (e instanceof RealExpr r) { + IntExpr floor = z3.mkReal2Int(r); + // floor == trunc for non-negative values; for negatives trunc = floor + 1 (unless already integral). + IntExpr trunc = (IntExpr) z3.mkITE(z3.mkGe(r, z3.mkReal(0)), floor, + z3.mkITE(z3.mkEq(z3.mkInt2Real(floor), r), floor, z3.mkAdd(floor, z3.mkInt(1)))); + return z3.mkInt2BV(32, trunc); + } throw new NotImplementedException(); } - private FPExpr toFP(Expr e) { + /** + * Common floating-point sort for a binary operation, mirroring Java binary numeric promotion: if either operand is + * a {@code double} (binary64) the result is binary64, otherwise binary32 (a lone {@code float} operand, possibly + * mixed with an integral operand that Java would convert to {@code float}). At least one operand must be an + * {@link FPExpr} for this to be called. + */ + private FPSort commonFPSort(Expr e1, Expr e2) { + if (isDoubleSort(e1) || isDoubleSort(e2)) + return z3.mkFPSort64(); + return z3.mkFPSort32(); + } + + private boolean isDoubleSort(Expr e) { + return e instanceof FPExpr && ((FPExpr) e).getSort().equals(z3.mkFPSort64()); + } + + /** + * Coerces {@code e} to the floating-point sort {@code target}. Float (binary32) operands meeting a binary64 sort + * are widened with {@link com.microsoft.z3.Context#mkFPToFP} so the cast mirrors Java's float-to-double promotion; + * integral and real operands are converted into {@code target} directly. + */ + private FPExpr toFP(Expr e, FPSort target) { FPExpr f; - if (e instanceof FPExpr) { - f = (FPExpr) e; + if (e instanceof FPExpr fe) { + f = fe.getSort().equals(target) ? fe : z3.mkFPToFP(z3.mkFPRoundNearestTiesToEven(), fe, target); + } else if (e instanceof BitVecNum bvn) { + // A literal integral value (e.g. `5` widened to float in `5 + 1.0f`): use its signed long value + // directly so the rounded FP constant matches what Java's int/long-to-float promotion produces. + f = z3.mkFP(bvn.getLong(), target); + } else if (e instanceof BitVecExpr bv) { + // A symbolic integral value mixed with floating point: reinterpret as a signed integer, then a real, + // then round into the target FP sort (Java's integral-to-floating promotion, JLS §5.1.2). + RealExpr re = z3.mkInt2Real(z3.mkBV2Int(bv, true)); + f = z3.mkFPToFP(z3.mkFPRoundNearestTiesToEven(), re, target); } else if (e instanceof IntNum) - f = z3.mkFP(((IntNum) e).getInt(), z3.mkFPSort64()); + f = z3.mkFP(((IntNum) e).getInt(), target); else if (e instanceof IntExpr ee) { RealExpr re = z3.mkInt2Real(ee); - f = z3.mkFPToFP(z3.mkFPRoundNearestTiesToEven(), re, z3.mkFPSort64()); + f = z3.mkFPToFP(z3.mkFPRoundNearestTiesToEven(), re, target); } else if (e instanceof RealExpr) { - f = z3.mkFPToFP(z3.mkFPRoundNearestTiesToEven(), (RealExpr) e, z3.mkFPSort64()); + f = z3.mkFPToFP(z3.mkFPRoundNearestTiesToEven(), (RealExpr) e, target); } else { throw new NotImplementedException(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java index 0f6cd964f..a691dcb66 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java @@ -11,4 +11,11 @@ public final class Keys { public static final String VARIABLE = "Variable"; public static final String GHOST = "Ghost"; public static final String ALIAS = "Alias"; + /** + * Reserved builtin function name modeling a Java floating-point-to-integral narrowing cast (e.g. {@code (int) d}), + * which truncates its single argument toward zero (JLS §5.1.3). Translated directly by the SMT backend (see + * {@link liquidjava.smt.TranslatorToZ3#makeFunctionInvocation}); it is not a user-visible ghost, so it never + * participates in ghost overload resolution. + */ + public static final String TRUNCATE = "$truncateToZero"; } \ No newline at end of file diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestSoundnessHoleRuntime.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestSoundnessHoleRuntime.java new file mode 100644 index 000000000..86501f7ce --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestSoundnessHoleRuntime.java @@ -0,0 +1,127 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertInstanceOf; +import static org.junit.jupiter.api.Assertions.assertNotNull; +import static org.junit.jupiter.api.Assertions.fail; + +import java.io.File; +import java.lang.reflect.InvocationTargetException; +import java.lang.reflect.Method; +import java.net.URL; +import java.net.URLClassLoader; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.concurrent.ExecutionException; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; +import java.util.concurrent.TimeUnit; +import java.util.concurrent.TimeoutException; +import java.util.stream.Stream; + +import javax.tools.JavaCompiler; +import javax.tools.ToolProvider; + +import liquidjava.specification.Refinement; + +import org.junit.jupiter.api.io.TempDir; +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.MethodSource; + +/** + * Validates that every soundness-hole test program is a genuine soundness hole and not a mislabeled safe program. + * + *

+ * The companion {@link TestExamples} cases named {@code Error*Unsound} document programs the verifier currently accepts + * but which are actually unsafe. For each such program this test compiles it and runs it in-process under a child class + * loader with assertions enabled (no forked JVM); each embeds a runtime {@code assert} that mirrors its + * {@code @Refinement} — an independent oracle that does not trust the verifier — so a valid hole MUST abort with an + * {@link AssertionError} at runtime. If a program runs to completion (its refinement actually holds at runtime), it is + * not a real hole and this test fails — keeping the soundness-hole suite honest. + */ +public class TestSoundnessHoleRuntime { + + private static final Path SUITE = Paths.get("../liquidjava-example/src/main/java/testSuite/"); + + /** + * Per-case compile output; JUnit creates a fresh dir per invocation and deletes it (with the .class files) after. + */ + @TempDir + private Path out; + + /** + * Cases for the runtime validator: a generated self-check fixture (so the harness is exercised even before any + * soundness-hole test exists, e.g. in the framework commit) followed by the testSuite {@code Error*Unsound.java} + * programs. + */ + private static Stream holePrograms() throws Exception { + Stream holes = Files.list(SUITE).filter(Files::isRegularFile).filter(p -> { + String n = p.getFileName().toString(); + return n.startsWith("Error") && n.contains("Unsound") && n.endsWith(".java"); + }).sorted(); + return Stream.concat(Stream.of(selfCheckFixture()), holes); + } + + /** + * Generates a tiny program whose assertion always fails, used to confirm the harness actually observes a + * {@code -ea} abort. It is generated (not a testSuite file), so it is a passing self-check, not a soundness hole. + */ + private static Path selfCheckFixture() throws Exception { + Path dir = Files.createTempDirectory("ljselfcheck"); + Path src = dir.resolve("HarnessSelfCheck.java"); + Files.writeString(src, "package testSuite;\n" + "public class HarnessSelfCheck {\n" + + " public static void main(String[] args) { assert false : \"harness self-check\"; }\n" + "}\n"); + dir.toFile().deleteOnExit(); + src.toFile().deleteOnExit(); + return src; + } + + @ParameterizedTest + @MethodSource("holePrograms") + public void runtimeViolatesRefinement(final Path source) throws Exception { + String fileName = source.getFileName().toString(); + String className = fileName.substring(0, fileName.length() - ".java".length()); + String fqcn = "testSuite." + className; + + // Classpath only needs liquidjava-api (where @Refinement / @StateRefinement live). Locate it from + // the already-loaded annotation class so we do not depend on the surefire classpath representation. + String apiPath = new File(Refinement.class.getProtectionDomain().getCodeSource().getLocation().toURI()) + .getAbsolutePath(); + + JavaCompiler javac = ToolProvider.getSystemJavaCompiler(); + assertNotNull(javac, "system Java compiler unavailable (tests must run on a JDK)"); + int compileRc = javac.run(null, null, null, "-cp", apiPath, "-d", out.toString(), source.toString()); + assertEquals(0, compileRc, fileName + " must compile as valid Java"); + + // Run in-process (no forked JVM): load the freshly compiled class through a child class loader with + // assertions enabled, then invoke main on a daemon thread bounded by a timeout. liquidjava-api is already + // on the parent loader (Refinement is loaded), so the child only needs the compiled program. + ExecutorService executor = Executors.newSingleThreadExecutor(r -> { + Thread t = new Thread(r, "soundness-hole-" + className); + t.setDaemon(true); + return t; + }); + try (URLClassLoader loader = new URLClassLoader(new URL[] { out.toUri().toURL() }, + getClass().getClassLoader())) { + loader.setDefaultAssertionStatus(true); // equivalent to -ea, without a subprocess + Method main = Class.forName(fqcn, true, loader).getMethod("main", String[].class); + try { + executor.submit(() -> main.invoke(null, (Object) new String[0])).get(60, TimeUnit.SECONDS); + fail(fileName + " is NOT a valid soundness hole: it ran to completion without violating its " + + "refinement at runtime."); + } catch (ExecutionException e) { + Throwable cause = e.getCause(); + if (cause instanceof InvocationTargetException invocation) { + cause = invocation.getCause(); + } + assertInstanceOf(AssertionError.class, cause, + fileName + " aborted, but not via the refinement assertion: " + cause); + } catch (TimeoutException e) { + fail(fileName + " timed out while running"); + } + } finally { + executor.shutdownNow(); + } + } +}