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 00000000..475cab70 --- /dev/null +++ b/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 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()); + // 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 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 955db914..6eafd068 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 4afd6a5e..ab00bc95 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 a9838440..0578e62b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java +++ b/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> 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) { + 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 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(); } 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 453be0fa..9089873a 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 372acccf..0e886a0e 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 e36532fe..31c1ca55 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 00000000..2461db4a --- /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 863f761b..813da9b5 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) {