How does inline assembly and the physical machine fit into the abstract machine model, or exist outside of it?

I think Ralf is arguing that your freeze is different because it always modifies the data, whereas a real freeze only modifies the data if it was uninit.

Ralf, is that right?

But…

You're arguing that @newpavlov's asm! example is currently impossible to "rationalize".

But what does it mean to be impossible to rationalize? Does that mean UB?

[Well, actually the example is definitely UB, because it loads from memory while being marked nomem. But I assume that's just a mistake. Let's pretend nomem is removed. Is it still UB?]

I think you are arguing yes, it is UB, because it would violate what future "MIR-level compiler optimizations" may "assume"?

That seems pretty alarming to me. The asm block can be assigned a well-defined AM state transition function. If you do a case analysis, it's easy to show why the asm block would obey that function for the init case, for the uninit case, and for every possible partially-uninit case. And of course, for each case, the state transition function for that case can be simulated in pure Rust.

But because the overall state transition function can't be simulated in pure Rust, the asm block is UB anyway?

If so, that seems like an argument for adding freeze to the language, to avoid adding UB to what seems to be perfectly well-behaved asm.

I don't know if there are any other situations besides freeze where an AM state transition function can be broken down into individually-simulatable cases but is not simulatable as a whole.

Not to put you on the spot, but is this really what you meant before by "every UB-free Rust program is guaranteed to never depend on the contents of uninitialized memory"?

Surely you were at least alluding to the security issue of disclosing the contents of asm-level uninitialized memory, even if you had the simulation issue in mind as well.

Or else I badly misinterpreted you.

2 Likes