Pointer cast #1564
Merged
Pointer cast #1564
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
This produces a new setup value that points to the same location, but is assumed to point to values of the provided type. This is useful when, e.g., verifing code that contains `union` values inside structs, as the type provided by the bitcode will not accurately reflect all the intended uses. It may also be useful for other "polymorphic" C programming styles.
It is only used in the LLVM mode, and I'd like to make some changes. It is unclear that having this be shared code is worthwhile.
This check is necessarily approximate, and the system may miss incompatible resolved values if overlapping regions are resolved through different pointer casts. This should not be a soundness issue, as the verification will fail at a later point instead (albeit, with less-useful information provided to the user).
This plays more nicely with `llvm_field`, as alias information is retained longer.
…re function, similar to `llvm_field`, `llvm_elem`, etc.
robdockins
force-pushed
the
pointer-cast
branch
from
4dca5af to
cda04b1
Compare
|
I plan to add a unit test, but I think this is otherwise ready to go. |
RyanGlScott
reviewed
Feb 9, 2022
The new form still needs to be piped through the Python client.
|
I'm not sure I have the necessary context to pipe the new pointer cast form through the Python client code. |
RyanGlScott
approved these changes
Feb 9, 2022
There was a problem hiding this comment.
I'm not sure I have the necessary context to pipe the new pointer cast form through the Python client code.
I've opened #1575 to track this.
robdockins
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 implements a new
llvm_cast_pointeroperation for setup blocks. It allows the user to specify that a pointer should be treated as a pointer to a given llvm type, despite the information contained in its initial allocation site.This is primarily intended to make it easier to work with unions, as the type information provided by the LLVM bitcode in these cases is not terribly useful.