Change handling of messages with implicit size in SPARK

Ref. #844, #736

doc/Language-Reference.adoc

@@ -431,7 +431,7 @@ Allowed return types:
 // * Scalars [§S-P-F-R-S]
 // * Definite messages [§S-P-F-R-M]
 
-Definite messages are messages with no optional fields and a bounded size (i.e. all size aspects contain no reference to `Message`).
+Definite messages are messages with no optional fields and an explicit size (i.e. all size aspects contain no reference to `Message`).
 
 *SPARK*
 

rflx/ada.py

@@ -464,6 +464,22 @@ class Max(BinAttributeExpr):
     pass
 
 
+class NamedAttributeExpr(Attribute):
+    def __init__(self, prefix: Union[StrID, Expr], *associations: Tuple[StrID, Expr]) -> None:
+        self.associations = [(ID(n) if isinstance(n, str) else n, e) for n, e in associations]
+        super().__init__(prefix)
+
+    @property
+    def _representation(self) -> str:
+        assert len(self.associations) > 0
+        associations = ", ".join(f"{name} => {element}" for name, element in self.associations)
+        return f"{self.prefix}'{self.__class__.__name__} ({associations})"
+
+
+class Update(NamedAttributeExpr):
+    pass
+
+
 @invariant(lambda self: len(self.elements) > 0)
 class Indexed(Name):
     def __init__(self, prefix: Expr, *elements: Expr, negative: bool = False) -> None:

rflx/generator/common.py

@@ -146,7 +146,7 @@ def prefixed(name: str) -> expr.Expr:
         return expr.Variable(rid.ID("Ctx") * name) if not embedded else expr.Variable(name)
 
     first = prefixed("First")
-    last = prefixed("Last")
+    last = prefixed("Written_Last")
     cursors = prefixed("Cursors")
 
     def field_first(field: model.Field) -> expr.Expr:
@@ -469,11 +469,16 @@ def invalid_successors_invariant() -> ada.Expr:
             ]
         ),
         public_context_predicate(),
-        ada.LessEqual(ada.Sub(ada.Variable("First"), ada.Number(1)), ada.Variable("Message_Last")),
-        ada.LessEqual(ada.Variable("Message_Last"), ada.Variable("Last")),
+        ada.LessEqual(ada.Sub(ada.Variable("First"), ada.Number(1)), ada.Variable("Verified_Last")),
+        ada.LessEqual(ada.Sub(ada.Variable("First"), ada.Number(1)), ada.Variable("Written_Last")),
+        ada.LessEqual(ada.Variable("Verified_Last"), ada.Variable("Written_Last")),
+        ada.LessEqual(ada.Variable("Written_Last"), ada.Variable("Last")),
         ada.Equal(ada.Mod(ada.Variable("First"), ada.Size(const.TYPES_BYTE)), ada.Number(1)),
         ada.Equal(ada.Mod(ada.Variable("Last"), ada.Size(const.TYPES_BYTE)), ada.Number(0)),
