Clarify the definition of undefined behavior

[gnzlbg]

I think we should clarify in the definition of undefined behavior that:

• While this document (and the reference) often call out the behavior that is undefined, the behavior that is not explicitly defined in these documents is also undefined.

• Undefined behavior cannot be assumed to remain undefined.

To expand on this second point, we currently say that creating a &mut T with value 0 is undefined behavior, but we guarantee that this will always be undefined behavior (because the type has a niche), and therefore, this code is sound:

fn foo(x: &mut T) { unsafe {
   if transmute(x) == 0_usize {
      *std::ptr::null() // never invokes UB
   }
}}

Now follow me in this thought experiment, and imagine that, instead of guaranteeing that &mut T are never 0, we were just to say that creating a &mut T with value 0 is UB.

Would the example above be sound? I don't think so, because we could, in a future release of Rust, make this undefined behavior defined in such a way that would make that code unsound. For example, we could say that creating a &mut T with value 0 is ok, but dereferencing it panics, and that change in the language from undefined to defined behavior would break the code above.

That is, while the compiler can assume that undefined behavior never happens when optimizing Rust code, users cannot assume that undefined behavior will remain undefined when writing Rust code. The only thing users can assume are things that we guarantee.

If we want to say that some behavior is undefined, and that behavior will remain undefined forever, such that users can assume that it never happens, we need to word that as a guarantee, and breaking that guarantee would be a backward incompatible change.

So maybe we need to split our lists of undefined behavior into behaviors that are just undefined, and behaviors that are guaranteed to be undefined.

[RalfJung]

While this document (and the reference) often call out the behavior that is undefined, the behavior that is not explicitly defined in these documents is also undefined.

I think that is one of the worst possible definitions of UB.
IMO, it is a spec bug if the spec does not cover a case. That's just like having a non-exhaustive match. A mathematical definition has to cover all cases, otherwise it is not a valid definition. The same goes for a proper spec.

[gnzlbg]

So what do we call behavior not defined in the spec then ?

[gnzlbg]

Or are you suggesting that the spec is not valid until it becomes complete ?

[RalfJung]

"Not yet specified behavior"? It's basically a white spot on the map. That's very different from UB, for which there should be a precise (and conscious) definition. UB is where we know there are dragons; a white spot is where there might be dragons or not.

[RalfJung]

Or are you suggesting that the spec is not valid until it becomes complete ?

Not sure what you mean by "valid", but is certainly not complete until there are no more missing cases.

[gnzlbg]

"Not yet specified behavior"?

This sounds good to me.

Not sure what you mean by "valid", but is certainly not complete until there are no more missing cases.

You mentioned that:

A mathematical definition has to cover all cases, otherwise it is not a valid definition. The same goes for a proper spec.

So I asked whether this means that you consider any incomplete spec invalid. As in, if the spec is not complete, it is not a valid Rust spec, and nothing in it applies to Rust.

I don't think doing that would be very useful, because AFAIK there might never be a complete spec for Rust (this is a practical / engineering problem). Even if at some point the spec would be believed to be complete, any tiny detail that would make it incomplete would render it invalid (e.g. new nightly feature is added to Rust without spec wording, now nothing in the spec applies to nightly Rust anymore).

I think it would be more useful to say that the spec does not defines the behavior of all well-formed Rust programs because there is some behavior that has not yet been specified, but if you have a program for which the spec defines all of its behavior, then you can use the spec to reason about it.

[gnzlbg]

As in, the spec can tell you what some well-formed programs do or whether some well-formed programs have UB, but at least right now there definitely are well-formed programs for which the spec can't tell you what they do or whether they have UB or not because the behavior of these programs is not specified.

---

I worry a bit that "not-specified-behavior" is too similar to "unspecified behavior". There is a difference between unspecified behavior that's required not to be undefined, and unspecified behavior that could be undefined.

[Diggsey]

To expand on this second point, we currently say that creating a &mut T with value 0 is undefined behavior, but we guarantee that this will always be undefined behavior (because the type has a niche), and therefore, this code is sound:

It's the other way around: the spec says that a &mut T must refer to a valid T and as a result creating one with value 0 is UB.

It doesn't make sense for the spec to say "this is UB now but might not be UB in future" or for the spec to say "this is UB and will stay UB forever" - the spec describes rust at a point in time.

We can then take two versions of the spec and ask whether a newer one is backwards compatible with an older one: if something is UB in a previous version then it can continue to be UB or its behaviour may be defined in the newer version.

However, if the old spec says "&mut T must refer to a valid T" and the new spec relaxes that, then the new spec cannot be backwards compatible.

TLDR. "UB" already means "we are saying nothing about the behaviour in this case", and there's no reason to introduce a term to say "we will never say anything about the behaviour in this case" because that's not a useful thing to say - it restricts what we can do for no reason.

[hanna-kruppe]

@RalfJung

I think that is one of the worst possible definitions of UB.
IMO, it is a spec bug if the spec does not cover a case. That's just like having a non-exhaustive match. A mathematical definition has to cover all cases, otherwise it is not a valid definition. The same goes for a proper spec.

I agree that it is generally better to explicitly state when something is UB than risk declaring something reasonable UB by mistakenly not covering it. However, a spec is only a model of reality, and neither can nor should exhaustively list everything that could possibly happen in reality that might be relevant to the operation of a Rust program. So there's always going to be vast stretches of things that people might reasonably want to do, but which the spec (and implementation documentation) doesn't give any guarantees or even guidance about. Since these things often interact with the parts that are covered by the spec in non-trivial ways, it's not hard get something indistingushable from de jure UB (assumed not to happen by implementations, non-local and time-travelling effects, has cascading and arbitrarily bad consequences, etc.).

Clearly, it's overly conservative to declare everything not explicitly covered by the spec to be UB: many reasonable things that need to happen in real systems and work perfectly fine fall under that. But "it's probably UB" is a safer default answer and just calling these things "not specified" does not properly convey the distinction between "we'll get back to you" and "you're on your own and probably stuff will break". For example, if someone has a question about a tricky interplay of raw pointers and &mut's, we can say we don't yet have a finalized memory model so it's not settled yet. If someone does very funky stuff with page tables and linker scripts, I wouldn't call it a spec bug if the spec doesn't tell them if they're in the clear.

I'd also like to note that "we don't specify what this does" is not really any more restricted than "it's UB" because the thing it might do is causing UB. So it's not like people can look at the spec, see that the thing they want is "not specified", and then can feel justified in doing it. It's really just UB by a less scary-sounding name.

[gnzlbg]

We can then take two versions of the spec and ask whether a newer one is backwards compatible with an older one: if something is UB in a previous version then it can continue to be UB or its behaviour may be defined in the newer version.

@Diggsey If undefined behavior becomes defined, the safe and sound Rust API of the thought experiment becomes unsound.

There are dozens of places in the reference, nomicon, and the UCGs where we say that something is undefined.

For a concrete example, we used to say that the behavior of unwinding out of an extern "C" functions is undefined. That is, the following safe and stable Rust API is sound (it never invokes UB):

pub fn bar(x: extern "C" fn()) {
    if catch_unwind(|| x()).is_err() { unsafe { /* UB */ } }
}

If we were to "fix" that UB in the reference, by saying that "unwinding out of an extern "C" function is ok" (which feels like a perfectly reasonable thing that we should be able to do if we wanted), then that stable, safe, and sound Rust API becomes unsound. That would be a serious backward incompatible change.

I think we should be able to remove "X is UB" from the reference, and for that, we need to forbid users from relying on things being UB to write code like the above.

[Diggsey]

If undefined behavior becomes defined, the safe and sound Rust API of the thought experiment becomes unsound.

Undefined behaviour becoming defined is not what causes that example to become unsound. It becomes unsound because the spec previously said that &mut T referred to a valid T`, and the new version does not guarantee that, which is a breaking change.

[gnzlbg]

It becomes unsound because the spec previously said that &mut T referred to a valid T`, and the new version does not guarantee that, which is a breaking change.

I think you are focusing too much on the &mut T example instead of trying to understand the issue I'm trying to raise.

[Diggsey]

OK, to take your unwinding example, I don't believe that code is sound to begin with.

pub fn bar(x: extern "C" fn()) {
    if catch_unwind(|| x()).is_err() { unsafe { /* UB */ } }
}

You can't negatively reason about UB in this way. Just because the spec doesn't define what the behaviour of unwinding is, a specific compiler implementation on specific hardware may define that behaviour to be something sensible, or a future version of the spec may define that behaviour.

This is different from the &mut example, because in that case you are not relying on negative reasoning, you are relying on an explicit guarantee made by the spec.

edit:
If the spec explicitly said "extern C functions will never unwind" then that of course would be a different story.

[Lokathor]

It doesn't make sense for the spec to say "this is UB now but might not be UB in future" or for the spec to say "this is UB and will stay UB forever" - the spec describes rust at a point in time.

Actually a lot of people doing unsafe code really want to know the difference between "this is UB now and we're resolving to keep it always UB (at least for this edition)" compared to "this us UB now because we haven't gotten there yet, but it might change later".

[gnzlbg]

@Diggsey

You can't negatively reason about UB in this way.

Where do we say so?

[Diggsey]

Actually a lot of people doing unsafe code really want to know the difference between "this is UB now and we're resolving to keep it always UB (at least for this edition)" compared to "this us UB now because we haven't gotten there yet, but it might change later".

From the point of view of knowing about the development roadmap it might be useful. For writing unsafe rust code it can never be useful - if you have unsafe code relying on something continuing to be UB then the unsafe code is wrong.

Where do we say so?

The only purpose to declare something UB is to leave open the possibility for compiler implementations/future versions of the spec to do whatever they want. If people can apply negative reasoning and rely on the opposite then it entirely defeats the point of having UB.

Anytime you think "we should make X UB forever", it could and should be rephrased as "the spec should guarantee Y".

[gnzlbg]

The only purpose to declare something UB is to leave open the possibility for compiler implementations/future versions of the spec to do whatever they want. If people can apply negative reasoning and rely on the opposite then it entirely defeats the point of having UB.

The only reason I opened this issue is because I see this happening in Rust code and I think it is worth calling out in our definition of UB that such negative reasoning is not allowed.

Why do you think it is a bad idea to spell this out ?

[Diggsey]

I don't object to spelling it out, I object to this:

So maybe we need to split our lists of undefined behavior into behaviors that are just undefined, and behaviors that are guaranteed to be undefined.

Specifically I object to the concept of "guaranteeing something to be undefined". We should never do that. UB should always mean "we are making no guarantees".

[RalfJung]

Undefined behavior cannot be assumed to remain undefined.

This goes back to @nikomatsakis' concerns about "future-proofing" our validity invariant.

I am not sure how I feel about your choice of words here, because for any given closed program, making more behavior defined cannot break that program. What you are doing in your example is reasoning about a library, and what we do not want is to do "negative reasoning" about UB. I don't have a good concise way of expressing this, though.

So I asked whether this means that you consider any incomplete spec invalid. As in, if the spec is not complete, it is not a valid Rust spec, and nothing in it applies to Rust.

Oh I see. Well, an incomplete spec is not a valid mathematical spec, but that's fine -- it can still be useful as a (partial) Rust spec. To do anything formal (like proofs), all the holes have to be closed somehow, but that's a separate concern.

I worry a bit that "not-specified-behavior" is too similar to "unspecified behavior". There is a difference between unspecified behavior that's required not to be undefined, and unspecified behavior that could be undefined.

I think the two are actually very close. Isn't that just a quantitative difference? For "explicitly unspecified behavior", we are giving bounds on what the behavior can be, but we could in principle decide to give no bounds.

@rkruppe

However, a spec is only a model of reality, and neither can nor should exhaustively list everything that could possibly happen in reality that might be relevant to the operation of a Rust program.

I have no idea where you are going here. The spec is defined by describing the behavior of the Rust Abstract Machine. That is a discrete mathematical artifact and one can certainly do exhaustive case distinction on its states to describe its behavior.

Reality has no bearing here, we already abstracted everything away to the level we need by defining the abstract machine.

I have precisely described operational semantices of programming languages before, there is no magic here. Sure, Rust's Abstract Machine is "a bit" more complicated than what we usually work with, but that doesn't mean that somehow we couldn't or shouldn't properly define its behavior. Why would that approach suddenly fail...?

If someone does very funky stuff with page tables and linker scripts, I wouldn't call it a spec bug if the spec doesn't tell them if they're in the clear.

That's outside the scope of the spec. The Rust Abstract Machine has no page tables.

If you use volatile accesses, the Rust Abstract Machine provides an interface to communicate with "lower-level" machine models, and then you can consult those for further details.

But I think I understand now what where you are coming from. I tend to ignore all those details that are "outside" the Abstract Machine, they only make life complicated. ;)
What I feel strongly about is: if we describe some step in the abstract machine, and just neglect to say what happens in a certain case (like say some state machine can be in 5 states but we only over 4 of them), that in no way should be read as us saying the remaining cases is UB. This just means we forgot there is a fifth case to cover.

@Diggsey

Just because the spec doesn't define what the behaviour of unwinding is, a specific compiler implementation on specific hardware may define that behaviour to be something sensible, or a future version of the spec may define that behaviour.

That's not how UB works -- certainly not the part where you mention hardware. It doesn't matter that your x86 hardware says that unaligned accesses are defined; it is still UB to do unaligned accesses in Rust even when targeting only x86.

For specific compilers, the matter is somewhat different. But a compiler that defines behavior which is UB in Rust wouldn't really be a "Rust" compiler any more, we could consider this a language dialect. (I know @Centril has strong opinions on this. But then what don't they have strong opinions on? ;)

The only purpose to declare something UB is to leave open the possibility for compiler implementations/future versions of the spec to do whatever they want.

No, that's wrong. The purpose of UB is to simplify program analysis by having the programmer prove properties that would be hard for the compiler to prove.

UB used to be what you are describing it as, but it has long since changed its nature. C did not introduce TBAA because future compiler/hardware might suddenly have typed memory or some such things; TBAA was introduced to make alias analysis simpler. The same applies, for example, to noalias-induced UB in Rust.

Specifically I object to the concept of "guaranteeing something to be undefined". We should never do that. UB should always mean "we are making no guarantees".

Well, but we have some examples here where it could be useful go guarantee more. Like, we could guarantee that a NULL reference will always be invalid -- so the corresponding transmute will always be UB. That would help code like in the OP.

So, I think we should indeed consider to make some future-proofing guarantees where appropriate, if that turns out to be useful for unsafe code authors. It seems odd to refuse to declare the example program in the OP as sound.

[hanna-kruppe]

But I think I understand now what where you are coming from. I tend to ignore all those details that are "outside" the Abstract Machine, they only make life complicated. ;)
What I feel strongly about is: if we describe some step in the abstract machine, and just neglect to say what happens in a certain case (like say some state machine can be in 5 states but we only over 4 of them), that in no way should be read as us saying the remaining cases is UB. This just means we forgot there is a fifth case to cover.

I definitely agree with this, I think I'm just trying to point out that the eventual Rust spec will have to cover a fair bit more than just the abstract machine. Or at least, many reasonably questions people will ask and seek an answer to in the spec / UCG will involve such "life-complicating" matters.

[RalfJung]

Or at least, many reasonably questions people will ask and seek an answer to in the spec / UCG will involve such "life-complicating" matters.

I will forward them to you, then. ;)

On a more serious note, I am not sure if any of those deserve to be "undefined behavior". The purpose of UB is to be an assumption that the compiler can make during optimizations. To be useful as that, it needs to be precisely defined, which is decidedly not the case with all that "life-complicating mess".

Basically, if something is outside the scope of the abstract machine, I think it is also outside the scope of UB. While it may seem tempting to conflate "UB for optimizations" with "UB because we can't meaningfully specify things", I think that's a mistake as these are two very different things. They should be treated differently, and they should not both be called "undefined behavior".

---

This reminds me: I recently realized I am unhappy with statements like "transmuting Vec<u16> to Vec<[u8; 2]> is UB" (which we even say in the libstd docs). It is true that this code is "wrong" in some sense because, as the docs go on to explain, they rely on layout details that are unstable and can change any time. But there is no rule of the abstract machine (that I can imagine) that this code violates. So really I'd argue that that code relies on unspecified behavior, which fits exactly: behavior that the Rust implementation must make a concrete choice for, but that it not documented and that can also change any time. Relying on unspecified behavior is not UB, I think.

[hanna-kruppe]

Basically, if something is outside the scope of the abstract machine, I think it is also outside the scope of UB. While it may seem tempting to conflate "UB for optimizations" with "UB because we can't meaningfully specify things", I think that's a mistake as these are two very different things. They should be treated differently, and they should not both be called "undefined behavior".

I don't really understand this distinction. Many of these things, while not precisely specified, clearly are (often implicitly) assumed not to happen to enable many optimizations. To give a very clear example which actually comes up relatively frequently in reality: assuming that the floating point environment (e.g. FPU control and exception flags registers) is in its IEEE-754 mandated default state is necessary for a lot of optimizations (e.g. code motion, CSE, GVN, constant folding) to be effective for floating point operations. You can also phrase it as "we can't predict what will happen if you mess with that" (and it's true our spec won't say anything about what it means to set MSR[FE0] = 1 and MSR[FEX] = 1 on a PowerPC machine), but the main practical effect is enabling optimizations.

These optimizations are justified by the abstract machine, but only because any notion of floating point exceptions or dynamic rounding modes is out of scope [1] for the abstract machine (so that e.g. abstract-machine-fadd is a pure function of its two explicitly-given operands, it doesn't trap or set any exception flags or depend on a global, mutable rounding mode). There's no way to say precisely in terms of the abstract machine that it's UB to fiddle with this out-of-scope aspect of real computers, but people know that those parts exist and often have legitimate interest in accessing it. So it seems pretty clear to me that we have to tell them in the spec they must not do that because we rely on it not happening to enable optimizations, i.e., it's UB.

[1] Well, I hope eventually we'll grow a rough equivalent of C's FENV_ACCESS, but the example still serves as long as Rust doesn't have that.

[Diggsey]

That's not how UB works -- certainly not the part where you mention hardware. It doesn't matter that your x86 hardware says that unaligned accesses are defined; it is still UB to do unaligned accesses in Rust even when targeting only x86.

I meant that the combination of compiler and hardware may specify what happens in a situation that would be UB according to the Rust spec, not that the hardware alone would do that.

For specific compilers, the matter is somewhat different. But a compiler that defines behavior which is UB in Rust wouldn't really be a "Rust" compiler any more, we could consider this a language dialect. (I know @Centril has strong opinions on this. But then what don't they have strong opinions on? ;)

I don't agree with this at all. The definition of UB means that a compiler is allowed to do anything, including compiling the program "correctly" for some arbitrary definition of correct. A compiler that guarantees that unaligned accesses are fine on x86 is just as much a conforming Rust compiler as one that doesn't, at least until a new version of the Rust spec is released which is incompatible with that implementation choice. It is in no way deviating from the standard.

No, that's wrong. The purpose of UB is to simplify program analysis by having the programmer prove properties that would be hard for the compiler to prove.

Fair, although I intended that to be covered by "allowing compiler implementations to do whatever they want" - the fact that they have that freedom is what allows them to assume UB doesn't occur in a valid rust program, which in turn, is what makes those analyses valid to begin with.

Well, but we have some examples here where it could be useful go guarantee more. Like, we could guarantee that a NULL reference will always be invalid -- so the corresponding transmute will always be UB. That would help code like in the OP.

In this example, the only guarantee the spec needs to make is that "NULL" is not a valid reference, and will never be a valid reference. This is useful because unsafe code may rely on this property. We should not guarantee that the corresponding transmute will always be UB, because we may wish to define that transmute to do something else in future (eg. panic).

I don't believe it is ever useful for the spec to guarantee that something remain UB forever, but I welcome a counter-example.

[comex]

There's no way to say precisely in terms of the abstract machine that it's UB to fiddle with this out-of-scope aspect of real computers, but people know that those parts exist and often have legitimate interest in accessing it. So it seems pretty clear to me that we have to tell them in the spec they must not do that because we rely on it not happening to enable optimizations, i.e., it's UB.

Arguably these things need a concept of "implementation-defined as undefined". In other words, to set MSR[FE0] = 1 in the first place, you would have to use OS calls or inline assembly. From the perspective of the Rust abstract machine specification, the effects of OS calls and inline assembly are entirely out of scope; they are sort of "implementation-defined", in that they should be defined by the (semi-hypothetical) implementation specification. But then the implementation specification should say that using whatever OS call or assembly instruction sets MSR[FE0] = 1, and then returning to Rust code, results in undefined behavior.

Caveat: The C spec actually tends to avoid using the term "implementation-defined" in this manner. It mostly (though not exclusively) uses "implementation-defined" in cases where the implementation has to pick from a specific set of options, e.g. whether or not something is true, or which value of a certain type is returned in a certain case. OS calls and inline assembly instead fall into the sparsely described category of "extensions":

A conforming implementation may have extensions (including additional library functions), provided they do not alter the behavior of any strictly conforming program.

But that terminology may be too limited for Rust, which has constructs like asm! or #[link_args] where the existence of the thing is standard, but the specific details of what it does are platform- and thus implementation-dependent.

[Centril]

"Not yet specified behavior"? It's basically a white spot on the map. That's very different from UB, for which there should be a precise (and conscious) definition. UB is where we know there are dragons; a white spot is where there might be dragons or not.

True. But I think we need to also impress upon folks that relying on "not yet specified behavior" (hence: unspec) should be treated with the same seriousness as UB in terms of soundness. Basically some of what @rkruppe said in #202 (comment).

(I know @Centril has strong opinions on this. But then what don't they have strong opinions on? ;)

Lotsa things! ;) -- For example, tastes in music.

No, that's wrong. The purpose of UB is to simplify program analysis by having the programmer prove properties that would be hard for the compiler to prove.

I agree, but this does not negate the importance of providing language design with options in the future that unspec provides.

So really I'd argue that that code relies on unspecified behavior, which fits exactly: behavior that the Rust implementation must make a concrete choice for, but that it not documented and that can also change any time. Relying on unspecified behavior is not UB, I think.

If we consider the Rust Abstract Machine (hence: R-AM) to be parameterized by Cfg (for which we can define the scope & bounds of) then, can we not restate "sound" (for libraries) as "sound ∀ c: Cfg"?

A compiler that guarantees that unaligned accesses are fine on x86 is just as much a conforming Rust compiler as one that doesn't, [...]

A Rust compiler should not guarantee things which are UB or more importantly unspec that we have not explicitly decided are implementation defined. (This is more of a social issue to ensure language design options.)

[gnzlbg]

There's no way to say precisely in terms of the abstract machine that it's UB to fiddle with this out-of-scope aspect of real computers,

@rkruppe the Rust Abstract Machine could say "It is currently illegal for Rust programs to modify the floating point environment, this might change in the future". That allows the optimizer to assume it doesn't happen, and as long as safe Rust code does not provide a way to do that, the language remains sound. This also prevents portable Rust source code from relying that this will always remain this way.

That is, the abstract machine wouldn't consider the FP environment out-of-scope. It would recognize it exists, and specify how it can be used (e.g. that right now it cannot be used at all).

[hanna-kruppe]

@gnzlbg Here you are using "the Rust Abstract Machine" in a very different way than @RalfJung and I. Just saying that a thing called "floating point environment" exists and that it shall not be "modified" is completely informal. It has no connection whatsoever to the formal semantics that describe exactly how Rust programs execute (because no part of the Rust programs that exist can interact with it). So the wording you proposed can be nothing more than commentary. It is about how the abstract machine maps to real hardware, not about the abstract machine itself.

That is, unless you do all the hard work of designing an abstracted floating point environment (e.g., a set of global variables in the machine state, extra inputs/outputs to many MIR ops, etc.), exhaustively enough that anyone can recognize it's an abstraction of (insert hardware thingy here), and then say "it's UB to use any of this stuff". But this is a lot of effort to create "dead weight", vestigal specification text that is never exercised (so we don't even know if it's a good spec or completely busted) since no Rust program can use it.

[RalfJung]

@rkruppe

I don't really understand this distinction. [...]

These optimizations are justified by the abstract machine, but only because any notion of floating point exceptions or dynamic rounding modes is out of scope [1] for the abstract machine (so that e.g. abstract-machine-fadd is a pure function of its two explicitly-given operands, it doesn't trap or set any exception flags or depend on a global, mutable rounding mode). There's no way to say precisely in terms of the abstract machine that it's UB to fiddle with this out-of-scope aspect of real computers, but people know that those parts exist and often have legitimate interest in accessing it. So it seems pretty clear to me that we have to tell them in the spec they must not do that because we rely on it not happening to enable optimizations, i.e., it's UB.

If we think of what I usually call UB as an "error state in the Abstract Machine", then certainly messing with the floating point mode is not that, right? So there is some distinction here.

Formally, the floating point env issue comes up when one argues that the final assembly actually implements the Rust Abstract Machine: turns out that this is not actually "universally true" but the compiler makes some assumption on the environment when it argues that the resulting assembly is a faithful implementation of the Rust Abstract Machine for the particular input program it was compiling. Basically, we (want to) have a simulation proof relating the actual state of the real machine running the final assembly, to the state of the Rust Abstract Machine running the source program, and showing that those two "stay in sync" -- and that proof actually assumes (and preserves) some things about the real machine (like the floating point stuff, or page mappings for allocated memory not changing mid-execution) just like it assumes some things about the R-AM (such as not reaching the error state labelled "UB").

So I agree, these are assumptions, but when looking at things formally they are very different from the assumptions made with statements like "transmuting 3 to a bool is UB".

Does this help clarify the distinction?

@Diggsey

I don't agree with this at all. The definition of UB means that a compiler is allowed to do anything, including compiling the program "correctly" for some arbitrary definition of correct. A compiler that guarantees that unaligned accesses are fine on x86 is just as much a conforming Rust compiler as one that doesn't, at least until a new version of the Rust spec is released which is incompatible with that implementation choice. It is in no way deviating from the standard.

We could write the standard that way and this is certainly what C does.
But there are benefits (mostly orthogonal to this discussion) to explicitly say, for Rust, that such a compiler is not conforming: the emergence of such compilers would imply the emergence of language dialects. Programs that work fine on one compiler suddenly do not work fine on the other. To avoid ecosystem fragmentation, we might consider it useful to declare explicitly, when putting down a standard for Rust, that compilers may not provide any guarantees for what happens when things are UB.

This is more a social aspect of a UB definition than a technical one. I mentioned it for completeness sake only, but deciding about this is really orthogonal to everything else we are discussing here.

@Centril

If we consider the Rust Abstract Machine (hence: R-AM) to be parameterized by Cfg (for which we can define the scope & bounds of) then, can we not restate "sound" (for libraries) as "sound ∀ c: Cfg"?

That's my thinking indeed. Now, what exactly is Cfg? :D

[hanna-kruppe]

So I agree, these are assumptions, but when looking at things formally they are very different from the assumptions made with statements like "transmuting 3 to a bool is UB".

Does this help clarify the distinction?

I see how they have very different character in any formalization. But since you (IIUC) agree the fpenv example is an assumption necessary for optimizations, while also being something we do not (cannot reasonably) specify as part of the abstract machine, I still have trouble with the distinction I was responding to, which for reference (it's been a long thread) is this:

While it may seem tempting to conflate "UB for optimizations" with "UB because we can't meaningfully specify things", I think that's a mistake as these are two very different things. They should be treated differently, and they should not both be called "undefined behavior".

Since I've given an example of an assumption which is not specifiably (in terms of the abstract machine) but is chiefly about optimizations rather than "we just don't know what it would do", I don't know how this distinction, worded like that, is meaningful.

We can certainly distinguish different categories of assumptions made for optimizations when that is convenient for formalization or semi-formal discussion. However, I would not like to use "UB" [1] exclusively for one of these categories. You have frequently (including in the quote above) framed UB as a "contract with the compiler" and thus enabler of optimizations in the past, and I like this perspective. But from that perspective, the fp environment assumptions I've described should clearly also fall under UB, although it would not be related to any error conditions of the abstract machine and thus be a different kind of UB. This seems clearly different from a catch-all "whatever we haven't or can't specify is also UB" clause (I can understand how that would muddle the term UB beyond usefulness).

All of this is assuming we use "UB" at all, which has been called into question in some other discussions. Perhaps that provides a way out of this tedious fight over which of many competing interpretations should prevail for the term "UB"?

[gnzlbg]

If we think of what I usually call UB as an "error state in the Abstract Machine", then certainly messing with the floating point mode is not that, right?

Why not? It appears to me that we can and should say that:

• Modifying the floating-point environment triggers an error in the abstract machine
• If reading the floating-point environment does not return X (whatever we assume it to be), that's an error in the abstract machine.

And then specify that one of the things we do on program startup is reading the floating-point environment (which is something that miri could do).

[RalfJung]

But since you (IIUC) agree the fpenv example is an assumption necessary for optimizations

No I don't. :) I agree it is an assumption necessary for compilation. But optimizations transform one program running on the R-AM to another one running on the R-AM. You agree the FP env is not part of the R-AM, thus, by definition, no assumption about the FP env can ever be relevant for optimizations.

Assumptions like the ones about the FP env only come up when lowering R-AM code to a lower-level language that actually has a floating point environment. They never come up when lowering to languages like wasm that don't have an FP env either.

So, I maintain that these are two very different kinds of assumptions:

• When verifying the correctness optimizations (say, MIR-to-MIR transformations), the only machine we consider is the Rust Abstract Machine (R-AM). We have to show that the transformed program simulates the source program, but both run on the same model of computation. The only assumption we are making is that the program does not enter the error state called "UB". The R-AM has no page tables and no FP environment, so no such "environmental assumptions" can even come up here.
• When we are done transforming the R-AM program and ready to verify the pass that compiles the R-AM program to a lower-level target language, then some additional target-specific assumptions come in. Now we are proving a simulation between two different models of computation, and on top of assuming that the source program (running on the R-AM) does not enter the UB error state, we also make some suitable assumptions about the environment of the target program. These have to be determined for each target platform separately.

I hope this helps clarify why I see these two kinds of assumptions as being very different in nature.

Since I've given an example of an assumption which is not specifiably (in terms of the abstract machine) but is chiefly about optimizations rather than "we just don't know what it would do"

I'd say it is not at all about optimizations and only about how to translate the final R-AM program to assembly. (Let's ignore our middle-man LLVM for now.)

You have frequently (including in the quote above) framed UB as a "contract with the compiler" and thus enabler of optimizations in the past

That is fair; when considering the entire contract with the compiler, I suppose one could include the target-level assumptions. We would however then have to extend "enabler of optimizations" to also include "enabler of the given implementation strategy of the R-AM semantics in terms of assembly".

On the other hand, me and others have also frequently framed UB as "an error state in the abstract machine", and that quite clearly excludes anything concerning the FP environment.

[hanna-kruppe]

I hope this helps clarify why I see these two kinds of assumptions as being very different in nature.

It does, thanks.

I still maintain that, no matter what taxonomy of assumption we use for formalizations and specs, it would do users a disservice to choose terminology that casts any doubt on whether changing the rounding mode is "less bad" than e.g. transmuting 3 to bool.

Edit: to be clear, this does not mean I'm opposed to trying to communicate the distinction you draw to users, but it is a somewhat subtle point and doesn't affect most users (the end result is the same, "don't do X or rustc breaks your code"), so overly stressing it doesn't seem like a good use of time nor worth the risk of confusion.

[gnzlbg]

@RalfJung

I hope this helps clarify why I see these two kinds of assumptions as being very different in nature.

Thanks, that does clarify it, and it is related to what's discussed in rust-lang/miri#932 about UB due to incorrect usage of target-features: we make the assumption that the hardware the binary runs on is of a particular hardware architecture, has particular target features, the FP-environment configured in a particular way, etc. If the user then runs that binary on the wrong target, we make no guarantees, so that's UB, but is a different kind of UB than "an error in the abstract machine".

@rkruppe

I still maintain that, no matter what taxonomy of assumption we use for formalizations and specs, it would do users a disservice to choose terminology that casts any doubt on whether changing the rounding mode is "less bad" than e.g. transmuting 3 to bool.

I think that we should actively communicate that this different kind of UB is actually much worse. UB of the form "error in the abstract machine" is not possible in safe Rust, can be detected under miri in unsafe Rust, etc. UB of this other form cannot really be detected nor prevented. For example, if one compiles a safe Rust program for x86 and runs it on ARM, then that's UB of this other form in safe Rust, and there is nothing that we can really do about it.

[RalfJung]

@rkruppe

I still maintain that, no matter what taxonomy of assumption we use for formalizations and specs, it would do users a disservice to choose terminology that casts any doubt on whether changing the rounding mode is "less bad" than e.g. transmuting 3 to bool.

Indeed I can see that from a user perspective, it is not always helpful to distinguish between the two. But I find it important that for the deeper discussions we have here in the UCG, we agree on being able to tell apart (at least) two separate kinds of assumptions the compiler is making.

So maybe we should use "UB" as the overarching term for "assumptions the compiler is making" (one way or another), and then we can have a list of the kinds of assumptions it makes, and that list currently has two items:

• The Rust Abstract Machine classifies certain behavior as erroneous, such as transmute::<u8, bool>(3). The Rust compiler assumes that the program it compiles will never trigger such an error. Hence reaching this error state in the R-AM is UB.
• When generating target code, the Rust compiler makes some assumptions about its environment (e.g. on x86 it assumes the floating point environment to be set up in a certain way, it assumes the page tables not to "act up", things like that). Hence violating these assumptions is UB.

@gnzlbg

I think that we should actively communicate that this different kind of UB is actually much worse. UB of the form "error in the abstract machine" is not possible in safe Rust, can be detected under miri in unsafe Rust, etc. UB of this other form cannot really be detected nor prevented. For example, if one compiles a safe Rust program for x86 and runs it on ARM, then that's UB of this other form in safe Rust, and there is nothing that we can really do about it.

OTOH it is much less likely that someone will try to run an x86 program on ARM, than that someone creates a NULL reference. Also the failure mode is typically more graceful (it'll just SIGILL instead of having a security vulnerability).

[Centril]

and that list currently has two items:

Possibly with short-hands?

• (abstract) machine UB
• target UB

[Ixrec]

"machine UB" imo sounds too much like a hardware/target-specific thing.

But "abstract (machine) UB" versus "target UB" seems like a very helpful and concise way to describe this distinction.

[Lokathor]

well x86 itself is comfortable setting the rounding mode, but LLVM is not. So fpenv is "llvm ub".

[RalfJung]

LLVM is not part of the Rust spec.

[Lokathor]

Nor are the particulars of x86 and ARM, but we must still live in the universe they give us.

You yourself say that we can't possibly settle on any memory model that LLVM won't implement. This really isn't any different.

[hanna-kruppe]

It is also not a matter specific to LLVM, as "supporting changing the rounding mode" (even more so, changing other aspects of the FP env) conflicts with desirable optimizations and is thus unappealing as only or default mode for optimizing compilers regardless of what components they are built from. Thus the "don't touch fpenv" rule is common to optimizing compilers built on LLVM and those not built on LLVM as well as some language standards that are independent of/predating LLVM (most prominently, C99 and its Annex F).

Furthermore, there is ongoing work to support FP env access in LLVM, and for reasons discussed above rustc should IMO not use this capability by default but at most make it an option that some code sections can opt into.

So this UB cannot be blamed on LLVM or its limitations in any way.

[RalfJung]

When specifying "target UB", of course the details of that target are relevant for the Rust spec. But LLVM ist just a step in the pipeline and should not show up in our end-to-end spec.

[Lokathor]

@RalfJung Well, yes and no.

The term "target" currently means the architecture and OS combination you're building for. So my point was that we should use "target UB" for UB problems that come from the architecture and OS and that pile of "platform stuff".

However, LLVM's limits are also limits that we have to live by when we compile Rust via LLVM. I have no idea why you think we can just ignore talking about them.

@rkruppe yeah I know it's not just LLVM, and that it's a good limit, useful, etc etc. I'm not saying LLVM is at fault and should change, I'm just trying to correctly attribute where each of our limitations comes from.

[Centril]

However, LLVM's limits are also limits that we have to live by when we compile Rust via LLVM. I have no idea why you think we can just ignore talking about them.

Further to "it's not just LLVM", that goes for any backend -- we are bounded by the union of the set of things that each backend does not support. So for example, if Cranelift (🎉) does not support something then we are bounded by that as well. LLVM is not special.

[RalfJung]

I have no idea why you think we can just ignore talking about them.

I have no idea why you think I think that. All I am saying is that "LLVM UB" is not a thing in the Rust spec. When we use LLVM internally it is our obligation to satisfy its assumptions. Some of those we forward to the user by making them our own. But for a Rust user this will be Rust "target UB", nothing related to LLVM.