From 0136a4bc63e08563208afb6f9b92c25acf7be90c Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 5 Nov 2026 11:59:21 +0000 Subject: [PATCH] Write a call argument as the caller wrote it in refinement errors When an argument is a call, 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, keeping its instance counter. Only the display changes. Co-Authored-By: Claude Opus 5.5 --- .../classes/found_binders_error/Basket.java | 10 ++++++ .../liquidjava/api/CommandLineLauncher.java | 2 ++ .../MethodsFunctionsChecker.java | 5 +++ .../ast/formatter/ArgumentDisplayNames.java | 35 +++++++++++++++++++ .../ast/formatter/ExpressionNameResolver.java | 4 +-- .../ast/formatter/VariableFormatter.java | 4 +++ .../api/tests/TestFoundBinders.java | 15 +++++--- 7 files changed, 68 insertions(+), 7 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ArgumentDisplayNames.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java index 683d4ce5..784a0eeb 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java +++ b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java @@ -68,4 +68,14 @@ void addUp(int first, int second) { void forward(int t) { positive(t); // Expect: Refinement Error } + + @Refinement("_ >= 0") + static int count() { + return 0; + } + + // a call argument is written as the caller wrote it, not as the callee's parameter + int pickByCount() { + return random.nextInt(count()); // Expect: Refinement Error + } } 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 74233c3e..8c8f4ade 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,7 @@ 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.formatter.ArgumentDisplayNames; import liquidjava.utils.GeneratedNames; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; @@ -459,6 +460,10 @@ 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); + // a call in the source reads as written; any other argument is refined as equal to its code, which would read + // as a tautology + if (iArg instanceof CtInvocation && iArg.getPosition().isValidPosition()) + ArgumentDisplayNames.recordArgument(nVar, iArg.getOriginalSourceFragment().getSourceCode()); return nVar; } 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..0c72a785 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.isField(name) || ArgumentDisplayNames.argumentCode(name) != null) 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..66ccca41 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 @@ -25,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/api/tests/TestFoundBinders.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java index 6f5d44ff..6861fffa 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,21 @@ 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(79); + assertEquals("count() >= 0 is not a subtype of count() > 0", shown.message()); + assertEquals("Counterexample: count() == 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());