From 988441a56cb06ee8885b2b2b5ef6a14aafc3ba5d Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 19:39:27 +0000 Subject: [PATCH 1/3] Write a call argument as the caller wrote it in refinement errors When an argument is a call with a refinement, the error named its value after the callee's parameter (bound), which is not in the caller's code. It is now written as the call (items.size()) in Found, Expected and the counterexample. Only the display changes. Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/api/CommandLineLauncher.java | 2 ++ .../MethodsFunctionsChecker.java | 24 +++++++++++++ .../ast/formatter/ArgumentDisplayNames.java | 35 +++++++++++++++++++ .../ast/formatter/ExpressionNameResolver.java | 4 +-- .../ast/formatter/VariableFormatter.java | 11 ++++++ .../src/main/java/liquidjava/utils/Utils.java | 11 ++++++ .../api/tests/TestFoundBinders.java | 16 ++++++--- .../formatter/ExpressionNameResolverTest.java | 15 ++++++++ 8 files changed, 111 insertions(+), 7 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ArgumentDisplayNames.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 00b0256b..200c42f9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -9,6 +9,7 @@ import liquidjava.diagnostics.warnings.CustomWarning; import liquidjava.processor.RefinementProcessor; import liquidjava.processor.context.ContextHistory; +import liquidjava.rj_language.ast.formatter.ArgumentDisplayNames; import liquidjava.rj_language.ast.formatter.FieldDisplayNames; import liquidjava.specification.Refinement; import picocli.CommandLine; @@ -59,6 +60,7 @@ public static void launch(String... paths) { diagnostics.clear(); contextHistory.clearHistory(); FieldDisplayNames.clear(); + ArgumentDisplayNames.clear(); Launcher launcher = new Launcher(); for (String path : paths) { if (!new File(path).exists()) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 272c1e83..0e925fb8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -16,6 +16,10 @@ import liquidjava.processor.refinement_checker.object_checkers.AuxHierarchyRefinementsPassage; import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.Var; +import liquidjava.rj_language.ast.formatter.ArgumentDisplayNames; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; @@ -458,9 +462,29 @@ private String createVariableRepresentingArgument(CtExpression iArg, Variable met = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), met); String nVar = String.format(Formats.INSTANCE, fArg.getName(), rtc.getContext().getCounter()); rtc.getContext().addInstanceToContext(nVar, fArg.getType(), met.substituteVariable(Keys.WILDCARD, nVar), iArg); + if (describesCallResult(iArg, met)) + ArgumentDisplayNames.recordArgument(nVar, Utils.getSourceCode(iArg)); return nVar; } + /** + * Whether an argument is a call whose refinement states facts about its result, so that it reads best written as + * the call. Any other argument is refined as equal to its expression, and a call refined only as equal to the + * variable holding its result already reads well; named after their code, both would read as tautologies + */ + private static boolean describesCallResult(CtExpression argument, Predicate refinement) { + return argument instanceof CtInvocation && !isEqualityToVariable(refinement.getExpression()); + } + + /** + * Whether a refinement is {@code _ == x} for a variable {@code x} + */ + private static boolean isEqualityToVariable(Expression refinement) { + return refinement instanceof BinaryExpression equality && equality.getOperator().equals("==") + && equality.getFirstOperand()instanceof Var wildcard && wildcard.getName().equals(Keys.WILDCARD) + && equality.getSecondOperand() instanceof Var; + } + private void checkParameters(CtElement invocation, List> arguments, RefinedFunction f, Map map) throws LJError { List functionParams = f.getArguments(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ArgumentDisplayNames.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ArgumentDisplayNames.java new file mode 100644 index 00000000..832f26ae --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ArgumentDisplayNames.java @@ -0,0 +1,35 @@ +package liquidjava.rj_language.ast.formatter; + +import java.util.Map; +import java.util.concurrent.ConcurrentHashMap; + +/** + * The code of the call arguments that a verification names after the callee's parameter, so that + * {@link VariableFormatter} can write such an argument as the caller wrote it ({@code items.size()} rather than + * {@code bound}). Filled during a verification and cleared when the next one starts + */ +public final class ArgumentDisplayNames { + private static final Map ARGUMENTS = new ConcurrentHashMap<>(); + + private ArgumentDisplayNames() { + } + + /** + * Records that an argument instance ({@code #_}) stands for the argument {@code code}. Only the + * display changes + */ + public static void recordArgument(String instanceName, String code) { + ARGUMENTS.put(instanceName, code); + } + + /** + * Forgets what the previous verification recorded + */ + public static void clear() { + ARGUMENTS.clear(); + } + + static String argumentCode(String instanceName) { + return ARGUMENTS.get(instanceName); + } +} 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 35cdc836..5c3cf23f 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 @@ -22,8 +22,8 @@ public static ExpressionNameResolver forExpression(Expression expression) { public String resolveVariable(String name) { String formatted = VariableFormatter.format(name); - // a field is always written as in code, as its binder and the counterexample write it - if (VariableFormatter.isField(name)) + // a field or call argument is always written as in code, as its binder and the counterexample write it + if (VariableFormatter.isWrittenAsInCode(name)) return formatted; return isAmbiguous(name, variables, ExpressionNameResolver::getVariableSimpleName) ? formatted : Utils.getSimpleName(formatted); 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 8a1d57fd..f09a8444 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 @@ -16,6 +16,10 @@ public static String format(String name) { if (name == null) return null; + String argument = ArgumentDisplayNames.argumentCode(name); + if (argument != null) + return argument; + if (isApplication(name)) return formatApplication(name); @@ -37,6 +41,13 @@ public static String withoutInstance(String name) { return matcher.matches() ? matcher.group(1) : name; } + /** + * Whether a name is written as in code, qualifier included: a field or a call argument + */ + public static boolean isWrittenAsInCode(String name) { + return isField(name) || ArgumentDisplayNames.argumentCode(name) != null; + } + /** * Whether a name is that of a field, {@code this#.}, possibly with an instance counter */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index b85809e0..7215dae0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -178,6 +178,17 @@ public static String getExpressionFromPosition(SourcePosition position) { return null; } + /** + * The code of an element as written in the source, on one line; its printed form when the source is unknown + */ + public static String getSourceCode(CtElement element) { + SourcePosition position = element.getPosition(); + if (position == null || !position.isValidPosition() || position.getCompilationUnit() == null) + return element.toString(); + String source = position.getCompilationUnit().getOriginalSourceCode(); + return source.substring(position.getSourceStart(), position.getSourceEnd() + 1).replaceAll("\\s+", " "); + } + /** * Whether the context variable {@link #qualifyFieldName} names the field accessed here: a static field, or a field * of the current object ({@code f}, {@code this.f}, {@code super.f}, {@code Outer.this.f}). A field of another diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java index 6f5d44ff..6a839e0e 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -57,16 +57,22 @@ static void verify() { @Test void issueReproducerDropsTheTrueFieldRow() { Shown shown = ERRORS.get(25); - assertEquals(List.of("∀bound bound == size(this.items) && bound >= 0"), shown.rows()); - assertEquals("bound == size(this.items) && bound >= 0 is not a subtype of bound > 0", shown.message()); + assertEquals(List.of("∀items.size() items.size() == size(this.items) && items.size() >= 0"), shown.rows()); + } + + @Test + void callArgumentIsWrittenAsTheCallerWroteIt() { + Shown shown = ERRORS.get(25); + assertEquals("items.size() == size(this.items) && items.size() >= 0 is not a subtype of items.size() > 0", + shown.message()); + assertEquals("Counterexample: items.size() == 0", shown.counterexample()); } @Test void steppingBackReachesTheOriginalWithTheDroppedRow() { Shown shown = ERRORS.get(25); - assertEquals( - List.of("∀this.items true", "∀items items == this.items", "∀bound bound == size(items) && bound >= 0"), - shown.originalRows()); + assertEquals(List.of("∀this.items true", "∀items items == this.items", + "∀items.size() items.size() == size(items) && items.size() >= 0"), shown.originalRows()); assertEquals(List.of("Substitution", "Binder"), shown.steps()); assertEquals(List.of("this#testSuite.classes.found_binders_error.Basket.items", "#items_", "#bound_"), shown.originalBinders()); 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 index 848f70a5..ec77e281 100644 --- 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 @@ -2,6 +2,7 @@ import static org.junit.jupiter.api.Assertions.assertEquals; +import org.junit.jupiter.api.AfterEach; import org.junit.jupiter.api.Test; import liquidjava.rj_language.Predicate; @@ -11,6 +12,11 @@ class ExpressionNameResolverTest { + @AfterEach + void forgetRecordedNames() { + ArgumentDisplayNames.clear(); + } + private static Expression parse(String refinement, String prefix) { return RefinementsParser.createAST(refinement, prefix); } @@ -51,4 +57,13 @@ void writesFieldsAsInCodeNextToALocalOfTheSameName() { assertEquals("items⁵ == this.items", expression.toDisplayString()); } + + @Test + void writesACallArgumentAsTheCallerWroteIt() { + ArgumentDisplayNames.recordArgument("#bound_83", "failures.size()"); + Expression expression = Predicate + .createEquals(Predicate.createVar("#bound_83"), Predicate.createLit("0", "int")).getExpression(); + + assertEquals("failures.size() == 0", expression.toDisplayString()); + } } From 639de86f3502359f35b5864c1a1899f234c2fed2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 19:44:51 +0000 Subject: [PATCH 2/3] Join only the lines of a call argument, keeping its spacing Co-Authored-By: Claude Opus 5.5 --- liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 7215dae0..91ea2f81 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -179,14 +179,14 @@ public static String getExpressionFromPosition(SourcePosition position) { } /** - * The code of an element as written in the source, on one line; its printed form when the source is unknown + * The code of an element as written in the source, its lines joined; its printed form when the source is unknown */ public static String getSourceCode(CtElement element) { SourcePosition position = element.getPosition(); if (position == null || !position.isValidPosition() || position.getCompilationUnit() == null) return element.toString(); String source = position.getCompilationUnit().getOriginalSourceCode(); - return source.substring(position.getSourceStart(), position.getSourceEnd() + 1).replaceAll("\\s+", " "); + return source.substring(position.getSourceStart(), position.getSourceEnd() + 1).replaceAll("\\s*\\R\\s*", " "); } /** From abf341fc0ab2b336bfc3658292295e36a0440035 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 19:48:36 +0000 Subject: [PATCH 3/3] Keep the instance counter on a call argument written as code Two calls written alike can return different values, so the counter tells them apart, as it does for every other instance. Co-Authored-By: Claude Opus 5.5 --- .../rj_language/ast/formatter/VariableFormatter.java | 8 ++++---- .../ast/formatter/ExpressionNameResolverTest.java | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) 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 f09a8444..83cebd2c 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 @@ -16,10 +16,6 @@ public static String format(String name) { if (name == null) return null; - String argument = ArgumentDisplayNames.argumentCode(name); - if (argument != null) - return argument; - if (isApplication(name)) return formatApplication(name); @@ -29,6 +25,10 @@ public static String format(String name) { String baseName = matcher.group(1); String counter = matcher.group(2); + // the counter tells apart calls written alike, which can return different values + String argument = ArgumentDisplayNames.argumentCode(name); + if (argument != null) + return argument + toSuperscript(counter); String receiver = FieldDisplayNames.writeReceiver(name); if (receiver != null && isField(baseName)) return (receiver.isEmpty() ? "" : receiver + ".") + fieldOf(baseName) + toSuperscript(counter); 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 index ec77e281..1d58f282 100644 --- 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 @@ -64,6 +64,6 @@ void writesACallArgumentAsTheCallerWroteIt() { Expression expression = Predicate .createEquals(Predicate.createVar("#bound_83"), Predicate.createLit("0", "int")).getExpression(); - assertEquals("failures.size() == 0", expression.toDisplayString()); + assertEquals("failures.size()⁸³ == 0", expression.toDisplayString()); } }