Show the definitions of the aliases a refinement error uses

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

@@ -0,0 +1,96 @@
+package liquidjava.diagnostics;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+import liquidjava.processor.context.AliasWrapper;
+import liquidjava.rj_language.ast.AliasInvocation;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.Var;
+import spoon.reflect.cu.SourcePosition;
+
+/**
+ * An alias invocation in a diagnostic and what it stands for
+ *
+ * @param invocation
+ *            the invocation as shown in the diagnostic, e.g. {@code Nat(n)}
+ * @param expansion
+ *            the definition with the parameters replaced by the arguments, e.g. {@code n >= 0}; aliases it uses are
+ *            kept and have their own expansions
+ * @param alias
+ *            the alias name
+ * @param parameters
+ *            the parameter names of the alias
+ * @param definition
+ *            the definition as written in the alias declaration
+ * @param declarationPosition
+ *            where the alias is declared
+ */
+public record AliasExpansion(String invocation, String expansion, String alias, List<String> parameters,
+        String definition, SourcePosition declarationPosition) {
+
+    /** The alias as it is declared, e.g. {@code Nat(x) = x >= 0} */
+    public String declaration() {
+        return alias + "(" + String.join(", ", parameters) + ") = " + definition;
+    }
+
+    /**
+     * 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
+     */
+    public static List<AliasExpansion> of(Expression expression, List<AliasWrapper> aliases) {
+        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<>());
+        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,
+            Map<String, AliasExpansion> expansions, Set<String> expanding) {
+        List<AliasInvocation> invocations = new ArrayList<>();
+        invocationsOf(expression, invocations);
+        Map<String, Expression> bodies = new LinkedHashMap<>();
+        for (AliasInvocation invocation : invocations) {
+            AliasWrapper alias = aliases.get(invocation.getName());
+            // keyed by the invocation itself, since different names can display the same
+            String key = invocation.toString();
+            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()));
+            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);
+        }
+    }
+
+    private static void invocationsOf(Expression expression, List<AliasInvocation> invocations) {
+        if (expression instanceof AliasInvocation invocation)
+            invocations.add(invocation);
+        for (Expression child : expression.getChildren())
+            invocationsOf(child, invocations);
+    }
+
+    // Replaces all parameters at once, through placeholders, so an argument naming another parameter is kept
+    private static Expression substituteArguments(AliasWrapper alias, List<Expression> args) {
+        Expression body = alias.getClonedPredicate().getExpression();
+        List<String> parameters = alias.getVarNames();
+        int n = Math.min(parameters.size(), args.size());
+        for (int i = 0; i < n; i++)
+            body = body.substitute(new Var(parameters.get(i)), new Var("#alias_parameter_" + i));
+        for (int i = 0; i < n; i++)
+            body = body.substitute(new Var("#alias_parameter_" + i), args.get(i).clone());
+        return body;
+    }
+}

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

@@ -70,6 +70,11 @@ public SourcePosition getDeclarationPosition() {
         return null;
     }
 
