diff --git a/client/src/test/state-errors.test.ts b/client/src/test/state-errors.test.ts new file mode 100644 index 0000000..37d7c82 --- /dev/null +++ b/client/src/test/state-errors.test.ts @@ -0,0 +1,71 @@ +import * as assert from 'node:assert/strict'; +import * as path from 'node:path'; +import * as vscode from 'vscode'; +import type { LJDiagnostic, StateRefinementError } from '../types/diagnostics'; +import type { LJStateMachine } from '../types/fsm'; +import type { LiquidJavaTestApi, WebviewMessage } from '../types/test-api'; + +suite('Bundled LiquidJava state machine errors', () => { + test('sends the webview state errors from the caller file with the machine of the refinements file', async () => { + const installed = vscode.extensions.getExtension('AlcidesFonseca.liquid-java'); + assert.ok(installed); + const api = await installed.activate(); + await api.ready; + + const workspace = vscode.workspace.workspaceFolders?.[0]; + assert.ok(workspace); + const refinementsUri = vscode.Uri.joinPath(workspace.uri, 'src/main/java/TreeNodeRefinements.java'); + const callerUri = vscode.Uri.joinPath(workspace.uri, 'src/main/java/FailingTreeNodeState.java'); + const sameFile = (file: string, uri: vscode.Uri) => vscode.Uri.file(path.resolve(file)).fsPath === uri.fsPath; + const isStateError = (diagnostic: LJDiagnostic): diagnostic is StateRefinementError => + diagnostic.type === 'state-refinement-error' && sameFile(diagnostic.file, callerUri); + const subscriptions: vscode.Disposable[] = []; + const nextWebviewMessage = (description: string, matches: (event: WebviewMessage) => T | undefined) => + new Promise((resolve, reject) => { + const timeout = setTimeout(() => reject(new Error(`Timed out waiting for ${description}`)), 90_000); + const done = (callback: () => void) => { + clearTimeout(timeout); + subscription.dispose(); + failure.dispose(); + callback(); + }; + const subscription = api.onWebviewMessage(event => { + const value = matches(event); + if (value !== undefined) done(() => resolve(value)); + }); + const failure = api.onFailure(() => + done(() => reject(new Error(`LiquidJava verifier crashed while waiting for ${description}`)))); + subscriptions.push(subscription, failure, { dispose: () => clearTimeout(timeout) }); + }); + + try { + // hide the view first so showing it always loads a fresh webview + await vscode.commands.executeCommand('workbench.action.closeSidebar'); + const ready = nextWebviewMessage('the webview to be ready', event => + event.direction === 'fromWebview' && event.message.type === 'ready' ? true : undefined); + await vscode.commands.executeCommand('liquidjava.showView'); + await ready; + + const machine = nextWebviewMessage('the refinements file state machine', event => + event.direction === 'toWebview' && event.message.type === 'fsm' && event.message.sm + ? event.message.sm as LJStateMachine : undefined); + const stateError = nextWebviewMessage('the state error diagnostics', event => + event.direction === 'toWebview' && event.message.type === 'diagnostics' + ? (event.message.diagnostics as LJDiagnostic[]).find(isStateError) : undefined); + const document = await vscode.workspace.openTextDocument(refinementsUri); + await vscode.window.showTextDocument(document); + await vscode.commands.executeCommand('liquidjava.verify'); + + const [sm, error] = await Promise.all([machine, stateError]); + assert.equal(sm.className, 'javax.swing.tree.DefaultMutableTreeNode'); + assert.ok(error.stateMachine, 'the state error must carry its state machine'); + assert.equal(error.stateMachine.className, sm.className, 'errors are matched to the machine by class'); + assert.ok(error.stateMachine.errorContext, 'the state error must carry its error context'); + assert.ok(error.position && sameFile(error.position.file ?? error.file, callerUri)); + assert.ok(error.declarationPosition?.file && sameFile(error.declarationPosition.file, refinementsUri)); + } finally { + subscriptions.forEach(subscription => subscription.dispose()); + await vscode.commands.executeCommand('workbench.action.closeAllEditors'); + } + }); +}); diff --git a/client/src/types/fsm.ts b/client/src/types/fsm.ts index 0d252ec..1003955 100644 --- a/client/src/types/fsm.ts +++ b/client/src/types/fsm.ts @@ -11,4 +11,9 @@ export type LJStateMachine = { export type LJStateMachineErrorContext = { calledMethod: string | null; actualStates: string[]; + receiver?: string | null; + expectedStates?: string[]; + expectedCondition?: string | null; + foundCondition?: string | null; + definiteFoundState?: string | null; }; diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index 25dfdca..34edc0e 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -1,7 +1,7 @@ import { JSDOM } from 'jsdom'; import { afterEach, beforeEach, describe, expect, it, vi, type Mock } from 'vitest'; import type { LJContext, LJVariable } from '../types/context'; -import type { LJDiagnostic, SourcePosition } from '../types/diagnostics'; +import type { LJDiagnostic, SourcePosition, StateRefinementError } from '../types/diagnostics'; import type { LJStateMachine } from '../types/fsm'; const currentFile = '/workspace/src/Main.java'; @@ -57,6 +57,36 @@ const stateMachine: LJStateMachine = { errorContext: null, }; +const refinementsFile = '/workspace/src/DefaultMutableTreeNodeRefinements.java'; +const treeMachine: LJStateMachine = { + className: 'javax.swing.tree.DefaultMutableTreeNode', + initialTransitions: [{ to: 'childrenAllowed' }], + states: ['childrenAllowed', 'maybeHasChildren'], + transitions: [ + { from: 'childrenAllowed', to: 'maybeHasChildren', label: 'add' }, + { from: 'maybeHasChildren', to: 'childrenAllowed', label: 'removeAllChildren' }, + { from: 'maybeHasChildren', to: 'maybeHasChildren', label: 'getFirstChild' }, + ], + errorContext: null, +}; + +// state errors are reported in the caller file, while the machine comes from the refinements file +function stateError(line: number, calledMethod: string, receiver: string): StateRefinementError { + return { + category: 'error', type: 'state-refinement-error', title: 'State Refinement Error', + message: `found childrenAllowed(${receiver}) but expected maybeHasChildren(${receiver})`, hint: null, + file: otherFile, position: { file: otherFile, lineStart: line, colStart: 8, lineEnd: line, colEnd: 30 }, + translationTable: {}, expected: `maybeHasChildren(${receiver})`, + found: { implication: { name: receiver, type: 'DefaultMutableTreeNode', predicate: `childrenAllowed(${receiver})`, next: null }, origin: null, simplification: null }, + customMessage: '', + declarationPosition: { file: refinementsFile, lineStart: calledMethod === 'getFirstChild' ? 21 : 18, colStart: 4, lineEnd: 21, colEnd: 40 }, + stateMachine: { ...treeMachine, errorContext: { + calledMethod, actualStates: ['childrenAllowed'], receiver, + expectedStates: ['maybeHasChildren'], definiteFoundState: 'childrenAllowed', + } }, + }; +} + describe('webview script', () => { let dom: JSDOM; let root: HTMLElement; @@ -226,4 +256,175 @@ describe('webview script', () => { highlightRange: range, }]]); }); + + describe('state errors beside the diagram', () => { + const firstChildError = stateError(10, 'getFirstChild', 'root'); + const removeError = stateError(15, 'removeAllChildren', 'menu'); + + function showStateMachine(diagnostics: LJDiagnostic[]) { + receive({ type: 'file', file: refinementsFile }); + receive({ type: 'diagnostics', diagnostics }); + receive({ type: 'status', status: 'failed' }); + receive({ type: 'fsm', sm: treeMachine }); + click('[data-tab="fsm"]'); + } + + const items = () => Array.from(root.querySelectorAll('.state-error-select')); + const pressed = () => items().map(item => item.getAttribute('aria-pressed')); + const calls = () => Array.from(root.querySelectorAll('.state-error-call'), node => node.textContent); + const mermaidSource = () => root.querySelector('.mermaid')?.innerHTML ?? ''; + + it('lists errors from other files for the machine of the current file', () => { + showStateMachine([firstChildError, removeError, diagnostic(currentFile, 'Unrelated error')]); + + expect(root.querySelector('.diagram-title')?.textContent).toBe('javax.swing.tree.DefaultMutableTreeNode'); + expect(calls()).toEqual(['root.getFirstChild()', 'menu.removeAllChildren()']); + expect(pressed()).toEqual(['false', 'false']); + expect(mermaidSource()).not.toContain('ljStateErrorActual'); + }); + + it('selects an error to highlight it and clears the selection to show the general diagram', () => { + showStateMachine([firstChildError, removeError]); + + items()[0].click(); + expect(pressed()).toEqual(['true', 'false']); + expect(mermaidSource()).toContain('class childrenAllowed ljStateErrorActual'); + expect(mermaidSource()).toContain('lj-state-error-method">getFirstChild'); + expect(dom.window.document.activeElement).toBe(items()[0]); + + items()[1].click(); + expect(pressed()).toEqual(['false', 'true']); + expect(mermaidSource()).toContain('lj-state-error-method">removeAllChildren'); + expect(mermaidSource()).not.toContain('lj-state-error-method">getFirstChild'); + + // selecting the selected error again clears the selection + items()[1].click(); + expect(pressed()).toEqual(['false', 'false']); + expect(mermaidSource()).not.toContain('ljStateErrorActual'); + + items()[0].click(); + click('#state-error-clear-btn'); + expect(pressed()).toEqual(['false', 'false']); + expect(mermaidSource()).not.toContain('lj-state-error-method'); + expect(root.querySelector('#state-error-clear-btn')?.disabled).toBe(true); + expect(calls()).toEqual(['root.getFirstChild()', 'menu.removeAllChildren()']); + }); + + it('keeps the selection when its error remains after verification and drops fixed errors', () => { + showStateMachine([firstChildError, removeError]); + items()[1].click(); + + receive({ type: 'diagnostics', diagnostics: [stateError(10, 'getFirstChild', 'root'), stateError(15, 'removeAllChildren', 'menu')] }); + expect(pressed()).toEqual(['false', 'true']); + expect(mermaidSource()).toContain('lj-state-error-method">removeAllChildren'); + + receive({ type: 'diagnostics', diagnostics: [stateError(15, 'removeAllChildren', 'menu')] }); + expect(calls()).toEqual(['menu.removeAllChildren()']); + expect(pressed()).toEqual(['true']); + + receive({ type: 'diagnostics', diagnostics: [firstChildError] }); + expect(calls()).toEqual(['root.getFirstChild()']); + expect(pressed()).toEqual(['false']); + expect(mermaidSource()).not.toContain('ljStateErrorActual'); + }); + + it('keeps the diagram and drops the list once every state error is fixed', () => { + showStateMachine([firstChildError]); + items()[0].click(); + + receive({ type: 'diagnostics', diagnostics: [] }); + expect(root.querySelector('.diagram-title')?.textContent).toBe('javax.swing.tree.DefaultMutableTreeNode'); + expect(root.querySelector('.state-errors')).toBeNull(); + expect(root.querySelector('.fsm-layout')).toBeNull(); + expect(mermaidSource()).not.toContain('ljStateErrorActual'); + }); + + it('preselects the error opened with View error on state machine', () => { + receive({ type: 'file', file: otherFile }); + receive({ type: 'diagnostics', diagnostics: [firstChildError, removeError] }); + receive({ type: 'status', status: 'failed' }); + receive({ type: 'fsm', sm: null }); + + root.querySelectorAll('.diagnostic-state-machine-btn')[1].click(); + expect(root.querySelector('.nav-tab.selected')?.getAttribute('data-tab')).toBe('fsm'); + expect(calls()).toEqual(['root.getFirstChild()', 'menu.removeAllChildren()']); + expect(pressed()).toEqual(['false', 'true']); + expect(mermaidSource()).toContain('lj-state-error-method">removeAllChildren'); + + // the caller file has no machine of its own, so clearing keeps the error machine without its context + click('#state-error-clear-btn'); + expect(root.querySelector('.diagram-title')?.textContent).toBe('javax.swing.tree.DefaultMutableTreeNode'); + expect(pressed()).toEqual(['false', 'false']); + expect(mermaidSource()).not.toContain('lj-state-error-method'); + }); + + it('drops a fixed selection instead of selecting a sibling error for the same call', () => { + const sibling = stateError(20, 'getFirstChild', 'node'); + showStateMachine([firstChildError, sibling]); + items()[0].click(); + + receive({ type: 'diagnostics', diagnostics: [stateError(20, 'getFirstChild', 'node')] }); + expect(calls()).toEqual(['node.getFirstChild()']); + expect(pressed()).toEqual(['false']); + expect(mermaidSource()).not.toContain('lj-state-error-method'); + }); + + it('refreshes a machine from another file after its selection is cleared or fixed', () => { + // edits to the refinements file add a method to every error machine + const withState = (error: StateRefinementError, method: string): StateRefinementError => ({ + ...error, + stateMachine: { ...error.stateMachine!, transitions: [ + ...treeMachine.transitions, { from: 'childrenAllowed', to: 'childrenAllowed', label: method }, + ] }, + }); + // the caller file has no machine, so the diagram comes from the errors + receive({ type: 'file', file: otherFile }); + receive({ type: 'diagnostics', diagnostics: [firstChildError, removeError] }); + receive({ type: 'status', status: 'failed' }); + receive({ type: 'fsm', sm: null }); + root.querySelectorAll('.diagnostic-state-machine-btn')[0].click(); + click('#state-error-clear-btn'); + + receive({ type: 'diagnostics', diagnostics: [withState(firstChildError, 'cleared'), withState(removeError, 'cleared')] }); + expect(root.querySelector('.state-errors')).not.toBeNull(); + expect(root.querySelector('.mermaid')?.textContent).toContain('cleared'); + expect(mermaidSource()).not.toContain('ljStateErrorActual'); + + items()[0].click(); + receive({ type: 'diagnostics', diagnostics: [withState(removeError, 'fixed')] }); + expect(calls()).toEqual(['menu.removeAllChildren()']); + expect(pressed()).toEqual(['false']); + expect(root.querySelector('.mermaid')?.textContent).toContain('fixed'); + expect(mermaidSource()).not.toContain('ljStateErrorActual'); + }); + + it('keeps the rendered view and focus when a verification changes nothing', () => { + showStateMachine([firstChildError, removeError]); + items()[1].click(); + const renderedItem = items()[1]; + const mermaidRuns = runMermaid.mock.calls.length; + expect(dom.window.document.activeElement).toBe(renderedItem); + + receive({ type: 'diagnostics', diagnostics: [stateError(10, 'getFirstChild', 'root'), stateError(15, 'removeAllChildren', 'menu')] }); + receive({ type: 'status', status: 'failed' }); + expect(items()[1]).toBe(renderedItem); + expect(runMermaid.mock.calls.length).toBe(mermaidRuns); + expect(dom.window.document.activeElement).toBe(renderedItem); + + // a changed list is rendered again with focus on the same error + receive({ type: 'diagnostics', diagnostics: [stateError(15, 'removeAllChildren', 'menu'), stateError(30, 'getFirstChild', 'node')] }); + expect(calls()).toEqual(['menu.removeAllChildren()', 'node.getFirstChild()']); + expect(runMermaid.mock.calls.length).toBe(mermaidRuns + 1); + expect(dom.window.document.activeElement).toBe(items()[0]); + expect(pressed()).toEqual(['true', 'false']); + }); + + it('leaves the view unchanged when the machine has no state errors', () => { + showStateMachine([diagnostic(currentFile, 'Unrelated error')]); + + expect(root.querySelector('.diagram-title')?.textContent).toBe('javax.swing.tree.DefaultMutableTreeNode'); + expect(root.querySelector('.state-errors')).toBeNull(); + expect(root.querySelector('.fsm-layout')).toBeNull(); + }); + }); }); diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 05b6ed0..357a461 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -3,7 +3,7 @@ import { renderLoading } from "./views/loading"; import { renderStopped } from "./views/stopped"; import { renderStateMachineView } from "./views/fsm/fsm"; import { createMermaidDiagram, renderMermaidDiagram, resetZoom, zoomIn, zoomOut, copyDiagramToClipboard } from "./diagram"; -import type { LJDiagnostic, RefinementMismatchError } from "../types/diagnostics"; +import type { LJDiagnostic, RefinementMismatchError, StateRefinementError } from "../types/diagnostics"; import type { Range } from "../types/context"; import type { LJStateMachine } from "../types/fsm"; import type { ExtensionStatus } from "../state"; @@ -13,6 +13,7 @@ import type { LJContext } from "../types/context"; import { ContextSectionState, renderContextView } from "./views/context/context"; import type { DiagnosticRevealTarget } from "../types/diagnostics"; import { getDiagnosticRevealTargetFromKey, getDiagnosticRevealTargetKey } from "./diagnostic-reveal"; +import { findStateError, focusStateError, getStateErrorKey, getStateMachineErrors, renderStateErrorList } from "./views/fsm/state-errors"; type VSCodeApi = { postMessage(message: unknown): void; @@ -33,6 +34,8 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) let stateMachine: LJStateMachine | undefined; let diagnosticStateMachine: LJStateMachine | undefined; let diagnosticStateMachineFile: string | undefined; + let diagnosticStateMachineError: StateRefinementError | undefined; + let renderedStateMachineView: string | undefined; let context: LJContext; let errorAtCursor: RefinementMismatchError; let selectedTab: NavTab = 'diagnostics'; @@ -144,11 +147,28 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) if (diagnostic?.type !== 'state-refinement-error' || !diagnostic.stateMachine) return; selectedTab = 'fsm'; - diagnosticStateMachine = diagnostic.stateMachine; - diagnosticStateMachineFile = diagnostic.file; showDiagramConditions = false; - currentDiagram = ''; - updateView(); + selectStateError(diagnostic); + return; + } + + // select or clear a state error beside the diagram + const stateErrorButton = target.closest?.('.state-error-select'); + if (stateErrorButton) { + e.stopPropagation(); + const key = stateErrorButton.getAttribute('data-state-error-key'); + const error = getStateMachineErrors(diagnostics, diagnosticStateMachine ?? stateMachine) + .find(stateError => getStateErrorKey(stateError) === key); + const isSelected = !!diagnosticStateMachineError && getStateErrorKey(diagnosticStateMachineError) === key; + selectStateError(isSelected ? undefined : error); + if (key) focusStateError(root, key); + return; + } + if (target.closest?.('#state-error-clear-btn')) { + e.stopPropagation(); + const previousError = diagnosticStateMachineError; + selectStateError(undefined); + if (previousError) focusStateError(root, getStateErrorKey(previousError)); return; } @@ -273,6 +293,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) if (tab === 'fsm') { diagnosticStateMachine = undefined; diagnosticStateMachineFile = undefined; + diagnosticStateMachineError = undefined; } selectedTab = tab; updateView(); @@ -340,18 +361,16 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) updateView(); break; case 'diagnostics': { + const previousDiagnostics = diagnostics; diagnostics = msg.diagnostics as LJDiagnostic[]; if (diagnosticStateMachine) { - const updatedError = diagnostics.find(diagnostic => - diagnostic.type === 'state-refinement-error' - && diagnostic.file.toLowerCase() === diagnosticStateMachineFile?.toLowerCase() - && diagnostic.stateMachine?.className === diagnosticStateMachine?.className - ); - diagnosticStateMachine = updatedError?.type === 'state-refinement-error' - ? updatedError.stateMachine ?? diagnosticStateMachine - : { ...diagnosticStateMachine, errorContext: null }; + const errors = getStateMachineErrors(diagnostics, diagnosticStateMachine); + const updatedError = findStateError(errors, diagnosticStateMachineError, + getStateMachineErrors(previousDiagnostics, diagnosticStateMachine)); + if (updatedError) selectStateError(updatedError, false); + else clearStateErrorSelection(errors); } - if (selectedTab === 'diagnostics' || (selectedTab === 'fsm' && diagnosticStateMachine)) updateView(); + if (selectedTab === 'diagnostics' || selectedTab === 'fsm') updateView(); break; } case 'file': @@ -359,6 +378,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) if (diagnostics && !showAllDiagnostics && selectedTab === 'diagnostics') updateView(); diagnosticStateMachine = undefined; diagnosticStateMachineFile = undefined; + diagnosticStateMachineError = undefined; stateMachine = undefined; currentDiagram = ''; if (selectedTab === 'fsm') updateView(); @@ -383,6 +403,8 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) * Updates the webview content based on the current state */ function updateView() { + const previousStateMachineView = renderedStateMachineView; + renderedStateMachineView = undefined; if (status === 'stopped' || status === 'crashed') { currentDiagram = ''; root.innerHTML = renderStopped(status); @@ -404,7 +426,14 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) const displayedStateMachine = diagnosticStateMachine ?? stateMachine; const diagram = createMermaidDiagram(displayedStateMachine, diagramOrientation, showDiagramConditions); currentDiagram = diagram; - renderStateMachineView(root, displayedStateMachine, diagram, diagramOrientation, showDiagramConditions); + const errorList = renderStateErrorList(getStateMachineErrors(diagnostics, displayedStateMachine), diagnosticStateMachineError); + // skip unchanged views, since every verification would otherwise redraw the diagram + renderedStateMachineView = `${diagram}\n${errorList}`; + if (renderedStateMachineView === previousStateMachineView) break; + + const focusedStateError = document.activeElement?.closest?.('.state-error-select')?.getAttribute('data-state-error-key'); + renderStateMachineView(root, displayedStateMachine, diagram, diagramOrientation, showDiagramConditions, errorList); + if (focusedStateError) focusStateError(root, focusedStateError); if (displayedStateMachine) renderMermaidDiagram(document, window); break; } @@ -414,6 +443,39 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) } } + /** + * Shows a state error on its state machine, or the general diagram when no error is given + * @param error The state error to select + * @param render Whether to update the view + */ + function selectStateError(error: StateRefinementError | undefined, render = true) { + if (error?.stateMachine) { + diagnosticStateMachine = error.stateMachine; + diagnosticStateMachineFile = error.file; + diagnosticStateMachineError = error; + } else { + clearStateErrorSelection(getStateMachineErrors(diagnostics, diagnosticStateMachine)); + } + if (!render) return; + currentDiagram = ''; + updateView(); + } + + /** + * Shows the general diagram of the displayed state machine + * @param errors The current errors of the displayed state machine, used to refresh a machine from another file + */ + function clearStateErrorSelection(errors: StateRefinementError[]) { + if (diagnosticStateMachine) { + const latestStateMachine = errors.find(error => error.stateMachine)?.stateMachine ?? diagnosticStateMachine; + diagnosticStateMachine = stateMachine?.className === diagnosticStateMachine.className + ? undefined + : { ...latestStateMachine, errorContext: null }; + } + diagnosticStateMachineFile = undefined; + diagnosticStateMachineError = undefined; + } + function revealDiagnostic(target: DiagnosticRevealTarget) { selectedTab = 'diagnostics'; diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index e26a633..66d0a25 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -1016,5 +1016,95 @@ export function getStyles(): string { fill: var(--vscode-errorForeground) !important; stroke: var(--vscode-errorForeground) !important; } + .fsm-layout { + display: flex; + flex-wrap: wrap; + align-items: flex-start; + gap: 1rem; + } + .fsm-layout .diagram-section { + flex: 3 1 24rem; + min-width: 0; + } + .state-errors { + flex: 1 1 14rem; + min-width: 0; + } + .state-errors-header { + display: flex; + align-items: baseline; + justify-content: space-between; + flex-wrap: wrap; + gap: 0.5rem; + margin-bottom: 0.5rem; + } + .state-errors-header h3 { + margin: 0; + font-size: 0.95rem; + } + .state-errors-count { + font-weight: normal; + opacity: 0.7; + } + .state-errors-header .underline-button { + margin-bottom: 0; + } + .state-errors-header .underline-button:disabled { + opacity: 0.35; + cursor: default; + } + .state-error-item { + background-color: var(--vscode-textCodeBlock-background); + border-radius: 4px; + margin-bottom: 0.5rem; + padding: 0.5rem; + outline: 2px solid transparent; + } + .state-error-item.selected { + outline-color: var(--vscode-focusBorder); + } + .state-error-select { + display: flex; + align-items: flex-start; + gap: 0.5rem; + width: 100%; + padding: 0.25rem; + color: var(--vscode-foreground); + background: none; + border: none; + text-align: left; + } + .state-error-select:hover { + background: none; + } + .state-error-select:focus-visible { + outline: 1px solid var(--vscode-focusBorder); + outline-offset: -1px; + } + .state-error-marker { + flex-shrink: 0; + margin-top: 0.2rem; + } + .state-error-item.selected .state-error-marker { + color: var(--vscode-focusBorder); + } + .state-error-details { + display: flex; + flex-direction: column; + gap: 0.15rem; + min-width: 0; + overflow-wrap: anywhere; + } + .state-error-call { + font-weight: 600; + } + .state-error-label { + opacity: 0.8; + } + .state-error-location { + margin-top: 0.25rem; + padding: 0 0.25rem 0.25rem 1.75rem; + font-size: 0.85rem; + } `; } diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index 263090d..dc133ce 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -3,13 +3,13 @@ import { renderCodiconButton } from "../../icons"; import { escapeHtml } from "../../utils"; import { renderMainHeader } from "../sections"; -export function renderStateMachineView(root: HTMLElement, sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean) { +export function renderStateMachineView(root: HTMLElement, sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, errorList = '') { const previousDiagramContainer = root.querySelector('.diagram-container') as HTMLElement | null; const diagramHeight = previousDiagramContainer?.offsetHeight; - root.innerHTML = renderStateMachineViewHtml(sm, diagram, orientation, showConditions, diagramHeight); + root.innerHTML = renderStateMachineViewHtml(sm, diagram, orientation, showConditions, diagramHeight, errorList); } -function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, diagramHeight?: number): string { +function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, diagramHeight?: number, errorList = ''): string { const hasConditionExpansions = sm ? sm.initialTransitions.some(transition => !!transition.toCondition) || sm.transitions.some(transition => !!transition.fromCondition || !!transition.toCondition) @@ -21,7 +21,7 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str return /*html*/`
${renderMainHeader("", 'fsm')} - ${sm ? /*html*/` + ${sm ? renderWithErrorList(/*html*/`
@@ -45,8 +45,12 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str 
${diagram}
-
` +
`, errorList) : 'No state machine available for the current file'} `; } + +function renderWithErrorList(diagramSection: string, errorList: string): string { + return errorList ? /*html*/`
${diagramSection}${errorList}
` : diagramSection; +} diff --git a/client/src/webview/views/fsm/state-errors.spec.ts b/client/src/webview/views/fsm/state-errors.spec.ts new file mode 100644 index 0000000..3a37b39 --- /dev/null +++ b/client/src/webview/views/fsm/state-errors.spec.ts @@ -0,0 +1,172 @@ +import { afterEach, describe, expect, it } from 'vitest'; +import type { LJDiagnostic, StateRefinementError } from '../../../types/diagnostics'; +import type { LJStateMachine, LJStateMachineErrorContext } from '../../../types/fsm'; +import { findStateError, getStateErrorKey, getStateErrorSummary, getStateMachineErrors, renderStateErrorList } from './state-errors'; +import { renderStateMachineView } from './fsm'; + +const refinementsFile = '/workspace/src/DefaultMutableTreeNodeRefinements.java'; +const callerFile = '/workspace/src/OutlineBuilder.java'; + +function machine(errorContext: LJStateMachineErrorContext | null = null, className = 'javax.swing.tree.DefaultMutableTreeNode'): LJStateMachine { + return { + className, states: ['childrenAllowed', 'maybeHasChildren'], + initialTransitions: [{ to: 'childrenAllowed' }], + transitions: [{ from: 'childrenAllowed', to: 'maybeHasChildren', label: 'add' }], + errorContext, + }; +} + +function stateError(line: number, overrides: Partial = {}): StateRefinementError { + return { + category: 'error', type: 'state-refinement-error', title: 'State Refinement Error', + message: 'found childrenAllowed(root¹⁸) but expected maybeHasChildren(root¹⁸)', hint: null, + file: callerFile, position: { file: callerFile, lineStart: line, colStart: 15, lineEnd: line, colEnd: 35 }, + translationTable: {}, expected: 'maybeHasChildren(root¹⁸)', + found: { implication: { name: 'root¹⁸', type: 'DefaultMutableTreeNode', predicate: 'childrenAllowed(root¹⁸)', next: null }, origin: null, simplification: null }, + customMessage: '', + declarationPosition: { file: refinementsFile, lineStart: 21, colStart: 29, lineEnd: 21, colEnd: 51 }, + stateMachine: machine({ calledMethod: null, actualStates: ['childrenAllowed'] }), + ...overrides, + }; +} + +const fullContext: LJStateMachineErrorContext = { + calledMethod: 'getFirstChild', actualStates: ['childrenAllowed'], receiver: 'root', + expectedStates: ['maybeHasChildren'], expectedCondition: 'maybeHasChildren(root)', + foundCondition: 'childrenAllowed(root)', definiteFoundState: 'childrenAllowed', +}; + +afterEach(() => { + document.body.innerHTML = ''; +}); + +describe('state machine errors', () => { + it('matches errors to the machine by class, not by file', () => { + const matching = stateError(10); + const otherClass = stateError(12, { stateMachine: machine(null, 'java.util.ArrayList') }); + const withoutMachine = stateError(14, { stateMachine: null }); + const refinementError = { ...stateError(16), type: 'custom-error' } as unknown as LJDiagnostic; + + expect(getStateMachineErrors([matching, otherClass, withoutMachine, refinementError], machine())).toEqual([matching]); + expect(getStateMachineErrors([matching], undefined)).toEqual([]); + expect(getStateMachineErrors(undefined, machine())).toEqual([]); + }); + + it('summarizes errors with the state machine error context', () => { + expect(getStateErrorSummary(stateError(10, { stateMachine: machine(fullContext) }))).toEqual({ + call: 'root.getFirstChild()', receiver: 'root', found: 'childrenAllowed', required: 'maybeHasChildren', + }); + expect(getStateErrorSummary(stateError(10, { stateMachine: machine({ + calledMethod: 'getFirstChild', actualStates: [], expectedStates: [], + expectedCondition: 'maybeHasChildren(root)', foundCondition: 'true', definiteFoundState: null, + }) }))).toEqual({ + call: 'getFirstChild()', receiver: null, found: 'true', required: 'maybeHasChildren(root)', + }); + }); + + it('falls back to the diagnostic text without the extended error context', () => { + expect(getStateErrorSummary(stateError(10))).toEqual({ + call: null, receiver: null, found: 'childrenAllowed(root¹⁸)', required: 'maybeHasChildren(root¹⁸)', + }); + + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false, renderStateErrorList([stateError(10)], undefined)); + const item = document.querySelector('.state-error-item')!; + expect(item.querySelector('.state-error-call')?.textContent).toBe('State Refinement Error'); + expect(item.textContent).not.toContain('Receiver:'); + expect(item.textContent).toContain('Found: childrenAllowed(root¹⁸)'); + expect(item.textContent).toContain('Required: maybeHasChildren(root¹⁸)'); + }); + + it('renders each error with its call, receiver, states, and source link beside the diagram', () => { + const errors = [stateError(10, { stateMachine: machine(fullContext) }), stateError(15)]; + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false, renderStateErrorList(errors, undefined)); + + const layout = document.querySelector('.fsm-layout')!; + expect(Array.from(layout.children, child => child.className)).toEqual(['diagram-section', 'state-errors']); + expect(document.querySelector('#state-errors-title')?.textContent).toBe('State Errors (2)'); + const [first, second] = Array.from(document.querySelectorAll('.state-error-item')); + const details = Array.from(first.querySelectorAll('.state-error-details > *'), node => node.textContent?.replace(/\s+/g, ' ').trim()); + expect(details).toEqual(['root.getFirstChild()', 'Receiver: root', 'Found: childrenAllowed', 'Required: maybeHasChildren']); + const link = first.querySelector('.state-error-location .location-link')!; + expect(link.textContent).toBe('OutlineBuilder.java:11'); + expect(link.getAttribute('data-file')).toBe(callerFile); + expect(link.getAttribute('data-line')).toBe('10'); + expect(link.closest('button')).toBeNull(); + expect(second.querySelector('.location-link')?.textContent).toBe('OutlineBuilder.java:16'); + expect(document.querySelector('#state-error-clear-btn')?.disabled).toBe(true); + }); + + it('marks the selected error with state, icon, and enabled clear button', () => { + const errors = [stateError(10), stateError(15)]; + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false, renderStateErrorList(errors, errors[1])); + + const buttons = Array.from(document.querySelectorAll('.state-error-select')); + expect(buttons.map(button => button.getAttribute('aria-pressed'))).toEqual(['false', 'true']); + expect(buttons.map(button => button.tagName)).toEqual(['BUTTON', 'BUTTON']); + expect(buttons[0].querySelector('.codicon-circle-large-outline')).not.toBeNull(); + expect(buttons[1].querySelector('.codicon-pass-filled')).not.toBeNull(); + expect(buttons[1].closest('.state-error-item')?.classList.contains('selected')).toBe(true); + expect(buttons[1].getAttribute('data-state-error-key')).toBe(getStateErrorKey(errors[1])); + expect(document.querySelector('#state-error-clear-btn')?.disabled).toBe(false); + }); + + it('leaves the view unchanged when there are no state errors', () => { + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false); + const withoutList = document.body.innerHTML; + + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false, renderStateErrorList([], undefined)); + + expect(renderStateErrorList([], undefined)).toBe(''); + expect(document.body.innerHTML).toBe(withoutList); + expect(document.querySelector('.fsm-layout')).toBeNull(); + expect(document.querySelector('.state-errors')).toBeNull(); + }); + + it('escapes error text', () => { + const error = stateError(10, { stateMachine: machine({ ...fullContext, receiver: '', calledMethod: 'run' }) }); + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false, renderStateErrorList([error], undefined)); + + expect(document.querySelector('.state-error-call')?.textContent).toBe('.run()'); + expect(document.querySelector('.state-errors img')).toBeNull(); + }); + + it('finds the selected error again after verification', () => { + const selected = stateError(10); + const moved = stateError(12); + const otherCall = stateError(20, { declarationPosition: { file: refinementsFile, lineStart: 18, colStart: 29, lineEnd: 18, colEnd: 51 } }); + + expect(findStateError([otherCall, stateError(10)], selected, [selected, otherCall])).toEqual(selected); + // an edit moved the only error of this call + expect(findStateError([otherCall, moved], selected, [selected, otherCall])).toBe(moved); + expect(findStateError([otherCall, moved], selected)).toBeUndefined(); + expect(findStateError([otherCall], selected, [selected, otherCall])).toBeUndefined(); + expect(findStateError([moved, stateError(14)], selected, [selected])).toBeUndefined(); + expect(findStateError([selected], undefined)).toBeUndefined(); + }); + + it('drops a fixed selection instead of moving it to a sibling for the same call', () => { + const selected = stateError(10); + const sibling = stateError(20); + + expect(findStateError([sibling], selected, [selected, sibling])).toBeUndefined(); + }); + + it('keeps keys distinct for errors without a position', () => { + const first = stateError(10, { position: null, title: 'State Refinement Error', message: 'a' }); + const second = stateError(10, { position: null, title: 'State Conflict', message: 'a' }); + + expect(getStateErrorKey(first)).not.toBe(getStateErrorKey(second)); + expect(getStateErrorKey(first)).not.toMatch(/:\d+:\d+-\d+:\d+$/); + expect(findStateError([second], first)).toBeUndefined(); + }); + + it('escapes the file of the source link', () => { + const file = '/workspace/src/"onmouseover="alert(1).java'; + const error = stateError(10, { file, position: { file, lineStart: 1, colStart: 0, lineEnd: 1, colEnd: 4 } }); + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false, renderStateErrorList([error], undefined)); + + const link = document.querySelector('.state-error-location .location-link')!; + expect(link.getAttribute('data-file')).toBe(file); + expect(link.hasAttribute('onmouseover')).toBe(false); + }); +}); diff --git a/client/src/webview/views/fsm/state-errors.ts b/client/src/webview/views/fsm/state-errors.ts new file mode 100644 index 0000000..9e0c5a0 --- /dev/null +++ b/client/src/webview/views/fsm/state-errors.ts @@ -0,0 +1,161 @@ +import type { LJDiagnostic, StateRefinementError } from "../../../types/diagnostics"; +import type { LJStateMachine } from "../../../types/fsm"; +import type { VCImplication } from "../../../types/vc-implications"; +import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../../diagnostic-reveal"; +import { renderHighlightedInlineExpression } from "../../highlighting"; +import { renderCodicon } from "../../icons"; +import { escapeHtml } from "../../utils"; +import { renderLocationLink } from "../sections"; + +export type StateErrorSummary = { + call: string | null; + receiver: string | null; + found: string; + required: string; +}; + +/** + * Returns the state refinement errors that belong to the given state machine + * @param diagnostics All diagnostics in the workspace + * @param sm The displayed state machine + */ +export function getStateMachineErrors(diagnostics: LJDiagnostic[] | undefined, sm: LJStateMachine | undefined): StateRefinementError[] { + if (!diagnostics || !sm) return []; + return diagnostics.filter((diagnostic): diagnostic is StateRefinementError => + diagnostic.type === 'state-refinement-error' && belongsToStateMachine(diagnostic, sm) + ); +} + +// errors are usually reported in the caller file, so they are matched by class instead of file +function belongsToStateMachine(error: StateRefinementError, sm: LJStateMachine): boolean { + return !!error.stateMachine && error.stateMachine.className === sm.className; +} + +export function getStateErrorKey(error: StateRefinementError): string { + const target = getDiagnosticRevealTarget(error); + // errors without a position never match the position pattern of reveal keys + return target ? getDiagnosticRevealTargetKey(target) : `${error.file}#${error.title}#${error.message}`; +} + +/** + * Finds the selected error again after a new verification + * Since edits can move the error position, falls back to the same file and called method when that call was + * the only one before and after the verification, so a fixed error never passes its selection to a sibling + * @param errors The errors of the displayed state machine + * @param selected The previously selected error + * @param previousErrors The errors of the displayed state machine before the verification + */ +export function findStateError(errors: StateRefinementError[], selected: StateRefinementError | undefined, + previousErrors: StateRefinementError[] = []): StateRefinementError | undefined { + if (!selected) return undefined; + const key = getStateErrorKey(selected); + const exact = errors.find(error => getStateErrorKey(error) === key); + const declarationKey = getDeclarationKey(selected); + if (exact || !declarationKey) return exact; + + const isSameCall = (error: StateRefinementError) => + error.file.toLowerCase() === selected.file.toLowerCase() && getDeclarationKey(error) === declarationKey; + const candidates = errors.filter(isSameCall); + const previousCandidates = previousErrors.filter(isSameCall); + return candidates.length === 1 && previousCandidates.length === 1 ? candidates[0] : undefined; +} + +function getDeclarationKey(error: StateRefinementError): string | undefined { + const position = error.declarationPosition; + if (!position?.file) return undefined; + return getDiagnosticRevealTargetKey({ file: position.file, position }); +} + +/** + * Summarizes an error with the state machine error context, falling back to the diagnostic text + * @param error The state refinement error + */ +export function getStateErrorSummary(error: StateRefinementError): StateErrorSummary { + const context = error.stateMachine?.errorContext; + const receiver = context?.receiver || null; + const calledMethod = context?.calledMethod || null; + const call = calledMethod ? `${receiver ? `${receiver}.` : ''}${calledMethod}()` : null; + const found = context?.definiteFoundState || context?.foundCondition || formatFound(error.found?.implication); + const required = context?.expectedStates?.length + ? context.expectedStates.join(' || ') + : context?.expectedCondition || error.expected || ''; + return { call, receiver, found, required }; +} + +function formatFound(implication: VCImplication | null | undefined): string { + const predicates: string[] = []; + for (let node = implication; node; node = node.next) { + if (node.predicate) predicates.push(node.predicate); + } + return predicates.join(' && '); +} + +/** + * Renders the list of state errors shown beside the diagram + * @param errors The errors of the displayed state machine + * @param selected The selected error, if any + * @returns The list HTML, or an empty string when there are no errors + */ +export function renderStateErrorList(errors: StateRefinementError[], selected: StateRefinementError | undefined): string { + if (errors.length === 0) return ''; + const selectedKey = selected ? getStateErrorKey(selected) : undefined; + const hasSelection = errors.some(error => getStateErrorKey(error) === selectedKey); + + return /*html*/` +
+
+

State Errors (${errors.length})

+ +
+
    + ${errors.map(error => renderStateErrorItem(error, getStateErrorKey(error) === selectedKey)).join('')} +
+
+ `; +} + +function renderStateErrorItem(error: StateRefinementError, selected: boolean): string { + const summary = getStateErrorSummary(error); + const key = getStateErrorKey(error); + const position = error.position ? { ...error.position, file: error.position.file || error.file } : undefined; + + return /*html*/` +
  • + + ${position ? `
    ${renderLocationLink(position)}
    ` : ''} +
    • + `; +} + +function renderDetail(label: string, value: string): string { + return /*html*/`${label}: ${value}`; +} + +function renderExpression(expression: string): string { + return `${renderHighlightedInlineExpression(expression)}`; +} + +/** + * Restores keyboard focus on an error after the view is rendered again + * @param root The webview root element + * @param key The key of the error to focus + */ +export function focusStateError(root: HTMLElement, key: string) { + const button = Array.from(root.querySelectorAll('.state-error-select')) + .find(element => element.getAttribute('data-state-error-key') === key); + button?.focus(); +} diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index df94ec5..4502781 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -122,7 +122,7 @@ export function renderLocationLink(position?: SourcePosition): string { return /*html*/`${escapeHtml(getFile(position))}`; diff --git a/client/test-fixtures/failing/src/main/java/FailingTreeNodeState.java b/client/test-fixtures/failing/src/main/java/FailingTreeNodeState.java new file mode 100644 index 0000000..d2f09a3 --- /dev/null +++ b/client/test-fixtures/failing/src/main/java/FailingTreeNodeState.java @@ -0,0 +1,11 @@ +import javax.swing.tree.DefaultMutableTreeNode; +import javax.swing.tree.TreeNode; + +public class FailingTreeNodeState { + TreeNode rebuild() { + DefaultMutableTreeNode root = new DefaultMutableTreeNode("root"); + root.add(new DefaultMutableTreeNode("first")); + root.removeAllChildren(); + return root.getFirstChild(); + } +} diff --git a/client/test-fixtures/failing/src/main/java/TreeNodeRefinements.java b/client/test-fixtures/failing/src/main/java/TreeNodeRefinements.java new file mode 100644 index 0000000..47c1d7a --- /dev/null +++ b/client/test-fixtures/failing/src/main/java/TreeNodeRefinements.java @@ -0,0 +1,22 @@ +import javax.swing.tree.MutableTreeNode; +import javax.swing.tree.TreeNode; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.swing.tree.DefaultMutableTreeNode") +@StateSet({"childrenAllowed", "maybeHasChildren"}) +public interface TreeNodeRefinements { + @StateRefinement(to = "childrenAllowed(this)") + void DefaultMutableTreeNode(Object userObject); + + @StateRefinement(from = "childrenAllowed(this)", to = "maybeHasChildren(this)") + void add(MutableTreeNode newChild); + + @StateRefinement(from = "maybeHasChildren(this)", to = "childrenAllowed(this)") + void removeAllChildren(); + + @StateRefinement(from = "maybeHasChildren(this)") + TreeNode getFirstChild(); +} diff --git a/server/pom.xml b/server/pom.xml index 514d511..53bef18 100644 --- a/server/pom.xml +++ b/server/pom.xml @@ -172,7 +172,7 @@ io.github.liquid-java liquidjava-fsm - 0.1.3 + 0.1.4 tools.aqua