ivy_to_cpp generates invalid C++

[hidenori-shinohara]

I ran ivy_to_cpp target=test isolate=executable_runner build=false executable.ivy for the following ivy code

#lang ivy1.7

type id_t
type val_t
type counter_t
type statement_t = {prepare_st, commit_st}

interpret id_t -> bv[2]
interpret val_t -> bv[4]
interpret counter_t -> bv[8]

object network = {
    # Removing this struct definition removes the compilation bug.
    <<< header
    struct %`node.started_ballot_protocol`;
    >>>
}

object node(self:id_t) = {
    relation voted(TYPE:statement_t, CTR:counter_t, VAL:val_t)
    import action started_ballot_protocol(n:counter_t, x:val_t)
    after started_ballot_protocol {
        # Removing this `require` statement removes the compilation bug.
        require voted(prepare_st, n, x) = true;
    }
    after init {
        # Removing this initialization removes the compilation bug.
        voted(TYPE, X, V) := false;
    }
}

extract executable_runner = network, node

and tried to compile it using clang++ -c -O2 -g -std=c++17 -pthread -I /home/hidenori/ivy/ivy/include -o executable.o executable.cpp.

However, this failed with

executable.cpp:1279:20: error: use of undeclared identifier '__tup__unsigned__unsigned__statement_t'
        hash_thunk<__tup__unsigned__unsigned__statement_t,bool> __tmp0;
                   ^
executable.cpp:1283:9: error: use of undeclared identifier '__tmp0'
        __tmp0[executable::__tup__unsigned__unsigned__statement_t(V,X,TYPE)] = false;
        ^
executable.cpp:1283:28: error: no member named '__tup__unsigned__unsigned__statement_t' in 'executable'
        __tmp0[executable::__tup__unsigned__unsigned__statement_t(V,X,TYPE)] = false;
               ~~~~~~~~~~~~^
executable.cpp:1290:21: error: no matching constructor for initialization of 'executable::__tup__unsigned__statement_t__unsigned__unsigned'
        node__voted[executable::__tup__unsigned__statement_t__unsigned__unsigned(prm__V0,TYPE,X,V)] = __tmp0[executable::__tup__unsigned__unsigned__statement_t(V,X,TYPE)];
                    ^                                                            ~~~~~~~~~~~~~~~~
./executable.h:644:53: note: candidate constructor not viable: no known conversion from 'int' to 'const executable::statement_t' for 2nd argument
__tup__unsigned__statement_t__unsigned__unsigned(){}__tup__unsigned__statement_t__unsigned__unsigned(const unsigned &arg0,const statement_t &arg1,const unsigned &arg2,const unsigned &arg3) : arg0(arg0),arg1(arg1),arg2(arg2),arg3(arg3){}
                                                    ^
./executable.h:639:8: note: candidate constructor (the implicit copy constructor) not viable: requires 1 argument, but 4 were provided
struct __tup__unsigned__statement_t__unsigned__unsigned {
       ^
./executable.h:639:8: note: candidate constructor (the implicit move constructor) not viable: requires 1 argument, but 4 were provided
./executable.h:644:1: note: candidate constructor not viable: requires 0 arguments, but 4 were provided
__tup__unsigned__statement_t__unsigned__unsigned(){}__tup__unsigned__statement_t__unsigned__unsigned(const unsigned &arg0,const statement_t &arg1,const unsigned &arg2,const unsigned &arg3) : arg0(arg0),arg1(arg1),arg2(arg2),arg3(arg3){}
^
executable.cpp:1290:103: error: use of undeclared identifier '__tmp0'
        node__voted[executable::__tup__unsigned__statement_t__unsigned__unsigned(prm__V0,TYPE,X,V)] = __tmp0[executable::__tup__unsigned__unsigned__statement_t(V,X,TYPE)];
                                                                                                      ^
executable.cpp:1290:122: error: no member named '__tup__unsigned__unsigned__statement_t' in 'executable'
        node__voted[executable::__tup__unsigned__statement_t__unsigned__unsigned(prm__V0,TYPE,X,V)] = __tmp0[executable::__tup__unsigned__unsigned__statement_t(V,X,TYPE)];
                                                                                                             ~~~~~~~~~~~~^
6 errors generated.

It looks like Ivy is confused about the arity of the relation voted. For some reason, as denoted in comments, removing parts of the code makes the bug disappear.

[hidenori-shinohara]

I found a smaller example that produces the exact same issue.

#lang ivy1.7

type my_type_1
type my_type_2 = { val1, val2 }
type my_type_3

interpret my_type_1 -> bv[2]
interpret my_type_3 -> bv[8]

object node(type_1:my_type_1) = {
    relation voted(MY_TYPE_2:my_type_2, MY_TYPE_3:my_type_3)
    after init {
        # Removing this initialization removes the compilation bug.
        require voted(MY_TYPE_2, MY_TYPE_3);
    }
}

extract executable_runner = node

This seems like a very subtle bug. The order in which my_type_*'s are passed seem to important in reproducing this issue, and it seems that two of them have to interpreted as bit vectors of different sizes and the last one must be an enum. I think ctype_function and sym_decl seem related to this issue, but I am not sure.

[hidenori-shinohara]

For reference, my Ivy version is 1.8.22 (f0a6385)

[hidenori-shinohara]

For future reference: one workaround I found is to use bool instead of the enum type.

[prpr2770]

I found a similar error in my code-example, and I've raised it in #60 . Could you please elaborate upon the work-around that you identified? How are you using bool instead of enum type? Thank you for your help.

[hidenori-shinohara]

@prpr2770 Instead of type_2 I used bool since type_2 only had two values. The voted relation was identified by what type of voting it was (prepare or commit) and the actual value (=> type_3). But instead, I used true to represent prepare and false to represent commit. So instead of voted(prepare, val1), I would write voted(true, val1). I'm not sure if it works for all cases, but this worked for my particular case. (For instance, if the enum has more than 2 values, I don't think this approach makes sense.)