feldera · mihaibudiu · Jun 25, 2026 · Jun 22, 2026 · mihaibudiu · Jun 22, 2026
diff --git a/crates/dbsp/Cargo.toml b/crates/dbsp/Cargo.toml
@@ -217,6 +217,10 @@ path = "examples/tutorial/tutorial10.rs"
 name = "tutorial11"
 path = "examples/tutorial/tutorial11.rs"
 
+[[example]]
+name = "tutorial12"
+path = "examples/tutorial/tutorial12/tutorial12.rs"
+
 [[example]]
 name = "coord"
 path = "examples/dist/coord.rs"

diff --git a/crates/dbsp/examples/tutorial/tutorial10.rs b/crates/dbsp/examples/tutorial/tutorial10.rs
@@ -34,7 +34,7 @@ fn main() -> Result<()> {
                 //  |                                   |
                 //  ------------------3------------------
                 // zset_set! { Tup3(1,2,1), Tup3(4, 0, 3)}
-            ] as [_; STEPS])
+            ] as [OrdZSet<Tup3<usize, usize, usize>>; STEPS])
                 .into_iter();
 
             let edges = root_circuit.add_source(Generator::new(move || edges_data.next().unwrap()));
@@ -99,7 +99,7 @@ fn main() -> Result<()> {
         // This does not matter, as the computation does not terminate
         // anymore due to the cycle.
         // zset! {},
-    ] as [_; STEPS])
+    ] as [OrdZSet<Tup4<usize, usize, usize, usize>>; STEPS])
         .into_iter();
 
     for i in 0..STEPS {

diff --git a/crates/dbsp/examples/tutorial/tutorial11.rs b/crates/dbsp/examples/tutorial/tutorial11.rs
@@ -1,4 +1,5 @@
 use anyhow::Result;
+use dbsp::OrdZSet;
 use dbsp::typed_batch::IndexedZSetReader;
 use dbsp::{
     Circuit, NestedCircuit, OrdIndexedZSet, Runtime, Stream, indexed_zset,
@@ -32,7 +33,7 @@ fn main() -> Result<()> {
                 //  |                                   |
                 //  ------------------3------------------
                 zset_set! { Tup3(4, 0, 3)}
-            ] as [_; STEPS])
+            ] as [OrdZSet<Tup3<usize, usize, usize>>; STEPS])
                 .into_iter();
 
             let edges = root_circuit.add_source(Generator::new(move || edges_data.next().unwrap()));

diff --git a/crates/dbsp/examples/tutorial/tutorial12/README.md b/crates/dbsp/examples/tutorial/tutorial12/README.md
@@ -0,0 +1,166 @@
+# Tutorial 12
+
+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:
+
+```dl
+// 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](https://souffle-lang.github.io) 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:
+
+```sh
+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:
+
+```sh
+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:
+
+```sh
+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:
+
+```sh
+cargo run --example tutorial12
+```
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_1/ActualArg.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_1/ActualArg.facts
@@ -0,0 +1,3 @@
+site,arg
+s1,d
+s2,ac
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_1/Alloc.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_1/Alloc.facts
@@ -0,0 +1,4 @@
+var,obj
+g,oG
+d,oDog
+c,oCat
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_1/Assign.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_1/Assign.facts
@@ -0,0 +1,2 @@
+dst,src
+ac,c
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_1/Dispatch.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_1/Dispatch.facts
@@ -0,0 +1,4 @@
+site,recv,sig
+Greeter,greet,Greeter.greet
+Dog,speak,Dog.speak
+Cat,speak,Cat.speak
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_1/FormalParam.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_1/FormalParam.facts
@@ -0,0 +1,2 @@
+meth,param
+Greeter.greet,x
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_1/HeapType.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_1/HeapType.facts
@@ -0,0 +1,4 @@
+obj,ty
+oG,Greeter
+oDog,Dog
+oCat,Cat
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_1/VirtualCall.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_1/VirtualCall.facts
@@ -0,0 +1,4 @@
+site,recv,sig
+s1,g,greet
+s2,g,greet
+s3,x,speak
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_2/ActualArg.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_2/ActualArg.facts
@@ -0,0 +1,4 @@
+site,arg
+s1,d
+s2,ac
+s4,m
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_2/Alloc.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_2/Alloc.facts
@@ -0,0 +1,5 @@
+var,obj
+g,oG
+d,oDog
+c,oCat
+m,oMouse
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_2/Assign.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_2/Assign.facts
@@ -0,0 +1,2 @@
+dst,src
+ac,c
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_2/Dispatch.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_2/Dispatch.facts
@@ -0,0 +1,5 @@
+site,recv,sig
+Greeter,greet,Greeter.greet
+Dog,speak,Dog.speak
+Cat,speak,Cat.speak
+Mouse,speak,Mouse.speak
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_2/FormalParam.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_2/FormalParam.facts
@@ -0,0 +1,2 @@
+meth,param
+Greeter.greet,x
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_2/HeapType.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_2/HeapType.facts
@@ -0,0 +1,5 @@
+obj,ty
+oG,Greeter
+oDog,Dog
+oCat,Cat
+oMouse,Mouse
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_2/VirtualCall.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_2/VirtualCall.facts
@@ -0,0 +1,5 @@
+site,recv,sig
+s1,g,greet
+s2,g,greet
+s3,x,speak
+s4,g,greet
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_3/ActualArg.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_3/ActualArg.facts
@@ -0,0 +1,3 @@
+site,arg
+s1,d
+s4,m
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_3/Alloc.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_3/Alloc.facts
@@ -0,0 +1,5 @@
+var,obj
+g,oG
+d,oDog
+c,oCat
+m,oMouse
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_3/Assign.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_3/Assign.facts
@@ -0,0 +1 @@
+dst,src
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_3/Dispatch.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_3/Dispatch.facts
@@ -0,0 +1,5 @@
+site,recv,sig
+Greeter,greet,Greeter.greet
+Dog,speak,Dog.speak
+Cat,speak,Cat.speak
+Mouse,speak,Mouse.speak
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_3/FormalParam.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_3/FormalParam.facts
@@ -0,0 +1,2 @@
+meth,param
+Greeter.greet,x
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_3/HeapType.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_3/HeapType.facts
@@ -0,0 +1,5 @@
+obj,ty
+oG,Greeter
+oDog,Dog
+oCat,Cat
+oMouse,Mouse
diff --git a/crates/dbsp/examples/tutorial/tutorial12/data_step_3/VirtualCall.facts b/crates/dbsp/examples/tutorial/tutorial12/data_step_3/VirtualCall.facts
@@ -0,0 +1,4 @@
+site,recv,sig
+s1,g,greet
+s3,x,speak
+s4,g,greet
diff --git a/crates/dbsp/examples/tutorial/tutorial12/program_analysis.dl b/crates/dbsp/examples/tutorial/tutorial12/program_analysis.dl
@@ -0,0 +1,53 @@
+//============================================================================
+// Run: souffle program_analysis.dl --fact-dir data_step_{1,2,3}
+//============================================================================
+
+//--------------------------- Input relations (EDB) --------------------------
+.decl Alloc(var:symbol, obj:symbol)                         // var = new ...   (obj = alloc site)
+.input Alloc(delimiter=",", headers=true)
+.decl Assign(dst:symbol, src:symbol)                        // dst = src
+.input Assign(delimiter=",", headers=true)
+.decl VirtualCall(site:symbol, recv:symbol, sig:symbol)     // recv.sig(...) at `site`
+.input VirtualCall(delimiter=",", headers=true)
+.decl HeapType(obj:symbol, ty:symbol)                       // runtime type of an allocated object
+.input HeapType(delimiter=",", headers=true)
+.decl Dispatch(ty:symbol, sig:symbol, meth:symbol)          // type + signature -> method
+.input Dispatch(delimiter=",", headers=true)
+.decl ActualArg(site:symbol, arg:symbol)                    // argument variable passed at a call
+.input ActualArg(delimiter=",", headers=true)
+.decl FormalParam(meth:symbol, param:symbol)                // a method's parameter variable
+.input FormalParam(delimiter=",", headers=true)
+
+//------------------------- Derived relations (IDB) --------------------------
+.decl VarPointsTo(var:symbol, obj:symbol)
+.decl CallGraph(site:symbol, meth:symbol)
+.output VarPointsTo(IO=stdout)
+.output CallGraph(IO=stdout)
+
+//--------------------------------- Rules ------------------------------------
+
+// A variable points to whatever it was directly allocated.
+VarPointsTo(V, Obj) :- Alloc(V, Obj).
+
+// Copies propagate points-to facts (transitively).
+VarPointsTo(Dst, Obj) :-
+    Assign(Dst, Src),
+    VarPointsTo(Src, Obj).
+
+// Once a call edge exists, the actual arguments flow into the callee's
+// formal parameters.
+//   --> this rule READS CallGraph and WRITES VarPointsTo, closing the loop.
+VarPointsTo(Param, Obj) :-
+    CallGraph(Site, Meth),
+    ActualArg(Site, Arg),
+    FormalParam(Meth, Param),
+    VarPointsTo(Arg, Obj).
+
+// Resolve a virtual call: look at what the receiver points to, take that
+// object's type, and dispatch the signature on that type.
+//   --> this rule READS VarPointsTo.
+CallGraph(Site, Meth) :-
+    VirtualCall(Site, Recv, Sig),
+    VarPointsTo(Recv, Obj),
+    HeapType(Obj, Ty),
+    Dispatch(Ty, Sig, Meth).
-Original file line number
+Diff line change
@@ -0,0 +1,4 @@
+    var,obj
+    g,oG
+    d,oDog
+    c,oCat