Skip to content

Commit

Permalink
Merge pull request #353 from hwayne/fix-label-reporting
Browse files Browse the repository at this point in the history
Parse pluscal labels inserted due to macro
  • Loading branch information
FedericoPonzi authored Dec 20, 2024
2 parents a3169ad + 023467e commit c077132
Show file tree
Hide file tree
Showing 2 changed files with 60 additions and 2 deletions.
35 changes: 33 additions & 2 deletions src/parsers/pluscal.ts
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,7 @@ export class TranspilerStdoutParser extends ProcessOutputHandler<DCollection> {
*
* So we can start looking for labels as soon as we see (1)
* and stop as soon as we stop seeing label strings.
*
*/
private tryParseAddedLabels(line: string) {
// https://github.com/tlaplus/tlaplus/blob/21f92/tlatools/org.lamport.tlatools/src/pcal/ParseAlgorithm.java#L668
Expand All @@ -124,21 +125,25 @@ export class TranspilerStdoutParser extends ProcessOutputHandler<DCollection> {
return false;
}

const matcher = /^\s\s([A-Za-z0-9_]+) at line \d+, column \d+$/g.exec(line);
const matcher = /^\s\s([A-Za-z0-9_]+) at line \d+, column \d+/g.exec(line); // no closing `$` to handle macro statements
if (!matcher) { // done parsing
this.nowParsingAddedLabels = false;
return false;
}

const labelname = matcher[1];
const message = `Missing label, translator inserted \`${labelname}\` here`;
const locInfo = this.parseLocation(line) || ZERO_LOCATION_INFO;
const locInfo = this.parseLabelLocation(line) || ZERO_LOCATION_INFO;
const locRange = new vscode.Range(locInfo.location, locInfo.location);
this.result.addMessage(this.filePath, locRange, message, vscode.DiagnosticSeverity.Information);

return true;
}

/**
* Extracts location info from PlusCal translation strings.
* Note: not robust for labels. Use parseLabelLocation instead.
*/
private parseLocation(line: string): LocationInfo | undefined {
const rxLocation = /\s*(?:at )?line (\d+), column (\d+).?\s*$/g;
const matches = rxLocation.exec(line);
Expand All @@ -149,4 +154,30 @@ export class TranspilerStdoutParser extends ProcessOutputHandler<DCollection> {
const posCol = parseInt(matches[2]);
return new LocationInfo(new vscode.Position(posLine, posCol), matches[0].length);
}

/**
* Extracts label location info from label added strings.
* Similar to `parseLocation`, EXCEPT it's also robust against insertions due to macros:
*
* Lbl_2 at line 1, column 2 of macro called at line 23, column 5
*
* In this case, we want to capture "line 23, column 5" NOT "line 1".
*/

private parseLabelLocation(line: string): LocationInfo | undefined {
const rxLocation = /\s*(?:at )?line (\d+), column (\d+)(?: of macro called at line (\d+), column (\d+))?.?\s*$/g;
const matches = rxLocation.exec(line);
if (!matches) {
return undefined;
}

// get macro match if it exists, otherwise get label match
const matchLine = matches[3] || matches[1];
const matchCol = matches[4] || matches[2];

const posLine = parseInt(matchLine) - 1;
const posCol = parseInt(matchCol);

return new LocationInfo(new vscode.Position(posLine, posCol), matches[0].length);
}
}
27 changes: 27 additions & 0 deletions tests/suite/parsers/pluscal.test.ts
Original file line number Diff line number Diff line change
Expand Up @@ -142,6 +142,33 @@ suite('PlusCal Transpiler Output Parser Test Suite', () => {
]);
});

test('Captures inserted macro labels', () => {
const stdout = [
'pcal.trans Version 1.11 of 31 December 2020',
'The following labels were added:',
' Lbl_1 at line 16, column 5',
' Lbl_2 at line 1, column 5 of macro called at line 23, column 5',
' Lbl_3 at line 46, column 5',
'Parsing completed.',
'Translation completed.',
'New file saturation2.tla written.'
].join('\n');
assertOutput(stdout, '/Users/bob/TLA/needs_labels.tla', [
new vscode.Diagnostic(
new vscode.Range(15, 5, 15, 5),
'Missing label, translator inserted `Lbl_1` here',
vscode.DiagnosticSeverity.Information),
new vscode.Diagnostic(
new vscode.Range(22, 5, 22, 5),
'Missing label, translator inserted `Lbl_2` here',
vscode.DiagnosticSeverity.Information),
new vscode.Diagnostic(
new vscode.Range(45, 5, 45, 5),
'Missing label, translator inserted `Lbl_3` here',
vscode.DiagnosticSeverity.Information)
]);
});

test('Captures multiple errors after blank message', () => {
const stdout = [
'pcal.trans Version 1.11 of 31 December 2020',
Expand Down

0 comments on commit c077132

Please sign in to comment.