Automatically generating dependent type messages #85

prpr2770 · 2020-06-24T20:13:29Z

As per the implementation in QUIC, I understand that it's possible to send messages with dependent types. I would like to get some help in implementing this approach. The usecase I have is as follows:

I wish to generate message packets that are of this basic structure, where the load4 may or may not exist at all times.

    object datagram = {
        type this = struct{
            load1 : packetload,
            load2 : packetload,
            load3 : control,
            load4 : family
            }

    }

Further, if control is the following enumerated-type

type control = {msg1, msg2, msg3, msg4, msg5}

and family is a collection of data-types defined as follows

object family ={
    type this

    object family1 ={
        variant this of family = {f1msg1, f1msg2, f1msg3, f1msg4}
    }

    object family2 = {
        variant this of family = {f2msg1, f2msg2, f2msg3, f2msg4, f2msg5, f2msg6}
    }
}

I would like to select the type of datagram.load4 based on the value of datagram.load3 .i.e in the scenario where we have

if(datagram.load3 = msg1) { datagram.load4 : family1 ;}
else if (datagram.load3 = msg2) {datagram.load4 : family2; }

If the above two situations do not exist, then datagram.load4 = Not Defined .i.e the datagram shall only consist of 3 components {load1, load2, load3}
How should one define these structures, to ensure that the messages are _generated() based on the above criteria?
Further, how should the encoder, decoder be designed for the same?

I am currently trying to explore Ivy to figure out how to achieve this functionality based on the Networking Branch defined encoder/decoder architecture. I would really appreciate some guidance in this regard.

The text was updated successfully, but these errors were encountered:

prpr2770 · 2020-06-24T20:35:31Z

I'm not certain how to define the type of a variable, based on the value contained in another value. I assumed I would need to implement it using something similar to the following, which does not compile.

  before encode(dgram:datagram) returns(raw:stream){
        if _generating{
            if (dgram.load3 = msg1) {
                require dgram.load4 : family1;
            }else if (dgram.load3 = msg2) {
                require dgram.load4 : family2;
            }
        }

I have defined the complex-data message-structure and its codec here.
Further, I have the defined the enumerated-data-types (control) and the type-variants (family = {family1, family2}) here.

prpr2770 · 2020-06-29T18:36:27Z

In the following Quic Script quic_serdes_test.ivy
the following lines are provided

while idx < pkt.payload.end {
	var f := pkt.payload.value(idx);
        assert
	(exists (X:frame.stream) (f *> X)) |
	(exists (X:frame.ack) f *> X) |

...

if some (a:frame.ack) pkt.payload.value(idx) *> a {
	    assert a.ack_blocks.end > 0 & a.ack_blocks.value(0).gap = 0;
	};
	if some (s:frame.stream) pkt.payload.value(idx) *> s {
	    assert s.len & s.length = s.data.end;
	};

Is this a suitable way to handle this? I dont' understand the syntax that's being used, and I'd really appreciate some help in interpreting these commands.

Further, in quic_connection.ivy, we notice the following description

    if pkt.hdr_long & hdr_type_bits = 0 {
        require forall (I:frame.idx) 0 <= I & I < pkt.payload.end ->
        ((pkt.payload.value(I) isa frame.ack)
        | (pkt.payload.value(I) isa frame.crypto)
        | (pkt.payload.value(I) isa frame.rst_stream)
        | (pkt.payload.value(I) isa frame.connection_close));
        # require ~conn_closed(src,scid);  # [6]

I have tried to use these two references, to guide my code development. However, I constantly obtain the error statement
stating that data of type family1/family2 cannot be converted into the type family.

complexdata_codec_variants.ivy: line 55: error: cannot convert argument of type {family.family1.f1msg1,family.family1.f1msg2,family.family1.f1msg3,family.family1.f1msg4} to family

I have updated the gists with the information I have identified above. Please do help in this regard.

kenmcmil · 2020-06-29T21:06:39Z

Sorry it took me a while to get to this. Ivy doesn't have dependent types. It does have a form of subtyping, however, that might be helpful. In QUIC, this is used to represent the various frame types. Below, you can see an example using subtyping. There is an abstract type 'message' that has two subtypes called 'request' and 'response'. In Ivy these are called 'variants'.

type message

object request = {
    variant this of message = struct {
        content : data
    }
}

object response = {
    variant this of message = struct {
        content : data
    }
}

There is an object called service.net that sends and receives messages. In the implementation of service, you can see this code:

        implement client_request {
            var m : request;
            m.content := content;
            call net.send(self,dst,m);
            call protocol.request_event(self,dst,m);
        }

Here net.send is being called with a message m of subtype request. This is an example of an upcast from the subtype to the abstract type. In the implementation of net.recv, you can see an example of a downcast:

            if some (req:request) m *> req {
                var resp : response;
                resp.content := req.content;
                call net.send(self,src,resp);
                call protocol.response_event(self,src,resp)
            } else if some (resp:response) m *> resp {
                call client_response(self,resp.content);
            }

Here, if m is of type request, its value is bound to req and subsequently a response is constructed and sent. If it is of type response, then its value is bound to resp. Subtypes can also override methods of the abstract type, though this is not done in the example.

My apologies that this is not yet in the language documentation.

#lang ivy1.7

# include ip
include udp
include order

object ip = {
#    instance endpoint : iterable
    type endpoint
    interpret endpoint -> bv[1]
}

type data

type message

object request = {
    variant this of message = struct {
        content : data
    }
}

object response = {
    variant this of message = struct {
        content : data
    }
}

type pkt = struct {
    src : ip.endpoint,
    payload : message
}

isolate protocol = {

    action request_event(src:ip.endpoint,dst:ip.endpoint,msg:request)
    action response_event(src:ip.endpoint,dst:ip.endpoint,msg:response)

    specification {
        relation request_sent(X:data,S:ip.endpoint,D:ip.endpoint)
        relation response_sent(X:data,S:ip.endpoint,D:ip.endpoint)

        after init {
            request_sent(X,S,D) := false;
            response_sent(X,S,D) := false;
        }


        after request_event {
            request_sent(msg.content,src,dst) := true
        }

        around response_event {
            require request_sent(msg.content,dst,src);
            ...
            response_sent(msg.content,src,dst) := true
        }

        invariant response_sent(X,S,D) -> request_sent(X,D,S)
    }
}

isolate service = {

    isolate net = {

        action recv(dst:ip.endpoint,src:ip.endpoint,v:message)
        action send(src:ip.endpoint,dst:ip.endpoint,v:message)


        specification {
            relation sent(X:message,S:ip.endpoint,D:ip.endpoint)

            after init {
	        sent(X,S,D) := false
	    }
    
	    before send {
	        sent(v,src,dst) := true
	    }
	    before recv {
	        require sent(v,src,dst)
	    }
        }

        implementation {

            instance low : udp_simple(ip.endpoint,pkt)

            implement send {
                var p : pkt;
                p.src := src;
                p.payload := v;
                call low.send(src,dst,p)
            }

            implement low.recv(dst:ip.endpoint,v:pkt) {
                call recv(dst,v.src,v.payload)
            }
        }

        private {
            invariant low.spec.sent(P,D) -> sent(payload(P),src(P),D)
        }
    }

    action client_request(self:ip.endpoint,dst:ip.endpoint,content:data)
    action client_response(self:ip.endpoint,content:data)

    specification {
        var request_pending(S:ip.endpoint) : bool
        var request_content(S:ip.endpoint) : data

        before client_request {
            require ~request_pending(self);
            request_pending(self) := true;
            request_content(self) := content;
        }

        before client_response {
            require request_pending(self);
            require content = request_content(self);
#             request_pending := false;
        }
    }

    implementation {
        implement client_request {
            var m : request;
            m.content := content;
            call net.send(self,dst,m);
            call protocol.request_event(self,dst,m);
        }
        implement net.recv(self:ip.endpoint,src:ip.endpoint,m:message) {
            if some (req:request) m *> req {
                var resp : response;
                resp.content := req.content;
                call net.send(self,src,resp);
                call protocol.response_event(self,src,resp)
            } else if some (resp:response) m *> resp {
                call client_response(self,resp.content);
            }
        }
    }

    private {
        invariant net.sent(M,S,D) & M *> (R:request) -> protocol.request_sent(request.content(R),S,D)
        invariant net.sent(M,S,D) & M *> (R:response) -> protocol.response_sent(response.content(R),S,D)
        invariant protocol.request_sent(X,S,D) -> request_pending(S) & request_content(S) = X
    }
} with protocol   

export service.client_request
import service.client_response

extract process(self:ip.endpoint) = service(self)

prpr2770 · 2020-06-29T23:53:55Z

Thank you for the above example, in which we manually generate messages of only one subtype request and then pass that as examples into the actions that require the type messsage as a parameter. Thus, the upcast is handled by the compiler implicitly.

The code for receive addresses an example of handling downcast, which is very helpful.

I am however, having challenges in understanding how to automatically generate messages which may be of either subtype.
How do we inform the script, that when it's generating packets containing message, it needs to choose between either of the two variants. If we interpret message -> bit_vector(8), it's possible to create random bit-allocations for the message. However, if we intend to constrain the instantiations of message, to only two different enumerated sets, represented by request or response, then won't we have to specify some constraints to the _generator?

I'm trying to build an encoder/decoder for the example you've described above. And I have difficulty in determining, how to describe the decoder, where different codecs need to be used, depending on the nature of the bit-stream.

#lang ivy1.7

include stream

type port = {inputPort, outputPort}

#instance bv16 : bit_vector(16)
#instance bv8 : bit_vector(8)

interpret port -> bv[16]
instance port_codec : bv_codec(port, 2)

# -----------
# SubTypes

type message

object request = {
	variant this of message = {msg1req1, msg1req2, msg1req3}

}

object response = {
	variant this of message = {msg2req1, msg2req2, msg2req3, msg2req4}

}


interpret message -> bv[8]
instance msg_codec : bv_codec(message,1)
instance req_codec : bv_codec(request,1)
instance res_codec : bv_codec(response,1)

# ---------
# Define Packets

object packet = {
	
	type this = struct{
	load1 : port,
	load2 : message
	}


	action encode(pkt:packet) returns (raw:stream) = {
		call show_data(pkt);
        raw := raw.resize(3,0);
        raw := port_codec.encode(raw,0,pkt.load1);

        var m:= pkt.load2;

        # Handling DownCast of Message to make it specific
		if some (req:request) m *> req {
			raw := req_codec.encode(raw,2,req);

        } else if some (resp:response) m *> resp {
            raw := res_codec.encode(raw,2,resp);

        } else{
        	raw := msg_codec.encode(raw, 2, m);
        };
        
        call show_stream(raw);
	}

	action decode(raw:stream) returns (pkt:packet) = {
        require raw.end >= 3;
        var portVal := port_codec.decode(raw,0);
        pkt.load1 := portVal; 

        if (portVal = inputPort){
			pkt.load2 := req_codec.decode(raw,2);
        } else if (portVal = outputPort){
			pkt.load2 := res_codec.decode(raw,2);
        } else {
        	pkt.load2 := msg_codec.decode(raw,2);
        };

        call show_data(pkt);
	}

  


    import action show_data(x:packet) 
    import action show_stream(y:stream) 

}


attribute radix=16

I obtain the following error while compiling it:

ivyc target=test subtypes_message.ivy 
subtypes_message.ivy: line 72: error: cannot convert argument of type {request.msg1req1,request.msg1req2,request.msg1req3} to message

kenmcmil · 2020-06-30T00:28:49Z

Here's a simple example. We have two types of message with different payload types. Instead of using downcasts in the encoder, I've given each subtype its own encode method. Notice the abstract type message also has to have an encode action, though it doesn't need an implementation. In the before part of my test action, I've given a different requirement on each message type using a downcast. In the implementation of my test action, I encode the message and show it. In actual testing I would pass it as input to the code being tested, by sending it through a networking API, or by some other means.

Now if you run this, you'll see that Ivy's constrained randomization of bit vectors is not very good!

#lang ivy1.7

include order
include stream

object message = {
    type this
    action encode(self:this) returns (s:stream)
}        

instance request_content : bit_vector(16)

instance response_content : bit_vector(8)

object request = {
    variant this of message = struct {
        content : request_content
    }
    action encode(self:this) returns (s:stream) = {
        s := s.resize(3,0);
        s := s.set(0,0);
        s := s.set(1,bfe[0][7](self.content));
        s := s.set(2,bfe[8][15](self.content));
    }
}

object response = {
    variant this of message = struct {
        content : response_content
    }
    action encode(self:this) returns (s:stream) = {
        s := s.resize(2,0);
        s := s.set(0,1);
        s := s.set(1,bfe[0][7](self.content));
    }
}

export action test(m:message)

before test {
    if some (req:request) m *> req {
        require req.content >= 0x8000;
    } else if some (rsp:response) m *> rsp {
        require rsp.content >= 0x80;
    }
}

implement test {
    var bytes := m.encode;
    call show_bytes(bytes);
}

import action show_bytes(bytes:stream)

attribute radix=16

Output of this program:

./random3 
> test({response:{content:255}})
< show_bytes([0x1,0xff])
> test({response:{content:0xab}})
< show_bytes([0x1,0xab])
> test({response:{content:0xc2}})
< show_bytes([0x1,0xc2])
> test({response:{content:0x8d}})
< show_bytes([0x1,0x8d])
> test({response:{content:0x8d}})
< show_bytes([0x1,0x8d])
> test({response:{content:0x8d}})
< show_bytes([0x1,0x8d])
> test({response:{content:0x8d}})
< show_bytes([0x1,0x8d])
> test({request:{content:0x845e}})
< show_bytes([0,0x5e,0x84])
> test({request:{content:0x845e}})
< show_bytes([0,0x5e,0x84])
> test({request:{content:0x845e}})
< show_bytes([0,0x5e,0x84])
> test({response:{content:0x80}})
< show_bytes([0x1,0x80])
> test({response:{content:0x80}})
< show_bytes([0x1,0x80])
> test({response:{content:0x80}})
< show_bytes([0x1,0x80])
> test({response:{content:0x80}})
< show_bytes([0x1,0x80])
> test({request:{content:0x89ec}})
< show_bytes([0,0xec,0x89])
> test({request:{content:0xf902}})
< show_bytes([0,0x2,0xf9])
> test({request:{content:0xdeaa}})
< show_bytes([0,0xaa,0xde])
> test({request:{content:0xb77c}})
< show_bytes([0,0x7c,0xb7])
...

prpr2770 · 2020-06-30T14:21:14Z

Thank you for your guidance on this part. I have tried to write a decoder for the same, to test the decoding/encoding function and I prepared the following script, which however, leads to some compilation errors. Could you please help me debug the issue, to determine what I might have misunderstood about IvY? Thank you.

#lang ivy1.7

include stream


instance port : bit_vector(16)
instance port_codec : bv_codec(port, 2)

# -----------
# SubTypes

instance data : bit_vector(8)
instance request_content : bit_vector(16)
instance response_content : bit_vector(8)


object message = {
	type this
	action encode(raw:this) returns (s:stream)
	action decode(self:this, s:stream) returns (raw:this)
}

object request = {
	#variant this of message = {msg1req1, msg1req2, msg1req3}
	variant this of message = struct{
		content : request_content
	}
    action encode(self:this) returns (raw:stream) = {
        raw := raw.resize(3,0); # why do we initialize 3 bytes, instead of 2 bytes that's needed? 
        raw := raw.set(0,0);
        raw := raw.set(1,bfe[0][7](self.content));
        raw := raw.set(2,bfe[8][15](self.content));
    }

	action decode(self:this, raw:stream) returns (self:this) = {
        #self.content := bfe[0][15](raw.segment(1, raw.end));

        var val : request_content := 0;
        #val := 0;
        var idx :pos := 0;
        var end :pos := 2;

        while idx < end {
            # left-shift the bytes and add the byte-content
            val := 256 * val + bfe[0][7](raw.value(idx));
            idx := idx + 1;
        };

        self.content := val;
	}

}

object response = {
	#variant this of message = {msg2req1, msg2req2, msg2req3, msg2req4}
	variant this of message = struct{
		content : response_content
	}
    action encode(self:this) returns (raw:stream) = {
        raw := raw.resize(2,0); # why do we initialize 2 bytes, instead of 1 byte that's needed? 
        raw := raw.set(0,1);
        raw := raw.set(1,bfe[0][7](self.content));
    }

	action decode(self:this,raw:stream) returns (self:this) = {

        #self.content := bfe[0][8](raw.segment(1,raw.end));
        self.content := bfe[0][8](raw.value(1));
	}

}



# ---------
# Define Packets

object packet = {
	
	type this = struct{
	load1 : port,
	load2 : message
	}


	action encode(pkt:packet) returns (raw:stream) = {
		call show_data(pkt);
        raw := raw.resize(2,0);
        raw := port_codec.encode(raw,0,pkt.load1);

        var m:= pkt.load2;

        # Handling DownCast of Message to make it specific
		if some (req:request) m *> req {
			#raw := req_codec.encode(raw,2,req);
			raw := raw.extend(req.encode);

        } else if some (resp:response) m *> resp {
            #raw := res_codec.encode(raw,2,resp);
            raw := raw.extend(resp.encode);

        };
        # else{
        #	raw := msg_codec.encode(raw, 2, m);
        #	raw := raw.extend(m.encode);
        #};
        
        call show_stream(raw);
	}

	action decode(raw:stream) returns (pkt:packet) = {
        require raw.end >= 3;
        var portVal := port_codec.decode(raw,0);
        pkt.load1 := portVal; 

		var m:= pkt.load2;
        if (portVal = 0x0001){
        	if some (req:request) m *> req {
				#raw := req_codec.encode(raw,2,req);
				raw := raw.segment(2,raw.end);
				m := m.decode(raw);

        	} 
			#pkt.load2 := req_codec.decode(raw,2);
        } else if (portVal = 0x0002){
        	if some (res:response) m *> res {
				#raw := req_codec.encode(raw,2,req);
				raw := raw.segment(2,raw.end);
				m := m.decode(raw);

        	} 
			#pkt.load2 := res_codec.decode(raw,2);
        };
        pkt.load2 := m;

        call show_data(pkt);
	}

  


    import action show_data(x:packet) 
    import action show_stream(y:stream) 

}



#interpret data -> bv[8]
#instance message : bit_vector(8)
#interpret message -> bv8
#instance message : bv8
#interpret message -> bv[8]
#interpret response -> bv[8]
#interpret request -> bv[8]

#instance msg_codec : bv_codec(message,1)
#instance req_codec : bv_codec(request,1)
#instance res_codec : bv_codec(response,1)

attribute radix=16

The test-script that I have written is as follows:

#lang ivy1.7


include stream
include subtypes_message

# Test that decoding is the inverse of encoding

export action test(dgram:packet) = {

    call show_decoded(dgram);

	# encode the packetgram
    var raw := packet.encode(dgram);
    call show_encoded(raw);

    # decode the raw
    var redec := packet.decode(raw);
    call show_decoded(redec);

    # compare the packetgrams
    assert redec = dgram;


    var raw2 := packet.encode(redec);
    call show_encoded(raw2);

    # compare the two serialized forms: This is not fail-proof. As the serialization can be of same error-form. 
    # assert raw2 = raw; 
}

before test(dgram:packet) { 
    if _generating{
            
        
        # Downcast type of Message
        var f := dgram.load2;
        assert
        (exists (X:request) (f *> X)) |
        (exists (X:response) (f *> X)) ;

        if some (a:request) dgram.load2 *> a {
           # assert ( modulo(dgram.load1 , 2) ~= 0 )
            assert ( dgram.load1 - dgram.load1*(dgram.load1 / 2) ~= 0);
        };
        if some (a:response) dgram.load2 *> a {
            # assert ( modulo(dgram.load1 , 2) = 0 )
            assert ( dgram.load1 - dgram.load1*(dgram.load1 / 2) = 0);
        };

        # if modulo(dgram.load1, 2) ~=0 
        if (dgram.load1 - dgram.load1*(dgram.load1 / 2) ~= 0){
            require dgram.load2 isa request;
        }else if (dgram.load1 - dgram.load1*(dgram.load1 / 2) = 0){ # if modulo(dgram.load1, 2) =0 
            require dgram.load2 isa response;
        };

    }

    
}

import action show_encoded(raw:stream)
import action show_decoded(dgram:packet)

attribute radix = 16

The compilation error obtained when compiling the test-script is as follows:

ivyc target=test subtypes_message_test.ivy 
g++  -I /usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/include -L /usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/lib -Wl,-rpath=/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/lib -g -o subtypes_message_test subtypes_message_test.cpp -lz3 -pthread

subtypes_message_test.cpp: In member function 'virtual subtypes_message_test::packet subtypes_message_test::packet__decode(subtypes_message_test::stream)':
subtypes_message_test.cpp:1476:66: error: no match for 'operator=' (operand types are 'subtypes_message_test::message' and 'subtypes_message_test::response')
                                                         __tmp0 = self__COLON__response; response__decode(__tmp0, raw);
                                                                  ^~~~~~~~~~~~~~~~~~~~~
In file included from subtypes_message_test.cpp:1:0:
subtypes_message_test.h:665:14: note: candidate: subtypes_message_test::message& subtypes_message_test::message::operator=(const subtypes_message_test::message&)
     message& operator=(const message&other){
              ^~~~~~~~
subtypes_message_test.h:665:14: note:   no known conversion for argument 1 from 'subtypes_message_test::response' to 'const subtypes_message_test::message&'
subtypes_message_test.cpp:1476:117: error: no matching function for call to 'subtypes_message_test::response__decode(subtypes_message_test::message&, subtypes_message_test::stream&)'
                                                         __tmp0 = self__COLON__response; response__decode(__tmp0, raw);
                                                                                                                     ^
In file included from subtypes_message_test.cpp:1:0:
subtypes_message_test.h:752:18: note: candidate: virtual void subtypes_message_test::response__decode(subtypes_message_test::response&, const subtypes_message_test::stream&)
     virtual void response__decode(response& self, const stream& raw);
                  ^~~~~~~~~~~~~~~~
subtypes_message_test.h:752:18: note:   no known conversion for argument 1 from 'subtypes_message_test::message' to 'subtypes_message_test::response&'
subtypes_message_test.cpp:1487:74: error: no match for 'operator=' (operand types are 'subtypes_message_test::message' and 'subtypes_message_test::request')
                                                                 __tmp1 = self__COLON__request; request__decode(__tmp1, raw);
                                                                          ^~~~~~~~~~~~~~~~~~~~
In file included from subtypes_message_test.cpp:1:0:
subtypes_message_test.h:665:14: note: candidate: subtypes_message_test::message& subtypes_message_test::message::operator=(const subtypes_message_test::message&)
     message& operator=(const message&other){
              ^~~~~~~~
subtypes_message_test.h:665:14: note:   no known conversion for argument 1 from 'subtypes_message_test::request' to 'const subtypes_message_test::message&'
subtypes_message_test.cpp:1487:123: error: no matching function for call to 'subtypes_message_test::request__decode(subtypes_message_test::message&, subtypes_message_test::stream&)'
                                                                 __tmp1 = self__COLON__request; request__decode(__tmp1, raw);
                                                                                                                           ^
In file included from subtypes_message_test.cpp:1:0:
subtypes_message_test.h:757:18: note: candidate: virtual void subtypes_message_test::request__decode(subtypes_message_test::request&, const subtypes_message_test::stream&)
     virtual void request__decode(request& self, const stream& raw);
                  ^~~~~~~~~~~~~~~
subtypes_message_test.h:757:18: note:   no known conversion for argument 1 from 'subtypes_message_test::message' to 'subtypes_message_test::request&'
subtypes_message_test.cpp:1517:70: error: no match for 'operator=' (operand types are 'subtypes_message_test::message' and 'subtypes_message_test::response')
                                                             __tmp2 = self__COLON__response; response__decode(__tmp2, raw);
                                                                      ^~~~~~~~~~~~~~~~~~~~~
In file included from subtypes_message_test.cpp:1:0:
subtypes_message_test.h:665:14: note: candidate: subtypes_message_test::message& subtypes_message_test::message::operator=(const subtypes_message_test::message&)
     message& operator=(const message&other){
              ^~~~~~~~
subtypes_message_test.h:665:14: note:   no known conversion for argument 1 from 'subtypes_message_test::response' to 'const subtypes_message_test::message&'
subtypes_message_test.cpp:1517:121: error: no matching function for call to 'subtypes_message_test::response__decode(subtypes_message_test::message&, subtypes_message_test::stream&)'
                                                             __tmp2 = self__COLON__response; response__decode(__tmp2, raw);
                                                                                                                         ^
In file included from subtypes_message_test.cpp:1:0:
subtypes_message_test.h:752:18: note: candidate: virtual void subtypes_message_test::response__decode(subtypes_message_test::response&, const subtypes_message_test::stream&)
     virtual void response__decode(response& self, const stream& raw);
                  ^~~~~~~~~~~~~~~~
subtypes_message_test.h:752:18: note:   no known conversion for argument 1 from 'subtypes_message_test::message' to 'subtypes_message_test::response&'
subtypes_message_test.cpp:1528:78: error: no match for 'operator=' (operand types are 'subtypes_message_test::message' and 'subtypes_message_test::request')
                                                                     __tmp3 = self__COLON__request; request__decode(__tmp3, raw);
                                                                              ^~~~~~~~~~~~~~~~~~~~
In file included from subtypes_message_test.cpp:1:0:
subtypes_message_test.h:665:14: note: candidate: subtypes_message_test::message& subtypes_message_test::message::operator=(const subtypes_message_test::message&)
     message& operator=(const message&other){
              ^~~~~~~~
subtypes_message_test.h:665:14: note:   no known conversion for argument 1 from 'subtypes_message_test::request' to 'const subtypes_message_test::message&'
subtypes_message_test.cpp:1528:127: error: no matching function for call to 'subtypes_message_test::request__decode(subtypes_message_test::message&, subtypes_message_test::stream&)'
                                                                     __tmp3 = self__COLON__request; request__decode(__tmp3, raw);
                                                                                                                               ^
In file included from subtypes_message_test.cpp:1:0:
subtypes_message_test.h:757:18: note: candidate: virtual void subtypes_message_test::request__decode(subtypes_message_test::request&, const subtypes_message_test::stream&)
     virtual void request__decode(request& self, const stream& raw);
                  ^~~~~~~~~~~~~~~
subtypes_message_test.h:757:18: note:   no known conversion for argument 1 from 'subtypes_message_test::message' to 'subtypes_message_test::request&'

kenmcmil · 2020-06-30T17:00:31Z

I'm not seeing that error. Perhaps we have a different versions of g++, or different versions of Ivy. Can you do the following and post the output:

$ g++ --version
$ cd $IVYDIR
$ git log -1

where $IVYDIR is the Ivy source directory.

Thanks.

prpr2770 · 2020-06-30T18:19:35Z

I apologize for the delay. I didn't see the updated notification in my mail.

g++ --version
g++ (Ubuntu 7.5.0-3ubuntu1~18.04) 7.5.0
Copyright (C) 2017 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

base) /home/ivy_networking/ivy# git log -1
commit 01d425eaf907d2d02321b6a13ebe1da6d94d7521 (HEAD -> networking, origin/networking)
Author: Ken McMillan <[email protected]>
Date:   Wed Jun 17 12:51:25 2020 -0700

    added networking examples

kenmcmil · 2020-06-30T19:52:33Z

Looks like we have the same versions of Ivy and g++. Can you attach a zip with the files subtypes_message_test.h and subtypes_message_test.cpp?

prpr2770 · 2020-06-30T21:17:32Z

subtype_message.zip

I have zipped the two files you've requested for. Please do let me know if you can unzip these files. Else, I'll try to share the files via email.

prpr2770 · 2020-06-30T23:30:21Z

I feel uncertain about the following lines of code that I have included in the test-script. I'd appreciate it if you could provide some criticism about the following lines, as it'll help me understand what's the right way of specifying the requirements

before test(dgram:packet) { 
    if _generating{
            
        
        # Downcast type of Message
        var f := dgram.load2;
        assert
        (exists (X:request) (f *> X)) |
        (exists (X:response) (f *> X)) ;

        if some (a:request) dgram.load2 *> a {
           # assert ( modulo(dgram.load1 , 2) ~= 0 )
            assert ( dgram.load1 - dgram.load1*(dgram.load1 / 2) ~= 0);
        };
        if some (a:response) dgram.load2 *> a {
            # assert ( modulo(dgram.load1 , 2) = 0 )
            assert ( dgram.load1 - dgram.load1*(dgram.load1 / 2) = 0);
        };

        # if modulo(dgram.load1, 2) ~=0 
        if (dgram.load1 - dgram.load1*(dgram.load1 / 2) ~= 0){
            require dgram.load2 isa request;
        }else if (dgram.load1 - dgram.load1*(dgram.load1 / 2) = 0){ # if modulo(dgram.load1, 2) =0 
            require dgram.load2 isa response;
        };

    }    
}

Thank you for your help in this issue.

kenmcmil · 2020-07-01T01:07:05Z

It's fine, but I think you could simplify a bit:

before test(dgram:packet) { 
    if _generating{
            
        var f := dgram.load2;
        assert (f isa request) | (f isa response);

        var load1_even := dgram.load1 - 2*(dgram.load1 / 2) = 0;

        assert load1_even <-> (f isa response);  
    }

    
}

I was able to repro the compile error above. I'll try to get that resolve soon.

prpr2770 · 2020-07-01T17:29:50Z

I tried to modify the above message-structure, to represent enumerated data-types, and the code doesn't compile in Ivy.

#lang ivy1.7

# Create sub-types that are based on enum-types

include stream


instance port : bit_vector(16)
instance port_codec : bv_codec(port, 2)

# -----------
# SubTypes

instance data : bit_vector(8)
instance request_content : bit_vector(16)
instance response_content : bit_vector(8)


object message = {
	type this
	action encode(raw:this) returns (s:stream)
	action decode(self:this, s:stream) returns (raw:this)
}


object control = {
    type this = {msg1, msg2, msg3, msg4, msg5}

    var length : pos

    after init{
        # Initalize length of the enumerated type
        length := 5; 
    }
    # The `next` action computes the next packet type
    # according to the normal sequence.

    action next(e:this) returns (e:this) = {
        if e = msg1 {
            e := msg2;
        } else if e = msg2{
            e := msg3;
        } else if e = msg3{
            e := msg4;
        } else if e = msg4{
            e := msg5;
        } else if e = msg5{
            e := msg1;
        }
    }

    action first(e:this) returns(e:this) = {
        e := msg1;
    }

}

object request = {
	variant this of message = {msg1req1, msg1req2, msg1req3}
    var length: pos

    after init{
        length:=3
    }
    action next(e:this) returns (e:this) = {
        if e = msg1req1{ e:= msg1req2;}
        else if e = msg1req2 { e:= msg1req3;}
        else if e = msg1req3 { e:= msg1req1; }
    }

    action first(e:this) returns (e:this)={
        e:=msg1req1;
    }


    action encode(self:this) returns (raw:stream) = {
        raw := raw.resize(3,0); # why do we initialize 3 bytes, rather than 2 bytes? 
        raw := raw.set(0,0);
        raw := raw.set(1,bfe[0][7](self));
        raw := raw.set(2,bfe[8][15](self));
    }

	action decode(self:this, raw:stream) returns (self:this) = {
        #self.content := bfe[0][15](raw.segment(1, raw.end));

        var val : pos := 0;
        #val := 0;
        var idx :pos := 0;
        var end :pos := 2;

        while idx < end {
            # left-shift the bytes and add the byte-content
            val := 256 * val + bfe[0][7](raw.value(idx));
            idx := idx + 1;
        };

        if val = 0 {self := msg1req1;}
        else if (val = 1) {self := msg1req2;}
        else if (val = 2) {self := msg1req3;}
        else {self := msg1req1;}    # how to handle exceptions? WHy assign default value? 
        
	}

}

object response = {
	variant this of message = {msg2res1, msg2res2, msg2res3, msg2res4}
    var length: pos

    after init{
        length:=4;
    }
    action next(e:this) returns (e:this) = {
        if e = msg2res1{ e:= msg2res2;}
        else if e = msg2res2 { e:= msg2res3;}
        else if e = msg2res3 { e:= msg2res4;}
        else if e = msg2res4 { e:= msg2res1;}

    }

    action first(e:this) returns (e:this)={
        e:=msg2res1;
    }

    action encode(self:this) returns (raw:stream) = {
        raw := raw.resize(2,0); # why do we initialize 2 bytes rather than 1 byte? 
        raw := raw.set(0,1);
        raw := raw.set(1,bfe[0][7](self));
    }

	action decode(self:this,raw:stream) returns (self:this) = {

        #self.content := bfe[0][8](raw.segment(1,raw.end));
        var val: pos := bfe[0][8](raw.value(1));

        if val = 0 {self := msg2res1;}
        else if (val = 1) {self := msg2res2;}
        else if (val = 2) {self := msg2res3;}
        else if (val = 3) {self := msg2res4;}
        else {self := msg2res1;}    # how to handle exceptions? WHy assign default value? 

	}

}



# ---------
# Define Packets

object packet = {
	
	type this = struct{
	load1 : port,
	load2 : message
	}


	action encode(pkt:packet) returns (raw:stream) = {
		call show_data(pkt);
        raw := raw.resize(2,0);
        raw := port_codec.encode(raw,0,pkt.load1);

        var m:= pkt.load2;

        # Handling DownCast of Message to make it specific
		if some (req:request) m *> req {
			#raw := req_codec.encode(raw,2,req);
			raw := raw.extend(req.encode);

        } else if some (resp:response) m *> resp {
            #raw := res_codec.encode(raw,2,resp);
            raw := raw.extend(resp.encode);

        };
        # else{
        #	raw := msg_codec.encode(raw, 2, m);
        #	raw := raw.extend(m.encode);
        #};
        
        call show_stream(raw);
	}

	action decode(raw:stream) returns (pkt:packet) = {
        require raw.end >= 3;
        var portVal := port_codec.decode(raw,0);
        pkt.load1 := portVal; 

		var m: message;
		
        #if (portVal = 0x0001){
        if (portVal - 2*(portVal/2) ~= 0 ){
        	if some (req:request) m *> req {
				#raw := req_codec.encode(raw,2,req);
				raw := raw.segment(2,raw.end);
				#m := m.decode(raw);
				m := req.decode(raw);

        	} 
			#pkt.load2 := req_codec.decode(raw,2);
        } else if (portVal - 2*(portVal/2) = 0 ){
        	if some (res:response) m *> res {
				#raw := req_codec.encode(raw,2,req);
				raw := raw.segment(2,raw.end);
				#m := m.decode(raw);
				m := res.decode(raw);

        	} 
			#pkt.load2 := res_codec.decode(raw,2);
        };
        pkt.load2 := m;

        call show_data(pkt);
	}

  


    import action show_data(x:packet) 
    import action show_stream(y:stream) 

}



#interpret data -> bv[8]
#instance message : bit_vector(8)
#interpret message -> bv8
#instance message : bv8
#interpret message -> bv[8]
#interpret response -> bv[8]
#interpret request -> bv[8]

#instance msg_codec : bv_codec(message,1)
#instance req_codec : bv_codec(request,1)
#instance res_codec : bv_codec(response,1)

attribute radix=16

The above script generates the following compilation error

subtypes_message2.ivy: line 197: error: cannot convert argument of type {request.msg1req1,request.msg1req2,request.msg1req3} to message

So, I guess the sub-typing feature is not supported for enumerated types.

prpr2770 · 2020-07-01T18:38:48Z

I attempted to handle enum-types in the below format and obtained the following compilation error for the test-script

# ivyc target=test subtypes_message_test.ivy 
Traceback (most recent call last):
  File "/usr/local/bin/ivyc", line 11, in <module>
    load_entry_point('ms-ivy==0.3', 'console_scripts', 'ivyc')()
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 5755, in ivyc
    main_int(True)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 5879, in main_int
    header,impl = module_to_cpp_class(classname,basename)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 3281, in module_to_cpp_class
    emit_action(header,impl,a,classname)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 2035, in emit_action
    emit_some_action(header,impl,name,action,classname)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 2077, in emit_some_action
    action.emit(code)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 4509, in emit_sequence
    a.emit(header)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 4632, in emit_local
    self.args[-1].emit(header)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 4509, in emit_sequence
    a.emit(header)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 4632, in emit_local
    self.args[-1].emit(header)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 4509, in emit_sequence
    a.emit(header)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 4632, in emit_local
    self.args[-1].emit(header)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 4509, in emit_sequence
    a.emit(header)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 4648, in emit_if
    self.args[1].emit(header)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 4644, in emit_if
    self.args[0].emit(header,code)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_to_cpp.py", line 4270, in emit_some
    cpptype = sort_to_cpptype[fmla.args[0].sort]
KeyError: UninterpretedSort('message',)

where I have used the following scripts

prpr2770 · 2020-07-17T03:38:21Z

Please do help with any advice/suggestions on this topic. I really appreciate your guidance on this. Thank you.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Automatically generating dependent type messages #85

Automatically generating dependent type messages #85

prpr2770 commented Jun 24, 2020 •

edited

Loading

prpr2770 commented Jun 24, 2020

prpr2770 commented Jun 29, 2020 •

edited

Loading

kenmcmil commented Jun 29, 2020

prpr2770 commented Jun 29, 2020 •

edited

Loading

kenmcmil commented Jun 30, 2020

prpr2770 commented Jun 30, 2020 •

edited

Loading

kenmcmil commented Jun 30, 2020

prpr2770 commented Jun 30, 2020 •

edited

Loading

kenmcmil commented Jun 30, 2020

prpr2770 commented Jun 30, 2020

prpr2770 commented Jun 30, 2020

kenmcmil commented Jul 1, 2020

prpr2770 commented Jul 1, 2020

prpr2770 commented Jul 1, 2020

prpr2770 commented Jul 17, 2020

Automatically generating dependent type messages #85

Automatically generating dependent type messages #85

Comments

prpr2770 commented Jun 24, 2020 • edited Loading

prpr2770 commented Jun 24, 2020

prpr2770 commented Jun 29, 2020 • edited Loading

kenmcmil commented Jun 29, 2020

prpr2770 commented Jun 29, 2020 • edited Loading

kenmcmil commented Jun 30, 2020

prpr2770 commented Jun 30, 2020 • edited Loading

kenmcmil commented Jun 30, 2020

prpr2770 commented Jun 30, 2020 • edited Loading

kenmcmil commented Jun 30, 2020

prpr2770 commented Jun 30, 2020

prpr2770 commented Jun 30, 2020

kenmcmil commented Jul 1, 2020

prpr2770 commented Jul 1, 2020

prpr2770 commented Jul 1, 2020

prpr2770 commented Jul 17, 2020

prpr2770 commented Jun 24, 2020 •

edited

Loading

prpr2770 commented Jun 29, 2020 •

edited

Loading

prpr2770 commented Jun 29, 2020 •

edited

Loading

prpr2770 commented Jun 30, 2020 •

edited

Loading

prpr2770 commented Jun 30, 2020 •

edited

Loading