UB does not time travel

[RalfJung]

Fixes rust-lang/unsafe-code-guidelines#407 by saying that our UB does not have time travel semantics (in relation to observable behavior such as I/O and volatile accesses).

This does not require any compiler changes. The compiler already does not do time-traveling UB, we just need to change the docs to turn this into a promise for our users.
Note that this relies on LLVM 23. With LLVM 22, UB can time travel across volatile reads. We use LLVM 23 but still allow compiling with LLVM 22, though we also document that

The one or two preceding major versions are usually supported in the sense that they are expected to build successfully and pass most tests. However, fixes for miscompilations often do not get backported to past LLVM versions, so using rustc with older versions of LLVM comes with an increased risk of soundness bugs. We strongly recommend using the latest version of LLVM.

I don't know to what extent we consider inofficial builds of Rust (with different LLVM versions) as being governed by the Reference.
Cc @rust-lang/opsem @rust-lang/lang

[joshlf]

What is the advantage of providing this guarantee? Since everyone (as far as I'm aware) aspires to produce code which is entirely UB-free, I can't imagine someone wanting to rely on this.

Plus, as you say, it constrains us to specific versions of LLVM (and presumably to LLVM, period – what about Cranelift or other future backends?).

Maybe we could weaken this to say that we don't currently have time-traveling UB when compiling with the standard LLVM backend, but that this isn't a stability promise, and that it may not apply to other backends?

[RalfJung]

The advantage is that if you do

dbg!(...);
some_function_that_maybe_has_ub();

then you will reliably see that debug output before the UB. It is quite frustrating when you can't debug your null ptr deref because the dbg! that would print the pointer value is swallowed by time-traveling UB. The classic example from C is the equivalent of

eprintln!("going to load from {ptr:p}");
let _val = ptr.read();

and then seeing a crash without the print. Now you may think that the crash occurs from some other operation before the print. But actually the read is where it crashes, the compiler just moved the read above the print so you can't tell any more where the crash originates from.

Of course you don't rely on this for an actually deployed program. But you are not unlikely to rely on this while debugging a program and figuring out what the heck it is doing and where it is going wrong.

[joshlf]

That's a good point, but presumably it'd still be useful to those users for us to document this without documenting it as a stable guarantee?

I'd need to think more to convince myself that this is actually true, but I think that this guarantee would make it harder for Aeneas and Anneal to model UB (AeneasVerif/aeneas#1225). Currently the proposal is to model UB as a kind of "absorbing state" in which, once you reach UB, that's all that Aeneas says about your execution. If pre-UB effects are observable, then we'd need to expose those effects in addition.

I suppose could just say "Aeneas's model is strictly weaker than – but not inconsistent with – what Rust itself guarantees", but I'd like to avoid that, at least for Anneal, if possible. It makes it harder to keep straight the correspondence between Aeneas/Anneal and upstream Rust, makes it harder for us to explain to users, etc.

cc @sonmarcho @protz @mdittmer @Nadrieril

[RalfJung]

That's a good point, but presumably it'd still be useful to those users for us to document this without documenting it as a stable guarantee?

I feel quite strongly that time-traveling UB is something we don't want to do. Time-traveling UB defies people's intuition and is often used as an example for "look at this silly thing the compiler did" (and I can't even really argue that people are wrong when saying that). Even C finally got rid of time-traveling UB by accepting N3128, albeit as a recommendation rather than a normative requirement (IIUC).

Time-traveling UB is a disservice to our users. Therefore, we shouldn't do it, and we should promise not to do it.

I'd need to think more to convince myself that this is actually true, but I think that this guarantee would make it harder for Aeneas and Anneal to model UB (AeneasVerif/aeneas#1225). Currently the proposal is to model UB as a kind of "absorbing state" in which, once you reach UB, that's all that Aeneas says about your execution. If pre-UB effects are observable, then we'd need to expose those effects in addition.

Note that this model is already wrong. Consider a program like this:

fn main() {
    let mut buffer = String::new();
    let _ignore = io::stdin().read_line(&mut buffer);
    unsafe { std::hint::unreachable_unchecked() };
}

If I run this program and then hit Ctrl-C when it waits for input, that's an entirely well-defined execution. The compiler must create code that handles that execution correctly. It seems you are saying Aeneas would model this execution as equivalent to a program that always has UB; that is an incorrect model.

The only operations where UB as a sort of "absorbing" state is a correct model are operations that are guaranteed to always return. Many I/O operations are already allowed to never return and models have to deal with that.

[RalfJung]

@rustbot label +I-lang-nominated

[RalfJung]

I suppose could just say "Aeneas's model is strictly weaker than – but not inconsistent with – what Rust itself guarantees", but I'd like to avoid that, at least for Anneal, if possible. It makes it harder to keep straight the correspondence between Aeneas/Anneal and upstream Rust, makes it harder for us to explain to users, etc.

I think it would be a sad outcome if trying to support more formal reasoning tools would lead to Rust making fewer useful (and formally meaningful) promises to its users.

It is true that this can complicate modeling Rust programs with observable behavior. But I think that complication is well-invested effort to make Rust behavior better aligned with people's intuitions and with what we actually want the compiler to do.

If Aeneas/Anneal anyway proves that a program cannot reach UB on any path then I don't think it should cause significant complications. Complications mostly arise if you want to define the semantics of programs that sometimes do and sometimes do not have UB, and what it means to correctly compile such a program.