-
Notifications
You must be signed in to change notification settings - Fork 20
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Include definedness checks during exhale #457
Conversation
This will allow one to be able to be able to do permission definendess checks in a different state than the standard evaluation state.
…permission checks The setDefState field in DefinednessState is now mutable such that when unfolding one can change the definedness state (assuming there is a separate definedness state). An alternative would be to keep the same definedness state during an unfolding statement but to then explicitly reset this state via a Boogie statement at the end of an unfolding. Since Boogie performs constant propagation the resulting VC should essentially be the same for both approaches. The currently implemented approach is more in-line with the way encoding is currently handled, where new states are constructed instead of reusing previous states.
…nedness check) o special treatment for permission introspection since permission introspection within unfoldings still needs to be explored properly
…inside a package statement
…nedness state. As a result, we can remove the predicate in this state (but do not check whether it is there, because in this mode well-definedness is assumed; analogous to inhale).
… exhale this check should not be required, but I add it as a sanity check
…state if the exhale is non-empty
One aspect that this PR does not resolve and that should be handled in another PR is when one of the following two cases occur during an exhale:
The expected behavior is to evaluate those occurrences of permission introspection in the evaluation permission mask, that is, the mask which the exhale modifies when permissions are removed. Currently, these occurrences are evaluated in the well-definedness permission mask, that is, the permission mask right before the exhale. The code contains |
Update tests for Carbon exhale with well-definedness change (Carbon PR viperproject/carbon#457)
Previously, the encoding for
exhale A
first checked well-definedness ofA
and in a second step performed the actual exhale. This approach is flawed, because (1) well-definedness ofA
depends on the actual exhale in the general case and (2) in cases where the exhale fails, the reported errors are not the expected ones. See #406 for examples illustrating these two problems.This PR implements an exhale implementation, which (if enabled) does the well-definedness checks during the exhale (as we already do with inhale).