Fix state machine contracts for external IO buffers

Ref. eng/recordflux/RecordFlux#1704
AdaCore · Aug 12, 2024 · f4962f1 · f4962f1
1 parent 2e05a56
commit f4962f1
Show file tree

Hide file tree

Showing 29 changed files with 179 additions and 58 deletions.
diff --git a/rflx/generator/allocator.py b/rflx/generator/allocator.py
@@ -71,12 +71,14 @@ def __init__(self, session: ir.Session, integration: Integration, prefix: str =
         self._unit_part = UnitPart()
         self._integration = integration
 
+        self._external_io_buffers = (
+            common.external_io_buffers(session)
+            if integration.use_external_io_buffers(session.identifier)
+            else []
+        )
+
         global_slots, self._externally_managed_buffers = self._allocate_global_slots(
-            (
-                common.external_io_buffers(session)
-                if integration.use_external_io_buffers(session.identifier)
-                else []
-            ),
+            self._external_io_buffers,
         )
         local_slots: list[SlotInfo] = self._allocate_local_slots()
         numbered_slots: list[NumberedSlotInfo] = []

diff --git a/rflx/generator/session.py b/rflx/generator/session.py
@@ -621,8 +621,13 @@ def is_global(identifier: ID) -> bool:
             self._external_io_buffers,
             is_global,
         )
+        unit += self._create_buffers_initialized_function(
+            composite_globals,
+            self._external_io_buffers,
+            is_global,
+        )
         unit += self._create_global_allocated_function()
-        unit += self._create_initialized_function(composite_globals)
+        unit += self._create_initialized_function(composite_globals, self._external_io_buffers)
         unit += self._create_states(self._session, composite_globals, is_global)
         unit += self._create_active_function(self._session)
         unit += self._create_initialize_procedure(
@@ -660,10 +665,12 @@ def is_global(identifier: ID) -> bool:
             unit += self._create_has_buffer_function(self._external_io_buffers)
             unit += self._create_written_last_function(self._external_io_buffers)
             unit += self._create_add_buffer_procedure(
+                composite_globals,
                 self._external_io_buffers,
                 self.unit_identifier,
             )
             unit += self._create_remove_buffer_procedure(
+                composite_globals,
                 self._external_io_buffers,
                 self.unit_identifier,
             )
@@ -926,57 +933,111 @@ def _create_global_initialized_function(
 
         self._session_context.used_types.append(const.TYPES_INDEX)
 
+        composite_globals = [
+            v
+            for v in composite_globals
+            if all(b.identifier != v.identifier for b in external_io_buffers)
+        ]
+
         specification = FunctionSpecification(
             "Global_Initialized",
             "Boolean",
-            [Parameter(["Ctx"], "Context")],
+            [Parameter(["Ctx" if composite_globals else "Unused_Ctx"], "Context")],
         )
 
         return UnitPart(
+            [SubprogramDeclaration(specification)],
             private=[
                 ExpressionFunctionDeclaration(
                     specification,
                     AndThen(
                         *[
                             e
-                            for d in composite_globals
-                            for e in [
-                                Call(
-                                    d.type_.identifier * "Has_Buffer",
-                                    [Variable(context_id(d.identifier, is_global))],
-                                ),
-                                *(
-                                    [
-                                        Equal(
-                                            Variable(
-                                                context_id(d.identifier, is_global)
-                                                * "Buffer_First",
-                                            ),
-                                            First(const.TYPES_INDEX),
+                            for v in composite_globals
+                            for e in (
+                                [
+                                    Call(
+                                        v.type_.identifier * "Has_Buffer",
+                                        [Variable(context_id(v.identifier, is_global))],
+                                    ),
+                                    Equal(
+                                        Variable(
+                                            context_id(v.identifier, is_global) * "Buffer_First",
                                         ),
-                                        Equal(
-                                            Variable(
-                                                context_id(d.identifier, is_global) * "Buffer_Last",
-                                            ),
-                                            Add(
-                                                First(const.TYPES_INDEX),
-                                                Number(self._allocator.get_size(d.identifier) - 1),
-                                            ),
+                                        First(const.TYPES_INDEX),
+                                    ),
+                                    Equal(
+                                        Variable(
+                                            context_id(v.identifier, is_global) * "Buffer_Last",
                                         ),
-                                    ]
-                                    if all(
-                                        b.identifier != d.identifier for b in external_io_buffers
-                                    )
-                                    else []
-                                ),
-                            ]
+                                        Add(
+                                            First(const.TYPES_INDEX),
+                                            Number(self._allocator.get_size(v.identifier) - 1),
+                                        ),
+                                    ),
+                                ]
+                            )
+                        ],
+                    ),
+                ),
+            ],
+        )
+
+    def _call_global_initialized(self, composite_globals: Sequence[ir.VarDecl]) -> list[Expr]:
+        return [Call("Global_Initialized", [Variable("Ctx")])] if composite_globals else []
+
+    def _create_buffers_initialized_function(
+        self,
+        composite_globals: Sequence[ir.VarDecl],
+        external_io_buffers: Sequence[common.Message],
+        is_global: Callable[[ID], bool],
+    ) -> UnitPart:
+        if not external_io_buffers:
+            return UnitPart()
+
+        self._session_context.used_types.append(const.TYPES_INDEX)
+
+        specification = FunctionSpecification(
+            "Buffers_Initialized",
+            "Boolean",
+            [Parameter(["Ctx"], "Context")],
+        )
+
+        return UnitPart(
+            [SubprogramDeclaration(specification)],
+            private=[
+                ExpressionFunctionDeclaration(
+                    specification,
+                    AndThen(
+                        *[
+                            e
+                            for v in composite_globals
+                            if any(b.identifier == v.identifier for b in external_io_buffers)
+                            for e in (
+                                [
+                                    Call(
+                                        v.type_.identifier * "Has_Buffer",
+                                        [Variable(context_id(v.identifier, is_global))],
+                                    ),
+                                ]
+                            )
                         ],
                     ),
                 ),
             ],
         )
 
-    def _create_initialized_function(self, composite_globals: Sequence[ir.VarDecl]) -> UnitPart:
+    def _call_buffers_initialized(
+        self,
+        external_io_buffers: Sequence[common.Message],
+    ) -> list[Expr]:
+        return [Call("Buffers_Initialized", [Variable("Ctx")])] if external_io_buffers else []
+
+    def _create_initialized_function(
+        self,
+        composite_globals: Sequence[ir.VarDecl],
+        external_io_buffers: Sequence[common.Message],
+    ) -> UnitPart:
         specification = FunctionSpecification(
             "Initialized",
             "Boolean",
@@ -996,17 +1057,9 @@ def _create_initialized_function(self, composite_globals: Sequence[ir.VarDecl])
                     specification,
                     AndThen(
                         *[
-                            *(
-                                [
-                                    Call(
-                                        ID("Global_Initialized"),
-                                        [Variable("Ctx")],
-                                    ),
-                                ]
-                                if composite_globals
-                                else []
-                            ),
+                            *self._call_global_initialized(composite_globals),
                             *self._call_global_allocated(),
+                            *self._call_buffers_initialized(external_io_buffers),
                         ],
                     ),
                 ),
@@ -1055,11 +1108,7 @@ def _create_states(
                     type_identifier = self._ada_type(d.type_.identifier)
                     invariant.extend(
                         [
-                            *(
-                                [Call("Global_Initialized", [Variable("Ctx")])]
-                                if composite_globals
-                                else []
-                            ),
+                            *self._call_global_initialized(composite_globals),
                             Call(type_identifier * "Has_Buffer", [Variable(identifier)]),
                             Equal(
                                 Variable(identifier * "Buffer_First"),
@@ -1862,6 +1911,7 @@ def _create_written_last_function(external_io_buffers: Sequence[common.Message])
 
     def _create_add_buffer_procedure(
         self,
+        composite_globals: Sequence[ir.VarDecl],
         external_io_buffers: Sequence[common.Message],
         unit_id: ID,
     ) -> UnitPart:
@@ -1882,6 +1932,7 @@ def _create_add_buffer_procedure(
                     [
                         Precondition(
                             AndThen(
+                                *self._call_global_initialized(composite_globals),
                                 *self._call_global_allocated(),
                                 Call(
                                     "Buffer_Accessible",
@@ -1921,6 +1972,7 @@ def _create_add_buffer_procedure(
                         ),
                         Postcondition(
                             AndThen(
+                                *self._call_global_initialized(composite_globals),
                                 *self._call_global_allocated(),
                                 Call(
                                     "Buffer_Accessible",
@@ -1977,6 +2029,7 @@ def _create_add_buffer_procedure(
 
     def _create_remove_buffer_procedure(
         self,
+        composite_globals: Sequence[ir.VarDecl],
         external_io_buffers: Sequence[common.Message],
         unit_id: ID,
     ) -> UnitPart:
@@ -1996,6 +2049,7 @@ def _create_remove_buffer_procedure(
                     [
                         Precondition(
                             And(
+                                *self._call_global_initialized(composite_globals),
                                 *self._call_global_allocated(),
                                 Call(
                                     "Buffer_Accessible",
@@ -2006,6 +2060,7 @@ def _create_remove_buffer_procedure(
                         ),
                         Postcondition(
                             AndThen(
+                                *self._call_global_initialized(composite_globals),
                                 *self._call_global_allocated(),
                                 Call(
                                     "Buffer_Accessible",

diff --git a/tests/data/generator/generated/external_io_buffers/rflx-p-s-fsm.ads b/tests/data/generator/generated/external_io_buffers/rflx-p-s-fsm.ads
@@ -45,6 +45,10 @@ is
 
    function Uninitialized (Ctx : Context) return Boolean;
 
+   function Global_Initialized (Unused_Ctx : Context) return Boolean;
+
+   function Buffers_Initialized (Ctx : Context) return Boolean;
+
    function Initialized (Ctx : Context) return Boolean;
 
    function Active (Ctx : Context) return Boolean;
@@ -108,7 +112,8 @@ is
 
    procedure Add_Buffer (Ctx : in out Context; Ext_Buf : External_Buffer; Buffer : in out RFLX_Types.Bytes_Ptr; Written_Last : RFLX_Types.Bit_Length) with
      Pre =>
-       Buffer_Accessible (Next_State (Ctx), Ext_Buf)
+       Global_Initialized (Ctx)
+       and then Buffer_Accessible (Next_State (Ctx), Ext_Buf)
        and then not Has_Buffer (Ctx, Ext_Buf)
        and then Buffer /= null
        and then Buffer'Length > 0
@@ -118,7 +123,8 @@ is
                      and Written_Last <= RFLX_Types.To_Last_Bit_Index (Buffer'Last)))
        and then Written_Last mod RFLX_Types.Byte'Size = 0,
      Post =>
-       Buffer_Accessible (Next_State (Ctx), Ext_Buf)
+       Global_Initialized (Ctx)
+       and then Buffer_Accessible (Next_State (Ctx), Ext_Buf)
        and then Has_Buffer (Ctx, Ext_Buf)
        and then Buffer = null
        and then (if
@@ -131,10 +137,12 @@ is
 
    procedure Remove_Buffer (Ctx : in out Context; Ext_Buf : External_Buffer; Buffer : out RFLX_Types.Bytes_Ptr) with
      Pre =>
-       Buffer_Accessible (Next_State (Ctx), Ext_Buf)
+       Global_Initialized (Ctx)
+       and Buffer_Accessible (Next_State (Ctx), Ext_Buf)
        and Has_Buffer (Ctx, Ext_Buf),
      Post =>
-       Buffer_Accessible (Next_State (Ctx), Ext_Buf)
+       Global_Initialized (Ctx)
+       and then Buffer_Accessible (Next_State (Ctx), Ext_Buf)
        and then not Has_Buffer (Ctx, Ext_Buf)
        and then Buffer /= null
        and then Buffer'Length > 0
@@ -202,11 +210,15 @@ private
    function Uninitialized (Ctx : Context) return Boolean is
      (not TLV.Message.Has_Buffer (Ctx.P.M_Ctx));
 
-   function Global_Initialized (Ctx : Context) return Boolean is
+   function Global_Initialized (Unused_Ctx : Context) return Boolean is
+     (True);
+
+   function Buffers_Initialized (Ctx : Context) return Boolean is
      (TLV.Message.Has_Buffer (Ctx.P.M_Ctx));
 
    function Initialized (Ctx : Context) return Boolean is
-     (Global_Initialized (Ctx));
+     (Global_Initialized (Ctx)
+      and then Buffers_Initialized (Ctx));
 
    function Active (Ctx : Context) return Boolean is
      (Ctx.P.Next_State /= S_Final);

diff --git a/tests/feature/messages_with_implict_size/generated/rflx-test-session-fsm.ads b/tests/feature/messages_with_implict_size/generated/rflx-test-session-fsm.ads
@@ -40,6 +40,8 @@ is
 
    function Uninitialized (Ctx : Context) return Boolean;
 
+   function Global_Initialized (Ctx : Context) return Boolean;
+
    function Global_Allocated (Ctx : Context) return Boolean;
 
    function Initialized (Ctx : Context) return Boolean;

diff --git a/tests/feature/messages_with_single_opaque_field/generated/rflx-test-session-fsm.ads b/tests/feature/messages_with_single_opaque_field/generated/rflx-test-session-fsm.ads
@@ -39,6 +39,8 @@ is
 
    function Uninitialized (Ctx : Context) return Boolean;
 
+   function Global_Initialized (Ctx : Context) return Boolean;
+
    function Global_Allocated (Ctx : Context) return Boolean;
 
    function Initialized (Ctx : Context) return Boolean;

diff --git a/tests/feature/parameterized_messages/generated/rflx-test-session-fsm.ads b/tests/feature/parameterized_messages/generated/rflx-test-session-fsm.ads
@@ -39,6 +39,8 @@ is
 
    function Uninitialized (Ctx : Context) return Boolean;
 
+   function Global_Initialized (Ctx : Context) return Boolean;
+
    function Global_Allocated (Ctx : Context) return Boolean;
 
    function Initialized (Ctx : Context) return Boolean;

diff --git a/tests/feature/session_append_unconstrained/generated/rflx-test-session-fsm.ads b/tests/feature/session_append_unconstrained/generated/rflx-test-session-fsm.ads
@@ -40,6 +40,8 @@ is
 
    function Uninitialized (Ctx : Context) return Boolean;
 
+   function Global_Initialized (Ctx : Context) return Boolean;
+
    function Global_Allocated (Ctx : Context) return Boolean;
 
    function Initialized (Ctx : Context) return Boolean;

diff --git a/tests/feature/session_case_expression_aggregate/generated/rflx-test-session-fsm.ads b/tests/feature/session_case_expression_aggregate/generated/rflx-test-session-fsm.ads
@@ -40,6 +40,8 @@ is
 
    function Uninitialized (Ctx : Context) return Boolean;
 
+   function Global_Initialized (Ctx : Context) return Boolean;
+
    function Global_Allocated (Ctx : Context) return Boolean;
 
    function Initialized (Ctx : Context) return Boolean;

diff --git a/tests/feature/session_case_expression_numeric/generated/rflx-test-session-fsm.ads b/tests/feature/session_case_expression_numeric/generated/rflx-test-session-fsm.ads
@@ -39,6 +39,8 @@ is
 
    function Uninitialized (Ctx : Context) return Boolean;
 
+   function Global_Initialized (Ctx : Context) return Boolean;
+
    function Global_Allocated (Ctx : Context) return Boolean;
 
    function Initialized (Ctx : Context) return Boolean;

diff --git a/tests/feature/session_channel_multiplexing/generated/rflx-test-session-fsm.ads b/tests/feature/session_channel_multiplexing/generated/rflx-test-session-fsm.ads
@@ -40,6 +40,8 @@ is
 
    function Uninitialized (Ctx : Context) return Boolean;
 
+   function Global_Initialized (Ctx : Context) return Boolean;
+
    function Global_Allocated (Ctx : Context) return Boolean;
 
    function Initialized (Ctx : Context) return Boolean;