Skip to content

Commit 85d9a86

Browse files
rcosta358rcosta358
committed
Fix Origins
1 parent 9fc831a commit 85d9a86

4 files changed

Lines changed: 54 additions & 31 deletions

File tree

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,8 +28,7 @@ public static VCImplication apply(VCImplication implication) {
2828
Expression expression = implication.getRefinement().getExpression();
2929
Expression folded = fold(expression);
3030
if (!expression.equals(folded)) {
31-
VCImplication result = new SimplifiedVCImplication(implication, new Predicate(folded),
32-
implication.getOrigin());
31+
VCImplication result = new SimplifiedVCImplication(implication, new Predicate(folded), implication);
3332
result.setNext(implication.getNext() == null ? null : implication.getNext().clone());
3433
return result;
3534
}

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

Lines changed: 33 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ void foldsIntegerArithmeticAndComparisons() {
2626
VCImplication implication = vc("1 + 2 == 3");
2727

2828
assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 == 3", "1 + 2 == 3")),
29-
chain(expect("true", "1 + 2 == 3")));
29+
chain(expect("true", "3 == 3")));
3030
assertSimplificationSteps(VCFolding::apply, vc("4 > 7"), chain(expect("false", "4 > 7")));
3131
}
3232

@@ -36,9 +36,9 @@ void foldsRealAndMixedNumericExpressions() {
3636
VCImplication mixedArithmetic = vc("2 + 0.5 > 2");
3737

3838
assertSimplificationSteps(VCFolding::apply, realArithmetic, chain(expect("3.5 == 3.5", "1.5 + 2.0 == 3.5")),
39-
chain(expect("true", "1.5 + 2.0 == 3.5")));
39+
chain(expect("true", "3.5 == 3.5")));
4040
assertSimplificationSteps(VCFolding::apply, mixedArithmetic, chain(expect("2.5 > 2", "2 + 0.5 > 2")),
41-
chain(expect("true", "2 + 0.5 > 2")));
41+
chain(expect("true", "2.5 > 2")));
4242
}
4343

4444
@Test
@@ -55,6 +55,27 @@ void leavesRealDivisionAndModuloByZeroUnchanged() {
5555
chain(expect("4.0 % 0.0 == 0.0", "4.0 % 0.0 == 0.0")));
5656
}
5757

58+
@Test
59+
void foldsIntegerDivisionTowardZeroForNegativeResults() {
60+
VCImplication implication = vc("(2 - 7) / 2 == -2");
61+
62+
assertSimplificationSteps(VCFolding::apply, implication,
63+
chain(expect("(2 - 7) / 2 == -2", "(2 - 7) / 2 == -2")),
64+
chain(expect("-5 / 2 == -2", "(2 - 7) / 2 == -2")), chain(expect("-2 == -2", "-5 / 2 == -2")),
65+
chain(expect("-2 == -2", "-2 == -2")), chain(expect("true", "-2 == -2")));
66+
}
67+
68+
@Test
69+
void foldsIntegerModuloWithJavaSignedRemainder() {
70+
VCImplication negativeDividend = vc("-5 % 2 < 0");
71+
VCImplication negativeDivisor = vc("5 % -2 > 0");
72+
73+
assertSimplificationSteps(VCFolding::apply, negativeDividend, chain(expect("-5 % 2 < 0", "-5 % 2 < 0")),
74+
chain(expect("-1 < 0", "-5 % 2 < 0")), chain(expect("true", "-1 < 0")));
75+
assertSimplificationSteps(VCFolding::apply, negativeDivisor, chain(expect("5 % -2 > 0", "5 % -2 > 0")),
76+
chain(expect("1 > 0", "5 % -2 > 0")), chain(expect("true", "1 > 0")));
77+
}
78+
5879
@Test
5980
void foldsBooleanBinaryExpressions() {
6081
assertSimplificationSteps(VCFolding::apply, vc("true && false"), chain(expect("false", "true && false")));
@@ -100,7 +121,7 @@ void foldsIteBranchesBeforeComparingThem() {
100121
VCImplication implication = vc("cond ? 1 + 2 : 3");
101122

102123
assertSimplificationSteps(VCFolding::apply, implication, chain(expect("cond ? 3 : 3", "cond ? 1 + 2 : 3")),
103-
chain(expect("3", "cond ? 1 + 2 : 3")));
124+
chain(expect("3", "cond ? 3 : 3")));
104125
}
105126

106127
@Test
@@ -127,7 +148,7 @@ void foldsResolvedEnumLiterals() {
127148
new Predicate(new BinaryExpression(limit, "==", new LiteralInt(3))));
128149

