[Language Lawyer] Is this Undefined Behavior?

help
1

Hi every one

In the code below, I use unsafe code to obtain mutable and immutable references at the same time.

My question: Is it undefined behavior? Can the compiler just assume z does not change and print 0 in both statements?

Thanks.

fn main() {
    let mut x = 0;
    let ptr: *mut i32 = &mut x;
    let y = unsafe { &mut *ptr };
    let z = &x;

    println!("before : {}", z);
    *y += 1;
    println!("after  : {}", z);
}
2

Yes. The mere existence of a mutable and immutable reference to the same thing is UB.

It might not print anything at all. Or 100. Or segfault. Or make your computer catch on fire.
Undefined really means undefined.

6 Likes
3

The best way to resolve this would be to run the code example under MIRI, which you can do from a web browser using the Playground.

This is the output I get from running it (miri is in the Tools menu):

   Compiling playground v0.0.1 (/playground)
    Finished dev [unoptimized + debuginfo] target(s) in 0.91s
     Running `/playground/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/bin/cargo-miri runner target/miri/x86_64-unknown-linux-gnu/debug/playground`
error: Undefined Behavior: attempting a read access using <3121> at alloc1664[0x0], but that tag does not exist in the borrow stack for this location
 --> src/main.rs:8:5
  |
8 |     *y += 1;
  |     ^^^^^^^
  |     |
  |     attempting a read access using <3121> at alloc1664[0x0], but that tag does not exist in the borrow stack for this location
  |     this error occurs as part of an access at alloc1664[0x0..0x4]
  |
  = help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
  = help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <3121> was created by a Unique retag at offsets [0x0..0x4]
 --> src/main.rs:4:22
  |
4 |     let y = unsafe { &mut *ptr };
  |                      ^^^^^^^^^
help: <3121> was later invalidated at offsets [0x0..0x4] by a SharedReadOnly retag
 --> src/main.rs:5:13
  |
5 |     let z = &x;
  |             ^^
  = note: BACKTRACE (of the first span):
  = note: inside `main` at src/main.rs:8:5: 8:12

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to previous error
8 Likes
4

Thank you for your answer and for showing me such a powerful tool like this.

5

Be warned that Miri has false negatives, so using it doesn't constitue proof of soundness. If Miri says it's UB then it's UB, but if Miri says it's OK, then it might still be UB.

1 Like
6

Technically, if Miri says it's UB, it may turn out ok. It even warns in some cases that its rules are not final. But in this simple case it's definitely UB.

1 Like
7

It may later be reclassified as defined behavior, but right now it is still treated as undefined.

2 Likes
8

Even more importantly, miri will only detect UB that’s actually encountered, whereas “soundness” is concerned with all UB that could possibly be encountered by using potentially hard to find corner-case inputs to the function/API in question.

Furthermore, certain kinds of (almost-)UB tend to not manifest at all, for example a program incorrectly relying on the layout of structs (without an explicit repr(C) or repr(transparent)).[1]

  1. I believe if run-time checks for the struct size and field offsets in questions would be added, it’s actually even possible to manipulate such structs’ memory soundly, but without such checks, it’s UB that could actually appear at least with newer compiler versions in the future, if not even some way in current compilers. ↩︎

9 Likes
9

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.