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: existential function output perms #1549

Merged
merged 18 commits into from
Dec 23, 2021

Conversation

eddywestbrook
Copy link
Contributor

This PR adds existential ghost variables to the output of a function permission, so that now the general form of a function permission looks like this:

(x1:tp1, ..., xn:tpn). arg0:p0, ..., argm:pm, x1:p1', ..., xn:pn
-o (z1:tp1, ..., zk:tpk). arg0:p0'', ..., x1:p1''', ..., ret:p, z1:p1'''', ...

This change was needed to support Rust functions that return structs or other data structures that contain pointers with lifetimes as subterms. For example, a function that returns a slice type like &'a str actually returns a struct with a length and a pointer in lifetime 'a, and the pointer needs a variable, which we can now list in the output ghost variables, in order to reference it in the returned lifetime ownership permission.

As an added bonus, this PR also fixes lownedPermVarAndPerm, lownedPermsVars, and lownedPermsToDistPerms to accommodate for offsets on variables, thereby removing errors when ending lifetimes with offset variables in the lowned permissions.

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

LGTM, though I wasn't able to review the changes in RustTypes.hs beyond just general Haskell style since I don't know what goes on in that file. I did have a couple questions so I'm not hitting "Approve" yet.

heapster-saw/src/Verifier/SAW/Heapster/Parser.y Outdated Show resolved Hide resolved
heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs Outdated Show resolved Hide resolved
heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs Outdated Show resolved Hide resolved
@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 Dec 23, 2021
@mergify mergify bot merged commit d012ffe into master Dec 23, 2021
@mergify mergify bot deleted the heapster/existential-fun-out-perms branch December 23, 2021 23:11
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