+    /** Lines printed under the message that explain it, such as what the names it uses mean */
+    public List<String> getMessageNotes() {
+        return List.of();
+    }
+
     public void setPosition(SourcePosition pos) {
         if (pos == null || pos.getFile() == null)
             return;
@@ -108,6 +113,8 @@ public String toString() {
         // title
         sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message)
                 .append("\n");
+        for (String note : getMessageNotes())
+            sb.append("  ").append(note).append("\n");
 
         // snippet
         String snippet = getSnippet();

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

@@ -3,13 +3,17 @@
 import java.util.ArrayList;
 import java.util.Comparator;
 import java.util.HashSet;
+import java.util.LinkedHashMap;
 import java.util.List;
+import java.util.Map;
 import java.util.Set;
 import java.util.stream.Collectors;
 
+import liquidjava.diagnostics.AliasExpansion;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.diagnostics.categories.ErrorCategory;
 import liquidjava.diagnostics.hints.Hint;
+import liquidjava.processor.context.AliasWrapper;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Enum;
@@ -41,13 +45,21 @@ public class RefinementError extends LJError {
     private final VCSimplificationResult found;
     private final Counterexample counterexample;
     private final SourcePosition declarationPosition;
+    private final List<AliasExpansion> foundAliases;
+    private final List<AliasExpansion> expectedAliases;
+    private final List<String> aliasDeclarations;
 
     public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
             VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample,
-            String customMessage) {
+            String customMessage, List<AliasWrapper> aliases) {
         super("Refinement Error", message(expected, found), 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.aliasDeclarations = aliasDeclarations(linkedToExpected(foundExpression, expected.getExpression()),
+                expected.getExpression(), aliases);
         this.counterexample = filterCounterexample(counterexample);
         this.declarationPosition = declarationPosition;
         if (!this.counterexample.isEmpty()) {
@@ -73,6 +85,16 @@ private static String message(Predicate expected, VCSimplificationResult found)
                 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) {
+        Map<String, String> declarations = new LinkedHashMap<>();
+        for (Expression shown : List.of(shownFound, expected))
+            for (AliasExpansion expansion : AliasExpansion.of(shown, aliases))
+                declarations.putIfAbsent(expansion.alias(), expansion.declaration());
+        return new ArrayList<>(declarations.values());
+    }
+
     /** Unknown when what was found says nothing about the values the expected refinement constrains */
     private static ErrorCategory categoryOf(Predicate expected, VCSimplificationResult found) {
         List<String> foundVariables = found.getImplication().toPredicate().getVariableNames();
@@ -97,6 +119,22 @@ public VCSimplificationResult getFound() {
         return found;
     }
 
+    /** The alias invocations in found and what they stand for */
+    public List<AliasExpansion> getFoundAliases() {
+        return foundAliases;
+    }
+
+    /** The alias invocations in expected and what they stand for */
+    public List<AliasExpansion> getExpectedAliases() {
+        return expectedAliases;
+    }
+
+    /** A where line declaring each alias the message uses */
+    @Override
+    public List<String> getMessageNotes() {
+        return aliasDeclarations.stream().map(declaration -> "where " + declaration).toList();
+    }
+
     // Keeps the counterexample assignments to the terms of expected and of the found facts linked to them, except
     // values found already states, so there is none when found fixes every value expected depends on. The terms of
     // expected come first, those found says nothing about before the rest, then the linked terms in the order of the

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

@@ -2,9 +2,12 @@
 
 import java.util.ArrayList;
 import java.util.List;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
 import liquidjava.processor.facade.AliasDTO;
 import liquidjava.rj_language.Predicate;
 import liquidjava.utils.Utils;
+import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.factory.Factory;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -13,10 +16,17 @@ public class AliasWrapper {
     private final List<CtTypeReference<?>> varTypes;
     private final List<String> varNames;
     private final Predicate expression;
+    private final String definition;
+    private final SourcePosition position;
 
-    public AliasWrapper(AliasDTO a, Factory factory, String klass, String path) {
+    private static final Pattern LITERAL_OR_SPACES = Pattern
+            .compile("\"(?:\\\\.|[^\"\\\\])*\"|'(?:\\\\.|[^'\\\\])*'|\\s+");
+
+    public AliasWrapper(AliasDTO a, Factory factory, String klass, String path, SourcePosition position) {
         name = a.getName();
         expression = new Predicate(a.getExpression());
+        definition = a.getRef() == null ? expression.getExpression().toDisplayString() : oneLine(a.getRef());
+        this.position = position;
         varTypes = new ArrayList<>();
         varNames = a.getVarNames();
         for (String s : a.getVarTypes()) {
@@ -37,6 +47,22 @@ public List<String> getVarNames() {
         return varNames;
     }
 
+    // Collapses each run of whitespace into one space, except inside string and char literals
+    private static String oneLine(String definition) {
+        return LITERAL_OR_SPACES.matcher(definition.strip())
+                .replaceAll(m -> m.group().isBlank() ? " " : Matcher.quoteReplacement(m.group()));
+    }
+
+    /** The definition as written in the declaration, on one line */
+    public String getDefinition() {
+        return definition;
+    }
+
+    /** Position of the alias declaration */
+    public SourcePosition getPosition() {
+        return position;
+    }
+
     public Predicate getClonedPredicate() {
         return expression.clone();
     }

liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java

@@ -65,4 +65,9 @@ public List<String> getVarNames() {
     public Expression getExpression() {
         return expression;
     }
+
+    /** The definition as written in the alias declaration, or null when built from an expression */
+    public String getRef() {
+        return ref;
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -339,7 +339,7 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio
                     throw new InvalidRefinementError(position, "Refinement alias must return a boolean expression",
                             ref);
                 }
-                AliasWrapper aw = new AliasWrapper(a, factory, klass, path);
+                AliasWrapper aw = new AliasWrapper(a, factory, klass, path, position);
                 context.addAlias(aw);
             }
         } catch (LJError e) {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -85,7 +85,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         if (result.isError()) {
             throw new RefinementError(element.getPosition(), declarationPosition, expectedType,
                     implBeforeChange.simplify(NeededVariables.forRefinementError(expectedType)), map,
-                    result.getCounterexample(), customMessage);
+                    result.getCounterexample(), customMessage, context.getAliases());
         }
     }
 
@@ -445,7 +445,8 @@ protected void throwRefinementError(SourcePosition position, SourcePosition decl
         TranslationTable map = new TranslationTable();
         VCImplication premises = buildPremiseChain(map, expected, found);
         throw new RefinementError(position, declarationPosition, expected,
-                premises.simplify(NeededVariables.forRefinementError(expected)), map, counterexample, customMessage);
+                premises.simplify(NeededVariables.forRefinementError(expected)), map, counterexample, customMessage,
+                context.getAliases());
     }
 
     /** What a state refinement error shows as found: what is known about the variables of both predicates */

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestAliasExpansions.java

@@ -0,0 +1,53 @@
+package liquidjava.api.tests;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.util.List;
+
+import org.junit.jupiter.api.Test;
+
+import liquidjava.api.CommandLineLauncher;
+import liquidjava.diagnostics.AliasExpansion;
+import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.errors.LJError;
+import liquidjava.diagnostics.errors.RefinementError;
+
+class TestAliasExpansions {
+
+    private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/";
+
+    @Test
+    void foundAndExpectedRecordTheirSubstitutedAliases() {
+        RefinementError error = verify("ErrorAlias.java");
+        assertExpansion(error.getFoundAliases(), "InRange(j, 10, 16)", "10 < j && j < 16");
+        assertExpansion(error.getExpectedAliases(), "InRange(j, 10, 15)", "10 < j && j < 15");
+        AliasExpansion expected = error.getExpectedAliases().get(0);
+        assertEquals("InRange", expected.alias());
+        assertEquals(List.of("val", "low", "up"), expected.parameters());
+        assertEquals(7, expected.declarationPosition().getLine());
+    }
+
+    @Test
+    void messageDeclaresEachAliasOnceAsWritten() {
+        RefinementError error = verify("ErrorStaticFinalInAlias.java");
+        assertEquals(
+                List.of("where Mode(x) = x == ImageWriteParam.MODE_DISABLED || x == ImageWriteParam.MODE_DEFAULT "
+                        + "|| x == ImageWriteParam.MODE_EXPLICIT || x == ImageWriteParam.MODE_COPY_FROM_METADATA"),
+                error.getMessageNotes());
+        assertTrue(error.toString().contains(error.getMessage() + "\n  where Mode(x) = "));
+    }
+
+    private static void assertExpansion(List<AliasExpansion> expansions, String invocation, String expansion) {
+        assertEquals(1, expansions.size());
+        // instance numbers of variables are shown as superscripts
+        assertEquals(invocation, expansions.get(0).invocation().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""));
+        assertEquals(expansion, expansions.get(0).expansion().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""));
+    }
+
+    private static RefinementError verify(String test) {
+        CommandLineLauncher.launch(TEST_SUITE + test);
+        List<LJError> errors = Diagnostics.getInstance().getErrors().stream().toList();
+        assertEquals(1, errors.size(), "Expected exactly one error from " + test);
+        return assertInstanceOf(RefinementError.class, errors.get(0));
+    }
+}

liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java

@@ -174,7 +174,7 @@ private static RefinementError error(String expected, VCImplication found, Strin
         Counterexample counterexample = new Counterexample(
                 Arrays.stream(assignments).map(a -> a.split("=")).map(parts -> pair(parts[0], parts[1])).toList());
         return new RefinementError(null, null, new Predicate(RefinementsParser.createAST(expected, "")),
-                found.simplify(), new TranslationTable(), counterexample, null);
+                found.simplify(), new TranslationTable(), counterexample, null, List.of());
     }
 
     private static Pair<String, String> pair(String name, String value) {