Skip to content

Faster NameAnalyser implementation#631

Merged
marcoeilers merged 4 commits into
masterfrom
meilers_faster_resolver
Nov 30, 2022
Merged

Faster NameAnalyser implementation#631
marcoeilers merged 4 commits into
masterfrom
meilers_faster_resolver

Conversation

@marcoeilers

Copy link
Copy Markdown
Contributor

The current NameAnalyser's check to ensure that local variables are not used before they are declared is really really slow for large methods (see issue #630).
It first walks through the entire PAST and collects all declarations, then, in a second pass, it iterates over the the entire PAST again and, for every local variable reference it finds, walks through all AST nodes occurring in the current method again and checks if the current variable reference is found before its declaration (method containsSubnodeBefore).

This PR simplifies the process as follows:

  • We first walk over all global member declarations to collect all globally available names.
  • Then we walk through each member completely a single time, collecting all local declarations in the process, and checking for all references if they are already defined in the current context (which contains all global declarations, as well as all local declarations we have found so far).

This has the drawback that our error message can no longer state whether we are referencing a local variable that has not been declared yet or one that has not been declared at all, but it massively speeds up the entire checking process for large methods.

Also, I added an isPure function on the AST node for Viper functions because I need this for something else.

@marcoeilers marcoeilers requested a review from fpoli November 30, 2022 15:09

@fpoli fpoli left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice, thanks! I tested on the programs of #630 and Silicon terminates in a few seconds now.

Comment thread src/main/scala/viper/silver/parser/Resolver.scala Outdated
@marcoeilers marcoeilers merged commit 911ed71 into master Nov 30, 2022
@marcoeilers marcoeilers deleted the meilers_faster_resolver branch November 30, 2022 19:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants