Fix size determination of write buffer

Ref. #895
AdaCore · May 10, 2022 · 0d3836c · 0d3836c
1 parent 8f1a273
commit 0d3836c
Show file tree

Hide file tree

Showing 20 changed files with 267 additions and 63 deletions.
diff --git a/rflx/generator/session.py b/rflx/generator/session.py
@@ -386,7 +386,7 @@ def is_global(identifier: ID) -> bool:
 
         if has_reads:
             unit += self._create_needs_data_function(channel_reads)
-            unit += self._create_write_buffer_size_function(channel_reads)
+            unit += self._create_write_buffer_size_function(channel_reads, is_global)
             unit += self._create_write_procedure(channel_reads, is_global)
 
         return (
@@ -1397,28 +1397,59 @@ def _create_read_buffer_size_function(
 
     @staticmethod
     def _create_write_buffer_size_function(
-        channel_reads: dict[rid.ID, list[ChannelAccess]]
+        channel_reads: dict[rid.ID, list[ChannelAccess]],
+        is_global: Callable[[ID], bool],
     ) -> UnitPart:
         specification = FunctionSpecification(
             "Write_Buffer_Size",
             const.TYPES_LENGTH,
-            [Parameter(["Unused_Ctx"], "Context'Class"), Parameter(["Chan"], "Channel")],
+            [
+                Parameter(["Ctx"], "Context'Class"),
+                Parameter(["Chan"], "Channel"),
+            ],
         )
 
         return UnitPart(
             [
-                SubprogramDeclaration(specification),
+                SubprogramDeclaration(
+                    specification,
+                    [
+                        Precondition(
+                            AndThen(
+                                Call("Initialized", [Variable("Ctx")]),
+                                Call("Needs_Data", [Variable("Ctx"), Variable("Chan")]),
+                            )
+                        ),
+                    ],
+                ),
             ],
             private=[
                 ExpressionFunctionDeclaration(
                     specification,
                     Case(
                         Variable("Chan"),
                         [
-                            # ISSUE: Componolit/RecordFlux#895
-                            # Size of correspondig buffer must be returned instead of constant
-                            # value.
-                            (Variable(f"C_{channel}"), Number(4096) if reads else Number(0))
+                            (
+                                Variable(f"C_{channel}"),
+                                Case(
+                                    Variable("Ctx.P.Next_State"),
+                                    [
+                                        *[
+                                            (
+                                                Variable(f"S_{read.state}"),
+                                                Call(
+                                                    read.message_type * "Buffer_Length",
+                                                    [Variable(context_id(read.message, is_global))],
+                                                ),
+                                            )
+                                            for read in reads
+                                        ],
+                                        (Variable("others"), const.UNREACHABLE),
+                                    ],
+                                )
+                                if reads
+                                else Number(0),
+                            )
                             for channel, reads in channel_reads.items()
                         ],
                     ),

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-test-session.ads b/tests/integration/messages_with_implict_size/generated/rflx-test-session.ads
@@ -90,7 +90,10 @@ is
      Pre =>
        Initialized (Ctx);
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length;
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with
+     Pre =>
+       Initialized (Ctx)
+       and then Needs_Data (Ctx, Chan);
 
    procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with
      Pre =>
@@ -164,9 +167,13 @@ private
                  when others =>
                     False)));
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
      ((case Chan is
           when C_Channel =>
-             4096));
+             (case Ctx.P.Next_State is
+                 when S_Start =>
+                    Universal.Message.Buffer_Length (Ctx.P.M_R_Ctx),
+                 when others =>
+                    RFLX_Types.Unreachable)));
 
 end RFLX.Test.Session;
diff --git a/tests/integration/messages_with_single_opaque_field/generated/rflx-test-session.ads b/tests/integration/messages_with_single_opaque_field/generated/rflx-test-session.ads
@@ -89,7 +89,10 @@ is
      Pre =>
        Initialized (Ctx);
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length;
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with
+     Pre =>
+       Initialized (Ctx)
+       and then Needs_Data (Ctx, Chan);
 
    procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with
      Pre =>
@@ -163,9 +166,13 @@ private
                  when others =>
                     False)));
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
      ((case Chan is
           when C_Channel =>
-             4096));
+             (case Ctx.P.Next_State is
+                 when S_Start =>
+                    Test.Message.Buffer_Length (Ctx.P.M_R_Ctx),
+                 when others =>
+                    RFLX_Types.Unreachable)));
 
 end RFLX.Test.Session;
diff --git a/tests/integration/parameterized_messages/generated/rflx-test-session.ads b/tests/integration/parameterized_messages/generated/rflx-test-session.ads
@@ -89,7 +89,10 @@ is
      Pre =>
        Initialized (Ctx);
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length;
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with
+     Pre =>
+       Initialized (Ctx)
+       and then Needs_Data (Ctx, Chan);
 
    procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with
      Pre =>
@@ -163,9 +166,13 @@ private
                  when others =>
                     False)));
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
      ((case Chan is
           when C_C =>
-             4096));
+             (case Ctx.P.Next_State is
+                 when S_Receive =>
+                    Test.Message.Buffer_Length (Ctx.P.M_R_Ctx),
+                 when others =>
+                    RFLX_Types.Unreachable)));
 
 end RFLX.Test.Session;
diff --git a/tests/integration/session_binding/generated/rflx-test-session.ads b/tests/integration/session_binding/generated/rflx-test-session.ads
@@ -90,7 +90,10 @@ is
      Pre =>
        Initialized (Ctx);
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length;
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with
+     Pre =>
+       Initialized (Ctx)
+       and then Needs_Data (Ctx, Chan);
 
    procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with
      Pre =>
@@ -159,9 +162,13 @@ private
                  when others =>
                     False)));
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
      ((case Chan is
           when C_Channel =>
-             4096));
+             (case Ctx.P.Next_State is
+                 when S_Start =>
+                    Universal.Message.Buffer_Length (Ctx.P.Message_Ctx),
+                 when others =>
+                    RFLX_Types.Unreachable)));
 
 end RFLX.Test.Session;
diff --git a/tests/integration/session_channel_multiplexing/generated/rflx-test-session.ads b/tests/integration/session_channel_multiplexing/generated/rflx-test-session.ads
@@ -90,7 +90,10 @@ is
      Pre =>
        Initialized (Ctx);
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length;
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with
+     Pre =>
+       Initialized (Ctx)
+       and then Needs_Data (Ctx, Chan);
 
    procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with
      Pre =>
@@ -175,10 +178,20 @@ private
           when C_O =>
              False));
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
      ((case Chan is
-          when C_I_1 | C_I_2 =>
-             4096,
+          when C_I_1 =>
+             (case Ctx.P.Next_State is
+                 when S_Start =>
+                    Universal.Message.Buffer_Length (Ctx.P.Message_1_Ctx),
+                 when others =>
+                    RFLX_Types.Unreachable),
+          when C_I_2 =>
+             (case Ctx.P.Next_State is
+                 when S_Start =>
+                    Universal.Message.Buffer_Length (Ctx.P.Message_2_Ctx),
+                 when others =>
+                    RFLX_Types.Unreachable),
           when C_O =>
              0));
 

diff --git a/tests/integration/session_channels/generated/rflx-test-session.ads b/tests/integration/session_channels/generated/rflx-test-session.ads
@@ -90,7 +90,10 @@ is
      Pre =>
        Initialized (Ctx);
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length;
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with
+     Pre =>
+       Initialized (Ctx)
+       and then Needs_Data (Ctx, Chan);
 
    procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with
      Pre =>
@@ -165,10 +168,14 @@ private
           when C_O =>
              False));
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
      ((case Chan is
           when C_I =>
-             4096,
+             (case Ctx.P.Next_State is
+                 when S_Start =>
+                    Universal.Message.Buffer_Length (Ctx.P.Message_Ctx),
+                 when others =>
+                    RFLX_Types.Unreachable),
           when C_O =>
              0));
 

diff --git a/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session.ads b/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session.ads
@@ -90,7 +90,10 @@ is
      Pre =>
        Initialized (Ctx);
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length;
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with
+     Pre =>
+       Initialized (Ctx)
+       and then Needs_Data (Ctx, Chan);
 
    procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with
      Pre =>
