Lesson 19.8 — Points-to analysis as Datalog, and on demand¶

Techniques: points-to analysis in Datalog (the four rules; semi-naive evaluation; Doop on Soufflé; BDD-based evaluation in bddbddb); demand-driven points-to analysis (Heintze and Tardieu 2001; Sridharan and Bodík's refinement-based CFL reachability 2006) · Pebble implements: nothing new; the Datalog engine you wrote in Lab 14 runs this lesson's rules · Prerequisites: Lesson 14.8 (Datalog, semi-naive evaluation, stratification), Lesson 19.4 · Time: 3–4 hours

1. Problem and motivation¶

Datalog points-to¶

Lesson 19.4 wrote Andersen's analysis as four constraint forms and a hand-written solver with worklists, cycle detection and set representations. A Datalog program states the same four rules and leaves the solving to an engine: joins, indexes, semi-naive iteration and parallelism are the engine's job. Whaley and Lam's bddbddb evaluated such rules over binary decision diagrams and made cloning-based context sensitivity feasible [WL04, WACL05]; Bravenboer and Smaragdakis's Doop wrote a complete, context-sensitive Java points-to analysis in Datalog and found it faster than the hand-written framework it was compared with [BS09]; Soufflé compiles Datalog to parallel C++ and is Doop's engine today [JSS16]. The Dragon book presents pointer analysis this way [Dragon2, §12.3–12.7].

Demand-driven points-to¶

A compiler or a bug finder often needs only a few answers — "may this pointer be null?", "what can this virtual call target?" — not the whole solution. Demand-driven analysis answers one query by exploring only the part of the constraint graph that can influence it [HT01]. Sridharan and Bodík phrased field-sensitive points-to as CFL reachability (matched field stores and loads, matched calls and returns) and answered queries on demand, refining precision only where the client's answer is still too coarse, within a budget [SB06].

2. Definitions and algorithms¶

Datalog points-to¶

Definition 19.8.1 (Points-to Datalog program)

The EDB relations addr(p, a), copy(p, q), load(p, q), store(p, q) hold the statements of a pointer program (p = &a, p = q, p = *q, *p = q). The IDB relation pts(p, o) is defined by

pts(p, a) :- addr(p, a).
pts(p, o) :- copy(p, q), pts(q, o).
pts(p, o) :- load(p, q), pts(q, r), pts(r, o).
pts(r, o) :- store(p, q), pts(p, r), pts(q, o).

Its minimal model is the least set of pts facts closed under the rules (Lesson 14.8).

Algorithm 19.8.2 (Semi-naive evaluation of the points-to rules)

Input: the EDB facts.
Output: the minimal model of pts.
Precondition: the program is positive (no negation), so it has one minimal model.
Postcondition: pts is the minimal model, which equals Andersen's least solution (Theorem 19.8.5).
Invariant: after round \(i\), pts contains exactly the facts derivable in at most \(i\) rule applications; \(\Delta\) holds the facts first derived in round \(i\).

function SemiNaive(EDB):
    pts ← { (p, a) : addr(p, a) };  Δ ← pts
    while Δ ≠ ∅:
        new ← ∅
        new ∪= { (p, o) : copy(p, q), (q, o) ∈ Δ }
        new ∪= { (p, o) : load(p, q), (q, r) ∈ Δ, (r, o) ∈ pts } ∪ { (p, o) : load(p, q), (q, r) ∈ pts, (r, o) ∈ Δ }
        new ∪= { (r, o) : store(p, q), (p, r) ∈ Δ, (q, o) ∈ pts } ∪ { (r, o) : store(p, q), (p, r) ∈ pts, (q, o) ∈ Δ }
        Δ ← new \ pts;  pts ← pts ∪ Δ
    return pts

Each rule with two pts atoms is evaluated twice per round, once with each atom restricted to \(\Delta\): a new fact must use at least one fact from the previous round.

Demand-driven points-to¶

Definition 19.8.3 (Relevant variables of a query)

For a query \(\mathrm{pts}(v)\) and a partial solution \(\mathrm{pts}\), the relevant variables \(R\) form the least set with \(v \in R\) and closed under: if \(p \in R\) and p = q, then \(q \in R\); if \(p \in R\) and p = *q, then \(q \in R\) and every \(o \in \mathrm{pts}(q)\) is in \(R\); if some object is in \(R\), then the pointer \(x\) of every store *x = y is in \(R\); and if an object \(o \in R\) and a store *x = y has \(o \in \mathrm{pts}(x)\), then \(y \in R\). The relevant constraints are those whose left-hand side variable is in \(R\) (address-of, copy, load) and the stores whose pointer is in \(R\).

Algorithm 19.8.4 (Demand-driven query by growing the relevant set)

Input: a pointer program; a query variable \(v\).
Output: \(\mathrm{pts}^*(v)\).
Precondition: none.
Postcondition: the answer equals the whole-program least solution at \(v\) (Theorem 19.8.6).
Invariant: the partial solution is Andersen's least solution of the constraints whose left-hand side is in \(R\); \(R\) only grows.

function Query(v):
    R ← {v}
    repeat:
        C ← the relevant constraints of R (Definition 19.8.3)
        pts ← Andersen(C)                                   # Algorithm 19.4.4 on the sub-program
        R' ← the relevant variables for v under pts          # closure of Definition 19.8.3
        if R' = R: return pts(v)
        R ← R'

Heintze and Tardieu organise the same exploration as backward searches with caching of every intermediate answer [HT01]; Sridharan and Bodík match field stores and loads as parentheses (CFL reachability), explore on demand under a node budget, and fall back to the coarser answer when the budget runs out [SB06].

3. Worked example¶

Datalog points-to¶

The running example as facts is the first Soufflé box (§7). Semi-naive rounds (each row lists the facts first derived in that round):

round	new facts (\(\Delta\))	derived by
0	p→a, q→b, r→p, u→c	`addr` (1, 2, 3, 7)
1	q→c, s→b, t→a	copy 8 (`q = u`); copy 4 (`s = q`); load 6 (`t = *r`: r→p new, p→a)
2	b→a, p→b, s→c	copy 9 (`b = t`); store 5 (`*r = s`: r→p, s→b new); copy 4
3	p→c, q→a, t→b	store 5 (s→c new); copy 10 (`q = b`); load 6 (p→b new)
4	b→b, s→a, t→c	copy 9; copy 4; load 6 (p→c new)
5	b→c	copy 9 (t→c new)
6	— (q→b, p→a and q→c are re-derived, not new)	stop

The 17 facts are Andersen's solution (Lesson 19.4 §3), and Soufflé prints exactly them.

Demand-driven points-to¶

Query \(\mathrm{pts}(u)\). \(R = \{u\}\); its only constraint is u = &c; nothing is added to \(R\); answer \(\{c\}\) after exploring one of nine variables.

Query \(\mathrm{pts}(t)\). Round 1: \(R = \{t\}\); the constraint t = *r puts \(r\) in \(R\). Round 2: with r = &p, \(\mathrm{pts}(r) = \{p\}\), so the object \(p\) joins \(R\); an object in \(R\) makes the store pointer \(r\) relevant (already there), and since \(p \in \mathrm{pts}(r)\) the store *r = s adds \(s\). Round 3: s = q adds \(q\) (and p = &a is now solved). Round 4: q = u, q = b add \(u\) and \(b\). Round 5: b = t — \(t\) is already in \(R\); nothing new: \(R = \{t, r, p, s, q, u, b\}\) (7 of 9 variables, a and c never needed) and \(\mathrm{pts}(t) = \{a, b, c\}\). On large programs the relevant set of a typical query is a small fraction of the program, which is where demand-driven analysis wins.

4. Invariants and correctness¶

Datalog points-to¶

Theorem 19.8.5 (The Datalog minimal model is Andersen's least solution)

\((p, o)\) is in the minimal model of Definition 19.8.1 iff \(o \in \mathrm{pts}^*(p)\); semi-naive evaluation (Algorithm 19.8.2) computes it.

Proof

Read a set of pts facts as a function \(\mathrm{pts}(p) = \{ o : (p, o) \}\). A set of facts is closed under the four rules iff the function satisfies the four constraint forms of Definition 19.4.1: the addr rule is the base constraint; the copy rule is \(\mathrm{pts}(p) \supseteq \mathrm{pts}(q)\); the load rule says \(o \in \mathrm{pts}(r)\) and \(r \in \mathrm{pts}(q)\) imply \(o \in \mathrm{pts}(p)\) — the load constraint; the store rule the store constraint. So models are exactly solutions, and the minimal model is the least solution. Semi-naive evaluation computes the minimal model of a positive program (Lesson 14.8, Theorem 14.8.5): every derivation of depth \(i + 1\) uses at least one fact of depth exactly \(i\), which is in \(\Delta\) at round \(i\); it terminates because the number of facts is finite.

Demand-driven points-to¶

Theorem 19.8.6 (Demand-driven queries are exact)

Algorithm 19.8.4 terminates and returns \(\mathrm{pts}^*(v)\).

Proof

Termination: \(R\) grows in every round that does not return and is bounded by the finite set of variables. Let \(R\) and \(C\) be the final sets and \(\mathrm{pts}'\) the least solution of \(C\). (\(\subseteq\)) \(C\) is a subset of the program's constraints, so \(\mathrm{pts}^*\) is a solution of \(C\) and \(\mathrm{pts}' \subseteq \mathrm{pts}^*\). (\(\supseteq\)) Define \(S(x) = \mathrm{pts}'(x)\) for \(x \in R\) and \(S(x) = \mathrm{pts}^*(x)\) otherwise. \(S\) satisfies every constraint of the whole program. A constraint whose left-hand side is outside \(R\) holds because its left side has the full \(\mathrm{pts}^*\) value and every right-hand value of \(S\) is below \(\mathrm{pts}^*\). For a left-hand side in \(R\): an address-of or copy p = q is in \(C\), and \(q \in R\) by closure, so \(S(p) = \mathrm{pts}'(p) \supseteq \mathrm{pts}'(q) = S(q)\). A load p = *q is in \(C\), \(q \in R\), and every \(o \in \mathrm{pts}'(q)\) is in \(R\) by closure, so \(S(o) = \mathrm{pts}'(o) \subseteq \mathrm{pts}'(p)\). A store *x = y constrains an object \(o \in S(x)\): if \(o \notin R\) the left side is \(\mathrm{pts}^*(o)\) and holds as above; if \(o \in R\), then \(x \in R\) (an object is in \(R\)), the store is in \(C\), and \(o \in \mathrm{pts}'(x)\) puts \(y\) in \(R\), so \(S(o) = \mathrm{pts}'(o) \supseteq \mathrm{pts}'(y) = S(y)\). Hence \(S\) is a solution, \(\mathrm{pts}^* \subseteq S\), and in particular \(\mathrm{pts}^*(v) \subseteq \mathrm{pts}'(v)\).

5. Complexity¶

Technique	Time	Space	Notes
Datalog (semi-naive)	the number of rule instantiations: \(O(n^3)\) for the load and store rules over \(n\) variables (three variables per rule body), matching Proposition 19.4.16	\(O(n^2)\) facts	Soufflé adds indexes and parallel joins [JSS16]; no cycle detection unless encoded (`eqrel`)
Datalog over BDDs	depends on the BDD sizes, not the fact counts: \(10^{14}\) contexts fit when the variable order is good [WL04]	BDD nodes	variable ordering is the performance knob [WACL05]
Demand-driven	\(O(\text{relevant part})^3\) per query, with caching across queries	the relevant sub-graph	worst case equals whole-program; with a budget, answers degrade to "unknown" [SB06]

Justification. Semi-naive evaluation derives each fact once and, for a rule with body variables \(p, q, r, o\), enumerates at most the instantiations consistent with the facts, bounded by \(n^3\) for the join through the intermediate \(r\) (for fixed \(p, q\) from the EDB). Pathological family for demand-driven analysis: a query variable that depends, through a chain of copies, on every other variable — then \(R\) is the whole program and the query costs as much as whole-program analysis; caching makes later queries free.

Datalog points-to¶

Magic sets: the Datalog transformation that restricts bottom-up evaluation to facts relevant to a query — demand-driven analysis derived automatically from the rules; trade-off: rewritten rules, sometimes slower for many queries.
eqrel relations in Soufflé (union-find inside Datalog), which express Steensgaard-style unification and cycle collapsing; trade-off: equivalence relations only.
Context sensitivity by constructors in Doop: a context is a tuple built by rule, so switching between call-site, object and type sensitivity is a change of a few rules [BS09, SBL11].

Demand-driven points-to¶

Refinement-based [SB06]: start field-based and context-insensitive, refine only the matches a client needs; trade-off: answers depend on the budget.
Demand-driven flow- and context-sensitive analysis in SVF (ContextDDA, FlowDDA): budget per query, fall back to flow-sensitive answers when it is exhausted (§7).
Incremental analysis (reuse answers after program edits); trade-off: invalidation logic.

7. In real compilers¶

Datalog points-to¶

Datalog tools

Soufflé (souffle-lang/souffle, version 2.5) evaluates the rules of Definition 19.8.1 [SOUFFLE-DOC, JSS16]; Doop (plast-lab/doop) is a complete Java points-to framework in Datalog [BS09]; bddbddb evaluates Datalog over BDDs [WACL05]. Production compilers do not embed Datalog engines; GitHub's CodeQL (QL is Datalog-based) and Doop use them for program analysis around compilers. The Datalog engine of Lab 14 runs the same four rules.

Andersen's analysis as four Datalog rules, run by Soufflé

Reproduce (souffle 2.5; any OS):

cat > andersen.dl <<'DL'
// Andersen's analysis as four Datalog rules (Lesson 19.8), on the chapter's running example.
.decl addr(p:symbol, a:symbol)    // p = &a
.decl copy(p:symbol, q:symbol)    // p = q
.decl load(p:symbol, q:symbol)    // p = *q
.decl store(p:symbol, q:symbol)   // *p = q
.decl pts(p:symbol, o:symbol)
.output pts(IO=stdout)
addr("p","a"). addr("q","b"). addr("r","p"). copy("s","q"). store("r","s").
load("t","r"). addr("u","c"). copy("q","u"). copy("b","t"). copy("q","b").
pts(p, a) :- addr(p, a).
pts(p, o) :- copy(p, q), pts(q, o).
pts(p, o) :- load(p, q), pts(q, r), pts(r, o).
pts(r, o) :- store(p, q), pts(p, r), pts(q, o).
DL
souffle -D- andersen.dl

Output (complete):

---------------
pts
p   o
===============
p   a
p   b
p   c
q   a
q   b
q   c
b   a
b   b
b   c
r   p
u   c
s   a
s   b
s   c
t   a
t   b
t   c
===============

What to notice: the 17 facts of the §3 table and of Lesson 19.4's worklist: u points only to c, r only to p, and the five variables on the cycle to a, b, c; a and c hold nothing, so they have no facts.

Demand-driven points-to¶

SVF

svf/lib/DDA/ContextDDA.cpp — ContextDDA::computeDDAPts answers one query context-sensitively, with a budget (setMaxBudget(Options::CxtBudget())) and handleOutOfBudgetDpm, which downgrades an out-of-budget query to the flow-sensitive answer [SVF-DDA] (SVF 3.3). LLVM's own alias analysis is demand-driven in a lighter sense: BasicAA computes nothing ahead of time and walks use-def chains per query (Lesson 19.2).

SVF's budgeted demand-driven queries

Reproduce (curl 8.5.0; source at tag SVF-3.3):

curl -sL https://raw.githubusercontent.com/SVF-tools/SVF/SVF-3.3/svf/lib/DDA/ContextDDA.cpp -o ContextDDA.cpp
grep -nE 'Budget|budget' ContextDDA.cpp | head -8

Output (complete):

79:    LocDPItem::setMaxBudget(Options::CxtBudget());
91:    if(isOutOfBudgetQuery() == false)
94:        handleOutOfBudgetDpm(dpm);
113: * Handle out-of-budget dpm
115:void ContextDDA::handleOutOfBudgetDpm(const CxtLocDPItem& dpm)
118:    DBOUT(DGENERAL,outs() << "~~~Out of budget query, downgrade to flow sensitive analysis \n");
130:    addOutOfBudgetDpm(dpm);
306:                    outOfBudgetQuery = true;

What to notice: the maximum budget per query comes from an option (CxtBudget); a query that runs out is not answered "unknown" but downgraded ("Out of budget query, downgrade to flow sensitive analysis") — the refinement strategy of [SB06] in production-quality research code.

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Datalog points-to	Whatever the rules say: Andersen (Theorem 19.8.5) or context/field-sensitive variants	\(O(n^3)\) derivations · Soufflé is competitive with hand-written solvers [BS09, JSS16]	Relations you can query; every fact has a derivation (provenance)	Very low for the analysis (a page of rules), high for the engine	Doop, CodeQL, research; the Lab 14 engine
Demand-driven points-to	Exact per query (Theorem 19.8.6), or budget-limited	proportional to the relevant part · fast for few queries	Answers per query; "out of budget" fallback	Medium–high (caching, budgets)	IDE analyses, bug finders, SVF DDA, JIT-time queries

Choose Datalog to specify and experiment with analyses quickly, and to get provenance for free; choose demand-driven analysis when a client asks few questions about a large program.

9. Assessment¶

Quiz: datalog-rounds, datalog-rule-store (tag datalog-pta); demand-relevant-set, demand-budget (tag demand-driven).
Drill: ./course drill points-to-andersen (the solution the rules compute); Lesson 14.8's semi-naive exercises in the ch14 lab.
Flashcards: tags datalog-pta, demand-driven.
Exercises: run labs/ch14-dataflow/datalog/ (your Lab 14 engine) on Definition 19.8.1's rules and the running example's facts, and compare with the Soufflé box.

References¶

See the chapter references.

Lesson 19.8 — Points-to analysis as Datalog, and on demand¶

1. Problem and motivation¶

Datalog points-to¶

Demand-driven points-to¶

2. Definitions and algorithms¶

Datalog points-to¶

Demand-driven points-to¶

3. Worked example¶

Datalog points-to¶

Demand-driven points-to¶

4. Invariants and correctness¶

Datalog points-to¶

Demand-driven points-to¶

5. Complexity¶

6. Variants and refinements¶

Datalog points-to¶

Demand-driven points-to¶

7. In real compilers¶

Datalog points-to¶

Demand-driven points-to¶

8. Comparison¶

9. Assessment¶

References¶