Differences to MiniRust (aka the idealized interpreter)

[RalfJung]

MiniRust is basically an idealized Miri. There are many differences between the two that stem from the fact that Miri is a tool you can actually use, but some differences end up being observable during program execution and those are Miri bugs or pragmatic hacks to paper over lack of a properly designed language feature -- basically, if we can fix them all, then Miri becomes a reference interpreter for Rust! But until then, Miri's results have more grains of salt than just "there could be implementation bugs".

• #2181
• #2182
• #845
• Exposed provenance does not work as intended yet; this is tracked separately in #2133
• MiniRust does not impose requirements on place construction, and hence always allows addr_of!(*ptr). Miri requires places to be dereferenceable, and hence makes that expression UB for some choices of ptr. This is currently deliberate; we'll want to be sure we really want to allow such code before adjusting Miri. (Also see rust-lang/opsem-team#9: Rust and Miri will follow MiniRust.)
• MiniRust allows zero-sized accesses through all aligned pointers, no matter their provenance, and correspondingly also allows offset(0) on all pointers. Miri currently still rejects this. This is required to ensure provenance monotonicity. (Also see rust-lang/opsem-team#10: Rust and Miri will follow MiniRust offset semantics once we depend on an LLVM that documents this as allowed. For actual accesses we still need to decide if we also want to do this, see rust-lang/opsem-team#12.)
• MiniRust allows offset_from on two pointers with equal address no matter their provenance. Miri currently rejects this. rust-lang/rust#124921 should fix that on the Miri side.
• On a function call, the exact moment that we protect a place for in-place passing matters, and MiniRust and Miri are not consistent here.

More fundamentally, whenever there is non-determinism, Miri has a hard time. Ideally Miri would explore every possible MiniRust execution with some non-zero probability, but that is not currently the case:

• Allocation base addresses are not assigned completely arbitrarily
• Preemption of concurrent threads happens only at the end of each basic block, not after each access to global state
• "Guessing" a suitable provenance over-approximates the actually allowed set of programs

Additionally, Stacked Borrows is full of hacks (from the &mut Unpin situation to the magic retagging for return places, not to mention two-phase borrows and extern types), so breaking changes should be expected in the aliasing model.

And finally, until we have a proper operational weak memory model, we cannot even say whether our data race detection and weak memory load emulation precisely matches the spec.