Skip to content

Commit a43db5f

Browse files
rcosta358rcosta358
authored
Expression Pretty Printing (#200)
1 parent 8ac8d94 commit a43db5f

13 files changed

Lines changed: 314 additions & 100 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,10 @@
66

77
import liquidjava.api.CommandLineLauncher;
88
import liquidjava.diagnostics.TranslationTable;
9+
import liquidjava.rj_language.ast.Var;
10+
import liquidjava.rj_language.ast.formatter.VariableFormatter;
911
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
1012
import liquidjava.smt.Counterexample;
11-
import liquidjava.utils.VariableFormatter;
1213
import spoon.reflect.cu.SourcePosition;
1314

1415
/**
@@ -24,10 +25,8 @@ public class RefinementError extends LJError {
2425

2526
public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
2627
TranslationTable translationTable, Counterexample counterexample, String customMessage) {
27-
super("Refinement Error",
28-
String.format("%s is not a subtype of %s", VariableFormatter.formatText(found.getValue().toString()),
29-
VariableFormatter.formatText(expected.getValue().toString())),
30-
position, translationTable, customMessage);
28+
super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue().toDisplayString(),
29+
expected.getValue().toDisplayString()), position, translationTable, customMessage);
3130
this.expected = expected;
3231
this.found = found;
3332
this.counterexample = counterexample;
@@ -51,11 +50,11 @@ public String getCounterExampleString() {
5150
// only include variables that appear in the found value
5251
.filter(a -> CommandLineLauncher.cmdArgs.debugMode || foundVarNames.contains(a.first()))
5352
// format as "var == value"
54-
.map(a -> VariableFormatter.formatVariable(a.first()) + " == " + a.second())
53+
.map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
5554
// join with "&&"
5655
.collect(Collectors.joining(" && "));
5756

58-
String foundString = VariableFormatter.formatText(found.getValue().toString());
57+
String foundString = found.getValue().toDisplayString();
5958
if (counterexampleString.isEmpty() || counterexampleString.equals(foundString))
6059
return null;
6160

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java‎

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

33
import liquidjava.diagnostics.TranslationTable;
44
import liquidjava.rj_language.ast.Expression;
5-
import liquidjava.utils.VariableFormatter;
65
import spoon.reflect.cu.SourcePosition;
76

87
/**
@@ -17,11 +16,11 @@ public class StateRefinementError extends LJError {
1716

1817
public StateRefinementError(SourcePosition position, Expression expected, Expression found,
1918
TranslationTable translationTable, String customMessage) {
20-
super("State Refinement Error", String.format("Expected state %s but found %s",
21-
VariableFormatter.formatText(expected.toString()), VariableFormatter.formatText(found.toString())),
19+
super("State Refinement Error",
20+
String.format("Expected state %s but found %s", expected.toDisplayString(), found.toDisplayString()),
2221
position, translationTable, customMessage);
23-
this.expected = VariableFormatter.formatText(expected.toString());
24-
this.found = VariableFormatter.formatText(found.toString());
22+
this.expected = expected.toDisplayString();
23+
this.found = found.toDisplayString();
2524
}
2625

2726
public String getExpected() {

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -41,13 +41,13 @@ public boolean isArithmeticOperation() {
4141
}
4242

4343
@Override
44-
public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
45-
return visitor.visitBinaryExpression(this);
44+
public String toString() {
45+
return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString();
4646
}
4747

4848
@Override
49-
public String toString() {
50-
return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString();
49+
public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
50+
return visitor.visitBinaryExpression(this);
5151
}
5252

5353
@Override

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@
1111
import liquidjava.processor.context.Context;
1212
import liquidjava.processor.context.GhostFunction;
1313
import liquidjava.processor.facade.AliasDTO;
14+
import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
1415
import liquidjava.rj_language.ast.typing.TypeInfer;
1516
import liquidjava.rj_language.visitors.ExpressionVisitor;
1617
import liquidjava.utils.Utils;
@@ -36,6 +37,10 @@ public abstract class Expression {
3637

3738
public abstract String toString();
3839

40+
public String toDisplayString() {
41+
return ExpressionFormatter.format(this);
42+
}
43+
3944
List<Expression> children = new ArrayList<>();
4045

4146
public void addChild(Expression e) {

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
1818
return visitor.visitLiteralString(this);
1919
}
2020

21+
@Override
2122
public String toString() {
2223
return value;
2324
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java‎

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
package liquidjava.rj_language.ast.formatter;
2+
3+
import java.util.List;
4+
import java.util.stream.Collectors;
5+
6+
import liquidjava.rj_language.Predicate;
7+
import liquidjava.rj_language.ast.AliasInvocation;
8+
import liquidjava.rj_language.ast.BinaryExpression;
9+
import liquidjava.rj_language.ast.Expression;
10+
import liquidjava.rj_language.ast.FunctionInvocation;
11+
import liquidjava.rj_language.ast.GroupExpression;
12+
import liquidjava.rj_language.ast.Ite;
13+
import liquidjava.rj_language.ast.LiteralBoolean;
14+
import liquidjava.rj_language.ast.LiteralChar;
15+
import liquidjava.rj_language.ast.LiteralInt;
16+
import liquidjava.rj_language.ast.LiteralLong;
17+
import liquidjava.rj_language.ast.LiteralReal;
18+
import liquidjava.rj_language.ast.LiteralString;
19+
import liquidjava.rj_language.ast.UnaryExpression;
20+
import liquidjava.rj_language.ast.Var;
21+
import liquidjava.rj_language.visitors.ExpressionVisitor;
22+
import liquidjava.utils.Utils;
23+
24+
/**
25+
* Formatter for expressions that only adds parentheses when required by precedence and associativity rules and formats
26+
* variable names using {@link VariableFormatter}
27+
*/
28+
public class ExpressionFormatter implements ExpressionVisitor<String> {
29+
30+
public static String format(Predicate predicate) {
31+
return format(predicate.getExpression());
32+
}
33+
34+
public static String format(Expression expression) {
35+
return new ExpressionFormatter().formatExpression(expression);
36+
}
37+
38+
private String formatExpression(Expression expression) {
39+
return expression.accept(this);
40+
}
41+
42+
private String formatParentheses(Expression child, boolean shouldWrap) {
43+
if (shouldWrap)
44+
return "(" + formatExpression(child) + ")";
45+
if (child instanceof GroupExpression group)
46+
return "(" + formatExpression(group.getExpression()) + ")";
47+
return formatExpression(child);
48+
}
49+
50+
private String formatOperand(Expression parent, Expression child) {
51+
return formatParentheses(child, needsParentheses(parent, child));
52+
}
53+
54+
private String formatRightOperand(BinaryExpression parent, Expression child) {
55+
return formatParentheses(child, needsRightParentheses(parent, child));
56+
}
57+
58+
private String formatCondition(Expression child) {
59+
return formatParentheses(child, child instanceof Ite);
60+
}
61+
62+
private String formatArguments(List<Expression> args) {
63+
return args.stream().map(expression -> formatParentheses(expression, false)).collect(Collectors.joining(", "));
64+
}
65+
66+
private boolean needsParentheses(Expression parent, Expression child) {
67+
return ExpressionPrecedence.of(child).isLowerThan(ExpressionPrecedence.of(parent));
68+
}
69+
70+
private boolean needsRightParentheses(BinaryExpression parent, Expression child) {
71+
if (needsParentheses(parent, child))
72+
return true;
73+
74+
if (ExpressionPrecedence.of(child) != ExpressionPrecedence.of(parent))
75+
return false;
76+
77+
if (child instanceof BinaryExpression right)
78+
return !isAssociative(parent.getOperator()) || !parent.getOperator().equals(right.getOperator());
79+
80+
return false;
81+
}
82+
83+
private boolean isAssociative(String operator) {
84+
return operator.equals("&&") || operator.equals("||") || operator.equals("+") || operator.equals("*");
85+
}
86+
87+
@Override
88+
public String visitAliasInvocation(AliasInvocation alias) {
89+
return alias.getName() + "(" + formatArguments(alias.getArgs()) + ")";
90+
}
91+
92+
@Override
93+
public String visitBinaryExpression(BinaryExpression exp) {
94+
return formatOperand(exp, exp.getFirstOperand()) + " " + exp.getOperator() + " "
95+
+ formatRightOperand(exp, exp.getSecondOperand());
96+
}
97+
98+
@Override
99+
public String visitFunctionInvocation(FunctionInvocation fun) {
100+
return Utils.getSimpleName(fun.getName()) + "(" + formatArguments(fun.getArgs()) + ")";
101+
}
102+
103+
@Override
104+
public String visitGroupExpression(GroupExpression exp) {
105+
return "(" + formatExpression(exp.getExpression()) + ")";
106+
}
107+
108+
@Override
109+
public String visitIte(Ite ite) {
110+
return formatCondition(ite.getCondition()) + " ? " + formatCondition(ite.getThen()) + " : "
111+
+ formatOperand(ite, ite.getElse());
112+
}
113+
114+
@Override
115+
public String visitLiteralInt(LiteralInt lit) {
116+
return Integer.toString(lit.getValue());
117+
}
118+
119+
@Override
120+
public String visitLiteralLong(LiteralLong lit) {
121+
return Long.toString(lit.getValue());
122+
}
123+
124+
@Override
125+
public String visitLiteralBoolean(LiteralBoolean lit) {
126+
return lit.toString();
127+
}
128+
129+
@Override
130+
public String visitLiteralChar(LiteralChar lit) {
131+
return lit.toString();
132+
}
133+
134+
@Override
135+
public String visitLiteralReal(LiteralReal lit) {
136+
return lit.toString();
137+
}
138+
139+
@Override
140+
public String visitLiteralString(LiteralString lit) {
141+
return lit.toString();
142+
}
143+
144+
@Override
145+
public String visitUnaryExpression(UnaryExpression exp) {
146+
return exp.getOp() + formatOperand(exp, exp.getExpression());
147+
}
148+
149+
@Override
150+
public String visitVar(Var var) {
151+
return VariableFormatter.format(var.getName());
152+
}
153+
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
package liquidjava.rj_language.ast.formatter;
2+
3+
import liquidjava.rj_language.ast.BinaryExpression;
4+
import liquidjava.rj_language.ast.Expression;
5+
import liquidjava.rj_language.ast.GroupExpression;
6+
import liquidjava.rj_language.ast.Ite;
7+
import liquidjava.rj_language.ast.UnaryExpression;
8+
9+
public enum ExpressionPrecedence {
10+
TERNARY, IMPLICATION, OR, AND, COMPARISON, ADDITIVE, MULTIPLICATIVE, UNARY, ATOMIC;
11+
12+
public boolean isLowerThan(ExpressionPrecedence other) {
13+
return ordinal() < other.ordinal();
14+
}
15+
16+
public static ExpressionPrecedence of(Expression expression) {
17+
if (expression instanceof GroupExpression group)
18+
return of(group.getExpression());
19+
if (expression instanceof Ite)
20+
return TERNARY;
21+
if (expression instanceof UnaryExpression)
22+
return UNARY;
23+
if (expression instanceof BinaryExpression binary)
24+
return of(binary.getOperator());
25+
return ATOMIC;
26+
}
27+
28+
public static ExpressionPrecedence of(String operator) {
29+
return switch (operator) {
30+
case "-->" -> IMPLICATION;
31+
case "||" -> OR;
32+
case "&&" -> AND;
33+
case "==", "!=", ">=", ">", "<=", "<" -> COMPARISON;
34+
case "+", "-" -> ADDITIVE;
35+
case "*", "/", "%" -> MULTIPLICATIVE;
36+
default -> ATOMIC;
37+
};
38+
}
39+
}

liquidjava-verifier/src/main/java/liquidjava/utils/VariableFormatter.java renamed to liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java

Lines changed: 6 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,16 @@
1-
package liquidjava.utils;
1+
package liquidjava.rj_language.ast.formatter;
22

33
import java.util.regex.Matcher;
44
import java.util.regex.Pattern;
55

6+
/**
7+
* Formats internal variable names into a cleaner display representation using superscript notation
8+
*/
69
public final class VariableFormatter {
710
private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$");
8-
private static final Pattern INSTANCE_VAR_TEXT_PATTERN = Pattern.compile("#[^\\s,;:()\\[\\]{}]+_[0-9]+");
911
private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' };
1012

11-
public static String formatVariable(String name) {
13+
public static String format(String name) {
1214
if (name == null)
1315
return null;
1416

@@ -22,20 +24,6 @@ public static String formatVariable(String name) {
2224
return prefix + baseName + toSuperscript(counter);
2325
}
2426

25-
public static String formatText(String text) {
26-
if (text == null)
27-
return null;
28-
29-
Matcher textMatcher = INSTANCE_VAR_TEXT_PATTERN.matcher(text);
30-
StringBuilder sb = new StringBuilder();
31-
while (textMatcher.find()) {
32-
String token = textMatcher.group();
33-
textMatcher.appendReplacement(sb, Matcher.quoteReplacement(formatVariable(token)));
34-
}
35-
textMatcher.appendTail(sb);
36-
return sb.toString();
37-
}
38-
3927
private static String toSuperscript(String number) {
4028
StringBuilder sb = new StringBuilder(number.length());
4129
for (char c : number.toCharArray()) {
@@ -50,4 +38,4 @@ private static String toSuperscript(String number) {
5038
private static boolean isSpecialIdentifier(String id) {
5139
return id.equals("fresh") || id.equals("ret");
5240
}
53-
}
41+
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,6 @@
1414
import liquidjava.rj_language.ast.LiteralInt;
1515
import liquidjava.rj_language.ast.LiteralLong;
1616
import liquidjava.rj_language.ast.LiteralReal;
17-
import liquidjava.rj_language.ast.Var;
18-
import liquidjava.utils.VariableFormatter;
1917

2018
public class ValDerivationNode extends DerivationNode {
2119

@@ -50,9 +48,7 @@ public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationCo
5048
return new JsonPrimitive(v.getValue());
5149
if (exp instanceof LiteralBoolean v)
5250
return new JsonPrimitive(v.isBooleanTrue());
53-
if (exp instanceof Var v)
54-
return new JsonPrimitive(VariableFormatter.formatVariable(v.getName()));
55-
return new JsonPrimitive(VariableFormatter.formatText(exp.toString()));
51+
return new JsonPrimitive(exp.toDisplayString());
5652
}
5753
}
5854
}

0 commit comments

Comments
 (0)