Toolingspec

Abstract Interpretation

Execute the program over a deliberately impoverished set of values — signs, nullability, intervals — so that the analysis terminates and covers every input at once. Widening is the part that makes loops finish, and it is where the precision goes.

The question

How can a tool reason about every possible input without enumerating any of them?

Source→Lexing→Tokens→Parsing→AST→Semantics→Typed→IR→Optimize→Codegen→Machine code→Link→Execute

What the program is here

The program, plus an *abstract state* at every program point: a map from each variable to an element of an abstract domain rather than to a value. Where a concrete execution says x = 7, the abstract execution says x ∈ Positive or x ∈ [1, 10] or x ∈ NonNull. The domain is finite (or made finite), which is what turns "consider every execution" from an infinite enumeration into a terminating computation over a lattice.

What this phase may assume or do

The abstraction must be a sound over-approximation: for every concrete operation f and its abstract counterpart f#, the concretization of f#(a) must contain f applied to every concrete value that a represents — γ(f#(a)) ⊇ { f(c) | c ∈ γ(a) }. Under that precondition an abstract result of "never null here" really means never null on any execution. Break it — model malloc as always succeeding, model integer arithmetic without overflow, forget that a callee can modify a global — and every conclusion downstream is unsound even though the machinery still runs and still terminates.

Key points

