Skip to content

Commit 45de1b3

Browse files
rcosta358rcosta358
authored
Improve Verification Crashes (#92)
1 parent c7b2f44 commit 45de1b3

11 files changed

Lines changed: 100 additions & 45 deletions

File tree

‎client/src/lsp/client.ts‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ import { LanguageClient, LanguageClientOptions, ServerOptions } from 'vscode-lan
33
import { connectToPort } from '../utils/utils';
44
import { extension } from '../state';
55
import { updateStatusBar } from '../services/status-bar';
6-
import { handleLJDiagnostics } from '../services/diagnostics';
6+
import { handleLJDiagnostics, handleLJFailure } from '../services/diagnostics';
77
import { onActiveFileChange } from '../services/events';
88
import type { LJDiagnostic } from "../types/diagnostics";
99
import { LJContext } from '../types/context';
@@ -42,6 +42,10 @@ export async function runClient(context: vscode.ExtensionContext, port: number)
4242
handleLJDiagnostics(diagnostics);
4343
});
4444

45+
extension.client.onNotification("liquidjava/failure", () => {
46+
handleLJFailure();
47+
});
48+
4549
extension.client.onNotification("liquidjava/context", (context: LJContext) => {
4650
handleContext(context);
4751
});

‎client/src/services/diagnostics.ts‎

Lines changed: 16 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
import * as vscode from "vscode";
2-
import { extension } from "../state";
2+
import { extension, ExtensionStatus } from "../state";
33
import { LJDiagnostic } from "../types/diagnostics";
4-
import { StatusBarState, updateStatusBar } from "./status-bar";
4+
import { updateStatusBar } from "./status-bar";
55
import { updateErrorAtCursor } from "./context";
66
import { refreshCodeLenses } from "./codelens";
77

