Show state errors in the State Machine view

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<LiquidJavaTestApi>('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 = <T>(description: string, matches: (event: WebviewMessage) => T | undefined) =>
+            new Promise<T>((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');
+        }
+    });
+});

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;
 };

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<HTMLButtonElement>('.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<HTMLButtonElement>('#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<HTMLElement>('.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<HTMLElement>('.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();
+        });
+    });
 });