Lesson 9.7 — Semantics: undefined behavior, poison, undef, freeze, flags and refinement¶

Techniques: immediate undefined behavior; poison values and freeze; undef and why it is deprecated; poison-generating flags (nsw, nuw, exact, disjoint, samesign, nneg, GEP and cast flags); refinement, the correctness criterion for transformations · Pebble uses: nsw on unchecked arithmetic only where the language makes overflow a trap (checked first), freeze where a branch may see poison · Lab: R1 (every task must behave at -O2), E6, E7 · Prerequisites: Lesson 9.3, Lesson 9.4 · Time: 5 hours · Continued in: Ch 13 (refinement proofs for peephole rules, Alive2)

clang compiles int always(int x) { return x + 1 > x; } to ret i32 1, and the unsigned version to a real comparison with -1. Both are correct, and the difference is one flag: signed overflow is undefined in C, so clang writes add nsw, and in LLVM an nsw add that overflows produces poison, a value that "does not exist"; comparing poison yields poison, and the optimizer may replace poison by any value it likes, here true. This lesson gives LLVM IR's semantics of undefined behavior precisely enough to decide such questions: which operations are undefined behavior (UB), which only produce poison, how poison propagates, what freeze and select do with it, why the older undef is being removed, and what it means for a transformation to be correct (refinement). The course treats these as a first look; Ch 13 builds proofs of optimizations on them.

1. Problem and motivation¶

