Heapster: duplicate read memblocks #1505
Merged
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
added 6 commits
November 10, 2021 14:47
…time of a permission
…ed when they are used
…o duplicate read-only memblock permissions when they are used by a proof, so that Rust shared references can be duplicated in code; updated recombinePerm to handle this possibility by dropping redundant memblock perms or part of memblock perms that are redundant; also updated implEndLifetimeM to drop conjuncts that are relative to the just-ended lifetime
…ing Rust reference duplication
…termined variables as part of simplifying them, in case they contain non-determined variables that are provably equal to determined ones
m-yac
approved these changes
Nov 11, 2021
m-yac
added
the
subsystem: heapster
eddywestbrook
added
the
PR: ready to merge
added 2 commits
November 11, 2021 15:56
…well as logic to drop redundant fields when they are recombined
…r; also added a case to simplify1PermForDetVars to generalize eq(llvmword e) perms when e has undetermined vars
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.
This PR changes the implication prover (specifically in
proveVarLLVMBlocks) to duplicate read-onlymemblockpermissions when they are used by a proof, so that Rust shared references can be duplicated in code. As part of supporting this change, this PR also:recombinePermto handle this possibility by dropping redundantmemblockperms or parts ofmemblockperms that are redundantimplEndLifetimeMto drop conjuncts that are relative to the just-ended lifetime, which could cause therecombinePermchange to drop necessarymemblockperms in favor ofmemblockperms whose lifetimes have endeddouble_dup_reffunction to the rust_data example to exercise type-checking Rust reference duplicationsimplifyPermsForDetVarsto cast the permissions on determined variables as part of simplifying them, in case they contain non-determined variables that are provably equal to determined ones