Improve Heapster implication prover for opaque named shapes #1394
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
…es, including: modalizeShape for opaque named shapes is now a no-op; and proveVarLLVMBlock now eliminates a perm on the LHS when it cannot find a match to prove opaque named shapes on the right
eddywestbrook
added
the
subsystem: heapster
| @@ -5402,6 +5410,27 @@ proveVarLLVMBlocks' x ps psubst mb_bps_in mb_ps = case mbMatch mb_bps_in of | |||
| implSwapInsertConjM x (Perm_LLVMBlock bp') ps_out' 0 | |||
|
|
|||
|
|
|||
| -- If proving an opaque named shape, the only way to prove the memblock | |||
| -- permission is to have it on the left, but we don't have a memblock | |||
| -- permission on the left with this exactly offset, length, and shape, because | |||
There was a problem hiding this comment.
Grammar nitpick: Should be "exact offset, length, ..." instead of "exactly offset, length, ..."
ChrisEPhifer
approved these changes
Jul 22, 2021
There was a problem hiding this comment.
I'm not really up-to-speed on how the implication prover works, but the code looks sensible / consistent with the documentation and PR description! Minor grammar nitpick on the comments for the non-unfoldable shape case, otherwise I think this is good (a second set of eyes belonging to someone who knows how the implication prover works would be good, though!)
|
Note: the CI did pass before I tweaked the comment per Chris's suggestion, so I did not think the CI had to be re-run with that change to a comment. |
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.
Did some work to improve the implication prover for opaque named shapes, in support of some Rust verification. This included:
modalizeShapefor opaque named shapes is now a no-op, because we assume that opaque shapes do not contain any pointers (at least, none that we will ever access), and the point ofmodalizeShapeis to adjust the modalities on any pointers contained in a shape; andproveVarLLVMBlocknow eliminates a perm on the LHS when it cannot find a match to prove opaque named shapes on the right.