From 5efcfa3ce2613cf5f0b7b9d665cdf964b3e2c8c1 Mon Sep 17 00:00:00 2001 From: Leo Stewen Date: Mon, 22 Jun 2026 11:50:07 +0100 Subject: [PATCH] [DBSP] Fix tutorial 10 and 11. Add tutorial 12 on mutual recursion with DBSP. --- crates/dbsp/Cargo.toml | 4 + crates/dbsp/examples/tutorial/tutorial10.rs | 4 +- crates/dbsp/examples/tutorial/tutorial11.rs | 3 +- .../examples/tutorial/tutorial12/README.md | 166 +++++++ .../tutorial12/data_step_1/ActualArg.facts | 3 + .../tutorial12/data_step_1/Alloc.facts | 4 + .../tutorial12/data_step_1/Assign.facts | 2 + .../tutorial12/data_step_1/Dispatch.facts | 4 + .../tutorial12/data_step_1/FormalParam.facts | 2 + .../tutorial12/data_step_1/HeapType.facts | 4 + .../tutorial12/data_step_1/VirtualCall.facts | 4 + .../tutorial12/data_step_2/ActualArg.facts | 4 + .../tutorial12/data_step_2/Alloc.facts | 5 + .../tutorial12/data_step_2/Assign.facts | 2 + .../tutorial12/data_step_2/Dispatch.facts | 5 + .../tutorial12/data_step_2/FormalParam.facts | 2 + .../tutorial12/data_step_2/HeapType.facts | 5 + .../tutorial12/data_step_2/VirtualCall.facts | 5 + .../tutorial12/data_step_3/ActualArg.facts | 3 + .../tutorial12/data_step_3/Alloc.facts | 5 + .../tutorial12/data_step_3/Assign.facts | 1 + .../tutorial12/data_step_3/Dispatch.facts | 5 + .../tutorial12/data_step_3/FormalParam.facts | 2 + .../tutorial12/data_step_3/HeapType.facts | 5 + .../tutorial12/data_step_3/VirtualCall.facts | 4 + .../tutorial/tutorial12/program_analysis.dl | 53 +++ .../tutorial/tutorial12/tutorial12.rs | 406 ++++++++++++++++++ crates/dbsp/src/tutorial.rs | 13 +- 28 files changed, 721 insertions(+), 4 deletions(-) create mode 100644 crates/dbsp/examples/tutorial/tutorial12/README.md create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_1/ActualArg.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_1/Alloc.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_1/Assign.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_1/Dispatch.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_1/FormalParam.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_1/HeapType.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_1/VirtualCall.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_2/ActualArg.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_2/Alloc.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_2/Assign.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_2/Dispatch.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_2/FormalParam.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_2/HeapType.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_2/VirtualCall.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_3/ActualArg.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_3/Alloc.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_3/Assign.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_3/Dispatch.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_3/FormalParam.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_3/HeapType.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/data_step_3/VirtualCall.facts create mode 100644 crates/dbsp/examples/tutorial/tutorial12/program_analysis.dl create mode 100644 crates/dbsp/examples/tutorial/tutorial12/tutorial12.rs diff --git a/crates/dbsp/Cargo.toml b/crates/dbsp/Cargo.toml index d820af34634..8af54c76821 100644 --- 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 index 005bdffb659..38090af4e62 100644 --- 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>; 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>; STEPS]) .into_iter(); for i in 0..STEPS { diff --git a/crates/dbsp/examples/tutorial/tutorial11.rs b/crates/dbsp/examples/tutorial/tutorial11.rs index 8b3f01368b4..09580d4b1ea 100644 --- 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>; 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 new file mode 100644 index 00000000000..1bed451b49b --- /dev/null +++ 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 new file mode 100644 index 00000000000..1bfd659c257 --- /dev/null +++ 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 new file mode 100644 index 00000000000..cadadee1331 --- /dev/null +++ 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 new file mode 100644 index 00000000000..b5d2643f2b3 --- /dev/null +++ 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 new file mode 100644 index 00000000000..45fb55b8076 --- /dev/null +++ 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 new file mode 100644 index 00000000000..96030e0c01e --- /dev/null +++ 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 new file mode 100644 index 00000000000..a376ee59bb6 --- /dev/null +++ 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 new file mode 100644 index 00000000000..a3ee6486edf --- /dev/null +++ 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 new file mode 100644 index 00000000000..29622479d0f --- /dev/null +++ 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 new file mode 100644 index 00000000000..ca517628b6d --- /dev/null +++ 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 new file mode 100644 index 00000000000..b5d2643f2b3 --- /dev/null +++ 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 new file mode 100644 index 00000000000..111d4a44d1b --- /dev/null +++ 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 new file mode 100644 index 00000000000..96030e0c01e --- /dev/null +++ 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 new file mode 100644 index 00000000000..7a9a123bb34 --- /dev/null +++ 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 new file mode 100644 index 00000000000..6f39b499aa4 --- /dev/null +++ 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 new file mode 100644 index 00000000000..3c02e13c0ae --- /dev/null +++ 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 new file mode 100644 index 00000000000..ca517628b6d --- /dev/null +++ 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 new file mode 100644 index 00000000000..e08ed75eac6 --- /dev/null +++ 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 new file mode 100644 index 00000000000..111d4a44d1b --- /dev/null +++ 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 new file mode 100644 index 00000000000..96030e0c01e --- /dev/null +++ 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 new file mode 100644 index 00000000000..7a9a123bb34 --- /dev/null +++ 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 new file mode 100644 index 00000000000..28c2261e169 --- /dev/null +++ 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 new file mode 100644 index 00000000000..e601ffea506 --- /dev/null +++ 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). diff --git a/crates/dbsp/examples/tutorial/tutorial12/tutorial12.rs b/crates/dbsp/examples/tutorial/tutorial12/tutorial12.rs new file mode 100644 index 00000000000..696966a542d --- /dev/null +++ b/crates/dbsp/examples/tutorial/tutorial12/tutorial12.rs @@ -0,0 +1,406 @@ +use anyhow::Result; +use dbsp::typed_batch::IndexedZSetReader; +use dbsp::{ + NestedCircuit, Runtime, Stream, + utils::{Tup2, Tup3}, +}; +use dbsp::{OrdZSet, ZWeight, zset}; + +// Some helper types. +type WeightedValue = Tup2; +type String2 = Tup2; +type String3 = Tup3; + +// And some helper functions. +fn owned_string2(((s1, s2), weight): ((&str, &str), ZWeight)) -> WeightedValue { + Tup2(Tup2(s1.to_owned(), s2.to_owned()), weight) +} +fn owned_string3(((s1, s2, s3), weight): ((&str, &str, &str), ZWeight)) -> WeightedValue { + Tup2(Tup3(s1.to_owned(), s2.to_owned(), s3.to_owned()), weight) +} + +fn main() -> Result<()> { + const STEPS: usize = 3; + + let threads = std::thread::available_parallelism() + .map(|n| n.get()) + .unwrap_or(4); + + let ( + mut circuit, + ( + ( + alloc_input, + assign_input, + virtual_call_input, + heap_type_input, + dispatch_input, + actual_arg_input, + formal_param_input, + ), + (var_points_to_output, call_graph_output), + ), + ) = Runtime::init_circuit(threads, move |root_circuit| { + let (alloc, alloc_input) = root_circuit.add_input_zset::(); + let (assign, assign_input) = root_circuit.add_input_zset::(); + let (virtual_call, virtual_call_input) = root_circuit.add_input_zset::(); + let (heap_type, heap_type_input) = root_circuit.add_input_zset::(); + let (dispatch, dispatch_input) = root_circuit.add_input_zset::(); + let (actual_arg, actual_arg_input) = root_circuit.add_input_zset::(); + let (formal_param, formal_param_input) = root_circuit.add_input_zset::(); + + let (var_points_to, call_graph) = root_circuit.recursive( + // Note that recursive has an implicit distinct (see its Docs)! + |child_circuit, + // var_points_to and call_graph are the recursive computations we are + // interested in. + (var_points_to, call_graph): ( + Stream>, + Stream>, + )| { + // Import streams from the parent circuit into the child circuit. + let alloc = alloc.delta0(child_circuit); + let assign = assign.delta0(child_circuit); + let virtual_call = virtual_call.delta0(child_circuit); + let heap_type = heap_type.delta0(child_circuit); + let dispatch = dispatch.delta0(child_circuit); + let actual_arg = actual_arg.delta0(child_circuit); + let formal_param = formal_param.delta0(child_circuit); + + // call_graph_next computes this Datalog query: + // CallGraph(Site, Meth) :- + // VirtualCall(Site, Recv, Sig), + // VarPointsTo(Recv, Obj), + // HeapType(Obj, Ty), + // Dispatch(Ty, Sig, Meth). + let call_graph_next = virtual_call + .map_index(|Tup3(site, recv, sig)| { + (recv.clone(), Tup3(site.clone(), recv.clone(), sig.clone())) + }) + .join_index( + // 1. virtual_call JOIN var_points_to ON recv + // Mutual recursion: call_graph uses var_points_to + &var_points_to.map_index(|Tup2(recv, obj)| { + (recv.clone(), Tup2(recv.clone(), obj.clone())) + }), + |_recv, Tup3(site, _, sig), Tup2(_, obj)| { + Some((obj.clone(), Tup3(site.clone(), sig.clone(), obj.clone()))) + }, + ) + .join_index( + // 2. ... JOIN heap_type ON obj + &heap_type.map_index(|Tup2(obj, ty)| { + (obj.clone(), Tup2(obj.clone(), ty.clone())) + }), + |_obj, Tup3(site, sig, _), Tup2(_, ty)| { + Some(( + Tup2(ty.clone(), sig.clone()), + Tup2(site.clone(), ty.clone()), + )) + }, + ) + .join_index( + // 3. ... JOIN dispatch ON ty and sig + &dispatch.map_index(|Tup3(ty, sig, meth)| { + (Tup2(ty.clone(), sig.clone()), meth.clone()) + }), + |_, Tup2(site, _), meth| { + Some(( + Tup2(site.clone(), meth.clone()), + Tup2(site.clone(), meth.clone()), + )) + }, + ); + + // var_points_to_next computes this Datalog query: + // VarPointsTo(V, Obj) :- Alloc(V, Obj). + // VarPointsTo(Dst, Obj) :- + // Assign(Dst, Src), + // VarPointsTo(Src, Obj). + // VarPointsTo(Param, Obj) :- + // CallGraph(Site, Meth), + // ActualArg(Site, Arg), + // FormalParam(Meth, Param), + // VarPointsTo(Arg, Obj). + let var_points_to_next = var_points_to // Recursion: var_points_to is also self-recursive + .map_index(|Tup2(src, obj)| (src.clone(), Tup2(src.clone(), obj.clone()))) + .join_index( + // var_points_to JOIN assign ON src + &assign.map_index(|Tup2(dst, src)| { + (src.clone(), Tup2(dst.clone(), src.clone())) + }), + |_src, Tup2(_, obj), Tup2(dst, _)| { + Some(( + Tup2(dst.clone(), obj.clone()), + Tup2(dst.clone(), obj.clone()), + )) + }, + ) + .plus( + // "base case": alloc feeds into var_points_to + &alloc.map_index(|Tup2(var, obj)| { + ( + Tup2(var.clone(), obj.clone()), + Tup2(var.clone(), obj.clone()), + ) + }), + ) + .plus( + // This argument to plus() computes this part of the Datalog query: + // VarPointsTo(Param, Obj) :- + // CallGraph(Site, Meth), + // ActualArg(Site, Arg), + // FormalParam(Meth, Param), + // VarPointsTo(Arg, Obj). + // Mutual recursion: var_points_to uses call_graph + &call_graph + .map_index(|Tup2(site, meth)| { + (site.clone(), Tup2(site.clone(), meth.clone())) + }) + .join_index( + // 1. call_graph JOIN actual_arg ON site + &actual_arg.map_index(|Tup2(site, arg)| { + (site.clone(), Tup2(site.clone(), arg.clone())) + }), + |_site, Tup2(_, meth), Tup2(_, arg)| { + Some((meth.clone(), Tup2(meth.clone(), arg.clone()))) + }, + ) + .join_index( + // .2. ... JOIN formal_param ON meth + &formal_param.map_index(|Tup2(meth, param)| { + (meth.clone(), Tup2(meth.clone(), param.clone())) + }), + |_meth, Tup2(_, arg), Tup2(_, param)| { + Some(((arg.clone()), Tup2(arg.clone(), param.clone()))) + }, + ) + .join_index( + // 3. ... JOIN var_points_to ON arg + &var_points_to.map_index(|Tup2(arg, obj)| { + (arg.clone(), Tup2(arg.clone(), obj.clone())) + }), + |_arg, Tup2(_, param), Tup2(_, obj)| { + Some(( + Tup2(param.clone(), obj.clone()), + Tup2(param.clone(), obj.clone()), + )) + }, + ), + ); + + Ok(( + var_points_to_next + .map(|(Tup2(param, obj), _)| Tup2(param.clone(), obj.clone())), + call_graph_next.map(|(Tup2(site, meth), _)| Tup2(site.clone(), meth.clone())), + )) + }, + )?; + + Ok(( + ( + alloc_input, + assign_input, + virtual_call_input, + heap_type_input, + dispatch_input, + actual_arg_input, + formal_param_input, + ), + ( + var_points_to.accumulate_output(), + call_graph.accumulate_output(), + ), + )) + })?; + + // Define the inputs at each "step". + + let mut alloc_inputs = ([ + vec![(("g", "oG"), 1), (("d", "oDog"), 1), (("c", "oCat"), 1)] + .into_iter() + .map(owned_string2) + .collect(), + vec![(("m", "oMouse"), 1)] + .into_iter() + .map(owned_string2) + .collect(), + vec![], + ] as [Vec>; STEPS]) + .into_iter(); + + let mut assign_inputs = ([ + vec![(("ac", "c"), 1)] + .into_iter() + .map(owned_string2) + .collect(), + vec![], + vec![(("ac", "c"), -1)] + .into_iter() + .map(owned_string2) + .collect(), + ] as [Vec>; STEPS]) + .into_iter(); + + let mut virtual_call_inputs = ([ + vec![ + (("s1", "g", "greet"), 1), + (("s2", "g", "greet"), 1), + (("s3", "x", "speak"), 1), + ] + .into_iter() + .map(owned_string3) + .collect(), + vec![(("s4", "g", "greet"), 1)] + .into_iter() + .map(owned_string3) + .collect(), + vec![(("s2", "g", "greet"), -1)] + .into_iter() + .map(owned_string3) + .collect(), + ] as [Vec>; STEPS]) + .into_iter(); + + let mut heap_type_inputs = ([ + vec![ + (("oG", "Greeter"), 1), + (("oDog", "Dog"), 1), + (("oCat", "Cat"), 1), + ] + .into_iter() + .map(owned_string2) + .collect(), + vec![(("oMouse", "Mouse"), 1)] + .into_iter() + .map(owned_string2) + .collect(), + vec![], + ] as [Vec>; STEPS]) + .into_iter(); + + let mut dispatch_inputs = ([ + vec![ + (("Greeter", "greet", "Greeter.greet"), 1), + (("Dog", "speak", "Dog.speak"), 1), + (("Cat", "speak", "Cat.speak"), 1), + ] + .into_iter() + .map(owned_string3) + .collect(), + vec![(("Mouse", "speak", "Mouse.speak"), 1)] + .into_iter() + .map(owned_string3) + .collect(), + vec![], + ] as [Vec>; STEPS]) + .into_iter(); + + let mut actual_arg_inputs = ([ + vec![(("s1", "d"), 1), (("s2", "ac"), 1)] + .into_iter() + .map(owned_string2) + .collect(), + vec![(("s4", "m"), 1)] + .into_iter() + .map(owned_string2) + .collect(), + vec![(("s2", "ac"), 1)] + .into_iter() + .map(owned_string2) + .collect(), + ] as [Vec>; STEPS]) + .into_iter(); + + let mut formal_param_inputs = ([ + vec![(("Greeter.greet", "x"), 1)] + .into_iter() + .map(owned_string2) + .collect(), + vec![], + vec![], + ] as [Vec>; STEPS]) + .into_iter(); + + // Define the expected outputs at each "step". + + let mut var_points_to_expected_outputs = ([ + zset! { + Tup2("ac".to_string(), "oCat".to_string()) => 1, + Tup2("c".to_string(), "oCat".to_string()) => 1, + Tup2("d".to_string(), "oDog".to_string()) => 1, + Tup2("g".to_string(), "oG".to_string()) => 1, + Tup2("x".to_string(), "oDog".to_string()) => 1, + Tup2("x".to_string(), "oCat".to_string()) => 1, + }, + zset! { + Tup2("m".to_string(), "oMouse".to_string()) => 1, + Tup2("x".to_string(), "oMouse".to_string()) => 1, + }, + zset! { + Tup2("ac".to_string(), "oCat".to_string()) => -1, + Tup2("x".to_string(), "oCat".to_string()) => -1, + }, + ] as [OrdZSet; STEPS]) + .into_iter(); + + let mut call_graph_expected_outputs = ([ + zset! { + Tup2("s1".to_string(), "Greeter.greet".to_string()) => 1, + Tup2("s2".to_string(), "Greeter.greet".to_string()) => 1, + Tup2("s3".to_string(), "Dog.speak".to_string()) => 1, + Tup2("s3".to_string(), "Cat.speak".to_string()) => 1, + }, + zset! { + Tup2("s3".to_string(), "Mouse.speak".to_string()) => 1, + Tup2("s4".to_string(), "Greeter.greet".to_string()) => 1, + }, + zset! { + Tup2("s2".to_string(), "Greeter.greet".to_string()) => -1, + Tup2("s3".to_string(), "Cat.speak".to_string()) => -1, + }, + ] as [OrdZSet; STEPS]) + .into_iter(); + + // Execute the circuit. + for i in 1..=STEPS { + // 1. Feed input data. + alloc_input.append(&mut alloc_inputs.next().unwrap()); + assign_input.append(&mut assign_inputs.next().unwrap()); + virtual_call_input.append(&mut virtual_call_inputs.next().unwrap()); + heap_type_input.append(&mut heap_type_inputs.next().unwrap()); + dispatch_input.append(&mut dispatch_inputs.next().unwrap()); + actual_arg_input.append(&mut actual_arg_inputs.next().unwrap()); + formal_param_input.append(&mut formal_param_inputs.next().unwrap()); + + // 2. Execute the transaction. + circuit.transaction()?; + + // 3. Print and check outputs. + println!("=== Outputs Iteration {i} ==="); + println!("=== VarPointsTo Output ==="); + let var_points_to_output = var_points_to_output.concat(); + var_points_to_output + .iter() + .for_each(|(Tup2(var, o_type), _, z_weight)| { + println!("var: {var} -> object_type: {o_type} => {z_weight}"); + }); + assert_eq!( + var_points_to_output.consolidate(), + var_points_to_expected_outputs.next().unwrap(), + ); + println!("=== CallGraph Output ==="); + let call_graph_output = call_graph_output.concat(); + call_graph_output + .iter() + .for_each(|(Tup2(call_site, method), _, z_weight)| { + println!("call_site {call_site} -> method {method} => {z_weight}"); + }); + assert_eq!( + call_graph_output.consolidate(), + call_graph_expected_outputs.next().unwrap(), + ); + } + + Ok(()) +} diff --git a/crates/dbsp/src/tutorial.rs b/crates/dbsp/src/tutorial.rs index ef218cb03dd..2c4d5887693 100644 --- a/crates/dbsp/src/tutorial.rs +++ b/crates/dbsp/src/tutorial.rs @@ -2002,7 +2002,10 @@ //! Fixed-point computations are useful if you want to repeat a query until //! its result does not change anymore. Then, a fixed-point is reached and //! the query processing terminates, yielding the result. SQL provides this -//! mechanism through recursive common table expressions (CTEs). +//! mechanism through recursive common table expressions (CTEs). DBSP supports +//! both self and mutual recursion. +//! +//! ## Fixed-Point Computation with Self-Recursion //! //! A classical use case for a fixed-point computation is the [transitive closure //! of a graph](https://en.wikipedia.org/wiki/Transitive_closure#In_graph_theory). @@ -2283,6 +2286,14 @@ //! optimum of the aggregation function (here, the minimum function), //! even though there exists a finite solution. //! +//! ## Fixed-Point Computation with Mutual Recursion +//! +//! The examples on the transitive closure above demonstrate how to express +//! self-recursive queries. DBSP also supports _mutually_-recursive queries. +//! As this is a little bit more involved than what would fit in here, we defer +//! the interested reader to the example given in `tutorial12` which +//! demonstrates mutual recursion in the domain of static program analysis. +//! //! # Next steps //! //! We've shown how input, computation, and output work in DBSP. That's all