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
77
stars
24
forks
source link
ivy_to_c++: "Missing members in `tuple_test`" errors #30
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;
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:(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:I can make it successfully pass by:
rel(X,Y,Z) := false;
;rel
now consumes only an X and a Y);range_t
type;target=test
.Thanks! Nathan