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*
 

examples/apps/ping/Makefile

@@ -7,10 +7,10 @@ bin = obj/ping
 test: test_python test_spark
 
 test_python:
-	sudo -n timeout 5 `which python3` ping.py 127.0.0.1 | grep -q "64 bytes from 127.0.0.1: icmp_seq=0"
+	sudo -n timeout 5 `command -v python3` ping.py 127.0.0.1 | tee /dev/tty | grep -q "64 bytes from 127.0.0.1: icmp_seq=0"
 
 test_spark: $(bin)
-	sudo -n timeout 3 obj/ping 127.0.0.1 | grep -q "64 bytes from 127.0.0.1: icmp_seq=0"
+	sudo -n timeout 3 obj/ping 127.0.0.1 | tee /dev/tty | grep -q "64 bytes from 127.0.0.1: icmp_seq=0"
 
 build: $(bin)
 

examples/apps/ping/src/icmpv4.adb

@@ -169,20 +169,9 @@ is
                        Last :    out RFLX.RFLX_Builtin_Types.Index)
    is
       use type RFLX.ICMP.Sequence_Number;
-      use type RFLX.RFLX_Builtin_Types.Bit_Length;
       IP_Context   : RFLX.IPv4.Packet.Context;
       ICMP_Context : RFLX.ICMP.Message.Context;
       Data         : constant RFLX.RFLX_Builtin_Types.Bytes (1 .. 56) := (others => 65);
-      function Valid_Length (L : RFLX.RFLX_Builtin_Types.Length) return Boolean is
-         (L = Data'Length);
-      procedure Process_Data (Buffer : out RFLX.RFLX_Builtin_Types.Bytes) with
-         Pre => Valid_Length (Buffer'Length);
-      procedure Process_Data (Buffer : out RFLX.RFLX_Builtin_Types.Bytes)
-      is
-      begin
-         Buffer := Data;
-      end Process_Data;
-      procedure Set_Data is new RFLX.ICMP.Message.Generic_Set_Data (Process_Data, Valid_Length);
    begin
       --  WORKAROUND: Componolit/Workarounds#32
       pragma Warnings (Off, "unused assignment to ""*_Context""");
@@ -215,7 +204,7 @@ is
                                              0, 0, Sequence, Data));
          RFLX.ICMP.Message.Set_Identifier (ICMP_Context, 0);
          RFLX.ICMP.Message.Set_Sequence_Number (ICMP_Context, Sequence);
-         Set_Data (ICMP_Context);
+         RFLX.ICMP.Message.Set_Data (ICMP_Context, Data);
          Last := RFLX.RFLX_Types.To_Index (RFLX.ICMP.Message.Message_Last (ICMP_Context));
          RFLX.ICMP.Message.Take_Buffer (ICMP_Context, Buf);
          Sequence := Sequence + 1;
@@ -244,7 +233,7 @@ is
       --  WORKAROUND: Componolit/Workarounds#32
       pragma Warnings (Off, "unused assignment to ""*_Context""");
       pragma Warnings (Off, """*_Context"" is set by ""*"" but not used after the call");
-      RFLX.IPv4.Packet.Initialize (IP_Context, Buf);
+      RFLX.IPv4.Packet.Initialize (IP_Context, Buf, RFLX.RFLX_Types.To_Last_Bit_Index (Buf'Last));
       RFLX.IPv4.Packet.Verify_Message (IP_Context);
       if
          not RFLX.IPv4.Packet.Structural_Valid_Message (IP_Context)

examples/apps/ping/src/icmpv4.ads

@@ -12,7 +12,6 @@ is
    pragma Unevaluated_Use_Of_Old (Allow);
 
    use type RFLX.RFLX_Builtin_Types.Bytes_Ptr;
-   use type RFLX.RFLX_Builtin_Types.Length;
    use type RFLX.RFLX_Builtin_Types.Index;
 
    procedure Get_Address (Str   : String;

examples/apps/ping/tools/create_privileged_python

@@ -1,4 +1,4 @@
 #!/bin/sh
 
-cp $(readlink -f $(which python3)) python
+cp $(readlink -f $(command -v python3)) python
 sudo -n setcap "cap_net_raw,cap_net_admin+ep" python

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"