Chopper & Termination Plugin Interference

[ArquintL]

There are two orthogonal causes that together result in consistency errors when verifying a file in Gobra-IDE (or Gobra with ViperServer backend) and using the chopper (e.g. to verify a single member):

Cause 1: ViperServer internally invokes plugins

ViperServer (and Viper-IDE) recently fixed an issue that plugins have not been supported.
Since then, ViperServer first invokes the plugins (in particular beforeVerify) and performs caching on the resulting Viper AST.
(This has been introduced to Gobra in 9974336.)

Since Gobra invokes the termination (and predicate instance) plugin after encoding into Viper, these plugins get invoked twice when choosing the ViperServer backend. This in itself does not seem to be an issue but it's certainly not desirable.

Fixing Cause 1

Gobra should distinguish between the backends and only invoke plugins when (directly) using the Carbon & Silicon backends. For this purpose, the plugins should no longer be invoked as a part of the translation (into Viper) but within Gobra's backend wrapper (i.e. viper.gobra.backend.Silicion and viper.gobra.backend.Carbon).

Cause 2: Chopper has to run after plugins

The chopper takes dependencies between Viper members into account when deciding how to split up a Viper program into multiple smaller programs. These dependencies are tracked via calls (to domain functions, heap-dependent functions, and methods) and uses of predicates. However, the chopper does not take (future) transformations of plugins into account. E.g., the existence of a termination measure does not introduce a dependency to the WellFoundedOrder domain with its decreasing and bounded domain functions.

Thus, the chopper should run after plugins have performed their transformations such that no (implicit) dependencies are missed and the chopper does not produce a Viper program with missing declarations.

Fixing Cause 2

Since the chopper should run after the plugins and it became part of Viper, I propose to turn the chopper into a plugin, which is placed last in the list of plugins. Since I'm not aware of a way to configure plugins, we might have to sufficiently enrich the Viper AST (e.g. with Info objects), such that the chopper can retrieve all information it needs (e.g. how many subprograms should be created or which members should be verified) from the AST itself.