Document the current MIR semantics that are clear from existing code

[JakobDegen]

This PR adds documentation to places, operands, rvalues, statementkinds, and terminatorkinds that describes their existing semantics and requirements. In many places the semantics depend on the Rust memory model or other T-Lang decisions - when this is the case, it is just noted as such with links to UCG issues where possible. I'm hopeful that none of the documentation added here can be used to justify optimizations that depend on the memory model. The documentation for places and operands probably comes closest to running afoul of this - if people think that it cannot be merged as is, it can definitely also be taken out.

The goal here is to only document parts of MIR that seem to be decided already, or are at least depended on by existing code. That leaves quite a number of open questions - those are marked as "needs clarification." I'm not sure what to do with those in this PR - we obviously can't decide all these questions here. Should I just leave them in as is? Take them out? Keep them in but as // instead of /// comments?

If this is too big to review at once, I can split this up.

r? rust-lang/mir-opt

[JakobDegen]

I've left a bunch of FIXME's in here. I may try and get to some of them before merging, but they should all be non-critical and can just be added later.

The test change has a relevant Zulip conversation

Also, I didn't add anything for SetDiscriminant pending #95125 . If we decide against such a change, I'll put up a PR documenting the current semantics

[bjorn3]

A place stores an address and an optional meta value.

[JakobDegen]

Yeah, this is probably the right thing to have. That being said, I'm going to leave this open until I get a chance to more thoroughly go through all of the documentation and deal with DSTs (or probably someone else should do that because I know very little about it)

[bjorn3]

I think it should be left undefined in which order theybare evaluated.

[JakobDegen]

I've changed the ordering question to a "needs clarification" section in an effort to only document things which are already decided.

That being said, I don't think this is a good option. First of all, I'm not sure "order is left indeterminate" implies "any attempt on depending on the order is UB" - it might be the case that we instead get two distinct well-defined possibilities. More importantly though, this doesn't feel like a thing that MIRI can implement, which is concerning.

I also can't produce an example, but I would not be surprised if this is actually required for current Rust, since the evaluation order in Rust is well-defined. I can't get MIR building to produce such MIR, but it would at least imply that the temporaries produced by this are required:

pub fn foo(a: &mut i32) -> i32 {
    let derived = &mut *a;
    *derived + *a
}

[bjorn3]

intrinsics may be codegened in the future.

[JakobDegen]

Indeed. I think at that point this check should be refined to verify those bodies that do get codegened only. Even better would be if code elsewhere got changed to stop passing intrinsics that don't get codegened through the MIR validator. cc @oli-obk

[bjorn3]

Miri should be made to match whatever is decided. It is currently very relaxed.

[bjorn3]

I think order should be left indetermimate so any attempt on depending on the order is UB.

[JakobDegen]

(see the comment above - basically the same concerns apply here)

[RalfJung]

I think leaving evaluation order indeterminate is a bad idea. We should specify some order eventually, and probably it should be left-to-right. (That's what Miri does.)

The disjointness thing can be enforced without leaving the order indeterminate, using the aliasing model instead. That's better because it can be checked by Miri.

[bjorn3]

Must not alias the place given to any Operand::Move passed as argument. All codegen backends depend on this property to allow passing Operand::Move by reference in case of a type not fitting inside registers without having to male a copy on the stack or having to restrict the callee to not mutate the value.

[JakobDegen]

I've added in a mention of that in the "needs clarification" section above. Based on the status of the linked issue, it seems that it is still unclear how we are justifying that optimization

[JakobDegen]

cc @RalfJung - want to check that everything written here (of specific concern is the place and operand stuff) is at least compatible with your model of MIR

[RalfJung]

FWIW I think "place to value conversion" is a terrible term, though I know it is standard in C. This operation accesses memory! It shouldn't be described as if it was a simple cast.

So I'd say something more along the lines of: it evaluates the LHS and RHS to places, loads a value from the place denoted by the RHS, and then stores that value into the place denoted by the LHS.

But also, this doesn't even do place-to-value conversion? The RHS is evaluated to a value, and that is stored to the place denoted by the LHS.

[RalfJung]

I don't think CFG paths are relevant. What's relevant is the actual sequence of statements that are executed when the function runs. There's basically a boolean flag dead-or-alive for each local that starts out 'dead' for locals with annotations, and that is set appropriately by these annotations. Accessing (evaluating the place expression) of a local is UB if it is currently 'dead'.

Actually it's more than that, each StorageLive allows the local to be put at a different location in memory.

[JakobDegen]

I don't think CFG paths are relevant

Well, because of the MaybeStorageLiveLocals in the validator, this is already the case. Certainly CFG paths should not be relevant in the spec/miri, but the docs here have to also mention what is required by the validator, which might have a stronger opinion

[tmiasko]

I think the storage check currently present in the validator should be considered to be merely a debugging aid. It is possible to write unsafe code that uses local when it does not have storage. With additional optimizations present such code would fail the check. When we get to that point the check should be disabled.

[JakobDegen]

Ah, this is a good point. With the current setup, we can't turn *r into x even if we know that r = &mut x;, because that might turn UB into an ICE. I'll mention this in the documentation

[scottmcm]

Come to think of it, we should probably mention that we often don't want to "remove" UB in MIR optimizations in general, since keeping it visible to the codegen backend is important.

For example, we don't want to lower switchInt [0 => bb3] otherwise: bbUnreachable to goto bb3, since that keeps LLVM from knowing about the impossible condition.

[JakobDegen]

Yeah, these kinds of things should definitely be documented, but imo not here. I do want to start an organized way of defining "canonicalized MIR" at some point, because I think that will be increasingly important, and this seems like the kind of thing to include there

[RalfJung]

Note that this operation can cause UB: the crated place must be dereferencable and suitably aligned, as determined by its type.

[RalfJung]

That's what Miri does, and I think it is the right model.

[RalfJung]

Ah now this is the right place for the rant that I put earlier. ;)

I don't think we should all this a "conversion". That sounds like an as cast, like just putting something into a different representation. That's not at all what happens though. This is a load from memory, and should be described as that.

[oli-obk]

@bors r+

[bors]

📌 Commit 8732bf5 has been approved by oli-obk