Skip to content

Commit 9c7ed97

Browse files
committed
Fix Expression Parentheses
1 parent c68a166 commit 9c7ed97

7 files changed

Lines changed: 147 additions & 17 deletions

File tree

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java

Lines changed: 20 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,14 +40,31 @@ public boolean isArithmeticOperation() {
4040
return !isLogicOperation() && !isBooleanOperation();
4141
}
4242

43+
private boolean isAssociative() {
44+
return op.equals("&&") || op.equals("||") || op.equals("+") || op.equals("*");
45+
}
46+
4347
@Override
44-
public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
45-
return visitor.visitBinaryExpression(this);
48+
protected Precedence getPrecedence() {
49+
return Precedence.fromOperator(op);
50+
}
51+
52+
private String formatRightOperand(Expression operand) {
53+
if (operand.getPrecedence() == getPrecedence() && operand instanceof BinaryExpression right)
54+
if (!isAssociative() || !op.equals(right.getOperator()))
55+
return parenthesize(operand);
56+
57+
return formatChild(operand);
4658
}
4759

4860
@Override
4961
public String toString() {
50-
return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString();
62+
return formatChild(getFirstOperand()) + " " + op + " " + formatRightOperand(getSecondOperand());
63+
}
64+
65+
@Override
66+
public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
67+
return visitor.visitBinaryExpression(this);
5168
}
5269

