Skip to content

Miri disables debug_assertions in std, and so misses some library UB it could be reporting #2497

Closed
@asquared31415

Description

@asquared31415

Miri should not disable debug_assertions in std (it should in fact explicitly enable them) to improve the detection of bugs in programs, even when they are not language level UB, "only" library UB.

std has several additional library invariants that are not language level UB, for example Vec's len being less than or equal to its capacity, slice::get_unchecked needing an index that is in bounds in element count not just bytes (the case where the resulting byte index is out of bounds is handled by other language rules), CStr::from_bytes_with_nul_unchecked having a trailing null byte and no interior null bytes, and String containing UTF-8 bytes. Some of these conditions are checked by std using debug assertions, specifically a macro that when debug_assertions are enabled, aborts when the condition fails. When debug_assertions are disabled, it conditionally compiles out to a no-op. Currently Miri disables debug_assertions explicitly, noting that it helps performance. I know nothing about this performance nor have I tested performance with or without debug_assertions.

As a concrete example, the following code:

fn main() {
    let _foo = unsafe { *[()].get_unchecked(1) };
}

passes miri with no warnings or errors currently (nightly 2022-08-18), however, it fails to complete execution successfully under a -Zbuild-std with debug_assertions enabled, aborting due to an illegal instruction caused by the abort.

Modifying Miri to enable the flag produces an error, which, even though it's not optimal, is much better than nothing. This error could also be improved with cooperation from std to improve the debug checks.

error: abnormal termination: the program aborted execution
   --> .rustup/toolchains/miri/lib/rustlib/src/rust/library/core/src/slice/index.rs:225:13
    |
225 |             assert_unsafe_precondition!(self < slice.len());
    |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the program aborted execution
    |
<snip trace through std internals>
note: inside `main` at src/main.rs:2:26
   --> src/main.rs:2:26
    |
2   |     let _foo = unsafe { *[()].get_unchecked(1) };
    |                          ^^^^^^^^^^^^^^^^^^^^^
    = note: this error originates in the macro `assert_unsafe_precondition` (in Nightly builds, run with -Z macro-backtrace for more info)

This, with no other modifications, raises an error, points to the code the user passed, mentions assert_unsafe_precondition, and has the condition that failed, which should tell the user to check that they're satisfying the unsafe conditions of the function they're calling. This is a sufficient, but not ideal error.

std could also benefit from an additional pass over unsafe conditions for debug checks. Currently most of the checks are on pointer-like operations. The Vec example given above, and Strings's UTF-8 bytes and several other cases of library-only UB are not checked even in debug mode. This would have even more benefit if Miri also ran those checks by enabling debug_assertions.

I would be willing to add these assertions and improve the output from the failure of these checks under Miri.

Downsides

  • Running debug assertions is running more code, which inherently will have some cost.

  • Several debug assertions check things that Miri would already check via language UB, such as the slice::get_unchecked case but for a T that is not zero sized. Importantly, in these cases that Miri would have already checked, the error gets worse since it's now an abort. (!!this is really bad!!)

I believe that there could be a workaround to have certain language level UB not be asserted on if it would already be checked in Miri, but it would be more complicated, involve manually determining whether an unsafe condition causes language or library UB, and being conservative with assertions if it could be both.

Metadata

Metadata

Assignees

No one assigned

    Labels

    C-proposalCategory: a proposal for something we might want to do, or maybe not; details still being worked out

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions