From 6519c7be576713c3fe16c64263657ff819a2999a Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 02:55:36 +0000 Subject: [PATCH 01/21] Add TestSoundnessHoleRuntime: runtime validation for soundness-hole tests Compiles each testSuite/Error*Unsound.java and runs it in-process under a child class loader with assertions enabled (no forked JVM), requiring it to abort with an AssertionError -- validating each as a genuine hole: the verifier accepts it AND the program is unsafe at runtime. The embedded assert is an independent oracle (it does not trust the verifier). A generated self-check fixture keeps the harness exercised (and this commit green) before any soundness-hole test exists. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../api/tests/TestSoundnessHoleRuntime.java | 127 ++++++++++++++++++ 1 file changed, 127 insertions(+) create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestSoundnessHoleRuntime.java 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(); + } + } +} From 4eb45ac858912a1126d60e38fde562ae7ba5773f Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 02:55:36 +0000 Subject: [PATCH 02/21] Add soundness-hole test: double remainder (IEEE vs fmod) Verifier proves _ < 1.0 for 7.0 % 4.0, but Java yields 3.0. Root: floating-point % is lowered to IEEE-754 remainder via mkFPRem (TranslatorToZ3.java:344-345); Java % is fmod. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../testSuite/ErrorFloatRemainderUnsound.java | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorFloatRemainderUnsound.java 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; + } +} From 5c6a6abc01e921cfc6aaa0b6d4bee676a5468ced Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 03:33:38 +0000 Subject: [PATCH 03/21] Fix floating-point % to use Java fmod, not IEEE-754 remainder TranslatorToZ3.makeMod lowered FP `%` to z3.mkFPRem (IEEE-754 remainder, which rounds the quotient to nearest), but Java `%` on float/double is fmod: a - b * trunc(a/b), with the quotient rounded toward zero and the result taking the sign of the dividend. Encode fmod directly. Closes the ErrorFloatRemainderUnsound hole: 7.0 % 4.0 now evaluates to 3.0 (not the IEEE remainder -1.0), so the verifier correctly rejects @Refinement("_ < 1.0"). CorrectFPArithmetic (6.0 % 4.0 == 2.0) stays green. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../src/main/java/liquidjava/smt/TranslatorToZ3.java | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index cf568927a..e611f5429 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -342,8 +342,15 @@ public Expr makeDiv(Expr eval, Expr 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. + FPExpr a = toFP(eval); + FPExpr b = toFP(eval2); + 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 (eval instanceof RealExpr || eval2 instanceof RealExpr) return z3.mkMod(toInt(eval), toInt(eval2)); return z3.mkMod((IntExpr) eval, (IntExpr) eval2); From 9ee52f74f75d5f761b349b3ae31d2386d3388bb1 Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 02:55:36 +0000 Subject: [PATCH 04/21] Add soundness-hole test: float precision (FP64 vs binary32) Verifier proves _ == 0.1 for float f = 0.1f, but the single-precision value is not 0.1. Root: float is modeled as FP64 in the constant path (TranslatorContextToZ3.java:97; literals TranslatorToZ3.java:110), inconsistent with the FP32 mapping at :136-137. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../testSuite/ErrorFloatPrecisionUnsound.java | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorFloatPrecisionUnsound.java 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; + } +} From 1b64f32a066bebfeca07ce815304cbbd8c05da55 Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 03:44:34 +0000 Subject: [PATCH 05/21] Model Java float as 32-bit FP (binary32) with float->double promotion float values were translated to FP64, so single-precision rounding was lost. Model float-origin values as binary32 and apply Java's binary numeric promotion: when a binary32 operand meets a binary64 one, widen the float to binary64 (mkFPToFP) so sorts match and semantics mirror Java. FP comparison/arithmetic helpers now coerce operands to a common FP sort (FP64 if either is double, else FP32). LiteralReal carries an isFloat flag (float vs double origin); Predicate tags Types.FLOAT literals; ExpressionToZ3Visitor emits makeFloatLiteral (mkFP at FP32) for them; TranslatorContextToZ3 creates float constants at FP32 (consistent with the existing getSort mapping). Closes ErrorFloatPrecisionUnsound: (float)0.1 widened to double != 0.1, so @Refinement("_ == 0.1") on float f = 0.1f is correctly rejected. CorrectFPArithmetic (double) and CorrectPrimitiveNumbersTypes (float) stay green. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../liquidjava/rj_language/Predicate.java | 3 +- .../rj_language/ast/LiteralReal.java | 25 ++++- .../liquidjava/smt/ExpressionToZ3Visitor.java | 2 + .../liquidjava/smt/TranslatorContextToZ3.java | 5 +- .../java/liquidjava/smt/TranslatorToZ3.java | 102 +++++++++++++----- 5 files changed, 107 insertions(+), 30 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index e6a4f04fb..3248c9dcc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -338,7 +338,8 @@ public static Predicate createLit(String value, String type) { case Types.BOOLEAN -> 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..736e0ae05 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -94,7 +94,10 @@ private static Expr getExpr(Context z3, String name, CtTypeReference type) .mkIntConst(name); 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()); + // Java `float` is binary32 and `double` is binary64; modeling float as FP64 would lose single-precision + // rounding. Mixed-precision expressions are reconciled via Java numeric promotion in TranslatorToZ3. + case "float", "java.lang.Float" -> (FPExpr) z3.mkConst(name, z3.mkFPSort32()); + case "double", "java.lang.Double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64()); case "int[]" -> z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort()); default -> z3.mkConst(name, z3.mkUninterpretedSort(typeName)); }; diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index e611f5429..f4d0687c2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -6,6 +6,7 @@ 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; @@ -111,6 +112,15 @@ 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); } @@ -233,8 +243,10 @@ 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 (e1 instanceof RealExpr || e2 instanceof RealExpr) return z3.mkEq(toReal(e1), toReal(e2)); return z3.mkEq(e1, e2); @@ -242,8 +254,10 @@ public Expr makeEquals(Expr e1, Expr 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 (e1 instanceof RealExpr || e2 instanceof RealExpr) return z3.mkLt(toReal(e1), toReal(e2)); return z3.mkLt((ArithExpr) e1, (ArithExpr) e2); @@ -251,8 +265,10 @@ 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 (e1 instanceof RealExpr || e2 instanceof RealExpr) return z3.mkLe(toReal(e1), toReal(e2)); return z3.mkLe((ArithExpr) e1, (ArithExpr) e2); @@ -260,8 +276,10 @@ 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 (e1 instanceof RealExpr || e2 instanceof RealExpr) return z3.mkGt(toReal(e1), toReal(e2)); return z3.mkGt((ArithExpr) e1, (ArithExpr) e2); @@ -269,8 +287,10 @@ 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 (e1 instanceof RealExpr || e2 instanceof RealExpr) return z3.mkGe(toReal(e1), toReal(e2)); return z3.mkGe((ArithExpr) e1, (ArithExpr) e2); @@ -307,8 +327,10 @@ public Expr makeMinus(Expr 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 (eval instanceof RealExpr || eval2 instanceof RealExpr) return z3.mkAdd(toReal(eval), toReal(eval2)); return z3.mkAdd((ArithExpr) eval, (ArithExpr) eval2); @@ -316,8 +338,10 @@ 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 (eval instanceof RealExpr || eval2 instanceof RealExpr) return z3.mkSub(toReal(eval), toReal(eval2)); return z3.mkSub((ArithExpr) eval, (ArithExpr) eval2); @@ -325,8 +349,10 @@ 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 (eval instanceof RealExpr || eval2 instanceof RealExpr) return z3.mkMul(toReal(eval), toReal(eval2)); return z3.mkMul((ArithExpr) eval, (ArithExpr) eval2); @@ -334,8 +360,10 @@ 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 (eval instanceof RealExpr || eval2 instanceof RealExpr) return z3.mkDiv(toReal(eval), toReal(eval2)); return z3.mkDiv((ArithExpr) eval, (ArithExpr) eval2); @@ -346,8 +374,9 @@ public Expr makeMod(Expr eval, Expr eval2) { // 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. - FPExpr a = toFP(eval); - FPExpr b = toFP(eval2); + 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)); } @@ -372,17 +401,38 @@ private IntExpr toInt(Expr e) { 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 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(); } From 5d3f1c298bf86cee611092d9bee3128e9a90ccbd Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 02:55:36 +0000 Subject: [PATCH 06/21] Add soundness-hole test: short-circuit RHS side effect applied Verifier proves _ == 1 for x after false && ((x = 1) == 1), but the && short-circuits so x stays 0. Root: both operands are refined unconditionally (OperationsChecker.java:68-69). Co-Authored-By: Claude Opus 4.8 (1M context) --- .../ErrorShortCircuitAssignUnsound.java | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorShortCircuitAssignUnsound.java 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; + } +} From c23f819d73215acea67f1016d52690299ee4047b Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 03:52:58 +0000 Subject: [PATCH 07/21] Discard assignments in the short-circuited operand of && / || MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit RefinementTypeChecker (a CtScanner) descends into a binary operator's children before its override runs, so an assignment in the right operand of `&&`/`||` (which executes only conditionally at runtime) was committed to the variable context unconditionally. visitCtBinaryOperator now, after computing the boolean value refinement, havocs every variable written in the conditionally-evaluated (right) operand — installing a fresh unconstrained instance — so its post-value is treated as unknown. This only ever weakens knowledge, so it cannot accept an unsound program. Closes ErrorShortCircuitAssignUnsound: after `false && ((x=1)==1)` the verifier no longer believes x==1, so @Refinement("_ == 1") int y = x is correctly rejected. &&/|| Correct tests (CorrectImplies, CorrectBooleanLitAndInvocations, CorrectOperatorPrecedence) stay green. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../RefinementTypeChecker.java | 47 +++++++++++++++++++ 1 file changed, 47 insertions(+) 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..4f9102983 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 @@ -20,6 +20,7 @@ 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; @@ -46,11 +47,13 @@ import spoon.reflect.code.CtUnaryOperator; import spoon.reflect.code.CtVariableAccess; import spoon.reflect.code.CtVariableRead; +import spoon.reflect.code.CtVariableWrite; 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 { @@ -335,6 +338,50 @@ 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; + + CtExpression conditionalOperand = operator.getRightHandOperand(); + for (CtVariableWrite write : conditionalOperand.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) { + 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); } @Override From cc0ae001f1154df6495174b8adb2d1f84c78102b Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 02:55:36 +0000 Subject: [PATCH 08/21] Add soundness-hole test: field refinement assumed not established Verifier proves _ > 0 reading a field annotated _ > 0 that defaults to 0. Root: field refinements are trusted on read (RefinementTypeChecker.java:256,272) without proving establishment. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../testSuite/ErrorFieldDefaultUnsound.java | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorFieldDefaultUnsound.java 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; + } +} From 7ffc2ac43e4acd3382a69db9571d0dbdcccab821 Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 04:09:08 +0000 Subject: [PATCH 09/21] Read an unestablished external field at its default, not its refinement visitCtFieldRead modeled every `o.field` read as `_ == this#field`, pulling in the field's declared @Refinement even when the field was never established. For an external read (not a this-access) of a field with no initializer, the runtime value is the Java default, which the declared refinement may not satisfy. Now such reads are modeled as `_ == ` (0 / 0.0 / false; references unchanged) instead of assuming the refinement. this-accesses and initialized fields keep their existing behavior. Closes ErrorFieldDefaultUnsound: reading uninitialized `int n` (default 0) into @Refinement("_ > 0") int x is correctly rejected. Field / static-final / enum Correct tests stay green. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../RefinementTypeChecker.java | 68 ++++++++++++++++++- 1 file changed, 66 insertions(+), 2 deletions(-) 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 4f9102983..9235c0aea 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 @@ -286,8 +286,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(); @@ -320,6 +332,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); From ff8623f6c8bfa6b6dba946175e799f47f9d39549 Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 02:55:36 +0000 Subject: [PATCH 10/21] Add soundness-hole test: loop modeled as one iteration Verifier proves _ == 1 after while (x < 2) x = x + 1, but the loop exits with x == 2. Root: no loop fixpoint or havoc; the body is treated as completing once (RefinementTypeChecker.java:458-459). Co-Authored-By: Claude Opus 4.8 (1M context) --- .../testSuite/ErrorLoopSinglePassUnsound.java | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLoopSinglePassUnsound.java 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; + } +} From e5ce86151c5c7f61c39202db3c67f237437cef44 Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 04:20:02 +0000 Subject: [PATCH 11/21] Havoc variables written in loop bodies Loops had no special handling: the body was scanned once and its assignments committed, so a variable mutated in a loop kept a single-pass value afterward (e.g. while(x<2) x=x+1 left x==1). Added visitors for while/do/for/for-each that, after visiting the body once (so in-body refinement/typestate errors are still reported), havoc every variable written in the body (and the for-update/condition) via the existing havocVariable helper, so post-loop values are treated as unknown. Havoc only weakens knowledge, so it cannot accept an unsound program. Only direct value writes (CtVariableWrite) are havoc'd; typestate mutated through method calls (e.g. rs.next()) is untouched, so loop-based typestate/iterator Correct tests stay green. Closes ErrorLoopSinglePassUnsound: after the loop x is unknown, so @Refinement("_ == 1") int y = x is correctly rejected. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../RefinementTypeChecker.java | 64 ++++++++++++++++++- 1 file changed, 62 insertions(+), 2 deletions(-) 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 9235c0aea..d7e0b51ab 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 @@ -30,13 +30,17 @@ 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; @@ -48,6 +52,7 @@ 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; @@ -423,8 +428,19 @@ private void forgetShortCircuitedAssignments(CtBinaryOperator operator) { if (kind != BinaryOperatorKind.AND && kind != BinaryOperatorKind.OR) return; - CtExpression conditionalOperand = operator.getRightHandOperand(); - for (CtVariableWrite write : conditionalOperand.getElements(new TypeFilter<>(CtVariableWrite.class))) { + 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; @@ -448,6 +464,50 @@ private void havocVariable(String name, CtElement element) { context.addRefinementToVariableInContext(name, rv.getType(), new Predicate(), element); } + // ############################### 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()); + } + @Override public void visitCtUnaryOperator(CtUnaryOperator operator) { super.visitCtUnaryOperator(operator); From 9dcb85034dd96c20ffd780b0780e78c5a1d50db8 Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 02:55:36 +0000 Subject: [PATCH 12/21] Add soundness-hole test: exceptional control flow ignored Verifier proves _ == 1 after a try whose first statement 1 / 0 throws, but x stays 0. Root: try/catch flow is not modeled (RefinementTypeChecker.java:458-459). Co-Authored-By: Claude Opus 4.8 (1M context) --- .../testSuite/ErrorExceptionFlowUnsound.java | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorExceptionFlowUnsound.java 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; + } +} From 95aef14124122f686a7e1d8ee15dca582bd4cd25 Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 04:24:57 +0000 Subject: [PATCH 13/21] Havoc variables written in try/catch bodies try/catch flow was unmodeled: the try body was scanned straight-line, so an assignment after a throwing statement was trusted though it may never run. Added visitCtTry that, after visiting (so in-body/in-handler errors are still reported), havocs every variable written in the try body and each catch block, treating their post-try values as uncertain. finally blocks always complete, so their definite assignments are left trusted. Closes ErrorExceptionFlowUnsound: 1/0 throws so x stays 0; after havoc x is unknown, so @Refinement("_ == 1") int y = x is correctly rejected. The existing try/catch typestate test (IteratorRemoveBeforeNext) stays green. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../RefinementTypeChecker.java | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) 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 d7e0b51ab..d98dc97dd 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 @@ -27,6 +27,7 @@ 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; @@ -48,6 +49,7 @@ 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; @@ -508,6 +510,29 @@ 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 public void visitCtUnaryOperator(CtUnaryOperator operator) { super.visitCtUnaryOperator(operator); From 1b7d95acfb5b67b22e0f4038e5d9128e2c0d538e Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 02:55:36 +0000 Subject: [PATCH 14/21] Add soundness-hole test: narrowing cast ignored Verifier proves _ == 1.9 for (int) 1.9, but the cast yields 1. Root: cast expressions are not modeled (RefinementTypeChecker.java around 544); the subtype check can then pass vacuously (SMTEvaluator.java:36). Co-Authored-By: Claude Opus 4.8 (1M context) --- .../testSuite/ErrorNarrowingCastUnsound.java | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorNarrowingCastUnsound.java 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; + } +} From 12a6cf34afc3b8f4fafb1736b7fb967300cfe223 Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 04:35:46 +0000 Subject: [PATCH 15/21] Model floating-point to integral narrowing casts as truncation Cast expressions were ignored, so `(int) 1.9` was modeled as 1.9 and @Refinement("_ == 1.9") int x = (int) 1.9 was vacuously accepted. A float/double -> integral narrowing cast now rewrites the value refinement `_ == E` to `_ == $truncateToZero(E)` (JLS 5.1.3, round toward zero), applied at the assignment-RHS chokepoints. The builtin $truncateToZero reuses the existing FunctionInvocation path (no parser or simplifier changes). Identity and widening casts are left untouched. Closes ErrorNarrowingCastUnsound: (int)1.9 is 1, so _ == 1.9 is correctly rejected (counterexample x == 1). Cast/numeric Correct tests (CorrectOperatorAssignments, CorrectFPArithmetic, CorrectBoxedTypes, CorrectPrimitiveNumbersTypes) stay green. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../RefinementTypeChecker.java | 64 ++++++++++++++++++- .../java/liquidjava/smt/TranslatorToZ3.java | 29 +++++++++ .../java/liquidjava/utils/constants/Keys.java | 7 ++ 3 files changed, 99 insertions(+), 1 deletion(-) 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 d98dc97dd..d683b2db1 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,10 +13,14 @@ 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; @@ -157,6 +161,7 @@ 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); @@ -734,7 +739,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 { @@ -793,4 +798,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/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index f4d0687c2..339f456a4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -174,6 +174,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); @@ -401,6 +403,33 @@ private IntExpr toInt(Expr e) { throw new NotImplementedException(); } + /** + * 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 operand is already integral and returned unchanged. + */ + @SuppressWarnings({ "unchecked", "rawtypes" }) + private Expr makeTruncateToZero(Expr e) { + if (e instanceof IntExpr) + return e; + if (e instanceof FPExpr fp) { + FPExpr integral = z3.mkFPRoundToIntegral(z3.mkFPRoundTowardZero(), fp); + return 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). + return z3.mkITE(z3.mkGe(r, z3.mkReal(0)), floor, + z3.mkITE(z3.mkEq(z3.mkInt2Real(floor), r), floor, z3.mkAdd(floor, z3.mkInt(1)))); + } + throw new NotImplementedException(); + } + /** * 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 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 From 671ad43531e5309d0bd05fd93b3253f64607129a Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 02:55:36 +0000 Subject: [PATCH 16/21] Add soundness-hole test: typestate stale under aliasing After b = a then a.close(), the verifier still treats b as open and accepts b.read(), but b aliases the closed object. Root: a transition attaches the new state to the receiver variable only (object_checkers/AuxStateHandler.java); aliases keep stale state. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../testSuite/ErrorTypestateAliasUnsound.java | 35 +++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorTypestateAliasUnsound.java 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 + } +} From 9106d321ed68a0c6a27f8cc316f7b83c051a9a14 Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 04:48:43 +0000 Subject: [PATCH 17/21] Invalidate aliased typestate on a state transition A reference-copy `X b = a;` makes b's instance value-equal to a's current instance, but a transition (a.close()) created a new instance for a while leaving the shared old instance in its stale state, so b kept the pre-transition state. Added an object-alias registry to Context: reference-copy assignments (bare variable read of another tracked reference) record an alias; any other RHS clears it. On a successful state transition, AuxStateHandler havocs the tracked state of all aliases of the receiver, so they are no longer trusted at the old state. Triggers only on real aliasing, so single-reference usage is unaffected. Closes ErrorTypestateAliasUnsound: after `b = a; a.close()`, b's state is unknown, so b.read() (requires open) is correctly rejected. Typestate Correct tests stay green. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../liquidjava/processor/context/Context.java | 69 +++++++++++++++++++ .../RefinementTypeChecker.java | 42 +++++++++-- .../refinement_checker/TypeChecker.java | 41 +++++++++++ .../object_checkers/AuxStateHandler.java | 3 + 4 files changed, 149 insertions(+), 6 deletions(-) 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 d683b2db1..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 @@ -165,6 +165,7 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) { 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); } } @@ -226,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(); @@ -462,13 +464,41 @@ private void havocVariablesWrittenIn(CtElement scope) { * value. Subsequent reads resolve to this instance and therefore carry no refinement. */ private void havocVariable(String name, CtElement element) { - RefinedVariable rv = context.getVariableByName(name); - if (!(rv instanceof Variable)) + 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; - 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); + } + // 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 ########################################## 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 Date: Mon, 15 Jun 2026 02:55:36 +0000 Subject: [PATCH 18/21] Add soundness-hole test: int multiplication overflow Verifier proves _ > 0 for int c = 46341 * 46341, but the product overflows int to -2147479015. Root: int is modeled as an unbounded Z3 Int (TranslatorContextToZ3.java:93; TranslatorToZ3.java:103,327). Co-Authored-By: Claude Opus 4.8 (1M context) --- .../java/testSuite/ErrorIntOverflowUnsound.java | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorIntOverflowUnsound.java 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; + } +} From 6243c93803953d1b4567ea0dad6c4e10c935b481 Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 02:55:36 +0000 Subject: [PATCH 19/21] Add soundness-hole test: int negative modulo Verifier proves _ >= 0 for (-7) % 3, but Java yields -1. Root: makeMod uses Euclidean Z3 mkMod (TranslatorToZ3.java:344); Java % follows the sign of the dividend. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../testSuite/ErrorNegativeModuloUnsound.java | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorNegativeModuloUnsound.java 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; + } +} From a6c5b858ee1f89f66471fd3f3ba34294294e17e1 Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 02:55:36 +0000 Subject: [PATCH 20/21] Add soundness-hole test: long division truncation Verifier proves _ > 3 for 7L / 2L, but Java truncates to 3. Root: long is modeled as a Z3 Real (TranslatorContextToZ3.java:96; makeLongLiteral :106), so division is exact and rational (makeDiv:336). Co-Authored-By: Claude Opus 4.8 (1M context) --- .../ErrorLongAsRealDivisionUnsound.java | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLongAsRealDivisionUnsound.java 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; + } +} From 11c748ccca69bc984b58cdc3f72ce90c13ef1481 Mon Sep 17 00:00:00 2001 From: Guilherme Espada Date: Mon, 15 Jun 2026 05:37:25 +0000 Subject: [PATCH 21/21] Model Java integral types as fixed-width BitVectors Migrate int/short/char/byte -> 32-bit BitVec and long -> 64-bit BitVec in the SMT translation. Z3 BitVec ops match Java exactly: mkBVAdd/Sub/Mul wrap (two's-complement overflow), mkBVSDiv truncates toward zero, mkBVSRem takes the sign of the dividend, signed comparisons; int<->long mixing sign-extends, and BV<->real/FP coercions go through mkBV2Int/getLong. ExpressionFolding (Java-int constant folding) is now consistent with the solver. Closes three holes at once: ErrorIntOverflowUnsound (46341*46341 wraps to -2147479015), ErrorNegativeModuloUnsound (-7 % 3 == -1), and ErrorLongAsRealDivisionUnsound (7L/2L == 3). Sound fixed-width semantics also exposed six Correct tests that were themselves latently unsound (they asserted mathematically-true but Java-false postconditions that overflow): CorrectSimpleIfElse (-a at MIN_VALUE), CorrectSpecificFunctionInvocation / CorrectLongUsage / CorrectFunctionsTutorial / CorrectIfThen / CorrectOperatorAssignments (+,-,* overflow). Each now carries overflow-guard preconditions/bounds so its postcondition genuinely holds (CorrectLongUsage widens to long before multiplying). ErrorLongUsage gains a third expected-error marker for the now-correctly-rejected overflow in its own body. Whole verifier suite is green (304 tests, 0 failures); all 11 Error*Unsound holes are now rejected. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../testSuite/CorrectFunctionsTutorial.java | 11 +- .../main/java/testSuite/CorrectIfThen.java | 4 +- .../main/java/testSuite/CorrectLongUsage.java | 15 +- .../testSuite/CorrectOperatorAssignments.java | 12 +- .../java/testSuite/CorrectSimpleIfElse.java | 10 +- .../CorrectSpecificFunctionInvocation.java | 6 +- .../main/java/testSuite/ErrorLongUsage.java | 2 +- .../liquidjava/smt/TranslatorContextToZ3.java | 19 ++- .../java/liquidjava/smt/TranslatorToZ3.java | 141 +++++++++++++++++- 9 files changed, 188 insertions(+), 32 deletions(-) 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/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-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index 736e0ae05..0719ad479 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -90,15 +90,18 @@ private static Expr getExpr(Context z3, String name, CtTypeReference type) String typeName = type.getQualifiedName(); return switch (typeName) { - case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" -> z3 - .mkIntConst(name); + // Java integral types are fixed-width two's-complement values, so they are modeled as Z3 BitVectors + // (32-bit for int/short/char/byte and their boxed forms, 64-bit for long). This makes overflow, + // signed division/remainder, and signed comparison faithful to the JLS instead of unbounded integers. + case "int", "short", "char", "byte", "java.lang.Integer", "java.lang.Short", "java.lang.Character", "java.lang.Byte" -> z3 + .mkBVConst(name, 32); case "boolean", "java.lang.Boolean" -> z3.mkBoolConst(name); - case "long", "java.lang.Long" -> z3.mkRealConst(name); + case "long", "java.lang.Long" -> z3.mkBVConst(name, 64); // Java `float` is binary32 and `double` is binary64; modeling float as FP64 would lose single-precision // rounding. Mixed-precision expressions are reconciled via Java numeric promotion in TranslatorToZ3. case "float", "java.lang.Float" -> (FPExpr) z3.mkConst(name, z3.mkFPSort32()); case "double", "java.lang.Double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64()); - case "int[]" -> z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort()); + case "int[]" -> z3.mkArrayConst(name, z3.mkBitVecSort(32), z3.mkBitVecSort(32)); default -> z3.mkConst(name, z3.mkUninterpretedSort(typeName)); }; } @@ -133,12 +136,14 @@ private static void addBuiltinFunctions(Context z3, Map> 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 339f456a4..6a4bf5835 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -2,6 +2,9 @@ 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; @@ -101,11 +104,13 @@ 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) { @@ -249,8 +254,14 @@ public Expr makeEquals(Expr e1, Expr e2) { 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); } @@ -260,6 +271,10 @@ public Expr makeLt(Expr e1, Expr e2) { 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); @@ -271,6 +286,10 @@ public Expr makeLtEq(Expr e1, Expr e2) { 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); @@ -282,6 +301,10 @@ public Expr makeGt(Expr e1, Expr e2) { 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); @@ -293,6 +316,10 @@ public Expr makeGtEq(Expr e1, Expr e2) { 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); @@ -323,6 +350,9 @@ 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); } @@ -333,6 +363,10 @@ public Expr makeAdd(Expr eval, Expr eval2) { 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); @@ -344,6 +378,10 @@ public Expr makeSub(Expr eval, Expr eval2) { 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); @@ -355,6 +393,10 @@ public Expr makeMul(Expr eval, Expr eval2) { 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); @@ -366,6 +408,10 @@ public Expr makeDiv(Expr eval, Expr eval2) { 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); @@ -382,6 +428,12 @@ public Expr makeMod(Expr eval, Expr eval2) { 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); @@ -392,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(); } @@ -400,9 +454,71 @@ 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. @@ -411,21 +527,23 @@ private IntExpr toInt(Expr e) { * 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 operand is already integral and returned unchanged. + * 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 IntExpr) - return e; + if (e instanceof BitVecExpr bv) + return toBV(bv, 32); if (e instanceof FPExpr fp) { FPExpr integral = z3.mkFPRoundToIntegral(z3.mkFPRoundTowardZero(), fp); - return z3.mkReal2Int(z3.mkFPToReal(integral)); + 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). - return z3.mkITE(z3.mkGe(r, z3.mkReal(0)), floor, + 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(); } @@ -455,6 +573,15 @@ private FPExpr toFP(Expr e, FPSort target) { FPExpr f; 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(), target); else if (e instanceof IntExpr ee) {