Lesson 20.5 — Interprocedural analysis: IPSCCP, summaries vs contexts, IFDS and IDE¶

Techniques: interprocedural constant propagation with jump functions (Callahan, Cooper, Kennedy & Torczon 1986) and LLVM's interprocedural SCCP, IPSCCP (Wegman–Zadeck's SCCP over the call graph); summary-based (functional) vs context-sensitive (call-string) analysis (Sharir & Pnueli 1981); IFDS (Reps, Horwitz & Sagiv 1995) and IDE (Sagiv, Reps & Horwitz 1996) — the exploded supergraph, the tabulation algorithm and its \(O(E D^3)\) bound, micro-functions and jump functions · Pebble implements: nothing in the compiler (LLVM's ipsccp runs in pebblec -O2); the IFDS tabulation is the oracle of the drill ifds-tabulation (tools/course/lib/ipo.py) · Drill: ifds-tabulation · Prerequisites: SCCP (Lesson 17.1); monotone frameworks and MOP/MFP (Ch 14); the IFDS preview (Lesson 14.8); Lesson 20.2 · Time: 7–9 hours

Lesson 14.8 introduced IFDS as "dataflow analysis as graph reachability". This lesson places it in the family of interprocedural analyses and goes deeper: why summaries are exact for distributive problems and call strings are not, how the tabulation algorithm builds summaries on demand, what its bound counts, and how IDE extends it from sets of facts to values. The running example for IFDS is a taint analysis:

proc main():                     proc id(p):
  n1: a = source()                 n7: r = p
  n2: b = 0                        n8: return r
  n3: x = call id(a)
  n4: y = call id(b)
  n5: sink(y)
  n6: return x

a is tainted, b is not; both flow through the same identity function id. The question "is y tainted at the sink n5?" has the answer no — but only an analysis that matches each return of id with the call it came from sees that.

1. Problem and motivation¶

IPSCCP¶

Constant propagation within one function (Lesson 17.1) treats a call as unknown: every argument of the callee is \(\top\) and every result of a call is \(\top\). Callahan, Cooper, Kennedy and Torczon made constant propagation interprocedural by attaching jump functions to call sites (how each actual argument depends on the caller's parameters) and return jump functions to procedures, and solving over the call graph [CCKT86]. LLVM's IPSCCP runs the SCCP solver of Lesson 17.1 on the whole module at once: the lattice value of an argument of an internal function is the join of the values passed at its (executable) call sites, and the value of a call is the join of the callee's returned values, so constants flow into and out of functions and dead branches are found across calls [LLVM-IPSCCP]. It runs early in default<O2>, before inlining, and again (with function specialization, Lesson 20.4) in LTO.

Summary-based vs context-sensitive analysis¶

Sharir and Pnueli gave two exact ways to analyze a program with procedures [SP81]. The call-string approach tags every fact with the stack of pending call sites, so a return goes back to its own call — exact, but the stacks are unbounded with recursion and in practice are cut to length \(k\) (\(k\)-CFA). The functional approach computes, per procedure, a summary: a function from the facts at its entry to the facts at its exit, and applies it at every call — exact for distributive problems, and each procedure is analyzed once. LLVM's function-attrs (Lesson 20.6), GCC's ipa-modref and ThinLTO's module summaries (Lesson 20.9) are summary-based; points-to analyses often choose call strings or object sensitivity (Ch 19). A context-insensitive analysis merges all calls of a procedure and returns to all callers: cheapest, and imprecise along unrealizable paths.

IFDS and IDE¶

Reps, Horwitz and Sagiv showed that for interprocedural, finite, distributive, subset problems — gen/kill problems such as reaching definitions, live variables, taint, possibly-uninitialized variables — the exact meet-over-valid-paths solution is a graph reachability problem in an exploded supergraph with one node per (program point, fact), solvable by a worklist tabulation algorithm that builds procedure summaries on demand in \(O(E D^3)\) time [RHS95]. Sagiv, Reps and Horwitz's IDE generalizes the sets to environments mapping facts to values of a lattice, with micro-functions on the exploded edges — enough for linear constant propagation and typestate [SRH96]. Heros (Soot), WALA and PhASAR (for LLVM IR) are IFDS/IDE solvers; Soufflé-based analyses encode the tabulation in Datalog (§7).

2. Definitions and algorithms¶

Definition 20.5.1 (Supergraph, valid paths)

The supergraph \(G^{\ast}\) has the nodes of all procedures' CFGs; for a call node \(c\) in \(p\) calling \(q\) with return site \(r_c\) (the node after \(c\)), it has a call edge \(c \to s_q\), a return edge \(e_q \to r_c\) (\(s_q\), \(e_q\) are \(q\)'s start and exit nodes) and a call-to-return edge \(c \to r_c\). Label the call edge \((_c\) and the return edge \()_c\). A path is realizable (same-level) if its labels form a balanced string of parentheses, and valid if every \()_c\) is matched by the nearest unmatched \((_c\) (unmatched opens allowed: the path may end inside a call). \(\mathrm{VP}(n)\) is the set of valid paths from \(s_{\mathtt{main}}\) to \(n\).

Definition 20.5.2 (IFDS problem, MVP)

An IFDS problem is \((G^{\ast}, D, M)\): a finite set \(D\) of facts and, for each supergraph edge \(e\), a distributive flow function \(M(e) : \mathcal{P}(D) \to \mathcal{P}(D)\), i.e. \(M(e)(X \cup Y) = M(e)(X) \cup M(e)(Y)\) (hence \(M(e)(X) = M(e)(\emptyset) \cup \bigcup_{d \in X} M(e)(\{d\})\)). For a path \(\pi = e_1 \dots e_m\), \(M(\pi) = M(e_m) \circ \dots \circ M(e_1)\). The meet-over-valid-paths solution is \(\mathrm{MVP}(n) = \bigcup_{\pi \in \mathrm{VP}(n)} M(\pi)(\emptyset)\).

Definition 20.5.3 (Exploded supergraph)

Let \(D_0 = D \cup \{0\}\). A distributive \(f\) is represented by the relation \(R_f = \{(0, 0)\} \cup \{(0, d) \mid d \in f(\emptyset)\} \cup \{(d, d') \mid d' \in f(\{d\}) \setminus f(\emptyset)\}\), so that \(f(X) = \{\, d' \mid \exists d \in X \cup \{0\}.\ (d, d') \in R_f \,\}\). The exploded supergraph \(G^{\sharp}\) has nodes \(N^{\ast} \times D_0\) and an edge \((m, d) \to (n, d')\) for each supergraph edge \(m \to n\) and \((d, d') \in R_{M(m \to n)}\).

Flow functions of the running example

a = source() (node n1): \(R = \{(0,0), (0,a), (b,b), (x,x), (y,y)\}\) — \(a\) is generated from 0 and killed from itself. r = p (n7): \(\{(0,0), (p,p), (p,r)\}\) — \(r\) is killed unless \(p\) holds. Call edge at n3 (x = call id(a)): \(\{(0,0), (a,p)\}\) — actual to formal. Call-to-return at n3: identity except \(x\) (killed: the call assigns it). Return edge at n3: \(\{(0,0), (r,x)\}\) — the returned variable to the target.

Algorithm 20.5.4 (IFDS tabulation, Reps–Horwitz–Sagiv, with the Incoming map)

Input: an IFDS problem; the seed \(\langle s_{\mathtt{main}}, 0 \rangle\).
Output: the set PathEdge; \(\mathrm{facts}(n) = \{\, d \ne 0 \mid \exists \langle s, d_1 \rangle \to \langle n, d \rangle \in \mathrm{PathEdge} \,\}\); the summary edges.
Precondition: every flow function distributive; \(D\) finite.
Postcondition: \(\mathrm{facts}(n) = \mathrm{MVP}(n)\) (Theorem 20.5.6).
Invariant: (I1) every path edge \(\langle s_p, d_1 \rangle \to \langle n, d_2 \rangle\) is witnessed by a same-level realizable path in \(G^{\sharp}\) from \((s_p, d_1)\) to \((n, d_2)\), and \((s_p, d_1)\) is reachable from the seed along a valid path; (I2) every summary edge \(\langle c, d_4 \rangle \to \langle r_c, d_5 \rangle\) is witnessed by a same-level path \((c, d_4) \to (s_q, d_1) \leadsto (e_q, d_2) \to (r_c, d_5)\); (I3) every path edge not yet processed is on the worklist.

function Tabulate():
    PathEdge ← {⟨s_main,0⟩→⟨s_main,0⟩};  W ← [that edge];  Summary ← ∅
    Incoming ← ∅;  EndSum ← ∅                      # (s_q,d) ↦ call sites that entered with d / exits reached
    while W ≠ []:
        ⟨s_p,d1⟩→⟨n,d2⟩ ← pop front W
        if n is a call node c (callee q, return site r):
            for d3 in R_call(c)(d2):                                   # enter q
                Propagate(⟨s_q,d3⟩→⟨s_q,d3⟩)
                if (c, d2) ∉ Incoming[s_q,d3]:                          # first entry of c with d2 → d3
                    Incoming[s_q,d3] ∪= {(c, d2)}
                    for (e_q,d4) in EndSum[s_q,d3]:                     # q already summarized for d3
                        for d5 in R_ret(c)(d4): Summary ∪= {⟨c,d2⟩→⟨r,d5⟩}
            for d3 in R_c2r(c)(d2): Propagate(⟨s_p,d1⟩→⟨r,d3⟩)          # locals survive the call
            for ⟨c,d2⟩→⟨r,d5⟩ in Summary: Propagate(⟨s_p,d1⟩→⟨r,d5⟩)    # apply summaries
        else if n is the exit e_p of p:
            EndSum[s_p,d1] ∪= {(e_p, d2)}
            for (c, d4) in Incoming[s_p,d1]:                             # every caller that entered with d1
                for d5 in R_ret(c)(d2):
                    if ⟨c,d4⟩→⟨r_c,d5⟩ ∉ Summary:
                        Summary ∪= {⟨c,d4⟩→⟨r_c,d5⟩}
                        for ⟨s',d3⟩→⟨c,d4⟩ in PathEdge: Propagate(⟨s',d3⟩→⟨r_c,d5⟩)
        else:
            for (n → m) and d3 in R_{M(n→m)}(d2): Propagate(⟨s_p,d1⟩→⟨m,d3⟩)
    return PathEdge, Summary

function Propagate(e): if e ∉ PathEdge: PathEdge ∪= {e}; append e to W

Definition 20.5.5 (IDE problem, micro-functions, jump functions)

An IDE problem replaces sets by environments \(\mathit{Env} = D \to L\) for a lattice \(L\) of finite height (e.g. constants \(\bot \sqsubset c \sqsubset \top\)), and each flow function by a distributive environment transformer represented by exploded edges \(d \to d'\) labelled with micro-functions \(L \to L\) (e.g. \(\lambda v.\, 2v + 1\) for r = 2*p + 1). A jump function \(\mathrm{jf}(\langle s_p, d \rangle \to \langle n, d' \rangle)\) is the join of the compositions of micro-functions along all same-level paths; IDE's phase I is tabulation over jump functions (composing and joining them instead of adding edges), phase II computes the values \(\mathrm{val}(n, d')\) by applying jump functions to the values at procedure starts, top-down. IFDS is the case \(L = \{\bot \sqsubset \top\}\) with identity micro-functions.

3. Worked example¶

IPSCCP¶

On ipc.c (box in §7): version() returns 3 on every path; limit(level) is called only with 3, so level > 2 folds and it returns 64; buffer_size(3) returns 64 * 3 = 192 at both of its call sites. SCCP's lattice values across functions:

value	first visit	after the call-site joins	final
`buffer_size.level`	⊥	join(3 from `small`, 3 from `large`) = 3	3
`limit.level`	⊥	3 (one call site, argument `level` = 3)	3
`limit` return	⊥	only `ret 64` is executable (`3 > 2`)	64
`version` return	⊥	3	3
`buffer_size` return	⊥	64 × 3	192
`small` return	⊥	192	192
`large` return	⊥	192 + 1	193

The calls remain (they may have side effects in general; here the callee bodies become ret i32 poison, meaning "the return value is never used", and later passes delete the calls).

Summary-based vs context-sensitive analysis¶

On the taint example, three analyses:

analysis	fact at `n5` (before `sink(y)`)	why
context-insensitive (merge all calls of `id`)	{a, x, y}	`id`'s entry facts are joined: \(p\) tainted (from the call at `n3`); its exit returns \(r\) tainted to both return sites, so `y` is tainted — an unrealizable path `n3 → id → n5`
call strings, \(k = 1\)	{a, x}	facts in `id` are tagged `[n3]` or `[n4]`; the `[n4]` context has \(p\) untainted, and a return goes only to its own call's return site
functional (summaries)	{a, x}	`id`'s summary for entry fact \(p\) is \(\{p \mapsto \{p, r\}\}\); applied at `n3` it taints `x` (summary edge \(a \to x\)); at `n4` the entry facts are \(\{0\}\) only, whose summary returns nothing tainted

The IFDS tabulation below is the functional approach, restricted to the (call site, entry fact) pairs that actually occur.

IFDS and IDE¶

Algorithm 20.5.4 on the running example (FIFO worklist; generated by ./course drill ifds-tabulation, whose oracle is ipo.ifds):

step	popped path edge	node	new path edges / summaries
1	⟨n1,0⟩→⟨n1,0⟩	`a = source()`	⟨n1,0⟩→⟨n2,0⟩; ⟨n1,0⟩→⟨n2,a⟩
2	⟨n1,0⟩→⟨n2,0⟩	`b = 0`	⟨n1,0⟩→⟨n3,0⟩
3	⟨n1,0⟩→⟨n2,a⟩	`b = 0`	⟨n1,0⟩→⟨n3,a⟩
4	⟨n1,0⟩→⟨n3,0⟩	`x = call id(a)`	⟨n7,0⟩→⟨n7,0⟩ (enter `id` with 0); ⟨n1,0⟩→⟨n4,0⟩ (call-to-return)
5	⟨n1,0⟩→⟨n3,a⟩	`x = call id(a)`	⟨n7,p⟩→⟨n7,p⟩ (a → p); ⟨n1,0⟩→⟨n4,a⟩
6	⟨n7,0⟩→⟨n7,0⟩	`r = p`	⟨n7,0⟩→⟨n8,0⟩
7	⟨n1,0⟩→⟨n4,0⟩	`y = call id(b)`	⟨n1,0⟩→⟨n5,0⟩ (0 enters `id` again: nothing new)
8	⟨n7,p⟩→⟨n7,p⟩	`r = p`	⟨n7,p⟩→⟨n8,p⟩; ⟨n7,p⟩→⟨n8,r⟩
9	⟨n1,0⟩→⟨n4,a⟩	`y = call id(b)`	⟨n1,0⟩→⟨n5,a⟩ (a is not an argument: only call-to-return)
10	⟨n7,0⟩→⟨n8,0⟩	exit of `id`	summaries ⟨n3,0⟩→⟨n4,0⟩, ⟨n4,0⟩→⟨n5,0⟩
11	⟨n1,0⟩→⟨n5,0⟩	`sink(y)`	⟨n1,0⟩→⟨n6,0⟩
12	⟨n7,p⟩→⟨n8,p⟩	exit of `id`	— (`p` is not returned)
13	⟨n7,p⟩→⟨n8,r⟩	exit of `id`	summary ⟨n3,a⟩→⟨n4,x⟩; ⟨n1,0⟩→⟨n4,x⟩
14	⟨n1,0⟩→⟨n5,a⟩	`sink(y)`	⟨n1,0⟩→⟨n6,a⟩
15	⟨n1,0⟩→⟨n6,0⟩	exit of `main`	— (no callers)
16	⟨n1,0⟩→⟨n4,x⟩	`y = call id(b)`	⟨n1,0⟩→⟨n5,x⟩
17	⟨n1,0⟩→⟨n6,a⟩	exit of `main`	—
18	⟨n1,0⟩→⟨n5,x⟩	`sink(y)`	⟨n1,0⟩→⟨n6,x⟩
19	⟨n1,0⟩→⟨n6,x⟩	exit of `main`	—

