Preserve skipped paths for boolean if conditions

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

@@ -0,0 +1,79 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// Regression for issue #371: preserve both outcomes of a boolean condition.
+@StateSet({"open", "closed"})
+public class CorrectBareBooleanIf {
+    @StateRefinement(to = "open(this)")
+    public CorrectBareBooleanIf() {}
+    @StateRefinement(to = "open(this)")
+    public void reopen() {}
+    @StateRefinement(to = "closed(this)")
+    public void close() {}
+    @StateRefinement(from = "open(this)")
+    public void use() {}
+
+    @Refinement("_ == value")
+    public static boolean identity(boolean value) { return value; }
+
+    public static void bothPathsSafe(boolean again) {
+        CorrectBareBooleanIf r = new CorrectBareBooleanIf();
+        if (again) {
+            r.reopen();
+        }
+        r.use();
+    }
+
+    public static void knownTrue() {
+        CorrectBareBooleanIf r = new CorrectBareBooleanIf();
+        r.close();
+        boolean again = true;
+        if (again) {
+            r.reopen();
+        }
+        r.use();
+    }
+
+    public static void knownFalseCall() {
+        CorrectBareBooleanIf r = new CorrectBareBooleanIf();
+        if (identity(false)) {
+            r.close();
+        }
+        r.use();
+    }
+
+    public static void negatedKnownFalse() {
+        CorrectBareBooleanIf r = new CorrectBareBooleanIf();
+        r.close();
+        boolean again = false;
+        if (!again) {
+            r.reopen();
+        }
+        r.use();
+    }
+
+    public static void guardedUse(boolean again) {
+        CorrectBareBooleanIf r = new CorrectBareBooleanIf();
+        r.close();
+        if (again) {
+            r.reopen();
+        }
+        if (again) {
+            r.use();
+        }
+    }
+
+    public static void explicitElse(boolean again) {
+        CorrectBareBooleanIf r = new CorrectBareBooleanIf();
+        r.close();
+        if (again) {
+            r.reopen();
+        } else {
+            r.reopen();
+        }
+        r.use();
+    }
+}

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

@@ -0,0 +1,29 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// Regression for issue #371: preserve both outcomes of a boolean condition.
+@StateSet({"open", "closed"})
+public class ErrorBareBooleanIfCall {
+    @StateRefinement(to = "open(this)")
+    public ErrorBareBooleanIfCall() {}
+    @StateRefinement(to = "open(this)")
+    public void reopen() {}
+    @StateRefinement(to = "closed(this)")
+    public void close() {}
+    @StateRefinement(from = "open(this)")
+    public void use() {}
+    @Refinement("_ == value")
+    public static boolean identity(boolean value) { return value; }
+
+    public static void check(boolean again) {
+        ErrorBareBooleanIfCall r = new ErrorBareBooleanIfCall();
+        r.close();
+        if (identity(again)) {
+            r.reopen();
+        }
+        r.use(); // Expect: State Refinement Error
+    }
+}

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

@@ -0,0 +1,30 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// Regression for issue #371: preserve both outcomes of a boolean condition.
+@StateSet({"open", "closed"})
+public class ErrorBareBooleanIfIndependentConstraint {
+    @StateRefinement(to = "open(this)")
+    public ErrorBareBooleanIfIndependentConstraint() {}
+    @StateRefinement(to = "open(this)")
+    public void reopen() {}
+    @StateRefinement(to = "closed(this)")
+    public void close() {}
+    @StateRefinement(from = "open(this)")
+    public void use() {}
+
+    @Refinement("n > 0")
+    public static boolean query(@Refinement("_ > 0") int n, boolean value) { return value; }
+
+    public static void check(boolean again) {
+        ErrorBareBooleanIfIndependentConstraint r = new ErrorBareBooleanIfIndependentConstraint();
+        r.close();
+        if (query(1, again)) {
+            r.reopen();
+        }
+        r.use(); // Expect: State Refinement Error
+    }
+}

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

@@ -0,0 +1,27 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// Regression for issue #371: preserve both outcomes of a boolean condition.
+@StateSet({"open", "closed"})
+public class ErrorBareBooleanIfUnknownCall {
+    @StateRefinement(to = "open(this)")
+    public ErrorBareBooleanIfUnknownCall() {}
+    @StateRefinement(to = "open(this)")
+    public void reopen() {}
+    @StateRefinement(to = "closed(this)")
+    public void close() {}
+    @StateRefinement(from = "open(this)")
+    public void use() {}
+    public static boolean unknown(boolean value) { return value; }
+
+    public static void check(boolean again) {
+        ErrorBareBooleanIfUnknownCall r = new ErrorBareBooleanIfUnknownCall();
+        r.close();
+        if (unknown(again)) {
+            r.reopen();
+        }
+        r.use(); // Expect: State Refinement Error
+    }
+}

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

