feat: Improve macro resolution

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

Hide file tree

Showing 3 changed files with 65 additions and 39 deletions.
diff --git a/CONTRIBUTE.md b/CONTRIBUTE.md
@@ -80,7 +80,7 @@ Go to definition:
 - [x] Add go to definition functionality; see https://tomassetti.me/integrating-code-completion-in-visual-studio-code/
 - [x] Invalidate cache of consumers when library stored
 - [x] Support additional ways of declaring variables (e.g. in REDUCTION lib)
-- [ ] Properly implement macro resolution
+- [ ] Properly implement macro resolution (see TODOs in corresponding unit test)
 - [ ] Improve performance by considering previous resolutions
 
 Support writing ProVerif:

diff --git a/server/src/go_to_definition.ts b/server/src/go_to_definition.ts
@@ -6,7 +6,6 @@ import {DefinitionLink} from "vscode-languageserver-protocol";
 import {ParseTree} from "antlr4ts/tree";
 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 }
@@ -27,55 +26,51 @@ export const getDefinitionSymbolFromPosition = async (identifier: TextDocumentId
 
 
 export const getDefinitionSymbolFromMatch = async (parseResult: ParseResult, matchingParseTree: TerminalNode, documentManager: DocumentManagerInterface): Promise<DefinitionSymbol | undefined> => {
-    return  getDefinitionSymbolFromMatchMacroAware(parseResult, matchingParseTree, documentManager);
-};
-
-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);
-    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) {
-            continue;
-        }
-
-        const dependencyParseResult = await documentManager.getParseResult(dependency);
-        if (!dependencyParseResult) {
+    // collect relevant files in order
+    const getParseResults: (() => Promise<ParseResult | undefined>)[] = parseResult.dependencyTokens
+        .filter(dependencyToken => dependencyToken.exists)
+        .map(dependencyToken => () => documentManager.getParseResult(dependencyToken));
+    getParseResults.unshift(async () => parseResult);
+
+    // look for best matching symbol
+    let currentContext: ParseTree | undefined = matchingParseTree;
+    let currentClosestSymbol: ProverifSymbol | undefined;
+    let currentClosestSymbolDependency: TextDocumentIdentifier | undefined;
+    while (getParseResults.length > 0) {
+        const getParseResult = getParseResults.shift()!;
+        const parseResult = await getParseResult();
+        const symbolTable = parseResult?.symbolTable;
+        if (!parseResult || !symbolTable) {
             continue;
         }
 
-        const closestSymbol = dependencyParseResult.symbolTable.findClosestSymbol(matchingParseTree.text, undefined);
+        const closestSymbol = symbolTable.findClosestSymbol(matchingParseTree.text, currentContext);
         if (!closestSymbol) {
+            currentContext = undefined;
             continue;
         }
 
         currentClosestSymbol = closestSymbol;
-        currentClosestSymbolDependency = dependency;
+        currentClosestSymbolDependency = parseResult.identifier;
+
+        // if defined by macro, try to find real definition
         if (closestSymbol.declaration === DeclarationType.ExpandParameter) {
-            // TODO: check in library first for previous declaration, before going to another library
+            // 1st parent: the expand LibContext; 2nd parent: whatever is before
+            currentContext = closestSymbol.context?.parent?.parent;
+            if (currentContext) {
+                // recheck in same file
+                getParseResults.unshift(async () => parseResult);
+            }
             continue;
         }
 
         break;
     }
 
     if (currentClosestSymbol && currentClosestSymbolDependency) {
-        return {uri: currentClosestSymbolDependency, symbol: currentClosestSymbol, origin}
+        return {uri: currentClosestSymbolDependency, symbol: currentClosestSymbol, origin};
     }
 
     return undefined;

diff --git a/server/tests/go_to_definition.test.ts b/server/tests/go_to_definition.test.ts
@@ -99,13 +99,44 @@ def My(ProcImplementation,SystemInterface) {
 expand My(Proc, System).
 process System`;
 
-        const click = {line: 2, character: 28};
+        // ProcImplementation defined outside, hence this is the real definition
+        const click = {line: 1, character: 7};
         const target = {line: 1, character: 7};
-        await assertSingleFileNavigation(code, click, target, 18);
-
-        const click2 = {line: 5, character: 9};
-        const target2 = {line: 4, character: 16};
-        await assertSingleFileNavigation(code, click2, target2, 6);
+        await assertSingleFileNavigation(code, click, target, 'ProcImplementation'.length);
+
+        /* TODO implement
+        // SystemInterface defined inside macro
+        const click1 = {line: 1, character: 25};
+        const target1 = {line: 2, character: 12};
+        await assertSingleFileNavigation(code, click1, target1, 'SystemInterface'.length);
+        */
+
+        // SystemInterface defined inside macro
+        const click2 = {line: 2, character: 8};
+        const target2 = {line: 2, character: 8};
+        await assertSingleFileNavigation(code, click2, target2, 'SystemInterface'.length);
+
+        // ProcImplementation defined outside, hence definition inside macro signature
+        const click3 = {line: 2, character: 30};
+        const target3 = {line: 1, character: 7};
+        await assertSingleFileNavigation(code, click3, target3, 'ProcImplementation'.length);
+
+        // Proc defined at start
+        const click4 = {line: 4, character: 10};
+        const target4 = {line: 0, character: 4};
+        await assertSingleFileNavigation(code, click4, target4, 'Proc'.length);
+
+        /* TODO implement
+        // System defined by macro, hence navigate to macro signature
+        const click5 = {line: 4, character: 18};
+        const target5 = {line: 1, character: 23};
+        await assertSingleFileNavigation(code, click5, target5, 'Proc'.length);
+         */
+
+        // System defined by macro
+        const click6 = {line: 5, character: 9};
+        const target6 = {line: 4, character: 16};
+        await assertSingleFileNavigation(code, click6, target6, 'System'.length);
     });
 
     it("consider query variables", async () => {