Encoding EnumType as ByteStream

[prpr2770]

I would like to encode an EnumType as a ByteStream, in the manner similar to bv_encode has been defined within stream.ivy. I am however, not clear about the way the Enum has been implemented.

I'm raising this as a request to address the encoding and decoding of custom data-types that contain enumerated types.

type control={msg1, msg2, msg3, msg4}
interpret control -> bv[8]

instance packetload : bit_vector(16)
instance packet_codec : bv_codec(packetload, 2)


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

    }

I have written a small ivy-script that compiles successfully when executed individually. However, it fails when I test it by initializing objects.

#lang ivy1.7



include order
include collections
include stream

#
# Here, we have some generic procedures for encoding EnumTypes
# as BitVector. This is a template that takes two parameter:
#
# - enumTy : the EnumType to be encoded/decoded
# - bits : the number of bytes used for encoding
#

instance codec : bv_codec(pos, 4 )

module enum_codec(enumTy,bits) = {


    var tempEnum : enumTy
    var end : pos
    var numBytes : pos

    
    after init{

        numBytes := bits/8;
        # ----------
        # Compute the limit of number
        var cnt : pos;
        
        end := 1;
        cnt := 0;
        while(cnt < bits){
            end := 2*end;
        };

    }

    instance codec : bv_codec(pos, numBytes )




    # ----------
    # Encode a value of the type at byte position `idx` in stream `raw`
    action encode(val:enumTy) returns(raw:stream) = {        



        var idx : pos; 
        var numBytes : pos;
        var enumLength : pos; 
        
        #var end := tempEnum.length; # ceil(bits/8);
        numBytes :=  (bits/8);  # compute number of bytes
        #enumLength := tempEnum.length; 

        idx := 0; 
        
        while (idx < end ){
        #while (idx < end & idx < enumLength ){
            if (val = tempEnum[idx]){
                
                raw := codec.encode(raw,0,idx); 
                #raw := idx;     # how to guarantee that this has the same bit-size as that expected ? 
                #break; 
            };                       # assuming enumTy[idx] = msg1;
            idx := idx + 1 ;
        }

    }

    # ----------
    # Decode a value of the type at byte position `idx` in stream `raw`

    
    action decode(raw:stream) returns(val:enumTy) = {
        

        # -- works
        var idx : pos;
        idx := 0;
        var rawIdx : stream;

        rawIdx := raw.resize(end,0);


        while idx < end {
            
            var bitIdx := codec.encode(rawIdx,0,idx);
            #var bitIdx := idx;

            if bvand(raw,bitIdx){val := tempEnum[idx]; };                    # assuming enumTy[idx] = msg1;
            idx := idx + 1 ;
        }

    }


}

[prpr2770]

Is there a way in which the enum-type elements can be accessed and compared?

[kenmcmil]

There isn't any way to iterate over enums in Ivy because enums aren't ordered. It would be a useful feature, though. Or instead just a way to cast between enums and integers. For now, though, there is no good way I can see to write a generic encoder for enumerated types. The closest thing I can think of is to define the order of the enum using an array, like this:

#lang ivy1.7

include stream

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

instance control_array : array(pos,control)
var control_order : control_array

after init {
    control_order := control_order.append(msg1);
    control_order := control_order.append(msg2);
    control_order := control_order.append(msg3);
    control_order := control_order.append(msg4);
}

module enum_codec(enumTy,order,bytes) = {
    
    action decode(raw:stream,idx:pos) returns(val:enumTy) = {
        var enc : pos := 0;
        var end := idx + bytes;
        while idx < end {
            enc := 256 * enc + bfe[0][7](raw.value(idx));
            idx := idx + 1;
        };
        if enc < order.end {
            val := order.value(enc);
        }
    }

    action encode(raw:stream,idx:pos,val:enumTy) returns(raw:stream) = {
        var enc := order.begin;
        while order.value(enc) ~= val & enc < order.end {
            enc := enc.next;
        };
        var end := idx + bytes;
        while idx < end {
            end := end - 1;
            raw := raw.set(end,bfe[0][7](enc));
            enc := enc / 256;
        }
    }
}

instance foo : enum_codec(control,control_order,2)

export action test(x:control) returns (y:control) = {
    var s : stream;
    s := s.resize(2,0);
    s := foo.encode(s,0,x);
    y := foo.decode(s,0);
    ensure x = y;
}

A slightly more efficient way to do this for large enums would be to also define an encoding map as a function (which is implemented as a hash table). Or just use a bit vector as your type and define a global variable for each value.

Notice that I added a test action that checks that decoding is the inverse of encoding. If you compile this code with target=test it will feed in random values of type control and verify this. This is a god idea to do first for any codec.

Also, if you use that above code, be sure to pull the latest code on the networking branch, since I fixed a bug related to arrays of enumerated types that prevents C++ compilation.

[prpr2770]

I have modified the use-case by adopting an object based description of the enumerated type as defined in this gist.

Further, I have defined the enum-object-codec as follows.

I intend to generate random messages of the following datagram using the _generating() engine. However, I cannot generate any data when I use these definitions, though there's no compilation error.

include stream
include enum_object_codec

instance packetload : bit_vector(16)
instance packet_codec : bv_codec(packetload, 2)

include control_packet
instance control_codec : enum_codec(control, 8)

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

    }

[kenmcmil]

The problem is that the while loop in the initialiizer is an infinite loop. Change it to this:

        while(cnt < bits){
            end := 2*end;
            cnt := cnt.next;
        };

I used this as a test action:

export action test(x:datagram) = {
}

attribute radix=16

The last line just causes the log to be printed in hex. This is the result:

$ ./test_codec 
> test({load1:0x9869,load2:0x4873,load3:msg4})
> test({load1:0x944a,load2:0x58ec,load3:msg5})
> test({load1:0x58ba,load2:0xd7ab,load3:msg1})
> test({load1:0xa9e3,load2:0xe146,load3:msg1})
> test({load1:0x854,load2:0x27f8,load3:msg2})
...
> test({load1:0x4208,load2:0x8df5,load3:msg2})
> test({load1:0x2c5e,load2:0x8153,load3:msg5})
> test({load1:0xd2d2,load2:0x8ab2,load3:msg5})
> test({load1:0xf5fa,load2:0xd054,load3:msg4})
test_completed

[prpr2770]

Thank you for your help with this issue. I had some difficulty in getting the codec to work, but I figured it out.