kenmcmil / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
82 stars 24 forks source link

Subclass actions don't typecheck until ivytocpp #55

Open dijkstracula opened 2 years ago

dijkstracula commented 2 years ago

Hi Ken,

I have the following message type with a bunch of subclasses thereof:

 16     class msg_t = {
 17         action handle(cid: node, ^msg:msg_t)
 18     }
...
 38     subclass commit_msg_t of msg_t = {
 39         field src: node
 40         field txn: txn_t
 41         field execute_at: timestamp
 42
 43         field deps: vector[txn_t]
 44
 45         action handle(self: node, ^msg:commit_msg_t)
 46     }
 47
 48     subclass accept_msg_t of msg_t = {
 49         field src: node
 50         field txn: txn_t
 51         field execute_at: timestamp
 52
 53         field deps: vector[txn_t]
 54
 55         action handle(self: node, ^msg:commit_msg_t)
 56     }

Note the copy and paste error on line 55: clearly, that should be accept_msg_t. However, ivy appears to accept this, only to die while trying to compile the extracted C++.

(venv) ➜  accord-ivy git:(main) ✗ make
cd src; ivyc target=test protocol.ivy
g++ -Wno-parentheses-equality  -std=c++11  -I /Users/ntaylor/code/ivy/ivy/include -L /Users/ntaylor/code/ivy/ivy/lib -Xlinker -rpath -Xlinker /Users/ntaylor/code/ivy/ivy/lib -I /Users/ntaylor/code/ivy/submodules/z3/src/api/python/z3/include -L /Users/ntaylor/code/ivy/submodules/z3/src/api/python/z3/lib -Xlinker -rpath -Xlinker /Users/ntaylor/code/ivy/submodules/z3/src/api/python/z3/lib -I /usr/local/opt/openssl/include -L /usr/local/opt/openssl/lib -Xlinker -rpath -Xlinker /usr/local/opt/openssl/lib -g -o protocol protocol.cpp -lz3 -pthread
protocol.cpp:3382:47: error: no viable conversion from 'protocol::accept_msg_t' to 'const protocol::commit_msg_t'
                accept_msg_t__handle(prm__V0, self__COLON__accept_msg_t);
                                              ^~~~~~~~~~~~~~~~~~~~~~~~~
./protocol.h:829:12: note: candidate constructor (the implicit copy constructor) not viable: no known conversion from 'protocol::accept_msg_t' to 'const protocol::commit_msg_t &' for 1st argument
    struct commit_msg_t {
           ^
./protocol.h:829:12: note: candidate constructor (the implicit move constructor) not viable: no known conversion from 'protocol::accept_msg_t' to 'protocol::commit_msg_t &&' for 1st argument
protocol.cpp:3090:67: note: passing argument to parameter 'msg' here
void protocol::accept_msg_t__handle(int self, const commit_msg_t& msg){
                                                                  ^
1 error generated.
make: *** [srcprotocol] Error 1
(venv) ➜  accord-ivy git:(main) ✗

Seems like either the parsing or extraction code should complain; or, C++ codegen should compile. (I suspect the former is the thing we want; not sure exactly what the execution semantics of the latter would be.)