Simplify setting of opaque fields

Ref. #557

README.md

@@ -163,7 +163,11 @@ All types and subprograms related to `Message` can be found in the package `RFLX
     - Set value of `Tag` field
 - `procedure Set_Length (Ctx : in out Context; Value : Length)`
     - Set value of `Length` field
-- `generic with procedure Process_Value (Value : out Types.Bytes); procedure Set_Value (Ctx : in out Context)`
+- `procedure Set_Value_Empty (Ctx : in out Context; Value : Types.Bytes)`
+    - Set empty `Value` field
+- `procedure Set_Value (Ctx : in out Context; Value : Types.Bytes)`
+    - Set content of `Value` field
+- `generic with procedure Process_Value (Value : out Types.Bytes); procedure Generic_Set_Value (Ctx : in out Context)`
     - Set content of `Value` field
 - `procedure Initialize_Value (Ctx : in out Context)`
     - Initialize `Value` field (precondition to switch context for generating contained message)
@@ -212,26 +216,12 @@ with RFLX.TLV.Message;
 procedure Main is
    Buffer  : RFLX.RFLX_Builtin_Types.Bytes_Ptr := new RFLX.RFLX_Builtin_Types.Bytes'(0, 0, 0, 0, 0, 0);
    Context : RFLX.TLV.Message.Context;
-   Data : RFLX.RFLX_Builtin_Types.Bytes (RFLX.RFLX_Builtin_Types.Index'First .. RFLX.RFLX_Builtin_Types.Index'First + 2**14);
-
-   function Valid_Data_Length (Length : RFLX.RFLX_Builtin_Types.Length) return Boolean is
-      (Length <= Data'Length);
-
-   procedure Write_Data (Buffer : out RFLX.RFLX_Builtin_Types.Bytes) with
-      Pre => Valid_Data_Length (Buffer'Length)
-   is
-   begin
-      Buffer := Data (Data'First .. Data'First + Buffer'Length - 1);
-   end Write_Data;
-
-   procedure Set_Value is new RFLX.TLV.Message.Set_Value (Write_Data, Valid_Data_Length);
 begin
    --  Generating message
    RFLX.TLV.Message.Initialize (Context, Buffer);
    RFLX.TLV.Message.Set_Tag (Context, RFLX.TLV.Msg_Data);
    RFLX.TLV.Message.Set_Length (Context, 4);
-   Data := (1, 2, 3, 4, others => 0);
-   Set_Value (Context);
+   RFLX.TLV.Message.Set_Value (Context, (1, 2, 3, 4));
 
    --  Checking generated message
    RFLX.TLV.Message.Take_Buffer (Context, Buffer);

examples/apps/ping/src/icmpv4.adb

@@ -186,7 +186,7 @@ is
       begin
          Buffer := Data;
       end Process_Data;
-      procedure Set_Data is new RFLX.ICMP.Message.Set_Data (Process_Data, Valid_Length);
+      procedure Set_Data is new RFLX.ICMP.Message.Generic_Set_Data (Process_Data, Valid_Length);
    begin
       pragma Warnings (Off, "unused assignment to ""*_Context""");
       RFLX.IPv4.Packet.Initialize (IP_Context, Buf);

rflx/generator/generator.py

@@ -382,6 +382,7 @@ def __create_generic_message_unit(self, message: Message) -> None:
         unit += self.__serializer.create_composite_setter_empty_procedures(message)
         unit += self.__serializer.create_array_setter_procedures(message, sequence_fields)
         unit += self.__serializer.create_opaque_setter_procedures(message)
+        unit += self.__serializer.create_generic_opaque_setter_procedures(message)
         unit += self.__serializer.create_composite_initialize_procedures(message)
 
         unit += self.__create_switch_procedures(message, sequence_fields)

rflx/generator/serializer.py

@@ -28,6 +28,7 @@
     In,
     Indexed,
     InOutParameter,
+    Length,
     LessEqual,
     Mod,
     NamedAggregate,
@@ -46,6 +47,7 @@
     Size,
     Slice,
     Statement,
+    Sub,
     Subprogram,
     SubprogramBody,
     SubprogramDeclaration,
@@ -550,7 +552,93 @@ def specification(field: Field) -> ProcedureSpecification:
 
     def create_opaque_setter_procedures(self, message: Message) -> UnitPart:
         def specification(field: Field) -> ProcedureSpecification:
-            return ProcedureSpecification(f"Set_{field.name}", [InOutParameter(["Ctx"], "Context")])
+            return ProcedureSpecification(
+                f"Set_{field.name}",
+                [InOutParameter(["Ctx"], "Context"), Parameter(["Value"], const.TYPES_BYTES)],
+            )
+
+        return UnitPart(
+            [
+                SubprogramDeclaration(
+                    specification(f),
+                    [
+                        Precondition(
+                            AndThen(
+                                *self.setter_preconditions(f),
+                                *self.composite_setter_preconditions(message, f),
+                                Equal(
+                                    Length("Value"),
+                                    Add(
+                                        Sub(
+                                            Call(
+                                                const.TYPES_BYTE_INDEX,
+                                                [
+                                                    Call(
+                                                        "Field_Last",
+                                                        [
+                                                            Variable("Ctx"),
+                                                            Variable(f.affixed_name),
+                                                        ],
+                                                    )
+                                                ],
+                                            ),
+                                            Call(
+                                                const.TYPES_BYTE_INDEX,
+                                                [
+                                                    Call(
+                                                        "Field_First",
+                                                        [
+                                                            Variable("Ctx"),
+                                                            Variable(f.affixed_name),
+                                                        ],
+                                                    )
+                                                ],
+                                            ),
+                                        ),
+                                        Number(1),
+                                    ),
+                                ),
+                            )
+                        ),
+                        Postcondition(
+                            And(
+                                *self.composite_setter_postconditions(message, f),
+                            )
+                        ),
+                    ],
+                )
+                for f, t in message.types.items()
+                if isinstance(t, Opaque) and setter_required(message, f)
+            ],
+            [
+                SubprogramBody(
+                    specification(f),
+                    [
+                        *common.field_bit_location_declarations(Variable(f.affixed_name)),
+                        *self.__field_byte_location_declarations(),
+                    ],
+                    [
+                        CallStatement(f"Initialize_{f.name}", [Variable("Ctx")]),
+                        Assignment(
+                            Slice(
+                                Selected(Variable("Ctx.Buffer"), "all"),
+                                Variable("Buffer_First"),
+                                Variable("Buffer_Last"),
+                            ),
+                            Variable("Value"),
+                        ),
+                    ],
+                )
+                for f, t in message.types.items()
+                if isinstance(t, Opaque) and setter_required(message, f)
+            ],
+        )
+
+    def create_generic_opaque_setter_procedures(self, message: Message) -> UnitPart:
+        def specification(field: Field) -> ProcedureSpecification:
+            return ProcedureSpecification(
+                f"Generic_Set_{field.name}", [InOutParameter(["Ctx"], "Context")]
+            )
 
         def formal_parameters(field: Field) -> Sequence[FormalSubprogramDeclaration]:
             return [

tests/spark/generated/rflx-arrays-generic_inner_message.adb

@@ -403,7 +403,7 @@ is
       Ctx.Cursors (Successor (Ctx, F_Payload)) := (State => S_Invalid, Predecessor => F_Payload);
    end Set_Payload_Empty;
 
-   procedure Set_Payload (Ctx : in out Context) is
+   procedure Set_Payload (Ctx : in out Context; Value : Types.Bytes) is
       First : constant Types.Bit_Index := Field_First (Ctx, F_Payload);
       Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload);
       function Buffer_First return Types.Index is
@@ -412,9 +412,21 @@ is
         (Types.Byte_Index (Last));
    begin
       Initialize_Payload (Ctx);
-      Process_Payload (Ctx.Buffer.all (Buffer_First .. Buffer_Last));
+      Ctx.Buffer.all (Buffer_First .. Buffer_Last) := Value;
    end Set_Payload;
 
+   procedure Generic_Set_Payload (Ctx : in out Context) is
+      First : constant Types.Bit_Index := Field_First (Ctx, F_Payload);
+      Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload);
+      function Buffer_First return Types.Index is
+        (Types.Byte_Index (First));
+      function Buffer_Last return Types.Index is
+        (Types.Byte_Index (Last));
+   begin
+      Initialize_Payload (Ctx);
+      Process_Payload (Ctx.Buffer.all (Buffer_First .. Buffer_Last));
+   end Generic_Set_Payload;
+
    procedure Initialize_Payload (Ctx : in out Context) is
       First : constant Types.Bit_Index := Field_First (Ctx, F_Payload);
       Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload);

tests/spark/generated/rflx-arrays-generic_inner_message.ads

@@ -247,10 +247,32 @@ is
        and Get_Length (Ctx) = Get_Length (Ctx)'Old
        and Structural_Valid (Ctx, F_Payload);
 
+   procedure Set_Payload (Ctx : in out Context; Value : Types.Bytes) with
+     Pre =>
+       not Ctx'Constrained
+       and then Has_Buffer (Ctx)
+       and then Valid_Next (Ctx, F_Payload)
+       and then Field_Condition (Ctx, (Fld => F_Payload))
+       and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod Types.Byte'Size = 1
+       and then Field_Size (Ctx, F_Payload) mod Types.Byte'Size = 0
+       and then Value'Length = Types.Byte_Index (Field_Last (Ctx, F_Payload)) - Types.Byte_Index (Field_First (Ctx, F_Payload)) + 1,
+     Post =>
+       Has_Buffer (Ctx)
+       and Message_Last (Ctx) = Field_Last (Ctx, F_Payload)
+       and Ctx.Buffer_First = Ctx.Buffer_First'Old
+       and Ctx.Buffer_Last = Ctx.Buffer_Last'Old
+       and Ctx.First = Ctx.First'Old
+       and Ctx.Last = Ctx.Last'Old
+       and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old
+       and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old
+       and Get_Length (Ctx) = Get_Length (Ctx)'Old
+       and Structural_Valid (Ctx, F_Payload);
+
    generic
       with procedure Process_Payload (Payload : out Types.Bytes);
       with function Valid_Length (Length : Types.Length) return Boolean;
-   procedure Set_Payload (Ctx : in out Context) with
+   procedure Generic_Set_Payload (Ctx : in out Context) with
      Pre =>
        not Ctx'Constrained
        and then Has_Buffer (Ctx)

tests/spark/generated/rflx-ethernet-generic_frame.adb

@@ -904,7 +904,7 @@ is
       Ctx.Cursors (Successor (Ctx, F_Type_Length)) := (State => S_Invalid, Predecessor => F_Type_Length);
    end Set_Type_Length;
 
-   procedure Set_Payload (Ctx : in out Context) is
+   procedure Set_Payload (Ctx : in out Context; Value : Types.Bytes) is
       First : constant Types.Bit_Index := Field_First (Ctx, F_Payload);
       Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload);
       function Buffer_First return Types.Index is
@@ -913,9 +913,21 @@ is
         (Types.Byte_Index (Last));
    begin
       Initialize_Payload (Ctx);
-      Process_Payload (Ctx.Buffer.all (Buffer_First .. Buffer_Last));
+      Ctx.Buffer.all (Buffer_First .. Buffer_Last) := Value;
    end Set_Payload;
 
+   procedure Generic_Set_Payload (Ctx : in out Context) is
+      First : constant Types.Bit_Index := Field_First (Ctx, F_Payload);
+      Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload);
+      function Buffer_First return Types.Index is
+        (Types.Byte_Index (First));
+      function Buffer_Last return Types.Index is
+        (Types.Byte_Index (Last));
+   begin
+      Initialize_Payload (Ctx);
+      Process_Payload (Ctx.Buffer.all (Buffer_First .. Buffer_Last));
+   end Generic_Set_Payload;
+
    procedure Initialize_Payload (Ctx : in out Context) is
       First : constant Types.Bit_Index := Field_First (Ctx, F_Payload);
       Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload);

tests/spark/generated/rflx-ethernet-generic_frame.ads

@@ -429,10 +429,35 @@ is
        and Context_Cursor (Ctx, F_TPID) = Context_Cursor (Ctx, F_TPID)'Old
        and Context_Cursor (Ctx, F_TCI) = Context_Cursor (Ctx, F_TCI)'Old;
 
+   procedure Set_Payload (Ctx : in out Context; Value : Types.Bytes) with
+     Pre =>
+       not Ctx'Constrained
+       and then Has_Buffer (Ctx)
+       and then Valid_Next (Ctx, F_Payload)
+       and then Field_Condition (Ctx, (Fld => F_Payload), Field_Size (Ctx, F_Payload))
+       and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod Types.Byte'Size = 1
+       and then Field_Size (Ctx, F_Payload) mod Types.Byte'Size = 0
+       and then Value'Length = Types.Byte_Index (Field_Last (Ctx, F_Payload)) - Types.Byte_Index (Field_First (Ctx, F_Payload)) + 1,
+     Post =>
+       Has_Buffer (Ctx)
+       and Message_Last (Ctx) = Field_Last (Ctx, F_Payload)
+       and Ctx.Buffer_First = Ctx.Buffer_First'Old
+       and Ctx.Buffer_Last = Ctx.Buffer_Last'Old
+       and Ctx.First = Ctx.First'Old
+       and Ctx.Last = Ctx.Last'Old
+       and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old
+       and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old
+       and Get_Destination (Ctx) = Get_Destination (Ctx)'Old
+       and Get_Source (Ctx) = Get_Source (Ctx)'Old
+       and Get_Type_Length_TPID (Ctx) = Get_Type_Length_TPID (Ctx)'Old
+       and Get_Type_Length (Ctx) = Get_Type_Length (Ctx)'Old
+       and Structural_Valid (Ctx, F_Payload);
+
    generic
       with procedure Process_Payload (Payload : out Types.Bytes);
       with function Valid_Length (Length : Types.Length) return Boolean;
-   procedure Set_Payload (Ctx : in out Context) with
+   procedure Generic_Set_Payload (Ctx : in out Context) with
      Pre =>
        not Ctx'Constrained
        and then Has_Buffer (Ctx)

tests/spark/generated/rflx-expression-generic_message.adb

@@ -263,7 +263,7 @@ is
       Process_Payload (Ctx.Buffer.all (First .. Last));
    end Get_Payload;
 
-   procedure Set_Payload (Ctx : in out Context) is
+   procedure Set_Payload (Ctx : in out Context; Value : Types.Bytes) is
       First : constant Types.Bit_Index := Field_First (Ctx, F_Payload);
       Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload);
       function Buffer_First return Types.Index is
@@ -272,9 +272,21 @@ is
         (Types.Byte_Index (Last));
    begin
       Initialize_Payload (Ctx);
-      Process_Payload (Ctx.Buffer.all (Buffer_First .. Buffer_Last));
+      Ctx.Buffer.all (Buffer_First .. Buffer_Last) := Value;
    end Set_Payload;
 
+   procedure Generic_Set_Payload (Ctx : in out Context) is
+      First : constant Types.Bit_Index := Field_First (Ctx, F_Payload);
+      Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload);
+      function Buffer_First return Types.Index is
+        (Types.Byte_Index (First));
+      function Buffer_Last return Types.Index is
+        (Types.Byte_Index (Last));
+   begin
+      Initialize_Payload (Ctx);
+      Process_Payload (Ctx.Buffer.all (Buffer_First .. Buffer_Last));
+   end Generic_Set_Payload;
+
    procedure Initialize_Payload (Ctx : in out Context) is
       First : constant Types.Bit_Index := Field_First (Ctx, F_Payload);
       Last : constant Types.Bit_Index := Field_Last (Ctx, F_Payload);

tests/spark/generated/rflx-expression-generic_message.ads

@@ -196,10 +196,31 @@ is
        Has_Buffer (Ctx)
        and Present (Ctx, F_Payload);
 
+   procedure Set_Payload (Ctx : in out Context; Value : Types.Bytes) with
+     Pre =>
+       not Ctx'Constrained
+       and then Has_Buffer (Ctx)
+       and then Valid_Next (Ctx, F_Payload)
+       and then Field_Condition (Ctx, (Fld => F_Payload))
+       and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod Types.Byte'Size = 1
+       and then Field_Size (Ctx, F_Payload) mod Types.Byte'Size = 0
+       and then Value'Length = Types.Byte_Index (Field_Last (Ctx, F_Payload)) - Types.Byte_Index (Field_First (Ctx, F_Payload)) + 1,
+     Post =>
+       Has_Buffer (Ctx)
+       and Message_Last (Ctx) = Field_Last (Ctx, F_Payload)
+       and Ctx.Buffer_First = Ctx.Buffer_First'Old
+       and Ctx.Buffer_Last = Ctx.Buffer_Last'Old
+       and Ctx.First = Ctx.First'Old
+       and Ctx.Last = Ctx.Last'Old
+       and Predecessor (Ctx, F_Payload) = Predecessor (Ctx, F_Payload)'Old
+       and Valid_Next (Ctx, F_Payload) = Valid_Next (Ctx, F_Payload)'Old
+       and Structural_Valid (Ctx, F_Payload);
+
    generic
       with procedure Process_Payload (Payload : out Types.Bytes);
       with function Valid_Length (Length : Types.Length) return Boolean;
-   procedure Set_Payload (Ctx : in out Context) with
+   procedure Generic_Set_Payload (Ctx : in out Context) with
      Pre =>
        not Ctx'Constrained
        and then Has_Buffer (Ctx)