Skip to content

Commit 3ae3e9b

Browse files
CatarinaGamboaCatarinaGamboa
committed
Preserve skipped paths for boolean if conditions
1 parent dcfc4eb commit 3ae3e9b

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)