Merge branch 'main' into vc-function-substitution

Author: rcosta358

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

@@ -0,0 +1,7 @@
+package testSuite;
+
+import liquidjava.specification.StateSet;
+
+@StateSet({"idle", "running"})
+public interface CorrectInterfaceStateSet {
+}

liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java

@@ -62,4 +62,20 @@ float readAverage(Connection conn) throws SQLException {
             return 0.0f;
         }
     }
+
+    float readAverageStoredCondition(Connection conn) throws SQLException {
+        Statement parentstmt = conn.createStatement();
+        ResultSet parentMessage =
+                parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL");
+        // 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");
+            return avgsum;
+        } else {
+            return 0.0f;
+        }
+    }
 }

liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java

@@ -67,4 +67,29 @@ float readAverage(Connection conn) throws SQLException {
         float avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error
         return avgsum;
     }
+
+    // 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");
+        float avgsum = 0.0f;
+        boolean b = parentMessage.next();
+        if (b) {
+            avgsum = parentMessage.getFloat("IMPAVG");
+        } else {
+            avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error
+        }
+        return avgsum;
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -321,6 +321,10 @@ private <T> boolean tryStaticFinalConstantRefinement(CtFieldRead<T> fieldRead) {
     public <T> void visitCtVariableRead(CtVariableRead<T> variableRead) {
         super.visitCtVariableRead(variableRead);
         CtVariable<T> 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());
     }
 
@@ -538,8 +542,11 @@ 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<?> fieldRead) {
+            visitCtFieldRead(fieldRead);
+            return getRefinement(element);
+        } else if (element instanceof CtVariableRead<?> varRead) {
+            visitCtVariableRead(varRead);
             return getRefinement(element);
         } else if (element instanceof CtBinaryOperator<?>) {
             CtBinaryOperator<?> binop = (CtBinaryOperator<?>) element;

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -263,40 +263,32 @@ private void createStateGhost(String string, CtElement element, SourcePosition p
     }
 
     protected String getQualifiedClassName(CtElement element) {
-        if (element.getParent() instanceof CtClass<?>) {
-            return ((CtClass<?>) element.getParent()).getQualifiedName();
-        } else if (element instanceof CtClass<?>) {
-            return ((CtClass<?>) element).getQualifiedName();
-        }
-        return null;
+        return getEnclosingType(element).map(CtType::getQualifiedName).orElse(null);
     }
 
     protected String getSimpleClassName(CtElement element) {
-        if (element.getParent() instanceof CtClass<?>) {
-            return ((CtClass<?>) element.getParent()).getSimpleName();
-        } else if (element instanceof CtClass<?>) {
-            return ((CtClass<?>) element).getSimpleName();
-        }
-        return null;
+        return getEnclosingType(element).map(CtType::getSimpleName).orElse(null);
     }
 
     protected Optional<GhostFunction> createStateGhost(int order, CtElement element) {
-        CtClass<?> klass = null;
-        if (element.getParent() instanceof CtClass<?>) {
-            klass = (CtClass<?>) element.getParent();
-        } else if (element instanceof CtClass<?>) {
-            klass = (CtClass<?>) element;
-        }
-        if (klass != null) {
+        Optional<CtType<?>> enclosingType = getEnclosingType(element);
+        if (enclosingType.isPresent()) {
+            CtType<?> type = enclosingType.get();
             CtTypeReference<?> ret = factory.Type().INTEGER_PRIMITIVE;
-            List<String> params = Collections.singletonList(klass.getSimpleName());
+            List<String> params = Collections.singletonList(type.getSimpleName());
             String name = String.format("state%d", order);
-            GhostFunction gh = new GhostFunction(name, params, ret, factory, klass.getQualifiedName());
+            GhostFunction gh = new GhostFunction(name, params, ret, factory, type.getQualifiedName());
             return Optional.of(gh);
         }
         return Optional.empty();
     }
 
+    private Optional<CtType<?>> getEnclosingType(CtElement element) {
+        if (element instanceof CtType<?> type)
+            return Optional.of(type);
+        return Optional.ofNullable(element.getParent(CtType.class));
+    }
+
     protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError {
         GhostDTO f = getGhostDeclaration(value, position);
         CtType<?> type = element instanceof CtType<?> t ? t : element.getParent()instanceof CtType<?> t ? t : null;

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java

@@ -75,7 +75,8 @@ private Optional<Substitution> findSubstitution(VCImplication implication) {
         if (implication == null)
             return Optional.empty();
 
-        Optional<Substitution> current = getSubstitution(implication);
+        Optional<Substitution> current = containsVar(implication.getNext(), implication.getName())
+                ? getSubstitution(implication) : Optional.empty();
         if (current.isPresent())
             return current;
 
@@ -120,4 +121,15 @@ private boolean containsVar(Expression expression, String name) {
         expression.getVariableNames(names);
         return names.contains(name);
     }
+
+    /**
+     * Checks whether a VC suffix contains a variable name
+     */
+    private boolean containsVar(VCImplication implication, String name) {
+        for (VCImplication current = implication; current != null; current = current.getNext()) {
+            if (containsVar(current.getRefinement().getExpression(), name))
+                return true;
+        }
+        return false;
+    }
 }

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

@@ -338,12 +338,14 @@ public Expr<?> makeDiv(Expr<?> eval, Expr<?> eval2) {
             return z3.mkFPDiv(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2));
         if (eval instanceof RealExpr || eval2 instanceof RealExpr)
             return z3.mkDiv(toReal(eval), toReal(eval2));
+        // Z3 integer division does not model Java's truncation toward zero for negative operands
         return z3.mkDiv((ArithExpr) eval, (ArithExpr) eval2);
     }
 
     public Expr<?> makeMod(Expr<?> eval, Expr<?> eval2) {
         if (eval instanceof FPExpr || eval2 instanceof FPExpr)
             return z3.mkFPRem(toFP(eval), toFP(eval2));
+        // Z3 integer modulo does not model Java's dividend-signed remainder for negative operands
         if (eval instanceof RealExpr || eval2 instanceof RealExpr)
             return z3.mkMod(toInt(eval), toInt(eval2));
         return z3.mkMod((IntExpr) eval, (IntExpr) eval2);

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java

@@ -53,10 +53,17 @@ void preservesRemainingBinderAfterSubstitution() {
     }
 
     @Test
-    void removesSourceNodeWhenItIsLastInChain() {
+    void keepsSourceNodeWhenItIsLastInChain() {
         VCImplication implication = vc("x > 0", "∀y:int. y == 1");
 
-        assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 0")));
+        assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 0"), expect("y == 1")));
+    }
+
+    @Test
+    void keepsReturnBinderWhenConclusionIsSeparate() {
+        VCImplication implication = vc("∀x:int. true", "∀#ret_8:int. #ret_8 == x + 1");
+
+        assertSimplificationSteps(substitution::apply, implication, chain(expect("true"), expect("#ret⁸ == x + 1")));
     }
 
     @Test