Skip to content

Commit 7a0b1fe

Browse files
rcosta358rcosta358
authored
Add VC Binder Simplification (#255)
1 parent 75f9487 commit 7a0b1fe

5 files changed

Lines changed: 232 additions & 3 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java‎

Lines changed: 118 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import java.util.ArrayList;
4+
import java.util.List;
5+
6+
import liquidjava.processor.SimplifiedVCImplication;
7+
import liquidjava.processor.VCImplication;
8+
import liquidjava.rj_language.Predicate;
9+
import liquidjava.rj_language.ast.Expression;
10+
import liquidjava.rj_language.ast.LiteralBoolean;
11+
12+
/**
13+
* Simplifies VCImplication chains by removing vacuous binder implications
14+
*/
15+
public class VCBinderSimplification implements VCSimplificationPass {
16+
17+
/**
18+
* Applies one binder simplification in a VC chain
19+
*/
20+
@Override
21+
public VCImplication apply(VCImplication implication) {
22+
VCImplication cloned = implication.clone();
23+
VCImplication simplified = simplify(cloned);
24+
return simplified == null ? cloned : simplified;
25+
}
26+
27+
/**
28+
* Simplifies the first applicable binder in a VC chain
29+
*/
30+
private VCImplication simplify(VCImplication implication) {
31+
if (implication == null)
32+
return null;
33+
34+
if (isFalseBinder(implication))
35+
return collapseFalseBinder(implication);
36+
37+
if (isTrueBinder(implication) && !containsVar(implication.getNext(), implication.getName()))
38+
return removeTrueBinder(implication);
39+
40+
VCImplication next = simplify(implication.getNext());
41+
if (next == null)
42+
return null;
43+
44+
VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone());
45+
result.setNext(next);
46+
return result;
47+
}
48+
49+
/**
50+
* Removes a true binder whose name is not used in the suffix
51+
*/
52+
private VCImplication removeTrueBinder(VCImplication implication) {
53+
VCImplication next = implication.getNext();
54+
55+
// ∀x. true => P -> P
56+
if (next != null) {
57+
VCImplication origin = new VCImplication(implication.getName(), implication.getType(),
58+
next.getOriginRefinement());
59+
VCImplication result = new SimplifiedVCImplication(next, next.getRefinement().clone(), origin);
60+
result.setNext(next.getNext() == null ? null : next.getNext().clone());
61+
return result;
62+
}
63+
64+
// ∀x. true -> true
65+
Predicate truePredicate = new Predicate(new LiteralBoolean(true));
66+
return new SimplifiedVCImplication(new VCImplication(truePredicate), truePredicate, implication);
67+
}
68+
69+
/**
70+
* Replaces a false binder implication with true
71+
*/
72+
private VCImplication collapseFalseBinder(VCImplication implication) {
73+
// ∀x. false => P -> true
74+
Predicate truePredicate = new Predicate(new LiteralBoolean(true));
75+
return new SimplifiedVCImplication(new VCImplication(truePredicate), truePredicate, implication);
76+
}
77+
78+
/**
79+
* Checks whether a VC node is a binder refined with true
80+
*/
81+
private boolean isTrueBinder(VCImplication implication) {
82+
return implication.hasBinder() && isTrue(implication.getRefinement().getExpression());
83+
}
84+
85+
/**
86+
* Checks whether a VC node is a binder refined with false
87+
*/
88+
private boolean isFalseBinder(VCImplication implication) {
89+
return implication.hasBinder() && isFalse(implication.getRefinement().getExpression());
90+
}
91+
92+
/**
93+
* Checks whether an expression is true
94+
*/
95+
private boolean isTrue(Expression expression) {
96+
return expression instanceof LiteralBoolean literal && literal.isBooleanTrue();
97+
}
98+
99+
/**
100+
* Checks whether an expression is false
101+
*/
102+
private boolean isFalse(Expression expression) {
103+
return expression instanceof LiteralBoolean literal && !literal.isBooleanTrue();
104+
}
105+
106+
/**
107+
* Checks whether a VC suffix contains a variable name
108+
*/
109+
private boolean containsVar(VCImplication implication, String name) {
110+
for (VCImplication current = implication; current != null; current = current.getNext()) {
111+
List<String> names = new ArrayList<>();
112+
current.getRefinement().getExpression().getVariableNames(names);
113+
if (names.contains(name))
114+
return true;
115+
}
116+
return false;
117+
}
118+
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@
99
*/
1010
public class VCSimplification {
1111

12-
private static final List<VCSimplificationPass> PASSES = List.of(new VCSubstitution(), new VCFolding(),
13-
new VCArithmeticSimplification(), new VCLogicalSimplification());
12+
private static final List<VCSimplificationPass> PASSES = List.of(new VCSubstitution(), new VCBinderSimplification(),
13+
new VCFolding(), new VCArithmeticSimplification(), new VCLogicalSimplification());
1414

1515
/**
1616
* Applies all available simplification steps to a VC chain until a fixed point is reached

‎liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderSimplificationTest.java‎

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import static liquidjava.utils.VCTestUtils.*;
4+
import static org.junit.jupiter.api.Assertions.assertFalse;
5+
6+
import liquidjava.processor.VCImplication;
7+
import org.junit.jupiter.api.Test;
8+
9+
class VCBinderSimplificationTest {
10+
11+
private final VCBinderSimplification binderSimplification = new VCBinderSimplification();
12+
13+
@Test
14+
void removesTrueBinderWhenVariableIsUnusedDownstream() {
15+
VCImplication implication = vc("∀x:int. true", "y > 0");
16+
17+
assertSimplificationSteps(binderSimplification::apply, implication, chain(expect("y > 0", "∀x:int. y > 0")));
18+
}
19+
20+
@Test
21+
void keepsTrueBinderWhenVariableIsUsedDownstream() {
22+
VCImplication implication = vc("∀x:int. true", "x > 0");
23+
24+
assertSimplificationSteps(binderSimplification::apply, implication,
25+
chain(expect("true", "∀x:int. true"), expect("x > 0", "x > 0")));
26+
}
27+
28+
@Test
29+
void collapsesFalseBinderSuffixToPlainTrue() {
30+
VCImplication implication = vc("∀x:int. false", "x > 0", "y > 0");
31+
VCImplication result = binderSimplification.apply(implication);
32+
33+
assertFalse(result.hasBinder());
34+
assertSimplifiedVC(result, expect("true", "∀x:int. false"));
35+
}
36+
37+
@Test
38+
void simplifiesOnlyFirstApplicableBinder() {
39+
VCImplication implication = vc("∀x:int. true", "∀y:int. true", "z > 0");
40+
41+
assertSimplificationSteps(binderSimplification::apply, implication,
42+
chain(expect("true", "∀x:int. true"), expect("z > 0", "z > 0")));
43+
}
44+
45+
@Test
46+
void skipsInapplicableTrueBinderAndSimplifiesLaterBinder() {
47+
VCImplication implication = vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0");
48+
49+
assertSimplificationSteps(binderSimplification::apply, implication,
50+
chain(expect("true", "∀x:int. true"), expect("x > 0", "x > 0"), expect("z > 0", "∀y:int. z > 0")));
51+
}
52+
53+
@Test
54+
void ignoresNonBinderBooleanLiterals() {
55+
VCImplication implication = vc("true", "false");
56+
57+
assertSimplificationSteps(binderSimplification::apply, implication,
58+
chain(expect("true", "true"), expect("false", "false")));
59+
}
60+
61+
@Test
62+
void trueBinderWithoutSuffixBecomesPlainTrue() {
63+
VCImplication implication = vc("∀x:int. true");
64+
VCImplication result = binderSimplification.apply(implication);
65+
66+
assertFalse(result.hasBinder());
67+
assertSimplifiedVC(result, expect("true", "∀x:int. true"));
68+
}
69+
}

‎liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ public VCImplicationGenerator() {
2121

2222
@Override
2323
public VCImplication generate(SourceOfRandomness random, GenerationStatus status) {
24-
return switch (random.nextInt(0, 12)) {
24+
return switch (random.nextInt(0, 14)) {
2525
case 0 -> vc(substitution(random, "x"), comparison(random, "x"));
2626
case 1 -> vc(reverseSubstitution(random, "x"), comparison(random, "x"));
2727
case 2 -> vc(nonSubstitution(random, "x"), substitution(random, "y"), comparison(random, "y"));
@@ -34,6 +34,8 @@ public VCImplication generate(SourceOfRandomness random, GenerationStatus status
3434
case 9 -> vc(arithmeticIdentity(random));
3535
case 10 -> guardedArithmeticIdentity(random);
3636
case 11 -> vc(logicalIdentity(random));
37+
case 12 -> vc(unusedTrueBinder(random));
38+
case 13 -> vc(falseBinder(random));
3739
default -> vc(substitution(random, "x"), substitution(random, "y"), foldableComparison(random));
3840
};
3941
}
@@ -60,6 +62,14 @@ private static String nonSubstitution(SourceOfRandomness random, String binder)
6062
return "∀" + binder + ":int. " + binder + " == " + binder + " " + signed(random.nextInt(1, 5));
6163
}
6264

65+
private static String[] unusedTrueBinder(SourceOfRandomness random) {
66+
return new String[] { "∀x:int. true", comparison(random, "a") };
67+
}
68+
69+
private static String[] falseBinder(SourceOfRandomness random) {
70+
return new String[] { "∀x:int. false", comparison(random, "x") };
71+
}
72+
6373
private static String comparison(SourceOfRandomness random, String preferredVar) {
6474
String left = random.nextBoolean() ? preferredVar : arithmetic(random, preferredVar);
6575
String right = random.nextBoolean() ? intLiteral(random)

‎liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,31 @@ void simplifyOnceDoesNotFoldAfterSubstitutionInSameStep() {
3636
chain(expect("true", "3 == 3")));
3737
}
3838

39+
@Test
40+
void simplifyOnceAppliesSubstitutionBeforeBinderSimplification() {
41+
VCImplication implication = vc("∀x:int. x == 3", "∀y:int. true", "x > 0");
42+
43+
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
44+
chain(expect("true", "∀y:int. true"), expect("3 > 0", "∀x:int. x > 0")),
45+
chain(expect("3 > 0", "∀y:int. x > 0")), chain(expect("true", "3 > 0")));
46+
}
47+
48+
@Test
49+
void simplifyOnceAppliesBinderSimplificationBeforeFolding() {
50+
VCImplication implication = vc("∀x:int. true", "1 + 2 > 0");
51+
52+
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
53+
chain(expect("1 + 2 > 0", "∀x:int. 1 + 2 > 0")), chain(expect("3 > 0", "1 + 2 > 0")));
54+
}
55+
56+
@Test
57+
void simplifyOnceAppliesBinderSimplificationBeforeLogicalSimplification() {
58+
VCImplication implication = vc("∀x:int. true", "y && true");
59+
60+
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
61+
chain(expect("y && true", "∀x:int. y && true")), chain(expect("y", "y && true")));
62+
}
63+
3964
@Test
4065
void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() {
4166
VCImplication implication = vc("1 + 2 > 2");
@@ -91,6 +116,13 @@ void simplifyKeepsApplyingStepsUntilFixedPoint() {
91116
chain(expect("4 > 3", "3 + 1 > 3")), chain(expect("true", "4 > 3")));
92117
}
93118

119+
@Test
120+
void simplifyToFixedPointRemovesTrueBindersOverMultipleSteps() {
121+
VCImplication implication = vc("∀x:int. true", "∀y:int. true", "z > 0");
122+
123+
assertSimplifiedVC(VCSimplification.simplifyToFixedPoint(implication), expect("z > 0", "∀y:int. z > 0"));
124+
}
125+
94126
@Test
95127
void simplifyAppliesMultipleSubstitutionsBeforeReachingFixedPoint() {
96128
VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x");

0 commit comments

Comments
 (0)