From 98c26fd0e1434c4c5dfb6e630ef1c35e6cb7f755 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Thu, 5 Nov 2026 13:20:57 +0000 Subject: [PATCH 1/3] Show the definitions of the aliases a refinement error uses A refinement error now records, for found and for expected, each alias invocation with its definition substituted by the arguments, the alias parameters, its definition as written and where it is declared, so a client can show what an alias means and link back to it. The CLI keeps the alias names in the message and adds one where line per alias the message uses, with the aliases their definitions use. Co-Authored-By: Claude Opus 5.5 --- .../diagnostics/AliasExpansion.java | 95 +++++++++++++++++++ .../liquidjava/diagnostics/LJDiagnostic.java | 7 ++ .../diagnostics/errors/RefinementError.java | 40 +++++++- .../processor/context/AliasWrapper.java | 18 +++- .../liquidjava/processor/facade/AliasDTO.java | 5 + .../refinement_checker/TypeChecker.java | 2 +- .../refinement_checker/VCChecker.java | 5 +- .../api/tests/TestAliasExpansions.java | 53 +++++++++++ .../RefinementErrorCounterexampleTest.java | 2 +- 9 files changed, 221 insertions(+), 6 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/AliasExpansion.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestAliasExpansions.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/AliasExpansion.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/AliasExpansion.java new file mode 100644 index 000000000..a29bcc35b --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/AliasExpansion.java @@ -0,0 +1,95 @@ +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 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 of(Expression expression, List aliases) { + Map byName = new LinkedHashMap<>(); + for (AliasWrapper alias : aliases) + byName.put(alias.getName(), alias); + Map 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 aliases, + Map expansions, Set expanding) { + List invocations = new ArrayList<>(); + invocationsOf(expression, invocations); + Map bodies = new LinkedHashMap<>(); + for (AliasInvocation invocation : invocations) { + AliasWrapper alias = aliases.get(invocation.getName()); + String shown = invocation.toDisplayString(); + if (alias == null || expanding.contains(alias.getName()) || expansions.containsKey(shown)) + continue; + Expression body = substituteArguments(alias, invocation.getArgs()); + expansions.put(shown, new AliasExpansion(shown, body.toDisplayString(), alias.getName(), + alias.getVarNames(), alias.getDefinition(), alias.getPosition())); + bodies.put(shown, body); + } + for (Map.Entry body : bodies.entrySet()) { + Set inner = new HashSet<>(expanding); + inner.add(expansions.get(body.getKey()).alias()); + collect(body.getValue(), aliases, expansions, inner); + } + } + + private static void invocationsOf(Expression expression, List 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 args) { + Expression body = alias.getClonedPredicate().getExpression(); + List 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; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 955db914d..6eafd0687 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/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 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(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 4afd6a5e2..ab00bc958 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/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 foundAliases; + private final List expectedAliases; + private final List aliasDeclarations; public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected, VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample, - String customMessage) { + String customMessage, List 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 aliasDeclarations(Expression shownFound, Expression expected, + List aliases) { + Map 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 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 getFoundAliases() { + return foundAliases; + } + + /** The alias invocations in expected and what they stand for */ + public List getExpectedAliases() { + return expectedAliases; + } + + /** A where line declaring each alias the message uses */ + @Override + public List 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 diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java index a9838440e..e3f235a38 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java @@ -5,6 +5,7 @@ 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 +14,15 @@ public class AliasWrapper { private final List> varTypes; private final List varNames; private final Predicate expression; + private final String definition; + private final SourcePosition position; - public AliasWrapper(AliasDTO a, Factory factory, String klass, String path) { + 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() + : a.getRef().strip().replaceAll("\\s+", " "); + this.position = position; varTypes = new ArrayList<>(); varNames = a.getVarNames(); for (String s : a.getVarTypes()) { @@ -37,6 +43,16 @@ public List getVarNames() { return varNames; } + /** 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(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java index 453be0fa3..9089873ad 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java @@ -65,4 +65,9 @@ public List 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; + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 372acccf5..0e886a0ea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/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) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index e36532fee..31c1ca553 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -85,7 +85,7 @@ public void processSubtyping(Predicate expectedType, List 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 */ diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestAliasExpansions.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestAliasExpansions.java new file mode 100644 index 000000000..2461db4a4 --- /dev/null +++ b/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 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 errors = Diagnostics.getInstance().getErrors().stream().toList(); + assertEquals(1, errors.size(), "Expected exactly one error from " + test); + return assertInstanceOf(RefinementError.class, errors.get(0)); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java index 863f761b4..813da9b55 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java +++ b/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 pair(String name, String value) { From 782d206c7638326f63c2736dc4c297544764ebc3 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Thu, 5 Nov 2026 13:28:28 +0000 Subject: [PATCH 2/3] Keep whitespace inside string literals of an alias definition Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/processor/context/AliasWrapper.java | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java index e3f235a38..0578e62b0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java @@ -2,6 +2,8 @@ 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; @@ -17,11 +19,13 @@ public class AliasWrapper { private final String definition; private final SourcePosition position; + 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() - : a.getRef().strip().replaceAll("\\s+", " "); + definition = a.getRef() == null ? expression.getExpression().toDisplayString() : oneLine(a.getRef()); this.position = position; varTypes = new ArrayList<>(); varNames = a.getVarNames(); @@ -43,6 +47,12 @@ public List 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; From 5731d46f12dfebd67c643d498b9c86375e7b75c3 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Thu, 5 Nov 2026 13:33:37 +0000 Subject: [PATCH 3/3] Tell apart alias invocations that display the same Co-Authored-By: Claude Opus 5.5 --- .../java/liquidjava/diagnostics/AliasExpansion.java | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/AliasExpansion.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/AliasExpansion.java index a29bcc35b..475cab70a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/AliasExpansion.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/AliasExpansion.java @@ -59,13 +59,14 @@ private static void collect(Expression expression, Map ali Map bodies = new LinkedHashMap<>(); for (AliasInvocation invocation : invocations) { AliasWrapper alias = aliases.get(invocation.getName()); - String shown = invocation.toDisplayString(); - if (alias == null || expanding.contains(alias.getName()) || expansions.containsKey(shown)) + // 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(shown, new AliasExpansion(shown, body.toDisplayString(), alias.getName(), - alias.getVarNames(), alias.getDefinition(), alias.getPosition())); - bodies.put(shown, body); + expansions.put(key, new AliasExpansion(invocation.toDisplayString(), body.toDisplayString(), + alias.getName(), alias.getVarNames(), alias.getDefinition(), alias.getPosition())); + bodies.put(key, body); } for (Map.Entry body : bodies.entrySet()) { Set inner = new HashSet<>(expanding);