Blurry Interpreters Live in Your Compiler

A type checker is an interpreter with bad eyesight.

That is a compliment.

The ordinary interpreter runs a program over concrete values:

3
"hello"
{ x: 1 }

A type checker runs a related program over abstract values:

number
string
object with field x

It does not know the exact integer. It knows enough to reject "hello" / 2. It does not know the exact object. It knows enough to reject point.z when there is no z. The program has been executed in a smaller semantic universe.

Abstract interpretation is the theory that takes this intuition seriously. Instead of treating type checking, constant propagation, null analysis, interval analysis, taint tracking, liveness, and effect systems as unrelated compiler tricks, it asks a more general question:

What property of all possible executions do we want,
and what abstract universe is precise enough to prove it?

The answer is never free. If the abstract universe is too small, the analyzer is fast and vague. If it is too rich, it may be slow, memory-hungry, or unable to converge. Static analysis is the art of choosing what to forget.

Learn to Think in Lattices

Kildall’s 1973 paper on global program optimization already has the shape of modern dataflow analysis: represent program flow as a graph, attach facts to program points, and iterate until the facts stop changing.¹ The facts live in an ordered space. More precise facts sit below less precise facts. Merges at control-flow joins use a least upper bound.

For a type checker, a tiny lattice might be:

        unknown
       /   |   \
   number string object
       \   |   /
      impossible

For an interval analyzer:

[0, 0] <= [0, 1] <= [0, 10] <= [-inf, inf]

The ordering means “is at least as precise as.” The interval [0, 1] tells a strictly sharper story than [0, 10]. The top interval [-inf, inf] says only “it is a number.” That is still information. It just may not be enough information for the proof you wanted.

Cousot and Cousot’s 1977 abstract-interpretation paper made this a unifying semantic framework: compute properties by approximating program semantics and their fixed points.² A later line of work made the type-system connection explicit. Cousot’s “Types as Abstract Interpretations” starts from a lambda-calculus semantics with runtime errors and derives type systems as abstract semantics approximating a collecting semantics.³

That phrase, “collecting semantics,” is the key. Imagine collecting every reachable runtime state at every program point. That would answer many questions perfectly. It would also be infinite or undecidable for real languages. Abstract interpretation replaces that huge set with a summary.

The summary must be conservative:

every concrete behavior is represented

If the analyzer says “no division by zero,” there must be no hidden execution where the denominator becomes zero. If the analyzer is not sure, it must warn. This is why a sound analyzer can be annoying. It is allowed to cry wolf; it is not allowed to miss the wolf.

Loops Make You Pay the Fixed-Point Bill

Loops are where the metaphor stops being cute and starts earning rent.

Consider:

i = 0
while (i < 10) {
  i = i + 1
}
assert(i <= 10)

A concrete run visits i = 0, 1, 2, ..., 10. An interval analyzer can discover the loop invariant:

i in [0, 10]

but it does not get it in one step. It begins with [0, 0], applies the loop body, joins the new information with the old information, and repeats:

[0, 0]
[0, 1]
[0, 2]
...
[0, 10]

At the fixed point, another pass through the loop does not change the abstract state. The analysis is done.

Now change 10 to 1000000000. The same iteration can take too long. For infinite-height domains, it may never terminate. Abstract interpretation solves this with widening:

[0, 0], [0, 1], [0, 2], ...

is accelerated to:

[0, inf]

The analyzer terminates, but it has forgotten the useful upper bound. Widening is a controlled loss of memory. Threshold widening remembers selected constants like 10, 100, or 1000, so the jump can land on a meaningful invariant instead of the sky.

This is not a toy issue. The Astree analyzer, built for proving absence of runtime errors in safety-critical C, is based on abstract interpretation and combines intervals with thresholds, loop unrolling, trace partitioning, and domain-specific abstractions.⁴ Its public project page describes the same bargain: a sound analyzer must signal all possible errors, may report false alarms, and gains practical precision by composing abstract domains and widening/narrowing strategies.⁵

The beautiful engineering lesson is that precision is not one knob. It is a portfolio.

A Blurry Interpreter You Can Poke

The lab below runs four little programs without running them concretely. It interprets them over one of three abstract universes:

type, where every number is just number;
sign, where numbers become negative, zero, positive, or mixtures;
interval, where numbers become lower and upper bounds.

It also lets you choose a loop strategy. Plain widening terminates quickly but may forget a bound. Threshold widening remembers selected constants from the program. No widening is precise on small loops and useless on large ones unless the iteration budget is big enough.

Program Abstract domain Loop strategy Iteration budget

proved possible alarm real counterexample possible current abstraction loop upper bound

The analyzer is sound for this toy language: if it proves an assertion, all concrete executions represented by the input intervals satisfy it. A warning means the abstraction cannot justify the claim; it may be a real bug or a false alarm caused by lost precision.

Use the default Guarded division program. With the interval domain, the analyzer knows x in [1, 12], so 10 / x cannot divide by zero and y <= 10 is proved. Switch to type: everything numeric becomes number, zero comes back into view, and the analyzer must warn. Switch to sign: division by zero is gone, but the y <= 10 bound is too fine for a sign domain.

Now select Widening staircase. With no widening, the upper bound climbs one step per iteration and the analyzer fails to reach a fixed point within a small budget. With plain widening, it reaches a fixed point quickly but forgets the upper bound. With threshold widening, it remembers the loop constant and proves the final assertion.

Finally try Lost correlation. The program copies x into y and asserts y - x == 0. The interval analyzer knows:

x in [0, 20]
y in [0, 20]

but it does not know they are the same value. It computes:

y - x in [-20, 20]

and warns. A relational domain could prove it. This is the core experience of static-analysis engineering: when the warning is spurious, do not merely silence the warning. Ask what relation the abstraction forgot.

The Proof Ledger I Want

Most teams experience static analysis as a list of warnings. That hides the interesting object: a proof economy.

Every warning is a failed proof attempt. The right next question is not only “is this warning true?” but:

What fact would have made the proof go through,
and is that fact local, relational, temporal, probabilistic, or domain-specific?

For production code, this suggests a different interface. A static analyzer should expose a precision ledger:

which abstraction proved each claim;
where widening lost a bound;
where a merge lost a branch condition;
where a non-relational domain lost equality or ordering;
which user annotation or domain extension would remove the alarm;
how much analysis cost that extra precision would add.

That would make static analysis feel less like scolding and more like debugging the proof. It would also make type checking feel less separate from other program analyses. A type checker is one useful abstraction. It is not the end of the ladder.

The most valuable analyzers will not be the ones with the loudest warning list. They will be the ones that can explain, with engineering honesty, exactly what they forgot.

Learn to Think in Lattices

Loops Make You Pay the Fixed-Point Bill

A Blurry Interpreter You Can Poke

The Proof Ledger I Want

Further Reading

Related notes