Skip to content

Commit a784e4a

Browse files
rcosta358rcosta358
authored
Add VC Logical Simplification (#253)
1 parent 10c0e6e commit a784e4a

7 files changed

Lines changed: 405 additions & 51 deletions

File tree

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

Lines changed: 6 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -243,29 +243,18 @@ private static Expression simplifyModulo(Expression left, Expression right, List
243243
}
244244

245245
/**
246-
* Records direct non-zero premises from equalities and inequalities
246+
* Records direct non-zero premises shaped as x != 0 or 0 != x
247247
*/
248248
private static void addNonZeroExpression(Expression expression, List<Expression> nonZeroExpressions) {
249-
if (!(expression instanceof BinaryExpression binary))
249+
if (!(expression instanceof BinaryExpression binary) || !"!=".equals(binary.getOperator()))
250250
return;
251251

252252
Expression left = binary.getFirstOperand();
253253
Expression right = binary.getSecondOperand();
254-
if ("!=".equals(binary.getOperator())) {
255-
// x != 0 -> x is non-zero
256-
if (isZero(right))
257-
nonZeroExpressions.add(left.clone());
258-
// 0 != x -> x is non-zero
259-
if (isZero(left))
260-
nonZeroExpressions.add(right.clone());
261-
} else if ("==".equals(binary.getOperator())) {
262-
// x == n && n != 0 -> x is non-zero
263-
if (isNumericLiteral(right) && !isZero(right))
264-
nonZeroExpressions.add(left.clone());
265-
// n == x && n != 0 -> x is non-zero
266-
if (isNumericLiteral(left) && !isZero(left))
267-
nonZeroExpressions.add(right.clone());
268-
}
254+
if (isZero(left))
255+
nonZeroExpressions.add(right.clone());
256+
if (isZero(right))
257+
nonZeroExpressions.add(left.clone());
269258
}
270259

271260
/**
@@ -286,13 +275,6 @@ private static boolean isZero(Expression expression) {
286275
return false;
287276
}
288277

289-
/**
290-
* Checks whether an expression is a numeric literal
291-
*/
292-
private static boolean isNumericLiteral(Expression expression) {
293-
return expression instanceof LiteralInt || expression instanceof LiteralReal;
294-
}
295-
296278
/**
297279
* Checks whether an expression is a numeric one literal
298280
*/

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

Lines changed: 251 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,251 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import liquidjava.processor.SimplifiedVCImplication;
4+
import liquidjava.processor.VCImplication;
5+
import liquidjava.rj_language.Predicate;
6+
import liquidjava.rj_language.ast.BinaryExpression;
7+
import liquidjava.rj_language.ast.Expression;
8+
import liquidjava.rj_language.ast.GroupExpression;
9+
import liquidjava.rj_language.ast.Ite;
10+
import liquidjava.rj_language.ast.LiteralBoolean;
11+
import liquidjava.rj_language.ast.UnaryExpression;
12+
13+
/**
14+
* Simplifies VCImplication chains by applying logical identities inside refinements
15+
*/
16+
public class VCLogicalSimplification {
17+
18+
/**
19+
* Applies the first logical simplification available in a VC chain
20+
*/
21+
public static VCImplication apply(VCImplication implication) {
22+
if (implication == null)
23+
return null;
24+
25+
Expression expression = implication.getRefinement().getExpression();
26+
Expression simplified = simplify(expression);
27+
if (!expression.equals(simplified)) {
28+
VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), implication);
29+
result.setNext(implication.getNext() == null ? null : implication.getNext().clone());
30+
return result;
31+
}
32+
33+
VCImplication next = apply(implication.getNext());
34+
if (implication.getNext() == null || implication.getNext().equals(next))
35+
return implication;
36+
37+
VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone());
38+
result.setNext(next);
39+
return result;
40+
}
41+
42+
/**
43+
* Simplifies the first logical identity found inside an expression
44+
*/
45+
private static Expression simplify(Expression expression) {
46+
if (expression instanceof BinaryExpression binary)
47+
return simplifyBinary(binary);
48+
if (expression instanceof UnaryExpression unary)
49+
return simplifyUnary(unary);
50+
if (expression instanceof Ite ite)
51+
return simplifyIte(ite);
52+
if (expression instanceof GroupExpression group)
53+
return simplifyGroup(group);
54+
return expression.clone();
55+
}
56+
57+
/**
58+
* Simplifies a binary expression by visiting operands before the current node
59+
*/
60+
private static Expression simplifyBinary(BinaryExpression binary) {
61+
Expression left = binary.getFirstOperand();
62+
Expression simplifiedLeft = simplify(left);
63+
if (!left.equals(simplifiedLeft))
64+
return new BinaryExpression(simplifiedLeft, binary.getOperator(), binary.getSecondOperand().clone());
65+
66+
Expression right = binary.getSecondOperand();
67+
Expression simplifiedRight = simplify(right);
68+
if (!right.equals(simplifiedRight))
69+
return new BinaryExpression(left.clone(), binary.getOperator(), simplifiedRight);
70+
71+
Expression simplifiedBinary = simplifyLocalBinary(left, right, binary.getOperator());
72+
if (simplifiedBinary != null)
73+
return simplifiedBinary;
74+
75+
return new BinaryExpression(left.clone(), binary.getOperator(), right.clone());
76+
}
77+
78+
/**
79+
* Simplifies a unary expression by visiting its operand before the current node
80+
*/
81+
private static Expression simplifyUnary(UnaryExpression unary) {
82+
Expression operand = unary.getExpression();
83+
Expression simplifiedOperand = simplify(operand);
84+
if (!operand.equals(simplifiedOperand))
85+
return new UnaryExpression(unary.getOp(), simplifiedOperand);
86+
87+
// !!x -> x
88+
if ("!".equals(unary.getOp()) && isNot(operand))
89+
return negatedExpression(operand).clone();
90+
91+
return new UnaryExpression(unary.getOp(), operand.clone());
92+
}
93+
94+
/**
95+
* Simplifies a ternary expression by visiting condition, then branch, and else branch
96+
*/
97+
private static Expression simplifyIte(Ite ite) {
98+
Expression condition = ite.getCondition();
99+
Expression simplifiedCondition = simplify(condition);
100+
if (!condition.equals(simplifiedCondition))
101+
return new Ite(simplifiedCondition, ite.getThen().clone(), ite.getElse().clone());
102+
103+
Expression thenExpression = ite.getThen();
104+
Expression simplifiedThen = simplify(thenExpression);
105+
if (!thenExpression.equals(simplifiedThen))
106+
return new Ite(condition.clone(), simplifiedThen, ite.getElse().clone());
107+
108+
Expression elseExpression = ite.getElse();
109+
Expression simplifiedElse = simplify(elseExpression);
110+
if (!elseExpression.equals(simplifiedElse))
111+
return new Ite(condition.clone(), thenExpression.clone(), simplifiedElse);
112+
113+
return new Ite(condition.clone(), thenExpression.clone(), elseExpression.clone());
114+
}
115+
116+
/**
117+
* Simplifies an expression wrapped in parentheses while preserving the group node
118+
*/
119+
private static Expression simplifyGroup(GroupExpression group) {
120+
Expression expression = group.getExpression();
121+
Expression simplified = simplify(expression);
122+
if (!expression.equals(simplified))
123+
return new GroupExpression(simplified);
124+
return group.clone();
125+
}
126+
127+
/**
128+
* Dispatches a local binary logical identity by operator
129+
*/
130+
private static Expression simplifyLocalBinary(Expression left, Expression right, String op) {
131+
return switch (op) {
132+
case "&&" -> simplifyConjunction(left, right);
133+
case "||" -> simplifyDisjunction(left, right);
134+
case "==" -> simplifyEquality(left, right);
135+
case "!=" -> simplifyInequality(left, right);
136+
case "-->" -> simplifyImplication(left, right);
137+
default -> null;
138+
};
139+
}
140+
141+
/**
142+
* Applies conjunction identities involving boolean literals and same operands
143+
*/
144+
private static Expression simplifyConjunction(Expression left, Expression right) {
145+
// x && true -> x
146+
if (isTrue(right))
147+
return left.clone();
148+
// true && x -> x
149+
if (isTrue(left))
150+
return right.clone();
151+
// x && false -> false
152+
if (isFalse(right))
153+
return right.clone();
154+
// false && x -> false
155+
if (isFalse(left))
156+
return left.clone();
157+
// p && p -> p
158+
if (left.equals(right))
159+
return left.clone();
160+
return null;
161+
}
162+
163+
/**
164+
* Applies disjunction identities involving boolean literals and same operands
165+
*/
166+
private static Expression simplifyDisjunction(Expression left, Expression right) {
167+
// x || true -> true
168+
if (isTrue(right))
169+
return right.clone();
170+
// true || x -> true
171+
if (isTrue(left))
172+
return left.clone();
173+
// x || false -> x
174+
if (isFalse(right))
175+
return left.clone();
176+
// false || x -> x
177+
if (isFalse(left))
178+
return right.clone();
179+
// p || p -> p
180+
if (left.equals(right))
181+
return left.clone();
182+
return null;
183+
}
184+
185+
/**
186+
* Applies equality identity for same operands
187+
*/
188+
private static Expression simplifyEquality(Expression left, Expression right) {
189+
// x == x -> true
190+
if (left.equals(right))
191+
return new LiteralBoolean(true);
192+
return null;
193+
}
194+
195+
/**
196+
* Applies inequality identity for same operands
197+
*/
198+
private static Expression simplifyInequality(Expression left, Expression right) {
199+
// x != x -> false
200+
if (left.equals(right))
201+
return new LiteralBoolean(false);
202+
return null;
203+
}
204+
205+
/**
206+
* Applies implication identities involving boolean literals and same operands
207+
*/
208+
private static Expression simplifyImplication(Expression left, Expression right) {
209+
// x --> true -> true
210+
if (isTrue(right))
211+
return right.clone();
212+
// false --> x -> true
213+
if (isFalse(left))
214+
return new LiteralBoolean(true);
215+
// true --> x -> x
216+
if (isTrue(left))
217+
return right.clone();
218+
// x --> x -> true
219+
if (left.equals(right))
220+
return new LiteralBoolean(true);
221+
return null;
222+
}
223+
224+
/**
225+
* Checks whether an expression is true
226+
*/
227+
private static boolean isTrue(Expression expression) {
228+
return expression instanceof LiteralBoolean literal && literal.isBooleanTrue();
229+
}
230+
231+
/**
232+
* Checks whether an expression is false
233+
*/
234+
private static boolean isFalse(Expression expression) {
235+
return expression instanceof LiteralBoolean literal && !literal.isBooleanTrue();
236+
}
237+
238+
/**
239+
* Checks whether an expression is unary logical negation
240+
*/
241+
private static boolean isNot(Expression expression) {
242+
return expression instanceof UnaryExpression unary && "!".equals(unary.getOp());
243+
}
244+
245+
/**
246+
* Returns the operand of a unary logical negation expression
247+
*/
248+
private static Expression negatedExpression(Expression expression) {
249+
return ((UnaryExpression) expression).getExpression();
250+
}
251+
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111
public class VCSimplification {
1212

1313
private static final List<UnaryOperator<VCImplication>> PASSES = List.of(VCSubstitution::apply, VCFolding::apply,
14-
VCArithmeticSimplification::apply);
14+
VCArithmeticSimplification::apply, VCLogicalSimplification::apply);
1515

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

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