@@ -159,9 +162,13 @@ private
                  when others =>
                     False)));
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
      ((case Chan is
           when C_Channel =>
-             4096));
+             (case Ctx.P.Next_State is
+                 when S_Start =>
+                    Universal.Message.Buffer_Length (Ctx.P.Message_Ctx),
+                 when others =>
+                    RFLX_Types.Unreachable)));
 
 end RFLX.Test.Session;
diff --git a/tests/integration/session_conversion/generated/rflx-test-session.ads b/tests/integration/session_conversion/generated/rflx-test-session.ads
@@ -91,7 +91,10 @@ is
      Pre =>
        Initialized (Ctx);
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length;
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with
+     Pre =>
+       Initialized (Ctx)
+       and then Needs_Data (Ctx, Chan);
 
    procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with
      Pre =>
@@ -165,9 +168,13 @@ private
                  when others =>
                     False)));
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
      ((case Chan is
           when C_Channel =>
-             4096));
+             (case Ctx.P.Next_State is
+                 when S_Start =>
+                    Universal.Message.Buffer_Length (Ctx.P.Message_Ctx),
+                 when others =>
+                    RFLX_Types.Unreachable)));
 
 end RFLX.Test.Session;
diff --git a/tests/integration/session_endianness/generated/rflx-test-session.ads b/tests/integration/session_endianness/generated/rflx-test-session.ads
@@ -92,7 +92,10 @@ is
      Pre =>
        Initialized (Ctx);
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length;
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with
+     Pre =>
+       Initialized (Ctx)
+       and then Needs_Data (Ctx, Chan);
 
    procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with
      Pre =>
@@ -187,10 +190,16 @@ private
           when C_O =>
              False));
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
      ((case Chan is
           when C_I =>
-             4096,
+             (case Ctx.P.Next_State is
+                 when S_Start =>
+                    Messages.Msg_LE_Nested.Buffer_Length (Ctx.P.In_Msg_Ctx),
+                 when S_Read2 =>
+                    Messages.Msg_LE.Buffer_Length (Ctx.P.In_Msg2_Ctx),
+                 when others =>
+                    RFLX_Types.Unreachable),
           when C_O =>
              0));
 

diff --git a/tests/integration/session_functions/generated/rflx-test-session.ads b/tests/integration/session_functions/generated/rflx-test-session.ads
@@ -110,7 +110,10 @@ is
      Pre =>
        Initialized (Ctx);
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length;
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with
+     Pre =>
+       Initialized (Ctx)
+       and then Needs_Data (Ctx, Chan);
 
    procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with
      Pre =>
@@ -184,9 +187,13 @@ private
                  when others =>
                     False)));
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
      ((case Chan is
           when C_Channel =>
-             4096));
+             (case Ctx.P.Next_State is
+                 when S_Start =>
+                    Universal.Message.Buffer_Length (Ctx.P.Message_Ctx),
+                 when others =>
+                    RFLX_Types.Unreachable)));
 
 end RFLX.Test.Session;
diff --git a/tests/integration/session_integration/generated/rflx-test-session.ads b/tests/integration/session_integration/generated/rflx-test-session.ads
@@ -90,7 +90,10 @@ is
      Pre =>
        Initialized (Ctx);
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length;
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length with
+     Pre =>
+       Initialized (Ctx)
+       and then Needs_Data (Ctx, Chan);
 
    procedure Write (Ctx : in out Context'Class; Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with
      Pre =>
@@ -159,9 +162,13 @@ private
                  when others =>
                     False)));
 
-   function Write_Buffer_Size (Unused_Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
+   function Write_Buffer_Size (Ctx : Context'Class; Chan : Channel) return RFLX_Types.Length is
      ((case Chan is
           when C_Channel =>
-             4096));
+             (case Ctx.P.Next_State is
+                 when S_Start =>
+                    Universal.Message.Buffer_Length (Ctx.P.Message_Ctx),
+                 when others =>
+                    RFLX_Types.Unreachable)));
 
 end RFLX.Test.Session;