diff --git a/liquidjava-example/src/main/java/testSuite/CorrectBareBooleanIf.java b/liquidjava-example/src/main/java/testSuite/CorrectBareBooleanIf.java new file mode 100644 index 00000000..23379e7d --- /dev/null +++ b/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(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBareBooleanIfCall.java b/liquidjava-example/src/main/java/testSuite/ErrorBareBooleanIfCall.java new file mode 100644 index 00000000..089bb502 --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBareBooleanIfIndependentConstraint.java b/liquidjava-example/src/main/java/testSuite/ErrorBareBooleanIfIndependentConstraint.java new file mode 100644 index 00000000..84e2d795 --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBareBooleanIfUnknownCall.java b/liquidjava-example/src/main/java/testSuite/ErrorBareBooleanIfUnknownCall.java new file mode 100644 index 00000000..d4468b64 --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBareBooleanIfVariable.java b/liquidjava-example/src/main/java/testSuite/ErrorBareBooleanIfVariable.java new file mode 100644 index 00000000..9bd4b86c --- /dev/null +++ b/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 + } +} 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 0810c24d..bfbcca34 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 @@ -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(); }