eyeprolog

Pointer analysis

Which objects can each pointer variable point to?

A compiler cannot run a program to learn where its pointers go, so it reasons about every statement at once. This example does that the way Andersen-style analyses do: a handful of inclusion rules computed to a fixed point, here over a six-statement program.

Run it in the playground · Source

The question

Take this small C-like program:

x = &object_a
z = &object_b
y = x
*y = z
q = *x
r = q

Which variables may point to object_b? The answer is not visible in any one line: q only gets object_b because *y = z wrote it through y, and y is an alias of x.

The program as facts

addr(x, object_a).
addr(z, object_b).
assign(y, x).
store(y, z).
load(q, x).
assign(r, q).

Each statement becomes one fact: addr for taking an address, assign for copying a pointer, store for writing through a pointer (*y = z), and load for reading through one (q = *x).

The rules

points_to(Var, Object) :- addr(Var, Object).
points_to(To, Object) :- assign(To, From), points_to(From, Object).

field_points_to(Heap_object, Value_object) :-
  store(Pointer, Value),
  points_to(Pointer, Heap_object),
  points_to(Value, Value_object).
points_to(To, Value_object) :-
  load(To, Pointer),
  points_to(Pointer, Heap_object),
  field_points_to(Heap_object, Value_object).

Assignment copies points-to sets. A store makes the pointed-to object hold a reference (field_points_to); a load reads it back out. The rules are mutually recursive, and their least fixed point is the analysis result.

The answer

eyeprolog examples/pointer-analysis.pl

pointsTo(x, object_a).
pointsTo(z, object_b).
pointsTo(y, object_a).
pointsTo(r, object_b).
pointsTo(q, object_b).
heapField(object_a, object_b).
pointerFlow(load_q_from_x, object_b).
pointerConclusion(case, "the load q = *x recovers object_b through the store *y = z and y = x").

y aliases x, so the store through y puts object_b inside object_a, and the load through x hands it to q, and from there to r.

The reason

eyeprolog --proof examples/pointer-analysis.pl

step(points_to(q, object_b),
     rule(12),
     ['To' = q, 'Value_object' = object_b, 'Pointer' = x, 'Heap_object' = object_a],
     [load(q, x), points_to(x, object_a), field_points_to(object_a, object_b)]).
step(field_points_to(object_a, object_b),
     rule(11),
     ['Heap_object' = object_a, 'Value_object' = object_b, 'Pointer' = y, 'Value' = z],
     [store(y, z), points_to(y, object_a), points_to(z, object_b)]).

The proof is exactly the argument a reviewer would want: q reads object_b out of object_a (the load rule), because the store *y = z put it there while y pointed to object_a (the store rule).

The check

condition('C1', resolution, ok, 20).
condition('C4', coverage, ok, 28).
condition('C7', relevance, ok, 28).
verified(20).
trusted(0).
verdict(checked).

All 20 steps resolve against the clauses they cite, and the analysis rests on nothing but the six statement facts.

Try it

Add assign(s, r). and predict which object s may point to.
Add a second store store(x, x). (that is, *x = x). Which new heapField/2 and pointsTo/2 answers appear?
Andersen’s analysis ignores statement order. Which line of the source program would a flow-sensitive analysis treat differently?

Learn more in The Art of EyeProlog, Chapter 13 (fixed points and tabling).

This site is open source. Improve this page.