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

Add support to validity checks in the presence of copy_nonoverlapping, copy. #3762

Open
Tracked by #3203
celinval opened this issue Dec 5, 2024 · 0 comments
Open
Tracked by #3203

Comments

@celinval
Copy link
Contributor

celinval commented Dec 5, 2024

These intrinsics can affect the value of a place that may be read later using safe code. It is not immediate UB to write the value to the allocation space, but it would be to later use it with a type T where the value written is not valid.

E.g.:

use std::ptr;

/// # Safety
/// - Users must not read from `ptr` until a new valid value is written to it
unsafe fn copy_invalid_char(ptr: &mut char) {
    let invalid_value: u32 = 0xDE01;
    // SAFETY: This is
    unsafe { ptr::copy(&invalid_value, ptr as *mut _ as *mut u32, 1) };
}

/// This checks that there is no UB if the user ensures that a valid character is written before next read.
#[cfg_attr(kani, kani::proof)]
fn check_no_ub() {
    let mut c = 'a';
    // SAFETY: We will write to `c` before reading it again
    unsafe { copy_invalid_char(&mut c) };
    c = 'b';
    assert_ne!(c, 'a');
}

/// This checks that there is UB if a read exposes the invalid value.
#[cfg_attr(kani, kani::proof)]
fn check_with_ub() {
    let mut c = 'a';
    // SAFETY: This is not safe and it will trigger UB
    unsafe { copy_invalid_char(&mut c) };
    assert_ne!(c, 'a');
}

// Run this with MIRI
#[cfg(miri)]
fn main() {
    check_no_ub();
    check_with_ub();
}
@celinval celinval changed the title Intrinsics: copy_nonoverlapping, copy. Add support to validity checks in the presence of copy_nonoverlapping, copy. Dec 5, 2024
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

1 participant