Lines changed: 0 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -70,16 +70,6 @@ void simplifiesGuardedDivisionAndModuloIdentities() {
7070
chain(expect("0 != x", "0 != x"), expect("0 == 0", "x % x == 0")));
7171
}
7272

73-
@Test
74-
void simplifiesGuardedDivisionAndModuloIdentitiesWhenEqualityImpliesNonZero() {
75-
assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x == 1", "0 / x == 0"),
76-
chain(expect("x == 1", "x == 1"), expect("0 == 0", "0 / x == 0")));
77-
assertSimplificationSteps(VCArithmeticSimplification::apply, vc("1 == x", "x / x == 1"),
78-
chain(expect("1 == x", "1 == x"), expect("1 == 1", "x / x == 1")));
79-
assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x == 1", "x % x == 0"),
80-
chain(expect("x == 1", "x == 1"), expect("0 == 0", "x % x == 0")));
81-
}
82-
8373
@Test
8474
void leavesUnguardedDivisionAndModuloIdentitiesUnchanged() {
8575
assertSimplificationSteps(VCArithmeticSimplification::apply, vc("0 / x == 0"),
@@ -96,21 +86,6 @@ void simplifiesOnlyFirstArithmeticIdentity() {
9686
chain(expect("x + 1 > 0", "x + 0 + 1 > 0")));
9787
}
9888

99-
@Test
100-
void simplifiesTernaryExpressionsInConditionThenElseOrder() {
101-
assertSimplificationSteps(VCArithmeticSimplification::apply, vc("(flag + 0 > 0 ? x + 0 : y + 0) > 0"),
102-
chain(expect("(flag > 0 ? x + 0 : y + 0) > 0", "(flag + 0 > 0 ? x + 0 : y + 0) > 0")),
103-
chain(expect("(flag > 0 ? x : y + 0) > 0", "(flag > 0 ? x + 0 : y + 0) > 0")),
104-
chain(expect("(flag > 0 ? x : y) > 0", "(flag > 0 ? x : y + 0) > 0")));
105-
}
106-
107-
@Test
108-
void simplifiesGroupedExpressionsAndLeavesUnchangedGroupsAlone() {
109-
assertSimplificationSteps(VCArithmeticSimplification::apply, vc("(x + 0) * y > 0"),
110-
chain(expect("x * y > 0", "(x + 0) * y > 0")));
111-
assertSimplificationSteps(VCArithmeticSimplification::apply, vc("(x) > 0"), chain(expect("x > 0", "x > 0")));
112-
}
113-
11489
@Test
11590
void recordsOriginWhenSimplifyingLaterImplication() {
11691
VCImplication implication = vc("x > 0", "y + 0 > x");

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

Lines changed: 25 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, 11)) {
24+
return switch (random.nextInt(0, 12)) {
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"));
@@ -33,6 +33,7 @@ public VCImplication generate(SourceOfRandomness random, GenerationStatus status
3333
case 8 -> vc(adjacentConstants(random) + " " + comparisonOperator(random) + " " + intLiteral(random));
3434
case 9 -> vc(arithmeticIdentity(random));
3535
case 10 -> guardedArithmeticIdentity(random);
36+
case 11 -> vc(logicalIdentity(random));
3637
default -> vc(substitution(random, "x"), substitution(random, "y"), foldableComparison(random));
3738
};
3839
}
@@ -124,6 +125,29 @@ private static VCImplication guardedArithmeticIdentity(SourceOfRandomness random
124125
return vc(guard, use);
125126
}
126127

128+
private static String logicalIdentity(SourceOfRandomness random) {
129+
String predicate = "(" + comparison(random, FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)]) + ")";
130+
return switch (random.nextInt(0, 16)) {
131+
case 0 -> predicate + " && true";
132+
case 1 -> "true && " + predicate;
133+
case 2 -> predicate + " && false";
134+
case 3 -> "false && " + predicate;
135+
case 4 -> predicate + " || true";
136+
case 5 -> "true || " + predicate;
137+
case 6 -> predicate + " || false";
138+
case 7 -> "false || " + predicate;
139+
case 8 -> predicate + " && " + predicate;
140+
case 9 -> predicate + " || " + predicate;
141+
case 10 -> predicate + " --> true";
142+
case 11 -> "false --> " + predicate;
143+
case 12 -> "true --> " + predicate;
144+
case 13 -> predicate + " --> " + predicate;
145+
case 14 -> predicate + " == " + predicate;
146+
case 15 -> predicate + " != " + predicate;
147+
default -> "!!" + predicate;
148+
};
149+
}
150+
127151
private static String comparisonOperator(SourceOfRandomness random) {
128152
return COMPARISON_OPS[random.nextInt(0, COMPARISON_OPS.length - 1)];
129153
}

0 commit comments

Comments
 (0)