Souffle crashed on aggregates

[DerZc]

Hi,

I have a program as below:

.decl ufdm(A:number, B:number)
.decl adaw(A:unsigned, B:number)
.decl ajha(A:number)
.decl wcvj(A:unsigned, B:unsigned)
.decl nzev(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned) btree
.decl edwj(A:number, B:unsigned) magic btree
.decl lroc(A:number, B:unsigned, C:number, D:number) no_magic btree
.decl zhob(A:number, B:number, C:unsigned, D:number, E:number, F:number) brie
.decl ihsf(A:number) no_magic
.decl pylt(A:number, B:number, C:number, D:number) btree
.decl zyuj(A:number, B:number, C:unsigned) brie
.decl qebx(A:unsigned, B:unsigned) brie
.decl iobl(A:unsigned, B:number) btree
.decl vvur(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned) magic
.decl ftbk(A:number, B:number, C:number, D:number)
.decl japo(A:unsigned, B:number) no_magic
.decl nxop(A:number, B:number) no_magic btree
.decl qpft(A:number, B:number) brie
.decl ykow(A:unsigned, B:number, C:unsigned, D:number, E:unsigned)
.decl vnjk(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned, G:unsigned)
.decl uhuk(A:unsigned, B:unsigned) btree
.decl stql(A:number, B:number, C:number, D:unsigned, E:number, F:unsigned, G:unsigned, H:unsigned) no_inline brie
.decl dsxz(A:unsigned) brie
.decl yhnz(A:unsigned, B:number, C:number, D:number, E:unsigned, F:unsigned, G:unsigned, H:number)
.decl ifmk(A:number, B:number, C:number) no_inline
.decl gcly(A:unsigned, B:unsigned, C:unsigned, D:number, E:unsigned, F:number) inline brie
.decl uucy(A:number, B:unsigned, C:unsigned, D:number, E:unsigned, F:unsigned, G:unsigned) brie
.decl hhtd(A:number, B:unsigned, C:unsigned, D:number, E:unsigned, F:unsigned)
.decl ftcv(A:number, B:number, C:number, D:number) btree
.decl zczf(A:number, B:number, C:number, D:number, E:number, F:number, G:number)
.decl izsi(A:number) btree
.decl ligf(A:number, B:number, C:number, D:number, E:unsigned, F:number, G:number, H:number) no_magic btree
.decl dvvu(A:number, B:number, C:unsigned, D:unsigned, E:unsigned, F:number, G:number) brie
.decl ttwr(A:number, B:number, C:number, D:number, E:unsigned, F:unsigned, G:number) btree
.decl ebbf(A:number) no_magic brie
.decl apug(A:number, B:unsigned, C:number, D:unsigned, E:number, F:number, G:unsigned) btree
.decl zevi(A:unsigned, B:unsigned, C:number, D:unsigned) no_magic btree
.decl ellc(A:number, B:number) magic
.decl uxkx(A:number) inline brie
.decl uwtz(A:number, B:number, C:number, D:number, E:number, F:number, G:number) no_inline btree
.decl cqpn(A:number, B:number, C:unsigned, D:unsigned, E:number, F:number, G:unsigned)
.decl xyoq(A:number, B:unsigned, C:number, D:unsigned, E:number, F:unsigned, G:number, H:unsigned) btree
.decl zdxk(A:number, B:number, C:unsigned, D:number, E:unsigned)

ufdm(1, -9).
ufdm(2, 4).
ufdm(-9, -2).
ufdm(3, 10).
ufdm(4, 0).
ufdm(6, -4).
adaw(0, -8).
adaw(5, -6).
adaw(8, 7).
adaw(4, -9).
adaw(9, 10).
adaw(1, 5).
adaw(5, 0).
adaw(2, 4).
adaw(0, 6).
ajha(3).
ajha(-8).
ajha(-7).
ajha(9).

