Skip to content

Commit

Permalink
Do not parse messages when defragging.
Browse files Browse the repository at this point in the history
  • Loading branch information
@gebner
gebner committed Oct 15, 2024
1 parent 2da3c7e commit 1c8ce62
Show file tree
Hide file tree
Showing 3 changed files with 63 additions and 127 deletions.
58 changes: 47 additions & 11 deletions lspserver/src/fstar.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,17 +19,23 @@ import { checkFileInDirectory, findFilesByExtension, getEnclosingDirectories } f

// FStar executable
export class FStar {
proc: cp.ChildProcess;
config: FStarConfig;
// Indicates whether the F* process supports full-buffer mode
supportsFullBuffer: boolean;
lax: boolean;

constructor(proc: cp.ChildProcess, config: FStarConfig, supportsFullBuffer: boolean, lax: boolean) {
this.proc = proc;
this.config = config;
this.supportsFullBuffer = supportsFullBuffer;
this.lax = lax;
jsonlIface: JsonlInterface;

public handleResponse: (msg: any) => void = () => {};

constructor(
public proc: cp.ChildProcess,
public config: FStarConfig,
// Indicates whether the F* process supports full-buffer mode
public supportsFullBuffer: boolean,
public lax: boolean,
) {
this.jsonlIface =
new JsonlInterface(
msg => this.handleResponse(msg),
chunk => this.proc.stdin?.write(chunk),
);
this.proc.stdout?.on('data', chunk => this.jsonlIface.onChunkReceived(chunk));
}

// Tries to spawn an fstar.exe process using the given configuration and
Expand Down Expand Up @@ -88,6 +94,8 @@ export class FStar {
{ cwd: config.cwd }
);

proc.stdin?.setDefaultEncoding('utf-8');

return new FStar(proc, config, supportsFullBuffer, !!lax);
}

Expand Down Expand Up @@ -249,3 +257,31 @@ export interface FStarConfig {
fstar_exe?: string; // path to fstar.exe
cwd?: string; // working directory for fstar.exe (usually not specified; defaults to workspace root)
}

export class JsonlInterface {
private buffer = '';
constructor(
public onMessageReceived: (_: any) => void,
public sendChunk: (_: string) => void,
) {}

onChunkReceived(chunk: Buffer | string) {
this.buffer = this.buffer + chunk.toString();

while (true) {
const i = this.buffer.indexOf('\n');
if (i < 0) break;
const msgJson = this.buffer.slice(0, i);
this.buffer = this.buffer.slice(i + 1);
try {
this.onMessageReceived(JSON.parse(msgJson));
} catch (e) {
console.log('failed to handle message', msgJson, e);
}
}
}

sendMessage(msg: any) {
this.sendChunk(JSON.stringify(msg) + '\n');
}
}
90 changes: 3 additions & 87 deletions lspserver/src/fstar_connection.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,19 +40,7 @@ export class FStarConnection {
onFullBufferResponse: (msg: any, query: FullBufferQuery) => void = _ => {};

constructor(private fstar: FStar, public debug: boolean) {
// TODO(klinvill): Should try to spawn F* from within this constructor
// instead.
this.fstar.proc.stdin?.setDefaultEncoding('utf-8');

// Register message handlers that will resolve the appropriate pending
// response promises for each query.
//
// The bufferedHandler buffers up received input until it finds a valid
// message. The wrapped handler will then be called with the parsed
// valid message. This handles receiving fragmented messages or multiple
// messages over the stream from the F* process.
const bufferedHandler = FStarConnection.bufferedMessageHandlerFactory((msg: object) => this.handleResponse(msg));
this.fstar.proc.stdout?.on('data', bufferedHandler);
this.fstar.handleResponse = msg => this.handleResponse(msg);

// F* error messages are just printed out
const fstar_proc_name = this.fstar.lax ? 'fstar lax' : 'fstar';
Expand Down Expand Up @@ -94,8 +82,7 @@ export class FStarConnection {
////////////////////////////////////////////////////////////////////////////////////

private sendLineNow(msg: any) {
const text = JSON.stringify(msg);
if (this.debug) console.log(">>> " + text);
if (this.debug) console.log(">>> " + JSON.stringify(msg));

if (this.fstar.proc.exitCode != null) {
const process_name = this.fstar.lax ? "flycheck" : "checker";
Expand All @@ -104,7 +91,7 @@ export class FStarConnection {
}

try {
this.fstar.proc?.stdin?.write(text + '\n');
this.fstar.jsonlIface.sendMessage(msg);
} catch (e) {
const msg = "ERROR: Error writing to F* process: " + e;
throw new Error(msg);
Expand Down Expand Up @@ -347,75 +334,4 @@ export class FStarConnection {
console.error("fstar.exe does not support full-buffer queries.");
}
}

// 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: any) => void) {
// 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_messages: any[] = [];
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.warn("Partially buffered message discarded: " + buffer);
}
buffer = "";
// Valid messages are valid JSON objects
valid_messages.push(JSON.parse(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 messages are valid JSON objects
valid_messages.push(JSON.parse(buffer));
buffer = "";
}
}
}

// Invoke the message handler for each received message in-order
valid_messages.forEach(message => handler(message));
};
}

// All messages from F* are expected to be valid JSON objects.
//
// TODO(klinvill): this should likely be refactored into `fstar_messages.ts` and
// potentially 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;
}
}
}
42 changes: 13 additions & 29 deletions lspserver/tests/fstar_connection.test.ts
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
import { beforeEach, describe, expect, test, jest } from '@jest/globals';

