Lesson 19.5 — Unification-based points-to analysis: Steensgaard and Das's one-level flow¶

Techniques: Steensgaard's analysis (unification with union-find, almost-linear time, the precision ordering Andersen ⊆ Steensgaard); Das's one-level flow (inclusion at the top level of each assignment, unification below) · Pebble implements: Steensgaard in the comparison lab (computePointsTo(M, PointsToAlgorithm::Steensgaard), labs/ch19-points-to/SPEC.md R4); Das's analysis is theory + drill, and a ★ extension of the lab · Prerequisites: Lesson 19.4 (the pointer language and its constraints); union-find (Ch 17, Lesson 17.8 uses it for e-classes) · Time: 5–6 hours

1. Problem and motivation¶

Andersen's analysis is cubic in the worst case and, even with cycle detection, needs minutes on programs with millions of lines. Steensgaard asked what precision can be kept if the analysis must be almost linear [Ste96]. His answer: replace every inclusion "\(\mathrm{pts}(p) \supseteq \mathrm{pts}(q)\)" by an equality — put the targets of \(p\) and \(q\) into one equivalence class — and represent classes with union-find. Each statement is processed once, in any order.

Steensgaard's analysis¶

On the running example (Lesson 19.4 §1), statement 5 (*r = s, with r pointing to p) unifies what p points to (a) with what s points to (b); statement 8 (q = u) then brings in c. After that, everything that points into {a, b, c} points to all three: Steensgaard gives \(\mathrm{pts}(u) = \{a, b, c\}\) where Andersen gives \(\{c\}\). The loss comes from direction: q = u should only let u's target flow into q, not q's targets into u.

Das's one-level flow¶

Das observed that most of that loss happens at the top level: in C, pointer assignments are mostly between variables holding addresses, and it is their direction that matters; the pointers stored inside the pointed-to objects are much less often confused [Das00]. One-level flow keeps inclusion (a directed flow edge) for the top level of every assignment and unifies everything below. It recovers most of Andersen's precision on real C programs at nearly Steensgaard's cost [Das00]. On the running example it gives \(\mathrm{pts}(u) = \{c\}\) like Andersen, but keeps Steensgaard's answer for the objects' contents.

2. Definitions and algorithms¶

Steensgaard's analysis¶

Definition 19.5.1 (Union-find)

A union-find structure maintains a partition of a set of cells into classes, each named by a representative. \(\mathrm{find}(x)\) returns the representative of \(x\)'s class; \(\mathrm{union}(x, y)\) merges two classes. With union by rank (attach the shallower tree under the deeper one) and path compression (make every node on a \(\mathrm{find}\) path point directly to the root), \(m\) operations on \(n\) cells take \(O(m \, \alpha(m, n))\) time, where \(\alpha\) is the inverse Ackermann function (\(\alpha \le 4\) for every practical input) [Tar75].

Definition 19.5.2 (Unification-based solution)

Every variable \(v\) is a cell (its location). A unification solution is a union-find partition of cells (variables plus fresh cells \(\tau_1, \tau_2, \dots\)) with a partial function \(\mathrm{ptr}\) from classes to classes — "every location in class \(C\) holds a pointer into \(\mathrm{ptr}(C)\)" — such that for every statement:

\[ \begin{aligned} p = \&a &:\ \ \mathrm{find}(a) = \mathrm{ptr}(p) \\ p = q &:\ \ \mathrm{ptr}(p) = \mathrm{ptr}(q) \\ p = {*}q &:\ \ \mathrm{ptr}(p) = \mathrm{ptr}(\mathrm{ptr}(q)) \\ {*}p = q &:\ \ \mathrm{ptr}(\mathrm{ptr}(p)) = \mathrm{ptr}(q) \end{aligned} \]

(every \(\mathrm{ptr}\) on the right exists). Its points-to sets are \(\mathrm{pts}_S(v) = \{ o \in \mathit{Obj} : \mathrm{find}(o) = \mathrm{ptr}(\mathrm{find}(v)) \}\).

