Lesson 14.8 — Declarative and interprocedural analysis: Datalog, IFDS and IDE¶

Techniques: Datalog-based analysis (least models, naive and semi-naive evaluation, stratified negation; Soufflé, Doop); IFDS and IDE (interprocedural distributive problems as graph reachability — a preview of Ch 20) · Pebble implements: a semi-naive Datalog engine and liveness as Datalog rules (lab requirements L3, L4) · Lab: naive vs semi-naive (labs/ch14-dataflow/datalog/compare.py) and Datalog vs C++ liveness (ch14.datalog) · Prerequisites: Lessons 14.2–14.3 · Time: 5–7 hours

Liveness in four lines:

live_out(V, B) :- edge(B, S), live_in(V, S).
live_out(V, P) :- phiuse(V, P, B).
live_in(V, B)  :- use(V, B).
live_in(V, B)  :- live_out(V, B), !def(V, B).

These rules are the equations of Definition 14.3.9, and a Datalog engine computes their least solution — the same MFP your C++ solver computes — with no worklist, no bit vectors and no visiting order in sight. That is the promise of declarative analysis: state the facts and the inference rules, let an optimized engine (Soufflé compiles them to parallel C++) do the fixed point. Doop specifies a complete points-to analysis for Java this way. The second half of the lesson turns to calls: IFDS shows that every distributive dataflow problem over a finite fact set can be solved precisely across procedures — matching calls with returns — as reachability in an "exploded" graph, and IDE extends it to values such as constants.

1. Problem and motivation¶

Datalog-based analysis¶

Datalog is Prolog without function symbols: rules over finite relations, evaluated bottom-up to a least model. It comes from deductive databases, where naive and semi-naive bottom-up evaluation and stratified negation were worked out [BR86, AHV95, Ch. 12–15]. Its use for program analysis took off when Whaley and Lam scaled context-sensitive points-to analysis with Datalog over BDDs (bddbddb) [WL04], Bravenboer and Smaragdakis wrote Doop, a full Java points-to analysis in Datalog that outperformed hand-written ones [BS09], and Jordan, Scholz and Subotić built Soufflé, which synthesizes efficient C++ analyzers from Datalog [JSS16]. The course's lab implements the core evaluation algorithm — semi-naive evaluation with stratified negation [BR86] — and runs Pebble's liveness as rules.

IFDS/IDE¶

Intraprocedural analysis treats a call as an opaque statement. Merging all calls of a function into one CFG (a supergraph) and iterating is sound but imprecise: facts from one call site flow back to another through the shared return (the "unrealizable path" problem). Reps, Horwitz and Sagiv showed that for interprocedural, finite, distributive, subset problems the precise answer over realizable paths is computable in polynomial time by reachability in an exploded supergraph [RHS95]; Sagiv, Reps and Horwitz generalized it to IDE (environments with values, e.g. linear constant propagation) [SRH96]. Soot/Heros, WALA, and PhASAR (for LLVM IR) implement them. Ch 20 treats interprocedural analysis in full; this lesson gives the reduction and the tabulation algorithm.

2. Definitions and algorithms¶

Datalog-based analysis¶

Definition 14.8.1 (Datalog program)

A Datalog program is a finite set of rules \(h \leftarrow b_1, \dots, b_k\) (written h :- b1, ..., bk.) and facts (rules with \(k = 0\) and no variables). Each \(h\), \(b_i\) is an atom \(R(t_1, \dots, t_m)\) over a relation name \(R\) and terms (constants or variables); a body atom may be negated (!R(...)). Relations that appear in heads are IDB (intensional), the others EDB (extensional: the input facts). A rule is safe if every variable of its head and of its negated atoms occurs in a positive body atom.

Definition 14.8.2 (Immediate consequence, least model, stratification)

For a program \(P\) without negation, a database \(D\) assigns a finite set of tuples to each relation. The immediate-consequence operator \(T_P(D)\) is \(D\) plus every head instance \(h\theta\) such that all body atoms \(b_i\theta\) are in \(D\) (for a substitution \(\theta\) of the variables by constants). Databases ordered by \(\subseteq\) form a complete lattice, \(T_P\) is monotone, and the least model is \(\mathrm{lfp}(T_P)\) above the EDB. With negation, \(P\) is stratified if its relations can be numbered so that a head's stratum is \(\ge\) that of each positive body relation and \(>\) that of each negated one; the perfect model evaluates strata in order, treating lower strata (including negated ones) as fixed EDB.

Algorithm 14.8.3 (Naive evaluation)

Input: a stratified safe program \(P\) and EDB facts.
Output: the perfect model (all relations).
Precondition: safety and stratification (Definitions 14.8.1, 14.8.2).
Postcondition: each stratum's IDB relations equal \(\mathrm{lfp}\) of that stratum's \(T_P\) (Theorem 14.8.5).
Invariant: before each round, the current IDB is contained in the least model.

function Naive(P, EDB):
    D ← EDB
    for each stratum S of P, lowest first:
        repeat                                        # one round
            new ← ∅
            for each rule h :- b1, ..., bk in S:
                for each substitution θ with every positive bi θ ∈ D
                                      and no negated bi θ ∈ D:
                    new ← new ∪ { hθ }
            changed ← new ⊄ D
            D ← D ∪ new
        until not changed
    return D

Algorithm 14.8.4 (Semi-naive evaluation)

Input: as Algorithm 14.8.3.
Output: the perfect model.
Precondition: as Algorithm 14.8.3.
Postcondition: as Algorithm 14.8.3 (Theorem 14.8.5); moreover, after round 1 no rule instance is fired unless one of its positive recursive body atoms was new in the previous round.
Invariant: \(\Delta_R\) holds exactly the tuples of \(R\) first derived in the previous round; every tuple derivable from \(D\) with no body atom in \(\Delta\) is already in \(D\).

function SemiNaive(P, EDB):
    D ← EDB
    for each stratum S of P, lowest first:
        new ← fire every rule of S once on D           # round 1, as in Naive
        Δ ← new ∖ D;  D ← D ∪ Δ
        while Δ ≠ ∅:                                     # later rounds
            new ← ∅
            for each rule h :- b1, ..., bk in S:
                for each position j whose atom bj is positive and in S (recursive):
                    for each θ with bj θ ∈ Δ, every other positive bi θ ∈ D,
                                     and no negated bi θ ∈ D:
                        new ← new ∪ { hθ }
            Δ ← new ∖ D;  D ← D ∪ Δ
    return D

The lab's contract datalog.evaluate(program, facts, method="naive" | "semi-naive") (labs/ch14-dataflow/datalog/datalog.py) returns the relations, the number of rounds and the number of derivations (successful body instantiations, duplicates included).

Theorem 14.8.5 (Correctness of naive and semi-naive evaluation)

For a safe stratified program both algorithms terminate and return the perfect model. Within a stratum, every tuple first derivable in round \(k + 1\) of naive evaluation is derived in round \(k + 1\) of semi-naive evaluation, and semi-naive evaluation never repeats a derivation whose body uses only tuples older than the previous round.

Proof

Termination: safety means every derived tuple consists of constants of the program and the EDB, so a stratum's relations are bounded by \(c^{m}\) tuples (\(c\) constants, arity \(m\)); each round that does not stop adds at least one tuple. Naive = least model: rounds apply \(T_S\) (the stratum's operator, lower strata fixed) to an ascending sequence starting at the EDB; this is Kleene iteration (Theorem 14.1.14) on the finite lattice of databases, so it stops at \(\mathrm{lfp}(T_S)\) above the EDB. Negated atoms refer only to lower strata, which are final, so \(T_S\) is monotone in the stratum's own relations. Semi-naive = naive: by induction on rounds, \(D\) after round \(k\) is the same in both. Any instance \(\theta\) of a rule that is satisfiable in \(D_k\) but not in \(D_{k-1}\) has some positive recursive body atom in \(D_k \setminus D_{k-1} = \Delta\), and the variant with \(j\) at that atom finds it (the other atoms are looked up in all of \(D_k\)). An instance satisfiable in \(D_{k-1}\) was already fired in round \(k\) or earlier, so its head is in \(D\). Hence both compute the same \(D_{k+1}\). Instances with no atom in \(\Delta\) are exactly the ones naive evaluation repeats. \(\square\)

Liveness in Soufflé

Reproduce (Soufflé 2.5, from the release package x86_64-ubuntu-2204-souffle-2.5-Linux.deb on github.com/souffle-lang/souffle; the facts are count10 from tests/ch14/Inputs/loops.facts):

cat > live.dl <<'EOF'
.decl edge(b: symbol, s: symbol)
.decl def(v: symbol, b: symbol)
.decl use(v: symbol, b: symbol)
.decl phiuse(v: symbol, p: symbol, b: symbol)
.decl live_in(v: symbol, b: symbol)
.decl live_out(v: symbol, b: symbol)
.output live_in(IO=stdout)
.output live_out(IO=stdout)
live_out(V, B) :- edge(B, S), live_in(V, S).
live_out(V, P) :- phiuse(V, P, _).
live_in(V, B)  :- use(V, B).
live_in(V, B)  :- live_out(V, B), !def(V, B).
// facts for count10 (tests/ch14/Inputs/loops.facts, printed by print<pebble-datalog-facts>)
edge("count10:entry", "count10:while.cond").
edge("count10:while.cond", "count10:while.body").
edge("count10:while.cond", "count10:while.end").
phiuse("count10:add", "count10:while.body", "count10:while.cond").
def("count10:i.0", "count10:while.cond").
def("count10:cmp", "count10:while.cond").
edge("count10:while.body", "count10:while.cond").
use("count10:i.0", "count10:while.body").
def("count10:add", "count10:while.body").
use("count10:i.0", "count10:while.end").
EOF
souffle -D- live.dl

Output:

---------------
live_in
v   b
===============
count10:i.0 count10:while.body
count10:i.0 count10:while.end
===============
---------------
live_out
v   b
===============
count10:i.0 count10:while.cond
count10:add count10:while.body
===============

What to notice: Soufflé's .decl lines give each relation a type; the four rules are the lab's liveness.dl. The result is exactly print<pebble-liveness> for count10: the phi %i.0 is live-out of while.cond but not live-in there, and %add is live-out of the latch only through the phi use. Soufflé's README describes the language as "similar to Datalog ... frequently used as a domain-specific language for analysis problems" [SOUFFLE-DOC]; it evaluates the rules semi-naively after compiling them to C++ [JSS16].

IFDS/IDE¶

Definition 14.8.6 (IFDS problem, realizable paths)

The supergraph \(G^{*}\) has the CFGs of all procedures, plus for each call site \(c\) (with return site \(r\)) a call edge \(c \to s_q\) to the callee's start and a return edge \(e_q \to r\) from its exit, and a call-to-return edge \(c \to r\) for effects local to the caller. A path is realizable if its call and return edges are properly matched, like parentheses labelled by call site (a valid path when a suffix may have unmatched calls). An IFDS problem is \((G^{*}, D, F, M, \sqcup)\): a finite fact set \(D\), flow functions \(M(e) \in F\) on edges, all distributive on \(\mathcal{P}(D)\), and join \(\cup\) (or \(\cap\)). Its meet-over-valid-paths solution is \(\mathrm{MVP}(n) = \bigcup_{p \in \mathrm{VP}(n)} f_p(\emptyset)\), where \(\mathrm{VP}(n)\) is the set of valid paths from the start of main to \(n\).

Definition 14.8.7 (Exploded supergraph)

