Skip to content

Commit 5fbcef7

Browse files
rcosta358rcosta358
committed
Return Null Origin for Unsimplified VCs
1 parent 8588a9d commit 5fbcef7

8 files changed

Lines changed: 50 additions & 48 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -33,11 +33,14 @@ public VCImplication(VCImplication implication, Predicate ref) {
3333
}
3434

3535
public VCImplication getOrigin() {
36-
return new VCImplication(this, refinement.clone());
36+
return null;
3737
}
3838

3939
public Predicate getOriginRefinement() {
40-
return getOrigin().getRefinement().clone();
40+
VCImplication origin = getOrigin();
41+
if (origin == null)
42+
return refinement.clone();
43+
return origin.getRefinement().clone();
4144
}
4245

4346
public VCImplication copyWithRefinement(Predicate refinement) {

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -43,18 +43,18 @@ void simplifiesMultiplicativeIdentities() {
4343
@Test
4444
void simplifiesGuardedDivisionAndModuloIdentities() {
4545
assertSimplificationSteps(simplification::apply, vc("x != 0", "0 / x == 0"),
46-
chain(expect("x != 0", "x != 0"), expect("0 == 0", "0 / x == 0")));
46+
chain(expect("x != 0"), expect("0 == 0", "0 / x == 0")));
4747
assertSimplificationSteps(simplification::apply, vc("x != 0", "x / x == 1"),
48-
chain(expect("x != 0", "x != 0"), expect("1 == 1", "x / x == 1")));
48+
chain(expect("x != 0"), expect("1 == 1", "x / x == 1")));
4949
assertSimplificationSteps(simplification::apply, vc("0 != x", "x % x == 0"),
50-
chain(expect("0 != x", "0 != x"), expect("0 == 0", "x % x == 0")));
50+
chain(expect("0 != x"), expect("0 == 0", "x % x == 0")));
5151
}
5252

5353
@Test
5454
void leavesUnguardedDivisionAndModuloIdentitiesUnchanged() {
55-
assertSimplificationSteps(simplification::apply, vc("0 / x == 0"), chain(expect("0 / x == 0", "0 / x == 0")));
56-
assertSimplificationSteps(simplification::apply, vc("x / x == 1"), chain(expect("x / x == 1", "x / x == 1")));
57-
assertSimplificationSteps(simplification::apply, vc("x % x == 0"), chain(expect("x % x == 0", "x % x == 0")));
55+
assertSimplificationSteps(simplification::apply, vc("0 / x == 0"), chain(expect("0 / x == 0")));
56+
assertSimplificationSteps(simplification::apply, vc("x / x == 1"), chain(expect("x / x == 1")));
57+
assertSimplificationSteps(simplification::apply, vc("x % x == 0"), chain(expect("x % x == 0")));
5858
}
5959

6060
@Test
@@ -68,7 +68,7 @@ void recordsOriginWhenSimplifyingLaterImplication() {
6868
VCImplication implication = vc("x > 0", "y + 0 > x");
6969

7070
VCImplication result = assertSimplificationSteps(simplification::apply, implication,
71-
chain(expect("x > 0", "x > 0"), expect("y > x", "y + 0 > x")));
71+
chain(expect("x > 0"), expect("y > x", "y + 0 > x")));
7272

7373
SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
7474
assertEquals("y + 0 > x", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString());

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

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,7 @@ void removesTrueBinderWhenVariableIsUnusedDownstream() {
2121
void keepsTrueBinderWhenVariableIsUsedDownstream() {
2222
VCImplication implication = vc("∀x:int. true", "x > 0");
2323

24-
assertSimplificationSteps(binderSimplification::apply, implication,
25-
chain(expect("true", "∀x:int. true"), expect("x > 0", "x > 0")));
24+
assertSimplificationSteps(binderSimplification::apply, implication, chain(expect("true"), expect("x > 0")));
2625
}
2726

2827
@Test
@@ -39,23 +38,22 @@ void simplifiesOnlyFirstApplicableBinder() {
3938
VCImplication implication = vc("∀x:int. true", "∀y:int. true", "z > 0");
4039

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

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

4948
assertSimplificationSteps(binderSimplification::apply, implication,
50-
chain(expect("true", "∀x:int. true"), expect("x > 0", "x > 0"), expect("z > 0", "∀y:int. z > 0")));
49+
chain(expect("true"), expect("x > 0"), expect("z > 0", "∀y:int. z > 0")));
5150
}
5251

5352
@Test
5453
void ignoresNonBinderBooleanLiterals() {
5554
VCImplication implication = vc("true", "false");
5655

57-
assertSimplificationSteps(binderSimplification::apply, implication,
58-
chain(expect("true", "true"), expect("false", "false")));
56+
assertSimplificationSteps(binderSimplification::apply, implication, chain(expect("true"), expect("false")));
5957
}
6058

6159
@Test

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

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -39,16 +39,14 @@ void foldsRealAndMixedNumericExpressions() {
3939

4040
@Test
4141
void leavesDivisionAndModuloByZeroUnchanged() {
42-
assertSimplificationSteps(folding::apply, vc("4 / 0 == 0"), chain(expect("4 / 0 == 0", "4 / 0 == 0")));
43-
assertSimplificationSteps(folding::apply, vc("4 % 0 == 0"), chain(expect("4 % 0 == 0", "4 % 0 == 0")));
42+
assertSimplificationSteps(folding::apply, vc("4 / 0 == 0"), chain(expect("4 / 0 == 0")));
43+
assertSimplificationSteps(folding::apply, vc("4 % 0 == 0"), chain(expect("4 % 0 == 0")));
4444
}
4545

4646
@Test
4747
void leavesRealDivisionAndModuloByZeroUnchanged() {
48-
assertSimplificationSteps(folding::apply, vc("4.0 / 0.0 == 0.0"),
49-
chain(expect("4.0 / 0.0 == 0.0", "4.0 / 0.0 == 0.0")));
50-
assertSimplificationSteps(folding::apply, vc("4.0 % 0.0 == 0.0"),
51-
chain(expect("4.0 % 0.0 == 0.0", "4.0 % 0.0 == 0.0")));
48+
assertSimplificationSteps(folding::apply, vc("4.0 / 0.0 == 0.0"), chain(expect("4.0 / 0.0 == 0.0")));
49+
assertSimplificationSteps(folding::apply, vc("4.0 % 0.0 == 0.0"), chain(expect("4.0 % 0.0 == 0.0")));
5250
}
5351

5452
@Test
@@ -173,13 +171,12 @@ void recordsOriginWhenFoldingLaterImplication() {
173171
VCImplication implication = vc("x > 0", "1 + 2 > 0");
174172

175173
VCImplication result = assertSimplificationSteps(folding::apply, implication,
176-
chain(expect("x > 0", "x > 0"), expect("3 > 0", "1 + 2 > 0")));
174+
chain(expect("x > 0"), expect("3 > 0", "1 + 2 > 0")));
177175

178176
SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
179177
assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString());
180178

181-
result = assertSimplificationSteps(folding::apply, result,
182-
chain(expect("x > 0", "x > 0"), expect("true", "3 > 0")));
179+
result = assertSimplificationSteps(folding::apply, result, chain(expect("x > 0"), expect("true", "3 > 0")));
183180

184181
simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
185182
assertEquals("3 > 0", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString());

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,7 @@ void recordsOriginWhenSimplifyingLaterImplication() {
7676
VCImplication implication = vc("x > 0", "y || false");
7777

7878
VCImplication result = assertSimplificationSteps(simplification::apply, implication,
79-
chain(expect("x > 0", "x > 0"), expect("y", "y || false")));
79+
chain(expect("x > 0"), expect("y", "y || false")));
8080

8181
SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
8282
assertEquals("y || false", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString());

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

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -41,8 +41,8 @@ void simplifyOnceAppliesSubstitutionBeforeBinderSimplification() {
4141
VCImplication implication = vc("∀x:int. x == 3", "∀y:int. true", "x > 0");
4242

4343
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")));
44+
chain(expect("true"), expect("3 > 0", "∀x:int. x > 0")), chain(expect("3 > 0", "∀y:int. x > 0")),
45+
chain(expect("true", "3 > 0")));
4646
}
4747

4848
@Test
@@ -138,9 +138,8 @@ void simplifyAppliesLongSubstitutionChainBeforeReachingFixedPoint() {
138138
VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 1", "∀z:int. z == y + 1", "z == 3");
139139

140140
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
141-
chain(expect("y == 1 + 1", "∀x:int. y == x + 1"), expect("z == y + 1", "∀z:int. z == y + 1"),
142-
expect("z == 3", "z == 3")),
143-
chain(expect("z == 1 + 1 + 1", "∀y:int. z == y + 1"), expect("z == 3", "z == 3")),
141+
chain(expect("y == 1 + 1", "∀x:int. y == x + 1"), expect("z == y + 1"), expect("z == 3")),
142+
chain(expect("z == 1 + 1 + 1", "∀y:int. z == y + 1"), expect("z == 3")),
144143
chain(expect("1 + 1 + 1 == 3", "∀z:int. z == 3")), chain(expect("2 + 1 == 3", "1 + 1 + 1 == 3")),
145144
chain(expect("3 == 3", "2 + 1 == 3")), chain(expect("true", "3 == 3")));
146145
}
@@ -150,7 +149,7 @@ void simplifyCombinesSubstitutionAndNestedFoldingAcrossFixedPoint() {
150149
VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 2", "y - 1 == 2");
151150

152151
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
153-
chain(expect("y == 1 + 2", "∀x:int. y == x + 2"), expect("y - 1 == 2", "y - 1 == 2")),
152+
chain(expect("y == 1 + 2", "∀x:int. y == x + 2"), expect("y - 1 == 2")),
154153
chain(expect("1 + 2 - 1 == 2", "∀y:int. y - 1 == 2")), chain(expect("3 - 1 == 2", "1 + 2 - 1 == 2")),
155154
chain(expect("2 == 2", "3 - 1 == 2")), chain(expect("true", "2 == 2")));
156155
}
@@ -167,7 +166,6 @@ void simplifyStopsAfterSubstitutionWhenOnlyNegativeLiteralShapeChanges() {
167166
void simplifyLeavesUnchangedVcAsPlainPredicates() {
168167
VCImplication implication = vc("x > 0", "y > x");
169168

170-
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
171-
chain(expect("x > 0", "x > 0"), expect("y > x", "y > x")));
169+
assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x > 0"), expect("y > x")));
172170
}
173171
}

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

Lines changed: 9 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -49,30 +49,30 @@ void preservesRemainingBinderAfterSubstitution() {
4949
VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y > x", "y > 0");
5050

5151
assertSimplificationSteps(substitution::apply, implication,
52-
chain(expect("y > 3", "∀x:int. y > x"), expect("y > 0", "y > 0")));
52+
chain(expect("y > 3", "∀x:int. y > x"), expect("y > 0")));
5353
}
5454

5555
@Test
5656
void removesSourceNodeWhenItIsLastInChain() {
5757
VCImplication implication = vc("x > 0", "∀y:int. y == 1");
5858

59-
assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 0", "x > 0")));
59+
assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 0")));
6060
}
6161

6262
@Test
6363
void usesFirstSubstitutionFoundInChain() {
6464
VCImplication implication = vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0");
6565

6666
assertSimplificationSteps(substitution::apply, implication,
67-
chain(expect("x > 0", "∀x:int. x > 0"), expect("x + 4 > 0", "∀y:int. x + y > 0")));
67+
chain(expect("x > 0"), expect("x + 4 > 0", "∀y:int. x + y > 0")));
6868
}
6969

7070
@Test
7171
void substitutesInnerKnownValueAcrossNestedImplications() {
7272
VCImplication implication = vc("∀x:int. true", "∀y:int. y == 1", "∀z:int. z > y", "y + z > 0");
7373

74-
assertSimplificationSteps(substitution::apply, implication, chain(expect("true", "∀x:int. true"),
75-
expect("z > 1", "∀y:int. z > y"), expect("1 + z > 0", "∀y:int. y + z > 0")));
74+
assertSimplificationSteps(substitution::apply, implication,
75+
chain(expect("true"), expect("z > 1", "∀y:int. z > y"), expect("1 + z > 0", "∀y:int. y + z > 0")));
7676
}
7777

