ivy icon indicating copy to clipboard operation
ivy copied to clipboard

ivy_to_c++: "Missing members in `tuple_test`" errors

Open dijkstracula opened this issue 3 years ago • 0 comments

I'm writing an Ivy specification which attempted to partially initialise a relation in an after init block. Here's a distillation of the intention:

#lang ivy1.8

type range_t = {0..max}

process proc = {
    specification {
        relation rel(X: range_t, Y: range_t, Z: range_t)

        after init {
            rel(X,0,Z) := false;
        }
    }
}

(apologies if this code sample is opaque in its intent.)

When compiling with ivyc target=test tuple_test.ivy, I'd expect either an Ivy compilation error, or, a successful ivy -> g++ pipeline pass. However, we die inside some generated code:

➜  sandbox git:(main) ✗ ivyc target=test tuple_test.ivy
g++ -Wno-parentheses-equality  -std=c++11  -I /Library/Python/2.7/site-packages/ms_ivy-1.8.4-py2.7.egg/ivy/include -L /Library/Python/2.7/site-packages/ms_ivy-1.8.4-py2.7.egg/ivy/lib -Xlinker -rpath -Xlinker /Library/Python/2.7/site-packages/ms_ivy-1.8.4-py2.7.egg/ivy/lib -I /usr/local/opt/openssl/include -L /usr/local/opt/openssl/lib -Xlinker -rpath -Xlinker /usr/local/opt/openssl/lib -g -o tuple_test tuple_test.cpp -lz3 -pthread
tuple_test.cpp:1216:16: error: unknown type name '__tup__int__int'; did you mean '__tup__int__int__int'?
    hash_thunk<__tup__int__int,bool> __tmp0;
               ^~~~~~~~~~~~~~~
               __tup__int__int__int
./tuple_test.h:637:8: note: '__tup__int__int__int' declared here
struct __tup__int__int__int {
       ^
tuple_test.cpp:1219:32: error: no member named '__tup__int__int' in 'tuple_test'
            __tmp0[tuple_test::__tup__int__int(X,Z)] = false;
                   ~~~~~~~~~~~~^
tuple_test.cpp:1224:116: error: no member named '__tup__int__int' in 'tuple_test'
            proc__rel[tuple_test::__tup__int__int__int(X,( 0 < 0 ? 0 : max < 0 ? max : 0),Z)] = __tmp0[tuple_test::__tup__int__int(X,Z)];
                                                                                                       ~~~~~~~~~~~~^
3 errors generated.

I can make it successfully pass by:

  • Changing the set assignment to rel(X,Y,Z) := false;;
  • Removing a column from the tuple (i.e. rel now consumes only an X and a Y);
  • Giving a concrete upper bound on the range_t type;
  • Removing target=test.

Thanks! Nathan

dijkstracula avatar Sep 22 '21 23:09 dijkstracula