Lesson 18.9 — Bounds-check elimination: ranges, ABCD, IRCE and loop predication

Techniques: range-based bounds-check elimination, ABCD (array bounds checks on demand), inductive range-check elimination (IRCE) and loop predication · Pebble implements: ★ pebble-bce (E5) · Lab: — (E5's tests compare the program before and after with lli, including a check that must stay) · Prerequisites: Lesson 18.3 (add recurrences, no-wrap flags), Lesson 18.5 (versioning, peeling), Ch 16 (SSA) · Time: 4–5 hours

A safe language checks every array access: xs[i] in Pebble, Go, Rust, Java or Swift means "if \(i \ge \mathit{len}\), trap (or panic, or throw); otherwise load". In a loop for i in 0..n { s += xs[i] } that is one compare and one branch per iteration, and — worse — a branch to a trap that blocks vectorization and other loop optimizations. Bounds-check elimination (BCE) removes the checks that can never fail and moves the others out of the loop, without changing which programs trap and where. Pebble's assert c, bounds, lowered by pebblec --emit=llvm to a branch to a pebble_trap(3, …) block, produces exactly such checks; E5 removes them.

1. Problem and motivation

The problem. Given a program with checks if !(0 <= e < len) trap, remove every check that provably never fails, and, for checks inside loops that cannot be removed, reduce their cost — without changing the observable behavior: a program that trapped must still trap, with the same side effects before the trap (or, in a managed runtime, with the same state visible to the exception handler).

Range-based bounds-check elimination

The oldest approach computes, for each index expression, a range of values that holds at the check, and compares it with the array length: flow analyses over ranges [Gup93], the induction-variable view of Kolte and Wolfe [KW95], and range propagation in JIT compilers such as HotSpot's client compiler [WWM07]. In LLVM, ScalarEvolution's add recurrences with no-wrap flags (Lesson 18.3) combined with the loop guard give the range of an induction variable directly; indvars, correlated-propagation and constraint-elimination then fold the checks [LLVM-IndVars; LLVM-CE]. Pebble's pebble-bce (E5) is this technique on top of SCEV.

ABCD

Bodík, Gupta and Sarkar observed that most checks are proved by short chains of inequalities between program variables — "\(i < n\) from the loop test, \(n \le \mathit{len}\) from a dominating comparison" — and designed ABCD (Array Bounds Checks on Demand): an inequality graph over an extended SSA form (e-SSA, with π-nodes that rename a variable after a branch) and a demand-driven shortest-path search per check [BGS00]. Go's prove pass keeps the same kind of facts — a partial order over SSA values with their limits — and proves bounds checks with it [Go-Prove].

IRCE and loop predication

When a check cannot be removed because the loop bound and the array length are unrelated (for i < n: xs[i] with \(n\) unknown), the check can still be taken out of the hot loop. IRCE splits the iteration space into a middle part where the check is provably true and pre/post loops that keep it [LLVM-IRCE]. Loop predication replaces a check on each iteration by one check of the whole range before the loop, which is legal only when failing early is acceptable — in LLVM, for guards whose failure deoptimizes to an interpreter that re-executes precisely (LLVM's guard intrinsics and these two passes serve JIT compilers for managed languages, which can deoptimize) [LLVM-LoopPredication].

2. Definitions and algorithms

Range-based bounds-check elimination

Definition 18.9.1 (Bounds check; redundant check)

A bounds check is a conditional branch on icmp ult e, len (unsigned: it also rejects negative \(e\) in two's complement) whose false successor traps. It is redundant at its program point \(p\) if \(0 \le e < \mathit{len}\) holds (as signed integers, \(\mathit{len} \ge 0\)) in every execution that reaches \(p\). A value range for \(e\) at \(p\) is an interval \([\ell, h]\) with \(\ell \le e \le h\) on every execution reaching \(p\).

Theorem 18.9.2 (Range of an affine index in a guarded loop)

Let \(i\) be an induction variable with add recurrence \(\{a, +, s\}\) in loop \(L\), with \(s \ge 1\) and the no-signed-wrap flag (Lesson 18.3), and let every path from the header to the check pass the test \(i < n\) (signed) of the current iteration. Then at the check, \(a \le i \le n - 1\), and the index \(e = i + c\) lies in \([a + c,\ n - 1 + c]\). Consequently the check \(0 \le e < \mathit{len}\) is redundant if \(a + c \ge 0\) and \(n + c \le \mathit{len}\) (the latter as a fact that holds at the check: constant values, or a dominating comparison).

Proof

By induction on the iteration number \(k \ge 0\): the value of \(i\) in iteration \(k\) is \(a + ks\) (the CR evaluated at \(k\), Lemma 18.3.2), and the no-signed-wrap flag guarantees that the sequence is the mathematical one, strictly increasing since \(s \ge 1\); so \(i \ge a\) in every iteration. The check is reached only after \(i < n\) was tested true in the same iteration and \(i\) has not changed since (it is an SSA value), so \(i \le n - 1\) there. Adding \(c\) (without overflow, since \(e\) stays between \(a + c\) and \(n - 1 + c\), both representable when \(a + c \ge 0\) and \(n + c \le \mathit{len}\)) gives the interval; with \(a + c \ge 0\) and \(n - 1 + c < \mathit{len}\) both bounds of the check hold.

Algorithm 18.9.3 (Range-based bounds-check elimination — pebble-bce)

• Input: a function with bounds checks (Definition 18.9.1), ScalarEvolution.
• Output: the function with the redundant checks replaced by unconditional branches and unreachable trap blocks deleted.
• Precondition: loops in loop-simplify form (so SCEV can form add recurrences); the checks in the unsigned form idx <u len.
• Postcondition: only checks that can never fail are removed (Theorem 18.9.10).
• Invariant: the set of removed checks only grows; SCEV facts are not invalidated because branches are replaced only after all queries.

function BCE(F):
    redundant ← []
    for each conditional branch br on (idx <u len) whose false successor is a trap block:
        if SCEV.isKnownPredicateAt(idx <u len, br):     # uses the CR of idx, its no-wrap
            redundant += br                              # flags, and dominating conditions
    for br in redundant:                                 # (Theorem 18.9.2 for affine idx)
        replace br by "br ok"; remove br's block from the trap block's predecessors
        if the trap block has no predecessors: delete it

Go's prove pass: which bounds checks remain

Reproduce (go 1.24.7):

cat > bce.go <<'X'
package bce

func sum(xs []int) int {
    s := 0
    for i := 0; i < len(xs); i++ {
        s += xs[i] // proved: 0 <= i < len(xs)
    }
    return s
}

func sumN(xs []int, n int) int {
    s := 0
    for i := 0; i < n; i++ {
        s += xs[i] // n unrelated to len(xs): check stays
    }
    return s
}

func pairs(xs []int) int {
    s := 0
    for i := 1; i < len(xs); i++ {
        s += xs[i] - xs[i-1] // both proved
    }
    return s
}

func hint(xs []int) int {
    _ = xs[3] // one check here ...
    return xs[0] + xs[1] + xs[2] + xs[3] // ... makes these four redundant
}
X
printf 'module bce\ngo 1.21\n' > go.mod
echo "== checks that remain"
go build -a -gcflags='-d=ssa/check_bce/debug=1' . 2>&1 | grep -v '^#'
echo "== what prove proved"
go build -a -gcflags='-d=ssa/prove/debug=1' . 2>&1 | grep -v '^#'

Output (complete):

== checks that remain
./bce.go:14:10: Found IsInBounds
./bce.go:28:8: Found IsInBounds
== what prove proved
./bce.go:5:21: Induction variable: limits [0,?), increment 1
./bce.go:6:10: Proved IsInBounds
./bce.go:13:16: Induction variable: limits [0,?), increment 1
./bce.go:21:21: Induction variable: limits [1,?), increment 1
./bce.go:22:10: Proved IsInBounds
./bce.go:22:21: Proved IsInBounds
./bce.go:29:12: Proved IsInBounds
./bce.go:29:20: Proved IsInBounds
./bce.go:29:28: Proved IsInBounds
./bce.go:29:36: Proved IsInBounds

What to notice: of seven indexing operations, two checks remain: xs[i] in sumN (line 14: nothing relates n to len(xs)) and the explicit xs[3] in hint (line 28: nothing is known about len(xs) — but once it passed, len(xs) > 3, so the four accesses on line 29 are proved). The loops show Theorem 18.9.2's two ingredients: the induction variable's range (limits [0,?), increment 1 — lower bound from the start value) and the loop test i < len(xs) for the upper bound. In pairs also xs[i-1] is proved: \(i \ge 1\) from the start value, and \(i - 1 < i < \mathit{len}\) — a chain of two inequalities, the kind of proof ABCD searches for.

LLVM: which pass removes which check

Reproduce (clang 23.1.2, opt 23.1.2):

cat > ce.c <<'X'
#include <stdlib.h>
#define AT(a, len, i) ((unsigned long)(i) < (unsigned long)(len) ? (a)[i] : (abort(), 0))
long sum(const long *a, long len) {              /* the IV is in range: indvars */
  long s = 0;
  for (long i = 0; i < len; i++) s += AT(a, len, i);
  return s;
}
long sum_n(const long *a, long len, long n) {    /* n unrelated to len: kept */
  long s = 0;
  for (long i = 0; i < n; i++) s += AT(a, len, i);
  return s;
}
long window(const long *a, unsigned long len, unsigned long i) {
  if (len >= 3 && i < len - 2)                   /* facts: len >= 3, i < len - 2 */
    return AT(a, len, i) + AT(a, len, i + 1) + AT(a, len, i + 2);
  return 0;
}
long wrap(const long *a, unsigned long len, unsigned long i) {
  if (i + 2 < len)                               /* i + 2 may wrap around to 0 */
    return AT(a, len, i);
  return 0;
}
X
clang-23 -O0 -Xclang -disable-O0-optnone -fno-discard-value-names -S -emit-llvm ce.c -o - |
  opt -passes='mem2reg,instcombine,simplifycfg,loop-simplify,lcssa,loop(loop-rotate)' -S -o ce.ll
count() { for f in sum sum_n window wrap; do
  printf ' %s=%s' $f $(sed -n "/^define.*@$f(/,/^}/p" $1 | grep -c 'call void @abort'); done; echo; }
printf '%-46s' 'checks before:'; count ce.ll
for p in 'loop(indvars)' constraint-elimination correlated-propagation \
         'correlated-propagation,constraint-elimination' 'default<O2>'; do
  opt -passes="$p,simplifycfg" -S ce.ll -o t.ll; printf '%-46s' "$p:"; count t.ll
done

Output (complete):

checks before:                                 sum=1 sum_n=1 window=3 wrap=1
loop(indvars):                                 sum=0 sum_n=1 window=3 wrap=1
constraint-elimination:                        sum=1 sum_n=1 window=2 wrap=1
correlated-propagation:                        sum=1 sum_n=1 window=3 wrap=1
correlated-propagation,constraint-elimination: sum=1 sum_n=1 window=0 wrap=1
default<O2>:                                   sum=0 sum_n=1 window=0 wrap=1

What to notice: indvars removes the loop check in sum — Theorem 18.9.2 with SCEV's {0,+,1}<nuw><nsw> and the guard i < len. constraint-elimination alone removes only the first check of window: from i <u len - 2 it can derive i <u len, but the adds i + 1, i + 2 carry no nuw flag, so it must assume they wrap. correlated-propagation computes the range of i from the dominating condition and adds nuw to those adds; then constraint-elimination proves all three. -O2 runs both. The check in wrap stays under every pipeline, correctly: for i \(= 2^{64} - 1\), i + 2 wraps to 1, which may be < len while i is not — the unsigned-overflow pitfall of every range-based argument. sum_n keeps its check (next technique).

ABCD

Definition 18.9.4 (e-SSA; inequality graph)

e-SSA is SSA form extended with π-nodes: after a branch on \(x < y\), each successor gets fresh names \(x_1 = \pi(x)\), \(y_1 = \pi(y)\), so that the fact holding on that edge can be attached to the new names. The inequality graph \(G\) for upper bounds has a vertex per SSA name and per integer constant, and a weighted edge \(u \xrightarrow{c} v\) for each fact \(v \le u + c\): v = u + c gives \(u \xrightarrow{c} v\); a π-node \(x_1 = \pi(x)\) on the true edge of \(x < y\) gives \(x \xrightarrow{0} x_1\) and \(y \xrightarrow{-1} x_1\); a φ-node \(v = \varphi(u_1, \dots, u_k)\) gives \(u_j \xrightarrow{0} v\) for each \(j\) and is marked as a max-vertex (it is bounded by the maximum of its inputs, so a bound must hold for all of them). A lower-bound graph is built symmetrically.

Algorithm 18.9.5 (ABCD: demand-driven proof of an upper-bound check)

• Input: the inequality graph \(G\); a check \(x < \mathit{len}\), i.e. the query "\(x - \mathit{len} \le -1\)".
• Output: "proved" or "unknown".
• Precondition: \(G\) built from e-SSA facts that hold wherever the named values are defined.
• Postcondition: "proved" only if \(x \le \mathit{len} - 1\) holds at the check (Theorem 18.9.11).
• Invariant: active holds the φ-vertices on the current search path with the bound they were entered with.

function Prove(a, v, c):                            # is v − a ≤ c ?  (v ≤ a + c)
    if v = a: return c ≥ 0
    if v is a φ (max-vertex) on the active path:
        c0 ← the bound v was entered with
        return c ≥ c0 ? "reduced (harmless cycle)" : "false (amplifying cycle)"
    if memo has (v, c'): answer from the memo if it decides c
    if v has no incoming edges: return false
    if v is a max-vertex:                           # all inputs must satisfy the bound
        push (v, c) on active; r ← AND over edges u →w v of Prove(a, u, c − w); pop
    else:                                           # any one fact suffices
        r ← OR over edges u →w v of Prove(a, u, c − w)
    memoize (v, c, r); return r

check x < len is redundant iff Prove(len, x, -1) is true (and the lower bound symmetrically)

Lemma 18.9.6 (Paths are inequalities)

If \(G\) has a path \(a = w_0 \xrightarrow{c_1} w_1 \xrightarrow{c_2} \dots \xrightarrow{c_k} w_k = v\) through non-φ vertices, then \(v \le a + \sum_j c_j\) at every point where the values on the path are all defined along one execution.

Proof

Each edge is a fact \(w_j \le w_{j-1} + c_j\) that holds wherever \(w_j\) is defined (by construction: assignments define it, π-nodes are placed where the branch condition holds). Chaining the inequalities gives \(v \le a + \sum c_j\) by transitivity of \(\le\).

LLVM's constraint elimination chains two dominating facts

Reproduce (opt 23.1.2):

cat > chain.ll <<'X'
define i1 @chain(i64 %i, i64 %n, i64 %len) {
entry:
  %c1 = icmp ult i64 %i, %n
  br i1 %c1, label %l1, label %out
l1:
  %c2 = icmp ule i64 %n, %len
  br i1 %c2, label %l2, label %out
l2:
  %check = icmp ult i64 %i, %len        ; the bounds check: implied by i < n <= len
  ret i1 %check
out:
  ret i1 false
}
X
opt -passes=constraint-elimination -S chain.ll | sed -n '/^l2:/,/ret/p'

Output (complete):

l2:                                               ; preds = %l1
  ret i1 true

What to notice: the check i <u len is proved from two dominating facts, \(i < n\) and \(n \le \mathit{len}\) — in ABCD's graph, the path \(\mathit{len} \xrightarrow{0} n_1 \xrightarrow{-1} i_1\) of weight \(-1\) (Lemma 18.9.6). LLVM's ConstraintElimination collects the facts of dominating conditions in a system of linear inequalities per dominator-tree scope and decides implication by Fourier–Motzkin elimination rather than by shortest paths [LLVM-CE]; for chains of difference constraints like this one both methods agree.

IRCE and loop predication

Definition 18.9.7 (Inductive range check; safe iteration space; guard)

A check \(0 \le a\,i + b < \mathit{len}\) in a loop with induction variable \(i = \{i_0, +, 1\}\) and exit test \(i < n\), with \(a, b, \mathit{len}\) loop-invariant, is an inductive range check. Its safe iteration space is the set of \(i\) where it holds, an interval \([\lceil -b/a \rceil, \lceil (\mathit{len} - b)/a \rceil)\) for \(a > 0\). A guard guard(c) [deopt state] (LLVM llvm.experimental.guard, or a widenable branch) continues if \(c\) holds and otherwise transfers control to the runtime's deoptimization handler with the recorded state, which resumes execution in an interpreter at that program point.

Algorithm 18.9.8 (Inductive range-check elimination — IRCE)

• Input: a loop with inductive range checks (Definition 18.9.7), a computable exit bound \(n\).
• Output: up to three loops: a pre-loop for \(i <\) start of the safe space, the main loop without the checks, a post-loop for the rest.
• Precondition: the IV does not wrap; the check's operands are invariant; profitability (the check's branch is likely to pass).
• Postcondition: the three loops execute the same iterations in the same order as the original (Theorem 18.9.12).
• Invariant: every iteration of the main loop lies in the intersection of all checks' safe spaces.

function IRCE(L):
    [lo, hi) ← intersection of the safe iteration spaces of all inductive range checks
    pre   ← clone of L running i from i0 while i < min(n, lo)     # checks kept
    main  ← L running from max(i0, lo) while i < min(n, hi)       # checks replaced by true
    post  ← clone of L running from there while i < n             # checks kept
    connect pre → main → post, each passing the IV and live values to the next

Algorithm 18.9.9 (Loop predication — widening a guard over the loop)

• Input: a loop with a guard on an inductive range check \(i < \mathit{len}\), IV \(\{0, +, 1\}\), latch test \(i + 1 < n\).
• Output: the guard's condition replaced by a loop-invariant one computed in the preheader.
• Precondition: the check is a guard (failing it may deoptimize at an earlier point); the latch condition gives the last value of \(i\).
• Postcondition: the widened guard fails iff some iteration's original guard would fail (Theorem 18.9.13).
• Invariant: the widened condition implies the original condition in every iteration.

function Predicate(L):
    for each guard(i <u len) in L with i = {start, +, 1} and latch "i.next < n":
        last ← n − 1                                  # the largest i the loop executes
        widened ← (start <u len) ∧ (last <u len)      # the check at both ends of the range
        compute widened in the preheader (freeze it: it must not be poison)
        guard(widened) replaces guard(i <u len); the old condition becomes an assume
    # a later unswitch/LICM can hoist the now-invariant guard out of the loop

LLVM's IRCE splits off the iterations that need the check

Reproduce (clang 23.1.2, opt 23.1.2):

cat > ce.c <<'X'
#include <stdlib.h>
#define AT(a, len, i) ((unsigned long)(i) < (unsigned long)(len) ? (a)[i] : (abort(), 0))
long sum_n(const long *a, long len, long n) {
  long s = 0;
  for (long i = 0; i < n; i++) s += AT(a, len, i);
  return s;
}
X
clang-23 -O0 -Xclang -disable-O0-optnone -fno-discard-value-names -S -emit-llvm ce.c -o - |
  opt -passes='mem2reg,instcombine,simplifycfg,loop-simplify,lcssa,loop(loop-rotate)' -S -o ce.ll
opt -passes='irce,simplifycfg,dce' -irce-print-range-checks -irce-print-changed-loops -S ce.ll -o irce.ll 2>&1
sed -n '/^define.*@sum_n(/,/^}/p' irce.ll | grep -E '^[a-z._0-9]+:|icmp|br i1|exit.mainloop.at =' |
  sed -E 's/ +;.*//; s/, !llvm.loop ![0-9]+//; s/, !loop_constrainer.loop.clone ![0-9]+//'

Output (complete):

irce: looking at loop Loop at depth 1 containing: %for.body<header><exiting>,%cond.true<latch><exiting>
irce: loop has 1 inductive range checks: 
InductiveRangeCheck:
  Begin: 0  Step: 1  End: %len
  CheckUse:   br i1 %cmp1, label %cond.true, label %cond.false Operand: 0
irce: in function sum_n: constrained Loop at depth 1 containing: %for.body<header><exiting>,%cond.true<latch><exiting>
entry:
  %cmp2 = icmp slt i64 0, %n
  br i1 %cmp2, label %for.body.lr.ph, label %for.end
for.body.lr.ph:
  %exit.mainloop.at = call i64 @llvm.smax.i64(i64 %smin2, i64 0)
  %4 = icmp slt i64 0, %exit.mainloop.at
  br i1 %4, label %for.body, label %postloop
for.body:
  %6 = icmp slt i64 %inc, %exit.mainloop.at
  br i1 %6, label %for.body, label %main.exit.selector
main.exit.selector:
  %7 = icmp slt i64 %inc.lcssa, %n
  br i1 %7, label %postloop, label %for.end
cond.false:
for.end:
postloop:
for.body.postloop:
  %cmp1.postloop = icmp ult i64 %i.04.postloop, %len
  br i1 %cmp1.postloop, label %cond.true.postloop, label %cond.false
cond.true.postloop:
  %cmp.postloop = icmp slt i64 %inc.postloop, %n
  br i1 %cmp.postloop, label %for.body.postloop, label %for.end

What to notice: IRCE found one inductive range check (begin 0, step 1, end %len: safe space \([0, \mathit{len})\)), computed %exit.mainloop.at \(= \max(\min(n, \mathit{len}'), 0)\) and built the main loop for.body, whose only branch is the latch — the check is gone — followed by main.exit.selector and a postloop that still checks %i.04.postloop <u %len and aborts on failure. No pre-loop is needed because the safe space starts at the IV's start, 0.

LLVM's loop predication widens a guard to the whole iteration range

Reproduce (opt 23.1.2):

cat > lp.ll <<'X'
declare void @llvm.experimental.guard(i1, ...)

; for (i = 0; i < n; i++) { guard(i < len) "deoptimize otherwise"; s += a[i]; }
define i32 @sum(ptr %a, i32 %len, i32 %n) {
entry:
  %tc.pos = icmp sgt i32 %n, 0
  br i1 %tc.pos, label %loop, label %exit

loop:
  %i = phi i32 [ 0, %entry ], [ %i.next, %loop ]
  %s = phi i32 [ 0, %entry ], [ %s.next, %loop ]
  %within.bounds = icmp ult i32 %i, %len
  call void (i1, ...) @llvm.experimental.guard(i1 %within.bounds) [ "deopt"() ]
  %i.64 = zext i32 %i to i64
  %p = getelementptr inbounds i32, ptr %a, i64 %i.64
  %x = load i32, ptr %p, align 4
  %s.next = add i32 %s, %x
  %i.next = add nuw i32 %i, 1
  %continue = icmp slt i32 %i.next, %n
  br i1 %continue, label %loop, label %exit

exit:
  %r = phi i32 [ 0, %entry ], [ %s.next, %loop ]
  ret i32 %r
}
X
opt -passes='loop-mssa(loop-predication)' -S lp.ll | sed -n '/^loop.preheader:/,/guard/p'

Output (complete):

loop.preheader:                                   ; preds = %entry
  %0 = icmp sle i32 %n, %len
  %1 = icmp ult i32 0, %len
  %2 = and i1 %1, %0
  %3 = freeze i1 %2
  br label %loop

loop:                                             ; preds = %loop.preheader, %loop
  %i = phi i32 [ %i.next, %loop ], [ 0, %loop.preheader ]
  %s = phi i32 [ %s.next, %loop ], [ 0, %loop.preheader ]
  %within.bounds = icmp ult i32 %i, %len
  call void (i1, ...) @llvm.experimental.guard(i1 %3) [ "deopt"() ]

What to notice: the guard inside the loop now tests %3, computed once in the preheader: \(0 <_u \mathit{len}\) (the check for the first iteration) and \(n \le \mathit{len}\) (for the last one, \(i = n - 1\): \(n - 1 < \mathit{len}\)) — Algorithm 18.9.9. The original condition survives only as an llvm.assume for later passes. The freeze makes the widened condition a definite boolean even if %n or %len were poison: a guard on poison would be undefined behavior, which the original loop (which might never have evaluated the check) did not have.

3. Worked example

Range-based bounds-check elimination on the running example

The four functions of tests/ch18/lit/bce.ll (written in Pebble, lowered to LLVM IR): xs: [i64; 4] has \(\mathit{len} = 4\).

function	loop and index	CR of index	range at the check (Theorem 18.9.2)	verdict
sum4	for i in 0..4: xs[i]	\(\{0,+,1\}\)	\([0, 3]\)	removed
next3	for i in 0..3: xs[i + 1]	\(\{1,+,1\}\)	\([0 + 1, 2 + 1] = [1, 3]\)	removed
sum5	for i in 0..5: xs[i]	\(\{0,+,1\}\)	\([0, 4]\); \(4 \not< 4\)	kept (and it does trap at \(i = 4\))
sumn	for i in 0..n: xs[i]	\(\{0,+,1\}\)	\([0, n - 1]\), \(n\) unknown	kept

sum5 shows why "kept" must not become "removed" by accident: the program's observable behavior is the trap pebble: trap: kind 3, which the lit test checks after pebble-bce too.

ABCD on the running example

Go's pairs in e-SSA: i = φ(1, i2), loop test i < len gives \(i_1 = \pi(i)\) with edges \(i \xrightarrow{0} i_1\) and \(\mathit{len} \xrightarrow{-1} i_1\); t = i1 - 1 gives \(i_1 \xrightarrow{-1} t\); i2 = i1 + 1 gives \(i_1 \xrightarrow{1} i_2\).

• Check xs[i1] (upper): \(\text{Prove}(\mathit{len}, i_1, -1)\): \(i_1\) is not a φ; edge \(\mathit{len} \xrightarrow{-1} i_1\) gives \(\text{Prove}(\mathit{len}, \mathit{len}, 0)\): true. Proved.
• Check xs[t] (upper): \(\text{Prove}(\mathit{len}, t, -1)\) → via \(i_1 \xrightarrow{-1} t\): \(\text{Prove}(\mathit{len}, i_1, 0)\) → via \(\mathit{len} \xrightarrow{-1} i_1\): \(\text{Prove}(\mathit{len}, \mathit{len}, 1)\): true. Proved (path weight \(-2 \le -1\)).
• Check xs[t] (lower, \(t \ge 0\)), in the lower-bound graph (edges for \(v \ge u + c\)): \(t \ge i_1 - 1\), \(i_1 \ge i\), and \(i = \varphi(1, i_2)\) is a max-vertex (a min-vertex for lower bounds: both inputs must be \(\ge 1\)): input 1 is the constant 1 — fine; input \(i_2 \ge i_1 + 1 \ge i + 1\) leads back to the φ with bound \(\ge 1 - 1 = 0\) required of \(i\)... entering \(i\) again with a weaker requirement: a harmless cycle (the IV only increases). Proved: \(i \ge 1\), \(t \ge 0\).

For sumN, the upper-bound query for xs[i1] needs a path from len(xs) to \(i_1\); the only facts about \(i_1\) are \(i_1 \le n - 1\) and \(i_1 \le i\), and nothing connects \(n\) to \(\mathit{len}\): no path, "unknown" — the check stays, as in the Go box.

IRCE and loop predication on the running example

sum_n with \(n = 10\), \(\mathit{len} = 6\). IRCE: safe space \([0, 6)\); exit.mainloop.at \(= \max(\min(10, 6), 0) = 6\). The main loop runs \(i = 0..5\) without checks; the post-loop runs \(i = 6\), whose check fails: abort() at iteration 6 — exactly where the original loop aborts, after the same six additions (\(i = 0..5\)). With \(n = 4\): main loop \(i = 0..3\), post-loop empty.

Loop predication for the guard version with \(n = 10\), \(\mathit{len} = 6\): widened condition \(0 <_u 6 \wedge 10 \le 6\) is false: the guard fails on entry to iteration 0 and deoptimizes. The interpreter then runs iterations \(0..5\) and fails the check at \(i = 6\) — the same observable behavior, only the switch to the interpreter happened earlier. With \(n = 4\) the widened condition is true: no check is ever evaluated again.

Try it

opt -load-pass-plugin=<build>/lib/PebblePasses.so -passes=pebble-bce -S tests/ch18/lit/bce.ll runs the reference (or your) E5 on the four functions above; change sum4's loop bound to 5 in the IR and check that the check reappears.

4. Invariants and correctness

Range-based bounds-check elimination

Theorem 18.9.10 (Range-based BCE preserves behavior)

Replacing a redundant bounds check (Definition 18.9.1) by an unconditional branch to its success successor preserves the behavior of every execution; Algorithm 18.9.3 removes only redundant checks.

Proof

On every execution reaching the check, the condition is true (redundancy), so the conditional branch goes to the success successor — exactly what the unconditional branch does; the trap block is not executed on any execution either way, so deleting it when it has no predecessors changes nothing. Algorithm 18.9.3 removes a check only when isKnownPredicateAt returns true, which SCEV answers only from facts valid at that point (the check's CRs with their no-wrap flags, and conditions of dominating branches); for affine indices this is Theorem 18.9.2. Removing one check does not invalidate the facts used for another, because all queries are made before any branch is replaced (the invariant), and a removed check's success edge was taken on all executions anyway.

ABCD

Theorem 18.9.11 (Soundness of ABCD)

If \(\text{Prove}(\mathit{len}, x, -1)\) returns true, then \(x \le \mathit{len} - 1\) at every execution of the check.

Proof

By induction on the (finite) recursion tree of the successful proof, with an inner induction on the number of times execution has passed a φ-vertex. An OR step used one edge \(u \xrightarrow{w} v\) with \(\text{Prove}(a, u, c - w)\) true: by induction \(u \le a + c - w\), and the edge fact gives \(v \le u + w \le a + c\) (Lemma 18.9.6). An AND step at a φ-vertex \(v = \varphi(u_1..u_k)\) proved \(u_j \le a + c\) for every input, so whichever input the execution took, \(v \le a + c\). A "reduced (harmless cycle)" answer arises when the search returns to a φ-vertex \(v\) it entered with requirement \(v \le a + c_0\) and now needs only \(v_{\text{old}} \le a + c'\) with \(c' \ge c_0\) for the value \(v_{\text{old}}\) of the previous iteration. The edges along the cycle then establish: if \(v_{\text{old}} \le a + c_0\) then the value flowing back into \(v\) satisfies \(\le a + c_0\) as well (because \(c' \ge c_0\) is implied). That is the inductive step of an induction over loop iterations; the φ's other inputs (entering the loop) were proved \(\le a + c_0\) directly, which is the base case. So \(v \le a + c_0\) in every iteration. An amplifying cycle (\(c' < c_0\): each trip around the cycle can increase the value) would need a stronger hypothesis than it provides, so the search returns false there and never relies on it. Hence every "true" is backed by a valid inductive argument.

IRCE and loop predication

Theorem 18.9.12 (IRCE preserves behavior)

The pre-loop, main loop and post-loop of Algorithm 18.9.8 execute the same iterations in the same order as the original loop, and every check removed from the main loop would have succeeded.

Proof

The three loops cover consecutive, disjoint ranges of the IV — \([i_0, \min(n, lo))\), \([\max(i_0, lo), \min(n, hi))\), and the rest up to \(n\) — each starting where the previous one stopped, with the live values passed along; so the sequence of iterations is the original one (Theorem 18.5.14's argument for peeling, applied at both ends). The pre- and post-loops keep all checks, so a failing check fails in the same iteration with the same prior effects. Every iteration of the main loop has \(i \in [lo, hi)\), the intersection of the safe spaces, so every inductive range check there is true, and replacing it by true changes nothing (Theorem 18.9.10's argument). The IV's no-wrap precondition ensures the ranges are computed without overflow.

Theorem 18.9.13 (Loop predication preserves behavior under deoptimization semantics)

Assume a failing guard may transfer control to the interpreter at any earlier guard point with the corresponding state, and that the interpreter executes the original program precisely. Then Algorithm 18.9.9 preserves behavior: the widened guard fails iff some iteration's original guard fails.

Proof

The loop runs \(i = 0, 1, \dots, n - 1\) (for \(n > 0\); the entry test excludes \(n \le 0\)). The original guard fails in some iteration iff \(\exists i \in [0, n - 1]: i \ge_u \mathit{len}\), iff \(0 \ge_u \mathit{len}\) or \(n - 1 \ge_u \mathit{len}\) (the IV's values form an increasing range without wrapping, so the maximum is \(n - 1\) and the minimum is 0) — the negation of the widened condition. If the widened guard succeeds, no original guard fails, and removing them changes nothing. If it fails, it fails at the first iteration's guard point, and the interpreter re-executes from there: it runs the original iterations until the first real failure, producing the original behavior. The freeze ensures the widened condition is a definite value even where an operand could be poison, so no undefined behavior is introduced.

5. Complexity

\(C\) = number of checks, \(V\) = SSA values, \(E\) = inequality-graph edges, \(S\) = loop size.

Technique	Per check	Transformation	Worst case	Variables
Range-based bounds-check elimination	One SCEV query (cached CRs; dominating conditions walked up the dominator tree)	\(O(1)\) per removed check	SCEV's dominating-condition walk is bounded by a depth limit	\(C\)
ABCD	Demand-driven search, memoized: \(O(E)\) per query in the worst case, typically a few edges	\(O(1)\)	\(O(C \cdot E)\)	\(C\), \(E\)
IRCE and loop predication	Recognition \(O(S)\)	IRCE: up to \(3S\) code; predication: \(O(1)\) new instructions	Pre- and post-loops triple the loop's code	\(S\)

Proposition 18.9.14 (Checks executed)

For for i in 0..n: xs[i] with \(n > \mathit{len} \ge 0\): the original loop executes \(\mathit{len} + 1\) checks before trapping; after IRCE, 1 (the post-loop's first iteration); after loop predication, 1 widened check (plus the interpreter's \(\mathit{len} + 1\) after deoptimizing). For \(n \le \mathit{len}\): \(n\) checks originally, 0 after IRCE's main loop, 1 after predication.

Proof

The original loop checks in each iteration \(0..\mathit{len}\) and traps at \(i = \mathit{len}\). IRCE's main loop covers \([0, \min(n, \mathit{len}))\) without checks; the post-loop starts at \(i = \min(n, \mathit{len})\), which is \(\mathit{len}\) when \(n > \mathit{len}\), and its first check fails; when \(n \le \mathit{len}\) the post-loop is empty. Predication evaluates the widened condition once per loop entry (after hoisting); it fails iff \(n > \mathit{len}\) (Theorem 18.9.13).

Pathological input. A check whose index is not an add recurrence — xs[perm[i]] — defeats all three: no range, no inequality chain, no inductive structure. Only a runtime check of the whole permutation's range (versioning, Lesson 18.5) could help, and compilers do not attempt it.

At scale. JIT compilers for Java and JavaScript rely on these techniques because checks are everywhere; ahead-of-time compilers for Rust, Swift and Go rely mostly on range reasoning (SCEV/CVP/constraint elimination in LLVM, prove in Go) plus programmer hints like Go's _ = xs[3] or Rust's assert!(i < xs.len()) before a loop.

6. Variants and refinements

Range-based bounds-check elimination

• Dominating-check elimination: a check of xs[i+3] makes later checks of xs[i]..xs[i+3] redundant (the hint function) — trade-off: only works forward from an existing check.
• Check hoisting with versioning: test n <= len once and run a check-free copy of the loop — trade-off: code size (Lesson 18.5).

ABCD

• Partial redundancy of checks: ABCD's paper also inserts checks at cheaper points when a check is only partially redundant — trade-off: needs profile or careful placement.
• Poset-based facts (Go): keep a partial order of SSA values incrementally while walking the dominator tree — trade-off: no general shortest paths, but no separate graph.

IRCE and loop predication

• Guard widening (guard-widening): merge two guards into one stronger guard earlier in the code — trade-off: deoptimizes earlier in more cases.
• Widenable branches (llvm.experimental.widenable.condition): the guard semantics expressed with ordinary branches, so other passes understand them — trade-off: a special intrinsic in the condition.

7. In real compilers

Range-based bounds-check elimination

LLVM

llvm/lib/Transforms/Scalar/IndVarSimplify.cpp and llvm/lib/Transforms/Utils/SimplifyIndVar.cpp — SimplifyIndvar::eliminateIVComparison (folds comparisons of an IV using SCEV) [LLVM-IndVars]; llvm/lib/Transforms/Scalar/ConstraintElimination.cpp — ConstraintInfo, checkCondition, facts from dominating conditions [LLVM-CE]; llvm/lib/Transforms/Scalar/CorrelatedValuePropagation.cpp (ranges, nuw/nsw inference); ScalarEvolution::isKnownPredicateAt in llvm/lib/Analysis/ScalarEvolution.cpp [LLVM-SCEV] (LLVM 23.1.2).

• Go src/cmd/compile/internal/ssa/prove.go (prove, factsTable.update) and loopbce.go (findIndVar) (Go 1.24.7) [Go-Prove].

Find where LLVM does it. Open SimplifyIndVar.cpp and find the function that replaces an IV comparison by a constant when SCEV can decide it. Question: what is its name? (Quiz bce-find-indvar.)

The real-world boxes for this technique are in §2.

ABCD

LLVM

LLVM has no ABCD pass; the same proofs come from llvm/lib/Transforms/Scalar/ConstraintElimination.cpp (ConstraintInfo, checkCondition), whose system of linear constraints over dominating facts is decided by Fourier–Motzkin elimination in llvm/lib/Analysis/ConstraintSystem.cpp (ConstraintSystem::eliminateUsingFM) [LLVM-CE] (LLVM 23.1.2).

• Go src/cmd/compile/internal/ssa/poset.go — a partial order over SSA values ("a union-find data structure that can represent a partially ordered set of SSA values") used by prove to chain inequalities (Go 1.24.7) [Go-Prove].

The real-world box for this technique is in §2.

IRCE and loop predication

LLVM

llvm/lib/Transforms/Scalar/InductiveRangeCheckElimination.cpp — InductiveRangeCheck::extractRangeChecksFromBranch, InductiveRangeCheckElimination::run; the loop splitting in llvm/lib/Transforms/Utils/LoopConstrainer.cpp [LLVM-IRCE]; llvm/lib/Transforms/Scalar/LoopPredication.cpp — LoopPredication::widenICmpRangeCheck, with the header comment explaining why SCEV's facts must not be used circularly; llvm/lib/Transforms/Scalar/GuardWidening.cpp [LLVM-LoopPredication] (LLVM 23.1.2).

• HotSpot C2 (OpenJDK, tag jdk-21-ga) performs range-check elimination by loop splitting and loop predication for Java in src/hotspot/share/opto/loopTransform.cpp and loopPredicate.cpp; [WWM07] describes the client compiler's (C1) variant.

The real-world boxes for this technique are in §2.

8. Comparison

Technique	Power / precision	Speed	Output / error quality	Implementation effort	Typical use
Range-based bounds-check elimination	Affine indices with known ranges; defeated by wrap-around and unrelated bounds	One analysis query per check	Checks disappear; kept checks unchanged	Low given SCEV (E5 is ~80 lines)	AOT compilers of safe languages
ABCD	Chains of inequalities between variables, including loop-carried ones	Demand-driven, cheap per check	Proof or nothing	Medium (e-SSA, cycle handling)	JITs; Go's prove in poset form
IRCE and loop predication	Checks whose bounds are unrelated to the loop bound	Linear	IRCE: more loops; predication: one invariant check	Medium to high	JITs with deoptimization (predication); AOT (IRCE)

Choose range-based BCE first — it removes the common for i < len(xs) checks. Choose ABCD-style inequality reasoning when proofs chain through several variables. Choose IRCE when the loop bound is unrelated to the length and the checks almost always pass; choose predication in a runtime that can deoptimize.

9. Assessment

Technique	Quiz ids (solutions/quizzes/ch18.yaml)	Drill	Flashcard tag	Exercises
Range-based bounds-check elimination	bce-range, bce-wrap, bce-find-indvar	./course drill trip-count (the IV's range comes from the trip count)	range-bce	E5 ★
ABCD	abcd-path, abcd-cycle	none: ABCD's proofs are short paths, computed in the quiz	abcd	—
IRCE and loop predication	irce-split, predication-widen	none: the split points are computed in the quiz	irce-predication	—

Pitfall

Removing a check is only half the job: the trap must still happen in every execution that trapped before, at the same point. A "bounds-check elimination" that hoists if (n > len) trap before a loop without deoptimization semantics is wrong — the original program would have executed (and possibly printed, or written memory in) iterations \(0..\mathit{len} - 1\) first.

References

See the chapter references.