Compilers · Intermediate Representation
Poison, Undef, and What an IR Must Say About Speculation
How deferred undefined behaviour lets an IR move and duplicate operations that might trap, why poison propagates through flags like nsw, and what a freeze instruction buys in exchange for lost optimisation.
An optimising compiler wants to move instructions earlier, duplicate them along paths where they may not be needed, and delete them when their results are unused. Each of those transformations is illegal if the instruction can trap, because a trap that did not happen in the source would happen in the compiled program. The usual solution is to restrict motion around instructions that may trap, which costs scheduling freedom and blocks many useful rewrites.
The alternative, adopted for the operations covered by flags in LLVM and in several other IRs, is to give the IR a notion of deferred undefined behaviour. An arithmetic operation that would produce an unrepresentable result on some inputs does not wrap or trap on those inputs; it produces a distinguished value that marks the result as poisoned. The undefined behaviour is only realised if the poisoned value reaches a point where it affects observable behaviour, such as a branch condition, a store address, or a call argument. Until then, the value can be moved, duplicated, and discarded freely, because a program that never observes the poison has no undefined behaviour to violate.
The design buys a great deal of optimisation and costs a great deal of subtlety. Getting the semantics right is hard enough that the formal tools used to check it were built specifically for the problem, and the definitions have been revised as holes were found.
Two Kinds of “No Value”
The IR distinguishes two notions that are easy to conflate. An undefined value is one with no fixed content: every use may observe a different value drawn from the whole range of the type, so two uses are not guaranteed to agree. A poison value is a single well-defined marker; it makes any operation that consumes it produce poison in turn, and it produces immediate undefined behaviour if it reaches a position where the program would have to act on its value.
The difference shows up in the transformations each permits. A computation on an undefined value can be folded to any value, because the operand could have been anything; but duplicating a use of an undefined value is not equivalent to using it once, because the two uses may see different values. A computation on a poison value produces poison, which is a single fact that propagates, so duplicating it is safe: both copies are poison, and both are equally unobservable.
Poison is the more useful of the two for optimisation, and modern IRs have been moving work from the undefined category to the poison category precisely because poison composes. The remaining uses of undefined are mostly places where the front end cannot give a definite value, such as uninitialised memory or a variable read before assignment, and the transformations that touch them must be careful not to duplicate reads.
Why Flags Rather than Checks
The flag mechanism is what makes poison cheap. An arithmetic instruction can carry a flag asserting that its result does not overflow, or that a right shift is of a non-negative value, or that a divisor is nonzero. The flag is a promise from the producer of the IR to the consumer: if the promise holds, the instruction behaves as the plain operation; if it does not, the result is poison rather than an unspecified or trapped outcome.
The promise is what allows the optimiser to treat the operation as having algebraic properties that the wrapped version lacks. An addition flagged as non-overflowing can be reassociated, because the mathematical sum is the same regardless of grouping; an addition without the flag cannot, because reassociation can change which intermediate overflows and therefore the wrapped result. A multiply flagged as non-overflowing can be strength-reduced or hoisted out of a loop, because the value is invariant in the mathematical sense; without the flag, the wrapped value is still invariant, but the reasoning is more delicate.
The flags are usually attached by the front end, which knows the source language’s rules. A language whose signed overflow is undefined behaviour can flag every signed addition, because the program has no defined behaviour when the flag’s condition fails. A language with wrapping semantics cannot, and its additions stay unflagged, which is why the same algorithm compiled from a language with undefined signed overflow optimises better than from one with defined wrapping.
The trade is visible at the IR level: a flagged instruction is smaller and more optimisable than an explicit check, but it is only valid if the source semantics justify it. Attaching a flag that the source does not justify is a miscompile, and the failure is silent because the program that overflows was already outside the defined set.
Speculation and the Deferred Trap
The payoff is speculation on the operations that carry the flag. A multiplication flagged as non-overflowing produces poison instead of a trap on the overflow path, so a loop body can be unswitched or a computation hoisted above a guard, and the transformation is valid whenever the poison is not consumed on the path where it is produced. A division by zero, and a dereference of an invalid pointer, are different: both are immediate undefined behaviour, not a deferred marker, so moving either above the guard that protected it changes a defined program into an undefined one and is never legal.
Without deferred behaviour, the same motions would require a proof that the guarded condition holds on every path reaching the operation, which is exactly the situation the motion was meant to improve. The IR would have to keep the operation below the branch, and the scheduler would have to work around it.
The cost is that the compiler must know which operations produce poison and which produce immediate undefined behaviour. A store to a poisoned address, a branch on a poisoned condition, and a call with a poisoned argument are all points where the deferred behaviour becomes immediate. The set of such points is part of the IR’s semantics, and a pass that moves a poisoned value into one of those positions has changed the program from “undefined if the poison is observed” to “undefined always”, which is only valid if the observation was going to happen anyway.
Freeze and the Cost of Ordering
Poison propagates, which is what makes it composable, but propagation is also a problem when a value is used more than once. If a poisoned value is used twice, both uses are poison, and if one of them is guarded and the other is not, the program is undefined. A front end that wants to use a value speculatively and then check it needs a way to stop propagation at the check.
The instruction that does this is a freeze: it takes a value and returns a value that is never poison, choosing an arbitrary but fixed value if the input was poison. Every use of one frozen value sees the same value, so a comparison against it is meaningful and a chain of uses cannot disagree with itself. Freezing also confines the poison: a store whose value is frozen cannot make the whole program undefined through that operand, because the operand is no longer poison.
The cost is that freeze blocks the algebraic reasoning that poison enabled. A frozen value is opaque: the optimiser cannot assume it satisfies the flag’s condition, because the flag may have failed and the freeze may have chosen a value outside the range. Every freeze is therefore a barrier to the transformations that motivated the flag in the first place, and its placement is a trade between safety and optimisation. Placing the freeze early, close to the producer, means every consumer sees a defined value but none of them can be folded under the flag’s assumption; placing it late, at the point where the value is actually observed, leaves the intervening code able to reason about the unflagged value but requires confidence that no other consumer observes poison in the meantime.
Some transformations can remove a freeze entirely. If the value is provably not poison, the freeze is a no-op and can be deleted. If the value is provably always poison, the freeze can be replaced by an arbitrary constant, because the choice is unobservable. Both cases require the kind of value reasoning described in Sparse Conditional Constant Propagation Across the SSA Graph, extended with a fourth lattice element for poison, and the extension is where most of the implementation complexity lives.
What This Does to the Rest of the IR
The presence of poison changes the correctness conditions of nearly every pass. A pass that duplicates a computation must check that the duplication does not create an observation of poison on a path where the original had none. A pass that sinks a computation into a colder block must check that the sink does not remove the only observation that made the program defined. A pass that folds a comparison must check that the folded result is not poison.
The checks are usually expressed as refinement: the transformed program must be at least as defined as the original on every input, and must produce the same observable behaviour wherever the original was defined. Refinement is the right notion because it permits the optimiser to weaken undefined behaviour, which is what makes dead-code elimination of a computation legal: the original program would have been undefined on inputs that reach the deleted code, the transformed one simply does not execute it, and the transformed one refines because everything the original defined it reproduces.
That directionality is the source of the well-known hazards. An optimisation that is a refinement when applied to one construct may not be when applied to another, because the set of inputs on which the original was defined differs, and a transformation that looks like a simple reordering can turn a defined program into an undefined one if it moves a poison-producing operation to a point where its result is observed. The formal tools that check these transformations work by encoding the semantics of the source and target and asking a solver whether the target refines the source; the counterexamples they produce are usually small, which is a sign that the semantics are subtle rather than that the tools are weak.
The Design Constraint Restated
The constraint that forces all of this is the tension between motion and safety. An IR that traps immediately on every erroneous operation is easy to reason about and hard to optimise. An IR that never traps is easy to optimise and useless for a language with checks. Deferred undefined behaviour is the middle position: operations that would trap produce a marker, motion is free until the marker is observed, and the front end decides which source-level errors are allowed to become markers.
The position is not free of cost. It requires a formal semantics that most IRs do not have, a verifier that understands the marker, and a discipline across every pass that a value may be poison. It also requires the front end to be honest about which operations can fail, because a flag attached without justification is a miscompile that no test will catch.
The alternative positions are worth naming. A fully defined IR, in which every operation has a specified result for every input, makes every transformation provable but forces the front end to emit explicit checks, and the checks dominate the optimised code. A fully undefined IR, in which any operation may do anything, makes optimisation trivial and compilation meaningless. The interesting designs all sit between, and the marker mechanism is the most developed point in that space: it gives the optimiser the freedom of the undefined position for operations whose results are not observed, and the precision of the defined position for those that are.
References
- LLVM Language Reference Manual — Undefined Behavior and Poison Values — LLVM project
- Alive2: Bounded Translation Validation for LLVM — Lopes, Lee, Hur, Liu, Regehr; PLDI 2021
- Formal Verification of a Realistic Compiler — Leroy, ACM Communications 2009