error in generation of random bytestream data from a custom datatype

[prpr2770]

I'm trying to create a random packet of a particular datatype arbit_data defined as follows

#lang ivy1.7

include ip_codec


# define a new data-type
type packetload
interpret packetload -> bv[16]



object arbitdata = { 

    object datagram = {
    type this = struct{
        load : packetload
        }

    }

    instance packet_codec : bv_codec(packetload,2)

    action decode(raw:stream) returns (dgram:datagram) = {
        require raw.end = 2;
        dgram.load := packet_codec.decode(raw,0);

    }

    action encode(dgram:datagram) returns (raw:stream) = {
        raw := raw.resize(2,0);
        raw := packet_codec.encode(raw,0,dgram.load);
    }

}

After defining the above data-type, I attempt to send randomly generated data through the UDP socket using the following script.

#lang ivy1.7

include udp_host
include udp_spec

parameter client_addr : ip.addr = 0x7f000001
parameter server_addr : ip.addr = 0x7f000001
parameter client_port : udp.port = 8008
parameter server_port : udp.port = 8585

instance udp_intf : udp_host(udp.endpoint,stream)

var udp_endpoint : udp.endpoint
var udp_sock : udp_intf.socket

after init {
    udp_endpoint := udp.endpoint.make(client_addr,client_port);
    udp_sock := udp_intf.open(udp_endpoint)            
}


include arbitdata_codec

action client_send_data(src:udp.endpoint,dst:udp.endpoint,pkt:arbitdata.datagram)
#action client_send_data(pkt:arbitdata.datagram)

implement client_send_data(src:udp.endpoint,dst:udp.endpoint,pkt:arbitdata.datagram){
#implement client_send_data(pkt:arbitdata.datagram){
    if _generating{
        
        # obtain the byte-stream payload
        var pyld := arbitdata.encode(pkt);

        if src.addr = client_addr & src.port = client_port {
            call udp_sending_pkt(dst,pyld);
            call udp_sock.send(dst,pyld);
        }

    }
}

export client_send_data
import action udp_sending_pkt(dst:udp.endpoint,pyld:stream)

I however, end up with the following error, which I do not know how to resolve.

# ivyc target=test udp_networkingref_echoclient.ivy
stream.ivy: line 49: error: cannot determine an iteration bound for loop over pos

Could you please help resolve this issue? Is there something wrong in the way I'm implementing this?

[prpr2770]

Is there any reference documentation available, on understanding how the _generating() engine of Ivy works and the procedure for generating random data of custom data-types?

[prpr2770]

I could not resolve this issue. This error, continue to occur, with all attempts at instantiating the module.

stream.ivy: line 49: error: cannot determine an iteration bound for loop over pos

[prpr2770]

Some of the compilation results I obtained are as follows

/ivy/doc/examples/networking# ivyc target=test ip_codec.ivy 
g++  -I /usr/local/lib/python2.7/dist-packages/ms_ivy-1.7.0-py2.7.egg/ivy/include -L /usr/local/lib/python2.7/dist-packages/ms_ivy-1.7.0-py2.7.egg/ivy/lib -Wl,-rpath=/usr/local/lib/python2.7/dist-packages/ms_ivy-1.7.0-py2.7.egg/ivy/lib -g -o ip_codec ip_codec.cpp -lz3 -pthread

ivy/doc/examples/networking# ivyc target=test ip_codec_test.ivy 
stream.ivy: line 48: error: symbol has no interpretation: bfe[0][7] : pos -> byte

ivy/doc/examples/networking# ivyc target=test ip_test.ivy 
stream.ivy: line 48: error: symbol has no interpretation: bfe[0][7] : pos -> byte

ivy/doc/examples/networking# ivyc target=test stream.ivy 
error: Cannot create C++ class stream with member stream.
Use command line option classname=... to change the class name.
ivy/doc/examples/networking# ivyc classname=bytestream target=test stream.ivy 
g++  -I /usr/local/lib/python2.7/dist-packages/ms_ivy-1.7.0-py2.7.egg/ivy/include -L /usr/local/lib/python2.7/dist-packages/ms_ivy-1.7.0-py2.7.egg/ivy/lib -Wl,-rpath=/usr/local/lib/python2.7/dist-packages/ms_ivy-1.7.0-py2.7.egg/ivy/lib -g -o bytestream bytestream.cpp -lz3 -pthread

[kenmcmil]

Sorry, that's a bug that is fixed on the networking branch but not propagated to master. I'll leave this open until it the fix gets merged.

[kenmcmil]

For the constraint-based random generation, this paper describes the general idea:

http://mcmil.net/pubs/SECDEV19.pdf

However, it may not be particularly helpful in specific cases. For bit vector fields, Ivy should generate values uniformly. For arrays, it chooses a length uniformly in the range 0..3 and then chooses the elements uniformly (a bit arbitrary, I know). It then goes through in iterative process of mutating the assignment until an assignment satisfying the constraints is reached. This means the obtained distribution won't be the same as what you would get by rejection sampling, but hopefully it is much more efficient in the case that the rate of rejection is close to one.

It is on the to-do list to allow the user more control of distributions.