129150
assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 == 3", "Config.LIMIT == 3")),
130-
chain(expect("true", "Config.LIMIT == 3")));
151+
chain(expect("true", "3 == 3")));
131152
}
132153

133154
@Test
@@ -139,15 +160,15 @@ void foldsResolvedEnumLiteralsInsideLargerExpression() {
139160
new Predicate(new BinaryExpression(arithmetic, "==", new LiteralInt(5))));
140161

141162
assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 + 2 == 5", "Config.LIMIT + 2 == 5")),
142-
chain(expect("5 == 5", "Config.LIMIT + 2 == 5")), chain(expect("true", "Config.LIMIT + 2 == 5")));
163+
chain(expect("5 == 5", "3 + 2 == 5")), chain(expect("true", "5 == 5")));
143164
}
144165

145166
@Test
146-
void preservesOriginFromExistingSimplifiedImplication() {
167+
void recordsCurrentImplicationAsOriginWhenFoldingExistingSimplifiedImplication() {
147168
VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == 1", "x + 1 + 2 > 0"));
148169

149-
assertSimplificationSteps(VCFolding::apply, substituted, chain(expect("2 + 2 > 0", "∀x:int. x + 1 + 2 > 0")),
150-
chain(expect("4 > 0", "∀x:int. x + 1 + 2 > 0")), chain(expect("true", "∀x:int. x + 1 + 2 > 0")));
170+
assertSimplificationSteps(VCFolding::apply, substituted, chain(expect("2 + 2 > 0", "1 + 1 + 2 > 0")),
171+
chain(expect("4 > 0", "2 + 2 > 0")), chain(expect("true", "4 > 0")));
151172
}
152173

153174
@Test
@@ -169,13 +190,13 @@ void recordsOriginWhenFoldingLaterImplication() {
169190
chain(expect("x > 0", "x > 0"), expect("3 > 0", "1 + 2 > 0")));
170191

171192
SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
172-
assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().toString());
193+
assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString());
173194

174195
result = assertSimplificationSteps(VCFolding::apply, result,
175-
chain(expect("x > 0", "x > 0"), expect("true", "1 + 2 > 0")));
196+
chain(expect("x > 0", "x > 0"), expect("true", "3 > 0")));
176197

177198
simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
178-
assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().toString());
199+
assertEquals("3 > 0", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString());
179200
}
180201

181202
}

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

Lines changed: 13 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -23,34 +23,34 @@ void simplifyOnceAppliesSubstitutionBeforeFolding() {
2323
VCImplication implication = vc("∀x:int. x == 1 + 2", "x > 2");
2424

2525
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
26-
chain(expect("1 + 2 > 2", "∀x:int. x > 2")), chain(expect("3 > 2", "∀x:int. x > 2")),
27-
chain(expect("true", "∀x:int. x > 2")));
26+
chain(expect("1 + 2 > 2", "∀x:int. x > 2")), chain(expect("3 > 2", "1 + 2 > 2")),
27+
chain(expect("true", "3 > 2")));
2828
}
2929

3030
@Test
3131
void simplifyOnceDoesNotFoldAfterSubstitutionInSameStep() {
3232
VCImplication implication = vc("∀x:int. x == 1 + 2", "x == 3");
3333

3434
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
35-
chain(expect("1 + 2 == 3", "∀x:int. x == 3")), chain(expect("3 == 3", "∀x:int. x == 3")),
36-
chain(expect("true", "∀x:int. x == 3")));
35+
chain(expect("1 + 2 == 3", "∀x:int. x == 3")), chain(expect("3 == 3", "1 + 2 == 3")),
36+
chain(expect("true", "3 == 3")));
3737
}
3838

3939
@Test
4040
void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() {
4141
VCImplication implication = vc("1 + 2 > 2");
4242

4343
assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("3 > 2", "1 + 2 > 2")),
44-
chain(expect("true", "1 + 2 > 2")));
44+
chain(expect("true", "3 > 2")));
4545
}
4646

4747
@Test
4848
void simplifyKeepsApplyingStepsUntilFixedPoint() {
4949
VCImplication implication = vc("∀x:int. x == 1 + 2", "x + 1 > 3");
5050

5151
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
52-
chain(expect("1 + 2 + 1 > 3", "∀x:int. x + 1 > 3")), chain(expect("3 + 1 > 3", "∀x:int. x + 1 > 3")),
53-
chain(expect("4 > 3", "∀x:int. x + 1 > 3")), chain(expect("true", "∀x:int. x + 1 > 3")));
52+
chain(expect("1 + 2 + 1 > 3", "∀x:int. x + 1 > 3")), chain(expect("3 + 1 > 3", "1 + 2 + 1 > 3")),
53+
chain(expect("4 > 3", "3 + 1 > 3")), chain(expect("true", "4 > 3")));
5454
}
5555

5656
@Test
@@ -59,8 +59,8 @@ void simplifyAppliesMultipleSubstitutionsBeforeReachingFixedPoint() {
5959

6060
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
6161
chain(expect("y == 3 + 1", "∀x:int. y == x + 1"), expect("y > 3", "∀x:int. y > x")),
62-
chain(expect("3 + 1 > 3", "∀y:int. y > x")), chain(expect("4 > 3", "∀y:int. y > x")),
63-
chain(expect("true", "∀y:int. y > x")));
62+
chain(expect("3 + 1 > 3", "∀y:int. y > x")), chain(expect("4 > 3", "3 + 1 > 3")),
63+
chain(expect("true", "4 > 3")));
6464
}
6565

6666
@Test
@@ -71,8 +71,8 @@ void simplifyAppliesLongSubstitutionChainBeforeReachingFixedPoint() {
7171
chain(expect("y == 1 + 1", "∀x:int. y == x + 1"), expect("z == y + 1", "∀z:int. z == y + 1"),
7272
expect("z == 3", "z == 3")),
7373
chain(expect("z == 1 + 1 + 1", "∀y:int. z == y + 1"), expect("z == 3", "z == 3")),
74-
chain(expect("1 + 1 + 1 == 3", "∀z:int. z == 3")), chain(expect("2 + 1 == 3", "∀z:int. z == 3")),
75-
chain(expect("3 == 3", "∀z:int. z == 3")), chain(expect("true", "∀z:int. z == 3")));
74+
chain(expect("1 + 1 + 1 == 3", "∀z:int. z == 3")), chain(expect("2 + 1 == 3", "1 + 1 + 1 == 3")),
75+
chain(expect("3 == 3", "2 + 1 == 3")), chain(expect("true", "3 == 3")));
7676
}
7777

7878
@Test
@@ -81,9 +81,8 @@ void simplifyCombinesSubstitutionAndNestedFoldingAcrossFixedPoint() {
8181

8282
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
8383
chain(expect("y == 1 + 2", "∀x:int. y == x + 2"), expect("y - 1 == 2", "y - 1 == 2")),
84-
chain(expect("1 + 2 - 1 == 2", "∀y:int. y - 1 == 2")),
85-
chain(expect("3 - 1 == 2", "∀y:int. y - 1 == 2")), chain(expect("2 == 2", "∀y:int. y - 1 == 2")),
86-
chain(expect("true", "∀y:int. y - 1 == 2")));
84+
chain(expect("1 + 2 - 1 == 2", "∀y:int. y - 1 == 2")), chain(expect("3 - 1 == 2", "1 + 2 - 1 == 2")),
85+
chain(expect("2 == 2", "3 - 1 == 2")), chain(expect("true", "2 == 2")));
8786
}
8887

8988
@Test

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

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplif
5353
ExpectedSimplifiedVCImplication expectedPredicate = expected[i];
5454
assertEquals(Predicate.class, current.getRefinement().getClass(),
5555
"Expected simplified refinement at implication " + i + " to be a plain Predicate");
56-
assertEquals(expectedPredicate.simplified(), current.getRefinement().toString(),
56+
assertEquals(expectedPredicate.simplified(), formatRefinement(current),
5757
"Unexpected simplified expression at implication " + i);
5858
if (expectedPredicate.origin() != null)
5959
assertEquals(expectedPredicate.origin(), formatOrigin(current.getOrigin()),
@@ -83,8 +83,12 @@ public static ExpectedSimplifiedVCImplication expect(String simplified, String o
8383

8484
private static String formatOrigin(VCImplication origin) {
8585
if (!origin.hasBinder())
86-
return origin.getRefinement().toString();
87-
return "∀" + origin.getName() + ":" + origin.getType().getQualifiedName() + ". " + origin.getRefinement();
86+
return formatRefinement(origin);
87+
return "∀" + origin.getName() + ":" + origin.getType().getQualifiedName() + ". " + formatRefinement(origin);
88+
}
89+
90+
private static String formatRefinement(VCImplication implication) {
91+
return implication.getRefinement().getExpression().toDisplayString();
8892
}
8993

9094
public record ExpectedSimplifiedVCImplication(String simplified, String origin) {

0 commit comments

Comments
 (0)