From 6d4179eeffa54e97df3d2bc33e3992611ef1247e Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Fri, 26 Feb 2021 15:33:06 +0100 Subject: [PATCH] Ensure message size is multiple of 8 bit Ref. #579 --- README.md | 12 +++--- doc/Language-Reference.md | 2 + rflx/model/message.py | 43 ++++++++++++++++++++++ rflx/pyrflx/typevalue.py | 4 +- tests/data/models.py | 6 +-- tests/data/specs/tlv.rflx | 4 +- tests/data/specs/tlv_with_checksum.rflx | 4 +- tests/ide/ide_test.py | 4 ++ tests/integration/session/greentls.rflx | 5 ++- tests/integration/specs_test.py | 10 ++--- tests/property/strategies.py | 27 ++++++++------ tests/spark/generated/rflx-enumeration.ads | 4 +- tests/spark/generated/rflx-tlv.ads | 8 ++-- tests/spark/rflx-derivation_tests.adb | 8 ++-- tests/spark/rflx-enumeration_tests.adb | 8 ++-- tests/spark/rflx-in_tlv_tests.adb | 4 +- tests/spark/rflx-tlv_tests.adb | 24 ++++++------ tests/unit/pyrflx_test.py | 22 +++++------ 18 files changed, 127 insertions(+), 72 deletions(-) diff --git a/README.md b/README.md index 12ecb1346..e0f0a5555 100644 --- a/README.md +++ b/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") ``` diff --git a/doc/Language-Reference.md b/doc/Language-Reference.md index e72778241..460303cce 100644 --- a/doc/Language-Reference.md +++ b/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 diff --git a/rflx/model/message.py b/rflx/model/message.py index 9cafe7350..d44aa1247 100644 --- a/rflx/model/message.py +++ b/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 = [ diff --git a/rflx/pyrflx/typevalue.py b/rflx/pyrflx/typevalue.py index f370fe1fd..666acf2cc 100644 --- a/rflx/pyrflx/typevalue.py +++ b/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)] ) diff --git a/tests/data/models.py b/tests/data/models.py index 46cd83a1e..571ce7c37 100644 --- a/tests/data/models.py +++ b/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( diff --git a/tests/data/specs/tlv.rflx b/tests/data/specs/tlv.rflx index b6b5f30d1..82bfade10 100644 --- a/tests/data/specs/tlv.rflx +++ b/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 diff --git a/tests/data/specs/tlv_with_checksum.rflx b/tests/data/specs/tlv_with_checksum.rflx index 13338f694..ef5c3e7d9 100644 --- a/tests/data/specs/tlv_with_checksum.rflx +++ b/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 diff --git a/tests/ide/ide_test.py b/tests/ide/ide_test.py index 6ea7a0203..6a251d46d 100644 --- a/tests/ide/ide_test.py +++ b/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", ], ) diff --git a/tests/integration/session/greentls.rflx b/tests/integration/session/greentls.rflx index be41bdda5..d34646ed2 100644 --- a/tests/integration/session/greentls.rflx +++ b/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; diff --git a/tests/integration/specs_test.py b/tests/integration/specs_test.py index 1005f8519..301edfcc0 100644 --- a/tests/integration/specs_test.py +++ b/tests/integration/specs_test.py @@ -402,14 +402,14 @@ 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 @@ -417,7 +417,7 @@ def test_tlv_parsing_tlv_data_zero(tlv_message_value: pyrflx.MessageValue) -> No 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: diff --git a/tests/property/strategies.py b/tests/property/strategies.py index 21be2b414..346267313 100644 --- a/tests/property/strategies.py +++ b/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_) diff --git a/tests/spark/generated/rflx-enumeration.ads b/tests/spark/generated/rflx-enumeration.ads index 846eb5c1c..f33f662bd 100644 --- a/tests/spark/generated/rflx-enumeration.ads +++ b/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 diff --git a/tests/spark/generated/rflx-tlv.ads b/tests/spark/generated/rflx-tlv.ads index e9a5e29d3..d38df6ea9 100644 --- a/tests/spark/generated/rflx-tlv.ads +++ b/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"); diff --git a/tests/spark/rflx-derivation_tests.adb b/tests/spark/rflx-derivation_tests.adb index ee970ce28..85be8ba8b 100644 --- a/tests/spark/rflx-derivation_tests.adb +++ b/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,7 +72,7 @@ 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 @@ -80,8 +80,8 @@ package body RFLX.Derivation_Tests is 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); diff --git a/tests/spark/rflx-enumeration_tests.adb b/tests/spark/rflx-enumeration_tests.adb index 998729952..fb010677d 100644 --- a/tests/spark/rflx-enumeration_tests.adb +++ b/tests/spark/rflx-enumeration_tests.adb @@ -19,7 +19,7 @@ package body RFLX.Enumeration_Tests is SPARK_Mode, Pre => True is pragma Unreferenced (T); - Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(32, 0); + Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(1, 0); Context : Enumeration.Message.Context; Prio : Enumeration.Priority; begin @@ -49,7 +49,7 @@ package body RFLX.Enumeration_Tests is SPARK_Mode, Pre => True is pragma Unreferenced (T); - Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(160, 0); + Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(5, 0); Context : Enumeration.Message.Context; Prio : Enumeration.Priority; begin @@ -79,13 +79,13 @@ package body RFLX.Enumeration_Tests is SPARK_Mode, Pre => True is pragma Unreferenced (T); - Expected : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(RFLX_Builtin_Types.Index'First => 32); + Expected : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(RFLX_Builtin_Types.Index'First => 4); Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(0, 0); Context : Enumeration.Message.Context; begin Enumeration.Message.Initialize (Context, Buffer); - Enumeration.Message.Set_Priority (Context, Enumeration.Low); + Enumeration.Message.Set_Priority (Context, Enumeration.Medium); Assert (Enumeration.Message.Structural_Valid_Message (Context), "Structural invalid message"); Assert (Enumeration.Message.Valid_Message (Context), "Invalid message"); diff --git a/tests/spark/rflx-in_tlv_tests.adb b/tests/spark/rflx-in_tlv_tests.adb index 855dbb4cb..e1e53d9c3 100644 --- a/tests/spark/rflx-in_tlv_tests.adb +++ b/tests/spark/rflx-in_tlv_tests.adb @@ -19,7 +19,7 @@ package body RFLX.In_TLV_Tests is SPARK_Mode, Pre => True is pragma Unreferenced (T); - Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(64, 0); + Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(1, 0, 0); TLV_Message_Context : TLV.Message.Context; Valid : Boolean; begin @@ -35,7 +35,7 @@ package body RFLX.In_TLV_Tests is TLV.Message.Take_Buffer (TLV_Message_Context, Buffer); Free_Bytes_Ptr (Buffer); - Assert (TLV_Message_Context.Last'Image, RFLX_Builtin_Types.Bit_Length (16)'Image, "Invalid Context.Last"); + Assert (TLV_Message_Context.Last'Image, RFLX_Builtin_Types.Bit_Length (24)'Image, "Invalid Context.Last"); end Test_Null_In_TLV; overriding diff --git a/tests/spark/rflx-tlv_tests.adb b/tests/spark/rflx-tlv_tests.adb index 6f43587ef..d3830b14b 100644 --- a/tests/spark/rflx-tlv_tests.adb +++ b/tests/spark/rflx-tlv_tests.adb @@ -42,7 +42,7 @@ package body RFLX.TLV_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 : TLV.Message.Context; Tag : TLV.Tag; Length : TLV.Length; @@ -71,14 +71,14 @@ package body RFLX.TLV_Tests is TLV.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_TLV_Data; procedure Test_Parsing_TLV_Data_Zero (T : in out AUnit.Test_Cases.Test_Case'Class) with SPARK_Mode, Pre => True is pragma Unreferenced (T); - Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(64, 0); + Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(1, 0, 0); Context : TLV.Message.Context; Tag : TLV.Tag; Length : TLV.Length; @@ -102,14 +102,14 @@ package body RFLX.TLV_Tests is TLV.Message.Take_Buffer (Context, Buffer); Free_Bytes_Ptr (Buffer); - Assert (Context.Last'Image, RFLX_Builtin_Types.Bit_Length (16)'Image, "Invalid Context.Last"); + Assert (Context.Last'Image, RFLX_Builtin_Types.Bit_Length (24)'Image, "Invalid Context.Last"); end Test_Parsing_TLV_Data_Zero; procedure Test_Parsing_TLV_Error (T : in out AUnit.Test_Cases.Test_Case'Class) with SPARK_Mode, Pre => True is pragma Unreferenced (T); - Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(1 => 192); + Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(RFLX_Builtin_Types.Index'First => 3); Context : TLV.Message.Context; Tag : TLV.Tag; begin @@ -151,8 +151,8 @@ package body RFLX.TLV_Tests is SPARK_Mode, Pre => True is pragma Unreferenced (T); - Expected : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(64, 4, 1, 2, 3, 4); - 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, 1, 2, 3, 4); + Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(0, 0, 0, 0, 0, 0, 0); Context : TLV.Message.Context; begin TLV.Message.Initialize (Context, Buffer); @@ -180,8 +180,8 @@ package body RFLX.TLV_Tests is is pragma Unreferenced (T); procedure Set_Value is new TLV.Message.Generic_Set_Value (Write_Data, Valid_Data_Length); - Expected : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(64, 4, 1, 2, 3, 4); - 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, 1, 2, 3, 4); + Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(0, 0, 0, 0, 0, 0, 0); Context : TLV.Message.Context; begin TLV.Message.Initialize (Context, Buffer); @@ -209,8 +209,8 @@ package body RFLX.TLV_Tests is SPARK_Mode, Pre => True is pragma Unreferenced (T); - Expected : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(64, 0); - Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(0, 0); + Expected : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(1, 0, 0); + Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(0, 0, 0); Context : TLV.Message.Context; begin TLV.Message.Initialize (Context, Buffer); @@ -238,7 +238,7 @@ package body RFLX.TLV_Tests is is pragma Unreferenced (T); Expected : RFLX_Builtin_Types.Bytes_Ptr := - new RFLX_Builtin_Types.Bytes'(RFLX_Builtin_Types.Index'First => 192); + new RFLX_Builtin_Types.Bytes'(RFLX_Builtin_Types.Index'First => 3); Buffer : RFLX_Builtin_Types.Bytes_Ptr := new RFLX_Builtin_Types.Bytes'(RFLX_Builtin_Types.Index'First => 0); Context : TLV.Message.Context; begin diff --git a/tests/unit/pyrflx_test.py b/tests/unit/pyrflx_test.py index a9d8de3f7..abfbace3e 100644 --- a/tests/unit/pyrflx_test.py +++ b/tests/unit/pyrflx_test.py @@ -121,11 +121,11 @@ def test_message_value_eq(tlv_package: Package) -> None: def test_message_value_bitstring(tlv_message_value: MessageValue) -> None: assert tlv_message_value.bitstring == Bitstring("") tlv_message_value.set("Tag", "Msg_Data") - assert tlv_message_value.bitstring == Bitstring("01") + assert tlv_message_value.bitstring == Bitstring("00000001") tlv_message_value.set("Length", 1) - assert tlv_message_value.bitstring == Bitstring("0100000000000001") + assert tlv_message_value.bitstring == Bitstring("000000010000000000000001") tlv_message_value.set("Value", b"\x01") - assert tlv_message_value.bitstring == Bitstring("010000000000000100000001") + assert tlv_message_value.bitstring == Bitstring("00000001000000000000000100000001") def test_message_value_all_fields( @@ -197,7 +197,7 @@ def test_message_value_valid_message(tlv_message_value: MessageValue) -> None: assert_bytestring_error(tlv_message_value, tlv_message_value.identifier) 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" tlv_message_value.set("Tag", "Msg_Data") assert not tlv_message_value.valid_message assert_bytestring_error(tlv_message_value, tlv_message_value.identifier) @@ -206,7 +206,7 @@ def test_message_value_valid_message(tlv_message_value: MessageValue) -> None: assert_bytestring_error(tlv_message_value, tlv_message_value.identifier) tlv_message_value.set("Value", b"\x01") assert tlv_message_value.valid_message - assert tlv_message_value.bytestring == b"\x40\x01\x01" + assert tlv_message_value.bytestring == b"\x01\x00\x01\x01" def test_message_value_valid_fields(tlv_message_value: MessageValue) -> None: @@ -239,7 +239,7 @@ def test_message_value_set_value(tlv_message_value: MessageValue) -> None: def test_message_value_generate(tlv_message_value: MessageValue) -> None: test_message_value_payload = b"\x01\x02\x03\x04\x05\x06\x07\x08" - test_message_value_data = b"\x40\x08" + test_message_value_payload + test_message_value_data = b"\x01\x00\x08" + test_message_value_payload tlv_message_value.set("Tag", "Msg_Data") tlv_message_value.set("Length", 8) tlv_message_value.set("Value", test_message_value_payload) @@ -262,7 +262,7 @@ def test_message_value_binary_length(tlv_message_value: MessageValue) -> None: tlv_message_value.set("Tag", "Msg_Data") tlv_message_value.set("Length", 8) tlv_message_value.set("Value", bytes(8)) - assert tlv_message_value.bytestring == b"\x40\x08\x00\x00\x00\x00\x00\x00\x00\x00" + assert tlv_message_value.bytestring == b"\x01\x00\x08\x00\x00\x00\x00\x00\x00\x00\x00" def test_message_value_set_get_value(tlv_message_value: MessageValue) -> None: @@ -347,7 +347,7 @@ def test_message_value_empty_opaque_field(tlv_message_value: MessageValue) -> No tlv_message_value.set("Length", 0) tlv_message_value.set("Value", b"") assert tlv_message_value.valid_message - assert tlv_message_value.bytestring == b"\x40\x00" + assert tlv_message_value.bytestring == b"\x01\x00\x00" def test_message_value_field_eq() -> None: @@ -444,7 +444,7 @@ def test_message_value_parse_from_bitstring_invalid(tlv_message_value: MessageVa Bitstring("123") assert Bitstring("01") + Bitstring("00") == Bitstring("0100") - test_bytes = b"\x40" + test_bytes = b"\x01" with pytest.raises( PyRFLXError, match=( @@ -809,7 +809,7 @@ def test_array_assign_invalid( "$" ), ): - msg_array.parse(Bitstring("0001111")) + msg_array.parse(Bitstring("00000000000000")) tlv_message_value.set("Tag", "Msg_Data") tlv_message_value._fields["Length"].typeval.assign(111111111111111, False) @@ -1131,7 +1131,7 @@ def msg_checksum(_: bytes, **__: object) -> int: tlv_package = pyrflx_["TLV_With_Checksum"] refinement_package.set_checksum_functions({"Message": {"Checksum": msg_checksum}}) tlv_package.set_checksum_functions({"Message": {"Checksum": tlv_checksum}}) - data = b"\x08\xff\x40\x02\x01\x02\x00\x00\x00\x00" + data = b"\x09\xff\x01\x00\x02\x01\x02\x00\x00\x00\x00" message = refinement_package["Message"] message.set_checksum_function({"Checksum": msg_checksum}) message.parse(data)