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

@@ -409,30 +409,35 @@ 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) {
+            context.newRefinementToVariableInContext(pathVarName, expRefs);
+            vcChecker.removePathVariable(freshRV);
+        } else {
+            context.newRefinementToVariableInContext(pathVarName, thenCompletes ? thenRefs : elseRefs);
+        }
         context.exitContext();
         context.variablesCombineFromIf(expRefs);
         context.variablesFinishIfCombination();