Relax length precondition of To_Context

Ref. #1054
AdaCore · Jun 1, 2022 · aa1cb6d · aa1cb6d
1 parent 74d1384
commit aa1cb6d
Show file tree

Hide file tree

Showing 16 changed files with 124 additions and 76 deletions.
diff --git a/rflx/expression.py b/rflx/expression.py
@@ -1138,7 +1138,9 @@ def substituted(
         func = substitution(mapping or {}, func)
         expr = func(-self if self.negative else self)
         if isinstance(expr, Attribute):
-            expr = expr.__class__(expr.prefix.substituted(func))
+            prefix = expr.prefix.substituted(func)
+            if not isinstance(prefix, Attribute):
+                expr = expr.__class__(prefix)
         return -expr if self.negative else expr
 
     def simplified(self) -> Expr:

diff --git a/rflx/generator/message.py b/rflx/generator/message.py
@@ -2924,7 +2924,7 @@ def create_structure(message: Message, prefix: str) -> UnitPart:
     unit += _create_structure_type(message, prefix)
     unit += _create_valid_structure_function(message, prefix)
     unit += _create_to_structure_procedure(message)
-    unit += _create_to_context_procedure(message)
+    unit += _create_to_context_procedure(message, prefix)
     return unit
 
 
@@ -2997,27 +2997,7 @@ def _create_valid_structure_function(message: Message, prefix: str) -> UnitPart:
                 # ISSUE: Componolit/RecordFlux#276
                 mapping={expr.ValidChecksum(f): expr.TRUE for f in message.checksums},
             )
-            .substituted(
-                lambda x: expr.Size(expr.Variable("Struct" * x.prefix.identifier))
-                if isinstance(x, expr.Size)
-                and isinstance(x.prefix, expr.Variable)
-                and Field(x.prefix.identifier) in message.fields
-                else x
-            )
-            .substituted(
-                lambda x: expr.Call(
-                    "To_U64",
-                    [expr.Variable("Struct" * x.identifier)],
-                )
-                if isinstance(x, expr.Variable)
-                and Field(x.identifier) in message.fields
-                and isinstance(message.types[Field(x.identifier)], Scalar)
-                else expr.Variable("Struct" * x.identifier)
-                if isinstance(x, expr.Variable)
-                and Field(x.identifier) in message.fields
-                and isinstance(message.types[Field(x.identifier)], Opaque)
-                else x
-            )
+            .substituted(_struct_substitution(message))
             .substituted(common.substitution(message, prefix))
             .simplified()
             .ada_expr()
@@ -3152,7 +3132,40 @@ def _create_to_structure_procedure(message: Message) -> UnitPart:
     )
 
 
-def _create_to_context_procedure(message: Message) -> UnitPart:
+def _struct_substitution(
+    message: Message,
+) -> ty.Callable[[expr.Expr], expr.Expr]:
+    def func(expression: expr.Expr) -> expr.Expr:
+        if (
+            isinstance(expression, expr.Size)
+            and isinstance(expression.prefix, expr.Variable)
+            and Field(expression.prefix.identifier) in message.fields
+        ):
+            return expr.Size(expr.Variable("Struct" * expression.prefix.identifier))
+
+        if isinstance(expression, expr.Variable) and Field(expression.identifier) in message.fields:
+            field_type = message.types[Field(expression.identifier)]
+
+            if isinstance(field_type, Enumeration):
+                return expr.Call(
+                    "To_U64",
+                    [expr.Variable("Struct" * expression.identifier)],
+                )
+
+            if isinstance(field_type, Scalar):
+                return expr.Call(
+                    const.TYPES_U64,
+                    [expr.Variable("Struct" * expression.identifier)],
+                )
+
+            return expr.Variable("Struct" * expression.identifier)
+
+        return expression
+
+    return func
+
+
+def _create_to_context_procedure(message: Message, prefix: str) -> UnitPart:
     assert len(message.paths(FINAL)) == 1
 
     body: ty.List[Statement] = [CallStatement("Reset", [Variable("Ctx")])]
@@ -3224,8 +3237,7 @@ def _create_to_context_procedure(message: Message) -> UnitPart:
         "To_Context",
         [Parameter(["Struct"], "Structure"), InOutParameter(["Ctx"], "Context")],
     )
-    message_size = message.max_size()
-    assert isinstance(message_size, expr.Number)
+    message_size = message.size()
 
     return UnitPart(
         [
@@ -3238,18 +3250,26 @@ def _create_to_context_procedure(message: Message) -> UnitPart:
                             Not(Constrained("Ctx")),
                             Call("Has_Buffer", [Variable("Ctx")]),
                             GreaterEqual(
-                                Add(
-                                    Call(
-                                        const.TYPES * "To_Last_Bit_Index",
-                                        [Variable("Ctx.Buffer_Last")],
-                                    ),
-                                    -Call(
-                                        const.TYPES * "To_First_Bit_Index",
-                                        [Variable("Ctx.Buffer_First")],
-                                    ),
-                                    Number(1),
+                                Call(
+                                    const.TYPES_U64,
+                                    [
+                                        Add(
+                                            Call(
+                                                const.TYPES * "To_Last_Bit_Index",
+                                                [Variable("Ctx.Buffer_Last")],
+                                            ),
+                                            -Call(
+                                                const.TYPES * "To_First_Bit_Index",
+                                                [Variable("Ctx.Buffer_First")],
+                                            ),
+                                            Number(1),
+                                        )
+                                    ],
                                 ),
-                                message_size.ada_expr(),
+                                message_size.substituted(_struct_substitution(message))
+                                .substituted(common.substitution(message, prefix))
+                                .simplified()
+                                .ada_expr(),
                             ),
                         )
                     ),

diff --git a/rflx/model/message.py b/rflx/model/message.py
@@ -936,6 +936,15 @@ def is_definite(self) -> bool:
         )
 
     def size(self, field_values: Mapping[Field, expr.Expr] = None) -> expr.Expr:
+        """
+        Determine the size of the message based on the given field values.
+
+        If the message is not definite, a value for each field on one message path is required.
+        The reason for this is that only for messages without optional fields the size can be
+        represented by a single mathematical expression, if no field values are given.
+
+        An exception is raised if no size can be determined.
+        """
         field_values = field_values if field_values else {}
 
         def remove_variable_prefix(expression: expr.Expr) -> expr.Expr:
@@ -979,10 +988,15 @@ def remove_variable_prefix(expression: expr.Expr) -> expr.Expr:
         failures = []
 
         for path in self.paths(FINAL):
-            if not self.has_fixed_size and fields != {
-                *self.parameters,
-                *(l.target for l in path if l.target != FINAL),
-            }:
+            if (
+                not self.is_definite
+                and not self.has_fixed_size
+                and fields
+                != {
+                    *self.parameters,
+                    *(l.target for l in path if l.target != FINAL),
+                }
+            ):
                 continue
             message_size = expr.Add(
                 *[

diff --git a/tests/data/models.py b/tests/data/models.py
@@ -530,6 +530,26 @@
     },
 )
 
+DEFINITE_MESSAGE = Message(
+    "Definite::Message",
+    [
+        Link(INITIAL, Field("Length")),
+        Link(
+            Field("Length"),
+            Field("Data"),
+            size=Mul(Variable("Length"), Number(8)),
+        ),
+        Link(
+            Field("Data"),
+            FINAL,
+        ),
+    ],
+    {
+        Field("Length"): UNIVERSAL_LENGTH,
+        Field("Data"): OPAQUE,
+    },
+)
+
 SESSION = Session(
     identifier="P::S",
     initial="A",

diff --git a/tests/integration/session_endianness/generated/rflx-messages-msg.ads b/tests/integration/session_endianness/generated/rflx-messages-msg.ads
@@ -461,7 +461,7 @@ is
        Valid_Structure (Struct)
        and then not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1 >= 64,
+       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 64,
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)

diff --git a/tests/integration/session_endianness/generated/rflx-messages-msg_le.ads b/tests/integration/session_endianness/generated/rflx-messages-msg_le.ads
@@ -461,7 +461,7 @@ is
        Valid_Structure (Struct)
        and then not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1 >= 64,
+       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 64,
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)

diff --git a/tests/integration/session_endianness/generated/rflx-messages-msg_le_nested.ads b/tests/integration/session_endianness/generated/rflx-messages-msg_le_nested.ads
@@ -494,7 +494,7 @@ is
        Valid_Structure (Struct)
        and then not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1 >= 96,
+       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 96,
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)

diff --git a/tests/integration/session_functions/generated/rflx-test-definite_message.ads b/tests/integration/session_functions/generated/rflx-test-definite_message.ads
@@ -611,7 +611,7 @@ is
        Valid_Structure (Struct)
        and then not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1 >= 2056,
+       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= RFLX_Types.U64 (Struct.Length) * 8 + 16,
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)

diff --git a/tests/spark/generated/rflx-enumeration-message.ads b/tests/spark/generated/rflx-enumeration-message.ads
@@ -430,7 +430,7 @@ is
        Valid_Structure (Struct)
        and then not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1 >= 8,
+       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 8,
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)

diff --git a/tests/spark/generated/rflx-expression-message.ads b/tests/spark/generated/rflx-expression-message.ads
@@ -509,7 +509,7 @@ is
        Valid_Structure (Struct)
        and then not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1 >= 16,
+       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 16,
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)

diff --git a/tests/spark/generated/rflx-fixed_size-simple_message.ads b/tests/spark/generated/rflx-fixed_size-simple_message.ads
@@ -557,7 +557,7 @@ is
        Valid_Structure (Struct)
        and then not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1 >= 32,
+       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 32,
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)

diff --git a/tests/spark/generated/rflx-sequence-inner_message.ads b/tests/spark/generated/rflx-sequence-inner_message.ads
@@ -573,7 +573,7 @@ is
        Valid_Structure (Struct)
        and then not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1 >= 2048,
