From 06879069bd3a9007e793ab0b14fbf886a7f5d7b7 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sat, 13 Jun 2026 19:18:00 +0200 Subject: [PATCH 1/3] add visit call and examples --- .../resultset_forward_correct/ResultSetTests.java | 15 +++++++++++++++ .../resultset_forward_error/ResultSetTests.java | 14 ++++++++++++++ .../refinement_checker/RefinementTypeChecker.java | 6 ++++-- 3 files changed, 33 insertions(+), 2 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java index f865a82c9..491e5c64b 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java @@ -62,4 +62,19 @@ float readAverage(Connection conn) throws SQLException { return 0.0f; } } + + float readAverage2(Connection conn) throws SQLException { + Statement parentstmt = conn.createStatement(); + ResultSet parentMessage = + parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); + // FIX (from accepted answer): parentMessage.next(); + // VIOLATION: cursor is before the first row; getFloat() with no next(). + boolean b = parentMessage.next(); + if( b ) { + float avgsum = parentMessage.getFloat("IMPAVG"); + return avgsum; + } else { + return 0.0f; + } + } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java index 508b09a82..98160c42a 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java @@ -67,4 +67,18 @@ float readAverage(Connection conn) throws SQLException { float avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error return avgsum; } + + // Branch-sensitive: legal in the then-branch (onRow), illegal in the else-branch (endRows). + float readAverageVarElse(Connection conn) throws SQLException { + Statement parentstmt = conn.createStatement(); + ResultSet parentMessage = parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); + float avgsum = 0.0f; + boolean b = parentMessage.next(); + if (b) { + avgsum = parentMessage.getFloat("IMPAVG"); + } else { + avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error + } + return avgsum; + } } 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 5cc2a09d6..7bc6f57d2 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 @@ -538,8 +538,10 @@ private Predicate getAssignmentRefinement(String name, CtExpression assignmen } private Predicate getExpressionRefinements(CtExpression element) throws LJError { - if (element instanceof CtVariableRead) { - // CtVariableRead elemVar = (CtVariableRead) element; + if (element instanceof CtFieldRead) { + return getRefinement(element); + } else if (element instanceof CtVariableRead varRead) { + visitCtVariableRead(varRead); return getRefinement(element); } else if (element instanceof CtBinaryOperator) { CtBinaryOperator binop = (CtBinaryOperator) element; From ddead1b6dc3f60ec13db7a2561861bfef2e120c8 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sat, 13 Jun 2026 19:26:16 +0200 Subject: [PATCH 2/3] renames and add if null --- .../resultset_forward_correct/ResultSetTests.java | 7 ++++--- .../resultset_forward_error/ResultSetTests.java | 13 ++++++++++++- .../refinement_checker/RefinementTypeChecker.java | 11 +++++++++++ 3 files changed, 27 insertions(+), 4 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java index 491e5c64b..4e1312265 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java @@ -63,12 +63,13 @@ float readAverage(Connection conn) throws SQLException { } } - float readAverage2(Connection conn) throws SQLException { + float readAverageStoredCondition(Connection conn) throws SQLException { Statement parentstmt = conn.createStatement(); ResultSet parentMessage = parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); - // FIX (from accepted answer): parentMessage.next(); - // VIOLATION: cursor is before the first row; getFloat() with no next(). + // Regression for issue #241: next()'s result is stored in a boolean before the `if`. + // The transition (_ ? onRow : endRows) must still flow through `b`, so the guarded + // getFloat() is on a row (onRow) and verifies — exactly as the inline readAverage above. boolean b = parentMessage.next(); if( b ) { float avgsum = parentMessage.getFloat("IMPAVG"); diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java index 98160c42a..166c52756 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java @@ -68,7 +68,18 @@ float readAverage(Connection conn) throws SQLException { return avgsum; } - // Branch-sensitive: legal in the then-branch (onRow), illegal in the else-branch (endRows). + // Issue #241 soundness: storing next()'s result in a boolean must NOT make getFloat() + // unconditionally legal. With no guard the state is `next ? onRow : endRows`, so onRow is + // not guaranteed and getFloat() must still be rejected. + float readAverageStoredNoGuard(Connection conn) throws SQLException { + Statement parentstmt = conn.createStatement(); + ResultSet parentMessage = parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); + boolean b = parentMessage.next(); + float avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error + return avgsum; + } + + // Issue #241 branch-sensitivity: legal in the then-branch (onRow), illegal in the else-branch (endRows). float readAverageVarElse(Connection conn) throws SQLException { Statement parentstmt = conn.createStatement(); ResultSet parentMessage = parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); 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 7bc6f57d2..7265f1d1a 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 @@ -321,6 +321,10 @@ private boolean tryStaticFinalConstantRefinement(CtFieldRead fieldRead) { public void visitCtVariableRead(CtVariableRead variableRead) { super.visitCtVariableRead(variableRead); CtVariable varDecl = variableRead.getVariable().getDeclaration(); + // Some CtVariableRead forms have no resolvable declaration (e.g. accesses to symbols outside the + // model); with no name there is no context entry to attach, so leave the metadata as-is. + if (varDecl == null) + return; getPutVariableMetadata(variableRead, varDecl.getSimpleName()); } @@ -539,8 +543,15 @@ private Predicate getAssignmentRefinement(String name, CtExpression assignmen private Predicate getExpressionRefinements(CtExpression element) throws LJError { if (element instanceof CtFieldRead) { + // CtFieldRead is a subtype of CtVariableRead and MUST be matched first: field reads (including + // the array pseudo-field `.length`, whose declaration is null) are handled by visitCtFieldRead + // during the surrounding scan, so here we just read the metadata it already set. return getRefinement(element); } else if (element instanceof CtVariableRead varRead) { + // Visit the read so its metadata becomes `_ == `, linking the variable to the + // instance that carries its refinement (e.g. a stored method result). Without this, `if (b)` + // looks refinement-free and is treated as uninformative, dropping the typestate that b's + // defining call established (#241). visitCtVariableRead(varRead); return getRefinement(element); } else if (element instanceof CtBinaryOperator) { From b39d80627a291ee8e31b4b16e5da69e15e46eead Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sat, 13 Jun 2026 19:32:13 +0200 Subject: [PATCH 3/3] remove comments --- .../refinement_checker/RefinementTypeChecker.java | 10 ++-------- 1 file changed, 2 insertions(+), 8 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 7265f1d1a..33b5198c8 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 @@ -542,16 +542,10 @@ private Predicate getAssignmentRefinement(String name, CtExpression assignmen } private Predicate getExpressionRefinements(CtExpression element) throws LJError { - if (element instanceof CtFieldRead) { - // CtFieldRead is a subtype of CtVariableRead and MUST be matched first: field reads (including - // the array pseudo-field `.length`, whose declaration is null) are handled by visitCtFieldRead - // during the surrounding scan, so here we just read the metadata it already set. + if (element instanceof CtFieldRead fieldRead) { + visitCtFieldRead(fieldRead); return getRefinement(element); } else if (element instanceof CtVariableRead varRead) { - // Visit the read so its metadata becomes `_ == `, linking the variable to the - // instance that carries its refinement (e.g. a stored method result). Without this, `if (b)` - // looks refinement-free and is treated as uninformative, dropping the typestate that b's - // defining call established (#241). visitCtVariableRead(varRead); return getRefinement(element); } else if (element instanceof CtBinaryOperator) {