Skip to content

Allow user to specify aliasing model for Miri #1074

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 and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Mar 4, 2025

Conversation

GoldsteinE
Copy link
Contributor

Very useful for comparing stacked borrows and tree borrows.

An example for testing:

fn main() {
    let val = [1u8, 2];
    let ptr = &val[0] as *const u8;
    let _val = unsafe { *ptr.add(1) };
}

is valid under Tree Borrows, but not under Stacked Borrows.

UI looks like this:

image

@GoldsteinE GoldsteinE changed the title Allow user to specify aliasing mode for Miri Allow user to specify aliasing model for Miri Jul 22, 2024
@GoldsteinE
Copy link
Contributor Author

The one problem I have with my implementation is that this knob is not saved when sharing via link. I could easily fix this, but it will add an extra &aliasing_model=stacked at the end of every single URL. Alternatively, I could make “Share” omit unchanged parameters, but I suppose there’s a reason why it isn’t this way already.

@GoldsteinE
Copy link
Contributor Author

@shepmaster Hi! Looking at the commit history, I think I should ask you to review these changes.

@shepmaster shepmaster added the CI: approved Allowed access to CI secrets label Mar 3, 2025
@shepmaster
Copy link
Member

this knob is not saved when sharing via link

I think that's fine for now. Similarly, the "backtrace" configuration is not added as a query parameter.

I suppose there’s a reason why [“Share” does not omit unchanged parameters]

That's basically to avoid dealing with changing defaults. For example, if you click on a playground link from the year 2015, it will not have the edition query parameter since editions did not exist yet. That means that the value for a missing edition needs to forever be 2015. Moving forward, we always add the edition parameter even when the edition matches the current default, as the default changes over time.

In this case, Miri defaults to stacked borrows today, but conceptually could switch to tree borrows tomorrow. A URL generated today with no value would become ambigous if loaded tomorrow.


All that said, I've been mulling over a richer way of saving data about the current playground instance. If enough interest arises from people missing this setting sticking around, I might look into that.

@shepmaster
Copy link
Member

shepmaster commented Mar 3, 2025

Thanks for your patience! The code looks good, but I did pull it down and make some small tweaks, as well as rebasing it to address some conflicts. I then force-pushed those changes. Due to that, your two commits are no longer verified. If that's OK with you, I can go ahead and merge this. Otherwise, feel free to review the commits then rebase them and force-push yourself with the new approvals.

The updated UI

image

@shepmaster shepmaster added CI: approved Allowed access to CI secrets and removed CI: approved Allowed access to CI secrets labels Mar 3, 2025
@GoldsteinE
Copy link
Contributor Author

All that said, I've been mulling over a richer way of saving data about the current playground instance. If enough interest arises from people missing this setting sticking around, I might look into that.

The thing I find myself missing the most is the state of the big “Run” button: I often want to share some code in ASM or LLVM IR mode and right now the best way to do it is to just specify it in prose. (Aside: I think “Expand macros”, “Miri” and “Clippy” could also be under the “Run” button instead of in “Tools”). I don’t think not saving Miri mode is that bad, since it’s mostly useful for comparing Miri modes, so you’ll need to switch it anyway.

Due to that, your two commits are no longer verified. If that's OK with you, I can go ahead and merge this. Otherwise, feel free to review the commits then rebase them and force-push yourself with the new approvals.

Give me a minute, I’ll review and re-sign these commits.

@GoldsteinE
Copy link
Contributor Author

I signed the commits (adding you as a co-author for the second one).

@RalfJung
Copy link
Member

RalfJung commented Mar 4, 2025

We usually spell the tool's name "Miri", would be good to be consistent here as well. :)

@RalfJung
Copy link
Member

RalfJung commented Mar 4, 2025

Ah, seems like the section titles are generally all-caps... I guess this will lead to more people spelling it MIRI but oh well.

@shepmaster
Copy link
Member

Ah, seems like the section titles are generally all-caps

If it makes you feel any better, I do spell it the right way in the pre-stylized code 😉 :

<MenuGroup title="Miri">

I feel your pain though, albeit in the opposite direction. I generally prefer SNAFU to be in all caps as it's an acronym, but most people pick something else.

This has the side benefit of not exceeding the width of the config
widget.
@shepmaster shepmaster added CI: approved Allowed access to CI secrets and removed CI: approved Allowed access to CI secrets labels Mar 4, 2025
GoldsteinE and others added 2 commits March 4, 2025 18:51
`#!/bin/bash` is non-standard and doesn't work on e.g. NixOS.
@shepmaster
Copy link
Member

Tests passed

@shepmaster shepmaster merged commit ae0b81d into rust-lang:main Mar 4, 2025
@shepmaster shepmaster added the enhancement Something new the playground could do label Mar 4, 2025
@shepmaster
Copy link
Member

Thank you for your patience.

@RalfJung
Copy link
Member

RalfJung commented Mar 4, 2025 via email

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CI: approved Allowed access to CI secrets enhancement Something new the playground could do
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants