Enable use of Opaque attribute in function calls

Ref. #984

rflx/generator/allocator.py

@@ -126,7 +126,7 @@ def get_slot_ptr(self, location: Optional[Location]) -> ID:
         slot_id: int = self._allocation_slots[location]
         return self._slot_name(slot_id)
 
-    def get_size(self, variable: rid.ID, state: Optional[rid.ID] = None) -> int:
+    def get_size(self, variable: Optional[rid.ID] = None, state: Optional[rid.ID] = None) -> int:
         return self._integration.get_size(self._session.identifier, variable, state)
 
     @staticmethod

rflx/generator/session.py

@@ -2703,7 +2703,7 @@ def _assign_to_call(  # pylint: disable = too-many-locals
         exception_handler: ExceptionHandler,
         is_global: Callable[[ID], bool],
     ) -> Sequence[Statement]:
-        pre_call = []
+        pre_call: list[Statement] = []
         post_call = []
         local_declarations = []
         target_id = variable_id(target, is_global)
@@ -2793,7 +2793,7 @@ def _assign_to_call(  # pylint: disable = too-many-locals
                                 First(const.TYPES_INDEX),
                                 Add(
                                     First(const.TYPES_INDEX),
-                                    Number(4095),
+                                    Number(self._allocator.get_size() - 1),
                                 ),
                             ),
                             NamedAggregate(("others", Number(0))),
@@ -2832,6 +2832,85 @@ def _assign_to_call(  # pylint: disable = too-many-locals
                     ),
                 )
                 arguments.append(argument)
+            elif (
+                isinstance(a, expr.Opaque)
+                and isinstance(a.prefix, expr.Variable)
+                and isinstance(a.prefix.type_, rty.Message)
+            ):
+                argument_name = f"RFLX_{call_expr.identifier}_Arg_{i}_{a.prefix}"
+                argument_length = f"{argument_name}_Length"
+                argument = expr.Slice(
+                    expr.Variable(argument_name),
+                    expr.First(const.TYPES_INDEX),
+                    expr.Add(
+                        expr.First(const.TYPES_INDEX),
+                        expr.Call(
+                            const.TYPES_INDEX,
+                            [expr.Add(expr.Variable(argument_length), expr.Number(1))],
+                        ),
+                        -expr.Number(2),
+                    ),
+                )
+                type_identifier = self._ada_type(a.prefix.type_.identifier)
+                message_context = context_id(a.prefix.identifier, is_global)
+                local_declarations.extend(
+                    [
+                        # ISSUE: Componolit/RecordFlux#917
+                        # The use of intermediate buffers should be removed.
+                        ObjectDeclaration(
+                            [argument_name],
+                            Slice(
+                                Variable(const.TYPES_BYTES),
+                                First(const.TYPES_INDEX),
+                                Add(
+                                    First(const.TYPES_INDEX),
+                                    Number(self._allocator.get_size() - 1),
+                                ),
+                            ),
+                            NamedAggregate(("others", Number(0))),
+                        ),
+                        ObjectDeclaration(
+                            [argument_length],
+                            const.TYPES_LENGTH,
+                            Call(
+                                type_identifier * "Byte_Size",
+                                [
+                                    Variable(message_context),
+                                ],
+                            ),
+                            constant=True,
+                        ),
+                    ]
+                )
+                pre_call.extend(
+                    [
+                        self._raise_exception_if(
+                            Not(
+                                Call(
+                                    type_identifier * "Structural_Valid_Message",
+                                    [Variable(message_context)],
+                                )
+                            ),
+                            f'invalid message "{message_context}"',
+                            exception_handler,
+                        ),
+                        CallStatement(
+                            type_identifier * "Message_Data",
+                            [
+                                Variable(message_context),
+                                argument.ada_expr(),
+                            ],
+                        ),
+                    ]
+                )
+                arguments.append(argument)
+            elif (
+                isinstance(a, expr.Variable)
+                and isinstance(a.type_, rty.Enumeration)
+                and a.type_.always_valid
+                and a.identifier in self._session.literals
+            ):
+                arguments.append(expr.NamedAggregate(("Known", expr.TRUE), ("Enum", a)))
             else:
                 arguments.append(a)
 
@@ -3542,6 +3621,24 @@ def _ensure(
         )
         return nested
 
+    def _raise_exception_if(
+        self,
+        condition: Expr,
+        error_message: str,
+        exception_handler: ExceptionHandler,
+    ) -> IfStatement:
+        return IfStatement(
+            [
+                (
+                    condition,
+                    [
+                        *self._debug_output(f"Error: {error_message}"),
+                        *exception_handler.execute(),
+                    ],
+                ),
+            ]
+        )
+
     @staticmethod
     def _exit_on_deferred_exception() -> ExitStatement:
         return ExitStatement(Variable("RFLX_Exception"))

rflx/integration.py

@@ -87,14 +87,15 @@ def validate(self, model: Model, error: RecordFluxError) -> None:
                 self._validate_globals(package, integration, session, error)
                 self._validate_states(package, integration, session, error)
 
-    def get_size(self, session: ID, variable: ID, state: Optional[ID]) -> int:
+    def get_size(self, session: ID, variable: Optional[ID], state: Optional[ID]) -> int:
         """
         Return the requested buffer size for a variable of a given session and state.
 
-        If state is None, the variable is assumed to be a global
-        variable. If no specific buffer size was requested for the variable,
-        return the default buffer size for the session, if present, or the
-        default buffer size for RecordFlux.
+        If state is None, the variable is assumed to be a global variable. If variable is None or no
+        specific buffer size was requested for the variable, return the default buffer size for the
+        session, if present, or the default buffer size for RecordFlux.
+
+        The returned size is in bytes.
         """
         integration_package = str(session.parent).lower()
         if integration_package not in self._packages:
@@ -105,8 +106,12 @@ def get_size(self, session: ID, variable: ID, state: Optional[ID]) -> int:
             return self.defaultsize
 
         buffer_size = self._packages[integration_package].session[session_name].buffer_size
-        variable_name = str(variable.name)
         default_size = self.defaultsize if buffer_size.default is None else buffer_size.default
+
+        if variable is None:
+            return default_size
+
+        variable_name = str(variable.name)
         if state is None:
             if buffer_size.global_ is not None and variable_name in buffer_size.global_:
                 return buffer_size.global_[variable_name]

rflx/model/session.py

@@ -1,3 +1,5 @@
+from __future__ import annotations
+
 import itertools
 from abc import abstractmethod
 from collections import defaultdict
@@ -200,6 +202,10 @@ def __str__(self) -> str:
             f"is\n{indent(declarations, 3)}begin\n{indent(states, 3)}\nend {self.identifier.name}"
         )
 
+    @property
+    def literals(self) -> Mapping[ID, mty.Type]:
+        return self._literals
+
     def _resolve_function_calls(self) -> None:
         """
         Replace variables by function calls where necessary.

tests/integration/session_functions/config.yml

@@ -7,6 +7,10 @@ sequence: |
   Write Channel: 1 0 3 0 1 2
   State: Start
   State: Process
-  Read Channel: 1 0 1 2
+  Read Channel: 1 3 0 1 2
   State: Reply
-prove:
+  State: Process_2
+  Read Channel: 1 6 1 0 3 0 1 2
+  State: Reply_2
+# ISSUE: Componolit/RecordFlux#691
+# prove:

tests/integration/session_functions/generated/rflx-fixed_size-simple_message.adb → tests/integration/session_functions/generated/rflx-test-definite_message.adb

@@ -1,7 +1,7 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 
-package body RFLX.Fixed_Size.Simple_Message with
+package body RFLX.Test.Definite_Message with
   SPARK_Mode
 is
 
@@ -83,6 +83,8 @@ is
    function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
      ((case Fld is
           when F_Message_Type =>
+             F_Length,
+          when F_Length =>
              F_Data,
           when F_Data =>
              F_Final))
@@ -97,6 +99,8 @@ is
    function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is
      ((case Fld is
           when F_Message_Type =>
+             Invalid (Ctx.Cursors (F_Length)),
+          when F_Length =>
              Invalid (Ctx.Cursors (F_Data)),
           when F_Data =>
              True));
@@ -174,7 +178,7 @@ is
       Buffer_Last : constant RFLX_Types.Index := RFLX_Types.To_Index (Last);
       Offset : constant RFLX_Types.Offset := RFLX_Types.Offset ((RFLX_Types.Byte'Size - Last mod RFLX_Types.Byte'Size) mod RFLX_Types.Byte'Size);
       Size : constant Positive := (case Fld is
-          when F_Message_Type =>
+          when F_Message_Type | F_Length =>
              8,
           when others =>
              Positive'Last);
@@ -276,7 +280,11 @@ is
        and then (case Fld is
                     when F_Message_Type =>
                        Get_Message_Type (Ctx) = To_Actual (Val)
-                       and (Predecessor (Ctx, F_Data) = F_Message_Type
+                       and (Predecessor (Ctx, F_Length) = F_Message_Type
+                            and Valid_Next (Ctx, F_Length)),
+                    when F_Length =>
+                       Get_Length (Ctx) = To_Actual (Val)
+                       and (Predecessor (Ctx, F_Data) = F_Length
                             and Valid_Next (Ctx, F_Data)),
                     when F_Data =>
                        (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, Fld)))
@@ -297,10 +305,10 @@ is
       Ctx := Ctx'Update (Verified_Last => ((Last + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size, Written_Last => ((Last + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size);
       pragma Warnings (On, "attribute Update is an obsolescent feature");
       pragma Assert (Size = (case Fld is
-                         when F_Message_Type =>
+                         when F_Message_Type | F_Length =>
                             8,
                          when F_Data =>
-                            24));
+                            RFLX_Types.Bit_Length (Ctx.Cursors (F_Length).Value) * 8));
       if State_Valid then
          Ctx.Cursors (Fld) := (State => S_Valid, First => First, Last => Last, Value => Val, Predecessor => Ctx.Cursors (Fld).Predecessor);
       else
@@ -318,6 +326,15 @@ is
       RFLX_Types.Insert (Value, Ctx.Buffer, Buffer_First, Buffer_Last, Offset, 8, RFLX_Types.High_Order_First);
    end Set_Message_Type;
 
+   procedure Set_Length (Ctx : in out Context; Val : RFLX.Test.Length) is
+      Value : constant RFLX_Types.U64 := To_U64 (Val);
+      Buffer_First, Buffer_Last : RFLX_Types.Index;
+      Offset : RFLX_Types.Offset;
+   begin
+      Set (Ctx, F_Length, Value, 8, True, Buffer_First, Buffer_Last, Offset);
+      RFLX_Types.Insert (Value, Ctx.Buffer, Buffer_First, Buffer_Last, Offset, 8, RFLX_Types.High_Order_First);
+   end Set_Length;
+
    procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type) with
      Pre =>
        not Ctx'Constrained
@@ -330,9 +347,10 @@ is
        Has_Buffer (Ctx)
        and Valid (Ctx, F_Message_Type)
        and Get_Message_Type (Ctx) = Val
+       and Invalid (Ctx, F_Length)
        and Invalid (Ctx, F_Data)
-       and (Predecessor (Ctx, F_Data) = F_Message_Type
-            and Valid_Next (Ctx, F_Data))
+       and (Predecessor (Ctx, F_Length) = F_Message_Type
+            and Valid_Next (Ctx, F_Length))
        and Ctx.Buffer_First = Ctx.Buffer_First'Old
        and Ctx.Buffer_Last = Ctx.Buffer_Last'Old
        and Ctx.First = Ctx.First'Old
@@ -348,6 +366,13 @@ is
       RFLX_Types.Insert (Value, Ctx.Buffer, Buffer_First, Buffer_Last, Offset, 8, RFLX_Types.High_Order_First);
    end Set_Message_Type;
 
+   procedure Set_Data_Empty (Ctx : in out Context) is
+      Unused_Buffer_First, Unused_Buffer_Last : RFLX_Types.Index;
+      Unused_Offset : RFLX_Types.Offset;
+   begin
+      Set (Ctx, F_Data, 0, 0, True, Unused_Buffer_First, Unused_Buffer_Last, Unused_Offset);
+   end Set_Data_Empty;
+
    procedure Initialize_Data_Private (Ctx : in out Context; Length : RFLX_Types.Length) with
      Pre =>
        not Ctx'Constrained
@@ -368,6 +393,7 @@ is
        and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
        and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
        and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old
+       and Get_Length (Ctx) = Get_Length (Ctx)'Old
    is
       First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data);
       Last : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data) + RFLX_Types.Bit_Length (Length) * RFLX_Types.Byte'Size - 1;
@@ -408,6 +434,7 @@ is
    procedure To_Structure (Ctx : Context; Struct : out Structure) is
    begin
       Struct.Message_Type := Get_Message_Type (Ctx);
+      Struct.Length := Get_Length (Ctx);
       Struct.Data := (others => 0);
       Get_Data (Ctx, Struct.Data (Struct.Data'First .. Struct.Data'First + RFLX_Types.Index (RFLX_Types.To_Length (Field_Size (Ctx, F_Data)) + 1) - 2));
    end To_Structure;
@@ -416,7 +443,8 @@ is
    begin
       Reset (Ctx);
       Set_Message_Type (Ctx, Struct.Message_Type);
-      Set_Data (Ctx, Struct.Data);
+      Set_Length (Ctx, Struct.Length);
+      Set_Data (Ctx, Struct.Data (Struct.Data'First .. Struct.Data'First + RFLX_Types.Index (RFLX_Types.To_Length (RFLX_Types.Bit_Length (Struct.Length) * 8) + 1) - 2));
    end To_Context;
 
-end RFLX.Fixed_Size.Simple_Message;
+end RFLX.Test.Definite_Message;