Skip to content

[Plugin] Translation of Entity Verification Results#641

Merged
ArquintL merged 5 commits into
masterfrom
plugin-entity-result-translation
Jan 6, 2023
Merged

[Plugin] Translation of Entity Verification Results#641
ArquintL merged 5 commits into
masterfrom
plugin-entity-result-translation

Conversation

@ArquintL

@ArquintL ArquintL commented Jan 3, 2023

Copy link
Copy Markdown
Member

This PR adds another hook to the plugin infrastructure such that plugins can translation entity verification results.
For most plugins, the translation in this step is supposed to be identical to translating the overall verification result (which is the case for the current set of plugins).

The refute plugin has been adapted to (1) be aware of refute statements per entity (and thus support streaming of verification results) and (2) be stateless. The latter is achieved by storing all necessary information in the AST (as Info) instead of in the plugin's state. For this purpose, mapVerificationResult takes now the AST (as produced after applying all plugins' beforeVerify) as parameter such that plugins do not need to store the AST.

Furthermore, this PR changes SilFrontend to apply filtering of methods (based on the configuration) and to apply all plugins' beforeVerify at the beginning of the verification phase (instead of at the end of the consistency check phase). This is irrelevant for instances of SilFrontend that execute both, the consistency check phase followed by the verification phase. However, ViperAstProvider is an instance that only performs the phases up to including consistency checking (i.e. without verifying the resulting AST).
This change has two purposes:

  1. It's imho more sensible to perform beforeVerify before verifying an AST.
  2. ViperServer splits the overall process into two steps: (1) generating an AST (by using ViperAstProvider) and (2) verifying an AST (by using SiliconFrontend, CarbonFrontend or a custom frontend in an abusive way such that the enclosed verifier is used without executing all phases). This change moves the application of beforeVerify to ViperServer's second step, which not only gives the second step more flexibility to decide when exactly to apply beforeVerify (i.e. before or after applying the cache) but also provides flexibility to plugin implementations as their state is maintained between beforeVerify and mapVerificationResult (this was not the case in the past because separate instances of the plugin are used by the two ViperServer steps (which however remains the case)).

The latter change made the changes to AstPositionsTests necessary because the resulting AST (produced by ViperAstProvider) now looks apparently different (imho better / as one would expect).

Fixes #634

@ArquintL ArquintL marked this pull request as draft January 4, 2023 09:44
@ArquintL

ArquintL commented Jan 4, 2023

Copy link
Copy Markdown
Member Author

I've noticed some issues that I first need to address

…rmining whether a verification has occurred or not for a given refute statement

@marcoeilers marcoeilers left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

LGTM

Comment thread src/main/scala/viper/silver/plugin/PluginTemplate.scala Outdated
@ArquintL ArquintL merged commit d7fa226 into master Jan 6, 2023
@ArquintL ArquintL deleted the plugin-entity-result-translation branch January 6, 2023 16:07
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.

[Plugins] Streaming of Verification Results

2 participants