Add a magic comment syntax to set MIRIFLAGS #781

saethlin · 2022-02-23T01:34:54Z

I really want to be able to set MIRIFLAGS when running code in the playground. The community Discord uses a bot that accesses the playground and we use it for demos. It's a real bummer that any time -Zmiri-tag-raw-pointers is required to demonstrate something, we can't use the bot. I don't think changing the defaults is a particularly good option either, because we may want to make a point about the impact of -Zmiri-tag-raw-pointers. And I recently added -Zmiri-backtrace which should be left as its default, but in a pinch can remove backtraces entirely to make the output fit in Discord message length limit.

thomcc · 2022-02-23T16:43:01Z

Related, but probably is more difficult to handle (and can't be bolted on here): #698

RalfJung · 2022-02-23T18:30:15Z

ui/src/sandbox.rs

            let mut cmd = self.docker_command(None);
            cmd.apply_edition(req);

+            let miri_env =
+                if let Some((_, flags)) = env_settings.iter().find(|(k, _)| k == &"MIRIFLAGS") {
+                    format!("MIRIFLAGS={} -Zmiri-disable-isolation", flags)


Changing the flags like this seems potentially confusing, in particular a flag like this that can heavily affect debugging (since it introduces non-determinism).

If people can set their own flag I am not sure if we even still need the default flag?

That's a good point.

I'm concerned that if this flag is removed by default, that people will find programs that used to work and don't anymore. How would we direct them to add the magic comment? I can definitely add something to the help page, but is that enough?

Stuff already breaks on the playground over time, as crate versions change. I especially hope there's nobody relying on miri-in-playground not changing in any real way...

Edit: That said, I do kind of think -Zmiri-disable-isolation makes sense to be on by default in the playground, since it's already sandboxed.

If you want to be really fancy, when Miri shows the error saying "pass -Zmiri-disable-isolation to run this operation", the playground could turn that into a link that adds the relevant magic command. ;) The playground has such links for other situations. Those are easier though since here, if there already is a MIRIFLAGS comment, one has to now change the existing comment...

I could probably handle most cases. Would it be better to do this edit which is almost always correct, or append something to the output that points to documentation? Both options seem sort of bad in slight ways. I like that currently the playground just echoes cargo output.

danielhenrymantilla · 2022-02-28T17:09:18Z

ui/src/sandbox.rs

@@ -280,6 +281,27 @@ fn set_execution_environment(
    cmd.apply_backtrace(&req);
 }

+fn parse_magic_comments(code: &str) -> Vec<(&'static str, String)> {
+    lazy_static::lazy_static! {
+        pub static ref MIRIFLAGS: Regex = Regex::new(r#"(///|//!|//)\s*MIRIFLAGS\s*=\s*(.*)"#).unwrap();


An outer attribute seems weird, here:

Suggested change

pub static ref MIRIFLAGS: Regex = Regex::new(r#"(///|//!|//)\s*MIRIFLAGS\s*=\s*(.*)"#).unwrap();

pub static ref MIRIFLAGS: Regex = Regex::new(r#"(//!|//)\s*MIRIFLAGS\s*=\s*(.*)"#).unwrap();

/// MIRIFLAGS=-Zmiri-tag-raw-pointers fn main() { }

seems plausible to me. My instinct here is to err on the side of accepting as much as possible, because I think the only alternative we have is silently ignoring things.

I agree... whenever I use magic comments on ui tests I am nervous that they might be silently ignored.

So, the thing is that:

#![feature(…)] /// MIRIFLAGS=-Zmiri-tag-raw-pointers fn main() {

would fail, IIUC, since it wouldn't be the first-line of a file. And I can imagine the transition from your snippet to mine occurring quite easily, especially given that

/// MIRIFLAGS=-Zmiri-tag-raw-pointers #![feature(…)] fn main() {

would not be valid Rust.

I'd rather have Miri start saying with which MIRIFLAGS it is being run (which seems like a nice addition overall), rather than have an outer attribute be accepter where an inner one should be used: it is all too reminiscent of:

//! src/lib.rs #[forbid(unsafe_code)] use …; fn foo… /* actually allowed to use `unsafe`! */

would fail, IIUC, since it wouldn't be the first-line of a file.

Hm... good point. Playground will also add feature lines at the very top of the snippet when you click the error message that complains about a missing feature gate.

I think #![feature(...)] is pretty problematic here. I was afraid magic comments would run into this kind of complexity.

Parsing the magic comment on lines other than the first makes some sense in response to this, but then we run into this:

// This example works totally fine by default. But it breaks if we set // MIRIFLAGS=-Zmiri-tag-raw-pointers fn main() { 🤦 }

I agree that Miri should report its configuration somewhere.

Other things we could do...

Add a new UI element. I don't really want to do this because it's a lot of work, and also MIRIFLAGS is quite unique in that it needs to be provided as an environment variable when cargo-miri is run. All other build options we would want as arguments to cargo rustc.

Try to parse the first comment line without leading whitespace. Is it sufficiently unlikely to accidentally set MIRIFLAGS this way?

I don't think this is unreasonable. It's not like people are shipping code using the playground, and this seems to be quite an edge case (https://grep.app/search?q=//%20MIRIFLAGS and https://cs.github.com/?scopeName=All+repos&scope=&q=%22%2F%2F+MIRIFLAGS%22 say enough of one that it doesn't exist in open source rust code).

@thomcc Can you clarify what exactly "it" is here?

I don't think this is unreasonable.

Parsing the magic comment on lines other than the first makes some sense in response to this, but then we run into this...

The issue you are describing here.

I think it's fine if that turns on that MIRIFLAG

ui/src/sandbox.rs

Noratrieb · 2022-06-16T15:59:53Z

Any updates on this?

Add a magic comment syntax to set MIRIFLAGS

73f7c7c

RalfJung reviewed Feb 23, 2022

View reviewed changes

Don't default to diabling isolation, but demo it in docs

e1c07ef

danielhenrymantilla approved these changes Feb 28, 2022

View reviewed changes

saethlin added 2 commits February 28, 2022 17:01

Parse magic comment on lines after the first if they are not indented

605f1fe

Accept the comment anywhere

0e47158

saethlin mentioned this pull request Oct 9, 2023

Inlining causes miscompilation of code that mixes target features rust-lang/rust#116573

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add a magic comment syntax to set MIRIFLAGS #781

Add a magic comment syntax to set MIRIFLAGS #781

saethlin commented Feb 23, 2022

thomcc commented Feb 23, 2022

RalfJung Feb 23, 2022 •

edited

Loading

saethlin Feb 23, 2022

thomcc Feb 23, 2022 •

edited

Loading

RalfJung Feb 23, 2022

saethlin Feb 23, 2022

danielhenrymantilla Feb 28, 2022

saethlin Feb 28, 2022

RalfJung Feb 28, 2022

danielhenrymantilla Feb 28, 2022

RalfJung Feb 28, 2022

saethlin Feb 28, 2022 •

edited

Loading

thomcc Feb 28, 2022

saethlin Feb 28, 2022

thomcc Feb 28, 2022

thomcc Feb 28, 2022

Noratrieb commented Jun 16, 2022

	pub static ref MIRIFLAGS: Regex = Regex::new(r#"(///\|//!\|//)\sMIRIFLAGS\s=\s(.)"#).unwrap();
	pub static ref MIRIFLAGS: Regex = Regex::new(r#"(//!\|//)\sMIRIFLAGS\s=\s(.)"#).unwrap();

Add a magic comment syntax to set MIRIFLAGS #781

Are you sure you want to change the base?

Add a magic comment syntax to set MIRIFLAGS #781

Conversation

saethlin commented Feb 23, 2022

thomcc commented Feb 23, 2022

RalfJung Feb 23, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thomcc Feb 23, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

saethlin Feb 28, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Noratrieb commented Jun 16, 2022

RalfJung Feb 23, 2022 •

edited

Loading

thomcc Feb 23, 2022 •

edited

Loading

saethlin Feb 28, 2022 •

edited

Loading