Lesson 13.8 — Transformation correctness: refinement, undefined behavior, flags and fast-math¶

Techniques: refinement as the correctness criterion (a formal relation, its preorder and congruence theorems); undefined behavior, poison, the deprecated undef and freeze; poison-generating flags (nsw, nuw, exact, disjoint, samesign, nneg) and when rewrites must drop them; floating-point semantics and fast-math flags (nnan, ninf, nsz, arcp, contract, afn, reassoc) · Pebble implements: the flag functions of pebble-peephole (E2), flag intersection in pebble-lvn (E3), flag rules of pebble-reassociate (E5) · Lab: ch13-rewrite-check decides refinement (Part B) · Prerequisites: Lesson 9.7, which introduces UB, poison, undef, freeze, the flags and refinement; this lesson builds the proof tools on top of it · Time: 5 hours

Lesson 9.7 defined what LLVM IR means when things go wrong: immediate undefined behavior (UB), poison, undef, freeze, and poison-generating flags, and it defined refinement for single expressions. Every optimization in this chapter was justified by one sentence: "the target refines the source". This lesson makes that sentence a tool. It defines refinement for whole straight-line programs with UB, poison and nondeterminism; proves it is a preorder and a congruence, so that a rule proven on a four-instruction pattern is correct in every program (the theorem Lesson 13.2 relied on); gives one algorithm that decides, for any rewrite, which poison-generating flags the result may keep — and derives from it every flag rule of E2; and treats floating point, where IEEE 754 already forbids most algebra and fast-math flags selectively allow it.

1. Problem and motivation¶

A transformation is correct when no execution of the optimized program does something the original could not have done. Compilers exploit UB to optimize (Lesson 9.7 §1), so "could have done" is a set: the original's behaviors include everything after UB, and every value where the original produced poison. The problem is to state this precisely, to check it mechanically (Lesson 13.9), and to get the flags right: most real miscompilations found by Alive in LLVM were flag errors [LMNR15].

Refinement comes from program verification (a program refines a specification if it only exhibits specified behaviors); for compilers it is the correctness criterion of CompCert's backward simulation [Ler09] and of Alive/Alive2 [LMNR15, LLM+21]. Lee et al. defined LLVM's refinement with poison and freeze [LHK+17]; Lesson 9.7 Definition 9.7.8 gives the value-level version that this lesson extends.

Undefined behavior and poison¶

LLVM has two kinds of undefinedness: immediate UB (the whole execution is meaningless) and deferred UB (poison, which becomes UB only when it reaches a branch, an address, or a noundef use). undef, an older third kind, lets each use pick a value independently and is being removed because it breaks rewrites that duplicate a use [LHK+17]; freeze turns poison into an arbitrary but fixed value [LLVM-LangRef].

Poison-generating flags¶

