HarvardPL / formulog

Datalog with support for SMT queries and first-order functional programming
https://harvardpl.github.io/formulog/
Apache License 2.0
155 stars 10 forks source link

Compiler generates invalid query plans #79

Open aaronbembenek opened 8 months ago

aaronbembenek commented 8 months ago

The Formulog-to-Souffle transpiler generates invalid query plans in the presence of the CODEGEN_PROJECT relation, which it seems to treat as being in the same stratum as the predicate being defined.

$ cat foo.flg
rel a(i32)
rel b(i32, i32)
b(3, 42).
a(0).
a(1).
a(X + 2) :- a(X), a(X + 1), !b(X + 2, _).
$ java -Doptimize=5 -jar target/formulog-0.7.0-SNAPSHOT-jar-with-dependencies.jar foo.flg -c
$ cd codegen
$ cmake -B build -S .
...
$ cmake --build build
-- Configuring done
-- Generating done
-- Build files have been written to: /root/codegen/build
[  6%] Generating formulog.cpp
Error: Invalid execution order in plan (expected 2 atoms, not 3) in file formulog.dl at line 30
.plan 0: (1,2,3), 1: (2,1,3)
---------^-------------------
Error: Invalid execution order in plan (expected 2 atoms, not 3) in file formulog.dl at line 30
.plan 0: (1,2,3), 1: (2,1,3)
---------------------^-------
2 errors generated, evaluation aborted
gmake[2]: *** [CMakeFiles/flg.dir/build.make:74: formulog.cpp] Error 1
gmake[1]: *** [CMakeFiles/Makefile2:82: CMakeFiles/flg.dir/all] Error 2
gmake: *** [Makefile:91: all] Error 2

The offending rule in the generated Souffle is

a_(@expr_5(X)) :-
        a_(X),
        a_(@expr_4(X)),
        !CODEGEN_PROJECT_b_10(@expr_5(X)).
.plan 0: (1,2,3), 1: (2,1,3)
aaronbembenek commented 8 months ago

Actually, it looks like this bug arises in the case of negation more generally, such as in this program:

rel a(i32)
rel b(i32)
b(2).
a(0).
a(1).
a(X + 2) :- a(X), !b(X).

The invalid query plan is here:

a_(@expr_4(X)) :-
        a_(X),
        !b_(X).
.plan 0: (1,2)

It works fine if the query plan is changed to

.plan 0: (1)

Surprisingly this program works okay:

rel a(i32)
rel b(i32)
b(2).
a(0).
a(1).
a(X) :- a(X), !b(X).

with the Souffle rule

a_(X) :-
        a_(X),
        !b_(X).
.plan 0: (1,2)

I'm not sure why Souffle accepts one rule but not the other. The surface difference is that there's a functor call in the head of the rule. Moreover, it seems like it's necessary for the functor call to use a variable to trigger the issue.

aaronbembenek commented 8 months ago

Query plans are applied after optimizations (https://github.com/souffle-lang/souffle/issues/2370), and so it risky for us to generate query plans since we do not know what optimizations Souffle will do. A safer alternative is that users specify a SIPS when they compile the Souffle program we generate.