Replace message attributes when merging message types

Closes #729

rflx/model/message.py

@@ -1569,6 +1569,52 @@ def proven(self, skip_proof: bool = False) -> "DerivedMessage":
         return copy(self)
 
 
+def replace_message_attributes(
+    message: AbstractMessage,
+) -> Tuple[AbstractMessage, List[Optional[Location]]]:
+    """
+    Replace all occurences of the message attribute Message'Size by the equivalent term
+    Message'Last - Message'First + 1. Then replace all occurences of the message attribute
+    Message'First by a reference to the first field of the message. Return the new message and
+    a list of locations where Message'Last or Message'Size have been used.
+    """
+    first_field = message.outgoing(INITIAL)[0].target
+    locations = []
+
+    def replace(expression: expr.Expr) -> expr.Expr:
+        if (
+            not isinstance(expression, expr.Attribute)
+            or not isinstance(expression.prefix, expr.Variable)
+            or expression.prefix.name != "Message"
+        ):
+            return expression
+        if isinstance(expression, expr.First):
+            return expr.First(expr.ID(first_field.identifier, location=expression.location))
+        locations.append(expression.location)
+        if isinstance(expression, expr.Last):
+            return expression
+        if isinstance(expression, expr.Size):
+            return expr.Add(
+                expr.Sub(expr.Last("Message"), expr.First(first_field.identifier)),
+                expr.Number(1),
+                location=expression.location,
+            )
+        raise NotImplementedError
+
+    structure = [
+        Link(
+            l.source,
+            l.target,
+            l.condition.substituted(replace),
+            l.size.substituted(replace),
+            l.first.substituted(replace),
+            l.location,
+        )
+        for l in message.structure
+    ]
+    return message.copy(structure=structure), locations
+
+
 class UnprovenMessage(AbstractMessage):
     # pylint: disable=too-many-arguments
     def copy(
@@ -1602,6 +1648,7 @@ def proven(self, skip_proof: bool = False) -> Message:
 
     @ensure(lambda result: valid_message_field_types(result))
     def merged(self) -> "UnprovenMessage":
+        # pylint: disable=too-many-locals
         def prune_dangling_fields(
             structure: List[Link], types: Dict[Field, mty.Type]
         ) -> Tuple[List[Link], Dict[Field, mty.Type]]:
@@ -1632,7 +1679,28 @@ def prune_dangling_fields(
                 break
 
             field, inner_message = inner_messages.pop(0)
-            inner_message = inner_message.prefixed(f"{field.name}_")
+            inner_message, message_attribute_locations = replace_message_attributes(
+                inner_message.prefixed(f"{field.name}_")
+            )
+
+            message_next_fields = message.outgoing(field)
+            if len(message_attribute_locations) > 0 and (
+                len(message_next_fields) > 1 or message_next_fields[0].target != FINAL
+            ):
+                self.error.append(
+                    "Message types with message attribute may only be used for fields preceeding"
+                    " FINAL",
+                    Subsystem.MODEL,
+                    Severity.ERROR,
+                    field.identifier.location,
+                )
+                for loc in message_attribute_locations:
+                    self.error.append(
+                        f"Message attribute used in {inner_message.identifier}",
+                        Subsystem.MODEL,
+                        Severity.INFO,
+                        loc,
+                    )
 
             name_conflicts = [
                 f for f in message.fields for g in inner_message.fields if f.name == g.name

tests/unit/model/message_test.py

@@ -3269,3 +3269,91 @@ def test_refinement_invalid_condition_unqualified_literal() -> None:
         r' of "P::M"'
         r"$",
     )
+
+
+def test_message_type_with_message_aspect() -> None:
+    inner = UnprovenMessage(
+        "P::I",
+        [
+            Link(INITIAL, Field("I1")),
+            Link(
+                Field("I1"),
+                Field("I2"),
+                condition=Less(Variable("I1"), Number(128)),
+                size=Sub(Size(ID("Message", location=Location((5, 10)))), Number(8)),
+            ),
+            Link(
+                Field("I1"),
+                Field("I2"),
+                condition=GreaterEqual(Variable("I1"), Number(128)),
+                size=Sub(
+                    Sub(Last(ID("Message", location=Location((6, 10)))), First("Message")),
+                    Number(7),
+                ),
+            ),
+            Link(Field("I2"), FINAL),
+        ],
+        {Field("I1"): MODULAR_INTEGER, Field("I2"): OPAQUE},
+    )
+    valid_outer = (
+        UnprovenMessage(
+            "P::O",
+            [
+                Link(INITIAL, Field("O1")),
+                Link(Field("O1"), Field("O2")),
+                Link(Field("O2"), FINAL),
+            ],
+            {Field("O1"): MODULAR_INTEGER, Field("O2"): inner},
+        )
+        .merged()
+        .proven()
+    )
+    assert_equal(
+        valid_outer,
+        Message(
+            "P::O",
+            [
+                Link(INITIAL, Field("O1")),
+                Link(Field("O1"), Field("O2_I1")),
+                Link(
+                    Field("O2_I1"),
+                    Field("O2_I2"),
+                    condition=Less(Variable("O2_I1"), Number(128)),
+                    size=Add(Add(Add(Last("Message"), -First("O2_I1")), Number(1)), -Number(8)),
+                ),
+                Link(
+                    Field("O2_I1"),
+                    Field("O2_I2"),
+                    condition=GreaterEqual(Variable("O2_I1"), Number(128)),
+                    size=Add(Add(Last("Message"), -First("O2_I1")), -Number(7)),
+                ),
+                Link(Field("O2_I2"), FINAL),
+            ],
+            {Field("O1"): MODULAR_INTEGER, Field("O2_I1"): MODULAR_INTEGER, Field("O2_I2"): OPAQUE},
+        ),
+    )
+    with pytest.raises(
+        RecordFluxError,
+        match=(
+            "^"
+            "<stdin>:2:10: model: error: Message types with message attribute may only be used for"
+            " fields preceeding FINAL\n"
+            "<stdin>:5:10: model: info: Message attribute used in P::I\n"
+            "<stdin>:6:10: model: info: Message attribute used in P::I"
+            "$"
+        ),
+    ):
+        o1 = Field(ID("O1", location=Location((2, 10))))
+        valid_outer = (
+            UnprovenMessage(
+                "P::O",
+                [
+                    Link(INITIAL, o1),
+                    Link(o1, Field("O2")),
+                    Link(Field("O2"), FINAL),
+                ],
+                {o1: inner, Field("O2"): MODULAR_INTEGER},
+            )
+            .merged()
+            .proven()
+        )