Improve accessing and setting opaque fields in SPARK

Ref. #292, #650

rflx/generator/const.py

@@ -43,6 +43,7 @@
 TYPES_BIT_INDEX = TYPES * "Bit_Index"
 TYPES_BIT_LENGTH = TYPES * "Bit_Length"
 TYPES_BYTE_INDEX = TYPES * "Byte_Index"
+TYPES_BYTE_LENGTH = TYPES * "Byte_Length"
 TYPES_FIRST_BIT_INDEX = TYPES * "First_Bit_Index"
 TYPES_LAST_BIT_INDEX = TYPES * "Last_Bit_Index"
 TYPES_OFFSET = TYPES * "Offset"

rflx/generator/generator.py

@@ -367,6 +367,7 @@ def __create_message(self, message: Message) -> None:
         unit += self.__parser.create_incomplete_message_function(message)
         unit += self.__parser.create_scalar_accessor_functions(scalar_fields)
         unit += self.__parser.create_composite_accessor_procedures(composite_fields)
+        unit += self.__parser.create_generic_composite_accessor_procedures(composite_fields)
 
         unit += self.__serializer.create_internal_functions(message, scalar_fields)
         unit += self.__serializer.create_scalar_setter_procedures(message, scalar_fields)

rflx/generator/parser.py

@@ -1,3 +1,5 @@
+# pylint: disable = too-many-lines
+
 from typing import List, Mapping, Sequence, Tuple
 
 import rflx.expression as expr
@@ -23,6 +25,7 @@
     IfStatement,
     Indexed,
     InOutParameter,
+    Length,
     Less,
     Mod,
     Mul,
@@ -31,6 +34,7 @@
     ObjectDeclaration,
     Old,
     Or,
+    OutParameter,
     Parameter,
     Postcondition,
     Pragma,
@@ -717,7 +721,104 @@ def result(field: Field) -> Expr:
     @staticmethod
     def create_composite_accessor_procedures(composite_fields: Sequence[Field]) -> UnitPart:
         def specification(field: Field) -> ProcedureSpecification:
-            return ProcedureSpecification(f"Get_{field.name}", [Parameter(["Ctx"], "Context")])
+            return ProcedureSpecification(
+                f"Get_{field.name}",
+                [Parameter(["Ctx"], "Context"), OutParameter(["Data"], const.TYPES_BYTES)],
+            )
+
+        return UnitPart(
+            [
+                SubprogramDeclaration(
+                    specification(f),
+                    [
+                        Precondition(
+                            AndThen(
+                                Call("Has_Buffer", [Variable("Ctx")]),
+                                Call(
+                                    "Present",
+                                    [Variable("Ctx"), Variable(f.affixed_name)],
+                                ),
+                                Call(
+                                    "Valid_Next",
+                                    [Variable("Ctx"), Variable(f.affixed_name)],
+                                ),
+                                Equal(
+                                    Length("Data"),
+                                    Call(
+                                        const.TYPES_BYTE_LENGTH,
+                                        [
+                                            Call(
+                                                "Field_Size",
+                                                [
+                                                    Variable("Ctx"),
+                                                    Variable(f.affixed_name),
+                                                ],
+                                            )
+                                        ],
+                                    ),
+                                ),
+                            )
+                        )
+                    ],
+                )
+                for f in composite_fields
+            ],
+            [
+                SubprogramBody(
+                    specification(f),
+                    [
+                        ObjectDeclaration(
+                            ["First"],
+                            const.TYPES_INDEX,
+                            Call(
+                                const.TYPES_BYTE_INDEX,
+                                [
+                                    Selected(
+                                        Indexed(
+                                            Variable("Ctx.Cursors"),
+                                            Variable(f.affixed_name),
+                                        ),
+                                        "First",
+                                    )
+                                ],
+                            ),
+                            True,
+                        ),
+                        ObjectDeclaration(
+                            ["Last"],
+                            const.TYPES_INDEX,
+                            Call(
+                                const.TYPES_BYTE_INDEX,
+                                [
+                                    Selected(
+                                        Indexed(
+                                            Variable("Ctx.Cursors"),
+                                            Variable(f.affixed_name),
+                                        ),
+                                        "Last",
+                                    )
+                                ],
+                            ),
+                            True,
+                        ),
+                    ],
+                    [
+                        Assignment(
+                            "Data",
+                            Slice(Variable("Ctx.Buffer.all"), Variable("First"), Variable("Last")),
+                        )
+                    ],
+                )
+                for f in composite_fields
+            ],
+        )
+
+    @staticmethod
+    def create_generic_composite_accessor_procedures(composite_fields: Sequence[Field]) -> UnitPart:
+        def specification(field: Field) -> ProcedureSpecification:
+            return ProcedureSpecification(
+                f"Generic_Get_{field.name}", [Parameter(["Ctx"], "Context")]
+            )
 
         return UnitPart(
             [

rflx/generator/serializer.py

@@ -1,5 +1,3 @@
-# pylint: disable=too-many-lines
-
 from typing import Mapping, Sequence
 
 from rflx.ada import (
@@ -49,7 +47,6 @@
     Size,
     Slice,
     Statement,
-    Sub,
     Subprogram,
     SubprogramBody,
     SubprogramDeclaration,
@@ -564,7 +561,7 @@ def create_opaque_setter_procedures(self, message: Message) -> UnitPart:
         def specification(field: Field) -> ProcedureSpecification:
             return ProcedureSpecification(
                 f"Set_{field.name}",
-                [InOutParameter(["Ctx"], "Context"), Parameter(["Value"], const.TYPES_BYTES)],
+                [InOutParameter(["Ctx"], "Context"), Parameter(["Data"], const.TYPES_BYTES)],
             )
 
         return UnitPart(
@@ -577,35 +574,18 @@ def specification(field: Field) -> ProcedureSpecification:
                                 *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),
-                                                        ],
-                                                    )
-                                                ],
-                                            ),
+                                    Length("Data"),
+                                    Call(
+                                        const.TYPES_BYTE_LENGTH,
+                                        [
                                             Call(
-                                                const.TYPES_BYTE_INDEX,
+                                                "Field_Size",
                                                 [
-                                                    Call(
-                                                        "Field_First",
-                                                        [
-                                                            Variable("Ctx"),
-                                                            Variable(f.affixed_name),
-                                                        ],
-                                                    )
+                                                    Variable("Ctx"),
+                                                    Variable(f.affixed_name),
                                                 ],
-                                            ),
-                                        ),
-                                        Number(1),
+                                            )
+                                        ],
                                     ),
                                 ),
                             )
@@ -636,7 +616,7 @@ def specification(field: Field) -> ProcedureSpecification:
                                 Variable("Buffer_First"),
                                 Variable("Buffer_Last"),
                             ),
-                            Variable("Value"),
+                            Variable("Data"),
                         ),
                     ],
                 )

rflx/templates/rflx_generic_types.ads

@@ -50,6 +50,9 @@ is
    function Byte_Index (Bit_Idx : Bit_Length) return Index is
      (Index (Length ((Bit_Idx - 1) / 8) + 1));
 
+   function Byte_Length (Bit_Len : Bit_Length) return Length is
+     (Length ((Bit_Len + 7) / 8));
+
    function First_Bit_Index (Idx : Index) return Bit_Index is
      ((Bit_Length (Idx) - 1) * 8 + 1);
 

tests/spark/generated/rflx-derivation-message.adb

@@ -264,13 +264,20 @@ is
       Verify (Ctx, F_Value);
    end Verify_Message;
 
-   procedure Get_Value (Ctx : Context) is
+   procedure Get_Value (Ctx : Context; Data : out RFLX_Types.Bytes) is
       First : constant RFLX_Types.Index := RFLX_Types.Byte_Index (Ctx.Cursors (F_Value).First);
       Last : constant RFLX_Types.Index := RFLX_Types.Byte_Index (Ctx.Cursors (F_Value).Last);
    begin
-      Process_Value (Ctx.Buffer.all (First .. Last));
+      Data := Ctx.Buffer.all (First .. Last);
    end Get_Value;
 
+   procedure Generic_Get_Value (Ctx : Context) is
+      First : constant RFLX_Types.Index := RFLX_Types.Byte_Index (Ctx.Cursors (F_Value).First);
+      Last : constant RFLX_Types.Index := RFLX_Types.Byte_Index (Ctx.Cursors (F_Value).Last);
+   begin
+      Process_Value (Ctx.Buffer.all (First .. Last));
+   end Generic_Get_Value;
+
    procedure Set_Field_Value (Ctx : in out Context; Val : Field_Dependent_Value; Fst, Lst : out RFLX_Types.Bit_Index) with
      Pre =>
        not Ctx'Constrained
@@ -395,7 +402,7 @@ is
       Initialize_Value_Private (Ctx);
    end Initialize_Value;
 
-   procedure Set_Value (Ctx : in out Context; Value : RFLX_Types.Bytes) is
+   procedure Set_Value (Ctx : in out Context; Data : RFLX_Types.Bytes) is
       First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Value);
       Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Value);
       function Buffer_First return RFLX_Types.Index is
@@ -404,7 +411,7 @@ is
         (RFLX_Types.Byte_Index (Last));
    begin
       Initialize_Value_Private (Ctx);
-      Ctx.Buffer.all (Buffer_First .. Buffer_Last) := Value;
+      Ctx.Buffer.all (Buffer_First .. Buffer_Last) := Data;
    end Set_Value;
 
    procedure Generic_Set_Value (Ctx : in out Context) is

tests/spark/generated/rflx-derivation-message.ads

@@ -267,9 +267,16 @@ is
 
    pragma Warnings (On, "precondition is always False");
 
+   procedure Get_Value (Ctx : Context; Data : out RFLX_Types.Bytes) with
+     Pre =>
+       Has_Buffer (Ctx)
+       and then Present (Ctx, F_Value)
+       and then Valid_Next (Ctx, F_Value)
+       and then Data'Length = RFLX_Types.Byte_Length (Field_Size (Ctx, F_Value));
+
    generic
       with procedure Process_Value (Value : RFLX_Types.Bytes);
-   procedure Get_Value (Ctx : Context) with
+   procedure Generic_Get_Value (Ctx : Context) with
      Pre =>
        Has_Buffer (Ctx)
        and Present (Ctx, F_Value);
@@ -381,7 +388,7 @@ is
        and Get_Tag (Ctx) = Get_Tag (Ctx)'Old
        and Get_Length (Ctx) = Get_Length (Ctx)'Old;
 
-   procedure Set_Value (Ctx : in out Context; Value : RFLX_Types.Bytes) with
+   procedure Set_Value (Ctx : in out Context; Data : RFLX_Types.Bytes) with
      Pre =>
        not Ctx'Constrained
        and then Has_Buffer (Ctx)
