Support `StatementKind::PlaceMention`

[N1ark]

Though a comment in Charon's driver seems to imply StatementKind::PlaceMention is there "only to make borrow-checking accept less code", which is not entirely true I think. In particular it requires the place to be valid, so one of the projections may be invalid within and this UB is lost if we compile this statement away. In MiniRust this statement is mentioned so I'm not sure we can avoid it.

This is an exemple of UB code that we would miss:

let p = {
    let b = Box::new(42);
    &*b as *const i32 as *const (u8, u8, u8, u8)
};
unsafe {
    let _ = (*p).1; //~ ERROR: in-bounds pointer arithmetic failed
}

There are a few Miri tests that I believe check for exactly this, i.e. a tool using Charon cannot pass them:

• https://github.com/rust-lang/miri/blob/fa8b9658497810f5ee5db69b437b062fbc5e527c/tests/fail/dangling_pointers/dangling_pointer_project_underscore_let.rs
• https://github.com/rust-lang/miri/blob/fa8b9658497810f5ee5db69b437b062fbc5e527c/tests/fail/dangling_pointers/dangling_pointer_project_underscore_let_type_annotation.rs
• https://github.com/rust-lang/miri/blob/fa8b9658497810f5ee5db69b437b062fbc5e527c/tests/fail/dangling_pointers/dangling_pointer_project_underscore_match.rs

[N1ark]

(I'm happy to quickly add this once I have the time! I would like avoiding adding an additional statementkind but I don't think there's a clean way to mention a place without side effects).

[Nadrieril]

Interesting, I was not aware of that! I thought PlaceMention was removed in runtime MIR but looking through rustc I see a -Zmir-preserve-ub flag that keeps it! So I agree with you, I'd like to have the statement and we should set this flag also.