feat: Support let arguments

ProVerif · Sep 17, 2023 · 187259b · 187259b
1 parent 204ab20
commit 187259b
Show file tree

Hide file tree

Showing 3 changed files with 41 additions and 5 deletions.
diff --git a/server/src/tasks/collectors.ts b/server/src/tasks/collectors.ts
@@ -1,6 +1,6 @@
 import {
-    BasicpatternContext,
-    NeidentseqContext, NepatternseqContext,
+    BasicpatternContext, MayfailvartypeseqContext,
+    NeidentseqContext, NemayfailvartypeseqContext, NepatternseqContext,
     NevartypeContext,
     OnevartypeContext,
     TpatternContext, TpatternseqContext
@@ -70,4 +70,15 @@ export const collectBasicpattern = (ctx: BasicpatternContext): TerminalNode[] =>
     }
 
     return [];
+};
+
+export const collectNemayfailvartypeseq = (ctx: NemayfailvartypeseqContext) : TerminalNode[] => {
+    const identifiers = collectNeidentseqIDENTs(ctx.mayfailvartype().neidentseq());
+
+    const nemayfailvartypeseq = ctx.nemayfailvartypeseq();
+    if (nemayfailvartypeseq) {
+        return [...identifiers, ...collectNemayfailvartypeseq(nemayfailvartypeseq)];
+    }
+
+    return [...identifiers];
 };
diff --git a/server/src/tasks/create_symbol_table.ts b/server/src/tasks/create_symbol_table.ts
@@ -5,7 +5,11 @@ import {
     TprocessContext
 } from "../parser-proverif/ProverifParser";
 import {TerminalNode} from "antlr4ts/tree/TerminalNode";
-import {collectNeidentseqIDENTs, collectNevartypeIDENTs, collectTPatternIDENTs} from "./collectors";
+import {
+    collectNeidentseqIDENTs, collectNemayfailvartypeseq,
+    collectNevartypeIDENTs,
+    collectTPatternIDENTs
+} from "./collectors";
 
 
 export type CreateSymbolTableResult = {
@@ -50,7 +54,20 @@ class SymbolTableVisitor extends AbstractParseTreeVisitor<ProverifSymbolTable> i
             });
         }
 
-        return this.visitChildren(ctx);
+        if (ctx.LET()) {
+            return this.withContext(ctx, () => {
+                const mayfailvartypeseq = ctx.mayfailvartypeseq();
+                const nemayfailvartypeseq = mayfailvartypeseq?.nemayfailvartypeseq();
+                if (nemayfailvartypeseq) {
+                    collectNemayfailvartypeseq(nemayfailvartypeseq).forEach(identifier => {
+                        this.registerVariable(identifier);
+                    });
+                }
+                return this.visitChildren(ctx);
+            });
+        } else {
+            return this.visitChildren(ctx);
+        }
     };
 
     public visitTprocess = (ctx: TprocessContext) => {

diff --git a/server/tests/go_to_definition.test.ts b/server/tests/go_to_definition.test.ts
@@ -106,13 +106,21 @@ describe('parser', function () {
     });
 
     it("consider query variables", async () => {
-        const code = `free b: bitstring.\nquery x:bitstring; attacker(x). process \nin(c, b)`;
+        const code = `free b: bitstring.\nquery x:bitstring; attacker(x). process 0`;
         const click = {line: 1, character: 29};
         const target = {line: 1, character: 6};
 
         await assertSingleFileNavigation(code, click, target, 1);
     });
 
+    it("consider let arguments", async () => {
+        const code = `let Proc(c: channel) = \nin(c, b:bitstring).\nprocess 0`;
+        const click = {line: 1, character: 4};
+        const target = {line: 0, character: 9};
+
+        await assertSingleFileNavigation(code, click, target, 1);
+    });
+
     it("checks in dependencies if not found in main", async () => {
         const dependencyCode = `channel c.`;
         const dependencyUri = 'dependency';