Ensure message size is multiple of 8 bit

Ref. #579

README.md

@@ -58,8 +58,8 @@ The structure of messages is often non-linear because of optional fields. For th
 ```Ada RFLX
 package TLV is
 
-   type Tag is (Msg_Data => 1, Msg_Error => 3) with Size => 2;
-   type Length is mod 2**14;
+   type Tag is (Msg_Data => 1, Msg_Error => 3) with Size => 8;
+   type Length is mod 2**16;
 
    type Message is
       message
@@ -179,7 +179,7 @@ with RFLX.RFLX_Builtin_Types;
 with RFLX.TLV.Message;
 
 procedure Main is
-   Buffer  : RFLX.RFLX_Builtin_Types.Bytes_Ptr := new RFLX.RFLX_Builtin_Types.Bytes'(64, 4, 0, 0, 0, 0);
+   Buffer  : RFLX.RFLX_Builtin_Types.Bytes_Ptr := new RFLX.RFLX_Builtin_Types.Bytes'(1, 0, 4, 0, 0, 0, 0);
    Context : RFLX.TLV.Message.Context;
 begin
    RFLX.TLV.Message.Initialize (Context, Buffer);
@@ -213,7 +213,7 @@ with RFLX.RFLX_Builtin_Types; use type RFLX.RFLX_Builtin_Types.Length, RFLX.RFLX
 with RFLX.TLV.Message;
 
 procedure Main is
-   Buffer  : RFLX.RFLX_Builtin_Types.Bytes_Ptr := new RFLX.RFLX_Builtin_Types.Bytes'(0, 0, 0, 0, 0, 0);
+   Buffer  : RFLX.RFLX_Builtin_Types.Bytes_Ptr := new RFLX.RFLX_Builtin_Types.Bytes'(0, 0, 0, 0, 0, 0, 0);
    Context : RFLX.TLV.Message.Context;
 begin
    --  Generating message
@@ -224,7 +224,7 @@ begin
 
    --  Checking generated message
    RFLX.TLV.Message.Take_Buffer (Context, Buffer);
-   if Buffer.all = (64, 4, 1, 2, 3, 4) then
+   if Buffer.all = (1, 0, 4, 1, 2, 3, 4) then
       Ada.Text_IO.Put_Line ("Expected");
    else
       Ada.Text_IO.Put_Line ("Unexpected");
@@ -260,7 +260,7 @@ def create_message() -> MessageValue:
     return msg
 
 
-if parse_message(b"\x40\x04\x01\x02\x03\x04") != create_message():
+if parse_message(b"\x01\x00\x04\x01\x02\x03\x04") != create_message():
     sys.exit("Error")
 ```
 

doc/Language-Reference.md

@@ -119,6 +119,8 @@ A message type is a collection components. Additional then clauses allow to defi
 
 A message type specifies the message format of a protocol. Each component corresponds to one field in a message. A then clause of a component allows to define which field follows. If no then clause is given, it is assumed that always the next component of the message follows. If no further component follows, it is assumed that the message ends with this field. The end of a message can also be denoted explicitly by adding a then clause to __null__. Optionally a then clause can contain a condition under which the corresponding field follows and aspects which allow to define the size of the next field and the location of its first bit. These aspects can also be specified in the component. Each aspect can be specified either in the component or in all incoming then clauses, but not in both. The condition can refer to previous fields (including the component containing the then clause). A condition can also be added to a component. A component condition is equivalent to adding a condition to all incoming then clauses. If a component condition as well as a condition at an incoming then clause exists, both conditions are combined by a logical conjunction. If required, a null component can be used to specify the size of the first field in the message. An empty message can be represented by a null message.
 
