souffle icon indicating copy to clipboard operation
souffle copied to clipboard

"inline" causes assertion failure "functor type not set"

Open DerZc opened this issue 3 years ago • 3 comments

Hi,

The following program meets assertion failure:

.decl xxjm(A:unsigned)
.decl muis(A:number, B:unsigned)
.decl nngh(A:number, B:unsigned, C:number, D:unsigned, E:unsigned, F:unsigned, G:number, H:unsigned) btree
.decl mspn(A:number, B:unsigned, C:unsigned) no_magic
.decl bcqg(A:number, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:number) magic brie
.decl fpfy(A:unsigned, B:number, C:number, D:unsigned, E:number, F:unsigned, G:unsigned) no_magic
.decl kyqo(A:number, B:unsigned, C:unsigned)
.decl jsse(A:unsigned, B:number, C:number, D:number, E:number, F:number, G:number)
.decl hfay(A:unsigned, B:number)
.decl mhve(A:unsigned, B:number) magic brie
.decl male(A:unsigned, B:unsigned, C:unsigned, D:number, E:number, F:unsigned) btree
.decl ayin(A:unsigned, B:unsigned, C:number, D:number, E:unsigned, F:number, G:unsigned, H:unsigned) no_inline
.decl mzre(A:unsigned, B:unsigned, C:number, D:unsigned, E:number, F:unsigned, G:number) btree
.decl ygvr(A:number, B:unsigned, C:unsigned, D:number, E:unsigned, F:number, G:unsigned) inline
.decl omfk(A:number, B:number, C:unsigned, D:number) brie
.decl amys(A:unsigned, B:number, C:unsigned) no_inline
.decl hiut(A:unsigned, B:number, C:number, D:unsigned, E:unsigned, F:unsigned, G:unsigned) brie
.decl dxpz(A:unsigned, B:number, C:number, D:number) brie
.decl puau(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned) brie
.decl kbgx(A:number, B:number, C:number, D:number) no_inline btree
.decl pcao(A:unsigned, B:number, C:unsigned, D:number, E:unsigned, F:number, G:number) no_inline brie
.decl zwdd(A:unsigned, B:number, C:unsigned, D:number)
.decl tcgd(A:number, B:unsigned, C:unsigned, D:number) brie
.decl gvvz(A:unsigned, B:unsigned, C:number, D:unsigned, E:number, F:unsigned)
.decl vcgb(A:number, B:number) btree
.decl zriq(A:unsigned, B:number, C:unsigned, D:unsigned, E:number, F:unsigned) no_inline
.decl anqy(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned, G:unsigned) magic brie
.decl lzrn(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned) btree
.decl unou(A:unsigned, B:number, C:number, D:number, E:unsigned)
.decl aqon(A:number, B:unsigned, C:unsigned, D:number)
.decl leuh(A:unsigned, B:unsigned) btree
.decl vumz(A:number, B:unsigned, C:number, D:number, E:unsigned, F:number, G:number, H:number) no_magic btree
.decl jfui(A:unsigned, B:number, C:unsigned, D:unsigned, E:number, F:number, G:number, H:unsigned) btree
.decl xxdo(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:number, F:unsigned, G:number) inline
.decl zyps(A:unsigned, B:unsigned, C:unsigned, D:number, E:number, F:number, G:number, H:unsigned) no_magic brie
.decl gvae(A:number) brie
.decl uzdp(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned) inline btree
.decl kxiu(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned, G:unsigned)
.decl igst(A:unsigned, B:unsigned) btree
.decl tynw(A:unsigned, B:unsigned)
.decl pvzo(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned) brie
.decl ymmi(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned, G:unsigned, H:number) brie
.decl tzwg(A:number, B:unsigned, C:number, D:unsigned, E:unsigned, F:number)
.decl nsur(A:unsigned, B:number, C:number, D:number, E:unsigned)
.decl yfeh(A:number, B:number, C:number, D:number, E:number, F:number) no_magic
.decl pzyc(A:unsigned, B:unsigned) brie


xxjm(3).
xxjm(8).
xxjm(0).
xxjm(0).
xxjm(2).
xxjm(8).
xxjm(4).
muis(-8, 7).
muis(-3, 10).
muis(4, 2).
muis(6, 0).
muis(6, 1).
muis(-4, 2).
muis(-3, 2).


