How Go Deletes Your Bounds Checks: The Facts Table That Proves i < len(s)

TL;DR: Every s[i] in Go compiles to a compare-and-panic. Then the compiler tries to prove the compare is always true and deletes it. The proof lives in cmd/compile/internal/ssacompile/prove.go, and it works by tracking relations between SSA values in separate domains — signed, unsigned, pointer, boolean — because the same bit pattern means different things in each. When the facts table learns 0 <= i < len(s) on one branch, it can answer the question “is i in bounds?” with a constant true, and the branch disappears.

Every index operation in Go is a potential panic. That is a language guarantee, and it is enforced by the compiler generating a comparison and a branch to a panic call. The interesting question is what happens after that.

Go has always deleted bounds checks it can prove redundant. It is one of the oldest and most valuable optimisations in the compiler, and it is also one of the least known. The mechanism is a static analysis pass called prove, and its data structure is a small, sound, deliberately incomplete theorem prover.

What a bounds check looks like

In SSA, an index operation becomes an IsInBounds value. The architecture rules lower it to a single unsigned compare:

text

// src/cmd/compile/internal/ssa/_gen/AMD64.rules:463
(IsInBounds idx len) => (SETB (CMPQ idx len))

One CMPQ, one SETB. Cheap. But not free — it is a branch that the CPU cannot predict, sitting in the middle of what is otherwise a tight loop.

The generic rules can also fold it away at the lowering level, before the prove pass ever runs:

text

// src/cmd/compile/internal/ssa/_gen/generic.rules:265
(IsInBounds (ZeroExt8to32  _) (Const32 [c])) && (1 << 8)  <= c => (ConstBool [true])
(IsInBounds (ZeroExt16to32 _) (Const32 [c])) && (1 << 16) <= c => (ConstBool [true])
(IsInBounds x x) => (ConstBool [false])

The first two are trivially true: a byte cannot index past 256 elements. The third is a curiosity — s[s] is always out of bounds, because the length is strictly less than the length.

But these are special cases. The general case needs real reasoning.

Domains: the key insight

Here is the problem that makes naive range analysis wrong in Go.

go
func f(x int) {
    var a [4]int
    _ = a[x] // must panic for x >= 4 or x < 0
}

If you only tracked “x is between 0 and 3”, you would prove the check redundant — and be wrong, because x could be -1.

The classic fix is to track signedness. Go’s prove pass goes further: it maintains a set of domains per value, and relations are only ever transferred within a domain.

go
// src/cmd/compile/internal/ssacompile/prove.go:85
// domain represents the domain of a variable pair in which a set
// of relations is known. For example, relations learned for unsigned
// pairs cannot be transferred to signed pairs because the same bit
// representation can mean something else.
type domain uint

const (
	signed domain = 1 << iota
	unsigned
	pointer
	boolean
)

And the relation itself is a three-bit mask:

go
// src/cmd/compile/internal/ssacompile/prove.go:65
type relation uint

const (
	lt relation = 1 << iota
	eq
	gt
)

var relationStrings = [...]string{
	0: "none", lt: "<", eq: "==", lt | eq: "<=",
	gt: ">", gt | lt: "!=", gt | eq: ">=", gt | eq | lt: "any",
}

So “less than”, “equal”, “greater than” are three independent bits, and a relation is a set of possibilities, not a single answer. Before a branch, the compiler knows x could be less than, equal to, or greater than y. After a branch on x < y, the relation on the taken edge becomes {lt} and on the other edge becomes {eq, gt}.

This is a “domain-partitioned range analysis” and it is the standard trick for making bounds-check elimination sound in the presence of signed arithmetic.

The facts table

go
// src/cmd/compile/internal/ssacompile/prove.go:146

