Merged
Conversation
The type of the offset that can reach this rule can be unsigned or signed, depending on the method used in the source code (offset, get_unchecked). This PR makes that change, and updates the relevant tests.
#937) * When casting pointers, projections are added which adjust the type of the pointee to the target pointee type. * Some of these projections naturally cancel out against other inverse ones. The `appendP` function is adjusted to do these cancellations. * Test expectations are adjusted accordingly. The `iterator_simple` test is now passing.
`PtrToPtr` casts were mistakenly ignoring metadata `ORIGIN_SIZE` and setting it to `noMetadataSize` after the cast each time. This PR preserves the `ORIGIN_SIZE` across the cast. ### More Details This issue was discovered working with `Iterator`s, in particular the relationship between `std::slice::Iter<'_, T>::new` and `<std::slice::iter<'_, thing> as std::iter::Iterator>::next`. When iterating through a collection there was no match at the end that should of terminated iterating. An [Iter](https://github.com/rust-lang/rust/blob/3c9faa0d037b9eecda4a440cc482ff7f960fb8a5/library/core/src/slice/iter.rs#L69-L80) tracks position through the collection with 2 pointers: ```rust pub struct Iter<'a, T: 'a> { /// The pointer to the next element to return, or the past-the-end location /// if the iterator is empty. /// /// This address will be used for all ZST elements, never changed. ptr: NonNull<T>, /// For non-ZSTs, the non-null pointer to the past-the-end element. /// /// For ZSTs, this is `ptr::without_provenance_mut(len)`. end_or_len: *const T, _marker: PhantomData<&'a T>, } ``` In order to terminate `ptr == end_or_len`, however in KMIR this check was always failing due to the pointer representation: <img width="1132" height="105" alt="image" src="https://github.com/user-attachments/assets/63b4e35c-fc50-4bd5-922e-ffefc5b46dd4" /> Pointers in KMIR check equality on all metadata fields, so this equality would never pass. The correct `ORIGIN_SIZE` should be `dynamicSize(2)` as they are pointers to elements of a slice. The `Iter` is instantiated with the incorrect `ORIGIN_SIZE`. The construction of an `Iter` by the `new` function does a series of pointer casts. The cast that strips the `ORIGIN_SIZE` in KMIR came from `_5 = Cast-PtrToPtr mv(6)` which is a cast of `*mut Thing` to `*const Thing`: <img width="754" height="986" alt="image" src="https://github.com/user-attachments/assets/165c3156-333d-4b3e-b89e-0108882b5e44" />
Collaborator
Author
|
I accidentally pushed to this branch after resolving the conflicts and bypassed the CI checks. There is a manual run here https://github.com/runtimeverification/mir-semantics/actions/runs/22151035614 |
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
BinOp::Offsettests MoreBinOp::Offsettests #935PtrToPtrcast Fix metadata onPtrToPtrcast #941