Expression Pretty Printing

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

@@ -5,9 +5,10 @@
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.TranslationTable;
+import liquidjava.rj_language.ast.Var;
+import liquidjava.rj_language.ast.formatter.VariableFormatter;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 import liquidjava.smt.Counterexample;
-import liquidjava.utils.VariableFormatter;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -23,10 +24,8 @@ public class RefinementError extends LJError {
 
     public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
             TranslationTable translationTable, Counterexample counterexample, String customMessage) {
-        super("Refinement Error",
-                String.format("%s is not a subtype of %s", VariableFormatter.formatText(found.getValue().toString()),
-                        VariableFormatter.formatText(expected.getValue().toString())),
-                position, translationTable, customMessage);
+        super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue().toDisplayString(),
+                expected.getValue().toDisplayString()), position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
         this.counterexample = counterexample;
@@ -50,11 +49,11 @@ public String getCounterExampleString() {
                 // only include variables that appear in the found value
                 .filter(a -> foundVarNames.contains(a.first()))
                 // format as "var == value"
-                .map(a -> VariableFormatter.formatVariable(a.first()) + " == " + a.second())
+                .map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
                 // join with "&&"
                 .collect(Collectors.joining(" && "));
 
-        String foundString = VariableFormatter.formatText(found.getValue().toString());
+        String foundString = found.getValue().toDisplayString();
         if (counterexampleString.isEmpty() || counterexampleString.equals(foundString))
             return null;
 

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

@@ -2,7 +2,6 @@
 
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.ast.Expression;
-import liquidjava.utils.VariableFormatter;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -17,11 +16,11 @@ public class StateRefinementError extends LJError {
 
     public StateRefinementError(SourcePosition position, Expression expected, Expression found,
             TranslationTable translationTable, String customMessage) {
-        super("State Refinement Error", String.format("Expected state %s but found %s",
-                VariableFormatter.formatText(expected.toString()), VariableFormatter.formatText(found.toString())),
+        super("State Refinement Error",
+                String.format("Expected state %s but found %s", expected.toDisplayString(), found.toDisplayString()),
                 position, translationTable, customMessage);
-        this.expected = VariableFormatter.formatText(expected.toString());
-        this.found = VariableFormatter.formatText(found.toString());
+        this.expected = expected.toDisplayString();
+        this.found = found.toDisplayString();
     }
 
     public String getExpected() {

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

@@ -41,13 +41,13 @@ public boolean isArithmeticOperation() {
     }
 
     @Override
-    public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
-        return visitor.visitBinaryExpression(this);
+    public String toString() {
+        return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString();
     }
 
     @Override
-    public String toString() {
-        return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString();
+    public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
+        return visitor.visitBinaryExpression(this);
     }
 
     @Override

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

@@ -11,6 +11,7 @@
 import liquidjava.processor.context.Context;
 import liquidjava.processor.context.GhostFunction;
 import liquidjava.processor.facade.AliasDTO;
+import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
 import liquidjava.rj_language.ast.typing.TypeInfer;
 import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.utils.Utils;
@@ -36,6 +37,10 @@ public abstract class Expression {
 
     public abstract String toString();
 
+    public String toDisplayString() {
+        return ExpressionFormatter.format(this);
+    }
+
     List<Expression> children = new ArrayList<>();
 
     public void addChild(Expression e) {

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

@@ -18,6 +18,7 @@ public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
         return visitor.visitLiteralString(this);
     }
 
+    @Override
     public String toString() {
         return value;
     }

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

@@ -0,0 +1,153 @@
+package liquidjava.rj_language.ast.formatter;
+
+import java.util.List;
+import java.util.stream.Collectors;
+
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.AliasInvocation;
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.FunctionInvocation;
+import liquidjava.rj_language.ast.GroupExpression;
+import liquidjava.rj_language.ast.Ite;
+import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.LiteralChar;
+import liquidjava.rj_language.ast.LiteralInt;
+import liquidjava.rj_language.ast.LiteralLong;
+import liquidjava.rj_language.ast.LiteralReal;
+import liquidjava.rj_language.ast.LiteralString;
+import liquidjava.rj_language.ast.UnaryExpression;
+import liquidjava.rj_language.ast.Var;
+import liquidjava.rj_language.visitors.ExpressionVisitor;
+import liquidjava.utils.Utils;
+
+/**
+ * Formatter for expressions that only adds parentheses when required by precedence and associativity rules and formats
+ * variable names using {@link VariableFormatter}
+ */
+public class ExpressionFormatter implements ExpressionVisitor<String> {
+
+    public static String format(Predicate predicate) {
+        return format(predicate.getExpression());
+    }
+
+    public static String format(Expression expression) {
+        return new ExpressionFormatter().formatExpression(expression);
+    }
+
+    private String formatExpression(Expression expression) {
+        return expression.accept(this);
+    }
+
+    private String formatParentheses(Expression child, boolean shouldWrap) {
+        if (shouldWrap)
+            return "(" + formatExpression(child) + ")";
+        if (child instanceof GroupExpression group)
+            return "(" + formatExpression(group.getExpression()) + ")";
+        return formatExpression(child);
+    }
+
+    private String formatOperand(Expression parent, Expression child) {
+        return formatParentheses(child, needsParentheses(parent, child));
+    }
+
+    private String formatRightOperand(BinaryExpression parent, Expression child) {
+        return formatParentheses(child, needsRightParentheses(parent, child));
+    }
+
+    private String formatCondition(Expression child) {
+        return formatParentheses(child, child instanceof Ite);
+    }
+
+    private String formatArguments(List<Expression> args) {
+        return args.stream().map(expression -> formatParentheses(expression, false)).collect(Collectors.joining(", "));
+    }
+
+    private boolean needsParentheses(Expression parent, Expression child) {
+        return ExpressionPrecedence.of(child).isLowerThan(ExpressionPrecedence.of(parent));
+    }
+
+    private boolean needsRightParentheses(BinaryExpression parent, Expression child) {
+        if (needsParentheses(parent, child))
+            return true;
+
+        if (ExpressionPrecedence.of(child) != ExpressionPrecedence.of(parent))
+            return false;
+
+        if (child instanceof BinaryExpression right)
+            return !isAssociative(parent.getOperator()) || !parent.getOperator().equals(right.getOperator());
+
+        return false;
+    }
+
+    private boolean isAssociative(String operator) {
+        return operator.equals("&&") || operator.equals("||") || operator.equals("+") || operator.equals("*");
+    }
+
+    @Override
+    public String visitAliasInvocation(AliasInvocation alias) {
+        return alias.getName() + "(" + formatArguments(alias.getArgs()) + ")";
+    }
+
+    @Override
+    public String visitBinaryExpression(BinaryExpression exp) {
+        return formatOperand(exp, exp.getFirstOperand()) + " " + exp.getOperator() + " "
+                + formatRightOperand(exp, exp.getSecondOperand());
+    }
+
+    @Override
+    public String visitFunctionInvocation(FunctionInvocation fun) {
+        return Utils.getSimpleName(fun.getName()) + "(" + formatArguments(fun.getArgs()) + ")";
+    }
+
+    @Override
+    public String visitGroupExpression(GroupExpression exp) {
+        return "(" + formatExpression(exp.getExpression()) + ")";
+    }
+
+    @Override
+    public String visitIte(Ite ite) {
+        return formatCondition(ite.getCondition()) + " ? " + formatCondition(ite.getThen()) + " : "
+                + formatOperand(ite, ite.getElse());
+    }
+
+    @Override
+    public String visitLiteralInt(LiteralInt lit) {
+        return Integer.toString(lit.getValue());
+    }
+
+    @Override
+    public String visitLiteralLong(LiteralLong lit) {
+        return Long.toString(lit.getValue());
+    }
+
+    @Override
+    public String visitLiteralBoolean(LiteralBoolean lit) {
+        return lit.toString();
+    }
+
+    @Override
+    public String visitLiteralChar(LiteralChar lit) {
+        return lit.toString();
+    }
+
+    @Override
+    public String visitLiteralReal(LiteralReal lit) {
+        return lit.toString();
+    }
+
+    @Override
+    public String visitLiteralString(LiteralString lit) {
+        return lit.toString();
+    }
+
+    @Override
+    public String visitUnaryExpression(UnaryExpression exp) {
+        return exp.getOp() + formatOperand(exp, exp.getExpression());
+    }
+
+    @Override
+    public String visitVar(Var var) {
+        return VariableFormatter.format(var.getName());
+    }
+}

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

@@ -0,0 +1,39 @@
+package liquidjava.rj_language.ast.formatter;
+
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.GroupExpression;
+import liquidjava.rj_language.ast.Ite;
+import liquidjava.rj_language.ast.UnaryExpression;
+
+public enum ExpressionPrecedence {
+    TERNARY, IMPLICATION, OR, AND, COMPARISON, ADDITIVE, MULTIPLICATIVE, UNARY, ATOMIC;
+
+    public boolean isLowerThan(ExpressionPrecedence other) {
+        return ordinal() < other.ordinal();
+    }
+
+    public static ExpressionPrecedence of(Expression expression) {
+        if (expression instanceof GroupExpression group)
+            return of(group.getExpression());
+        if (expression instanceof Ite)
+            return TERNARY;
+        if (expression instanceof UnaryExpression)
+            return UNARY;
+        if (expression instanceof BinaryExpression binary)
+            return of(binary.getOperator());
+        return ATOMIC;
+    }
+
+    public static ExpressionPrecedence of(String operator) {
+        return switch (operator) {
+        case "-->" -> IMPLICATION;
+        case "||" -> OR;
+        case "&&" -> AND;
+        case "==", "!=", ">=", ">", "<=", "<" -> COMPARISON;
+        case "+", "-" -> ADDITIVE;
+        case "*", "/", "%" -> MULTIPLICATIVE;
+        default -> ATOMIC;
+        };
+    }
+}

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

@@ -1,14 +1,16 @@
-package liquidjava.utils;
+package liquidjava.rj_language.ast.formatter;
 
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
+/**
+ * Formats internal variable names into a cleaner display representation using superscript notation
+ */
 public final class VariableFormatter {
     private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$");
-    private static final Pattern INSTANCE_VAR_TEXT_PATTERN = Pattern.compile("#[^\\s,;:()\\[\\]{}]+_[0-9]+");
     private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' };
 
-    public static String formatVariable(String name) {
+    public static String format(String name) {
         if (name == null)
             return null;
 
@@ -22,20 +24,6 @@ public static String formatVariable(String name) {
         return prefix + baseName + toSuperscript(counter);
     }
 
-    public static String formatText(String text) {
-        if (text == null)
-            return null;
-
-        Matcher textMatcher = INSTANCE_VAR_TEXT_PATTERN.matcher(text);
-        StringBuilder sb = new StringBuilder();
-        while (textMatcher.find()) {
-            String token = textMatcher.group();
-            textMatcher.appendReplacement(sb, Matcher.quoteReplacement(formatVariable(token)));
-        }
-        textMatcher.appendTail(sb);
-        return sb.toString();
-    }
-
     private static String toSuperscript(String number) {
         StringBuilder sb = new StringBuilder(number.length());
         for (char c : number.toCharArray()) {
@@ -50,4 +38,4 @@ private static String toSuperscript(String number) {
     private static boolean isSpecialIdentifier(String id) {
         return id.equals("fresh") || id.equals("ret");
     }
-}
+}

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

@@ -14,8 +14,6 @@
 import liquidjava.rj_language.ast.LiteralInt;
 import liquidjava.rj_language.ast.LiteralLong;
 import liquidjava.rj_language.ast.LiteralReal;
-import liquidjava.rj_language.ast.Var;
-import liquidjava.utils.VariableFormatter;
 
 public class ValDerivationNode extends DerivationNode {
 
@@ -50,9 +48,7 @@ public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationCo
                 return new JsonPrimitive(v.getValue());
             if (exp instanceof LiteralBoolean v)
                 return new JsonPrimitive(v.isBooleanTrue());
-            if (exp instanceof Var v)
-                return new JsonPrimitive(VariableFormatter.formatVariable(v.getName()));
-            return new JsonPrimitive(VariableFormatter.formatText(exp.toString()));
+            return new JsonPrimitive(exp.toDisplayString());
         }
     }
 }