So it looks like the defects that miri can detect overlaps heavily with the existing sanitizers (but I see at least one language-specific constraint that isn't covered by sanitizers). I suppose it's nice not to have the hassle/complexity of the sanitizers (especially nice not to have to deal with the ODR noise from UBSan), but is the intent that miri could find much beyond what the sanitizers could?
Regarding aligned accesses: does miri consider the alignment constraints of the most restrictive target? Or are there language specifications regarding alignment?
To my uneducated eye, it looks like many/most of these defects that miri detects require unsafe to cause (barring compiler defects). Is that accurate?
> is the intent that miri could find much beyond what the sanitizers could?
Miri serves two purposes. One of them is completely unrelated to this stuff, and that's to deal with const functions.
This stuff, on the other hand, yes. Those tools don't know anything about the language themselves. Miri is able to model the exact rules that we lay out for pointer usage. This means that it should be a lot better, not only at finding things, but also stuff like error messages, eventually.
> Regarding aligned accesses: does miri consider the alignment constraints of the most restrictive target? Or are there language specifications regarding alignment?
Because it's an interpreter, miri can run like any target. That said, I'm not 100% sure that 'cargo miri' exposes this easily yet; I gave it a shot but it's giving me an interesting error. The idea is that you'd specify the target you're testing for.
> To my uneducated eye, it looks like many/most of these defects that miri detects require unsafe to cause (barring compiler defects). Is that accurate?
Yes. Safe code should never produce undefined behavior, that's a hard design constraint of Rust.
> is the intent that miri could find much beyond what the sanitizers could?
I believe so. AIUI miri is checking that the code follows a formally specified definition of what is defined behavior, at least as far as the memory model goes (it doesn't check data races for instance). While it can't say that on any input your program doesn't hit undefined pointer behavior, it can say with certainty that the execution it ran through did not (w.r.t. the memory model).
Here's an example of some code that miri does catch, and where ubsan doesn't catch the closest translation I could make of it to C, despite both containing undefined behavior. If you just run the code (at least with debug settings on the current stable) it does what you would naively expect despite the undefined behavior.
Try sticking a `println!("Hello");` statement at the start of main, it will get run before we run into this error.