Skip to content

Commit 08ec730

Browse files
rcosta358rcosta358
committed
Refactoring
1 parent ea7ad09 commit 08ec730

9 files changed

Lines changed: 187 additions & 240 deletions

File tree

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

Lines changed: 19 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -21,32 +21,35 @@ public static VCSimplificationResult simplifyToFixedPoint(VCImplication implicat
2121

2222
VCSimplificationResult current = new VCSimplificationResult(implication);
2323
while (true) {
24-
VCSimplificationResult simplified = simplifyOnce(current.getImplication(), current);
25-
if (simplified.getOrigin() == null)
24+
VCSimplificationResult simplified = simplifyOnce(current);
25+
if (simplified == current)
2626
return current; // fixed point reached
2727
current = simplified;
2828
}
2929
}
3030

3131
/**
32-
* Applies one simplification step to a VC chain
32+
* Applies one simplification step to a VC chain from all available simplification passes
3333
*/
34-
public static VCSimplificationResult simplifyOnce(VCImplication implication) {
35-
if (implication == null)
36-
return null;
37-
38-
return simplifyOnce(implication, new VCSimplificationResult(implication));
34+
public static VCSimplificationResult simplifyOnce(VCSimplificationResult implication) {
35+
for (VCSimplificationPass pass : PASSES) {
36+
VCSimplificationResult simplified = simplifyOnce(implication, pass);
37+
if (simplified != implication)
38+
return simplified;
39+
}
40+
return implication;
3941
}
4042

4143
/**
42-
* Applies one simplification step to a VC chain, keeping track of the origin of the simplification
44+
* Applies one selected simplification pass to a VC chain
4345
*/
44-
private static VCSimplificationResult simplifyOnce(VCImplication implication, VCSimplificationResult origin) {
45-
for (VCSimplificationPass pass : PASSES) {
46-
VCImplication simplified = pass.apply(implication);
47-
if (!implication.equals(simplified))
48-
return new VCSimplificationResult(simplified, origin);
49-
}
50-
return new VCSimplificationResult(implication);
46+
public static VCSimplificationResult simplifyOnce(VCSimplificationResult implication, VCSimplificationPass pass) {
47+
if (implication == null)
48+
return null;
49+
50+
VCImplication simplified = pass.apply(implication.getImplication());
51+
if (implication.getImplication().equals(simplified))
52+
return implication;
53+
return new VCSimplificationResult(simplified, implication);
5154
}
5255
}

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

Lines changed: 24 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -10,60 +10,55 @@ class VCArithmeticSimplificationTest {
1010

1111
@Test
1212
void simplifiesAdditiveIdentities() {
13-
assertSimplificationSteps(simplification::apply, vc("x + 0 > 0"), chain(expect("x > 0", "x + 0 > 0")));
14-
assertSimplificationSteps(simplification::apply, vc("0 + x > 0"), chain(expect("x > 0", "0 + x > 0")));
15-
assertSimplificationSteps(simplification::apply, vc("x - 0 > 0"), chain(expect("x > 0", "x - 0 > 0")));
16-
assertSimplificationSteps(simplification::apply, vc("0 - x > 0"), chain(expect("-x > 0", "0 - x > 0")));
13+
assertSimplificationSteps(simplification, vc("x + 0 > 0"), step("x > 0"));
14+
assertSimplificationSteps(simplification, vc("0 + x > 0"), step("x > 0"));
15+
assertSimplificationSteps(simplification, vc("x - 0 > 0"), step("x > 0"));
16+
assertSimplificationSteps(simplification, vc("0 - x > 0"), step("-x > 0"));
1717
}
1818

1919
@Test
2020
void simplifiesNegatedAdditionAndSubtraction() {
21-
assertSimplificationSteps(simplification::apply, vc("x + -x == 0"), chain(expect("0 == 0", "x + -x == 0")));
22-
assertSimplificationSteps(simplification::apply, vc("-x + x == 0"), chain(expect("0 == 0", "-x + x == 0")));
23-
assertSimplificationSteps(simplification::apply, vc("x - x == 0"), chain(expect("0 == 0", "x - x == 0")));
24-
assertSimplificationSteps(simplification::apply, vc("--x == x"), chain(expect("x == x", "-(-x) == x")));
25-
assertSimplificationSteps(simplification::apply, vc("x + -y == 0"), chain(expect("x - y == 0", "x + -y == 0")));
26-
assertSimplificationSteps(simplification::apply, vc("x - -y == 0"), chain(expect("x + y == 0", "x - -y == 0")));
21+
assertSimplificationSteps(simplification, vc("x + -x == 0"), step("0 == 0"));
22+
assertSimplificationSteps(simplification, vc("-x + x == 0"), step("0 == 0"));
23+
assertSimplificationSteps(simplification, vc("x - x == 0"), step("0 == 0"));
24+
assertSimplificationSteps(simplification, vc("--x == x"), step("x == x"));
25+
assertSimplificationSteps(simplification, vc("x + -y == 0"), step("x - y == 0"));
26+
assertSimplificationSteps(simplification, vc("x - -y == 0"), step("x + y == 0"));
2727
}
2828

2929
@Test
3030
void simplifiesMultiplicativeIdentities() {
31-
assertSimplificationSteps(simplification::apply, vc("x * 1 > 0"), chain(expect("x > 0", "x * 1 > 0")));
32-
assertSimplificationSteps(simplification::apply, vc("1 * x > 0"), chain(expect("x > 0", "1 * x > 0")));
33-
assertSimplificationSteps(simplification::apply, vc("x * 0 == 0"), chain(expect("0 == 0", "x * 0 == 0")));
34-
assertSimplificationSteps(simplification::apply, vc("0 * x == 0"), chain(expect("0 == 0", "0 * x == 0")));
35-
assertSimplificationSteps(simplification::apply, vc("x / 1 > 0"), chain(expect("x > 0", "x / 1 > 0")));
36-
assertSimplificationSteps(simplification::apply, vc("x % 1 == 0"), chain(expect("0 == 0", "x % 1 == 0")));
31+
assertSimplificationSteps(simplification, vc("x * 1 > 0"), step("x > 0"));
32+
assertSimplificationSteps(simplification, vc("1 * x > 0"), step("x > 0"));
33+
assertSimplificationSteps(simplification, vc("x * 0 == 0"), step("0 == 0"));
34+
assertSimplificationSteps(simplification, vc("0 * x == 0"), step("0 == 0"));
35+
assertSimplificationSteps(simplification, vc("x / 1 > 0"), step("x > 0"));
36+
assertSimplificationSteps(simplification, vc("x % 1 == 0"), step("0 == 0"));
3737
}
3838

3939
@Test
4040
void simplifiesGuardedDivisionAndModuloIdentities() {
41-
assertSimplificationSteps(simplification::apply, vc("x != 0", "0 / x == 0"),
42-
chain(expect("x != 0"), expect("0 == 0", "0 / x == 0")));
43-
assertSimplificationSteps(simplification::apply, vc("x != 0", "x / x == 1"),
44-
chain(expect("x != 0"), expect("1 == 1", "x / x == 1")));
45-
assertSimplificationSteps(simplification::apply, vc("0 != x", "x % x == 0"),
46-
chain(expect("0 != x"), expect("0 == 0", "x % x == 0")));
41+
assertSimplificationSteps(simplification, vc("x != 0", "0 / x == 0"), step("x != 0", "0 == 0"));
42+
assertSimplificationSteps(simplification, vc("x != 0", "x / x == 1"), step("x != 0", "1 == 1"));
43+
assertSimplificationSteps(simplification, vc("0 != x", "x % x == 0"), step("0 != x", "0 == 0"));
4744
}
4845

4946
@Test
5047
void leavesUnguardedDivisionAndModuloIdentitiesUnchanged() {
51-
assertSimplificationSteps(simplification::apply, vc("0 / x == 0"), chain(expect("0 / x == 0")));
52-
assertSimplificationSteps(simplification::apply, vc("x / x == 1"), chain(expect("x / x == 1")));
53-
assertSimplificationSteps(simplification::apply, vc("x % x == 0"), chain(expect("x % x == 0")));
48+
assertSimplificationSteps(simplification, vc("0 / x == 0"), step("0 / x == 0"));
49+
assertSimplificationSteps(simplification, vc("x / x == 1"), step("x / x == 1"));
50+
assertSimplificationSteps(simplification, vc("x % x == 0"), step("x % x == 0"));
5451
}
5552

5653
@Test
5754
void simplifiesOnlyFirstArithmeticIdentity() {
58-
assertSimplificationSteps(simplification::apply, vc("x + 0 + 1 > 0"),
59-
chain(expect("x + 1 > 0", "x + 0 + 1 > 0")));
55+
assertSimplificationSteps(simplification, vc("x + 0 + 1 > 0"), step("x + 1 > 0"));
6056
}
6157

6258
@Test
6359
void recordsOriginWhenSimplifyingLaterImplication() {
6460
VCImplication implication = vc("x > 0", "y + 0 > x");
6561

66-
assertSimplificationSteps(simplification::apply, implication,
67-
chain(expect("x > 0"), expect("y > x", "y + 0 > x")));
62+
assertSimplificationSteps(simplification, implication, step("x > 0", "y > x"));
6863
}
6964
}

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

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -14,14 +14,14 @@ class VCBinderSimplificationTest {
1414
void removesTrueBinderWhenVariableIsUnusedDownstream() {
1515
VCImplication implication = vc("∀x:int. true", "y > 0");
1616

17-
assertSimplificationSteps(binderSimplification::apply, implication, chain(expect("y > 0", "∀x:int. y > 0")));
17+
assertSimplificationSteps(binderSimplification, implication, step("y > 0"));
1818
}
1919

2020
@Test
2121
void keepsTrueBinderWhenVariableIsUsedDownstream() {
2222
VCImplication implication = vc("∀x:int. true", "x > 0");
2323

24-
assertSimplificationSteps(binderSimplification::apply, implication, chain(expect("true"), expect("x > 0")));
24+
assertSimplificationSteps(binderSimplification, implication, step("true", "x > 0"));
2525
}
2626

2727
@Test
@@ -30,30 +30,28 @@ void collapsesFalseBinderSuffixToPlainTrue() {
3030
VCImplication result = binderSimplification.apply(implication);
3131

3232
assertFalse(result.hasBinder());
33-
assertSimplifiedVC(result, expect("true", "∀x:int. false"));
33+
assertSimplifiedVC(result, "true");
3434
}
3535

3636
@Test
3737
void simplifiesOnlyFirstApplicableBinder() {
3838
VCImplication implication = vc("∀x:int. true", "∀y:int. true", "z > 0");
3939

40-
assertSimplificationSteps(binderSimplification::apply, implication,
41-
chain(expect("true", "∀x:int. true"), expect("z > 0")));
40+
assertSimplificationSteps(binderSimplification, implication, step("true", "z > 0"));
4241
}
4342

4443
@Test
4544
void skipsInapplicableTrueBinderAndSimplifiesLaterBinder() {
4645
VCImplication implication = vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0");
4746

48-
assertSimplificationSteps(binderSimplification::apply, implication,
49-
chain(expect("true"), expect("x > 0"), expect("z > 0", "∀y:int. z > 0")));
47+
assertSimplificationSteps(binderSimplification, implication, step("true", "x > 0", "z > 0"));
5048
}
5149

5250
@Test
5351
void ignoresNonBinderBooleanLiterals() {
5452
VCImplication implication = vc("true", "false");
5553

56-
assertSimplificationSteps(binderSimplification::apply, implication, chain(expect("true"), expect("false")));
54+
assertSimplificationSteps(binderSimplification, implication, step("true", "false"));
5755
}
5856

5957
@Test
@@ -62,6 +60,6 @@ void trueBinderWithoutSuffixBecomesPlainTrue() {
6260
VCImplication result = binderSimplification.apply(implication);
6361

6462
assertFalse(result.hasBinder());
65-
assertSimplifiedVC(result, expect("true", "∀x:int. true"));
63+
assertSimplifiedVC(result, "true");
6664
}
6765
}

0 commit comments

Comments
 (0)