Heapster rust string lits #1504
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
…ng the recent merge
…example that no longer work
…sion on the lhs when appropriate
…(bv) permissions, since they seem to be used to lengths of arrays, which Heapster needs to know at type-checking time
…e implication prover
…nd field permission
… by the array shape length when it should not (thanks to MattY for finding this!)
eddywestbrook
added
the
subsystem: heapster
m-yac
approved these changes
Nov 11, 2021
| @@ -91,6 +93,13 @@ import Debug.Trace | |||
| -- * Utility Functions and Definitions | |||
| ---------------------------------------------------------------------- | |||
|
|
|||
| -- | FIXME: put this somewhere more appropriate | |||
There was a problem hiding this comment.
Any objections to me making an issue in GaloisInc/parameterized-utils asking if they would be interested in adding this function?
There was a problem hiding this comment.
Sure, that makes sense. Let's leave it here for now and remove it if they accept the change there.
| [w_term, elem_tp, transTerm1 ptrans_cell] in | ||
| [w_tm, elem_tp, transTerm1 ptrans_cell] | ||
| -} | ||
| applyOpenTermMulti (globalOpenTerm "Prelude.repeatBVVec") |
There was a problem hiding this comment.
Should we remove singletonBVVec from the Prelude now since it's no longer used?
There was a problem hiding this comment.
I dunno, I feel like we should leave it there as I guess a sort of documentation...?
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.
More work trying to support Rust string literals, though this PR does not quite get it all the way there... :(
This PR changes the interpretation of string literals, as defined by the
translateLLVMValuefunction, to generate equality permissions for string literals. This was needed for Rust string literals because the lengths of LLVM globals for Rust slices seem to be stored as strings; e.g., the length of a 4-element slice is stored as the string literal"\04\00\00\00", and the Heapster type system needs to know this value in the permissions. Thus, this PR causes Heapster to translate every string literal of some sizeNto a pointer permission to anN-byte field whose contents are an equality permission to anN-byte word. E.g., a symbol "foo" that is defined to be a string literal for the string "bar" is now translated under this PR to have permissionptr((W,0,24) |-> eq(6713199)), where 6713199 is the decimal value of 0x666f6f, 0x66 is the ASCII code for "f", and 0x6f is the ASCII code for "o".Most of the time, however, string literals are just used as arrays of bytes. This requires these large, N-byte pointer permissions to be split up into N individual byte pointer permissions. Implementing this is most of the work of this PR. Specifically, this PR adds the following implication rules:
SImpl_SplitLLVMWordFieldsplits a pointer permission to a single wordwinto two consecutive pointer permissions to wordsw1andw2such that concatenatingw1++w2equalsw;SImpl_ConcatLLVMWordFieldsgoes the other way, concatenating two consecutive pointer permissions to wordsw1andw2into a single pointer to their concatenationw1++w2;SImpl_SplitLLVMTrueFieldsplits a pointer to atruepermission into two smaller consecutive pointers totrue; andSImpl_ConcatLLVMTrueFieldsconcatenates two consecutive pointer permissions totrueinto a single pointer totrue.