@@ -11,7 +11,7 @@ import { refreshCodeLenses } from "./codelens";
1111
*/
1212
export function handleLJDiagnostics(diagnostics: LJDiagnostic[]) {
1313
const containsError = diagnostics.some(d => d.category === "error");
14-
const statusBarState: StatusBarState = containsError ? "failed" : "passed";
14+
const statusBarState: ExtensionStatus = containsError ? "failed" : "passed";
1515
updateStatusBar(statusBarState);
1616
extension.diagnostics = diagnostics;
1717
refreshCodeLenses();
@@ -21,6 +21,19 @@ export function handleLJDiagnostics(diagnostics: LJDiagnostic[]) {
2121
extension.webview?.sendMessage({ type: "context", context: extension.context, errorAtCursor: extension.errorAtCursor });
2222
}
2323

24+
/**
25+
* Handles LiquidJava verifier crashes received from the language server
26+
*/
27+
export function handleLJFailure() {
28+
extension.diagnostics = [];
29+
extension.errorAtCursor = undefined;
30+
refreshCodeLenses();
31+
extension.webview?.sendMessage({ type: "diagnostics", diagnostics: [] });
32+
if (extension.context)
33+
extension.webview?.sendMessage({ type: "context", context: extension.context, errorAtCursor: extension.errorAtCursor });
34+
updateStatusBar("crashed");
35+
}
36+
2437
/**
2538
* Triggers the LiquidJava verification manually
2639
*/

‎client/src/services/status-bar.ts‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,20 @@
11
import * as vscode from "vscode";
22
import { ExtensionStatus, extension } from "../state";
33

4-
export type StatusBarState = ExtensionStatus;
5-
6-
const icons = {
4+
const icons = {
75
loading: "$(sync~spin)",
86
stopped: "$(circle-slash)",
97
passed: "$(check)",
108
failed: "$(x)",
9+
crashed: "$(x)",
1110
};
1211

1312
const statusText = {
1413
loading: "Loading",
1514
stopped: "Stopped",
1615
passed: "Verification passed",
1716
failed: "Verification failed",
17+
crashed: "Crashed",
1818
};
1919

2020
/**
@@ -31,15 +31,15 @@ export function registerStatusBar(context: vscode.ExtensionContext) {
3131

3232
/**
3333
* Updates the status bar with the current state
34-
* @param status The current status ("loading", "stopped", "passed", "failed")
34+
* @param status The current status ("loading", "stopped", "passed", "failed", "crashed")
3535
* @param notifyWebview Whether the webview should reflect this status update.
3636
*/
37-
export function updateStatusBar(status: StatusBarState, notifyWebview = status !== "loading") {
37+
export function updateStatusBar(status: ExtensionStatus, notifyWebview = status !== "loading") {
3838
if (notifyWebview) {
3939
extension.status = status;
4040
extension.webview?.sendMessage({ type: "status", status });
4141
}
42-
const color = status === "stopped" ? "errorForeground" : "statusBar.foreground";
42+
const color = status === "stopped" || status === "crashed" ? "errorForeground" : "statusBar.foreground";
4343
if (!extension.statusBar) return;
4444
extension.statusBar.color = new vscode.ThemeColor(color);
4545
extension.statusBar.text = icons[status] + " LiquidJava";

‎client/src/services/webview.ts‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,11 +25,11 @@ export function registerWebview(context: vscode.ExtensionContext) {
2525
context.subscriptions.push(
2626
extension.webview.onDidReceiveMessage(message => {
2727
if (message.type === "ready") {
28-
if (extension.status) extension.webview?.sendMessage({ type: "status", status: extension.status });
2928
if (extension.file) extension.webview?.sendMessage({ type: "file", file: extension.file });
3029
if (extension.diagnostics) extension.webview?.sendMessage({ type: "diagnostics", diagnostics: extension.diagnostics });
3130
if (extension.context) extension.webview?.sendMessage({ type: "context", context: extension.context , errorAtCursor: extension.errorAtCursor });
3231
if (extension.stateMachine) extension.webview?.sendMessage({ type: "fsm", sm: extension.stateMachine });
32+
if (extension.status) extension.webview?.sendMessage({ type: "status", status: extension.status });
3333
}
3434
})
3535
);

‎client/src/state.ts‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ import type { LJDiagnostic, RefinementMismatchError } from "./types/diagnostics"
88
import type { LJStateMachine } from "./types/fsm";
99
import { LJContext, Range } from "./types/context";
1010

11-
export type ExtensionStatus = "loading" | "stopped" | "passed" | "failed";
11+
export type ExtensionStatus = "loading" | "stopped" | "passed" | "failed" | "crashed";
1212

1313
export class ExtensionState {
1414
// server/client state

‎client/src/webview/script.ts‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -299,9 +299,9 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
299299
* Updates the webview content based on the current state
300300
*/
301301
function updateView() {
302-
if (status === 'stopped') {
302+
if (status === 'stopped' || status === 'crashed') {
303303
currentDiagram = '';
304-
root.innerHTML = renderStopped();
304+
root.innerHTML = renderStopped(status);
305305
return;
306306
}
307307
if (status === 'loading') {

‎client/src/webview/styles.ts‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -428,6 +428,7 @@ export function getStyles(): string {
428428
}
429429
.stopped-view {
430430
display: flex;
431+
position: relative;
431432
min-height: calc(100vh - 2rem);
432433
flex-direction: column;
433434
align-items: center;

‎client/src/webview/views/stopped.ts‎

Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,23 @@
1-
export function renderStopped(): string {
1+
type StoppedViewStatus = "stopped" | "crashed";
2+
3+
const stoppedViewContent: Record<StoppedViewStatus, { title: string; message: string }> = {
4+
stopped: {
5+
title: "LiquidJava Not Running",
6+
message: /*html*/`To use LiquidJava, run <code>LiquidJava: Start</code> from the command palette.`,
7+
},
8+
crashed: {
9+
title: "LiquidJava Crashed",
10+
message: /*html*/`LiquidJava could not verify this project. <br /> Check for Java compilation errors.<br /><br />To inspect the problem, run <code>LiquidJava: Show Logs</code> from the command palette.`,
11+
},
12+
};
13+
14+
export function renderStopped(status: StoppedViewStatus): string {
15+
const { title, message } = stoppedViewContent[status];
216
return /*html*/`
317
<div class="stopped-view">
418
<div class="stopped-status-icon" aria-hidden="true">!</div>
5-
<h2>LiquidJava Not Running</h2>
6-
<p class="info">To use LiquidJava, run <code>LiquidJava: Start</code> from the command palette</p>
19+
<h2>${title}</h2>
20+
<p class="info">${message}</p>
721
</div>
822
`;
923
}

‎server/src/main/java/LJDiagnosticsHandler.java‎

Lines changed: 14 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@
1414
import liquidjava.api.CommandLineLauncher;
1515
import liquidjava.diagnostics.Diagnostics;
1616
import liquidjava.diagnostics.LJDiagnostic;
17-
import liquidjava.diagnostics.errors.CustomError;
1817
import liquidjava.diagnostics.errors.LJError;
1918
import liquidjava.diagnostics.warnings.LJWarning;
2019
import spoon.reflect.cu.SourcePosition;
@@ -29,28 +28,23 @@ public class LJDiagnosticsHandler {
2928
* @param path the file path
3029
* @return LJDiagnostics
3130
*/
32-
public static LJDiagnostics getLJDiagnostics(String path) {
31+
public static LJDiagnostics getLJDiagnostics(String path) throws Exception {
3332
List<LJError> errors = new ArrayList<>();
3433
List<LJWarning> warnings = new ArrayList<>();
35-
try {
36-
CommandLineLauncher.cmdArgs.lspMode = true;
37-
CommandLineLauncher.launch(path);
38-
Diagnostics diagnostics = Diagnostics.getInstance();
39-
if (diagnostics.foundWarning()) {
40-
warnings.addAll(diagnostics.getWarnings());
41-
}
42-
if (diagnostics.foundError()) {
43-
System.out.println("Failed verification");
44-
errors.addAll(diagnostics.getErrors());
45-
} else {
46-
System.out.println("Passed verification");
47-
}
48-
return new LJDiagnostics(errors, warnings);
49-
} catch (Exception e) {
50-
e.printStackTrace();
51-
errors.add(new CustomError("LiquidJava verification failed, check for Java errors"));
52-
return new LJDiagnostics(errors, warnings);
34+
35+
CommandLineLauncher.cmdArgs.lspMode = true;
36+
CommandLineLauncher.launch(path);
37+
Diagnostics diagnostics = Diagnostics.getInstance();
38+
if (diagnostics.foundWarning()) {
39+
warnings.addAll(diagnostics.getWarnings());
40+
}
41+
if (diagnostics.foundError()) {
42+
System.out.println("Failed verification");
43+
errors.addAll(diagnostics.getErrors());
44+
} else {
45+
System.out.println("Passed verification");
5346
}
47+
return new LJDiagnostics(errors, warnings);
5448
}
5549

5650
/**

‎server/src/main/java/LJDiagnosticsService.java‎

Lines changed: 31 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
import java.io.File;
22
import java.net.URI;
3+
import java.util.HashSet;
34
import java.util.List;
5+
import java.util.Set;
46
import java.util.concurrent.CompletableFuture;
57
import java.util.concurrent.ExecutorService;
68
import java.util.concurrent.Executors;
@@ -27,6 +29,7 @@ public class LJDiagnosticsService implements TextDocumentService, WorkspaceServi
2729

2830
private LJLanguageClient client;
2931
private String workspaceRoot;
32+
private final Set<String> publishedDiagnosticUris = new HashSet<>();
3033
private final ExecutorService diagnosticsExecutor = Executors.newSingleThreadExecutor(r -> {
3134
Thread thread = new Thread(r, "liquidjava-diagnostics");
3235
thread.setDaemon(true);
@@ -61,14 +64,26 @@ public void sendDiagnosticsNotification(List<LJDiagnostic> diagnostics) {
6164
*/
6265
public void generateDiagnostics(String uri) {
6366
String path = PathUtils.extractBasePath(uri);
64-
LJDiagnostics ljDiagnostics = LJDiagnosticsHandler.getLJDiagnostics(path);
65-
List<PublishDiagnosticsParams> nativeDiagnostics = LJDiagnosticsHandler.getNativeDiagnostics(ljDiagnostics, uri);
66-
nativeDiagnostics.forEach(params -> {
67-
this.client.publishDiagnostics(params);
68-
});
69-
List<LJDiagnostic> diagnostics = Stream.concat(ljDiagnostics.errors().stream(), ljDiagnostics.warnings().stream()).collect(Collectors.toList());
70-
sendDiagnosticsNotification(diagnostics);
71-
this.client.sendContext(ContextHistoryConverter.convertToDTO(ContextHistory.getInstance()));
67+
clearPublishedDiagnostics(uri);
68+
69+
try {
70+
LJDiagnostics ljDiagnostics = LJDiagnosticsHandler.getLJDiagnostics(path);
71+
List<PublishDiagnosticsParams> nativeDiagnostics = LJDiagnosticsHandler.getNativeDiagnostics(ljDiagnostics, uri);
72+
nativeDiagnostics.forEach(params -> {
73+
this.client.publishDiagnostics(params);
74+
if (!params.getDiagnostics().isEmpty()) {
75+
publishedDiagnosticUris.add(params.getUri());
76+
}
77+
});
78+
List<LJDiagnostic> diagnostics = Stream.concat(ljDiagnostics.errors().stream(), ljDiagnostics.warnings().stream()).collect(Collectors.toList());
79+
sendDiagnosticsNotification(diagnostics);
80+
this.client.sendContext(ContextHistoryConverter.convertToDTO(ContextHistory.getInstance()));
81+
} catch (Exception e) {
82+
System.err.println("LiquidJava verification crashed while checking: " + path);
83+
e.printStackTrace(System.err);
84+
clearPublishedDiagnostics(uri);
85+
this.client.sendFailure();
86+
}
7287
}
7388

7489
/**
@@ -93,10 +108,18 @@ public void shutdown() {
93108
*/
94109
public void clearDiagnostic(String uri) {
95110
this.client.publishDiagnostics(LJDiagnosticsHandler.getEmptyDiagnostics(uri));
111+
publishedDiagnosticUris.remove(uri);
96112
// TODO: fix consistency between native and custom diagnostics
97113
// sendDiagnosticsNotification(List.of());
98114
}
99115

116+
private void clearPublishedDiagnostics(String uri) {
117+
Set<String> urisToClear = new HashSet<>(publishedDiagnosticUris);
118+
urisToClear.add(uri);
119+
urisToClear.forEach(clearUri -> this.client.publishDiagnostics(LJDiagnosticsHandler.getEmptyDiagnostics(clearUri)));
120+
publishedDiagnosticUris.clear();
121+
}
122+
100123
/**
101124
* Checks diagnostics when a document is opened
102125
* @param params

0 commit comments

Comments
 (0)