microsoft / 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
223 stars 80 forks source link

another code-generation issue with value types #63

Open nano-o opened 4 years ago

nano-o commented 4 years ago

Hello, ivyc generates invalid C++ code on the example below. Should it be working?

instance elem : iterable
object obj = {
    type my_set = struct {
        member(N:elem) : bool
    }
    relation empty(S:my_set)
    definition empty(s:my_set) = forall N . ~member(s,N)
    export action emptyset returns (s:my_set) = {
        member(s,N) := false;
    }
    export action add(s:my_set, n:elem) returns (s:my_set) = {
        if ~member(s,n) {
            member(s,N) := member(s,N) | N = n
        }
    }
}
extract code = obj, elem
kenmcmil commented 4 years ago

That's a really painful bug. Structs have to have computable equality. So if a struct has a function member, then the function's domain has to be of a type that is iterable. So far, so good. The problem is that the equality comparator is a static overload in C++. But the size parameter of type elem is a non-static member of the class, so the equality comparator can't access it to iterate over elem. So there are few bad options:

1) Make equality comparison a non-static member function 2) Make the size parameter static 3) Store the size parameter in the struct

Probably the last is the least disruptive option. It might take a while to get this fixed, though.