Skip to content

Commit 37c3594

Browse files
CatarinaGamboaCatarinaGamboa
authored
Preserve skipped paths for boolean if conditions (#382)
An `if (again) { r.reopen(); }` following `r.close()` previously allowed `r.use()` even though the skipped branch leaves `r` closed. The join used the condition's refinement relation as its guard, which made the then branch appear selected whenever that relation held. Keep expression value constraints separate from the boolean guard used for branch assumptions and state joins. Unannotated calls and calls with constraints independent of their return value retain both possible outcomes. Preserve the value constraints after the join without asserting that the condition is true. Regression examples cover unsafe boolean variables, refined calls, unannotated calls, and calls with independent constraints; passing examples cover known true and false values, negation, repeated guards, and safe joins with and without an explicit else. Validation: `./mvnw -pl liquidjava-verifier -am test -Dsurefire.failIfNoSpecifiedTests=false` passes on main including #366. All five new fixtures also pass when run directly after rebasing. Fixes #371.
1 parent dcfc4eb commit 37c3594

6 files changed

Lines changed: 212 additions & 40 deletions

File tree

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

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
7+
// Regression for issue #371: preserve both outcomes of a boolean condition.
8+
@StateSet({"open", "closed"})
9+
public class CorrectBareBooleanIf {
10+
@StateRefinement(to = "open(this)")
11+
public CorrectBareBooleanIf() {}
12+
@StateRefinement(to = "open(this)")
13+
public void reopen() {}
14+
@StateRefinement(to = "closed(this)")
15+
public void close() {}
16+
@StateRefinement(from = "open(this)")
17+
public void use() {}
18+
19+
@Refinement("_ == value")
20+
public static boolean identity(boolean value) { return value; }
21+
22+
public static void bothPathsSafe(boolean again) {
23+
CorrectBareBooleanIf r = new CorrectBareBooleanIf();
24+
if (again) {
25+
r.reopen();
26+
}
27+
r.use();
28+
}
29+
30+
public static void knownTrue() {
31+
CorrectBareBooleanIf r = new CorrectBareBooleanIf();
32+
r.close();
33+
boolean again = true;
34+
if (again) {
35+
r.reopen();
36+
}
37+
r.use();
38+
}
39+
40+
public static void knownFalseCall() {
41+
CorrectBareBooleanIf r = new CorrectBareBooleanIf();
42+
if (identity(false)) {
43+
r.close();
44+
}
45+
r.use();
46+
}
47+
48+
public static void negatedKnownFalse() {
49+
CorrectBareBooleanIf r = new CorrectBareBooleanIf();
50+
r.close();
51+
boolean again = false;
52+
if (!again) {
53+
r.reopen();
54+
}
55+
r.use();
56+
}
57+
58+
public static void guardedUse(boolean again) {
59+
CorrectBareBooleanIf r = new CorrectBareBooleanIf();
60+
r.close();
61+
if (again) {
62+
r.reopen();
63+
}
64+
if (again) {
65+
r.use();
66+
}
67+
}
68+
69+
public static void explicitElse(boolean again) {
70+
CorrectBareBooleanIf r = new CorrectBareBooleanIf();
71+
r.close();
72+
if (again) {
73+
r.reopen();
74+
} else {
75+
r.reopen();
76+
}
77+
r.use();
78+
}
79+
}

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

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
7+
// Regression for issue #371: preserve both outcomes of a boolean condition.
8+
@StateSet({"open", "closed"})
9+
public class ErrorBareBooleanIfCall {
10+
@StateRefinement(to = "open(this)")
11+
public ErrorBareBooleanIfCall() {}
12+
@StateRefinement(to = "open(this)")
13+
public void reopen() {}
14+
@StateRefinement(to = "closed(this)")
15+
public void close() {}
16+
@StateRefinement(from = "open(this)")
17+
public void use() {}
18+
@Refinement("_ == value")
19+
public static boolean identity(boolean value) { return value; }
20+
21+
public static void check(boolean again) {
22+
ErrorBareBooleanIfCall r = new ErrorBareBooleanIfCall();
23+
r.close();
24+
if (identity(again)) {
25+
r.reopen();
26+
}
27+
r.use(); // Expect: State Refinement Error
28+
}
29+
}

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

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
7+
// Regression for issue #371: preserve both outcomes of a boolean condition.
8+
@StateSet({"open", "closed"})
9+
public class ErrorBareBooleanIfIndependentConstraint {
10+
@StateRefinement(to = "open(this)")
11+
public ErrorBareBooleanIfIndependentConstraint() {}
12+
@StateRefinement(to = "open(this)")
13+
public void reopen() {}
14+
@StateRefinement(to = "closed(this)")
15+
public void close() {}
16+
@StateRefinement(from = "open(this)")
17+
public void use() {}
18+
19+
@Refinement("n > 0")
20+
public static boolean query(@Refinement("_ > 0") int n, boolean value) { return value; }
21+
22+
public static void check(boolean again) {
23+
ErrorBareBooleanIfIndependentConstraint r = new ErrorBareBooleanIfIndependentConstraint();
24+
r.close();
25+
if (query(1, again)) {
26+
r.reopen();
27+
}
28+
r.use(); // Expect: State Refinement Error
29+
}
30+
}

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

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateRefinement;
4+
import liquidjava.specification.StateSet;
5+
6+
// Regression for issue #371: preserve both outcomes of a boolean condition.
7+
@StateSet({"open", "closed"})
8+
public class ErrorBareBooleanIfUnknownCall {
9+
@StateRefinement(to = "open(this)")
10+
public ErrorBareBooleanIfUnknownCall() {}
11+
@StateRefinement(to = "open(this)")
12+
public void reopen() {}
13+
@StateRefinement(to = "closed(this)")
14+
public void close() {}
15+
@StateRefinement(from = "open(this)")
16+
public void use() {}
17+
public static boolean unknown(boolean value) { return value; }
18+
19+
public static void check(boolean again) {
20+
ErrorBareBooleanIfUnknownCall r = new ErrorBareBooleanIfUnknownCall();
21+
r.close();
22+
if (unknown(again)) {
23+
r.reopen();
24+
}
25+
r.use(); // Expect: State Refinement Error
26+
}
27+
}

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

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateRefinement;
4+
import liquidjava.specification.StateSet;
5+
6+
// Regression for issue #371: preserve both outcomes of a boolean condition.
7+
@StateSet({"open", "closed"})
8+
public class ErrorBareBooleanIfVariable {
9+
@StateRefinement(to = "open(this)")
10+
public ErrorBareBooleanIfVariable() {}
11+
@StateRefinement(to = "open(this)")
12+
public void reopen() {}
13+
@StateRefinement(to = "closed(this)")
14+
public void close() {}
15+
@StateRefinement(from = "open(this)")
16+
public void use() {}
17+
18+
public static void check(boolean again) {
19+
ErrorBareBooleanIfVariable r = new ErrorBareBooleanIfVariable();
20+
r.close();
21+
if (again) {
22+
r.reopen();
23+
}
24+
r.use(); // Expect: State Refinement Error
25+
}
26+
}

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

Lines changed: 21 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -406,46 +406,27 @@ public void visitCtIf(CtIf ifElement) {
406406
Predicate expRefs = getExpressionRefinements(exp);
407407

408408
String pathVarName = String.format(Formats.FRESH, context.getCounter());
409-
RefinedVariable freshRV;
410-
411-
// When the condition's predicate uses Keys.WILDCARD as a stand-in for its boolean value (e.g. _ == true -->
412-
// state(this) or _ == k), the fresh path variable IS that value — assert it true in the then branch and false
413-
// in the else, since negating the whole predicate is unsound for implications and equality forms.
414-
boolean valueIsCondition = false;
415-
Predicate thenRefs;
416-
Predicate elseRefs;
417-
if (isUninformativeCondition(expRefs, exp)) {
418-
// No refinement means the condition is unknown, not true: model it as a fresh
419-
// boolean so the SMT solver may pick either truth value for each branch.
420-
expRefs = Predicate.createVar(pathVarName);
421-
thenRefs = expRefs;
422-
elseRefs = expRefs.negate();
423-
freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, new Predicate(), exp);
424-
} else {
425-
valueIsCondition = expRefs.getVariableNames().contains(Keys.WILDCARD);
426-
expRefs = expRefs.substituteVariable(Keys.WILDCARD, pathVarName);
427-
Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs);
428-
expRefs = Predicate.createConjunction(expRefs, lastExpRefs);
429-
430-
// TODO Change in future
431-
if (expRefs.getVariableNames().contains("null")) {
432-
expRefs = new Predicate();
433-
valueIsCondition = false;
434-
}
435-
436-
thenRefs = expRefs;
437-
elseRefs = expRefs.negate();
438-
if (valueIsCondition) {
439-
Predicate freshIsTrue = Predicate.createEquals(Predicate.createVar(pathVarName),
440-
Predicate.createLit("true", Types.BOOLEAN));
441-
Predicate freshIsFalse = Predicate.createEquals(Predicate.createVar(pathVarName),
442-
Predicate.createLit("false", Types.BOOLEAN));
443-
thenRefs = Predicate.createConjunction(expRefs, freshIsTrue);
444-
elseRefs = Predicate.createConjunction(expRefs, freshIsFalse);
445-
}
446-
447-
freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp);
409+
// A value refinement constrains the result of evaluating the expression; it is not
410+
// itself the truth value selecting the branch. Calls without a wildcard likewise
411+
// provide no information about their boolean result.
412+
boolean valueIsCondition = expRefs.getVariableNames().contains(Keys.WILDCARD) || exp instanceof CtInvocation<?>
413+
|| isUninformativeCondition(expRefs, exp);
414+
expRefs = expRefs.substituteVariable(Keys.WILDCARD, pathVarName);
415+
Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs);
416+
expRefs = Predicate.createConjunction(expRefs, lastExpRefs);
417+
418+
// TODO Change in future
419+
if (expRefs.getVariableNames().contains("null")) {
420+
expRefs = new Predicate();
421+
valueIsCondition = true;
448422
}
423+
424+
Predicate branchGuard = valueIsCondition ? Predicate.createVar(pathVarName) : expRefs;
425+
Predicate thenRefs = valueIsCondition ? Predicate.createConjunction(expRefs, branchGuard) : branchGuard;
426+
Predicate elseRefs = valueIsCondition ? Predicate.createConjunction(expRefs, branchGuard.negate())
427+
: branchGuard.negate();
428+
RefinedVariable freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs,
429+
exp);
449430
vcChecker.addPathVariable(freshRV);
450431

451432
context.variablesNewIfCombination();
@@ -488,7 +469,7 @@ public void visitCtIf(CtIf ifElement) {
488469
context.newRefinementToVariableInContext(pathVarName, thenCompletes ? thenRefs : elseRefs);
489470
}
490471
context.exitContext();
491-
context.variablesCombineFromIf(expRefs);
472+
context.variablesCombineFromIf(branchGuard);
492473
context.variablesFinishIfCombination();
493474
}
494475

0 commit comments

Comments
 (0)