@@ -391,7 +398,7 @@ is
        and then Field_First (Ctx, F_Value) mod RFLX_Types.Byte'Size = 1
        and then Field_Last (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0
        and then Field_Size (Ctx, F_Value) mod RFLX_Types.Byte'Size = 0
-       and then Value'Length = RFLX_Types.Byte_Index (Field_Last (Ctx, F_Value)) - RFLX_Types.Byte_Index (Field_First (Ctx, F_Value)) + 1,
+       and then Data'Length = RFLX_Types.Byte_Length (Field_Size (Ctx, F_Value)),
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid (Ctx, F_Value)

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

@@ -403,13 +403,20 @@ is
       Verify (Ctx, F_Payload);
    end Verify_Message;
 
-   procedure Get_Payload (Ctx : Context) is
+   procedure Get_Payload (Ctx : Context; Data : out RFLX_Types.Bytes) is
       First : constant RFLX_Types.Index := RFLX_Types.Byte_Index (Ctx.Cursors (F_Payload).First);
       Last : constant RFLX_Types.Index := RFLX_Types.Byte_Index (Ctx.Cursors (F_Payload).Last);
    begin
-      Process_Payload (Ctx.Buffer.all (First .. Last));
+      Data := Ctx.Buffer.all (First .. Last);
    end Get_Payload;
 
+   procedure Generic_Get_Payload (Ctx : Context) is
+      First : constant RFLX_Types.Index := RFLX_Types.Byte_Index (Ctx.Cursors (F_Payload).First);
+      Last : constant RFLX_Types.Index := RFLX_Types.Byte_Index (Ctx.Cursors (F_Payload).Last);
+   begin
+      Process_Payload (Ctx.Buffer.all (First .. Last));
+   end Generic_Get_Payload;
+
    procedure Set_Field_Value (Ctx : in out Context; Val : Field_Dependent_Value; Fst, Lst : out RFLX_Types.Bit_Index) with
      Pre =>
        not Ctx'Constrained
@@ -580,7 +587,7 @@ is
       Initialize_Payload_Private (Ctx);
    end Initialize_Payload;
 
-   procedure Set_Payload (Ctx : in out Context; Value : RFLX_Types.Bytes) is
+   procedure Set_Payload (Ctx : in out Context; Data : RFLX_Types.Bytes) is
       First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Payload);
       Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Payload);
       function Buffer_First return RFLX_Types.Index is
@@ -589,7 +596,7 @@ is
         (RFLX_Types.Byte_Index (Last));
    begin
       Initialize_Payload_Private (Ctx);
-      Ctx.Buffer.all (Buffer_First .. Buffer_Last) := Value;
+      Ctx.Buffer.all (Buffer_First .. Buffer_Last) := Data;
    end Set_Payload;
 
    procedure Generic_Set_Payload (Ctx : in out Context) is

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

@@ -289,9 +289,16 @@ is
 
    pragma Warnings (On, "precondition is always False");
 
+   procedure Get_Payload (Ctx : Context; Data : out RFLX_Types.Bytes) with
+     Pre =>
+       Has_Buffer (Ctx)
+       and then Present (Ctx, F_Payload)
+       and then Valid_Next (Ctx, F_Payload)
+       and then Data'Length = RFLX_Types.Byte_Length (Field_Size (Ctx, F_Payload));
+
    generic
       with procedure Process_Payload (Payload : RFLX_Types.Bytes);
-   procedure Get_Payload (Ctx : Context) with
+   procedure Generic_Get_Payload (Ctx : Context) with
      Pre =>
        Has_Buffer (Ctx)
        and Present (Ctx, F_Payload);
@@ -513,7 +520,7 @@ is
        and Get_Type_Length_TPID (Ctx) = Get_Type_Length_TPID (Ctx)'Old
        and Get_Type_Length (Ctx) = Get_Type_Length (Ctx)'Old;
 
-   procedure Set_Payload (Ctx : in out Context; Value : RFLX_Types.Bytes) with
+   procedure Set_Payload (Ctx : in out Context; Data : RFLX_Types.Bytes) with
      Pre =>
        not Ctx'Constrained
        and then Has_Buffer (Ctx)
@@ -523,7 +530,7 @@ is
        and then Field_First (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 1
        and then Field_Last (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0
        and then Field_Size (Ctx, F_Payload) mod RFLX_Types.Byte'Size = 0
-       and then Value'Length = RFLX_Types.Byte_Index (Field_Last (Ctx, F_Payload)) - RFLX_Types.Byte_Index (Field_First (Ctx, F_Payload)) + 1,
+       and then Data'Length = RFLX_Types.Byte_Length (Field_Size (Ctx, F_Payload)),
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid (Ctx, F_Payload)