nngh(A, C, A, C, C, C, A, B) :- xxjm(C), muis(A, C), muis(A, B).
mspn(C, E, F) :- nngh(A, D, C, J, J, J, B, H), nngh(C, F, B, E, F, J, A, F).
bcqg(A, B, B, B, B, A) :- mspn(A, B, B).
fpfy(C, B, B, G, A, E, E) :- mspn(B, E, C), bcqg(A, E, C, D, G, B).
kyqo(A, C, B) :- bcqg(A, B, C, C, B, A).
jsse(B, A, A, A, A, A, A) :- muis(A, B).
hfay(C, A) :- bcqg(B, E, E, F, E, A), kyqo(A, C, C).
mhve(E, B) :- bcqg(B, C, E, F, F, B), nngh(A, D, A, E, F, C, A, F).
male(D, C, C, B, A, C) :- mhve(E, A), bcqg(A, C, C, D, C, B), xxjm(D).
ayin(B, B, A, A, B, A, B, B) :- muis(A, B).
mzre(E, D, B, D, B, D, B) :- hfay(D, B), kyqo(B, D, C), mhve(E, B).
ygvr(A, F, E, D, E, A, F) :- nngh(A, E, D, E, F, F, C, E), male(E, F, F, C, A, F), xxjm(F).
omfk(A, A, B, A) :- hfay(B, A).
amys(E, B, F) :- male(E, E, F, D, D, F), mspn(C, E, F), ayin(G, E, C, C, E, B, F, G).
hiut(E, B, B, D, D, E, E) :- fpfy(2, B, B, E, B, E, D).
dxpz(E, A, C, B) :- hfay(2, A), muis(A, E), ygvr(A, E, E, B, D, C, E).
puau(A, A, A, A, A) :- xxjm(A).
kbgx(A, D, D, B) :- jsse(E, D, A, B, D, C, A), mhve(E, B).
pcao(B, A, B, A, B, A, A) :- muis(A, B).
zwdd(F, B, E, A) :- male(F, H, E, A, B, I), bcqg(B, 2, E, F, J, A), hiut(E, B, B, J, D, J, G).
tcgd(B, D, F, B) :- jsse(D, B, B, C, B, B, B), bcqg(A, F, D, E, D, B), B > sum BBB : { dxpz(CCC, AAA, BBB, AAA), 7 <= BBB, to_number("-3") >= AAA}.
gvvz(C, B, A, D, A, D) :- bcqg(A, B, C, D, C, A), A != count : {amys(BBB, AAA, BBB), to_number("6") > AAA}.
vcgb(B, C) :- mspn(D, F, F), bcqg(C, F, G, E, F, A), male(E, E, E, B, B, G).
zriq(C, A, D, D, A, D) :- tcgd(A, D, C, A), kyqo(B, C, D), 0 = 0.
anqy(A, A, A, B, A, A, A) :- puau(A, A, B, A, A), puau(B, A, A, B, A).
lzrn(A, A, B, A, B, A) :- puau(A, B, B, B, A).
unou(C, B, B, B, C) :- ayin(C, C, A, B, C, B, C, D), !zriq(C, B, C, C, B, C).
aqon(bnot -A, C, D, A) :- fpfy(D, A, A, C, A, C, C).
leuh(H, H) :- male(H, I, L, D, D, G), unou(K, D, B, E, H), nngh(A, F, A, F, G, H, B, H).
vumz(E, J, E, A, J, D, D, A) :- jsse(J, _, D, A, H, G, C), unou(J, D, E, B, J), unou(J, E, A, B, L).
jfui(K, B, N, H, A, E, E, M) :- mspn(B, F, M), ygvr(A, J, N, E, H, A, L), hiut(I, B, E, H, K, G, M).
xxdo(I, G, I, G, C, H, A) :- mhve(G, C), vcgb(A, C), pcao(H, E, I, A, I, B, A), !mspn(A, I, I).
zyps(B, B, B, A, A, A, A, B) :- bcqg(A, B, B, B, B, A).
gvae(B) :- gvvz(J, I, G, K, A, I), zyps(K, H, H, D, F, C, B, K), jsse(H, B, E, F, B, B, E), !pcao(H, F, H, E, H, F, A).
uzdp(C, C, B, C, C) :- anqy(C, C, C, A, A, B, C).
kxiu(C, A, B, B, C, C, B) :- uzdp(B, C, C, B, A).
igst(H, H) :- zriq(H, A, G, F, A, H), ygvr(B, G, H, B, F, A, H), ayin(G, H, A, A, H, A, H, H).
tynw(C, C) :- uzdp(D, B, B, B, D), uzdp(C, C, B, C, C).
pvzo(A, B, A, B, A) :- lzrn(B, B, A, A, A, B).
ymmi(C, C, D, C, C, C, C, B) :- xxjm(D), tcgd(B, C, C, B), hfay(E, A).
tzwg(A, C, A, D, C, B) :- fpfy(C, A, A, D, B, C, D).
nsur(B, A, A, A, B) :- tcgd(A, B, B, A).
yfeh(B, B, A, A, B, A) :- kbgx(B, A, A, A).
pzyc(B, min(max(B,B),8)) :- uzdp(B, B, A, C, 8).

.output pzyc

I run it with souffle -w example.dl, and the output is:

souffle: /souffle/src/ast/analysis/typesystem/Type.cpp:309: souffle::FunctorOp souffle::ast::analysis::TypeAnalysis::getPolymorphicOperator(const souffle::ast::IntrinsicFunctor&) const: Assertion `hasValidTypeInfo(inf) && "functor type not set"' failed.

If I remove the inline keyword of uzdp, the program can execute correctly. I use the last release version of Souffle.

DerZc avatar Oct 19 '22 07:10 DerZc

Hi,

I reduce this test case:

.decl a(b:unsigned)
.decl h(c:unsigned, d:unsigned) inline
.decl i(c:unsigned) 

a(0).

h(d, d) :- a(d).
i(min(max(c,c),8)) :- h(c, 8).

.output i

I guess it's probably because the inline subgoal contains constants.

DerZc avatar Oct 21 '22 15:10 DerZc

I am not sure about the reason, because I find this test case also can trigger the bug:

.decl a(x:unsigned) inline
.decl b(x:unsigned)

a(0).
b(max(max(x,0),0)) :- a(x).

.output b

DerZc avatar Oct 31 '22 01:10 DerZc

There is no valid overload for max(unsigned, number) in max(x,0) because 0 is a signed number.

Either replace all literals 0 by 0u, or make x a number.

Souffle should not crash/raise an assertion. It should report that there is no valid overload.

quentin avatar Nov 28 '23 04:11 quentin