7878
@Test
@@ -88,31 +88,27 @@ void substitutesOuterKnownValueIntoNestedBinderRefinements() {
8888
void ignoresRecursiveBinderEquality() {
8989
VCImplication implication = vc("∀x:int. x == x + 1", "x > 0");
9090

91-
assertSimplificationSteps(substitution::apply, implication,
92-
chain(expect("x == x + 1", "∀x:int. x == x + 1"), expect("x > 0", "x > 0")));
91+
assertSimplificationSteps(substitution::apply, implication, chain(expect("x == x + 1"), expect("x > 0")));
9392
}
9493

9594
@Test
9695
void ignoresNonEqualityBinderRefinement() {
9796
VCImplication implication = vc("∀x:int. x > 3", "x > 0");
9897

99-
assertSimplificationSteps(substitution::apply, implication,
100-
chain(expect("x > 3", "∀x:int. x > 3"), expect("x > 0", "x > 0")));
98+
assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 3"), expect("x > 0")));
10199
}
102100

103101
@Test
104102
void ignoresDerivedBinderEquality() {
105103
VCImplication implication = vc("∀x:int. x + 1 == 3", "x > 0");
106104

107-
assertSimplificationSteps(substitution::apply, implication,
108-
chain(expect("x + 1 == 3", "∀x:int. x + 1 == 3"), expect("x > 0", "x > 0")));
105+
assertSimplificationSteps(substitution::apply, implication, chain(expect("x + 1 == 3"), expect("x > 0")));
109106
}
110107

111108
@Test
112109
void ignoresEqualityWithoutBinder() {
113110
VCImplication implication = vc("x == 3", "x > 0");
114111

115-
assertSimplificationSteps(substitution::apply, implication,
116-
chain(expect("x == 3", "x == 3"), expect("x > 0", "x > 0")));
112+
assertSimplificationSteps(substitution::apply, implication, chain(expect("x == 3"), expect("x > 0")));
117113
}
118114
}

‎liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java‎

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package liquidjava.utils;
22

33
import static org.junit.jupiter.api.Assertions.assertEquals;
4+
import static org.junit.jupiter.api.Assertions.assertNotNull;
45
import static org.junit.jupiter.api.Assertions.assertNull;
56

67
import java.util.function.UnaryOperator;
@@ -55,9 +56,14 @@ public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplif
5556
"Expected simplified refinement at implication " + i + " to be a plain Predicate");
5657
assertEquals(expectedPredicate.simplified(), formatRefinement(current),
5758
"Unexpected simplified expression at implication " + i);
58-
if (expectedPredicate.origin() != null)
59-
assertEquals(expectedPredicate.origin(), formatOrigin(current.getOrigin()),
59+
if (expectedPredicate.origin() == null)
60+
assertNull(current.getOrigin(), "Unexpected origin VC at implication " + i);
61+
else {
62+
VCImplication origin = current.getOrigin();
63+
assertNotNull(origin, "Expected origin VC at implication " + i);
64+
assertEquals(expectedPredicate.origin(), formatOrigin(origin),
6065
"Unexpected origin VC at implication " + i);
66+
}
6167
current = current.getNext();
6268
}
6369
assertNull(current, "Expected VC chain to end after " + expected.length + " implications");
@@ -81,6 +87,10 @@ public static ExpectedSimplifiedVCImplication expect(String simplified, String o
8187
return new ExpectedSimplifiedVCImplication(simplified, origin);
8288
}
8389

90+
public static ExpectedSimplifiedVCImplication expect(String simplified) {
91+
return new ExpectedSimplifiedVCImplication(simplified, null);
92+
}
93+
8494
private static String formatOrigin(VCImplication origin) {
8595
if (!origin.hasBinder())
8696
return formatRefinement(origin);

0 commit comments

Comments
 (0)