Skip to content

Commit 99131d4

Browse files
rcosta358rcosta358
committed
Fixes
1 parent 84f9727 commit 99131d4

8 files changed

Lines changed: 102 additions & 62 deletions

File tree

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

Lines changed: 34 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -36,36 +36,44 @@ public static VCImplication apply(VCImplication implication) {
3636

3737
VCImplication next = apply(implication.getNext());
3838
if (implication.getNext() == null || implication.getNext().equals(next))
39-
return implication.clone();
39+
return implication;
4040

4141
VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone());
4242
result.setNext(next);
4343
return result;
4444
}
4545

4646
/**
47-
* Folds an expression
47+
* Folds the first foldable expression found
4848
*/
4949
private static Expression fold(Expression expression) {
50+
if (expression instanceof Enum en && en.getResolvedLiteral() != null)
51+
return en.getResolvedLiteral().clone();
5052
if (expression instanceof BinaryExpression binary)
5153
return foldBinary(binary);
5254
if (expression instanceof UnaryExpression unary)
5355
return foldUnary(unary);
5456
if (expression instanceof Ite ite)
5557
return foldIte(ite);
5658
if (expression instanceof GroupExpression group && group.getChildren().size() == 1)
57-
return fold(group.getExpression());
59+
return group.getExpression().clone();
5860
return expression.clone();
5961
}
6062

