Fix detection of negative field size

Ref. eng/recordflux/RecordFlux#1357
AdaCore · Jul 13, 2023 · d5256a0 · d5256a0
1 parent 8b7561f
commit d5256a0
Show file tree

Hide file tree

Showing 7 changed files with 42 additions and 21 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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'^<stdin>:1:2: model: error: negative size for field "F2" [(]F1 -> F2[)]$',
+    )
+
+
 def test_payload_no_size() -> None:
     structure = [
         Link(INITIAL, Field("F1")),