From 258708b50f8eb347f661590abebaac02ddf3f1db Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 11 Nov 2026 18:37:20 +0000 Subject: [PATCH 1/5] Show a variable's line tag as a subscript and name every part of an error alike Verifier 0.0.38 writes variables by their name and, only when an error has several values of one, tags the others with the line their value comes from (x@12, numbered x@12#2 when they share a line). The message and the context already used those names, but the server sent the expected, the Found steps, the counterexample and the translation table with the default formatter, so the steps of one error wrote three different values as `preview` and numbered clashes per line (`preview#1`). - Server: the refinement and state refinement DTOs format the expected, each step's binder and predicate, the counterexample and the translation-table keys with the error's DisplayNames. - Webview: a tag is drawn as a subscript, preview with l51 below, titled "value of preview at line 51", in highlighted expressions, binders and the code of messages; the step diff keeps a tagged name as one token; the Unicode superscript digits are no longer matched. Co-Authored-By: Claude Opus 5.5 --- client/src/webview/highlighting.ts | 56 ++++++++++++++++++- client/src/webview/message-text.ts | 3 +- client/src/webview/styles.ts | 6 ++ .../src/webview/views/context/context.spec.ts | 4 +- client/src/webview/views/context/variables.ts | 4 +- .../views/diagnostics/vc-changes.spec.ts | 17 ++++++ .../webview/views/diagnostics/vc-changes.ts | 8 +-- client/src/webview/views/sections.ts | 6 +- .../dtos/diagnostics/CounterexampleDTO.java | 6 +- .../dtos/diagnostics/TranslationTableDTO.java | 8 ++- .../dtos/diagnostics/VCImplicationDTO.java | 11 ++-- .../VCSimplificationResultDTO.java | 7 ++- .../src/main/java/dtos/errors/LJErrorDTO.java | 4 +- .../java/dtos/errors/RefinementErrorDTO.java | 6 +- .../dtos/errors/StateRefinementErrorDTO.java | 4 +- .../java/utils/DiagnosticConverterTest.java | 23 ++++++++ server/src/test/resources/names/Negate.java | 9 +++ 17 files changed, 147 insertions(+), 35 deletions(-) create mode 100644 server/src/test/resources/names/Negate.java diff --git a/client/src/webview/highlighting.ts b/client/src/webview/highlighting.ts index 3b50bf1..c41ca73 100644 --- a/client/src/webview/highlighting.ts +++ b/client/src/webview/highlighting.ts @@ -18,15 +18,22 @@ type ScopeColorRule = { color: string; }; +// the tag the verifier gives a variable written like others in an error: the line its value comes from, x@12, +// numbered when values share a line or have none, x@12#2 and x#2 +const LINE_TAG = "@\\d+(?:#\\d+)?\\b|(?<=[\\w)])#\\d+\\b"; +const LINE_TAG_SCOPE = "line-tag"; +const LINE_TAGS = new RegExp(LINE_TAG, "g"); + const repository = liquidJavaGrammar.repository as GrammarRepository; const patterns = (name: string): GrammarPattern[] => repository[name]?.patterns || []; const expressionPatterns: GrammarPattern[] = [ + { match: LINE_TAG, name: LINE_TAG_SCOPE }, { match: "\\b(return|break|continue|if|else|switch|case|default|for|while|do|try|catch|finally|throw|throws|new)\\b", name: "keyword.control.liquidjava.webview" }, ...patterns("keywords"), ...patterns("functions"), ...patterns("operators"), - { match: "\\b[a-zA-Z_][a-zA-Z0-9_#⁰¹²³⁴⁵⁶⁷⁸⁹]*(?=\\s*\\()", name: "entity.name.function.liquidjava.webview" }, + { match: "\\b[a-zA-Z_][a-zA-Z0-9_#]*(?=\\s*\\()", name: "entity.name.function.liquidjava.webview" }, { match: "\\b[A-Z][a-zA-Z0-9_]*(?=\\s*\\()", name: "entity.name.function.constructor.liquidjava.webview" }, ...patterns("qualified-names"), { match: "\\b(byte|short|long|char|void)\\b", name: "storage.type.primitive.liquidjava.webview" }, @@ -34,7 +41,7 @@ const expressionPatterns: GrammarPattern[] = [ { match: "\\bnull\\b", name: "constant.language.null.liquidjava.webview" }, ...patterns("literals"), { match: "[(){}.,;\\[\\]]", name: "punctuation.separator.liquidjava" }, - { match: "#*[a-zA-Z_][a-zA-Z0-9_#⁰¹²³⁴⁵⁶⁷⁸⁹]*", name: "variable.other.liquidjava" } + { match: "#*[a-zA-Z_](?:[a-zA-Z0-9_]|#(?!\\d))*", name: "variable.other.liquidjava" } ]; const highlightRules: HighlightRule[] = expressionPatterns @@ -61,6 +68,47 @@ function colorForScope(scope: string): string { ?? "var(--vscode-editor-foreground)"; } +// the variable that ends at an index: a name such as this.items, or a call such as failures.size() +function variableBefore(text: string, end: number): string { + let start = end; + for (let depth = 0; start > 0; start--) { + const c = text[start - 1]; + if (c === ")") depth++; + else if (c === "(") { + if (depth === 0) break; + depth--; + } + else if (depth === 0 && !/[\w#.]/.test(c)) break; + } + return text.slice(start, end); +} + +// a line tag as a subscript, l12, that says which value of the variable it stands for +function renderLineTag(tag: string, variable: string): string { + const [, line, number] = /^(?:@(\d+))?(?:#(\d+))?$/.exec(tag) ?? []; + const value = ["value", number, variable && `of ${variable}`, line && `at line ${line}`].filter(Boolean).join(" "); + const text = (line ? `l${line}` : "") + (number ? `#${number}` : ""); + return `${escapeHtml(text)}`; +} + +/** + * Renders text with the line tags of its variables as subscripts, x@12 as x with l12 below + */ +export function renderLineTags(text: string): string { + let html = ""; + let index = 0; + for (const match of text.matchAll(LINE_TAGS)) { + html += escapeHtml(text.slice(index, match.index)) + renderLineTag(match[0], variableBefore(text, match.index)); + index = match.index + match[0].length; + } + return html + escapeHtml(text.slice(index)); +} + +/** The name of a variable without its line tag, as it is written in code */ +export function withoutLineTag(name: string): string { + return name.replace(new RegExp(`(?:${LINE_TAG})$`), ""); +} + function renderHighlightedContent(expression: string): string { let html = ""; let index = 0; @@ -79,7 +127,9 @@ function renderHighlightedContent(expression: string): string { const match = matchingRule.regex.exec(expression); const content = match?.[0] || expression[index] || ""; - html += `${escapeHtml(content)}`; + html += matchingRule.scope === LINE_TAG_SCOPE + ? renderLineTag(content, variableBefore(expression, index)) + : `${escapeHtml(content)}`; index += content.length; } return html; diff --git a/client/src/webview/message-text.ts b/client/src/webview/message-text.ts index f45b2cb..595915f 100644 --- a/client/src/webview/message-text.ts +++ b/client/src/webview/message-text.ts @@ -1,4 +1,5 @@ import type { LJSourceReference } from "../types/diagnostics"; +import { renderLineTags } from "./highlighting"; import { escapeHtml } from "./utils"; // a run of backticks, the code, and a run of the same length, as the verifier marks code in its messages @@ -24,7 +25,7 @@ export function renderMessageText(message: string, references: LJSourceReference CODE_SPAN.lastIndex = index; const span = message[index] === "`" ? CODE_SPAN.exec(message) : null; if (span) { - html += `${escapeHtml(unpad(span[2]))}`; + html += `${renderLineTags(unpad(span[2]))}`; index += span[0].length; continue; } diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 922cfa9..c85bdc1 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -394,6 +394,12 @@ export function getStyles(): string { text-indent: -2ch; color: var(--vscode-descriptionForeground); } + /* the line a variable's value comes from, when the error has several values of it */ + .lj-line-tag { + font-size: 0.75em; + color: var(--vscode-descriptionForeground); + cursor: help; + } .lj-expression, .lj-expression-code { font-family: var(--vscode-editor-font-family); diff --git a/client/src/webview/views/context/context.spec.ts b/client/src/webview/views/context/context.spec.ts index adb357d..a0546bb 100644 --- a/client/src/webview/views/context/context.spec.ts +++ b/client/src/webview/views/context/context.spec.ts @@ -44,8 +44,8 @@ describe('context view', () => { expect(text('#context-ghosts tr:first-child td:last-child')).toBe('ghost'); expect(text('#context-ghosts tr:last-child td:first-child')).toBe('phase(Example) == open'); expect(text('#context-ghosts tr:last-child td:last-child')).toBe('state'); - expect(text('#context-vars tbody td:first-child')).toBe('count@3'); - expect(text('#context-vars tbody td:last-child')).toBe('count@3 > 0'); + expect(text('#context-vars tbody td:first-child')).toBe('countl3'); + expect(text('#context-vars tbody td:last-child')).toBe('countl3 > 0'); expect(Array.from(document.querySelectorAll('.context-toggle-btn'), node => node.getAttribute('aria-expanded'))).toEqual(['true', 'true', 'true']); expect(document.querySelectorAll('.context-section-content.collapsed')).toHaveLength(0); }); diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 79fee22..75d4817 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -1,11 +1,11 @@ import { LJVariable } from "../../../types/context"; import { RefinementMismatchError } from "../../../types/diagnostics"; -import { renderHighlightedInlineExpression } from "../../highlighting"; +import { renderHighlightedInlineExpression, withoutLineTag } from "../../highlighting"; import { escapeHtml, getSimpleName } from "../../utils"; import { renderToggleSection, renderVariableHighlightButton, renderDiagnosticRevealButton } from "../sections"; export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, errorAtCursor?: RefinementMismatchError): string { - const relevantNames = new Set(Object.keys(errorAtCursor?.translationTable || {})); + const relevantNames = new Set(Object.keys(errorAtCursor?.translationTable || {}).map(withoutLineTag)); return /*html*/`
${renderToggleSection('Variables', 'context-vars', isExpanded)} diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts index 2028727..4e2d034 100644 --- a/client/src/webview/views/diagnostics/vc-changes.spec.ts +++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts @@ -50,6 +50,23 @@ describe('verification implications', () => { expect(Array.from(document.querySelectorAll('.vc-change-fragment')).map(fragment => fragment.textContent)) .toEqual(['x > 0 &&']); }); + it('writes a line tag under its variable, saying which value it stands for, and changes it with its variable', () => { + document.body.innerHTML = renderImplication({ + name: 'x@12', type: 'int', predicate: 'x@12 > failures.size()@84 && y#2 > 0', next: conclusion, + }); + + const tags = Array.from(document.querySelectorAll('sub.lj-line-tag')); + expect(tags.map(tag => [tag.textContent, tag.getAttribute('title')])).toEqual([ + ['l12', 'value of x at line 12'], ['l12', 'value of x at line 12'], + ['l84', 'value of failures.size() at line 84'], ['#2', 'value 2 of y'], + ]); + + document.body.innerHTML = renderImplicationChange( + { ...conclusion, predicate: 'x@12 > 0' }, { ...conclusion, predicate: 'x@13 > 0' }, + ); + expect(Array.from(document.querySelectorAll('.vc-change-fragment')).map(fragment => fragment.innerHTML)) + .toEqual([expect.stringMatching(/^]*>x<\/span>]*>l13<\/sub>$/)]); + }); it.each([ ['initial rendering', () => renderImplication({ ...implication, next: null })], ['simplification change', () => renderImplicationChange(implication, { ...implication, next: null })], diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index 24f2e74..5846f30 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -1,6 +1,6 @@ import type { VCImplication } from "../../../types/vc-implications"; import type { TranslationTable } from "../../../types/diagnostics"; -import { getExpressionLines, renderExpressionLines, renderHighlightedInlineExpression } from "../../highlighting"; +import { getExpressionLines, renderExpressionLines, renderHighlightedInlineExpression, renderLineTags } from "../../highlighting"; import { escapeHtml } from "../../utils"; import { renderSourceHighlightButton } from "../sections"; @@ -8,7 +8,7 @@ type ChangeKind = "unchanged" | "removed" | "added"; type DiffOperation = { kind: ChangeKind; value: T }; const MIN_LINE_SIMILARITY = 0.3; -const TOKEN_PATTERN = /\s+|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#⁰¹²³⁴⁵⁶⁷⁸⁹]*|\d+(?:\.\d+)?|[^\s]/gu; +const TOKEN_PATTERN = /\s+|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#]*(?:@\d+(?:#\d+)?)?|@\d+(?:#\d+)?|\d+(?:\.\d+)?|[^\s]/gu; const WHITESPACE_PATTERN = /^\s+$/u; const VC_LINE_SEPARATOR = "\t"; @@ -39,10 +39,10 @@ function getImplicationLines(node: VCImplication): string[] { function renderBinder(binder: string, type: string, translationTable?: TranslationTable): string { const placement = translationTable?.[binder.slice(1)]; if (!placement?.position?.file) { - return `${escapeHtml(binder)}`; + return `${renderLineTags(binder)}`; } return renderSourceHighlightButton( - escapeHtml(binder), + renderLineTags(binder), type ? `Go to source (${type})` : "Go to source", placement.position, "vc-node vc-binder clickable", diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index c427fc8..a571d57 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -113,11 +113,11 @@ export const renderLocation = (diagnostic: LJDiagnostic): string => { }; export function renderVariableHighlightButton(variable: LJVariable): string { - const displayName = variable.displayName; + const name = `${renderHighlightedInlineExpression(variable.displayName)}`; const position = variable.position; - if (!position || !position.file) return `${displayName}`; + if (!position || !position.file) return name; return renderSourceHighlightButton( - `${renderHighlightedInlineExpression(displayName)}`, + name, variable.type ? `Go to source (${variable.type})` : "Go to source", position, "clickable", diff --git a/server/src/main/java/dtos/diagnostics/CounterexampleDTO.java b/server/src/main/java/dtos/diagnostics/CounterexampleDTO.java index 0269f9d..f12ded7 100644 --- a/server/src/main/java/dtos/diagnostics/CounterexampleDTO.java +++ b/server/src/main/java/dtos/diagnostics/CounterexampleDTO.java @@ -2,7 +2,7 @@ import java.util.List; -import liquidjava.rj_language.ast.formatter.VariableFormatter; +import liquidjava.rj_language.ast.formatter.DisplayNames; import liquidjava.smt.Counterexample; /** @@ -10,13 +10,13 @@ */ public record CounterexampleDTO(List assignments) { - public static CounterexampleDTO from(Counterexample counterexample) { + public static CounterexampleDTO from(Counterexample counterexample, DisplayNames names) { if (counterexample == null) return null; List assignments = counterexample.assignments().stream() .map(assignment -> new AssignmentDTO( - VariableFormatter.format(assignment.first()), + names.get(assignment.first()), assignment.second())) .toList(); return new CounterexampleDTO(assignments); diff --git a/server/src/main/java/dtos/diagnostics/TranslationTableDTO.java b/server/src/main/java/dtos/diagnostics/TranslationTableDTO.java index c1a0f56..c422859 100644 --- a/server/src/main/java/dtos/diagnostics/TranslationTableDTO.java +++ b/server/src/main/java/dtos/diagnostics/TranslationTableDTO.java @@ -3,6 +3,7 @@ import java.util.HashMap; import liquidjava.diagnostics.TranslationTable; +import liquidjava.rj_language.ast.formatter.DisplayNames; import liquidjava.rj_language.ast.formatter.VariableFormatter; /** @@ -11,11 +12,14 @@ */ public class TranslationTableDTO extends HashMap { - public static TranslationTableDTO from(TranslationTable translationTable) { + /** + * @param names the names the error gives its variables, or null to write them as in code + */ + public static TranslationTableDTO from(TranslationTable translationTable, DisplayNames names) { TranslationTableDTO dto = new TranslationTableDTO(); if (translationTable != null) { translationTable.forEach((key, value) -> { - dto.put(VariableFormatter.format(key), PlacementInCodeDTO.from(value)); + dto.put(names == null ? VariableFormatter.format(key) : names.get(key), PlacementInCodeDTO.from(value)); }); } return dto; diff --git a/server/src/main/java/dtos/diagnostics/VCImplicationDTO.java b/server/src/main/java/dtos/diagnostics/VCImplicationDTO.java index 4bc76f4..289f6b9 100644 --- a/server/src/main/java/dtos/diagnostics/VCImplicationDTO.java +++ b/server/src/main/java/dtos/diagnostics/VCImplicationDTO.java @@ -1,7 +1,8 @@ package dtos.diagnostics; import liquidjava.processor.VCImplication; -import liquidjava.rj_language.ast.formatter.VariableFormatter; +import liquidjava.rj_language.ast.formatter.DisplayNames; +import liquidjava.rj_language.ast.formatter.ExpressionFormatter; import liquidjava.utils.Utils; /** @@ -9,20 +10,20 @@ */ public record VCImplicationDTO(String name, String type, String predicate, VCImplicationDTO next) { - public static VCImplicationDTO from(VCImplication implication) { + public static VCImplicationDTO from(VCImplication implication, DisplayNames names) { if (implication == null) return null; String name = null; String type = null; if (implication.hasBinder()) { - name = VariableFormatter.format(implication.getName()); + name = names.get(implication.getName()); type = Utils.getSimpleName(implication.getType().getQualifiedName()); } return new VCImplicationDTO( name, type, - implication.getRefinement().getExpression().toDisplayString(), - from(implication.getNext())); + ExpressionFormatter.format(implication.getRefinement().getExpression(), names), + from(implication.getNext(), names)); } } diff --git a/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java b/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java index 0dc9d26..5fc2384 100644 --- a/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java +++ b/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java @@ -1,5 +1,6 @@ package dtos.diagnostics; +import liquidjava.rj_language.ast.formatter.DisplayNames; import liquidjava.rj_language.opt.VCSimplificationResult; /** @@ -7,13 +8,13 @@ */ public record VCSimplificationResultDTO(VCImplicationDTO implication, VCSimplificationResultDTO origin, String simplification) { - public static VCSimplificationResultDTO from(VCSimplificationResult result) { + public static VCSimplificationResultDTO from(VCSimplificationResult result, DisplayNames names) { if (result == null) return null; return new VCSimplificationResultDTO( - VCImplicationDTO.from(result.getImplication()), - from(result.getOrigin()), + VCImplicationDTO.from(result.getImplication(), names), + from(result.getOrigin(), names), result.getSimplification() ); } diff --git a/server/src/main/java/dtos/errors/LJErrorDTO.java b/server/src/main/java/dtos/errors/LJErrorDTO.java index 9293491..b450d65 100644 --- a/server/src/main/java/dtos/errors/LJErrorDTO.java +++ b/server/src/main/java/dtos/errors/LJErrorDTO.java @@ -17,12 +17,12 @@ public class LJErrorDTO extends LJDiagnosticDTO { public LJErrorDTO(String type, LJError error) { super("error", type, error); - this.translationTable = TranslationTableDTO.from(error.getTranslationTable()); + this.translationTable = TranslationTableDTO.from(error.getTranslationTable(), error.getDisplayNames()); } protected LJErrorDTO(String category, String type, LJError error) { super(category, type, error); - this.translationTable = TranslationTableDTO.from(error.getTranslationTable()); + this.translationTable = TranslationTableDTO.from(error.getTranslationTable(), error.getDisplayNames()); } public LJErrorDTO(String category, String type, String title, String message, List hints, String file, diff --git a/server/src/main/java/dtos/errors/RefinementErrorDTO.java b/server/src/main/java/dtos/errors/RefinementErrorDTO.java index 196e5b2..ba369a8 100644 --- a/server/src/main/java/dtos/errors/RefinementErrorDTO.java +++ b/server/src/main/java/dtos/errors/RefinementErrorDTO.java @@ -25,10 +25,10 @@ public class RefinementErrorDTO extends LJErrorDTO { public RefinementErrorDTO(RefinementError error) { super("refinement-error", error); - this.expected = error.getExpected() == null ? null : ExpressionFormatter.format(error.getExpected()); - this.found = VCSimplificationResultDTO.from(error.getFound()); + this.expected = error.getExpected() == null ? null : ExpressionFormatter.format(error.getExpected().getExpression(), error.getDisplayNames()); + this.found = VCSimplificationResultDTO.from(error.getFound(), error.getDisplayNames()); this.customMessage = error.getCustomMessage(); - this.counterexample = CounterexampleDTO.from(error.getCounterexample()); + this.counterexample = CounterexampleDTO.from(error.getCounterexample(), error.getDisplayNames()); this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition()); this.declarationPositions = error.getDeclarationPositions().stream().map(SourcePositionDTO::from).toList(); this.declarationNotes = error.getDeclarationNotes(); diff --git a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java index 7a83166..10ac195 100644 --- a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java +++ b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java @@ -35,8 +35,8 @@ public class StateRefinementErrorDTO extends LJErrorDTO { public StateRefinementErrorDTO(StateRefinementError error) { super("state-refinement-error", error); - this.expected = error.getExpected() == null ? null : ExpressionFormatter.format(error.getExpected()); - this.found = VCSimplificationResultDTO.from(error.getFoundSimplification()); + this.expected = error.getExpected() == null ? null : ExpressionFormatter.format(error.getExpected().getExpression(), error.getDisplayNames()); + this.found = VCSimplificationResultDTO.from(error.getFoundSimplification(), error.getDisplayNames()); this.customMessage = error.getCustomMessage(); this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition()); this.declarationPositions = error.getDeclarationPositions().stream().map(SourcePositionDTO::from).toList(); diff --git a/server/src/test/java/utils/DiagnosticConverterTest.java b/server/src/test/java/utils/DiagnosticConverterTest.java index a0c79c2..605782c 100644 --- a/server/src/test/java/utils/DiagnosticConverterTest.java +++ b/server/src/test/java/utils/DiagnosticConverterTest.java @@ -5,18 +5,25 @@ import java.nio.file.Files; import java.nio.file.Path; import java.util.List; +import java.util.Objects; +import java.util.Set; import java.util.function.UnaryOperator; +import java.util.stream.Stream; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; import org.junit.jupiter.api.io.TempDir; +import dtos.diagnostics.CounterexampleDTO.AssignmentDTO; import dtos.diagnostics.HintDTO; import dtos.diagnostics.LJDiagnosticDTO; import dtos.diagnostics.SourcePositionDTO; import dtos.diagnostics.SourceReferenceDTO; +import dtos.diagnostics.VCImplicationDTO; import dtos.errors.*; import dtos.warnings.*; +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.SourceReference; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.errors.*; @@ -198,6 +205,22 @@ void preservesStateRefinementDetailsWithoutDeclarationFile() { assertEquals(List.of(), dto.stateMachines); } + @Test + void namesTheVariablesOfEveryPartOfAnErrorAsItsMessageDoes() { + String file = Path.of("src", "test", "resources", "names", "Negate.java").toAbsolutePath().toString(); + CommandLineLauncher.launch(file); + RefinementErrorDTO dto = (RefinementErrorDTO) DiagnosticConverter + .convertToDTO(Diagnostics.getInstance().getErrors().iterator().next()); + assertEquals("found `b@7 == 8 && b@7 > 0 && b == -b@7` but expected `b > 0`", dto.message); + VCImplicationDTO original = dto.found.origin().implication(); + assertEquals(List.of("∀b@6 b@6 == 8", "∀b@7 b@7 == b@6 && b@7 > 0", "∀b b == -b@7"), + Stream.iterate(original, Objects::nonNull, VCImplicationDTO::next) + .map(step -> "∀" + step.name() + " " + step.predicate()).toList()); + assertEquals("b > 0", dto.expected); + assertEquals(Set.of("b@6", "b@7", "b"), dto.translationTable.keySet()); + assertEquals(List.of("b"), dto.counterexample.assignments().stream().map(AssignmentDTO::variable).toList()); + } + @Test void convertsTranslationTablePlacementsWithNamesAsInCode() { TranslationTable table = new TranslationTable(); diff --git a/server/src/test/resources/names/Negate.java b/server/src/test/resources/names/Negate.java new file mode 100644 index 0000000..d8980e1 --- /dev/null +++ b/server/src/test/resources/names/Negate.java @@ -0,0 +1,9 @@ +import liquidjava.specification.Refinement; + +class Negate { + void negate() { + @Refinement("_ > 0") + int b = 8; + b = -b; + } +} From c0b86a885792a02643ea3925c00ace095b3b593f Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 11 Nov 2026 18:40:32 +0000 Subject: [PATCH 2/5] Leave text that looks like a line tag inside string literals of messages Co-Authored-By: Claude Opus 5.5 --- client/src/webview/highlighting.ts | 6 ++++-- client/src/webview/views/diagnostics/diagnostics.spec.ts | 5 +++-- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/client/src/webview/highlighting.ts b/client/src/webview/highlighting.ts index c41ca73..2a940af 100644 --- a/client/src/webview/highlighting.ts +++ b/client/src/webview/highlighting.ts @@ -22,7 +22,8 @@ type ScopeColorRule = { // numbered when values share a line or have none, x@12#2 and x#2 const LINE_TAG = "@\\d+(?:#\\d+)?\\b|(?<=[\\w)])#\\d+\\b"; const LINE_TAG_SCOPE = "line-tag"; -const LINE_TAGS = new RegExp(LINE_TAG, "g"); +// the line tags of a text and its string and character literals, which keep their text +const LINE_TAGS_OUTSIDE_LITERALS = new RegExp(`"(?:\\\\.|[^"\\\\])*"|'(?:\\\\.|[^'\\\\])*'|${LINE_TAG}`, "g"); const repository = liquidJavaGrammar.repository as GrammarRepository; const patterns = (name: string): GrammarPattern[] => repository[name]?.patterns || []; @@ -97,7 +98,8 @@ function renderLineTag(tag: string, variable: string): string { export function renderLineTags(text: string): string { let html = ""; let index = 0; - for (const match of text.matchAll(LINE_TAGS)) { + for (const match of text.matchAll(LINE_TAGS_OUTSIDE_LITERALS)) { + if (/^["']/.test(match[0])) continue; html += escapeHtml(text.slice(index, match.index)) + renderLineTag(match[0], variableBefore(text, match.index)); index = match.index + match[0].length; } diff --git a/client/src/webview/views/diagnostics/diagnostics.spec.ts b/client/src/webview/views/diagnostics/diagnostics.spec.ts index 2b17bcc..3a01601 100644 --- a/client/src/webview/views/diagnostics/diagnostics.spec.ts +++ b/client/src/webview/views/diagnostics/diagnostics.spec.ts @@ -92,7 +92,7 @@ describe('diagnostics view', () => { const position = { file: '/workspace/Reader.java', lineStart: 133, colStart: 8, lineEnd: 133, colEnd: 8 }; document.body.innerHTML = renderDiagnosticsView([{ ...error(), messageNotes: [note], references: [{ message: note, text: 'line 134', start: 8, position }], - hints: [{ kind: 'general', message: "Call `` b.f('`') `` first" }], + hints: [{ kind: 'general', message: "Call `` b.f('`') `` first" }, { kind: 'general', message: 'Set `s@9 = "x@1"`' }], }], false, currentFile); const link = document.querySelector('.message-note a.location-link'); @@ -100,7 +100,8 @@ describe('diagnostics view', () => { expect([link?.getAttribute('data-file'), link?.getAttribute('data-line')]).toEqual(['/workspace/Reader.java', '133']); expect(text('.message-note')).toBe('Origin: line 134, new BufferedInputStream(stream) makes markState(b) == unmarked'); expect(Array.from(document.querySelectorAll('.lj-code')).map(code => code.textContent)) - .toEqual(['new BufferedInputStream(stream)', 'markState(b) == unmarked', "b.f('`')"]); + .toEqual(['new BufferedInputStream(stream)', 'markState(b) == unmarked', "b.f('`')", 'sl9 = "x@1"']); + expect(document.querySelector('.lj-code sub.lj-line-tag')?.getAttribute('title')).toBe('value of s at line 9'); }); it('shows every declaration of a refinement with their notes under them', () => { From 77882220c16026abb97baa4f66642e56f0554ab9 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 11 Nov 2026 18:43:02 +0000 Subject: [PATCH 3/5] Keep string and character literals whole when highlighting and diffing steps Co-Authored-By: Claude Opus 5.5 --- client/src/webview/highlighting.ts | 6 ++++-- client/src/webview/views/diagnostics/vc-changes.spec.ts | 5 +++-- client/src/webview/views/diagnostics/vc-changes.ts | 2 +- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/client/src/webview/highlighting.ts b/client/src/webview/highlighting.ts index 2a940af..3b48b32 100644 --- a/client/src/webview/highlighting.ts +++ b/client/src/webview/highlighting.ts @@ -22,13 +22,15 @@ type ScopeColorRule = { // numbered when values share a line or have none, x@12#2 and x#2 const LINE_TAG = "@\\d+(?:#\\d+)?\\b|(?<=[\\w)])#\\d+\\b"; const LINE_TAG_SCOPE = "line-tag"; -// the line tags of a text and its string and character literals, which keep their text -const LINE_TAGS_OUTSIDE_LITERALS = new RegExp(`"(?:\\\\.|[^"\\\\])*"|'(?:\\\\.|[^'\\\\])*'|${LINE_TAG}`, "g"); +// string and character literals, whose text is shown as it is even where it looks like a line tag +const LITERAL = `"(?:\\\\.|[^"\\\\])*"|'(?:\\\\.|[^'\\\\])*'`; +const LINE_TAGS_OUTSIDE_LITERALS = new RegExp(`${LITERAL}|${LINE_TAG}`, "g"); const repository = liquidJavaGrammar.repository as GrammarRepository; const patterns = (name: string): GrammarPattern[] => repository[name]?.patterns || []; const expressionPatterns: GrammarPattern[] = [ + { match: LITERAL, name: "string.quoted.liquidjava.webview" }, { match: LINE_TAG, name: LINE_TAG_SCOPE }, { match: "\\b(return|break|continue|if|else|switch|case|default|for|while|do|try|catch|finally|throw|throws|new)\\b", name: "keyword.control.liquidjava.webview" }, ...patterns("keywords"), diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts index 4e2d034..b8237f9 100644 --- a/client/src/webview/views/diagnostics/vc-changes.spec.ts +++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts @@ -52,7 +52,7 @@ describe('verification implications', () => { }); it('writes a line tag under its variable, saying which value it stands for, and changes it with its variable', () => { document.body.innerHTML = renderImplication({ - name: 'x@12', type: 'int', predicate: 'x@12 > failures.size()@84 && y#2 > 0', next: conclusion, + name: 'x@12', type: 'int', predicate: 'x@12 > failures.size()@84 && y#2 > 0 && s == "x@1"', next: conclusion, }); const tags = Array.from(document.querySelectorAll('sub.lj-line-tag')); @@ -62,8 +62,9 @@ describe('verification implications', () => { ]); document.body.innerHTML = renderImplicationChange( - { ...conclusion, predicate: 'x@12 > 0' }, { ...conclusion, predicate: 'x@13 > 0' }, + { ...conclusion, predicate: 'x@12 > 0 && s == "x@1"' }, { ...conclusion, predicate: 'x@13 > 0 && s == "x@1"' }, ); + expect(document.querySelectorAll('sub')).toHaveLength(1); expect(Array.from(document.querySelectorAll('.vc-change-fragment')).map(fragment => fragment.innerHTML)) .toEqual([expect.stringMatching(/^]*>x<\/span>]*>l13<\/sub>$/)]); }); diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index 5846f30..8b7cc5f 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -8,7 +8,7 @@ type ChangeKind = "unchanged" | "removed" | "added"; type DiffOperation = { kind: ChangeKind; value: T }; const MIN_LINE_SIMILARITY = 0.3; -const TOKEN_PATTERN = /\s+|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#]*(?:@\d+(?:#\d+)?)?|@\d+(?:#\d+)?|\d+(?:\.\d+)?|[^\s]/gu; +const TOKEN_PATTERN = /\s+|"(?:\\.|[^"\\])*"|'(?:\\.|[^'\\])*'|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#]*(?:@\d+(?:#\d+)?)?|@\d+(?:#\d+)?|\d+(?:\.\d+)?|[^\s]/gu; const WHITESPACE_PATTERN = /^\s+$/u; const VC_LINE_SEPARATOR = "\t"; From 5993529084f7e15e8fda70359cffa53707015074 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 11 Nov 2026 18:49:08 +0000 Subject: [PATCH 4/5] Share the literal and line tag patterns with the step diff tokenizer Co-Authored-By: Claude Opus 5.5 --- client/src/webview/highlighting.ts | 4 ++-- client/src/webview/views/diagnostics/vc-changes.ts | 7 +++++-- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/client/src/webview/highlighting.ts b/client/src/webview/highlighting.ts index 3b48b32..33d1a1c 100644 --- a/client/src/webview/highlighting.ts +++ b/client/src/webview/highlighting.ts @@ -20,10 +20,10 @@ type ScopeColorRule = { // the tag the verifier gives a variable written like others in an error: the line its value comes from, x@12, // numbered when values share a line or have none, x@12#2 and x#2 -const LINE_TAG = "@\\d+(?:#\\d+)?\\b|(?<=[\\w)])#\\d+\\b"; +export const LINE_TAG = "@\\d+(?:#\\d+)?\\b|(?<=[\\w)])#\\d+\\b"; const LINE_TAG_SCOPE = "line-tag"; // string and character literals, whose text is shown as it is even where it looks like a line tag -const LITERAL = `"(?:\\\\.|[^"\\\\])*"|'(?:\\\\.|[^'\\\\])*'`; +export const LITERAL = `"(?:\\\\.|[^"\\\\])*"|'(?:\\\\.|[^'\\\\])*'`; const LINE_TAGS_OUTSIDE_LITERALS = new RegExp(`${LITERAL}|${LINE_TAG}`, "g"); const repository = liquidJavaGrammar.repository as GrammarRepository; diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index 8b7cc5f..a3ec82e 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -1,6 +1,8 @@ import type { VCImplication } from "../../../types/vc-implications"; import type { TranslationTable } from "../../../types/diagnostics"; -import { getExpressionLines, renderExpressionLines, renderHighlightedInlineExpression, renderLineTags } from "../../highlighting"; +import { + getExpressionLines, LINE_TAG, LITERAL, renderExpressionLines, renderHighlightedInlineExpression, renderLineTags, +} from "../../highlighting"; import { escapeHtml } from "../../utils"; import { renderSourceHighlightButton } from "../sections"; @@ -8,7 +10,8 @@ type ChangeKind = "unchanged" | "removed" | "added"; type DiffOperation = { kind: ChangeKind; value: T }; const MIN_LINE_SIMILARITY = 0.3; -const TOKEN_PATTERN = /\s+|"(?:\\.|[^"\\])*"|'(?:\\.|[^'\\])*'|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#]*(?:@\d+(?:#\d+)?)?|@\d+(?:#\d+)?|\d+(?:\.\d+)?|[^\s]/gu; +const TOKEN_PATTERN = new RegExp( + `\\s+|${LITERAL}|-->|&&|\\|\\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#]*(?:${LINE_TAG})?|${LINE_TAG}|\\d+(?:\\.\\d+)?|[^\\s]`, "gu"); const WHITESPACE_PATTERN = /^\s+$/u; const VC_LINE_SEPARATOR = "\t"; From cce8ff35444cb8b837529c140c906ab93c14e213 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 11 Nov 2026 19:35:09 +0000 Subject: [PATCH 5/5] Say in a line tag's tooltip which value of the variable it stands for, in words x@12 reads "x at line 12", x@25#2 "the 2nd value x gets at line 25", and x#2 "the 2nd value of x (line unknown)". Co-Authored-By: Claude Opus 5.5 --- client/src/webview/highlighting.ts | 11 ++++++++++- .../src/webview/views/diagnostics/diagnostics.spec.ts | 2 +- .../src/webview/views/diagnostics/vc-changes.spec.ts | 7 ++++--- 3 files changed, 15 insertions(+), 5 deletions(-) diff --git a/client/src/webview/highlighting.ts b/client/src/webview/highlighting.ts index 33d1a1c..4c46924 100644 --- a/client/src/webview/highlighting.ts +++ b/client/src/webview/highlighting.ts @@ -89,11 +89,20 @@ function variableBefore(text: string, end: number): string { // a line tag as a subscript, l12, that says which value of the variable it stands for function renderLineTag(tag: string, variable: string): string { const [, line, number] = /^(?:@(\d+))?(?:#(\d+))?$/.exec(tag) ?? []; - const value = ["value", number, variable && `of ${variable}`, line && `at line ${line}`].filter(Boolean).join(" "); + const name = variable || "the variable"; + const value = !number ? `${name} at line ${line}` + : line ? `the ${ordinal(Number(number))} value ${name} gets at line ${line}` + : `the ${ordinal(Number(number))} value of ${name} (line unknown)`; const text = (line ? `l${line}` : "") + (number ? `#${number}` : ""); return `${escapeHtml(text)}`; } +// 1st, 2nd, 3rd, 4th, ..., 11th, 12th, 13th, ..., 21st +function ordinal(n: number): string { + const suffix = n % 100 >= 11 && n % 100 <= 13 ? "th" : ["th", "st", "nd", "rd"][n % 10] ?? "th"; + return `${n}${suffix}`; +} + /** * Renders text with the line tags of its variables as subscripts, x@12 as x with l12 below */ diff --git a/client/src/webview/views/diagnostics/diagnostics.spec.ts b/client/src/webview/views/diagnostics/diagnostics.spec.ts index 3a01601..2466fcf 100644 --- a/client/src/webview/views/diagnostics/diagnostics.spec.ts +++ b/client/src/webview/views/diagnostics/diagnostics.spec.ts @@ -101,7 +101,7 @@ describe('diagnostics view', () => { expect(text('.message-note')).toBe('Origin: line 134, new BufferedInputStream(stream) makes markState(b) == unmarked'); expect(Array.from(document.querySelectorAll('.lj-code')).map(code => code.textContent)) .toEqual(['new BufferedInputStream(stream)', 'markState(b) == unmarked', "b.f('`')", 'sl9 = "x@1"']); - expect(document.querySelector('.lj-code sub.lj-line-tag')?.getAttribute('title')).toBe('value of s at line 9'); + expect(document.querySelector('.lj-code sub.lj-line-tag')?.getAttribute('title')).toBe('s at line 9'); }); it('shows every declaration of a refinement with their notes under them', () => { diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts index b8237f9..14a2d0c 100644 --- a/client/src/webview/views/diagnostics/vc-changes.spec.ts +++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts @@ -52,13 +52,14 @@ describe('verification implications', () => { }); it('writes a line tag under its variable, saying which value it stands for, and changes it with its variable', () => { document.body.innerHTML = renderImplication({ - name: 'x@12', type: 'int', predicate: 'x@12 > failures.size()@84 && y#2 > 0 && s == "x@1"', next: conclusion, + name: 'x@12', type: 'int', predicate: 'x@12 > failures.size()@84 && y#2 > z@25#2 && s == "x@1"', next: conclusion, }); const tags = Array.from(document.querySelectorAll('sub.lj-line-tag')); expect(tags.map(tag => [tag.textContent, tag.getAttribute('title')])).toEqual([ - ['l12', 'value of x at line 12'], ['l12', 'value of x at line 12'], - ['l84', 'value of failures.size() at line 84'], ['#2', 'value 2 of y'], + ['l12', 'x at line 12'], ['l12', 'x at line 12'], + ['l84', 'failures.size() at line 84'], ['#2', 'the 2nd value of y (line unknown)'], + ['l25#2', 'the 2nd value z gets at line 25'], ]); document.body.innerHTML = renderImplicationChange(