import { FStarConnection } from '../src/fstar_connection';
import { JsonlInterface } from '../src/fstar';


describe('bufferedMessageHandler tests', () => {
Expand All @@ -12,11 +12,12 @@ describe('bufferedMessageHandler tests', () => {
jest.clearAllMocks();

// Reset the function we're testing, this will create a fresh buffer.
bufferedMessageHandler = FStarConnection.bufferedMessageHandlerFactory(mockHandler);
const iface = new JsonlInterface(mockHandler, () => {});
bufferedMessageHandler = msg => iface.onChunkReceived(msg);
});

test('test valid message', () => {
const valid_message = '{"kind": "message"}';
const valid_message = '{"kind": "message"}\n';

bufferedMessageHandler(valid_message);
// Valid messages are passed on for further handling
Expand All @@ -27,7 +28,7 @@ describe('bufferedMessageHandler tests', () => {
test('test fragmented message', () => {
const fragment_0 = '{"kind": "';
const fragment_1 = 'message';
const fragment_2 = '"}';
const fragment_2 = '"}\n';

// Fragments are buffered until a full valid message is received, then it is
// passed on for further handling.
Expand All @@ -40,55 +41,38 @@ describe('bufferedMessageHandler tests', () => {
expect(mockHandler).toHaveBeenLastCalledWith(JSON.parse(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 valid_message = '{"kind": "message"}\n';
const fragment_0 = '{"kind": "';
const fragment_1 = 'message';
const fragment_2 = '"}';
const fragment_2 = '"}\n';

// 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(JSON.parse(valid_message));

bufferedMessageHandler(fragment_0);
expect(mockHandler).toHaveBeenCalledTimes(1);

bufferedMessageHandler(valid_message);
expect(mockHandler).toHaveBeenCalledTimes(2);
expect(mockHandler).toHaveBeenLastCalledWith(JSON.parse(valid_message));

bufferedMessageHandler(fragment_0);
expect(mockHandler).toHaveBeenCalledTimes(2);
bufferedMessageHandler(fragment_1);
expect(mockHandler).toHaveBeenCalledTimes(2);
bufferedMessageHandler(fragment_2);
expect(mockHandler).toHaveBeenCalledTimes(2);
expect(mockHandler).toHaveBeenCalledTimes(3);

});

test('test combined messages and fragments processed separately', () => {
const valid_message = '{"kind": "message"}';
const valid_message = '{"kind": "message"}\n';
const fragment_0 = '{"kind": "';
const fragment_1 = 'message';
const fragment_2 = '"}';
const fragment_2 = '"}\n';

const combined_messages = [valid_message, fragment_0, fragment_1, fragment_2].join('\n');
const combined_messages = [valid_message, fragment_0, fragment_1, fragment_2].join('');

// Messages that are separated by newlines should be processed just as
// if they were received as separate messages.
Expand Down

0 comments on commit 1c8ce62

Please sign in to comment.