diff --git a/client/src/webview/highlighting.ts b/client/src/webview/highlighting.ts index 3b50bf1..4c46924 100644 --- a/client/src/webview/highlighting.ts +++ b/client/src/webview/highlighting.ts @@ -18,15 +18,25 @@ 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 +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 +export 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"), ...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 +44,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 +71,57 @@ 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 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 + */ +export function renderLineTags(text: string): string { + let html = ""; + let index = 0; + 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; + } + 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 +140,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/diagnostics.spec.ts b/client/src/webview/views/diagnostics/diagnostics.spec.ts index 2b17bcc..2466fcf 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('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 2028727..14a2d0c 100644 --- a/client/src/webview/views/diagnostics/vc-changes.spec.ts +++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts @@ -50,6 +50,25 @@ 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 > 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', '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( + { ...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>$/)]); + }); 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..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 } 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+)?|[^\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"; @@ -39,10 +42,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; + } +}