From d5256a01d6cc40464414bdea9d4a3d438ec3f796 Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Thu, 13 Jul 2023 20:56:43 +0200 Subject: [PATCH] Fix detection of negative field size Ref. eng/recordflux/RecordFlux#1357 --- CHANGELOG.md | 1 + examples/specs/slpv2.rflx | 6 +++--- examples/specs/tcp.rflx | 6 +++--- examples/specs/tls_heartbeat.rflx | 6 +++--- rflx/model/message.py | 7 ------- tests/compilation/integration_test.py | 12 +++++++----- tests/unit/model/message_test.py | 25 +++++++++++++++++++++++++ 7 files changed, 42 insertions(+), 21 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index cb09686e9..469c2c9f7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,6 +13,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - Locations of message fields and field sizes in error messages (eng/recordflux/RecordFlux#1349) - Invalid use of First aspect that led to overlay of multiple fields (eng/recordflux/RecordFlux#1332) - Update of message field with invalid sequence (eng/recordflux/RecordFlux#1353) +- Detection of negative field size (eng/recordflux/RecordFlux#1357) ## [0.11.0] - 2023-06-16 diff --git a/examples/specs/slpv2.rflx b/examples/specs/slpv2.rflx index dae880aa8..2a29d21af 100644 --- a/examples/specs/slpv2.rflx +++ b/examples/specs/slpv2.rflx @@ -107,10 +107,10 @@ package SLPv2 is Authentication_Block_Timestamp : U32; SLP_SPI_String_Length : U16; SLP_SPI_String : Opaque - with Size => SLP_SPI_String_Length * 8; - Structured_Authentication_Block : Opaque - with Size => 8 * Authentication_Block_Length - (SLP_SPI_String'Last - Block_Structure_Descriptor'First + 1) + with Size => SLP_SPI_String_Length * 8 if (8 * Authentication_Block_Length >= (SLP_SPI_String'Last - Block_Structure_Descriptor'First + 1)); + Structured_Authentication_Block : Opaque + with Size => 8 * Authentication_Block_Length - (SLP_SPI_String'Last - Block_Structure_Descriptor'First + 1); end message; type Authentication_Blocks is sequence of Authentication_Block; diff --git a/examples/specs/tcp.rflx b/examples/specs/tcp.rflx index 052e4b04b..c27bbc250 100644 --- a/examples/specs/tcp.rflx +++ b/examples/specs/tcp.rflx @@ -87,7 +87,8 @@ package TCP is Destination_Port : Port; Sequence_Number : Sequence_Number; Acknowledgment_Number : Acknowledgment_Number; - Data_Offset : Data_Offset; + Data_Offset : Data_Offset + if Segment_Length >= Data_Offset * 4; Reserved : Reserved; NS : Boolean; -- Nonce Sum (RFC 3540) CWR : Boolean; -- Congestion Window Reduced (RFC 3168) @@ -106,8 +107,7 @@ package TCP is with Size => (Data_Offset * 32) - (Urgent_Pointer'Last - Source_Port'First + 1) if (Options'Last - Source_Port'First + 1) mod 32 = 0; Data : Opaque - with Size => (Segment_Length * 8) - (Data_Offset * 32) - if Segment_Length >= Data_Offset * 4; + with Size => (Segment_Length * 8) - (Data_Offset * 32); end message; end TCP; diff --git a/examples/specs/tls_heartbeat.rflx b/examples/specs/tls_heartbeat.rflx index 7322caa65..fe84e38e9 100644 --- a/examples/specs/tls_heartbeat.rflx +++ b/examples/specs/tls_heartbeat.rflx @@ -11,11 +11,11 @@ package TLS_Heartbeat is Message_Type : Message_Type; Payload_Length : Length; Payload : Opaque - with Size => Payload_Length * 8; + with Size => Payload_Length * 8 + if TLS_Plaintext_Length >= Payload_Length + (Message_Type'Size + Payload_Length'Size) / 8; Padding : Opaque with Size => (TLS_Plaintext_Length - Payload_Length) * 8 - Message_Type'Size - Payload_Length'Size - if TLS_Plaintext_Length >= Payload_Length + (Message_Type'Size + Payload_Length'Size) / 8 - and Padding'Size / 8 >= 16; + if Padding'Size / 8 >= 16; end message; end TLS_Heartbeat; diff --git a/rflx/model/message.py b/rflx/model/message.py index 516552da8..f3e13c7ec 100644 --- a/rflx/model/message.py +++ b/rflx/model/message.py @@ -1948,13 +1948,6 @@ def _prove_field_positions(self) -> None: ) facts = [fact for link in path for fact in self._link_expressions(link)] - - outgoing = self.outgoing(f) - if f != FINAL and outgoing: - facts.append( - expr.Or(*[o.condition for o in outgoing], location=f.identifier.location) - ) - facts.extend(self.type_constraints(negative)) facts.extend(self.type_constraints(start)) diff --git a/tests/compilation/integration_test.py b/tests/compilation/integration_test.py index b89c09809..b5ee8be4e 100644 --- a/tests/compilation/integration_test.py +++ b/tests/compilation/integration_test.py @@ -643,17 +643,19 @@ def test_session_move_content_of_opaque_field(tmp_path: Path) -> None: type M1 is message - Size : Payload_Size; - Payload : Opaque - with Size => Size + Size : Payload_Size if Size mod 8 = 0; + Payload : Opaque + with Size => Size; end message; type M2 (Size : Payload_Size) is message + null + then Payload + if Size mod 8 = 0; Payload : Opaque - with Size => Size - if Size mod 8 = 0; + with Size => Size; end message; generic diff --git a/tests/unit/model/message_test.py b/tests/unit/model/message_test.py index 32b7e6370..839535d88 100644 --- a/tests/unit/model/message_test.py +++ b/tests/unit/model/message_test.py @@ -1907,6 +1907,31 @@ def test_invalid_negative_field_size_2() -> None: ) +def test_invalid_negative_field_size_3() -> None: + structure = [ + Link(INITIAL, Field("F1")), + Link( + Field("F1"), + Field("F2"), + size=Sub(Mul(Variable("F1"), Number(8)), Number(16), location=Location((1, 2))), + ), + Link( + Field("F2"), + FINAL, + condition=Greater(Variable("F1"), Number(1)), + ), + ] + types = { + Field("F1"): INTEGER, + Field("F2"): OPAQUE, + } + assert_message_model_error( + structure, + types, + r'^:1:2: model: error: negative size for field "F2" [(]F1 -> F2[)]$', + ) + + def test_payload_no_size() -> None: structure = [ Link(INITIAL, Field("F1")),