Separate function for each field for Field_First

Ref. eng/recordflux/RecordFlux#1706
AdaCore · Jul 17, 2024 · fc96bb2 · fc96bb2
1 parent 7c2d2ed
commit fc96bb2
Show file tree

Hide file tree

Showing 30 changed files with 1,101 additions and 301 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -21,7 +21,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - LLVM exception in addition to Apache-2.0 for generated code (eng/recordflux/RecordFlux#1671)
 - Improve suggestions when a package name is not correct (eng/recordflux/RecordFlux#1611)
 - Severities of error messages (eng/recordflux/RecordFlux#1698, eng/recordflux/RecordFlux#1685)
-- Improve implementation of `Field_First_Internal` function (eng/recordflux/RecordFlux#1707)
+- Improve implementation of `Field_First_Internal` function (eng/recordflux/RecordFlux#1707, eng/recordflux/RecordFlux#1706)
 - Cache directory from `$HOME/.cache/RecordFlux` to `$PWD/.rflx_cache` (eng/recordflux/RecordFlux#1723)
 
 ### Fixed

diff --git a/rflx/generator/message.py b/rflx/generator/message.py
@@ -22,7 +22,6 @@
     Component,
     Constrained,
     ContractCases,
-    Decreases,
     DefaultInitialCondition,
     Depends,
     Discriminant,
@@ -79,7 +78,6 @@
     Sub,
     SubprogramBody,
     SubprogramDeclaration,
-    SubprogramVariant,
     UnitPart,
     UseTypeClause,
     ValueRange,
@@ -636,7 +634,7 @@ def create_field_size_internal_function(message: Message, prefix: str) -> UnitPa
 def create_field_first_internal_function(message: Message, prefix: str) -> UnitPart:
     def recursive_call(fld: Field) -> expr.Expr:
         return expr.Call(
-            "Field_First_Internal",
+            "Field_First_" + fld.name,
             rty.BIT_INDEX,
             [
                 expr.Variable("Cursors"),
@@ -645,7 +643,6 @@ def recursive_call(fld: Field) -> expr.Expr:
                 expr.Variable("Written_Last"),
                 expr.Variable("Buffer"),
                 *[expr.Variable(param.name) for param in message.parameter_types],
-                expr.Variable(fld.affixed_name),
             ],
         )
 
@@ -715,6 +712,63 @@ def fld_first_expr(fld: Field) -> expr.Expr:
             dist.substituted(field_size_substitution),
         ).simplified()
 
+    param_args = [Variable(param.name) for param in message.parameter_types]
+
+    def precond(fld: str) -> Precondition:
+        return Precondition(
+            AndThen(
+                Call(
+                    "Cursors_Invariant",
+                    [
+                        Variable("Cursors"),
+                        Variable("First"),
+                        Variable("Verified_Last"),
+                    ],
+                ),
+                Call(
+                    "Valid_Predecessors_Invariant",
+                    [
+                        Variable("Cursors"),
+                        Variable("First"),
+                        Variable("Verified_Last"),
+                        Variable("Written_Last"),
+                        Variable("Buffer"),
+                        *param_args,
+                    ],
+                ),
+                Call(
+                    "Valid_Next_Internal",
+                    [
+                        Variable("Cursors"),
+                        Variable("First"),
+                        Variable("Verified_Last"),
+                        Variable("Written_Last"),
+                        Variable("Buffer"),
+                        *param_args,
+                        Variable(fld),
+                    ],
+                ),
+            ),
+        )
+
+    def fld_first_func(fld: Field) -> ExpressionFunctionDeclaration:
+        return ExpressionFunctionDeclaration(
+            FunctionSpecification(
+                "Field_First_" + fld.name,
+                "RFLX_Types.Bit_Index'Base",
+                [
+                    Parameter(["Cursors"], "Field_Cursors"),
+                    Parameter(["First"], const.TYPES_BIT_INDEX),
+                    Parameter(["Verified_Last"], const.TYPES_BIT_LENGTH),
+                    Parameter(["Written_Last"], const.TYPES_BIT_LENGTH),
+                    Parameter(["Buffer"], const.TYPES_BYTES_PTR),
+                    *common.message_parameters(message),
+                ],
+            ),
+            expr_conv.to_ada(fld_first_expr(fld)),
+            [precond(fld.affixed_name)],
+        )
+
     specification = FunctionSpecification(
         "Field_First_Internal",
         "RFLX_Types.Bit_Index'Base",
@@ -729,59 +783,23 @@ def fld_first_expr(fld: Field) -> expr.Expr:
         ],
     )
 
-    param_args = [Variable(param.name) for param in message.parameter_types]
-
     return UnitPart(
         [],
         private=common.wrap_warning(
             [
+                *[fld_first_func(fld) for fld in message.fields],
                 ExpressionFunctionDeclaration(
                     specification,
                     Case(
                         Variable("Fld"),
                         [
-                            (Variable(f.affixed_name), expr_conv.to_ada(fld_first_expr(f)))
+                            (Variable(f.affixed_name), expr_conv.to_ada(recursive_call(f)))
                             for f in message.fields
                         ],
                     ),
                     [
-                        Precondition(
-                            AndThen(
-                                Call(
-                                    "Cursors_Invariant",
-                                    [
-                                        Variable("Cursors"),
-                                        Variable("First"),
-                                        Variable("Verified_Last"),
-                                    ],
-                                ),
-                                Call(
-                                    "Valid_Predecessors_Invariant",
-                                    [
-                                        Variable("Cursors"),
-                                        Variable("First"),
-                                        Variable("Verified_Last"),
-                                        Variable("Written_Last"),
-                                        Variable("Buffer"),
-                                        *param_args,
-                                    ],
-                                ),
-                                Call(
-                                    "Valid_Next_Internal",
-                                    [
-                                        Variable("Cursors"),
-                                        Variable("First"),
-                                        Variable("Verified_Last"),
-                                        Variable("Written_Last"),
-                                        Variable("Buffer"),
-                                        *param_args,
-                                        Variable("Fld"),
-                                    ],
-                                ),
-                            ),
-                        ),
+                        precond("Fld"),
                         Postcondition(TRUE),
-                        SubprogramVariant(Decreases(Variable("Fld"))),
                     ],
                 ),
             ],

diff --git a/tests/data/generator/generated/boolean_variable/rflx-p-message.ads b/tests/data/generator/generated/boolean_variable/rflx-p-message.ads
@@ -590,22 +590,35 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_A (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_A);
+
+   function Field_First_B (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 1)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_B);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_A =>
-             First,
+             Field_First_A (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_B =>
-             First + 1))
+             Field_First_B (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 

diff --git a/tests/data/generator/generated/external_io_buffers/rflx-tlv-message.ads b/tests/data/generator/generated/external_io_buffers/rflx-tlv-message.ads
@@ -702,24 +702,45 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Tag (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag);
+
+   function Field_First_Length (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 8)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length);
+
+   function Field_First_Value (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First + 24)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Tag =>
-             First,
+             Field_First_Tag (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Length =>
-             First + 8,
+             Field_First_Length (Cursors, First, Verified_Last, Written_Last, Buffer),
           when F_Value =>
-             First + 24))
+             Field_First_Value (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 

diff --git a/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads b/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads
@@ -560,32 +560,45 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_F1 (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; P : Boolean) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, P)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, P, F_F1);
+
+   function Field_First_F2 (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; P : Boolean) return RFLX_Types.Bit_Index'Base is
+     ((if
+          Well_Formed (Cursors (F_F1))
+          and then True
+       then
+          First + 8
+       elsif
+          True
+       then
+          First + 0
+       else
+          RFLX_Types.Unreachable))
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, P)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, P, F_F2);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; P : Boolean; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_F1 =>
-             First,
+             Field_First_F1 (Cursors, First, Verified_Last, Written_Last, Buffer, P),
           when F_F2 =>
-             (if
-                 Well_Formed (Cursors (F_F1))
-                 and then True
-              then
-                 First + 8
-              elsif
-                 True
-              then
-                 First + 0
-              else
-                 RFLX_Types.Unreachable)))
+             Field_First_F2 (Cursors, First, Verified_Last, Written_Last, Buffer, P)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, P)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, P, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 

diff --git a/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads b/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads
@@ -611,20 +611,25 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Data =>
-             First))
+             Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");
 

diff --git a/tests/feature/parameterized_messages/generated/rflx-test-message.ads b/tests/feature/parameterized_messages/generated/rflx-test-message.ads
@@ -710,22 +710,35 @@ private
 
    pragma Warnings (Off, "formal parameter ""*"" is not referenced");
 
+   function Field_First_Data (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Length : Test.Length; Extended : Boolean) return RFLX_Types.Bit_Index'Base is
+     (First)
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data);
+
+   function Field_First_Extension (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Length : Test.Length; Extended : Boolean) return RFLX_Types.Bit_Index'Base is
+     (Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data))
+    with
+     Pre =>
+       Cursors_Invariant (Cursors, First, Verified_Last)
+       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended)
+       and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Extension);
+
    function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Length : Test.Length; Extended : Boolean; Fld : Field) return RFLX_Types.Bit_Index'Base is
      ((case Fld is
           when F_Data =>
-             First,
+             Field_First_Data (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended),
           when F_Extension =>
-             Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data) + Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data)))
+             Field_First_Extension (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended)))
     with
      Pre =>
        Cursors_Invariant (Cursors, First, Verified_Last)
        and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended)
        and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, Fld),
      Post =>
-       True,
-     Subprogram_Variant =>
-       (Decreases =>
-         Fld);
+       True;
 
    pragma Warnings (On, "postcondition does not mention function result");