clarify semantics of ConstantIndex MIR projection by RalfJung · Pull Request #131285 · rust-lang/rust (original) (raw)
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service andprivacy statement. We’ll occasionally send you account related emails.
Already on GitHub?Sign in to your account
Conversation6 Commits1 Checks6 Files changed
Conversation
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
[ Show hidden characters]({{ revealButtonHref }})
This documents what Miri does:
| if n < min_length { |
|---|
| // This can only be reached in ConstProp and non-rustc-MIR. |
| throw_ub!(BoundsCheckFailed { len: min_length, index: n }); |
| } |
I am not sure what exactly the purpose of this min_length field is, TBH... but this seems like the most obvious meaning it could have?
r? @cjgillot
rustbot has assigned @cjgillot.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.
Use r? to explicitly pick a reviewer
Status: Awaiting review from the assignee but also interested parties.
Relevant to the compiler team, which will review and decide on the PR/issue.
labels
It's only meaningful use is in borrowck, where it's used to check conflict between two ConstantIndex projections.
@bors r+ rollup
📌 Commit f0ddc7b has been approved by cjgillot
It is now in the queue for this repository.
Status: Waiting on bors to run and complete tests. Bors will change the label on completion.
and removed S-waiting-on-review
Status: Awaiting review from the assignee but also interested parties.
labels
What exactly needs to be true about the semantics of this for whatever borrowck is doing to be sound?
If we can declare this field as being entirely irrelevant for the semantics, that'd surely make things a bit simpler, but then borrowck couldn't "trust" its value.
When checking conflict between [+offset1 of min_length1] and [-offset2 of min_length2], borrowck can conclude they are disjoint if offset1 + offset2 < max(min_length1, min_length2). If that inequality is not verified, the places may point to the same memory.
bors added a commit to rust-lang-ci/rust that referenced this pull request
…iaskrgr
Rollup of 5 pull requests
Successful merges:
- rust-lang#130555 ( Initial support for riscv32{e|em|emc}_unknown_none_elf)
- rust-lang#131280 (Handle
rustc_interfacecases ofrustc::potential_query_instabilitylint) - rust-lang#131281 (make Cell unstably const)
- rust-lang#131285 (clarify semantics of ConstantIndex MIR projection)
- rust-lang#131299 (fix typo in 'lang item with track_caller' message)
r? @ghost
@rustbot modify labels: rollup
rust-timer added a commit to rust-lang-ci/rust that referenced this pull request
Labels
Status: Waiting on bors to run and complete tests. Bors will change the label on completion.
Relevant to the compiler team, which will review and decide on the PR/issue.