-        ada.Equal(ada.Mod(ada.Variable("Message_Last"), ada.Size(const.TYPES_BYTE)), ada.Number(0)),
+        ada.Equal(
+            ada.Mod(ada.Variable("Verified_Last"), ada.Size(const.TYPES_BYTE)), ada.Number(0)
+        ),
+        ada.Equal(ada.Mod(ada.Variable("Written_Last"), ada.Size(const.TYPES_BYTE)), ada.Number(0)),
         ada.ForAllIn(
             "F",
             ada.ValueRange(ada.First("Field"), ada.Last("Field")),
@@ -495,7 +500,7 @@ def invalid_successors_invariant() -> ada.Expr:
                                 ada.Selected(
                                     ada.Indexed(ada.Variable("Cursors"), ada.Variable("F")), "Last"
                                 ),
-                                ada.Variable("Message_Last"),
+                                ada.Variable("Verified_Last"),
                             ),
                             ada.LessEqual(
                                 ada.Selected(
@@ -592,15 +597,14 @@ def valid_path_to_next_field_condition(
     ]
 
 
-def sufficient_space_for_field_condition(field_name: ada.Name) -> ada.Expr:
-    return ada.GreaterEqual(
-        ada.Call("Available_Space", [ada.Variable("Ctx"), field_name]),
-        ada.Call("Field_Size", [ada.Variable("Ctx"), field_name]),
-    )
+def sufficient_space_for_field_condition(field_name: ada.Name, size: ada.Expr = None) -> ada.Expr:
+    if size is None:
+        size = ada.Call("Field_Size", [ada.Variable("Ctx"), field_name])
+    return ada.GreaterEqual(ada.Call("Available_Space", [ada.Variable("Ctx"), field_name]), size)
 
 
 def initialize_field_statements(
-    message: model.Message, field: model.Field
+    message: model.Message, field: model.Field, reset_written_last: bool = False
 ) -> Sequence[ada.Statement]:
     comparison_to_aggregate = is_compared_to_aggregate(field, message)
 
@@ -614,7 +618,38 @@ def initialize_field_statements(
             "Reset_Dependent_Fields",
             [ada.Variable("Ctx"), ada.Variable(field.affixed_name)],
         ),
-        ada.Assignment("Ctx.Message_Last", ada.Variable("Last")),
+        # ISSUE: Componolit/RecordFlux#868
+        ada.PragmaStatement(
+            "Warnings",
+            [
+                ada.Variable("Off"),
+                ada.String("attribute Update is an obsolescent feature"),
+            ],
+        ),
+        ada.Assignment(
+            "Ctx",
+            ada.Update(
+                "Ctx",
+                ("Verified_Last", ada.Variable("Last")),
+                (
+                    "Written_Last",
+                    ada.Variable("Last")
+                    if reset_written_last
+                    else ada.Max(
+                        const.TYPES_BIT_LENGTH,
+                        ada.Variable("Ctx.Written_Last"),
+                        ada.Variable("Last"),
+                    ),
+                ),
+            ),
+        ),
+        ada.PragmaStatement(
+            "Warnings",
+            [
+                ada.Variable("On"),
+                ada.String("attribute Update is an obsolescent feature"),
+            ],
+        ),
         ada.Assignment(
             ada.Indexed(ada.Variable("Ctx.Cursors"), ada.Variable(field.affixed_name)),
             ada.NamedAggregate(
@@ -713,7 +748,17 @@ def field_byte_location_declarations() -> Sequence[ada.Declaration]:
     ]
 
 
-def field_condition_call(message: model.Message, field: model.Field, value: ada.Expr) -> ada.Expr:
+def field_condition_call(
+    message: model.Message, field: model.Field, value: ada.Expr, size: ada.Expr = None
+) -> ada.Expr:
+    if size is None:
+        size = ada.Call(
+            "Field_Size",
+            [
+                ada.Variable("Ctx"),
+                ada.Variable(field.affixed_name),
+            ],
+        )
     return ada.Call(
         "Field_Condition",
         [
@@ -730,19 +775,7 @@ def field_condition_call(message: model.Message, field: model.Field, value: ada.
                     else []
                 ),
             ),
-            *(
-                [
-                    ada.Call(
-                        "Field_Size",
-                        [
-                            ada.Variable("Ctx"),
-                            ada.Variable(field.affixed_name),
-                        ],
-                    )
-                ]
-                if size_dependent_condition(message)
-                else []
-            ),
+            *([size] if size_dependent_condition(message) else []),
         ],
     )
 

rflx/generator/const.py

@@ -44,6 +44,7 @@
 TYPES_BIT_LENGTH = TYPES * "Bit_Length"
 TYPES_TO_INDEX = TYPES * "To_Index"
 TYPES_TO_LENGTH = TYPES * "To_Length"
+TYPES_TO_BIT_LENGTH = TYPES * "To_Bit_Length"
 TYPES_TO_FIRST_BIT_INDEX = TYPES * "To_First_Bit_Index"
 TYPES_TO_LAST_BIT_INDEX = TYPES * "To_Last_Bit_Index"
 TYPES_OFFSET = TYPES * "Offset"