Borrow checker doesn't account for reads from `Proje... | rust-lang/rust

Nobody has claimed this yet.

This requires custom MIR to reproduce, but in theory the borrow checker should be capable of correctly handling this. Feel free to close if this is not the case.

#![feature(core_intrinsics, custom_mir)]
#![allow(internal_features)]

use core::intrinsics::mir::*;

// Passes borrowck but fails in Miri because `b[a]` reads `a` which invalidates `x`.
#[custom_mir(dialect = "built")]
pub fn foo(mut a: usize, mut b: [usize; 10]) {
    mir! {
        {
            let x = &mut a;
            // Miri evaluates these from left to right, so a is read first.
            b[a] = *x;
            Return()
        }
    }
}

// Same issue
#[custom_mir(dialect = "built")]
pub fn bar(mut a: usize, mut b: [usize; 10]) -> usize {
    mir! {
        {
            let x = &mut a;
            // Miri evaluates these from left to right, so a is read first.
            // Changing this to `*x + b[a]` fixes the issue.
            RET = b[a] + *x;
            Return()
        }
    }
}

fn main() {
    foo(0, [0; _]);
    bar(0, [0; _]);
}

Miri error from foo

error: Undefined Behavior: attempting a read access using <301> at alloc158[0x0], but that tag does not exist in the borrow stack for this location
  --> src/main.rs:13:13
   |
13 |             b[a] = *x;
   |             ^^^^^^^^^ this error occurs as part of an access at alloc158[0x0..0x8]
   |
   = 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: <301> was created by a Unique retag at offsets [0x0..0x8]
  --> src/main.rs:9:5
   |
 9 | /     mir! {
10 | |         {
11 | |             let x = &mut a;
...  |
16 | |     }
   | |_____^
help: <301> was later invalidated at offsets [0x0..0x8] by a read access
  --> src/main.rs:13:13
   |
13 |             b[a] = *x;
   |             ^^^^^^^^^
   = note: stack backtrace:
           0: foo
               at src/main.rs:13:13: 13:22
           1: main
               at src/main.rs:34:5: 34:19
   = note: this error originates in the macro `::core::intrinsics::mir::__internal_remove_let` which comes from the expansion of the macro `mir` (in Nightly builds, run with -Z macro-backtrace for more info)

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

Miri error from bar

error: Undefined Behavior: attempting a read access using <301> at alloc158[0x0], but that tag does not exist in the borrow stack for this location
  --> src/main.rs:27:13
   |
27 |             RET = b[a] + *x;
   |             ^^^^^^^^^^^^^^^ this error occurs as part of an access at alloc158[0x0..0x8]
   |
   = 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: <301> was created by a Unique retag at offsets [0x0..0x8]
  --> src/main.rs:22:5
   |
22 | /     mir! {
23 | |         {
24 | |             let x = &mut a;
...  |
30 | |     }
   | |_____^
help: <301> was later invalidated at offsets [0x0..0x8] by a read access
  --> src/main.rs:27:13
   |
27 |             RET = b[a] + *x;
   |             ^^^^^^^^^^^^^^^
   = note: stack backtrace:
           0: bar
               at src/main.rs:27:13: 27:28
           1: main
               at src/main.rs:35:5: 35:19
   = note: this error originates in the macro `::core::intrinsics::mir::__internal_remove_let` which comes from the expansion of the macro `mir` (in Nightly builds, run with -Z macro-backtrace for more info)

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

Start by running the custom MIR examples for foo and bar, then compare the borrow checker's treatment of ProjectionElem::Index with Miri's left-to-right evaluation. Trace the borrow-checking path for the index read and validate that the examples no longer pass borrowck while producing the reported Miri error.

Written by the indexing model from the issue text.

Borrow checker doesn't account for reads from `ProjectionElem::Index`

Description

Contributor guide

First steps

Research direction

Assessment