AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Apache License 2.0
106 stars 7 forks source link

Problems trying to specify HDLC #1288

Open ThyMYthOS opened 1 year ago

ThyMYthOS commented 1 year ago

Here are the problems I stumbled into, trying to implement a real world example: HDLC. For those who need a refresher what HDLC is, see Wikipedia and these lecture slides.

To keep it simple, we ignore the initial and final flag, as well as any bit stuffing or escape sequences. The basic layout of an HDLC frame is: Address Control Information FCS
8 bit 8 bit 8*n bit 16 bit

The main issue is the control field. It looks different, depending on the type of frame:

7 6 5 4 3 2 1 0
N(R) P/F N(S) 0 I-frame
N(R) P/F type 0 1 S-frame
type P/F type 1 1 U-frame
  1. The bit(s) to determine the basic frame type are 0 and if it's not an I-frame then also 1. HDLC transmits the least significant bit first, so this makes sense for the protocol. But since there is no aspect for the bit order in RecordFlux, the field(s) to determine the type come after the type dependant part.
  2. Since the amount of bits to determine the type are not of constant length, it's not possible to use an enumeration for the frame type.
  3. Notice that for U-frames, the type field is split into two parts.

I tried to solve this, by duplicating the Control field: first as 8-bit integer and then as Opaque field using the First attribute to overlay both. The Opaque field would then have a type refinement for I_Frame_Control, S_Frame_Control and U_Frame_Control. But it's not possible to actually write the type refinement, since the condition cannot do any bit operations on the 8-bit integer value.

I think this could be solved with two additional features in RecordFlux:

  1. Aspect for the bit order as in Ada95 bitorder_aspect ::= Bit_Order => bitorder_definition bitorder_definition ::= High_Order_First | Low_Order_First
  2. Virtual or computed fields, that get their value by combining other fields. Of course this has to be bi-directional to allow serialization and deserialization.

If you have other ideas how to write a specification for HDLC please feel free to comment.

treiher commented 1 year ago

By using the modulo operation in the conditions of the type refinements, the workaround that you described might work:

   type HDLC_Frame is
      message
         -- ...
         Virtual_Control : Control;
         Control : Opaque
            with First => Virtual_Control'First, Size => 8;
         -- ...
      end message;

   for HDLC_Frame use (Control => I_Frame_Control)
      if Virtual_Control mod 2 = 0;

   for HDLC_Frame use (Control => S_Frame_Control)
      if Virtual_Control mod 4 = 1;

   for HDLC_Frame use (Control => U_Frame_Control)
      if Virtual_Control mod 4 = 3;

I also think that for a reasonable specification, the bit order must be configurable. The mechanisms discussed in #1254 could probably be used to specify the type field in the U-frame, but #1254 is still in the design stage.