The worklist is empty after 19 pops: 19 path edges and 3 summary edges. Facts: n5 = {a, x}, n8 = {p, r} (the facts of id joined over its contexts). The call at n4 enters id only with 0, so the summary ⟨n3,a⟩→⟨n4,x⟩ is never applied there: y stays untainted. A context-insensitive analysis (return edges to every return site) additionally reports y at n5 and n6.

IDE, linear constant propagation. Take main: n1 x = 3; n2 y = call f(x); n3 z = call f(y) and f(p): n4 r = 2*p + 1; return r. The jump function of f from entry fact \(p\) to exit fact \(r\) is the micro-function \(\lambda v.\, 2v + 1\) (one edge \(p \to r\) labelled with it). Phase I at n2 composes: \(x \mapsto \lambda.\,3\), the call edge maps \(x\) to \(p\) (identity), the summary maps \(p\) to \(r\) (\(\lambda v.\,2v+1\)), the return edge \(r\) to \(y\): \(y = (\lambda v.\,2v+1)(3) = 7\). At n3: \(z = 2 \cdot 7 + 1 = 15\). Phase II gives f's start value \(p = 3 \sqcup 7 = \top\) — the context-insensitive answer inside f — while the call results stay exact: IPSCCP (which joins the arguments first) finds neither 7 nor 15.

Try it

./course drill ifds-tabulation --seed 3 --difficulty hard --solution — a helper that calls a second helper; the answer includes the summary edges and the facts a context-insensitive analysis adds.

4. Invariants and correctness¶

Theorem 20.5.6 (IFDS tabulation computes MVP in O(E D³))

For an IFDS problem, Algorithm 20.5.4 terminates, and \(\mathrm{facts}(n) = \mathrm{MVP}(n)\) for every node \(n\). With \(E\) supergraph edges, \(\mathit{Call}\) call nodes and \(D = \lvert D \rvert\) facts it runs in \(O(E D^3)\) time when every call-to-start relation \(R_{\mathrm{call}}(c)\) has \(O(D)\) edges (each formal fact is fed by \(O(1)\) actual facts, as in actual-to-formal copying), and in \(O(E D^3 + \mathit{Call} \cdot D^4)\) in general ([RHS95] state \(O(E D^3)\) for their formulation); for locally separable problems (every flow function is a gen/kill on single facts: \(R_f \subseteq \{(0,0)\} \cup \{(0,d)\} \cup \{(d,d)\}\)) in \(O(E D)\).

Proof (following [RHS95, §4])

Representation. By Definition 20.5.3 and distributivity, \(d' \in M(\pi)(\emptyset)\) iff there is a path in \(G^{\sharp}\) from \((\mathrm{start}(\pi), 0)\) to \((\mathrm{end}(\pi), d')\) over the exploded edges of \(\pi\) (induction on \(\lvert\pi\rvert\): composing functions is concatenating their relations). So \(d \in \mathrm{MVP}(n)\) iff \((n, d)\) is reachable from \((s_{\mathtt{main}}, 0)\) along a valid path of \(G^{\sharp}\).