Algorithm 19.5.3 (Steensgaard's analysis)

Input: a pointer program (Definition 19.4.1).
Output: \(\mathrm{pts}_S(v)\) for every variable.
Precondition: none.
Postcondition: the result satisfies Definition 19.5.2 and is independent of the statement order (Theorem 19.5.8); \(\mathrm{pts}_S \supseteq \mathrm{pts}^*\) (Corollary 19.5.7).
Invariant: after processing statements \(1..i\), the partition with \(\mathrm{ptr}\) satisfies Definition 19.5.2's equations for statements \(1..i\); every class has at most one \(\mathrm{ptr}\) target; two classes are merged only if every unification solution of statements \(1..i\) merges them.

function Steensgaard(program):
    for each variable v: make a cell v
    for each statement, in any order:
        case p = &a:   Join(Pointee(p), a)
        case p = q:    Join(Pointee(p), Pointee(q))
        case p = *q:   Join(Pointee(p), Pointee(Pointee(q)))
        case *p = q:   Join(Pointee(Pointee(p)), Pointee(q))
    return { v ↦ { o ∈ Obj : find(o) = find(ptr[find(v)]) } }   # {} if ptr undefined

function Pointee(x):            # the class x's class points to, created if missing
    r ← find(x)
    if ptr[r] is undefined: ptr[r] ← new cell τk
    return find(ptr[r])

function Join(x, y):            # unify two classes, then (recursively) their pointees
    x, y ← find(x), find(y)
    if x = y: return
    px, py ← ptr[x], ptr[y]
    z ← union(x, y)
    if px and py are both defined: ptr[z] ← px; Join(px, py)
    else: ptr[z] ← whichever of px, py is defined (or undefined)

The lab's LLVM version adds two things from Steensgaard's paper: a class that contains functions carries a signature (return and parameter cells: Steensgaard's λ types), unified at every indirect call; and null stores are skipped rather than unified with one shared "null" cell (which would merge everything that is ever null).

Das's one-level flow¶

Definition 19.5.4 (One-level flow graph)

Each variable \(v\) has a value node \(\mathrm{val}(v)\): what \(v\) holds. Value nodes are union-find classes; each class \(n\) has a set \(\mathrm{base}(n) \subseteq \mathit{Obj}\) of objects whose address it holds directly, a set of incoming flow edges, and a dereference node \(D(n)\) (created on demand): the class of what the locations \(n\) points to hold. The invariants: \(D\) is constant on each class, and every flow edge \(a \to b\) has \(D(a) = D(b)\) — flow is directional at this level and unified one level below. The result is \(\mathrm{pts}_D(v) = \bigcup \{ \mathrm{base}(n) : n \to^{*} \mathrm{val}(v) \}\) over flow edges.

Algorithm 19.5.5 (Das's one-level flow)

Input: a pointer program.
Output: \(\mathrm{pts}_D(v)\) for every variable.
Precondition: none.
Postcondition: \(\mathrm{pts}^* \subseteq \mathrm{pts}_D \subseteq \mathrm{pts}_S\) (Theorem 19.5.9).
Invariant: Definition 19.5.4's invariants hold after every statement; for every processed statement the corresponding inclusion holds for \(\mathrm{pts}_D\) computed from the current graph.

function Das(program):
    for each statement:
        case p = &a:   base[val(p)] ∪= {a};           Unify(Deref(val(p)), val(a))
        case p = q:    Flow(val(q), val(p))
        case p = *q:   Flow(Deref(val(q)), val(p))
        case *p = q:   Flow(val(q), Deref(val(p)))
    return { v ↦ ⋃ base[n] over the classes n that reach find(val(v)) along flow edges }

function Flow(a, b):     add the edge find(a) → find(b);  Unify(Deref(a), Deref(b))
function Deref(n):       if D[find(n)] undefined: D[find(n)] ← new node;  return find(D[find(n)])
function Unify(x, y):    x, y ← find(x), find(y);  if x = y: return
                         z ← union(x, y);  base[z] ← base[x] ∪ base[y];  in-edges[z] ← in-edges[x] ∪ in-edges[y]
                         if D[x], D[y] both defined: D[z] ← D[x]; Unify(D[x], D[y]) else D[z] ← the defined one

3. Worked example¶

Steensgaard's analysis¶

The running example, one row per statement (./course drill points-to-steensgaard's oracle; classes are named by their first member, fresh cells are \(\tau_k\); "ptr" lists \(C \to \mathrm{ptr}(C)\)):

step	statement	joins	classes after (≥ 2 members)	ptr after
1	`p = &a`	τ1 ∪ a	{a,τ1}	p→a
2	`q = &b`	τ2 ∪ b	{a,τ1}	p→a, q→b
3	`r = &p`	τ3 ∪ p	{p,τ3} {a,τ1} {b,τ2}	p→a, q→b, r→p
4	`s = q`	τ4 ∪ b	{p,τ3} {a,τ1} {b,τ2,τ4}	p→a, q→b, r→p, s→b
5	`*r = s`	a ∪ b	{p,τ3}	p→a, q→a, r→p, s→a
6	`t = *r`	τ5 ∪ a	{p,τ3}	… t→a
7	`u = &c`	τ6 ∪ c	…	… u→c
8	`q = u`	a ∪ c	{p,τ3}	… u→a
9	`b = t`	τ7 ∪ a	{p,τ3}	a→a, p→a, q→a, r→p, s→a, t→a, u→a
10	`q = b`	—	unchanged	unchanged

Step 1: Pointee(p) creates \(\tau_1\); joining it with a makes p's class point to a's class.
Step 5: Pointee(Pointee(r)) is a's class (r → p → a) and Pointee(s) is b's class: they are unified. Neither had a ptr, so the join stops.
Step 8: u's pointee c is unified into the same class: now u points to {a, b, c} — the precision loss.
Step 9: b (in the big class) must point where t points, the big class itself: \(\mathrm{ptr}(\{a,b,c\}) = \{a,b,c\}\).

Result: \(\mathrm{pts}_S(r) = \{p\}\) and every other variable, including a, c and u, points to \(\{a, b, c\}\). 28 of 36 variable pairs may alias (Andersen: 15). Three variables are strictly worse than Andersen: a, c (Andersen: \(\emptyset\)) and u (Andersen: \(\{c\}\)).

Try it yourself: ./course drill points-to-steensgaard --seed 2 --difficulty hard --solution.

Das's one-level flow¶

Algorithm 19.5.5 on the running example (\(n_k\) are fresh dereference nodes; the oracle das() in tools/course/lib/pointsto.py):

step	statement	flow edge	unifications (one level below)
1	`p = &a`	— (base of val(p) ∋ a)	D(val(p)) = n1 ∪ val(a)
2	`q = &b`	— (base of val(q) ∋ b)	n2 ∪ val(b)
3	`r = &p`	— (base of val(r) ∋ p)	n3 ∪ val(p)
4	`s = q`	val(q) → val(s)	D(val(q)) = val(b) ∪ n4
5	`*r = s`	val(s) → D(val(r)) = val(p)	D(val(s)) = val(b) ∪ D(val(p)) = val(a)
6	`t = *r`	D(val(r)) = val(p) → val(t)	val(a) ∪ n5
7	`u = &c`	— (base of val(u) ∋ c)	n6 ∪ val(c)
8	`q = u`	val(u) → val(q)	D(val(u)) = val(c) ∪ D(val(q)) = val(a)
9	`b = t`	val(t) → val(b) (= the class of val(a))	val(a)'s class ∪ n7
10	`q = b`	val(a)'s class → val(q)	—

Flow reaches val(u) from nothing, so \(\mathrm{pts}_D(u) = \mathrm{base}(\mathrm{val}(u)) = \{c\}\), as in Andersen. The class \(\{\mathrm{val}(a), \mathrm{val}(b), \mathrm{val}(c)\}\) is reached from val(t), val(p), val(s), val(q) and val(u), whose bases are \(\{a\}\), \(\{b\}\) and \(\{c\}\), so \(\mathrm{pts}_D(a) = \mathrm{pts}_D(b) = \mathrm{pts}_D(c) = \{a, b, c\}\), as in Steensgaard. In short: Andersen ⊊ Das ⊊ Steensgaard, with Das equal to Andersen on the top-level variable u and equal to Steensgaard on the contents a, c.

4. Invariants and correctness¶

Steensgaard's analysis¶

Theorem 19.5.6 (A unification solution is an inclusion solution)

If a partition with \(\mathrm{ptr}\) satisfies Definition 19.5.2, then \(\mathrm{pts}_S\) satisfies every inclusion constraint of Definition 19.4.1.

Proof

Write \([x] = \mathrm{find}(x)\) and \(\mathrm{Obj}(C) = \{o \in \mathit{Obj} : [o] = C\}\), so \(\mathrm{pts}_S(v) = \mathrm{Obj}(\mathrm{ptr}([v]))\). (1) p = &a: \([a] = \mathrm{ptr}([p])\), so \(a \in \mathrm{Obj}(\mathrm{ptr}([p])) = \mathrm{pts}_S(p)\). (2) p = q: \(\mathrm{ptr}([p]) = \mathrm{ptr}([q])\), so the sets are equal. (3) p = *q: let \(o \in \mathrm{pts}_S(q)\), i.e. \([o] = \mathrm{ptr}([q])\). Then \(\mathrm{pts}_S(o) = \mathrm{Obj}(\mathrm{ptr}([o])) = \mathrm{Obj}(\mathrm{ptr}(\mathrm{ptr}([q]))) = \mathrm{Obj}(\mathrm{ptr}([p])) = \mathrm{pts}_S(p)\) (if \(\mathrm{ptr}([o])\) is undefined, \(\mathrm{pts}_S(o) = \emptyset\)). (4) *p = q: for \(o \in \mathrm{pts}_S(p)\), \([o] = \mathrm{ptr}([p])\) and \(\mathrm{pts}_S(o) = \mathrm{Obj}(\mathrm{ptr}(\mathrm{ptr}([p]))) = \mathrm{Obj}(\mathrm{ptr}([q])) = \mathrm{pts}_S(q)\). Each inclusion holds, even as an equality.

Corollary 19.5.7 (Precision ordering: Andersen ⊆ Steensgaard)

\(\mathrm{pts}^*(v) \subseteq \mathrm{pts}_S(v)\) for every \(v\). Hence every pair Andersen's analysis answers MayAlias, Steensgaard's answers MayAlias; Steensgaard's analysis is sound.

Proof

By Theorem 19.5.6, \(\mathrm{pts}_S\) is a solution of the inclusion constraints, and \(\mathrm{pts}^*\) is the least one (Theorem 19.4.11). If \(\mathrm{pts}^*(p) \cap \mathrm{pts}^*(q) \neq \emptyset\), the larger sets intersect too. Soundness follows from Theorem 19.4.12, which holds for every solution.

Theorem 19.5.8 (Termination, almost-linear time and order independence)

Algorithm 19.5.3 terminates after \(O(m)\) calls of Join/Pointee plus at most one recursive Join per union, and its result — the partition and \(\mathrm{ptr}\) — is the finest unification solution; in particular it does not depend on the order of the statements.

Proof

Termination and count. Each statement makes at most four Pointee calls (creating at most four cells) and one Join. A Join either returns at once or performs a union, which decreases the number of classes by one, and then recurses at most once. With \(c \le \lvert V \rvert + 4m\) cells there are at most \(c - 1\) unions, so the total number of Join calls is \(O(m + c) = O(m + \lvert V \rvert)\).

Finest solution. Invariant: every merge the algorithm makes is forced, i.e. performed by every unification solution of the statements processed so far. A statement's equation forces its two sides into one class, and when two classes merge, Definition 19.5.2's requirement that a class has one \(\mathrm{ptr}\) target forces their targets to merge — the recursive Join. So the result is below every solution in the refinement order. It is itself a solution: after the last statement every equation holds (the invariant of Algorithm 19.5.3), because later merges only coarsen classes and find respects them. The finest solution is unique (the meet of all solutions in the partition lattice is a solution, by the same forcing argument), hence independent of the processing order. tools/course/tests/test_ch19.py checks order independence on 400 shuffled programs.

Unification is symmetric

q = u in Steensgaard does not mean "u's targets flow into q"; it means "q and u point into the same class". That is why u ends up pointing to a and b, which only ever flowed into q. Any assignment merges both sides' futures; Das's analysis restores direction at the top level.

Das's one-level flow¶

Theorem 19.5.9 (Das's analysis is sound and between Andersen and Steensgaard)

For the result of Algorithm 19.5.5, \(\mathrm{pts}^* \subseteq \mathrm{pts}_D \subseteq \mathrm{pts}_S\) pointwise.

Proof

Lower bound: \(\mathrm{pts}_D\) is an inclusion solution. Write \(n \leadsto m\) for reachability along flow edges between classes; \(\mathrm{pts}_D(v) = \bigcup_{n \leadsto [\mathrm{val}(v)]} \mathrm{base}(n)\). Unification only merges classes and unions their bases and in-edges, so reachability and bases only grow, and every inclusion established earlier stays true. (1) p = &a: \(a \in \mathrm{base}([\mathrm{val}(p)])\). (2) p = q: the edge \(\mathrm{val}(q) \to \mathrm{val}(p)\) makes everything reaching \(\mathrm{val}(q)\) reach \(\mathrm{val}(p)\). (3) p = *q: let \(o \in \mathrm{pts}_D(q)\), so \(o \in \mathrm{base}(n)\) with \(n \leadsto [\mathrm{val}(q)]\). When \(o\) entered \(\mathrm{base}(n')\) for the class \(n'\) that became part of \(n\), the address-of rule unified \(D(n')\) with \(\mathrm{val}(o)\); flow edges keep \(D\) equal along the path to \(\mathrm{val}(q)\) (Definition 19.5.4), so \([\mathrm{val}(o)] = D([\mathrm{val}(q)])\). The load added the edge \(D(\mathrm{val}(q)) \to \mathrm{val}(p)\), so every class reaching \([\mathrm{val}(o)]\) reaches \(\mathrm{val}(p)\): \(\mathrm{pts}_D(o) \subseteq \mathrm{pts}_D(p)\). (4) *p = q: symmetrically, for \(o \in \mathrm{pts}_D(p)\), \([\mathrm{val}(o)] = D([\mathrm{val}(p)])\), and the store's edge \(\mathrm{val}(q) \to D(\mathrm{val}(p))\) gives \(\mathrm{pts}_D(q) \subseteq \mathrm{pts}_D(o)\). So \(\mathrm{pts}_D\) is a solution and contains the least one.

Upper bound. Map every Das class to a Steensgaard class: \(h(\mathrm{val}(v)) = \mathrm{ptr}([v])\) and \(h(D(n)) = \mathrm{ptr}(h(n))\). Each Das operation is mirrored by an equation of Definition 19.5.2 that Steensgaard's solution satisfies: an address-of puts \(a\) in \(\mathrm{base}(\mathrm{val}(p))\) where Steensgaard has \([a] = \mathrm{ptr}([p]) = h(\mathrm{val}(p))\); a flow edge \(x \to y\) from p = q (resp. a load or store) joins two nodes that Steensgaard's corresponding equation makes equal, \(h(x) = h(y)\), and the one-level-below unification is the \(\mathrm{ptr}\) of that equality. By induction over the statements, \(h\) is constant on Das classes and along flow edges, and \(\mathrm{base}(n) \subseteq \mathrm{Obj}(h(n))\). Then every class reaching \(\mathrm{val}(v)\) has \(h = \mathrm{ptr}([v])\), so \(\mathrm{pts}_D(v) \subseteq \mathrm{Obj}(\mathrm{ptr}([v])) = \mathrm{pts}_S(v)\). (The course oracle checks both inclusions on 600 random programs.)

5. Complexity¶

Let \(n = \lvert V \rvert\) variables and \(m\) statements.

Technique	Time (worst)	Time (typical)	Space
Steensgaard	\(O((n + m)\,\alpha(n + m, n))\) union-find work (Theorem 19.5.8 with Definition 19.5.1) plus \(O(n \cdot k)\) to list the sets	linear; the lab's 4000-variable stress input takes 0.3 s including writing out \(\approx 2300\)-element sets	\(O(n + m)\) cells
Das's one-level flow	unification as Steensgaard, plus up to \(m\) flow edges; listing \(\mathrm{pts}_D\) for all variables by reverse reachability costs \(O(n (n + m))\)	near-linear: Das reports running times close to Steensgaard's on the large C programs he measured [Das00]	\(O(n + m)\) plus the flow edges

Justification. Steensgaard: Theorem 19.5.8 bounds the number of Join/Pointee calls by \(O(n + m)\), each doing \(O(1)\) union-find operations, and Tarjan's theorem bounds a sequence of such operations by the inverse Ackermann function [Tar75]. Das: the same unification cost; each statement adds at most one flow edge; the final sets require a graph search per variable. Pathological family for Steensgaard's precision: \(x_i = \&o_i\) for \(i = 1..n\) and one statement \(y = x_i\) for every \(i\) — a single y that receives every pointer. Steensgaard unifies all \(o_i\) into one class, so every \(x_i\) points to all \(n\) objects: \(\Theta(n^2)\) spurious alias pairs, where Andersen (and Das, since these are top-level assignments) keep \(\mathrm{pts}(x_i) = \{o_i\}\).

Steensgaard's analysis¶

Conditional joins [Ste96]: a variable that holds no pointer does not force its pointee to merge until it receives one ("cjoin"); trade-off: more bookkeeping, fewer merges in programs that mix integers and pointers in one location.
Field-sensitive unification (structure types in the unification types, one cell per field; Lesson 19.6 discusses the choice): trade-off: more cells, much better for C structs.
Context-sensitive unification (CFL-based formulations such as LLVM's former CFLSteensAA, "roughly one level context-sensitive Steensgaard" per its own comment, §7): trade-off: summaries per function and more work per query.

Das's one-level flow¶

Multi-level flow (flow edges also below the top level, up to a depth \(k\)): interpolates towards Andersen; trade-off: cost grows with \(k\).
Golf (CIL's golf.ml, a context-sensitive one-level flow): matches call and return edges by CFL reachability (its "matched" and "unmatched" bounds); trade-off: more complex constraints and solving.

7. In real compilers¶

Steensgaard's analysis¶

Where Steensgaard lives

CIL src/ext/pta/steensgaard.ml — unify_int, unify_ref, unify_fun (λ types) and unify_label over a union-find module Uref [CIL-PTA] (CIL 1.7.3). SVF svf/lib/WPA/Steensgaard.cpp [SX16]. LLVM shipped CFL-based Steensgaard and Andersen analyses (CFLSteensAliasAnalysis.cpp, CFLAndersAliasAnalysis.cpp) until LLVM 15; they were never enabled by default and were removed, so opt 23 rejects -aa-pipeline=cfl-steens-aa. Pebble: the lab's Steensgaard algorithm.

Steensgaard in CIL and in LLVM's past

Reproduce (curl 8.5.0, opt 23.1.2; sources at tags cil-1.7.3 and llvmorg-15.0.0):

curl -sL https://raw.githubusercontent.com/cil-project/cil/cil-1.7.3/src/ext/pta/steensgaard.ml -o steensgaard.ml
grep -nE '^and unify_(int|ref|fun|label)|U\.unify' steensgaard.ml
echo "== LLVM had a Steensgaard-style AA until release 15:"
curl -sL https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-15.0.0/llvm/lib/Analysis/CFLSteensAliasAnalysis.cpp \
  | grep -nE "one level context-sensitive|Steensgaard's algorithm"
opt -aa-pipeline=cfl-steens-aa -passes=aa-eval -disable-output /dev/null

Output (complete):

834:and unify_int (t,t' : tau * tau) : unit = 
840:    U.unify combine (t,t');
885:and unify_ref (ri,ri' : rinfo * rinfo) : unit =
892:and unify_fun (li,li' : finfo * finfo) : unit = 
907:and unify_label (l,l' : label * label) : unit =
936:    U.unify combine_label (l,l')
1273:      List.iter (fun x -> U.unify combine_lbounds 
== LLVM had a Steensgaard-style AA until release 15:
17:// analysis is roughly the same as that of an one level context-sensitive
18:// Steensgaard's algorithm.
opt: unknown alias analysis name 'cfl-steens-aa'

What to notice: CIL's analysis is a set of mutually recursive unify_* functions (types, references, functions, labels) ending in U.unify — Algorithm 19.5.3's Join recursing into pointees. LLVM 15's CFL analysis described itself as roughly one-level context-sensitive Steensgaard; LLVM 23 no longer knows the name.

Find where LLVM did it. At llvmorg-15.0.0, llvm/lib/Analysis/CFLSteensAliasAnalysis.cpp states the precision of its analysis in its header comment. What does it compare itself to? (Quiz llvm-where-cfl-steens.)

Das's one-level flow¶

Where one-level flow lives

CIL src/ext/pta/olf.ml — Leq constraints (the directed top-level flow) solved by leq_int, and Unification constraints by unify_int; add_toplev_constraint (Leq (actual, formal)) at calls [CIL-PTA]. Das implemented the analysis at Microsoft Research for large C code bases [Das00]. No mainstream optimizing compiler uses it today.

One-level flow in CIL: inclusion at the top level, unification below

Reproduce (curl 8.5.0; source at tag cil-1.7.3):

curl -sL https://raw.githubusercontent.com/cil-project/cil/cil-1.7.3/src/ext/pta/olf.ml -o olf.ml
grep -nE '^  \| (Unification|Leq) of|Leq \(t, t.\) ->|leq_int \(t, t.\)$|^and leq_int|^and unify_int|add_toplev_constraint \(Leq' olf.ml

Output (complete):

144:  | Leq of tau * tau
498:    | Leq (t, t') ->
716:and leq_int (t, t') : unit =
797:            | Leq (t, t') ->
799:                else leq_int (t, t')
846:        add_toplev_constraint (Leq (t, t''));
847:        add_toplev_constraint (Leq (t', t''));
855:    List.iter (function t -> add_toplev_constraint (Leq (t, t'))) tl;
868:  add_toplev_constraint (Leq (t, lv.contents))
871:  add_toplev_constraint (Leq (t, lv.contents))
930:         add_toplev_constraint (Leq (actual, formal)))
974:  add_toplev_constraint (Leq (t', t))

What to notice: two constraint kinds, Leq (inclusion) and Unification; top-level assignments (lines 846–871: assignment, contents; 930: actual to formal at calls) are Leq constraints solved by leq_int — Definition 19.5.4's flow edges — while unify_int handles the levels below.

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Steensgaard's analysis	Coarsest of the three: ⊇ Andersen (Corollary 19.5.7); 51 vs 45 MayAlias pairs of 224 on the lab corpus, 28 vs 15 of 36 on the running example	\(O((n + m)\,\alpha)\) · 0.3 s on the 4000-variable stress input (Andersen: 75 s, 1.8 s with cycles)	One class per pointee: a storage-shape graph; sets are shared, so large	Low (union-find, ~150 lines)	Very large code bases, first pass of demand-driven or staged analyses, CIL, historic LLVM CFL-AA
Das's one-level flow	Between the two (Theorem 19.5.9); equal to Andersen on the running example's top-level `u`	near-linear · close to Steensgaard [Das00]	Flow graph + classes	Medium (flow edges plus unification)	Large C programs where Steensgaard is too coarse (Das's MSR tools), CIL's `olf`

Choose Steensgaard when the program is huge and any sound answer is better than none, or as a pre-pass that bounds the work of a more precise analysis. Choose Das's one-level flow when you need most of Andersen's precision on C-like code at unification cost. Choose Andersen (Lesson 19.4) when precision matters more than time.

9. Assessment¶

Quiz: steens-running-pts, steens-join-step5, llvm-where-cfl-steens (tag steensgaard); das-u, das-between (tag das).
Drill: ./course drill points-to-steensgaard (easy: sets; medium: + classes; hard: + the variables Steensgaard makes worse than Andersen). Das's analysis is traced in this lesson; the drill's hard level compares Steensgaard with Andersen, and the oracle das() in tools/course/lib/pointsto.py computes Das's sets for your own programs.
Flashcards: tags steensgaard, das.
Exercises: lab milestone 4 (Steensgaard) and ★ stretch goal "Das's one-level flow" in labs/ch19-points-to/SPEC.md.

References¶

See the chapter references.

Lesson 19.5 — Unification-based points-to analysis: Steensgaard and Das's one-level flow¶

1. Problem and motivation¶

Steensgaard's analysis¶

Das's one-level flow¶

2. Definitions and algorithms¶

Steensgaard's analysis¶

Das's one-level flow¶

3. Worked example¶

Steensgaard's analysis¶

Das's one-level flow¶

4. Invariants and correctness¶

Steensgaard's analysis¶

Das's one-level flow¶

5. Complexity¶

6. Variants and refinements¶

Steensgaard's analysis¶

Das's one-level flow¶

7. In real compilers¶

Steensgaard's analysis¶

Das's one-level flow¶

8. Comparison¶

9. Assessment¶

References¶