diff --git a/server/src/errors.ts b/server/src/errors.ts new file mode 100644 index 0000000..102ee7b --- /dev/null +++ b/server/src/errors.ts @@ -0,0 +1,13 @@ +class FStarError extends Error { + constructor(message: string) { + super(message); + this.name = "FStarError"; + } +} + +class UnsupportedError extends Error { + constructor(message: string) { + super(message); + this.name = "UnsupportedError"; + } +} diff --git a/server/src/fstar.ts b/server/src/fstar.ts index 0c60835..e929bda 100644 --- a/server/src/fstar.ts +++ b/server/src/fstar.ts @@ -19,6 +19,7 @@ import path = require('path'); import { fstarVSCodeAssistantSettings } from './settings'; import { ClientConnection } from './client_connection'; import { checkFileInDirectory, findFilesByExtension, getEnclosingDirectories } from './utils'; +import { Ok, Result } from './result'; // FStar executable export class FStar { @@ -36,13 +37,12 @@ export class FStar { } // Tries to spawn an fstar.exe process using the given configuration and - // `textDocument` file. - static trySpawnFstar(config: FStarConfig, textDocument: TextDocument, configurationSettings: fstarVSCodeAssistantSettings, connection: ClientConnection, lax?: 'lax'): FStar | undefined { + // filePath. + static trySpawnFstar(config: FStarConfig, filePath: URI, debug: boolean, lax?: 'lax'): Result { // F* is assumed to support full-buffers unless it sends a message indicating otherwise const supportsFullBuffer = true; // Construct the options for fstar.exe - const filePath = URI.parse(textDocument.uri); const options = ["--ide", filePath.fsPath]; if (lax) { @@ -63,7 +63,7 @@ export class FStar { if (!config.cwd) { config.cwd = path.dirname(filePath.fsPath); } - if (configurationSettings.debug) { + if (debug) { console.log("Spawning fstar with options: " + options); } @@ -73,8 +73,7 @@ export class FStar { const fstar_exe_path = which.sync(config.fstar_exe); } catch (err) { - connection.sendAlert({ message: "Failed to find fstar.exe in path: " + err, uri: textDocument.uri }); - return undefined; + return new Error("Failed to find fstar.exe in path: " + err); } const proc = cp.spawn( @@ -83,14 +82,15 @@ export class FStar { { cwd: config.cwd } ); - return new FStar(proc, config, supportsFullBuffer, !!lax); + return new Ok(new FStar(proc, config, supportsFullBuffer, !!lax)); } // Dynamically loads the FStarConfiguration for a given file `textDocument` // before attempting to launch an instance of F*. - static fromInferredConfig(textDocument: TextDocument, workspaceFolders: WorkspaceFolder[], connection: ClientConnection, configurationSettings: fstarVSCodeAssistantSettings, lax?: 'lax'): FStar | undefined { + static fromInferredConfig(textDocument: TextDocument, workspaceFolders: WorkspaceFolder[], connection: ClientConnection, configurationSettings: fstarVSCodeAssistantSettings, lax?: 'lax'): Result { const config = this.getFStarConfig(textDocument, workspaceFolders, connection, configurationSettings); - return this.trySpawnFstar(config, textDocument, configurationSettings, connection, lax); + const filePath = URI.parse(textDocument.uri); + return this.trySpawnFstar(config, filePath, configurationSettings.debug, lax); } killZ3SubProcess(configurationSettings: fstarVSCodeAssistantSettings) { @@ -201,7 +201,7 @@ export class FStar { } // The type of an .fst.config.json file -interface FStarConfig { +export interface FStarConfig { include_dirs?: string[]; // --include paths options?: string[]; // other options to be passed to fstar.exe fstar_exe?: string; // path to fstar.exe diff --git a/server/src/fstar_connection.ts b/server/src/fstar_connection.ts new file mode 100644 index 0000000..6fae164 --- /dev/null +++ b/server/src/fstar_connection.ts @@ -0,0 +1,259 @@ +import { + Position +} from 'vscode-languageserver/node'; + +import { + URI +} from 'vscode-uri'; + +import { FStar, FStarConfig } from './fstar'; +import { Ok, Result } from './result'; + + +export class FStarConnection { + last_query_id: number; + fstar: FStar; + + constructor(fstar: FStar) { + // F*'s IDE protocol requires that each request have a unique query-id. + // We use a monotonic id. + this.last_query_id = 0; + this.fstar = fstar; + this.fstar.proc.stdin?.setDefaultEncoding('utf-8'); + } + + // Attempts to spawn an F* process, using the given configuration and filePath, and create a connection to it. + static tryCreateFStarConnection(fstarConfig: FStarConfig, filePath: URI, debug: boolean, lax?: 'lax') : Result { + const fstar = FStar.trySpawnFstar(fstarConfig, filePath, debug, lax); + if (fstar instanceof Ok) { + return new Ok(new FStarConnection(fstar.value)); + } + else { + return fstar; + } + } + + // Kills the F* process and closes the connection + close() { + this.fstar.proc.kill(); + } + + // Register an event handler on the F* process. Supports the special event + // 'message' which triggers on each valid F* message, as well as any event + // supported by a NodeJS `Stream`. + on(stream: 'stdout' | 'stderr' | 'stdin', event: string, handler: (...args:any[]) => void) { + let fstar_stream; + if (stream === 'stdout') { + fstar_stream = this.fstar.proc.stdout; + } else if (stream === 'stderr') { + fstar_stream = this.fstar.proc.stderr; + } else if (stream === 'stdin') { + fstar_stream = this.fstar.proc.stdin; + } + + // Add a higher-level message handler that will invoke the handler on + // each valid F* message. The message handler incorporates buffering to + // handle fragmented messages. + if (event === 'message') { + const messageHandler = FStarConnection.bufferedMessageHandlerFactory(handler); + fstar_stream?.on('data', messageHandler); + } else { + // Otherwise passes the event handler through to the stream + fstar_stream?.on(event, handler); + } + + } + + // All messages from F* are expected to be valid JSON objects. + // + // TODO(klinvill): this should likely be refactored into `fstar_messages.ts` and + // should check the structure of a message, not just that it's valid JSON. A + // better method could return either the appropriate message object, or an error + // otherwise, so that the parsing could be moved out of these handlers and into + // the same file as the message definitions. + private static is_valid_fstar_message(entry: string): boolean { + try { + JSON.parse(entry); + return true; + } + catch (err) { + return false; + } + } + + // Returns a message handler meant to run on top of a `Stream`'s 'data' + // handler. This handler will buffer received data to handle fragmented + // messages. It will invoke the given `handler` on each received valid F* + // message. + // + // Note that this function is created as a closure to keep the buffer scoped + // only to this function. The factory function exists to make unit-testing + // easier (creating a new function is like resetting the closure state). + static bufferedMessageHandlerFactory(handler: (message: string) => void) { + // TODO(klinvill): Gabriel suggests removing fragmentation (if another + // solution can be found). + // + // Stateful buffer to store partial messages. Messages appear to be + // fragmented into 8192 byte chunks if they exceed this size. + let buffer = ""; + + return function (data: string) { + const lines = data.toString().split('\n'); + + const valid_lines: string[] = []; + for (const line of lines) { + if (FStarConnection.is_valid_fstar_message(line)) { + // We assume that fragmented messages will always be read + // sequentially. This is a reasonable assumption to make since + // messages should be delivered over a local IO stream (which is + // FIFO and provides reliable delivery) from a single-threaded + // F* IDE process. Because of this assumption, receiving a + // non-fragmented message while the buffer is non-empty implies + // that some error occured before the process could finish + // sending a message, so the buffer is discarded. + if (buffer !== "") { + console.error("Partially buffered message discarded: " + buffer); + } + buffer = ""; + valid_lines.push(line); + } else { + // We assume that invalid messages are just message fragments. + // We therefore add this fragment to the buffer until the full + // message is received. + buffer += line; + // The message fragment we received may be the last fragment + // needed to complete a message. We therefore check here to see + // if the buffer constitutes a valid message. + if (FStarConnection.is_valid_fstar_message(buffer)) { + valid_lines.push(buffer); + buffer = ""; + } + } + } + + // Invoke the message handler for each received message in-order. + valid_lines.forEach(message => handler(message)); + }; + } + + // Utilities to send messages to an F* process. Sending a request wraps the + // request with a fresh query-id. + sendRequest(msg: any, debug: boolean) : Result { + const qid = this.last_query_id; + this.last_query_id = qid + 1; + msg["query-id"] = '' + (qid + 1); + const text = JSON.stringify(msg); + if (debug) { + console.log(">>> " + text); + } + if (this.fstar.proc.exitCode != null) { + const process_name = this.fstar.lax ? "flycheck" : "checker"; + const error_msg = "ERROR: F* " + process_name + " process exited with code " + this.fstar.proc.exitCode; + return new FStarError(error_msg); + } + else { + try { + this.fstar.proc?.stdin?.write(text); + this.fstar.proc?.stdin?.write("\n"); + return new Ok(undefined); + } catch (e) { + const msg = "ERROR: Error writing to F* process: " + e; + return new Error(msg); + } + } + } + + sendFullBufferRequest(code: string, kind: 'full' | 'lax' | 'cache' | 'reload-deps', withSymbols: boolean, debug: boolean) : Result { + if (!this.fstar.supportsFullBuffer) { + return new UnsupportedError("ERROR: F* process does not support full-buffer queries"); + } + const push_context: FullBufferQuery = { + query: "full-buffer", + args: { + kind, + "with-symbols": withSymbols, + code: code, + line: 0, + column: 0 + } + }; + return this.sendRequest(push_context, debug); + } + + sendPartialBufferRequest(code: string, kind: 'verify-to-position' | 'lax-to-position', position: { line: number, column: number }, debug: boolean) : Result { + if (!this.fstar.supportsFullBuffer) { + return new UnsupportedError("ERROR: F* process does not support full-buffer queries"); + } + const push_context: FullBufferQuery = { + query: "full-buffer", + args: { + kind, + "with-symbols": false, + code: code, + line: 0, + column: 0, + "to-position": position + } + }; + return this.sendRequest(push_context, debug); + } + + sendLookupQuery(filePath: string, position: Position, word: string, range: FStarRange, debug: boolean) : Result { + const query: LookupQuery = { + query: "lookup", + args: { + context: "code", + symbol: word, + "requested-info": ["type", "documentation", "defined-at"], + location: { + filename: filePath, + line: position.line + 1, + column: position.character + }, + "symbol-range": range + } + }; + return this.sendRequest(query, debug); + } + + sendVfsAddRequest(filePath: string, contents: string, debug: boolean) : Result { + const query: VfsAdd = { + query: "vfs-add", + args: { + filename: filePath, + contents: contents + } + }; + return this.sendRequest(query, debug); + } + + sendAutocompleteRequest(word: string, debug: boolean) : Result { + const query: AutocompleteRequest = { + "query": "autocomplete", + "args": { + "partial-symbol": word, + "context": "code" + } + }; + return this.sendRequest(query, debug); + } + + sendCancelRequest(range: { line: number; character: number }, debug: boolean) : Result { + const query: CancelRequest = { + query: "cancel", + args: { + "cancel-line": range.line + 1, + "cancel-column": range.character + } + }; + return this.sendRequest(query, debug); + } + + sendRestartSolverRequest(debug: boolean) : Result { + const query = { + query: "restart-solver", + args: {} + }; + return this.sendRequest(query, debug); + } +} diff --git a/server/src/fstar_handlers.ts b/server/src/fstar_handlers.ts index 917f56b..ff92aa1 100644 --- a/server/src/fstar_handlers.ts +++ b/server/src/fstar_handlers.ts @@ -11,9 +11,8 @@ import { import * as crypto from 'crypto'; -import { fstarVSCodeAssistantSettings } from './settings'; import { Server } from './server'; -import { ClientConnection, StatusOkMessage, ok_kind } from './client_connection'; +import { StatusOkMessage, ok_kind } from './client_connection'; import { mkPosition, fstarRangeAsRange, qualifyFilename } from './utils'; // Cyclic dependency to support mocking out functions within this module when @@ -25,92 +24,20 @@ import * as fstar_handlers from './fstar_handlers'; // Handling responses from the F* IDE protocol /////////////////////////////////////////////////////////////////////////////////// -// All messages from F* are expected to be valid JSON objects. -// -// TODO(klinvill): this should likely be refactored into `fstar_messages.ts` and -// should check the structure of a message, not just that it's valid JSON. A -// better method could return either the appropriate message object, or an error -// otherwise, so that the parsing could be moved out of these handlers and into -// the same file as the message definitions. -function is_valid_fstar_message(entry: string): boolean { - try { - JSON.parse(entry); - return true; - } - catch (err) { - return false; - } -} - -// Event handler for stdout on fstar_ide. Created as a closure to keep the -// buffer scoped only to this function. The factory function exists to make -// unit-testing easier (creating a new function is like resetting the closure -// state). -// // The server parameter is passed freshly with every request to avoid potential // rebinding errors in the future. Furthermore, server is passed instead of // configurationSettings (which is also stored on the server instance) to avoid // accidentally closing over stale configurationSettings arguments when this // function is called (since they can be rebound within the server). -export function handleFStarResponseForDocumentFactory(): ((textDocument: TextDocument, data: string, lax: boolean, server: Server) => void) { - // TODO(klinvill): fragmentation code should probably be refactored into a - // separate method, or removed as per Gabriel's suggestion (if another - // solution can be found). - // - // Stateful buffer to store partial messages. Messages appear to be - // fragmented into 8192 byte chunks if they exceed this size. - let buffer = ""; - - return function (textDocument: TextDocument, data: string, lax: boolean, server: Server) { - if (server.configurationSettings.debug) { - console.log("<<< " + (lax ? "lax" : "") + "uri:<" + textDocument.uri + ">:" + data); - } - const lines = data.toString().split('\n'); - - const valid_lines: string[] = []; - for (const line of lines) { - if (is_valid_fstar_message(line)) { - // We assume that fragmented messages will always be read - // sequentially. This is a reasonable assumption to make since - // messages should be delivered over a local IO stream (which is - // FIFO and provides reliable delivery) from a single-threaded - // F* IDE process. Because of this assumption, receiving a - // non-fragmented message while the buffer is non-empty implies - // that some error occured before the process could finish - // sending a message, so the buffer is discarded. - if (buffer !== "") { - console.error("Partially buffered message discarded: " + buffer); - } - buffer = ""; - valid_lines.push(line); - } else { - // We assume that invalid messages are just message fragments. - // We therefore add this fragment to the buffer until the full - // message is received. - buffer += line; - // The message fragment we received may be the last fragment - // needed to complete a message. We therefore check here to see - // if the buffer constitutes a valid message. - if (is_valid_fstar_message(buffer)) { - valid_lines.push(buffer); - buffer = ""; - } - } - } - - // Cyclic dependency on handleOneResponseForDocument to support mocking - // out the function when testing. Suggested as a solution in this post: - // https://stackoverflow.com/questions/51269431/jest-mock-inner-function - valid_lines.forEach(line => { fstar_handlers.handleOneResponseForDocument(textDocument, line, lax, server); }); - }; -} +export function handleFStarMessageForDocument(textDocument: TextDocument, message: string, lax: boolean, server: Server) { + if (server.configurationSettings.debug) { + console.log("<<< " + (lax ? "lax" : "") + "uri:<" + textDocument.uri + ">:" + message); + } -// Main event dispatch for F* IDE responses. -export function handleOneResponseForDocument(textDocument: TextDocument, data: string, lax: boolean, server: Server) { - if (data == "") { return; } + if (message == "") { return; } let r: IdeResponse; try { - r = JSON.parse(data); + r = JSON.parse(message); } catch (err) { console.error("Error parsing response: " + err); @@ -174,10 +101,10 @@ function handleIdeProtocolInfo(textDocument: TextDocument, pi: ProtocolInfo, ser // Both fstar and fstar_lax have their own supportsFullBuffer flag, we // set both of them here assuming that they both have the same support // for full-buffer queries. - const fstar = server.getFStar(textDocument); - const fstar_lax = server.getFStar(textDocument, 'lax'); - if (fstar) { fstar.supportsFullBuffer = false; } - if (fstar_lax) { fstar_lax.supportsFullBuffer = false; } + const fstar_conn = server.getFStarConnection(textDocument); + const fstar_lax_conn = server.getFStarConnection(textDocument, 'lax'); + if (fstar_conn) { fstar_conn.fstar.supportsFullBuffer = false; } + if (fstar_lax_conn) { fstar_lax_conn.fstar.supportsFullBuffer = false; } console.error("fstar.exe does not support full-buffer queries."); } } diff --git a/server/src/result.ts b/server/src/result.ts new file mode 100644 index 0000000..e1a0b61 --- /dev/null +++ b/server/src/result.ts @@ -0,0 +1,9 @@ +/// Basic Result type similar to Rust +export type Result = Ok | E; + +export class Ok { + value: T; + constructor(value: T) { + this.value = value; + } +} diff --git a/server/src/server.ts b/server/src/server.ts index 0f88c3c..539775e 100644 --- a/server/src/server.ts +++ b/server/src/server.ts @@ -33,7 +33,8 @@ import { defaultSettings, fstarVSCodeAssistantSettings } from './settings'; import { formatIdeProofState, formatIdeSymbol, fstarRangeAsRange, mkPosition, qualifyFilename, rangeAsFStarRange } from './utils'; import { AlertMessage, ClientConnection } from './client_connection'; import { FStar } from './fstar'; -import { handleFStarResponseForDocumentFactory } from './fstar_handlers'; +import { FStarConnection } from './fstar_connection'; +import { handleFStarMessageForDocument } from './fstar_handlers'; // LSP Server // @@ -99,7 +100,7 @@ export class Server { // Only keep settings for open documents this.documents.onDidClose(e => { - this.killFStarProcessesForDocument(e.document); + this.closeFStarProcessesForDocument(e.document); // Clear all diagnostics for a document when it is closed this.connection.sendDiagnostics({ uri: e.document.uri, @@ -238,59 +239,46 @@ export class Server { } } - // Some utilities to send messages to fstar_ide or fstar_lax_ide - // Sending a request to either fstar_ide or fstar_lax_ide - // Wraps the request with a fresh query-id - sendRequestForDocument(textDocument: TextDocument, msg: any, lax?: 'lax') { + // Some utilities to send requests to and handle errors from fstar_ide or + // fstar_lax_ide. + handleFStarError(uri: string, doc_state: DocumentState, err: FStarError | Error, lax?: 'lax') { + // F* process exited with some error code + if (err instanceof FStarError) { + // Only alert once per process + if (lax) { + if (doc_state.alerted_fstar_lax_process_exited) { return; } + doc_state.alerted_fstar_lax_process_exited = true; + } + else { + if (doc_state.alerted_fstar_process_exited) { return; } + doc_state.alerted_fstar_process_exited = true; + } + const msg: AlertMessage = { + uri: uri, + message: err.message + }; + console.error(msg); + this.connection.sendAlert(msg); + } + // Catch-all for other errors + else if (err instanceof Error) { + console.error(err); + this.connection.sendAlert({ uri: uri, message: err.message }); + } + } + + sendFStarRequestForDocument(textDocument: TextDocument, msg: any, lax?: 'lax') { const doc_state = this.getDocumentState(textDocument.uri); if (!doc_state) { return; } - const fstar = this.getFStar(textDocument, lax); - if (!fstar) { + const fstar_conn = this.getFStarConnection(textDocument, lax); + if (!fstar_conn) { return; } - else { - const qid = doc_state.last_query_id; - doc_state.last_query_id = qid + 1; - msg["query-id"] = '' + (qid + 1); - const text = JSON.stringify(msg); - if (this.configurationSettings.debug) { - console.log(">>> " + text); - } - if (fstar.proc.exitCode != null) { - if (lax) { - if (doc_state.alerted_fstar_lax_process_exited) { return; } - doc_state.alerted_fstar_lax_process_exited = true; - const msg: AlertMessage = { - uri: textDocument.uri, - message: "ERROR: F* flycheck process exited with code " + fstar.proc.exitCode - }; - this.connection.sendAlert(msg); - console.error(msg); - } - else { - if (doc_state.alerted_fstar_process_exited) { return; } - doc_state.alerted_fstar_process_exited = true; - const msg: AlertMessage = { - uri: textDocument.uri, - message: "ERROR: F* checker process exited with code " + fstar.proc.exitCode - }; - this.connection.sendAlert(msg); - console.error(msg); - } - return; - } - else { - try { - fstar.proc?.stdin?.write(text); - fstar.proc?.stdin?.write("\n"); - } catch (e) { - const msg = "ERROR: Error writing to F* process: " + e; - console.error(msg); - this.connection.sendAlert({ uri: textDocument.uri, message: msg }); - } - } + const result = fstar_conn.sendRequest(msg, this.configurationSettings.debug); + if (result instanceof Error) { + this.handleFStarError(textDocument.uri, doc_state, result, lax); } } @@ -310,29 +298,39 @@ export class Server { const ranges = [Range.create(mkPosition([0, 0]), mkPosition([textDocument.lineCount, 0]))]; if (kind == "full") { this.connection.sendStatusStarted({ uri: textDocument.uri, ranges: ranges }); } } - const fstar = this.getFStar(textDocument, lax); - if (fstar?.supportsFullBuffer) { - const push_context: FullBufferQuery = { - query: "full-buffer", - args: { - kind, - "with-symbols": withSymbols, - code: textDocument.getText(), - line: 0, - column: 0 - } - }; - this.sendRequestForDocument(textDocument, push_context, lax); + const fstar_conn = this.getFStarConnection(textDocument, lax); + const result = fstar_conn?.sendFullBufferRequest(textDocument.getText(), kind, withSymbols, this.configurationSettings.debug); + if (result instanceof UnsupportedError) { + // Ignore the error if the process doesn't support full-buffer + // queries. + // + // TODO(klinvill): Is this really the desired behavior? Shouldn't we + // surface some kind of warning message instead of silently + // suppressing full-buffer requests? + return; + } else if (result instanceof Error) { + const doc_state = this.getDocumentState(textDocument.uri); + if (!doc_state) { + // TODO(klinvill): This preserves the previous behavior of calling `sendFStarRequestForDocument` (which just returns if the document state can't be retrieved), but also suppresses some errors. Is this really the desired behavior? + return; + } + this.handleFStarError(textDocument.uri, doc_state, result, lax); } } validateFStarDocumentToPosition(textDocument: TextDocument, kind: 'verify-to-position' | 'lax-to-position', position: { line: number, column: number }) { + // TODO(klinvill): should `pendingChangeEvents` also be cleared on `validateFStarDocument`? this.pendingChangeEvents = []; // Clear pending change events, since we're checking it now // console.log("ValidateFStarDocumentToPosition( " + textDocument.uri + ", " + kind); this.connection.sendClearDiagnostics({ uri: textDocument.uri }); // If this is non-lax requests, send a status clear messages to VSCode - // to clear the gutter icons and error squiggles - // They will be reported again if the document is not verified + // to clear the gutter icons and error squiggles They will be reported + // again if the document is not verified + // + // TODO(klinvill): in `validateFStarDocument` this is done only for + // non-lax requests. Should a similar check be done here? The previous + // implementation of `validateFStarDocumentToPosition` implies that this + // function will never be called for lax requests. Is that true? const doc_state = this.getDocumentState(textDocument.uri); if (doc_state) { doc_state.prefix_stale = false; @@ -340,20 +338,24 @@ export class Server { this.connection.sendStatusClear({ uri: textDocument.uri }); const ranges = [Range.create(mkPosition([0, 0]), mkPosition([position.line, 0]))]; this.connection.sendStatusStarted({ uri: textDocument.uri, ranges: ranges }); - const fstar = this.getFStar(textDocument); - if (fstar && fstar.supportsFullBuffer) { - const push_context: FullBufferQuery = { - query: "full-buffer", - args: { - kind: kind, - "with-symbols": false, - code: textDocument.getText(), - line: 0, - column: 0, - "to-position": position - } - }; - this.sendRequestForDocument(textDocument, push_context); + + const fstar_conn = this.getFStarConnection(textDocument); + const result = fstar_conn?.sendPartialBufferRequest(textDocument.getText(), kind, position, this.configurationSettings.debug); + if (result instanceof UnsupportedError) { + // Ignore the error if the process doesn't support full-buffer + // queries. + // + // TODO(klinvill): Is this really the desired behavior? Shouldn't we + // surface some kind of warning message instead of silently + // suppressing full-buffer requests? + return; + } else if (result instanceof Error) { + const doc_state = this.getDocumentState(textDocument.uri); + if (!doc_state) { + // TODO(klinvill): This preserves the previous behavior of calling `sendFStarRequestForDocument` (which just returns if the document state can't be retrieved), but also suppresses some errors. Is this really the desired behavior? + return; + } + this.handleFStarError(textDocument.uri, doc_state, result); } } @@ -362,21 +364,16 @@ export class Server { requestSymbolInfo(textDocument: TextDocument, position: Position, wordAndRange: WordAndRange): void { const uri = textDocument.uri; const filePath = URI.parse(uri).fsPath; - const query: LookupQuery = { - query: "lookup", - args: { - context: "code", - symbol: wordAndRange.word, - "requested-info": ["type", "documentation", "defined-at"], - location: { - filename: filePath, - line: position.line + 1, - column: position.character - }, - "symbol-range": wordAndRange.range + const fstar_conn = this.getFStarConnection(textDocument, this.configurationSettings.flyCheck ? 'lax' : undefined); + const result = fstar_conn?.sendLookupQuery(filePath, position, wordAndRange.word, wordAndRange.range, this.configurationSettings.debug); + if (result instanceof Error) { + const doc_state = this.getDocumentState(textDocument.uri); + if (!doc_state) { + // TODO(klinvill): This preserves the previous behavior of calling `sendFStarRequestForDocument` (which just returns if the document state can't be retrieved), but also suppresses some errors. Is this really the desired behavior? + return; } - }; - this.sendRequestForDocument(textDocument, query, this.configurationSettings.flyCheck ? 'lax' : undefined); + this.handleFStarError(textDocument.uri, doc_state, result); + } } @@ -400,22 +397,22 @@ export class Server { }; } - killFStarProcessesForDocument(textDocument: TextDocument) { + closeFStarProcessesForDocument(textDocument: TextDocument) { const docState = this.getDocumentState(textDocument.uri); if (!docState) return; - docState.fstar.proc.kill(); - docState.fstar_lax.proc.kill(); + docState.fstar_connection.close(); + docState.fstar_lax_connection.close(); this.documentStates.delete(textDocument.uri); } - // Get the FStar instance for the given document - getFStar(textDocument: TextDocument, lax?: 'lax'): FStar | undefined { + // Get the F* connection for the given document + getFStarConnection(textDocument: TextDocument, lax?: 'lax'): FStarConnection | undefined { const uri = textDocument.uri; const doc_state = this.getDocumentState(uri); if (lax) { - return doc_state?.fstar_lax; + return doc_state?.fstar_lax_connection; } else { - return doc_state?.fstar; + return doc_state?.fstar_connection; } } @@ -446,21 +443,28 @@ export class Server { } async refreshDocumentState(textDocument: TextDocument) { - const fstar = FStar.fromInferredConfig(textDocument, this.workspaceFolders, this.connection, this.configurationSettings); + const fstar_config = FStar.getFStarConfig(textDocument, this.workspaceFolders, this.connection, this.configurationSettings); + + const fstar_conn = FStarConnection.tryCreateFStarConnection(fstar_config, URI.parse(textDocument.uri), this.configurationSettings.debug); // Failed to start F* - if (!fstar) { return; } + if (fstar_conn instanceof Error) { + this.connection.sendAlert({message: fstar_conn.message, uri: textDocument.uri}); + return; + } - // We can just re-use the configuration used for the non-lax F* instance. - const fstar_lax = FStar.trySpawnFstar(fstar.config, textDocument, this.configurationSettings, this.connection, 'lax'); + const fstar_lax_conn = FStarConnection.tryCreateFStarConnection(fstar_config, URI.parse(textDocument.uri), this.configurationSettings.debug, 'lax'); // Failed to start F* lax - if (!fstar_lax) { return; } + if (fstar_lax_conn instanceof Error) { + this.connection.sendAlert({message: fstar_lax_conn.message, uri: textDocument.uri}); + return; + } // Initialize the document state for this doc this.documentStates.set(textDocument.uri, { - fstar: fstar, + fstar_connection: fstar_conn.value, alerted_fstar_process_exited: false, fstar_diagnostics: [], - fstar_lax: fstar_lax, + fstar_lax_connection: fstar_lax_conn.value, alerted_fstar_lax_process_exited: false, fstar_lax_diagnostics: [], last_query_id: 0, @@ -470,21 +474,34 @@ export class Server { prefix_stale: false, }); - // Set the event handlers for the fstar processes - const handleFStarResponseForDocument = handleFStarResponseForDocumentFactory(); - - fstar.proc.stdin?.setDefaultEncoding('utf-8'); - fstar.proc.stdout?.on('data', (data) => { handleFStarResponseForDocument(textDocument, data, false, this); }); - fstar.proc.stderr?.on('data', (data) => { console.error("fstar stderr: " + data); }); - fstar_lax.proc.stdin?.setDefaultEncoding('utf-8'); - fstar_lax.proc.stdout?.on('data', (data) => { handleFStarResponseForDocument(textDocument, data, true, this); }); - fstar_lax.proc.stderr?.on('data', (data) => { console.error("fstar lax stderr: " + data); }); + // Set the event handlers for the fstar processes. + // + // We use the higher-level message handler exposed by `FStarConnection` + // for the stdout streams. This handler takes care of buffering messages + // and will invoke the handler once for each received valid F* message. + fstar_conn.value.on('stdout', 'message', (message) => { handleFStarMessageForDocument(textDocument, message, false, this); }); + fstar_conn.value.on('stderr','data', (data) => { console.error("fstar stderr: " + data); }); + fstar_lax_conn.value.on('stdout', 'message', (message) => { handleFStarMessageForDocument(textDocument, message, true, this); }); + fstar_lax_conn.value.on('stderr','data', (data) => { console.error("fstar lax stderr: " + data); }); // Send the initial dummy vfs-add request to the fstar processes - const filePath = URI.parse(textDocument.uri); - const vfs_add: VfsAdd = { "query": "vfs-add", "args": { "filename": filePath.fsPath, "contents": textDocument.getText() } }; - this.sendRequestForDocument(textDocument, vfs_add); - this.sendRequestForDocument(textDocument, vfs_add, 'lax'); + const filePath = URI.parse(textDocument.uri).fsPath; + const contents = textDocument.getText(); + const doc_state = this.getDocumentState(textDocument.uri); + // We should never fail to retrieve the document state since it was just set + if (!doc_state) { + console.error("Unable to retrieve document state after just setting it. This should never happen. Occured for document: " + textDocument.uri); + return; + } + + const result = fstar_conn.value.sendVfsAddRequest(filePath, contents, this.configurationSettings.debug); + if (result instanceof Error) { + this.handleFStarError(textDocument.uri, doc_state, result); + } + const lax_result = fstar_lax_conn.value.sendVfsAddRequest(filePath, contents, this.configurationSettings.debug); + if (lax_result instanceof Error) { + this.handleFStarError(textDocument.uri, doc_state, lax_result, 'lax'); + } } // Initialization of the LSP server: Called once when the workspace is opened @@ -588,14 +605,16 @@ export class Server { const wordAndRange = autoCompleteResponses.wordAndRange; // Don't send requests for very short words if (wordAndRange.word.length < 2) return []; - const autoCompletionRequest: AutocompleteRequest = { - "query": "autocomplete", - "args": { - "partial-symbol": wordAndRange.word, - "context": "code" + const lax = this.configurationSettings.flyCheck ? "lax" : undefined; + const fstar_conn = this.getFStarConnection(doc, lax); + + const doc_state = this.getDocumentState(doc.uri); + if (doc_state) { + const result = fstar_conn?.sendAutocompleteRequest(wordAndRange.word, this.configurationSettings.debug); + if (result instanceof Error) { + this.handleFStarError(doc.uri, doc_state, result, lax); } - }; - this.sendRequestForDocument(doc, autoCompletionRequest, this.configurationSettings.flyCheck ? "lax" : undefined); + } } const items: CompletionItem[] = []; bestMatch.value.forEach((response) => { @@ -740,7 +759,7 @@ export class Server { private async onRestartHandler(textDocument?: TextDocument) { if (!textDocument) { return; } - this.killFStarProcessesForDocument(textDocument); + this.closeFStarProcessesForDocument(textDocument); await this.refreshDocumentState(textDocument); this.connection.sendStatusClear({ uri: textDocument.uri }); // And ask the lax fstar process to verify it @@ -754,14 +773,18 @@ export class Server { const range: { line: number; character: number }[] = params[1]; const textDocument = this.getDocument(uri); if (!textDocument) { return; } - const cancelRequest: CancelRequest = { - query: "cancel", - args: { - "cancel-line": range[0].line + 1, - "cancel-column": range[0].character + // TODO(klinvill): It looks like this function can only be called for + // non-lax checking. Is that correct? + const fstar_conn = this.getFStarConnection(textDocument); + const result = fstar_conn?.sendCancelRequest(range[0], this.configurationSettings.debug); + if (result instanceof Error) { + const doc_state = this.getDocumentState(textDocument.uri); + if (!doc_state) { + // TODO(klinvill): This preserves the previous behavior of calling `sendFStarRequestForDocument` (which just returns if the document state can't be retrieved), but also suppresses some errors. Is this really the desired behavior? + return; } - }; - this.sendRequestForDocument(textDocument, cancelRequest); + this.handleFStarError(textDocument.uri, doc_state, result); + } } private onKillAndRestartSolverRequest(uri: any) { @@ -769,13 +792,16 @@ export class Server { if (!textDocument) { return; } const documentState = this.getDocumentState(textDocument.uri); if (!documentState) { return; } - const fstar = documentState.fstar; + const fstar_conn = documentState.fstar_connection; - fstar.killZ3SubProcess(this.configurationSettings); + fstar_conn.fstar.killZ3SubProcess(this.configurationSettings); // Wait for a second for processes to die before restarting the solver setTimeout(() => { - this.sendRequestForDocument(textDocument, { query: "restart-solver", args: {} }); + const result = fstar_conn.sendRestartSolverRequest(this.configurationSettings.debug); + if (result instanceof Error) { + this.handleFStarError(textDocument.uri, documentState, result); + } }, 1000); } @@ -783,7 +809,7 @@ export class Server { this.documentStates.forEach((docState, uri) => { const textDoc = this.getDocument(uri); if (!textDoc) { return; } - this.killFStarProcessesForDocument(textDoc); + this.closeFStarProcessesForDocument(textDoc); }); return; } @@ -796,12 +822,12 @@ export class Server { interface DocumentState { // The main fstar.exe process for verifying the current document - fstar: FStar; + fstar_connection: FStarConnection; alerted_fstar_process_exited: boolean; fstar_diagnostics: Diagnostic[]; // The fstar.exe process for quickly handling on-change events, symbol lookup etc - fstar_lax: FStar; + fstar_lax_connection: FStarConnection; alerted_fstar_lax_process_exited: boolean; fstar_lax_diagnostics: Diagnostic[]; diff --git a/server/src/utils.ts b/server/src/utils.ts index 04c2a13..766a995 100644 --- a/server/src/utils.ts +++ b/server/src/utils.ts @@ -36,8 +36,8 @@ export function qualifyFilename(fname: string, textdocUri: string, server: Serve if (fname != "") { // if we have a relative path, then qualify it to the base of the // F* process's cwd - if (!path.isAbsolute(fname) && doc_state && doc_state.fstar.config.cwd) { - const base = doc_state.fstar.config.cwd; + if (!path.isAbsolute(fname) && doc_state && doc_state.fstar_connection.fstar.config.cwd) { + const base = doc_state.fstar_connection.fstar.config.cwd; //concate the base and the relative path return pathToFileURL(path.join(base, fname)).toString(); } diff --git a/server/tests/fstar_connection.test.ts b/server/tests/fstar_connection.test.ts new file mode 100644 index 0000000..0f37612 --- /dev/null +++ b/server/tests/fstar_connection.test.ts @@ -0,0 +1,100 @@ +import { beforeEach, describe, expect, test, jest } from '@jest/globals'; + +import { FStarConnection } from '../src/fstar_connection'; + + +describe('bufferedMessageHandler tests', () => { + // The function we'll be testing, reset before each test + let bufferedMessageHandler: (msg: string) => void; + const mockHandler = jest.fn(); + + beforeEach(() => { + jest.clearAllMocks(); + + // Reset the function we're testing, this will create a fresh buffer. + bufferedMessageHandler = FStarConnection.bufferedMessageHandlerFactory(mockHandler); + }); + + test('test valid message', () => { + const valid_message = '{"kind": "message"}'; + + bufferedMessageHandler(valid_message); + // Valid messages are passed on for further handling + expect(mockHandler).toHaveBeenCalledTimes(1); + expect(mockHandler).toHaveBeenLastCalledWith(valid_message); + }); + + test('test fragmented message', () => { + const fragment_0 = '{"kind": "'; + const fragment_1 = 'message'; + const fragment_2 = '"}'; + + // Fragments are buffered until a full valid message is received, then it is + // passed on for further handling. + bufferedMessageHandler(fragment_0); + expect(mockHandler).toHaveBeenCalledTimes(0); + bufferedMessageHandler(fragment_1); + expect(mockHandler).toHaveBeenCalledTimes(0); + bufferedMessageHandler(fragment_2); + expect(mockHandler).toHaveBeenCalledTimes(1); + expect(mockHandler).toHaveBeenLastCalledWith(fragment_0 + fragment_1 + fragment_2); + }); + + test('test out-of-order fragmented messages are not handled', () => { + const fragment_0 = '{"kind": "'; + const fragment_1 = 'message'; + const fragment_2 = '"}'; + + // Fragments are assumed to be received in-order, so out-of-order + // fragments have undefined behavior. In this test case, no valid + // message can be collected. + bufferedMessageHandler(fragment_2); + expect(mockHandler).toHaveBeenCalledTimes(0); + bufferedMessageHandler(fragment_1); + expect(mockHandler).toHaveBeenCalledTimes(0); + bufferedMessageHandler(fragment_0); + expect(mockHandler).toHaveBeenCalledTimes(0); + }); + + test('test valid messages flush buffer', () => { + const valid_message = '{"kind": "message"}'; + const fragment_0 = '{"kind": "'; + const fragment_1 = 'message'; + const fragment_2 = '"}'; + + // Fragments are assumed to be received in-order and before other + // messages, so a valid message results in the buffer being flushed. + bufferedMessageHandler(valid_message); + expect(mockHandler).toHaveBeenCalledTimes(1); + expect(mockHandler).toHaveBeenLastCalledWith(valid_message); + + bufferedMessageHandler(fragment_0); + expect(mockHandler).toHaveBeenCalledTimes(1); + + bufferedMessageHandler(valid_message); + expect(mockHandler).toHaveBeenCalledTimes(2); + expect(mockHandler).toHaveBeenLastCalledWith(valid_message); + + bufferedMessageHandler(fragment_1); + expect(mockHandler).toHaveBeenCalledTimes(2); + bufferedMessageHandler(fragment_2); + expect(mockHandler).toHaveBeenCalledTimes(2); + + }); + + test('test combined messages and fragments processed separately', () => { + const valid_message = '{"kind": "message"}'; + const fragment_0 = '{"kind": "'; + const fragment_1 = 'message'; + const fragment_2 = '"}'; + + const combined_messages = [valid_message, fragment_0, fragment_1, fragment_2].join('\n'); + + // Messages that are separated by newlines should be processed just as + // if they were received as separate messages. + bufferedMessageHandler(combined_messages); + expect(mockHandler).toHaveBeenCalledTimes(2); + expect(mockHandler).toHaveBeenNthCalledWith(1, valid_message); + expect(mockHandler).toHaveBeenNthCalledWith(2, fragment_0 + fragment_1 + fragment_2); + }); +}); diff --git a/server/tests/fstar_handlers.test.ts b/server/tests/fstar_handlers.test.ts deleted file mode 100644 index 6bb857f..0000000 --- a/server/tests/fstar_handlers.test.ts +++ /dev/null @@ -1,127 +0,0 @@ -import { beforeEach, describe, expect, test, jest } from '@jest/globals'; - -import * as fstar_handlers from '../src/fstar_handlers'; -import { TextDocuments } from 'vscode-languageserver/node'; -import { TextDocument } from 'vscode-languageserver-textdocument'; -import { defaultSettings } from '../src/settings'; - -// Mocks -import { Server } from '../src/server'; -jest.mock('../src/server'); -import { ClientConnection } from '../src/client_connection'; -jest.mock('../src/client_connection'); - - -// Mocked objects to use in this test suite -// -// Note: jest.mocked() ensures that the mock is type-safe. See -// https://jestjs.io/docs/mock-function-api#jestmockedsource-options for more -// details. -const mockConnection = new (jest.mocked(ClientConnection))(); -const mockServer = new (jest.mocked(Server))(mockConnection, new TextDocuments(TextDocument)); - -beforeEach(() => { - jest.clearAllMocks(); - - // This test suite relies on being able to access configurationSettings. The - // mock sets configurationSettings to `undefined`, so we instead provide a - // default configuration for these tests. - mockServer.configurationSettings = defaultSettings; -}); - -describe('handleFStarResponseForDocument tests', () => { - // `handleFStarResponseForDocument` calls `handleOneResponseForDocument`. We - // therefore mock `handleOneResponseForDocument` out to simplify these - // tests. - const handleOneResponseForDocumentMock = jest.spyOn(fstar_handlers, 'handleOneResponseForDocument').mockReturnValue(undefined); - - // The function we'll be testing, complete with mocked dependencies - const handleFStarResponseForDocument = fstar_handlers.handleFStarResponseForDocumentFactory(); - - // Common test parameters - const td = TextDocument.create("test", "test", 0, "test"); - const lax = false; - - test('test valid message', () => { - const valid_message = '{"kind": "message"}'; - - handleFStarResponseForDocument(td, valid_message, lax, mockServer); - // Valid messages are passed on for further handling - expect(handleOneResponseForDocumentMock).toHaveBeenCalledTimes(1); - expect(handleOneResponseForDocumentMock).toHaveBeenLastCalledWith(td, valid_message, lax, mockServer); - }); - - test('test fragmented message', () => { - const fragment_0 = '{"kind": "'; - const fragment_1 = 'message'; - const fragment_2 = '"}'; - - // Fragments are buffered until a full valid message is received, then it is - // passed on for further handling. - handleFStarResponseForDocument(td, fragment_0, lax, mockServer); - expect(handleOneResponseForDocumentMock).toHaveBeenCalledTimes(0); - handleFStarResponseForDocument(td, fragment_1, lax, mockServer); - expect(handleOneResponseForDocumentMock).toHaveBeenCalledTimes(0); - handleFStarResponseForDocument(td, fragment_2, lax, mockServer); - expect(handleOneResponseForDocumentMock).toHaveBeenCalledTimes(1); - expect(handleOneResponseForDocumentMock).toHaveBeenLastCalledWith(td, fragment_0 + fragment_1 + fragment_2, lax, mockServer); - }); - - test('test out-of-order fragmented messages are not handled', () => { - const fragment_0 = '{"kind": "'; - const fragment_1 = 'message'; - const fragment_2 = '"}'; - - // Fragments are assumed to be received in-order, so out-of-order - // fragments have undefined behavior. In this test case, no valid - // message can be collected. - handleFStarResponseForDocument(td, fragment_2, lax, mockServer); - expect(handleOneResponseForDocumentMock).toHaveBeenCalledTimes(0); - handleFStarResponseForDocument(td, fragment_1, lax, mockServer); - expect(handleOneResponseForDocumentMock).toHaveBeenCalledTimes(0); - handleFStarResponseForDocument(td, fragment_0, lax, mockServer); - expect(handleOneResponseForDocumentMock).toHaveBeenCalledTimes(0); - }); - - test('test valid messages flush buffer', () => { - const valid_message = '{"kind": "message"}'; - const fragment_0 = '{"kind": "'; - const fragment_1 = 'message'; - const fragment_2 = '"}'; - - // Fragments are assumed to be received in-order and before other - // messages, so a valid message results in the buffer being flushed. - handleFStarResponseForDocument(td, valid_message, lax, mockServer); - expect(handleOneResponseForDocumentMock).toHaveBeenCalledTimes(1); - expect(handleOneResponseForDocumentMock).toHaveBeenLastCalledWith(td, valid_message, lax, mockServer); - - handleFStarResponseForDocument(td, fragment_0, lax, mockServer); - expect(handleOneResponseForDocumentMock).toHaveBeenCalledTimes(1); - - handleFStarResponseForDocument(td, valid_message, lax, mockServer); - expect(handleOneResponseForDocumentMock).toHaveBeenCalledTimes(2); - expect(handleOneResponseForDocumentMock).toHaveBeenLastCalledWith(td, valid_message, lax, mockServer); - - handleFStarResponseForDocument(td, fragment_1, lax, mockServer); - expect(handleOneResponseForDocumentMock).toHaveBeenCalledTimes(2); - handleFStarResponseForDocument(td, fragment_2, lax, mockServer); - expect(handleOneResponseForDocumentMock).toHaveBeenCalledTimes(2); - - }); - - test('test combined messages and fragments processed separately', () => { - const valid_message = '{"kind": "message"}'; - const fragment_0 = '{"kind": "'; - const fragment_1 = 'message'; - const fragment_2 = '"}'; - - const combined_messages = [valid_message, fragment_0, fragment_1, fragment_2].join('\n'); - - // Messages that are separated by newlines should be processed just as - // if they were received as separate messages. - handleFStarResponseForDocument(td, combined_messages, lax, mockServer); - expect(handleOneResponseForDocumentMock).toHaveBeenCalledTimes(2); - expect(handleOneResponseForDocumentMock).toHaveBeenNthCalledWith(1, td, valid_message, lax, mockServer); - expect(handleOneResponseForDocumentMock).toHaveBeenNthCalledWith(2, td, fragment_0 + fragment_1 + fragment_2, lax, mockServer); - }); -});