Soundness of the output (invariants I1, I2). Initially the seed edge is witnessed by the empty path. Each Propagate extends a witnessed same-level path by one exploded normal edge, by a call-to-return edge, or by a summary edge (itself witnessed by (I2), a same-level path through the callee); a new start edge \(\langle s_q, d_3 \rangle \to \langle s_q, d_3 \rangle\) is witnessed by the empty path, and \((s_q, d_3)\) is reachable along a valid path (the caller's valid path to \((c, d_2)\) plus the call edge). A summary edge created at an exit concatenates the call edge, a witnessed same-level path in \(q\) and the return edge: (I2). So every reported \((n, d)\) is the end of a valid path: \(\mathrm{facts}(n) \subseteq \mathrm{MVP}(n)\).

Completeness. By induction on the length of a valid path \(\pi\) from \((s_{\mathtt{main}}, 0)\) to \((n, d)\), decomposed as a sequence of same-level segments separated by unmatched call edges: each same-level segment inside procedure \(p\) from \((s_p, d_1)\) is found as a path edge, by an inner induction on the nesting of balanced call/return pairs — a balanced pair \((c, d_4) \to (s_q, d) \leadsto (e_q, d') \to (r_c, d_5)\) is found because the inner segment is (hypothesis), the exit rule then creates the summary edge, and the call rule or the exit rule's last loop applies it to every path edge reaching \((c, d_4)\) — whichever of the two events happens second. An unmatched call edge creates the start edge at \((s_q, d_3)\). So \((n, d)\) is reported: \(\mathrm{MVP}(n) \subseteq \mathrm{facts}(n)\).

Termination and cost. PathEdge \(\subseteq \{\langle s_p, d_1 \rangle \to \langle n, d_2 \rangle\}\) has at most \(N D_0^2\) elements (\(N\) nodes; one start per node), each propagated, and so processed, once; so the loop terminates. Count the work per rule, with \(D_0 = D + 1\). Normal and call-to-return edges: a path edge at \(n\) examines at most \(\delta(n) D_0\) exploded successors (\(\delta(n)\) = out-degree); with at most \(D_0^2\) path edges per node this is \(\sum_n \delta(n) D_0^3 = O(E D^3)\). Applying summaries at a call: a path edge at \(c\) scans the at most \(D_0\) summary edges from \(\langle c, d_2 \rangle\): \(O(D^3)\) per call node. Entering: the EndSum loop runs once per pair \((d_2, d_3) \in R_{\mathrm{call}}(c)\) (the guard), \(O(D^2)\) work each: \(O(\lvert R_{\mathrm{call}}(c) \rvert \, D^2)\). Exit: each exit path edge \(\langle s_q, d_1 \rangle \to \langle e_q, d_2 \rangle\) pairs, per call site \(c\), every \((c, d_4) \in \mathrm{Incoming}[s_q, d_1]\) with every \(d_5 \in R_{\mathrm{ret}}(c)(d_2)\); summed over \(d_1, d_2\) that is at most \(\lvert R_{\mathrm{call}}(c) \rvert \cdot \lvert R_{\mathrm{ret}}(c) \rvert \le \lvert R_{\mathrm{call}}(c) \rvert \, D_0^2\) pairs; and each of the at most \(D_0^2\) summary edges of \(c\) is created once and scans the at most \(D_0\) path edges into \(\langle c, d_4 \rangle\): \(O(D^3)\). With \(\lvert R_{\mathrm{call}}(c) \rvert = O(D)\) every call-site term is \(O(D^3)\), and the total is \(O(E D^3)\); with \(\lvert R_{\mathrm{call}}(c) \rvert \le D_0^2\) the pairing terms are \(O(D^4)\) per call site. When every \(R_f\) is locally separable, a path edge from \((s_p, d_1)\) with \(d_1 \ne 0\) can only end in \(d_1\) (facts map only to themselves), so there are at most \(2 D_0\) path edges per node (\(d_1 \to d_1\) and \(0 \to d\)), each with \(O(\delta)\) successors, and the bound drops to \(O(E D)\).

Theorem 20.5.7 (Functional approach = MVP for distributive frameworks; call strings need unbounded k)

(a) For a distributive framework, computing for each procedure the summary function \(\Phi_q = \bigsqcup_{\pi \text{ same-level } s_q \to e_q} M(\pi)\) and applying \(\Phi_q\) at every call yields MVP; for a merely monotone framework it yields an over-approximation of MVP (sound, possibly imprecise). (b) The call-string approach with strings of length at most \(k\) equals MVP when the program has no recursion and \(k \ge\) the depth of the call graph; with recursion no finite \(k\) is exact in general.

Proof sketch (full proof: [SP81, §3–4])

(a) A valid path to \(n\) decomposes into same-level segments and unmatched calls. Summarizing each maximal same-level subpath through \(q\) by \(\Phi_q\) is exact when \(M\) distributes over joins, because then \(M(\pi_2) \circ \bigsqcup_i M(\pi_1^i) = \bigsqcup_i M(\pi_2 \circ \pi_1^i)\): joining before or after composing is the same. With only monotonicity, \(\sqsupseteq\) holds: joining first loses precision, never soundness. (b) Without recursion, every valid path's pending-call stack has depth at most the call-graph depth, so strings of that length never truncate, and the analysis distinguishes exactly the valid paths. With recursion, a program whose result depends on the recursion depth modulo \(k + 1\) distinguishes paths that \(k\)-truncated strings merge.

Distributivity is a precondition

Constant propagation is not distributive: z = x + y with inputs \(\{x = 1, y = 2\}\) or \(\{x = 2, y = 1\}\) gives \(z = 3\) on both paths, but joining first gives \(x = y = \top\) and \(z = \top\). IFDS cannot encode it (its output depends on pairs of facts); IDE encodes the linear fragment (\(z = a x + b\) with one variable) and leaves the rest to \(\top\). IPSCCP is sound but merges contexts (it joins arguments over all call sites).

Theorem 20.5.8 (IPSCCP is sound and computes the least solution of the joined system)

IPSCCP's result is the least solution of the SCCP equations of Definition 17.1.7 extended with: an argument of an internal function equals the join of the actual arguments at its executable call sites; a call's result equals the join of the callee's values at its executable returns; arguments of externally visible functions are \(\top\). It is sound for every execution.

Proof sketch (full proof: [WZ91, §4] for SCCP; the interprocedural equations are [CCKT86]'s with all jump functions exact for constants)

The added equations are monotone joins over edges, so the system is monotone on a lattice of finite height and the worklist solver of Algorithm 17.1.8, with call and return edges added to its flow worklist, reaches the least solution (Theorem 17.1.9's argument). Soundness: every execution's values at a call are among the joined actual arguments, and returned values among the joined returns; visible functions may be called from outside, so their arguments are \(\top\). Merging over call sites makes it context-insensitive: it computes an over-approximation of the MVP of constant propagation.

5. Complexity¶

\(E\) = supergraph edges, \(D\) = facts, \(N\) = nodes, \(h\) = lattice height, \(k\) = call-string length, \(C\) = call sites.

Technique	Time (worst)	Time (typical)	Space	Justification
IPSCCP	\(O((U + E) \cdot h)\) for \(U\) SSA uses	near-linear, like SCCP	one lattice value per value	each value lowers at most \(h\) (= 2 or 3) times; each change re-visits its uses (Theorem 17.1.9)
Call strings, length \(k\)	\(O(C^k \cdot \text{intraprocedural cost})\)	exponential in \(k\); \(k \le 2\) in practice	\(O(C^k)\) copies of each fact	one context per string of \(\le k\) call sites
Functional / summaries	\(O(\lvert\text{summary space}\rvert \cdot E)\); for distributive problems \(O(E D^3)\) via IFDS	linear for bottom-up attribute summaries	one summary per procedure (or per entry fact)	summaries are computed once and reused at every call
IFDS tabulation	\(O(E D^3)\) (\(O(D)\)-edge call relations; else \(+\,\mathit{Call} \cdot D^4\)); locally separable \(O(E D)\)	far below the bound: on-demand exploration	\(O(N D^2)\) path edges	Theorem 20.5.6
IDE	\(O(E D^3)\) micro-function compositions, constant-size micro-functions	as IFDS plus phase II	\(O(N D^2)\) jump functions	[SRH96, §5]

Pathological family. For IFDS: a procedure copyall(p1, …, pD) whose body is \(D\) assignments p_{i+1} = p_i in a cycle, called from \(D\) call sites with a different single tainted argument each: every call enters with a different fact, each entry fact reaches all \(D\) facts at every node, so the procedure alone accounts for \(D \cdot N_q \cdot D\) path edges and the exit rule re-scans them per summary — the \(D^3\) is attained. For call strings: a chain of \(C\) procedures each calling the next from two sites has \(2^k\) distinct strings of length \(k\) at the bottom.

At scale. IFDS on the running example needs 19 path edges for 8 nodes and 5 facts (bound \(N D_0^2 = 8 \cdot 36 = 288\)); on 200 of the drill's hard instances (at most 14 nodes) the oracle never needs more than 45 path edges — typical of IFDS in practice, where the exploded graph is sparse.

Demand-driven / on-the-fly IFDS (Heros, PhASAR): explore only the exploded nodes a query needs; the tabulation above is already on-the-fly in the procedures it enters.
Sparse IFDS (Zero-fact elision, SSA-based sparse propagation): skip nodes that do not touch a fact, reducing \(E\) to def-use edges.
IDE for typestate and linear constants [SRH96]: micro-functions over a finite-height \(L\); trade-off: more expressive than IFDS at the cost of the micro-function algebra.
Jump functions of increasing power [CCKT86]: literal constants only, pass-through parameters, or polynomial jump functions — each more precise and more expensive to build.
\(k\)-limited call strings and object sensitivity (Ch 19): the context abstractions of points-to analysis, trading precision for \(C^k\) blow-up.
Summary reuse across compilations (ThinLTO, Lesson 20.9; incremental analysis): summaries are data that can be stored and shipped.

7. In real compilers¶

IPSCCP¶

LLVM: llvm/lib/Transforms/IPO/SCCP.cpp — runIPSCCP tracks arguments and return values of every function whose call sites are all known (internal linkage, address not taken), solves with SCCPSolver (llvm/lib/Transforms/Utils/SCCPSolver.cpp), then replaces constant arguments and returns and marks unused return values [LLVM-IPSCCP, LLVM-SCCP]. GCC: gcc/ipa-cp.cc — interprocedural constant propagation with jump functions (ipa-prop.cc) and cloning [GCC-IPACP].

IPSCCP returns constants out of functions

Reproduce (clang 23.1.2, opt 23.1.2):

cat > ipc.c <<'EOF'
static int version(void) { return 3; }
static int limit(int level) { return level > 2 ? 64 : 16; }
static int buffer_size(int level) { return limit(level) * version(); }
int small(void) { return buffer_size(3); }
int large(void) { return buffer_size(3) + 1; }
EOF
clang-23 -O1 -Xclang -disable-llvm-passes -fno-discard-value-names -S -emit-llvm ipc.c -o - | opt -passes=sroa -S -o ipc.ll
opt -passes=ipsccp -S ipc.ll | grep -vE '^;|^$|^attributes|^!' | sed -n '/^define/,$p'

Output:

define dso_local i32 @small() #0 {
entry:
  %call = call i32 @buffer_size(i32 noundef 3)
  ret i32 192
}
define internal i32 @buffer_size(i32 noundef %level) #0 {
entry:
  %call = call i32 @limit(i32 noundef 3)
  %call1 = call i32 @version()
  ret i32 poison
}
define dso_local i32 @large() #0 {
entry:
  %call = call i32 @buffer_size(i32 noundef 3)
  ret i32 193
}
define internal i32 @limit(i32 noundef %level) #0 {
entry:
  ret i32 poison
}
define internal i32 @version() #0 {
entry:
  ret i32 poison
}

