BoiseState-AdaptLab / IEGenLib

Inspector/Executor Generation Library for manipulating sets and relations with uninterpreted function symbols.
BSD 2-Clause "Simplified" License
2 stars 4 forks source link

IEGenLib CodeGen Bug #156

Open tpops opened 3 years ago

tpops commented 3 years ago

When IEGenLib generates code for an Uninterpreted function in the domain, it uses a macro to map the function to array access. For instance, if a statment has a domain {[i,j]: 0 <= i and i < NR and j = rowptr(i) }.

A macro for rowptr is created.

#define rowptr(t0) rowptr[t0]

Here rowptr(i) is mapped to rowptr[i]

There is however a problem when we make some UFs omega compliant before codegen. This results to the introduction of wrong mappings.

Computation specification below results in the wrong mapping.


    Computation * c = new Computation();
    c->addStmt(new Stmt("$ACSR$[k] = $ABCSR$[p];",
                        ¦   "{ [ii, kk, jj, hr, hc, p, k] : jj - bcol(kk) = 0"
                        ¦   " && k - col_inv(5 ii + hr, 5 jj + hc) = 0 && 5 jj + hc"
                        ¦   " - col(k) = 0 && 25 kk + 5 hr + hc - p = 0 && ii >= 0"
                        ¦   " && hr >= 0 && hc >= 0 && kk - browptr(ii) >= 0 && -hr"
                        ¦   " + 4 >= 0 && -hc + 4 >= 0 && k - rowptr(5 ii + hr) >= 0"
                        ¦   " && -ii + NR_BR - 1 >= 0 && -kk + browptr_1(ii) - 1 >= 0"
                        ¦   " && -k + rowptr1(5 ii + hr) - 1 >= 0 }",
                        ¦   "{[ii, kk, jj, hr, hc, p, k]->[ii, kk, jj, hr, hc, p, k]}",
                        ¦   {{"ABCSR" , "{[ii, kk, jj, hr, hc, p, k]->[p]}"}},
                        ¦   {{"ACSR" , "{[ii, kk, jj, hr, hc, p, k]->[k]}"}}));
   c->codeGen();
#define col_inv(t0,t1) col_inv[t0][t1]
#define col_inv_1(__tv0, __tv1, __tv2, __tv3, __tv4) col_inv(5 __tv0 + __tv3, 5 __tv2 + __tv4)
// Wrong macro, the macro below should not be introduced.
#define col_inv_1(t0,t1,t2,t3,t4) col_inv_1[t0][t1][t2][t3][t4]
#define col_inv_1_8(__tv0, __tv1, __tv2, __tv3, __tv4) col_inv_1(__tv0, __tv1, __tv2, __tv3, __tv4)
#define rowptr(t0) rowptr[t0]
#define rowptr1(t0) rowptr1[t0]
#define rowptr1_6(__tv0, __tv1, __tv2, __tv3) rowptr1(5 __tv0 + __tv3)
// Wrong macro, the macro below should not be introduced.
#define rowptr1_6(t0,t1,t2,t3) rowptr1_6[t0][t1][t2][t3]
#define rowptr1_6_13(__tv0, __tv1, __tv2, __tv3) rowptr1_6(__tv0, __tv1, __tv2, __tv3)
#define rowptr_4(__tv0, __tv1, __tv2, __tv3) rowptr(5 __tv0 + __tv3)
// Wrong macro, the macro below should not be introduced.
#define rowptr_4(t0,t1,t2,t3) rowptr_4[t0][t1][t2][t3]
#define rowptr_4_11(__tv0, __tv1, __tv2, __tv3) rowptr_4(__tv0, __tv1, __tv2, __tv3)
tpops commented 2 years ago
#define bcol(t0) bcol[t0]
#define bcol_0(__tv0, __tv1) bcol(__tv1)
#define browptr(t0) browptr[t0]
#define browptr_3(__tv0) browptr(__tv0)
#define browptr_5(__tv0) browptr(__tv0 + 1)
#define col(t0) col[t0]
#define col_2(__tv0, __tv1, __tv2, __tv3, __tv4, __tv5, __tv6) col(__tv6)
#define col_inv(t0,t1) col_inv[t0][t1]
#define col_inv_1(__tv0, __tv1, __tv2, __tv3, __tv4) col_inv(5 __tv0 + __tv3, 5 __tv2 + __tv4)
#define rowptr(t0) rowptr[t0]
#define rowptr_4(__tv0, __tv1, __tv2, __tv3) rowptr(5 __tv0 + __tv3)
#define rowptr_6(__tv0, __tv1, __tv2, __tv3) rowptr(5 __tv0 + __tv3 + 1)

Looks okay. Some other trivial bugs were fixed too

tpops commented 2 years ago

Add tests to reflect identifying UFs with different param expressions