Lesson 14.7 — Abstract interpretation: Galois connections, domains, widening¶

Techniques: Galois connections and sound abstract transformers (Cousot–Cousot 1977, 1979); non-relational domains — signs, constants, intervals, congruences; relational domains — octagons, polyhedra; widening and narrowing · Pebble implements: interval analysis of LLVM IR with widening and narrowing (exercise E6, print<pebble-intervals>) · Lab: soundness against concrete runs (tests/ch14/lit/intervals-sound.c, ch14.Intervals.*) · Prerequisites: Lessons 14.1–14.4 · Time: 7–9 hours

What values can i take at the loop head of i = 0; while (i < 10) i = i + 1;? The concrete answer is the set \(\{0, 1, \dots, 10\}\). The classic analyses of Lesson 14.3 cannot express it; the interval \([0, 10]\) can. But the interval lattice has infinite height, so Kleene iteration climbs \([0,0] \sqsubset [0,1] \sqsubset \cdots\) one trip at a time — 12 iterations here, a billion for i < 1000000000. Abstract interpretation explains what "the interval \([0, 10]\)" means (a Galois connection to sets of states), how to derive sound transfer functions, which domains trade precision for cost (signs, constants, intervals, congruences, octagons, polyhedra), and how widening jumps to a sound answer in a few steps and narrowing recovers precision.

1. Problem and motivation¶

Patrick and Radhia Cousot unified program analysis in 1977: every analysis is an approximation of the program's collecting semantics — the set of states reaching each point — computed in an abstract lattice related to the concrete one by a Galois connection [CC77]. The same paper introduced widening and narrowing to compute fixed points in lattices of infinite height, with the interval domain as the example. The 1979 paper systematized the design of analyses and their combination [CC79]. Relational domains followed: convex polyhedra [CH78] and, as a cheaper middle ground, octagons [Min06]. Industrial analyzers built on these ideas prove the absence of run-time errors in avionics code (Astrée [BCC+03]); compilers use the cheap non-relational domains: LLVM's ConstantRange/LazyValueInfo (intervals) and KnownBits (bit-level congruences), GCC's Ranger, MLIR's IntegerRangeAnalysis. Pebble's E6 is an interval analysis of LLVM IR checked against concrete executions.

Galois connections¶

A Galois connection pairs an abstraction \(\alpha\) (sets of concrete values → abstract value) with a concretization \(\gamma\) (abstract value → the set it describes) so that "\(\alpha(C) \sqsubseteq a\) iff \(C \subseteq \gamma(a)\)" [CC77, CC79]. It defines the best abstract transformer of every concrete operation and turns soundness into one inequality to check per operation. The textbook treatment, with full proofs, is [NNH, Ch. 4].

Non-relational domains¶

A non-relational domain abstracts each variable separately: signs \(\{\bot, -, 0, +, \top\}\) and refinements; constants \(\mathbb{Z}_\bot^\top\) [Kil73]; intervals \([a, b]\) [CC76, CC77]; congruences \(a\mathbb{Z} + b\) [Gra89]. They cost \(O(1)\) (congruences: a gcd) per operation per variable, and cannot express relations such as \(j = i\).

Relational domains¶

Relational domains keep constraints between variables: octagons \(\pm x \pm y \le c\) [Min06] at \(O(n^2)\) space and \(O(n^3)\) time, and convex polyhedra \(\sum a_i x_i \le c\) [CH78] with worst-case exponential cost but arbitrary linear invariants such as \(j = 2i\).

Widening and narrowing¶

A widening \(\nabla\) extrapolates an ascending sequence to a post-fixed point in finitely many steps; a narrowing \(\Delta\) then refines it without losing soundness [CC77]. They make intervals, octagons and polyhedra usable, and are the reason every abstract interpreter — and E6 — terminates.

2. Definitions and algorithms¶

Definition 14.7.1 (Collecting semantics)

Let \(\Sigma\) be the set of program states (a map from variables to values). The concrete domain is \((\mathcal{P}(\Sigma), \subseteq)\). Each statement \(s\) has a concrete transfer function \(\llbracket s \rrbracket : \mathcal{P}(\Sigma) \to \mathcal{P}(\Sigma)\), the image of the set under \(s\) (a branch condition keeps the states satisfying it). The collecting semantics assigns to each program point the set of states reaching it on some execution: the least fixed point of the equations of Lesson 14.2 in \(N \to \mathcal{P}(\Sigma)\), with join \(\cup\) and entry value \(\Sigma_0\) (the initial states). It is exact and not computable in general.

Galois connections¶

Definition 14.7.2 (Galois connection)

Let \((C, \subseteq)\) and \((A, \sqsubseteq)\) be complete lattices. Monotone maps \(\alpha : C \to A\) and \(\gamma : A \to C\) form a Galois connection \((C, \subseteq) \underset{\alpha}{\overset{\gamma}{\leftrightarrows}} (A, \sqsubseteq)\) if for all \(c \in C, a \in A\): \(\alpha(c) \sqsubseteq a \iff c \subseteq \gamma(a)\). An abstract function \(f^{\sharp} : A \to A\) is a sound abstraction of \(f : C \to C\) if \(f \circ \gamma \subseteq \gamma \circ f^{\sharp}\) pointwise, i.e. \(\alpha \circ f \circ \gamma \sqsubseteq f^{\sharp}\); the best abstraction is \(f^{\sharp} = \alpha \circ f \circ \gamma\).

The interval Galois connection

\(C = \mathcal{P}(\mathbb{Z})\), \(A\) = intervals \([a, b]\) with \(a \le b \in \mathbb{Z} \cup \{-\infty, +\infty\}\), plus \(\bot\). \(\gamma([a, b]) = \{\, x \mid a \le x \le b \,\}\), \(\alpha(\emptyset) = \bot\), \(\alpha(X) = [\min X, \max X]\) (with \(\pm\infty\) for unbounded \(X\)). \(\alpha(\{0, 3, 7\}) = [0, 7]\); the best abstraction of x + 1 is \([a, b] \mapsto [a + 1, b + 1]\); of x * x it is \([\min, \max]\) of the squares over the interval, not \([a, b] \times [a, b]\) computed by the product rule (which gives \([-3, 9]\) for \([-1, 3]\) instead of the best \([0, 9]\)).

Lemma 14.7.3 (Properties of Galois connections)

In a Galois connection: (1) \(c \subseteq \gamma(\alpha(c))\) and \(\alpha(\gamma(a)) \sqsubseteq a\); (2) \(\alpha\) preserves joins: \(\alpha(\bigcup_i c_i) = \bigsqcup_i \alpha(c_i)\); (3) \(\alpha\) determines \(\gamma\) and vice versa: \(\gamma(a) = \bigcup \{\, c \mid \alpha(c) \sqsubseteq a \,\}\); (4) \(\alpha \circ f \circ \gamma\) is the most precise sound abstraction of \(f\).

Proof

(1) Take \(a = \alpha(c)\) in the defining equivalence: \(\alpha(c) \sqsubseteq \alpha(c)\) gives \(c \subseteq \gamma(\alpha(c))\); take \(c = \gamma(a)\): \(\gamma(a) \subseteq \gamma(a)\) gives \(\alpha(\gamma(a)) \sqsubseteq a\). (2) \(\alpha(\bigcup c_i) \sqsubseteq a \iff \bigcup c_i \subseteq \gamma(a) \iff \forall i.\ c_i \subseteq \gamma(a) \iff \forall i.\ \alpha(c_i) \sqsubseteq a \iff \bigsqcup \alpha(c_i) \sqsubseteq a\); two elements with the same upper bounds are equal. (3) By the equivalence, \(\{c \mid \alpha(c) \sqsubseteq a\} = \{c \mid c \subseteq \gamma(a)\}\), whose union is \(\gamma(a)\). (4) \(f^{\sharp}\) is sound iff \(f(\gamma(a)) \subseteq \gamma(f^{\sharp}(a))\) for all \(a\), iff \(\alpha(f(\gamma(a))) \sqsubseteq f^{\sharp}(a)\) by the equivalence: every sound \(f^{\sharp}\) is above \(\alpha \circ f \circ \gamma\), which is itself sound. \(\square\)

Theorem 14.7.4 (Fixed-point transfer: sound abstract analysis)

Let \(F : C \to C\) be monotone (the collecting semantics' equation function), \(F^{\sharp} : A \to A\) monotone and sound (\(\alpha \circ F \circ \gamma \sqsubseteq F^{\sharp}\)). Then \(\mathrm{lfp}(F) \subseteq \gamma(\mathrm{lfp}(F^{\sharp}))\), and more generally \(\mathrm{lfp}(F) \subseteq \gamma(a)\) for every \(a\) with \(F^{\sharp}(a) \sqsubseteq a\).

Proof

Let \(a\) satisfy \(F^{\sharp}(a) \sqsubseteq a\) (for example \(a = \mathrm{lfp}(F^{\sharp})\)). Then \(F(\gamma(a)) \subseteq \gamma(\alpha(F(\gamma(a))))\) by Lemma 14.7.3(1), \(\subseteq \gamma(F^{\sharp}(a))\) by soundness and monotonicity of \(\gamma\), \(\subseteq \gamma(a)\) by monotonicity of \(\gamma\). So \(\gamma(a)\) is a pre-fixed point of \(F\) in \(C\), and \(\mathrm{lfp}(F) \subseteq \gamma(a)\) by Theorem 14.1.12. \(\square\)

An abstract value in Clang's static analyzer

Reproduce (clang 23.1.2):

cat > csa.c <<'EOF'
void clang_analyzer_value(int);
void clang_analyzer_eval(int);
int f(int x) {
  if (x > 10 && x < 20) {
    int y = x * 2;
    clang_analyzer_value(x);
    clang_analyzer_eval(x != 5);
  }
  return 0;
}
EOF
clang-23 --analyze -Xclang -analyzer-checker=debug.ExprInspection csa.c 2>&1 | grep 'warning:'

Output:

csa.c:5:9: warning: Value stored to 'y' during its initialization is never read [deadcode.DeadStores]
csa.c:6:5: warning: 32s:{ [11, 19] } [debug.ExprInspection]
csa.c:7:5: warning: TRUE [debug.ExprInspection]

What to notice: the analyzer does not track the set \(\{11, \dots, 19\}\) of values of x on this path; it tracks the abstract value 32s:{ [11, 19] } (32-bit signed, a union of ranges), exactly \(\alpha\) of that set in a domain of range sets. Queries are answered on \(\gamma\) of it: x != 5 holds for every value in \(\gamma([11, 19])\), so the answer is TRUE (Theorem 14.7.4's soundness in action). The deadcode.DeadStores line is the liveness client of Lesson 14.3.

Non-relational domains¶

Definition 14.7.5 (Signs, constants, intervals, congruences)

Each is a lattice \(A\) with a Galois connection to \(\mathcal{P}(\mathbb{Z})\); a state is abstracted variable-wise into \(\mathit{Vars} \to A\) (a non-relational domain):

Signs \(\{\bot, -, 0, +, \top\}\) (Hasse: \(\bot\) below \(-, 0, +\), below \(\top\)): \(\gamma(-) = \mathbb{Z}_{<0}\), \(\gamma(0) = \{0\}\), \(\gamma(+) = \mathbb{Z}_{>0}\). Abstract +: \((+) + (+) = +\), \((+) + (-) = \top\), \((0) + s = s\).
Constants \(\mathbb{Z}_\bot^\top\) (Definition 14.3.16): \(\gamma(c) = \{c\}\), \(\gamma(\top) = \mathbb{Z}\).
Intervals \(\mathcal{I}\): \([a, b] \sqcup [c, d] = [\min(a,c), \max(b,d)]\), \([a,b] \sqcap [c,d] = [\max(a,c), \min(b,d)]\) (or \(\bot\)), \([a,b] + [c,d] = [a+c, b+d]\), \([a,b] \times [c,d] = [\min P, \max P]\) with \(P = \{ac, ad, bc, bd\}\); conditions refine: after x < k holds, \(x \in [a, \min(b, k-1)]\).
Congruences \(a\mathbb{Z} + b\) (\(a \ge 0\), \(0 \le b < a\) when \(a > 0\); \(0\mathbb{Z} + b\) is the constant \(b\)): \(\gamma(a\mathbb{Z} + b) = \{\, a k + b \mid k \in \mathbb{Z} \,\}\); join \((a\mathbb{Z} + b) \sqcup (c\mathbb{Z} + d) = \gcd(a, c, \lvert b - d \rvert)\mathbb{Z} + b\); \((a\mathbb{Z} + b) + (c\mathbb{Z} + d) = \gcd(a, c)\mathbb{Z} + (b + d)\).

Heights: signs 2, constants 2, congruences infinite (but ACC holds: a strictly ascending chain divides the modulus each step, so has length at most the number of prime factors of the first nonzero modulus plus 2), intervals infinite with infinite ascending chains.

The four domains on the loop head of i = 0; while (i < 10) i = i + 2;

Concrete: \(\{0, 2, 4, 6, 8, 10\}\). Signs: \(\alpha = \top\) (it contains \(0\) and \(+\); a refined sign lattice with \(\ge 0\) gives \(\ge 0\)). Constants: \(\top\). Intervals: \([0, 10]\) (with widening and narrowing, §3). Congruences: \(2\mathbb{Z} + 0\) ("\(i\) is even"). The reduced product of intervals and congruences [CC79] gives "even and in \([0, 10]\)" — exactly the concrete set.

A bit-level congruence domain in LLVM: KnownBits

Reproduce (opt 23.1.2):

cat > kb.ll <<'EOF'
define i32 @k(i32 %x) {
  %y = shl i32 %x, 2
  %z = or i32 %y, 1
  %r = and i32 %z, 3
  ret i32 %r
}
EOF
opt -passes=instcombine -S kb.ll | sed -n '/^define/,/^}/p'

Output:

define i32 @k(i32 %x) {
  ret i32 1
}

What to notice: KnownBits (llvm/include/llvm/Support/KnownBits.h) [LLVM-KB] abstracts a value by which bits are known 0 and known 1 — a product of per-bit three-valued lattices. Knowing that the low \(k\) bits of a value are \(b\) is the congruence \(2^{k}\mathbb{Z} + b\) of Definition 14.7.5: shl 2 makes the low two bits known zero (\(4\mathbb{Z} + 0\)), or 1 makes them 01 (\(4\mathbb{Z} + 1\)), so and 3 is the constant 1. InstCombine queries computeKnownBits and folds the whole function.

Relational domains¶

Definition 14.7.6 (Octagons and polyhedra)

For variables \(x_1, \dots, x_n\), an octagon is a conjunction of constraints \(\pm x_i \pm x_j \le c\) (including \(x_i \le c\) as \(x_i + x_i \le 2c\)), represented as a difference-bound matrix (DBM) \(m\) of size \(2n \times 2n\) over \(\mathbb{Z} \cup \{+\infty\}\) on the variables \(v_{2i} = x_i\), \(v_{2i+1} = -x_i\), with \(m_{pq}\) bounding \(v_q - v_p\). A convex polyhedron is a conjunction of linear constraints \(\sum_i a_i x_i \le c\) (equivalently, by Minkowski–Weyl, the convex hull of vertices plus rays). Joins: octagons take the componentwise maximum of closed DBMs; polyhedra take the convex hull.

Algorithm 14.7.7 (Octagon strong closure, Miné)

Input: a DBM \(m\) (\(2n \times 2n\)) of an octagon.
Output: the strongly closed DBM \(m^{\bullet}\) with the same concretization, or "empty".
Precondition: \(m\) is coherent: \(m_{pq} = m_{\bar{q}\bar{p}}\) where \(\bar{p}\) is \(p\) with its low bit flipped.
Postcondition: every entry is the tightest bound implied by the constraints (Theorem 14.7.8); the octagon is empty iff some \(m_{pp} < 0\).
Invariant: after round \(k\), \(m_{pq}\) is the tightest bound using only intermediate variables \(v_0 .. v_{2k+1}\), followed by the strengthening step.

function StrongClose(m, n):                     # indices 0 .. 2n-1
    for k in 0 .. n-1:
        for p in 0 .. 2n-1:
            for q in 0 .. 2n-1:                    # shortest paths through v_2k and v_2k+1
                m[p][q] ← min(m[p][q],
                              m[p][2k]   + m[2k][q],
                              m[p][2k+1] + m[2k+1][q],
                              m[p][2k]   + m[2k][2k+1] + m[2k+1][q],
                              m[p][2k+1] + m[2k+1][2k] + m[2k][q])
        for p, q in 0 .. 2n-1:                     # strengthening: v_q - v_p ≤ (v_q - v_q̄ + v_p̄ - v_p)/2
            m[p][q] ← min(m[p][q], floor((m[p][p̄] + m[q̄][q]) / 2))
    for p in 0 .. 2n-1:
        if m[p][p] < 0: return empty
        m[p][p] ← 0
    return m

Theorem 14.7.8 (Strong closure is the tightest representation)

For a non-empty coherent DBM over \(\mathbb{Q}\), Algorithm 14.7.7 returns the unique DBM whose every entry equals the maximum of \(v_q - v_p\) over the octagon; over \(\mathbb{Z}\) the result is tight up to the rounding of the strengthening step (integer tightening needs an extra step). It runs in \(O(n^3)\) time.

Proof sketch (full proof: [Min06])

The first inner loops are Floyd–Warshall on the graph whose edges are the DBM entries, restricted to pairs of intermediates \(\{v_{2k}, v_{2k+1}\}\) at once so that coherence is preserved; shortest paths are exactly the bounds derivable by adding constraints. Strengthening adds the only other derivation that octagonal constraints allow: from \(2x_i \le a\) and \(-2x_j \le b\) infer \(x_i - x_j \le (a + b)/2\). Miné proves that interleaving the two per round reaches a fixed point after \(n\) rounds, and that the result is the tightest (the saturation argument of [Min06]). Cost: \(n\) rounds of \(O((2n)^2)\) updates.

A polyhedral join finds j = 2i: the isl library (via islpy)

Reproduce (islpy 2026.2.2, which bundles isl — the library LLVM's Polly and GCC's Graphite use; Python via uv):

cat > poly.py <<'EOF'
import islpy as isl

# (i, j) at the loop head of  i = 0; j = 0; while (...) { i = i + 1; j = j + 2; }
# after 0, 1 and 2 trips
states = (isl.Set("{ [i, j] : i = 0 and j = 0 }")
          .union(isl.Set("{ [i, j] : i = 1 and j = 2 }"))
          .union(isl.Set("{ [i, j] : i = 2 and j = 4 }")))
print("concrete states :", states)
print("polyhedral join :", states.convex_hull())
i_range = states.project_out(isl.dim_type.set, 1, 1).convex_hull()
j_range = states.project_out(isl.dim_type.set, 0, 1).convex_hull()
print("interval join   :", i_range, "x", j_range)
EOF
uv run --no-project --with islpy==2026.2.2 python poly.py

Output:

concrete states : { [i = 2, j = 4]; [i = 1, j = 2]; [i = 0, j = 0] }
polyhedral join : { [i, j] : j = 2i and 0 <= i <= 2 }
interval join   : { [i] : 0 <= i <= 2 } x { [j] : 0 <= j <= 4 }

What to notice: the polyhedral join (convex hull, Definition 14.7.6) of the three states keeps the relation \(j = 2i\); the interval join keeps only the bounding box, which also contains \((2, 0)\). Octagons would keep \(j - i \in [0, 2]\) and \(j + i \in [0, 6]\) but not \(j = 2i\) (a coefficient 2 is not octagonal). Production abstract interpreters (Astrée, IKOS, Frama-C EVA with Apron) use these domains; compilers mostly do not, because of their cost.

Widening and narrowing¶

Definition 14.7.9 (Widening, narrowing)

A widening on a poset \(A\) is \(\nabla : A \times A \to A\) with (1) \(x \sqsubseteq x \nabla y\) and \(y \sqsubseteq x \nabla y\), and (2) for every \(x_0\) and every ascending chain \(y_0 \sqsubseteq y_1 \sqsubseteq \cdots\) the sequence \(x_{k+1} = x_k \nabla y_k\) is eventually stationary. A narrowing is \(\Delta : A \times A \to A\) with (1) \(y \sqsubseteq x \Rightarrow y \sqsubseteq x \Delta y \sqsubseteq x\) and (2) for every \(x_0\) and every descending chain \(y_0 \sqsupseteq y_1 \sqsupseteq \cdots\) with \(y_0 \sqsubseteq x_0\), the sequence \(x_{k+1} = x_k \Delta y_k\) is eventually stationary. The standard interval widening and narrowing are

\[ \begin{aligned} [a, b] \nabla [c, d] &= [\,c < a \ ?\ -\infty : a,\ \ d > b \ ?\ +\infty : b\,], \qquad \bot \nabla y = y, \\ [a, b] \Delta [c, d] &= [\,a = -\infty \ ?\ c : a,\ \ b = +\infty \ ?\ d : b\,]. \end{aligned} \]

Theorem 14.7.10 (Termination and soundness of widening, then narrowing)

Let \(F^{\sharp}\) be monotone and sound (Theorem 14.7.4). The upward iteration \(x_0 = \bot\), \(x_{k+1} = x_k \nabla F^{\sharp}(x_k)\) stabilizes after finitely many steps at some \(x^{\nabla}\) with \(F^{\sharp}(x^{\nabla}) \sqsubseteq x^{\nabla}\). The downward iteration \(z_0 = x^{\nabla}\), \(z_{k+1} = z_k \Delta F^{\sharp}(z_k)\) stabilizes after finitely many steps, and every \(z_k\) satisfies \(\mathrm{lfp}(F^{\sharp}) \sqsubseteq z_k \sqsubseteq x^{\nabla}\). Hence \(\gamma(z_k)\) contains the collecting semantics: every result is sound. The standard interval operators satisfy Definition 14.7.9.

Proof

Upward: let \(y_k = F^{\sharp}(x_k)\). By (1), \(x_k \sqsubseteq x_k \nabla y_k = x_{k+1}\), so the \(x_k\) ascend, and by monotonicity so do the \(y_k\). Property (2) with this ascending chain says that \(x_{k+1} = x_k \nabla y_k\) is eventually stationary: \(x_{k+1} = x_k = x^{\nabla}\). Then \(F^{\sharp}(x^{\nabla}) = y_k \sqsubseteq x_k \nabla y_k = x^{\nabla}\) by (1). Downward: we show by induction that \(F^{\sharp}(z_k) \sqsubseteq z_k\) and \(\mathrm{lfp}(F^{\sharp}) \sqsubseteq z_k\). For \(k = 0\) this is the upward result and Theorem 14.1.12 (a pre-fixed point is above the least fixed point). If both hold for \(z_k\), narrowing's (1) with \(y = F^{\sharp}(z_k) \sqsubseteq z_k\) gives \(F^{\sharp}(z_k) \sqsubseteq z_{k+1} \sqsubseteq z_k\); hence \(F^{\sharp}(z_{k+1}) \sqsubseteq F^{\sharp}(z_k) \sqsubseteq z_{k+1}\) (monotonicity) and \(\mathrm{lfp}(F^{\sharp}) = F^{\sharp}(\mathrm{lfp}(F^{\sharp})) \sqsubseteq F^{\sharp}(z_k) \sqsubseteq z_{k+1}\). The chain \(F^{\sharp}(z_0) \sqsupseteq F^{\sharp}(z_1) \sqsupseteq \cdots\) descends and starts below \(z_0\), so (2) makes the \(z_k\) stationary. Soundness: each \(z_k\) (and \(x^{\nabla}\)) satisfies \(F^{\sharp}(a) \sqsubseteq a\), so Theorem 14.7.4 applies. Standard interval operators: widening (1): the new lower bound is \(a\) when \(c \ge a\) and \(-\infty\) otherwise, in both cases \(\le \min(a, c)\); symmetrically for upper bounds; \(\bot \nabla y = y\). Widening (2): after the first non-\(\bot\) value, each bound of \(x_k\) either stays or jumps to \(\pm\infty\), after which it never changes, so the sequence changes at most three times. Narrowing (1): if \([c, d] \subseteq [a, b]\), the result's lower bound is \(c\) (when \(a = -\infty\)) or \(a\), both in \([a, c]\); symmetrically above. Narrowing (2): only infinite bounds change, each at most once. \(\square\)

Algorithm 14.7.11 (Interval analysis of LLVM IR — exercise E6)

Input: an LLVM function in SSA form.
Output: for each tracked integer value (width 2–64), its interval at its definition.
Precondition: every transfer function is a sound abstraction (Definition 14.7.2) of the instruction's LLVM semantics, for executions without poison.
Postcondition: every value an execution without poison produces lies in its interval (Theorem 14.7.10 + Theorem 14.7.4); the iteration terminates.
Invariant: block-entry environments only grow during the ascending phase and only shrink during the descending phase; every loop head is a widening point.

function Intervals(F):
    order ← RPO of the CFG from the entry (successors in terminator order)
    heads ← { v : u → v is an edge with rpo(v) ≤ rpo(u) }          # targets of retreating edges
    IN[entry] ← (reachable, arguments ↦ full range, others ↦ ⊥);  IN[b] ← unreachable for b ≠ entry
    OUT[entry] ← Transfer(entry, IN[entry])
    Sweep(ascending);  Sweep(descending)
    return { x ↦ OUT[block(x)][x] }                               # phis: IN = OUT for phis

function Sweep(phase):
    visits[b] ← 0 for all b
    repeat
        changed ← false
        for b in order, b ≠ entry:
            X ← ⊔ { Edge(p, b, OUT[p]) : p ∈ preds(b) }           # environment join
            if b ∈ heads:
                visits[b] ← visits[b] + 1
                for each tracked value v:
                    if v is a phi of b or visits[b] > 8:
                        X[v] ← (IN[b][v] ∇ X[v]) if phase = ascending else (IN[b][v] Δ X[v])
            if X ≠ IN[b]: IN[b] ← X;  OUT[b] ← Transfer(b, X);  changed ← true
    until not changed

function Edge(p, b, env):                                          # refinement + phis
    if env is unreachable: return unreachable
    if p ends in `br i1 %c, ...` with two different successors:
        if %c is a constant: the other edge is infeasible → return unreachable
        if %c = icmp pred %x, %y on integers: refine env[%x], env[%y] by pred (on the edge to
            the first successor) or by its inverse; if either becomes ⊥ → return unreachable
    for each phi v of b: env[v] ← value of v's operand for p in env (constant ↦ [c, c])
    return env

function Transfer(b, env):                                         # non-phi instructions in order
    for I in b: if I is tracked: env[I] ← Eval(I, env)            # the rules of exercises.md, E6-R2
    return env

3. Worked example¶

count10 from tests/ch14/Inputs/c/loops.c in SSA form: %i.0 = phi(0 from entry, %add from while.body) at the head while.cond, %cmp = icmp slt %i.0, 10, body %add = add nsw %i.0, 1.

flowchart TD
  entry([entry]) --> head["while.cond: %i.0 = phi(0, %add)<br/>%cmp = %i.0 < 10"]
  head --> body["while.body: %add = %i.0 + 1"]
  head --> exit["while.end: ret %i.0"]
  body --> head

Galois connections on the worked example¶

The collecting semantics at the head is \(\{0, 1, \dots, 10\}\), and \(\alpha\) of it in the four domains of Definition 14.7.5 is: signs \(\top\) (0 and positive), constants \(\top\), intervals \([0, 10]\), congruences \(1\mathbb{Z} + 0 = \top\). The best abstraction of the body i + 1 in intervals maps \([a, b]\) to \([a+1, b+1]\); of the test i < 10 on the edge into the body, to \([a, \min(b, 9)]\).

Non-relational domains on the worked example¶

Plain Kleene iteration in intervals at the head, \(H_{k+1} = [0,0] \sqcup ((H_k \sqcap [-\infty, 9]) + 1)\):

\(k\)	0	1	2	3	…	11	12
\(H_k\)	\(\bot\)	\([0,0]\)	\([0,1]\)	\([0,2]\)	…	\([0,10]\)	\([0,10]\) (stable)

12 applications of the equation (./course drill widening --difficulty hard computes this count as kleene). With i < 1000000000 it would be a billion.

Relational domains on the worked example¶

Add j = 0 before and j = j + 1 in the body. Intervals at the head after widening: \(i \in [0, +\infty]\), \(j \in [0, +\infty]\); narrowing restores \(i \le 10\) through the test but has no test on \(j\), so \(j \in [0, +\infty]\) at the exit. The octagon domain keeps \(i - j \le 0\) and \(j - i \le 0\) (both variables start at 0 and grow by 1 together): at the head \(\{0 \le i, i - j = 0\}\) after widening; the test \(i \le 9\) on the body edge closes (Algorithm 14.7.7) to \(j \le 9\); after narrowing the head is \(\{0 \le i \le 10, i - j = 0\}\) and the exit \(\{i = 10, j = 10\}\) — the relational domain proves \(j = 10\), intervals cannot.

Widening and narrowing on the worked example¶

Upward iteration \(H_{k+1} = H_k \nabla F(H_k)\), \(F(H) = [0,0] \sqcup ((H \sqcap [-\infty, 9]) + 1)\):

\(k\)	\(H_k\)	\(H_k \sqcap\) cond	\(F(H_k)\)	\(H_{k+1} = H_k \nabla F(H_k)\)
0	\(\bot\)	\(\bot\)	\([0, 0]\)	\([0, 0]\)
1	\([0, 0]\)	\([0, 0]\)	\([0, 1]\)	\([0, +\infty]\) (upper bound grew)
2	\([0, +\infty]\)	\([0, 9]\)	\([0, 10]\)	\([0, +\infty]\) (stable)

Downward iteration \(H \gets H \Delta F(H)\):

step	\(H\)	\(F(H)\)	\(H \Delta F(H)\)
1	\([0, +\infty]\)	\([0, 10]\)	\([0, 10]\)
2	\([0, 10]\)	\([0, 10]\)	\([0, 10]\) (stable)

Exit: \(H \sqcap [10, +\infty] = [10, 10]\). The E6 solution prints exactly this (tests/ch14/lit/intervals.test):

Pebble intervals for function 'count10'
  %while.cond:
    %i.0 = [0, 10]
  %while.body:
    %add = [1, 10]

and nested (two nested loops) gets %i.0 = [0, 8], %j.0 = [0, 7] because Algorithm 14.7.11 widens only the phis of each head: widening the whole environment at the inner head would also widen the outer counter there, and narrowing could not recover it (a classic pitfall, §4).

Try it

./course drill widening --seed 4 --difficulty medium gives a counting loop and asks for the widening iterates, the narrowing iterates and the exit interval; --difficulty hard adds widening with thresholds and the Kleene iteration count.

4. Invariants and correctness¶

Galois connections¶

Lemma 14.7.3 and Theorem 14.7.4: soundness of a whole analysis reduces to soundness of each transfer function. When it breaks: an abstract operation that ignores machine arithmetic is unsound: \([0, +\infty] + 1 = [1, +\infty]\) is wrong for a wrapping add i32 (the maximum wraps to the minimum). E6 therefore returns the full range for any add that may overflow without nsw, and uses the nsw flag (overflow is poison) to clip otherwise; the tests stop a concrete run at the first poison, matching the precondition of Algorithm 14.7.11.

Non-relational domains¶

Each operation of Definition 14.7.5 is checked against \(\alpha \circ f \circ \gamma\). The course test ch14.Intervals.RandomFunctionsAreSoundOnConcreteRuns executes 150 random functions on 40 inputs each and checks every produced value against its interval; intervals-sound.c does the same with lli on C programs, and its <shrink> variant proves that the checks run (it must fail).

Relational domains¶

Theorem 14.7.8. When it breaks: joining unclosed DBMs loses precision (the join of two octagons is exact only on their closures), and applying widening to closed DBMs can break termination (Miné's widening is applied to the unclosed left argument [Min06]).

Widening and narrowing¶

Theorem 14.7.10. When it breaks: (1) widening at a point that is not on every cycle can loop forever — widening points must cut every cycle (loop heads; for irreducible CFGs every retreating-edge target, which is why Algorithm 14.7.11 uses retreating edges, not natural-loop headers); (2) widening only the phis at a head, as E6 does for precision, would not cut cycles of non-phi values in irreducible CFGs — hence the fallback that widens every component after 8 visits; (3) narrowing is not monotone, so the downward iteration must start from a post-fixed point.

5. Complexity¶

Let \(v\) = variables, \(n\) = blocks, \(e\) = edges, \(h\) = height of the domain per variable (or the number of widening jumps per variable when infinite).

Technique	Time (worst)	Time (typical)	Space	Variables
Galois connections	— (a proof method)	—	—	—
Signs / constants	\(O(1)\) per operation; \(O(e \cdot v)\) per pass, \(\le 2\) rises per variable	2–3 passes	\(O(n v)\)	\(n, e, v\)
Intervals (with widening)	\(O(1)\) per operation; \(O(e v)\) per pass; \(\le 2\) widening jumps per bound	3–6 passes	\(O(n v)\)	\(n, e, v\)
Congruences	\(O(\log M)\) (gcd) per operation	—	\(O(n v)\)	\(M\) = largest modulus
Octagons	\(O(v^3)\) closure; \(O(v^2)\) join, widening	cubic in variables per block	\(O(n v^2)\)	\(v\)
Polyhedra	exponential in \(v\) (double description; hull of \(m\) constraints can have exponentially many vertices)	quadratic–cubic on small \(v\)	exponential	\(v\)
Widening / narrowing	turns infinite ascending chains into \(\le 2\) jumps per bound	—	—	—

Proposition 14.7.12 (Cost of E6)

Let \(H\) be the number of loop heads. Each phase of Algorithm 14.7.11 makes at most \(H \cdot (8 + 4v) + 2\) sweeps; a sweep costs \(O((n + e) \cdot v + s)\) interval operations (\(s\) = instructions).

Proof

Blocks are swept in RPO, and every retreating edge ends at a head, so in a sweep where no head's IN changes, every other block is computed from final values; the next sweep then changes nothing. Hence the number of sweeps is at most (sweeps that change some head's IN) + 2. A head's IN changes at most 8 times before its fallback, and afterwards every component is widened (narrowed): each of the \(2v\) bounds can change at most twice (finite, then \(\pm\infty\); narrowing: once), i.e. \(4v\) more changes. A sweep visits every block once, joining \(v\) components per incoming edge and evaluating each instruction once. \(\square\)

Pathological input. Polyhedra: the hull of the \(2^{d}\) vertices of a \(d\)-dimensional hypercube, given as \(2d\) constraints, stays small, but the dual case — the cross-polytope with \(2d\) vertices — needs \(2^{d}\) constraints: converting between representations is exponential. Octagons on 100 variables: a \(200 \times 200\) DBM, \(n (2n)^2 = 4 \cdot 10^{6}\) entry updates per closure per block.

At scale: octagons were designed for, and are used in, Astrée's analysis of large avionics programs, where polyhedra were too costly [Min06, BCC+03].

Galois connections¶

Abstraction without \(\alpha\) (concretization-only frameworks) [CC92]: when no best abstraction exists (polyhedra have no \(\alpha\) for circles) use only \(\gamma\) and soundness — trade-off: loses "best transformer" reasoning.
Reduced product [CC79]: combine domains and refine each by the others (intervals × congruences) — trade-off: more precise, more expensive reduction.

Non-relational domains¶

Interval sets / range sets (Clang static analyzer, GCC Ranger's multi-range irange): unions of intervals — trade-off: express \(x \ne 0\) exactly, bounded number of ranges.
Known bits and demanded bits (LLVM KnownBits, DemandedBits): bit-level domains — trade-off: cheap, precise for masks and alignment, blind to magnitudes.

Relational domains¶

Zones / difference-bound matrices (\(x - y \le c\)): octagons without sums — trade-off: \(O(v^3)\) too, less expressive.
Weakly relational variable packing (Astrée): octagons on small packs of related variables — trade-off: linear in program size, needs a packing heuristic.

Widening and narrowing¶

Widening with thresholds [BCC+03]: jump to the next constant of the program instead of \(\pm\infty\) — trade-off: more precise (loop bounds survive widening), more steps (./course drill widening --difficulty hard).
Delayed widening / widening points from a weak topological order [Bou93]: join a few times before widening, widen only at the heads of Bourdoncle's components — trade-off: precision for small loops versus iterations. E6's "widen phis only, everything after 8 visits" is a simple form.
LLVM SCCP's range widening: after MaxNumRangeExtensions (10) extensions a range becomes overdefined — trade-off: termination without a descending phase, precision lost on long-running loops.

7. In real compilers¶

Galois connections¶

Clang

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp keeps each symbol's abstract value as a set of ranges; ExprEngine runs the transfer functions path by path (LLVM 23.1.2) [CLANG-SA].

MLIR mlir/include/mlir/Analysis/DataFlow/IntegerRangeAnalysis.h — IntegerRangeAnalysis, a sparse abstract interpretation in the interval domain (LLVM 23.1.2) [MLIR-DF].

Non-relational domains¶

LLVM

llvm/include/llvm/IR/ConstantRange.h (intervals with wrapping), llvm/lib/Analysis/LazyValueInfo.cpp (on-demand intervals per block, LazyValueInfoImpl::solveBlockValue), llvm/include/llvm/Support/KnownBits.h (bit-level congruences) (LLVM 23.1.2) [LLVM-CR, LLVM-LVI, LLVM-KB].

GCC gcc/gimple-range.cc — gimple_ranger::range_of_stmt, the on-demand range engine (Ranger) behind VRP (GCC 15) [GCC-RANGER].

Find where LLVM does it. Open llvm/include/llvm/IR/ConstantRange.h. Question: which method returns the sound result range of an add that has the nsw flag, and what extra argument does it take? (Quiz llvm-where-add-nowrap.)

Relational domains¶

LLVM

LLVM has no octagon or polyhedral value analysis in its default pipeline; Polly (polly/lib/) uses isl sets and maps — the polyhedral domain — to model loop nests for scheduling, not for invariants.

Research and industrial analyzers: Astrée (octagons, [BCC+03]), IKOS (NASA) and Frama-C EVA with the Apron library. Not runnable in the course container except through isl (the box above).

Widening and narrowing¶

LLVM

llvm/include/llvm/Analysis/ValueLattice.h — ValueLatticeElement::MergeOptions::setMaxWidenSteps and the comment "Simple form of widening. If a range is extended multiple times, go to overdefined"; llvm/lib/Transforms/Utils/SCCPSolver.cpp — MaxNumRangeExtensions = 10 (LLVM 23.1.2) [LLVM-VL, LLVM-SCCP].

Loop widening in Clang's static analyzer

Reproduce (clang 23.1.2):

cat > wl.c <<'EOF'
void clang_analyzer_value(int);
void clang_analyzer_warnIfReached(void);
int f(void) {
  int i = 0;
  while (i < 1000)
    i = i + 1;
  clang_analyzer_warnIfReached();
  clang_analyzer_value(i);
  return i;
}
EOF
echo "--- default"
clang-23 --analyze -Xclang -analyzer-checker=debug.ExprInspection wl.c 2>&1 | grep 'warning:'
echo "--- widen-loops"
clang-23 --analyze -Xclang -analyzer-checker=debug.ExprInspection \
  -Xclang -analyzer-config -Xclang widen-loops=true wl.c 2>&1 | grep 'warning:'

Output:

--- default
--- widen-loops
wl.c:7:3: warning: REACHABLE [debug.ExprInspection]
wl.c:8:3: warning: 32s:{ [1000, 2147483647] } [debug.ExprInspection]

What to notice: the path-sensitive analyzer unrolls loops a bounded number of times (4 by default) and then gives up on the path: without widening the code after the loop is never analyzed (no REACHABLE). With widen-loops=true it widens the loop state (getWidenedLoopState, clang/lib/StaticAnalyzer/Core/LoopWidening.cpp) [CLANG-SA]: the values modified in the loop become unknown, the exit test i >= 1000 refines them, and the result \([1000, 2^{31}-1]\) is the upward iteration of Theorem 14.7.10 without narrowing — sound, with the upper bound lost.

8. Comparison¶

Technique	Power / precision	Speed	Output / error quality	Implementation effort	Typical use
Galois connections	Defines the best transformer; soundness by construction	—	Proof obligations per operation	Conceptual	Designing and proving analyses
Non-relational domains (signs, constants, intervals, congruences)	One property per variable; no correlations	\(O(1)\) per operation	Ranges, constants, parities per value	Low	Compilers: LVI, ConstantRange, KnownBits, Ranger, E6
Relational domains (octagons, polyhedra)	Linear relations (\(\pm x \pm y \le c\); any linear)	Octagons \(O(v^3)\); polyhedra exponential	Invariants such as \(i = j\), \(j = 2i\)	High (DBMs, double description)	Verifiers (Astrée, IKOS, EVA); polyhedral loop optimization (Polly)
Widening and narrowing	Sound post-fixed point; narrowing recovers bounds	\(\le 2\) jumps per bound	Loss of bounds that only a later test restores	Low	Every analysis over an infinite-height domain

Choose a non-relational domain in a compiler: cost is linear and most optimizations need per-value facts. Choose octagons when correlations between a few variables decide the property (array bounds with two indices). Choose polyhedra when you need exact linear invariants on small loop nests. Use widening with narrowing whenever the domain has infinite ascending chains; add thresholds when loop bounds are constants.

Lab numbers: tests/ch14/lit/intervals-sound.c instruments every tracked value of seven functions and runs about 430 calls of them under lli without a violation; its <shrink> variant is caught.

9. Assessment¶

Technique	Quiz ids	Drill	Flashcard tag	Exercises
Galois connections	`galois-best-transformer`, `interval-mul`	`./course drill widening`	`galois`	E6
Non-relational domains	`congruence-join`, `interval-add-wrap`, `llvm-where-add-nowrap`	`./course drill widening`	`domains`	E6
Relational domains	`octagon-vs-interval`, `polyhedra-cost`	— (theory; the worked example and quiz)	`relational`	—
Widening and narrowing	`widening-iterates`, `narrowing-exit`	`./course drill widening`	`widening`	E6

Relational domains have no drill: their computations (DBM closure over \(2v \times 2v\) matrices) are too large to be pleasant by hand; the quiz asks for the octagon of a two-variable loop instead.

Pitfall

Widening is not "set everything to \(\top\)". The standard widening keeps every stable bound; only bounds that grew are extrapolated. And widening the whole environment at an inner loop head also widens variables that belong to the outer loop — E6 widens only the head's own phis for exactly that reason.

References¶

See the chapter references.

Lesson 14.7 — Abstract interpretation: Galois connections, domains, widening¶

1. Problem and motivation¶

Galois connections¶

Non-relational domains¶

Relational domains¶

Widening and narrowing¶

2. Definitions and algorithms¶

Galois connections¶

Non-relational domains¶

Relational domains¶

Widening and narrowing¶

3. Worked example¶

Galois connections on the worked example¶

Non-relational domains on the worked example¶

Relational domains on the worked example¶

Widening and narrowing on the worked example¶

4. Invariants and correctness¶

Galois connections¶

Non-relational domains¶

Relational domains¶

Widening and narrowing¶

5. Complexity¶

6. Variants and refinements¶

Galois connections¶

Non-relational domains¶

Relational domains¶

Widening and narrowing¶

7. In real compilers¶

Galois connections¶

Non-relational domains¶

Relational domains¶

Widening and narrowing¶

8. Comparison¶

9. Assessment¶

References¶