Generalized Heapster lifetime ownership permissions #1645
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
added 27 commits
April 15, 2022 14:07
…sions, not just field, array, and block permissions
…bitrary lowned permissions...
… of SImpl_ElimLOWnedSimple
…an error, since these can now come about from lifetimes ending
…ifetime that has an lowned perm that needs to be proved
… come from converting ExprPerms to DistPerms
…sions in solveForPermListImpl
…that occur as fieldsh(eq(y)) in shapes of block permissions that are needed
ChrisEPhifer
approved these changes
Apr 27, 2022
There was a problem hiding this comment.
As far as my limited understanding of the implication prover extends, everything here looks good. It might be good to have a second set of eyes look over the Permissions and Implication modules just to be sure there's no logic errors, but I've approved the changes anyway (I won't add the ready-to-merge label, however, in case you decide to have MattY or someone else take a look.)
|
Luckily, we have CI tests to check the logic! :) Also, I think Matt Y has about the same level of understanding as you. So, in the end, I think this is ready. Thanks! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR changes the
lowned (ps_in -o ps_out)lifetime ownership permissions to allow arbitrary permissions inps_inandps_out. Previously, only field, array, or block permissions were allowed in these positions. This change is necessary in order to support Rust functions with return types that contain lifetimes inside of complex shapes. For instance, many Rust collection types have methods with types likefn get_element <'a> (x: &'a Collection) -> Option<&'a Elem>that return an
Optional reference. This return type translates to the Heapster typeeq(0) or [l]memblock(...), which must be in the input permission set of thelownedpermission returned by the function.