Run-time checks/branch conditions based on predicate bodies/method contracts use declaration variable not current context variable

[jennalwise]

https://github.com/gradual-verification/gvc0/blob/master/src/test/resources/bugs/predicate_vars.c0 is failing with gvc.transformer.IRGraph$IRException: Variable 'node' not found. This happens as a few run-time checks related to folding the body of the wrappedAcc predicate are being created for the body's local variable node and not the current context’s variable taken in as an argument, e.g. b in fold wrappedAcc(b).

In general, before consuming or producing predicate bodies or method call preconditions/postconditions, Viper creates a new symbolic state where the callee’s symbolic values for its arguments are assigned to the local variables in the predicate body or precondition/postcondition. That new state is then used to consume or produce the specification, e.g. b’ in fold wrappedAcc(b) is mapped to node in the store {node->b’}, which is used to consume acc(node->next). Therefore, any run-time checks created during those consumes or produces use the local variable, e.g. node. The front-end fails since the local variable (node) does not exist in the callee’s context (b is the correct variable to use in place of node). Solution is to somehow carry around the information that the callee’s variable (b) should replace the local variable (node) in the run-time check, whether it be in the check itself or a branch condition and make that replacement when creating the run-time check. In, predicate_vars.c0 the replacement needs to happen in the run-time checks for the folds and in conditional_version.c0 (https://github.com/gradual-verification/gvc0/blob/master/src/test/resources/verifier/conditional_version.c0) the replacement needs to happen in a branch condition from testCall’s postcondition for the run-time check created in test.

Note: The solution needs to apply to both produces and consumes around method calls and folds/unfolds where the body of the predicate is being consumed or produced (doesn’t apply to producing or consuming access to the predicate as a whole).

[jennalwise]

Fix in commits: https://github.com/gradual-verification/silicon-gv/commit/a52d76ebbd5dd1908c0ddea962f3cd23deb5f3a3, https://github.com/gradual-verification/silicon-gv/commit/2cdde7ab734b7f39becadac371b6f6e132dbc3ee, and https://github.com/gradual-verification/silicon-gv/commit/da669862157fd01121a7546d86a1087d2d7f74fa

Note about solution:

The translator could house the code that sets the correct stores/heaps based on whether the old store is set for translation. However, the solution that has been implemented instead sets the correct stores/heaps before calling the translator. There are pros and cons/trade-offs to each of these approaches. Removing the decision from the translator seems kind of natural, because it seems natural to call the translator with the state that you want to translate in and it is unexpected that the translator would modify the state in some way and then translate. It also becomes more obvious throughout the system where the old store and old heap functionality is required for translation. On the other hand, it is nice to hide this functionality in translator to clean up the code and make further modifications to the code easier. That is, in a significant number of places where translator is called code has been injected to set the correct store/heap and so moving this functionality to the translator would clean up the code quite a bit. So, we might consider refactoring the implemented solution in the future.

[jennalwise]

Tested & fix looks good!