Fix Refinements After Early Return

Author: rcosta358

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

@@ -0,0 +1,15 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectEarlyReturn {
+
+    public static int divide(int a, @Refinement("b != 0") int b) {
+        return a / b;
+    }
+
+    public static void divideUnlessZero(int x, int y) {
+        if (y == 0) return;
+        divide(x, y);
+    }
+}

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

@@ -114,6 +114,7 @@ public <T> void visitCtConstructor(CtConstructor<T> constructor) {
         }
         contextHistory.saveContext(constructor, context);
         context.exitContext();
+        vcChecker.clearPathVariables();
     }
 
     public <R> void visitCtMethod(CtMethod<R> method) {
@@ -128,6 +129,7 @@ public <R> void visitCtMethod(CtMethod<R> method) {
         }
         contextHistory.saveContext(method, context);
         context.exitContext();
+        vcChecker.clearPathVariables();
     }
 
     @Override
@@ -409,30 +411,38 @@ public void visitCtIf(CtIf ifElement) {
         // VISIT THEN
         context.enterContext();
         visitCtBlock(ifElement.getThenStatement());
-        if (canCompleteNormally(ifElement.getThenStatement())) {
+        boolean thenCompletes = canCompleteNormally(ifElement.getThenStatement());
+        if (thenCompletes) {
             context.variablesSetThenIf();
         }
         contextHistory.saveContext(ifElement.getThenStatement(), context);
         context.exitContext();
 
         // VISIT ELSE
+        boolean elseCompletes = true;
         if (ifElement.getElseStatement() != null) {
             context.getVariableByName(pathVarName);
             context.newRefinementToVariableInContext(pathVarName, elseRefs);
 
             context.enterContext();
             visitCtBlock(ifElement.getElseStatement());
-            if (canCompleteNormally(ifElement.getElseStatement())) {
+            elseCompletes = canCompleteNormally(ifElement.getElseStatement());
+            if (elseCompletes) {
                 context.variablesSetElseIf();
             }
             contextHistory.saveContext(ifElement.getElseStatement(), context);
             context.exitContext();
         }
         // end
-        // Reset the path variable's refinement to the original condition after the if,
-        // so branch-local truth assertions (and any typestate they imply) don't leak past the join.
-        context.newRefinementToVariableInContext(pathVarName, expRefs);
-        vcChecker.removePathVariable(freshRV);
+        if (thenCompletes == elseCompletes) {
+            // Reset the path variable's refinement to the original condition after the if,
+            // so branch-local truth assertions (and any typestate they imply) don't leak past the join.
+            context.newRefinementToVariableInContext(pathVarName, expRefs);
+            vcChecker.removePathVariable(freshRV);
+        } else {
+            // Keep the refinement of the only branch that reaches the code after the if.
+            context.newRefinementToVariableInContext(pathVarName, thenCompletes ? thenRefs : elseRefs);
+        }
         context.exitContext();
         context.variablesCombineFromIf(expRefs);
         context.variablesFinishIfCombination();

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

@@ -353,6 +353,10 @@ public void removePathVariable(RefinedVariable rv) {
         pathVariables.remove(rv);
     }
 
+    void clearPathVariables() {
+        pathVariables.clear();
+    }
+
     void removePathVariableThatIncludes(String otherVar) {
         pathVariables.stream().filter(rv -> rv.getRefinement().getVariableNames().contains(otherVar)).toList()
                 .forEach(pathVariables::remove);