3 ms·

> As a starting example, here's some code that Miri reports as violating Rust's rules for references So...this was determined statically? Or "statically"? If

> As a starting example, here's some code that Miri reports as violating Rust's rules for references So...this was determined statically? Or "statically"? If there's no/few false positives could this be used as a check in rustc? Or clippy? BTW for this one specifically, why can't we look at the AST and see that a and b alias? EDIT: I guess it's because it's lost in the deref/take addr?

gpm 8y ago
It was determined dynamically, determining it statically with no false positives is impossible. Try sticking a `println!("Hello");` statement at the start of main, it will get run before we run into this error.
- wyldfire 8y ago
  > It was determined dynamically 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?
  - steveklabnik 8y ago
    > 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.
  - gpm 8y ago
    > 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. https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=ec01c06f7a415a66d6c83b56e47561d5 https://play.rust-lang.org/?version=stable&mode=debug&editio...
steveklabnik 8y ago
Miri is an interpreter, and so it works dynamically. Think ubsan. > why can't we look at the AST and see that a and b alias? The exact aliasing rules for raw pointers are under discussion at the moment. We may be able to look at the AST in this case, but in some cases, that requires control flow analysis. ASTs aren't great for this, but MIR is built around it, hence miri. (That said, I don't think that's the primary reason Miri works on MIR, it's more that MIR is kinda like "core Rust", the simplest possible expression of the language itself.)

gpm 8y ago

It was determined dynamically, determining it statically with no false positives is impossible. Try sticking a `println!("Hello");` statement at the start of main, it will get run before we run into this error.

wyldfire 8y ago
> It was determined dynamically 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?
- steveklabnik 8y ago
  > 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.
- gpm 8y ago
  > 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. https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=ec01c06f7a415a66d6c83b56e47561d5 https://play.rust-lang.org/?version=stable&mode=debug&editio...

steveklabnik 8y ago

Miri is an interpreter, and so it works dynamically. Think ubsan. > why can't we look at the AST and see that a and b alias? The exact aliasing rules for raw pointers are under discussion at the moment. We may be able to look at the AST in this case, but in some cases, that requires control flow analysis. ASTs aren't great for this, but MIR is built around it, hence miri. (That said, I don't think that's the primary reason Miri works on MIR, it's more that MIR is kinda like "core Rust", the simplest possible expression of the language itself.)