refactor: Avoid recursing twice

ProVerif · Mar 25, 2024 · 786b040 · 786b040
1 parent b7b6de1
commit 786b040
Show file tree

Hide file tree

Showing 2 changed files with 35 additions and 18 deletions.
diff --git a/server/src/go_to_definition.ts b/server/src/go_to_definition.ts
@@ -4,8 +4,9 @@ import {getMatchingParseTree} from "./parseTree/get_matching_parse_tree";
 import {getRange} from "./parseTree/get_range";
 import {DefinitionLink} from "vscode-languageserver-protocol";
 import {ParseTree} from "antlr4ts/tree";
-import {ProverifSymbol} from "./tasks/create_symbol_table";
+import {DeclarationType, ProverifSymbol} from "./tasks/create_symbol_table";
 import {TerminalNode} from "antlr4ts/tree/TerminalNode";
+import {LibraryDependencyToken} from "./tasks/parse_library_dependencies";
 
 type Origin = { uri: TextDocumentIdentifier, match: TerminalNode };
 export type DefinitionSymbol = { uri: TextDocumentIdentifier, symbol: ProverifSymbol, origin: Origin }
@@ -26,22 +27,27 @@ 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);
+    return  getDefinitionSymbolFromMatchMacroAware(parseResult, matchingParseTree, documentManager);
 };
 
-export const getDefinitionSymbolFromMatchMacroAware = async (parseResult: ParseResult, matchingParseTree: TerminalNode, documentManager: DocumentManagerInterface, considerMacros: boolean): Promise<DefinitionSymbol | undefined> => {
+const getDefinitionSymbolFromMatchMacroAware = async (parseResult: ParseResult, matchingParseTree: TerminalNode, documentManager: DocumentManagerInterface): Promise<DefinitionSymbol | undefined> => {
     const origin = {uri: parseResult.identifier, match: matchingParseTree};
 
-    const closestSymbol = parseResult.symbolTable.findClosestSymbol(matchingParseTree.text, matchingParseTree, considerMacros);
+    const closestSymbol = parseResult.symbolTable.findClosestSymbol(matchingParseTree.text, matchingParseTree);
     if (closestSymbol) {
+        if (closestSymbol.declaration === DeclarationType.ExpandParameter) {
+            // TODO: break the cycle
+            const originSymbol = await getDefinitionSymbolFromMatch(parseResult, closestSymbol.node, documentManager);
+            if (originSymbol) {
+                return originSymbol;
+            }
+        }
+
         return {uri: parseResult.identifier, symbol: closestSymbol, origin};
     }
 
+    let currentClosestSymbol: ProverifSymbol|undefined;
+    let currentClosestSymbolDependency: LibraryDependencyToken|undefined;
     for (let i = 0; i < parseResult.dependencyTokens.length; i++) {
         const dependency = parseResult.dependencyTokens[i];
         if (!dependency.exists) {
@@ -53,12 +59,23 @@ export const getDefinitionSymbolFromMatchMacroAware = async (parseResult: ParseR
             continue;
         }
 
-        const closestSymbol = dependencyParseResult.symbolTable.findClosestSymbol(matchingParseTree.text, undefined, considerMacros);
+        const closestSymbol = dependencyParseResult.symbolTable.findClosestSymbol(matchingParseTree.text, undefined);
         if (!closestSymbol) {
             continue;
         }
 
-        return {uri: dependency, symbol: closestSymbol, origin};
+        currentClosestSymbol = closestSymbol;
+        currentClosestSymbolDependency = dependency;
+        if (closestSymbol.declaration === DeclarationType.ExpandParameter) {
+            // TODO: check in library first for previous declaration, before going to another library
+            continue;
+        }
+
+        break;
+    }
+
+    if (currentClosestSymbol && currentClosestSymbolDependency) {
+        return {uri: currentClosestSymbolDependency, symbol: currentClosestSymbol, origin}
     }
 
     return undefined;

diff --git a/server/src/tasks/create_symbol_table.ts b/server/src/tasks/create_symbol_table.ts
@@ -409,28 +409,28 @@ export class ProverifSymbolTable {
         this.publicContext = publicContext;
     }
 
-    public findClosestSymbol(text: string, context: ParseTree|undefined, considerMacros: boolean): ProverifSymbol | undefined {
-        return this.findClosestSymbolInternal(text, context ?? this.publicContext, considerMacros);
+    public findClosestSymbol(text: string, context: ParseTree|undefined): ProverifSymbol | undefined {
+        return this.findClosestSymbolInternal(text, context ?? this.publicContext);
     }
 
     public getSymbols(): ProverifSymbol[] {
         return this.symbols;
     }
 
-    private findClosestSymbolInternal(name: string, context: ParseTree|undefined, considerMacros: boolean): ProverifSymbol | undefined {
+    private findClosestSymbolInternal(name: string, context: ParseTree|undefined): 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 && (considerMacros || matchingSymbol.declaration !== DeclarationType.ExpandParameter)) {
+        if (matchingSymbol) {
             return matchingSymbol;
         }
 
         // if in tprocess, check whether defined in library
         if (context instanceof TprocessContext && context.parent instanceof AllContext) {
-            return this.findClosestSymbolInternal(name, this.publicContext, considerMacros);
+            return this.findClosestSymbolInternal(name, this.publicContext);
         }
 
         // if in OTHERWISE, then jump directly to the real parent, not the previous clauses
@@ -440,10 +440,10 @@ export class ProverifSymbolTable {
                 realParent = realParent.parent;
             }
 
-            return this.findClosestSymbolInternal(name, realParent, considerMacros);
+            return this.findClosestSymbolInternal(name, realParent);
         }
 
-        return this.findClosestSymbolInternal(name, context.parent, considerMacros);
+        return this.findClosestSymbolInternal(name, context.parent);
     }
 }