Heapster array field implications #1459
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 16 commits
September 14, 2021 06:47
…Vecs instead of SAW core Vecs
…ixed up that for BVSext
…tuples of 2 or more types; updated foldList and unfoldList in the SAW core Prelude to fit this new approach; regenerated the resulting Coq files
eddywestbrook
added
the
subsystem: heapster
added 8 commits
September 15, 2021 17:28
…f existential shapes as arbitrary expressions
… all the mbox proofs work...
m-yac
approved these changes
Sep 17, 2021
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 extends the Heapster implication prover to apply permission implication to the fields of array permissions. That is, it allows proving an implication
x:array(off, <len, *stride, [fld1,...,fldn]) -o x:array(off, <len, *stride, [fld1',...,fldn'])by proving that
y:fld1 * ... * fldn -o y:fld1' * ... * fldn'. This required revisiting the oldSImpl_LLVMArrayContentsrule (which was not used before this PR) and updating it so that it uses a local permission implication, a concept that was created forlownedpermissions.This change also required revisiting how local permission implications are translated. Specifically, local implications
x1:p1,...,xn:pn -o y1:q1,...,ym:qmpreviously tupled the translations of the input and output permissions using strict tupling, which maps the list of types[T1,...,Tn]to the right-nested tuple typeT1 * (T2 * ... * (Tn * #())), with the tupling operation that leaves off the final unit type, i.e., that maps a list of types to the typeT1 * (T2 * ... * (Tn-1 * Tn)).The following minor changes were also added as part of this PR: