Add an optional Soufflé backend

[ecstatic-morse]

Allows polonius to execute Datalog programs directly using Soufflé.

In the long term, that means:

• We can test that the results of our datafrog computations are correct, even intermediate ones like subset.
• We can prototype new ideas more quickly. No need to do stratification or re-indexing by hand before seeing results.

This PR binds to Soufflé's C++ interface using cxx. As a result, we can initialize relations and extract results entirely in memory; no need to write intermediate results to disk. If I were to start from scratch, I might choose generate Soufflé binaries instead of libraries and serialize everything on tmpfs. It took a lot of work to get cxx, Rust, and the generated C++ code to play nicely.

This adds an Engine enum that can be used to select between the 🐸 and 🍮 (no "souffle" emoji unfortunately) backends. Algorithm variants that are implemented in 🍮 take an Engine field now, which can be changed to 🍮 by adding the -Souffle suffix to the -A command line argument or env variable. 🍮 is gated behind a feature flag (polonius-souffle) and is off by default, since it requires a working souffle installation. The frontend types will still be available when the feature is disabled, but trying to compute using them will cause a runtime panic. Both configurations (with and without the feature) are tested on CI.

We do comparison tests on the output of the Souffle versions of DatafrogOpt and Naive. LocationInsensitive is a no-brainer, I just haven't copied those rules over yet.

This is not the cleanest integration, and I wish I could share more code for dumping intermediate facts, checking results, etc. I think it's okay for an MVP though.

[ecstatic-morse]

@lqd @nikomatsakis Ready for review 😟.

It looks like there's a bug in the optimized variant of the datalog rules. I'll try to figure it out.

[ecstatic-morse]

It's starting to seem like there's a typo or a transcription error in the optimized rules. Both 🍮 and 🐸 compute the same number of subset facts for vec_push_ref::foo1, but don't agree on the other intermediate relations, specifically dying_can_reach.

Datafrog

# live_to_dying_regions
# 1
"\'_#10r"	"\'_#16r"	"Mid(bb11[5])"	"Start(bb12[0])"
# dying_region_requires
# 11
"\'_#6r"	"Mid(bb6[3])"	"Start(bb6[4])"	"bw0"
"\'_#7r"	"Mid(bb11[2])"	"Start(bb11[3])"	"bw1"
"\'_#10r"	"Mid(bb12[4])"	"Start(bb8[0])"	"bw0"
"\'_#14r"	"Mid(bb6[7])"	"Start(bb8[0])"	"bw0"
"\'_#14r"	"Mid(bb7[1])"	"Start(bb10[0])"	"bw0"
"\'_#14r"	"Mid(bb9[0])"	"Start(bb10[0])"	"bw0"
"\'_#14r"	"Mid(bb11[4])"	"Start(bb11[5])"	"bw0"
"\'_#15r"	"Mid(bb11[5])"	"Start(bb8[0])"	"bw1"
"\'_#15r"	"Mid(bb11[5])"	"Start(bb12[0])"	"bw1"
"\'_#17r"	"Mid(bb11[5])"	"Start(bb8[0])"	"bw0"
"\'_#17r"	"Mid(bb11[5])"	"Start(bb12[0])"	"bw0"
# dying_can_reach
# 17
"\'_#17r"	"\'_#10r"	"Mid(bb11[5])"	"Start(bb8[0])"
"\'_#16r"	"\'_#10r"	"Mid(bb11[5])"	"Start(bb12[0])"
"\'_#17r"	"\'_#10r"	"Mid(bb11[5])"	"Start(bb12[0])"
"\'_#6r"	"\'_#14r"	"Mid(bb6[3])"	"Start(bb6[4])"
"\'_#7r"	"\'_#15r"	"Mid(bb11[2])"	"Start(bb11[3])"
"\'_#17r"	"\'_#16r"	"Mid(bb11[5])"	"Start(bb8[0])"
"\'_#16r"	"\'_#16r"	"Mid(bb11[5])"	"Start(bb12[0])"
"\'_#17r"	"\'_#16r"	"Mid(bb11[5])"	"Start(bb12[0])"
"\'_#14r"	"\'_#17r"	"Mid(bb11[4])"	"Start(bb11[5])"
"\'_#17r"	"\'_#8r"	"Mid(bb11[5])"	"Start(bb8[0])"
"\'_#16r"	"\'_#8r"	"Mid(bb11[5])"	"Start(bb12[0])"
"\'_#17r"	"\'_#8r"	"Mid(bb11[5])"	"Start(bb12[0])"
"\'_#15r"	"\'_#22r"	"Mid(bb11[5])"	"Start(bb8[0])"
"\'_#17r"	"\'_#22r"	"Mid(bb11[5])"	"Start(bb8[0])"
"\'_#15r"	"\'_#22r"	"Mid(bb11[5])"	"Start(bb12[0])"
"\'_#16r"	"\'_#22r"	"Mid(bb11[5])"	"Start(bb12[0])"
"\'_#17r"	"\'_#22r"	"Mid(bb11[5])"	"Start(bb12[0])"
# dying_can_reach_live
# 5
"\'_#6r"	"\'_#14r"	"Mid(bb6[3])"	"Start(bb6[4])"
"\'_#7r"	"\'_#15r"	"Mid(bb11[2])"	"Start(bb11[3])"
"\'_#14r"	"\'_#17r"	"Mid(bb11[4])"	"Start(bb11[5])"
"\'_#16r"	"\'_#10r"	"Mid(bb11[5])"	"Start(bb12[0])"
"\'_#17r"	"\'_#10r"	"Mid(bb11[5])"	"Start(bb12[0])"
# dead_borrow_can_reach_root
# 2
"\'_#6r"	"Mid(bb6[3])"	"bw0"
"\'_#7r"	"Mid(bb11[2])"	"bw1"
# dead_borrow_can_reach_dead
# 4
"\'_#6r"	"Mid(bb6[3])"	"bw0"
"\'_#7r"	"Mid(bb11[2])"	"bw1"
"\'_#14r"	"Mid(bb6[3])"	"bw0"
"\'_#15r"	"Mid(bb11[2])"	"bw1"

Souffle

# live_to_dying_regions
# 1
"\'_#10r"	"\'_#16r"	"Mid(bb11[5])"	"Start(bb12[0])"
# dying_region_requires
# 0
# dying_can_reach
# 4
"\'_#16r"	"\'_#10r"	"Mid(bb11[5])"	"Start(bb12[0])"
"\'_#16r"	"\'_#16r"	"Mid(bb11[5])"	"Start(bb12[0])"
"\'_#16r"	"\'_#8r"	"Mid(bb11[5])"	"Start(bb12[0])"
"\'_#16r"	"\'_#22r"	"Mid(bb11[5])"	"Start(bb12[0])"
# dying_can_reach_live
# 1
"\'_#16r"	"\'_#10r"	"Mid(bb11[5])"	"Start(bb12[0])"
# dead_borrow_region_can_reach_root
# 2
"\'_#6r"	"Mid(bb6[3])"	"bw0"
"\'_#7r"	"Mid(bb11[2])"	"bw1"
# dead_borrow_region_can_reach_dead
# 4
"\'_#6r"	"Mid(bb6[3])"	"bw0"
"\'_#7r"	"Mid(bb11[2])"	"bw1"
"\'_#14r"	"Mid(bb6[3])"	"bw0"
"\'_#15r"	"Mid(bb11[2])"	"bw1"

If the problem really is that they were written down incorrectly in datafrog_opt, I don't think I'm going to be able to fix it: the tuple re-indexing makes the datafrog version inscrutable to me.

[lqd]

There was this datafrog join using another join's intermediate relation, that I thought we may have commented incorrectly, but it seemed equivalent to the datalog rules, and unrelated to dying_can_reach in any case.

It's been so long that I don't remember if we actually tested these opt rules in soufflé (my recollection is: I probably only did use the Naive rules, but maybe Niko did use the Opt ones), and the old datalog version of the opt variant I have looks too old/incorrect (at some point there also were differences between Naive and Opt in some edge cases, and these bugs have since been fixed).

I'll also try to look at these rules.

[lqd]

I've noticed this: dying_can_reach depends on a few relations that seem to be correct with soufflé, and dying_can_reach_origins which I expect to cause issues. This relation must be different between the 2 versions, right ?

dying_can_reach_origins is:

• rule 1: datafrog-opt and soufflé seem to match
• rule 2: datafrog-opt, but it's not present in the soufflé version ?

Maybe this rule wasn't extracted because of the _loan syntax used here, rather than _ elsewhere ? (I'm not sure how you created the opt.dl file)

dying_can_reach_origins(origin, point1, point2) :-
   dying_region_requires(origin, point1, point2, _loan).

[ecstatic-morse]

Ah, good find! I started looking for more missing rules and found that the base case for requires also got lost. That should fix it.

To extract the datalog, I just stripped everything that wasn't a comment from the relevant part of the .rs file and then rearranged things manually. I'm not sure how I messed that up.

[lqd]

🎉