A distributive \(f : \mathcal{P}(D) \to \mathcal{P}(D)\) is represented by a bipartite graph \(R_f\) on \((D \cup \{0\}) \times (D \cup \{0\})\): an edge \(0 \to 0\); \(0 \to d\) for every \(d \in f(\emptyset)\); \(d \to d'\) for every \(d' \in f(\{d\}) \setminus f(\emptyset)\). Then \(f(X) = \{\, d' \mid \exists d \in X \cup \{0\} : d \to d' \,\}\). The exploded supergraph \(G^{\sharp}\) has nodes \(N^{*} \times (D \cup \{0\})\) and, for each supergraph edge \(m \to n\), the edges \((m, d) \to (n, d')\) of \(R_{M(m \to n)}\).

Algorithm 14.8.8 (IFDS tabulation, Reps–Horwitz–Sagiv)

Input: an IFDS problem; the seed \((s_{\mathrm{main}}, 0)\).
Output: for every supergraph node \(n\), the facts \(d\) with \((n, d)\) reachable along a realizable path.
Precondition: flow functions distributive, \(D\) finite.
Postcondition: the result is \(\mathrm{MVP}\) (Theorem 14.8.9).
Invariant: every path edge \(\langle s_p, d_1 \rangle \to \langle n, d_2 \rangle\) in PathEdge witnesses a realizable same-level path from the start of \(n\)'s procedure; every summary edge \(\langle c, d_2 \rangle \to \langle r, d_5 \rangle\) witnesses a same-level path through the callee.

function Tabulate(G♯, seed = (s_main, 0)):
    PathEdge ← { ⟨s_main,0⟩ → ⟨s_main,0⟩ };  WorkList ← PathEdge;  SummaryEdge ← ∅
    while WorkList ≠ ∅:
        pop ⟨s_p, d1⟩ → ⟨n, d2⟩
        if n is a call node c with return site r and callee q:
            for each ⟨c, d2⟩ → ⟨s_q, d3⟩ in G♯:            # enter the callee
                Propagate(⟨s_q, d3⟩ → ⟨s_q, d3⟩)
            for each ⟨c, d2⟩ → ⟨r, d3⟩ in G♯ ∪ SummaryEdge:  # call-to-return and summaries
                Propagate(⟨s_p, d1⟩ → ⟨r, d3⟩)
        else if n is the exit e_p of procedure p:
            for each call site c of p (return site r), each ⟨c, d4⟩ → ⟨s_p, d1⟩ in G♯,
                and each ⟨e_p, d2⟩ → ⟨r, d5⟩ in G♯ (return edge for c):
                if ⟨c, d4⟩ → ⟨r, d5⟩ ∉ SummaryEdge:
                    add it to SummaryEdge
                    for each ⟨s_c, d3⟩ → ⟨c, d4⟩ in PathEdge:   # callers that reached c with d4
                        Propagate(⟨s_c, d3⟩ → ⟨r, d5⟩)
        else:
            for each ⟨n, d2⟩ → ⟨m, d3⟩ in G♯: Propagate(⟨s_p, d1⟩ → ⟨m, d3⟩)
    return { (n, d) : some ⟨·,·⟩ → ⟨n, d⟩ in PathEdge, d ≠ 0 }

function Propagate(e):
    if e ∉ PathEdge: add e to PathEdge and to WorkList

Theorem 14.8.9 (IFDS = realizable-path reachability)

For an IFDS problem, \(d \in \mathrm{MVP}(n)\) iff \((n, d)\) is reachable from \((s_{\mathrm{main}}, 0)\) in \(G^{\sharp}\) along a realizable path; Algorithm 14.8.8 computes this set in \(O(E \cdot \lvert D \rvert^{3})\) time, \(E\) = supergraph edges.

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

Representation: by Definition 14.8.7, \(f(X)\) is the set of facts reachable in \(R_f\) from \(X \cup \{0\}\), and composition of functions corresponds to concatenation of their graphs (reachability composes), so for any path \(p\), \(f_p(\emptyset)\) = the facts reachable from \(0\) along the exploded version of \(p\). Distributivity is what makes the per-fact graph exact: \(f(X) = \bigcup_{d \in X} f(\{d\}) \cup f(\emptyset)\). Joining over valid paths is reachability over valid paths. Algorithm: path edges are same-level realizable paths in the exploded graph; summary edges memoize "through the callee" once per (call site, entry fact, exit fact), which is what matches returns to calls. Complexity: at most \(\lvert D \rvert^{2}\) path edges per node, each processed against at most \(\lvert D \rvert\) successors per edge.

Definition 14.8.10 (IDE)

An IDE problem replaces sets of facts by environments \(D \to L\) for a lattice \(L\) of finite height, and each exploded edge \(d \to d'\) carries a micro-function \(L \to L\) (e.g. \(\lambda v.\, 2v + 3\) for linear constant propagation); flow functions are distributive environment transformers. Tabulation composes and joins micro-functions along path edges (jump functions) and then evaluates them in a second phase [SRH96]. IFDS is the special case \(L = \{\bot \sqsubset \top\}\) with identity micro-functions.

IFDS in Soufflé: context-sensitive uninitialized-variable analysis

Reproduce (Soufflé 2.5):

cat > ifds.dl <<'EOF'
// Possibly-uninitialized variables, interprocedural, as IFDS in Datalog.
//   main: m0 (entry: x, a, b uninitialized)  m1: a = id(x)  m2: b = id(1)  m3: use a, b
//   id(p): i0 (entry)  i1: r = p  i2 (exit: return r)
// Facts: "0" (the IFDS zero fact), and variable names = "may be uninitialized".
.decl flow(n: symbol, d: symbol, m: symbol, e: symbol)      // intraprocedural exploded edges
.decl callflow(c: symbol, d: symbol, s: symbol, e: symbol)  // call site -> callee entry
.decl retflow(x: symbol, d: symbol, r: symbol, e: symbol, c: symbol) // callee exit -> return site of c
.decl seed(n: symbol, d: symbol)
seed("m0", "0").
flow("m0", "0", "m1", "0"). flow("m0", "0", "m1", "x"). flow("m0", "0", "m1", "a"). flow("m0", "0", "m1", "b").
// call-to-return-site edges: the assigned variable is killed, the others pass
flow("m1", "0", "m2", "0"). flow("m1", "x", "m2", "x"). flow("m1", "b", "m2", "b").
flow("m2", "0", "m3", "0"). flow("m2", "x", "m3", "x"). flow("m2", "a", "m3", "a").
callflow("m1", "0", "i0", "0"). callflow("m1", "x", "i0", "p").   // x is passed as p
callflow("m2", "0", "i0", "0").                                    // 1 is initialized
flow("i0", "0", "i1", "0"). flow("i0", "p", "i1", "p").
flow("i1", "0", "i2", "0"). flow("i1", "p", "i2", "p"). flow("i1", "p", "i2", "r").
retflow("i2", "0", "m2", "0", "m1"). retflow("i2", "r", "m2", "a", "m1").
retflow("i2", "0", "m3", "0", "m2"). retflow("i2", "r", "m3", "b", "m2").

// IFDS tabulation: path edges (entry of the procedure, fact) ~> (node, fact), summaries per call site.
.decl path(s: symbol, d: symbol, n: symbol, e: symbol)
.decl summary(c: symbol, d: symbol, r: symbol, e: symbol)
path(n, d, n, d) :- seed(n, d).
path(s, d1, m, d3) :- path(s, d1, n, d2), flow(n, d2, m, d3).
path(q, d3, q, d3) :- path(_, _, c, d2), callflow(c, d2, q, d3).
summary(c, d2, r, d5) :- callflow(c, d2, q, d3), path(q, d3, x, d4), retflow(x, d4, r, d5, c).
path(s, d1, r, d5) :- path(s, d1, c, d2), summary(c, d2, r, d5).
.decl ifds(n: symbol, d: symbol)
ifds(n, d) :- path(_, _, n, d), d != "0".

// The same edges without matching calls to returns (every return edge is taken from every call).
.decl insensitive(n: symbol, d: symbol)
insensitive(n, d) :- seed(n, d).
insensitive(m, e) :- insensitive(n, d), flow(n, d, m, e).
insensitive(q, e) :- insensitive(c, d), callflow(c, d, q, e).
insensitive(r, e) :- insensitive(x, d), retflow(x, d, r, e, _).
.decl at_use(analysis: symbol, var: symbol)
at_use("ifds", d) :- ifds("m3", d).
at_use("insensitive", d) :- insensitive("m3", d), d != "0".
.output at_use(IO=stdout)
EOF
souffle -D- ifds.dl

Output:

---------------
at_use
analysis    var
===============
ifds    x
ifds    a
insensitive x
insensitive a
insensitive b
===============

What to notice: the rules for path and summary are Algorithm 14.8.8 in Datalog (the worklist becomes semi-naive evaluation). At the use in m3, IFDS reports x (never assigned) and a (assigned id(x)), but not b: the uninitialized r of id's exit belongs to the call from m1, and the summary edge for the call site m2 (argument 1) produces no r. The context-insensitive propagation, which lets every return edge follow every call, reports b too — a false positive along the unrealizable path m1 → i0 → i1 → i2 → m3.

3. Worked example¶

Datalog-based analysis on the running example¶

The facts of count10 (Soufflé box above) and the four liveness rules, numbered R1–R4 in the order of the introduction (R1: live_out from edge, R2: from phiuse, R3: live_in from use, R4: live_in from live_out and !def). One stratum (negation is on the EDB relation def). Semi-naive evaluation (Algorithm 14.8.4):

round	Δ `live_in`	Δ `live_out`	derivations (rule: count)
1	`(i.0, while.body)`, `(i.0, while.end)`	`(add, while.body)`	R2: 1, R3: 2
2	—	`(i.0, while.cond)`	R1 with Δ `live_in`: 2 (both give the same tuple)
3	—	—	R4 with Δ `live_out`: 0 (`def(i.0, while.cond)` blocks it; `def(add, while.body)` blocked it in round 2)

3 rounds, 5 derivations. Naive evaluation (Algorithm 14.8.3) also needs 3 rounds but re-fires every rule on the whole database each round: 13 derivations (3 + 5 + 5). On the running example's 16 values (tests/ch14/Inputs/running.facts), semi-naive needs 7 rounds and 55 derivations, naive 7 rounds and 303; on transitive closure of a 60-node chain (compare.py --chain 60), 1 770 versus 71 980 derivations, 54 ms versus 2 094 ms.

IFDS/IDE on the running example¶

The Soufflé box's program as an exploded supergraph (facts 0, x, a, b in main; 0, p, r in id). Tabulation from \(\langle m0, 0 \rangle\):

step	path edge popped	action	new path/summary edges
1	⟨m0,0⟩→⟨m0,0⟩	normal edges	⟨m0,0⟩→⟨m1,0⟩, →⟨m1,x⟩, →⟨m1,a⟩, →⟨m1,b⟩
2	⟨m0,0⟩→⟨m1,x⟩	call m1: enter with p; call-to-return keeps x	⟨i0,p⟩→⟨i0,p⟩; ⟨m0,0⟩→⟨m2,x⟩
3	⟨m0,0⟩→⟨m1,0⟩	call m1: enter with 0	⟨i0,0⟩→⟨i0,0⟩; ⟨m0,0⟩→⟨m2,0⟩
4	⟨m0,0⟩→⟨m1,b⟩	call-to-return keeps b (a is killed)	⟨m0,0⟩→⟨m2,b⟩
5	⟨i0,p⟩→⟨i0,p⟩ … ⟨i0,p⟩→⟨i2,r⟩	`r = p`	⟨i0,p⟩→⟨i1,p⟩, ⟨i0,p⟩→⟨i2,p⟩, ⟨i0,p⟩→⟨i2,r⟩
6	⟨i0,p⟩→⟨i2,r⟩ at the exit	caller m1 entered with x ↦ p: summary ⟨m1,x⟩→⟨m2,a⟩	⟨m0,0⟩→⟨m2,a⟩
7	⟨m0,0⟩→⟨m2,x⟩, ⟨m2,a⟩, ⟨m2,0⟩	call m2 (argument 1): enter only with 0; call-to-return kills b, keeps x, a	⟨m0,0⟩→⟨m3,x⟩, →⟨m3,a⟩, →⟨m3,0⟩
8	⟨i0,0⟩→⟨i2,0⟩ at the exit	summaries ⟨m1,0⟩→⟨m2,0⟩ and ⟨m2,0⟩→⟨m3,0⟩ only: no fact `r` from the 0 context	—

Result at m3: \(\{x, a\}\). The path edge ⟨i0,p⟩→⟨i2,r⟩ is never applied at call site m2 because m2 never enters id with p — this is the call/return matching that the insensitive analysis lacks.

Try it

After L3 and L4, run uv run python labs/ch14-dataflow/datalog/compare.py tests/ch14/Inputs/*.facts and --chain 200, and compare the derivation counts with the table above. The drills of this chapter do not cover Datalog or IFDS; the quiz questions seminaive-derivations and ifds-realizable compute them on concrete instances.

4. Invariants and correctness¶

Datalog-based analysis¶

Theorem 14.8.5. When it breaks: (1) unstratified negation — p(X) :- q(X), !p(X). has no least model (the lab's evaluator must reject it: DatalogError); (2) unsafe rules — p(X) :- !q(X). would need the complement of a relation over an unbounded domain; (3) arithmetic in heads (Soufflé allows x + 1) breaks the finite-universe termination argument: a rule n(X + 1) :- n(X). never terminates. For analyses this means: a lattice of infinite height cannot be encoded directly; Soufflé analyses keep finite domains (program entities) and encode lattices as sets.

IFDS/IDE¶

Theorem 14.8.9 requires distributivity: a non-distributive function (constant propagation's z = x + y) has no exact representation as a per-fact graph, because its output depends on pairs of input facts. IDE recovers some such problems by moving values into micro-functions (linear constants \(\lambda v.\, a v + b\)). Soundness also requires the call graph to be sound (all possible callees at indirect calls) — Ch 20.

5. Complexity¶

Let \(c\) = constants in the EDB, \(m\) = maximal arity, \(k\) = maximal body length; \(E\) = supergraph edges, \(D\) = facts, \(\lvert \mathrm{Call} \rvert\) = call sites.

Technique	Time (worst)	Time (typical)	Space	Variables
Naive Datalog	\(O(\text{rounds} \cdot \lvert \text{rules} \rvert \cdot c^{k \cdot m})\); rounds \(\le c^{m}\)	as many rounds as semi-naive, many more derivations	\(O(c^{m})\) per relation	\(c, m, k\)
Semi-naive Datalog	each derivation at most once per new tuple: polynomial, \(O(c^{\#\text{vars per rule}})\) per rule overall	near-linear in the output with good join indexes (Soufflé)	\(O(c^{m})\)	\(c, m\)
IFDS tabulation	\(O(E \cdot D^{3})\); \(O(E \cdot D)\) for locally separable (bit-vector) problems [RHS95]	—	\(O(E \cdot D^{2})\) path edges	\(E, D\)
IDE	\(O(E \cdot D^{3})\) jump-function compositions (micro-functions of constant size) [SRH96]	—	\(O(E \cdot D^{2})\)	\(E, D\)

Proposition 14.8.11 (Semi-naive transitive closure of a chain)

For path(X, Y) :- edge(X, Y). path(X, Z) :- path(X, Y), edge(Y, Z). on a chain of \(n\) nodes, both methods need \(n\) rounds; semi-naive makes exactly \(n(n-1)/2\) derivations, naive \(\Theta(n^{3})\).

Proof

The paths of length \(\ell\) are first derivable in round \(\ell\) (\(1 \le \ell \le n - 1\)), and round \(n\) derives nothing new: \(n\) rounds. Semi-naive round \(\ell \ge 2\) joins only the \(n - \ell + 1\) paths of length \(\ell - 1\) (the Δ) with the unique next edge: each path of length \(\ell\) is derived once; with the \(n - 1\) edges of round 1 this is \(\sum_{\ell=1}^{n-1} (n - \ell) = n(n-1)/2\) derivations. Naive round \(\ell\) re-derives every path of length \(\le \ell\): \(\sum_{j \le \ell} (n - j) = \Theta(\ell n)\), and summing over \(n\) rounds gives \(\Theta(n^{3})\). The course test checks \(435 = 30 \cdot 29 / 2\) for \(n = 30\). \(\square\)

Pathological input. For IFDS, \(D\) = all variables of a large program (thousands) makes \(D^{3}\) prohibitive; practical IFDS solvers exploit sparsity of the exploded graph and compute on demand.

At scale: Doop analyzes large Java programs (the DaCapo benchmarks) with context-sensitive points-to analysis; its paper reports it faster than the hand-written Paddle framework on the same analyses [BS09].

Datalog-based analysis¶

BDD-based Datalog (bddbddb) [WL04]: relations as binary decision diagrams — trade-off: exponentially compact for regular relations (context strings), unpredictable variable orders.
Compilation to C++ with specialized indexes (Soufflé) [JSS16]: parallel semi-naive evaluation with B-trees and automatically chosen indexes — trade-off: compile time, but orders of magnitude faster than interpretation.
Lattices in Datalog (Flix, Datalog with subsumption): allow lattice-valued relations — trade-off: expressive (constant propagation as rules), needs monotone aggregation semantics.

IFDS/IDE¶

IDE [SRH96]: values instead of sets — trade-off: linear constant propagation and typestate, at the price of micro-function algebra.
Demand-driven / on-the-fly IFDS (Heros, PhASAR) — trade-off: explore only what queries need.
Datalog encodings (the box above): path/summary edges as recursive rules — trade-off: one engine for many analyses, less control over the worklist order.

7. In real compilers¶

Datalog-based analysis¶

Datalog analyzers

Soufflé (souffle-lang/souffle, version 2.5) — the engine; its README: "The Soufflé language is similar to Datalog (but has terms known as records), and is frequently used as a domain-specific language for analysis problems" [SOUFFLE-DOC]. Doop (plast-lab/doop) — Java points-to and taint analysis as Datalog rules; its tutorial explains the evaluation model: rules "infer new information from facts already known to be true. This continues until no new information can be extracted (fixed-point computation)" [DOOP-DOC]. Production compilers (LLVM, GCC) do not embed Datalog engines; Datalog is used around them (static analyzers, security tools such as GitHub's CodeQL, whose QL language is Datalog-based).

Pebble lab labs/ch14-dataflow/datalog/ — your semi-naive engine and liveness.dl, compared against the C++ liveness by ch14.datalog.

IFDS/IDE¶

IFDS/IDE frameworks

No LLVM or GCC pass is an IFDS solver; LLVM's interprocedural analyses (IPSCCP, function attributes, llvm/lib/Transforms/IPO/) use call-graph SCC orders and summaries instead (Ch 20). IFDS/IDE solvers exist for LLVM IR (PhASAR), Java (Soot/Heros, WALA) and in industrial taint analyzers (FlowDroid); the course runs the tabulation algorithm as Datalog in Soufflé (box above) [RHS95, SRH96].

8. Comparison¶

Technique	Power / precision	Speed	Output / error quality	Implementation effort	Typical use
Datalog-based analysis	Least model = MFP for set-based (finite, monotone) analyses; any relation-valued analysis	Semi-naive: each derivation once per new tuple; Soufflé-compiled near hand-written speed	Relations queryable afterwards; derivations explainable (provenance)	Very low per analysis (rules), high for the engine	Points-to (Doop), security queries (CodeQL), rapid prototyping
IFDS/IDE	Exact over realizable paths for distributive problems (MVP)	\(O(E D^{3})\)	Context-sensitive facts per node	Medium (tabulation + flow functions)	Interprocedural taint, uninitialized variables, typestate, linear constants

Choose Datalog when the analysis is naturally relational (points-to, call graphs, reachability) or you want to iterate on its specification quickly. Choose hand-written solvers (Lesson 14.4) when the lattice has infinite height, when you need bit-vector speed inside a compiler, or when the IR is not already a database. Choose IFDS when a distributive analysis must cross procedure boundaries precisely; IDE when the facts carry values.

Lab numbers (reproduce with uv run python labs/ch14-dataflow/datalog/compare.py --chain 60): semi-naive 1 770 derivations / 54 ms, naive 71 980 / 2 094 ms (reference solution, this container).

9. Assessment¶

Technique	Quiz ids	Drill	Flashcard tag	Exercises
Datalog-based analysis	`seminaive-derivations`, `datalog-stratification`	— (see §3's tip)	`datalog`	lab L3, L4
IFDS/IDE	`ifds-realizable`, `ifds-distributive`	—	`ifds`	—

Neither technique has a drill: Datalog evaluation is exercised by the lab's tests (every round and derivation count), and IFDS instances large enough to be interesting are too large to trace by hand repeatedly; the quiz computes one of each.

Pitfall

"Datalog is slow because it recomputes everything." Naive evaluation does; semi-naive evaluation never fires a rule instance unless one of its body tuples is new, and compiled engines index every join. The derivation counts above (\(5\) vs \(13\), \(1\,770\) vs \(71\,980\)) are the whole story.

References¶

See the chapter references.

Lesson 14.8 — Declarative and interprocedural analysis: Datalog, IFDS and IDE¶

1. Problem and motivation¶

Datalog-based analysis¶

IFDS/IDE¶

2. Definitions and algorithms¶

Datalog-based analysis¶

IFDS/IDE¶

3. Worked example¶

Datalog-based analysis on the running example¶

IFDS/IDE on the running example¶

4. Invariants and correctness¶

Datalog-based analysis¶

IFDS/IDE¶

5. Complexity¶

6. Variants and refinements¶

Datalog-based analysis¶

IFDS/IDE¶

7. In real compilers¶

Datalog-based analysis¶

IFDS/IDE¶

8. Comparison¶

9. Assessment¶

References¶