This paper looks closely at the semantics of undef and poison in LLVM and finds that some of the optimizations in LLVM are making contradicting assumptions about these special values and their interaction, leading to end-to-end miscompilations. They also propose a solution, which has been also suggested to the LLVM community.
I have to say I really like the model they end up with. The model is simple, reducing the number of these “special bad values” from 2 to 1 and also getting rid of the surprising “propagating non-determinism” rules around undef. (Previously, in LLVM, x XOR x could be any value, because x could be undef. Under the proposed rules, x XOR x can only be 0 or poison.) Furthermore, the model supports all the optimizations LLVM does; some need some minor modification though precisely to guard against the existing miscompilations.
So, overall, I think it would make a lot of sense for Rust to adapt the same kind of approach for dealing with “bad values”. Incidentally, miri already has poison, though they call it Undef for additional confusion.
Oooh, cool. One thing that’s interesting about the paper is that it looks to me like undef has been replaced by freeze p for some poison p. Does this seem right to you @RalfJung?
That’s roughly right. However, freeze poison is significantly weaker than undef. Consider (everything of type i32)
%x = undef
%y = xor %x %x
Now %y could be any integer. If you replace undef by freeze poison, however, %y is guaranteed to be 0.
It turns out that freeze provides enough non-determinism to justify optimizations like loop unswitching, and the full blown “non-deterministic on every use” behavior of undef is not needed.
I really like the model as well. However, I was initially quite surprised by the suggestion that Rust should adopt something similar. The freeze/poison model seems very tailored to justifying optimizations, which isn’t terribly relevant to describing the semantics of Rust. In particular, “deferred UB” (which includes both ndef and poison) is usually motivated by the need to justify speculative execution, which is important when optimizing code but not at all when simply laying down the definition of UB (even when the rules should be executable). Furthermore, the model is as complex as it is partially because of C-language rules (e.g., the motivating example for poison is related to signed integer overflow being UB).
However, on further thought, I see the appeal of how poison propagates flawless through almost arbitrary computations. It seems like a good way to model uninitialized memory and padding bytes (which probably shouldn’t be UB to load from, since memcpy should be implementable). I assume you’re referring to that aspect? Because I still don’t see any use for the other half of the proposal, freeze.
Indeed, I mostly thought of the dreaded "uninitialized memory". Most places where LLVM uses poison are outright UB in C, and probably considered UB in Rust; however, C's rules for uninitialized memory are not entirely agreed-upon. Essentially, I think that this form of well-defined poison should be used instead C's fuzzy "indeterminate value" when it comes to standardizing Rust. We could also consider using poison for some things that are currently UB (and also UB in C), like out-of-bounds offset. More of this may become relevant if/when rustc starts to perform code motion optimization itself.
miri currently is even stricter here than LLVM, making any arithmetic on poison UB rather than propagating poison. That's fine, it just means we have fewer defined programs that we otherwise would.
I don't think that it's wise to introduce deferred-UB into the language solely for the purpose of enabling optimization. The optimizer IR is distinct from the language spec, therefore compiler optimizations (1) won't sufffer from keeping as much as possible insta-UB rather than deferred-UB, and (2) might actually suffer from being too liberal with deferred-UB. If optimizers want to use deferred-UB for something that the spec says is insta-UB, they are free to make that operation "more defined" unilaterally. How exactly they do this should be up to them. On the contrary, eagerly choosing a certain kind of deferred-UB in the language spec may inadvertedly constrain optimizers whose IR has an incompatible notion of deferred-UB.
Admittedly, if the IR used for optimization makes more programs defined than in the language spec does, said IR can't be easily be reused in a dynamic UB detector, which will want to model the insta-UB prescribed by the language. I guess the developers of such tools will have to find a way to deal with that