nsw (C's signed overflow is UB), nuw, exact, disjoint, samesign, nneg and the GEP flags state facts that let later passes optimize (x + 1 > x becomes true under nsw, Lesson 9.7 Theorem 9.7.15). A rewrite that keeps a flag the source did not justify makes the program more poisonous — the most common peephole bug.

Floating-point semantics and fast-math¶

IEEE 754 arithmetic is deterministic but neither associative nor distributive, and has \(-0\), infinities and NaNs (Lesson 13.1, Definition 13.1.9 and Proposition 13.1.14). So x + 0.0 → x and (a + b) - a → b are wrong in general. Fast-math flags (from -ffast-math, -fno-signed-zeros, -ffp-contract) let the programmer permit specific wrong-in-general rewrites; LLVM gives some of them value semantics (nnan, ninf produce poison) and others rewrite-based semantics (reassoc, contract, arcp, afn) [LLVM-LangRef, §Fast-Math Flags]. Alive-FP extended verification to them [MNG16].

2. Definitions and algorithms¶

Definition 13.8.1 (Outcomes and behaviors of a straight-line program)

An outcome of a straight-line function \(f\) of type \(\texttt{i}N\) on an input \(\vec{x}\) (each argument a bit pattern or poison) is a value in \(\mathbb{V}_N = \{0, \dots, 2^N - 1\} \cup \{\mathsf{poison}\}\) or the symbol \(\mathsf{UB}\). The behaviors \(\mathcal{B}(f, \vec{x})\) are the set of outcomes of all executions, one per choice of the nondeterministic values: each freeze of poison picks some \(k \in [0, 2^{w})\) once (Definition 9.7.4, rule FrzP); each use of undef picks a value independently (Definition 9.7.6). An execution's outcome is \(\mathsf{UB}\) if it performs immediate UB (Definition 9.7.1), else the returned value.

Definition 13.8.2 (Refinement)

Let the closure of an outcome set be \(\overline{B} :=\) all outcomes if \(\mathsf{UB} \in B\); else \(B \cup \mathbb{V}_N\) if \(\mathsf{poison} \in B\); else \(B\). A function \(t\) refines \(s\) (with the same signature), written \(s \sqsupseteq t\), if for every input \(\vec{x}\): \(\mathcal{B}(t, \vec{x}) \subseteq \overline{\mathcal{B}(s, \vec{x})}\). Two functions are equivalent if each refines the other. For single values this is Definition 9.7.8.

Refinement is not equivalence

\(s\): %a = add nsw i8 %x, 1; %r = icmp sgt i8 %a, %x, \(t\): ret i1 true. For \(x = 127\), \(\mathcal{B}(s) = \{\mathsf{poison}\}\), whose closure contains true; for every other non-poison \(x\), \(\mathcal{B}(s) = \{\mathit{true}\}\); for poison \(x\) both closures are everything. So \(s \sqsupseteq t\). But \(t \not\sqsupseteq s\): at \(x = 127\), \(t\) returns true and \(s\) returns poison, which is not in \(\overline{\{\mathit{true}\}}\). Alive2 reports exactly this (box in §7).

Theorem 13.8.3 (Refinement is a preorder)

\(\sqsupseteq\) is reflexive and transitive on functions of the same signature.

Proof

Reflexive: \(B \subseteq \overline{B}\) by definition of the closure. Transitive: suppose \(s \sqsupseteq t\) and \(t \sqsupseteq u\); fix \(\vec{x}\) and write \(S, T, U\) for the behavior sets. We have \(U \subseteq \overline{T}\) and \(T \subseteq \overline{S}\). The closure is monotone (\(A \subseteq B \Rightarrow \overline{A} \subseteq \overline{B}\), by cases on whether UB or poison is in \(B\)) and idempotent (\(\overline{\overline{A}} = \overline{A}\): the closure of a set containing UB is everything; of a set containing poison but not UB is \(A \cup \mathbb{V}_N\), whose closure is itself). Hence \(U \subseteq \overline{T} \subseteq \overline{\overline{S}} = \overline{S}\).

Definition 13.8.4 (Allowed outcome)

An outcome \(o_t\) is allowed by a source behavior set \(S\) if \(o_t \in \overline{S}\): always if \(\mathsf{UB} \in S\); otherwise \(o_t \ne \mathsf{UB}\) and (\(\mathsf{poison} \in S\) or \(o_t \in S\)). Deterministic special case: source outcome \(o_s\) allows \(o_t\) iff \(o_s = \mathsf{UB}\), or \(o_t \ne \mathsf{UB}\) and (\(o_s = \mathsf{poison}\) or \(o_t = o_s\)). This is the test the lab's checker and the drill rewrite-validity apply per input.

Undefined behavior and poison¶

Definition 13.8.5 (Definedness order on values)

On \(\mathbb{V}_N\) extended by \(\mathsf{undef}\) (standing for "any value, per use") define \(v \preceq w\) ("\(w\) is at least as defined as \(v\)") by \(\mathsf{poison} \preceq v\) for all \(v\), \(\mathsf{undef} \preceq k\) for every concrete \(k\), and reflexivity. Replacing a value by one at least as defined is a refinement at every use that does not duplicate it; LangRef: poison is "a stronger form of undef" [LLVM-LangRef, §Poison Values].

Poison-generating flags¶

Definition 13.8.6 (Exact result and flag condition)

For an integer instruction \(i\) with non-poison operands, its exact result \(\hat r(i) \in \mathbb{Z}\) is the result of the operation on the unbounded integers, reading the operands as unsigned for nuw and as signed for nsw (for shl by \(k\): \(x \cdot 2^k\); for udiv/sdiv exact: \(x / d\) as a rational). The flag condition of \(g\) is: nuw: \(\hat r_u \in [0, 2^N)\); nsw: \(\hat r_s \in [-2^{N-1}, 2^{N-1})\); exact: \(\hat r\) is an integer (for shifts: no non-zero bit is shifted out); disjoint: \(x \mathbin{\&} y = 0\); samesign: operands have equal sign bits; nneg: the operand's sign bit is 0. The instruction with flag \(g\) is poison iff its condition fails (Definition 9.7.3). For every flag except samesign, disjoint and nneg, "condition holds" means "the wrapped result equals the exact result".

Algorithm 13.8.7 (Flag transfer by exact-value reasoning)

Input: a rewrite \(s \Rightarrow t\) where \(t\)'s root instruction \(i_t\) may carry flags from a candidate set \(G\); the source's flags.
Output: the flags of \(G\) that \(i_t\) may keep, each with a proof or a counterexample.
Precondition: the flag-free target refines the source (check it first, e.g. with Algorithm 13.9.6).
Postcondition: every returned flag \(g\) satisfies: whenever \(s\) is not poison, \(g\)'s condition holds at \(i_t\) (so adding \(g\) keeps refinement, Theorem 13.8.13).
Invariant: a flag is kept only with a proof obligation discharged for every input.

function TransferFlags(s, t, G):
    kept ← ∅
    for g in G:
        # Step 1: a sufficient proof by exact values
        if the source root has flag g
           and every source node between the root and the leaves of t also has g
           and ExactEqual(s, t, g):                    # exact results agree when s is not poison
            kept ← kept ∪ {g}; continue
        # Step 2: otherwise search for a counterexample
        if some input x has s(x) ≠ poison and g's condition fails at i_t on x:
            record x as the reason to drop g              # e.g. by enumeration at small N
        else:
            kept ← kept ∪ {g}                             # holds for another reason: prove it separately
    return kept

function ExactEqual(s, t, g):
    # Evaluate both roots over Z (no wraparound) as polynomials in the leaves,
    # reading constants as signed (g = nsw) or unsigned (g = nuw) N-bit numbers.
    return the two polynomials are identical

Because flags only add poison, the set of flags that may be kept individually may be kept together (Proposition 9.7.9).

Floating-point semantics and fast-math¶

Definition 13.8.8 (Fast-math flags)

Let \([\![\circ]\!]_{\mathrm{IEEE}}\) be the correctly rounded operation of Definition 13.1.9. An FP instruction with flags \(F\) behaves as follows [LLVM-LangRef, §Fast-Math Flags]:

flag	meaning
`nnan`	if an operand or the result is NaN, the result is poison
`ninf`	if an operand or the result is \(\pm\infty\), the result is poison
`nsz`	the sign of a zero operand may be flipped nondeterministically
`arcp`	\(a / b\) may be treated as \(a \cdot (1/b)\), and \(a / (b / c)\) as \(a \cdot (c / b)\) (rewrite-based)
`contract`	a multiply followed by an add may be fused into one rounding (`fma`) (rewrite-based)
`afn`	library functions may be replaced by approximations (rewrite-based)
`reassoc`	algebraically equivalent rewrites (associativity, distributivity) are allowed (rewrite-based)
`fast`	all of the above

A rewrite-based flag licenses a rewrite of an expression only if every instruction of the rewritten expression carries it, and the new instructions get the intersection of the flags (LangRef, "Rewrite-based flags"; box in §7).

Algorithm 13.8.9 (Checking a floating-point peephole rule)

Input: an FP rule \(L \to R\) with the flags present on \(L\)'s instructions.
Output: valid or a counterexample among the IEEE special values.
Precondition: the rule is an algebraic identity over the reals (otherwise it is only licensed by reassoc/arcp/contract/afn).
Postcondition: valid means: for every input, \(R\)'s outcome is allowed by \(L\)'s outcome set under the flag semantics of Definition 13.8.8.
Invariant: each special class is checked under the flag semantics (poison for nnan/ninf violations, both zero signs for nsz operands).

function CheckFP(L → R, flags):
    if R differs from L by reassociation, reciprocal, contraction or approximation:
        return valid iff every instruction of L has the licensing flag       # rewrite-based
    for x in {±0, ±∞, NaN, ±min subnormal, ±max finite, 1, −1, a few randoms}^k:
        S ← outcomes of L on x   (nnan/ninf: poison if violated; nsz: both signs of zero operands)
        T ← outcomes of R on x
        if some outcome of T is not allowed by S: return counterexample x
    return valid                                     # exhaustive only for small formats (Lesson 13.9)

3. Worked example¶

Is mul i8 %x, 2 → add i8 %x, %x a refinement? Behavior sets for three inputs (Definition 13.8.1):

input \(x\)	\(\mathcal{B}(s)\): `mul x, 2`	\(\mathcal{B}(t)\): `add x, x`	\(\mathcal{B}(t) \subseteq \overline{\mathcal{B}(s)}\)?
3	{6}	{6}	yes
poison	{poison}	{poison}	yes
`undef`	{0, 2, 4, …, 254} (one use: even values)	{0, 1, …, 255} (two independent uses)	no: 1 is odd

So the rewrite is valid if undef inputs are excluded, invalid otherwise (Proposition 9.7.14; Alive2 box in §7). The reverse direction add x, x → mul x, 2 is valid in both cases.

Undefined behavior and poison¶

Converting select i1 %c, i32 %x, i32 %y into a branch and a phi, for \(c = \mathsf{poison}\), \(x = 1\), \(y = 2\) (the llubi box in §7):

version	outcome	allowed by the select's \(\{\mathsf{poison}\}\)?
`select` (source)	poison	—
branch on `%c`	UB (branch on poison)	no: UB is not in \(\overline{\{\mathsf{poison}\}}\)
branch on `freeze %c`	2 (freeze picked false)	yes: poison allows any value

Poison-generating flags¶

Algorithm 13.8.7 on three rules of E2, \(N = 8\):

rule	flag \(g\)	source nodes have \(g\)?	exact source	exact target	ExactEqual	result
R9: \((x + 100) + 100 \Rightarrow x + (-56)\)	nsw	yes	\(x + 200\)	\(x - 56\)	no	search: \(x = -100\) gives source 100, target \(-156\) → poison: drop
R9: \((x + 10) + 20 \Rightarrow x + 30\)	nsw	yes	\(x + 30\)	\(x + 30\)	yes	keep
R10: \(x \cdot 8 \Rightarrow x \ll 3\)	nsw	yes	\(8x\)	\(8x\)	yes	keep
R10: \(x \cdot (-128) \Rightarrow x \ll 7\)	nsw	yes	\(-128 x\) (signed constant)	\(128 x\)	no	search: \(x = 1\): source \(-128\) (in range), target \(\hat r = 128\): poison: drop
R8: \(x - 5 \Rightarrow x + (-5)\)	nsw	yes	\(x - 5\)	\(x - 5\)	yes	keep
R8: \(x - 5 \Rightarrow x + (-5)\)	nuw	yes	\(x - 5\) (unsigned)	\(x + 251\) (unsigned constant)	no	search: \(x = 10\): source 5, target \(\hat r = 261 \ge 256\): drop

Floating-point semantics and fast-math¶

Algorithm 13.8.9 on the FP rules of E2 and two rewrites E2 rejects (double):

rule	flags	special input	source	target	verdict
\(x + (-0) \to x\)	none	\(x = -0\)	\((-0) + (-0) = -0\)	\(-0\)	valid (also \(+0\): \(+0 + -0 = +0\))
\(x + (+0) \to x\)	none	\(x = -0\)	\((-0) + (+0) = +0\)	\(-0\)	invalid
\(x + (+0) \to x\)	`nsz`	\(x = -0\)	operand signs may flip: \(\{+0, -0\}\)	\(-0\)	valid
\(x - x \to +0\)	none	\(x = \infty\)	NaN	\(+0\)	invalid
\(x - x \to +0\)	`nnan`	\(x = \infty\)	NaN → poison	\(+0\)	valid
\(x \cdot 0 \to 0\)	`nnan`	\(x = -1\)	\(-0\)	\(+0\)	invalid without `nsz`
\((a + b) - a \to b\)	none	\(a = 10^{16}, b = 1\)	0	1	invalid (not an identity in floating point)
\((a + b) - a \to b\)	`reassoc nsz` on both	—	—	—	valid (rewrite-based license)

Try it

./course drill rewrite-validity --difficulty medium asks for verdicts and counterexamples on flag rewrites, UB-introducing rewrites and poison inputs; ./course drill flags (Ch 9) asks for the set of flags a target may keep.

4. Invariants and correctness¶

Lemma 13.8.10 (Every instruction is monotone in definedness)

For every integer instruction, select, freeze, cast and icmp: if each operand of a second evaluation is at least as defined as the corresponding operand of a first (Definition 13.8.5, poison below everything), then the second evaluation's outcome is allowed by the first's (Definition 13.8.4). For br, load, store and division, a poison operand in the first evaluation where it causes UB makes the first outcome UB, which allows anything.

Proof

By cases (Definition 9.7.4). Ordinary operations: if any first operand is poison, the first result is poison, which allows every non-UB outcome, and the second is not UB (these operations have no UB); otherwise all operands are equal and the results are equal. Flags: a flag condition depends only on the operand values, so with equal operands both fail or both hold. Division: a poison or zero divisor in the first evaluation is UB, which allows everything; otherwise the divisor is equal in both, and the dividend case is as above. select: a poison condition gives poison first; otherwise the same operand is chosen in both, and the claim reduces to that operand. freeze: of poison, the first may pick every value, so the second's result (any value, or the same pick) is among them; otherwise equal. br on poison: UB first. load/store through a poison address: UB first; with equal addresses, store writes an at-least-as-defined value, so later loads are covered by induction.

Theorem 13.8.11 (Refinement is a congruence: replacing an SSA value)

Let \(P\) be a function containing a value \(v\) defined by a side-effect-free, straight-line expression \(e_S\) over values \(\vec{a}\) available at \(v\)'s definition, and let \(e_T\) be an expression over the same \(\vec{a}\) with \(e_S \sqsupseteq e_T\) (for every \(\vec{a}\), every outcome of \(e_T\) is allowed by \(\mathcal{B}(e_S, \vec{a})\)). Let \(P'\) be \(P\) with \(v\) defined by \(e_T\) instead. Then \(P \sqsupseteq P'\), whatever the number of uses of \(v\) and whatever control flow follows.

Proof

Consider an execution of \(P'\) with some choices of its nondeterministic values. We construct an execution of \(P\) whose outcome allows the outcome of \(P'\)'s execution. Until \(v\) is defined, both run the same instructions with the same choices. At \(v\): \(P'\) produces an outcome \(o_T\) of \(e_T\); by hypothesis \(o_T\) is allowed by some outcome set \(S = \mathcal{B}(e_S, \vec{a})\). Case \(\mathsf{UB} \in S\): choose \(P\)'s execution that has UB there; its behavior set is everything, done. Case \(o_T \in S\) (in particular \(o_T\) not UB): choose \(P\)'s execution in which \(e_S\) produces \(o_T\); from then on both executions are identical. Case \(\mathsf{poison} \in S\) and \(o_T\) a value: choose \(P\)'s execution in which \(v\) is poison. Now run both on: at every later step, \(P\)'s operands are at most as defined as \(P'\)'s (poison where \(P'\) has \(o_T\), equal elsewhere, with \(P'\) choosing its freeze/undef values and \(P\) choosing the same where its operand is not poison, and where it is poison choosing \(P'\)'s value — allowed by rule FrzP). By Lemma 13.8.10, each step of \(P\) either reaches UB (then \(P\)'s behaviors include \(P'\)'s) or produces a result at most as defined, so the invariant continues through any number of uses of \(v\) and any branches (a branch whose condition differs is a branch on poison in \(P\): UB). At the end, \(P\)'s outcome allows \(P'\)'s. Since the execution of \(P'\) was arbitrary, \(\mathcal{B}(P') \subseteq \overline{\mathcal{B}(P)}\).

This is the theorem behind every local optimization in the chapter: a peephole rule, a value-numbering replacement or a reassociation proves \(e_S \sqsupseteq e_T\) on a small pattern; Theorem 13.8.11 lifts it to the whole function, and Theorem 13.8.3 chains the steps of a pass and the passes of a pipeline. The hypothesis "\(v\) is an SSA value" matters: with undef, replacing a single value by an expression that is evaluated per use would duplicate choices (Proposition 13.8.12).

Undefined behavior and poison¶

Proposition 13.8.12 (poison, undef and freeze are ordered)

For a value \(v\) of \(\texttt{i}N\): (a) replacing poison by undef, undef by freeze poison, or freeze poison by any constant is a refinement; (b) none of the reverse replacements is; (c) replacing \(f\) = freeze x by two separate freezes of \(x\) at two uses is not a refinement.

Proof

(a) Poison allows every value; undef is, per use, some value; freeze poison is one arbitrary but fixed value; a constant is one value. Each replacement shrinks (or keeps) the set of possible outcomes at every use, and Lemma 13.8.10 with Theorem 13.8.11 lifts this to the program. (b) Each reverse replacement adds an outcome in some context: a constant \(k\) replaced by freeze poison adds every other value; freeze poison replaced by undef in sub v, v turns \(\{0\}\) into all values (the two uses of undef choose independently); undef replaced by poison in and v, 0 turns \(\{0\}\) into \(\{\mathsf{poison}\}\), and a poison outcome is not allowed by \(\{0\}\) (Definition 13.8.4). (c) The source sub (freeze x), (freeze x) with one freeze value \(f\) used twice is always 0; the target with two separate freezes can, for \(x = \mathsf{poison}\), pick different values and return 1, which \(\{0\}\) does not allow (the lab's invalid-freeze-dup test; the reverse direction is valid).

Poison-generating flags¶

Theorem 13.8.13 (Flag transfer; the rules R8 and R10)

If in Algorithm 13.8.7 the source root and the target root carry the same flag \(g \in \{\texttt{nsw}, \texttt{nuw}\}\) and \(\mathrm{ExactEqual}(s, t, g)\) holds (their exact results agree as polynomials when constants are read in \(g\)'s signedness), then whenever \(s\) is not poison, \(g\)'s condition holds at \(t\)'s root, so the target may keep \(g\). In particular: R8 sub x, C \(\Rightarrow\) add x, -C keeps nsw iff \(C \ne \mathrm{INT\_MIN}\) and never keeps nuw (for \(C \ne 0\)); R10 mul x, 2^k \(\Rightarrow\) shl x, k keeps nuw always and nsw iff \(k < N - 1\).

Proof

If \(s\) is not poison, its root's flag condition holds, so the source's exact result lies in \(g\)'s range; the target's exact result is the same integer (ExactEqual), so it lies in the range too, and \(g\)'s condition holds at \(t\) (Definition 13.8.6: for nsw/nuw, the condition is "exact result in range"). R8, nsw: reading constants as signed, \(\widehat{x - C} = x - C\) and \(\widehat{x + (-C)} = x + \mathrm{wrap}(-C)\), equal iff \(\mathrm{wrap}(-C) = -C\), i.e. \(-C\) is representable, i.e. \(C \ne \mathrm{INT\_MIN}\); for \(C = \mathrm{INT\_MIN}\), \(x = -1\) gives source \(-1 - (-128) = 127\) (defined) and target \(-1 + (-128) = -129\) (poison with nsw) on \(\texttt{i}8\). R8, nuw: unsigned, source exact \(x - C\), target exact \(x + (2^N - C)\), never equal for \(0 < C < 2^N\); counterexample \(x = C\): source 0 with nuw defined, target \(\hat r = 2^N\), poison. R10: shl x, k has exact result \(x \cdot 2^k\) both as unsigned and as signed (shl nuw: no set bit shifted out \(\iff x \cdot 2^k < 2^N\) unsigned; shl nsw: the shifted-out bits equal the sign bit \(\iff x \cdot 2^k\) fits signed). mul x, C with \(C = 2^k\): unsigned \(C = 2^k\) always, so nuw transfers; signed, \(C\) reads as \(2^k\) if \(k < N - 1\) (transfer) and as \(-2^{N-1}\) if \(k = N - 1\): then \(x = 1\) gives source \(-2^{N-1}\) (defined with nsw) and target exact \(2^{N-1}\) (poison with nsw).

Theorem 13.8.14 (Flags of R9 add-add-const)

Let \(s = (x + C_1) + C_2\) and \(t = x + (C_1 + C_2)\) on \(\texttt{i}N\), and \(g \in \{\texttt{nsw}, \texttt{nuw}\}\). (a) If both adds of \(s\) have \(g\) and \(C_1 + C_2\) does not overflow in \(g\)'s sense, \(t\) may keep \(g\). (b) If \(C_1 + C_2\) overflows as signed numbers, \(t\) may not keep nsw (for \(N \ge 2\)). (c) If only one add of \(s\) has \(g\), \(t\) may not keep \(g\) in general.

Proof

(a) When \(s\) is not poison, both adds satisfy \(g\), so no wrap occurred and the exact source result is the integer \(x + C_1 + C_2\). The target's exact result is \(x + \mathrm{wrap}(C_1 + C_2) = x + C_1 + C_2\), because the constant sum does not overflow: ExactEqual holds and Theorem 13.8.13 applies. (b) The target's exact result differs from the source's by \(\pm 2^N\); it suffices to find a defined source. With \(C_1, C_2 > 0\) and \(C_1 + C_2 \ge 2^{N-1}\), choose \(x = -C_1\): the inner result is 0 and the outer \(C_2 < 2^{N-1}\), both in range, while the target's exact result is \(-C_1 + (C_1 + C_2 - 2^N)\), which is below \(-2^{N-1}\); the negative case is symmetric. On \(\texttt{i}8\) with \(C_1 = C_2 = 100\), \(x = -100\): source \(0\), then \(100\); target \(-100 + (-56) = -156\): poison. (For nuw, an unsigned overflow of \(C_1 + C_2\) makes every source execution poison — \(x + C_1 + C_2 \ge 2^N\) for all \(x \ge 0\) — so keeping nuw is vacuously allowed; E2 drops it anyway, the conservative choice.) (c) nsw only on the outer add of \((x + 1) + 1\) on \(\texttt{i}8\) with \(x = 127\): the flag-free inner add wraps to \(-128\), the outer gives \(-127\) without overflow, so the source is defined, but the target \(127 + 2\) with nsw is poison.

Example 13.8.15 (R15 icmp-strict and samesign)

icmp sge x, C \(\Rightarrow\) icmp sgt x, C - 1 for \(C \ne \mathrm{INT\_MIN}\) is valid: on the integers \(x \ge C \iff x > C - 1\), and \(C - 1\) does not wrap; for \(C = \mathrm{INT\_MIN}\) the new constant wraps to \(\mathrm{INT\_MAX}\) and the always-true source would become always false. The same holds for sle (\(C \ne \mathrm{INT\_MAX}\)), uge (\(C \ne 0\)) and ule (\(C \ne \mathrm{UINT\_MAX}\)). The flag needs its own case analysis. samesign is poison iff the two operands have different sign bits, so it depends on the constant's sign: when \(C\) and the new constant have the same sign bit, the poison conditions of source and target coincide and samesign may stay. When they differ — sge x, 0 → sgt x, -1, ule x, 127 → ult x, 128 on \(\texttt{i}8\) — the source is poison exactly for negative \(x\) and the target exactly for non-negative \(x\): for \(x = 0\) the source icmp samesign sge i8 0, 0 is true and the target is poison. So R15 keeps samesign only if the sign bit of the constant does not change. This case was missing from the first version of the course's own solution and was found by applying Algorithm 13.8.7 rule by rule, then confirmed with ch13-rewrite-check (tests/ch13/lab/Inputs/invalid-samesign.ll): a reminder that flag rules need a proof for every constant, including the ones where a sign changes.

Floating-point semantics and fast-math¶

Proposition 13.8.16 (The FP rules of E2)

(a) fadd x, -0.0 → x and fsub x, +0.0 → x are valid without flags. (b) fadd x, +0.0 → x and fsub x, -0.0 → x are valid with nsz and invalid without. (c) fsub x, x → +0.0 is valid with nnan and invalid without. (d) fmul x, 1.0 → x is valid without flags (up to the quieting of signaling NaNs, which LLVM does not model by default).

Proof

(a) For \(x \ne \pm 0\) finite: \(x + (-0) = x\) exactly. \((+0) + (-0) = +0\), \((-0) + (-0) = -0\) in round-to-nearest. \(\pm\infty + (-0) = \pm\infty\); NaN stays NaN. \(x - (+0) = x + (-0)\). (b) Without flags, \(x = -0\): \((-0) + (+0) = +0 \ne -0\) (Definition 13.1.9). With nsz, the source's zero operands may have either sign (Definition 13.8.8); choosing the constant as \(-0\) reduces to (a), so \(x\) itself is a possible source outcome. (c) For finite \(x\), \(x - x = +0\) exactly (round-to-nearest); for \(x = \pm\infty\) or NaN the result is NaN, which with nnan is poison and allows anything; without nnan, NaN is not \(+0\). (d) Multiplication by 1 is exact.

Theorem 13.8.17 (Rewrite-based flags must be on every instruction)

Reassociating \((a \oplus b) \oplus c\) into \(a \oplus (b \oplus c)\) for \(\oplus \in \{\texttt{fadd}, \texttt{fmul}\}\) is a refinement only if both source instructions carry reassoc; in general it changes the result.

Proof

The rewrite is a refinement exactly when the rewritten expression's outcome is among the source's; IEEE operations are deterministic, so it must be equal. Counterexample for fadd in double: \(a = 1\), \(b = 10^{16}\), \(c = -10^{16}\): \((a + b) + c = 0\) but \(a + (b + c) = 1\) (Proposition 13.1.14). Hence the rewrite needs a license that changes the semantics: the LangRef makes reassoc rewrite-based and requires it on every instruction involved (Definition 13.8.8); if only the outer fadd has it, the inner one's result must be rounded exactly as written, and the counterexample still applies.

When it breaks. Most historical InstCombine bugs found by Alive are flag transfers without ExactEqual [LMNR15]; most undef bugs are use-duplications (Proposition 13.8.12 (c) and Lesson 9.7 Proposition 9.7.14); most FP bugs ignore \(-0\) or NaN (Proposition 13.8.16). And Example 13.8.15 shows how easily a flag slips through: a case analysis must cover every constant, including the one where the sign changes.

5. Complexity¶

Technique	Time (worst)	Time (typical)	Space	Variables
Refinement check by enumeration	\(O\big((2^N + 1)^{a} \cdot 2^{F} \cdot n\big)\)	\(a \le 2\), \(N \le 8\): \(< 1\) s	\(O(2^{F})\) outcome set	\(a\) arguments of \(N\) bits, \(F\) bits of `freeze` choices, \(n\) instructions
Refinement check with SMT (Alive2)	NP-hard (bit-vector satisfiability); with nondeterminism \(\exists\forall\)	seconds for peepholes	solver memory	—
Flag transfer (Algorithm 13.8.7)	polynomial comparison \(O(\ell)\) + a counterexample search as above	instant	\(O(\ell)\)	\(\ell\) pattern size
FP rule check on special values	\(O(c^{k})\)	\(c \approx 12\) special values, \(k \le 3\) operands	\(O(1)\)	—

Justification. Enumeration runs both programs on every input (each argument has \(2^N + 1\) values including poison) and, for the source, on every assignment of freeze choices; the lab's checker does exactly this (Algorithm 13.9.6). Pathological family: each extra freeze of an \(\texttt{i}8\) multiplies the work by 256, so a rewrite with 3 freezes on the source and 2 arguments needs \(257^2 \cdot 2^{24} \approx 1.1 \cdot 10^{12}\) source runs: beyond enumeration, the point where SMT (with quantifiers over the choices) takes over (Lesson 13.9).

Refinement with memory (Alive2 [LLM+21]; Lee et al.'s memory model): behaviors include the final memory, and refinement must account for pointer provenance; trade-off: much harder to automate.
Simulation relations (forward/backward simulation in CompCert [Ler09]) prove refinement for whole compilers, loops and non-termination included; trade-off: interactive proofs.
Refinement for concurrency (weak memory models; Ch 19's scope).

Undefined behavior and poison¶

Removing undef: LLVM migrates uninitialized memory to poison or a byte type and forbids new undef uses (Lesson 9.7 §6); trade-off: compatibility.
Freeze placement in loop unswitching and select-to-branch conversion [LHK+17]; trade-off: a freeze blocks some optimizations (it is opaque to poison-based reasoning).

Poison-generating flags¶

Flag inference (InstCombine adds nneg, disjoint, samesign, nuw nsw when known bits prove the condition — box in §7); trade-off: analysis cost, but later passes profit.
Dropping instead of proving (dropPoisonGeneratingFlags, recommended by the InstCombine guide when a proof is complicated [LLVM-ICGuide]); trade-off: lost information.

Floating-point semantics and fast-math¶

Per-flag fast-math vs global -ffast-math (which also assumes no NaN/Inf inputs via nofpclass attributes, box in §7); trade-off: precision vs portability.
Constrained FP intrinsics / strictfp model rounding modes and exceptions; trade-off: blocks almost all optimization.
Alive-FP [MNG16] and Alive2's FP encoding verify FP rules including fast-math flags (Lesson 13.9).

7. In real compilers¶

Alive2: refinement in one direction, not the other

Reproduce (alive-tv from Alive2 commit 01a5ec4, built against LLVM 23.1.2, Z3 4.8.12; sed):

cat > fwd.ll <<'EOF'
define i1 @src(i8 %x) {
  %a = add nsw i8 %x, 1
  %r = icmp sgt i8 %a, %x
  ret i1 %r
}
define i1 @tgt(i8 %x) {
  ret i1 true
}
EOF
sed -e 's/@src(/@tmp(/; s/@tgt(/@src(/; s/@tmp(/@tgt(/' fwd.ll > bwd.ll       # swap the roles
echo "=== forward";  alive-tv fwd.ll | sed -n '/^Transformation/p;/^ERROR/,/^$/p'
echo "=== backward"; alive-tv bwd.ll | sed -n '/^Transformation/p;/^ERROR/,/^Target value/p'

Output (complete):

=== forward
Transformation seems to be correct!
=== backward
Transformation doesn't verify!
ERROR: Target is more poisonous than source

Example:
i8 %x = #x7f (127)

Source:

Target:
i8 %a = poison
i1 %r = poison
Source value: #x1 (1)
Target value: poison

What to notice: x + 1 > x (with nsw) → true verifies; the reverse "rewrite" fails with Target is more poisonous than source at \(x = 127\), exactly the Example after Definition 13.8.2: refinement is a preorder, not an equivalence.

Undefined behavior and poison¶

select vs branch vs frozen branch, executed by llubi

Reproduce (llubi 23.1.2; any OS):

cat > sel.ll <<'EOF'
define i32 @pick(i1 %c, i32 %x, i32 %y) {
  %r = select i1 %c, i32 %x, i32 %y
  ret i32 %r
}
define i32 @pick_br(i1 %c, i32 %x, i32 %y) {
entry:
  br i1 %c, label %t, label %j
t:
  br label %j
j:
  %r = phi i32 [ %x, %t ], [ %y, %entry ]
  ret i32 %r
}
define i32 @pick_br_frozen(i1 %c, i32 %x, i32 %y) {
entry:
  %f = freeze i1 %c
  br i1 %f, label %t, label %j
t:
  br label %j
j:
  %r = phi i32 [ %x, %t ], [ %y, %entry ]
  ret i32 %r
}
define i32 @main() {
  %big = add nsw i32 2147483647, 1
  %c = icmp sgt i32 %big, 0
  %a = call i32 @pick(i1 %c, i32 1, i32 2)
  %b = call i32 @pick_br_frozen(i1 %c, i32 1, i32 2)
  %d = call i32 @pick_br(i1 %c, i32 1, i32 2)
  ret i32 0
}
EOF
llubi --verbose sel.ll; echo "exit status $?"

Output (complete):

Entering function: main
  %big = add nsw i32 2147483647, 1 => poison
  %c = icmp sgt i32 %big, 0 => poison
Entering function: pick
  i1 %c = poison
  i32 %x = i32 1
  i32 %y = i32 2
  %r = select i1 %c, i32 %x, i32 %y => poison
  ret i32 %r
Exiting function: pick
  %a = call i32 @pick(i1 %c, i32 1, i32 2) => poison
Entering function: pick_br_frozen
  i1 %c = poison
  i32 %x = i32 1
  i32 %y = i32 2
  %f = freeze i1 %c => F
  br i1 %f, label %t, label %j jump to %j
  %r = phi i32 [ %x, %t ], [ %y, %entry ] => i32 2
  ret i32 %r
Exiting function: pick_br_frozen
  %b = call i32 @pick_br_frozen(i1 %c, i32 1, i32 2) => i32 2
Entering function: pick_br
  i1 %c = poison
  i32 %x = i32 1
  i32 %y = i32 2
Stacktrace:
#0   br i1 %c, label %t, label %j at @pick_br sel.ll:7
#1   %d = call i32 @pick_br(i1 %c, i32 1, i32 2) at @main sel.ll:29
Immediate UB detected: Branch on poison condition.
error: Execution of function 'main' failed.
exit status 1

What to notice: with a poison condition, select returns poison (a value), the frozen branch returns 2 (freeze picked false), and the unfrozen branch is immediate UB — the table in §3; Alive2 rejects the unfrozen conversion with "Source is more defined than target" (run alive-tv on @pick and @pick_br renamed to @src and @tgt; Lesson 13.9).

undef breaks a textbook strength reduction

Reproduce (alive-tv, Alive2 commit 01a5ec4):

cat > undef.ll <<'EOF'
define i8 @src(i8 %x) {
  %r = mul i8 %x, 2
  ret i8 %r
}
define i8 @tgt(i8 %x) {
  %r = add i8 %x, %x
  ret i8 %r
}
EOF
echo "=== undef inputs allowed (the default)"; alive-tv undef.ll | sed -n '/^Transformation/p;/^ERROR/,/^Target value/p'
echo "=== --disable-undef-input";              alive-tv --disable-undef-input undef.ll | grep '^Transformation'

Output (complete):

=== undef inputs allowed (the default)
Transformation doesn't verify!
ERROR: Value mismatch

Example:
i8 %x = undef

Source:
i8 %r = #x06 (6)    [based on undef]

Target:
i8 %r = #x01 (1)
Source value: #x06 (6)  [based on undef]
Target value: #x01 (1)
=== --disable-undef-input
Transformation seems to be correct!

What to notice: mul x, 2 → add x, x fails when %x may be undef (Alive2's counterexample: the source's single use picked 3, giving 6; the target's two uses picked different values giving 1) and verifies with --disable-undef-input: the first row of §3's table and Proposition 13.8.12.

Poison-generating flags¶

InstCombine infers flags from known bits

Reproduce (opt 23.1.2; any OS):

cat > infer.ll <<'EOF'
define i32 @sext_pos(i8 %x) {
  %a = lshr i8 %x, 1
  %r = sext i8 %a to i32
  ret i32 %r
}
define i8 @add_disjoint(i8 %x, i8 %y) {
  %lo = and i8 %x, 15
  %hi = shl i8 %y, 4
  %r = add i8 %lo, %hi
  ret i8 %r
}
define i1 @slt_same(i8 %x, i8 %y) {
  %a = lshr i8 %x, 1
  %b = lshr i8 %y, 1
  %r = icmp slt i8 %a, %b
  ret i1 %r
}
define i16 @add_zext(i8 %x, i8 %y) {
  %a = zext i8 %x to i16
  %b = zext i8 %y to i16
  %r = add i16 %a, %b
  ret i16 %r
}
EOF
opt -passes=instcombine -S infer.ll | grep -v '^;\|^$\|source_filename\|^define\|^}\|ret '

Output (complete):

  %a = lshr i8 %x, 1
  %r = zext nneg i8 %a to i32
  %lo = and i8 %x, 15
  %hi = shl i8 %y, 4
  %r = or disjoint i8 %lo, %hi
  %a = lshr i8 %x, 1
  %b = lshr i8 %y, 1
  %r = icmp samesign ult i8 %a, %b
  %a = zext i8 %x to i16
  %b = zext i8 %y to i16
  %r = add nuw nsw i16 %a, %b

What to notice: a sext of a value with a known-zero sign bit becomes zext nneg; an add of operands with no common bits becomes or disjoint; a signed compare of two non-negative values becomes icmp samesign ult; the sum of two zero-extended i8s cannot overflow i16 in either sense, so it gets nuw nsw. Each new flag is justified by the condition of Definition 13.8.6, proved with computeKnownBits (llvm/lib/Analysis/ValueTracking.cpp).

Floating-point semantics and fast-math¶

clang's fast-math options, flag by flag

Reproduce (clang 23.1.2; any OS):

cat > fm.c <<'EOF'
double self_sub(double x)         { return x - x; }
double add_zero(double x)         { return x + 0.0; }
double cancel(double a, double b) { return (a + b) - a; }
double mul_add(double a, double b, double c) { return a * b + c; }
EOF
for f in "" -fno-signed-zeros -ffast-math -ffp-contract=off; do
  echo "=== clang-23 -O2 $f"
  clang-23 --target=x86_64-unknown-linux-gnu -O2 $f -S -emit-llvm -o - fm.c \
    | grep -P '^  (%|ret|tail)' 
done

Output (complete):

=== clang-23 -O2 
  %2 = fsub double %0, %0
  ret double %2
  %2 = fadd double %0, 0.000000e+00
  ret double %2
  %3 = fadd double %0, %1
  %4 = fsub double %3, %0
  ret double %4
  %4 = tail call double @llvm.fmuladd.f64(double %0, double %1, double %2)
  ret double %4
=== clang-23 -O2 -fno-signed-zeros
  %2 = fsub nsz double %0, %0
  ret double %2
  ret double %0
  %3 = fadd nsz double %0, %1
  %4 = fsub nsz double %3, %0
  ret double %4
  %4 = tail call nsz double @llvm.fmuladd.f64(double %0, double %1, double %2)
  ret double %4
=== clang-23 -O2 -ffast-math
  ret double 0.000000e+00
  ret double %0
  ret double %1
  %4 = fmul fast double %1, %0
  %5 = fadd fast double %4, %2
  ret double %5
=== clang-23 -O2 -ffp-contract=off
  %2 = fsub double %0, %0
  ret double %2
  %2 = fadd double %0, 0.000000e+00
  ret double %2
  %3 = fadd double %0, %1
  %4 = fsub double %3, %0
  ret double %4
  %4 = fmul double %0, %1
  %5 = fadd double %4, %2
  ret double %5

What to notice: by default nothing is folded (Proposition 13.8.16 (b), (c), Theorem 13.8.17), but a * b + c becomes llvm.fmuladd, because clang's default for C is -ffp-contract=on (contraction within one expression). -fno-signed-zeros adds nsz and allows x + 0.0 → x, but not x - x → 0 (that needs nnan). -ffast-math adds fast and nofpclass(nan inf) on arguments, and folds all three. -ffp-contract=off keeps a separate multiply and add.

The LangRef's definitions of nsz and rewrite-based flags

Reproduce (LLVM 23.1.2 sources; curl):

curl -sL https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-23.1.2/llvm/docs/LangRef.md > LangRef.md
grep -A3 '^`nsz`$' LangRef.md
sed -n '/^#### Rewrite-based flags$/,/^generally have the intersection of the flags present on the input instruction\.$/p' LangRef.md

Output (complete):

`nsz`
:   No Signed Zeros - Unless otherwise mentioned, the sign bit of 0.0 or -0.0
   input operands can be non-deterministically flipped. This does not imply
   that -0.0 is poison and/or guaranteed to not exist in the operation.
#### Rewrite-based flags

The following flags have rewrite-based semantics. These flags allow expressions,
potentially containing multiple non-consecutive instructions, to be rewritten
into alternative instructions. When multiple instructions are involved in an
expression, it is necessary that all of the instructions have the necessary
rewrite-based flag present on them, and the rewritten instructions will
generally have the intersection of the flags present on the input instruction.

What to notice: nsz is defined on operands (their zero sign may be flipped), which is what makes x + 0.0 → x valid under nsz in Proposition 13.8.16 (b); rewrite-based flags must be present on all instructions of the rewritten expression (Theorem 13.8.17).

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Refinement	The correctness criterion: allows removing UB and nondeterminism, never adding them	Deciding it: Lesson 13.9	Counterexamples pinpoint inputs	Conceptual; tools do the work	Specifying every optimization; Alive2, CompCert
Undefined behavior and poison	Poison defers UB so speculation is sound; `freeze` stops propagation	—	Subtle: `undef` duplication bugs	High (every pass must respect it)	LLVM IR semantics, Rust MIR (UB), C/C++ front ends
Poison-generating flags	Carry source-level facts (no overflow, exactness) into the IR	\(O(1)\) per rule to decide with ExactEqual	Most peephole bugs are flag bugs	Medium per rule	InstCombine, E2, reassociation (E5), LVN (E3)
Floating-point semantics and fast-math	IEEE exactness by default; per-flag licenses	—	Rules must consider \(-0\), NaN, \(\infty\)	Medium	Numerics; `-ffast-math`, `-ffp-contract`

Choose refinement as the criterion for every transformation, and check it rather than argue it. Choose poison and freeze over undef in any new IR design (Lesson 8 of Ch 9 and [LHK+17]). Choose flag transfer by exact values (Algorithm 13.8.7) when writing a rule; drop the flag when the proof is not immediate. Choose per-flag FP licenses (nsz, nnan, contract) rather than -ffast-math when only some rewrites are wanted.

9. Assessment¶

Technique	Quiz questions	Drills	Flashcards	Exercises
Refinement	`refine-closure`, `refine-direction`	`./course drill rewrite-validity`	tag `refinement`	Lab Part B
Undefined behavior and poison	`freeze-dup`, `select-branch`	`./course drill poison-propagation` (Ch 9), `./course drill rewrite-validity --difficulty medium`	tag `ub-poison`	E3 (flags on merge), Lab Part B
Poison-generating flags	`flags-r9`, `flags-mul-min`, `find-flags-dropped`	`./course drill flags` (Ch 9), `./course drill rewrite-validity --difficulty easy`	tag `flags`	E2, E5
Floating-point semantics and fast-math	`fp-nsz`, `fp-contract`	`./course drill rewrite-validity` (integer only) — justification for FP: the FP rules are few and fixed; the quiz and E2's FP tests cover them	tag `fast-math`	E1 (FP folding), E2 (R16, R17)

References¶

See the chapter references.

Lesson 13.8 — Transformation correctness: refinement, undefined behavior, flags and fast-math¶

1. Problem and motivation¶

Refinement¶

Undefined behavior and poison¶

Poison-generating flags¶

Floating-point semantics and fast-math¶

2. Definitions and algorithms¶

Refinement¶

Undefined behavior and poison¶

Poison-generating flags¶

Floating-point semantics and fast-math¶

3. Worked example¶

Refinement¶

Undefined behavior and poison¶

Poison-generating flags¶

Floating-point semantics and fast-math¶

4. Invariants and correctness¶

Refinement¶

Undefined behavior and poison¶

Poison-generating flags¶

Floating-point semantics and fast-math¶

5. Complexity¶

Refinement¶

Undefined behavior and poison¶

Poison-generating flags¶

Floating-point semantics and fast-math¶

7. In real compilers¶

Refinement¶

Undefined behavior and poison¶

Poison-generating flags¶

Floating-point semantics and fast-math¶

8. Comparison¶

9. Assessment¶

References¶

Lesson 13.8 — Transformation correctness: refinement, undefined behavior, flags and fast-math¶

1. Problem and motivation¶

Refinement¶

Undefined behavior and poison¶

Poison-generating flags¶

Floating-point semantics and fast-math¶

2. Definitions and algorithms¶

Refinement¶

Undefined behavior and poison¶

Poison-generating flags¶

Floating-point semantics and fast-math¶

3. Worked example¶

Refinement¶

Undefined behavior and poison¶

Poison-generating flags¶

Floating-point semantics and fast-math¶

4. Invariants and correctness¶

Refinement¶

Undefined behavior and poison¶

Poison-generating flags¶

Floating-point semantics and fast-math¶

5. Complexity¶

6. Variants and refinements¶

Refinement¶

Undefined behavior and poison¶

Poison-generating flags¶

Floating-point semantics and fast-math¶

7. In real compilers¶

Refinement¶

Undefined behavior and poison¶

Poison-generating flags¶

Floating-point semantics and fast-math¶

8. Comparison¶

9. Assessment¶

References¶