Abstract interpretation runs the program over properties of values rather than values, so one analysis covers every input at once.
The abstract domain is a lattice: elements ordered by precision, Top for unknown, Bottom for unreachable, and a join used wherever control flow merges.
Soundness is the precondition γ(f#(a)) ⊇ f(γ(a)) — the abstract operation must cover every concrete outcome, or every conclusion is worthless.
A branch condition refines the state on its edge; a merge joins and therefore loses information. Both are what makes flow-sensitive null checking work.
Widening exists because domains such as intervals have infinite ascending chains and the iteration would not terminate. It jumps to a fixed point by throwing a bound away.
Narrowing after widening recovers precision from the loop guard, but only when the analysis can interpret the guard.
Choosing the domain decides which bugs are findable. Non-relational domains cannot prove i < len for variable len; relational ones can and cost far more.
Constant propagation and type checking are both instances of this framework, which is why the machinery is already in your compiler.

Run the program over the wrong values on purpose

simplifiedThis table is exact for mathematical integers and wrong for machine integers, which is the classic way a sign analysis becomes unsound. Positive * Positive is Positive in ℤ; in 32-bit two's-complement C it can be negative through signed overflow — though there the language declares overflow undefined, so a compiler is entitled to assume the table holds. In Java, Rust release builds or Go, overflow is defined to wrap and the table is simply incorrect: a sound sign domain for those languages must return Top for Positive * Positive, or track intervals and detect the wrap. The Zero row survives everywhere, which is why zero-tracking is the one part of sign analysis that is safe to reuse.

The problem with reasoning about every execution is that there are too many. A function taking two 32-bit integers has 2^64 inputs; add a loop bound and there is no enumeration to do. Abstract interpretation's move is to stop tracking values and start tracking *properties of values*, chosen so that there are only a handful of them, and then to run the program's operations over the properties instead.

Concretely: pick a domain. The sign domain has five elements — Positive, Negative, Zero, NonZero, plus Top for "could be anything" and Bottom for "unreachable". The nullability domain has Null, NonNull, Maybe. The interval domain represents a variable as [lo, hi] with infinities allowed. Then define what each operation does in that domain: multiplying a Positive by a Negative yields a Negative, no matter which positive and which negative.

That is the whole idea, and the reason it is worth learning as a compiler engineer rather than as a formal-methods topic: [[constant-propagation]] is abstract interpretation over the domain "this constant, or unknown", and it is running in your optimizer right now. The domain is just unusually small.

The abstract multiplication table for the sign domain — x * ysimplified

x \ y	Positive	Negative	Zero	Top
Positive	Positive	Negative	Zero	Top
Negative	Negative	Positive	Zero	Top
Zero	Zero	Zero	Zero	Zero
Top	Top	Top	Zero	Top

The lattice, and what happens where paths merge

A domain is not just a set of labels; it is a lattice, which means the labels are ordered by precision and any two of them have a least upper bound. Positive and Negative are incomparable, and their join is NonZero if the domain has it and Top if it does not. Bottom sits below everything and means "no execution reaches here" — which is how unreachable-code detection falls out of the same machinery for free.

The ordering is what makes control-flow joins work. When two branches merge, the analysis takes the join of their abstract states: if x is Positive on the then-branch and Negative on the else-branch, it is NonZero after the merge. That is a genuine loss — the analysis no longer knows which — and it is exactly the over-approximation that soundness requires. Nothing in the merged state is false; it is just weaker than either branch.

The reverse direction is where the precision comes back: a condition refines the state on the branch it guards. Inside if (p != null) { ... }, p is NonNull even though it was Maybe outside. Type-checker authors call this narrowing or flow typing, and it is the single most user-visible piece of abstract interpretation in a modern language — it is why [[nullability]] in Kotlin or TypeScript feels like the compiler is following your reasoning.

Nullability over a diamond: the join is where the information is lost

b0entryentry
```
p = lookup(key)   // p: Maybe
if (p != null)
```
lookup is modelled as possibly returning null, so the entry state is Maybe.
b1then
```
// p: NonNull  (refined by the guard)
use(p.field)
```
The condition refines the state on this edge only.

b2else

// p: Null     (refined by the negation)
p = fallback()    // p: NonNull

An assignment overwrites the fact rather than joining with it.

b3join
```
// p: NonNull ⊔ NonNull = NonNull
return p.field
```
Both predecessors say NonNull, so the join says NonNull and the dereference is safe.

Edges

b0→b1p != null
b0→b2p == null
b1→b3
b2→b3

Read it asDelete the p = fallback() line and the join becomes NonNull ⊔ Null = Maybe, and the dereference in b3 is reported. That single line is the difference between a warning and silence, and the analysis reached its conclusion by joining at b3 rather than by exploring two paths — which is what keeps it linear in the size of the CFG instead of exponential in the number of branches.

Widening: why loops terminate

Everything above works because the analysis iterates to a fixed point, and [[fixed-point-iteration]] terminates because the lattice has finite height — you can only move upward so many times before you hit Top. The sign domain has height three. The nullability domain has height two. Fine.

The interval domain does not. Consider for (i = 0; ; i++). The analysis starts with i ∈ [0,0], goes round the loop, joins to get [0,1], then [0,2], then [0,3] — and never stops, because the interval lattice has infinite ascending chains. The fixed point exists mathematically; the iteration does not reach it in finite time. This is not an edge case: any domain that can represent unboundedly many facts about a numeric variable has this problem.

Widening is the fix, and it is deliberately crude. When a loop header's state is being updated for the *n*th time, instead of joining, apply a widening operator ∇ that jumps to a fixed point in one move: if a bound is increasing, throw it to infinity. [0,1] ∇ [0,2] = [0, +∞]. The chain stops immediately, the analysis terminates, and the result is sound but weaker — you now know i ≥ 0 and nothing about the upper bound.

Narrowing claws some of it back. After widening has produced a post-fixed point, run the transfer functions again *without* widening: the loop condition i < n will refine [0, +∞] back down to [0, n-1]. Widening then narrowing is the standard recipe, and the reason a good interval analysis can still prove an array index in bounds after having thrown the bound away.

The practical consequence is worth stating plainly, because it is the most common surprise: a value analysis loses precision at loops specifically, and it loses it in whichever direction the loop grows. When a bounds-check-elimination pass or a null checker gives up on exactly the code inside a loop, widening is very often why — see [[bounds-check-elimination]].

Interval analysis of a counting loop, iteration by iteration

Without widening — does not terminate

iter 1:  i ∈ [0,0]
iter 2:  i ∈ [0,0] ⊔ [1,1] = [0,1]
iter 3:  i ∈ [0,1] ⊔ [1,2] = [0,2]
iter 4:  i ∈ [0,2] ⊔ [1,3] = [0,3]
...      (ascending forever)

With widening at the loop header, then narrowing

▸iter 1:  i ∈ [0,0]
▸iter 2:  i ∈ [0,0] ∇ [0,1] = [0,+inf)    <- widened: upper bound thrown away
▸iter 3:  i ∈ [0,+inf)                     <- stable, fixed point reached
▸narrow:  guard i < n refines to [0, n-1]
▸result:  i ∈ [0, n-1] at the loop body

Read it asThe widening step is the only unsound-looking move in the whole algorithm, and it is sound: [0,+inf) contains everything [0,1] did. What it is not is *precise*. Narrowing recovers the upper bound here only because the loop condition mentions it; a loop whose exit condition the analyser cannot interpret — a call, a flag set elsewhere, a pointer comparison — keeps the widened interval, and every downstream check on that variable becomes a maybe.

Choosing a domain is choosing which bugs you can find

The domain is the design decision. It fixes what the analysis can prove, what it costs, and where it will be uselessly imprecise, and no amount of engineering elsewhere compensates for the wrong one. Sign analysis proves a divisor is non-zero and cannot prove an index is in bounds. Intervals prove the index and cannot prove that two pointers are distinct. Relational domains such as octagons (x - y ≤ c) and polyhedra can prove relationships between variables — which is what you need for i < len where both are variable — and cost polynomial to exponential time in the number of variables, which is why they run on avionics control code and not on your monorepo.

The pattern generalises past numeric domains. A typestate domain tracks Open/Closed per handle and finds resource leaks. A taint domain tracks Tainted/Clean and finds injection. A lock domain tracks the set of held locks and finds ordering violations. Each is a lattice, a transfer function and a join; the framework does not change.

And the framework is not exotic infrastructure you have to adopt. Your type checker is abstract interpretation over the domain of types. Your optimizer's constant propagation is abstract interpretation over a flat lattice of constants. What a dedicated tool such as Astrée or Frama-C adds is a richer domain and a great deal more patience, not a different idea.

Domains, ordered by what they can prove and what they costtypical

Domain	Elements	Proves	Cannot prove	Cost
Constant	`c` or Top	This expression is always 42	Anything about a variable that varies	Near-linear
Sign	Pos / Neg / Zero / NonZero / Top	The divisor is non-zero; the length is non-negative	Any bound	Near-linear
Nullability	Null / NonNull / Maybe	This dereference is safe on every path	Which object it points at	Near-linear
Interval	[lo, hi]	The index is within [0, 255]	That `i < len` when `len` is variable	Linear, but needs widening
Octagon	±x ±y ≤ c	That `i < len` — a relation between two variables	Anything needing three variables at once	Cubic in variables
Polyhedra	Linear inequalities	Complex loop invariants over many variables	Non-linear relationships	Exponential in the worst case

How it works

The steps, in the order the compiler takes them.

Pick an abstract domain: a set of elements, a partial order, a join for merges, and Top/Bottom.
Define an abstraction function α mapping concrete values to abstract elements, and a concretization γ mapping back to the set of concrete values an element represents.
Define an abstract transfer function for every operation in the IR, each of which must over-approximate its concrete counterpart.
Initialise every program point to Bottom (unreachable) except the entry, and place the entry block on a worklist.
Pop a block, apply its transfer functions to its incoming state, and propagate the result to successors, joining with whatever they already held; re-queue any successor whose state changed.
Refine along branch edges using the condition, so the then- and else-successors receive different, stronger states than the block produced.
At loop headers, after a fixed number of ordinary joins, apply widening instead so that ascending chains terminate.
Once stable, optionally run a narrowing pass that re-applies the transfer functions without widening to recover precision from loop guards.

How it breaks

What the engineer observes when it goes wrong — not what goes wrong internally.

A tool reports a possible null dereference inside a loop that is obviously safe from the source, because widening threw away the bound that made it safe, and the engineer adds a redundant check to silence it.
An interval analysis runs for minutes on one function and then reports nothing useful, because the loop exit condition depended on a call it could not model and every variable widened to (-inf, +inf).
The abstract multiplication table is written for mathematical integers, the language defines wrapping overflow, and the analysis silently concludes a wrapped product is positive — an unsound result with no diagnostic anywhere.
A domain with no Bottom treats an unreachable branch as reachable, and every finding on dead code is a false positive that nobody can explain.
Flow-sensitive narrowing is defeated by an intervening assignment the analyser cannot see through — a field write, a method call, a closure capture — and a variable the reader can see is non-null reports as Maybe after every call.
The analysis is precise on the test file and useless on the real one, because the real one has a loop and the test did not.

When it helps

Proving the absence of a whole class of runtime error over all inputs — division by zero, out-of-bounds index, null dereference, overflow — where a test suite can only sample.
Safety-critical code with bounded loops and no dynamic allocation, which is precisely the shape abstract interpretation is most precise on. This is why it is standard practice in avionics and automotive rather than a research curiosity.
Optimizer analyses: range information enables bounds-check elimination, sign information enables strength reduction, and nullability enables removing implicit checks in managed runtimes.
Flow-sensitive type narrowing in a language front end, which is the same algorithm and is the reason modern null-safety features feel usable.

When it hurts

Highly dynamic code — reflection, eval, dynamic dispatch to an unknown target, heavy metaprogramming — where the analysis has to assume the worst at every step and every state widens to Top immediately.
Large heap-manipulating programs, where tracking properties of *locations* rather than of variables needs a heap abstraction, and the cost and imprecision both grow sharply.
When the property you care about is relational and you have a non-relational domain. No amount of tuning makes intervals prove i < len; the answer is a different domain, which is a different cost class.
As a merge gate on a fast-moving codebase: the precise domains are slow enough that the honest place for them is a nightly job.

What it costs

Every one of these is paid by something.

A richer domain buys the ability to prove stronger properties and pays in analysis time — near-linear for intervals, cubic for octagons, exponential in the worst case for polyhedra — and in implementation complexity that is genuinely hard to get right.
Widening buys termination and pays precision, in the one place your program spends most of its time. There is no version of this analysis that keeps both.
Path sensitivity buys precise conditionals and pays an exponential number of states, so every real tool bounds it and becomes imprecise at the bound rather than at the join.
A sound over-approximation buys the right to say "cannot happen" and pays in false positives on every construct the domain cannot model — which for most tools means every call into a library without a model.
Adding narrowing buys back precision after widening and pays a second full traversal of the program, plus the subtlety that narrowing can fail to terminate too if implemented carelessly.

What else you could do

What a different compiler or language does instead, and when that is better.

Symbolic execution keeps a path condition and an SMT solver instead of a lattice, so it is precise per path and pays with path explosion and solver time. It answers "give me an input that reaches this bug" — which abstract interpretation structurally cannot.
Model checking explores a finite state space exhaustively and gives a counterexample trace, which is far more actionable than a warning, at the cost of needing the state space to be finite.
Type systems push the same reasoning into the language, so the programmer supplies the invariants as annotations instead of the tool inferring them. Refinement types and dependent types are the extreme version — see [[type-inference]] and [[effect-systems]].
Dynamic checks: insert a runtime assertion and stop trying to prove anything. Always precise, never early, and it costs runtime and a failure in production rather than a warning at build time.
Bounded verification — prove the property for all inputs up to some size — which is decidable, fast, and finds most real bugs while proving nothing in general.

See it for yourself

The flag, dump or tool that shows you this directly.

Watch narrowing happen in a type checker: in TypeScript with strictNullChecks, hover a variable inside and outside an if (x !== null) guard and read the two types. That difference *is* the refined abstract state.
GCC's value-range propagation is an interval domain: gcc -O2 -fdump-tree-vrp-details -c file.c writes a dump showing the ranges it inferred per SSA name, and -fdump-tree-all gives you every intermediate.
LLVM: opt -passes=print<scalar-evolution> -disable-output file.ll prints inferred trip counts and value ranges; -passes=ipsccp is conditional constant propagation, a lattice analysis you can dump before and after.
Clang static analyzer: clang --analyze -Xclang -analyzer-checker=core,alpha.core file.c and read the printed path — the path is the sequence of abstract states it walked.
gcc -fanalyzer -fanalyzer-verbosity=3 prints the state at each program point along the reported path, which is the most readable exposure of an abstract state in a mainstream toolchain.
Full-strength tools where the domain is the product: Astrée (intervals plus octagons plus more, used on avionics code), Frama-C's EVA plugin (frama-c -eva file.c), IKOS, and the Apron library if you want to experiment with domains directly.
Python: mypy --strict performs narrowing; run it with --show-error-context on a function with a loop to see where flow-sensitivity gives up.

Plausible wrong readings

Stated the way a confident engineer states them.

"Abstract interpretation simulates the program with fake values." It does not simulate an execution; it computes a property that holds over *all* executions simultaneously. There is no single trace being followed.
"Widening is a hack to make the tool faster." It is what makes the analysis terminate at all on an infinite-height domain. Without it the fixed-point iteration does not finish, at any speed.
"If the domain is sound, the tool is sound." Soundness of the domain plus unsound library models equals an unsound tool. Most real unsoundness lives in the models, not in the lattice.
"A more precise domain is strictly better." It is strictly slower, and on code that is dynamic enough it is equally imprecise while costing more — the precision only materialises if the program is in the shape the domain can describe.
"This is formal methods, so it does not apply to my compiler." Constant propagation, value-range propagation and flow-sensitive null checking are all abstract interpretation, and at least one of them ran on your last build.

Misconceptions

The claim, and what is actually true.

The abstract domain is chosen for performance.

It is chosen for what it can express. Cost follows from expressiveness, but a cheap domain is not a fast version of an expensive one — it simply cannot represent the fact you needed.

Widening loses information only in exotic cases.

It fires on every loop with an unbounded-looking induction variable, which is most loops. If a value analysis is imprecise in your code, the loop is the first place to look.

Joining at merges is less precise than exploring both paths, so good tools explore both paths.

Joining is what keeps the analysis linear in the CFG. Path-sensitive tools explore both paths up to a bounded budget and then join anyway — the join does not go away, it moves.

Go deeper

The same idea at increasing depth. Stop wherever it stops being useful.

overview

Instead of running your program on one input, run it on a description of many inputs at once: not x = 7 but x is positive, not p = 0x7ffd... but p is non-null. Define what each operation does to those descriptions — positive times negative is negative — and you can compute what holds for every possible run in one pass. Loops are the hard part: descriptions that can keep growing (like number ranges) would never settle, so the analysis eventually gives up on the growing end and says "anything from zero upward". That giving-up step is called widening, and it is why value analyses are least precise exactly inside loops.

practical

You meet this most often as flow-sensitive narrowing in a type checker, and the practical skill is knowing what defeats it. A guard refines a variable on its branch; an assignment overwrites the fact; a call may invalidate it, because the analyser must assume the callee touched anything it could reach. That is why if (this.p != null) { this.p.f() } narrows in a local variable and often does not through a mutable field: between the check and the use, a call could have changed it. Assign to a local first. The same reasoning explains why a bounds check survives in a loop whose limit comes from a function call — the analyser widened, and there was no guard it could read to narrow back.

advanced

The deep structure is a Galois connection between the concrete lattice of sets of states and the abstract lattice, with abstraction α and concretization γ adjoint. Soundness of an abstract operation is then a one-line condition, and the whole edifice — including the guarantee that the widened result is a post-fixed point of the concrete semantics — follows from it. The engineering consequence is that domains compose: you can run a reduced product of intervals and congruences and get facts neither could derive alone, and you can add a trace partitioning that keeps separate abstract states per branch history to buy back path sensitivity where it pays. This is how a tool such as Astrée reaches zero false positives on a specific class of program — not by a cleverer lattice, but by combining several and partitioning where the target code needs it. It also explains the honest limit: the precision is bought against a known program shape, and the same tool on general-purpose code with dynamic dispatch would be unusable.

How much this depends on

Nothing in this domain is true of every compiler. These say how much.

specSoundness of an abstract domain is a proof obligation, not a testing outcome: the requirement is that the abstract transfer function over-approximates the concrete one for every input, which is why the classic presentation uses a Galois connection between the two lattices. Testing can refute it and cannot establish it. This is exactly why tools with formal soundness claims — Astrée, Frama-C EVA, CompCert's analyses — restrict the language they accept rather than trying to cover everything.

typicalThe widening-then-narrowing recipe with a delay of a few iterations before widening kicks in describes mainstream implementations, including GCC's value-range propagation and most interval analysers. It is a heuristic, not a specification: the number of delayed iterations, the widening thresholds (widening "up to the next constant in the program" is a common refinement) and whether narrowing runs at all differ per tool, and two sound analysers can give different answers on the same loop.

implementationWhich domain a given compiler runs, and how far, is version-specific. GCC has had value-range propagation since 4.1 and it has grown steadily more precise; LLVM's equivalent information comes from several places at once (LazyValueInfo, ScalarEvolution, ConstantRange) rather than one pass; MSVC exposes almost none of it. Do not carry a conclusion about which check was eliminated from one compiler to another.

If you were asked this in an interview

Give me the abstract multiplication table for the sign domain, and say where it stops being sound.
Why does an interval analysis need widening, and what does it cost you?
Why does a null check on a local variable narrow the type but a null check on a mutable field often does not?

Connections

DSAdirected-graph dfs topological-sort

Performanceprofiling-basics

Domains that do not exist yet

Programming Languages & Runtime Internals — The runtime checks that remain after a static analysis has removed the ones it could prove redundant
Whatever the abstract interpreter fails to prove becomes a check the runtime executes on every iteration — a bounds check, a null check, a type guard. The cost and the mechanism of those residual checks belong to the runtime; which ones survived and why the analysis could not discharge them is ours.

Runtime gain3

Compile cost4

Debuggability3

Implementation5

Context dependence4

runtimeGain is a middling 3 because the same machinery feeds real optimizations — range information is what removes a bounds check and what enables strength reduction — even though the analysis itself emits nothing. Compile cost and implementation complexity are both high: widening, narrowing and a correct join are individually simple and collectively the part of a static analyser that is hardest to get right, and a subtle unsoundness in one transfer function is invisible until it produces a wrong answer. Context dependence is high because the arithmetic domain depends on whether the language defines overflow.

Try it

dataflow stepper →cfg viewer →