Improve size calculation of fixed size messages

Ref. #292, #650
AdaCore · May 27, 2021 · 727efbe · 727efbe
1 parent 892357d
commit 727efbe
Show file tree

Hide file tree

Showing 3 changed files with 65 additions and 6 deletions.
diff --git a/rflx/model/message.py b/rflx/model/message.py
@@ -646,7 +646,16 @@ def is_possibly_empty(self, field: Field) -> bool:
 
         return False
 
-    def size(self, field_values: Mapping[Field, expr.Expr]) -> expr.Expr:
+    @property
+    def has_fixed_size(self) -> bool:
+        return len(self.paths(FINAL)) <= 1 and not (
+            {v.identifier for l in self.structure for v in l.size.variables()}
+            - set(self._type_literals.keys())
+        )
+
+    def size(self, field_values: Mapping[Field, expr.Expr] = None) -> expr.Expr:
+        field_values = field_values if field_values else {}
+
         def to_mapping(facts: Sequence[expr.Expr]) -> Dict[expr.Name, expr.Expr]:
             return {
                 f.left: f.right
@@ -665,6 +674,9 @@ def remove_variable_prefix(expression: expr.Expr) -> expr.Expr:
                 )
             return expression
 
+        if not self.structure:
+            return expr.Number(0)
+
         fields = set(field_values)
         values = [
             expr.Equal(expr.Variable(f.name), v, location=v.location)
@@ -692,7 +704,9 @@ def remove_variable_prefix(expression: expr.Expr) -> expr.Expr:
         failures = []
 
         for path in self.paths(FINAL):
-            if fields != set(l.target for l in path if l.target != FINAL):
+            if not self.has_fixed_size and fields != set(
+                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
@@ -330,7 +330,7 @@
 )
 UNIVERSAL_LENGTH = ModularInteger("Universal::Length", Pow(Number(2), Number(16)))
 UNIVERSAL_VALUE = RangeInteger("Universal::Value", Number(0), Number(100), Number(8))
-UNIVERSAL_VALUES = Array("Universal::Values", UNIVERSAL_VALUE)
+UNIVERSAL_VALUES = Sequence("Universal::Values", UNIVERSAL_VALUE)
 UNIVERSAL_OPTION_TYPE = Enumeration(
     "Universal::Option_Type",
     [
@@ -340,7 +340,7 @@
     size=Number(8),
     always_valid=True,
 )
-UNIVERSAL_OPTION_TYPES = Array("Universal::Option_Types", UNIVERSAL_OPTION_TYPE)
+UNIVERSAL_OPTION_TYPES = Sequence("Universal::Option_Types", UNIVERSAL_OPTION_TYPE)
 UNIVERSAL_OPTION = Message(
     "Universal::Option",
     [
@@ -368,7 +368,7 @@
         Field("Data"): Opaque(),
     },
 )
-UNIVERSAL_OPTIONS = Array("Universal::Options", UNIVERSAL_OPTION)
+UNIVERSAL_OPTIONS = Sequence("Universal::Options", UNIVERSAL_OPTION)
 UNIVERSAL_MESSAGE = Message(
     "Universal::Message",
     [
@@ -447,7 +447,7 @@
         Field("Options"): UNIVERSAL_OPTIONS,
     },
 )
-UNIVERSAL_MESSAGES = Array("Universal::Messages", UNIVERSAL_MESSAGE)
+UNIVERSAL_MESSAGES = Sequence("Universal::Messages", UNIVERSAL_MESSAGE)
 UNIVERSAL_MODEL = Model(
     [
         UNIVERSAL_MESSAGE_TYPE,
@@ -462,6 +462,38 @@
     ]
 )
 
+FIXED_SIZE_MESSAGE = Message(
+    "Fixed_Size::Message",
+    [
+        Link(INITIAL, Field("Message_Type")),
+        Link(
+            Field("Message_Type"),
+            Field("Data"),
+            size=Number(64),
+        ),
+        Link(
+            Field("Data"),
+            Field("Values"),
+            size=Mul(Number(8), Size("Universal::Value")),
+        ),
+        Link(
+            Field("Values"),
+            Field("Options"),
+            size=Number(64),
+        ),
+        Link(
+            Field("Options"),
+            FINAL,
+        ),
+    ],
+    {
+        Field("Message_Type"): UNIVERSAL_MESSAGE_TYPE,
+        Field("Data"): Opaque(),
+        Field("Values"): UNIVERSAL_VALUES,
+        Field("Options"): UNIVERSAL_OPTIONS,
+    },
+)
+
 SESSION = Session(
     identifier="P::S",
     initial="A",

diff --git a/tests/unit/model/message_test.py b/tests/unit/model/message_test.py
@@ -56,11 +56,14 @@
 from tests.data.models import (
     ENUMERATION,
     ETHERNET_FRAME,
+    FIXED_SIZE_MESSAGE,
     MODULAR_INTEGER,
+    NULL_MESSAGE,
     RANGE_INTEGER,
     SEQUENCE_INNER_MESSAGE,
     SEQUENCE_INNER_MESSAGES,
     SEQUENCE_LENGTH,
+    SEQUENCE_MESSAGE,
     SEQUENCE_MESSAGES_MESSAGE,
     SEQUENCE_MODULAR_VECTOR,
     TLV_LENGTH,
@@ -2486,7 +2489,17 @@ def test_is_possibly_empty() -> None:
     assert message.is_possibly_empty(c)
 
 
+def test_has_fixed_size() -> None:
+    assert NULL_MESSAGE.has_fixed_size
+    assert FIXED_SIZE_MESSAGE.has_fixed_size
+    assert not TLV_MESSAGE.has_fixed_size
+    assert not ETHERNET_FRAME.has_fixed_size
+    assert not SEQUENCE_MESSAGE.has_fixed_size
+
+
 def test_size() -> None:
+    assert NULL_MESSAGE.size() == Number(0)
+    assert FIXED_SIZE_MESSAGE.size() == Number(200)
     assert TLV_MESSAGE.size({Field("Tag"): Variable("Msg_Error")}) == Number(8)
     assert (
         TLV_MESSAGE.size(