Skip to content
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

Improved ptr permission implications #1373

Merged
merged 3 commits into from
Jul 9, 2021
Merged

Conversation

eddywestbrook
Copy link
Contributor

This commit changes implication for ptr perms to prioritize using LHS permissions that precisely match the offset of the ptr perm being proven. That is, if we are proving something like

ptr((W,0) |-> p1) * array(8, <z8, *8, [(W,0) |-> int64<>], []) -o ptr((W,0) |-> p2)

the old approach would consider using the array permission at index -1 as one way to perform the proof. The new way sees that there is indeed a ptr perm on the LHS with the correct offset, so ignores any other possibilities.

This PR also adds the clearbufs example which requires this change for its type-checking.

Eddy Westbrook added 2 commits July 8, 2021 17:32
… that precisely match the offset of the ptr perm being proven
@eddywestbrook eddywestbrook added the subsystem: heapster Issues specifically related to memory verification using Heapster label Jul 9, 2021
@eddywestbrook eddywestbrook requested a review from m-yac July 9, 2021 14:09
Copy link
Contributor

@m-yac m-yac left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me

@eddywestbrook eddywestbrook added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Jul 9, 2021
@mergify mergify bot merged commit e6d7f56 into master Jul 9, 2021
@mergify mergify bot deleted the heapster-improved-ptr-impls branch July 9, 2021 20:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run subsystem: heapster Issues specifically related to memory verification using Heapster
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants