Verus checking code in some external_body functions

[hayley-leblanc]

Hi folks, I'm writing some code involving MaybeUninit in external_body functions and have found that Verus is incorrectly checking the bodies of some of these functions. The specific case I encountered involves obtaining a mutable reference to a MaybeUninit object; attempting to verify an external_body function that does this results in a verification error about &mut not being supported.

An example of such a function that does not verify:

#[verifier::external_body]
fn test_maybe_uninit() {
    let mut maybe_uninit: MaybeUninit<u64> = MaybeUninit::uninit();
    let mut bytes: &mut [MaybeUninit<u8>] = maybe_uninit.as_bytes_mut();
    let new_bytes: [u8; 8] = [0, 0, 0, 0, 0, 0, 0, 0];
    MaybeUninit::write_slice(bytes, &new_bytes);
}

Attempting to verify this function results in error: The verifier does not yet support the following Rust feature: &mut types, except in special cases.

This does not happen with all external_body functions involving mutable references; for example, this function verifies as expected:

#[verifier::external_body]
fn test_vec() {
    let mut vec = vec![1, 2, 3];
    let mut bytes: &mut [u8] = vec.as_mut_slice();
    let new_bytes: [u8; 3] = [0, 0, 0];
    bytes.copy_from_slice(&new_bytes);
}

Both functions are implemented at https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=a677a25cc24042da30e69c076811d4c1

I also noticed that removing #[verifier::external_body] from test_maybe_uninit() results in a different error: error: The verifier does not yet support the following Rust feature: &mut dereference in this position (note: &mut dereference is implicit here)

[Chris-Hawblitzel]

This may be related to #657 .

[Chris-Hawblitzel]

For anyone who encounters this, the current recommended workaround is to move the code into an external function, called by the external_body function:

#[verifier::external]
fn test_maybe_uninit_external() {
    let mut maybe_uninit: MaybeUninit<u64> = MaybeUninit::uninit();
    let mut bytes: &mut [MaybeUninit<u8>] = maybe_uninit.as_bytes_mut();
    let new_bytes: [u8; 8] = [0, 0, 0, 0, 0, 0, 0, 0];
    MaybeUninit::write_slice(bytes, &new_bytes);
}
    
#[verifier::external_body]
#[inline(always)]
fn test_maybe_uninit() {
    test_maybe_uninit_external()
}