@@ -0,0 +1,26 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// Regression for issue #371: preserve both outcomes of a boolean condition.
+@StateSet({"open", "closed"})
+public class ErrorBareBooleanIfVariable {
+    @StateRefinement(to = "open(this)")
+    public ErrorBareBooleanIfVariable() {}
+    @StateRefinement(to = "open(this)")
+    public void reopen() {}
+    @StateRefinement(to = "closed(this)")
+    public void close() {}
+    @StateRefinement(from = "open(this)")
+    public void use() {}
+
+    public static void check(boolean again) {
+        ErrorBareBooleanIfVariable r = new ErrorBareBooleanIfVariable();
+        r.close();
+        if (again) {
+            r.reopen();
+        }
+        r.use(); // Expect: State Refinement Error
+    }
+}

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

@@ -406,46 +406,27 @@ public void visitCtIf(CtIf ifElement) {
         Predicate expRefs = getExpressionRefinements(exp);
 
         String pathVarName = String.format(Formats.FRESH, context.getCounter());
-        RefinedVariable freshRV;
-
-        // When the condition's predicate uses Keys.WILDCARD as a stand-in for its boolean value (e.g. _ == true -->
-        // state(this) or _ == k), the fresh path variable IS that value — assert it true in the then branch and false
-        // in the else, since negating the whole predicate is unsound for implications and equality forms.
-        boolean valueIsCondition = false;
-        Predicate thenRefs;
-        Predicate elseRefs;
-        if (isUninformativeCondition(expRefs, exp)) {
-            // No refinement means the condition is unknown, not true: model it as a fresh
-            // boolean so the SMT solver may pick either truth value for each branch.
-            expRefs = Predicate.createVar(pathVarName);
-            thenRefs = expRefs;
-            elseRefs = expRefs.negate();
-            freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, new Predicate(), exp);
-        } else {
-            valueIsCondition = expRefs.getVariableNames().contains(Keys.WILDCARD);
-            expRefs = expRefs.substituteVariable(Keys.WILDCARD, pathVarName);
-            Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs);
-            expRefs = Predicate.createConjunction(expRefs, lastExpRefs);
-
-            // TODO Change in future
-            if (expRefs.getVariableNames().contains("null")) {
-                expRefs = new Predicate();
-                valueIsCondition = false;
-            }
-
-            thenRefs = expRefs;
-            elseRefs = expRefs.negate();
-            if (valueIsCondition) {
-                Predicate freshIsTrue = Predicate.createEquals(Predicate.createVar(pathVarName),
-                        Predicate.createLit("true", Types.BOOLEAN));
-                Predicate freshIsFalse = Predicate.createEquals(Predicate.createVar(pathVarName),
-                        Predicate.createLit("false", Types.BOOLEAN));
-                thenRefs = Predicate.createConjunction(expRefs, freshIsTrue);
-                elseRefs = Predicate.createConjunction(expRefs, freshIsFalse);
-            }
-
-            freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp);
+        // A value refinement constrains the result of evaluating the expression; it is not
+        // itself the truth value selecting the branch. Calls without a wildcard likewise
+        // provide no information about their boolean result.
+        boolean valueIsCondition = expRefs.getVariableNames().contains(Keys.WILDCARD) || exp instanceof CtInvocation<?>
+                || isUninformativeCondition(expRefs, exp);
+        expRefs = expRefs.substituteVariable(Keys.WILDCARD, pathVarName);
+        Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs);
+        expRefs = Predicate.createConjunction(expRefs, lastExpRefs);
+
+        // TODO Change in future
+        if (expRefs.getVariableNames().contains("null")) {
+            expRefs = new Predicate();
+            valueIsCondition = true;
         }
+
+        Predicate branchGuard = valueIsCondition ? Predicate.createVar(pathVarName) : expRefs;
+        Predicate thenRefs = valueIsCondition ? Predicate.createConjunction(expRefs, branchGuard) : branchGuard;
+        Predicate elseRefs = valueIsCondition ? Predicate.createConjunction(expRefs, branchGuard.negate())
+                : branchGuard.negate();
+        RefinedVariable freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs,
+                exp);
         vcChecker.addPathVariable(freshRV);
 
         context.variablesNewIfCombination();
@@ -488,7 +469,7 @@ public void visitCtIf(CtIf ifElement) {
             context.newRefinementToVariableInContext(pathVarName, thenCompletes ? thenRefs : elseRefs);
         }
         context.exitContext();
-        context.variablesCombineFromIf(expRefs);
+        context.variablesCombineFromIf(branchGuard);
         context.variablesFinishIfCombination();
     }