// factsTable keeps track of relations between pairs of values.
//
// The fact table logic is sound, but incomplete. Outside of a few
// special cases, it performs no deduction or arithmetic. While there
// are known decision procedures for this, the ad hoc approach taken
// by the facts table is effective for real code while remaining very
// efficient.
type factsTable struct {
	// unsat is true if facts contains a contradiction.
	//
	// Note that the factsTable logic is incomplete, so if unsat
	// is false, the assertions in factsTable could be satisfiable
	// *or* unsatisfiable.
	unsat      bool // true if facts contains a contradiction
	unsatDepth int  // number of unsat checkpoints

	// order* is a couple of partial order sets that record information
	// about relations between SSA values in the signed and unsigned
	// domain.
	orderS *ssa.Poset
	orderU *ssa.Poset

Two things in that comment are worth pausing on.

“Sound, but incomplete.” The analysis never claims a check is redundant unless it is definitely redundant. It may leave redundant checks in place. That is the right trade for a compiler: a missed optimisation costs a nanosecond, an unsound one is a memory-safety bug.

“Known decision procedures for this.” There are complete algorithms for this problem (Presburger arithmetic, mostly). The compiler does not use them because they are slow. This is a deliberate engineering choice: an ad-hoc analysis that is fast enough to run on every function beats a complete one that is not.

The table keeps several kinds of facts:

orderS / orderU: two partial orders, one per numeric domain, tracking which values are greater than which.
additions: a map from a base value to a list of values equal to it plus a constant delta.
orderings: explicit pairwise relations.
limits: per-value numeric bounds.

That last one is where the really clever bit lives.

Limits: knowing the range of a value

go
// src/cmd/compile/internal/ssa/prove.go:120
// a Limit records known upper and lower bounds for a value.
//
// If we have min>max or umin>umax, then this Limit is
// called "unsatisfiable". When we encounter such a Limit, we
// know that any code for which that Limit applies is unreachable.
// We don't particularly care how unsatisfiable limits propagate,
// including becoming satisfiable, because any optimization
// decisions based on those limits only apply to unreachable code.
type Limit struct {
	Min, Max   int64  // min <= value <= max, signed
	Umin, Umax uint64 // umin <= value <= umax, unsigned
	// For booleans, we use 0==false, 1==true for both ranges
	// For pointers, we use 0,0,0,0 for nil and minInt64,maxInt64,1,maxUint64 for nonnil
}

A Limit is a range, and it is not just a range — it is a range in both domains simultaneously, plus the ability to represent “unsatisfiable”, which means “this code is unreachable”.

The initialisation is where the type system leaks into the analysis:

go
// src/cmd/compile/internal/ssa/prove.go:66
	// Default limits based on type.
	lim := NoLimitForBitsize(uint(v.Type.Size()) * 8)

	// Tighter limits on some opcodes.
	switch v.Op {
	// constants
	case ssaop.OpConst64:
		lim = Limit{Min: v.AuxInt, Max: v.AuxInt, Umin: uint64(v.AuxInt), Umax: uint64(v.AuxInt)}
	...
	// extensions
	case ssaop.OpZeroExt8to64, ssaop.OpZeroExt8to32, ssaop.OpZeroExt8to16:
		lim = lim.SignedMinMax(0, 1<<8-1)
		lim = lim.UnsignedMax(1<<8 - 1)

A uint8 has limits [0, 255]. A zero-extended byte has the same limits. A sign-extended byte has [-128, 127]. All of this is derived from the SSA opcode, before any dataflow — the type of the value tells you its range.

Then there is the length operation, which is the one that matters for bounds checks:

go
// src/cmd/compile/internal/ssa/prove.go:95
	// length operations
	case ssaop.OpSliceLen, ssaop.OpSliceCap:
		f := v.Block.Func
		elemSize := uint64(v.Args[0].Type.Elem().Size())
		if elemSize > 0 {
			heapSize := uint64(1)<<(uint64(f.Config.PtrSize)*8) - 1
			maximumElementsFittingInHeap := heapSize / elemSize
			lim = lim.UnsignedMax(maximumElementsFittingInHeap)
		}
		fallthrough
	case ssaop.OpStringLen:
		lim = lim.signedMin(0)

A slice length cannot exceed the number of elements that could physically fit in the address space. On a 64-bit machine, a []byte can have at most 2^64 - 1 elements. On a 32-bit machine, at most 2^32 - 1. This bound is weak in absolute terms, but it is exactly what is needed to make unsigned comparisons sound.

Learning from branches

The prove pass walks the control flow graph, and at each branch it refines the facts. The refinement is where IsInBounds gets its power:

go
// src/cmd/compile/internal/ssacompile/prove.go:460
		case ssaop.OpIsInBounds, ssaop.OpIsSliceInBounds:
			// 0 <= a0 < a1 (or 0 <= a0 <= a1)
			r := lt
			if v.Op == ssaop.OpIsSliceInBounds {
				r |= eq
			}
			if isTrue {
				// On the positive branch, we learn:
				//   signed: 0 <= a0 < a1 (or 0 <= a0 <= a1)
				//   unsigned:    a0 < a1 (or a0 <= a1)
				ft.setNonNegative(v.Args[0])
				ft.update(v.Block, v.Args[0], v.Args[1], signed, r)
				ft.update(v.Block, v.Args[0], v.Args[1], unsigned, r)
			} else {
				// On the negative branch, we learn (0 > a0 ||
				// a0 >= a1). In the unsigned domain, this is
				// simply a0 >= a1 (which is the reverse of the
				// positive branch, so nothing surprising).
				// But in the signed domain, we can't express the ||
				// condition, so check if a0 is non-negative instead,
				// to be able to learn something.
				r ^= lt | gt | eq // >= (index) or > (slice)
				if ft.isNonNegative(v.Args[0]) {
					ft.update(v.Block, v.Args[0], v.Args[1], signed, r)
				}
				ft.update(v.Block, v.Args[0], v.Args[1], unsigned, r)
				// TODO: v.Block is wrong here
			}

Read the positive branch carefully. When the compiler knows IsInBounds(i, n) is true, it learns two things: i is non-negative, and i < n. Those are separate facts, and the second one is exactly what a later IsInBounds(i, n) needs to be proved true.

The negative branch shows the domain partition doing its job. When the check fails, the compiler learns i >= n in the unsigned domain unconditionally, but in the signed domain it can only learn that if it already knows i is non-negative — because the failure condition is i < 0 || i >= n, and the signed domain cannot express a disjunction. The comment says exactly that:

But in the signed domain, we can’t express the || condition, so check if a0 is non-negative instead, to be able to learn something.

That is a small piece of textbook reasoning, expressed as three lines of Go.

The chunked-access special case

There is one genuinely clever piece of reasoning in the pass, and it handles the pattern that shows up in every hand-written parser:

go
for i := 0; i+4 <= len(s); i++ {
    x := binary.BigEndian.Uint32(s[i:])
    ...
}

Here the compiler must prove i, i+1, i+2 and i+3 are all in bounds.

go
// src/cmd/compile/internal/ssacompile/prove.go:1937
func checkForChunkedIndexBounds(ft *factsTable, b *ssa.Block, index, bound *ssa.Value, isReslice bool) bool {
	if bound.Op != ssaop.OpSliceLen && bound.Op != ssaop.OpStringLen && bound.Op != ssaop.OpSliceCap {
		return false
	}

	// this is a slice bounds check against len or capacity,
	// and refers back to a prior check against length, which
	// will also work for the cap since that is not smaller
	// than the length.

	slice := bound.Args[0]
	lim := ft.limits[index.ID]
	if lim.Min < 0 {
		return false
	}
	i, delta := isConstDelta(index)
	if i == nil {
		return false
	}
	if delta < 0 {
		return false
	}

The comment inside the function is a worked example of the logic:

go
	// special case for blocked iteration over a slice.
	// slicelen > i + delta && <==== if clauses above
	// && index >= 0           <==== if clause above
	// delta >= 0 &&           <==== if clause above
	// slicelen-K >/>= x       <==== checked below
	// && K >=/> delta         <==== checked below
	// then v > w
	// example: i <=/< len - 4/3 means i+{0,1,2,3} are legal indices

And the implementation:

go
	for o := ft.orderings[i.ID]; o != nil; o = o.next {
		if o.d != signed {
			continue
		}
		if ow := o.w; ow.Op == ssaop.OpAdd64 {
			var lenOffset *ssa.Value
			if bound := ow.Args[0]; (bound.Op == ssaop.OpSliceLen || bound.Op == ssaop.OpStringLen) && bound.Args[0] == slice {
				lenOffset = ow.Args[1]
			} else if bound := ow.Args[1]; (bound.Op == ssaop.OpSliceLen || bound.Op == ssaop.OpStringLen) && bound.Args[0] == slice {
				lenOffset = ow.Args[0]
			}
			if lenOffset == nil || lenOffset.Op != ssaop.OpConst64 {
				continue
			}
			if K := -lenOffset.AuxInt; K >= 0 {
				or := o.r
				if isReslice {
					K++
				}
				if or == lt {
					or = lt | eq
					K++
				}
				if K < 0 { // We hate thinking about overflow
					continue
				}

				if delta < K && or == lt|eq {
					return true
				}
			}
		}
	}
	return false
}

The idea: if the compiler knows i < len(s) - 4 (or i <= len(s) - 4), then i+3 < len(s) and the check on i+3 is redundant. The K bookkeeping handles the off-by-one difference between < and <=, and the reslice case (which allows the last element) needs an extra increment.

The comment // We hate thinking about overflow is doing a lot of work. K is derived from a negated constant, and negating math.MinInt64 overflows. The code refuses to reason about it rather than getting it wrong.

The `Limit` type is more than a range

Look again at the arithmetic operations available on a Limit:

go
// src/cmd/compile/internal/ssa/prove.go:308
func (l Limit) Add(l2 Limit, b uint) Limit {

go
// src/cmd/compile/internal/ssa/prove.go:349
func (l Limit) Sub(l2 Limit, b uint) Limit {

go
// src/cmd/compile/internal/ssa/prove.go:367
func (l Limit) Mul(l2 Limit, b uint) Limit {

go
// src/cmd/compile/internal/ssa/prove.go:401
func (l Limit) Com(b uint) Limit {

Add, Sub, Mul, Com (complement), Neg, Ctz, Bitlen, Popcount, Exp2. This is an interval-arithmetic library, embedded in the compiler, used to compute the range of a value from the ranges of its inputs.

The Com case is a nice example of the domain partition earning its keep:

go
// src/cmd/compile/internal/ssa/prove.go:401
func (l Limit) Com(b uint) Limit {

Complementing a signed value gives a different range than complementing an unsigned one, and the type knows which domain it is in.

The `poset`: transitivity for free

The orderS and orderU fields are *ssa.Poset — partial orders. That is the trick that makes the analysis cheap: you do not need to record a < b and b < c and a < c separately. The poset derives the third from the first two.

The explicit orderings map is for facts the poset cannot represent:

go
// src/cmd/compile/internal/ssacompile/prove.go:176
	// orderings contains a list of known orderings between values.
	// These lists are indexed by v.ID.
	// We do not record transitive orderings. Only explicitly learned
	// orderings are recorded. Transitive orderings can be obtained
	// by walking along the individual orderings.
	orderings map[ssa.ID]*ordering

So the poset handles the “greater than” relation (a total order on values, which is transitive) and the explicit list handles the mixed relations (!=, <=, >=) that are not.

Proving the check itself

Now the payoff. When the compiler reaches an IsInBounds, it asks whether the facts table already implies it:

go
// src/cmd/compile/internal/ssacompile/prove.go:2157
	case ssaop.OpIsInBounds:
		if checkForChunkedIndexBounds(ft, b, v.Args[0], v.Args[1], false) {
			if b.Func.Pass.Debug > 0 {
				b.Func.Warnl(v.Pos, "Proved %s for blocked indexing", v.Op)
			}
			ft.booleanTrue(v)
		}

ft.booleanTrue(v) sets the value’s limit to the constant 1. Once the value is a compile-time constant, the branch that depends on it folds away, and the panic path becomes dead code.

The b.Func.Warnl call is only active with -d=ssa/prove/debug=1 — the compiler will tell you exactly which checks it proved:

text

$ go build -gcflags='-d=ssa/prove/debug=1' ./...

How do you check the compiler’s work?

There is a dedicated debug facility:

go
// src/cmd/compile/internal/ssacompile/checkbce.go:14
// checkbce prints all bounds checks that are present in the function.
// Useful to find regressions. checkbce is only activated when with
// corresponding debug options, so it's off by default.
// See test/checkbce.go
func checkbce(f *ssa.Func) {
	if f.Pass.Debug <= 0 && !logopt.Enabled() {
		return
	}

With -d=ssa/checkbce/debug=1 you get a list of every bounds check that survived the optimisation. That is exactly the tool you want when you have written a hot loop and want to know why the check is still there.

The SSA dump itself (-d=ssa/dump=1) shows the IsInBounds values and, after the prove pass, whether they have been folded to ConstBool [true].

Trade-offs

Sound but incomplete. The analysis will leave provably-redundant checks in place. This is deliberate. A complete decision procedure exists (Presburger arithmetic) but is too slow to run on every function.

Domain partitioning costs completeness. Because signed and unsigned facts never mix freely, the analysis sometimes cannot prove things it “should” be able to. The || handling in the negative branch is the visible symptom.

The factsTable is ad hoc. The source says so, and it is a feature: the implementation optimises for real code shapes rather than for theoretical completeness.

Bounds checks are cheap, but not free. A CMPQ and a SETB are one instruction each. The branch is the expensive part, because it is unpredictable in exactly the loops where you care about performance.

Loop induction variables get special treatment. There is a whole separate file, loopbce.go, for finding induction variables and rewriting loops into “downward counting” form, which is easier to prove:

go
// src/cmd/compile/internal/ssacompile/loopbce.go:25
type indVar struct {
	ind   *ssa.Value // induction variable
	nxt   *ssa.Value // the incremented variable
	min   *ssa.Value // minimum value, inclusive/exclusive depends on flags
	max   *ssa.Value // maximum value, inclusive/exclusive depends on flags
	entry *ssa.Block // the block where the edge from the succeeded comparison of the induction variable goes to, means when the bound check has passed.
	step  int64      // it will always be positive.
	flags indVarFlags
	// Invariant: for all blocks dominated by entry:
	//	min <= ind <  max    [if flags == 0]
	//	min <  ind <  max    [if flags == indVarMinExc]
	//	min <= ind <= max    [if flags == indVarMaxInc]
	//	min <  ind <= max    [if flags == indVarMinExc|indVarMaxInc]
}

The Invariant comment is the contract, and the flag-based inclusivity is what lets the analysis handle for i := 0; i < n; i++ and for i := 0; i <= n-1; i++ with the same machinery.

Caveats

You cannot rely on a check being removed. The analysis may change between Go releases, or not fire for your particular code shape. If your code depends on the check not being there for performance, that is fragile.

The //go:nosplit and unsafe escape hatches bypass all of this. If you use unsafe, the compiler will not add checks in the first place, and the prove pass has nothing to work with.

Bounds checks on struct fields and pointers are different. The analysis here is about slice and string indexing. A nil-pointer dereference is a different check (OpIsNonNil), handled by the same facts table but with different rules — note the pointer domain in the domain type.

The -d=ssa/checkbce output is a debugging aid, not a contract. It prints what the pass saw, in the pass’s own terms.

IsSliceInBounds allows the last element, IsInBounds does not. The difference is one bit in the relation (r |= eq), and it matters for three-index slicing s[i:j:k].

Wrapping up

The one thing to remember: Go’s bounds-check elimination is a domain-partitioned range analysis. The same bit pattern means different things as a signed and an unsigned number, so the compiler keeps separate facts for each domain and refuses to mix them.

The part people get wrong: the compiler does not remove the check because it “knows” the index is small. It removes the check because an earlier branch already established the fact, and it re-establishes that fact on the taken edge. The proof is a dataflow property, not a syntactic one.

What to go do about it: write loops in the shape the analysis likes — for i := range s, or for i := 0; i < len(s); i++ — and check your work with -gcflags='-d=ssa/checkbce/debug=1'. If a check survives that you thought would go, the loop shape is probably the reason.

What a bounds check looks like

Domains: the key insight

The facts table

Limits: knowing the range of a value

Learning from branches

The chunked-access special case

The Limit type is more than a range

The poset: transitivity for free

Proving the check itself

How do you check the compiler’s work?

Trade-offs

Caveats

Wrapping up

Further reading

The `Limit` type is more than a range

The `poset`: transitivity for free