6163
/**
6264
* Folds a binary expression and its operands
6365
*/
6466
private static Expression foldBinary(BinaryExpression binary) {
65-
Expression leftExpression = fold(binary.getFirstOperand());
66-
Expression rightExpression = fold(binary.getSecondOperand());
67-
Expression left = resolvedLiteral(leftExpression);
68-
Expression right = resolvedLiteral(rightExpression);
67+
Expression left = binary.getFirstOperand();
68+
Expression foldedLeft = fold(left);
69+
if (!left.equals(foldedLeft))
70+
return new BinaryExpression(foldedLeft, binary.getOperator(), binary.getSecondOperand().clone());
71+
72+
Expression right = binary.getSecondOperand();
73+
Expression foldedRight = fold(right);
74+
if (!right.equals(foldedRight))
75+
return new BinaryExpression(left.clone(), binary.getOperator(), foldedRight);
76+
6977
String op = binary.getOperator();
7078

7179
Expression foldedBinary = foldLiteralBinary(left, right, op);
@@ -83,7 +91,11 @@ private static Expression foldBinary(BinaryExpression binary) {
8391
* Folds a unary expression and its operand
8492
*/
8593
private static Expression foldUnary(UnaryExpression unary) {
86-
Expression operand = fold(unary.getExpression());
94+
Expression operand = unary.getExpression();
95+
Expression foldedOperand = fold(operand);
96+
if (!operand.equals(foldedOperand))
97+
return new UnaryExpression(unary.getOp(), foldedOperand);
98+
8799
String op = unary.getOp();
88100

89101
if ("!".equals(op) && operand instanceof LiteralBoolean literal)
@@ -103,9 +115,20 @@ private static Expression foldUnary(UnaryExpression unary) {
103115
* Folds a conditional expression and its branches
104116
*/
105117
private static Expression foldIte(Ite ite) {
106-
Expression condition = fold(ite.getCondition());
107-
Expression thenExpression = fold(ite.getThen());
108-
Expression elseExpression = fold(ite.getElse());
118+
Expression condition = ite.getCondition();
119+
Expression foldedCondition = fold(condition);
120+
if (!condition.equals(foldedCondition))
121+
return new Ite(foldedCondition, ite.getThen().clone(), ite.getElse().clone());
122+
123+
Expression thenExpression = ite.getThen();
124+
Expression foldedThen = fold(thenExpression);
125+
if (!thenExpression.equals(foldedThen))
126+
return new Ite(condition.clone(), foldedThen, ite.getElse().clone());
127+
128+
Expression elseExpression = ite.getElse();
129+
Expression foldedElse = fold(elseExpression);
130+
if (!elseExpression.equals(foldedElse))
131+
return new Ite(condition.clone(), thenExpression.clone(), foldedElse);
109132

110133
if (condition instanceof LiteralBoolean literal)
111134
return literal.isBooleanTrue() ? thenExpression : elseExpression;
@@ -229,15 +252,6 @@ private static Expression foldBooleans(boolean left, boolean right, String op) {
229252
};
230253
}
231254

232-
/**
233-
* Replaces a resolved enum constant with its literal value
234-
*/
235-
private static Expression resolvedLiteral(Expression expression) {
236-
if (expression instanceof Enum en && en.getResolvedLiteral() != null)
237-
return en.getResolvedLiteral().clone();
238-
return expression;
239-
}
240-
241255
/**
242256
* Checks whether two expressions mix integer and real literals
243257
*/

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

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,6 @@
22

33
import liquidjava.processor.VCImplication;
44

5-
import static liquidjava.rj_language.opt.VCSimplificationUtils.*;
6-
75
/**
86
* Simplifies VCImplication chains by applying various simplification steps
97
*/
@@ -38,7 +36,6 @@ public static VCImplication simplifyOnce(VCImplication implication) {
3836
if (!implication.equals(substituted))
3937
return substituted;
4038

41-
// TODO: add more simplification steps here (e.g., folding)
42-
return substituted;
39+
return VCFolding.apply(implication);
4340
}
4441
}

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,6 @@
1111
import liquidjava.rj_language.ast.Expression;
1212
import liquidjava.rj_language.ast.Var;
1313

14-
import static liquidjava.rj_language.opt.VCSimplificationUtils.*;
15-
1614
/**
1715
* Simplifies VCImplication chains by replacing binder equalities with their known values
1816
*/

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

Lines changed: 19 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package liquidjava.rj_language.opt;
22

33
import static liquidjava.utils.VCTestUtils.assertSimplifiedVC;
4+
import static liquidjava.utils.VCTestUtils.assertSimplificationSteps;
45
import static liquidjava.utils.VCTestUtils.assertVC;
56
import static liquidjava.utils.VCTestUtils.parse;
67
import static liquidjava.utils.VCTestUtils.simplified;
@@ -27,14 +28,14 @@ void applyReturnsNullForNullImplication() {
2728

2829
@Test
2930
void foldsIntegerArithmeticAndComparisons() {
30-
assertFolded("1 + 2 == 3", "true");
31+
assertSimplificationSteps(vc("1 + 2 == 3"), VCFolding::apply, "1 + 2 == 3", "3 == 3", "true");
3132
assertFolded("4 > 7", "false");
3233
}
3334

3435
@Test
3536
void foldsRealAndMixedNumericExpressions() {
36-
assertFolded("1.5 + 2.0 == 3.5", "true");
37-
assertFolded("2 + 0.5 > 2", "true");
37+
assertSimplificationSteps(vc("1.5 + 2.0 == 3.5"), VCFolding::apply, "1.5 + 2.0 == 3.5", "3.5 == 3.5", "true");
38+
assertSimplificationSteps(vc("2 + 0.5 > 2"), VCFolding::apply, "2 + 0.5 > 2", "2.5 > 2", "true");
3839
}
3940

4041
@Test
@@ -75,7 +76,7 @@ void foldsPartialComparisonsWithoutDroppingSymbolicTerms() {
7576
@Test
7677
void foldsUnaryExpressions() {
7778
assertFolded("!true", "false");
78-
assertFolded("-3 < 0", "true");
79+
assertSimplificationSteps(vc("-3 < 0"), VCFolding::apply, "-3 < 0", "-3 < 0", "true");
7980
}
8081

8182
@Test
@@ -87,7 +88,7 @@ void foldsIteExpressions() {
8788

8889
@Test
8990
void foldsIteBranchesBeforeComparingThem() {
90-
assertFolded("cond ? 1 + 2 : 3", "3");
91+
assertSimplificationSteps(vc("cond ? 1 + 2 : 3"), VCFolding::apply, "cond ? 1 + 2 : 3", "cond ? 3 : 3", "3");
9192
}
9293

9394
@Test
@@ -111,9 +112,8 @@ void foldsResolvedEnumLiterals() {
111112
VCImplication implication = new VCImplication(
112113
new Predicate(new BinaryExpression(limit, "==", new LiteralInt(3))));
113114

114-
VCImplication result = VCFolding.apply(implication);
115-
116-
assertSimplifiedVC(result, simplified("true", "Config.LIMIT == 3"));
115+
assertSimplificationSteps(implication, VCFolding::apply, simplified("3 == 3", "Config.LIMIT == 3"),
116+
simplified("true", "Config.LIMIT == 3"));
117117
}
118118

119119
@Test
@@ -124,18 +124,16 @@ void foldsResolvedEnumLiteralsInsideLargerExpression() {
124124
VCImplication implication = new VCImplication(
125125
new Predicate(new BinaryExpression(arithmetic, "==", new LiteralInt(5))));
126126

127-
VCImplication result = VCFolding.apply(implication);
128-
129-
assertSimplifiedVC(result, simplified("true", "Config.LIMIT + 2 == 5"));
127+
assertSimplificationSteps(implication, VCFolding::apply, simplified("3 + 2 == 5", "Config.LIMIT + 2 == 5"),
128+
simplified("5 == 5", "Config.LIMIT + 2 == 5"), simplified("true", "Config.LIMIT + 2 == 5"));
130129
}
131130

132131
@Test
133132
void preservesOriginFromExistingSimplifiedImplication() {
134133
VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == 1", "x + 1 + 2 > 0"));
135134

136-
VCImplication result = VCFolding.apply(substituted);
137-
138-
assertSimplifiedVC(result, simplified("true", "∀x:int. x + 1 + 2 > 0"));
135+
assertSimplificationSteps(substituted, VCFolding::apply, simplified("2 + 2 > 0", "∀x:int. x + 1 + 2 > 0"),
136+
simplified("4 > 0", "∀x:int. x + 1 + 2 > 0"), simplified("true", "∀x:int. x + 1 + 2 > 0"));
139137
}
140138

141139
@Test
@@ -157,6 +155,13 @@ void recordsOriginWhenFoldingLaterImplication() {
157155

158156
assertEquals("x > 0", result.getRefinement().toString());
159157
SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
158+
assertEquals("3 > 0", simplifiedNext.getRefinement().toString());
159+
assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().toString());
160+
161+
result = VCFolding.apply(result);
162+
163+
assertEquals("x > 0", result.getRefinement().toString());
164+
simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
160165
assertEquals("true", simplifiedNext.getRefinement().toString());
161166
assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().toString());
162167
}

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

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22

33
import static liquidjava.rj_language.opt.VCSubstitution.containsVar;
44
import static liquidjava.rj_language.opt.VCSubstitution.isVar;
5-
import static org.junit.jupiter.api.Assertions.fail;
65
import static org.junit.jupiter.api.Assertions.assertTrue;
6+
import static org.junit.jupiter.api.Assertions.fail;
77

88
import com.pholser.junit.quickcheck.From;
99
import com.pholser.junit.quickcheck.Property;
@@ -21,19 +21,18 @@
2121
@RunWith(JUnitQuickcheck.class)
2222
public class VCSimplificationPropertyBasedTest {
2323

24-
private static final int TRIALS = 500; // number of random VCs to test
24+
private static final int TRIALS = 100; // number of random VCs to test
2525
private static final int MAX_STEPS = 20; // to prevent infinite loops in case of non-termination
2626

2727
@Property(trials = TRIALS)
2828
public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenerator.class) VCImplication vc) {
2929
setUpContext();
3030
VCImplication current = vc;
3131

32-
for (int step = 0; step < VCImplicationGenerator.BINDERS.length; step++) {
33-
VCImplication simplified = VCSimplification.simplifyToFixedPoint(current);
32+
for (int step = 0; step < MAX_STEPS; step++) {
33+
VCImplication simplified = VCSimplification.simplifyOnce(current);
3434
if (current.equals(simplified))
35-
break;
36-
35+
return;
3736
assertEquivalent(current, simplified, step);
3837
current = simplified;
3938
}
@@ -52,9 +51,6 @@ private static void assertEquivalent(VCImplication unsimplified, VCImplication s
5251
Predicate premises = substitutionPremises(unsimplified);
5352
Predicate unsimplifiedFormula = Predicate.createConjunction(premises, new Predicate(vcFormula(unsimplified)));
5453
Predicate simplifiedFormula = Predicate.createConjunction(premises, new Predicate(vcFormula(simplified)));
55-
System.out.println(unsimplifiedFormula);
56-
System.out.println("=>");
57-
System.out.println(simplifiedFormula);
5854
assertImplies(unsimplifiedFormula, simplifiedFormula, unsimplified, simplified, step,
5955
"unsimplified => simplified");
6056
assertImplies(simplifiedFormula, unsimplifiedFormula, unsimplified, simplified, step,

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

Lines changed: 17 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package liquidjava.rj_language.opt;
22

33
import static liquidjava.utils.VCTestUtils.assertSimplifiedVC;
4+
import static liquidjava.utils.VCTestUtils.assertSimplificationSteps;
45
import static liquidjava.utils.VCTestUtils.assertVC;
56
import static liquidjava.utils.VCTestUtils.simplified;
67
import static liquidjava.utils.VCTestUtils.vc;
@@ -25,27 +26,25 @@ void simplifyOnceReturnsNullForNullImplication() {
2526
void simplifyOnceAppliesSubstitutionBeforeFolding() {
2627
VCImplication implication = vc("∀x:int. x == 1 + 2", "x > 2");
2728

28-
VCImplication result = VCSimplification.simplifyOnce(implication);
29-
30-
assertSimplifiedVC(result, simplified("1 + 2 > 2", "∀x:int. x > 2"));
29+
assertSimplificationSteps(implication, VCSimplification::simplifyOnce, simplified("1 + 2 > 2", "∀x:int. x > 2"),
30+
simplified("3 > 2", "∀x:int. x > 2"), simplified("true", "∀x:int. x > 2"));
3131
}
3232

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

37-
VCImplication result = VCSimplification.simplifyOnce(implication);
38-
39-
assertSimplifiedVC(result, simplified("1 + 2 == 3", "∀x:int. x == 3"));
37+
assertSimplificationSteps(implication, VCSimplification::simplifyOnce,
38+
simplified("1 + 2 == 3", "∀x:int. x == 3"), simplified("3 == 3", "∀x:int. x == 3"),
39+
simplified("true", "∀x:int. x == 3"));
4040
}
4141

4242
@Test
4343
void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() {
4444
VCImplication implication = vc("1 + 2 > 2");
4545

46-
VCImplication result = VCSimplification.simplifyOnce(implication);
47-
48-
assertSimplifiedVC(result, simplified("true", "1 + 2 > 2"));
46+
assertSimplificationSteps(implication, VCSimplification::simplifyOnce, simplified("3 > 2", "1 + 2 > 2"),
47+
simplified("true", "1 + 2 > 2"));
4948
}
5049

5150
@Test
@@ -84,6 +83,15 @@ void simplifyCombinesSubstitutionAndNestedFoldingAcrossFixedPoint() {
8483
assertSimplifiedVC(result, simplified("true", "∀y:int. y - 1 == 2"));
8584
}
8685

86+
@Test
87+
void simplifyStopsAfterSubstitutionWhenOnlyNegativeLiteralShapeChanges() {
88+
VCImplication implication = vc("∀x:int. x == a + 0", "x >= -3");
89+
90+
VCImplication result = VCSimplification.simplifyToFixedPoint(implication);
91+
92+
assertSimplifiedVC(result, simplified("a + 0 >= -3", "∀x:int. x >= -3"));
93+
}
94+
8795
@Test
8896
void simplifyLeavesUnchangedVcAsPlainPredicates() {
8997
VCImplication implication = vc("x > 0", "y > x");

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

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@
22

33
import static liquidjava.utils.VCTestUtils.*;
44
import static org.junit.jupiter.api.Assertions.assertEquals;
5-
import static org.junit.jupiter.api.Assertions.assertNotSame;
65
import static org.junit.jupiter.api.Assertions.assertNull;
76

87
import liquidjava.processor.VCImplication;
@@ -22,6 +21,7 @@ void substitutesBinderEqualityIntoWholeChain() {
2221
VCImplication result = VCSubstitution.apply(implication);
2322

2423
assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0"));
24+
assertSimplificationSteps(result, VCSimplification::simplifyOnce, simplified("true", "∀x:int. x > 0"));
2525
}
2626

2727
@Test
@@ -31,6 +31,7 @@ void substitutesReverseBinderEquality() {
3131
VCImplication result = VCSubstitution.apply(implication);
3232

3333
assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0"));
34+
assertSimplificationSteps(result, VCSimplification::simplifyOnce, simplified("true", "∀x:int. x > 0"));
3435
}
3536

3637
@Test
@@ -58,6 +59,8 @@ void substitutesEveryOccurrenceInPredicate() {
5859
VCImplication result = VCSubstitution.apply(implication);
5960

6061
assertSimplifiedVC(result, simplified("2 + 2 > 0", "∀x:int. x + x > 0"));
62+
assertSimplificationSteps(result, VCSimplification::simplifyOnce, simplified("4 > 0", "∀x:int. x + x > 0"),
63+
simplified("true", "∀x:int. x + x > 0"));
6164
}
6265

6366
@Test
@@ -111,6 +114,8 @@ void substitutesOuterKnownValueIntoNestedBinderRefinements() {
111114

112115
assertSimplifiedVC(result, simplified("y == 3 + 1", "∀x:int. y == x + 1"),
113116
simplified("y > 3", "∀x:int. y > x"));
117+
assertSimplificationSteps(result, VCSimplification::simplifyOnce, simplified("3 + 1 > 3", "∀y:int. y > x"),
118+
simplified("4 > 3", "∀y:int. y > x"), simplified("true", "∀y:int. y > x"));
114119
}
115120

116121
@Test
@@ -119,7 +124,6 @@ void ignoresRecursiveBinderEquality() {
119124

120125
VCImplication result = VCSubstitution.apply(implication);
121126

122-
assertNotSame(implication, result);
123127
assertVC(result, "x == x + 1", "x > 0");
124128
}
125129

@@ -129,7 +133,6 @@ void ignoresNonEqualityBinderRefinement() {
129133

130134
VCImplication result = VCSubstitution.apply(implication);
131135

132-
assertNotSame(implication, result);
133136
assertVC(result, "x > 3", "x > 0");
134137
}
135138

@@ -139,7 +142,6 @@ void ignoresDerivedBinderEquality() {
139142

140143
VCImplication result = VCSubstitution.apply(implication);
141144

142-
assertNotSame(implication, result);
143145
assertVC(result, "x + 1 == 3", "x > 0");
144146
}
145147

@@ -151,4 +153,5 @@ void ignoresEqualityWithoutBinder() {
151153

152154
assertVC(result, "x == 3", "x > 0");
153155
}
156+
154157
}

0 commit comments

Comments
 (0)