From b73c128e9394b9ebe0e1f51677810a5bbc07fcc6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 8 Aug 2026 18:17:58 +0100 Subject: [PATCH 1/3] Simplify Unambiguous Qualified Names --- .../ast/formatter/ExpressionFormatter.java | 13 ++++-- .../ast/formatter/ExpressionNameResolver.java | 44 +++++++++++++++++++ .../ast/ExpressionFormatterTest.java | 24 ++++++++-- 3 files changed, 74 insertions(+), 7 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java 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 88cab1e1a..7016229d2 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 @@ -19,7 +19,6 @@ 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 @@ -27,12 +26,18 @@ */ public class ExpressionFormatter implements ExpressionVisitor { + private final ExpressionNameResolver nameResolver; + + private ExpressionFormatter(Expression expression) { + this.nameResolver = ExpressionNameResolver.forExpression(expression); + } + public static String format(Predicate predicate) { return format(predicate.getExpression()); } public static String format(Expression expression) { - return new ExpressionFormatter().formatExpression(expression); + return new ExpressionFormatter(expression).formatExpression(expression); } private String formatExpression(Expression expression) { @@ -108,7 +113,7 @@ public String visitBinaryExpression(BinaryExpression exp) { @Override public String visitFunctionInvocation(FunctionInvocation fun) { - return Utils.getSimpleName(fun.getName()) + "(" + formatArguments(fun.getArgs()) + ")"; + return nameResolver.resolveFunction(fun.getName()) + "(" + formatArguments(fun.getArgs()) + ")"; } @Override @@ -159,6 +164,6 @@ public String visitEnum(Enum en) { @Override public String visitVar(Var var) { - return VariableFormatter.format(var.getName()); + return nameResolver.resolveVariable(var.getName()); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java new file mode 100644 index 000000000..b585db3b7 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java @@ -0,0 +1,44 @@ +package liquidjava.rj_language.ast.formatter; + +import java.util.HashSet; +import java.util.Set; + +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.Var; +import liquidjava.utils.Utils; + +/** Simplifies unambiguous qualified names within one expression */ +final class ExpressionNameResolver { + private final Set variables = new HashSet<>(); + private final Set functions = new HashSet<>(); + + public static ExpressionNameResolver forExpression(Expression expression) { + ExpressionNameResolver resolver = new ExpressionNameResolver(); + resolver.collect(expression); + return resolver; + } + + public String resolveVariable(String name) { + return resolve(VariableFormatter.format(name), variables); + } + + public String resolveFunction(String name) { + return resolve(name, functions); + } + + private void collect(Expression expression) { + if (expression instanceof Var var) + variables.add(VariableFormatter.format(var.getName())); + else if (expression instanceof FunctionInvocation function) + functions.add(function.getName()); + expression.getChildren().forEach(this::collect); + } + + private static String resolve(String name, Set names) { + String simpleName = Utils.getSimpleName(name); + boolean ambiguous = names.stream() + .anyMatch(other -> !other.equals(name) && Utils.getSimpleName(other).equals(simpleName)); + return ambiguous ? name : simpleName; + } +} 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 ad96edad5..b00c7dbab 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 @@ -9,11 +9,15 @@ class ExpressionFormatterTest { private static Expression parse(String refinement) { - return RefinementsParser.createAST(refinement, ""); + return parse(refinement, ""); + } + + private static Expression parse(String refinement, String prefix) { + return RefinementsParser.createAST(refinement, prefix); } @Test - void formatsUnaryAtoms() { + void formatsUnary() { assertEquals("!x", parse("!x").toDisplayString()); assertEquals("!false", parse("!false").toDisplayString()); } @@ -50,7 +54,7 @@ void formatsBinaryPrecedence() { } @Test - void omitsUnnecessaryGroupParentheses() { + void formatsGrouping() { assertEquals("x", parse("(x)").toDisplayString()); assertEquals("x", parse("((x))").toDisplayString()); assertEquals("1", parse("(1)").toDisplayString()); @@ -97,4 +101,18 @@ void formatsTernaryExpressions() { 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()); } + + @Test + void formatsWithQualifiedNames() { + Expression exp = new BinaryExpression(parse("size(this)", "java.util.ArrayList"), "==", + parse("size(this)", "java.util.ArrayDeque")); + assertEquals("java.util.ArrayList.size(this) == java.util.ArrayDeque.size(this)", + exp.toDisplayString()); + } + + @Test + void formatsWithoutQualifiedNames() { + assertEquals("size(this)", parse("size(this)", "java.util.List").toDisplayString()); + assertEquals("size(this) == size(this)", parse("size(this) == size(this)", "java.util.List").toDisplayString()); + } } From 24158c7fe729a01904711c726deaa176051c076b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 8 Aug 2026 18:53:58 +0100 Subject: [PATCH 2/3] Fix Ambiguous Variable Names With Different Instances --- .../ast/formatter/ExpressionNameResolver.java | 25 +++++++++++-------- .../ast/formatter/VariableFormatter.java | 7 +++++- .../ast/ExpressionFormatterTest.java | 11 +++++--- 3 files changed, 29 insertions(+), 14 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java index b585db3b7..b7a2ae7e4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java @@ -2,6 +2,7 @@ import java.util.HashSet; import java.util.Set; +import java.util.function.Function; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.FunctionInvocation; @@ -20,25 +21,29 @@ public static ExpressionNameResolver forExpression(Expression expression) { } public String resolveVariable(String name) { - return resolve(VariableFormatter.format(name), variables); + String formatted = VariableFormatter.format(name); + return isAmbiguous(name, variables, ExpressionNameResolver::getVariableSimpleName) ? formatted + : Utils.getSimpleName(formatted); } public String resolveFunction(String name) { - return resolve(name, functions); + return isAmbiguous(name, functions, Utils::getSimpleName) ? name : Utils.getSimpleName(name); } private void collect(Expression expression) { if (expression instanceof Var var) - variables.add(VariableFormatter.format(var.getName())); - else if (expression instanceof FunctionInvocation function) - functions.add(function.getName()); + variables.add(var.getName()); + else if (expression instanceof FunctionInvocation fun) + functions.add(fun.getName()); expression.getChildren().forEach(this::collect); } - private static String resolve(String name, Set names) { - String simpleName = Utils.getSimpleName(name); - boolean ambiguous = names.stream() - .anyMatch(other -> !other.equals(name) && Utils.getSimpleName(other).equals(simpleName)); - return ambiguous ? name : simpleName; + private static String getVariableSimpleName(String name) { + return Utils.getSimpleName(VariableFormatter.withoutInstance(name)); + } + + private static boolean isAmbiguous(String name, Set names, Function getSimpleName) { + String simpleName = getSimpleName.apply(name); + return names.stream().anyMatch(other -> !other.equals(name) && getSimpleName.apply(other).equals(simpleName)); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java index 625aa619d..0a9422932 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java @@ -24,6 +24,11 @@ public static String format(String name) { return prefix + baseName + toSuperscript(counter); } + public static String withoutInstance(String name) { + Matcher matcher = INSTACE_VAR_PATTERN.matcher(name); + return matcher.matches() ? matcher.group(1) : name; + } + private static String toSuperscript(String number) { StringBuilder sb = new StringBuilder(number.length()); for (char c : number.toCharArray()) { @@ -38,4 +43,4 @@ private static String toSuperscript(String number) { private static boolean isSpecialIdentifier(String id) { return id.equals("fresh") || id.equals("ret"); } -} \ No newline at end of file +} 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 b00c7dbab..c2ea71b1d 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 @@ -4,6 +4,7 @@ import org.junit.jupiter.api.Test; +import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.RefinementsParser; class ExpressionFormatterTest { @@ -106,13 +107,17 @@ void formatsTernaryExpressions() { void formatsWithQualifiedNames() { Expression exp = new BinaryExpression(parse("size(this)", "java.util.ArrayList"), "==", parse("size(this)", "java.util.ArrayDeque")); - assertEquals("java.util.ArrayList.size(this) == java.util.ArrayDeque.size(this)", - exp.toDisplayString()); + assertEquals("java.util.ArrayList.size(this) == java.util.ArrayDeque.size(this)", exp.toDisplayString()); + + Predicate differentInstances = Predicate.createEquals(Predicate.createVar("#java.util.ArrayList.size_1"), + Predicate.createVar("#java.util.ArrayDeque.size_2")); + assertEquals("java.util.ArrayList.size¹ == java.util.ArrayDeque.size²", + differentInstances.getExpression().toDisplayString()); } @Test void formatsWithoutQualifiedNames() { assertEquals("size(this)", parse("size(this)", "java.util.List").toDisplayString()); - assertEquals("size(this) == size(this)", parse("size(this) == size(this)", "java.util.List").toDisplayString()); + assertEquals("size(this) == size(this)", parse("size(this) == size(this)", "java.util.List").toDisplayString()); } } From 06cbeebbba29a697216455b41f7e15b307ca8140 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 8 Aug 2026 19:08:05 +0100 Subject: [PATCH 3/3] Split Tests --- .../ast/ExpressionFormatterTest.java | 33 +------------- .../formatter/ExpressionNameResolverTest.java | 45 +++++++++++++++++++ .../ast/formatter/VariableFormatterTest.java | 17 +++++++ 3 files changed, 63 insertions(+), 32 deletions(-) create mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolverTest.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java 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 c2ea71b1d..a7d013ecc 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 @@ -4,17 +4,12 @@ import org.junit.jupiter.api.Test; -import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.RefinementsParser; class ExpressionFormatterTest { private static Expression parse(String refinement) { - return parse(refinement, ""); - } - - private static Expression parse(String refinement, String prefix) { - return RefinementsParser.createAST(refinement, prefix); + return RefinementsParser.createAST(refinement, ""); } @Test @@ -23,15 +18,6 @@ void formatsUnary() { assertEquals("!false", parse("!false").toDisplayString()); } - @Test - void formatsInternalVariables() { - 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", parse("Color.RED").toDisplayString()); @@ -103,21 +89,4 @@ void formatsTernaryExpressions() { assertEquals("a ? b : c", parse("a ? b : c").toDisplayString()); } - @Test - void formatsWithQualifiedNames() { - Expression exp = new BinaryExpression(parse("size(this)", "java.util.ArrayList"), "==", - parse("size(this)", "java.util.ArrayDeque")); - assertEquals("java.util.ArrayList.size(this) == java.util.ArrayDeque.size(this)", exp.toDisplayString()); - - Predicate differentInstances = Predicate.createEquals(Predicate.createVar("#java.util.ArrayList.size_1"), - Predicate.createVar("#java.util.ArrayDeque.size_2")); - assertEquals("java.util.ArrayList.size¹ == java.util.ArrayDeque.size²", - differentInstances.getExpression().toDisplayString()); - } - - @Test - void formatsWithoutQualifiedNames() { - assertEquals("size(this)", parse("size(this)", "java.util.List").toDisplayString()); - assertEquals("size(this) == size(this)", parse("size(this) == size(this)", "java.util.List").toDisplayString()); - } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolverTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolverTest.java new file mode 100644 index 000000000..3fc91abea --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolverTest.java @@ -0,0 +1,45 @@ +package liquidjava.rj_language.ast.formatter; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +import org.junit.jupiter.api.Test; + +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.parsing.RefinementsParser; + +class ExpressionNameResolverTest { + + private static Expression parse(String refinement, String prefix) { + return RefinementsParser.createAST(refinement, prefix); + } + + @Test + void stripsQualifiedNamesWhenUnambiguous() { + ExpressionNameResolver resolver = ExpressionNameResolver + .forExpression(parse("size(this) == size(this)", "java.util.List")); + + assertEquals("size", resolver.resolveFunction("java.util.List.size")); + } + + @Test + void keepsQualifiedNamesForDifferentPrefixes() { + Expression expression = new BinaryExpression(parse("size(this)", "java.util.ArrayList"), "==", + parse("size(this)", "java.util.ArrayDeque")); + ExpressionNameResolver resolver = ExpressionNameResolver.forExpression(expression); + + assertEquals("java.util.ArrayList.size", resolver.resolveFunction("java.util.ArrayList.size")); + assertEquals("java.util.ArrayDeque.size", resolver.resolveFunction("java.util.ArrayDeque.size")); + } + + @Test + void keepsQualifiedNamesForDifferentInstances() { + Predicate differentInstances = Predicate.createEquals(Predicate.createVar("#java.util.ArrayList.size_1"), + Predicate.createVar("#java.util.ArrayDeque.size_2")); + ExpressionNameResolver resolver = ExpressionNameResolver.forExpression(differentInstances.getExpression()); + + assertEquals("java.util.ArrayList.size¹", resolver.resolveVariable("#java.util.ArrayList.size_1")); + assertEquals("java.util.ArrayDeque.size²", resolver.resolveVariable("#java.util.ArrayDeque.size_2")); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java new file mode 100644 index 000000000..cf92ff266 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java @@ -0,0 +1,17 @@ +package liquidjava.rj_language.ast.formatter; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +import org.junit.jupiter.api.Test; + +class VariableFormatterTest { + + @Test + void formatsVariables() { + assertEquals("x", VariableFormatter.format("x")); + assertEquals("x²", VariableFormatter.format("#x_2")); + assertEquals("#fresh¹²", VariableFormatter.format("#fresh_12")); + assertEquals("#ret³", VariableFormatter.format("#ret_3")); + assertEquals("this#Class", VariableFormatter.format("this#Class")); + } +}