Understanding Abstract Interpretation
Before building abstract interpreters in OCaml, let's develop intuition for why we abstract concrete values, how different domains trade precision for efficiency, and the mathematical foundations (lattices, Galois connections, widening) that make it all sound.
Why Abstract Interpretation?
Testing runs your program on some inputs. Abstract interpretation analyzes all possible inputs at once — without ever running the code. It trades precision for coverage: instead of tracking exact values, it tracks properties of values (sign, range, constness).
Can you spot the bug? This code compiles fine and might pass some tests:
a = 10 b = a - a // b is always 0 c = 10 / b // CRASH: division by zero!
Concrete Execution
Runs the program on one input at a time. Fast, but misses bugs on untested paths.
Testing
Runs many inputs. Better coverage, but still finite — can't guarantee absence of bugs.
Abstract Interpretation
Covers ALL inputs at once. May report false positives, but never misses a real bug (soundness).
The Sign Domain
The simplest useful abstract domain: every integer is either negative, zero, or positive. Add Bot (unreachable) and Top (unknown sign) to form a complete lattice.
Click two elements above
Abstract Addition
| a | b | a + b |
|---|---|---|
| Pos | Pos | Pos |
| Pos | Zero | Pos |
| Pos | Neg | Top |
| Zero | Zero | Zero |
| Zero | Neg | Neg |
| Neg | Neg | Neg |
Abstract Multiplication
| a | b | a * b |
|---|---|---|
| Pos | Pos | Pos |
| Pos | Neg | Neg |
| Pos | Zero | Zero |
| Neg | Neg | Pos |
| Neg | Zero | Zero |
| Zero | Zero | Zero |
Loss of Precision
Notice: Pos + Neg = Top. We don't know if 5 + (-3) is positive or negative without the actual values. This is the fundamental trade-off: we gain coverage of all inputs but lose some precision. Also: x * x is always non-negative, but sign analysis says Top * Top = Top — it can't track correlations.
Constant Propagation
A flat lattice where each concrete constant gets its own element: Bot < Const(n) < Top for every integer n. Perfect when variables hold known constants — but any merge of different constants collapses to Top.
x = 5 y = x + 1 z = x + y
Literal 5 maps to Const(5).
Abstract Environment
Interval Domain & Widening
The interval domain tracks ranges [lo, hi]. It's more precise than sign or constant at merge points — but has infinite height. Without a special operator called widening, loop analysis can diverge forever.
Initial: i = 0
How Widening Works
Widening (∇) is an operator that forces convergence. When the upper bound of an interval increases between iterations, widening jumps it to +∞. When the lower bound decreases, it jumps to -∞. This guarantees the chain stabilizes in finite steps — at the cost of some over-approximation.
Galois Connections
A Galois connection is the formal bridge between concrete (sets of actual values) and abstract (domain elements) worlds. Two functions — alpha (α) and gamma (γ) — form this bridge.
Concrete World Abstract World
(sets of integers) (domain elements)
α
┌─────────────┐ ──────→ ┌──────────────┐
│ {5, 10} │ │ Pos │
│ {-1, 0, 1} │ │ Top │
│ {0} │ │ Zero │
└─────────────┘ ←────── └──────────────┘
γ
Key Property (adjunction):
α(S) ⊑ a ⟺ S ⊆ γ(a)
"Abstracting then checking ⊑ is the same
as checking ⊆ then concretizing"α : Concrete → Abstract
Click a concrete set to see its abstraction
γ : Abstract → Concrete
Click an abstract value to see its concretization
Why Does This Matter?
The Galois connection guarantees soundness: if the abstract analysis says a property holds, it truly holds for all concrete executions. The key property is: α(S) ⊑ a ⇔ S ⊆ γ(a). This means abstracting and then checking the ordering is equivalent to checking set inclusion in the concrete world. Your abstract interpreter is sound precisely because its transfer functions respect this connection.
Ready to Build Your Own?
You now understand sign domains, constant propagation, interval analysis with widening, and the Galois connection that ties abstract and concrete worlds together. Time to implement these concepts in OCaml.