Datalog for Program Analysis

2024-06-13 · Ryan Williams · Updated 2026-06-26

Introduction

Many program analyses boil down to the same shape: start with some facts you can read directly off the code, apply rules that derive new facts, and keep going until nothing changes. That pattern — facts plus rules, iterated to a fixpoint — is exactly what Datalog was built for.

This post is a hands-on tour. We start from the basics of Datalog, build a tiny program, watch it reach a fixpoint, and then use the same machinery to implement a real pointer analysis in a handful of rules.

What is Datalog?

Datalog is a declarative logic programming language — a decidable subset of Prolog. You describe what relationships hold, not how to compute them, and the engine figures out the rest. That declarative nature, plus guaranteed termination, is what makes it such a good fit for analysis.

Syntax

A Datalog program is made of three things:

Facts — ground assertions about the world:

parent("enzo", "mia").

Rules — implications that derive new facts from existing ones. Read :- as "if", and a comma as "and":

ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).

Queries — questions answered from the facts and rules:

?- ancestor("enzo", "mia").

Capitalized names (X, Y, Z) are variables; quoted strings are constants.

Setting up Soufflé

Soufflé is a fast, practical Datalog engine that compiles your rules down to parallel C++. It is the engine most modern analysis frameworks build on.

# Linux
sudo apt install souffle

# macOS
brew install souffle-lang/souffle/souffle

Your first program

Let's encode a family tree and ask who descends from whom.

Facts:

parent("enzo", "mia").
parent("mia", "piper").
parent("piper", "owen").

Rules:

ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).

If you save just this and run it, Soufflé complains — it needs to know the type of each relation up front via .decl, and what to output:

.decl parent (n: symbol, m: symbol)
parent("enzo", "mia").
parent("mia", "piper").
parent("piper", "owen").

.decl ancestor (n: symbol, m: symbol)
ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).

.output ancestor

Run it:

souffle -D . family.dl

This writes ancestor.csv with every derived relationship:

enzo	mia
enzo	piper
enzo	owen
mia	piper
mia	owen
piper	owen

Recursion and the fixpoint

Where did enzo → owen come from? It is not a fact, and no single rule application produces it directly. Datalog evaluates the recursive rule repeatedly, feeding each round's output back in as input, until a round produces no new facts. That stable result is the least fixpoint.

Step through the rounds:

Round 0 · baseRound 1Round 2 · fixpoint

Apply the base rule ancestor(X,Y) :- parent(X,Y). Every parent edge becomes an ancestor edge.

ancestor(enzo, mia)ancestor(mia, piper)ancestor(piper, owen)

Apply the recursive rule to Round 0: parent(X,Z), ancestor(Z,Y). Two new transitive edges appear.

ancestor(enzo, mia)ancestor(mia, piper)ancestor(piper, owen)ancestor(enzo, piper)ancestor(mia, owen)

One more round derives the last edge. A further round adds nothing — we have reached the least fixpoint, and the query is complete.

ancestor(enzo, mia)ancestor(mia, piper)ancestor(piper, owen)ancestor(enzo, piper)ancestor(mia, owen)ancestor(enzo, owen)

Because rules only ever add facts and the universe of possible facts is finite, this process always terminates — the guarantee that separates Datalog from full Prolog.

Datalog for program analysis

Here is the key insight: a great many program analyses are just recursive Datalog queries over relations extracted from source code. You emit facts like "there is an assignment from q to p" or "function f calls g", write a few rules, and let the engine compute the fixpoint. Frameworks like Doop analyze large Java programs this way.

Pointer analysis in four rules

Points-to analysis asks: at runtime, which memory objects can each pointer refer to? We extract four kinds of facts from the program — AddrOf, Assign, Load, and Store — and derive a single relation, PointsTo. This is the classic Andersen (inclusion-based) formulation. Expand each rule:

p = &xAddress-of — the base case

PointsTo(p, x) :- AddrOf(p, x).

Taking the address of x makes p point to it directly.

p = qCopy — p inherits q's targets

PointsTo(p, o) :- Assign(p, q), PointsTo(q, o).

An assignment copies every object in q's points-to set into p's.

p = *qLoad — dereference, then copy

PointsTo(p, o) :- Load(p, q), PointsTo(q, r), PointsTo(r, o).

To resolve *q, first find what q points to (call it r), then copy what those objects point to.

*p = qStore — write through p

PointsTo(r, o) :- Store(p, q), PointsTo(p, r), PointsTo(q, o).

Writing through p updates every object p may point to (r).

The Load and Store rules are why pointer analysis is recursive: resolving a dereference depends on the points-to sets we are still computing, so each new fact can unlock more. We iterate to a fixpoint, exactly as before.

A worked example

Consider this snippet and the relations it produces:

a = &x;     // AddrOf(a, x)
b = a;      // Assign(b, a)
c = &y;     // AddrOf(c, y)
*b = c;     // Store(b, c)
d = *a;     // Load(d, a)

Running the rules to a fixpoint yields:

Statement	Input relation	Newly derived
`a = &x;`	`AddrOf(a, x)`	`a → x`
`b = a;`	`Assign(b, a)`	`b → x`
`c = &y;`	`AddrOf(c, y)`	`c → y`
`*b = c;`	`Store(b, c)`	`x → y`
`d = *a;`	`Load(d, a)`	`d → y`

The interesting rows are the last two. The store *b = c flows y into x's points-to set (because b points to x), and the load d = *a then picks it up (because a points to x, and x now points to y). Two simple rules, composed by the fixpoint, capture indirect flow through the heap.

Beyond points-to

The same recipe scales to a surprising range of analyses:

Call-graph construction — resolve indirect/virtual calls from points-to sets, then derive Calls(caller, callee).
Taint analysis — seed Tainted(x) at sources and propagate along assignments and calls to find flows into sinks.
Dataflow and reachability — Reaches, LiveAt, and friends are one or two rules each.

Why Datalog scales

Writing analyses this way is not just elegant — it is fast. Engines like Soufflé apply semi-naïve evaluation (only re-deriving facts that could be affected by last round's new facts), choose efficient join orders, and compile the whole program to parallel C++. You get the readability of a few declarative rules with the performance of hand-tuned code.

Try it yourself

Install Soufflé (above).
Drop the points-to facts into pta.dl with .decl lines for AddrOf, Assign, Load, Store, and PointsTo, plus the four rules.
Add .output PointsTo and run souffle -D . pta.dl.
Add a statement to the snippet and predict the new rows before re-running.

Conclusion

Datalog turns "facts + rules + fixpoint" into a few lines of declarative code. That single idea — which we watched play out in the ancestor stepper and reused verbatim for pointer analysis — underpins production analysis frameworks. Once you start seeing analyses as queries, it is hard to stop.