Prevent use of specific messages as sequence element

Ref. #736
AdaCore · Dec 21, 2021 · c15f132 · c15f132
1 parent 60722f1
commit c15f132
Show file tree

Hide file tree

Showing 2 changed files with 92 additions and 22 deletions.
diff --git a/rflx/model/type_.py b/rflx/model/type_.py
@@ -523,9 +523,7 @@ def __init__(self, identifier: StrID, element_type: Type, location: Location = N
         super().__init__(identifier, location)
         self.element_type = element_type
 
-        if not isinstance(element_type, Scalar) and not (
-            isinstance(element_type, message.Message) and element_type.structure
-        ):
+        if not isinstance(element_type, Scalar) and not isinstance(element_type, message.Message):
             self.error.extend(
                 [
                     (
@@ -535,7 +533,7 @@ def __init__(self, identifier: StrID, element_type: Type, location: Location = N
                         location,
                     ),
                     (
-                        f'type "{element_type.name}" must be scalar or non-null message',
+                        f'type "{element_type.name}" must be scalar or message',
                         Subsystem.MODEL,
                         Severity.INFO,
                         element_type.location,
@@ -564,6 +562,45 @@ def __init__(self, identifier: StrID, element_type: Type, location: Location = N
                     ],
                 )
 
+        if isinstance(element_type, message.Message):
+            error = (
+                f'invalid element type of sequence "{self.name}"',
+                Subsystem.MODEL,
+                Severity.ERROR,
+                location,
+            )
+
+            if not element_type.structure:
+                self.error.extend(
+                    [
+                        error,
+                        (
+                            "null messages must not be used as sequence element",
+                            Subsystem.MODEL,
+                            Severity.INFO,
+                            element_type.location,
+                        ),
+                    ],
+                )
+
+            if any(
+                bool(e.findall(lambda x: x in [expr.Size("Message"), expr.Last("Message")]))
+                for l in element_type.structure
+                for e in [l.condition, l.size]
+            ):
+                self.error.extend(
+                    [
+                        error,
+                        (
+                            "messages used as sequence element must not depend"
+                            ' on "Message\'Size" or "Message\'Last"',
+                            Subsystem.MODEL,
+                            Severity.INFO,
+                            element_type.location,
+                        ),
+                    ],
+                )
+
     def __repr__(self) -> str:
         return verbose_repr(self, ["identifier", "element_type"])
 

diff --git a/tests/unit/model/type_test.py b/tests/unit/model/type_test.py
@@ -2,12 +2,16 @@
 
 import rflx.typing_ as rty
 from rflx.error import Location, RecordFluxError
-from rflx.expression import Add, Number, Pow, Sub, Variable
+from rflx.expression import Add, Equal, Number, Pow, Size, Sub, Variable
 from rflx.identifier import ID
 from rflx.model import (
     BOOLEAN,
+    FINAL,
+    INITIAL,
     OPAQUE,
     Enumeration,
+    Field,
+    Link,
     Message,
     ModularInteger,
     RangeInteger,
@@ -386,24 +390,53 @@ def test_sequence_dependencies() -> None:
     ]
 
 
-def test_sequence_invalid_element_type() -> None:
-    assert_type_error(
-        Sequence(
-            "P::A", Sequence("P::B", models.MODULAR_INTEGER, Location((3, 4))), Location((5, 4))
+@pytest.mark.parametrize(
+    "element_type, error",
+    [
+        (
+            Sequence("P::B", models.MODULAR_INTEGER, Location((3, 4))),
+            r'<stdin>:1:2: model: error: invalid element type of sequence "A"\n'
+            r'<stdin>:3:4: model: info: type "B" must be scalar or message',
         ),
-        r'^<stdin>:5:4: model: error: invalid element type of sequence "A"\n'
-        r'<stdin>:3:4: model: info: type "B" must be scalar or non-null message$',
-    )
-    assert_type_error(
-        Sequence("P::A", Message("P::B", [], {}, location=Location((3, 4))), Location((5, 4))),
-        r'^<stdin>:5:4: model: error: invalid element type of sequence "A"\n'
-        r'<stdin>:3:4: model: info: type "B" must be scalar or non-null message$',
-    )
-    assert_type_error(
-        Sequence("P::A", OPAQUE, Location((5, 4))),
-        r'^<stdin>:5:4: model: error: invalid element type of sequence "A"\n'
-        r'__BUILTINS__:0:0: model: info: type "Opaque" must be scalar or non-null message$',
-    )
+        (
+            OPAQUE,
+            r'<stdin>:1:2: model: error: invalid element type of sequence "A"\n'
+            r'__BUILTINS__:0:0: model: info: type "Opaque" must be scalar or message',
+        ),
+        (
+            Message("P::B", [], {}, location=Location((3, 4))),
+            r'<stdin>:1:2: model: error: invalid element type of sequence "A"\n'
+            r"<stdin>:3:4: model: info: null messages must not be used as sequence element",
+        ),
+        (
+            Message(
+                "P::B",
+                [Link(INITIAL, Field("A"), size=Size("Message")), Link(Field("A"), FINAL)],
+                {Field("A"): OPAQUE},
+                location=Location((3, 4)),
+            ),
+            r'<stdin>:1:2: model: error: invalid element type of sequence "A"\n'
+            r"<stdin>:3:4: model: info: messages used as sequence element must not depend"
+            ' on "Message\'Size" or "Message\'Last"',
+        ),
+        (
+            Message(
+                "P::B",
+                [
+                    Link(INITIAL, Field("A"), condition=Equal(Size("Message"), Number(8))),
+                    Link(Field("A"), FINAL),
+                ],
+                {Field("A"): models.MODULAR_INTEGER},
+                location=Location((3, 4)),
+            ),
+            r'<stdin>:1:2: model: error: invalid element type of sequence "A"\n'
+            r"<stdin>:3:4: model: info: messages used as sequence element must not depend"
+            ' on "Message\'Size" or "Message\'Last"',
+        ),
+    ],
+)
+def test_sequence_invalid_element_type(element_type: Type, error: str) -> None:
+    assert_type_error(Sequence("P::A", element_type, Location((1, 2))), f"^{error}$")
 
 
 def test_sequence_unsupported_element_type() -> None: