Change array permissions to contain shapes #1484
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 30 commits
August 31, 2021 12:27
…made the translation of bitvector permissions to just be bitvectors
…pes with no return value
… be converted to unit, not to the empty struct
…tly to the expected LLVM type
…a HeapsterEnv into a single function which iterates through the globals and adds those it can handle
…enerated LLVM files
…macro, because that seems to be the proper way to do things
…ons with different fields using the SImpl_LLVMArrayContents rule; to get the translation of the SImpl_LLVMArrayContents to work correctly, I had to change local implications to not use strict tuples, which in turn required changing the translation of lowned permissions (which are themselves local implications) to not use strict tuples as well
… prover can map array permission contents
added 20 commits
September 24, 2021 07:49
…-conjunctive permissions returned by implElimLLVMBlock; added pretty-printing and typing information for the names bound by local implications
… of defined permissions
…e local implication used to prove array contents!
…nerate the sub-array being borrowed, and to only take the borrows from the larger array that could overlap with the sub-array; Added cases to prove field permissions from arrays of smaller strides; added more debug information
…t from the sub-array instead of those the could overlap with it
… a tag first, thereby reducing the cases in which they bottom out into general disjunctions
…tImplBlock delete all the BVRanges of perms on the left-hand size from the BVRange of the right-hande side, and then creating blocks with existentially-quantified shapes for those ranges
…lockPermToField and llvmBlockPermToArray, because these do not take the current partial substitution into account
…ng the recent merge
…example that no longer work
m-yac
added
the
subsystem: heapster
m-yac
reviewed
Oct 19, 2021
m-yac
approved these changes
Oct 19, 2021
There was a problem hiding this comment.
Looks good to me, with the caveat that I really only glanced through large portions of the changes in Permissions.hs and SAWTranslation.hs as well as basically all of Implication.hs, simply because I'm not comfortable enough with what happens in these files to understand the changes being made. That being said, my understanding that is for a lot of the changes in this PR, there was only one way to adapt the existing code to use the new form of arrays. Plus, all the array examples work, which is the benchmark for correctness at the moment.
eddywestbrook
added
the
PR: ready to merge
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 LLVM array pointer permissions each array cell is described by an arbitrary LLVM shape, rather than as a sequence of field permissions.