From 133a2846003c835e17293138cd2c81bfd161d13f Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 21:09:41 +0000 Subject: [PATCH 1/3] Mark code in messages with backticks, and name the lines they refer to Headlines, hints, origin notes, the declared-here gloss, alias where lines and counterexamples write code as `code`. Plain-text clients get the backticks, as rustc gives them; the terminal shows code in blue without them, unless NO_COLOR is set or the output is not a terminal. A note or hint that names a line also carries it as a SourceReference (the line, the words naming the place, file, line and column), which LJDiagnostic.getReferences() gives clients to link to. Co-Authored-By: Claude Opus 5.5 --- .../java/liquidjava/diagnostics/Code.java | 48 +++++ .../java/liquidjava/diagnostics/Colors.java | 10 + .../liquidjava/diagnostics/LJDiagnostic.java | 24 ++- .../diagnostics/SourceReference.java | 26 +++ .../diagnostics/errors/ErrorMessage.java | 5 +- .../diagnostics/errors/RefinementError.java | 5 +- .../liquidjava/diagnostics/hints/Hint.java | 12 +- .../diagnostics/hints/StateHints.java | 63 +++--- .../refinement_checker/OriginNotes.java | 29 +-- .../refinement_checker/TypeChecker.java | 4 +- .../refinement_checker/VCChecker.java | 3 +- .../object_checkers/AuxStateHandler.java | 10 +- .../object_checkers/StateOrigin.java | 41 ++-- .../api/tests/TestAliasExpansions.java | 7 +- .../api/tests/TestCounterexamples.java | 2 +- .../api/tests/TestDeclarationPositions.java | 2 +- .../api/tests/TestFoundBinders.java | 16 +- .../api/tests/TestGeneratedNames.java | 2 +- .../liquidjava/api/tests/TestOriginNotes.java | 22 +- .../api/tests/TestStateErrorContext.java | 2 +- .../liquidjava/api/tests/TestStateHints.java | 197 +++++++++--------- .../api/tests/TestStaticConstantNames.java | 3 +- .../java/liquidjava/diagnostics/CodeTest.java | 24 +++ .../RefinementErrorCounterexampleTest.java | 18 +- 24 files changed, 373 insertions(+), 202 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/Code.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/SourceReference.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/diagnostics/CodeTest.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Code.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Code.java new file mode 100644 index 000000000..255c28f63 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Code.java @@ -0,0 +1,48 @@ +package liquidjava.diagnostics; + +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +/** + * Code inside a message, marked with backticks as in {@code found `x > 0`}. Clients that show plain text get the + * backticks; the terminal shows the code in colour instead, or keeps the backticks when colour is off + */ +public final class Code { + + // a run of backticks, the code, and a run of the same length + private static final Pattern SPAN = Pattern.compile("(`+)(.+?)(? 2 && code.startsWith(" ") && code.endsWith(" ")) + code = code.substring(1, code.length() - 1); + span.appendReplacement(rendered, Matcher.quoteReplacement(Colors.BLUE + code + Colors.RESET)); + } + span.appendTail(rendered); + return rendered.toString(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java index 50aa3ae8d..2ee68abe0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java @@ -2,6 +2,16 @@ // ANSI color codes public class Colors { + + /** + * Whether colour may mark code: not when NO_COLOR is set (https://no-color.org), nor when the output is not a + * terminal + */ + public static boolean enabled() { + String noColor = System.getenv("NO_COLOR"); + return (noColor == null || noColor.isEmpty()) && System.console() != null; + } + public static final String RESET = "\u001B[0m"; public static final String GREY = "\u001B[90m"; public static final String RED = "\u001B[31m"; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 5fd9c28a7..67dd672c9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -23,6 +23,7 @@ public class LJDiagnostic extends RuntimeException { private SourcePosition position; private final List hints = new ArrayList<>(); private final List messageNotes = new ArrayList<>(); + private final List references = new ArrayList<>(); private String counterexample; private ErrorCategory category; private static final String PIPE = " | "; @@ -87,6 +88,19 @@ public void addMessageNote(String note) { messageNotes.add(note); } + /** Adds a line printed under the message that names a place in the source, as {@code reference} tells */ + public void addMessageNote(SourceReference reference) { + messageNotes.add(reference.message()); + references.add(reference); + } + + /** The places in the source that the message notes and hints name, each with the line that names it */ + public List getReferences() { + List all = new ArrayList<>(references); + hints.stream().map(Hint::reference).filter(Objects::nonNull).forEach(all::add); + return all; + } + /** Lines printed under the excerpt of where the refinement is declared that explain it */ public List getDeclarationNotes() { return List.of(); @@ -128,10 +142,10 @@ public String toString() { StringBuilder sb = new StringBuilder(); // title - sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message) + sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(Code.render(message)) .append("\n"); for (String note : getMessageNotes()) - sb.append(" ").append(note).append("\n"); + sb.append(" ").append(Code.render(note)).append("\n"); // snippet String snippet = getSnippet(); @@ -142,14 +156,14 @@ public String toString() { // counterexample String counterexample = getCounterexampleStr(); if (counterexample != null && !counterexample.isBlank()) { - sb.append(" --> ").append(String.join("\n ", counterexample.split("\n"))).append("\n"); + sb.append(" --> ").append(Code.render(String.join("\n ", counterexample.split("\n")))).append("\n"); } // hints if (!hints.isEmpty()) { sb.append("\nHints:\n"); for (Hint hint : hints) - sb.append(" - ").append(String.join("\n ", hint.message().split("\n"))).append("\n"); + sb.append(" - ").append(Code.render(String.join("\n ", hint.message().split("\n")))).append("\n"); } // location @@ -165,7 +179,7 @@ public String toString() { if (declarationSnippet != null) { sb.append(declarationSnippet); for (String note : getDeclarationNotes()) - sb.append(" ").append(note).append("\n"); + sb.append(" ").append(Code.render(note)).append("\n"); } sb.append("\n").append(declPos.getFile().getPath()).append(":").append(declPos.getLine()) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/SourceReference.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/SourceReference.java new file mode 100644 index 000000000..854538d0c --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/SourceReference.java @@ -0,0 +1,26 @@ +package liquidjava.diagnostics; + +import spoon.reflect.cu.SourcePosition; + +/** + * A place in the source that a line of a diagnostic names, such as {@code line 134} in an origin note, for clients that + * link to it + * + * @param message + * the whole line, a message note or a hint, as the diagnostic gives it + * @param text + * the words of {@code message} that name the place, which occur in it once + * @param file + * the path of the file + * @param line + * the line, from 1 + * @param column + * the column, from 1 + */ +public record SourceReference(String message, String text, String file, int line, int column) { + + public static SourceReference of(String message, String text, SourcePosition position) { + return new SourceReference(message, text, position.getFile().getPath(), position.getLine(), + position.getColumn()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ErrorMessage.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ErrorMessage.java index 33c9beafe..1345f67a8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ErrorMessage.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ErrorMessage.java @@ -8,6 +8,7 @@ import java.util.function.UnaryOperator; import liquidjava.diagnostics.TranslationTable; +import liquidjava.diagnostics.Code; import liquidjava.processor.context.PlacementInCode; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.formatter.DisplayNames; @@ -36,9 +37,9 @@ static ErrorMessage of(Expression expected, VCSimplificationResult found, Transl PlacementInCode placement = translationTable == null ? null : translationTable.get(name); return placement == null ? null : placement.getLine(); }); - String expectedText = ExpressionFormatter.format(display.apply(expected), names); + String expectedText = Code.of(ExpressionFormatter.format(display.apply(expected), names)); String text = showsFound.test(shown) - ? String.format(frame, ExpressionFormatter.format(display.apply(shown), names), expectedText) + ? String.format(frame, Code.of(ExpressionFormatter.format(display.apply(shown), names)), expectedText) : String.format("expected %s but could not prove it", expectedText); return new ErrorMessage(text, names); } 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 ce62fcdc7..324f89910 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -11,6 +11,7 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.AliasExpansion; +import liquidjava.diagnostics.Code; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.processor.context.AliasWrapper; @@ -68,7 +69,7 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi String counterexampleString = this.counterexample.assignments().stream() .map(a -> getDisplayNames().get(a.first()) + " == " + a.second()) .collect(Collectors.joining(" && ")); - setCounterexampleStr("Counterexample: " + counterexampleString); + setCounterexampleStr("Counterexample: " + Code.of(counterexampleString)); } setCategory(categoryOf(expected, found)); } @@ -120,7 +121,7 @@ public List getExpectedAliases() { @Override public List getMessageNotes() { List notes = new ArrayList<>( - aliasDeclarations.stream().map(declaration -> "where " + declaration).toList()); + aliasDeclarations.stream().map(declaration -> "where " + Code.of(declaration)).toList()); notes.addAll(super.getMessageNotes()); return notes; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java index 9098f6ba5..cb3f7de0c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java @@ -1,14 +1,22 @@ package liquidjava.diagnostics.hints; +import liquidjava.diagnostics.SourceReference; + /** * A suggestion on how to fix a diagnostic * * @param kind * what the suggestion is about, so clients can show or filter hints separately * @param message - * the suggestion as shown to the user + * the suggestion as shown to the user, with code marked as {@link liquidjava.diagnostics.Code} marks it + * @param reference + * the place in the source the suggestion names, or null */ -public record Hint(Kind kind, String message) { +public record Hint(Kind kind, String message, SourceReference reference) { + + public Hint(Kind kind, String message) { + this(kind, message, null); + } public enum Kind { /** A suggestion that does not come from a specific analysis */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index a87b10631..9238dd4f8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -12,6 +12,8 @@ import java.util.stream.Stream; import liquidjava.diagnostics.categories.ErrorCategory; +import liquidjava.diagnostics.Code; +import liquidjava.diagnostics.SourceReference; import liquidjava.diagnostics.hints.Hint.Kind; import liquidjava.processor.context.RefinedFunction; import liquidjava.processor.context.Variable; @@ -41,6 +43,8 @@ public final class StateHints { private final StateMachine machine; private final String receiver; + // the receiver marked as code, for the words of a hint + private final String shownReceiver; /** The states that allow the failing call, grouped by the state refinement that allows it */ private final List> goals; /** The state sets the failing call checks, as indexes into {@link State#names()} */ @@ -57,6 +61,7 @@ private StateHints(StateMachine machine, String receiver, RefinedFunction call, Function> setNameOf) { this.machine = machine; this.receiver = receiver; + this.shownReceiver = Code.of(receiver); this.setNameOf = setNameOf; this.asValues = machine.states().stream().flatMap(s -> s.names().stream()) .anyMatch(name -> setNameOf.apply(name).isPresent()); @@ -113,10 +118,11 @@ public static Hint decidingArgument(DecidingArgument deciding, String receiver) ? "new " + Utils.getSimpleName(function.getTargetClass()) + namedParameters(function) : receiver + "." + declaration(function); String values = deciding.values().isEmpty() ? "other arguments" : deciding.values().entrySet().stream() - .map(e -> e.getKey() + " == " + e.getValue()).collect(Collectors.joining(" and ")); - return new Hint(Kind.DECIDING_ARGUMENT, - String.format("%s on line %d decides the state of %s: with %s, this call would be allowed", call, - deciding.call().position().getLine(), receiver, values)); + .map(e -> Code.of(e.getKey() + " == " + e.getValue())).collect(Collectors.joining(" and ")); + String line = "line " + deciding.call().position().getLine(); + String message = String.format("%s on %s decides the state of %s: with %s, this call would be allowed", + Code.of(call), line, Code.of(receiver), values); + return new Hint(Kind.DECIDING_ARGUMENT, message, SourceReference.of(message, line, deciding.call().position())); } /** @@ -128,8 +134,8 @@ public static Hint decidingArgument(DecidingArgument deciding, String receiver) * whether the state was checked, though the check did not decide it */ private List anyState(Set current, RefinedFunction call, boolean checkedElsewhere) { - String known = checkedElsewhere ? "What is known here does not decide the state of " + receiver - : "The state of " + receiver + " is unknown here"; + String known = checkedElsewhere ? "What is known here does not decide the state of " + shownReceiver + : "The state of " + shownReceiver + " is unknown here"; String message = known + ", and this call needs " + (asValues ? "" : "it to be ") + needed(); message += newObjects(call).map(c -> ". Objects created with " + c + " start in such a state").orElse(""); List hints = new ArrayList<>(); @@ -179,9 +185,9 @@ private List guard(Set current, RefinedFunction call) { CallVariant guard = guards.get(0); String check = (guard.negatedResult() ? "!" : "") + guardCall(guard.method()); String arguments = guard.method().getArguments().isEmpty() ? "" - : ", filling in the arguments of " + declaration(guard.method()); - String message = String.format("Guard this call with if (%s)%s; inside it, %s", check, arguments, - isIn(needed())); + : ", filling in the arguments of " + Code.of(declaration(guard.method())); + String message = String.format("Guard this call with %s%s; inside it, %s", Code.of("if (" + check + ")"), + arguments, isIn(needed())); return List.of(new Hint(Kind.GUARD, message)); } @@ -231,13 +237,13 @@ private Hint unreachable(Set current, RefinedFunction call, boolean pathD return new Hint(Kind.PATH_DEPENDENT_STATE, String.format( "Depending on the path taken, %s here, and no sequence of calls moves %s from all of them to %s. " + "Make %s reach this line in the same state on every path", - namesHere(current), receiver, needed(), receiver)); + namesHere(current), shownReceiver, needed(), shownReceiver)); if (pathDependent) return new Hint(Kind.PATH_DEPENDENT_STATE, String.format( "%s can be in %s here, depending on the path taken, and no sequence of calls moves all of them to %s. " + "Make %s reach this line in the same state on every path", - receiver, namesHere(current), needed(), receiver)); - String message = String.format("No sequence of calls moves %s from %s to %s", receiver, namesHere(current), + shownReceiver, namesHere(current), needed(), shownReceiver)); + String message = String.format("No sequence of calls moves %s from %s to %s", shownReceiver, namesHere(current), needed()); message += newObjects(call).map(c -> ". Create a new object instead with " + c).orElse(""); return new Hint(Kind.UNREACHABLE_STATE, message); @@ -246,18 +252,18 @@ private Hint unreachable(Set current, RefinedFunction call, boolean pathD private List allowedCalls(Set current) { List allowed = machine.allowedIn(current); if (!allowed.isEmpty()) { - List signatures = allowed.stream().map(StateHints::signature).toList(); + List signatures = allowed.stream().map(StateHints::signature).map(Code::of).toList(); String others = machine.complete() ? "" : " (and possibly others)"; return List.of(new Hint(Kind.AVAILABLE_CALLS, String.format("%s %s, %s can call: %s%s", - asValues ? "When" : "In state", namesHere(current), receiver, list(signatures), others))); + asValues ? "When" : "In state", namesHere(current), shownReceiver, list(signatures), others))); } boolean noCallsInAnyState = current.stream().allMatch(s -> machine.allowedIn(Set.of(s)).isEmpty()); if (machine.complete() && noCallsInAnyState) return List.of(new Hint(Kind.FINAL_STATE, asValues ? String.format("When %s, none of the methods of %s with state refinements can be called", - namesHere(current), receiver) + namesHere(current), shownReceiver) : String.format("%s is in state %s, where none of its methods with state refinements can be called", - receiver, namesHere(current)))); + shownReceiver, namesHere(current)))); return List.of(); } @@ -266,7 +272,7 @@ private Optional newObjects(RefinedFunction call) { if (receiver.equals(Keys.THIS)) return Optional.empty(); List constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor).distinct() - .toList(); + .map(Code::of).toList(); return constructors.isEmpty() ? Optional.empty() : Optional.of(String.join(" or ", constructors)); } @@ -292,17 +298,18 @@ private static String declaration(RefinedFunction method) { } /** - * A step of a sequence, with the condition on its arguments if it has one: as the call with its argument when the - * condition gives the only parameter a value, e.g. {@code p.setMode(2)}, and otherwise after the call, e.g. - * {@code p.set(int lo, int hi) with lo < hi} + * A step of a sequence, marked as code, with the condition on its arguments if it has one: as the call with its + * argument when the condition gives the only parameter a value, e.g. {@code p.setMode(2)}, and otherwise after the + * call, e.g. {@code p.set(int lo, int hi) with lo < hi} */ private String call(CallVariant step) { if (step.kind() != CallVariant.Kind.ARGUMENTS) - return call(step.method()); + return Code.of(call(step.method())); Expression condition = step.condition().getExpression(); - return argumentValue(step.method(), condition) - .map(value -> receiver + "." + Utils.getSimpleName(step.method().getName()) + "(" + value + ")") - .orElse(receiver + "." + declaration(step.method()) + " with " + condition.toDisplayString()); + return argumentValue(step.method(), condition).map( + value -> Code.of(receiver + "." + Utils.getSimpleName(step.method().getName()) + "(" + value + ")")) + .orElse(Code.of(receiver + "." + declaration(step.method())) + " with " + + Code.of(condition.toDisplayString())); } /** The value {@code condition} gives the only parameter of {@code method}, as {@code 2} in {@code mode == 2} */ @@ -346,7 +353,7 @@ private static String parameters(RefinedFunction function) { /** That the receiver is in {@code states}, e.g. {@code f is open}, or {@code states} if they name the receiver */ private String isIn(String states) { - return (asValues ? "" : receiver + " is ") + states; + return (asValues ? "" : shownReceiver + " is ") + states; } /** {@code states} named as briefly as possible, e.g. {@code open or loud} */ @@ -384,9 +391,9 @@ private String join(List> groups) { */ private String stateName(String state) { if (!asValues) - return state; - return setNameOf.apply(state).map(set -> set + "(" + receiver + ") == " + state) - .orElse(state + "(" + receiver + ")"); + return Code.of(state); + return Code.of(setNameOf.apply(state).map(set -> set + "(" + receiver + ") == " + state) + .orElse(state + "(" + receiver + ")")); } private static String list(List items) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/OriginNotes.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/OriginNotes.java index a094ef3d6..464b08d7d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/OriginNotes.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/OriginNotes.java @@ -5,6 +5,8 @@ import java.util.Optional; import java.util.stream.Collectors; +import liquidjava.diagnostics.Code; +import liquidjava.diagnostics.SourceReference; import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.errors.RefinementError; import liquidjava.processor.context.Context; @@ -44,14 +46,14 @@ private OriginNotes() { * When nothing is known about the values expected constrains and each is a parameter of the enclosing method that * is declared with no refinement, a note per parameter saying so. Nothing is said about the callers */ - static List unrefinedParameters(RefinementError error, CtElement checked, Context context) { + static List unrefinedParameters(RefinementError error, CtElement checked, Context context) { Optional> method = enclosingMethod(checked); List variables = error.getExpected().getVariableNames().stream().distinct().toList(); if (error.getCategory().filter(ErrorCategory.UNKNOWN::equals).isEmpty() || method.isEmpty() || variables.isEmpty()) return List.of(); - List notes = new ArrayList<>(); + List notes = new ArrayList<>(); for (String variable : variables) { Optional> parameter = method.get().getParameters().stream() .filter(p -> p.getSimpleName().equals(variable)).findFirst(); @@ -60,9 +62,11 @@ static List unrefinedParameters(RefinementError error, CtElement checked || !(context.getVariableByName(variable)instanceof Variable declared) || !declared.getMainRefinement().isBooleanTrue() || isRefined(parameter.get(), context)) return List.of(); - notes.add(String.format("Origin: line %d, %s is a parameter of %s with no refinement", - parameter.get().getPosition().getLine(), error.getDisplayNames().get(variable), - signature(method.get()))); + SourcePosition position = parameter.get().getPosition(); + String line = "line " + position.getLine(); + String note = String.format("Origin: %s, %s is a parameter of %s with no refinement", line, + Code.of(error.getDisplayNames().get(variable)), Code.of(signature(method.get()))); + notes.add(SourceReference.of(note, line, position)); } return notes; } @@ -73,8 +77,8 @@ static List unrefinedParameters(RefinementError error, CtElement checked * expects mentions that ghost application: it then constrains no value, so what is left is all the refinement says * about the value */ - static List returnedValues(RefinementError error, Context context) { - List notes = new ArrayList<>(); + static List returnedValues(RefinementError error, Context context) { + List notes = new ArrayList<>(); for (String variable : error.getExpected().getVariableNames().stream().distinct().toList()) { // a call argument, which has no variable of its own and is shown as the call if (!(context.getVariableByName(variable)instanceof VariableInstance instance) @@ -89,11 +93,12 @@ static List returnedValues(RefinementError error, Context context) { if (!namesOnlyCodeVariables(guaranteed, context)) continue; String value = ExpressionFormatter.format(new Var(variable), error.getDisplayNames()); - String says = isTrue(guaranteed) ? "guarantees nothing about " + value - : "guarantees only " + ExpressionFormatter.format( - guaranteed.substitute(new Var(Keys.WILDCARD), new Var(variable)), error.getDisplayNames()); - notes.add(String.format("Origin: %s:%d, %s %s", declared.getFile().getName(), declared.getLine(), value, - says)); + String says = isTrue(guaranteed) ? "guarantees nothing about " + Code.of(value) + : "guarantees only " + Code.of(ExpressionFormatter.format( + guaranteed.substitute(new Var(Keys.WILDCARD), new Var(variable)), error.getDisplayNames())); + String place = declared.getFile().getName() + ":" + declared.getLine(); + notes.add(SourceReference.of(String.format("Origin: %s, %s %s", place, Code.of(value), says), place, + declared)); } return notes; } 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 2cfed2c6f..984ff18a7 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 @@ -9,6 +9,7 @@ import java.util.Optional; import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.SourceReference; import liquidjava.diagnostics.errors.*; import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.hints.Hint; @@ -619,7 +620,8 @@ public void throwStateRefinementError(SourcePosition position, SourcePosition de public void throwStateRefinementError(SourcePosition position, List declarationPositions, Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category, - StateErrorContext context, List declarationNotes, List messageNotes) throws LJError { + StateErrorContext context, List declarationNotes, List messageNotes) + throws LJError { vcChecker.throwStateRefinementError(position, declarationPositions, found, expected, customMessage, hints, category, context, declarationNotes, messageNotes); } 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 25cd299bb..fec934424 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 @@ -11,6 +11,7 @@ import liquidjava.diagnostics.errors.*; import liquidjava.diagnostics.DebugLog; +import liquidjava.diagnostics.SourceReference; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.hints.Hint; @@ -460,7 +461,7 @@ protected Predicate shownFound(Predicate found, Predicate expected) { protected void throwStateRefinementError(SourcePosition position, List declarationPositions, Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category, - StateErrorContext context, List declarationNotes, List messageNotes) + StateErrorContext context, List declarationNotes, List messageNotes) throws StateRefinementError { TranslationTable map = new TranslationTable(); VCImplication foundState = buildPremiseChain(map, expected, found); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 2f8292433..0c91589e5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -5,6 +5,8 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.DebugLog; +import liquidjava.diagnostics.SourceReference; +import liquidjava.diagnostics.Code; import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.errors.IllegalConstructorTransitionError; import liquidjava.diagnostics.errors.InvalidRefinementError; @@ -827,7 +829,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc StateErrorContext context = states .map(r -> StateErrorContext.of(r.machine(), function, r.current(), writtenReceiver(invocation))) .orElse(null); - List messageNotes = receiverOf(invocation) + List messageNotes = receiverOf(invocation) .flatMap(r -> fromNote(tc, vi, r, function, ghostStates, states, prevState, expected, invocation)) .stream().toList(); tc.throwStateRefinementError(invocation.getPosition(), declarationPositions, prevState, @@ -836,7 +838,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc } /** Best effort, like {@link #receiverStates}: see {@link StateOrigin} */ - private static Optional fromNote(TypeChecker tc, VariableInstance receiver, String written, + private static Optional fromNote(TypeChecker tc, VariableInstance receiver, String written, RefinedFunction function, List ghostStates, Optional states, Predicate found, Predicate expected, CtElement invocation) { try { @@ -862,8 +864,8 @@ private static List declarationNotes(Expression written, Context context private static void addMeanings(Expression e, Context context, List meanings) { if (e instanceof FunctionInvocation state && state.getArgs().size() == 1 && StateValues.setNameOf(state.getName(), context.getGhostStates(), context.getGhosts()).isPresent()) { - String meaning = state.toDisplayString() + " means " - + StateValues.toSetForm(state, context.getGhostStates(), context.getGhosts()).toDisplayString(); + String meaning = Code.of(state.toDisplayString()) + " means " + Code + .of(StateValues.toSetForm(state, context.getGhostStates(), context.getGhosts()).toDisplayString()); if (!meanings.contains(meaning)) meanings.add(meaning); return; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java index 043d3eac9..204523594 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java @@ -7,7 +7,9 @@ import java.util.Set; import java.util.stream.Collectors; +import liquidjava.diagnostics.Code; import liquidjava.diagnostics.DebugLog; +import liquidjava.diagnostics.SourceReference; import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.CallResult; import liquidjava.processor.context.Context; @@ -94,9 +96,9 @@ private StateOrigin(TypeChecker tc, VariableInstance receiver, String written, S * @param expected * the states the call needs */ - static Optional note(TypeChecker tc, VariableInstance receiver, String written, RefinedFunction failing, - List ghostStates, Optional machine, Set current, Predicate found, - Predicate expected, CtElement invocation) throws LJError { + static Optional note(TypeChecker tc, VariableInstance receiver, String written, + RefinedFunction failing, List ghostStates, Optional machine, Set current, + Predicate found, Predicate expected, CtElement invocation) throws LJError { Set checked = setsOf(failing.getFromStates(), ghostStates); Set wrong = machine.filter(m -> m.models(failing)) .map(m -> wrongSets(checked, current, m.statesAllowing(failing), ghostStates)).orElse(Set.of()); @@ -129,7 +131,7 @@ private static Set setsOf(List predicates, List note(Predicate shownFound) throws LJError { + private Optional note(Predicate shownFound) throws LJError { if (mayBeAliased()) return Optional.empty(); VariableInstance at = receiver; @@ -230,7 +232,7 @@ private Optional foundAbout(VariableInstance at, Predicate shownFound * That the facts of found on the shown sets {@code change} names were last set by it, if what it gave {@code after} * proves them */ - private Optional lastSetNote(StateChange change, VariableInstance after, Predicate shownFound) + private Optional lastSetNote(StateChange change, VariableInstance after, Predicate shownFound) throws LJError { Set changed = setsOf(List.of(change.change().getTo()), ghostStates).stream() .filter(shown::contains).collect(Collectors.toSet()); @@ -238,8 +240,9 @@ private Optional lastSetNote(StateChange change, VariableInstance after, if (facts.isEmpty() || !implies(after.getRefinement(), facts.get())) return Optional.empty(); // the call last set these sets, so it is what makes them so - return code(change.position()).map(code -> String.format("Origin: line %d, %s makes %s", - change.position().getLine(), code, display(facts.get(), after.getName()))); + String line = "line " + change.position().getLine(); + return code(change.position()).map(code -> SourceReference.of(String.format("Origin: %s, %s makes %s", line, + Code.of(code), Code.of(display(facts.get(), after.getName()))), line, change.position())); } /** @@ -247,18 +250,22 @@ private Optional lastSetNote(StateChange change, VariableInstance after, * them, or that it says nothing about them when found says nothing either and its return refinement names no state * of them and no other value the state could come from */ - private Optional returnedNote(CallResult call, VariableInstance assigned, Predicate shownFound) + private Optional returnedNote(CallResult call, VariableInstance assigned, Predicate shownFound) throws LJError { Optional code = code(call.position()); if (code.isEmpty()) return Optional.empty(); - String origin = String.format("Origin: line %d, %s ", call.position().getLine(), code.get()); + String line = "line " + call.position().getLine(); + String origin = String.format("Origin: %s, %s ", line, Code.of(code.get())); Optional facts = factsOn(call.returned(), Keys.WILDCARD, shown); Optional found = foundAbout(assigned, shownFound, shown); if (facts.isPresent()) return found.isPresent() && implies(facts.get().substituteVariable(Keys.WILDCARD, assigned.getName()), found.get()) - ? Optional.of(origin + "returns " + display(facts.get(), Keys.WILDCARD)) : Optional.empty(); + ? Optional.of(SourceReference.of( + origin + "returns " + Code.of(display(facts.get(), Keys.WILDCARD)), line, + call.position())) + : Optional.empty(); Predicate returned = call.returned(); // a set declared without a name has a generated one, which the message does not otherwise show // a state refinement of the method may give the value its state, as `to = "running(_)"` does @@ -268,8 +275,10 @@ && setsOf(List.of(returned), ghostStates).stream().noneMatch(shown::contains) && returned.getVariableNames().stream().allMatch(Keys.WILDCARD::equals) && !hasAlias(returned.getExpression()); String sets = shown.stream().map(set -> Utils.getSimpleName(set.getName()) + "(" + written + ")").sorted() - .collect(Collectors.joining(", ")); - return saysNothing ? Optional.of(origin + "says nothing about " + sets) : Optional.empty(); + .map(Code::of).collect(Collectors.joining(", ")); + return saysNothing + ? Optional.of(SourceReference.of(origin + "says nothing about " + sets, line, call.position())) + : Optional.empty(); } /** @@ -277,7 +286,7 @@ && setsOf(List.of(returned), ghostStates).stream().noneMatch(shown::contains) * constructor makes it in the shown sets, if found still says it is in that state. It is a fact about the * constructor only, given when the walk back to the call that last set the state broke, e.g. at a join of branches */ - private Optional creationNote(VariableInstance unknown, Predicate shownFound) throws LJError { + private Optional creationNote(VariableInstance unknown, Predicate shownFound) throws LJError { DebugLog.warn("Origin note: no known call gives " + unknown.getName() + " its state, e.g. a join of branches"); if (!(invocation instanceof CtInvocation call && call.getTarget()instanceof CtVariableRead read && read.getVariable().getDeclaration()instanceof CtLocalVariable local @@ -293,8 +302,10 @@ private Optional creationNote(VariableInstance unknown, Predicate shownF || !implies(found.get(), facts.get().substituteVariable(Keys.THIS, unknown.getName()))) return Optional.empty(); // not "makes": a later call may have set the state again, which found no longer tells - return Optional.of(String.format("Origin: line %d, %s creates %s with %s", created.position().getLine(), - code.get(), written, display(facts.get(), Keys.THIS))); + String line = "line " + created.position().getLine(); + return Optional + .of(SourceReference.of(String.format("Origin: %s, %s creates %s with %s", line, Code.of(code.get()), + Code.of(written), Code.of(display(facts.get(), Keys.THIS))), line, created.position())); } /** diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestAliasExpansions.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestAliasExpansions.java index acb942baa..d05c93688 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestAliasExpansions.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestAliasExpansions.java @@ -30,11 +30,10 @@ void foundAndExpectedRecordTheirSubstitutedAliases() { @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"), + 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) = ")); + assertTrue(error.toString().contains(error.getMessage() + "\n where `Mode(x) = ")); } private static void assertExpansion(List expansions, String invocation, String expansion) { diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java index 59bc05012..35bdd8b74 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java @@ -159,7 +159,7 @@ void refinementAliasArgumentIsKept() { void ghostOfArgumentFoundKnowsNothingAboutIsKept() { RefinementError error = verify("ErrorCounterexampleGhostArgument.java"); assertAssignments(error, assignment("size(bag)", "0")); - assertTrue(error.getCounterexampleStr().contains("Counterexample: size(bag) == 0")); + assertTrue(error.getCounterexampleStr().contains("Counterexample: `size(bag) == 0`")); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDeclarationPositions.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDeclarationPositions.java index 8fc733d94..89bd22bcb 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDeclarationPositions.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDeclarationPositions.java @@ -55,7 +55,7 @@ void stateErrorPointsToEveryEntryStateWithWhatItMeans() throws IOException { assertPosition(positions.get(0), path, fromStart(source, "shut(this)"), "shut(this)"); // the second annotation's from, not the same text the first writes as its to assertPosition(positions.get(1), path, fromStart(source, "ajar(this)"), "ajar(this)"); - String notes = " where shut(this) means door(this) == shut\n where ajar(this) means door(this) == ajar\n"; + String notes = " where `shut(this)` means `door(this) == shut`\n where `ajar(this)` means `door(this) == ajar`\n"; assertTrue(errors.get(0).toString().contains(notes)); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java index bd9e2ea91..fcfc7508d 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -63,8 +63,8 @@ void issueReproducerDropsTheTrueFieldRow() { @Test void callArgumentIsWrittenAsTheCallerWroteIt() { Shown shown = ERRORS.get(79); - assertEquals("found count() >= 0 but expected count() > 0", shown.message()); - assertEquals("Counterexample: count() == 0", shown.counterexample()); + assertEquals("found `count() >= 0` but expected `count() > 0`", shown.message()); + assertEquals("Counterexample: `count() == 0`", shown.counterexample()); } @Test @@ -81,26 +81,26 @@ void steppingBackReachesTheOriginalWithTheDroppedRow() { void staticFieldIsWrittenWithItsClass() { Shown shown = ERRORS.get(31); assertEquals(List.of("∀count count == Basket.served + 1"), shown.rows()); - assertEquals("Counterexample: count == 0 && Basket.served == -1", shown.counterexample()); + assertEquals("Counterexample: `count == 0 && Basket.served == -1`", shown.counterexample()); } @Test void variablesAnotherRowShowsGetNoTrueRow() { Shown shown = ERRORS.get(64); assertEquals(List.of("∀sum sum == first + second"), shown.rows()); - assertEquals("Counterexample: sum == 0 && first == 0 && second == 0", shown.counterexample()); + assertEquals("Counterexample: `sum == 0 && first == 0 && second == 0`", shown.counterexample()); } @Test void variableOnlyExpectedNamesKeepsItsTrueRow() { Shown shown = ERRORS.get(69); assertEquals(List.of("∀t true"), shown.rows()); - assertEquals("Counterexample: t == 0", shown.counterexample()); + assertEquals("Counterexample: `t == 0`", shown.counterexample()); } @Test void writeToAnotherObjectsFieldIsNamedAfterThatObject() { - assertEquals("found other.level == -1 but expected other.level >= 0", ERRORS.get(36).message()); + assertEquals("found `other.level == -1` but expected `other.level >= 0`", ERRORS.get(36).message()); assertEquals(List.of("∀this.level this.level >= 0", "∀other.level other.level == this.level - 1"), ERRORS.get(48).rows()); } @@ -108,8 +108,8 @@ void writeToAnotherObjectsFieldIsNamedAfterThatObject() { @Test void earlierValuesOfAVariableAreWrittenWithTheirLine() { Shown shown = ERRORS.get(86); - assertEquals("found b@86 == 8 && b@86 > 0 && b == -b@86 but expected b > 0", shown.message()); - assertEquals("Counterexample: b == -8", shown.counterexample()); + assertEquals("found `b@86 == 8 && b@86 > 0 && b == -b@86` but expected `b > 0`", shown.message()); + assertEquals("Counterexample: `b == -8`", shown.counterexample()); assertEquals(List.of("∀b@85 b@85 == 8", "∀b@86 b@86 == b@85 && b@86 > 0", "∀b b == -b@86"), shown.originalRows()); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java index 0acd3489a..3f76e7e02 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java @@ -33,7 +33,7 @@ void namesEachGeneratedValueAfterWhatItIs() { "#ternary_condition == #ready_result && #ternary_condition == true", 43, "!#try_branch && !#catch_branch", 48, "x == #read_result - 1", 54, "isNull == #operation_result && #if_condition == isNull && #if_condition && x == 0", 58, - "found closed(#new_Door) but expected opened(#new_Door)"), messages); + "found `closed(#new_Door)` but expected `opened(#new_Door)`"), messages); } private static String originalFound(RefinementError error) { diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java index 7404045ac..bf083c25b 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java @@ -8,6 +8,7 @@ import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.SourceReference; import liquidjava.diagnostics.errors.LJError; class TestOriginNotes { @@ -17,20 +18,30 @@ class TestOriginNotes { @Test void unrefinedParameterIsNamedWithItsMethod() { LJError error = verify("ErrorUnknownArgument.java"); - assertEquals(List.of("Origin: line 10, amount is a parameter of use(int) with no refinement"), + assertEquals(List.of("Origin: line 10, `amount` is a parameter of `use(int)` with no refinement"), error.getMessageNotes()); - assertTrue(error.toString().contains(error.getMessage() + "\n Origin: line 10, amount is a parameter")); + assertTrue(error.toString().contains(error.getMessage() + "\n Origin: line 10, `amount` is a parameter")); } @Test void stateIsTracedToTheCallThatLastSetTheSetThatIsWrong() { - assertEquals(List.of("Origin: line 27, d.lock() makes lockState(d) == locked"), + assertEquals(List.of("Origin: line 27, `d.lock()` makes `lockState(d) == locked`"), verify("ErrorStateHintMultipleSets.java").getMessageNotes()); } + @Test + void noteNamesTheLineOfTheCallForClientsToLinkTo() { + LJError error = verify("ErrorStateHintMultipleSets.java"); + SourceReference reference = error.getReferences().get(0); + assertEquals(error.getMessageNotes().get(0), reference.message()); + assertEquals("line 27", reference.text()); + assertEquals(27, reference.line()); + assertTrue(reference.file().endsWith("ErrorStateHintMultipleSets.java")); + } + @Test void stateIsTracedToTheReturnRefinementOfTheCallAssigned() { - assertEquals(List.of("Origin: line 27, FromReturnedTask.create() returns phase(task) == idle"), + assertEquals(List.of("Origin: line 27, `FromReturnedTask.create()` returns `phase(task) == idle`"), verify("ErrorStateFromReturnedValue.java").getMessageNotes()); } @@ -47,7 +58,8 @@ void callArgumentIsTracedToWhatItsReturnRefinementGuaranteesAboutIt() { CommandLineLauncher.launch(TEST_SUITE + "classes/found_binders_error"); LJError pick = Diagnostics.getInstance().getErrors().stream().filter(e -> e.getPosition().getLine() == 25) .findFirst().orElseThrow(); - assertEquals(List.of("Origin: ArrayListRefinements.java:13, items.size() guarantees only items.size() >= 0"), + assertEquals( + List.of("Origin: ArrayListRefinements.java:13, `items.size()` guarantees only `items.size() >= 0`"), pick.getMessageNotes()); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java index a0f448bc3..6410aa8a6 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java @@ -54,7 +54,7 @@ void classWithoutStateSetHasNoContext() { @Test void foundEndsWithTheFactsRelevantToTheExpectedStateSet() { StateRefinementError error = errorOf("ErrorArgumentPicksTheStateEarlier.java"); - assertEquals("found tilingOff(param@25) && state1(param) == state1(param@25) but expected tilingOn(param)", + assertEquals("found `tilingOff(param@25) && state1(param) == state1(param@25)` but expected `tilingOn(param)`", error.getMessage()); VCSimplificationResult found = error.getFoundSimplification(); assertEquals("Relevant to Expected", found.getSimplification()); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index cd9727b18..ce6857c28 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -11,6 +11,7 @@ import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.SourceReference; import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.StateRefinementError; @@ -24,33 +25,33 @@ class TestStateHints { @Test void missingCallIsSuggestedWithTheStateItLeadsTo() { assertHints("ErrorStateHintCallSequence.java", - new Hint(Kind.CALL_SEQUENCE, "Call f.open() before this call; afterwards f is open")); + new Hint(Kind.CALL_SEQUENCE, "Call `f.open()` before this call; afterwards `f` is `open`")); } @Test void missingCallsAreSuggestedInOrder() { assertHints("ErrorStateHintTwoCalls.java", new Hint(Kind.CALL_SEQUENCE, - "Call r.prepare(), then r.start() before this call; afterwards r is running")); + "Call `r.prepare()`, then `r.start()` before this call; afterwards `r` is `running`")); } @Test void callSequenceNamesOnlyTheStateSetsItChanges() { - assertHints("ErrorStateHintMultipleSets.java", - new Hint(Kind.CALL_SEQUENCE, "Call d.unlock() before this call; afterwards lockState(d) == unlocked")); + assertHints("ErrorStateHintMultipleSets.java", new Hint(Kind.CALL_SEQUENCE, + "Call `d.unlock()` before this call; afterwards `lockState(d) == unlocked`")); } @Test void finalStateSuggestsCreatingANewObject() { assertHints("ErrorStateHintFinalState.java", new Hint(Kind.UNREACHABLE_STATE, - "No sequence of calls moves f from closed to open. Create a new object instead with new ErrorStateHintFinalState()"), + "No sequence of calls moves `f` from `closed` to `open`. Create a new object instead with `new ErrorStateHintFinalState()`"), new Hint(Kind.FINAL_STATE, - "f is in state closed, where none of its methods with state refinements can be called")); + "`f` is in state `closed`, where none of its methods with state refinements can be called")); } @Test void transitionDependingOnArgumentsIsSuggestedWithItsConditionButPreventsClaimingStateIsFinal() { assertHints("ErrorStateHintIncomplete.java", new Hint(Kind.CALL_SEQUENCE, - "Call f.reopen(int attempts) with attempts > 0 before this call; afterwards f is open")); + "Call `f.reopen(int attempts)` with `attempts > 0` before this call; afterwards `f` is `open`")); } @Test @@ -61,31 +62,31 @@ void subclassTransitionsPreventClaimingStateIsUnreachable() { @Test void subclassReceiverCanUseItsOwnTransitionsOnInheritedStates() { assertHints("ErrorStateHintInheritedStates.java", - new Hint(Kind.CALL_SEQUENCE, "Call s.bc() before this call; afterwards s is c")); + new Hint(Kind.CALL_SEQUENCE, "Call `s.bc()` before this call; afterwards `s` is `c`")); } @Test void overrideInTheReceiversClassReplacesTheInheritedTransition() { assertHints("ErrorStateHintOverride.java", - new Hint(Kind.CALL_SEQUENCE, "Call s.next() before this call; afterwards s is c")); + new Hint(Kind.CALL_SEQUENCE, "Call `s.next()` before this call; afterwards `s` is `c`")); } @Test void stateSetAndMethodsFromSpecsOfTheReceiversSuperclasses() { assertHints("classes/state_hints_grandchild_spec_error", new Hint(Kind.CALL_SEQUENCE, - "Call window.dispose() before this call; afterwards window is notDisplayable")); + "Call `window.dispose()` before this call; afterwards `window` is `notDisplayable`")); } @Test void superclassRefinementOfAMethodTheReceiversClassRedeclaresIsNotSuggested() { assertHints("classes/state_hints_redeclared_method_error", new Hint(Kind.CALL_SEQUENCE, - "Call host.dispose() before this call; afterwards host is notDisplayable")); + "Call `host.dispose()` before this call; afterwards `host` is `notDisplayable`")); } @Test void stateSetAndMethodsFromTheReceiversSuperclassSpec() { assertHints("classes/state_hints_superclass_spec_error", new Hint(Kind.CALL_SEQUENCE, - "Call host.dispose() before this call; afterwards host is notDisplayable")); + "Call `host.dispose()` before this call; afterwards `host` is `notDisplayable`")); } @Test @@ -96,28 +97,25 @@ void ownGenericRefinementOfAnInheritedMethodIsNotSuggested() { @Test void statesOfAnotherClassWithTheSimpleNameOfASupertypeAreLeftOut() { assertHints("classes/state_hints_same_simple_name_error", - new Hint(Kind.CALL_SEQUENCE, "Call l.add(E) before this call; afterwards l is nonEmpty")); + new Hint(Kind.CALL_SEQUENCE, "Call `l.add(E)` before this call; afterwards `l` is `nonEmpty`")); } @Test void stateDependingOnThePathAsksForTheSameStateOnEveryPath() { assertHints("ErrorStateHintPathDependent.java", new Hint(Kind.PATH_DEPENDENT_STATE, - "f can be in created or open here, depending on the path taken, and no sequence of calls moves all of them to open. " - + "Make f reach this line in the same state on every path")); + "`f` can be in `created` or `open` here, depending on the path taken, and no sequence of calls moves all of them to `open`. Make `f` reach this line in the same state on every path")); } @Test void stateDependingOnThePathInEveryStateIsNotReportedAsUnknown() { assertHints("ErrorStateHintJoinOfAllStates.java", new Hint(Kind.PATH_DEPENDENT_STATE, - "f can be in created or open here, depending on the path taken, and no sequence of calls moves all of them to open. " - + "Make f reach this line in the same state on every path")); + "`f` can be in `created` or `open` here, depending on the path taken, and no sequence of calls moves all of them to `open`. Make `f` reach this line in the same state on every path")); } @Test void callAllowedByDifferentRefinementsInEachStateIsNotSuggested() { assertHints("ErrorStateHintSeveralRefinements.java", new Hint(Kind.PATH_DEPENDENT_STATE, - "f can be in created or open here, depending on the path taken, and no sequence of calls moves all of them to open. " - + "Make f reach this line in the same state on every path")); + "`f` can be in `created` or `open` here, depending on the path taken, and no sequence of calls moves all of them to `open`. Make `f` reach this line in the same state on every path")); } @Test @@ -128,35 +126,35 @@ void receiverThatIsNotAVariableGetsNoHints() { @Test void unknownStateDoesNotSuggestACallThatNeedsAnotherUnknownState() { assertHints("ErrorStateHintUnknownState.java", - new Hint(Kind.NEEDED_STATE, "The state of f is unknown here, and this call needs it to be open")); + new Hint(Kind.NEEDED_STATE, "The state of `f` is unknown here, and this call needs it to be `open`")); } @Test void unknownStateOfAnExternalClassNamesOnlyTheCheckedStateSet() { assertHints("classes/state_hint_undo_manager_error", new Hint(Kind.NEEDED_STATE, - "The state of undoManager is unknown here, and this call needs it to be redoable"), + "The state of `undoManager` is unknown here, and this call needs it to be `redoable`"), new Hint(Kind.GUARD, - "Guard this call with if (undoManager.canRedo()); inside it, undoManager is redoable")); + "Guard this call with `if (undoManager.canRedo())`; inside it, `undoManager` is `redoable`")); } @Test void unknownStateSuggestsCallsAllowedInAnyState() { assertHints("ErrorStateHintUnknownAnyState.java", - new Hint(Kind.NEEDED_STATE, "The state of f is unknown here, and this call needs it to be open"), - new Hint(Kind.CALL_SEQUENCE, "Call f.reset(), then f.open() before this call; afterwards f is open")); + new Hint(Kind.NEEDED_STATE, "The state of `f` is unknown here, and this call needs it to be `open`"), + new Hint(Kind.CALL_SEQUENCE, + "Call `f.reset()`, then `f.open()` before this call; afterwards `f` is `open`")); } @Test void statesAreNamedOnlyInTheStateSetsThatMatter() { List errors = errors("ErrorStateHintNaming.java", 3); assertHints(errors.get(0), new Hint(Kind.NEEDED_STATE, - "The state of s is unknown here, and this call needs it to be open or loud")); - assertHints(errors.get(1), - new Hint(Kind.NEEDED_STATE, "The state of t is unknown here, and this call needs it to be a or b. " - + "Objects created with new ErrorStateHintNamingToggle() start in such a state")); + "The state of `s` is unknown here, and this call needs it to be `open` or `loud`")); + assertHints(errors.get(1), new Hint(Kind.NEEDED_STATE, + "The state of `t` is unknown here, and this call needs it to be `a` or `b`. Objects created with `new ErrorStateHintNamingToggle()` start in such a state")); assertHints(errors.get(2), - new Hint(Kind.UNREACHABLE_STATE, "No sequence of calls moves this from notRedoable to redoable")); + new Hint(Kind.UNREACHABLE_STATE, "No sequence of calls moves `this` from `notRedoable` to `redoable`")); } @Test @@ -165,15 +163,15 @@ void failedCheckOfTheReceiverIsNotAnUnknownState() { // the check is suggested even where it was made with the opposite result assertHints(errors.get(0), new Hint(Kind.NEEDED_STATE, - "What is known here does not decide the state of it, and this call needs it to be hasMore"), - new Hint(Kind.GUARD, "Guard this call with if (it.hasNext()); inside it, it is hasMore")); - assertHints(errors.get(1), - new Hint(Kind.NEEDED_STATE, - "What is known here does not decide the state of same, and this call needs it to be hasMore"), - new Hint(Kind.GUARD, "Guard this call with if (same.hasNext()); inside it, same is hasMore")); + "What is known here does not decide the state of `it`, and this call needs it to be `hasMore`"), + new Hint(Kind.GUARD, "Guard this call with `if (it.hasNext())`; inside it, `it` is `hasMore`")); + assertHints(errors.get(1), new Hint(Kind.NEEDED_STATE, + "What is known here does not decide the state of `same`, and this call needs it to be `hasMore`"), + new Hint(Kind.GUARD, "Guard this call with `if (same.hasNext())`; inside it, `same` is `hasMore`")); assertHints(errors.get(2), - new Hint(Kind.NEEDED_STATE, "The state of input is unknown here, and this call needs it to be hasMore"), - new Hint(Kind.GUARD, "Guard this call with if (input.hasNext()); inside it, input is hasMore")); + new Hint(Kind.NEEDED_STATE, + "The state of `input` is unknown here, and this call needs it to be `hasMore`"), + new Hint(Kind.GUARD, "Guard this call with `if (input.hasNext())`; inside it, `input` is `hasMore`")); assertEquals(List.of(Optional.empty(), Optional.empty(), Optional.of(ErrorCategory.UNKNOWN)), errors.stream().map(LJError::getCategory).toList()); } @@ -182,108 +180,106 @@ void failedCheckOfTheReceiverIsNotAnUnknownState() { void joinsAreNotTakenForAnUnknownState() { List errors = errors("ErrorStateHintJoins.java", 2); assertHints(errors.get(0), new Hint(Kind.UNREACHABLE_STATE, - "No sequence of calls moves d from (closed and unlocked) or (closed and locked) or (opened and unlocked) " - + "or (opened and locked) to closed and unlocked. " - + "Create a new object instead with new ErrorStateHintJoins()")); + "No sequence of calls moves `d` from (`closed` and `unlocked`) or (`closed` and `locked`) or (`opened` and `unlocked`) or (`opened` and `locked`) to `closed` and `unlocked`. Create a new object instead with `new ErrorStateHintJoins()`")); assertHints(errors.get(1), new Hint(Kind.UNREACHABLE_STATE, - "No sequence of calls moves d from (closed and unlocked) or (opened and unlocked) to closed and unlocked. " - + "Create a new object instead with new ErrorStateHintJoins()")); + "No sequence of calls moves `d` from (`closed` and `unlocked`) or (`opened` and `unlocked`) to `closed` and `unlocked`. Create a new object instead with `new ErrorStateHintJoins()`")); assertEquals(Optional.empty(), errors.get(0).getCategory()); } @Test void onlyConstructorsThatCanBeCalledAreSuggested() { List errors = errors("ErrorStateHintConstructors.java", 4); - assertHints(errors.get(0), - new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready. " - + "Objects created with new ErrorStateHintConstructors() start in such a state")); - assertHints(errors.get(1), - new Hint(Kind.NEEDED_STATE, "The state of this is unknown here, and this call needs it to be ready")); - assertHints(errors.get(2), - new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready")); - assertHints(errors.get(3), - new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready")); + assertHints(errors.get(0), new Hint(Kind.NEEDED_STATE, + "The state of `value` is unknown here, and this call needs it to be `ready`. Objects created with `new ErrorStateHintConstructors()` start in such a state")); + assertHints(errors.get(1), new Hint(Kind.NEEDED_STATE, + "The state of `this` is unknown here, and this call needs it to be `ready`")); + assertHints(errors.get(2), new Hint(Kind.NEEDED_STATE, + "The state of `value` is unknown here, and this call needs it to be `ready`")); + assertHints(errors.get(3), new Hint(Kind.NEEDED_STATE, + "The state of `value` is unknown here, and this call needs it to be `ready`")); } @Test void onlyPublicInheritedMethodsAreSuggested() { List errors = errors("classes/state_hints_inaccessible_inherited_error", 2); // the files are verified in no fixed order - assertEquals(Set.of( - List.of(new Hint(Kind.CALL_SEQUENCE, - "Call hatch.openPublicly() before this call; afterwards hatch is open")), - List.of(new Hint(Kind.CALL_SEQUENCE, "Call door.push() before this call; afterwards door is ajar"))), + assertEquals( + Set.of(List.of(new Hint(Kind.CALL_SEQUENCE, + "Call `hatch.openPublicly()` before this call; afterwards `hatch` is `open`")), + List.of(new Hint(Kind.CALL_SEQUENCE, + "Call `door.push()` before this call; afterwards `door` is `ajar`"))), errors.stream().map(StateRefinementError::getHints).collect(Collectors.toSet())); } @Test void argumentThatDecidedTheStateIsShownWithAValueThatWouldWork() { assertHints("ErrorArgumentPicksTheState.java", new Hint(Kind.DECIDING_ARGUMENT, - "buffer.reset(boolean keep) on line 20 decides the state of buffer: with keep == true, this call would be allowed")); + "`buffer.reset(boolean keep)` on line 20 decides the state of `buffer`: with `keep == true`, this call would be allowed")); + // the line it names, for clients to link to + SourceReference reference = errors("ErrorArgumentPicksTheState.java", 1).get(0).getHints().get(0).reference(); + assertEquals("line 20", reference.text()); + assertEquals(20, reference.line()); } @Test void deciderIsTheLastCallThatChangedTheCheckedStateSet() { assertHints("ErrorArgumentPicksTheStateEarlier.java", new Hint(Kind.DECIDING_ARGUMENT, - "param.setTilingMode(int mode) on line 25 decides the state of param: with mode == 2, this call would be allowed")); + "`param.setTilingMode(int mode)` on line 25 decides the state of `param`: with `mode == 2`, this call would be allowed")); } @Test void checksAreSuggestedOnlyWhenTheRefinementsProveThem() { List errors = errors("ErrorStateHintGuards.java", 12); - assertHints(errors.get(0), - new Hint(Kind.NEEDED_STATE, - "The state of c is unknown here, and this call needs it to be open. " - + "Objects created with new GuardChannel() start in such a state"), - new Hint(Kind.GUARD, "Guard this call with if (!c.isClosed()); inside it, c is open")); - assertHints(errors.get(1), new Hint(Kind.GUARD, "Guard this call with if (l.tryLock(...)), " - + "filling in the arguments of tryLock(long timeout); inside it, l is locked")); + assertHints(errors.get(0), new Hint(Kind.NEEDED_STATE, + "The state of `c` is unknown here, and this call needs it to be `open`. Objects created with `new GuardChannel()` start in such a state"), + new Hint(Kind.GUARD, "Guard this call with `if (!c.isClosed())`; inside it, `c` is `open`")); + assertHints(errors.get(1), new Hint(Kind.GUARD, + "Guard this call with `if (l.tryLock(...))`, filling in the arguments of `tryLock(long timeout)`; inside it, `l` is `locked`")); assertHints(errors.get(2), - new Hint(Kind.NEEDED_STATE, "The state of p is unknown here, and this call needs it to be ready")); + new Hint(Kind.NEEDED_STATE, "The state of `p` is unknown here, and this call needs it to be `ready`")); assertHints(errors.get(3), - new Hint(Kind.NEEDED_STATE, "The state of w is unknown here, and this call needs it to be accept")); + new Hint(Kind.NEEDED_STATE, "The state of `w` is unknown here, and this call needs it to be `accept`")); assertHints(errors.get(4), - new Hint(Kind.GUARD, "Guard this call with if (w.canWrite()); inside it, w is accept")); + new Hint(Kind.GUARD, "Guard this call with `if (w.canWrite())`; inside it, `w` is `accept`")); assertHints(errors.get(5), new Hint(Kind.NEEDED_STATE, - "The state of b is unknown here, and this call needs it to be undoable and redoable")); + "The state of `b` is unknown here, and this call needs it to be `undoable` and `redoable`")); assertHints(errors.get(6), - new Hint(Kind.NEEDED_STATE, "The state of p is unknown here, and this call needs it to be armed")); + new Hint(Kind.NEEDED_STATE, "The state of `p` is unknown here, and this call needs it to be `armed`")); assertHints(errors.get(7), - new Hint(Kind.NEEDED_STATE, "The state of m is unknown here, and this call needs it to be s1")); - assertHints(errors.get(8), - new Hint(Kind.NEEDED_STATE, "The state of t is unknown here, and this call needs it to be fresh. " - + "Objects created with new GuardToken() start in such a state")); + new Hint(Kind.NEEDED_STATE, "The state of `m` is unknown here, and this call needs it to be `s1`")); + assertHints(errors.get(8), new Hint(Kind.NEEDED_STATE, + "The state of `t` is unknown here, and this call needs it to be `fresh`. Objects created with `new GuardToken()` start in such a state")); assertHints(errors.get(9), - new Hint(Kind.AVAILABLE_CALLS, "In state live, r can call: read() (and possibly others)")); - assertHints(errors.get(10), - new Hint(Kind.NEEDED_STATE, "The state of g is unknown here, and this call needs it to be running")); + new Hint(Kind.AVAILABLE_CALLS, "In state `live`, `r` can call: `read()` (and possibly others)")); + assertHints(errors.get(10), new Hint(Kind.NEEDED_STATE, + "The state of `g` is unknown here, and this call needs it to be `running`")); assertHints(errors.get(11), - new Hint(Kind.CALL_SEQUENCE, "Call f.dispose() before this call; afterwards f is hidden")); + new Hint(Kind.CALL_SEQUENCE, "Call `f.dispose()` before this call; afterwards `f` is `hidden`")); } @Test void argumentConditionsAreSuggestedOnlyWhenEveryArgumentMeetingThemWorks() { List errors = errors("ErrorStateHintArgumentConditions.java", 7); assertHints(errors.get(0), new Hint(Kind.CALL_SEQUENCE, - "Call r.set(int lo, int hi) with lo < hi before this call; afterwards r is high")); + "Call `r.set(int lo, int hi)` with `lo < hi` before this call; afterwards `r` is `high`")); assertHints(errors.get(1), new Hint(Kind.CALL_SEQUENCE, - "Call chain.pick(1), then chain.next() before this call; afterwards chain is c")); + "Call `chain.pick(1)`, then `chain.next()` before this call; afterwards `chain` is `c`")); assertHints(errors.get(2), new Hint(Kind.CALL_SEQUENCE, - "Call l.setLimit(int limit) with limit <= 0 before this call; afterwards l is unbounded")); + "Call `l.setLimit(int limit)` with `limit <= 0` before this call; afterwards `l` is `unbounded`")); // no condition, and no value of the earlier call's argument, is claimed to allow the call for (StateRefinementError error : errors.subList(3, 5)) assertHints(error, - new Hint(Kind.AVAILABLE_CALLS, "In state b, l can call: set(int) (and possibly others)")); + new Hint(Kind.AVAILABLE_CALLS, "In state `b`, `l` can call: `set(int)` (and possibly others)")); assertHints(errors.get(5), - new Hint(Kind.AVAILABLE_CALLS, "In state small, s can call: grow(int) (and possibly others)")); - assertHints(errors.get(6), - new Hint(Kind.AVAILABLE_CALLS, "In state empty, b can call: fill(ConditionBin) (and possibly others)")); + new Hint(Kind.AVAILABLE_CALLS, "In state `small`, `s` can call: `grow(int)` (and possibly others)")); + assertHints(errors.get(6), new Hint(Kind.AVAILABLE_CALLS, + "In state `empty`, `b` can call: `fill(ConditionBin)` (and possibly others)")); } @Test void callWhoseStateDependsOnItsArgumentIsSuggestedWithTheCondition() { assertHints("classes/state_hint_compression_mode_error", new Hint(Kind.CALL_SEQUENCE, - "Call wParam.setCompressionMode(2) before this call; afterwards wParam is compressionExplicit")); + "Call `wParam.setCompressionMode(2)` before this call; afterwards `wParam` is `compressionExplicit`")); } @Test @@ -291,20 +287,20 @@ void checksOfTheStudysUndoManagerAreSuggestedOneAfterTheOther() { List errors = errors("classes/state_hint_study_undo_manager_error", 2); assertHints(errors.get(0), new Hint(Kind.NEEDED_STATE, - "The state of undoManager is unknown here, and this call needs it to be redoable"), + "The state of `undoManager` is unknown here, and this call needs it to be `redoable`"), new Hint(Kind.GUARD, - "Guard this call with if (undoManager.canRedo()); inside it, undoManager is redoable")); + "Guard this call with `if (undoManager.canRedo())`; inside it, `undoManager` is `redoable`")); assertHints(errors.get(1), new Hint(Kind.NEEDED_STATE, - "The state of undoManager is unknown here, and this call needs it to be undoable"), + "The state of `undoManager` is unknown here, and this call needs it to be `undoable`"), new Hint(Kind.GUARD, - "Guard this call with if (undoManager.canUndo()); inside it, undoManager is undoable")); + "Guard this call with `if (undoManager.canUndo())`; inside it, `undoManager` is `undoable`")); } @Test void foundOfTheStudysUndoManagerOmitsTheResultsOfOtherCalls() { StateRefinementError error = errors("classes/state_hint_study_undo_manager_error", 2).get(0); - assertEquals("expected redoable(undoManager) but could not prove it", + assertEquals("expected `redoable(undoManager)` but could not prove it", error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); } @@ -312,32 +308,33 @@ void foundOfTheStudysUndoManagerOmitsTheResultsOfOtherCalls() { void foundKeepsANamedStateSetByItsName() { StateRefinementError error = errors("ErrorStateHintMultipleSets.java", 1).get(0); assertEquals( - "found doorState(d@26) == closed && lockState(d) == locked && doorState(d) == doorState(d@26) but expected doorState(d) == closed && lockState(d) == unlocked", + "found `doorState(d@26) == closed && lockState(d) == locked && doorState(d) == doorState(d@26)` but expected `doorState(d) == closed && lockState(d) == unlocked`", error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); // the declaration is shown as written, with what its states mean under it - assertTrue(error.toString().contains(" where closed(this) means doorState(this) == closed, " - + "unlocked(this) means lockState(this) == unlocked\n")); + assertTrue(error.toString().contains(" where `closed(this)` means `doorState(this) == closed`, " + + "`unlocked(this)` means `lockState(this) == unlocked`\n")); } @Test void setNameOfTheClassAndOfItsSuperclassKeepsTheShorthand() { StateRefinementError error = errors("ErrorStateSetNameInSuperclass.java", 1).get(0); - assertEquals("found ready(c) && idle(c) but expected ready(c) && busy(c)", + assertEquals("found `ready(c) && idle(c)` but expected `ready(c) && busy(c)`", error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); - assertHints(error, new Hint(Kind.CALL_SEQUENCE, "Call c.start() before this call; afterwards c is busy")); + assertHints(error, new Hint(Kind.CALL_SEQUENCE, "Call `c.start()` before this call; afterwards `c` is `busy`")); } @Test void queryWrittenWithItsStateSetIsOfferedAsAGuard() { assertHints("ErrorStateValueQuery.java", - new Hint(Kind.NEEDED_STATE, "The state of d is unknown here, and this call needs lock(d) == unlocked"), - new Hint(Kind.GUARD, "Guard this call with if (d.isUnlocked()); inside it, lock(d) == unlocked")); + new Hint(Kind.NEEDED_STATE, + "The state of `d` is unknown here, and this call needs `lock(d) == unlocked`"), + new Hint(Kind.GUARD, "Guard this call with `if (d.isUnlocked())`; inside it, `lock(d) == unlocked`")); } @Test void ghostNamedLikeAStateOfAnotherClassKeepsItsForm() { StateRefinementError error = errors("ErrorStateValueGhostName.java", 1).get(0); - assertEquals("found ready(sensor) == false but expected ready(sensor)", + assertEquals("found `ready(sensor) == false` but expected `ready(sensor)`", error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); } @@ -351,8 +348,10 @@ private static void assertHints(String test, Hint... expected) { assertHints(errors(test, 1).get(0), expected); } + // the place a hint names, if any, is checked on its own private static void assertHints(StateRefinementError error, Hint... expected) { - assertEquals(List.of(expected), error.getHints()); + assertEquals(List.of(expected), + error.getHints().stream().map(hint -> new Hint(hint.kind(), hint.message())).toList()); } /** The {@code count} errors {@code test} reports, in the order they are reported */ diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStaticConstantNames.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStaticConstantNames.java index 627b09c57..0bac8b290 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStaticConstantNames.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStaticConstantNames.java @@ -36,7 +36,8 @@ void constantPassedThroughLocalKeepsItsName() { } private static void assertShowsName(RefinementError error) { - assertEquals("found mode == ImageWriteParam.MODE_EXPLICIT but expected mode != ImageWriteParam.MODE_EXPLICIT", + assertEquals( + "found `mode == ImageWriteParam.MODE_EXPLICIT` but expected `mode != ImageWriteParam.MODE_EXPLICIT`", error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); assertTrue(error.getCounterexample().isEmpty()); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/CodeTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/CodeTest.java new file mode 100644 index 000000000..e472a3193 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/CodeTest.java @@ -0,0 +1,24 @@ +package liquidjava.diagnostics; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.jupiter.api.Test; + +class CodeTest { + + @Test + void codeHoldingABacktickGetsALongerFence() { + assertEquals("`x > 0`", Code.of("x > 0")); + assertEquals("``c == '`'``", Code.of("c == '`'")); + assertEquals("`` `a ``", Code.of("`a")); + } + + @Test + void terminalShowsCodeInColourWithoutItsBackticks() { + String message = "found " + Code.of("x > 0") + " but expected " + Code.of("`a"); + assertEquals( + "found " + Colors.BLUE + "x > 0" + Colors.RESET + " but expected " + Colors.BLUE + "`a" + Colors.RESET, + Code.render(message, true)); + assertEquals(message, Code.render(message, false)); + } +} 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 7a764efe0..899e7afe9 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java @@ -26,7 +26,7 @@ void keepsExpectedVariableSimplifiedOutOfFound() { RefinementError error = error("timeout >= 0", vc("∀port:int. port > 0", "∀timeout:int. true", "true"), "timeout=-1", "port=1"); assertEquals(List.of(pair("timeout", "-1")), error.getCounterexample().assignments()); - assertEquals("Counterexample: timeout == -1", error.getCounterexampleStr()); + assertEquals("Counterexample: `timeout == -1`", error.getCounterexampleStr()); } @Test @@ -66,7 +66,7 @@ void keepsGhostApplicationsOfExpectedAndFormatsTheirArguments() { RefinementError error = error("size(#s_3) > 0", vc("∀port:int. port > 0", "true"), "port=1", "size(#s_3)=0", "length(#a_1)=4"); assertEquals(List.of(pair("size(#s_3)", "0")), error.getCounterexample().assignments()); - assertEquals("Counterexample: size(s) == 0", error.getCounterexampleStr()); + assertEquals("Counterexample: `size(s) == 0`", error.getCounterexampleStr()); } @Test @@ -120,13 +120,13 @@ void keepsAGuardThatRelatesExpectedToAnotherVariable() { void messageSaysExpectedCouldNotBeProvedWhenFoundOnlyGuardsOtherVariables() { RefinementError error = error("timeout >= 0", vc("∀port:int. true", "∀timeout:int. true", "∀##if_condition_1:boolean. !(port < 0 || port > 65535)", "true"), "port=0", "timeout=-1"); - assertEquals("expected timeout >= 0 but could not prove it", error.getMessage()); + assertEquals("expected `timeout >= 0` but could not prove it", error.getMessage()); } @Test void messageWithNothingFoundGivesNoHint() { RefinementError error = error("timeout >= 0", vc("∀timeout:int. true", "true"), "timeout=-1"); - assertEquals("expected timeout >= 0 but could not prove it", error.getMessage()); + assertEquals("expected `timeout >= 0` but could not prove it", error.getMessage()); assertTrue(error.getHints().isEmpty()); } @@ -136,13 +136,13 @@ void messageKeepsOnlyTheGuardsLinkedToExpected() { vc("∀port:int. true", "∀retries:int. true", "∀t:int. true", "∀##if_condition_1:boolean. !(port < 0 || retries > t)", "true"), "port=0", "retries=-2", "t=-1"); - assertEquals("found !(retries > t) but expected t >= 0", error.getMessage()); + assertEquals("found `!(retries > t)` but expected `t >= 0`", error.getMessage()); } @Test void messageKeepsFoundAsWrittenWhenEveryFactIsLinked() { RefinementError error = error("x >= 0", vc("∀x:int. !(x < 0 || x > 5)", "true"), "x=-1"); - assertEquals("found !(x < 0 || x > 5) but expected x >= 0", error.getMessage()); + assertEquals("found `!(x < 0 || x > 5)` but expected `x >= 0`", error.getMessage()); } @Test @@ -152,7 +152,7 @@ void stateMessageKeepsAStateReachingExpectedThroughAnAlias() { new VCSimplificationResult( vc("∀b1:Object. empty(b1)", "∀x:int. x > 0", "∀box:Object. box == b1", "true")), new TranslationTable(), null, List.of(), null, null, UnaryOperator.identity(), List.of()); - assertEquals("found empty(b1) && box == b1 but expected full(box)", error.getMessage()); + assertEquals("found `empty(b1) && box == b1` but expected `full(box)`", error.getMessage()); } @Test @@ -167,7 +167,7 @@ void omitsGhostValuesWithSeveralArgumentsFoundAlreadyStates() { RefinementError error = error("at(#l_1, #i_2) > 0 && #i_2 > 0", vc("∀#i_2:int. at(#l_1, #i_2) == 0", "true"), "at(#l_1, #i_2)=0", "#i_2=0"); assertEquals(List.of(pair("#i_2", "0")), error.getCounterexample().assignments()); - assertEquals("Counterexample: i == 0", error.getCounterexampleStr()); + assertEquals("Counterexample: `i == 0`", error.getCounterexampleStr()); } @Test @@ -175,7 +175,7 @@ void keepsGhostValuesWithSeveralArgumentsFoundSaysNothingAbout() { RefinementError error = error("at(#l_1, #i_2) > 0", vc("∀#i_2:int. #i_2 > 0", "true"), "at(#l_1, #i_2)=0", "#i_2=1"); assertEquals(List.of(pair("at(#l_1, #i_2)", "0"), pair("#i_2", "1")), error.getCounterexample().assignments()); - assertEquals("Counterexample: at(l, i) == 0 && i == 1", error.getCounterexampleStr()); + assertEquals("Counterexample: `at(l, i) == 0 && i == 1`", error.getCounterexampleStr()); } private static RefinementError error(String expected, VCImplication found, String... assignments) { From ec924a18046f186ef5f07a8093d95c4512f6f9bc Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 22:31:33 +0000 Subject: [PATCH 2/3] Keep the spaces of code, name where a reference starts, mark names not found - Code.render strips only the padding Code.of adds around code that starts or ends with a backtick, and reads code across line breaks. - SourceReference gives where its words start in the message, since the code of a call may hold the same words. - Not-found errors and their suggestion mark the name as code. Co-Authored-By: Claude Opus 5.5 --- .../src/main/java/liquidjava/diagnostics/Code.java | 9 ++++++--- .../liquidjava/diagnostics/SourceReference.java | 13 ++++++++++--- .../diagnostics/errors/NotFoundError.java | 6 ++++-- .../liquidjava/diagnostics/hints/StateHints.java | 9 ++++++--- .../java/liquidjava/api/tests/TestOriginNotes.java | 1 + .../java/liquidjava/api/tests/TestStateHints.java | 1 + .../test/java/liquidjava/diagnostics/CodeTest.java | 3 +++ 7 files changed, 31 insertions(+), 11 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Code.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Code.java index 255c28f63..e88f08a14 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Code.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Code.java @@ -10,7 +10,7 @@ public final class Code { // a run of backticks, the code, and a run of the same length - private static final Pattern SPAN = Pattern.compile("(`+)(.+?)(? 2 && code.startsWith(" ") && code.endsWith(" ")) - code = code.substring(1, code.length() - 1); + // the padding of() adds around code that starts or ends with a backtick, not spaces of the code + String inner = code.length() > 2 && code.startsWith(" ") && code.endsWith(" ") + ? code.substring(1, code.length() - 1) : code; + if (inner.startsWith("`") || inner.endsWith("`")) + code = inner; span.appendReplacement(rendered, Matcher.quoteReplacement(Colors.BLUE + code + Colors.RESET)); } span.appendTail(rendered); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/SourceReference.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/SourceReference.java index 854538d0c..4f09c0280 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/SourceReference.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/SourceReference.java @@ -9,7 +9,9 @@ * @param message * the whole line, a message note or a hint, as the diagnostic gives it * @param text - * the words of {@code message} that name the place, which occur in it once + * the words of {@code message} that name the place + * @param start + * where {@code text} starts in {@code message}, as an index of its characters * @param file * the path of the file * @param line @@ -17,10 +19,15 @@ * @param column * the column, from 1 */ -public record SourceReference(String message, String text, String file, int line, int column) { +public record SourceReference(String message, String text, int start, String file, int line, int column) { + /** {@code text} where it first occurs in {@code message}, naming {@code position} */ public static SourceReference of(String message, String text, SourcePosition position) { - return new SourceReference(message, text, position.getFile().getPath(), position.getLine(), + return of(message, text, message.indexOf(text), position); + } + + public static SourceReference of(String message, String text, int start, SourcePosition position) { + return new SourceReference(message, text, start, position.getFile().getPath(), position.getLine(), position.getColumn()); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java index 7f5567735..31fcf0210 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -3,6 +3,7 @@ import java.util.Collection; import java.util.Locale; +import liquidjava.diagnostics.Code; import liquidjava.diagnostics.NameSuggester; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.hints.Hint; @@ -29,11 +30,12 @@ public NotFoundError(SourcePosition position, String name, Kind kind, Collection public NotFoundError(SourcePosition position, String name, Kind kind, TranslationTable translationTable, Collection availableElements) { - super("Not Found Error", String.format("%s '%s' could not be found", kind, name), position, translationTable); + super("Not Found Error", String.format("%s %s could not be found", kind, Code.of(name)), position, + translationTable); this.name = Utils.getSimpleName(name); this.kind = kind; NameSuggester.findClosest(name, availableElements) - .ifPresent(match -> addHint(Hint.general(String.format("Did you mean '%s'?", match)))); + .ifPresent(match -> addHint(Hint.general(String.format("Did you mean %s?", Code.of(match))))); } public String getName() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index 9238dd4f8..a8a3f1104 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -120,9 +120,12 @@ public static Hint decidingArgument(DecidingArgument deciding, String receiver) String values = deciding.values().isEmpty() ? "other arguments" : deciding.values().entrySet().stream() .map(e -> Code.of(e.getKey() + " == " + e.getValue())).collect(Collectors.joining(" and ")); String line = "line " + deciding.call().position().getLine(); - String message = String.format("%s on %s decides the state of %s: with %s, this call would be allowed", - Code.of(call), line, Code.of(receiver), values); - return new Hint(Kind.DECIDING_ARGUMENT, message, SourceReference.of(message, line, deciding.call().position())); + String before = Code.of(call) + " on "; + String message = String.format("%s%s decides the state of %s: with %s, this call would be allowed", before, + line, Code.of(receiver), values); + // the call's code may hold the same words + return new Hint(Kind.DECIDING_ARGUMENT, message, + SourceReference.of(message, line, before.length(), deciding.call().position())); } /** diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java index bf083c25b..75a40a857 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java @@ -35,6 +35,7 @@ void noteNamesTheLineOfTheCallForClientsToLinkTo() { SourceReference reference = error.getReferences().get(0); assertEquals(error.getMessageNotes().get(0), reference.message()); assertEquals("line 27", reference.text()); + assertEquals("Origin: ".length(), reference.start()); assertEquals(27, reference.line()); assertTrue(reference.file().endsWith("ErrorStateHintMultipleSets.java")); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index ce6857c28..a8cb7ca9a 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -218,6 +218,7 @@ void argumentThatDecidedTheStateIsShownWithAValueThatWouldWork() { // the line it names, for clients to link to SourceReference reference = errors("ErrorArgumentPicksTheState.java", 1).get(0).getHints().get(0).reference(); assertEquals("line 20", reference.text()); + assertEquals("line 20", reference.message().substring(reference.start(), reference.start() + 7)); assertEquals(20, reference.line()); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/CodeTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/CodeTest.java index e472a3193..b82322671 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/CodeTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/CodeTest.java @@ -20,5 +20,8 @@ void terminalShowsCodeInColourWithoutItsBackticks() { "found " + Colors.BLUE + "x > 0" + Colors.RESET + " but expected " + Colors.BLUE + "`a" + Colors.RESET, Code.render(message, true)); assertEquals(message, Code.render(message, false)); + // spaces and line breaks of the code itself are kept + assertEquals(Colors.BLUE + " a " + Colors.RESET, Code.render(Code.of(" a "), true)); + assertEquals(Colors.BLUE + "a\nb" + Colors.RESET, Code.render(Code.of("a\nb"), true)); } } From b5e5332c2323ee5c5b05512c3474ff7df80cb0e8 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 22:47:30 +0000 Subject: [PATCH 3/3] Pad code that holds a backtick or ends with a space, so render keeps it exact Co-Authored-By: Claude Opus 5.5 --- .../src/main/java/liquidjava/diagnostics/Code.java | 13 ++++++------- .../test/java/liquidjava/diagnostics/CodeTest.java | 3 ++- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Code.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Code.java index e88f08a14..a1d373dea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Code.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Code.java @@ -16,13 +16,14 @@ private Code() { } /** - * {@code code} marked as code, fenced by more backticks than any run it holds, padded if it starts or ends with one + * {@code code} marked as code, fenced by more backticks than any run it holds, and padded with a space on each side + * if it holds a backtick or starts or ends with a space, so {@link #render} can tell the padding from the code */ public static String of(String code) { String fence = "`"; while (code.contains(fence)) fence += "`"; - String pad = code.startsWith("`") || code.endsWith("`") ? " " : ""; + String pad = code.contains("`") || code.startsWith(" ") || code.endsWith(" ") ? " " : ""; return fence + pad + code + pad + fence; } @@ -38,11 +39,9 @@ static String render(String message, boolean colour) { StringBuilder rendered = new StringBuilder(); while (span.find()) { String code = span.group(2); - // the padding of() adds around code that starts or ends with a backtick, not spaces of the code - String inner = code.length() > 2 && code.startsWith(" ") && code.endsWith(" ") - ? code.substring(1, code.length() - 1) : code; - if (inner.startsWith("`") || inner.endsWith("`")) - code = inner; + // the padding of() adds: code with a space at both ends is always padded + if (code.length() >= 2 && code.startsWith(" ") && code.endsWith(" ")) + code = code.substring(1, code.length() - 1); span.appendReplacement(rendered, Matcher.quoteReplacement(Colors.BLUE + code + Colors.RESET)); } span.appendTail(rendered); diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/CodeTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/CodeTest.java index b82322671..64d4ed42e 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/CodeTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/CodeTest.java @@ -9,7 +9,7 @@ class CodeTest { @Test void codeHoldingABacktickGetsALongerFence() { assertEquals("`x > 0`", Code.of("x > 0")); - assertEquals("``c == '`'``", Code.of("c == '`'")); + assertEquals("`` c == '`' ``", Code.of("c == '`'")); assertEquals("`` `a ``", Code.of("`a")); } @@ -23,5 +23,6 @@ void terminalShowsCodeInColourWithoutItsBackticks() { // spaces and line breaks of the code itself are kept assertEquals(Colors.BLUE + " a " + Colors.RESET, Code.render(Code.of(" a "), true)); assertEquals(Colors.BLUE + "a\nb" + Colors.RESET, Code.render(Code.of("a\nb"), true)); + assertEquals(Colors.BLUE + " ` " + Colors.RESET, Code.render(Code.of(" ` "), true)); } }