What to notice: the §3 table: level became 3 inside buffer_size (the argument of the call to limit is now the literal 3), limit's 16 branch was never executable, and 192/193 appear in the callers. Every return value is now known at every call site, so the callees return poison ("unused") and the calls are left for dead-code elimination (they could have side effects in general).

Summary-based vs context-sensitive analysis¶

GCC: gcc/ipa-modref.cc — analyze_function builds a mod/ref summary per function (which parameters' memory is read or written, whether global memory is written, which parameters escape), propagated bottom-up over the IPA call graph and used by alias analysis at every call [GCC-Modref]. LLVM's summaries are its function and argument attributes (Lesson 20.6) and ThinLTO's module summary (Lesson 20.9). Context-sensitive analyses in production are mostly points-to analyses (Doop's object sensitivity, SVF's call-string options).

GCC's modref summaries

Reproduce (gcc 14.2.0):

cat > modref.c <<'EOF'
struct acc { long sum, n; };
__attribute__((noinline)) static void add(struct acc *a, long v) { a->sum += v; a->n++; }
__attribute__((noinline)) static long mean(const struct acc *a) { return a->n ? a->sum / a->n : 0; }
long g;
long run(const long *v, int k) {
  struct acc a = {0, 0};
  for (int i = 0; i < k; i++) add(&a, v[i]);
  g = 1;
  return mean(&a) + g;
}
EOF
gcc-14 -O2 -fdump-ipa-modref -c modref.c
grep -E "modref analyzing|- modref done" -A12 modref.c.*modref | grep -vE 'Analyzing|current flags|flags of ssa|^--$' | head -40

Output (the first 40 lines: the three summaries):

modref analyzing 'run/3' (ipa=1)
 - modref done with result: tracked.
  loads:
      Base 0: alias set 1
        Ref 0: alias set 1
          access: Parm 0
  stores:
      Base 0: alias set 1
        Ref 0: alias set 1
          Every access
  Global memory written
  parm 0 flags: no_direct_clobber no_direct_escape not_returned_directly
  parm 1 flags: no_direct_clobber no_indirect_clobber no_direct_escape no_indirect_escape not_returned_directly not_returned_indirectly no_direct_read no_indirect_read

modref analyzing 'mean/1' (ipa=1) (pure)
 - modref done with result: tracked.
  loads:
      Base 0: alias set 2
        Ref 0: alias set 1
          access: Parm 0 param offset:0 offset:0 size:64 max_size:128
  stores:
  Try dse
  parm 0 flags: not_returned_directly no_indirect_read


modref analyzing 'add/0' (ipa=1)
          ssa name saved to memory
 - modref done with result: tracked.
  loads:
      Base 0: alias set 2
        Ref 0: alias set 1
          access: Parm 0 param offset:0 offset:0 size:64 max_size:128
  stores:
      Base 0: alias set 2
        Ref 0: alias set 1
          access: Parm 0 param offset:0 offset:0 size:64 max_size:128
  kills:
     Parm 0 param offset:0 offset:0 size:128 max_size:128
  Try dse
  parm 0 flags: no_direct_escape

What to notice: each summary is a function of the parameters ("reads and writes 64 bits through parameter 0, within the first 128"; kills says the store overwrites the whole 128-bit object), not of any particular call: the functional approach. A caller applies it with its own argument (&a, a local), so add and mean cannot touch g; run's own summary records the global store.

IFDS and IDE¶

Heros (the IFDS/IDE solver behind Soot/FlowDroid), WALA's TabulationSolver and PhASAR (IFDS/IDE for LLVM IR) implement Algorithm 20.5.4 [RHS95]; Soufflé-based analyses encode it as Datalog rules, as in Lesson 14.8.

IFDS tabulation as Soufflé Datalog

Reproduce (Soufflé 2.5, Ubuntu 24.04 package souffle):

cat > taint.dl <<'EOF'
.decl next(n:symbol, m:symbol)
.decl flow(n:symbol, d:symbol, e:symbol)
.decl callsite(c:symbol, callee:symbol, r:symbol)
.decl callflow(c:symbol, d:symbol, e:symbol)
.decl c2r(c:symbol, d:symbol, e:symbol)
.decl exitnode(e:symbol, start:symbol)
.decl retflow(c:symbol, d:symbol, e:symbol)
.decl path(sp:symbol, d1:symbol, n:symbol, d2:symbol)
.decl summary(c:symbol, d1:symbol, d2:symbol)
.decl fact(n:symbol, d:symbol)
.output fact
.output summary
next("n1","n2"). next("n2","n3"). next("n5","n6"). next("n7","n8").
flow("n1","0","0"). flow("n1","0","a"). flow("n1","b","b"). flow("n1","x","x"). flow("n1","y","y").
flow("n2","0","0"). flow("n2","a","a"). flow("n2","x","x"). flow("n2","y","y").
flow("n5",d,d) :- d = "0" ; d = "a" ; d = "b" ; d = "x" ; d = "y".
flow("n7","0","0"). flow("n7","p","p"). flow("n7","p","r").
callsite("n3","n7","n4"). callsite("n4","n7","n5").
callflow("n3","0","0"). callflow("n3","a","p"). callflow("n4","0","0"). callflow("n4","b","p").
c2r("n3",d,d) :- d = "0" ; d = "a" ; d = "b" ; d = "y".
c2r("n4",d,d) :- d = "0" ; d = "a" ; d = "b" ; d = "x".
exitnode("n8","n7").
retflow("n3","0","0"). retflow("n3","r","x"). retflow("n4","0","0"). retflow("n4","r","y").
path("n1","0","n1","0").
path(sp,d1,m,d3) :- path(sp,d1,n,d2), next(n,m), flow(n,d2,d3).
path(s,d3,s,d3) :- path(_,_,c,d2), callsite(c,s,_), callflow(c,d2,d3).
path(sp,d1,r,d3) :- path(sp,d1,c,d2), callsite(c,_,r), c2r(c,d2,d3).
summary(c,d4,d5) :- path(_,_,c,d4), callsite(c,s,_), callflow(c,d4,d1),
                    path(s,d1,e,d2), exitnode(e,s), retflow(c,d2,d5).
path(sp,d1,r,d5) :- path(sp,d1,c,d4), callsite(c,_,r), summary(c,d4,d5).
fact(n,d) :- path(_,_,n,d), d != "0".
EOF
souffle -D- taint.dl

Output:

---------------
summary
c   d1  d2
===============
n3  0   0
n3  a   x
n4  0   0
===============
---------------
fact
n   d
===============
n3  a
n4  a
n4  x
n7  p
n5  a
n5  x
n8  p
n8  r
n2  a
n6  a
n6  x
===============

What to notice: the same three summary edges and the same facts as the §3 trace (Soufflé prints the rows in its own order): y is never a fact, because the summary rule only fires for the entry facts a call site actually provides. The four path rules are the four cases of Algorithm 20.5.4; semi-naive evaluation plays the worklist.

Find where LLVM does it. Open llvm/lib/Transforms/IPO/SCCP.cpp and find the function that implements the module-level IPSCCP driver (it is called from IPSCCPPass::run). What is its name? (Quiz llvm-where-ipsccp.)

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
IPSCCP	Constants and dead branches across calls; merges all call sites of a function (context-insensitive)	near-linear · cheap, runs in `default<O2>`	Replaced arguments and returns; `poison` for unused returns	Medium on top of SCCP	LLVM `ipsccp`, GCC `ipa-cp`
Summary-based vs context-sensitive	Summaries: exact for distributive problems, reusable; call strings: exact only without recursion, \(C^k\) blow-up	summaries once per function; call strings exponential in \(k\)	Summaries are inspectable data (modref dumps, ThinLTO index)	Low (summaries of simple lattices) to high (general call strings)	FunctionAttrs, modref, ThinLTO (summaries); points-to (call strings, object sensitivity)
IFDS / IDE	MVP exactly for distributive (IFDS) and linear-environment (IDE) problems	\(O(E D^3)\), \(O(E D)\) separable · on-demand	Facts per point plus the summary edges that explain them	Medium (tabulation) to high (IDE micro-functions)	Taint and security analyses (FlowDroid/Heros, PhASAR), typestate; rarely in optimizers

Choose IPSCCP when you optimize: it is cheap, runs on SSA and finds the constants that inlining and specialization then exploit. Choose summaries when facts about callees are reused at many call sites and the problem is distributive or a small lattice (attributes, side effects). Choose call strings or object sensitivity when the problem is not distributive (points-to) and contexts matter. Choose IFDS/IDE when you need exact interprocedural gen/kill results — taint, uninitialized variables, typestate — across a whole program.

9. Assessment¶

Quiz (./course quiz 20): ipsccp-return, llvm-where-ipsccp (tag ipsccp); summary-vs-callstring, context-insensitive-spurious (tag summaries); ifds-path-edges, ide-linear (tag ifds-ide).
Drill: ./course drill ifds-tabulation (easy: facts; medium: also summary edges; hard: also the facts a context-insensitive analysis adds — the summary-vs-context comparison of §3). IPSCCP is practiced by Ch 17's sccp-trace (the same solver with the interprocedural edges of Theorem 20.5.8 added); its quiz question ipsccp-return computes a cross-call result.
Flashcards: tags ipsccp, summaries, ifds-ide.
Exercises: none in the compiler; the drill's oracle (ipo.ifds) is a complete tabulation to read.

References¶

See the chapter references.

Lesson 20.5 — Interprocedural analysis: IPSCCP, summaries vs contexts, IFDS and IDE¶

1. Problem and motivation¶

IPSCCP¶

Summary-based vs context-sensitive analysis¶

IFDS and IDE¶

2. Definitions and algorithms¶

3. Worked example¶

IPSCCP¶

Summary-based vs context-sensitive analysis¶

IFDS and IDE¶

4. Invariants and correctness¶

5. Complexity¶

6. Variants and refinements¶

7. In real compilers¶

IPSCCP¶

Summary-based vs context-sensitive analysis¶

IFDS and IDE¶

8. Comparison¶

9. Assessment¶

References¶