Why does Miri not complain?

[SUPERCILEX]

#![feature(c_str_literals)]
#![feature(ptr_from_ref)]

use std::cell::*;
use std::ffi::*;
use std::mem::*;
use std::ptr;

fn call<F: FnOnce()>(ff: *mut (), just_drop: bool) {
    let f = unsafe { ff.cast::<F>().read() };
    println!("size {}", size_of::<F>());
    f();
    let z = unsafe { ff.cast::<F>().read() }; // VERY BAD!!!
    z();
}

pub fn main() {
    let mut a = Vec::new();
    a.push(0);
    let f = || { // Add move to get miri to detect the UAF
        println!("yo {:?}", a);
    };
    foo(f);
}

fn foo<F: FnOnce()>(f: F) {
    let mut f = ManuallyDrop::new(f);
    let fn_ptr = call::<F> as *const ();
    let fns = unsafe { transmute::<_, fn(*const (), bool)>(fn_ptr) };
    fns(ptr::from_mut(&mut f).cast(), false);
}

I'm working on a task scheduler (so that involves very gnarly unsafe code) and I was hoping to be able to rely on Miri, but it seems to require drop types to be able to detect nastiness. The code above passed Miri, but will start failing only if you move the Vec into the closure.

[bjorn3]

It doesn't complain because F is a Copy type and thus can be copied using ptr.read() without issue. You can prove this by adding an where F: Copy bound to foo and call and observing that it compiles just fine. Miri can only detect UB for a concrete execution path of a concrete instantiation of a function. Miri is not an abstract interpreter or formal verification system capable of answering the question if your code is correct for all possible invocations.

[SUPERCILEX]

Miri is not an abstract interpreter

Ah, for some reason I thought this was the case. Are there good patterns to use that will increase the likelihood of Miri catching bugs then? Having your unsafe code use a type that contains an allocation seems like a good trick, but maybe there are others?

[oli-obk]

I guess just having good code coverage. It's always a good idea to fuzz your code or at least quickcheck/proptest it.

You can try using tools like the Kani model checker to find more test cases for you.

But when it comes to testing generic unsafe code, right now we don't have good guidelines beyond being your own worst user and thinking about the possible mis-uses that could happen

[RalfJung]

Indeed Miri tests for UB, not soundness. We're open to suggestions for how to better document this, but things are working as intended here.

Proving soundness is a really hard problem and I am not aware of any tool that can do it -- you need to do manual proofs in RustBelt. Various tools mentioned above can help find more bugs, though.

[SUPERCILEX]

Thanks for the suggestions!

We're open to suggestions for how to better document this

Minimal code examples of what Miri is able to catch vs what it isn't would probably be helpful. And maybe a link to how Miri works so you can figure out the full set of things Miri will be able to catch.

[RalfJung]

That sounds like way too much for a readme.^^ We can maybe add a sentence or two to the initial paragraphs that introduce Miri.

Miri can catch UB. The problem here isn't a lack of documentation of what Miri does / how it works, the problem is missing the distinction between UB and soundness -- which maybe we can preempt with a short note in the readme? That was my hope anyway. Assuming anyone reads the readme. ;)
See this talk for more discussion of that distinction.