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

Bugfix: infinite loop in eliminating an LLVM block permission #1401

Merged
merged 1 commit into from
Aug 3, 2021

Conversation

eddywestbrook
Copy link
Contributor

When trying to prove memblock(R,off,len,Sh1<args1>) -o memblock(R,off,len,Sh2<args2>) for an unfoldable name Sh1 and an opaque name Sh2, the implication prover would first duplicate the Sh1<args1> permission, because it is copyable, unfold it, and then try to prove Sh2<args2>, where it would identify that Sh1<args1> permission as a candidate, so it would duplicate it, unfold it, ...

The fix is to not duplicate when eliminating a block permission on the left, even if it is copyable.

…on before eliminating it and would then go right back to trying to eliminate that same permission again...
@eddywestbrook eddywestbrook added the subsystem: heapster Issues specifically related to memory verification using Heapster label Aug 3, 2021
@eddywestbrook eddywestbrook requested review from glguy and m-yac August 3, 2021 00:45
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 Aug 3, 2021
@eddywestbrook eddywestbrook merged commit d3a8872 into master Aug 3, 2021
@mergify mergify bot deleted the bugfix-impl-elim-llvm-block branch August 3, 2021 18:06
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