+The size of a message must be a multiple of 8 bit. Opaque fields and array fields must be byte aligned.
+
 #### Example
 
 ```Ada RFLX declaration

rflx/model/message.py

@@ -613,6 +613,7 @@ def verify(self) -> None:
             self.__prove_coverage()
             self.__prove_overlays()
             self.__prove_field_positions()
+            self.__prove_message_size()
 
             self.error.propagate()
 
@@ -1180,6 +1181,48 @@ def __prove_field_positions(self) -> None:
                         )
                         return
 
+    def __prove_message_size(self) -> None:
+        """
+        Prove that all message paths lead to a message with a size that is a multiple of 8 bit.
+        """
+        type_constraints = self.type_constraints(expr.TRUE)
+        field_size_constraints = [
+            expr.Equal(expr.Mod(expr.Size(f.name), expr.Number(8)), expr.Number(0))
+            for f, t in self.types.items()
+            if isinstance(t, (mty.Opaque, mty.Array))
+        ]
+
+        for path in [p[:-1] for p in self.paths(FINAL) if p]:
+            message_size = expr.Add(
+                *[
+                    expr.Size(link.target.name)
+                    for link in path
+                    if link.target != FINAL and link.first == expr.UNDEFINED
+                ]
+            )
+            facts = [
+                *[fact for link in path for fact in self.__link_expression(link)],
+                *type_constraints,
+                *field_size_constraints,
+            ]
+            proof = expr.NotEqual(expr.Mod(message_size, expr.Number(8)), expr.Number(0)).check(
+                facts
+            )
+            if proof.result == expr.ProofResult.SAT:
+                self.error.append(
+                    "message size must be multiple of 8 bit",
+                    Subsystem.MODEL,
+                    Severity.ERROR,
+                    self.identifier.location,
+                )
+                self.error.append(
+                    "on path " + " -> ".join(l.target.name for l in path),
+                    Subsystem.MODEL,
+                    Severity.INFO,
+                    self.identifier.location,
+                )
+                return
+
     def __prove_path_property(self, prop: expr.Expr, path: Sequence[Link]) -> expr.Proof:
         conditions = [l.condition for l in path if l.condition != expr.TRUE]
         sizes = [

rflx/pyrflx/typevalue.py

@@ -1036,9 +1036,7 @@ def value(self) -> Any:
 
     def _unchecked_bytestring(self) -> bytes:
         bits = str(self.bitstring)
-        if len(bits) < 8:
-            bits = bits.ljust(8, "0")
-
+        assert len(bits) % 8 == 0
         return b"".join(
             [int(bits[i : i + 8], 2).to_bytes(1, "big") for i in range(0, len(bits), 8)]
         )

tests/data/models.py

@@ -39,9 +39,9 @@
 NULL_MODEL = Model([NULL_MESSAGE])
 
 TLV_TAG = Enumeration(
-    "TLV::Tag", [("Msg_Data", Number(1)), ("Msg_Error", Number(3))], Number(2), False
+    "TLV::Tag", [("Msg_Data", Number(1)), ("Msg_Error", Number(3))], Number(8), False
 )
-TLV_LENGTH = ModularInteger("TLV::Length", Pow(Number(2), Number(14)))
+TLV_LENGTH = ModularInteger("TLV::Length", Pow(Number(2), Number(16)))
 TLV_MESSAGE = Message(
     "TLV::Message",
     [
@@ -126,7 +126,7 @@
 ENUMERATION_PRIORITY = Enumeration(
     "Enumeration::Priority",
     [("Low", Number(1)), ("Medium", Number(4)), ("High", Number(7))],
-    Number(3),
+    Number(8),
     True,
 )
 ENUMERATION_MESSAGE = Message(

tests/data/specs/tlv.rflx

@@ -1,7 +1,7 @@
 package TLV is
 
-   type Tag is (Msg_Data => 1, Msg_Error => 3) with Size => 2;
-   type Length is mod 2**14;
+   type Tag is (Msg_Data => 1, Msg_Error => 3) with Size => 8;
+   type Length is mod 2**16;
 
    type Message is
       message

tests/data/specs/tlv_with_checksum.rflx

@@ -1,7 +1,7 @@
 package TLV_With_Checksum is
 
-   type Tag is (Msg_Data => 1, Msg_Error => 3) with Size => 2;
-   type Length is mod 2**14;
+   type Tag is (Msg_Data => 1, Msg_Error => 3) with Size => 8;
+   type Length is mod 2**16;
    type Checksum is mod 2**32;
 
    type Message is

tests/ide/ide_test.py

@@ -74,6 +74,8 @@ def test_multiple_errors() -> None:
             f'{path}:86:9: model: error: unsupported element type size of array "A3"',
             f'{path}:85:9: model: info: type "E6" has size 4, must be multiple of 8',
             f'{path}:93:30: model: error: invalid First for field "Final"',
+            f"{path}:96:9: model: error: message size must be multiple of 8 bit",
+            f"{path}:96:9: model: info: on path Field",
             f'{path}:103:26: model: error: size of opaque field "Data" not multiple of 8 bit'
             " (Length -> Data)",
             f'{path}:106:4: parser: error: undefined type "RFLX_Invalid::PDU1" in refinement',
@@ -174,5 +176,7 @@ def test_parse_error_invalid_location() -> None:
         path,
         [
             f'{path}:7:21: parser: error: invalid aspect "Invalid"',
+            f"{path}:3:9: model: error: message size must be multiple of 8 bit",
+            f"{path}:3:9: model: info: on path Y",
         ],
     )

tests/integration/session/greentls.rflx

@@ -44,7 +44,7 @@ package GreenTLS is
    for Control_Message use (Data => Key_Update_Message)
       if Tag = Key_Update_Client or Tag = Key_Update_Server;
 
-   type Heartbeat_Mode is (Heartbeat_Enabled, Heartbeat_Disabled) with Size => 4;
+   type Heartbeat_Mode is (Heartbeat_Enabled, Heartbeat_Disabled) with Size => 8;
 
    type Heartbeat_Control_Message is
       message
@@ -112,6 +112,8 @@ package GreenTLS is
          Data : Opaque;
       end message;
 
+   type Padding is range 0 .. 0 with Size => 2;
+
    type Configuration is
       message
          PSK_Key_Exchange_Modes : TLS_Handshake::PSK_Key_Exchange_Modes;  -- FIXME: must only contain PSK_KE and/or PSK_DHE_KE
@@ -136,6 +138,7 @@ package GreenTLS is
          Max_Fragment_Length_Enabled : Boolean;
          Max_Fragment_Length : TLS_Handshake::Max_Fragment_Length_Value;
          Heartbeat_Mode : Heartbeat_Mode;
+         Padding : Padding;
       end message;
 
    type Name_Length is range 1 .. 253 with Size => 8;

tests/integration/specs_test.py

@@ -402,22 +402,22 @@ def test_tlv() -> None:
 
 
 def test_tlv_parsing_tlv_data(tlv_message_value: pyrflx.MessageValue) -> None:
-    test_bytes = b"\x40\x04\x00\x00\x00\x00"
+    test_bytes = b"\x01\x00\x04\x00\x00\x00\x00"
     tlv_message_value.parse(test_bytes)
     assert tlv_message_value.valid_message
     assert tlv_message_value.bytestring == test_bytes
 
 
 def test_tlv_parsing_tlv_data_zero(tlv_message_value: pyrflx.MessageValue) -> None:
-    test_bytes = b"\x40\x00"
+    test_bytes = b"\x01\x00\x00"
     tlv_message_value.parse(test_bytes)
     assert tlv_message_value.get("Tag") == "Msg_Data"
     assert tlv_message_value.get("Length") == 0
     assert tlv_message_value.valid_message
 
 
 def test_tlv_parsing_tlv_error(tlv_message_value: pyrflx.MessageValue) -> None:
-    test_bytes = b"\xc0"
+    test_bytes = b"\x03"
     tlv_message_value.parse(test_bytes)
     assert tlv_message_value.get("Tag") == "Msg_Error"
     assert tlv_message_value.valid_message
@@ -439,7 +439,7 @@ def test_tlv_parsing_invalid_tlv_invalid_tag(tlv_message_value: pyrflx.MessageVa
 
 
 def test_tlv_generating_tlv_data(tlv_message_value: pyrflx.MessageValue) -> None:
-    expected = b"\x40\x04\x00\x00\x00\x00"
+    expected = b"\x01\x00\x04\x00\x00\x00\x00"
     tlv_message_value.set("Tag", "Msg_Data")
     tlv_message_value.set("Length", 4)
     tlv_message_value.set("Value", b"\x00\x00\x00\x00")
@@ -456,7 +456,7 @@ def test_tlv_generating_tlv_data_zero(tlv_message_value: pyrflx.MessageValue) ->
 def test_tlv_generating_tlv_error(tlv_message_value: pyrflx.MessageValue) -> None:
     tlv_message_value.set("Tag", "Msg_Error")
     assert tlv_message_value.valid_message
-    assert tlv_message_value.bytestring == b"\xc0"
+    assert tlv_message_value.bytestring == b"\x03"
 
 
 def test_tls(tmp_path: Path) -> None:

tests/property/strategies.py

@@ -183,7 +183,7 @@ def messages(
     unique_identifiers: Generator[ID, None, None],
     not_null: bool = False,
 ) -> Message:
-    # pylint: disable=too-many-locals
+    # pylint: disable=too-many-locals, too-many-statements
 
     @dataclass
     class FieldPair:
@@ -266,15 +266,11 @@ def outgoing(field: Field) -> Sequence[Link]:
                 field_size = int(types_[source].size) if isinstance(types_[source], Scalar) else 0
                 target_alignment = (alignments[source] + field_size) % 8
                 potential_targets = [
-                    f
-                    for f in fields_[i + 1 :]
-                    if alignments[f] == target_alignment and f != out[0].target
+                    f for f in fields_[i + 1 :] if alignments[f] == target_alignment
                 ]
-                target = draw(
-                    st.sampled_from(
-                        potential_targets if potential_targets else [out[0].target, FINAL]
-                    )
-                )
+                if target_alignment == 0:
+                    potential_targets.append(FINAL)
+                target = draw(st.sampled_from(potential_targets))
                 pair = FieldPair(
                     source, target, types_[source], types_[target] if target != FINAL else None
                 )
@@ -288,8 +284,17 @@ def outgoing(field: Field) -> Sequence[Link]:
                 )
 
         loose_ends = [f for f in fields_ if all(l.source != f for l in structure)]
-        for l in loose_ends:
-            structure.append(Link(l, FINAL))
+        for field in loose_ends:
+            field_size = int(types_[f].size) if isinstance(types_[f], Scalar) else 0
+            padding = (alignments[field] + field_size) % 8
+            if padding == 0:
+                structure.append(Link(field, FINAL))
+            else:
+                f = draw(fields())
+                t = draw(scalars(unique_identifiers, align_to_8=padding))
+                types_[f] = t
+                structure.append(Link(field, f))
+                structure.append(Link(f, FINAL))
 
     message = UnprovenMessage(next(unique_identifiers), structure, types_)
 

tests/spark/generated/rflx-enumeration.ads

@@ -5,11 +5,11 @@ package RFLX.Enumeration with
   SPARK_Mode
 is
 
-   type Priority_Base is mod 2**3;
+   type Priority_Base is mod 2**8;
 
    type Priority_Enum is (Low, Medium, High) with
      Size =>
-       3;
+       8;
    for Priority_Enum use (Low => 1, Medium => 4, High => 7);
 
    type Priority (Known : Boolean := False) is

tests/spark/generated/rflx-tlv.ads

@@ -5,11 +5,11 @@ package RFLX.TLV with
   SPARK_Mode
 is
 
-   type Tag_Base is mod 2**2;
+   type Tag_Base is mod 2**8;
 
    type Tag is (Msg_Data, Msg_Error) with
      Size =>
-       2;
+       8;
    for Tag use (Msg_Data => 1, Msg_Error => 3);
 
    pragma Warnings (Off, "precondition is * false");
@@ -52,9 +52,9 @@ is
 
    pragma Warnings (On, "unreachable branch");
 
-   type Length is mod 2**14 with
+   type Length is mod 2**16 with
      Size =>
-       14;
+       16;
 
    pragma Warnings (Off, "precondition is * false");
 

tests/spark/rflx-derivation_tests.adb

@@ -43,7 +43,7 @@ package body RFLX.Derivation_Tests is
      SPARK_Mode, Pre => True
    is
       pragma Unreferenced (T);
-      Buffer  : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(64, 4, 0, 0, 0, 0);
+      Buffer  : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(1, 0, 4, 0, 0, 0, 0);
       Context : Derivation.Message.Context;
       Tag     : TLV.Tag;
       Length  : TLV.Length;
@@ -72,16 +72,16 @@ package body RFLX.Derivation_Tests is
       Derivation.Message.Take_Buffer (Context, Buffer);
       Free_Bytes_Ptr (Buffer);
 
-      Assert (Context.Last'Image, RFLX_Builtin_Types.Bit_Length (48)'Image, "Invalid Context.Last");
+      Assert (Context.Last'Image, RFLX_Builtin_Types.Bit_Length (56)'Image, "Invalid Context.Last");
    end Test_Parsing;
 
    procedure Test_Generating (T : in out AUnit.Test_Cases.Test_Case'Class) with
      SPARK_Mode, Pre => True
    is
       pragma Unreferenced (T);
       procedure Set_Value is new Derivation.Message.Generic_Set_Value (Write_Data, Valid_Data_Length);
-      Expected : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(64, 4, 0, 0, 0, 0);
-      Buffer   : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(0, 0, 0, 0, 0, 0);
+      Expected : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(1, 0, 4, 0, 0, 0, 0);
+      Buffer   : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(0, 0, 0, 0, 0, 0, 0);
       Context  : Derivation.Message.Context;
    begin
       Derivation.Message.Initialize (Context, Buffer);