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

Heapster bugfixes for sha512 example #1523

Merged
merged 11 commits into from
Nov 23, 2021
Merged

Heapster bugfixes for sha512 example #1523

merged 11 commits into from
Nov 23, 2021

Conversation

eddywestbrook
Copy link
Contributor

This PR fixed the following Heapster bugs, that were found while trying to get the sha512 example to type-check in Heapster. Note that that example does not yet type-check fully, but these bug fixes are useful to Heapster in general so we are merging them now:

  • changed tcJumpTarget to freshen up the argument names in any jump, as both the type-checker and translator rely on all arguments being distinct variables

  • changed the translation of calls to multi-entry blocks so they no longer accumulate Hobbits variables from the caller

  • removed an infinite loop in splitLLVMBlockPerm when it is called on a block with the empty shape

@eddywestbrook eddywestbrook added the subsystem: heapster Issues specifically related to memory verification using Heapster label Nov 23, 2021
@eddywestbrook eddywestbrook requested a review from m-yac November 23, 2021 19:25
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.

This looks great! Since your change to tcJumpTarget made foldrAndBuildDistPerms obsolete, I'm going to remove it. But once that's committed this should be ready to merge.

heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs Outdated Show resolved Hide resolved
@m-yac m-yac added PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run and removed PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run labels Nov 23, 2021
@m-yac m-yac 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 Nov 23, 2021
@mergify mergify bot merged commit 4570404 into master Nov 23, 2021
@mergify mergify bot deleted the heapster/sha512-bugfixes branch November 23, 2021 22:51
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