souffle-lang / souffle

Soufflé is a variant of Datalog for tool designers crafting analyses in Horn clauses. Soufflé synthesizes a native parallel C++ program from a logic specification.
http://souffle-lang.github.io/
Universal Permissive License v1.0
916 stars 207 forks source link

compiler error: cannot compile source file #1858

Closed rhendrix42 closed 3 years ago

rhendrix42 commented 3 years ago

Hi guys, Consider the following program:

.decl Instance1(d:number) 
.decl Instance2(d:number) 
.decl Instance3(d:number) 
.decl Instance4(d:number) 
.decl In(s1: number, s2:number, s3:number, d1:number, d2:number, d3:number, d:number) 
.decl Tbl(s1: number, s2:number, s3:number, in:number) 
.decl GCHW(a:number, b:number) inline
.decl MTYI(a:number)
.decl LBVT(a:number, b:number, c:number)
.decl JRKR(a:number, b:number, c:number)
.decl FVSZ(a:number, b:number)
.decl ZMNZ(a:number, b:number, c:number)
.decl PVBD(a:number)
.decl SVPF(a:number)
.decl NNZA(a:number, b:number)
.decl GIHN(a:number, b:number, c:number)
.decl EBWT(a:number)

.input In()
.input Tbl()

Instance1(d)  :- In(s1,_,s3,d1,d2,_,d), Tbl(s1,_,s3,1), Tbl(d1,d2,_,0), s1=5, s3=2, d1=1, d2=3.
Instance2(d)  :- In(s1,_,_,d1,_,_,d), Tbl(s1,_,_,1), Tbl(d1,d2,d3,0), s1=4, d1=2, d2=4, d3=4.
Instance3(d)  :- In(_,s2,s3,d1,d2,d3,d), Tbl(_,s2,s3,1), Tbl(d1,d2,d3,0), s2=4, s3=2, d1=3, d2=5, d3=3.
Instance3(d)  :- In(_,s2,_,d1,_,d3,d), Tbl(_,s2,_,1), Tbl(d1,_,d3,0), s2=4, d1=4, d3=3.
Instance4(d)  :- In(s1,_,_,d1,_,_,d), Tbl(s1,_,_,1), Tbl(d1,d2,_,0), s1=0, d1=4, d2=4.
In(s1, s2, s3, 4, d2, d3, d)  :- In(s1,s2,s3,d1,d2,d3,d), Tbl(s1,s2,s3,1), Tbl(d1,_,_,0).
MTYI(i) :- Tbl(mhg,gdy,i,gkq), Tbl(nzb,ijt,gdy,gkq),  Instance3(gdy).
LBVT(i,i,min(i,wut)),  GCHW(bed,i) :- In(i,bed,wut,bed,bed,i,i), -8 > wut.
JRKR(min(--n,5),n,p) :- Instance2(n), Instance1(p).
FVSZ(v,i) :- LBVT(i,lub,i), GCHW(lau,v).  
ZMNZ(r,x,j) :- FVSZ(qix,x), LBVT(r,j,iei).
PVBD(t) :- Instance3(t).
SVPF(p) :- MTYI(p). 
NNZA(m,j) :- Instance1(j), SVPF(cvk), LBVT(llb,cvk,m), GCHW(m,m), ZMNZ(llb,llb,tln).  
GIHN(c,j,i) :- NNZA(j,nmu),GCHW(c,wdx), FVSZ(i,cos). 
EBWT(e) :- GIHN(wqg,zet,wqg), MTYI(e).

.output EBWT

Running this in compiler mode gives me compiler error: cannot compile source file Full error message: error_message.txt

Fact files: facts.zip

I am running this on Souffle verison: 68d4dcdbbd6a285169d06dfec461e652cf7ec8ae

Operating System: Debian GNU/Linux 10 (buster) Kernel: Linux 4.19.75.1.amd64-smp Architecture: x86-64

Please let me know if you cannot reproduce this. I can share some other examples.

b-scholz commented 3 years ago

The synthesiser produces an incorrect C++ program. The interpreter does not have any issues with the program.

b-scholz commented 3 years ago

The comparator fails to compile:

range<iterator_1> lowerUpperRange_1111111(const t_tuple& lower, const t_tuple& upper, context& h) const {
t_comparator_1 comparator;
int cmp = comparator(&lower, &upper);
if (cmp == 0) {
    auto pos = find(lower, h);
    auto fin = end();
    if (pos != fin) {fin = pos; ++fin;}
    return make_range(pos, fin);  <==== this is not working!!
}
if (cmp > 0) {
    return range<iterator_1>(ind_1.end(), ind_1.end());
}
return range<iterator_1>(ind_1.lower_bound(&lower, h.hints_1_lower), ind_1.upper_bound(&upper, h.hints_1_upper));
}

for the data-structure t_btree_iiii__0_3_2__2_3_1_0__1_3_0__1001__1011__1111__1101__0111__0101__0011.

SamArch27 commented 3 years ago

Great catch @rhendrix42!

Thanks for reporting this issue!