Scalar types represented by complex structure

[treiher]

Context and Problem Statement

There are cases where a scalar value (usually an integer) is represented by a complex structure. One example would be variable-length integers (#8). While some of these constructs are representable with the current means, their handling is cumbersome. That is caused by the fact that a single logical entity (like the Tag type or the Length in the ASN.1 BER encoding) cannot be represented as a single message field. In each place where such a logical entity is used, a differentiation between the possible variants is required to determine which message field for the desired value must be actually accessed.

Another example would be the ASN.1 BER encoding, where each message and each message field is represented by a TLV structure. Using the generated code to serialize such a message would require to determine and set the values of the Tag and the Length for each field manually, which gets very cumbersome for nested messages.

Use Cases

• #8
• ASN.1 encodings

Design

• Link scalar types to structure
• Allow messages to be interpreted as scalar value
• Allow sequences to be interpreted as scalar value

Examples

(see also example specifications on issue_8 branch)

package QUIC is

   type Length is (L6, L14, L30, L62) with Size => 2;
   type U6 is range 0 .. 2 ** 6 - 1 with Size => 6;
   type U14 is range 0 .. 2 ** 14 - 1 with Size => 14;
   type U30 is range 0 .. 2 ** 30 - 1 with Size => 30;
   type U62 is range 0 .. 2 ** 62 - 1 with Size => 62;

   type Variable_Length_Integer is
      message
         Length : Length
            then U6
               if Length = L6
            then U14
               if Length = L14
            then U30
               if Length = L30
            then U62
               if Length = L62;
         U6 : U6
            then null;
         U14 : U14
            then null;
         U30 : U30
            then null;
         U62 : U62;
      end message with
         Deserialize =>
            (case Length is
               L6 => U6,
               L14 => U14,
               L30 => U30,
               L62 => U62),
         Serialize =>
            (case Variable_Length_Integer'Value is
               0 .. 2 ** 6 - 1 =>
                  (Length => L6,
                   U6 => Variable_Length_Integer'Value),
               2 ** 6 .. 2 ** 14 - 1 =>
                  (Length => L14,
                   U14 => Variable_Length_Integer'Value),
               2 ** 14 .. 2 ** 30 - 1 =>
                  (Length => L30,
                   U30 => Variable_Length_Integer'Value),
               2 ** 30 .. 2 ** 62 - 1 =>
                  (Length => L62,
                   U62 => Variable_Length_Integer'Value));


   type Integer is range 0 .. 2 ** 62 - 1
   with
      Structure => Variable_Length_Integer;

end QUIC;

package MQTT is

   type Integer is range 0 .. 2 ** 32 - 1 with
      Structure => Variable_Byte_Integer;

   type U7 is range 0 .. 2 ** 7 -1 with Size => 7;

   type Variable_Byte_Integer_Element is
      message
         More : Boolean;
         Value : U7;
      end message;

   type Variable_Byte_Integer is sequence of Variable_Byte_Integer_Element
   with
      Deserialize =>
         (Initial => 0,
          Next => Variable_Byte_Integer'Current + Variable_Byte_Integer'Element.Value * 128 ** (Variable_Byte_Integer'Position - 1),
          Until => (Variable_Byte_Integer'Element.More = False)),
      Serialize =>
         (Size => Variable_Byte_Integer'Value'Size,
          Set => (More => Variable_Byte_Integer'Current >= 128,
                  Value => Variable_Byte_Integer'Current mod 128),
          Next => Variable_Byte_Integer'Current / 128,
          Until => Variable_Byte_Integer'Current = 0);

end MQTT;

package BER is

   --
   -- Identifier
   --

   type Tag_Class is (TC_Universal, TC_Application, TC_Context_Specific, TC_Private) with
      Size => 2;
   type Tag_Type_Short is range 0 .. 31 with
      Size => 5;

   type Tag_Type_Long_Octet is
      message
         More : Boolean;
         Tag_Type_Part : Tag_Type_Part;
      end message;

   type Tag_Type_Long_Structure is sequence of Tag_Type_Long_Structure_Octet with
      Deserialize =>
        (Initial => 0,
         Next => Tag_Type_Long_Structure'Current * 128 + Tag_Type_Long_Structure'Element.Tag_Type_Part,
         Until => (Tag_Type_Long_Structure'Element.More = False)),
      Serialize =>
         (Size => Tag_Type_Long_Structure'Value'Size,
          Set => (More => Tag_Type_Long_Structure'Position < Tag_Type_Long_Structure'Last_Element,
                  Value => Tag_Type_Long_Structure'Current mod 128),
          Next => Tag_Type_Long_Structure'Current / 128,
          Reverse => True);

   type Tag_Type_Long is range 0 .. 2 ** 63 - 1 with
      Structure => Tag_Type_Long_Structure;

   type Identifier is
      message
         Tag_Class : Tag_Class;
         Primitive : Boolean;
         null : Ignore
            with Size => 5;
         Tag_Type : Tag_Type
            with First => Tag_Class'First;
      end message;

   type Tag_Type is range 0 .. 2 ** 63  - 1 with
      Structure => Tag_Type_Structure;

   type Tag_Type_Structure is
      message
         null : Ignore
            with Size => 3;
         Tag_Type_Short : Tag_Type_Short
            then null
               if Tag_Type_Short < 31,
            then Tag_Type_Long = 31;
         Tag_Type_Long : Tag_Type_Long;
      end message with
         Deserialize =>
            (if Tag_Type_Short < 31 then Tag_Type_Short else Tag_Type_Long),
         Serialize =>
            (if Tag_Type_Structure'Value < 31
             then (Tag_Type_Short => Tag_Type_Structure'Value)
             else (Tag_Type_Long => Tag_Type_Structure'Value));

   --
   -- Length
   --
 
   type Octet is range 0 .. 2 ** 8 - 1 with
      Size => 8;

   type Long_Length_Octets is sequence of Octet with
      Deserialize =>
        (Initial => 0,
         Next    => Long_Length_Octets'Current * 256 + Long_Length_Octets'Element);
      Serialize =>
        (Value   => Long_Length_Octets'Value mod 256,
         Next    => Long_Length_Octets'Value / 256,
         Reverse => True);

   type Long_Length is range 0 .. 2 ** 63 - 1 with
      Structure => Long_Length_Octets;
 
   type Short_Length is range 0 .. 2 ** 7 - 1 with
      Size => 7;

   type Length_Octets is
      message
         Form : Boolean;
         Short_Length : Short_Length
            then null
               if Form = False or (Form = True and Short_Length = 127)
            then Long_Length
               with Size => Short_Length * 8
               if Form = True;
         Long_Length : Long_Length;
      end message with
         Deserialize =>
           (if Form = False then Short_Length else Long_Length),
         Serialize =>
           (if Length_Octets'Value >= 128
            then (Form => True,
                  Short_Length => Length_Octets'Value'Size / 8 + 1,
                  Long_Length  => Length_Octets'Value)
            else (Form => False,
                  Short_Length => Length_Octets'Value);

         -- Serialize =>
         --    (Form         => Length_Octets'Value >= 128,
         --     Short_Length => (if Length_Octets'Value < 128
         --                      then Length_Octets'Value
         --                      else (Length_Octets'Value'Size / 8 + 1)),
         --     Long_Length => (if Length_Octets'Value >= 128
         --                     then Length_Octets'Value
         --                     else null));

         -- Serialize =>
         --    (Form         => Length_Octets'Value >= 128,
         --     if Form then
         --       Long_Length => Length_Octets'Value,
         --       Short_Length => Length_Octets'Value'Size / 8 + 1
         --     else
         --       Short_Length => Length_Octets'Value);

   type Length is range 0 .. 2 ** 63 - 1 with
      Structure => Length_Octets;

   --
   -- TLV
   --

   type TLV is
      message
         Identifier : Identifier:
         Length : Length:
         Content : Opaque
            with Size => Length * 8;
      end message;