wcvj(B, B) :- ajha(A), adaw(B, A).
wcvj(B1, B) <= wcvj(B2, B) :- B1<=B2.
nzev(A, A, A, A, A, A) :- wcvj(A, A).
edwj(A, B) :- wcvj(B, B), ajha(A).
lroc(A, B, A, A) :- adaw(B, A), A != count : {ajha(AAA), to_number("8") < AAA, 2 <= AAA}.
zhob(A, A, F, A, A, A) :- adaw(F, A), nzev(C, B, B, _, C, F).
ihsf(C) :- lroc(B, E, C, C), ajha(A), lroc(A, E, A, D).
pylt(A, A, A, A) :- ajha(A), !ihsf(A).
zyuj(lnot A, lnot A, B) :- ihsf(A), edwj(A, B).
qebx(F, E) :- nzev(E, D, E, F, H, G), nzev(F, E, F, G, H, H), lroc(A, C, A, B).
iobl(B, A) :- edwj(A, B), !lroc(A, B, A, A).
vvur(D, D, D, D, D) :- adaw(D, A), edwj(A, D), zhob(A, A, C, A, B, B), A = range(-393,946).
ftbk(A, A, A, A) :- ihsf(A), !ajha(A), 0 = 0.
japo(C, B) :- nzev(I, G, F, I, C, J), vvur(G, I, E, K, K), ftbk(A, A, B, A).
nxop(A, A) :- zyuj(A, A, B), A != sum AAA : { lroc(AAA, CCC, BBB, AAA), -2 != BBB}.
qpft(B, B) :- ftbk(B, A, B, C).
ykow(B, A, B, A, B) :- wcvj(B, B), adaw(B, A).
ykow(B, A1, B, A, B) <= ykow(B, A2, B, A, B) :- A1<=A2.
vnjk(A, A, A, A, A, A, A) :- qebx(A, A).
uhuk(G, F) :- vnjk(G, G, E, F, F, G, F), ftbk(D, C, B, D), edwj(A, G).
stql(B, A, A, D, A, D, D, D) :- uhuk(D, D), ykow(D, A, D, A, E), adaw(C, B).
dsxz(B) :- nxop(A, A), nzev(C, C, B, D, C, B).
yhnz(C, A, A, A, B, B, B, A) :- ykow(B, A, C, A, C), !ufdm(A, A).
ifmk(A, A, A) :- yhnz(C, A, A, A, C, D, C, B), adaw(D, A), dsxz(D).
gcly(C, D, C, B bshr A, C, A/A) :- uhuk(_, C), yhnz(C, B, A, A, D, C, C, B), vvur(D, C, C, C, D).
uucy(A, D, C, A, C, D, C) :- yhnz(C, A, A, A, C, D, D, A).
hhtd(A, B, B, A, B, B) :- ykow(B, A, _, A, B).
ftcv(A, A, A, A) :- uucy(A, B, D, A, 0, C, C).
zczf(B, C, C, B, C, C, A) :- ftbk(A, B, C, C).
izsi(A) :- uucy(B, D, G, B, C, J, H), adaw(F, A), nzev(G, I, F, K, D, E).
ligf(B, B, B, B, E, B, A, B) :- izsi(B), uhuk(F, D), stql(B, B, B, F, A, G, E, E).
dvvu(B, B, E, E, E, B, B) :- zhob(C, C, E, A, B, B).
ttwr(B, A, C, B, E, E, B) :- zhob(B, A, E, A, B, C).
ebbf(A) :- ihsf(A).
apug(A, B, A, B, A, A, B) :- nxop(A, A), wcvj(B, B).
zevi(E, E, A, E) :- zczf(A, C, A, A, D, C, B), wcvj(E, E).
ellc(B, A) :- ifmk(A, B, A).
ellc(B1, A) <= ellc(B2, A) :- B1>=B2.
uxkx(A) :- zyuj(A, B, C), zyuj(A, A, C).
uwtz(A, A, A, A, A, A, A) :- qpft(A, A).
cqpn(A, A, C, C, B, A, C) :- lroc(A, C, B, A), adaw(C, A), A = A.
xyoq(C, F, B, H, C, F, B, H) :- apug(A, F, D, H, D, E, F), apug(C, F, C, G, B, C, H), !ifmk(E, A, C).
zdxk(E, D, G, E, F) :- nxop(B, E), apug(D, G, D, G, E, E, F), E = count : {zczf(FFF, BBB, GGG, FFF, FFF, GGG, DDD), ttwr(BBB, EEE, GGG, BBB, HHH, HHH, BBB), ufdm(BBB, BBB), to_number("-4") >= BBB}.

.output zdxk

I run it with souffle -w example.dl and it crashed and only return _Map_base::at.

If I remove the last rule of zdxk, it can run correctly.

I use the last release version of Souffle.

[quentin]

Hi, may I ask where these programs originate from? Are they obfuscated versions of actual useful programs, or are they generated by a fuzzer ?

[quentin]

The throw happens in interpreter::constructNodeType when node type I_Erase_Btree_2 is searched for relation @poscopy_1.wcvj. There can only be Erase nodes for BtreeDelete relations, not for Btree relations.

@poscopy prefix indicates that magic is involved and Erase indicates subsumption is involved. I guess the semantics checkers have to be enhanced in some way ?

[DerZc]

Hi, may I ask where these programs originate from? Are they obfuscated versions of actual useful programs, or are they generated by a fuzzer ?

Hi, these programs generated randomly by a fuzzer as we discussed before.

[DerZc]

Sure, I get a reduced version of this program and this is the simplest version I can get:

.decl adaw(A:unsigned, B:number)
.decl wcvj(A:unsigned, B:unsigned)
.decl ttwr(A:unsigned) magic
.decl zdxk(A:number, B:unsigned)

adaw(1, 5).

wcvj(B, B) :- adaw(B, A).
wcvj(B1, B) <= wcvj(B2, B) :- B1<=B2.

ttwr(E) :- wcvj(E, E).

zdxk(E, B) :- wcvj(B, B), E = count : {ttwr(EEE)}.
.output zdxk

In the rule of zdxk, there is a dependence chain of zdxk: zdxk->wcvj, and wcvj involve subsumption. There is a dependence chain of ttwr: ttwr->wcvj, ttwr involves magic and wcvj involves subsumption. Take away any of them, the program can execute correctly. Hope this is useful.

[DerZc]

Hi, may I ask where these programs originate from? Are they obfuscated versions of actual useful programs, or are they generated by a fuzzer ?

The method we used to generate the programs and find this bug has been published at OOPSLA2024, this is the preprint version of our paper https://arxiv.org/abs/2402.12863