An optimizer must know when two programs are "the same". For programs without undefined behavior that is simple, but source languages have UB (C's signed overflow, out-of-bounds access, null dereference), and optimizers want to speculate: execute an operation before knowing that it is needed, e.g. hoist a + b out of a loop that might not run. If a + b on overflow were immediate UB, speculating it would introduce UB into a program that had none. LLVM's answer is a deferred kind of UB, poison: an operation with an invalid input produces a poison value, which becomes UB only when it reaches something that matters (a branch, a memory address, a call argument marked noundef) [LLVM-UB].

Undefined behavior¶

Immediate UB means "the program has no meaning from this point": LLVM may assume it does not happen. Division by zero, a load from a null or dangling pointer, branching on poison, and reaching unreachable are immediate UB. The LangRef documents each; the design goals are laid out in the UndefinedBehavior document [LLVM-UB] and in Lee et al.'s paper [LHK+17].

Poison and freeze¶

Before 2017, LLVM had both undef (an arbitrary value) and an informally defined "poison". Lee et al. showed that the combination was inconsistent: some optimizations LLVM performed were justified only under one reading, others only under the other, and together they could miscompile [LHK+17]. They proposed keeping only poison as the deferred UB and adding freeze, an instruction that turns poison into an arbitrary but fixed value, so that transformations like "branch → select" and loop unswitching could be made correct. freeze landed in LLVM 10 (2020).

Undef and why it is deprecated¶

undef means "any value, chosen independently at each use". That makes %x + %x with %x = undef able to produce an odd number, so it is not equivalent to %x * 2; it makes GVN's "replace a value by an equal one" unsound in corner cases; and it forbids simple rewrites. LLVM is moving every source of undef (uninitialized memory, insertelement placeholders, padding) to poison or to the byte type (Lesson 9.2); the LangRef now says to use poison "whenever possible" [LLVM-LangRef, §Undefined Values].

Poison-generating flags¶

Flags let the front end state facts that make overflow or inexactness impossible in defined executions: nsw (no signed wrap) on C's signed arithmetic, nuw, exact on divisions and shifts known to be exact, disjoint on an or of values with no common bits, samesign on a comparison of values with equal signs, nneg on a zext of a non-negative value, inbounds/nusw/nuw on GEPs (Lesson 9.4). Violating a flag produces poison. Optimizers both use flags (x + 1 > x → true under nsw) and must drop them when a rewrite would make them false.

A transformation is correct if the new program's behaviors are a subset of the old program's allowed behaviors: it may remove nondeterminism and UB, never add them. This is refinement; Alive and Alive2 check it automatically for LLVM transformations with an SMT solver [LMNR15, LLM+21].

2. Definitions and algorithms¶

Definition 9.7.1 (Immediate undefined behavior)

An execution has undefined behavior (UB) from the first point at which it performs an operation the LangRef declares UB; a program's set of behaviors then includes every behavior. The immediate-UB operations include: udiv/sdiv/urem/srem by zero or by poison, and sdiv/srem of \(\mathrm{INT\_MIN}\) by \(-1\); load/store/call through a pointer that is poison, null (in address space 0) or not dereferenceable for the access; br/switch on a poison (or undef) condition; executing unreachable; passing poison to a noundef parameter or returning it from a noundef return; violating a function attribute such as memory(none) or willreturn. A data race is not immediate UB in LLVM IR, unlike in C++: a non-atomic load that may see more than one write returns undef for those bytes [LLVM-LangRef, §Memory Model for Concurrent Operations] (Lesson 9.4).

Definition 9.7.2 (Values with poison)

For a first-class integer type \(\texttt{i}N\), the semantic domain is \(\mathbb{V}_N = \{0, \dots, 2^N - 1\} \cup \{\mathsf{poison}\}\) (bit patterns plus poison); vectors are tuples of lane values, aggregates tuples of field values, and each lane or field is independently poison or not. A value is well defined if it is not poison and contains no undef bits.

Definition 9.7.3 (Poison-generating flags and operations)

Let \(x, y\) be the (non-poison) operands of width \(N\), \(\mathrm{s}(\cdot)\) the signed reading. The result is poison exactly when:

instruction	condition for poison
`add`/`sub`/`mul` `nuw`	the exact unsigned result \(\notin [0, 2^N)\)
`add`/`sub`/`mul` `nsw`	the exact signed result \(\notin [-2^{N-1}, 2^{N-1})\)
`shl`, `lshr`, `ashr` (any)	shift amount \(y \ge N\)
`shl nuw` / `shl nsw`	a non-zero bit is shifted out / a shifted-out bit differs from the result's sign bit
`lshr exact`, `ashr exact`	a non-zero bit is shifted out
`udiv exact`, `sdiv exact`	the division has a remainder
`or disjoint`	\(x \mathbin{\&} y \ne 0\)
`icmp samesign`	\(x\) and \(y\) have different sign bits
`zext nneg`, `uitofp nneg`	\(x\)'s sign bit is set
`trunc nuw` / `trunc nsw`	the truncation changes the value read as unsigned / signed
`fptosi`, `fptoui`	the value does not fit the integer type
`getelementptr inbounds`/`nusw`/`nuw`	the conditions of Definition 9.4.6 fail
`load` with `!range`/`!nonnull`/`!align`	the loaded value violates the metadata (Definition 9.6.4)
FP ops with `nnan`/`ninf`	an operand or the result is NaN / infinite

Definition 9.7.4 (Poison propagation rules)

Write \(e \Downarrow v\) for "instruction \(e\) evaluates to \(v\)" and \(\mathsf{op}\) for any operation other than select, phi and freeze. With \(\mathsf{P}\) for poison:

\[ \dfrac{x \Downarrow \mathsf{P} \ \lor\ y \Downarrow \mathsf{P}}{\mathsf{op}(x, y) \Downarrow \mathsf{P}}\ (\mathsf{P\text{-}Op}) \qquad \dfrac{x \Downarrow a \quad y \Downarrow b \quad a, b \ne \mathsf{P} \quad \mathrm{flagfails}(\mathsf{op}, a, b)}{\mathsf{op}(x, y) \Downarrow \mathsf{P}}\ (\mathsf{P\text{-}Flag}) \]

\[ \dfrac{c \Downarrow \mathsf{P}}{\mathsf{select}(c, x, y) \Downarrow \mathsf{P}}\ (\mathsf{P\text{-}SelC}) \qquad \dfrac{c \Downarrow 1 \quad x \Downarrow v}{\mathsf{select}(c, x, y) \Downarrow v}\ (\mathsf{Sel1}) \qquad \dfrac{c \Downarrow 0 \quad y \Downarrow v}{\mathsf{select}(c, x, y) \Downarrow v}\ (\mathsf{Sel0}) \]

\[ \dfrac{x \Downarrow a \quad a \ne \mathsf{P}}{\mathsf{freeze}(x) \Downarrow a}\ (\mathsf{Frz}) \qquad \dfrac{x \Downarrow \mathsf{P} \quad k \in [0, 2^N)}{\mathsf{freeze}(x) \Downarrow k}\ (\mathsf{FrzP}) \]

\(\mathrm{flagfails}\) is the condition of Definition 9.7.3; (FrzP) is nondeterministic: freeze picks some \(k\), and all uses of that one freeze see the same \(k\). A phi takes the value of the incoming edge (poison if that value is poison). and x, 0 is still poison when \(x\) is (rule P-Op): poison is not "some unknown bits".

Algorithm 9.7.5 (Evaluating straight-line code with poison and freeze)

Input: a sequence of instructions over integer types, and concrete input values in \(\mathbb{V}_N\).
Output: for each instruction: its value, poison, or depends (different for different choices of the freezes), and whether a final branch is UB.
Precondition: no instruction is immediate UB on any choice (division only by non-zero constants other than \(-1\)).
Postcondition: the output agrees with Definition 9.7.4 for every choice of freeze results.
Invariant: after instruction \(j\), env maps every value defined so far to its value under the current choice.

function Evaluate(prog, inputs):
    F ← the freeze instructions of prog whose operand may be poison
    results ← map from instruction to set of observed values
    for choice in ∏ over f ∈ F of [0, 2^width(f)):          # all ways freeze may pick
        env ← inputs
        for ins in prog:
            args ← [env[a] for a in operands(ins)]
            if ins is freeze: env[ins] ← args[0] if args[0] ≠ P else choice[ins]
            else if ins is select: env[ins] ← SelectRule(args)          # rules P-SelC, Sel0, Sel1
            else if P ∈ args: env[ins] ← P                               # rule P-Op
            else if FlagFails(ins, args): env[ins] ← P                  # rule P-Flag (Definition 9.7.3)
            else: env[ins] ← the exact result modulo 2^width
            results[ins] ← results[ins] ∪ {env[ins]}
    for ins in prog:
        answer[ins] ← the single element of results[ins] if |results[ins]| = 1 else "depends"
    branch ← "ub" if answer[cond] = P else answer[cond]            # branching on poison is UB
    return answer, branch

This is program_outcome in tools/course/lib/llvmir.py, the oracle of the poison-propagation drill; its answers agree with LLVM's UB-aware interpreter llubi on the drill's corpus (Section 7).

Definition 9.7.6 (undef)

The constant undef of type \(\tau\) denotes the set of all values of \(\tau\); each use of an undef (directly, or through an instruction whose result is undef-derived) may independently pick any element. Uninitialized memory reads as undef (Lesson 9.4). An operation on undef operands returns the set of results over all choices, which the optimizer may replace by any element.

Definition 9.7.7 (Behaviors)

The behaviors \(\mathcal{B}(P, \iota)\) of program \(P\) on input \(\iota\) are the observable traces (calls to external functions, volatile accesses, final return value and memory) of its executions, where every nondeterministic choice (freeze, undef, races) ranges over all possibilities; if some execution reaches immediate UB, \(\mathcal{B}(P, \iota)\) is the set of all traces. A returned value that is poison stands for every value of its type.

Definition 9.7.8 (Refinement)

A program \(T\) refines \(S\), written \(S \sqsupseteq T\), if \(\mathcal{B}(T, \iota) \subseteq \mathcal{B}(S, \iota)\) for every input \(\iota\). For single values: \(v_T\) refines \(v_S\) if \(v_S = \mathsf{P}\), or \(v_S = v_T\); for a value expression \(e_T\) and \(e_S\) over inputs \(\vec{x}\): for all \(\vec{x}\), either \(e_S(\vec{x}) = \mathsf{P}\) or \(e_T(\vec{x}) = e_S(\vec{x}) \ne \mathsf{P}\). A transformation is correct iff its output always refines its input.

Proposition 9.7.9 (Allowed flag sets are closed under union)

Let \(e_T^G\) be a target expression carrying the set \(G\) of poison-generating flags on one instruction, and suppose each flag \(g \in G\) individually keeps refinement: \(e_S \sqsupseteq e_T^{\{g\}}\). Then \(e_S \sqsupseteq e_T^{G}\).

Proof

Flags only add poison: for every input, \(e_T^G(\vec{x}) = \mathsf{P}\) iff \(e_T^{\emptyset}(\vec{x}) = \mathsf{P}\) or \(\mathrm{flagfails}(g)\) holds for some \(g \in G\), and otherwise \(e_T^G(\vec{x}) = e_T^{\emptyset}(\vec{x})\) (Definition 9.7.3 changes only the poison condition, not the value). Take an input with \(e_S(\vec{x}) \ne \mathsf{P}\). For each \(g\), refinement by \(e_T^{\{g\}}\) gives \(e_T^{\{g\}}(\vec{x}) = e_S(\vec{x}) \ne \mathsf{P}\), hence \(g\)'s condition does not fail on \(\vec{x}\) and \(e_T^\emptyset(\vec{x}) = e_S(\vec{x})\). So no flag of \(G\) fails and \(e_T^G(\vec{x}) = e_S(\vec{x})\): refinement holds for \(G\).

Algorithm 9.7.10 (Which flags may a rewritten instruction keep, by enumeration)

Input: a source expression \(e_S\) and a flag-free target \(e_T\) over \(m\) variables of width \(N\) (small), and candidate flags \(C\) for the target instruction.
Output: invalid, or the set of \(g \in C\) with \(e_S \sqsupseteq e_T^{\{g\}}\).
Precondition: \(N \cdot m\) small enough to enumerate (\(2^{Nm}\) inputs); the rewrite is width-independent, so small widths are representative (Alive2's bounded-verification assumption).
Postcondition: by Proposition 9.7.9, the returned set is the largest allowed set.
Invariant: every input checked so far satisfies the refinement condition for the flags still in the candidate set.

function AllowedFlags(eS, eT, C, N, m):
    if not Refines(eS, eT with no flags): return invalid
    return { g ∈ C | Refines(eS, eT with flag g) }

function Refines(eS, eT):
    for x in [0, 2^N)^m:
        s ← eS(x)
        if s = P: continue                      # source poison: anything is allowed
        if eT(x) = P or eT(x) ≠ s: return false  # a counterexample
    return true

This is the oracle of the flags drill (refines in tools/course/lib/llvmir.py); Alive2 answers the same question for all widths with an SMT solver [LLM+21].

3. Worked example¶

Following poison (Algorithm 9.7.5) through the LangRef's own example, extended (the real-world box in "Poison and freeze" runs it in llubi):

value	instruction	result	rule
`%p`	`add nsw i8 127, 1`	poison	P-Flag: \(127 + 1 = 128 \notin [-128, 128)\)
`%and0`	`and i8 %p, 0`	poison	P-Op (not 0!)
`%sel`	`select i1 true, i8 5, i8 %p`	5	Sel1: the unchosen operand does not matter
`%f`	`freeze i8 %p`	some fixed \(k\)	FrzP
`%d`	`sub i8 %f, %f`	0	both uses see the same \(k\)
`%e`	`sub i8 %p, %p`	poison	P-Op
`%c`	`icmp eq i8 %d, 0`	true	normal evaluation
—	`br i1 %c, …`	well defined	the condition is not poison

Had the branch used %e (or any value derived from %p without freeze), the execution would be UB.

The same code with undef. Replace %p by undef and freeze by nothing: %d = sub i8 undef, undef may be any value, because each use of undef picks separately (Definition 9.7.6), so %c may be false and the branch may go either way. Folding %d to 0 would still be a refinement (0 is one of the allowed values; instsimplify folds sub i8 %x, %x to 0 for every %x, and sub i8 undef, undef to undef), but the source no longer guarantees 0. What undef breaks is the opposite kind of rewrite, one that duplicates a use and thereby adds choices, such as mul %x, 2 → add %x, %x (Proposition 9.7.14). After freeze, %d is 0 in every execution, because both uses see one choice.

Why add nsw x, x → shl nsw x, 1 is right, and nuw does not follow from nsw (Algorithm 9.7.10 on \(N = 8\)):

target flags	refines `add nsw %x, %x`?	first counterexample
none	yes	— (same bits: \(2x \bmod 256\))
`nsw`	yes	— (`shl nsw` by 1 is poison iff \(2x\) leaves the signed range, exactly when `add nsw` is)
`nuw`	no	\(x = -1\): source \(-2\) (no signed overflow), target poison (a set bit is shifted out)

So the answer is \(\{\texttt{nsw}\}\), and by Proposition 9.7.9 no larger set works. ./course drill flags generates such questions; instcombine does this rewrite in the flags box below and keeps exactly nsw.

Refinement with a dropped flag. InstCombine folds add nsw (add nsw %x, 100), 100 on i8 into add %x, -56 (\(100 + 100 = 200 \equiv -56\)). May the target keep nsw? Take \(x = -100\): the source computes \(-100 + 100 = 0\) and \(0 + 100 = 100\), neither overflowing, so the source is the well-defined value 100. The target computes \(-100 + (-56) = -156\), which leaves the signed range: with nsw it would be poison where the source is not, so nsw must go (and nuw too, since \(156 + 200\) wraps unsigned). Without flags the target returns \(-156 \bmod 256 = 100\), the source's value: a valid refinement. On inputs where the source itself overflows, e.g. \(x = 0\) (\(0 + 100 + 100 = 200\)), the source is poison and the target may return anything, here \(-56\).

Try it

./course drill poison-propagation --seed 4 --difficulty hard --solution traces a program with casts, flags, a select and a final branch on poison (other seeds add freeze); ./course drill flags --seed 493 --difficulty medium --solution is the add nsw folding above.

4. Invariants and correctness¶

Undefined behavior¶

Proposition 9.7.11 (Deleting code after UB, and the null-check example)

If every execution that reaches a program point \(q\) has UB before or at \(q\), then replacing \(q\)'s block by unreachable is a refinement; in particular, a null check after a dereference of the same pointer may be removed.

Proof

By Definition 9.7.7, an execution that has UB has all traces as behaviors, so any behavior of the transformed program on that input is included. Executions that do not reach \(q\) are unchanged. For the null check: %v = load i32, ptr %p is UB if %p is null (Definition 9.7.1), so every execution that reaches icmp eq ptr %p, null after the load, with %p null, already had UB; hence the comparison may be replaced by false. This is the transformation behind the famous removal of a null check in the Linux kernel (2009), and clang does it for deref_then_check in the box below.

Poison and freeze¶

Proposition 9.7.12 (select's poison rule makes speculation sound)

Let %t be a speculatable instruction that may produce poison but never immediate UB. Then executing %t unconditionally and using it only as the unchosen operand of a select on the paths where the original did not execute it is a refinement.

Proof

On paths where the original executes %t, the new program computes the same value and the select chooses it (rule Sel1 or Sel0 with the same operand). On the other paths the select chooses the other operand, so by rules Sel0/Sel1 its result does not depend on %t at all, even if %t is poison; %t itself has no side effects and no UB. So every execution of the new program produces the original's values, except that the new one may compute an unused poison. That is why select does not propagate poison from the unchosen operand, and why simplifycfg may speculate add nsw (Lesson 9.3, Proposition 9.3.10).

Theorem 9.7.13 (Freeze makes branch conversions correct)

For any %c: (a) br i1 (freeze %c), label %A, label %B refines br i1 %c, label %A, label %B; (b) select i1 %c, i8 %x, i8 %y is refined by the diamond that branches on freeze %c and joins with a phi, but in general not by the diamond that branches on %c directly.

Proof

(a) If %c is not poison, freeze %c = %c (rule Frz) and both branch the same way. If %c is poison, the original has UB (Definition 9.7.1), whose behaviors include anything, in particular jumping to either target. (b) If %c is not poison, both select the same operand's value. If %c is poison, the select yields poison (P-SelC), which refines to any value; the frozen diamond picks some \(k\) and yields %x or %y, a particular value, which is allowed because poison is refined by every value. The diamond on the unfrozen %c instead has UB when %c is poison, which is not a refinement of "poison": a program that used the select's result only in a way that does not trigger UB (e.g. never used it) was well defined, and now is not.

Undef and why it is deprecated¶

Proposition 9.7.14 (With undef, x + x is not 2·x)

Let \(f(x) = \texttt{add}\ x, x\) and \(g(x) = \texttt{mul}\ x, 2\) on \(\texttt{i}8\). Then \(g\) refines \(f\) for every argument, including undef and poison, but \(f\) does not refine \(g\) when \(x\) is undef.

Proof

For a well-defined \(x\), both compute \(2x \bmod 256\); for poison \(x\), both are poison. For \(x\) = undef: in \(g\), the single use of \(x\) picks some \(a\) and the result is \(2a \bmod 256\), an even number: \(\mathcal{B}(g) = \{\text{even values}\}\). In \(f\), the two uses pick \(a\) and \(b\) independently, and \(a + b \bmod 256\) takes every value: \(\mathcal{B}(f) = \{0, \dots, 255\}\). So \(\mathcal{B}(g) \subseteq \mathcal{B}(f)\) (\(f \sqsupseteq g\)), but \(\mathcal{B}(f) \not\subseteq \mathcal{B}(g)\): rewriting mul %x, 2 into add %x, %x (a classic strength reduction) is incorrect if %x may be undef. With poison instead of undef, both are equally poison and the rewrite is correct in both directions.

This is the core argument of [LHK+17] against undef: any rewrite that duplicates a use of a value is unsound for undef, and duplicating uses is everywhere (GVN, instruction combining, loop unswitching). LLVM keeps undef only for backward compatibility and is replacing its sources.

Poison-generating flags¶

Theorem 9.7.15 (x + 1 > x under nsw)

icmp sgt i32 (add nsw i32 %x, 1), %x is refined by true for every %x.

Proof

If %x is poison, the add and the compare are poison (P-Op), refined by any value. Otherwise let \(a = \mathrm{s}(x)\). If \(a = 2^{31} - 1\), add nsw overflows and yields poison (P-Flag), so the comparison is poison, refined by true. Otherwise \(a + 1 \le 2^{31} - 1\) is representable, and \(a + 1 > a\), so the comparison is true. In all cases true refines the source. Without nsw the wrapped sum for \(a = 2^{31} - 1\) is \(-2^{31} < a\) and the comparison is false: the fold is invalid, which is why the unsigned C version in the box below keeps a comparison.

Theorem 9.7.16 (Refinement is a preorder and a congruence for straight-line code)

(a) \(\sqsupseteq\) is reflexive and transitive. (b) If \(e_S \sqsupseteq e_T\) as value expressions (Definition 9.7.8), then for every context \(C[\cdot]\) built from the operations of Definition 9.7.4 (with one occurrence of the hole), \(C[e_S] \sqsupseteq C[e_T]\).

Proof

(a) Inclusion of behavior sets is reflexive and transitive. (b) By structural induction on \(C\); fix an input. If the hole is the whole context, this is the hypothesis. If \(e_S\) is poison on this input, then (by the induction hypothesis applied to the sub-context containing the hole) the corresponding operand of \(C\)'s outermost operation is poison or refined by anything: for an ordinary operation the source result is poison (P-Op) and any target result refines it; for select with the hole in the condition, the same (P-SelC); with the hole in an operand, the source result is poison if that operand is chosen and equal to the target's otherwise; for freeze, the source may produce any \(k\) (FrzP), which includes whatever the target produces; for an operation whose operand is immediate UB on poison (a divisor), the source has UB, which every behavior refines. If \(e_S\) is not poison, then \(e_T = e_S\) on this input, and the two contexts compute the same thing, including whether a flag fails, because each operation is a function of its operands' values.

Theorem 9.7.16 is what makes local reasoning about peephole rules valid: InstCombine proves each rule as a refinement of two small expressions, and the theorem lifts it to whole programs. Ch 13 develops the full treatment, including memory and Alive2's encoding [LLM+21].

5. Complexity¶

Technique	Time (worst)	Time (typical)	Space	Variables
Poison evaluation, no `freeze` of poison (Algorithm 9.7.5)	\(O(i)\)	\(O(i)\)	\(O(i)\)	\(i\) = instructions
… with \(f\) nondeterministic `freeze`s	\(O(i \cdot 2^{Nf})\)	tiny in the drill (\(f \le 1\), \(N = 8\))	\(O(i)\)	\(N\) = width
Flag check by enumeration (Algorithm 9.7.10)	\(O(\lvert C \rvert \cdot 2^{Nm} \cdot i)\)	256–65 536 inputs	\(O(i)\)	\(m\) = variables, \(C\) = candidate flags
Refinement for all widths (Alive2)	NP-hard in general; SMT	seconds per rule	—	—
UB-aware interpretation (`llubi`)	linear in the execution length	—	—	—

Proposition 9.7.17 (Cost of the enumerative checks)

Algorithm 9.7.5 performs \(i \cdot \prod_{f} 2^{N_f}\) instruction evaluations, and Algorithm 9.7.10 at most \((1 + \lvert C \rvert) \cdot 2^{Nm}\) evaluations of each side.

Proof

Algorithm 9.7.5 runs the program once per element of the product of the freeze choice sets, and each run evaluates \(i\) instructions in \(O(1)\) each. Algorithm 9.7.10 calls Refines once for the flag-free target and once per candidate flag; each call enumerates at most \(2^{Nm}\) inputs and stops at the first counterexample.

Pathological input. Enumeration is exponential in \(N \cdot m\): a two-variable rewrite at \(N = 8\) needs 65 536 evaluations, at \(N = 32\) about \(1.8 \cdot 10^{19}\). That is why the flags drill checks two-variable rewrites at i4 and why real tools use SMT (Alive2) or rely on width-independence arguments. Another pathology is poison-aware analysis in the compiler itself: isGuaranteedNotToBePoison walks operands recursively and is depth-limited (to 6 in LLVM) to stay linear.

Undefined behavior¶

UB-aware interpreters: llubi (LLVM 23, the tool in the boxes), Alive2's interpreter, and Miri for Rust MIR execute programs while detecting UB; trade-off: slow, but exact.
Sanitizers (-fsanitize=undefined) check source-level UB at run time before it becomes IR-level UB.

Poison and freeze¶

freeze placement: passes that turn selects into branches (SimplifyCFG), unswitch loops, or hoist conditions insert freeze; isGuaranteedNotToBePoison removes redundant ones (the !noundef fold in Lesson 9.6).
Poison in memory: a stored poison value comes back as poison; the byte type bN (Lesson 9.2) makes it per-bit, so copying a struct with a poison field does not poison the whole copy.

Undef and why it is deprecated¶

Replacing sources of undef: insertelement placeholders use poison (the insertelement <4 x float> poison, … idiom in Lesson 9.2's box); uninitialized memory remains undef for now, with the byte type as the long-term replacement.
noundef on parameters and returns (Lesson 9.5): clang marks almost every C value noundef, which lets LLVM treat those values as well defined even while undef exists.

Poison-generating flags¶

Flag inference (InstCombine, CorrelatedValuePropagation, IndVarSimplify): adds nsw/nuw/nneg/disjoint/samesign when analysis proves them (box below).
Flag dropping: every rewrite that changes an instruction must drop flags it cannot justify (dropPoisonGeneratingFlags), as in the fold_big example.

Alive / Alive2 [LMNR15, LLM+21]: automated refinement checking for peephole rules and whole functions; Alive2 found hundreds of LLVM bugs.
Vellvm [ZNMZ12]: a Coq formalization of LLVM IR semantics in which refinement proofs are machine-checked.

7. In real compilers¶

Undefined behavior¶

LLVM

llvm/lib/Analysis/ValueTracking.cpp — programUndefinedIfPoison and handleGuaranteedNonPoisonOps (which operands make poison immediate UB: divisors, addresses, branch conditions, noundef arguments); llvm/lib/Transforms/InstCombine/InstructionCombining.cpp — the canonical unreachable marker store i1 true, ptr poison (LLVM 23.1.2) [LLVM-ValueTracking].

GCC 15: exploits the same C rules but has no IR-level poison: signed overflow is UB on the operation's type (TYPE_OVERFLOW_UNDEFINED), and the "UB" information is used by value-range propagation (gcc/tree-vrp.cc).
rustc: safe Rust has no UB; its codegen emits nsw/nuw only where overflow is impossible or checked (unchecked_add → add nsw), and the MIR interpreter Miri detects UB in unsafe code.

Find where LLVM does it. In llvm/lib/Analysis/ValueTracking.cpp, find handleGuaranteedNonPoisonOps. Question: for a udiv, which operand is listed?

Exploiting UB in C, and detecting it in IR with llubi

Reproduce (clang 23.1.2, llubi 23.1.2):

cat > ub.c <<'EOF'
int always(int x) { return x + 1 > x; }
int wraps(unsigned x) { return x + 1 > x; }
int deref_then_check(int *p) { int v = *p; if (!p) return -1; return v; }
EOF
clang-23 --target=x86_64-unknown-linux-gnu -O1 -S -emit-llvm ub.c -o - | sed -n '/^define/,/^}/p' | grep -v "^$"
cat > ub.ll <<'EOF'
define i32 @main() {
entry:
  %x = add nsw i32 2147483647, 1
  %c = icmp sgt i32 %x, 0
  br i1 %c, label %a, label %b
a:
  ret i32 1
b:
  ret i32 0
}
EOF
llubi --verbose ub.ll; echo "exit status $?"
printf 'define i32 @main() {\n  %%d = sdiv i32 7, 0\n  ret i32 %%d\n}\n' > div.ll
llubi div.ll; echo "exit status $?"

Output (complete):

define dso_local noundef i32 @always(i32 noundef %0) local_unnamed_addr #0 {
  ret i32 1
}
define dso_local range(i32 0, 2) i32 @wraps(i32 noundef %0) local_unnamed_addr #0 {
  %2 = icmp ne i32 %0, -1
  %3 = zext i1 %2 to i32
  ret i32 %3
}
define dso_local i32 @deref_then_check(ptr nofree noundef readonly captures(none) %0) local_unnamed_addr #1 {
  %2 = load i32, ptr %0, align 4, !tbaa !9
  ret i32 %2
}
Entering function: main
  %x = add nsw i32 2147483647, 1 => poison
  %c = icmp sgt i32 %x, 0 => poison
Stacktrace:
#0   br i1 %c, label %a, label %b at @main ub.ll:5
Immediate UB detected: Branch on poison condition.
error: Execution of function 'main' failed.
exit status 1
Stacktrace:
#0   %d = sdiv i32 7, 0 at @main div.ll:2
Immediate UB detected: Division by zero.
error: Execution of function 'main' failed.
exit status 1

What to notice: Theorem 9.7.15 (always → 1, while wraps keeps a comparison) and Proposition 9.7.11 (the null check after *p is gone). llubi evaluates by Definition 9.7.4: the overflowing add nsw and the comparison are poison, but the program fails only at the branch, the first immediate UB; division by zero is immediate UB at the division itself.

Poison and freeze¶

LLVM

llvm/lib/Analysis/ValueTracking.cpp — propagatesPoison (rule P-Op, with select and freeze as the exceptions), canCreatePoison (the flags of Definition 9.7.3), isGuaranteedNotToBePoison; llvm/lib/Transforms/InstCombine/InstructionCombining.cpp — InstCombinerImpl::visitFreeze (LLVM 23.1.2) [LLVM-ValueTracking].

GCC 15: no poison and no freeze; GCC avoids the problems freeze solves by not speculating operations whose UB is type-based, or by rewriting them to unsigned arithmetic first (rewrite_to_defined_overflow, gcc/gimple-fold.cc).
Cranelift 37: no poison at all: integer operations wrap, and trapping operations (sdiv) trap; the IR has no deferred UB to reason about (Lesson 9.8).

Find where LLVM does it. In llvm/lib/Analysis/ValueTracking.cpp, find propagatesPoison. Question: does it return true for the condition operand of a select? For the other two operands?

Poison, select and freeze under llubi; select as a poison-safe 'and'

Reproduce (llubi 23.1.2, opt 23.1.2):

cat > poison.ll <<'EOF'
define i32 @main() {
entry:
  %p = add nsw i8 127, 1
  %and0 = and i8 %p, 0
  %sel = select i1 true, i8 5, i8 %p
  %f = freeze i8 %p
  %d = sub i8 %f, %f
  %e = sub i8 %p, %p
  %c = icmp eq i8 %d, 0
  br i1 %c, label %ok, label %bad
ok:
  ret i32 0
bad:
  ret i32 1
}
EOF
llubi --verbose poison.ll; echo "exit status $?"
cat > logic.ll <<'EOF'
define i1 @logical_and(i1 %a, i1 %b) {
  %r = select i1 %a, i1 %b, i1 false
  ret i1 %r
}
define i1 @logical_and_nu(i1 %a, i1 noundef %b) {
  %r = select i1 %a, i1 %b, i1 false
  ret i1 %r
}
EOF
opt -passes=instcombine -S logic.ll | grep -E "^define|^  "

Output (complete):

Entering function: main
  %p = add nsw i8 127, 1 => poison
  %and0 = and i8 %p, 0 => poison
  %sel = select i1 true, i8 5, i8 %p => i8 5
  %f = freeze i8 %p => i8 62
  %d = sub i8 %f, %f => i8 0
  %e = sub i8 %p, %p => poison
  %c = icmp eq i8 %d, 0 => T
  br i1 %c, label %ok, label %bad jump to %ok
  ret i32 0
Exiting function: main
exit status 0
define i1 @logical_and(i1 %a, i1 %b) {
  %r = select i1 %a, i1 %b, i1 false
  ret i1 %r
define i1 @logical_and_nu(i1 %a, i1 noundef %b) {
  %r = and i1 %a, %b
  ret i1 %r

What to notice: the Section 3 table, row by row; 62 is the value llubi happened to pick for the frozen poison (any value is correct, and both uses of %f see it). select i1 %a, i1 %b, i1 false is C's a && b: if %a is false, a poison %b does not matter. InstCombine turns it into and (which does propagate poison from %b) only when %b is noundef.

Undef and why it is deprecated¶

LLVM

llvm/lib/Analysis/InstructionSimplify.cpp — the undef folds (add X, undef → undef, and X, undef → 0, or X, undef → -1), each choosing some element of the set of Definition 9.7.6; llvm/lib/IR/Constants.cpp — UndefValue and its subclass PoisonValue (poison "is an undef" in the class hierarchy, as the stronger form of undefinedness: poison may be replaced by undef or by any value, never the other way round) (LLVM 23.1.2).

GCC 15: uninitialized values are default definitions of SSA names (x_1(D)) with unspecified value; GCC's optimizers treat them as "some value" and warn (-Wmaybe-uninitialized), without an undef constant in the IR.
Swift SIL: has undef as a value (Lesson 9.8's SIL quote mentions it), used by the compiler for unreachable code.

Find where LLVM does it. In llvm/lib/IR/Constants.cpp, find PoisonValue::get. Question: which class does PoisonValue derive from?

undef folds pick a value; poison stays poison

Reproduce (opt 23.1.2):

cat > undef.ll <<'EOF'
define i8 @add_u(i8 %x) {
  %r = add i8 %x, undef
  ret i8 %r
}
define i8 @and_u(i8 %x) {
  %r = and i8 %x, undef
  ret i8 %r
}
define i8 @or_u(i8 %x) {
  %r = or i8 %x, undef
  ret i8 %r
}
define i8 @twice_u() {
  %r = add i8 undef, undef
  ret i8 %r
}
define i8 @mul2_u() {
  %r = mul i8 undef, 2
  ret i8 %r
}
define i8 @and_p(i8 %x) {
  %r = and i8 %x, poison
  ret i8 %r
}
EOF
opt -passes=instsimplify -S undef.ll | grep -E "^define|^  ret"

Output (complete):

define i8 @add_u(i8 %x) {
  ret i8 undef
define i8 @and_u(i8 %x) {
  ret i8 0
define i8 @or_u(i8 %x) {
  ret i8 -1
define i8 @twice_u() {
  ret i8 undef
define i8 @mul2_u() {
  ret i8 0
define i8 @and_p(i8 %x) {
  ret i8 poison

What to notice: and X, undef folds to 0 (choose undef = 0) and or X, undef to -1, each a legal choice from the set. add undef, undef stays undef (every value is possible, since the two uses choose independently) while mul undef, 2 becomes 0, an even value: Proposition 9.7.14 in LLVM's own folder. With poison there is nothing to choose: and X, poison is poison.

Poison-generating flags¶

LLVM

llvm/include/llvm/IR/Operator.h — OverflowingBinaryOperator (nuw/nsw), PossiblyExactOperator (exact), GEPOperator; llvm/include/llvm/IR/InstrTypes.h — PossiblyDisjointInst (disjoint), PossiblyNonNegInst (nneg); llvm/lib/IR/Instruction.cpp — Instruction::dropPoisonGeneratingFlags; flags are inferred in llvm/lib/Transforms/InstCombine/ (e.g. InstCombinerImpl::visitZExt for nneg) and llvm/lib/Transforms/Scalar/CorrelatedValuePropagation.cpp (LLVM 23.1.2).

GCC 15: no per-instruction flags; overflow facts come from types (signed = no overflow in C) and from value ranges.
rustc: emits nuw/nsw for unchecked_* intrinsics and after overflow checks; disjoint and nneg come from LLVM's own inference.

Find where LLVM does it. In llvm/lib/IR/Instruction.cpp, find dropPoisonGeneratingFlags. Question: which instruction kinds does it handle besides integer binary operators?

instcombine keeps, drops and infers flags

Reproduce (opt 23.1.2):

cat > flags.ll <<'EOF'
define i8 @fold_small(i8 %x) {
  %a = add nsw i8 %x, 3
  %b = add nsw i8 %a, 4
  ret i8 %b
}
define i8 @fold_big(i8 %x) {
  %a = add nsw i8 %x, 100
  %b = add nsw i8 %a, 100
  ret i8 %b
}
define i8 @mul_to_shl(i8 %x) {
  %r = mul nsw i8 %x, 4
  ret i8 %r
}
define i8 @add_to_or(i8 %x, i8 %y) {
  %lo = and i8 %x, 15
  %hi = shl i8 %y, 4
  %r = add i8 %lo, %hi
  ret i8 %r
}
define i16 @sext_to_zext(i8 %x) {
  %a = lshr i8 %x, 1
  %r = sext i8 %a to i16
  ret i16 %r
}
define i1 @slt_to_ult(i8 %x, i8 %y) {
  %xa = and i8 %x, 127
  %ya = and i8 %y, 127
  %r = icmp slt i8 %xa, %ya
  ret i1 %r
}
EOF
opt -passes=instcombine -S flags.ll | grep -E "^define|^  "

Output (complete):

define i8 @fold_small(i8 %x) {
  %b = add nsw i8 %x, 7
  ret i8 %b
define i8 @fold_big(i8 %x) {
  %b = add i8 %x, -56
  ret i8 %b
define i8 @mul_to_shl(i8 %x) {
  %r = shl nsw i8 %x, 2
  ret i8 %r
define i8 @add_to_or(i8 %x, i8 %y) {
  %lo = and i8 %x, 15
  %hi = shl i8 %y, 4
  %r = or disjoint i8 %lo, %hi
  ret i8 %r
define i16 @sext_to_zext(i8 %x) {
  %a = lshr i8 %x, 1
  %r = zext nneg i8 %a to i16
  ret i16 %r
define i1 @slt_to_ult(i8 %x, i8 %y) {
  %xa = and i8 %x, 127
  %ya = and i8 %y, 127
  %r = icmp samesign ult i8 %xa, %ya
  ret i1 %r

What to notice: nsw survives folding \(3 + 4\) but not \(100 + 100\) (the Section 3 example); mul nsw by 4 becomes shl nsw (not nuw); InstCombine adds disjoint, nneg and samesign where known bits prove them, and uses them to switch to the canonical unsigned forms. The drill flags asks you to predict exactly these sets.

LLVM

LLVM has no refinement checker in-tree; the reference tool is Alive2 (github.com/AliveToolkit/alive2, alive-tv compares two functions, opt-alive checks every pass application) [LLM+21]. LLVM's InstCombine tests cite Alive2 proofs (https://alive2.llvm.org/ce/z/… links) in llvm/test/Transforms/InstCombine/ and in commit messages.

GCC 15: no refinement checker; correctness of folds is argued in comments and tested.
The course: tools/course/lib/llvmir.py (refines, Algorithm 9.7.10) is a bounded refinement checker by enumeration, the oracle of ./course drill flags.

Find where LLVM does it. In llvm/test/Transforms/InstCombine/, search the test files for alive2.llvm.org. Question: what does such a link attach to a test?

A refinement check by enumeration, and the same rewrite in opt

Reproduce (course CLI with the LLVM 23.1.2 toolchain, run from the repository root; opt 23.1.2):

./course drill flags --seed 493 --difficulty medium --solution | sed -n '/^source: %a/,$p'
printf 'define i8 @f(i8 %%x) {\n  %%a = add nsw i8 %%x, 100\n  %%r = add nsw i8 %%a, 100\n  ret i8 %%r\n}\n' \
  | opt -passes=instcombine -S | grep "  %r"

Output (complete):

source: %a = add nsw i8 %x, 100 ; %r = add nsw i8 %a, 100
target: %r = add G i8 %x, -56

| target flags | refines? | counterexample |
|---|---|---|
| (none) | yes | — |
| nuw | no | %x = -128: source = 72, target = poison |
| nsw | no | %x = -128: source = 72, target = poison |

Answer:
```text
allowed: {}
```
  %r = add i8 %x, -56

What to notice: Algorithm 9.7.10 enumerates inputs as unsigned bytes and stops at the first counterexample, \(x = -128\) for both flags (source \(-128 + 100 = -28\), then \(-28 + 100 = 72\), well defined; target \(-128 + (-56) = -184\) overflows signed, and \(128 + 200\) overflows unsigned); the \(x = -100\) of Section 3 is another counterexample. So the allowed set is empty, and opt indeed emits the fold without flags. For inputs where the source is poison (e.g. \(x = 0\): \(0 + 100 + 100\) overflows) the target may return anything, here \(-56\).

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Undefined behavior	lets the optimizer assume impossible situations away (null checks, overflow)	free at compile time	silent miscompile of UB programs; `llubi`/sanitizers to detect	low for the compiler, high for users	C/C++ semantics; `unreachable`
Poison and freeze	deferred UB: speculation is safe; `freeze` pins a value	propagation \(O(1)\) per instruction	`llubi --verbose` shows poison per value	moderate: every pass must respect `select`/`freeze` rules	flags, speculation, branch↔select
Undef and why it is deprecated	"any value per use": weaker than poison	—	breaks use-duplicating rewrites (Proposition 9.7.14)	high (hard to reason about)	legacy; uninitialized memory
Poison-generating flags	precise per-instruction facts (overflow, exactness, disjointness, sign)	\(O(1)\) checks; inference by known bits	flags visible in IR; dropped when unjustified	moderate (must drop on every rewrite)	C signed arithmetic, canonical forms
Refinement	the correctness criterion for all transformations	exponential by enumeration; SMT for all widths	counterexamples	Alive2 or proofs	validating InstCombine rules, drills

Choose poison over UB for anything an optimizer may want to speculate; choose immediate UB only where the operation cannot be executed at all (division by zero, invalid memory access). Never emit undef in new code: use poison for "no value" and freeze where a well-defined arbitrary value is needed. Add a flag only when the source language guarantees it in every defined execution; drop flags whenever a rewrite changes the operation. Check every rewrite you write as a refinement (Alive2 in Ch 13).

9. Assessment¶

Technique	Quiz ids (`solutions/quizzes/ch09.yaml`)	Drill	Flashcard tag	Exercises
Undefined behavior	`ub-or-poison`, `branch-on-poison`	`./course drill poison-propagation --difficulty medium` (branch)	`ub`	R1 of the lab (`-O2`)
Poison and freeze	`poison-trace`, `freeze-sub`	`./course drill poison-propagation`	`poison`	E6, E7
Undef and why it is deprecated	`undef-twice`, `undef-vs-poison`	— (see below)	`undef`	—
Poison-generating flags	`nsw-fold`, `flags-allowed`, `find-propagates-poison`	`./course drill flags`	`flags`	E1 (`nuw nsw` in the solution), E6
Refinement	`refinement-direction`, `flags-allowed`	`./course drill flags --difficulty hard`	`refinement`	—

undef has no drill of its own: its semantics differs from poison's mainly in use duplication, which the quiz asks directly (undef-twice); drilling random undef programs would teach a representation LLVM is removing.

Poison is not 'random bits'

and i8 %p, 0 with %p poison is poison, not 0, and %p == %p is poison, not true. If you need "some value, the same everywhere", freeze it first. Conversely, a well-defined program may compute poison as long as it never branches on it, stores through it or passes it to a noundef parameter: computing poison is not a bug; using it is.

References¶

See the chapter references.

Lesson 9.7 — Semantics: undefined behavior, poison, undef, freeze, flags and refinement¶

1. Problem and motivation¶

Undefined behavior¶

Poison and freeze¶

Undef and why it is deprecated¶

Poison-generating flags¶

Refinement¶

2. Definitions and algorithms¶

3. Worked example¶

4. Invariants and correctness¶

Undefined behavior¶

Poison and freeze¶

Undef and why it is deprecated¶

Poison-generating flags¶

Refinement¶

5. Complexity¶

Undefined behavior¶

Poison and freeze¶

Undef and why it is deprecated¶

Poison-generating flags¶

Refinement¶

7. In real compilers¶

Undefined behavior¶

Poison and freeze¶

Undef and why it is deprecated¶

Poison-generating flags¶

Refinement¶

8. Comparison¶

9. Assessment¶

References¶

Lesson 9.7 — Semantics: undefined behavior, poison, undef, freeze, flags and refinement¶

1. Problem and motivation¶

Undefined behavior¶

Poison and freeze¶

Undef and why it is deprecated¶

Poison-generating flags¶

Refinement¶

2. Definitions and algorithms¶

3. Worked example¶

4. Invariants and correctness¶

Undefined behavior¶

Poison and freeze¶

Undef and why it is deprecated¶

Poison-generating flags¶

Refinement¶

5. Complexity¶

6. Variants and refinements¶

Undefined behavior¶

Poison and freeze¶

Undef and why it is deprecated¶

Poison-generating flags¶

Refinement¶

7. In real compilers¶

Undefined behavior¶

Poison and freeze¶

Undef and why it is deprecated¶

Poison-generating flags¶

Refinement¶

8. Comparison¶

9. Assessment¶

References¶