Show variables by their name, with a line only to tell instances apart

liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java

@@ -78,4 +78,11 @@ static int count() {
     int pickByCount() {
         return random.nextInt(count()); // Expect: Refinement Error
     }
+
+    // the earlier values of a variable are written with the line they come from
+    void negate() {
+        @Refinement("_ > 0")
+        int b = 8;
+        b = -b; // Expect: Refinement Error
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/AliasExpansion.java

@@ -11,6 +11,8 @@
 import liquidjava.rj_language.ast.AliasInvocation;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.Var;
+import liquidjava.rj_language.ast.formatter.DisplayNames;
+import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -40,19 +42,19 @@ public String declaration() {
 
     /**
      * The expansions of the alias invocations in an expression, each invocation once in order of appearance, followed
-     * by those of the aliases their definitions use
+     * by those of the aliases their definitions use, naming the variables as the diagnostic does
      */
-    public static List<AliasExpansion> of(Expression expression, List<AliasWrapper> aliases) {
+    public static List<AliasExpansion> of(Expression expression, List<AliasWrapper> aliases, DisplayNames names) {
         Map<String, AliasWrapper> byName = new LinkedHashMap<>();
         for (AliasWrapper alias : aliases)
             byName.put(alias.getName(), alias);
         Map<String, AliasExpansion> expansions = new LinkedHashMap<>();
-        collect(expression, byName, expansions, new HashSet<>());
+        collect(expression, byName, names, expansions, new HashSet<>());
         return new ArrayList<>(expansions.values());
     }
 
     // Expands the invocations under expression, skipping aliases already being expanded so recursive ones end
-    private static void collect(Expression expression, Map<String, AliasWrapper> aliases,
+    private static void collect(Expression expression, Map<String, AliasWrapper> aliases, DisplayNames names,
             Map<String, AliasExpansion> expansions, Set<String> expanding) {
         List<AliasInvocation> invocations = new ArrayList<>();
         invocationsOf(expression, invocations);
@@ -64,14 +66,16 @@ private static void collect(Expression expression, Map<String, AliasWrapper> ali
             if (alias == null || expanding.contains(alias.getName()) || expansions.containsKey(key))
                 continue;
             Expression body = substituteArguments(alias, invocation.getArgs());
-            expansions.put(key, new AliasExpansion(invocation.toDisplayString(), body.toDisplayString(),
-                    alias.getName(), alias.getVarNames(), alias.getDefinition(), alias.getPosition()));
+            expansions.put(key,
+                    new AliasExpansion(ExpressionFormatter.format(invocation, names),
+                            ExpressionFormatter.format(body, names), alias.getName(), alias.getVarNames(),
+                            alias.getDefinition(), alias.getPosition()));
             bodies.put(key, body);
         }
         for (Map.Entry<String, Expression> body : bodies.entrySet()) {
             Set<String> inner = new HashSet<>(expanding);
             inner.add(expansions.get(body.getKey()).alias());
-            collect(body.getValue(), aliases, expansions, inner);
+            collect(body.getValue(), aliases, names, expansions, inner);
         }
     }
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ErrorMessage.java

@@ -0,0 +1,43 @@
+package liquidjava.diagnostics.errors;
+
+import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedToExpected;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.function.Predicate;
+
+import liquidjava.diagnostics.TranslationTable;
+import liquidjava.processor.context.PlacementInCode;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.formatter.DisplayNames;
+import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
+import liquidjava.rj_language.opt.VCSimplificationResult;
+
+/** The message of an error that found does not prove expected, and the names it gives the variables of both */
+record ErrorMessage(String text, DisplayNames names) {
+
+    /**
+     * Writes the facts of found about the values expected constrains and expected in frame, or only expected when
+     * showsFound rejects those facts; path conditions about other values stay in the derivation
+     */
+    static ErrorMessage of(Expression expected, VCSimplificationResult found, TranslationTable translationTable,
+            Predicate<Expression> showsFound, String frame) {
+        Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(), expected);
+        // the names of the message first, then those only the original found has, each with the line of its value
+        List<String> message = new ArrayList<>();
+        shown.getVariableNames(message);
+        expected.getVariableNames(message);
+        VCSimplificationResult original = found.getOriginal();
+        List<String> others = original.getBinders();
+        original.getImplication().toPredicate().getExpression().getVariableNames(others);
+        DisplayNames names = DisplayNames.of(message, others, name -> {
+            PlacementInCode placement = translationTable == null ? null : translationTable.get(name);
+            return placement == null ? null : placement.getLine();
+        });
+        String expectedText = ExpressionFormatter.format(expected, names);
+        String text = showsFound.test(shown)
+                ? String.format(frame, ExpressionFormatter.format(shown, names), expectedText)
+                : String.format("expected %s but could not prove it", expectedText);
+        return new ErrorMessage(text, names);
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java

@@ -3,6 +3,7 @@
 import liquidjava.diagnostics.LJDiagnostic;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.diagnostics.Colors;
+import liquidjava.rj_language.ast.formatter.DisplayNames;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -11,18 +12,30 @@
 public abstract class LJError extends LJDiagnostic {
 
     private final TranslationTable translationTable;
+    private final DisplayNames displayNames;
 
     public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable) {
         this(title, message, pos, translationTable, null);
     }
 
     public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable,
             String customMessage) {
-        super(title, message, pos, Colors.BOLD_RED, customMessage);
+        this(title, new ErrorMessage(message, null), pos, translationTable, customMessage);
+    }
+
+    LJError(String title, ErrorMessage message, SourcePosition pos, TranslationTable translationTable,
+            String customMessage) {
+        super(title, message.text(), pos, Colors.BOLD_RED, customMessage);
         this.translationTable = translationTable != null ? translationTable : new TranslationTable();
+        this.displayNames = message.names();
     }
 
     public TranslationTable getTranslationTable() {
         return translationTable;
     }
+
+    /** The names the error gives its variables, for every view of it to show them alike, or null when it has none */
+    public DisplayNames getDisplayNames() {
+        return displayNames;
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -19,7 +19,6 @@
 import liquidjava.rj_language.ast.Enum;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.Var;
-import liquidjava.rj_language.ast.formatter.VariableFormatter;
 import liquidjava.rj_language.opt.VCSimplificationResult;
 import liquidjava.smt.Counterexample;
 import liquidjava.utils.GeneratedNames;
@@ -52,19 +51,20 @@ public class RefinementError extends LJError {
     public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
             VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample,
             String customMessage, List<AliasWrapper> aliases) {
-        super("Refinement Error", message(expected, found), position, translationTable, customMessage);
+        super("Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable,
+                shown -> !isTrue(shown), "%s is not a subtype of %s"), position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
         Expression foundExpression = found.getImplication().toPredicate().getExpression();
-        this.foundAliases = AliasExpansion.of(foundExpression, aliases);
-        this.expectedAliases = AliasExpansion.of(expected.getExpression(), aliases);
+        this.foundAliases = AliasExpansion.of(foundExpression, aliases, getDisplayNames());
+        this.expectedAliases = AliasExpansion.of(expected.getExpression(), aliases, getDisplayNames());
         this.aliasDeclarations = aliasDeclarations(linkedToExpected(foundExpression, expected.getExpression()),
                 expected.getExpression(), aliases);
         this.counterexample = filterCounterexample(counterexample);
         this.declarationPosition = declarationPosition;
         if (!this.counterexample.isEmpty()) {
             String counterexampleString = this.counterexample.assignments().stream()
-                    .map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
+                    .map(a -> getDisplayNames().get(a.first()) + " == " + a.second())
                     .collect(Collectors.joining(" && "));
             setCounterexampleStr("Counterexample: " + counterexampleString);
         }
@@ -74,23 +74,11 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi
                     "Not enough information to prove the expected refinement. Add a refinement or condition to constrain it."));
     }
 
-    // Only the facts of found about the values expected constrains; path conditions about other values stay in the
-    // derivation
-    private static String message(Predicate expected, VCSimplificationResult found) {
-        Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(),
-                expected.getExpression());
-        if (isTrue(shown))
-            return String.format("expected %s but could not prove it", expected.getExpression().toDisplayString());
-        return String.format("%s is not a subtype of %s", shown.toDisplayString(),
-                expected.getExpression().toDisplayString());
-    }
-
     // Each alias the message uses once, with those their definitions use, as declared
-    private static List<String> aliasDeclarations(Expression shownFound, Expression expected,
-            List<AliasWrapper> aliases) {
+    private List<String> aliasDeclarations(Expression shownFound, Expression expected, List<AliasWrapper> aliases) {
         Map<String, String> declarations = new LinkedHashMap<>();
         for (Expression shown : List.of(shownFound, expected))
-            for (AliasExpansion expansion : AliasExpansion.of(shown, aliases))
+            for (AliasExpansion expansion : AliasExpansion.of(shown, aliases, getDisplayNames()))
                 declarations.putIfAbsent(expansion.alias(), expansion.declaration());
         return new ArrayList<>(declarations.values());
     }
@@ -182,10 +170,7 @@ private static boolean states(Expression term, Expression value, Pair<String, St
 
     // Binders of the VC chain before simplification, which keeps the variables in the order they were introduced
     private List<String> originalBinders() {
-        VCSimplificationResult original = getFound();
-        while (original.getOrigin() != null)
-            original = original.getOrigin();
-        return original.getBinders();
+        return getFound().getOriginal().getBinders();
     }
 
     // 0 for terms of expected found says nothing about, whose values alone break it, 1 for the other terms of

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java

@@ -1,7 +1,6 @@
 package liquidjava.diagnostics.errors;
 
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
-import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedToExpected;
 
 import java.util.List;
 
@@ -30,7 +29,9 @@ public class StateRefinementError extends LJError {
     public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
             VCSimplificationResult found, TranslationTable translationTable, String customMessage, List<Hint> hints,
             ErrorCategory category, StateErrorContext context) {
-        super("State Refinement Error", message(expected, found), position, translationTable, customMessage);
+        super("State Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable,
+                StateRefinementError::appliesGhost, "found %s but expected %s"), position, translationTable,
+                customMessage);
         this.declarationPosition = declarationPosition;
         this.expected = expected;
         this.found = found;
@@ -44,15 +45,6 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP
 
     // Only the facts of found about the objects of expected, and only when one of them tells a state: an alias or a
     // guard on another value says nothing about the state expected needs
-    private static String message(Predicate expected, VCSimplificationResult found) {
-        Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(),
-                expected.getExpression());
-        if (!appliesGhost(shown))
-            return String.format("expected %s but could not prove it", expected.getExpression().toDisplayString());
-        return String.format("found %s but expected %s", shown.toDisplayString(),
-                expected.getExpression().toDisplayString());
-    }
-
     private static boolean appliesGhost(Expression expression) {
         return expression instanceof FunctionInvocation
                 || expression.getChildren().stream().anyMatch(StateRefinementError::appliesGhost);

liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java

@@ -3,7 +3,9 @@
 import java.util.HashMap;
 import java.util.HashSet;
 import java.util.Map;
+import java.util.Objects;
 import java.util.Set;
+import java.util.stream.Stream;
 
 import liquidjava.api.CommandLineLauncher;
 import liquidjava.utils.Utils;
@@ -96,4 +98,11 @@ public Set<RefinedFunction> getMethods() {
     public Map<String, Set<String>> getFileScopes() {
         return fileScopes;
     }
+
+    /** The line where the value of a saved variable comes from, or null when unknown */
+    public Integer lineOf(String name) {
+        return Stream.concat(localVars.stream(), globalVars.stream()).filter(v -> v.getName().equals(name))
+                .map(RefinedVariable::getPlacementInCode).filter(Objects::nonNull).map(PlacementInCode::getLine)
+                .filter(Objects::nonNull).findFirst().orElse(null);
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java

@@ -31,6 +31,11 @@ public SourcePosition getAnnotationPosition() {
         return annotationPosition;
     }
 
+    /** The line of this placement, or null when it is not in code */
+    public Integer getLine() {
+        return position == null || !position.isValidPosition() ? null : position.getLine();
+    }
+
     public static PlacementInCode createPlacement(CtElement elem) {
         CtElement elemCopy = elem.clone();
         // cleanup annotations

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/DisplayNames.java

@@ -0,0 +1,81 @@
+package liquidjava.rj_language.ast.formatter;
+
+import java.util.Collection;
+import java.util.Comparator;
+import java.util.HashMap;
+import java.util.LinkedHashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+/**
+ * The names of the variables of one scope, such as an error or a refinement, as they are shown. A name is written as in
+ * code; when the scope has several variables written alike, one keeps the plain name and each other one gets the line
+ * its value comes from, {@code x@12}, numbered when they share a line or have none, {@code x@12#1} and {@code x@12#2}.
+ * The plain name goes to the declared variable, or else to its latest instance, preferring those shown first
+ */
+public final class DisplayNames {
+    private final Map<String, String> tags = new HashMap<>();
+
+    private DisplayNames() {
+    }
+
+    /**
+     * @param shown
+     *            the names shown first, such as those of an error message
+     * @param others
+     *            the other names of the scope
+     * @param lineOf
+     *            the line where the value of a variable comes from, or null when unknown
+     */
+    public static DisplayNames of(Collection<String> shown, Collection<String> others,
+            Function<String, Integer> lineOf) {
+        DisplayNames names = new DisplayNames();
+        Set<String> all = new LinkedHashSet<>(shown);
+        all.addAll(others);
+        Map<String, List<String>> alike = all.stream().collect(Collectors.groupingBy(VariableFormatter::format));
+        for (List<String> variables : alike.values()) {
+            if (variables.size() > 1)
+                names.tag(variables, shown, lineOf);
+        }
+        return names;
+    }
+
+    /**
+     * The display name of a variable, or of a ghost application over variables such as {@code size(#s_2)}
+     */
+    public String get(String name) {
+        return VariableFormatter.format(name, variable -> tags.getOrDefault(variable, ""));
+    }
+
+    private void tag(List<String> alike, Collection<String> shown, Function<String, Integer> lineOf) {
+        String plain = plainOf(alike, shown);
+        Map<String, List<String>> byLine = alike.stream().filter(name -> !name.equals(plain))
+                .sorted(Comparator.comparingInt(VariableFormatter::counterOf))
+                .collect(Collectors.groupingBy(name -> lineTag(lineOf.apply(name))));
+        byLine.forEach((line, variables) -> {
+            for (int i = 0; i < variables.size(); i++)
+                tags.put(variables.get(i), tagFor(line, i, variables.size()));
+        });
+    }
+
+    // The declared variable, or else the latest instance, preferring those shown
+    private static String plainOf(List<String> alike, Collection<String> shown) {
+        List<String> candidates = alike.stream().filter(shown::contains).toList();
+        return (candidates.isEmpty() ? alike : candidates).stream()
+                .max(Comparator.comparing((String name) -> VariableFormatter.counterOf(name) < 0)
+                        .thenComparing(VariableFormatter::counterOf))
+                .orElseThrow();
+    }
+
+    // The line alone tells apart a single value from it; values that share a line, or have none, are numbered
+    private static String tagFor(String line, int index, int count) {
+        return count == 1 && !line.isEmpty() ? line : line + "#" + (index + 1);
+    }
+
+    private static String lineTag(Integer line) {
+        return line == null ? "" : "@" + line;
+    }
+}