diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 09095f35..e5655d5a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -379,7 +379,7 @@ public void visitCtIf(CtIf ifElement) { thenRefs = Predicate.createConjunction(expRefs, freshIsTrue); elseRefs = Predicate.createConjunction(expRefs, freshIsFalse); } - + freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp); } vcChecker.addPathVariable(freshRV); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java index 80e03261..cf6e4fdc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java @@ -40,51 +40,70 @@ private String formatExpression(Expression expression) { return expression.accept(this); } - private String formatParentheses(Expression child, boolean shouldWrap) { + private String formatExpression(Expression expression, boolean shouldWrap) { + expression = unwrapGroup(expression); if (shouldWrap) - return "(" + formatExpression(child) + ")"; - if (child instanceof GroupExpression group) - return "(" + formatExpression(group.getExpression()) + ")"; - return formatExpression(child); + return "(" + formatExpression(expression) + ")"; + return formatExpression(expression); } - 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 formatOperand(Expression parent, Expression child, boolean rightOperand) { + child = unwrapGroup(child); + return formatExpression(child, needsParentheses(parent, child, rightOperand)); } private String formatCondition(Expression child) { - return formatParentheses(child, child instanceof Ite); + return formatExpression(child, unwrapGroup(child) instanceof Ite); } private String formatArguments(List args) { - return args.stream().map(expression -> formatParentheses(expression, false)).collect(Collectors.joining(", ")); + return args.stream().map(expression -> formatExpression(expression, false)).collect(Collectors.joining(", ")); } - private boolean needsParentheses(Expression parent, Expression child) { - return ExpressionPrecedence.of(child).isLowerThan(ExpressionPrecedence.of(parent)); + private Expression unwrapGroup(Expression expression) { + while (expression instanceof GroupExpression group) + expression = group.getExpression(); + return expression; } - private boolean needsRightParentheses(BinaryExpression parent, Expression child) { - if (needsParentheses(parent, child)) + private boolean needsParentheses(Expression parent, Expression child, boolean rightOperand) { + ExpressionPrecedence parentPrecedence = ExpressionPrecedence.of(parent); + ExpressionPrecedence childPrecedence = ExpressionPrecedence.of(child); + if (childPrecedence.isLowerThan(parentPrecedence)) return true; - - if (ExpressionPrecedence.of(child) != ExpressionPrecedence.of(parent)) + if (childPrecedence != parentPrecedence) return false; - if (child instanceof BinaryExpression right) - return !isAssociative(parent.getOperator()) || !parent.getOperator().equals(right.getOperator()); + if (parent instanceof BinaryExpression parentBinary && child instanceof BinaryExpression childBinary) + return needsBinaryParentheses(parentBinary, childBinary, rightOperand); + + if (parent instanceof Ite && child instanceof Ite) + return true; + + if (parent instanceof UnaryExpression parentUnary && child instanceof UnaryExpression childUnary) + return parentUnary.getOp().equals("-") && childUnary.getOp().equals("-"); return false; } + private boolean needsBinaryParentheses(BinaryExpression parent, BinaryExpression child, boolean rightOperand) { + if (rightOperand) { + if (isRightAssociative(parent.getOperator())) + return true; + return !isRightAssociative(parent.getOperator()) + && (!isAssociative(parent.getOperator()) || !parent.getOperator().equals(child.getOperator())); + } + return isRightAssociative(parent.getOperator()); + } + private boolean isAssociative(String operator) { return operator.equals("&&") || operator.equals("||") || operator.equals("+") || operator.equals("*"); } + private boolean isRightAssociative(String operator) { + return operator.equals("-->"); + } + @Override public String visitAliasInvocation(AliasInvocation alias) { return alias.getName() + "(" + formatArguments(alias.getArgs()) + ")"; @@ -92,8 +111,8 @@ public String visitAliasInvocation(AliasInvocation alias) { @Override public String visitBinaryExpression(BinaryExpression exp) { - return formatOperand(exp, exp.getFirstOperand()) + " " + exp.getOperator() + " " - + formatRightOperand(exp, exp.getSecondOperand()); + return formatOperand(exp, exp.getFirstOperand(), false) + " " + exp.getOperator() + " " + + formatOperand(exp, exp.getSecondOperand(), true); } @Override @@ -103,13 +122,13 @@ public String visitFunctionInvocation(FunctionInvocation fun) { @Override public String visitGroupExpression(GroupExpression exp) { - return "(" + formatExpression(exp.getExpression()) + ")"; + return formatExpression(exp.getExpression()); } @Override public String visitIte(Ite ite) { return formatCondition(ite.getCondition()) + " ? " + formatCondition(ite.getThen()) + " : " - + formatOperand(ite, ite.getElse()); + + formatOperand(ite, ite.getElse(), true); } @Override @@ -144,7 +163,7 @@ public String visitLiteralString(LiteralString lit) { @Override public String visitUnaryExpression(UnaryExpression exp) { - return exp.getOp() + formatOperand(exp, exp.getExpression()); + return exp.getOp() + formatOperand(exp, exp.getExpression(), true); } @Override diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java index 25db19ab..ad96edad 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java @@ -1,93 +1,100 @@ package liquidjava.rj_language.ast; import static org.junit.jupiter.api.Assertions.assertEquals; + import org.junit.jupiter.api.Test; +import liquidjava.rj_language.parsing.RefinementsParser; + class ExpressionFormatterTest { + private static Expression parse(String refinement) { + return RefinementsParser.createAST(refinement, ""); + } + @Test void formatsUnaryAtoms() { - assertEquals("!x", new UnaryExpression("!", new Var("x")).toDisplayString()); - assertEquals("!false", new UnaryExpression("!", new LiteralBoolean(false)).toDisplayString()); + assertEquals("!x", parse("!x").toDisplayString()); + assertEquals("!false", parse("!false").toDisplayString()); } @Test void formatsInternalVariables() { - assertEquals("x", new Var("x").toDisplayString()); - assertEquals("x²", new Var("#x_2").toDisplayString()); - assertEquals("#fresh¹²", new Var("#fresh_12").toDisplayString()); - assertEquals("#ret³", new Var("#ret_3").toDisplayString()); - assertEquals("this#Class", new Var("this#Class").toDisplayString()); + assertEquals("x", parse("x").toDisplayString()); + assertEquals("x²", parse("#x_2").toDisplayString()); + assertEquals("#fresh¹²", parse("#fresh_12").toDisplayString()); + assertEquals("#ret³", parse("#ret_3").toDisplayString()); + assertEquals("this#Class", parse("this#Class").toDisplayString()); } @Test void formatsEnums() { - assertEquals("Color.RED", new Enum("Color", "RED").toDisplayString()); + assertEquals("Color.RED", parse("Color.RED").toDisplayString()); } @Test void formatsUnaryCompounds() { - Expression comparison = new BinaryExpression(new Var("x"), ">", new LiteralInt(0)); - - assertEquals("x > 0", comparison.toDisplayString()); - assertEquals("!(x > 0)", new UnaryExpression("!", comparison).toDisplayString()); - assertEquals("-(-x)", new UnaryExpression("-", new GroupExpression(new UnaryExpression("-", new Var("x")))) - .toDisplayString()); + assertEquals("x > 0", parse("x > 0").toDisplayString()); + assertEquals("!(x > 0)", parse("!(x > 0)").toDisplayString()); + assertEquals("-(-x)", parse("-(-x)").toDisplayString()); } @Test void formatsBinaryPrecedence() { - Expression sum = new BinaryExpression(new Var("a"), "+", new Var("b")); - Expression product = new BinaryExpression(new Var("b"), "*", new Var("c")); + assertEquals("(a + b) * c", parse("(a + b) * c").toDisplayString()); + assertEquals("a * (a + b)", parse("a * (a + b)").toDisplayString()); + assertEquals("a + b * c", parse("a + b * c").toDisplayString()); + assertEquals("a - (a + b)", parse("a - (a + b)").toDisplayString()); + assertEquals("a + b + c", parse("a + b + c").toDisplayString()); + assertEquals("b * c * c", parse("b * c * c").toDisplayString()); + } - assertEquals("(a + b) * c", new BinaryExpression(sum, "*", new Var("c")).toDisplayString()); - assertEquals("a * (a + b)", new BinaryExpression(new Var("a"), "*", sum).toDisplayString()); - assertEquals("a + b * c", new BinaryExpression(new Var("a"), "+", product).toDisplayString()); - assertEquals("a - (a + b)", new BinaryExpression(new Var("a"), "-", sum).toDisplayString()); - assertEquals("a + b + c", new BinaryExpression(sum, "+", new Var("c")).toDisplayString()); - assertEquals("b * c * c", new BinaryExpression(product, "*", new Var("c")).toDisplayString()); + @Test + void omitsUnnecessaryGroupParentheses() { + assertEquals("x", parse("(x)").toDisplayString()); + assertEquals("x", parse("((x))").toDisplayString()); + assertEquals("1", parse("(1)").toDisplayString()); + assertEquals("a > 0", parse("(a > 0)").toDisplayString()); + assertEquals("a + b + c", parse("a + (b + c)").toDisplayString()); + assertEquals("a + b * c", parse("a + (b * c)").toDisplayString()); + assertEquals("a && b > 0", parse("a && (b > 0)").toDisplayString()); + assertEquals("a && b && c", parse("a && (b && c)").toDisplayString()); + assertEquals("size(stack²⁹⁴) > 0", parse("(size(#stack_294) > 0)").toDisplayString()); + assertEquals("size(stack²⁹⁴) > 0 && ready", parse("(size(#stack_294) > 0) && ready").toDisplayString()); + assertEquals("ready && size(stack²⁹⁴) > 0", parse("ready && (size(#stack_294) > 0)").toDisplayString()); } @Test void formatsRightGrouping() { - Expression groupedSum = new GroupExpression(new BinaryExpression(new Var("b"), "+", new Var("c"))); - Expression groupedComparison = new GroupExpression( - new BinaryExpression(new LiteralInt(1), ">", new LiteralInt(0))); - - assertEquals("a - (b + c)", new BinaryExpression(new Var("a"), "-", groupedSum).toDisplayString()); - assertEquals("x == (1 > 0)", new BinaryExpression(new Var("x"), "==", groupedComparison).toDisplayString()); + assertEquals("a - (b + c)", parse("a - (b + c)").toDisplayString()); + assertEquals("a - (b - c)", parse("a - (b - c)").toDisplayString()); + assertEquals("a / (b * c)", parse("a / (b * c)").toDisplayString()); + assertEquals("(a || b) && c", parse("(a || b) && c").toDisplayString()); + assertEquals("x == (1 > 0)", parse("x == (1 > 0)").toDisplayString()); + assertEquals("a == (b == c)", parse("a == (b == c)").toDisplayString()); } @Test void formatsLogicalExpressions() { - Expression andExpression = new BinaryExpression(new Var("a"), "&&", new Var("b")); - Expression orExpression = new BinaryExpression(new Var("b"), "||", new Var("c")); - Expression implication = new BinaryExpression(new Var("b"), "-->", new Var("c")); - - assertEquals("a && b || c", new BinaryExpression(andExpression, "||", new Var("c")).toDisplayString()); - assertEquals("a && (b || c)", new BinaryExpression(new Var("a"), "&&", orExpression).toDisplayString()); - assertEquals("a --> (b --> c)", new BinaryExpression(new Var("a"), "-->", implication).toDisplayString()); - assertEquals("a && b && c", new BinaryExpression(andExpression, "&&", new Var("c")).toDisplayString()); - assertEquals("a || b || c", - new BinaryExpression(new BinaryExpression(new Var("a"), "||", new Var("b")), "||", new Var("c")) - .toDisplayString()); + assertEquals("a && b || c", parse("a && b || c").toDisplayString()); + assertEquals("a && (b || c)", parse("a && (b || c)").toDisplayString()); + assertEquals("a --> (b --> c)", parse("a --> b --> c").toDisplayString()); + assertEquals("a --> (b --> c)", parse("a --> (b --> c)").toDisplayString()); + assertEquals("a --> (b --> (c --> d))", parse("a --> b --> c --> d").toDisplayString()); + assertEquals("(a --> b) --> c", parse("(a --> b) --> c").toDisplayString()); + assertEquals("a && b && c", parse("a && b && c").toDisplayString()); + assertEquals("a || b || c", parse("a || b || c").toDisplayString()); } @Test void formatsTernaryExpressions() { - Expression ite = new Ite(new Var("a"), new Var("b"), new Var("c")); - Expression nestedElse = new Ite(new Var("c"), new Var("d"), new Var("e")); - - assertEquals("(a ? b : c) + d", new BinaryExpression(ite, "+", new Var("d")).toDisplayString()); - assertEquals("(a ? b : c) ? d : e", new Ite(ite, new Var("d"), new Var("e")).toDisplayString()); - assertEquals("a ? (b ? c : d) : e", - new Ite(new Var("a"), new Ite(new Var("b"), new Var("c"), new Var("d")), new Var("e")) - .toDisplayString()); - assertEquals("a ? b : c ? d : e", new Ite(new Var("a"), new Var("b"), nestedElse).toDisplayString()); - assertEquals("(a ? b : c) ? d : e", - new Ite(new GroupExpression(ite), new Var("d"), new Var("e")).toDisplayString()); - assertEquals("a ? b : (c ? d : e)", - new Ite(new Var("a"), new Var("b"), new GroupExpression(nestedElse)).toDisplayString()); - assertEquals("a ? b : c", new Ite(new Var("a"), new Var("b"), new Var("c")).toDisplayString()); + assertEquals("(a ? b : c) + d", parse("(a ? b : c) + d").toDisplayString()); + assertEquals("(a ? b : c) ? d : e", parse("(a ? b : c) ? d : e").toDisplayString()); + assertEquals("a ? (b ? c : d) : e", parse("a ? (b ? c : d) : e").toDisplayString()); + assertEquals("a ? b : (c ? d : e)", parse("a ? b : c ? d : e").toDisplayString()); + assertEquals("(a ? b : c) ? d : e", parse("(a ? b : c) ? d : e").toDisplayString()); + assertEquals("a ? b : (c ? d : e)", parse("a ? b : (c ? d : e)").toDisplayString()); + assertEquals("a ? b : (c ? d : (e ? f : g))", parse("a ? b : c ? d : e ? f : g").toDisplayString()); + assertEquals("a ? b : c", parse("a ? b : c").toDisplayString()); } }