5370
@Override

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,39 @@ public abstract class Expression {
3636

3737
public abstract String toString();
3838

39+
protected enum Precedence {
40+
TERNARY, IMPLICATION, OR, AND, COMPARISON, ADDITIVE, MULTIPLICATIVE, PREFIX, ATOMIC;
41+
42+
private boolean isLowerThan(Precedence other) {
43+
return ordinal() < other.ordinal();
44+
}
45+
46+
protected static Precedence fromOperator(String op) {
47+
return switch (op) {
48+
case "-->" -> IMPLICATION;
49+
case "||" -> OR;
50+
case "&&" -> AND;
51+
case "==", "!=", ">=", ">", "<=", "<" -> COMPARISON;
52+
case "+", "-" -> ADDITIVE;
53+
case "*", "/", "%" -> MULTIPLICATIVE;
54+
default -> ATOMIC;
55+
};
56+
}
57+
}
58+
59+
protected Precedence getPrecedence() {
60+
return Precedence.ATOMIC;
61+
}
62+
63+
protected String parenthesize(Expression expression) {
64+
return "(" + expression.toString() + ")";
65+
}
66+
67+
protected String formatChild(Expression child) {
68+
boolean needsParentheses = child.getPrecedence().isLowerThan(getPrecedence());
69+
return needsParentheses ? parenthesize(child) : child.toString();
70+
}
71+
3972
List<Expression> children = new ArrayList<>();
4073

4174
public void addChild(Expression e) {

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,11 @@ public String toString() {
2424
return getExpression().toString();
2525
}
2626

27+
@Override
28+
protected Precedence getPrecedence() {
29+
return getExpression().getPrecedence();
30+
}
31+
2732
@Override
2833
public void getVariableNames(List<String> toAdd) {
2934
getExpression().getVariableNames(toAdd);

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,21 @@ public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
3030
return visitor.visitIte(this);
3131
}
3232

33+
@Override
34+
protected Precedence getPrecedence() {
35+
return Precedence.TERNARY;
36+
}
37+
38+
private String formatCondition(Expression operand) {
39+
if (operand instanceof Ite)
40+
return parenthesize(operand);
41+
42+
return formatChild(operand);
43+
}
44+
3345
@Override
3446
public String toString() {
35-
return getCondition().toString() + " ? " + getThen().toString() + " : " + getElse().toString();
47+
return formatCondition(getCondition()) + " ? " + formatCondition(getThen()) + " : " + formatChild(getElse());
3648
}
3749

3850
@Override

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,9 +27,14 @@ public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
2727
return visitor.visitUnaryExpression(this);
2828
}
2929

30+
@Override
31+
protected Precedence getPrecedence() {
32+
return Precedence.PREFIX;
33+
}
34+
3035
@Override
3136
public String toString() {
32-
return op + getExpression().toString();
37+
return op + formatChild(getExpression());
3338
}
3439

3540
@Override
Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
package liquidjava.rj_language.ast;
2+
3+
import static org.junit.jupiter.api.Assertions.assertEquals;
4+
5+
import org.junit.jupiter.api.Test;
6+
7+
class ExpressionPrinterTest {
8+
9+
@Test
10+
void printsUnaryWithoutExtraParenthesesForAtoms() {
11+
assertEquals("!x", new UnaryExpression("!", new Var("x")).toString());
12+
assertEquals("!false", new UnaryExpression("!", new LiteralBoolean(false)).toString());
13+
}
14+
15+
@Test
16+
void printsUnaryWithParenthesesForCompoundOperands() {
17+
Expression comparison = new BinaryExpression(new Var("x"), ">", new LiteralInt(0));
18+
19+
assertEquals("x > 0", comparison.toString());
20+
assertEquals("!(x > 0)", new UnaryExpression("!", comparison).toString());
21+
}
22+
23+
@Test
24+
void printsBinaryExpressionsWithOperatorPrecedence() {
25+
Expression sum = new BinaryExpression(new Var("a"), "+", new Var("b"));
26+
Expression product = new BinaryExpression(new Var("b"), "*", new Var("c"));
27+
28+
assertEquals("(a + b) * c", new BinaryExpression(sum, "*", new Var("c")).toString());
29+
assertEquals("a * (a + b)", new BinaryExpression(new Var("a"), "*", sum).toString());
30+
assertEquals("a + b * c", new BinaryExpression(new Var("a"), "+", product).toString());
31+
assertEquals("a - (a + b)", new BinaryExpression(new Var("a"), "-", sum).toString());
32+
assertEquals("a + b + c", new BinaryExpression(sum, "+", new Var("c")).toString());
33+
assertEquals("b * c * c", new BinaryExpression(product, "*", new Var("c")).toString());
34+
}
35+
36+
@Test
37+
void printsLogicalExpressionsWithNeededParentheses() {
38+
Expression andExpression = new BinaryExpression(new Var("a"), "&&", new Var("b"));
39+
Expression orExpression = new BinaryExpression(new Var("b"), "||", new Var("c"));
40+
Expression implication = new BinaryExpression(new Var("b"), "-->", new Var("c"));
41+
42+
assertEquals("a && b || c", new BinaryExpression(andExpression, "||", new Var("c")).toString());
43+
assertEquals("a && (b || c)", new BinaryExpression(new Var("a"), "&&", orExpression).toString());
44+
assertEquals("a --> (b --> c)", new BinaryExpression(new Var("a"), "-->", implication).toString());
45+
assertEquals("a && b && c", new BinaryExpression(andExpression, "&&", new Var("c")).toString());
46+
assertEquals("a || b || c",
47+
new BinaryExpression(new BinaryExpression(new Var("a"), "||", new Var("b")), "||", new Var("c"))
48+
.toString());
49+
}
50+
51+
@Test
52+
void printsTernaryExpressionsWithNeededParentheses() {
53+
Expression ite = new Ite(new Var("a"), new Var("b"), new Var("c"));
54+
Expression nestedElse = new Ite(new Var("c"), new Var("d"), new Var("e"));
55+
56+
assertEquals("(a ? b : c) + d", new BinaryExpression(ite, "+", new Var("d")).toString());
57+
assertEquals("(a ? b : c) ? d : e", new Ite(ite, new Var("d"), new Var("e")).toString());
58+
assertEquals("a ? (b ? c : d) : e",
59+
new Ite(new Var("a"), new Ite(new Var("b"), new Var("c"), new Var("d")), new Var("e")).toString());
60+
assertEquals("a ? b : c ? d : e", new Ite(new Var("a"), new Var("b"), nestedElse).toString());
61+
assertEquals("a ? b : c", new Ite(new Var("a"), new Var("b"), new Var("c")).toString());
62+
}
63+
}

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java

Lines changed: 7 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@
2323
import org.junit.jupiter.api.Test;
2424

2525
/**
26-
* Test suite for expression simplification using constant propagation and folding
26+
* Test suite for expression simplification
2727
*/
2828
class ExpressionSimplifierTest {
2929

@@ -562,8 +562,6 @@ void testTransitive() {
562562
@Test
563563
void testShouldNotOversimplifyToTrue() {
564564
// Given: x > 5 && x == y && y == 10
565-
// Iteration 1: resolves y == 10, substitutes y -> 10: x > 5 && x == 10
566-
// Iteration 2: resolves x == 10, substitutes x -> 10: 10 > 5 && 10 == 10 -> true
567565
// Expected: x > 5 && x == 10 (should NOT simplify to true)
568566

569567
Expression varX = new Var("x");
@@ -592,8 +590,7 @@ void testShouldNotOversimplifyToTrue() {
592590
@Test
593591
void testShouldUnwrapBooleanInEquality() {
594592
// Given: x == (1 > 0)
595-
// Without unwrapping: x == true (unhelpful - hides what "true" came from)
596-
// Expected: x == 1 > 0 (unwrapped to show the original comparison)
593+
// Expected: x == (1 > 0) (unwrapped to show the original comparison)
597594

598595
Expression varX = new Var("x");
599596
Expression one = new LiteralInt(1);
@@ -606,15 +603,14 @@ void testShouldUnwrapBooleanInEquality() {
606603

607604
// Then
608605
assertNotNull(result, "Result should not be null");
609-
assertEquals("x == 1 > 0", result.getValue().toString(),
606+
assertEquals("x == (1 > 0)", result.getValue().toString(),
610607
"Boolean in equality should be unwrapped to show the original comparison");
611608
}
612609

613610
@Test
614611
void testShouldUnwrapBooleanInEqualityWithPropagation() {
615612
// Given: x == (a > b) && a == 3 && b == 1
616-
// Without unwrapping: x == true (unhelpful)
617-
// Expected: x == 3 > 1 (unwrapped and propagated)
613+
// Expected: x == (3 > 1) (unwrapped and propagated)
618614

619615
Expression varX = new Var("x");
620616
Expression varA = new Var("a");
@@ -635,7 +631,7 @@ void testShouldUnwrapBooleanInEqualityWithPropagation() {
635631

636632
// Then
637633
assertNotNull(result, "Result should not be null");
638-
assertEquals("x == 3 > 1", result.getValue().toString(),
634+
assertEquals("x == (3 > 1)", result.getValue().toString(),
639635
"Boolean in equality should be unwrapped after propagation");
640636
}
641637

@@ -666,8 +662,7 @@ void testShouldNotUnwrapBooleanWithBooleanChildren() {
666662
@Test
667663
void testShouldUnwrapNestedBooleanInEquality() {
668664
// Given: x == (a + b > 10) && a == 3 && b == 5
669-
// Without unwrapping: x == true (unhelpful)
670-
// Expected: x == 8 > 10 (shows the actual comparison that produced the boolean)
665+
// Expected: x == (8 > 10) (shows the actual comparison that produced the boolean)
671666

672667
Expression varX = new Var("x");
673668
Expression varA = new Var("a");
@@ -690,7 +685,7 @@ void testShouldUnwrapNestedBooleanInEquality() {
690685

691686
// Then
692687
assertNotNull(result, "Result should not be null");
693-
assertEquals("x == 8 > 10", result.getValue().toString(),
688+
assertEquals("x == (8 > 10)", result.getValue().toString(),
694689
"Boolean in equality should be unwrapped to show the computed comparison");
695690
}
696691

0 commit comments

Comments
 (0)