feat: Improve macro support, support in-lib declarations

ProVerif · Mar 24, 2024 · c1240b7 · c1240b7
1 parent 1a4d218
commit c1240b7
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 11 deletions.
diff --git a/server/src/go_to_definition.ts b/server/src/go_to_definition.ts
@@ -26,9 +26,18 @@ export const getDefinitionSymbolFromPosition = async (identifier: TextDocumentId
 
 
 export const getDefinitionSymbolFromMatch = async (parseResult: ParseResult, matchingParseTree: TerminalNode, documentManager: DocumentManagerInterface): Promise<DefinitionSymbol | undefined> => {
+    const definition = getDefinitionSymbolFromMatchMacroAware(parseResult, matchingParseTree, documentManager, false);
+    if (definition) {
+        return definition
+    }
+
+    return getDefinitionSymbolFromMatchMacroAware(parseResult, matchingParseTree, documentManager, true)
+};
+
+export const getDefinitionSymbolFromMatchMacroAware = async (parseResult: ParseResult, matchingParseTree: TerminalNode, documentManager: DocumentManagerInterface, considerMacros: boolean): Promise<DefinitionSymbol | undefined> => {
     const origin = {uri: parseResult.identifier, match: matchingParseTree};
 
-    const closestSymbol = parseResult.symbolTable.findClosestSymbol(matchingParseTree.text, matchingParseTree);
+    const closestSymbol = parseResult.symbolTable.findClosestSymbol(matchingParseTree.text, matchingParseTree, considerMacros);
     if (closestSymbol) {
         return {uri: parseResult.identifier, symbol: closestSymbol, origin};
     }
@@ -44,7 +53,7 @@ export const getDefinitionSymbolFromMatch = async (parseResult: ParseResult, mat
             continue;
         }
 
-        const closestSymbol = dependencyParseResult.symbolTable.findClosestSymbol(matchingParseTree.text);
+        const closestSymbol = dependencyParseResult.symbolTable.findClosestSymbol(matchingParseTree.text, undefined, considerMacros);
         if (!closestSymbol) {
             continue;
         }

diff --git a/server/src/tasks/create_symbol_table.ts b/server/src/tasks/create_symbol_table.ts
@@ -240,14 +240,24 @@ class SymbolTableVisitor extends AbstractParseTreeVisitor<ProverifSymbolTable> i
             }
 
             this.collectProcessStyleTerms(ctx, true);
-            return this.visitInners(() => ctx.tprocess());
+
+            this.visitInners(() => ctx.tprocess());
+            this.visitInner(() => ctx.opttprocess());
+            this.visitInner(() => ctx.optinprocess());
+            this.visitInner(() => ctx.optelseprocess());
+
+            return this.defaultResult();
         });
     };
 
     public visitPterm = (ctx: PtermContext) => {
         return this.withContext(ctx, () => {
             this.collectProcessStyleTerms(ctx, false);
-            return this.visitInners(() => ctx.pterm());
+
+            this.visitInners(() => ctx.pterm());
+            this.visitInner(() => ctx.optelseterm());
+
+            return this.defaultResult();
         });
     };
 
@@ -399,28 +409,28 @@ export class ProverifSymbolTable {
         this.publicContext = publicContext;
     }
 
-    public findClosestSymbol(text: string, context?: ParseTree): ProverifSymbol | undefined {
-        return this.findClosestSymbolInternal(text, context ?? this.publicContext);
+    public findClosestSymbol(text: string, context: ParseTree|undefined, considerMacros: boolean): ProverifSymbol | undefined {
+        return this.findClosestSymbolInternal(text, context ?? this.publicContext, considerMacros);
     }
 
     public getSymbols(): ProverifSymbol[] {
         return this.symbols;
     }
 
-    private findClosestSymbolInternal(name: string, context?: ParseTree): ProverifSymbol | undefined {
+    private findClosestSymbolInternal(name: string, context: ParseTree|undefined, considerMacros: boolean): ProverifSymbol | undefined {
         if (!context) {
             return undefined;
         }
 
         const symbolsOfContext = this.symbols.filter(symbol => symbol.context === context);
         const matchingSymbol = symbolsOfContext.find(symbol => symbol.node.text === name);
-        if (matchingSymbol) {
+        if (matchingSymbol && (considerMacros || matchingSymbol.declaration !== DeclarationType.ExpandParameter)) {
             return matchingSymbol;
         }
 
         // if in tprocess, check whether defined in library
         if (context instanceof TprocessContext && context.parent instanceof AllContext) {
-            return this.findClosestSymbolInternal(name, this.publicContext);
+            return this.findClosestSymbolInternal(name, this.publicContext, considerMacros);
         }
 
         // if in OTHERWISE, then jump directly to the real parent, not the previous clauses
@@ -430,10 +440,10 @@ export class ProverifSymbolTable {
                 realParent = realParent.parent
             }
 
-            return this.findClosestSymbolInternal(name, realParent);
+            return this.findClosestSymbolInternal(name, realParent, considerMacros);
         }
 
-        return this.findClosestSymbolInternal(name, context.parent);
+        return this.findClosestSymbolInternal(name, context.parent, considerMacros);
     }
 }