Skip to content

Instantly share code, notes, and snippets.

@prpr2770
Last active June 29, 2020 19:53
Show Gist options
  • Save prpr2770/362495dbc4c80c606dffdbe62abdaa5c to your computer and use it in GitHub Desktop.
Save prpr2770/362495dbc4c80c606dffdbe62abdaa5c to your computer and use it in GitHub Desktop.
Define a complex-data message-structure that's got a component who's type depends on the value in an earlier defined component.
#lang ivy1.7
include stream # for bv_codec(), stream, etc.
include enum_object_codec # for enum_codec()
include control_packet # for control-type , family-type
instance packetload : bit_vector(16)
instance packet_codec : bv_codec(packetload, 2) # 2 bytes
instance control_codec : enum_codec(control, 8) # 8 bits
# Dependent type encoder/decoder
instance family1_codec : enum_codec(family.family1, 8) # 8 bits
instance family2_codec : enum_codec(family.family2, 8) # 8 bits
object data = {
object datagram = {
type this = struct{
load1 : packetload,
load2 : packetload,
load3 : control,
load4 : family
}
}
# instantiate codecs for various types occuring in header
# Encode a TCP datagram into a raw byte stream
action decode(raw:stream) returns (dgram:datagram) = {
require raw.end >= 5;
#require raw.end = 5;
dgram.load1 := packet_codec.decode(raw,0);
dgram.load2 := packet_codec.decode(raw,2);
#var load3byte := raw.value(4); # Obtains a byte
var load3Stream := raw.segment(4,5); # Obtains a byte
# Translate between Stream and BV[8]
#dgram.load3 := interpretAsEnum(load3byte);
dgram.load3 := control_codec.decode(load3Stream);
if (raw.end > 5){
var load4Stream := raw.segment(5,raw.end);
var load4 : family;
if (dgram.load3 = control.msg1){
load4 := family1_codec.decode(load4Stream);
} else if (dgram.load3 = control.msg2){
load4 := family2_codec.decode(load4Stream);
};
dgram.load4 := load4;
};
call test(dgram);
}
before encode(dgram:datagram) returns(raw:stream){
# what are the ways in which we can constrain the creation of an arbitrary datagram?
# if the value of dgram.load3 is of a specific value, we intend to generate
if _generating{
require (dgram.load3 = control.msg1) -> (dgram.load4 isa family.family1);
require (dgram.load3 = control.msg2) -> (dgram.load4 isa family.family2);
var f:= dgram.load4;
assert
(exists (X:family.family1) (f *> X)) |
(exists (X:family.family2) (f *> X));
if some (a:family.family1) dgram.load4 *> a{
assert dgram.load3 = control.msg1;
};
if some (a:family.family2) dgram.load4 *> a{
assert dgram.load3 = control.msg2;
};
# --- previous aattempts
#if (dgram.load3 = control.msg1) {
# require (dgram.load4 isa family.family1);
# #var load4 : family1;
# #dgram.load4 = load4;
# dgram.load4 := family.family1;
#
#}else if (dgram.load3 = control.msg2) {
# #require dgram.load4 : family2;
# #var load4 : family2;
# #dgram.load4 := load4
# dgram.load4 := family.family2;
# require (dgram.load4 isa family.family1);
#}
#dgram.load4 = load4
}
}
action encode(dgram:datagram) returns (raw:stream) = {
call test(dgram);
# 4 bytes to represent the packetloads
raw := raw.resize(4,0);
raw := packet_codec.encode(raw,0,dgram.load1);
raw := packet_codec.encode(raw,2,dgram.load2);
call show_stream(raw);
# -------------------------------
# How to serialize the enumerated data-type?
# raw := control_codec.encode(raw,4,dgram.load3); # Doesn't work.
#var load3 := interpretAsByte(dgram.load3);
#raw := raw.set(4,load3);
var load3 := control_codec.encode(dgram.load3);
call show_stream(load3);
raw := raw.extend(load3); # Extending the earlier RAW by as many bytes!
# -------------------------------
# Handling the Dependent Data-Type
if (dgram.load3 = control.msg1){
assert (dgram.load4 isa family.family1);
var load4 := family1_codec.encode(dgram.load4);
call show_stream(load4);
raw := raw.extend(load4); # Extending the earlier RAW by as many bytes!
} else if (dgram.load3 = control.msg2){
assert (dgram.load4 isa family.family2);
var load4 := family2_codec.encode(dgram.load4);
call show_stream(load4);
raw := raw.extend(load4); # Extending the earlier RAW by as many bytes!
}
}
import action test(x:datagram) #= {};
import action show_stream(y:stream) #= {};
}
attribute radix=16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment