Write a call argument as the caller wrote it in refinement errors

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()) {

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<CtExpression<?>> arguments, RefinedFunction f,
             Map<String, String> map) throws LJError {
         List<Variable> functionParams = f.getArguments();

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<String, String> ARGUMENTS = new ConcurrentHashMap<>();
+
+    private ArgumentDisplayNames() {
+    }
+
+    /**
+     * Records that an argument instance ({@code #<parameter>_<n>}) 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);
+    }
+}

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);

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);
@@ -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#<declaring type>.<field>}, possibly with an instance counter
      */

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, 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*\\R\\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

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());

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());
+    }
 }