This tutorial deals with static program analysis. Specifically, we aim to find out two things about a program in some fictional language using polymorphism:

1. To which class type a variable can point to throughout the execution of the program (later called VarPointsTo).
2. Which exact method is invoked at every call site in the presence of polymorphism (later called CallGraph).

Look at the following program in our fictional language. We have a super class Animal and two subclasses Cat and Dog. There is also the Greeter class whose greet() method expects a value of type Animal upon which it calls the speak() method (this is the polymorphic part):

class Greeter { void greet(Animal x) { x.speak(); } }  // s3
class Animal { void speak() {} }
class Dog  extends Animal { void speak() {...} }
class Cat  extends Animal { void speak() {...} }

void main() {
  Greeter g = new Greeter();
  Dog     d = new Dog();
  g.greet(d);                                          // s1
  Cat     c = new Cat();
  Animal ac = c;
  g.greet(ac);                                         // s2
}

For instance, we may want to find out which types the variable x in Greeter.greet actually assumes (VarPointsTo) and to which (concrete) methods the call site x.speak() resolves to (CallGraph).

To succinctly express VarPointsTo and CallGraph we resort to Datalog. A fictional driver program preparing the static analysis could generate the following base facts about the program being analyzed:

1. Alloc(var, obj) whenever var = new Obj() (new allocation).
2. Assign(dst, src) whenever dst = src (new assignment).
3. VirtualCall(site, recv, sig) whenever recv.sig(...) at call site site (imagine the driver program keeping track of all call sites as indicated above in the comments: s1, s2, and s3).
4. HeapType(obj, ty) stores the runtime type ty of an allocated object obj.
5. Dispatch(ty, sig, meth) stores for each type ty and each signature sig its method meth.
6. ActualArg(site, arg) stores for each call site site the given argument arg.
7. FormalParam(meth, param) stores for each method meth its parameter param.

The properties of our interest, VarPointsTo and CallGraph, can be expressed with Datalog as follows:

// The base case is an allocation.
VarPointsTo(V, Obj) :- Alloc(V, Obj).
// The self-recursive case is an alias.
VarPointsTo(Dst, Obj) :-
    Assign(Dst, Src),
    VarPointsTo(Src, Obj).
// This resolves to which object a parameter points to. Notice that this is
// self-recursive and mutually recursive with `CallGraph`!
VarPointsTo(Param, Obj) :-
    CallGraph(Site, Meth),
    ActualArg(Site, Arg),
    FormalParam(Meth, Param),
    VarPointsTo(Arg, Obj).

// This resolves to which concrete method each call site resolves to.
// Notice that this is mutually recursive with `VarPointsTo`.
CallGraph(Site, Meth) :-
    VirtualCall(Site, Recv, Sig),
    VarPointsTo(Recv, Obj),
    HeapType(Obj, Ty),
    Dispatch(Ty, Sig, Meth).

Souffle is a Datalog engine that can actually run this query. The folder data_step_1 contains the base facts to the fictional program shown above. This is how you can run it:

souffle program_analysis.dl --fact-dir data_step_1

Notice how the analysis tells us, among other things, that the variable x can point to both an instance of Dog and Cat (as part of VarPointsTo) and that call site s3 (corresponding to x.speak()) uses both Dog.speak and Cat.speak (see CallGraph).

Now the fictional program is modified, say, by its programmer, to introduce another subclass called Mouse of Animal. Also main() is extended by two lines to create a mouse and have it be greeted by the greeter:

class Greeter { void greet(Animal x) { x.speak(); } }  // s3
class Animal { void speak() {} }
class Dog  extends Animal { void speak() {...} }
class Cat  extends Animal { void speak() {...} }
class Mouse extends Animal { void speak() {...} }

void main() {
  Greeter g = new Greeter();   // oG
  Dog     d = new Dog();       // oDog
  g.greet(d);                  // s1
  Cat     c = new Cat();       // oCat
  Animal ac = c;               // alias (exercises the Assign rule)
  g.greet(ac);                 // s2
  Mouse   m = new Mouse()      // oMouse
  g.greet(m);                  // s4
}

The new base facts and the old ones are stored in the data_step_2 folder. Again you can run this via:

souffle program_analysis.dl --fact-dir data_step_2

This now tells us that both x and m can point to variables of type Mouse and that call site s3 (x.speak()) is also invoking Mouse.speak, plus that call site s4 is only using Greeter.greet.

Finally, we face a deletion of code. The alias ac is gone and, consequently, its usage afterwards is removed, too:

class Greeter { void greet(Animal x) { x.speak(); } }   // s3
class Animal { void speak() {} }
class Dog  extends Animal { void speak() {...} }
class Cat  extends Animal { void speak() {...} }
class Mouse extends Animal { void speak() {...} }

void main() {
  Greeter g = new Greeter();   // oG
  Dog     d = new Dog();       // oDog
  g.greet(d);                  // s1
  Cat     c = new Cat();       // oCat
  Mouse   m = new Mouse()      // oMouse
  g.greet(m);                  // s4
}

As you might be guessing already, some previously derived facts are not part of the output anymore. You can verify which ones by running:

souffle program_analysis.dl --fact-dir data_step_3

While each computation caused by a code change starts from scratch every time if we rely on Souffle, we now turn towards incremental computations with DBSP. The file tutorial12.rs contains the analogous DBSP circuit for the computation of VarPointsTo and CallGraph. Note that the translation from Datalog to a DBSP circuit has been done manually here. To observe how DBSP computes the output changes in response to the program modifications discussed above (as opposed to a full recomputation of the state with Souffle), run:

cargo run --example tutorial12