Add diagnostic for pluscal labels inserted by translation (#350)

[Feature][PlusCal] Signed-off-by: Hillel <h@hillelwayne.com>
tlaplus · Nov 20, 2024 · a3169ad · a3169ad
1 parent 3c89285
commit a3169ad
Show file tree

Hide file tree

Showing 2 changed files with 99 additions and 0 deletions.
diff --git a/src/parsers/pluscal.ts b/src/parsers/pluscal.ts
@@ -23,6 +23,7 @@ export class TranspilerStdoutParser extends ProcessOutputHandler<DCollection> {
     private readonly filePath: string;
     private errMessage: string | null = null;
     private nextLineIsError = false;
+    private nowParsingAddedLabels = false; // TODO should the parser be a state machine?
 
     constructor(source: Readable | string[] | null, filePath: string) {
         super(source, new DCollection());
@@ -51,6 +52,8 @@ export class TranspilerStdoutParser extends ProcessOutputHandler<DCollection> {
             this.addError(locInfo.location, this.errMessage);
             this.errMessage = null;
         }
+
+        this.tryParseAddedLabels(line);
     }
 
     private tryParseUnrecoverableError(line: string): boolean {
@@ -91,11 +94,51 @@ export class TranspilerStdoutParser extends ProcessOutputHandler<DCollection> {
         return true;
     }
 
+
     private addError(location: vscode.Position, message: string) {
         const locRange = new vscode.Range(location, location);
         this.result.addMessage(this.filePath, locRange, message);
     }
 
+    /**
+     * Adds info on labels added by the pluscal translated.
+     *
+     * Only takes effect if the `-reportLabels` was added to PlusCal options. Output looks like:
+     *
+     *       The following labels were added: // 1
+     *           Lbl_1 at line 16, column 5
+     *           Lbl_2 at line 23, column 9
+     *
+     *
+     * 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
+        const addStartPrefixes = ['The following labels were added:', 'The following label was added:'];
+        if (addStartPrefixes.some(prefix => line.startsWith(prefix))) {
+            this.nowParsingAddedLabels = true;
+            return true;
+        }
+        if (!this.nowParsingAddedLabels) {
+            return false;
+        }
+
+        const matcher = /^\s\s([A-Za-z0-9_]+) at line \d+, column \d+$/g.exec(line);
+        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 locRange = new vscode.Range(locInfo.location, locInfo.location);
+        this.result.addMessage(this.filePath, locRange, message, vscode.DiagnosticSeverity.Information);
+
+        return true;
+    }
+
     private parseLocation(line: string): LocationInfo | undefined {
         const rxLocation = /\s*(?:at )?line (\d+), column (\d+).?\s*$/g;
         const matches = rxLocation.exec(line);

diff --git a/tests/suite/parsers/pluscal.test.ts b/tests/suite/parsers/pluscal.test.ts
@@ -86,6 +86,62 @@ suite('PlusCal Transpiler Output Parser Test Suite', () => {
         ]);
     });
 
+    test('Captures single inserted label', () => {
+        const stdout = [
+            'pcal.trans Version 1.11 of 31 December 2020',
+            'The following label was added:',
+            '  Lbl_1 at line 16, 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),
+        ]);
+    });
+
+    test('Captures custom labels', () => {
+        const stdout = [
+            'pcal.trans Version 1.11 of 31 December 2020',
+            'The following label was added:',
+            '  AQX_Z1 at line 16, 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 `AQX_Z1` here',
+                vscode.DiagnosticSeverity.Information),
+        ]);
+    });
+
+    test('Captures inserted multiple 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 23, column 9',
+            '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, 9, 22, 9),
+                'Missing label, translator inserted `Lbl_2` here',
+                vscode.DiagnosticSeverity.Information)
+        ]);
+    });
+
     test('Captures multiple errors after blank message', () => {
         const stdout = [
             'pcal.trans Version 1.11 of 31 December 2020',