+       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= RFLX_Types.U64 (Struct.Length) * 8 + 8,
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)

diff --git a/tests/spark/generated/rflx-udp-datagram.ads b/tests/spark/generated/rflx-udp-datagram.ads
@@ -687,7 +687,7 @@ is
        Valid_Structure (Struct)
        and then not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1 >= 524280,
+       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= (RFLX_Types.U64 (Struct.Length) - 8) * 8 + 64,
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)

diff --git a/tests/unit/generator_test.py b/tests/unit/generator_test.py
@@ -33,6 +33,18 @@
 from tests.data import models
 from tests.utils import assert_compilable_code, assert_equal, assert_equal_code
 
+MODELS = [
+    models.DERIVATION_MODEL,
+    models.ENUMERATION_MODEL,
+    models.ETHERNET_MODEL,
+    models.EXPRESSION_MODEL,
+    models.NULL_MESSAGE_IN_TLV_MESSAGE_MODEL,
+    models.NULL_MODEL,
+    models.SEQUENCE_MODEL,
+    models.TLV_MODEL,
+    Model(models.FIXED_SIZE_SIMPLE_MESSAGE.dependencies),
+]
+
 
 def units(generator: Generator) -> Mapping[str, str]:
     result = {}
@@ -118,19 +130,7 @@ def test_generate_missing_template_files(monkeypatch: MonkeyPatch, tmp_path: Pat
         Generator().generate(Model(), Integration(), tmp_path)
 
 
-@pytest.mark.parametrize(
-    "model",
-    [
-        models.NULL_MODEL,
-        models.TLV_MODEL,
-        models.NULL_MESSAGE_IN_TLV_MESSAGE_MODEL,
-        models.ETHERNET_MODEL,
-        models.ENUMERATION_MODEL,
-        models.SEQUENCE_MODEL,
-        models.EXPRESSION_MODEL,
-        models.DERIVATION_MODEL,
-    ],
-)
+@pytest.mark.parametrize("model", MODELS)
 def test_equality(model: Model, tmp_path: Path) -> None:
     assert_equal_code(model, Integration(), GENERATED_DIR, tmp_path, accept_extra_files=True)
 

diff --git a/tests/unit/model/message_test.py b/tests/unit/model/message_test.py
@@ -58,6 +58,7 @@
 )
 from rflx.model.message import ByteOrder
 from tests.data.models import (
+    DEFINITE_MESSAGE,
     ENUMERATION,
     ETHERNET_FRAME,
     FIXED_SIZE_MESSAGE,
@@ -2717,6 +2718,7 @@ def test_has_implicit_size() -> None:
 def test_is_definite() -> None:
     assert NULL_MESSAGE.is_definite
     assert FIXED_SIZE_SIMPLE_MESSAGE.is_definite
+    assert DEFINITE_MESSAGE.is_definite
     assert not FIXED_SIZE_MESSAGE.is_definite
     assert not TLV_MESSAGE.is_definite
     assert not ETHERNET_FRAME.is_definite
@@ -2726,6 +2728,8 @@ def test_is_definite() -> None:
 def test_size() -> None:
     assert NULL_MESSAGE.size() == Number(0)
     assert FIXED_SIZE_MESSAGE.size() == Number(200)
+    assert DEFINITE_MESSAGE.size() == Add(Mul(Variable("Length"), Number(8)), Number(16))
+    assert DEFINITE_MESSAGE.size({Field("Length"): Number(8)}) == Number(80)
     assert TLV_MESSAGE.size({Field("Tag"): Variable("TLV::Msg_Error")}) == Number(8)
     assert TLV_MESSAGE.size(
         {

diff --git a/tools/generate_spark_test_code.py b/tools/generate_spark_test_code.py
@@ -6,29 +6,17 @@
 import sys
 from pathlib import Path
 
-import tests.data.models
 from rflx.generator import Generator
 from rflx.integration import Integration
-from rflx.model import Model
 from rflx.specification import Parser
 from tests.const import SPEC_DIR
+from tests.unit.generator_test import MODELS
 
 logging.basicConfig(level=logging.INFO, format="%(message)s")
 logging.disable(logging.NOTSET)
 
 OUTPUT_DIRECTORY = Path("tests/spark/generated")
 
-MODELS = [
-    tests.data.models.EXPRESSION_MODEL,
-    tests.data.models.ENUMERATION_MODEL,
-    tests.data.models.SEQUENCE_MODEL,
-    tests.data.models.DERIVATION_MODEL,
-    tests.data.models.NULL_MODEL,
-    tests.data.models.TLV_MODEL,
-    tests.data.models.NULL_MESSAGE_IN_TLV_MESSAGE_MODEL,
-    Model(tests.data.models.FIXED_SIZE_SIMPLE_MESSAGE.dependencies),
-]
-
 SPECIFICATION_FILES = [
     SPEC_DIR / "ethernet.rflx",
     SPEC_DIR / "in_ethernet.rflx",