Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Possible false positive of stacked borrow rules #3657

Closed
saecki opened this issue Jun 8, 2024 · 1 comment
Closed

Possible false positive of stacked borrow rules #3657

saecki opened this issue Jun 8, 2024 · 1 comment

Comments

@saecki
Copy link

saecki commented Jun 8, 2024

/// # SAFETY
/// At least `additional` bytes are required inside the source string after the `lit` slice.
pub unsafe fn extend_str_back(lit: &str, additional: usize) -> &str {
    let ptr = lit.as_ptr();
    let len = lit.len() + additional;
    let slice = std::slice::from_raw_parts(ptr, len);
    std::str::from_utf8_unchecked(slice)
}

fn main() {
    let input = "hello ";
    let slice = &input[0..5];
    let extended = unsafe { extend_str_back(slice, 1) };
    dbg!(slice);
    dbg!(extended);
}

The code above fails with the following message:

   Compiling miri_stacked_borrow_repro v0.1.0 (/home/tobi/Projects/miri_stacked_borrow_repro)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.07s
     Running `/home/tobi/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/bin/cargo-miri runner target/miri/x86_64-unknown-linux-gnu/debug/miri_stacked_borrow_repro`
error: Undefined Behavior: trying to retag from <2561> for SharedReadOnly permission at alloc1181[0x5], but that tag does not exist in the borrow stack for this location
   --> /home/tobi/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/raw.rs:107:9
    |
107 |         &*ptr::slice_from_raw_parts(data, len)
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |         |
    |         trying to retag from <2561> for SharedReadOnly permission at alloc1181[0x5], but that tag does not exist in the borrow stack for this location
    |         this error occurs as part of retag at alloc1181[0x0..0x6]
    |
    = 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: <2561> was created by a SharedReadOnly retag at offsets [0x0..0x5]
   --> src/main.rs:4:15
    |
4   |     let ptr = lit.as_ptr();
    |               ^^^^^^^^^^^^
    = note: BACKTRACE (of the first span):
    = note: inside `std::slice::from_raw_parts::<'_, u8>` at /home/tobi/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/raw.rs:107:9: 107:47
note: inside `extend_str_back`
   --> src/main.rs:6:17
    |
6   |     let slice = std::slice::from_raw_parts(ptr, len);
    |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
note: inside `main`
   --> src/main.rs:13:29
    |
13  |     let extended = unsafe { extend_str_back(slice, 1) };
    |                             ^^^^^^^^^^^^^^^^^^^^^^^^^

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

error: aborting due to 1 previous error

Is the unsafe code not quite right, or is this a false positive?

@saethlin
Copy link
Member

saethlin commented Jun 8, 2024

This is not a false positive. The ranges printed by the diagnostics are exclusive on the end, like Rust ranges. 0..5 does not include 5.

Alternatively if you mean you think that Stacked Borrows should be changed to accept this code, that's part of what Tree Borrows is for. Set MIRIFLAGS=-Zmiri-tree-borrows to use that model instead. Your code is trying to do the &Header pattern: rust-lang/unsafe-code-guidelines#256

I'm closing this because it is not a bug in Miri (which essentially does not have false positives), but I don't want to discourage you from asking further questions about this situation or diagnostic.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants